diff options
author | Anthony Wang | 2025-03-15 19:16:52 -0400 |
---|---|---|
committer | Anthony Wang | 2025-03-15 19:16:52 -0400 |
commit | 0addc7bfc88690d51f57e33f5ec5f0719eade1ce (patch) | |
tree | 16cd995891895322cc8012ea0293d878c6bae55c | |
parent | 5e5535142f65861af1223ff6f7ca81f0e9d18cd2 (diff) |
Yay it almost works
-rw-r--r-- | fenwick.dfy | 235 |
1 files changed, 181 insertions, 54 deletions
diff --git a/fenwick.dfy b/fenwick.dfy index ae0da2a..a30f32b 100644 --- a/fenwick.dfy +++ b/fenwick.dfy @@ -20,16 +20,6 @@ lemma lsb_correct(i: nat) { } -lemma lsb_shared_par(i: nat) - requires i > 0 - requires i - lsb(i) > i + lsb(i) - lsb(i + lsb(i)) - ensures i - lsb(i) + lsb(i - lsb(i)) == i + lsb(i) -{ - if i % 2 == 0 { - lsb_shared_par(i / 2); - } -} - // Used for termination in update lemma lsb_add(i: nat) requires i > 0 @@ -48,6 +38,26 @@ lemma lsb_next(i: nat) { } +// Used for correctness in constructor +lemma lsb_no_par(i: nat, j: nat) + requires 0 < j < i + requires i - lsb(i) == i + lsb(i) - lsb(i + lsb(i)) + ensures j + lsb(j) != i + lsb(i) +{ + lsb_add(j); +} + +// Used for correctness in constructor +lemma lsb_shared_par(i: nat) + requires i > 0 + requires i - lsb(i) > i + lsb(i) - lsb(i + lsb(i)) + ensures i - lsb(i) + lsb(i - lsb(i)) == i + lsb(i) +{ + if i % 2 == 0 { + lsb_shared_par(i / 2); + } +} + // Pretty trivial recursive sum // opaque for perf reasons since we always use split or split3 to reason about it // https://dafny.org/latest/VerificationOptimization/VerificationOptimization#opaque-definitions @@ -101,71 +111,189 @@ class fenwick { |A| == N && F.Length == N + 1 && forall i :: 0 < i <= N ==> F[i] == sum(A[i - lsb(i)..i]) } - lemma blah(i: nat, j: nat) - requires N == |A| == F.Length - 1 - requires 0 < i < j <= N - requires i + lsb(i) == j - requires i - lsb(i) > j - lsb(j) - requires forall j :: 0 < j <= i <= N ==> F[j] == sum(A[j - lsb(j)..j]) - requires forall j :: 0 < j < i && i <= j + lsb(j) <= N ==> lsb(j) <= lsb(j + lsb(j)) && F[j + lsb(j)] == A[j + lsb(j) - 1] + sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) - ensures i - lsb(i) + lsb(i - lsb(i)) == j - // ensures 0 < i - lsb(i) < i && i <= i - lsb(i) + lsb(i - lsb(i)) <= N - // ensures F[j] == A[j - 1] + sum(A[j - lsb(j)..i - lsb(i)]) - // ensures F[i] == sum(A[i - lsb(i)..i]) - // ensures F[j] + F[i] == A[j - 1] + sum(A[j - lsb(j)..i - lsb(i)]) + sum(A[i - lsb(i)..i]) - ensures F[j] + F[i] == A[j - 1] + sum(A[j - lsb(j)..i]) - { - lsb_shared_par(i); - // assert i - lsb(i) + lsb(i - lsb(i)) == j; - // assert 0 < i - lsb(i) < i && i <= i - lsb(i) + lsb(i - lsb(i)) <= N; - // assert F[j] == A[j - 1] + sum(A[j - lsb(j)..i - lsb(i)]); - // assert F[i] == sum(A[i - lsb(i)..i]); - // assert F[j] + F[i] == A[j - 1] + sum(A[j - lsb(j)..i - lsb(i)]) + sum(A[i - lsb(i)..i]); - split(A, j - lsb(j), i - lsb(i), i); - // assert F[j] + F[i] == A[j - 1] + sum(A[j - lsb(j)..i]); - } + // method walk_back(i: nat) returns (ret: int) + // requires N == |A| == F.Length - 1 + // requires 0 < i <= N + // requires forall j :: 0 < j < i ==> F[j] == sum(A[j - lsb(j)..j]) + // ensures ret == sum(A[i - lsb(i)..i]) + // { + - lemma zero_sum(A: seq<int>, i: nat, j: nat) - decreases |A| - i - requires 0 <= i <= j <= |A| - requires forall k :: 0 <= k < |A| ==> A[k] == 0 - ensures sum(A[i..j]) == 0 - { - if i < j { - zero_sum(A, i + 1, j); - } - reveal sum; - } + + // } // Create FT from seq A' - constructor (A': seq<int>) - ensures A == A' - ensures valid() + constructor {:isolate_assertions} (A': seq<int>) // https://dafny.org/latest/HowToFAQ/FAQUpdateArrayField ensures fresh(F) + ensures A == A' + ensures valid() { // A is 0-indexed // F is 1-indexed for Fenwick reasons // Sorry... N := |A'|; A := A'; - F := new int[|A'| + 1](i => 0);// if 0 < i <= |A'| then A'[i - 1] else 0); - // A := seq(|A'|, i => 0); - // F := new int[|A'| + 1](i => 0); + F := new int[|A'| + 1](i => 0);//if 0 < i <= |A'| then A'[i - 1] else 0); new; for i := 1 to F.Length modifies F - invariant forall j :: 0 <= j < i ==> F[j] == sum(A[j - lsb(j)..j]) - invariant forall j :: i <= j <= N ==> if j - lsb(j) > i then F[j] == 0 else F[j] == 1 + invariant A == A' + // invariant forall j :: 0 < j < i ==> F[j] == sum(A[j - lsb(j)..j]) + // invariant forall j :: i <= j <= N && j - lsb(j) / 2 >= i ==> F[j] == 0 + // invariant forall j :: 0 < j < i && j + lsb(j) / 2 > i && j + lsb(j) <= N ==> F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) { + assume forall j :: 0 < j < i ==> F[j] == sum(A[j - lsb(j)..j]); + assume forall j :: i <= j <= N && j - lsb(j) / 2 >= i ==> F[j] == 0; + assume forall j :: 0 < j < i && j + lsb(j) / 2 >= i - 1 && j + lsb(j) <= N ==> lsb(j) < lsb(j + lsb(j)) && F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]); + + if lsb(i) == 1 { + assert F[i] == sum(A[i - lsb(i)..i - 1]) by { reveal sum; } + } else { + assert lsb(i - 1) == 1; + } + assert F[i] == sum(A[i - lsb(i)..i - 1]); + assert A'[i - 1] == sum(A[i - 1..i]) by { reveal sum; } + split(A, i - lsb(i), i - 1, i); F[i] := F[i] + A'[i - 1]; + assert F[i] == sum(A[i - lsb(i)..i]); var j := i + lsb(i); if j < F.Length { - F[j] := F[j] + F[i]; + lsb_add(i); + if i - lsb(i) == j - lsb(j) { + assert F[j] == 0; + assert j - lsb(j) / 2 <= i; + assert F[i] == sum(A[j - lsb(j)..i]); + assert i + lsb(i) / 2 >= i && i + lsb(i) <= N ==> F[i] == sum(A[j - lsb(j)..i]); + F[j] := F[j] + F[i]; + assert i + lsb(i) / 2 >= i && i + lsb(i) <= N ==> lsb(i) < lsb(i + lsb(i)) && F[i + lsb(i)] == sum(A[i + lsb(i) - lsb(i + lsb(i))..i]); + forall j | 0 < j < i && lsb(j) / 2 >= i && j + lsb(j) <= N + ensures lsb(j) < lsb(j + lsb(j)) && F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) + { + lsb_no_par(i, j); + } + // assert forall j :: 0 < j <= i && j + lsb(j) / 2 >= i && j + lsb(j) <= N ==> lsb(j) < lsb(j + lsb(j)) && F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) by { + // assert i + lsb(i) / 2 >= i && i + lsb(i) <= N ==> lsb(i) < lsb(i + lsb(i)) && F[i + lsb(i)] == sum(A[i + lsb(i) - lsb(i + lsb(i))..i]); + // forall j | 0 < j < i && lsb(j) / 2 >= i && j + lsb(j) <= N + // ensures lsb(j) < lsb(j + lsb(j)) && F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) + // { + // lsb_no_par(i, j); + // } + // } + } else { + assert i - lsb(i) > j - lsb(j); + lsb_shared_par(i); + assert lsb(i - lsb(i)) >= 2 * lsb(i); + // assert F[j] == sum(A[j - lsb(j)..i - lsb(i)]); + F[j] := F[j] + F[i]; + // assert F[j] == sum(A[j - lsb(j)..i - lsb(i)]) + F[i]; + split(A, j - lsb(j), i - lsb(i), i); + assert F[j] == sum(A[j - lsb(j)..i]); + assert i + lsb(i) / 2 >= i && i + lsb(i) <= N ==> lsb(i) < lsb(i + lsb(i)) && F[i + lsb(i)] == sum(A[i + lsb(i) - lsb(i + lsb(i))..i]); + forall j | 0 < j < i && lsb(j) / 2 >= i && j + lsb(j) <= N + ensures lsb(j) < lsb(j + lsb(j)) && F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) + { + lsb_no_par(i, j); + } + // assert forall j :: 0 < j <= i && j + lsb(j) / 2 >= i && j + lsb(j) <= N ==> lsb(j) < lsb(j + lsb(j)) && F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) by { + // assert i + lsb(i) / 2 >= i && i + lsb(i) <= N ==> lsb(i) < lsb(i + lsb(i)) && F[i + lsb(i)] == sum(A[i + lsb(i) - lsb(i + lsb(i))..i]); + // forall j | 0 < j < i && lsb(j) / 2 >= i && j + lsb(j) <= N + // ensures lsb(j) < lsb(j + lsb(j)) && F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) + // { + // lsb_no_par(i, j); + // } + // } + } + } + // assume false; + assert forall j :: 0 < j <= i ==> F[j] == sum(A[j - lsb(j)..j]); + assert forall j :: i + 1 <= j <= N && j - lsb(j) / 2 >= i + 1 ==> F[j] == 0; } + // assume false; assert false; + } + + + +// Alternative linear time construction algorithm + // The usual construction algorithm (in fenwick.c) is EXTREMELY tricky to verify + // Because its state during loop iterations is very complicated + // var j := i - 1; + // var k := 1; + // var l := lsb(i); + // while k < l { + + // } + + + + + + // if i % 2 == 0 { + // assert lsb(i) > 1; + // assert lsb(i - 1) == 1; + // var j := i - lsb(i); + // var k := i - 1; + // while k > j + // invariant k <= j || k + lsb(k) == i + // { + // if k - lsb(k) > j { + // lsb_shared_par(k); + // } + // k := k - lsb(k); + // } + // assert k == j; + + // } + // var j := i - 1; + // if j > i - lsb(i) { + // lsb_even(i); + // assert j + lsb(j) == i; + // } + // assert j > i - lsb(i) ==> j + lsb(j) == i; + // // assert j > i - lsb(i) ==> j + lsb(j) == i; + // // assert F[i] == sum(A[i - 1..i]) by { reveal sum; } + // while j > i - lsb(i) + // invariant j + lsb(j) == i + // // invariant F[i] == sum(A[j..i]) + // // invariant forall j :: 0 < j <= N && j != i ==> if j < i then F[j] == sum(A[j - lsb(j)..j]) else F[j] == A[j - 1] + // { + // // F[i] := F[i] + F[j]; + // // assert F[j] == sum(A[j - lsb(j)..j]); + // // split(A, j - lsb(j), j, i); + // // assert F[i] == sum(A[j - lsb(j)..i]); + + // j := j - lsb(j); + // } + + + + // ghost var R := seq(N + 1, i => if i > 0 then i - lsb(i) else 0); + // for i := 1 to F.Length + // modifies F + // invariant |R| == N + 1 + // invariant forall j :: 0 < j <= N ==> if j < i then F[j] == sum(A[j - lsb(j)..j]) else F[j] == sum(A[j - lsb(j)..R[j]]) + // { + + + // F[i] := F[i] + A'[i - 1]; + // var j := i + lsb(i); + // if j < F.Length { + // // assert F[j] == sum(A[j - lsb(j)..R[j]]); + // F[j] := F[j] + F[i]; + // R := R[..j] + [i] + R[j + 1..]; + + // // lsb_add(i); + // // if i - lsb(i) == j - lsb(j) { + + // // } else { + + // // } + // // if j - lsb(j) + // } + // } // assert |A| == N && F.Length == N + 1 && forall i :: 0 < i <= N ==> F[i] == sum(A[i - lsb(i)..i]); // assert forall i :: 0 <= i < N ==> A[i] == F[i + 1] == 0; @@ -246,7 +374,6 @@ class fenwick { // // } // } // assert false; - } // Add v to A[i'] method update(i': nat, v: int) |