diff options
| author | Anthony Wang | 2025-03-15 22:39:20 -0400 |
|---|---|---|
| committer | Anthony Wang | 2025-03-15 22:39:20 -0400 |
| commit | a9d3267b86e144898c674ebe760024a12876460a (patch) | |
| tree | b80f960dbe314a880df9a81fa48b11be503e9457 | |
| parent | 6a53b84c19d7ebaf1430679d3880dc6ad38dd319 (diff) | |
Use int instead of nat for perf reasons
| -rw-r--r-- | fenwick.dfy | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/fenwick.dfy b/fenwick.dfy index 4366668..41231ee 100644 --- a/fenwick.dfy +++ b/fenwick.dfy @@ -1,12 +1,12 @@ // Proof of some functions from fenwick.c -// Dafny only supports bitwise ops on bitvectors, not nats +// Dafny only supports bitwise ops on bitvectors, not ints // But bitvectors are super gross -// So let's implement i & -i for nats +// So let's implement i & -i for ints // Basically the largest power of 2 that divides i // opaque for perf reasons since be always use lsb_* lemmas to reason about it // https://dafny.org/latest/VerificationOptimization/VerificationOptimization#opaque-definitions -opaque function lsb(i: nat): nat +opaque function lsb(i: int): int requires i > 0 ensures 0 < lsb(i) <= i { @@ -14,11 +14,11 @@ opaque function lsb(i: nat): nat } // Verify lsb(i) == i & -i -lemma lsb_correct(i: nat) +lemma lsb_correct(i: int) // Literally just check every i // Uh you can bump this up to 2^32 and bv32 but it takes forever to check requires 0 < i < 256 - ensures lsb(i) == ((i as bv8) & -(i as bv8)) as nat + ensures lsb(i) == ((i as bv8) & -(i as bv8)) as int { // Dafny can autoprove this using aggressive inlining reveal lsb; @@ -28,7 +28,7 @@ lemma lsb_correct(i: nat) // 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) +lemma lsb_add(i: int) requires i > 0 ensures 2 * lsb(i) <= lsb(i + lsb(i)) { @@ -40,7 +40,7 @@ lemma lsb_add(i: nat) // Used for correctness in update // No intervals touch i between i and i + lsb(i) -lemma lsb_next(i: nat) +lemma lsb_next(i: int) requires i > 0 ensures forall j :: i < j < i + lsb(i) ==> j - lsb(j) >= i { @@ -50,7 +50,7 @@ lemma lsb_next(i: nat) // Used for correctness in constructor // If the i and i + lsb(i) intervals start at the same place // Then i is the first child for i + lsb(i) -lemma lsb_no_par(i: nat, j: nat) +lemma lsb_no_par(i: int, j: int) requires 0 < j < i requires i - lsb(i) == i + lsb(i) - lsb(i + lsb(i)) ensures j + lsb(j) != i + lsb(i) @@ -62,7 +62,7 @@ lemma lsb_no_par(i: nat, j: nat) // Used for correctness in constructor // If the interval for i starts after the interval for i + lsb(i) // Then i - lsb(i) also has parent i + lsb(i) -lemma lsb_shared_par(i: nat) +lemma lsb_shared_par(i: int) 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) @@ -76,7 +76,7 @@ lemma lsb_shared_par(i: nat) // Used for correctness in constructor // If j is pretty close to its parent // Then its parent cannot be i + lsb(i) -lemma lsb_bad_par(i: nat, j: nat) +lemma lsb_bad_par(i: int, j: int) requires 0 < j < i requires j + (lsb(j) + 1) / 2 > i ensures j + lsb(j) != i + lsb(i) @@ -94,7 +94,7 @@ opaque ghost function sum(s: seq<int>): int } // Sum behaves nicely when splitting a slice -lemma split(A: seq<int>, i: nat, j: nat, k: nat) +lemma split(A: seq<int>, i: int, j: int, k: int) decreases |A| - i requires 0 <= i <= j <= k <= |A| ensures sum(A[i..j]) + sum(A[j..k]) == sum(A[i..k]) @@ -106,7 +106,7 @@ lemma split(A: seq<int>, i: nat, j: nat, k: nat) } // Similar to split, but with an element in the middle -lemma split3(A: seq<int>, i: nat, j: nat, k: nat) +lemma split3(A: seq<int>, i: int, j: int, k: int) requires 0 <= i < j <= k <= |A| ensures sum(A[i..j - 1]) + A[j - 1] + sum(A[j..k]) == sum(A[i..k]) { @@ -118,7 +118,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 + var N: int // A is the "ground truth" array // Spooky spooky // It's easier to use a seq here because unlike arrays, they're immutable @@ -226,7 +226,7 @@ class fenwick { } // Add v to A[i'] - method update(i': nat, v: int) + method update(i': int, v: int) modifies this modifies F requires 0 < i' <= N @@ -311,14 +311,14 @@ class fenwick { } // Query for prefix sum up to i' inclusive - method query(i': nat) returns (ret: int) + method query(i': int) returns (ret: int) requires 0 < i' <= N requires valid() ensures ret == sum(A[0..i']) { - reveal sum; ret := 0; var i := i'; + assert ret == sum(A[i'..i']) by { reveal sum; } while i > 0 decreases i invariant i >= 0 |