progree on B+ tree

test/arrays/array_util.rav

@@ -14,6 +14,17 @@ interface Array {
     ensures forall a:T :: {length(a)} length(a) >= 0
 
   field value: E
+
+  val default: E
+
+  pred arr(a: T; m: Map[Int, E]) {
+    (forall j: Int :: 0 <= j < length(a) ==> own(loc(a, j), value, m[j], 1.0)) 
+    && (forall j: Int :: {m[j]} (0 > j || j >= length(a)) ==> m[j] == default)
+  }
+
+  proc alloc(len: Int, d: E) returns (a: T)
+    requires 0 <= len
+    ensures length(a) == len && arr(a, {| i: Int :: 0 <= i < len ? d : default |})
 }
 
 interface ArrayUtil[K: Library.OrderedType] {
@@ -23,12 +34,8 @@ interface ArrayUtil[K: Library.OrderedType] {
     type E = K
   }
 
-  //import A.value
-
-  pred arr(a: A, m: Map[Int, K]) {
-    forall j: Int :: 0 <= j < A.length(a) ==> own(A.loc(a, j), A.value, m[j], 1.0)
-  }
-
+  import A.arr
+
   // project map segment m[i..j] to set of its elements
   func set_of_map(m: Map[Int, K], i: Int, j: Int)
     returns (res: Set[K])
@@ -250,11 +257,11 @@ interface ArrayUtil[K: Library.OrderedType] {
         invariant 0 <= dst <= dst + len <= A.length(a)
         invariant -1 <= i < len
       {
-        //ghost var m1 := a.map;
         unfold arr(a, map_shift(amap, src + i + 1, dst + i + 1, len - i - 1));
         var tmp: K := A.loc(a, src + i).A.value;
         A.loc(a, dst + i).A.value := tmp;
-        //pure assert a.map == m1[dst + i := tmp];
+        ghost var m : Map[Int, K] = map_shift(amap, src + i, dst + i, len - i);
+        assert m == map_shift(amap, src + i + 1, dst + i + 1, len - i - 1)[dst + i := tmp];
         i := i - 1;
         fold arr(a, map_shift(amap, src + i + 1, dst + i + 1, len - i - 1));
       }
@@ -267,11 +274,11 @@ interface ArrayUtil[K: Library.OrderedType] {
         invariant 0 <= dst <= dst + len <= A.length(a)
         invariant 0 <= i <= len 
       {
-        //ghost var m1 := a.map;
         unfold arr(a, map_shift(amap, src, dst, i));
         var tmp: K := A.loc(a, src + i).A.value;
         A.loc(a, dst + i).A.value := tmp;
-        //pure assert a.map == m1[dst + i := tmp];
+        ghost var m : Map[Int, K] = map_shift(amap, src, dst, i + 1);
+        assert m == map_shift(amap, src, dst, i)[dst + i := tmp];
         i := i + 1;
         fold arr(a, map_shift(amap, src, dst, i));
       }
@@ -299,12 +306,14 @@ interface ArrayUtil[K: Library.OrderedType] {
       fold arr(a, amap);
       unfold arr(b, map_copy(bmap, amap, src, dst, i));
       A.loc(b, dst + i).A.value := tmp;
+      ghost var m: Map[Int, K] = map_copy(bmap, amap, src, dst, i + 1);
+      assert m == map_copy(bmap, amap, src, dst, i)[dst + i := tmp];
       i := i + 1;
       fold arr(b, map_copy(bmap, amap, src, dst, i));
     }
   }
 
-  pred sorted_array_with_content(a: A, len: Int, m: Map[Int, K])
+  pred sorted_array_with_content(a: A, len: Int; m: Map[Int, K])
   {
     0 <= len <= A.length(a) && arr(a, m) && sorted_map_seg(m, 0, len)
   }

test/concurrent/templates/bplustree.rav

@@ -0,0 +1,103 @@
+include "give-up.rav"
+include "../../arrays/array_util.rav"
+
+interface BPlusTree[O: Library.OrderedType] : NodeImpl {
+
+  module Spec : SearchStructureSpec {
+    type K = O
+    val keyspace: Set[K] = {| k: K :: true |}
+  }
+
+  import Spec._
+
+  module KOption = Library.Option[O]
+
+  import KOption.some
+  import KOption.none
+
+  import Flow_K._
+  import Multiset_K.elem
+
+  interface AU = ArrayUtil[O]
+
+  import AU._
+
+  interface AN : Array {
+    type E = Ref
+  }
+
+  // Width parameter of the B-tree
+  val b: Int
+
+  auto axiom bValid() 
+    ensures b > 0
+
+  // Fields of a B-tree node
+  field len: Int
+  field rangeLb: KOption
+  field rangeUb: KOption
+  field keys: A.T
+  field ptrs: AN.T
+
+  func le(ko: KOption, k: K) returns (res : Bool)
+  {
+    ko == none ? true : O.le(ko.KOption.value, k)
+  }
+
+  func lt(k: K, ko: KOption) returns (res : Bool)
+  {
+    ko == none ? true : O.lt(k, ko.KOption.value)
+  }
+
+  func flow_int_of(n: Ref, lb: KOption, ub: KOption, kmap: Map[Int, K], cmap: Map[Int, Ref]) returns (flow_int: Flow_K)
+  {
+    Flow_K.int({| np: Ref :: np == n ? {| k: K :: le(lb, k) && lt(k, ub) ? 1 : 0 |} : Multiset_K.id |},
+               {| np: Ref :: Multiset_K.id /* TODO: fix this */ |},
+               {| n |})
+  }
+
+
+  pred node(n: Ref; c: Set[K], flow_int: Flow_K) {
+    exists l: Int, lb: KOption, ub: KOption, ks: A.T, chlds: AN.T, kmap: Map[Int, K], cmap: Map[Int, Ref] ::
+       0 <= l && l < 2*b 
+    && A.length(ks) == 2*b 
+    && AN.length(chlds) == 2*b
+    // Definition of flow interface
+    && flow_int == flow_int_of(n, lb, ub, kmap, cmap)
+    // Definition of contents
+    && c == (cmap[0] == null ? /* Leaf */ AU.set_of_map(kmap, 0, l) : {||})
+    // Keys are sorted
+    && (forall i: Int, j: Int :: {kmap[i], kmap[j]} 0 <= i < j < l ==> O.lt(kmap[i], kmap[j]))
+    // Keys are within range
+    && (l > 0 ==> le(lb, kmap[0]) && lt(kmap[l-1], ub))
+    // Consistency of cmap
+    && (cmap[0] != null ==>
+           (forall i: Int :: {cmap[i]} 0 <= i <= l ==> n != cmap[i])
+        && (forall i: Int, j: Int :: {cmap[i], cmap[j]} 0 <= i < j <= l ==> cmap[i] != cmap[j])
+        && (forall i: Int :: {cmap[i]} 0 <= i <= l ==> cmap[i] != null))       
+    // Heap resources
+    && own(n, len, l, 1.0)
+    && own(n, rangeLb, lb, 1.0)
+    && own(n, rangeLb, ub, 1.0)
+    && own(n, keys, ks, 1.0)
+    && AU.sorted_array_with_content(ks, l, kmap)
+    && own(n, ptrs, chlds, 1.0)
+    && AN.arr(chlds, cmap)
+  }
+
+
+  /* Initialize a new root node */
+  proc createRoot() returns (r: Ref)
+    ensures node(r, {||}, 
+      Flow_K.int({| l: Ref :: l == r ? Multiset_K.fromSet(keyspace) : Multiset_K.id |}, zeroFlow, {| r |}))
+  {
+    var ka: A.T;
+    ka := A.alloc(2*b, A.default);
+    var pa: AN.T;
+    pa := AN.alloc(2*b, null);
+    r := new(len: 0, rangeLb: none, rangeUb: none, keys: ka, ptrs: pa);
+
+    fold node(r, {||}, 
+      Flow_K.int({| l: Ref :: l == r ? Multiset_K.fromSet(keyspace) : Multiset_K.id |}, zeroFlow, {| r |}));    
+  }
+}

test/concurrent/templates/give-up.rav

@@ -23,7 +23,7 @@ interface SearchStructureSpec {
 
   type Op = data { case searchOp ; case insertOp ; case deleteOp }
 
-	pred opSpec(op: Op, k: K, c_in: Set[K], c_out: Set[K], res: Bool) {
+	pred opSpec(op: Op, k: K, c_in: Set[K]; c_out: Set[K], res: Bool) {
     op == searchOp() ? 
       c_in == c_out && res == (k in c_in) :
     (op == insertOp() ?