[Civl] Fixed treiber stack (#885)

This PR fixes the Treiber stack sample. - new feature to split One T with respect to a given Set K using new type Fraction T K and new APIs to go between One T and Fraction T K - use the feature to fix the proof --------- Co-authored-by: Shaz Qadeer <[email protected]>
boogie-org · May 14, 2024 · 0558613 · 0558613
1 parent 3583ebb
commit 0558613
Show file tree

Hide file tree

Showing 5 changed files with 210 additions and 172 deletions.
diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs
@@ -59,6 +59,8 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
     switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
     {
       case "One_New":
+      case "One_To_Fractions":
+      case "Fractions_To_One":
       case "Cell_Pack":
       case "Cell_Unpack":
       case "Set_MakeEmpty":

diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs
@@ -180,7 +180,7 @@ public static class CivlPrimitives
   {
     public static HashSet<string> LinearPrimitives = new()
     {
-      "One_New",
+      "One_New", "One_To_Fractions", "Fractions_To_One",
       "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"

diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl
@@ -278,7 +278,8 @@ function {:inline} Map_Swap<T,U>(a: Map T U, t1: T, t2: T): Map T U
   (var u1, u2 := Map_At(a, t1), Map_At(a, t2); Map_Update(Map_Update(a, t1, u2), t2, u1))
 }
 
-function {:inline} Map_WellFormed<T,U>(a: Map T U): bool {
+function {:inline} Map_WellFormed<T,U>(a: Map T U): bool
+{
   a->val == MapIte(a->dom->val, a->val, MapConst(Default()))
 }
 
@@ -295,6 +296,19 @@ function {:inline} One_Collector<T>(a: One T): [T]bool
   MapOne(a->val)
 }
 
+datatype Fraction<T, K> { Fraction(val: T, id: K, ids: [K]bool) }
+
+pure procedure {:inline 1} One_To_Fractions<T,K>({:linear_in} one_t: One T, ids: [K]bool) returns ({:linear} pieces: Set (Fraction T K))
+{
+  pieces := Set((lambda piece: Fraction T K :: piece->val == one_t->val && ids[piece->id] && piece->ids == ids));
+}
+
+pure procedure {:inline 1} Fractions_To_One<T,K>({:linear_out} one_t: One T, ids: [K]bool, {:linear_in} pieces: Set (Fraction T K))
+{
+  assert (forall piece: Fraction T K:: Set_Contains(pieces, piece) ==> piece->val == one_t->val && piece->ids == ids);
+  assert pieces == Set((lambda piece: Fraction T K :: piece->val == one_t->val && ids[piece->id] && piece->ids == ids));
+}
+
 /// singleton map
 datatype Cell<T,U> { Cell(key: T, val: U) }