Inductive Invariants and Counterexamples in TLAPS

[Willy Schultz]

Have there been any previous attempts to incorporate counterexample generation into TLAPS? For example, say we are trying to prove an inductive invariant, Ind. If it is not inductive, it is helpful to get a counterexample to induction i.e. some state that satisfies Ind but which can reach a state violating Ind via some protocol transition. Recently, I have been using the probabilistic method of checking inductive invariance described in [1], and it has seemed to work surprisingly well. Of course, it only works on finite protocol instances, but this is still very helpful when debugging an inductive invariant. 

I am curious about whether this could be done with TLAPS, though, since TLAPS can produce an SMT encoding of a TLA+ invariant and transition relation. In theory, it seems that the probabilistic method is solving something at least as hard as satisfiability, since it first needs to generate states that satisfy some arbitrary predicate, Ind. It takes a completely "dumb" approach, though, and just randomly samples states and checks to see if they satisfy Ind. I would think, though, that state of the art SMT solvers would be able to outperform the efficiency of this technique. So, it would seem TLAPS would be well suited to handle this problem, since it is able to generate an SMT encoding that can be handed to a solver. 

Presumably, Apalache [2] is another candidate for this task, since it also produces an SMT encoding that can be given to an SMT solver. Their OOPSLA '19 paper [3] claims that it can prove certain inductive invariants automatically, and that it can detect invariant violations quickly as well. I suppose it would be interesting to compare the performance of the probabilistic method for finding inductiveness violations with Apalache, and/or compare Apalache with TLAPS. I suppose the details of the SMT encoding can make a significant difference in performance here? Tools like Ivy [4] are supposed to be fast at inductive invariant checking because they restrict the input language in a rather spartan way. It would seem that TLA+ seems cannot utilize similar ideas due to its expressiveness.

In general, I would be interested to hear others' thoughts on this, if they worked on or considered these problems in the past.

[1] https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

[2] https://github.com/informalsystems/apalache

[3] https://forsyte.at/wp-content/uploads/kkt-oopsla19.pdf

[4] https://cs.stanford.edu/~padon/ivy.pdf

[Stephan Merz]

Thank you for the interesting question. We made a few experiments on counter-example generation for TLAPS a few years ago, and the results were quite disappointing. My conclusion at the time was that we would need to produce a different encoding for producing counter-examples than the one that we use for proving. Indeed, since the formulas that we produce do not fall within the decidable fragments that SMT solvers can handle – due to the heavy use of quantifiers that arise from set theory – the results that we get from SMT solvers are either UNSAT (indicating that the original proof obligation is valid) or timeout but almost never SAT (which would lead to a counter-example).

Other proof assistants provide tools for counter-example generation (e.g., nitpick and nunchaku in Isabelle) that are useful in practice, so I remain convinced that this could also be done for TLAPS, but we do not currently have the manpower to investigate this. If somebody is interested, I'd be happy to discuss this further.

And as you mention, Apalache is effective for checking inductive invariants or producing counter-examples to their inductiveness.

Regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/546a3817-a702-4930-bb51-1af83da9238en%40googlegroups.com.

[Igor Konnov]

Hi Willy,

> On 13.09.2021, at 00:55, Willy Schultz <will...@gmail.com> wrote:
>
> Presumably, Apalache [2] is another candidate for this task, since it also produces an SMT encoding that can be given to an SMT solver. Their OOPSLA '19 paper [3] claims that it can prove certain inductive invariants automatically, and that it can detect invariant violations quickly as well.

Apalache assumes that all constants have been fixed (or that they belong to a finite set that is captured with ConstInit [1]). So for fixed parameters, we can prove inductive invariants. For instance, we have checked safety of the Tendermint consensus by proving an inductive invariant [2]. It is true that invariant violations are often easier to find with Apalache. It basically expands all quantifiers in disjunctions and conjunctions, which is probably what model-based quantifier instantiation has to do anyways. For the same reason, proving inductive invariants with Apalache takes longer, as the solver cannot use the structure of the quantified formulas to easily show unsatisfiability.

We are planning to implement a quantified encoding, in addition to the current unquantified encoding. But to do so, we will have to restrict the fragment of TLA+. For instance, we don’t know what to do about Cardinality, if we use a quantified encoding. I will not be surprised, if that restricted fragment of TLA+ happens to be very similar to the language of Ivy.

> I suppose it would be interesting to compare the performance of the probabilistic method for finding inductiveness violations with Apalache, and/or compare Apalache with TLAPS.

Yes, that is interesting. It would be also interesting to compare inductiveness checking when using predefined bounds on the data structures. We have recently introduced the operator `Apalache!Gen` that tells the model checker to produce data structures of bounded sizes [3], similar to generators in property-based testing. Intuitively, this is another instance of the small model hypothesis.


[1] https://apalache.informal.systems/docs/apalache/parameters.html#constinit-predicate
[2] https://github.com/tendermint/spec/blob/master/spec/light-client/accountability/Synopsis.md
[3] https://apalache.informal.systems/docs/adr/006rfc-unit-testing.html#5-bounding-the-inputs


Cheers,
Igor

[Willy Schultz]

Thank you to both Stephan and Igor for the helpful replies. A few thoughts in response.

Apalache assumes that all constants have been fixed (or that they belong to a finite set that is captured with ConstInit [1]). So for fixed parameters, we can prove inductive invariants. For instance, we have checked safety of the Tendermint consensus by proving an inductive invariant [2]. It is true that invariant violations are often easier to find with Apalache. It basically expands all quantifiers in disjunctions and conjunctions, which is probably what model-based quantifier instantiation has to do anyways. For the same reason, proving inductive invariants with Apalache takes longer, as the solver cannot use the structure of the quantified formulas to easily show unsatisfiability.

 

 In general, if we work over only finite domains, can't all SMT problems, in theory, be reduced to plain (i.e. boolean) SAT? Not suggesting this is necessarily more efficient than using some finite encoding with an SMT solver, but I just want to clarify the theoretical hardness of the problem.

Yes, that is interesting. It would be also interesting to compare inductiveness checking when using predefined bounds on the data structures. We have recently introduced the operator `Apalache!Gen` that tells the model checker to produce data structures of bounded sizes [3], similar to generators in property-based testing. Intuitively, this is another instance of the small model hypothesis.

Yes, the "small model hypothesis" indeed seems to come into play here. It also seems to be exploited more concretely by recent tools like ic3po [1], which use Ivy as an input language but search for inductive invariants over finite domains, and then generalize them to the unbounded domain.

[1] https://link.springer.com/chapter/10.1007/978-3-030-76384-8_9

 

[Igor Konnov]

> In general, if we work over only finite domains, can't all SMT problems, in theory, be reduced to plain (i.e. boolean) SAT? Not suggesting this is necessarily more efficient than using some finite encoding with an SMT solver, but I just want to clarify the theoretical hardness of the problem.

If we assume that we have no integers or use integers of fixed bit width, yes, everything could be reduced to SAT. Actually, we first tried uninterpreted functions to encode sets (basically having the membership relation as an uninterpreted function). That worked, but it was relatively slow, so we switched to the propositional encoding of set membership. However, that was in the early stages of the project. One needs a large set of experiments to draw conclusions about what is more efficient in practice.

The interesting thing about Apalache is that it supports unbounded integers as individual constants. So you are not allowed to reason about infinite subsets of Int or Nat, but you can have a bounded number of integers. This is useful when you have to reason about clocks, smart contracts, etc. In theory, we could encode fix-width integers in SAT with bit-blasting, but as far as I know, tuning these SAT encodings is quite hard in practice.


Regards,
Igor

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b70abf32-886d-4e45-b215-2b7cf74278a8n%40googlegroups.com.