Add semi-blank Fenwick proof files if people/LLMs want to try writing it themselvesHEADmaster

3 files changed, 479 insertions, 0 deletions

diff --git a/fenwick-blank.dfy b/fenwick-blank.dfy
new file mode 100644
index 0000000..5336ae9
--- /dev/null
+++ b/fenwick-blank.dfy
@@ -0,0 +1,109 @@
+// Dafny only supports bitwise ops on bitvectors, not ints
+// But bitvectors are super gross
+// Ex: https://github.com/dafny-lang/dafny/wiki/Bit-Vector-Cookbook
+// So let's implement i & -i for ints
+// Basically the largest power of 2 that divides i
+// https://dafny.org/latest/VerificationOptimization/VerificationOptimization#opaque-definitions
+opaque function lsb(i: int): int
+    requires i > 0
+    ensures 0 < lsb(i) <= i
+{
+    if i % 2 == 1 then 1 else 2 * lsb(i / 2)
+}
+
+// Pretty trivial recursive sum
+opaque ghost function sum(s: seq<int>): int
+{
+    if |s| == 0 then 0 else s[0] + sum(s[1..])
+}
+
+class fenwick {
+    // Size
+    var N: int
+    // "Ground truth" seq
+    ghost var A: seq<int>
+    // FT array
+    // 1-indexed and size N + 1 for Fenwick reasons
+    // Sorry...
+    var F: array<int>
+
+    // Check if F is a valid FT over A
+    ghost predicate valid()
+        reads this
+        reads F
+    {
+        N < 0x80000000 && |A| == N && F.Length == N + 1 && forall i :: 0 < i <= N ==> F[i] == sum(A[i - lsb(i)..i])
+    }
+
+    // Create FT from seq A'
+    // Use {:isolate_assertions} for perf reasons
+    constructor {:isolate_assertions} (A': seq<int>)
+        requires |A'| < 0x80000000
+        // https://dafny.org/latest/HowToFAQ/FAQUpdateArrayField
+        ensures fresh(F)
+        ensures A == A'
+        ensures valid()
+    {
+        N := |A'|;
+        A := A';
+        F := new int[|A'| + 1](i => 0);
+        new;
+
+        for i := 1 to F.Length
+            modifies F
+            // Don't change A
+            invariant A == A'
+        {
+            F[i] := F[i] + A'[i - 1];
+            var j := i + lsb(i);
+            if j < F.Length {
+                F[j] := F[j] + F[i];
+            }
+        }
+    }
+
+    // Add v to A[i']
+    method update(i': int, v: int)
+        modifies this
+        modifies F
+        requires 0 < i' <= N
+        requires valid()
+        // Check that A is updated correctly
+        ensures A == old(A)[0..i' - 1] + [old(A)[i' - 1] + v] + old(A)[i'..]
+        // Make sure F is still a valid FT over A
+        ensures valid()
+    {
+        // Update "ground truth" ghost seq
+        A := A[0..i' - 1] + [A[i' - 1] + v] + A[i'..];
+
+        var i := i';
+        ghost var t := 1;
+        while i <= N
+        {
+            F[i] := F[i] + v;
+            i := i + lsb(i);
+            t := 2 * t;
+        }
+        // Loop ran at most log(N) + 1 iterations
+        assert t <= 2 * N;
+    }
+
+    // Query for prefix sum up to i' inclusive
+    method query(i': int) returns (ret: int)
+        requires 0 < i' <= N
+        requires valid()
+        ensures ret == sum(A[0..i'])
+    {
+        ret := 0;
+        var i := i';
+        ghost var t := 1;
+        while i > 0
+        {
+            ret := ret + F[i];
+            i := i - lsb(i);
+            t := 2 * t;
+        }
+        // Loop ran at most log(N) + 1 iterations
+        assert t <= 2 * N;
+    }
+}
diff --git a/fenwick-lemmas-proved.dfy b/fenwick-lemmas-proved.dfy
new file mode 100644
index 0000000..9996516
--- /dev/null
+++ b/fenwick-lemmas-proved.dfy
@@ -0,0 +1,191 @@
+// Dafny only supports bitwise ops on bitvectors, not ints
+// But bitvectors are super gross
+// Ex: https://github.com/dafny-lang/dafny/wiki/Bit-Vector-Cookbook
+// 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: int): int
+    requires i > 0
+    ensures 0 < lsb(i) <= i
+{
+    if i % 2 == 1 then 1 else 2 * lsb(i / 2)
+}
+
+// Crucial lemma used in several 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: int)
+    requires i > 0
+    ensures 2 * lsb(i) <= lsb(i + lsb(i))
+{
+    reveal lsb;
+    if i % 2 == 0 {
+        lsb_add(i / 2);
+    }
+}
+
+// No intervals touch i between i and i + lsb(i)
+lemma lsb_next(i: int)
+    requires i > 0
+    ensures forall j :: i < j < i + lsb(i) ==> j - lsb(j) >= i
+{
+    reveal lsb;
+}
+
+// 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: 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)
+{
+    reveal lsb;
+    lsb_add(j);
+}
+
+// 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: 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)
+{
+    reveal lsb;
+    if i % 2 == 0 {
+        lsb_shared_par(i / 2);
+    }
+}
+
+// If j is pretty close to its parent
+// Then its parent cannot be i + lsb(i)
+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)
+{
+    reveal lsb;
+}
+
+// Pretty trivial recursive sum
+// opaque for perf reasons since we always use split or split3 to reason about it
+// ghost because we don't use it outside of proof
+// So it doesn't need to be compiled
+opaque ghost function sum(s: seq<int>): int
+{
+    if |s| == 0 then 0 else s[0] + sum(s[1..])
+}
+
+// Sum behaves nicely when splitting a slice
+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])
+{
+    reveal sum;
+    if i < j {
+        split(A, i + 1, j, k);
+    }
+}
+
+// Similar to split, but with an element in the middle
+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])
+{
+    reveal sum;
+    split(A, i, j - 1, k);
+    split(A, j - 1, j, k);
+}
+
+class fenwick {
+    // Size
+    var N: int
+    // "Ground truth" seq
+    ghost var A: seq<int>
+    // FT array
+    // 1-indexed and size N + 1 for Fenwick reasons
+    // Sorry...
+    var F: array<int>
+
+    // Check if F is a valid FT over A
+    ghost predicate valid()
+        reads this
+        reads F
+    {
+        N < 0x80000000 && |A| == N && F.Length == N + 1 && forall i :: 0 < i <= N ==> F[i] == sum(A[i - lsb(i)..i])
+    }
+
+    // Create FT from seq A'
+    // Use {:isolate_assertions} for perf reasons
+    constructor {:isolate_assertions} (A': seq<int>)
+        requires |A'| < 0x80000000
+        // https://dafny.org/latest/HowToFAQ/FAQUpdateArrayField
+        ensures fresh(F)
+        ensures A == A'
+        ensures valid()
+    {
+        N := |A'|;
+        A := A';
+        F := new int[|A'| + 1](i => 0);
+        new;
+
+        for i := 1 to F.Length
+            modifies F
+            // Don't change A
+            invariant A == A'
+        {
+            F[i] := F[i] + A'[i - 1];
+            var j := i + lsb(i);
+            if j < F.Length {
+                F[j] := F[j] + F[i];
+            }
+        }
+    }
+
+    // Add v to A[i']
+    method update(i': int, v: int)
+        modifies this
+        modifies F
+        requires 0 < i' <= N
+        requires valid()
+        // Check that A is updated correctly
+        ensures A == old(A)[0..i' - 1] + [old(A)[i' - 1] + v] + old(A)[i'..]
+        // Make sure F is still a valid FT over A
+        ensures valid()
+    {
+        // Update "ground truth" ghost seq
+        A := A[0..i' - 1] + [A[i' - 1] + v] + A[i'..];
+
+        var i := i';
+        ghost var t := 1;
+        while i <= N
+        {
+            F[i] := F[i] + v;
+            i := i + lsb(i);
+            t := 2 * t;
+        }
+        // Loop ran at most log(N) + 1 iterations
+        assert t <= 2 * N;
+    }
+
+    // Query for prefix sum up to i' inclusive
+    method query(i': int) returns (ret: int)
+        requires 0 < i' <= N
+        requires valid()
+        ensures ret == sum(A[0..i'])
+    {
+        ret := 0;
+        var i := i';
+        ghost var t := 1;
+        while i > 0
+        {
+            ret := ret + F[i];
+            i := i - lsb(i);
+            t := 2 * t;
+        }
+        // Loop ran at most log(N) + 1 iterations
+        assert t <= 2 * N;
+    }
+}
diff --git a/fenwick-lemmas.dfy b/fenwick-lemmas.dfy
new file mode 100644
index 0000000..b87dd85
--- /dev/null
+++ b/fenwick-lemmas.dfy
@@ -0,0 +1,179 @@
+// Dafny only supports bitwise ops on bitvectors, not ints
+// But bitvectors are super gross
+// Ex: https://github.com/dafny-lang/dafny/wiki/Bit-Vector-Cookbook
+// 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: int): int
+    requires i > 0
+    ensures 0 < lsb(i) <= i
+{
+    if i % 2 == 1 then 1 else 2 * lsb(i / 2)
+}
+
+// Crucial lemma used in several 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: int)
+    requires i > 0
+    ensures 2 * lsb(i) <= lsb(i + lsb(i))
+{
+
+}
+
+// No intervals touch i between i and i + lsb(i)
+lemma lsb_next(i: int)
+    requires i > 0
+    ensures forall j :: i < j < i + lsb(i) ==> j - lsb(j) >= i
+{
+    
+}
+
+// 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: 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)
+{
+    
+}
+
+// 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: 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)
+{
+    
+}
+
+// If j is pretty close to its parent
+// Then its parent cannot be i + lsb(i)
+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)
+{
+    
+}
+
+// Pretty trivial recursive sum
+// opaque for perf reasons since we always use split or split3 to reason about it
+// ghost because we don't use it outside of proof
+// So it doesn't need to be compiled
+opaque ghost function sum(s: seq<int>): int
+{
+    if |s| == 0 then 0 else s[0] + sum(s[1..])
+}
+
+// Sum behaves nicely when splitting a slice
+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])
+{
+    
+}
+
+// Similar to split, but with an element in the middle
+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])
+{
+    
+}
+
+class fenwick {
+    // Size
+    var N: int
+    // "Ground truth" seq
+    ghost var A: seq<int>
+    // FT array
+    // 1-indexed and size N + 1 for Fenwick reasons
+    // Sorry...
+    var F: array<int>
+
+    // Check if F is a valid FT over A
+    ghost predicate valid()
+        reads this
+        reads F
+    {
+        N < 0x80000000 && |A| == N && F.Length == N + 1 && forall i :: 0 < i <= N ==> F[i] == sum(A[i - lsb(i)..i])
+    }
+
+    // Create FT from seq A'
+    // Use {:isolate_assertions} for perf reasons
+    constructor {:isolate_assertions} (A': seq<int>)
+        requires |A'| < 0x80000000
+        // https://dafny.org/latest/HowToFAQ/FAQUpdateArrayField
+        ensures fresh(F)
+        ensures A == A'
+        ensures valid()
+    {
+        N := |A'|;
+        A := A';
+        F := new int[|A'| + 1](i => 0);
+        new;
+
+        for i := 1 to F.Length
+            modifies F
+            // Don't change A
+            invariant A == A'
+        {
+            F[i] := F[i] + A'[i - 1];
+            var j := i + lsb(i);
+            if j < F.Length {
+                F[j] := F[j] + F[i];
+            }
+        }
+    }
+
+    // Add v to A[i']
+    method update(i': int, v: int)
+        modifies this
+        modifies F
+        requires 0 < i' <= N
+        requires valid()
+        // Check that A is updated correctly
+        ensures A == old(A)[0..i' - 1] + [old(A)[i' - 1] + v] + old(A)[i'..]
+        // Make sure F is still a valid FT over A
+        ensures valid()
+    {
+        // Update "ground truth" ghost seq
+        A := A[0..i' - 1] + [A[i' - 1] + v] + A[i'..];
+
+        var i := i';
+        ghost var t := 1;
+        while i <= N
+        {
+            F[i] := F[i] + v;
+            i := i + lsb(i);
+            t := 2 * t;
+        }
+        // Loop ran at most log(N) + 1 iterations
+        assert t <= 2 * N;
+    }
+
+    // Query for prefix sum up to i' inclusive
+    method query(i': int) returns (ret: int)
+        requires 0 < i' <= N
+        requires valid()
+        ensures ret == sum(A[0..i'])
+    {
+        ret := 0;
+        var i := i';
+        ghost var t := 1;
+        while i > 0
+        {
+            ret := ret + F[i];
+            i := i - lsb(i);
+            t := 2 * t;
+        }
+        // Loop ran at most log(N) + 1 iterations
+        assert t <= 2 * N;
+    }
+}