Re: [tlaplus] The CASE keyword

[Saswata Paul <paulsaswata1@xxxxxxxxx>]

Thanks. This was helpful. 

On Monday, August 19, 2019, Saksham Chand <schand@xxxxxxxxxxxxxxxxx> wrote:

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

On Mon, Aug 19, 2019 at 4:10 PM Saswata Paul <paulsaswata1@xxxxxxxxx> wrote:

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

--
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8ff72031-c37d-4fad-b2eb-e50f6ab32ac4%40googlegroups.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.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHeFUE_BK8u7V7y72gNd-V_Bob%3D9xuDx28U0jPw3W8fNzXMDXw%40mail.gmail.com.