Yay it almost works

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)
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)
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)