aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAnthony Wang2025-03-15 19:16:52 -0400
committerAnthony Wang2025-03-15 19:16:52 -0400
commit0addc7bfc88690d51f57e33f5ec5f0719eade1ce (patch)
tree16cd995891895322cc8012ea0293d878c6bae55c
parent5e5535142f65861af1223ff6f7ca81f0e9d18cd2 (diff)
Yay it almost works
-rw-r--r--fenwick.dfy235
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)