Merge branch 'dev' into nisarg-wip

Raven.opam

@@ -6,7 +6,7 @@ description:
 depends: [
   "ocaml" {>= "4.12.0"}
   "dune" {>= "3.12" & >= "3.12"}
-  "z3" {= "4.12.2"}
+  "z3" {>= "4.13.0"}
   "ocamlformat" {>= "0.22.4"}
   "base" {>= "0.14"}
   "stdio" {>= "0.14"}

dune-project

@@ -14,7 +14,7 @@
   (dune
    (>= 3.12))
   (z3
-   (= 4.12.2))
+   (>= 4.13.0))
   (ocamlformat
    (>= 0.22.4))
   (base

test/concurrent/templates/keyset_ra.rav

@@ -0,0 +1,85 @@
+module KeysetRA[K: Library.Type] : Library.ResourceAlgebra {
+    rep type T = data {
+        case prodKS(inset: Set[K], contents: Set[K]);
+        case topKS
+    }
+
+    val id: T = prodKS({||}, {||});
+
+    func valid(n:T) returns (ret:Bool) {
+        n == prodKS(n.inset, n.contents) && n.contents subseteq n.inset
+    }
+
+
+    func ks_composable(a:T, b:T) returns (ret:Bool) {
+        valid(a) && valid(b) && a.inset ** b.inset == {||}
+    }
+
+    func comp(a:T, b:T) returns (ret:T) {
+        a == id ? 
+            b :
+            (b == id ? 
+                a :
+                (ks_composable(a, b) ?
+                    prodKS(a.inset ++ b.inset, a.contents ++ b.contents) : topKS())
+            )
+    }
+
+    func frame(a:T, b:T) returns (ret:T) {
+        b == id ? a :
+        (valid(a) && valid(b) && b.inset subseteq a.inset && b.contents subseteq a.contents ?
+            prodKS(a.inset -- b.inset, a.contents -- b.contents) : topKS())
+    }
+
+    func fpuAllowed(a:T, b:T) returns (ret:Bool) {
+        a == b ? true : 
+        (valid(a) && valid(b) && b.inset subseteq a.inset ?
+            true : false)
+    }
+
+    auto lemma idValid()
+        ensures valid(id)
+    {}
+
+    auto lemma compAssoc()
+        ensures forall a:T, b:T, c:T :: {comp(comp(a, b), c)} {comp(a, comp(b, c))} (comp(comp(a, b), c) == comp(a, comp(b, c)))
+    {}
+
+    auto lemma compCommute()
+        ensures forall a:T, b:T :: {comp(a,b)} {comp(b,a)} comp(a, b) == comp(b, a)
+    { 
+    }
+
+    auto lemma compId()
+        ensures forall a:T :: {comp(a, id)} comp(a, id) == a
+    {}
+
+    auto lemma compValid()
+        ensures forall a:T, b:T :: {comp(a,b)} valid(comp(a, b)) ==> valid(a) && valid(b)
+    {}
+
+    auto lemma frameId()
+        ensures forall a:T :: {frame(a,id)} frame(a, id) == a
+    {}
+
+    auto lemma compFrameInv()
+        ensures forall a:T, b:T :: {comp(frame(a, b), b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a
+    {}
+
+    auto lemma fpuValid()
+        ensures forall a:T, b:T, c:T :: {fpuAllowed(a,b), comp(a,c)} {fpuAllowed(a,b), comp(b,c)}
+            (fpuAllowed(a,b) && valid(a) && valid(comp(a,c))) ==> valid(comp(b,c))
+    {}
+
+    auto lemma fpuReflexive()
+        ensures (forall a:T :: {fpuAllowed(a,a)} valid(a) ==> fpuAllowed(a,a))
+    {}
+
+    auto lemma frameValid()
+        ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a,b)) ==> valid(a) && valid(b)
+    {}
+
+    auto lemma weak_frameCompInv()
+        ensures forall a:T, b:T:: {frame(comp(a, b), b)} valid(comp(a, b)) ==> valid(frame(comp(a, b), b))
+    {}
+}