The CASE keyword

20 views
Skip to first unread message

Saswata Paul

unread,
Aug 19, 2019, 4:10:10 PM8/19/19
to tlaplus
Hi,

  In the example of hierarchical proofs in the TLAPS tutorial (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html), the two possible actions of Next are considered in the proof using the CASE keyword:

Next == \/ /\ x < y /\ y' = y - x /\ x' = x \/ /\ y < x /\ x' = x-y /\ y' = y

 THEOREM NextProperty == InductiveInvariant /\ Next => InductiveInvariant'
<1> SUFFICES ASSUME InductiveInvariant, Next PROVE InductiveInvariant' <1> USE DEF InductiveInvariant, Next <1>1 (x < y) \/ (y < x) <1>a CASE x < y <1>b CASE y < x <1>2 QED BY <1>1, <1>a, <1>b

It is quite intuitive because this can be read as "the two separate cases that can occur in the next step.".

However, in the proof for Paxos (https://github.com/tlaplus/v1-tlapm/blob/master/examples/paxos/Paxos.tla), in the proof of the intermediate Lemma SafeAtStable, the different cases that can happen in the next state are expressed by using ASSUME keyword:

Next == \/ \E b \in Ballots : Phase1a(b) \/ Phase2a(b)
\/ \E a \in Acceptors : Phase1b(a) \/ Phase2b(a)

LEMMA SafeAtStable == Inv /\ Next /\ TypeOK' =>
\A v \in Values, b \in Ballots:
SafeAt(v, b) => SafeAt(v, b)'
<1> SUFFICES ASSUME Inv, Next, TypeOK',
NEW v \in Values, NEW b \in Ballots, SafeAt(v, b)
PROVE SafeAt(v, b)'
OBVIOUS
<1> USE DEF Send, Inv, Ballots
<1> USE TRUE /\ TRUE
<1>1. ASSUME NEW bb \in Ballots, Phase1a(bb)
PROVE SafeAt(v, b)'
BY <1>1, SMT DEF SafeAt, Phase1a, VotedForIn, WontVoteIn
<1>2. ASSUME NEW a \in Acceptors, Phase1b(a)
PROVE SafeAt(v, b)'
BY <1>2, QuorumAssumption, SMTT(60) DEF TypeOK, SafeAt, WontVoteIn, VotedForIn, Phase1b
<1>3. ASSUME NEW bb \in Ballots, Phase2a(bb)
PROVE SafeAt(v, b)'
BY <1>3, QuorumAssumption, SMT DEF TypeOK, SafeAt, WontVoteIn, VotedForIn, Phase2a
<1>4. ASSUME NEW a \in Acceptors, Phase2b(a)
PROVE SafeAt(v, b)'
<2>1. PICK m \in msgs : Phase2b(a)!(m)
BY <1>4 DEF Phase2b
<2>2 \A aa \in Acceptors, bb \in Ballots, vv \in Values :
VotedForIn(aa, vv, bb) => VotedForIn(aa, vv, bb)'
BY <2>1 DEF TypeOK, VotedForIn
<2>3. \A aa \in Acceptors, bb \in Ballots : maxBal[aa] > bb => maxBal'[aa] > bb
BY <2>1 DEF TypeOK
<2>4. ASSUME NEW aa \in Acceptors, NEW bb \in Ballots,
WontVoteIn(aa, bb), NEW vv \in Values,
VotedForIn(aa, vv, bb)'
PROVE FALSE
<3> DEFINE mm == [type |-> "2b", val |-> vv, bal |-> bb, acc |-> aa]
<3>1. mm \notin msgs
BY <2>4 DEF WontVoteIn, VotedForIn
<3>2. mm \in msgs'
<4>1. PICK m1 \in msgs' :
/\ m1.type = "2b"
/\ m1.val = vv
/\ m1.bal = bb
/\ m1.acc = aa
BY <2>4 DEF VotedForIn
<4>. QED BY <4>1 DEF TypeOK, Messages \* proved by Zenon
<3>3. aa = a /\ m.bal = bb
BY <2>1, <3>1, <3>2 DEF TypeOK
<3>. QED
BY <2>1, <2>4, <3>3 DEF Phase2b, WontVoteIn, TypeOK
<2>5 \A aa \in Acceptors, bb \in Ballots : WontVoteIn(aa, bb) => WontVoteIn(aa, bb)'
BY <2>3, <2>4 DEF WontVoteIn
<2> QED
BY <2>2, <2>5, QuorumAssumption DEF SafeAt
My question is: Has the ASSUME construct been used in the proof of SafeAtStable because Next is a disjunction of two existential quantifiers? Or could this have been written using the CASE keyword somehow?


Thank you

Saksham Chand

unread,
Aug 19, 2019, 5:30:31 PM8/19/19
to tla...@googlegroups.com
ASSUME .. PROVE is independent of what Next is. This could have been written using CASE as well. However, look at <1>4:

<1>4. CASE \E a \in Acceptors: Phase2b(a)
is not the same as
<1>4. ASSUME NEW a \in Acceptors, Phase2b(a)  PROVE SafeAt(v, b)'

because ASSUME .. PROVE defines new constant a \in Acceptors which you can use in the proof (<2>1, <3>3).
If using CASE and wanting the witness a, you would have to write
<1>4. CASE \E a \in Acceptors: Phase2b(a) 
   <2>1. PICK a \in Acceptors: Phase2b(a) BY <1>4

But for <1>1,2,3 you could just write CASE and it should not be any different because for them,
we are not writing a further hierarchical proof. TLAPS is able to prove it using the BY DEF itself
and none of the statements in the BY clause use any of the newly defined constants.

Hope this helps,
Saksham

--
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/8ff72031-c37d-4fad-b2eb-e50f6ab32ac4%40googlegroups.com.

Saswata Paul

unread,
Aug 19, 2019, 10:15:06 PM8/19/19
to tla...@googlegroups.com
Thanks. This was helpful. 
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.

--
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/fLr1hhx1KIw/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO-_4VnGQ-KXf9DPZhvKhpabPQeCcsrCoP8OEa5TK0Ldwhg%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages