Proving eventualities with TLAPS (1.5.0)

[Ramon Snir]

Hi,

I am trying to overcome some property-checking limitations of TLC by learning TLAPS, specifically using the unreleased features regarding ENABLED and \cdot.

I am using TLAPM built from source from this commit: https://github.com/tlaplus/tlapm/tree/dc344b6d6e92332ba4a54f4cc86c577a9a137ecd (From the master branch, but not the latest commit)

I have experience with Coq and I think I understand the general idea of how to use TLAPS, up to the PTL/sl4 solver. I'm not sure what proof rules and axioms it has access to and most results I found online are 2+ years old so they focus on proving safety, without ENABLED usage.

For a concrete example, see this module which is inspired by https://github.com/tlaplus/tlapm/blob/dc344b6d6e92332ba4a54f4cc86c577a9a137ecd/examples/SimpleEventually.tla

--------------------------- MODULE RingEventually ---------------------------
EXTENDS TLAPS

VARIABLE x
Init == x = "red"
Next ==
  \/ (x = "red" /\ x' = "blue")
  \/ (x = "blue" /\ x' = "green")
  \/ (x = "green" /\ x' = "blue")

Spec == Init /\ [][Next]_x /\ WF_x(Next)

TypeOK == x \in {"red", "green", "blue"}

LEMMA TypeSafety == Spec => []TypeOK
PROOF
<1> USE DEF TypeOK
<1>1. Init => TypeOK
  BY DEF Init
<1>2. ASSUME TypeOK /\ [Next]_x
      PROVE TypeOK'
  BY <1>2 DEF Next
<1> QED
  BY <1>1, <1>2, PTL DEF Spec

LEMMA Spec => <>(x = "red")
PROOF BY PTL DEF Spec, Init

\* The QED step fails
THEOREM Spec => <>(x = "blue")
PROOF
<1>1. (Init /\ [][Next]_x) => []TypeOK
  <2>1. Init => TypeOK
    BY DEF Init, TypeOK
  <2>2. ASSUME TypeOK /\ [Next]_x
        PROVE TypeOK'
    BY <2>2 DEF TypeOK, Next
  <2> QED
    BY <2>1, <2>2, PTL
<1>2. ASSUME TypeOK /\ Init
      PROVE ENABLED <<Next>>_x
  BY <1>2, ExpandENABLED DEF Init, Next
<1>3. ASSUME Init /\ <<Next>>_x
      PROVE (x = "blue")'
  BY <1>3 DEF Init, Next
<1> QED \* failed
  BY <1>1, <1>2, <1>3, PTL DEF Spec, Init
 
(*

The proof state at the failing QED:

ASSUME NEW VARIABLE x,
       x = "red" /\ [][Next]_x => []TypeOK ,
       ASSUME TypeOK /\ x = "red" (* non-[] *)
       PROVE  ENABLED <<Next>>_x ,
       ASSUME x = "red" /\ <<Next>>_x (* non-[] *)
       PROVE  (x = "blue")' ,
       TRUE
PROVE  x = "red" /\ [][Next]_x /\ (WF_(x) (Next)) => <>(x = "blue")
*)

\* How should this proof be structured?
THEOREM Spec => <>(x = "green")
PROOF OMITTED

\* And my actual goal: how should _this_ proof be structured?
THEOREM Spec => []<>(x = "red")
PROOF OMITTED

=============================================================================

There are three theorems that I think are within reach for TLAPS but I don't know what PTL would need to prove them.

THEOREM Spec => <>(x = "blue") \* Witness: after one non-stuttering action, it will be blue

THEOREM Spec => <>(x = "green") \* Witness: after two non-stuttering actions, it will be green

THEOREM Spec => []<>(x = "red") \* Depending on the current state, the witness would be zero/one/two non-stuttering actions

Any hints on how I could approach these?

[Stephan Merz]

Hi Ramon,

thank you for your question and indeed, documentation for the more recent features of the prover is sorely lacking. The only examples using the ENABLED backends that I am aware of are

- module SimpleExampleWF in the examples_draft directory of the tlapm repository (https://github.com/tlaplus/tlapm/tree/main/examples_draft)

- the termination proof of the termination detection algorithm described in EWD998 at https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998_proof.tla (that proof uses some features beyond the elementary ExpandENABLED primitive)

In order to answer your question, the PTL backend is not based on axioms but on a decision procedure for propositional temporal logic. The details are described in our "coalescing" paper [1]. This has two fundamental consequences:

1. In first approximation, PTL does not handle sequents (ASSUME / PROOF constructs), except for constant-level assumptions [2]. I recommend only invoking it in such contexts. The "non-[]" warnings that you see in the proof output are an indication of this: they tell you that these ASSUME / PROOF steps should be rewritten as plain implications.

2. PTL only handles propositions and does not perform even trivial first-order reasoning. It will abstract atomic formulas such as `x = "red"' into a proposition, but sometimes it may be helpful to introduce propositional abstractions yourself, and it won't know that trivialities such as

x = "red" => ~(x = "blue")

holds. (I believe it doesn't even know that `x # "red"' is equivalent to `~(x = "red")'.)

Below is your proof rewritten with these caveats in mind, and an outline of your "main" theorem whose QED step is checked by PTL. Note in particular that it is really necessary in that proof to write

<1>1. Spec => []((x = "red") => <>(~(x = "red") /\ (x = "blue")))

due to observation (2) above, otherwise PTL won't know that the step from red to blue cannot just be a stuttering step. The missing proofs for steps <1>1 to <1>3 should be similar to the proof of your lemma that x will eventually be blue. (I'd actually recommend setting up the lemma in the way that it fits the steps required in the main proof so that you can use lemmas there.)

In the proof of your first real liveness theorem, besides rewriting ASSUME / PROOF to implications I also had to add the step

<1>4. Init /\ [Next]_x => Init' \/ (x = "blue")'

  BY DEF Init, Next

Without it, the conclusion wouldn't hold: weak fairness ensures that a <<Next>>_x transition will be taken only if it remains enabled, not if it just happens to be enabled at some point.

Besides, I made a few cosmetic changes to your proofs, in particular by reformulating the type-correctness lemma so that it can be used within the liveness proof.

I do hope this helps you to make progress: feel free to come back with further questions that will invariably arise.

Best,

Stephan

[1] https://members.loria.fr/SMerz/papers/arqnl2014.html

[2] More generally, all assumptions of lemmas should be "boxed" formulas, i.e., trivially equivalent to []F for some F.

--------------------------- MODULE RingEventually ---------------------------

EXTENDS TLAPS

VARIABLE x

Init == x = "red"

Next ==

  \/ (x = "red" /\ x' = "blue")

  \/ (x = "blue" /\ x' = "green")

  \/ (x = "green" /\ x' = "blue")

Spec == Init /\ [][Next]_x /\ WF_x(Next)

TypeOK == x \in {"red", "green", "blue"}

LEMMA TypeSafety == Init /\ [][Next]_x => []TypeOK

PROOF

<1> USE DEF TypeOK

<1>1. Init => TypeOK

  BY DEF Init

<1>2. ASSUME TypeOK /\ [Next]_x

      PROVE TypeOK'

  BY <1>2 DEF Next

<1> QED

  BY <1>1, <1>2, PTL DEF Spec

LEMMA EventuallyRed == Spec => <>(x = "red")

PROOF BY PTL DEF Spec, Init

THEOREM Spec => <>(x = "blue")

PROOF

<1>2. TypeOK /\ Init => ENABLED <<Next>>_x

  BY ExpandENABLED DEF Init, Next

<1>3. Init /\ <<Next>>_x => (x = "blue")'

  BY DEF Init, Next

<1>4. Init /\ [Next]_x => Init' \/ (x = "blue")'

  BY DEF Init, Next

<1> QED

  BY <1>2, <1>3, <1>4, TypeSafety, PTL DEF Spec

\* And my actual goal: how should _this_ proof be structured?

THEOREM Spec => []<>(x = "red")

<1>1. Spec => []((x = "red") => <>(~(x = "red") /\ (x = "blue")))

<1>2. Spec => []((x = "blue") => <>(~(x = "blue") /\ (x = "green")))

<1>3. Spec => []((x = "green") => <>(~(x = "green") /\ (x = "red")))

<1>. QED  BY <1>1, <1>2, <1>3, EventuallyRed, PTL

=============================================================================

--
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/0d5368ca-6221-404a-a144-362e874a1431n%40googlegroups.com.

[Ramon Snir]

Thank you, Stephan!

I followed your email and I managed to prove everything except for the final theorem. I started reading the "coalescing" paper. I can't say yet that I understand what the decision procedure would decide as valid, but I'm still working through it, so crossing my fingers and I'll write here afterward.

One question that I had so far:

I saw in EWD998 a reference to ENABLEDRules. I don't see it defined anywhere, and neither does my installed version of TLAPM. It says "Unknown operator ENABLEDRules".

<1>2. (ENABLED <<System>>_vars) <=> (ENABLED System)

  BY <1>1, ENABLEDrules

Is it coming from a side library? I'm not sure how to use it and I don't know when I would choose to use it versus ExpandENABLED.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/JNXR9DaJH2Q/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6883916B-8B2D-426C-90C9-E7AC3781E981%40gmail.com.

[Stephan Merz]

Hi Ramon,

not entirely sure what you mean when you say you proved everything except for the final theorem (whose QED proof was included in yesterday's message). For what it's worth, here is the proof of the first of the intermediate steps, the two others are similar:

LEMMA RedBlue == Spec => []((x = "red") => <>(~(x = "red") /\ (x = "blue")))

<1>1. x = "red" => ENABLED <<Next>>_x

  BY ExpandENABLED DEF Next

<1>2. x = "red" /\ [Next]_x => (x = "red")' \/ (~(x = "red") /\ (x = "blue"))'

  BY DEF Next

<1>3. x = "red" /\ <<Next>>_x => (~(x = "red") /\ (x = "blue"))'

  BY DEF Next

<1>. QED  BY <1>1, <1>2, <1>3, PTL DEF Spec

About validity checking for temporal logic, there used to be a number of online tools for LTL that could help you with that. A quick search brought up Owl [1], a tool that converts LTL formulas to different forms of automata. For example, you can paste the formula "!(G(a -> b) -> (G a -> G b))" into the input box (note that you need to negate the formula for validity checking) and generate an NBA (non-deterministic Büchi automaton). You'll see that the automaton is trivial and has no acceptance cycle (marked in green), which means that the formula is unsatisfiable, therefore the formula without the outermost negation is valid.

Concerning your question: the "updated_enabled_cdot" branch contains two more proof primitives for reasoning about ENABLED that have not yet made it into the main branch:

- ENABLEDrewrites applies simplification rules such as

ENABLED (A \/ B) <=> (ENABLED A) \/ (ENABLED B)

ENABLED (A /\ B) <=> (ENABLED A) /\ (ENABLED B)  if A and B do not share primed variables

ENABLED (x' = e) <=> TRUE  if e is a state function

with the purpose of simplifying an ENABLED expression before applying ExpandENABLED (which introduces existential quantification that may be difficult for the backends to prove).

- ENABLEDRules allows reasoning about monotonicity of ENABLED:

ASSUME A => B  PROVE (ENABLED A) => (ENABLED B)

ASSUME A <=> B  PROVE (ENABLED A) <=> (ENABLED B)

For example, this is useful to reduce ENABLED <<A>>_v to ENABLED A if A is an action that cannot stutter (as is often the case), since the latter is easier to reason about.

These additional primitives sometimes make proofs easier but they are not essential.

Stephan

[1] https://owl.model.in.tum.de

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAGNViOMZFg-7EEeH9xFMHGdoqiwVgXPq%3DkJ33d324Xm4T%2BGHHw%40mail.gmail.com.

[Ramon Snir]

Hi Stephan, thanks again!

I will re-build my version of TLAPM to include the updated_enabled_cdot branch, those two additions look useful.

As someone not familiar enough with LTL, Büchi automata, and how TLA translates into the "Spot" syntax, using the Owl tool did not click for me easily. But - it led me the right way. I found a similar tool to Owl on this website: https://spot.lre.epita.fr/app/

In the "Rewrite" tab, with "Simplify" checked, I can enter Spot/LTL expressions and see how they are simplified. If I understand correctly, when it's simplified to "1", the expression is valid and PTL in TLAPS will accept it.

Perhaps for future readers, here are some translations I figured out, all are simplified to "1".

Proving invariants in TLAPS usually looks like this:

PROPOSITION Init /\ [][Next]_x => []Inv

<1>. Init => Inv

<1>. Inv /\ [Next]_x => Inv'

<1> QED BY PTL

Which is this Spot/LTL expression, ignoring stuttering: (init -> inv) -> G(inv & next -> Xinv) -> (init & Gnext -> Ginv)

What I learned from this: In TLA, there is an implied "always" around the induction step, which must be explicit in Spot form. It actually makes sense and years ago confused me when learning TLA, so I've finally come full circle on this :)

Proving an eventuality based on a single step could look like this:

PROPOSITION Init /\ [][Next]_x /\ WF_x(Next) => <>(x = "done")

<1>. Init => ENABLED <<Next>>_x

<1>. Init /\ <<Next>>_x => (x = "done")'

<1>. Init /\ [Next]_x => Init' \/ (x = "done")'

<1>. QED BY PTL

Which is approximately this, ignoring stuttering: (init -> enabled) -> G(init & next -> Xdone) -> (init & Gnext & (FGenabled -> GFnext) -> Fdone)

This shows how to deal with weak fairness.

Including stuttering complicates the expression, but shows that it would still be accepted:

G(init -> enabled) ->

  G(init & next -> Xdone) ->

  G(init & (next | stutter) -> X(init | done)) ->

  (init & G(next | stutter) & (FGenabled -> GFnext) -> Fdone)

Adding stuttering makes it visible why each of the three steps before the QED is important.

Finally, I could convince myself why the proof you wrote for "RedBlue" is being accepted by PTL as sufficient. In skeleton form, it is:

PROPOSITION Init /\ [][Next]_x /\ WF_x(Next) => []((x = "start") => <>(~(x = "start") /\ (x = "done")))

<1>. x = "start" => ENABLED <<Next>>_x

<1>. x = "start" /\ [Next]_x => (x = "start")' \/ (~(x = "start") /\ (x = "done"))'

<1>. x = "start" /\ <<Next>>_x => (~(x = "start") /\ (x = "done"))'

<1>. QED BY PTL

Which is approximately this:

G(start -> enabled) ->

  G(start & (next | stutter) -> X(start | (!start & done))) ->

  G(start & next -> (!start & done)) ->

  (init & G(next | stutter) & (FGenabled -> GFnext) -> G(start -> F(!start & done)))

I will note that when I first read your proof I had no sense at all as to why PTL accepted it. Seeing it this way, with explicit "always"s, it makes complete sense.

Now that I can translate between the two forms, and verify correctness both manually and with a computer, I should be able to come up with my own proofs without copying from existing proofs!

P.S.: I went back to Owl, and entered (negated) some of the Spot expressions above, and didn't get automata without acceptance cycles. I'm probably misunderstanding something about how to use Owl, but I guess it doesn't matter as long as I have the other website which does seem to work. Doing the same negation trick with the other website does show an automaton with no acceptance cycle.

P.P.S.: I think this shows a gap in the tutorials for the future TLAPS 1.5.0. With TLAPS 1.4.5, things made sense assuming a good understanding of TLA+ and of proof systems (Coq/Isabelle), because for proofs that rely very little on temporal propositions, one can copy-paste a few proof rules and be independent. With many more capabilities unlocked, I was not able to use them without also understanding something new - what LTL formulae are valid or not. I'm not sure if this is something people care about, especially as this has been unreleased for 2+ years, but IMHO it's useful.

Finally - thanks again, Stephan! It helped me a lot.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6178623B-7D82-4711-854B-26091E6EF685%40gmail.com.

[Stephan Merz]

Thanks for the nice explanations, and indeed I should have pointed you to Spot right away. I believe I now understand that what bothered you is a fundamental reasoning principle in modal / temporal logics, namely what logicians call the necessitation rule

F |- []F

It asserts that if F is a valid formula (true in all interpretations of interest) then so is []F. Indeed, if sigma |= F holds for all sequences of states sigma, then also sigma[n ..] |= F holds for all n (i.e., F is true for all suffixes of sigma), since every suffix sigma[n..] is again a sequence of states, and so sigma |= []F holds.

However, quite obviously the implication F => []F is not valid, so in temporal reasoning you cannot equate implication and consequence, as we are used to from ordinary first-order logic. This is why Leslie keeps saying that temporal logic is evil.

In TLAPS, "|-" is written ASSUME ... PROVE ..., and we wanted it to be the ordinary consequence relation from first-order logic because that's where 95% of the reasoning is done. When we designed how to handle the temporal logic part of TLA+, we debated adding a separate "temporal consequence" relation that could have been written []ASSUME ... []PROVE ...

We decided that this would have been a complication that we didn't want to introduce. Instead, the PTL backend silently promotes every formula F that has been derived in a constant context (more generally, a context in which all assumptions are equivalent to formulas []G) to []F. The price to pay is that ASSUMEs with state- or action-level hypotheses are useless in contexts where temporal reasoning will be performed. However, you can freely use them in purely predicate-logic proof blocks. This explains the standard pattern in invariance proofs

<1>1. Init => Inv

<1>2. Inv /\ [Next]_v => Inv'    \* stated as an implication because the step will be used in temporal reasoning

  <2>. SUFFICES ASSUME Inv, [Next]_v PROVE Inv'   

          \* switch to ASSUME ... PROVE, since it is more useful for first-order reasoning

  <2>. QED

<1>. QED  BY <1>1, <1>2, PTL

By the way, if you are more comfortable with applying proof rules, Leslie's proof rules in the original TLA paper [1] are a good starting point. They are mostly propositional and will therefore be understood by the PTL decision procedure without needing to apply them explicitly.

Stephan

[1] http://lamport.azurewebsites.net/pubs/pubs.html#lamport-actions

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAGNViONzco7vTcTobuMdVY24dYjUojSx7qvDfPRb3ABX9Q5xiw%40mail.gmail.com.