Unit type

Author: shazqadeer

Source/Core/base.bpl

@@ -358,4 +358,9 @@ pure procedure Assume(b: bool);
 ensures b;
 
 pure procedure Move<T>({:linear_in} v: T, {:linear_out} v': T);
-requires v == v';
+requires v == v';
+
+datatype Unit { Unit() }
+function {:inline} UnitSet(): Set Unit {
+  Set_Add(Set_Empty(), Unit())
+}

Test/civl/large-samples/treiber-stack.bpl

@@ -1,11 +1,6 @@
 // RUN: %parallel-boogie -lib:base -lib:node -timeLimit:0 -vcsSplitOnEveryAssert "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-datatype LocPiece { Right() }
-function {:inline} AllLocPieces(): Set LocPiece {
-  Set_Add(Set_Empty(), Right())
-}
-
 type LocTreiberStack = Loc;
 type LocTreiberNode = Loc;
 type StackElem T = Node LocTreiberNode T;
@@ -61,41 +56,41 @@ invariant Map_At(TreiberPool, loc_t) == Abs(Map_At(TreiberPoolLow, loc_t));
 yield invariant {:layer 4} StackDom();
 invariant TreiberPool->dom == TreiberPoolLow->dom;
 
-yield invariant {:layer 4} PushLocInStack(loc_t: LocTreiberStack, node: StackElem X, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One (TaggedLoc LocPiece));
+yield invariant {:layer 4} PushLocInStack(loc_t: LocTreiberStack, node: StackElem X, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One (TaggedLoc Unit));
 invariant Map_Contains(TreiberPoolLow, loc_t);
 invariant Set_Contains(Domain(TreiberPoolLow, loc_t), new_loc_n);
-invariant right_loc_piece->val == TaggedLoc(new_loc_n, Right());
+invariant right_loc_piece->val == TaggedLoc(new_loc_n, Unit());
 invariant (var t := TreiberPoolLow->val[loc_t]; Map_At(t->nodes, new_loc_n) == node && !BetweenSet(t->nodes->val, t->top, None())[new_loc_n]);
 
 /// Layered implementation
 
-atomic action {:layer 5} AtomicAlloc() returns ({:linear} right_loc_piece: One (TaggedLoc LocPiece))
+atomic action {:layer 5} AtomicAlloc() returns ({:linear} right_loc_piece: One (TaggedLoc Unit))
 {
   var {:linear} one_loc_t: One LocTreiberStack;
-  var {:linear} loc_pieces: Set (TaggedLoc LocPiece);
+  var {:linear} loc_pieces: Set (TaggedLoc Unit);
 
-  call one_loc_t, loc_pieces := TaggedLocSet_New(AllLocPieces());
-  call right_loc_piece := One_Get(loc_pieces, TaggedLoc(one_loc_t->val, Right()));
+  call one_loc_t, loc_pieces := TaggedLocSet_New(UnitSet());
+  call right_loc_piece := One_Get(loc_pieces, TaggedLoc(one_loc_t->val, Unit()));
   assume !Map_Contains(TreiberPool, one_loc_t->val);
   TreiberPool := Map_Update(TreiberPool, one_loc_t->val, Vec_Empty());
 }
-yield procedure {:layer 4} Alloc() returns ({:linear} right_loc_piece: One (TaggedLoc LocPiece))
+yield procedure {:layer 4} Alloc() returns ({:linear} right_loc_piece: One (TaggedLoc Unit))
 refines AtomicAlloc;
 ensures call TopInStack(right_loc_piece->val->loc);
 ensures call ReachInStack(right_loc_piece->val->loc);
 preserves call StackDom();
 {
   var {:linear} one_loc_t: One LocTreiberStack;
-  var {:linear} loc_pieces: Set (TaggedLoc LocPiece);
+  var {:linear} loc_pieces: Set (TaggedLoc Unit);
   var top: Option LocTreiberNode;
   var {:linear} stack: StackMap X;
   var {:linear} treiber: Treiber X;
 
   top := None();
   call stack := Map_MakeEmpty();
   treiber := Treiber(top, stack);
-  call one_loc_t, loc_pieces := TaggedLocSet_New(AllLocPieces());
-  call right_loc_piece := One_Get(loc_pieces, TaggedLoc(one_loc_t->val, Right()));
+  call one_loc_t, loc_pieces := TaggedLocSet_New(UnitSet());
+  call right_loc_piece := One_Get(loc_pieces, TaggedLoc(one_loc_t->val, Unit()));
   call AllocTreiber#0(one_loc_t, treiber);
   call {:layer 4} TreiberPool := Copy(Map_Update(TreiberPool, one_loc_t->val, Vec_Empty()));
   call {:layer 4} AbsLemma(treiber);
@@ -118,7 +113,7 @@ preserves call StackDom();
 {
   var loc_n: Option LocTreiberNode;
   var new_loc_n: LocTreiberNode;
-  var {:linear} right_loc_piece: One (TaggedLoc LocPiece);
+  var {:linear} right_loc_piece: One (TaggedLoc Unit);
   var {:layer 4} old_treiber: Treiber X;
 
   call {:layer 4} old_treiber := Copy(TreiberPoolLow->val[loc_t]);
@@ -166,39 +161,39 @@ preserves call StackDom();
 }
 
 atomic action {:layer 4} AtomicCreateNewTopOfStack(loc_t: LocTreiberStack, x: X)
-  returns (loc_n: Option LocTreiberNode, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One (TaggedLoc LocPiece))
+  returns (loc_n: Option LocTreiberNode, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One (TaggedLoc Unit))
 asserts Map_Contains(TreiberPoolLow, loc_t);
 {
   var {:linear} one_loc_t: One LocTreiberStack;
   var {:linear} treiber: Treiber X;
   var top: Option LocTreiberNode;
   var {:linear} stack: StackMap X;
   var {:linear} one_loc_n: One LocTreiberNode;
-  var {:linear} loc_pieces: Set (TaggedLoc LocPiece);
+  var {:linear} loc_pieces: Set (TaggedLoc Unit);
 
   call one_loc_t, treiber := Map_Get(TreiberPoolLow, loc_t);
   Treiber(top, stack) := treiber;
   assume loc_n is None || Map_Contains(stack, loc_n->t);
-  call one_loc_n, loc_pieces := TaggedLocSet_New(AllLocPieces());
+  call one_loc_n, loc_pieces := TaggedLocSet_New(UnitSet());
   new_loc_n := one_loc_n->val;
-  call right_loc_piece := One_Get(loc_pieces, TaggedLoc(new_loc_n, Right()));
+  call right_loc_piece := One_Get(loc_pieces, TaggedLoc(new_loc_n, Unit()));
   call Map_Put(stack, one_loc_n, Node(loc_n, x));
   treiber := Treiber(top, stack);
   call Map_Put(TreiberPoolLow, one_loc_t, treiber);
 }
 yield procedure {:layer 3} CreateNewTopOfStack(loc_t: LocTreiberStack, x: X)
-  returns (loc_n: Option LocTreiberNode, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One (TaggedLoc LocPiece))
+  returns (loc_n: Option LocTreiberNode, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One (TaggedLoc Unit))
 preserves call TopInStack(loc_t);
 ensures call LocInStackOrNone(loc_t, Some(new_loc_n));
 refines AtomicCreateNewTopOfStack;
 {
   var {:linear} one_loc_n: One LocTreiberNode;
-  var {:linear} loc_pieces: Set (TaggedLoc LocPiece);
+  var {:linear} loc_pieces: Set (TaggedLoc Unit);
 
   call loc_n := ReadTopOfStack#Push(loc_t);
-  call one_loc_n, loc_pieces := TaggedLocSet_New(AllLocPieces());
+  call one_loc_n, loc_pieces := TaggedLocSet_New(UnitSet());
   new_loc_n := one_loc_n->val;
-  call right_loc_piece := One_Get(loc_pieces, TaggedLoc(new_loc_n, Right()));
+  call right_loc_piece := One_Get(loc_pieces, TaggedLoc(new_loc_n, Unit()));
   call AllocNode#0(loc_t, one_loc_n, Node(loc_n, x));
 }