[Civl] Add Cell type (#882)

This PR adds the Cell type to capture a singleton map. 
- Map_Pack and Map_Unpack are replaced with Cell_Pack and Cell_Unpack
respectively.
- The signatures of Map_Get and Map_Put are updated to use Cell.

Source/Concurrency/LinearDomainCollector.cs

@@ -150,6 +150,12 @@ private void RegisterType(Type type)
         var collector = program.monomorphizer.InstantiateFunction("Set_Collector", typeParamInstantiationMap);
         collectors[type][permissionType] = collector;
       }
+      else if (typeName == "Cell")
+      {
+        var typeParamInstantiationMap = new Dictionary<string, Type> { { "T", actualTypeParams[0] }, { "U", actualTypeParams[1] } };
+        var collector = program.monomorphizer.InstantiateFunction("Cell_Collector", typeParamInstantiationMap);
+        collectors[type][permissionType] = collector;
+      }
       else
       {
         Debug.Assert(typeName == "One");

Source/Concurrency/LinearRewriter.cs

@@ -59,10 +59,10 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
     switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
     {
       case "One_New":
+      case "Cell_Pack":
+      case "Cell_Unpack":
       case "Set_MakeEmpty":
       case "Map_MakeEmpty":
-      case "Map_Pack":
-      case "Map_Unpack":
       case "Map_Assume":
         return new List<Cmd>{callCmd};
       case "Set_Split":
@@ -153,6 +153,14 @@ private Function OneConstructor(Type type)
     return oneConstructor;
   }
 
+  private Function CellConstructor(Type keyType, Type valType)
+  {
+    var actualTypeParams = new List<Type>() { keyType, valType };
+    var cellTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Cell", actualTypeParams);
+    var cellConstructor = cellTypeCtorDecl.Constructors[0];
+    return cellConstructor;
+  }
+
   private Function SetConstructor(Type type)
   {
     var actualTypeParams = new List<Type>() { type };
@@ -161,6 +169,11 @@ private Function SetConstructor(Type type)
     return setConstructor;
   }
 
+  private static Expr Key(Expr path)
+  {
+    return ExprHelper.FieldAccess(path, "key");
+  }
+
   private static Expr Val(Expr path)
   {
     return ExprHelper.FieldAccess(path, "val");
@@ -299,8 +312,7 @@ private List<Cmd> RewriteMapGet(CallCmd callCmd)
     var cmdSeq = new List<Cmd>();
     var path = callCmd.Ins[0];
     var k = callCmd.Ins[1];
-    var l = callCmd.Outs[0];
-    var v = callCmd.Outs[1];
+    var c = callCmd.Outs[0];
 
     var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc);
     var domain = instantiation["K"];
@@ -309,9 +321,9 @@ private List<Cmd> RewriteMapGet(CallCmd callCmd)
     var mapRemoveFunc = MapRemove(domain, range);
     var mapAtFunc = MapAt(domain, range);
     cmdSeq.Add(AssertCmd(callCmd.tok, ExprHelper.FunctionCall(mapContainsFunc, path, k), "Map_Get failed"));
-    var oneConstructor = OneConstructor(domain);
-    cmdSeq.Add(CmdHelper.AssignCmd(l.Decl, ExprHelper.FunctionCall(oneConstructor, k)));
-    cmdSeq.Add(CmdHelper.AssignCmd(v.Decl, ExprHelper.FunctionCall(mapAtFunc, path, k)));
+    var cellConstructor = CellConstructor(domain, range);
+    cmdSeq.Add(
+      CmdHelper.AssignCmd(c.Decl, ExprHelper.FunctionCall(cellConstructor, k, ExprHelper.FunctionCall(mapAtFunc, path, k))));
     cmdSeq.Add(
       CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapRemoveFunc, path, k)));
 
@@ -323,18 +335,17 @@ private List<Cmd> RewriteMapPut(CallCmd callCmd)
   {
     var cmdSeq = new List<Cmd>();
     var path = callCmd.Ins[0];
-    var l = callCmd.Ins[1];
-    var v = callCmd.Ins[2];
+    var c = callCmd.Ins[1];
 
     var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc);
     var domain = instantiation["K"];
     var range = instantiation["V"];
     var mapContainsFunc = MapContains(domain, range);
     var mapUpdateFunc = MapUpdate(domain, range);
     var attribute = new QKeyValue(Token.NoToken, "linear", new List<object>(), null);
-    cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Not(ExprHelper.FunctionCall(mapContainsFunc, path, Val(l))), attribute));
+    cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Not(ExprHelper.FunctionCall(mapContainsFunc, path, Key(c))), attribute));
     cmdSeq.Add(
-      CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, Val(l), v)));
+      CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path), ExprHelper.FunctionCall(mapUpdateFunc, path, Key(c), Val(c))));
 
     ResolveAndTypecheck(options, cmdSeq);
     return cmdSeq;

Source/Concurrency/LinearTypeChecker.cs

@@ -774,7 +774,7 @@ public Type GetPermissionType(Type type)
       {
         var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
         var typeName = originalTypeCtorDecl.Name;
-        if (typeName == "Map" || typeName == "Set" || typeName == "One")
+        if (typeName == "Map" || typeName == "Set" || typeName == "Cell" | typeName == "One")
         {
           var actualTypeParams = program.monomorphizer.GetTypeInstantiation(datatypeTypeCtorDecl);
           return actualTypeParams[0];
@@ -974,7 +974,7 @@ private void CheckType(Type type)
         return;
       }
       var typeCtorDeclName = Monomorphizer.GetOriginalDecl(ctorType.Decl).Name;
-      if (typeCtorDeclName == "Map")
+      if (typeCtorDeclName == "Map" || typeCtorDeclName == "Cell")
       {
         hasLinearStoreAccess = true;
       }

Source/Core/CivlAttributes.cs

@@ -181,7 +181,8 @@ public static class CivlPrimitives
     public static HashSet<string> LinearPrimitives = new()
     {
       "One_New",
-      "Map_MakeEmpty", "Map_Pack", "Map_Unpack", "Map_Split", "Map_Get", "Map_Put", "Map_Assume",
+      "Cell_Pack", "Cell_Unpack",
+      "Map_MakeEmpty", "Map_Split", "Map_Get", "Map_Put", "Map_Assume",
       "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put"
     };
 
@@ -206,10 +207,10 @@ public static IdentifierExpr ModifiedArgument(CallCmd callCmd)
       switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
       {
         case "One_New":
+        case "Cell_Pack":
+        case "Cell_Unpack":
         case "Set_MakeEmpty":
         case "Map_MakeEmpty":
-        case "Map_Pack":
-        case "Map_Unpack":
         case "Map_Assume":
           return null;
         default:

Source/Core/base.bpl

@@ -287,14 +287,22 @@ function {:inline} Map_Collector<T,U>(a: Map T U): [T]bool
   Set_Collector(a->dom)
 }
 
-/// singleton
+/// singleton set
 datatype One<T> { One(val: T) }
 
 function {:inline} One_Collector<T>(a: One T): [T]bool
 {
   MapOne(a->val)
 }
 
+/// singleton map
+datatype Cell<T,U> { Cell(key: T, val: U) }
+
+function {:inline} Cell_Collector<T,U>(a: Cell T U): [T]bool
+{
+  MapOne(a->key)
+}
+
 /// linear primitives
 pure procedure {:inline 1} Set_MakeEmpty<K>() returns ({:linear} l: Set K)
 {
@@ -307,23 +315,23 @@ pure procedure One_Split<K>({:linear} path: Set K, {:linear_out} l: One K);
 pure procedure One_Get<K>({:linear} path: Set K, k: K) returns ({:linear} l: One K);
 pure procedure One_Put<K>({:linear} path: Set K, {:linear_in} l: One K);
 
-pure procedure {:inline 1} Map_MakeEmpty<K,V>() returns ({:linear} m: Map K V)
+pure procedure {:inline 1} Cell_Pack<K,V>({:linear_in} l: One K, {:linear_in} v: V) returns ({:linear} c: Cell K V)
 {
-  m := Map_Empty();
+  c := Cell(l->val, v);
 }
-pure procedure {:inline 1} Map_Pack<K,V>({:linear_in} l: One K, {:linear_in} v: V) returns ({:linear} m: Map K V)
+pure procedure {:inline 1} Cell_Unpack<K,V>({:linear_in} c: Cell K V) returns ({:linear} l: One K, {:linear} v: V)
 {
-  m := Map_Singleton(l->val, v);
+  l := One(c->key);
+  v := c->val;
 }
-pure procedure {:inline 1} Map_Unpack<K,V>(k: K, {:linear_in} m: Map K V) returns ({:linear} l: One K, {:linear} v: V)
+
+pure procedure {:inline 1} Map_MakeEmpty<K,V>() returns ({:linear} m: Map K V)
 {
-  assert Map_Contains(m, k);
-  l := One(k);
-  v := Map_At(m, k);
+  m := Map_Empty();
 }
 pure procedure Map_Split<K,V>({:linear} path: Map K V, {:linear_out} l: One K) returns ({:linear} v: V);
-pure procedure Map_Get<K,V>({:linear} path: Map K V, k: K) returns ({:linear} l: One K, {:linear} v: V);
-pure procedure Map_Put<K,V>({:linear} path: Map K V, {:linear_in} l: One K, {:linear_in} v: V);
+pure procedure Map_Get<K,V>({:linear} path: Map K V, k: K) returns ({:linear} c: Cell K V);
+pure procedure Map_Put<K,V>({:linear} path: Map K V, {:linear_in} c: Cell K V);
 pure procedure {:inline 1} Map_Assume<K,V>({:linear} src: Map K V, {:linear} dst: Map K V)
 {
   assume Set_IsDisjoint(src->dom, dst->dom);

Test/civl/paxos/PaxosImpl.bpl

@@ -376,31 +376,37 @@ refines A_ReceiveVoteResponse;
 pure action SendJoinResponseIntro(joinResponse: JoinResponse, {:linear_in} p: One Permission, {:linear_in} permJoinChannel: JoinResponseChannel)
 returns ({:linear} permJoinChannel': JoinResponseChannel)
 {
+  var {:linear} cell_p: Cell Permission JoinResponse;
   permJoinChannel' := permJoinChannel;
-  call Map_Put(permJoinChannel', p, joinResponse);
+  call cell_p := Cell_Pack(p, joinResponse);
+  call Map_Put(permJoinChannel', cell_p);
 }
 
 pure action ReceiveJoinResponseIntro(round: Round, joinResponse: JoinResponse, {:linear_in} permJoinChannel: JoinResponseChannel)
 returns ({:linear} receivedPermission: One Permission, {:linear} permJoinChannel': JoinResponseChannel)
 {
-  var x: JoinResponse;
+  var _x: JoinResponse;
   permJoinChannel' := permJoinChannel;
-  call receivedPermission, x := Map_Get(permJoinChannel', JoinPerm(round, joinResponse->from));
+  receivedPermission := One(JoinPerm(round, joinResponse->from));
+  call _x := Map_Split(permJoinChannel', receivedPermission);
 }
 
 pure action SendVoteResponseIntro(voteResponse: VoteResponse, {:linear_in} p: One Permission, {:linear_in} permVoteChannel: VoteResponseChannel)
 returns ({:linear} permVoteChannel': VoteResponseChannel)
 {
+  var {:linear} cell_p: Cell Permission VoteResponse;
   permVoteChannel' := permVoteChannel;
-  call Map_Put(permVoteChannel', p, voteResponse);
+  call cell_p := Cell_Pack(p, voteResponse);
+  call Map_Put(permVoteChannel', cell_p);
 }
 
 pure action ReceiveVoteResponseIntro(round: Round, voteResponse: VoteResponse, {:linear_in} permVoteChannel: VoteResponseChannel)
 returns ({:linear} receivedPermission: One Permission, {:linear} permVoteChannel': VoteResponseChannel)
 {
-  var x: VoteResponse;
+  var _x: VoteResponse;
   permVoteChannel' := permVoteChannel;
-  call receivedPermission, x := Map_Get(permVoteChannel', VotePerm(round, voteResponse->from));
+  receivedPermission := One(VotePerm(round, voteResponse->from));
+  call _x := Map_Split(permVoteChannel', receivedPermission);
 }
 
 //// Permission accounting