Skip to content

Commit

Permalink
progress on pblustree
Browse files Browse the repository at this point in the history
  • Loading branch information
@wies
wies committed Oct 25, 2024
1 parent 825047d commit e3b73ac
Show file tree
Hide file tree
Showing 4 changed files with 681 additions and 469 deletions.
366 changes: 366 additions & 0 deletions test/arrays/array.rav
View file
Original file line number Diff line number Diff line change
@@ -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);
}*/

}
Loading

0 comments on commit e3b73ac

Please sign in to comment.