diff --git a/hpaxos-tla/HMessage.tla b/hpaxos-tla/HMessage.tla index 8bcbbec..d1ef047 100644 --- a/hpaxos-tla/HMessage.tla +++ b/hpaxos-tla/HMessage.tla @@ -29,11 +29,11 @@ FINSUBSET(S, R) == { Range(seq) : seq \in [R -> S] } NoMessage == [ type |-> "null" ] MessageRec0 == - [ type : {"proposer"}, bal : Ballot, prev : {NoMessage}, refs : {{}} ] + [ type : {"1a"}, bal : Ballot, prev : {NoMessage}, refs : {{}} ] MessageRec1(M, n) == M \cup - [ type : {"acceptor"}, + [ type : {"1b", "2a", "2b"}, acc : Acceptor, prev : M \cup {NoMessage}, refs : FINSUBSET(M, RefCardinality), @@ -55,18 +55,15 @@ Message == UNION { MessageRec[n] : n \in MessageDepthRange } ----------------------------------------------------------------------------- (* Message types *) -Proposal(m) == m.type = "proposer" -NonProposal(m) == m.type = "acceptor" +Proposal(m) == m.type = "1a" -OneA(m) == m.type = "proposer" +OneA(m) == m.type = "1a" -OneB(m) == - /\ m.type = "acceptor" - /\ \E r \in m.refs : OneA(r) +OneB(m) == m.type = "1b" -TwoA(m) == - /\ m.type = "acceptor" - /\ \A r \in m.refs : ~OneA(r) +TwoA(m) == m.type = "2a" + +TwoB(m) == m.type = "2b" ----------------------------------------------------------------------------- (* Transitive references *) @@ -106,5 +103,5 @@ PrevTran(m) == UNION {PrevTranBound[n][m] : n \in PrevTranDepthRange} ============================================================================= \* Modification History -\* Last modified Fri Nov 22 20:52:10 CET 2024 by karbyshev +\* Last modified Tue Dec 17 17:59:35 CET 2024 by karbyshev \* Created Tue May 14 16:39:44 CEST 2024 by karbyshev diff --git a/hpaxos-tla/HMessage_proof.tla b/hpaxos-tla/HMessage_proof.tla index 610fb06..ae102d0 100644 --- a/hpaxos-tla/HMessage_proof.tla +++ b/hpaxos-tla/HMessage_proof.tla @@ -63,7 +63,7 @@ PROOF <1> DEFINE P(m) == MessageRec[m] # {} <1> SUFFICES ASSUME NEW j \in Nat PROVE P(j) OBVIOUS <1>0. P(0) - <2> [type |-> "proposer", bal |-> 0, prev |-> NoMessage, refs |-> {}] \in MessageRec[0] + <2> [type |-> "1a", bal |-> 0, prev |-> NoMessage, refs |-> {}] \in MessageRec[0] BY MessageRec_eq0 DEF MessageRec0, Ballot <2> QED OBVIOUS <1>1. ASSUME NEW m \in Nat, P(m) PROVE P(m+1) @@ -104,14 +104,14 @@ LEMMA Message_nontriv == Message # {} PROOF BY MessageRec_nontriv DEF Message, MessageDepthRange LEMMA Message_1a_ref == - \A m \in Message : m.type = "proposer" <=> m.refs = {} + \A m \in Message : OneA(m) <=> m.refs = {} PROOF -<1> DEFINE P(j) == \A mm \in MessageRec[j] : mm.type = "proposer" <=> mm.refs = {} -<1> SUFFICES ASSUME NEW j \in Nat PROVE P(j) BY DEF Message, MessageDepthRange +<1> DEFINE P(j) == \A mm \in MessageRec[j] : mm.type = "1a" <=> mm.refs = {} +<1> SUFFICES ASSUME NEW j \in Nat PROVE P(j) BY DEF Message, MessageDepthRange, OneA <1>0. P(0) BY MessageRec_eq0 DEF MessageRec0 <1>1. ASSUME NEW m \in Nat, P(m) PROVE P(m+1) <2> SUFFICES ASSUME NEW mm \in MessageRec[m+1] - PROVE mm.type = "proposer" <=> mm.refs = {} + PROVE mm.type = "1a" <=> mm.refs = {} BY DEF Message <2>3. QED BY <1>1, MessageRec_eq1, MessageRec_nontriv, FinSubset_sub_nontriv, RefCardinalitySpec DEF MessageRec1 @@ -194,11 +194,13 @@ PROOF LEMMA MessageSpec == ASSUME NEW m \in Message - PROVE \/ /\ m.type = "proposer" + PROVE \/ /\ m.type = "1a" /\ m.bal \in Ballot /\ m.prev = NoMessage /\ m.refs = {} - \/ /\ m.type = "acceptor" + \/ /\ \/ m.type = "1b" + \/ m.type = "2a" + \/ m.type = "2b" /\ m.acc \in Acceptor /\ m.prev \in Message \cup {NoMessage} /\ m.refs # {} @@ -207,11 +209,13 @@ LEMMA MessageSpec == PROOF <1> DEFINE P(n) == \A x \in MessageRec[n] : - \/ /\ x.type = "proposer" + \/ /\ x.type = "1a" /\ x.bal \in Ballot /\ x.prev = NoMessage /\ x.refs = {} - \/ /\ x.type = "acceptor" + \/ /\ \/ x.type = "1b" + \/ x.type = "2a" + \/ x.type = "2b" /\ x.acc \in Acceptor /\ x.prev \in Message \cup {NoMessage} /\ x.refs # {} @@ -221,11 +225,13 @@ PROOF <1>0. P(0) BY MessageRec_eq0 DEF MessageRec0 <1>1. ASSUME NEW k \in Nat, P(k) PROVE P(k + 1) <2> SUFFICES ASSUME NEW x \in MessageRec[k + 1] - PROVE \/ /\ x.type = "proposer" + PROVE \/ /\ x.type = "1a" /\ x.bal \in Ballot /\ x.prev = NoMessage /\ x.refs = {} - \/ /\ x.type = "acceptor" + \/ /\ \/ x.type = "1b" + \/ x.type = "2a" + \/ x.type = "2b" /\ x.acc \in Acceptor /\ x.prev \in Message \cup {NoMessage} /\ x.refs # {} @@ -234,13 +240,14 @@ PROOF OBVIOUS <2>1. CASE x \in MessageRec[k] BY <1>1, <2>1 - <2>3. CASE x \in [ type : {"acceptor"}, - lrns : SUBSET Learner, + <2>3. CASE x \in [ type : {"1b", "2a", "2b"}, acc : Acceptor, prev : MessageRec[k] \cup {NoMessage}, - refs : FINSUBSET(MessageRec[k], RefCardinality) ] - BY <2>3, Message_spec, MessageRec_nontriv, FinSubset_sub, - FinSubset_sub_nontriv, RefCardinalitySpec + refs : FINSUBSET(MessageRec[k], RefCardinality), + lrns : SUBSET Learner ] + BY <2>3, Message_spec, MessageRec_nontriv, + FinSubset_sub, FinSubset_sub_nontriv, + RefCardinalitySpec <2> QED BY <1>1, <2>1, <2>3, MessageRec_eq1 DEF MessageRec1 <1>2. HIDE DEF P <1>3. QED BY <1>0, <1>1, NatInduction, Isa @@ -250,13 +257,28 @@ LEMMA MessageTypeSpec == PROVE \/ /\ OneA(m) /\ ~OneB(m) /\ ~TwoA(m) + /\ ~TwoB(m) \/ /\ ~OneA(m) /\ OneB(m) /\ ~TwoA(m) + /\ ~TwoB(m) \/ /\ ~OneA(m) /\ ~OneB(m) /\ TwoA(m) -PROOF BY MessageSpec DEF OneA, OneB, TwoA + /\ ~TwoB(m) + \/ /\ ~OneA(m) + /\ ~OneB(m) + /\ ~TwoA(m) + /\ TwoB(m) +PROOF BY MessageSpec DEF OneA, OneB, TwoA, TwoB + +LEMMA MessageNonProposalSpec == + ASSUME NEW m \in Message, + ~Proposal(m) + PROVE \/ OneB(m) + \/ TwoA(m) + \/ TwoB(m) +PROOF BY MessageTypeSpec DEF Proposal, OneA ----------------------------------------------------------------------------- (* Transitive references *) @@ -756,5 +778,5 @@ PROOF BY Message_prev_PrevTranBound1, Zenon ============================================================================= \* Modification History -\* Last modified Mon Dec 09 16:10:10 CET 2024 by karbyshev +\* Last modified Tue Dec 17 19:23:14 CET 2024 by karbyshev \* Created Tue May 14 16:44:53 CEST 2024 by karbyshev diff --git a/hpaxos-tla/HPaxos_2.tla b/hpaxos-tla/HPaxos_2.tla index da63a64..5ee0556 100644 --- a/hpaxos-tla/HPaxos_2.tla +++ b/hpaxos-tla/HPaxos_2.tla @@ -4,6 +4,7 @@ EXTENDS HQuorum, HLearnerGraph, HMessage, TLAPS Assert(P, str) == P CONSTANT WellFormed2a(_) +CONSTANT WellFormed2b(_) ----------------------------------------------------------------------------- (* Algorithm specification *) @@ -44,9 +45,9 @@ CONSTANT WellFormed2a(_) \* which have equal previous messages (which may equal the NonMessage). CaughtMsg(x) == { m \in Tran(x) : - /\ m.type = "acceptor" + /\ ~Proposal(m) /\ \E m1 \in Tran(x) : - /\ m1.type = "acceptor" + /\ ~Proposal(m1) /\ m.acc = m1.acc /\ m # m1 /\ m.prev = m1.prev } @@ -62,13 +63,18 @@ CONSTANT WellFormed2a(_) { beta \in Learner : \E S \in ByzQuorum : ConByQuorum(alpha, beta, x, S) } + \* TODO rename + C(alpha, z) == \* alpha : Learner, z : 2a + \* previously: alpha \in z.lrns + z.lrns \cap Con(alpha, z) # {} + \* 2a-message is _buried_ if there exists another 2a-messages with \* a higher ballot number, a different value, and related to the \* given learner value. Buried(alpha, x, y) == \* x : 2a, y : 1b \E z \in Tran(y) : /\ TwoA(z) - /\ alpha \in z.lrns + /\ C(alpha, z) /\ \A bx, bz \in Ballot : B(x, bx) /\ B(z, bz) => bx < bz /\ \A vx, vz \in Value : @@ -88,20 +94,29 @@ CONSTANT WellFormed2a(_) \A m \in Con2as(alpha, x) : \A v \in Value : V(x, v) <=> V(m, v) \* Quorum of messages referenced by 2a for a learner instance - q(alpha, x) == \* x : 2a + q1b(alpha, x) == \* x : 2a LET Q == { m \in Tran(x) : /\ OneB(m) /\ Fresh(alpha, m) /\ \A b \in Ballot : B(m, b) <=> B(x, b) } IN { m.acc : m \in Q } + \* Quorum of 2a-messages referenced by the given 2b for a learner instance + q2a(alpha, x) == \* x : 2b + LET Q == { m \in Tran(x) : + /\ TwoA(m) + /\ alpha \in m.lrns + /\ \A b \in Ballot : B(m, b) <=> B(x, b) } + IN { m.acc : m \in Q } + ChainRef(m) == \/ m.prev = NoMessage - \/ m.prev \in m.refs /\ m.prev.acc = m.acc + \/ /\ m.prev \in m.refs + /\ m.prev.acc = m.acc WellFormed1b(m) == \A y \in Tran(m) : - m # y /\ SameBallot(m, y) => y.type = "proposer" + m # y /\ SameBallot(m, y) => Proposal(y) WellFormed(m) == /\ m \in Message @@ -109,28 +124,43 @@ CONSTANT WellFormed2a(_) /\ ChainRef(m) /\ OneB(m) => WellFormed1b(m) /\ TwoA(m) => + \* TODO check if this can be removed (most likely, is is not required for safety). + \* Implied by the condition m.lrns # {} /\ m.refs # {} \* Since the message structure embodies the learner values in our formalization, \* we must validate the correctness of these values. - /\ m.lrns = { l \in Learner : [lr |-> l, q |-> q(l, m)] \in TrustLive } + /\ m.lrns = { l \in Learner : [lr |-> l, q |-> q1b(l, m)] \in TrustLive } /\ WellFormed2a(m) + /\ TwoB(m) => + \* TODO check if this can be removed (most likely, it is not required for safety). + \* Implied by the condition m.lrns # {} + /\ m.refs # {} + \* Since the message structure embodies the learner values in our formalization, + \* we must validate the correctness of these values. + /\ m.lrns = { l \in Learner : [lr |-> l, q |-> q2a(l, m)] \in TrustLive } + /\ WellFormed2b(m) - Known2a(alpha, b, v) == + Known2b(alpha, b, v) == { x \in known_msgs[alpha] : - /\ TwoA(x) + /\ TwoB(x) /\ alpha \in x.lrns /\ B(x, b) /\ V(x, v) } ChosenIn(alpha, b, v) == - \E S \in SUBSET Known2a(alpha, b, v) : + \E S \in SUBSET Known2b(alpha, b, v) : [lr |-> alpha, q |-> { m.acc : m \in S }] \in TrustLive + + ReplyType(m, t) == + \/ OneA(m) /\ t = "1b" + \/ OneB(m) /\ t = "2a" + \/ TwoA(m) /\ t = "2b" } macro Send(m) { msgs := msgs \cup {m} } macro SendProposal(b) { - Send([type |-> "proposer", bal |-> b, prev |-> NoMessage, refs |-> {}]) + Send([type |-> "1a", bal |-> b, prev |-> NoMessage, refs |-> {}]) } macro Receive(m) { @@ -140,32 +170,40 @@ CONSTANT WellFormed2a(_) } macro Process(m) { - with (LL \in SUBSET Learner, - new = [type |-> "acceptor", - acc |-> self, + with (T \in {"1b", "2a", "2b"}, + LL \in SUBSET Learner, + new = [type |-> T, + acc |-> self, prev |-> prev_msg[self], refs |-> recent_msgs[self] \cup {m}, lrns |-> LL]) { assert new \in Message ; either { + when ReplyType(m, T); when WellFormed(new) ; prev_msg[self] := new ; recent_msgs[self] := {new} ; Send(new) } or { + when ReplyType(m, T); when ~WellFormed(new) ; when ~OneA(m) ; recent_msgs[self] := recent_msgs[self] \cup {m} } + or { + when TwoB(m) ; \* implies ~ReplyType(m, T) + recent_msgs[self] := recent_msgs[self] \cup {m} + } } } macro FakeSendControlMessage() { with (fin \in FINSUBSET(msgs, RefCardinality), LL \in SUBSET Learner, - msg = [type |-> "acceptor", acc |-> self, refs |-> fin, lrns |-> LL]) + T \in {"1b", "2a", "2b"}, + msg = [type |-> T, acc |-> self, refs |-> fin, lrns |-> LL]) { when WellFormed(msg) ; Send(msg) @@ -213,7 +251,7 @@ CONSTANT WellFormed2a(_) } ****************************************************************************) -\* BEGIN TRANSLATION (chksum(pcal) = "c07d66a2" /\ chksum(tla) = "dc25c029") +\* BEGIN TRANSLATION (chksum(pcal) = "b10276bc" /\ chksum(tla) = "5b536528") VARIABLES msgs, known_msgs, recent_msgs, prev_msg, decision, BVal (* define statement *) @@ -243,9 +281,9 @@ KnownRefs(a, m) == \A r \in m.refs : r \in known_msgs[a] CaughtMsg(x) == { m \in Tran(x) : - /\ m.type = "acceptor" + /\ ~Proposal(m) /\ \E m1 \in Tran(x) : - /\ m1.type = "acceptor" + /\ ~Proposal(m1) /\ m.acc = m1.acc /\ m # m1 /\ m.prev = m1.prev } @@ -262,12 +300,17 @@ Con(alpha, x) == \E S \in ByzQuorum : ConByQuorum(alpha, beta, x, S) } +C(alpha, z) == + + z.lrns \cap Con(alpha, z) # {} + + Buried(alpha, x, y) == \E z \in Tran(y) : /\ TwoA(z) - /\ alpha \in z.lrns + /\ C(alpha, z) /\ \A bx, bz \in Ballot : B(x, bx) /\ B(z, bz) => bx < bz /\ \A vx, vz \in Value : @@ -287,20 +330,29 @@ Fresh(alpha, x) == \A m \in Con2as(alpha, x) : \A v \in Value : V(x, v) <=> V(m, v) -q(alpha, x) == +q1b(alpha, x) == LET Q == { m \in Tran(x) : /\ OneB(m) /\ Fresh(alpha, m) /\ \A b \in Ballot : B(m, b) <=> B(x, b) } IN { m.acc : m \in Q } + +q2a(alpha, x) == + LET Q == { m \in Tran(x) : + /\ TwoA(m) + /\ alpha \in m.lrns + /\ \A b \in Ballot : B(m, b) <=> B(x, b) } + IN { m.acc : m \in Q } + ChainRef(m) == \/ m.prev = NoMessage - \/ m.prev \in m.refs /\ m.prev.acc = m.acc + \/ /\ m.prev \in m.refs + /\ m.prev.acc = m.acc WellFormed1b(m) == \A y \in Tran(m) : - m # y /\ SameBallot(m, y) => y.type = "proposer" + m # y /\ SameBallot(m, y) => Proposal(y) WellFormed(m) == /\ m \in Message @@ -308,23 +360,38 @@ WellFormed(m) == /\ ChainRef(m) /\ OneB(m) => WellFormed1b(m) /\ TwoA(m) => + + /\ m.refs # {} - /\ m.lrns = { l \in Learner : [lr |-> l, q |-> q(l, m)] \in TrustLive } + /\ m.lrns = { l \in Learner : [lr |-> l, q |-> q1b(l, m)] \in TrustLive } /\ WellFormed2a(m) + /\ TwoB(m) => + -Known2a(alpha, b, v) == + /\ m.refs # {} + + + /\ m.lrns = { l \in Learner : [lr |-> l, q |-> q2a(l, m)] \in TrustLive } + /\ WellFormed2b(m) + +Known2b(alpha, b, v) == { x \in known_msgs[alpha] : - /\ TwoA(x) + /\ TwoB(x) /\ alpha \in x.lrns /\ B(x, b) /\ V(x, v) } ChosenIn(alpha, b, v) == - \E S \in SUBSET Known2a(alpha, b, v) : + \E S \in SUBSET Known2b(alpha, b, v) : [lr |-> alpha, q |-> { m.acc : m \in S }] \in TrustLive +ReplyType(m, t) == + \/ OneA(m) /\ t = "1b" + \/ OneB(m) /\ t = "2a" + \/ TwoA(m) /\ t = "2b" + vars == << msgs, known_msgs, recent_msgs, prev_msg, decision, BVal >> @@ -339,7 +406,7 @@ Init == (* Global variables *) /\ BVal \in [Ballot -> Value] proposer(self) == /\ \E b \in Ballot: - msgs' = (msgs \cup {([type |-> "proposer", bal |-> b, prev |-> NoMessage, refs |-> {}])}) + msgs' = (msgs \cup {([type |-> "1a", bal |-> b, prev |-> NoMessage, refs |-> {}])}) /\ UNCHANGED << known_msgs, recent_msgs, prev_msg, decision, BVal >> @@ -348,22 +415,28 @@ safe_acceptor(self) == /\ \E m \in msgs: /\ KnownRefs(self, m) /\ known_msgs' = [known_msgs EXCEPT ![self] = known_msgs[self] \cup {m}] /\ WellFormed(m) - /\ \E LL \in SUBSET Learner: - LET new == [type |-> "acceptor", - acc |-> self, - prev |-> prev_msg[self], - refs |-> recent_msgs[self] \cup {m}, - lrns |-> LL] IN - /\ Assert(new \in Message, - "Failure of assertion at line 150, column 7 of macro called at line 196, column 9.") - /\ \/ /\ WellFormed(new) - /\ prev_msg' = [prev_msg EXCEPT ![self] = new] - /\ recent_msgs' = [recent_msgs EXCEPT ![self] = {new}] - /\ msgs' = (msgs \cup {new}) - \/ /\ ~WellFormed(new) - /\ ~OneA(m) - /\ recent_msgs' = [recent_msgs EXCEPT ![self] = recent_msgs[self] \cup {m}] - /\ UNCHANGED <> + /\ \E T \in {"1b", "2a", "2b"}: + \E LL \in SUBSET Learner: + LET new == [type |-> T, + acc |-> self, + prev |-> prev_msg[self], + refs |-> recent_msgs[self] \cup {m}, + lrns |-> LL] IN + /\ Assert(new \in Message, + "Failure of assertion at line 181, column 7 of macro called at line 234, column 9.") + /\ \/ /\ ReplyType(m, T) + /\ WellFormed(new) + /\ prev_msg' = [prev_msg EXCEPT ![self] = new] + /\ recent_msgs' = [recent_msgs EXCEPT ![self] = {new}] + /\ msgs' = (msgs \cup {new}) + \/ /\ ReplyType(m, T) + /\ ~WellFormed(new) + /\ ~OneA(m) + /\ recent_msgs' = [recent_msgs EXCEPT ![self] = recent_msgs[self] \cup {m}] + /\ UNCHANGED <> + \/ /\ TwoB(m) + /\ recent_msgs' = [recent_msgs EXCEPT ![self] = recent_msgs[self] \cup {m}] + /\ UNCHANGED <> /\ UNCHANGED << decision, BVal >> learner(self) == /\ \/ /\ \E m \in msgs: @@ -381,9 +454,10 @@ learner(self) == /\ \/ /\ \E m \in msgs: fake_acceptor(self) == /\ \E fin \in FINSUBSET(msgs, RefCardinality): \E LL \in SUBSET Learner: - LET msg == [type |-> "acceptor", acc |-> self, refs |-> fin, lrns |-> LL] IN - /\ WellFormed(msg) - /\ msgs' = (msgs \cup {msg}) + \E T \in {"1b", "2a", "2b"}: + LET msg == [type |-> T, acc |-> self, refs |-> fin, lrns |-> LL] IN + /\ WellFormed(msg) + /\ msgs' = (msgs \cup {msg}) /\ UNCHANGED << known_msgs, recent_msgs, prev_msg, decision, BVal >> @@ -405,7 +479,7 @@ Recv(a, m) == /\ known_msgs' = [known_msgs EXCEPT ![a] = known_msgs[a] \cup {m}] SendProposal(b) == - /\ Send([type |-> "proposer", bal |-> b, prev |-> NoMessage, refs |-> {}]) + /\ Send([type |-> "1a", bal |-> b, prev |-> NoMessage, refs |-> {}]) /\ UNCHANGED << known_msgs, recent_msgs, prev_msg >> /\ UNCHANGED decision /\ UNCHANGED BVal @@ -414,20 +488,26 @@ Process(a, m) == /\ Recv(a, m) /\ WellFormed(m) /\ \E LL \in SUBSET Learner : - LET new == [type |-> "acceptor", - acc |-> a, + \E T \in {"1b", "2a", "2b"} : + LET new == [type |-> T, + acc |-> a, prev |-> prev_msg[a], refs |-> recent_msgs[a] \cup {m}, lrns |-> LL] IN /\ new \in Message - /\ \/ /\ WellFormed(new) + /\ \/ /\ ReplyType(m, T) + /\ WellFormed(new) /\ prev_msg' = [prev_msg EXCEPT ![a] = new] /\ recent_msgs' = [recent_msgs EXCEPT ![a] = {new}] /\ Send(new) - \/ /\ ~WellFormed(new) + \/ /\ ReplyType(m, T) + /\ ~WellFormed(new) /\ ~OneA(m) /\ recent_msgs' = [recent_msgs EXCEPT ![a] = recent_msgs[a] \cup {m}] /\ UNCHANGED << msgs, prev_msg >> + \/ /\ TwoB(m) + /\ recent_msgs' = [recent_msgs EXCEPT ![a] = recent_msgs[a] \cup {m}] + /\ UNCHANGED << msgs, prev_msg >> /\ UNCHANGED decision /\ UNCHANGED BVal @@ -440,7 +520,8 @@ SafeAcceptorAction(a) == FakeSendControlMessage(a) == /\ \E fin \in FINSUBSET(msgs, RefCardinality) : \E LL \in SUBSET Learner : - LET new == [type |-> "acceptor", acc |-> a, refs |-> fin, lrns |-> LL] IN + \E T \in {"1b", "2a", "2b"} : + LET new == [type |-> T, acc |-> a, refs |-> fin, lrns |-> LL] IN /\ WellFormed(new) /\ Send(new) /\ UNCHANGED << known_msgs, recent_msgs, prev_msg >> @@ -534,5 +615,5 @@ UniqueDecision == ============================================================================= \* Modification History -\* Last modified Mon Nov 25 16:02:54 CET 2024 by karbyshev +\* Last modified Thu Dec 19 23:41:24 CET 2024 by karbyshev \* Created Mon Jun 19 12:24:03 CEST 2022 by karbyshev diff --git a/hpaxos-tla/HPaxos_2_proof.tla b/hpaxos-tla/HPaxos_2_proof.tla index eb9abde..2262acd 100644 --- a/hpaxos-tla/HPaxos_2_proof.tla +++ b/hpaxos-tla/HPaxos_2_proof.tla @@ -5,8 +5,16 @@ EXTENDS HPaxos_2, Sequences, HMessage_proof, HLearnerGraph_proof, TLAPS LEMMA CaughtMsgSpec == ASSUME NEW M \in Message PROVE /\ CaughtMsg(M) \in SUBSET Message - /\ \A X \in CaughtMsg(M) : X.type # "proposer" -BY Tran_Message DEF CaughtMsg + /\ \A X \in CaughtMsg(M) : ~Proposal(X) +BY Tran_Message DEF CaughtMsg, Proposal + +----------------------------------------------------------------------------- +LEMMA ReplyTypeSpec == + ASSUME NEW m \in Message, + NEW t \in {"1b", "2a", "2b"}, + ReplyType(m, t) + PROVE ~TwoB(m) +PROOF BY MessageTypeSpec DEF ReplyType, TwoB ----------------------------------------------------------------------------- (* Facts about Get1a, B and V relations *) @@ -234,41 +242,47 @@ PROOF <1>1. CASE \E p \in Proposer : ProposerAction(p) <2> PICK p \in Proposer, bal \in Ballot : SendProposal(bal) BY <1>1 DEF ProposerAction - <2> [type |-> "proposer", bal |-> bal, prev |-> NoMessage, refs |-> {}] \in Message + <2> [type |-> "1a", bal |-> bal, prev |-> NoMessage, refs |-> {}] \in Message BY Message_spec, MessageRec_eq0 DEF MessageRec0 <2> QED BY Zenon DEF SendProposal, Send, TypeOK <1>3. CASE \E a \in SafeAcceptor : \E m \in msgs : Process(a, m) - <2> PICK acc \in SafeAcceptor, m1b \in msgs : Process(acc, m1b) + <2> PICK acc \in SafeAcceptor, m \in msgs : Process(acc, m) BY <1>3 - <2> USE DEF Process <2> acc \in Acceptor BY DEF Acceptor - <2> m1b \in Message BY DEF TypeOK + <2> m \in Message BY DEF TypeOK <2> msgs' \in SUBSET Message BY WellFormedMessage, Zenon DEF Send, TypeOK <2> known_msgs' \in [Acceptor \cup Learner -> SUBSET Message] BY DEF Recv, TypeOK <2> recent_msgs' \in [Acceptor -> SUBSET Message] - <4> PICK ll \in SUBSET Learner : - LET new == [type |-> "acceptor", - acc |-> acc, + <4> PICK ll \in SUBSET Learner, + t \in {"1b", "2a", "2b"} : + LET new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], - refs |-> recent_msgs[acc] \cup {m1b}, + refs |-> recent_msgs[acc] \cup {m}, lrns |-> ll] IN /\ new \in Message - /\ \/ /\ WellFormed(new) + /\ \/ /\ ReplyType(m, t) + /\ WellFormed(new) /\ Send(new) /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = {new}] /\ prev_msg' = [prev_msg EXCEPT ![acc] = new] - \/ /\ ~WellFormed(new) - /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = recent_msgs[acc] \cup {m1b}] - BY Zenon - <4> DEFINE new == [type |-> "acceptor", - acc |-> acc, + \/ /\ ReplyType(m, t) + /\ ~WellFormed(new) + /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = recent_msgs[acc] \cup {m}] + \/ /\ TwoB(m) + /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = recent_msgs[acc] \cup {m}] + BY Zenon DEF Process + <4> DEFINE new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], - refs |-> recent_msgs[acc] \cup {m1b}, + refs |-> recent_msgs[acc] \cup {m}, lrns |-> ll] <4> new \in Message OBVIOUS + <4> recent_msgs[acc] \cup {m} \in SUBSET Message + BY DEF TypeOK <4> QED BY Isa DEF TypeOK <2> QED BY DEF TypeOK, Send <1>7. CASE \E l \in Learner : LearnerAction(l) @@ -311,7 +325,7 @@ PROOF LEMMA WellFormed_monotone == ASSUME NEW m \in Message, WellFormed(m), BVal' = BVal PROVE WellFormed(m)' -PROOF BY Isa DEF WellFormed, WellFormed1b, q, Fresh, Con2as, Buried, V +PROOF BY Isa DEF WellFormed, WellFormed1b, q1b, Fresh, Con2as, Buried, V LEMMA KnownMsgMonotone == TypeOK /\ NextTLA => @@ -342,18 +356,18 @@ PROOF <1>10. QED BY <1>1, <1>3, <1>7, <1>8, <1>9 DEF NextTLA, SafeAcceptorAction, LearnerAction -LEMMA Known2aMonotone == +LEMMA Known2bMonotone == TypeOK /\ NextTLA => \A L \in Learner, bal \in Ballot, val \in Value : - Known2a(L, bal, val) \subseteq Known2a(L, bal, val)' + Known2b(L, bal, val) \subseteq Known2b(L, bal, val)' PROOF <1> SUFFICES ASSUME TypeOK, NextTLA, NEW L \in Learner, NEW BB \in Ballot, NEW VV \in Value, - NEW S \in Known2a(L, BB, VV) - PROVE S \in Known2a(L, BB, VV)' + NEW S \in Known2b(L, BB, VV) + PROVE S \in Known2b(L, BB, VV)' OBVIOUS <1> TypeOK' BY TypeOKInvariant -<1> USE DEF Known2a +<1> USE DEF Known2b <1>1. CASE \E p \in Proposer : ProposerAction(p) <2> PICK bal \in Ballot : SendProposal(bal) BY <1>1 DEF ProposerAction @@ -395,21 +409,28 @@ PROOF <1>3. CASE \E a \in SafeAcceptor : \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, m \in msgs : Process(acc, m) BY <1>3 - <2> USE DEF Process <2> m \in Message BY DEF TypeOK - <2> PICK ll \in SUBSET Learner : - LET new == [type |-> "acceptor", - acc |-> acc, + <2> PICK ll \in SUBSET Learner, + t \in {"1b", "2a", "2b"} : + LET new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {m}, lrns |-> ll] IN - \/ /\ WellFormed(new) + \/ /\ ReplyType(m, t) + /\ WellFormed(new) + /\ Send(new) /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = {new}] - \/ /\ ~WellFormed(new) + \/ /\ ReplyType(m, t) + /\ ~WellFormed(new) /\ ~OneA(m) /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = recent_msgs[acc] \cup {m}] - BY Zenon DEF TypeOK - <2> QED BY DEF RecentMsgsSpec1, Recv, Send, SentBy, OneA, TypeOK + /\ UNCHANGED << msgs >> + \/ /\ TwoB(m) + /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = recent_msgs[acc] \cup {m}] + /\ UNCHANGED << msgs >> + BY Zenon DEF Process + <2> QED BY MessageTypeSpec DEF RecentMsgsSpec1, ReplyType, Recv, Send, SentBy, OneA, TypeOK <1>7. CASE \E lrn \in Learner : \E m \in msgs : LearnerRecv(lrn, m) <2> PICK lrn \in Learner, msg \in msgs : LearnerRecv(lrn, msg) BY <1>7 @@ -437,13 +458,13 @@ PROOF <1>1. CASE \E p \in Proposer : ProposerAction(p) <2> PICK bal \in Ballot : SendProposal(bal) BY <1>1 DEF ProposerAction - <2> QED BY Known2aMonotone DEF SendProposal + <2> QED BY Known2bMonotone DEF SendProposal <1>3. CASE \E a \in SafeAcceptor : \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, msg \in msgs : Process(acc, msg) BY <1>3 - <2> QED BY Known2aMonotone DEF Process + <2> QED BY Known2bMonotone DEF Process <1>7. CASE \E lrn \in Learner : \E m \in msgs : LearnerRecv(lrn, m) - BY <1>7, Known2aMonotone DEF LearnerRecv + BY <1>7, Known2bMonotone DEF LearnerRecv <1>8. CASE \E lrn \in Learner : \E bal \in Ballot : \E val \in Value : LearnerDecide(lrn, bal, val) <2> PICK lrn \in Learner, bal \in Ballot, val \in Value : @@ -451,9 +472,9 @@ PROOF /\ decision' = [decision EXCEPT ![<>] = decision[lrn, bal] \cup {val}] /\ UNCHANGED << msgs, known_msgs, recent_msgs, BVal >> BY <1>8, Zenon DEF LearnerDecide - <2>0. QED BY Known2aMonotone DEF TypeOK + <2>0. QED BY Known2bMonotone DEF TypeOK <1>9. CASE \E a \in FakeAcceptor : FakeAcceptorAction(a) - BY <1>9, Known2aMonotone DEF FakeAcceptorAction, FakeSendControlMessage + BY <1>9, Known2bMonotone DEF FakeAcceptorAction, FakeSendControlMessage <1>10. QED BY <1>1, <1>3, <1>7, <1>8, <1>9 DEF NextTLA, SafeAcceptorAction, LearnerAction @@ -479,29 +500,34 @@ PROOF <1>3. CASE \E a \in SafeAcceptor : \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, m \in msgs : Process(acc, m) BY <1>3 - <2> USE DEF Process - <2> PICK ll \in SUBSET Learner : - LET new == [type |-> "acceptor", + <2> m \in Message BY DEF TypeOK + <2> PICK ll \in SUBSET Learner, + t \in {"1b", "2a", "2b"} : + LET new == [type |-> t, acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {m}, lrns |-> ll] IN /\ new \in Message - /\ \/ /\ WellFormed(new) + /\ \/ /\ ReplyType(m, t) + /\ WellFormed(new) /\ Send(new) /\ prev_msg' = [prev_msg EXCEPT ![acc] = new] - \/ /\ ~WellFormed(new) + \/ /\ ReplyType(m, t) + /\ ~WellFormed(new) /\ ~OneA(m) /\ UNCHANGED << prev_msg, msgs >> - BY Zenon - <2> DEFINE new == [type |-> "acceptor", + \/ /\ TwoB(m) + /\ UNCHANGED << prev_msg, msgs >> + BY Zenon DEF Process + <2> DEFINE new == [type |-> t, acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {m}, lrns |-> ll] <2> new \in Message OBVIOUS - <2> CASE WellFormed(new) + <2> CASE WellFormed(new) /\ ~TwoB(m) <3> prev_msg' = [prev_msg EXCEPT ![acc] = new] BY Zenon <3> new \in msgs' @@ -513,6 +539,8 @@ PROOF <3> QED BY Zenon, NoMessageIsNotAMessage DEF SentBy, Send, OneA, TypeOK <2> CASE ~WellFormed(new) BY DEF SentBy + <2> CASE TwoB(m) + BY MessageTypeSpec, ReplyTypeSpec DEF SentBy <2> QED OBVIOUS <1>6. CASE \E l \in Learner : LearnerAction(l) BY <1>6 DEF LearnerAction, LearnerRecv, LearnerDecide, Send, SentBy @@ -555,32 +583,37 @@ PROOF \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, m \in msgs : Process(acc, m) BY <1>3 - <2> USE DEF Process - <2> PICK ll \in SUBSET Learner : - LET new == [type |-> "acceptor", - acc |-> acc, + <2> PICK ll \in SUBSET Learner, + t \in {"1b", "2a", "2b"} : + LET new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {m}, lrns |-> ll] IN /\ new \in Message - /\ \/ /\ WellFormed(new) + /\ \/ /\ ReplyType(m, t) + /\ WellFormed(new) /\ Send(new) /\ prev_msg' = [prev_msg EXCEPT ![acc] = new] /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = {new}] - \/ /\ ~WellFormed(new) + \/ /\ ReplyType(m, t) + /\ ~WellFormed(new) /\ ~OneA(m) /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = recent_msgs[acc] \cup {m}] /\ UNCHANGED << prev_msg, msgs >> - BY Zenon - <2> DEFINE new == [type |-> "acceptor", - acc |-> acc, + \/ /\ TwoB(m) + /\ recent_msgs' = [recent_msgs EXCEPT ![acc] = recent_msgs[acc] \cup {m}] + /\ UNCHANGED << prev_msg, msgs >> + BY Zenon DEF Process + <2> DEFINE new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {m}, lrns |-> ll] <2> new \in Message OBVIOUS <2> CASE acc = A - <3> CASE WellFormed(new) + <3> CASE WellFormed(new) /\ ~TwoB(m) <4> msgs' = msgs \cup {new} BY DEF Send, OneA <4> new # NoMessage @@ -600,7 +633,9 @@ PROOF <4> HIDE DEF new <4> QED BY PrevTran_trans, PrevTran_refl DEF SafeAcceptorPrevSpec1 <3> CASE ~WellFormed(new) - <4> QED BY DEF SentBy, TypeOK + BY DEF SentBy, TypeOK + <3> CASE TwoB(m) + BY MessageTypeSpec, ReplyTypeSpec DEF SentBy, TypeOK <3> QED OBVIOUS <2> CASE acc # A BY DEF SentBy, Send, TypeOK @@ -653,28 +688,20 @@ PROOF <1>3. CASE \E a \in SafeAcceptor : \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, m \in msgs : Process(acc, m) BY <1>3 - <2> USE DEF Process <2> known_msgs[AL]' \in SUBSET msgs' - <3> PICK ll \in SUBSET Learner : - LET new == [type |-> "acceptor", - acc |-> acc, - prev |-> prev_msg[acc], - refs |-> recent_msgs[acc] \cup {m}, - lrns |-> ll] IN - new \in Message - BY Zenon DEF TypeOK - <3> QED BY DEF Send, Recv + BY DEF Process, Send, Recv <2> KnownRefs(AL, M)' - BY DEF KnownRefs, Recv + BY DEF Process, KnownRefs, Recv <2> WellFormed(M)' - BY WellFormed_monotone DEF Recv, TypeOK + BY WellFormed_monotone DEF Process, Recv, TypeOK <2> Tran(M) \in SUBSET known_msgs[AL]' <3> CASE M \notin known_msgs[AL] + <4> USE DEF Process <4> M = m BY DEF Recv <4> AL = acc BY DEF Recv <4> M \in Message BY DEF WellFormed <4> QED BY Tran_eq, KnownMsgMonotone DEF Recv, KnownRefs - <3> QED BY DEF Recv + <3> QED BY DEF Process, Recv <2> \E b \in Ballot : B(M, b) BY DEF WellFormed <2> QED OBVIOUS @@ -747,33 +774,34 @@ PROOF <1> TypeOK' BY TypeOKInvariant <1> SUFFICES ASSUME NEW A \in SafeAcceptor, NEW m1 \in msgs, NEW m2 \in msgs' \ msgs, - m1.type # "proposer", m2.type # "proposer", + ~Proposal(m1), + ~Proposal(m2), m1.acc = A, m2.acc = A PROVE m1 \in PrevTran(m2) - <2> USE DEF MsgsSafeAcceptorPrevTranLinearSpec - <2> QED BY UniqueMessageSent, PrevTran_refl DEF SentBy, OneA, TypeOK + BY UniqueMessageSent, PrevTran_refl + DEF MsgsSafeAcceptorPrevTranLinearSpec, SentBy, Proposal, OneA, TypeOK <1> m1 \in SentBy(A) - BY DEF SentBy, OneA + BY DEF SentBy, Proposal, OneA <1> prev_msg[A] # NoMessage BY DEF SafeAcceptorPrevSpec1 <1>1. CASE \E p \in Proposer : ProposerAction(p) - BY <1>1 DEF ProposerAction, SendProposal, Send, OneA + BY <1>1 DEF ProposerAction, SendProposal, Send, Proposal, OneA <1>3. CASE \E a \in SafeAcceptor : \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, msg \in msgs : Process(acc, msg) BY <1>3 - <2> USE DEF Process - <2> PICK ll \in SUBSET Learner : - LET new2a == [type |-> "acceptor", - acc |-> acc, + <2> PICK ll \in SUBSET Learner, + t \in {"1b", "2a", "2b"} : + LET new2a == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {msg}, lrns |-> ll] IN /\ new2a \in Message /\ Send(new2a) /\ prev_msg' = [prev_msg EXCEPT ![acc] = new2a] - BY Zenon DEF TypeOK - <2> DEFINE new2a == [type |-> "acceptor", - acc |-> acc, + BY Zenon DEF Process, TypeOK + <2> DEFINE new2a == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {msg}, lrns |-> ll] @@ -815,35 +843,37 @@ PROOF <1> TypeOK' BY TypeOKInvariant <1> SUFFICES ASSUME NEW A \in SafeAcceptor, NEW m1 \in msgs, NEW m2 \in msgs' \ msgs, - m1.acc = A, m2.acc = A, - m1.type # "proposer", m2.type # "proposer", + m1.acc = A, + m2.acc = A, + ~Proposal(m1), + ~Proposal(m2), m1.prev = m2.prev - PROVE m1 = m2 - <2> USE DEF MsgsSafeAcceptorSpec3 - <2> QED BY UniqueMessageSent DEF SentBy, OneA, TypeOK + PROVE m1 = m2 + BY UniqueMessageSent + DEF MsgsSafeAcceptorSpec3, SentBy, OneA, Proposal, TypeOK <1> m1 \in Message BY DEF TypeOK <1> SentBy(A) # {} - BY DEF SentBy, Send, OneA, TypeOK + BY DEF SentBy, Send, Proposal, OneA, TypeOK <1> prev_msg[A] # NoMessage BY DEF SafeAcceptorPrevSpec1 <1>1. CASE \E p \in Proposer : ProposerAction(p) - BY <1>1 DEF ProposerAction, SendProposal, Send + BY <1>1 DEF ProposerAction, SendProposal, Proposal, Send <1>3. CASE \E a \in SafeAcceptor : \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, msg \in msgs : Process(acc, msg) BY <1>3 - <2> USE DEF Process - <2> PICK ll \in SUBSET Learner : - LET new == [type |-> "acceptor", - acc |-> acc, + <2> PICK ll \in SUBSET Learner, + t \in {"1b", "2a", "2b"} : + LET new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {msg}, lrns |-> ll] IN /\ Send(new) /\ prev_msg' = [prev_msg EXCEPT ![acc] = new] - BY Zenon DEF TypeOK - <2> DEFINE new == [type |-> "acceptor", - acc |-> acc, + BY Zenon DEF Process, TypeOK + <2> DEFINE new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {msg}, lrns |-> ll] @@ -854,11 +884,11 @@ PROOF <2> prev_msg[A] \in Message BY DEF TypeOK <2> prev_msg[A] \in m1.refs - BY DEF MsgsSafeAcceptorPrevRefSpec, SentBy, OneA + BY DEF MsgsSafeAcceptorPrevRefSpec, SentBy, Proposal, OneA <2> m1 \notin Tran(prev_msg[A]) BY Tran_ref_acyclic <2> m1 \in Tran(prev_msg[A]) - BY DEF SafeAcceptorPrevSpec2, MsgsSafeAcceptorPrevTranSpec, SentBy, OneA + BY DEF SafeAcceptorPrevSpec2, MsgsSafeAcceptorPrevTranSpec, SentBy, Proposal, OneA <2> QED OBVIOUS <1>6. CASE \E l \in Learner : LearnerAction(l) BY <1>6 DEF LearnerAction, LearnerRecv, LearnerDecide, Send @@ -886,10 +916,11 @@ PROOF <1> TypeOK' BY TypeOKInvariant <1> SUFFICES ASSUME NEW A \in SafeAcceptor, NEW mm \in msgs', mm \notin msgs, - mm.acc = A, mm.type # "proposer", + mm.acc = A, + ~Proposal(mm), mm.prev # NoMessage PROVE mm.prev \in mm.refs - BY DEF MsgsSafeAcceptorPrevRefSpec, SentBy, Send, OneA + BY DEF MsgsSafeAcceptorPrevRefSpec, SentBy, Send, Proposal, OneA <1> A \in Acceptor BY DEF Acceptor <1> USE DEF MsgsSafeAcceptorPrevRefSpec <1>1. CASE \E p \in Proposer : ProposerAction(p) @@ -900,18 +931,18 @@ PROOF \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, msg \in msgs : Process(acc, msg) BY <1>3 - <2> USE DEF Process - <2> PICK ll \in SUBSET Learner : - LET new == [type |-> "acceptor", - acc |-> acc, + <2> PICK ll \in SUBSET Learner, + t \in {"1b", "2a", "2b"} : + LET new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {msg}, lrns |-> ll] IN /\ Send(new) /\ prev_msg' = [prev_msg EXCEPT ![acc] = new] - BY Zenon DEF TypeOK - <2> DEFINE new == [type |-> "acceptor", - acc |-> acc, + BY Zenon DEF Process, TypeOK + <2> DEFINE new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {msg}, lrns |-> ll] @@ -941,10 +972,12 @@ PROOF <1> TypeOK' BY TypeOKInvariant <1> SUFFICES ASSUME NEW A \in SafeAcceptor, NEW m1 \in msgs' \ msgs, - m1.acc = A, m1.type # "proposer", + m1.acc = A, + ~Proposal(m1), NEW m2 \in PrevTran(m1), m2 # m1 PROVE m2 \in Tran(m1) - BY Tran_refl DEF MsgsSafeAcceptorPrevTranSpec, SentBy, Send, OneA, TypeOK + BY Tran_refl + DEF MsgsSafeAcceptorPrevTranSpec, SentBy, Send, Proposal, OneA, TypeOK <1> m1 \in Message BY DEF TypeOK <1> A \in Acceptor BY DEF Acceptor @@ -952,24 +985,24 @@ PROOF <1>1. CASE \E p \in Proposer : ProposerAction(p) <2> PICK p \in Proposer, bal \in Ballot : SendProposal(bal) BY <1>1 DEF ProposerAction - <2> QED BY DEF SendProposal, SentBy, Send + <2> QED BY DEF SendProposal, SentBy, Send, Proposal <1>3. CASE \E a \in SafeAcceptor : \E m \in msgs : Process(a, m) <2> PICK acc \in SafeAcceptor, msg \in msgs : Process(acc, msg) BY <1>3 - <2> USE DEF Process - <2> PICK ll \in SUBSET Learner : - LET new == [type |-> "acceptor", - acc |-> acc, + <2> PICK ll \in SUBSET Learner, + t \in {"1b", "2a", "2b"} : + LET new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {msg}, lrns |-> ll] IN /\ Send(new) /\ prev_msg' = [prev_msg EXCEPT ![acc] = new] - BY Zenon DEF TypeOK - <2> DEFINE new == [type |-> "acceptor", - acc |-> acc, + BY Zenon DEF Process, TypeOK + <2> DEFINE new == [type |-> t, + acc |-> acc, prev |-> prev_msg[acc], refs |-> recent_msgs[acc] \cup {msg}, lrns |-> ll] @@ -1000,7 +1033,7 @@ LEMMA MsgsSafeAcceptorSpecImpliesCaughtSpec == PROVE CaughtSpec PROOF BY MessageSpec DEF MsgsSafeAcceptorSpec3, CaughtSpec, Caught, CaughtMsg, - KnownMsgsSpec, SentBy, OneA, TypeOK + KnownMsgsSpec, SentBy, Proposal, OneA, TypeOK LEMMA QuorumIntersection == ASSUME TypeOK,