From c6562b0941129171e8af070a304736c385fca297 Mon Sep 17 00:00:00 2001
From: Ekanshdeep Gupta <ekanshdeep_gupta@yahoo.co.in>
Date: Tue, 7 May 2024 14:35:45 -0400
Subject: [PATCH] Added keyset_ra; updated z3 from 4.12.2 to 4.13

---
 Raven.opam                              |  2 +-
 dune-project                            |  2 +-
 test/concurrent/templates/keyset_ra.rav | 85 +++++++++++++++++++++++++
 3 files changed, 87 insertions(+), 2 deletions(-)
 create mode 100644 test/concurrent/templates/keyset_ra.rav

diff --git a/Raven.opam b/Raven.opam
index 48164cb..9189282 100644
--- a/Raven.opam
+++ b/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"}
diff --git a/dune-project b/dune-project
index fb163ea..9762515 100644
--- a/dune-project
+++ b/dune-project
@@ -14,7 +14,7 @@
   (dune
    (>= 3.12))
   (z3
-   (= 4.12.2))
+   (>= 4.13.0))
   (ocamlformat
    (>= 0.22.4))
   (base
diff --git a/test/concurrent/templates/keyset_ra.rav b/test/concurrent/templates/keyset_ra.rav
new file mode 100644
index 0000000..8b9a8b6
--- /dev/null
+++ b/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))
+    {}
+}
\ No newline at end of file