[Civl] Fix initialization in Paxos (#802)

Test/civl/inductive-sequentialization/paxos/Paxos.bpl

@@ -92,12 +92,12 @@ function {:inline} VotePAs(r: Round, v: Value) : [A_Vote]bool
 // Abstract
 var {:layer 1,3} joinedNodes: [Round]NodeSet;
 var {:layer 1,3} voteInfo: [Round]Option VoteInfo;
+var {:layer 1,3} decision: [Round]Option Value; // spec
 
 // Concrete
 var {:layer 0,1} acceptorState: [Node]AcceptorState;
 var {:layer 0,1} joinChannel: [Round][JoinResponse]int;
 var {:layer 0,1} voteChannel: [Round][VoteResponse]int;
-var {:layer 0,3} decision: [Round]Option Value; // spec
 
 // Intermediate channel representation
 var {:layer 1,1} {:linear "perm"} permJoinChannel: JoinResponseChannel;
@@ -106,13 +106,9 @@ var {:layer 1,1} {:linear "perm"} permVoteChannel: VoteResponseChannel;
 ////////////////////////////////////////////////////////////////////////////////
 
 function {:inline} Init (
-  rs: [Round]bool, joinedNodes:[Round]NodeSet, voteInfo: [Round]Option VoteInfo,
-  decision:[Round]Option Value) : bool
+  rs: [Round]bool) : bool
 {
-  rs == (lambda r: Round :: true) &&
-  (forall r: Round :: joinedNodes[r] == NoNodes()) &&
-  (forall r: Round :: voteInfo[r] is None) &&
-  (forall r: Round :: decision[r] is None)
+  rs == (lambda r: Round :: true)
 }
 
 function {:inline} InitLow (

Test/civl/inductive-sequentialization/paxos/PaxosImpl.bpl

@@ -56,7 +56,7 @@ function InvChannels (joinChannel: [Round][JoinResponse]int, permJoinChannel: Jo
 }
 
 yield invariant {:layer 1} YieldInit({:linear "perm"} rs: [Round]bool);
-invariant Init(rs, joinedNodes, voteInfo, decision);
+invariant Init(rs);
 invariant InitLow(acceptorState, joinChannel, voteChannel, permJoinChannel, permVoteChannel);
 
 yield invariant {:layer 1} YieldInv();
@@ -77,6 +77,9 @@ requires call YieldInit(rs);
   var {:layer 1}{:linear "perm"} rs': [Round]bool;
   var {:layer 1}{:pending_async} PAs:[A_StartRound]int;
 
+  call InitJoinedNodes();
+  call InitVoteInfo();
+  call InitDecision();
   r := 0;
   rs' := rs;
   while (*)
@@ -193,7 +196,7 @@ requires call YieldInvChannels();
     n := n + 1;
   }
   async call Conclude(r, maxValue, cp);
-  call ProposeIntro(r, maxValue);
+  call SetVoteInfoInPropose(r, maxValue);
 }
 
 yield procedure {:layer 1}
@@ -247,7 +250,7 @@ requires call YieldInv();
   if (doJoin) {
     call SendJoinResponse(r, n, lastVoteRound, lastVoteValue);
     call SendJoinResponseIntro(r, n, lastVoteRound, lastVoteValue, p);
-    call JoinIntro(r, n);
+    call SetJoinedNodes(r, n);
   }
 }
 
@@ -263,31 +266,55 @@ requires call YieldInv();
   if (doVote) {
     call SendVoteResponse(r, n);
     call SendVoteResponseIntro(r, n, p);
-    call JoinIntro(r, n);
-    call VoteIntro(r, n);
+    call SetJoinedNodes(r, n);
+    call SetVoteInfoInVote(r, n);
   }
 }
 
 ////////////////////////////////////////////////////////////////////////////////
 
-action {:layer 1} JoinIntro(r: Round, n: Node)
+action {:layer 1} InitJoinedNodes()
+modifies joinedNodes;
+{
+  joinedNodes := (lambda r: Round:: NoNodes());
+}
+
+action {:layer 1} SetJoinedNodes(r: Round, n: Node)
 modifies joinedNodes;
 {
   joinedNodes[r][n] := true;
 }
 
-action {:layer 1} ProposeIntro(r: Round, v: Value)
+action {:layer 1} InitVoteInfo()
+modifies voteInfo;
+{
+  voteInfo := (lambda r: Round:: None());
+}
+
+action {:layer 1} SetVoteInfoInPropose(r: Round, v: Value)
 modifies voteInfo;
 {
   voteInfo[r] := Some(VoteInfo(v, NoNodes()));
 }
 
-action {:layer 1} VoteIntro(r: Round, n: Node)
+action {:layer 1} SetVoteInfoInVote(r: Round, n: Node)
 modifies voteInfo;
 {
   voteInfo[r] := Some(VoteInfo(voteInfo[r]->t->value, voteInfo[r]->t->ns[n := true]));
 }
 
+action {:layer 1} InitDecision()
+modifies decision;
+{
+  decision := (lambda r: Round :: None());
+}
+
+action {:layer 1} SetDecision(round: Round, value: Value)
+modifies decision;
+{
+  decision[round] := Some(value);
+}
+
 // Trusted lemmas for the proof of Propose and Conclude
 pure procedure AddToQuorum(q: NodeSet, n: Node) returns (q': NodeSet);
 requires !q[n];
@@ -303,12 +330,6 @@ ensures MaxRound(r, MapOr(ns1, ns2), voteInfo) ==
 
 ////////////////////////////////////////////////////////////////////////////////
 
-atomic action {:layer 1} A_SetDecision(round: Round, value: Value)
-modifies decision;
-{
-  decision[round] := Some(value);
-}
-
 atomic action {:layer 1} A_JoinUpdate(r: Round, n: Node)
 returns (join:bool, lastVoteRound: Round, lastVoteValue: Value)
 modifies acceptorState;
@@ -339,9 +360,6 @@ modifies acceptorState;
   }
 }
 
-yield procedure {:layer 0} SetDecision(round: Round, value: Value);
-refines A_SetDecision;
-
 yield procedure {:layer 0} JoinUpdate(r: Round, n: Node) returns (join:bool, lastVoteRound: Round, lastVoteValue: Value);
 refines A_JoinUpdate;
 

Test/civl/inductive-sequentialization/paxos/PaxosSeq.bpl

@@ -1,21 +1,24 @@
 atomic action {:layer 2} A_Paxos({:linear_in "perm"} rs: [Round]bool)
+modifies joinedNodes, voteInfo, decision;
 refines A_Paxos' using INV;
 creates A_StartRound;
 {
   var {:pool "NumRounds"} numRounds: int;
-  assert
-    Init(rs, joinedNodes, voteInfo, decision);
+  assert Init(rs);
   assume
     {:add_to_pool "Round", 0, numRounds}
     {:add_to_pool "NumRounds", numRounds}
     0 <= numRounds;
+  joinedNodes := (lambda r: Round:: NoNodes());
+  voteInfo := (lambda r: Round:: None());
+  decision := (lambda r: Round:: None());
   call create_asyncs((lambda pa: A_StartRound :: pa->r == pa->r_lin && Round(pa->r) && pa->r <= numRounds));
 }
 
 atomic action {:layer 3} A_Paxos'({:linear_in "perm"} rs: [Round]bool)
 modifies joinedNodes, voteInfo, decision;
 {
-  assert Init(rs, joinedNodes, voteInfo, decision);
+  assert Init(rs);
   havoc joinedNodes, voteInfo, decision;
   assume (forall r1: Round, r2: Round :: decision[r1] is Some && decision[r2] is Some ==> decision[r1] == decision[r2]);
 }
@@ -29,7 +32,7 @@ modifies joinedNodes, voteInfo, decision;
   var {:pool "Round"} k: int;
   var {:pool "Node"} m: Node;
 
-  assert Init(rs, joinedNodes, voteInfo, decision);
+  assert Init(rs);
 
   havoc joinedNodes, voteInfo, decision;
 

Test/civl/inductive-sequentialization/paxos/is.sh.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 69 verified, 0 errors
+Boogie program verifier finished with 72 verified, 0 errors