diff options
| author | Anthony Wang | 2025-03-15 20:30:52 -0400 |
|---|---|---|
| committer | Anthony Wang | 2025-03-15 20:30:52 -0400 |
| commit | 6a53b84c19d7ebaf1430679d3880dc6ad38dd319 (patch) | |
| tree | a7cebd0071c4c68be7476cc02803369451e82d25 | |
| parent | a3c07d893344f5c5943fe2b513a29aa0ff905ea0 (diff) | |
More helpful comments
| -rw-r--r-- | fenwick.dfy | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/fenwick.dfy b/fenwick.dfy index 3f05b2e..4366668 100644 --- a/fenwick.dfy +++ b/fenwick.dfy @@ -20,13 +20,14 @@ lemma lsb_correct(i: nat) requires 0 < i < 256 ensures lsb(i) == ((i as bv8) & -(i as bv8)) as nat { - // Inline lsb + // Dafny can autoprove this using aggressive inlining reveal lsb; } -// Used for termination in update +// Used for termination in update and some other places // i + lsb(i) is the parent of i // The lsb of i is less than the lsb of its parent +// Definitely the most important property of lsb lemma lsb_add(i: nat) requires i > 0 ensures 2 * lsb(i) <= lsb(i + lsb(i)) @@ -98,8 +99,6 @@ lemma split(A: seq<int>, i: nat, j: nat, k: nat) requires 0 <= i <= j <= k <= |A| ensures sum(A[i..j]) + sum(A[j..k]) == sum(A[i..k]) { - // A ghost appears! - // Dafny can autoprove this using aggressive inlining reveal sum; if i < j { split(A, i + 1, j, k); @@ -117,6 +116,7 @@ lemma split3(A: seq<int>, i: nat, j: nat, k: nat) } // Alright time for the fun stuff +// Buckle up, it's gonna get super crazy class fenwick { var N: nat // A is the "ground truth" array @@ -156,7 +156,7 @@ class fenwick { for i := 1 to F.Length modifies F - // Don't break A + // Don't change A invariant A == A' // These three invariants are all interlocking // Yeah it's super complicated, sorry @@ -169,6 +169,7 @@ class fenwick { // Not sure why it's j + (lsb(j + 1) / 2 >= i other than that it works invariant forall j :: 0 < j < i && j + (lsb(j) + 1) / 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]) { + // Get initial state of F[i] if lsb(i) == 1 { assert F[i] == sum(A[i - lsb(i)..i - 1]) by { reveal sum; } } else { @@ -182,7 +183,7 @@ class fenwick { assert F[i] == sum(A[i - lsb(i)..i]); // Now comes the insanity - // Took me 12 hours to write this + // Took me 10 hours to write this var j := i + lsb(i); if j < F.Length { F[j] := F[j] + F[i]; @@ -331,10 +332,12 @@ class fenwick { } method Main() { + // Example usage var A := [1, 5, 3, 14, -2, 4, -3]; var FT := new fenwick(A); var a := FT.query(5); + assert a == sum(A[0..5]); print a, "\n"; ghost var B := FT.A[0..5]; assert B[0..5] == FT.A[0..5]; |