From e3b73ac90059911045c8292615c67195752d22bc Mon Sep 17 00:00:00 2001 From: Thomas Wies Date: Thu, 24 Oct 2024 21:36:23 -0400 Subject: [PATCH] progress on pblustree --- test/arrays/array.rav | 366 +++++++++++++++++++ test/arrays/array_util.rav | 448 ------------------------ test/arrays/ordered_array.rav | 270 ++++++++++++++ test/concurrent/templates/bplustree.rav | 66 ++-- 4 files changed, 681 insertions(+), 469 deletions(-) create mode 100644 test/arrays/array.rav delete mode 100644 test/arrays/array_util.rav create mode 100644 test/arrays/ordered_array.rav diff --git a/test/arrays/array.rav b/test/arrays/array.rav new file mode 100644 index 0000000..00e5d59 --- /dev/null +++ b/test/arrays/array.rav @@ -0,0 +1,366 @@ +interface Array[E: Library.Type] { + rep type T + + func loc(a: T, i: Int) returns (r: Ref) + func length(a: T) returns (l: Int) + func first(r: Ref) returns (a: T) + func second(r: Ref) returns (i: Int) + + auto axiom all_diff() + ensures forall a:T, i: Int :: {loc(a, i)} first(loc(a, i)) == a && second(loc(a, i)) == i + + auto axiom len_nonneg() + ensures forall a:T :: {length(a)} length(a) >= 0 + + field value: E + + val default: E + + val default_map: Map[Int, E] = {| i: Int :: default |} + + 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 |}) + + func injective(m: Map[Int, E], i: Int, j: Int) returns (res: Bool) + { + forall i1: Int, i2: Int :: {m[i1], m[i2]} i <= i1 < i2 < j ==> m[i1] != m[i2] + } + + func inverse_help(m: Map[Int, E], i: Int, j: Int, k: E, i1: Int) returns (res: Int) + { + m[i1] == k && i1 < j ? i1 : (i1 < j ? inverse_help(m, i, j, k, i1+1) : i-1) + } + + func inverse(m: Map[Int, E], i: Int, j: Int, k: E) returns (res: Int) + { + inverse_help(m, i, j, k, i) + } + + lemma invertable_help(m: Map[Int, E], i: Int, j: Int, i1: Int, i2: Int) + requires injective(m, i, j) + ensures i <= i2 <= i1 < j ==> inverse_help(m, i, j, m[i1], i2) == i1 + { + if (i <= i2 <= i1 < j) { + if (i2 < i1) { + invertable_help(m, i, j, i1, i2+1); + } + } + } + + auto lemma invertable() + ensures forall m: Map[Int, E], i: Int, j: Int, i1: Int :: {injective(m, i, j), m[i1]} + injective(m, i, j) && i <= i1 < j ==> inverse(m, i, j, m[i1]) == i1 + { + assert forall m: Map[Int, E], i: Int, j: Int, i1: Int :: {injective(m, i, j), m[i1]} + injective(m, i, j) && i <= i1 < j ==> inverse(m, i, j, m[i1]) == i1 with { + if (injective(m, i, j) && i <= i1 < j) { + invertable_help(m, i, j, i1, i); + } + } + } + + lemma invertable2_help(m: Map[Int, E], i: Int, j: Int, k: E, i2: Int) + ensures i <= i2 <= inverse_help(m, i, j, k, i2) < j ==> m[inverse_help(m, i, j, k, i2)] == k + ensures i2 > inverse_help(m, i, j, k, i2) || inverse_help(m, i, j, k, i2) >= j ==> inverse_help(m, i, j, k, i2) == i-1 + { + if (i2 < j) { + invertable2_help(m, i, j, k, i2+1); + } + } + + auto lemma invertable2() + ensures forall m: Map[Int, E], i: Int, j: Int, k: E :: {inverse(m, i, j, k)} + (i <= inverse(m, i, j, k) < j ==> m[inverse(m, i, j, k)] == k) && + (i > inverse(m, i, j, k) || inverse(m, i, j, k) >= j ==> inverse(m, i, j, k) == i-1) + { + assert forall m: Map[Int, E], i: Int, j: Int, k: E :: {inverse(m, i, j, k)} + (i <= inverse(m, i, j, k) < j ==> m[inverse(m, i, j, k)] == k) && + (i > inverse(m, i, j, k) || inverse(m, i, j, k) >= j ==> inverse(m, i, j, k) == i-1) + with { + invertable2_help(m, i, j, k, i); + } + } + + lemma inverse_update_help(m: Map[Int, E], i: Int, j: Int, k: E, i1: Int, k2: E, i2: Int) + requires inverse_help(m, i, j, k2, i2) < i2 || i1 < i2 || i1 >= j + ensures inverse_help(m[i1 := k], i, j, k2, i2) == (k == k2 && i2 <= i1 < j ? i1 : inverse_help(m, i, j, k2, i2)) + { + if (i2 < j) { + inverse_update_help(m, i, j, k, i1, k2, i2+1); + } + } + + auto lemma inverse_update() + ensures forall m: Map[Int, E], i: Int, j: Int, k: E, i1: Int, k2: E :: {inverse(m[i1 := k], i, j, k2)} + inverse(m, i, j, k2) < i || i1 < i || i1 >= j ==> + inverse(m[i1 := k], i, j, k2) == (k == k2 && i <= i1 < j ? i1 : inverse(m, i, j, k2)) + { + assert forall m: Map[Int, E], i: Int, j: Int, k: E, i1: Int, k2: E :: {inverse(m[i1 := k], i, j, k2)} + inverse(m, i, j, k2) < i || i1 < i || i1 >= j ==> + inverse(m[i1 := k], i, j, k2) == (k == k2 && i <= i1 < j ? i1 : inverse(m, i, j, k2)) with { + if (inverse(m, i, j, k2) < i || i1 < i || i1 >= j) { + inverse_update_help(m, i, j, k, i1, k2, i); + } + } + } + + func set_of_map(m: Map[Int, E], i: Int, j: Int) returns (res: Set[E]) + { + {| k: E :: injective(m, i, j) && i <= inverse(m, i, j, k) < j |} //&& m[inverse(m, i, j, k)] == k |} + } + + lemma injective_split() + ensures forall m: Map[Int, E], i: Int, j: Int, l: Int :: {injective(m, i, l), injective(m, i, j)} + i <= j <= l && injective(m, i, l) ==> injective(m, i, j) + ensures forall m: Map[Int, E], i: Int, j: Int, l: Int :: {injective(m, i, l), injective(m, j, l)} + i <= j <= l && injective(m, i, l) ==> injective(m, j, l) + {} + + lemma set_of_map_split(m: Map[Int, E], i: Int, j: Int, l: Int) + requires i <= j <= l && injective(m, i, l) + ensures set_of_map(m, i, l) == set_of_map(m, i, j) ++ set_of_map(m, j, l) + { } + + func map_shift(m: Map[Int, E], src: Int, dst: Int, len: Int) + returns (res: Map[Int, E]) + { + {| i: Int :: i < dst || dst + len <= i ? m[i] : m[src + (i - dst)] |} + } + + func map_copy(m1: Map[Int, E], m2: Map[Int, E], src: Int, dst: Int, len: Int) + returns (res: Map[Int, E]) + { + {| i: Int :: dst <= i < dst + len ? m2[src + (i - dst)] : m1[i] |} + } + + lemma set_of_map_equal(m1: Map[Int, E], m2: Map[Int, E], i1: Int, i2: Int, len: Int) + requires forall j: Int :: {m1[j]} i1 <= j < i1 + len ==> m1[j] == m2[j + (i2 - i1)] + requires injective(m1, i1, i1 + len) && injective(m2, i2, i2 + len) + ensures set_of_map(m1, i1, i1 + len) == set_of_map(m2, i2, i2 + len) + { + if (0 < len) { + set_of_map_equal(m1, m2, i1 + 1, i2 + 1, len - 1); + } + } + + lemma frame_set_of_map(m: Map[Int, E], i: Int, j: Int) + requires i <= j + requires injective(m, i, j) + ensures forall i1: Int, k: E :: {set_of_map(m[i1 := k], i, j)} + i1 < i || j <= i1 ==> set_of_map(m, i, j) == set_of_map(m[i1 := k], i, j) + { + + } + + // Shift a[src..src+len] to a[dst..dst+len] + proc arr_shift(a: T, src: Int, dst: Int, len: Int, implicit ghost amap: Map[Int, E]) + requires arr(a, amap) + requires 0 <= src <= src + len <= length(a) && 0 <= dst <= dst + len <= length(a) + ensures arr(a, map_shift(amap, src, dst, len)) + { + if (src < dst) { + var i: Int := len - 1; + + while (i >= 0) + invariant arr(a, map_shift(amap, src + i + 1, dst + i + 1, len - i - 1)) + invariant src < dst + invariant 0 <= src <= src + len <= length(a) + invariant 0 <= dst <= dst + len <= length(a) + invariant -1 <= i < len + { + unfold arr(a, map_shift(amap, src + i + 1, dst + i + 1, len - i - 1)); + var tmp: E := loc(a, src + i).value; + loc(a, dst + i).value := tmp; + ghost var m : Map[Int, E] = 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)); + } + } else if (src > dst) { + var i: Int := 0; + while (i < len) + invariant arr(a, map_shift(amap, src, dst, i)) + invariant src > dst + invariant 0 <= src <= src + len <= length(a) + invariant 0 <= dst <= dst + len <= length(a) + invariant 0 <= i <= len + { + unfold arr(a, map_shift(amap, src, dst, i)); + var tmp: E := loc(a, src + i).value; + loc(a, dst + i).value := tmp; + ghost var m : Map[Int, E] = 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)); + } + } + } + + // Copy a[src..src+len] to b[dst..dst+len] + proc arr_copy(a: T, b: T, src: Int, dst: Int, len: Int, implicit ghost amap: Map[Int, E], implicit ghost bmap: Map[Int, E] ) + requires arr(a, amap) && arr(b, bmap) + requires 0 <= src <= src + len <= length(a) + requires 0 <= dst <= dst + len <= length(b) + ensures arr(a, amap) && arr(b, map_copy(bmap, amap, src, dst, len)) + { + var i: Int := 0; + + while (i < len) + invariant arr(a, amap) && arr(b, map_copy(bmap, amap, src, dst, i)) + invariant 0 <= i <= len + invariant 0 <= src <= src + len <= length(a) + invariant 0 <= dst <= dst + len <= length(b) + { + unfold arr(a, amap); + var tmp: E := loc(a, src + i).value; + fold arr(a, amap); + unfold arr(b, map_copy(bmap, amap, src, dst, i)); + loc(b, dst + i).value := tmp; + ghost var m: Map[Int, E] = 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)); + } + } + + + /* + func sorted_map_seg(m: Map[Int, E], i: Int, j: Int) returns (res: Bool) + { + forall i1: Int, i2: Int :: {m[i1], m[i2]} i <= i1 && i1 < i2 && i2 < j ==> lt(m[i1], m[i2]) + } + + lemma sorted_injective() + ensures forall m: Map[Int, E], i: Int, j: Int :: {sorted_map_seg(m, i, j)} + sorted_map_seg(m, i, j) ==> injective(m, i, j) + { } + + lemma not_in_sorted_seg(m: Map[Int, E], i: Int, j: Int, k: E) + requires sorted_map_seg(m, i, j) + ensures i >= j || lt(k, m[i]) || lt(m[j-1], k) ==> k !in set_of_map(m, i, j) + { + } + + + auto lemma map_find_content_set() + ensures forall m: Map[Int, E], i: Int, j: Int, k: E :: {sorted_map_seg(m, i, j), map_find(m, i, j, k)} + i <= j && sorted_map_seg(m, i, j) ==> + k !in set_of_map(m, i, map_find(m, i, j, k)) && + k !in set_of_map(m, map_find(m, i, j, k) + 1, j) + { } + + lemma map_find_in_set(m: Map[Int, E], i: Int, j: Int, k: E) + requires i <= j + requires sorted_map_seg(m, i, j) + ensures k in set_of_map(m, i, j) ==> map_find(m, i, j, k) < j && m[map_find(m, i, j, k)] == k + ensures k !in set_of_map(m, i, j) ==> map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)]) + { + //map_find_content_set(m, i, j, k); + } + + lemma map_insert_content_set(m: Map[Int, E], m1: Map[Int, E], idx: Int, k: E, len: Int, new_len: Int) + //requires sorted_map_seg(m, 0, len) + requires injective(m, 0, len) + requires idx == map_find(m, 0, len, k) + requires 0 <= idx <= len + requires k in set_of_map(m, 0, len) ==> new_len == len && m1 == m + requires k !in set_of_map(m, 0, len) ==> new_len == len + 1 && m1 == map_shift(m, idx, idx + 1, len - idx)[idx := k] + ensures set_of_map(m1, 0, new_len) == set_of_map(m, 0, len) ++ {| k |} + { + if (m[idx] == k && idx < len) { + //in_set_of_map(m, 0, len); + return; + } + //assume false; + var ms: Map[Int, E] := map_shift(m, idx, idx + 1, len - idx); + + // prove set_of_map(m, 0, len) == set_of_map(ms, 0, idx) ++ set_of_array(ms, idx + 1, len + 1); + + //set_of_map_split(m, 0, idx, len); + set_of_map_equal(m, ms, 0, 0, idx); + set_of_map_equal(m, ms, idx, idx + 1, len - idx); + + // prove set_of_map(m1, 0, new_len) == set_of_array(ms, 0, idx) ++ {k} ++ set_of_map(ms, idx + 1, len + 1) + //frame_set_of_map(ms, 0, idx); + //frame_set_of_map(ms, idx + 1, len + 1); + set_of_map_split(m1, 0, idx, len + 1); + }*/ + + /* + func sorted_map_seg(m: Map[Int, E], i: Int, j: Int) returns (res: Bool) + { + forall i1: Int, i2: Int :: {m[i1], m[i2]} i <= i1 && i1 < i2 && i2 < j ==> lt(m[i1], m[i2]) + } + + func map_find(m: Map[Int, E], i: Int, j: Int, k: E) returns (idx: Int) + /*ensures + i <= j && sorted_map_seg(m, i, j) ==> + i <= idx <= j && + (m[idx] == k || idx == j || lt(k, m[idx])) && + (i < idx ==> lt(m[idx - 1], k))*/ + { + i < j && lt(m[i], k) ? map_find(m, i + 1, j, k) : i + } + + lemma map_find_spec(m: Map[Int, E], i: Int, j: Int, k: E) + ensures i <= j && sorted_map_seg(m, i, j) ==> + i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && + (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && + (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) + { + if (i < j && sorted_map_seg(m, i, j)) { + map_find_spec(m, i+1, j, k); + } + } + + auto lemma map_find_spec_auto() + ensures forall m: Map[Int, E], i: Int, j: Int, k: E :: i <= j && sorted_map_seg(m, i, j) ==> + i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && + (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && + (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) + { + assert forall m: Map[Int, E], i: Int, j: Int, k: E :: i <= j && sorted_map_seg(m, i, j) ==> + i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && + (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && + (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) with { + map_find_spec(m, i, j, k); + } + } + + auto lemma sorted_injective() + ensures forall m: Map[Int, E], i: Int, j: Int :: {sorted_map_seg(m, i, j)} + sorted_map_seg(m, i, j) ==> injective(m, i, j) + { } + + lemma map_delete_content_set(m: Map[Int, E], m1: Map[Int, E], len: Int, new_len: Int, idx: Int, k: E) + requires sorted_map_seg(m, 0, len) + requires idx == map_find(m, 0, len, k) + requires 0 <= idx <= len + requires k !in set_of_map(m, 0, len) ==> new_len == len && m1 == m + requires k in set_of_map(m, 0, len) ==> new_len == len - 1 && m1 == map_shift(m, idx + 1, idx, len - (idx + 1)) + ensures set_of_map(m1, 0, new_len) == set_of_map(m, 0, len) -- {|k|} + { + //map_find_content_set(m, 0, len, idx, k); + //set_of_map_split(m, 0, idx, len); + + if (idx == len || m[idx] != k) { + return; + } + + // prove: set_of_map(m, 0, len) -- {k} == set_of_map(m1, 0, idx - 1) ++ set_of_map(m1, idx - 1, len - 1) + set_of_map_equal(m, m1, 0, 0, idx); + set_of_map_equal(m, m1, idx + 1, idx, len - (idx + 1)); + + //not_in_sorted_seg(m, 0, idx - 1, k); + //not_in_sorted_seg(m, idx + 1, len, k); + + set_of_map_split(m1, 0, idx, len - 1); + }*/ + +} \ No newline at end of file diff --git a/test/arrays/array_util.rav b/test/arrays/array_util.rav deleted file mode 100644 index 4890447..0000000 --- a/test/arrays/array_util.rav +++ /dev/null @@ -1,448 +0,0 @@ -interface Array { - rep type T - type E - - func loc(a: T, i: Int) returns (r: Ref) - func length(a: T) returns (l: Int) - func first(r: Ref) returns (a: T) - func second(r: Ref) returns (i: Int) - - auto axiom all_diff() - ensures forall a:T, i: Int :: {loc(a, i)} first(loc(a, i)) == a && second(loc(a, i)) == i - - auto axiom len_nonneg() - 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] { - import K.lt - - interface A : Array { - type E = K - } - - 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]) - requires i <= j - { - i < j ? {| m[i] |} ++ set_of_map(m, i + 1, j) : {||} - } - - lemma extend_right(m: Map[Int, K], i: Int, j: Int) - requires i <= j - ensures set_of_map(m, i, j) ++ {| m[j] |} == set_of_map(m, i, j + 1) - { - if (i < j) { - extend_right(m, i + 1, j); - } - } - - lemma in_set_of_map(m: Map[Int, K], i: Int, j: Int) - requires i <= j - ensures forall k: Int :: {m[k]} i <= k < j ==> m[k] in set_of_map(m, i, j) - { - if (i < j) { - in_set_of_map(m, i + 1, j); - } - } - - lemma set_of_map_split(m: Map[Int, K], i: Int, j: Int, k: Int) - requires i <= j <= k - ensures set_of_map(m, i, k) == set_of_map(m, i, j) ++ set_of_map(m, j, k) - { - if (j < k) { - extend_right(m, i, j); - set_of_map_split(m, i, j + 1, k); - } - } - - lemma set_of_map_equal(m1: Map[Int, K], m2: Map[Int, K], i1: Int, i2: Int, len: Int) - requires forall j: Int :: {m1[j]} i1 <= j < i1 + len ==> m1[j] == m2[j + (i2 - i1)] - ensures set_of_map(m1, i1, i1 + len) == set_of_map(m2, i2, i2 + len) - { - if (0 < len) { - set_of_map_equal(m1, m2, i1 + 1, i2 + 1, len - 1); - } - } - - lemma frame_set_of_map(m: Map[Int, K], i: Int, j: Int) - requires i <= j - ensures forall i1: Int, k: K :: {set_of_map(m[i1 := k], i, j)} - i1 < i || j <= i1 ==> set_of_map(m, i, j) == set_of_map(m[i1 := k], i, j) - { - if (i < j) { - frame_set_of_map(m, i + 1, j); - } - } - - func sorted_map_seg(m: Map[Int, K], i: Int, j: Int) returns (res: Bool) - { - forall i1: Int, i2: Int :: {m[i1], m[i2]} i <= i1 && i1 < i2 && i2 < j ==> lt(m[i1], m[i2]) - } - - - lemma not_in_sorted_seg(m: Map[Int, K], i: Int, j: Int, k: K, implicit ghost c: Set[K]) - requires sorted_map_seg(m, i, j) && c == set_of_map(m, i, j) - ensures i >= j || lt(k, m[i]) || lt(m[j-1], k) ==> k !in c - { - if (i >= j) return; - - if (lt(m[j - 1], k)) { - extend_right(m, i, j - 1); - not_in_sorted_seg(m, i, j - 1, k); - return; - } - - if (lt(k, m[i])) { - not_in_sorted_seg(m, i + 1, j, k); - return; - } - - } - - func map_find(m: Map[Int, K], i: Int, j: Int, k: K) returns (idx: Int) - /*ensures - i <= j && sorted_map_seg(m, i, j) ==> - i <= idx <= j && - (m[idx] == k || idx == j || lt(k, m[idx])) && - (i < idx ==> lt(m[idx - 1], k))*/ - { - i < j && lt(m[i], k) ? map_find(m, i + 1, j, k) : i - } - - lemma map_find_spec(m: Map[Int, K], i: Int, j: Int, k: K) - ensures i <= j && sorted_map_seg(m, i, j) ==> - i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && - (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && - (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) - { - if (i < j && sorted_map_seg(m, i, j)) { - map_find_spec(m, i+1, j, k); - } - } - - auto lemma map_find_spec_auto() - ensures forall m: Map[Int, K], i: Int, j: Int, k: K :: i <= j && sorted_map_seg(m, i, j) ==> - i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && - (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && - (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) - { - assert forall m: Map[Int, K], i: Int, j: Int, k: K :: i <= j && sorted_map_seg(m, i, j) ==> - i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && - (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && - (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) with { - map_find_spec(m, i, j, k); - } - } - - - lemma map_find_in_set(m: Map[Int, K], i: Int, j: Int, k: K) - requires i <= j - requires sorted_map_seg(m, i, j) - ensures k in set_of_map(m, i, j) ==> map_find(m, i, j, k) < j && m[map_find(m, i, j, k)] == k - ensures k !in set_of_map(m, i, j) ==> map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)]) - { - val idx: Int := map_find(m, i, j, k); - map_find_content_set(m, i, j, idx, k); - set_of_map_split(m, i, idx, j); - } - - lemma map_find_content_set(m: Map[Int, K], i: Int, j: Int, idx: Int, k: K) - requires i <= j - requires sorted_map_seg(m, i, j) - requires idx == map_find(m, i, j, k) - ensures k !in set_of_map(m, i, idx) - ensures k !in set_of_map(m, idx + 1, j) - { - // prove k !in set_of_map(a, 0, idx) - not_in_sorted_seg(m, i, idx, k); - // prove: k !in set_of_map(a, idx + 1, len) - not_in_sorted_seg(m, idx + 1, j, k); - } - - - func map_shift(m: Map[Int, K], src: Int, dst: Int, len: Int) - returns (res: Map[Int, K]) - { - {| i: Int :: i < dst || dst + len <= i ? m[i] : m[src + (i - dst)] |} - } - - func map_copy(m1: Map[Int, K], m2: Map[Int, K], src: Int, dst: Int, len: Int) - returns (res: Map[Int, K]) - { - {| i: Int :: dst <= i < dst + len ? m2[src + (i - dst)] : m1[i] |} - } - - lemma map_insert_content_set(m: Map[Int, K], m1: Map[Int, K], idx: Int, k: K, len: Int, new_len: Int) - requires sorted_map_seg(m, 0, len) - requires idx == map_find(m, 0, len, k) - requires 0 <= idx <= len - requires k in set_of_map(m, 0, len) ==> new_len == len && m1 == m - requires k !in set_of_map(m, 0, len) ==> new_len == len + 1 && m1 == map_shift(m, idx, idx + 1, len - idx)[idx := k] - ensures set_of_map(m1, 0, new_len) == set_of_map(m, 0, len) ++ {| k |} - { - if (m[idx] == k && idx < len) { - in_set_of_map(m, 0, len); - return; - } - - var ms: Map[Int, K] := map_shift(m, idx, idx + 1, len - idx); - - // prove set_of_map(m, 0, len) == set_of_map(ms, 0, idx) ++ set_of_array(ms, idx + 1, len + 1); - - set_of_map_split(m, 0, idx, len); - set_of_map_equal(m, ms, 0, 0, idx); - set_of_map_equal(m, ms, idx, idx + 1, len - idx); - - // prove set_of_map(m1, 0, new_len) == set_of_array(ms, 0, idx) ++ {k} ++ set_of_map(ms, idx + 1, len + 1) - frame_set_of_map(ms, 0, idx); - frame_set_of_map(ms, idx + 1, len + 1); - set_of_map_split(m1, 0, idx, len + 1); - } - - lemma map_delete_content_set(m: Map[Int, K], m1: Map[Int, K], len: Int, new_len: Int, idx: Int, k: K) - requires sorted_map_seg(m, 0, len) - requires idx == map_find(m, 0, len, k) - requires 0 <= idx <= len - requires k !in set_of_map(m, 0, len) ==> new_len == len && m1 == m - requires k in set_of_map(m, 0, len) ==> new_len == len - 1 && m1 == map_shift(m, idx + 1, idx, len - (idx + 1)) - ensures set_of_map(m1, 0, new_len) == set_of_map(m, 0, len) -- {|k|} - { - map_find_content_set(m, 0, len, idx, k); - set_of_map_split(m, 0, idx, len); - - if (idx == len || m[idx] != k) { - return; - } - - // prove: set_of_map(m, 0, len) -- {k} == set_of_map(m1, 0, idx - 1) ++ set_of_map(m1, idx - 1, len - 1) - set_of_map_equal(m, m1, 0, 0, idx); - set_of_map_equal(m, m1, idx + 1, idx, len - (idx + 1)); - - not_in_sorted_seg(m, 0, idx - 1, k); - not_in_sorted_seg(m, idx + 1, len, k); - - set_of_map_split(m1, 0, idx, len - 1); - } - - // Shift a[src..src+len] to a[dst..dst+len] - proc arr_shift(a: A, src: Int, dst: Int, len: Int, implicit ghost amap: Map[Int, K]) - requires arr(a, amap) - requires 0 <= src <= src + len <= A.length(a) && 0 <= dst <= dst + len <= A.length(a) - ensures arr(a, map_shift(amap, src, dst, len)) - { - if (src < dst) { - var i: Int := len - 1; - - while (i >= 0) - invariant arr(a, map_shift(amap, src + i + 1, dst + i + 1, len - i - 1)) - invariant src < dst - invariant 0 <= src <= src + len <= A.length(a) - invariant 0 <= dst <= dst + len <= A.length(a) - invariant -1 <= i < len - { - 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; - 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)); - } - } else if (src > dst) { - var i: Int := 0; - while (i < len) - invariant arr(a, map_shift(amap, src, dst, i)) - invariant src > dst - invariant 0 <= src <= src + len <= A.length(a) - invariant 0 <= dst <= dst + len <= A.length(a) - invariant 0 <= i <= len - { - 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; - 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)); - } - } - } - - - // Copy a[src..src+len] to b[dst..dst+len] - proc arr_copy(a: A, b: A, src: Int, dst: Int, len: Int, implicit ghost amap: Map[Int, K], implicit ghost bmap: Map[Int, K] ) - requires arr(a, amap) && arr(b, bmap) - requires 0 <= src <= src + len <= A.length(a) - requires 0 <= dst <= dst + len <= A.length(b) - ensures arr(a, amap) && arr(b, map_copy(bmap, amap, src, dst, len)) - { - var i: Int := 0; - - while (i < len) - invariant arr(a, amap) && arr(b, map_copy(bmap, amap, src, dst, i)) - invariant 0 <= i <= len - invariant 0 <= src <= src + len <= A.length(a) - invariant 0 <= dst <= dst + len <= A.length(b) - { - unfold arr(a, amap); - var tmp: K := A.loc(a, src + i).A.value; - 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]) - { - 0 <= len <= A.length(a) && arr(a, m) && sorted_map_seg(m, 0, len) - } - - // Find key `k` in sorted array segment `a[0..len]` using binary search - proc arr_find(a: A, len: Int, k: K, implicit ghost m: Map[Int, K]) - returns (found: Bool, idx: Int) - requires sorted_array_with_content(a, len, m) - requires 0 <= len <= A.length(a) - ensures sorted_array_with_content(a, len, m) - // what we actually care about - ensures idx == map_find(m, 0, len, k) - ensures found == (k in set_of_map(m, 0, len)) - { - var lo: Int := 0; - var hi: Int := len; - - while (hi != lo) - invariant sorted_array_with_content(a, len, m) - // what we actually care about - invariant 0 <= lo <= hi <= len <= A.length(a) - invariant hi == len || m[lo] == k || lt(k, m[hi]) - invariant 0 < lo ==> lt(m[lo - 1], k) - invariant hi < len - 1 ==> lt(k, m[hi + 1]) - { - unfold sorted_array_with_content(a, len, m); - unfold arr(a, m); - var mid: Int := (hi + lo) / 2; - var amid: K := A.loc(a, mid).A.value; - var cmp: Int := K.compare(k, amid); - if (cmp < 0) { - hi := mid; // look in first half - } else if (cmp > 0) { - lo := mid + 1; // look in second half - } else { - // found it - hi := mid; - lo := mid; - } - fold arr(a, m); - fold sorted_array_with_content(a, len, m); - } - - idx := lo; - - if (idx == len) { - found := false; - } else { - unfold sorted_array_with_content(a, len, m); - unfold arr(a, m); - var alo: K := A.loc(a, lo).A.value; - found := !lt(k, alo); - fold arr(a, m); - fold sorted_array_with_content(a, len, m); - } - - unfold sorted_array_with_content(a, len, m); - map_find_in_set(m, 0, len, k); - fold sorted_array_with_content(a, len, m); - } - - // Given a sorted array segment `a[0..len]`, - // insert `k` into `a[0..len+1]` while preserving sortedness. - // If `k` is already contained in `a[0..len]`, then do not modify `a`. - proc arr_insert(a: A, k: K, len: Int, implicit ghost m: Map[Int, K]) - returns (idx: Int, new_len: Int, implicit ghost m1: Map[Int, K]) - requires sorted_array_with_content(a, len, m) - requires 0 <= len < A.length(a) - ensures sorted_array_with_content(a, new_len, m1) - ensures idx == map_find(m, 0, len, k) - ensures k in set_of_map(m, 0, len) ==> new_len == len && m1 == m - ensures k !in set_of_map(m, 0, len) ==> new_len == len + 1 && m1 == map_shift(m, idx, idx + 1, len - idx)[idx := k] - { - // find position for insertion - var i: Int; - var found: Bool; - found, i := arr_find(a, len, k, m); - - unfold sorted_array_with_content(a, len, m); - map_find_in_set(m, 0, len, k); - fold sorted_array_with_content(a, len, m); - - // k already in C? - if (found) return i, len, m; - - unfold sorted_array_with_content(a, len, m); - arr_shift(a, i, i + 1, len - i, m); - - unfold arr(a, map_shift(m, i, i + 1, len - i)); - A.loc(a, i).A.value := k; - m1 := map_shift(m, i, i + 1, len - i)[i := k]; - fold arr(a, m1); - //pure assert a.map == ms[i := k]; - fold sorted_array_with_content(a, len + 1, m1); - - return i, len + 1, m1; - } - - // Given a sorted array segment `a[0..len]`, - // delete `k` from the segment while preserving sortedness. - // If `k` is already contained in `a[0..len]`, then do not modify `a`. - proc arr_delete(a: A, k: K, len: Int, implicit ghost m: Map[Int, K]) - returns (new_len: Int, idx: Int, implicit ghost m1: Map[Int, K]) - requires 0 <= len <= A.length(a) - requires sorted_array_with_content(a, len, m) - ensures sorted_array_with_content(a, new_len, m1) - ensures idx == map_find(m, 0, len, k) - ensures k !in set_of_map(m, 0, len) ==> new_len == len && m1 == m - ensures k in set_of_map(m, 0, len) ==> new_len == len - 1 && m1 == map_shift(m, idx + 1, idx, len - (idx + 1)) - { - // find position for insertion - var found: Bool; - found, idx := arr_find(a, len, k, m); - - unfold sorted_array_with_content(a, len, m); - map_find_in_set(m, 0, len, k); - fold sorted_array_with_content(a, len, m); - - // k !in C? - if (!found) { - return len, idx, m; - } - - // shift array entries a[i+1..len] by 1 entry to the left - unfold sorted_array_with_content(a, len, m); - arr_shift(a, idx + 1, idx, len - (idx + 1), m); - m1 := map_shift(m, idx + 1, idx, len - (idx + 1)); - fold sorted_array_with_content(a, len - 1, m1); - return len - 1, idx, m1; - } - -} \ No newline at end of file diff --git a/test/arrays/ordered_array.rav b/test/arrays/ordered_array.rav new file mode 100644 index 0000000..2d5f712 --- /dev/null +++ b/test/arrays/ordered_array.rav @@ -0,0 +1,270 @@ +include "array.rav" + +interface OrderedArray[E: Library.OrderedType] : Array { + import E.lt + + func sorted_map_seg(m: Map[Int, E], i: Int, j: Int) returns (res: Bool) + { + forall i1: Int, i2: Int :: {m[i1], m[i2]} i <= i1 && i1 < i2 && i2 < j ==> lt(m[i1], m[i2]) + } + + pred sorted_array_with_content(a: T, len: Int; m: Map[Int, E]) + { + 0 <= len <= length(a) && arr(a, m) && sorted_map_seg(m, 0, len) + } + + auto lemma sorted_injective() + ensures forall m: Map[Int, E], i: Int, j: Int :: {sorted_map_seg(m, i, j)} + sorted_map_seg(m, i, j) ==> injective(m, i, j) + { } + + /*lemma not_in_sorted_seg(m: Map[Int, E], i: Int, j: Int, k: E, implicit ghost c: Set[E]) + requires sorted_map_seg(m, i, j) && c == set_of_map(m, i, j) + ensures i >= j || lt(k, m[i]) || lt(m[j-1], k) ==> k !in c + { + /*if (i >= j) return; + + if (lt(m[j - 1], k)) { + extend_right(m, i, j - 1); + not_in_sorted_seg(m, i, j - 1, k); + return; + } + + if (lt(k, m[i])) { + not_in_sorted_seg(m, i + 1, j, k); + return; + } + */ + }*/ + + func map_find(m: Map[Int, E], i: Int, j: Int, k: E) returns (idx: Int) + /*ensures + i <= j && sorted_map_seg(m, i, j) ==> + i <= idx <= j && + (m[idx] == k || idx == j || lt(k, m[idx])) && + (i < idx ==> lt(m[idx - 1], k))*/ + { + i < j && lt(m[i], k) ? map_find(m, i + 1, j, k) : i + } + + lemma map_find_spec(m: Map[Int, E], i: Int, j: Int, k: E) + ensures i <= j && sorted_map_seg(m, i, j) ==> + i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && + (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && + (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) + { + if (i < j && sorted_map_seg(m, i, j)) { + map_find_spec(m, i+1, j, k); + } + } + + auto lemma map_find_spec_auto() + ensures forall m: Map[Int, E], i: Int, j: Int, k: E :: i <= j && sorted_map_seg(m, i, j) ==> + i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && + (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && + (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) + { + assert forall m: Map[Int, E], i: Int, j: Int, k: E :: i <= j && sorted_map_seg(m, i, j) ==> + i <= map_find(m, i, j, k) && map_find(m, i, j, k) <= j && + (m[map_find(m, i, j, k)] == k || map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)])) && + (i < map_find(m, i, j, k) ==> lt(m[map_find(m, i, j, k) - 1], k)) with { + map_find_spec(m, i, j, k); + } + } + + + auto lemma map_find_content_set() + ensures forall m: Map[Int, E], i: Int, j: Int, k: E :: {sorted_map_seg(m, i, j), map_find(m, i, j, k)} + i <= j && sorted_map_seg(m, i, j) ==> + k !in set_of_map(m, i, map_find(m, i, j, k)) && + k !in set_of_map(m, map_find(m, i, j, k) + 1, j) + { } + + /*lemma map_find_in_set(m: Map[Int, E], i: Int, j: Int, k: E) + requires i <= j + requires sorted_map_seg(m, i, j) + ensures k in set_of_map(m, i, j) ==> map_find(m, i, j, k) < j && m[map_find(m, i, j, k)] == k + ensures k !in set_of_map(m, i, j) ==> map_find(m, i, j, k) == j || lt(k, m[map_find(m, i, j, k)]) + { + //map_find_content_set(m, i, j, k); + }*/ + + + lemma map_insert_content_set(m: Map[Int, E], m1: Map[Int, E], idx: Int, k: E, len: Int, new_len: Int) + requires sorted_map_seg(m, 0, len) + //requires injective(m, 0, len) + requires idx == map_find(m, 0, len, k) + requires 0 <= idx <= len + requires k in set_of_map(m, 0, len) ==> new_len == len && m1 == m + requires k !in set_of_map(m, 0, len) ==> new_len == len + 1 && m1 == map_shift(m, idx, idx + 1, len - idx)[idx := k] + ensures set_of_map(m1, 0, new_len) == set_of_map(m, 0, len) ++ {| k |} + { + if (m[idx] == k && idx < len) { + //in_set_of_map(m, 0, len); + return; + } + var ms: Map[Int, E] := map_shift(m, idx, idx + 1, len - idx); + + // prove set_of_map(m, 0, len) == set_of_map(ms, 0, idx) ++ set_of_array(ms, idx + 1, len + 1); + set_of_map_split(m, 0, idx, len); + set_of_map_equal(m, ms, 0, 0, idx); + set_of_map_equal(m, ms, idx, idx + 1, len - idx); + // prove set_of_map(m1, 0, new_len) == set_of_array(ms, 0, idx) ++ {k} ++ set_of_map(ms, idx + 1, len + 1) + inverse_update(); + frame_set_of_map(ms, 0, idx); + frame_set_of_map(ms, idx + 1, len + 1); + set_of_map_split(m1, 0, idx, len + 1); + } + + lemma map_delete_content_set(m: Map[Int, E], m1: Map[Int, E], len: Int, new_len: Int, idx: Int, k: E) + requires sorted_map_seg(m, 0, len) + requires idx == map_find(m, 0, len, k) + requires 0 <= idx <= len + requires k !in set_of_map(m, 0, len) ==> new_len == len && m1 == m + requires k in set_of_map(m, 0, len) ==> new_len == len - 1 && m1 == map_shift(m, idx + 1, idx, len - (idx + 1)) + ensures set_of_map(m1, 0, new_len) == set_of_map(m, 0, len) -- {|k|} + { + //map_find_content_set(m, 0, len, idx, k); + //set_of_map_split(m, 0, idx, len); + + if (idx == len || m[idx] != k) { + return; + } + + // prove: set_of_map(m, 0, len) -- {k} == set_of_map(m1, 0, idx - 1) ++ set_of_map(m1, idx - 1, len - 1) + set_of_map_equal(m, m1, 0, 0, idx); + set_of_map_equal(m, m1, idx + 1, idx, len - (idx + 1)); + + //not_in_sorted_seg(m, 0, idx - 1, k); + //not_in_sorted_seg(m, idx + 1, len, k); + + set_of_map_split(m1, 0, idx, len - 1); + } + + // Find key `k` in sorted array segment `a[0..len]` using binary search + proc arr_find(a: T, len: Int, k: E, implicit ghost m: Map[Int, E]) + returns (found: Bool, idx: Int) + requires sorted_array_with_content(a, len, m) + requires 0 <= len <= length(a) + ensures sorted_array_with_content(a, len, m) + // what we actually care about + ensures idx == map_find(m, 0, len, k) + ensures found == (k in set_of_map(m, 0, len)) + { + var lo: Int := 0; + var hi: Int := len; + + while (hi != lo) + invariant sorted_array_with_content(a, len, m) + // what we actually care about + invariant 0 <= lo <= hi <= len <= length(a) + invariant hi == len || m[lo] == k || lt(k, m[hi]) + invariant 0 < lo ==> lt(m[lo - 1], k) + invariant hi < len - 1 ==> lt(k, m[hi + 1]) + { + unfold sorted_array_with_content(a, len, m); + unfold arr(a, m); + var mid: Int := (hi + lo) / 2; + var amid: E := loc(a, mid).value; + var cmp: Int := E.compare(k, amid); + if (cmp < 0) { + hi := mid; // look in first half + } else if (cmp > 0) { + lo := mid + 1; // look in second half + } else { + // found it + hi := mid; + lo := mid; + } + fold arr(a, m); + fold sorted_array_with_content(a, len, m); + } + + idx := lo; + + if (idx == len) { + found := false; + } else { + unfold sorted_array_with_content(a, len, m); + unfold arr(a, m); + var alo: E := loc(a, lo).value; + found := !lt(k, alo); + fold arr(a, m); + fold sorted_array_with_content(a, len, m); + } + + unfold sorted_array_with_content(a, len, m); + //map_find_in_set(m, 0, len, k); + fold sorted_array_with_content(a, len, m); + } + + // Given a sorted array segment `a[0..len]`, + // insert `k` into `a[0..len+1]` while preserving sortedness. + // If `k` is already contained in `a[0..len]`, then do not modify `a`. + proc arr_insert(a: T, k: E, len: Int, implicit ghost m: Map[Int, E]) + returns (idx: Int, new_len: Int, implicit ghost m1: Map[Int, E]) + requires sorted_array_with_content(a, len, m) + requires 0 <= len < length(a) + ensures sorted_array_with_content(a, new_len, m1) + ensures idx == map_find(m, 0, len, k) + ensures k in set_of_map(m, 0, len) ==> new_len == len && m1 == m + ensures k !in set_of_map(m, 0, len) ==> new_len == len + 1 && m1 == map_shift(m, idx, idx + 1, len - idx)[idx := k] + { + // find position for insertion + var i: Int; + var found: Bool; + found, i := arr_find(a, len, k, m); + + unfold sorted_array_with_content(a, len, m); + //map_find_in_set(m, 0, len, k); + fold sorted_array_with_content(a, len, m); + + // k already in C? + if (found) return i, len, m; + + unfold sorted_array_with_content(a, len, m); + arr_shift(a, i, i + 1, len - i, m); + + unfold arr(a, map_shift(m, i, i + 1, len - i)); + loc(a, i).value := k; + m1 := map_shift(m, i, i + 1, len - i)[i := k]; + fold arr(a, m1); + //pure assert a.map == ms[i := k]; + fold sorted_array_with_content(a, len + 1, m1); + + return i, len + 1, m1; + } + + // Given a sorted array segment `a[0..len]`, + // delete `k` from the segment while preserving sortedness. + // If `k` is already contained in `a[0..len]`, then do not modify `a`. + proc arr_delete(a: T, k: E, len: Int, implicit ghost m: Map[Int, E]) + returns (new_len: Int, idx: Int, implicit ghost m1: Map[Int, E]) + requires 0 <= len <= length(a) + requires sorted_array_with_content(a, len, m) + ensures sorted_array_with_content(a, new_len, m1) + ensures idx == map_find(m, 0, len, k) + ensures k !in set_of_map(m, 0, len) ==> new_len == len && m1 == m + ensures k in set_of_map(m, 0, len) ==> new_len == len - 1 && m1 == map_shift(m, idx + 1, idx, len - (idx + 1)) + { + // find position for insertion + var found: Bool; + found, idx := arr_find(a, len, k, m); + + unfold sorted_array_with_content(a, len, m); + fold sorted_array_with_content(a, len, m); + + // k !in C? + if (!found) { + return len, idx, m; + } + + // shift array entries a[i+1..len] by 1 entry to the left + unfold sorted_array_with_content(a, len, m); + arr_shift(a, idx + 1, idx, len - (idx + 1), m); + m1 := map_shift(m, idx + 1, idx, len - (idx + 1)); + fold sorted_array_with_content(a, len - 1, m1); + return len - 1, idx, m1; + } + +} \ No newline at end of file diff --git a/test/concurrent/templates/bplustree.rav b/test/concurrent/templates/bplustree.rav index 034836f..9720566 100644 --- a/test/concurrent/templates/bplustree.rav +++ b/test/concurrent/templates/bplustree.rav @@ -1,5 +1,5 @@ include "give-up.rav" -include "../../arrays/array_util.rav" +include "../../arrays/ordered_array.rav" interface BPlusTree[O: Library.OrderedType] : NodeImpl { @@ -18,14 +18,14 @@ interface BPlusTree[O: Library.OrderedType] : NodeImpl { import Flow_K._ import Multiset_K.elem - interface AU = ArrayUtil[O] + interface AK = OrderedArray[O] - import AU._ - - interface AN : Array { - type E = Ref + module RefType : Library.Type { + rep type T = Ref } + interface AN = Array[RefType] + // Width parameter of the B-tree val b: Int @@ -36,7 +36,7 @@ interface BPlusTree[O: Library.OrderedType] : NodeImpl { field len: Int field rangeLb: KOption field rangeUb: KOption - field keys: A.T + field keys: AK.T field ptrs: AN.T func le(ko: KOption, k: K) returns (res : Bool) @@ -49,38 +49,40 @@ interface BPlusTree[O: Library.OrderedType] : NodeImpl { 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) + func flow_int_of(n: Ref, l: Int, 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 */ |}, + {| np: Ref :: 0 <= AN.inverse(cmap, 0, l, np) < l ? + {| k: K :: (0 < AN.inverse(cmap, 0, l, np) ==> O.le(kmap[AN.inverse(cmap, 0, l, np) - 1], k)) && + O.lt(k, kmap[AN.inverse(cmap, 0, l, np)]) ? 1 : 0 |} : Multiset_K.id |}, {| 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] :: + exists l: Int, lb: KOption, ub: KOption, ks: AK.T, chlds: AN.T, kmap: Map[Int, K], cmap: Map[Int, Ref] :: 0 <= l && l < 2*b - && A.length(ks) == 2*b + && AK.length(ks) == 2*b && AN.length(chlds) == 2*b // Definition of flow interface - && flow_int == flow_int_of(n, lb, ub, kmap, cmap) + && flow_int == flow_int_of(n, l, lb, ub, kmap, cmap) // Definition of contents - && c == (cmap[0] == null ? /* Leaf */ AU.set_of_map(kmap, 0, l) : {||}) + && c == (cmap[0] == null ? /* Leaf */ AK.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)) + && (forall i: Int :: {cmap[i]} 0 <= i <= l ==> n != cmap[i]) + && AN.injective(cmap, 0, l) + // Internal nodes don't point to null + && cmap[0] != null ==> (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, rangeUb, ub, 1.0) && own(n, keys, ks, 1.0) - && AU.sorted_array_with_content(ks, l, kmap) + && AK.sorted_array_with_content(ks, l, kmap) && own(n, ptrs, chlds, 1.0) && AN.arr(chlds, cmap) } @@ -91,12 +93,34 @@ interface BPlusTree[O: Library.OrderedType] : NodeImpl { 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 ka: AK.T; + ka := AK.alloc(2*b, AK.default); var pa: AN.T; pa := AN.alloc(2*b, null); r := new(len: 0, rangeLb: none, rangeUb: none, keys: ka, ptrs: pa); + assert own(r, len, 0, 1.0); + + val cmap: Map[Int, Ref] = {| i: Int :: 0 <= i < 2*b ? null : AN.default |}; + val kmap: Map[Int, K] = AK.default_map; + + assert AN.arr(pa, cmap); + fold AK.sorted_array_with_content(ka, 0, AK.default_map); + assert own(r, len, 0, 1.0) + && own(r, rangeLb, none, 1.0) + && own(r, rangeUb, none, 1.0) + && own(r, keys, ka, 1.0) + && AK.sorted_array_with_content(ka, 0, AK.default_map) + && own(r, ptrs, pa, 1.0) + && AN.arr(pa, cmap); + assert (forall i: Int, j: Int :: {kmap[i], kmap[j]} 0 <= i < j < 0 ==> O.lt(kmap[i], kmap[j])); + // Keys are within range + assert (0 > 0 ==> le(none, kmap[0]) && lt(kmap[0-1], none)); + // Consistency of cmap + assert (forall i: Int :: {cmap[i]} 0 <= i < 0 ==> r != cmap[i]); + assert AN.injective(cmap, 0, 0); + assert cmap[0] != null ==> (forall i: Int :: {cmap[i]} 0 <= i <= 0 ==> cmap[i] != null); + fold node(r, {||}, Flow_K.int({| l: Ref :: l == r ? Multiset_K.fromSet(keyspace) : Multiset_K.id |}, zeroFlow, {| r |})); }