prove pivotsAreCorrectAfterSplit

Author: Travis Hance

immutable-btree/BtreeInv.dfy

@@ -517,20 +517,71 @@ abstract module BtreeInv {
     }
   }
 
+  lemma pivotsAreCorrectAfterSplit(tree: Node, newtree: Node, l: Key, u: Key, childrenToLeft: int, pos: int)
+  requires WFTree(tree);
+  requires SplitTransform(tree, newtree, l, u, childrenToLeft);
+  requires pos == Keyspace.LargestLte(tree.pivots, l) + 1;
+  requires 0 <= pos < |tree.children|;
+  requires tree.children[pos].lb == l;
+  requires tree.children[pos].ub == u;
+  ensures Keyspace.IsStrictlySorted(newtree.pivots);
+  {
+    var child := tree.children[pos];
+    assert |newtree.children| == |tree.children| + 1;
+    var left_child := newtree.children[pos];
+    var right_child := newtree.children[pos+1];
+    assert WFTree(child);
+    if (pos < |tree.pivots|) {
+      if (child.Leaf?) {
+        assert newtree.pivots[pos]
+            == right_child.keys[0]
+            == child.keys[childrenToLeft];
+        assert Keyspace.lt(child.keys[childrenToLeft], child.ub);
+      } else {
+        assert newtree.pivots[pos] == child.pivots[childrenToLeft-1];
+        assert Keyspace.lt(child.pivots[childrenToLeft-1], child.ub);
+      }
+      assert child.ub == tree.pivots[pos];
+      assert Keyspace.lt(newtree.pivots[pos], tree.pivots[pos]);
+    }
+    if (pos > 0) {
+      if (child.Leaf?) {
+        assert Keyspace.lte(child.lb, child.keys[0]);
+        Keyspace.reveal_IsStrictlySorted();
+        assert Keyspace.lt(child.keys[0], child.keys[childrenToLeft]);
+        assert Keyspace.lt(child.lb, child.keys[childrenToLeft]);
+      } else {
+        assert Keyspace.lt(child.lb, child.pivots[childrenToLeft-1]);
+      }
+      assert child.lb == tree.pivots[pos-1];
+      assert Keyspace.lt(tree.pivots[pos-1], newtree.pivots[pos]);
+    }
+    Keyspace.strictlySortedInsert2(tree.pivots, newtree.pivots[pos], pos);
+  }
+
   lemma SplitIsCorrect<Value>(tree: Node, newtree: Node, l: Key, u: Key, childrenToLeft: int)
   requires WFTree(tree);
   requires CantEquivocate(tree);
   requires SplitTransform(tree, newtree, l, u, childrenToLeft);
+  ensures WFTree(newtree);
   ensures PreservesLookups(tree, newtree);
   ensures PreservesLookups(newtree, tree);
-  ensures WFTree(newtree)
-  ensures CantEquivocate(newtree)
-  decreases tree
+  ensures CantEquivocate(newtree);
+  decreases tree;
   {
     var pos := Keyspace.LargestLte(tree.pivots, l) + 1;
     var child := tree.children[pos];
     if (child.lb == l && child.ub == u) {
+      var left_child := newtree.children[pos];
+      var right_child := newtree.children[pos+1];
+      pivotsAreCorrectAfterSplit(tree, newtree, l, u, childrenToLeft, pos);
+      assert WFTree(newtree);
+      assume false;
+      assert PreservesLookups(tree, newtree);
+      assert PreservesLookups(newtree, tree);
+      assert CantEquivocate(newtree);
     } else {
+      assume false;
       // Before we can call Define recursively, we must prove that the child CantEquivocate.
       forall key', valueA, valueB, lookup, lookup'
       |

immutable-btree/BtreeSpec.dfy

@@ -27,9 +27,9 @@ abstract module BtreeSpec {
       && CSMap.Keyspace.IsStrictlySorted(tree.keys)
       && |tree.keys| == |tree.values|
       && (forall i :: 0 <= i < |tree.keys| ==>
-          && CSMap.Keyspace.lte(tree.lb, tree.keys[i])
-          && CSMap.Keyspace.lt(tree.keys[i], tree.ub)
-         )
+          && CSMap.Keyspace.lte(tree.lb, tree.keys[i]))
+      && (forall i :: 0 <= i < |tree.keys| ==>
+          && CSMap.Keyspace.lt(tree.keys[i], tree.ub))
     else
       && |tree.pivots| > 0
       && CSMap.Keyspace.IsStrictlySorted(tree.pivots)
@@ -193,7 +193,7 @@ abstract module BtreeSpec {
   {
     && node.lb == left_node.lb
     && left_node.ub == pivot
-    && pivot == right_node.ub
+    && pivot == right_node.lb
     && right_node.ub == node.ub
     && (if node.Leaf? then (
       && left_node.Leaf?

lib/total_order.dfy

@@ -243,6 +243,16 @@ abstract module Total_Order {
     {
     }
   }
+
+  lemma strictlySortedInsert2(l: seq<Element>, k: Element, pos: int)
+  requires 0 <= pos <= |l|;
+  requires 0 < pos ==> lt(l[pos-1], k);
+  requires pos < |l| ==> lt(k, l[pos]);
+  ensures IsStrictlySorted(Seq.insert(l, k, pos));
+  {
+    Seq.reveal_insert();
+    reveal_IsStrictlySorted();
+  }
 }
 
 abstract module Bounded_Total_Order refines Total_Order {