[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Saswata Paul <paulsaswata1@xxxxxxxxx>*Date*: Mon, 19 Aug 2019 22:15:03 -0400*References*: <8ff72031-c37d-4fad-b2eb-e50f6ab32ac4@googlegroups.com> <CAJSuO-_4VnGQ-KXf9DPZhvKhpabPQeCcsrCoP8OEa5TK0Ldwhg@mail.gmail.com>

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>4But 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 itselfand none of the statements in the BY clause use any of the newly defined constants.Hope this helps,SakshamOn 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/ ), the two possible actions of Next are considered in the proof using the CASE keyword:Documentation/Tutorial/ Hierarchical_proofs.html Next == \/ /\ x < y /\ y' = y - x /\ x' = x \/ /\ y < x /\ x' = x-y /\ y' = yTHEOREM 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>bIt 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/ ), in the proof of the intermediate Lemma SafeAtStable, the different cases that can happen in the next state are expressed by using ASSUME keyword:paxos/Paxos.tla

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- .KXf9DPZhvKhpabPQeCcsrCoP8OEa5T K0Ldwhg%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.

**References**:**[tlaplus] The CASE keyword***From:*Saswata Paul

**Re: [tlaplus] The CASE keyword***From:*Saksham Chand

- Prev by Date:
**Re: [tlaplus] Usage of the ! operator** - Next by Date:
**[tlaplus] Re: Help with a TLAPS proof for a refinement involving records (and a Proof Decomposition bug)** - Previous by thread:
**Re: [tlaplus] The CASE keyword** - Next by thread:
**[tlaplus] Record Equality** - Index(es):