Merge remote-tracking branch 'origin/master' into checkCommand

boogie-org · Sep 25, 2024 · 5b8179e · 5b8179e
2 parents 8664d8a + 4af59b3
commit 5b8179e
Show file tree

Hide file tree

Showing 2 changed files with 66 additions and 66 deletions.
diff --git a/Test/civl/paxos/PaxosActions.bpl b/Test/civl/paxos/PaxosActions.bpl
@@ -20,6 +20,23 @@ asserts Round(r);
   call {:linear joinPermissions} create_asyncs(JoinPAs(r));
 }
 
+async atomic action {:layer 2} A_Join(r: Round, n: Node, {:linear_in} p: One Permission)
+modifies joinedNodes;
+{
+  assert Round(r);
+  assert p->val == JoinPerm(r, n);
+
+  assume
+    {:add_to_pool "Round", r, r-1}
+    {:add_to_pool "Node", n}
+    true;
+
+  if (*) {
+    assume (forall r': Round :: Round(r') && joinedNodes[r'][n] ==> r' < r);
+    joinedNodes[r][n] := true;
+  }
+}
+
 async atomic action {:layer 2} A_Propose(r: Round, {:linear_in} ps: Set Permission)
 creates A_Vote, A_Conclude;
 modifies voteInfo;
@@ -56,59 +73,42 @@ asserts voteInfo[r] is None;
   }
 }
 
-async atomic action {:layer 2} A_Conclude(r: Round, v: Value, {:linear_in} p: One Permission)
-modifies decision;
+async atomic action {:layer 2} A_Vote(r: Round, n: Node, v: Value, {:linear_in} p: One Permission)
+modifies joinedNodes, voteInfo;
 {
-  var {:pool "NodeSet"} q: NodeSet;
-
   assert Round(r);
-  assert p->val == ConcludePerm(r);
+  assert p->val == VotePerm(r, n);
   assert voteInfo[r] is Some;
   assert voteInfo[r]->t->value == v;
-
-  assume {:add_to_pool "Round", r} {:add_to_pool "NodeSet", q} true;
-
-  if (*) {
-    assume IsSubset(q, voteInfo[r]->t->ns) && IsQuorum(q);
-    decision[r] := Some(v);
-  }
-}
-
-async atomic action {:layer 2} A_Join(r: Round, n: Node, {:linear_in} p: One Permission)
-modifies joinedNodes;
-{
-  assert Round(r);
-  assert p->val == JoinPerm(r, n);
+  assert !voteInfo[r]->t->ns[n];
 
   assume
     {:add_to_pool "Round", r, r-1}
     {:add_to_pool "Node", n}
     true;
 
   if (*) {
-    assume (forall r': Round :: Round(r') && joinedNodes[r'][n] ==> r' < r);
+    assume (forall r': Round :: Round(r') && joinedNodes[r'][n] ==> r' <= r);
+    voteInfo[r] := Some(VoteInfo(v, voteInfo[r]->t->ns[n := true]));
     joinedNodes[r][n] := true;
   }
 }
 
-async atomic action {:layer 2} A_Vote(r: Round, n: Node, v: Value, {:linear_in} p: One Permission)
-modifies joinedNodes, voteInfo;
+async atomic action {:layer 2} A_Conclude(r: Round, v: Value, {:linear_in} p: One Permission)
+modifies decision;
 {
+  var {:pool "NodeSet"} q: NodeSet;
+
   assert Round(r);
-  assert p->val == VotePerm(r, n);
+  assert p->val == ConcludePerm(r);
   assert voteInfo[r] is Some;
   assert voteInfo[r]->t->value == v;
-  assert !voteInfo[r]->t->ns[n];
 
-  assume
-    {:add_to_pool "Round", r, r-1}
-    {:add_to_pool "Node", n}
-    true;
+  assume {:add_to_pool "Round", r} {:add_to_pool "NodeSet", q} true;
 
   if (*) {
-    assume (forall r': Round :: Round(r') && joinedNodes[r'][n] ==> r' <= r);
-    voteInfo[r] := Some(VoteInfo(v, voteInfo[r]->t->ns[n := true]));
-    joinedNodes[r][n] := true;
+    assume IsSubset(q, voteInfo[r]->t->ns) && IsQuorum(q);
+    decision[r] := Some(v);
   }
 }
 

diff --git a/Test/civl/paxos/PaxosImpl.bpl b/Test/civl/paxos/PaxosImpl.bpl
@@ -121,6 +121,24 @@ requires call YieldInvChannels();
   async call Propose(r, ps');
 }
 
+yield procedure {:layer 1}
+Join(r: Round, n: Node, {:layer 1}{:linear_in} p: One Permission)
+refines A_Join;
+requires {:layer 1} Round(r) && Node(n) && p->val == JoinPerm(r, n);
+requires call YieldInv();
+{
+  var doJoin: bool;
+  var lastVoteRound: Round;
+  var lastVoteValue: Value;
+
+  call doJoin, lastVoteRound, lastVoteValue := JoinUpdate(r, n);
+  if (doJoin) {
+    call SendJoinResponse(r, n, lastVoteRound, lastVoteValue);
+    call {:layer 1} permJoinChannel := SendJoinResponseIntro(JoinResponse(n, lastVoteRound, lastVoteValue), p, permJoinChannel);
+    call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]);
+  }
+}
+
 yield right procedure {:layer 1} ProposeHelper(r: Round) returns (maxRound: Round, maxValue: Value, {:layer 1} ns: NodeSet)
 modifies permJoinChannel, joinChannel;
 requires {:layer 1} Round(r);
@@ -201,6 +219,23 @@ requires call YieldInvChannels();
   call {:layer 1} voteInfo := Copy(voteInfo[r := Some(VoteInfo(maxValue, NoNodes()))]);
 }
 
+yield procedure {:layer 1}
+Vote(r: Round, n: Node, v: Value, {:layer 1}{:linear_in} p: One Permission)
+refines A_Vote;
+requires {:layer 1} Round(r) && Node(n) && p->val == VotePerm(r, n);
+requires call YieldInv();
+{
+  var doVote:bool;
+
+  call doVote := VoteUpdate(r, n, v);
+  if (doVote) {
+    call SendVoteResponse(r, n);
+    call {:layer 1} permVoteChannel := SendVoteResponseIntro(VoteResponse(n), p, permVoteChannel);
+    call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]);
+    call {:layer 1} voteInfo := Copy(voteInfo[r := Some(VoteInfo(voteInfo[r]->t->value, voteInfo[r]->t->ns[n := true]))]);
+  }
+}
+
 yield procedure {:layer 1}
 Conclude(r: Round, v: Value, {:layer 1}{:linear_in} p: One Permission)
 refines A_Conclude;
@@ -238,41 +273,6 @@ requires call YieldInvChannels();
   }
 }
 
-yield procedure {:layer 1}
-Join(r: Round, n: Node, {:layer 1}{:linear_in} p: One Permission)
-refines A_Join;
-requires {:layer 1} Round(r) && Node(n) && p->val == JoinPerm(r, n);
-requires call YieldInv();
-{
-  var doJoin: bool;
-  var lastVoteRound: Round;
-  var lastVoteValue: Value;
-
-  call doJoin, lastVoteRound, lastVoteValue := JoinUpdate(r, n);
-  if (doJoin) {
-    call SendJoinResponse(r, n, lastVoteRound, lastVoteValue);
-    call {:layer 1} permJoinChannel := SendJoinResponseIntro(JoinResponse(n, lastVoteRound, lastVoteValue), p, permJoinChannel);
-    call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]);
-  }
-}
-
-yield procedure {:layer 1}
-Vote(r: Round, n: Node, v: Value, {:layer 1}{:linear_in} p: One Permission)
-refines A_Vote;
-requires {:layer 1} Round(r) && Node(n) && p->val == VotePerm(r, n);
-requires call YieldInv();
-{
-  var doVote:bool;
-
-  call doVote := VoteUpdate(r, n, v);
-  if (doVote) {
-    call SendVoteResponse(r, n);
-    call {:layer 1} permVoteChannel := SendVoteResponseIntro(VoteResponse(n), p, permVoteChannel);
-    call {:layer 1} joinedNodes := Copy(joinedNodes[r := joinedNodes[r][n := true]]);
-    call {:layer 1} voteInfo := Copy(voteInfo[r := Some(VoteInfo(voteInfo[r]->t->value, voteInfo[r]->t->ns[n := true]))]);
-  }
-}
-
 ////////////////////////////////////////////////////////////////////////////////
 
 // Trusted lemmas for the proof of Propose and Conclude