[Civl] allow variable hiding in action refinement (#831)

This PR makes it possible to hide variables in an action refinement
step. The main motivation at the moment is to have the description of
```A_Paxos'``` refer only to ```decision```.

Co-authored-by: Shaz Qadeer <[email protected]>

Source/Concurrency/InductiveSequentialization.cs

@@ -182,7 +182,6 @@ private Cmd Transform(Dictionary<CtorType, Implementation> eliminatedPendingAsyn
   public class InductiveSequentialization : Sequentialization
   {
     private Action invariantAction;
-    private HashSet<Variable> frame;
     private IdentifierExpr choice;
     private Dictionary<CtorType, Variable> newPAs;
 
@@ -193,7 +192,6 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target
       // - the modified set of each of each eliminated and abstract action associated with this invariant.
       // - the target and refined action of every application of inductive sequentialization that refers to this invariant.
       this.invariantAction = invariantAction;
-      frame = new HashSet<Variable>(invariantAction.ModifiedGlobalVars);
       choice = Expr.Ident(invariantAction.ImplWithChoice.OutParams.Last());
       newPAs = invariantAction.PendingAsyncs.ToDictionary(decl => decl.PendingAsyncType,
         decl => (Variable)civlTypeChecker.LocalVariable($"newPAs_{decl.Name}", decl.PendingAsyncMultisetType));
@@ -202,7 +200,7 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target
     private List<Declaration> GenerateBaseCaseChecker()
     {
       var requires = invariantAction.Gate.Select(g => new Requires(false, g.Expr)).ToList();
-      
+
       var subst = targetAction.GetSubstitution(invariantAction);
       var cmds = targetAction.GetGateAsserts(subst,
         $"Gate of {targetAction.Name} fails in IS base check against invariant {invariantAction.Name}").ToList<Cmd>();
@@ -215,7 +213,7 @@ private List<Declaration> GenerateBaseCaseChecker()
       outputVars.AddRange(targetAction.PendingAsyncs.Select(action =>
         invariantAction.Impl.OutParams[pendingAsyncTypeToOutputParamIndex[action.PendingAsyncType]]));
       cmds.Add(CmdHelper.CallCmd(targetAction.Impl.Proc, invariantAction.Impl.InParams, outputVars));
-      
+
       // Assign empty multiset to the rest
       var remainderPendingAsyncs = invariantAction.PendingAsyncs.Except(targetAction.PendingAsyncs);
       if (remainderPendingAsyncs.Any())
@@ -228,6 +226,7 @@ private List<Declaration> GenerateBaseCaseChecker()
         cmds.Add(CmdHelper.AssignCmd(lhss, rhss));
       }
 
+      var frame = new HashSet<Variable>(invariantAction.ModifiedGlobalVars);
       cmds.Add(GetCheck(targetAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame),
         $"IS base of {targetAction.Name} failed"));
 
@@ -246,6 +245,7 @@ private List<Declaration> GenerateConclusionChecker()
       cmds.Add(CmdHelper.CallCmd(invariantAction.Impl.Proc, invariantAction.Impl.InParams,
         invariantAction.Impl.OutParams));
       cmds.Add(CmdHelper.AssumeCmd(NoPendingAsyncs));
+      var frame = new HashSet<Variable>(refinedAction.ModifiedGlobalVars);
       cmds.Add(GetCheck(targetAction.tok, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame)),
         $"IS conclusion of {targetAction.Name} failed"));
 
@@ -300,6 +300,7 @@ private List<Declaration> GenerateStepChecker(Action pendingAsync)
         cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
       }
 
+      var frame = new HashSet<Variable>(invariantAction.ModifiedGlobalVars);
       cmds.Add(GetCheck(invariantAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame),
         $"IS step of {invariantAction.Name} with {abs.Name} failed"));
 
@@ -315,7 +316,7 @@ private List<Declaration> GenerateStepChecker(Action pendingAsync)
      * A key concept used in the generation of this extra assumption is the input-output transition relation of an action.
      * This relation is obtained by taking the conjunction of the gate and transition relation of the action and
      * existentially quantifying globals in the pre and the post state.
-     * 
+     *
      * There are two parts to the assumption, one for leftMover and the other for action.
      * Both parts are stated in the context of the input-output relation of the invariant action.
      * - The invocation of leftMover is identical to the choice made by the invariant.
@@ -427,7 +428,7 @@ private List<Declaration> GetCheckerTuple(string checkerName, List<Requires> req
         inParams,
         outParams,
         requires,
-        frame.Select(Expr.Ident).ToList(),
+        invariantAction.ModifiedGlobalVars.Select(Expr.Ident).ToList(),
         new List<Ensures>());
       var impl = DeclHelper.Implementation(
         proc,
@@ -457,7 +458,7 @@ private Expr ChoiceTest(CtorType pendingAsyncType)
     {
       return ExprHelper.IsConstructor(choice, invariantAction.ChoiceConstructor(pendingAsyncType).Name);
     }
-    
+
     private Expr NoPendingAsyncs
     {
       get
@@ -468,7 +469,7 @@ private Expr NoPendingAsyncs
         return expr;
       }
     }
-    
+
     private AssignCmd RemoveChoice(CtorType pendingAsyncType)
     {
       var rhs = Expr.Sub(Expr.Select(PAs(pendingAsyncType), Choice(pendingAsyncType)), Expr.Literal(1));

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

@@ -90,8 +90,8 @@ function {:inline} VotePAs(r: Round, v: Value) : [A_Vote]bool
 ////////////////////////////////////////////////////////////////////////////////
 //// Global variables
 // Abstract
-var {:layer 1,3} joinedNodes: [Round]NodeSet;
-var {:layer 1,3} voteInfo: [Round]Option VoteInfo;
+var {:layer 1,2} joinedNodes: [Round]NodeSet;
+var {:layer 1,2} voteInfo: [Round]Option VoteInfo;
 var {:layer 1,3} decision: [Round]Option Value; // spec
 
 // Concrete
@@ -106,9 +106,10 @@ var {:layer 1,1} {:linear "perm"} permVoteChannel: VoteResponseChannel;
 ////////////////////////////////////////////////////////////////////////////////
 
 function {:inline} Init (
-  rs: [Round]bool) : bool
+  rs: [Round]bool, decision: [Round]Option Value) : bool
 {
-  rs == (lambda r: Round :: true)
+  rs == (lambda r: Round :: true) &&
+  decision == (lambda r: Round :: None())
 }
 
 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);
+invariant Init(rs, decision);
 invariant InitLow(acceptorState, joinChannel, voteChannel, permJoinChannel, permVoteChannel);
 
 yield invariant {:layer 1} YieldInv();

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

@@ -4,22 +4,21 @@ refines A_Paxos' using INV;
 creates A_StartRound;
 {
   var {:pool "NumRounds"} numRounds: int;
-  assert Init(rs);
+  assert Init(rs, decision);
   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;
+modifies decision;
 {
-  assert Init(rs);
-  havoc joinedNodes, voteInfo, decision;
+  assert Init(rs, decision);
+  havoc decision;
   assume (forall r1: Round, r2: Round :: decision[r1] is Some && decision[r2] is Some ==> decision[r1] == decision[r2]);
 }
 
@@ -32,7 +31,7 @@ modifies joinedNodes, voteInfo, decision;
   var {:pool "Round"} k: int;
   var {:pool "Node"} m: Node;
 
-  assert Init(rs);
+  assert Init(rs, decision);
 
   havoc joinedNodes, voteInfo, decision;
 

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

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