chore: reflow core algorithm, get build to build

SSA/Experimental/Bits/Fast/BitStream.lean

@@ -811,27 +811,27 @@ abbrev negOne : BitStream := fun _ => true
 /-- 'falseIffEq n i' = false ↔ i = n -/
 abbrev falseIffEq (n : Nat) : BitStream := fun i => decide (i != n)
 theorem falseIffEq_eq_false_iff (n i : Nat) :
-    falseIffEq n i = false ↔ i = n := by simp; try omega
+    falseIffEq n i = false ↔ i = n := by simp
 
 abbrev falseIffNeq (n : Nat) : BitStream := fun i => decide (i == n)
 theorem falseIffNeq_eq_false_iff (n i : Nat) :
-    falseIffNeq n i = false ↔ i ≠ n := by simp; try omega
+    falseIffNeq n i = false ↔ i ≠ n := by simp
 
 abbrev falseIffLe (n : Nat) : BitStream := fun i => decide (i > n)
 theorem falseIffLe_eq_false_iff (n i : Nat) :
-    falseIffLe n i = false ↔ i ≤ n := by simp; try omega
+    falseIffLe n i = false ↔ i ≤ n := by simp
 
 abbrev falseIffLt (n : Nat) : BitStream := fun i => decide (i ≥ n)
 theorem falseIffLt_eq_false_iff (n i : Nat) :
-    falseIffLt n i = false ↔ i < n := by simp; try omega
+    falseIffLt n i = false ↔ i < n := by simp
 
 abbrev falseIffGe (n : Nat) : BitStream := fun i => decide (i < n)
 theorem falseIffGe_eq_false_iff (n i : Nat) :
-    falseIffGe n i = false ↔ i ≥ n := by simp; try omega
+    falseIffGe n i = false ↔ i ≥ n := by simp
 
 abbrev falseIffGt (n : Nat) : BitStream := fun i => decide (i ≤ n)
 theorem falseIffGt_eq_false_iff (n i : Nat) :
-    falseIffGt n i = false ↔ i > n := by simp; try omega
+    falseIffGt n i = false ↔ i > n := by simp
 
 section Lemmas
 

SSA/Experimental/Bits/Fast/FiniteStateMachine.lean

@@ -1222,16 +1222,18 @@ def predicateEvalEqFSM : ∀ (p : Predicate), FSMPredicateSolution p
     let t₁' := termEvalEqFSM t₁
     let t₂' := termEvalEqFSM t₂
     {
-     toFSM := (composeBinary FSM.xor t₁' t₂')
-     good := by ext; simp;
+     -- At width 0, all things are equal.
+     toFSM := composeUnaryAux (FSM.ls false) <| (composeUnaryAux FSM.scanOr <| composeBinary FSM.xor t₁' t₂')
+     good := by ext; simp; sorry
     }
   | .neq t₁ t₂ =>
     let t₁' := termEvalEqFSM t₁
     let t₂' := termEvalEqFSM t₂
     {
+     -- At width 0, all things are equal, so the predicate is untrue.
      -- If it ever becomes `0`, it should stay `0` forever, because once
      -- two bitstreams become disequal, they stay disequal!
-     toFSM := composeUnaryAux FSM.scanAnd <| (composeBinary FSM.nxor t₁' t₂')
+     toFSM := composeUnaryAux (FSM.ls true) <| (composeUnaryAux FSM.scanAnd <| composeBinary FSM.nxor t₁' t₂')
      good := by sorry -- ext; simp;
     }
    | .land p q =>
@@ -1255,14 +1257,17 @@ def predicateEvalEqFSM : ∀ (p : Predicate), FSMPredicateSolution p
    | .slt t₁ t₂ =>
      let q₁ := termEvalEqFSM t₁
      let q₂ := termEvalEqFSM t₂
-     { toFSM := composeUnaryAux FSM.not <| composeBinary FSM.sub q₁ q₂,
-       good := by sorry --   ext; simp }
+     { toFSM := 
+       composeUnaryAux (FSM.ls true) <| composeUnaryAux FSM.not <| composeBinary FSM.sub q₁ q₂,
+       good := by sorry -- ext; simp
      }
    | .sle t₁ t₂ =>
       let t₁' := termEvalEqFSM t₁
       let t₂' := termEvalEqFSM t₂
-      let slt := (composeUnaryAux FSM.not <| composeBinaryAux FSM.sub t₁'.toFSM t₂'.toFSM)
-      let eq := (composeBinaryAux FSM.xor t₁'.toFSM t₂'.toFSM)
+      let slt := 
+        composeUnaryAux (FSM.ls true) <| composeUnaryAux FSM.not <| composeBinaryAux FSM.sub t₁'.toFSM t₂'.toFSM
+      let eq := 
+        composeUnaryAux (FSM.ls false) <| (composeBinaryAux FSM.xor t₁'.toFSM t₂'.toFSM)
       have hsz : max (max t₁.arity t₂.arity) (max t₁.arity t₂.arity) = (max t₁.arity t₂.arity) :=
         Nat.max_self ..
       have hsz : max (max t₁.arity t₂.arity) (max t₁.arity t₂.arity) = Predicate.arity (.sle t₁ t₂) := by
@@ -1278,14 +1283,14 @@ def predicateEvalEqFSM : ∀ (p : Predicate), FSMPredicateSolution p
       let t₂' := termEvalEqFSM t₂
       {
        -- a <u b if when we compute (a - b), we must borrow a value.
-       toFSM := (composeUnaryAux FSM.not $ composeBinary FSM.borrow t₁' t₂')
+       toFSM := composeUnaryAux (FSM.ls true) <| (composeUnaryAux FSM.not $ composeBinary FSM.borrow t₁' t₂')
        good := by sorry -- TODO: show that it's good 'ext; simp';
       }
    | .ule t₁ t₂ =>
       let t₁' := termEvalEqFSM t₁
       let t₂' := termEvalEqFSM t₂
-      let ult := (composeUnaryAux FSM.not $ composeBinaryAux FSM.borrow t₁'.toFSM t₂'.toFSM)
-      let eq := (composeBinaryAux FSM.xor t₁'.toFSM t₂'.toFSM)
+      let ult := composeUnaryAux (FSM.ls true) <| (composeUnaryAux FSM.not $ composeBinary FSM.borrow t₁' t₂')
+      let eq := composeUnaryAux (FSM.ls false) <| (composeBinaryAux FSM.xor t₁'.toFSM t₂'.toFSM)
       have hsz : max (max t₁.arity t₂.arity) (max t₁.arity t₂.arity) = (max t₁.arity t₂.arity) :=
         Nat.max_self ..
       have hsz : max (max t₁.arity t₂.arity) (max t₁.arity t₂.arity) = Predicate.arity (.ule t₁ t₂) := by
@@ -1391,19 +1396,36 @@ def FSM.nextBitCircIterate {arity : Type _ } [DecidableEq arity]
      -- | the .fst performs quantifier elimination, by running over all possible values of inputs.
     fsm.nextBitCirc none |>.fst
   | n' + 1 =>
-     -- | the .fst performs quantifier elimination, by running over all possible values of inputs.
      let c := fsm.nextBitCircIterate n'
-     -- | for each input, compute the next bit circuit, quantifier eliminate it, and then compose.
+     -- | for each input, compute the next bit circuit, quantifier eliminate it for all inputs, and then compose.
      let c' := (c.bind (fsm.nextBitCirc ∘ some)).fst
      c'
 
 /-- Decide if the FSM produces zeroes for all inputs at a given index of the bitstream -/
-def decideIfZerosAtIx {arity : Type _} [DecidableEq arity]
+def decideIfZerosAtIxOld {arity : Type _} [DecidableEq arity]
       (fsm : FSM arity) (w : Nat) : Bool :=
     let c := fsm.nextBitCircIterate w
     -- evaluate at the initial carry bit.
     c.eval fsm.initCarry
 
+/-- Decide if the FSM produces zeroes for all inputs at a given index of the bitstream -/
+def decideIfZerosAtIxAux {arity : Type _} [DecidableEq arity]
+      (fsm : FSM arity) (c : Circuit fsm.α) (nItersLeft : Nat) : Bool :=
+    if (c.eval fsm.initCarry)
+    then false
+    else
+      match nItersLeft with 
+      | 0 => true -- c has accumulated the effects so far.
+      | nItersLeft' + 1 => 
+        -- accumulate one iteration
+        have c' := (c.bind (fsm.nextBitCirc ∘ some)).fst
+        if h : c' ≤ c 
+        then true
+        else decideIfZerosAtIxAux fsm (c' ||| c) nItersLeft'
+
+def decideIfZerosAtIx {arity : Type _} [DecidableEq arity]
+      (fsm : FSM arity) (w : Nat) : Bool :=
+    decideIfZerosAtIxAux fsm (fsm.nextBitCirc none).fst w
 /--
 The correctness statement of decideIfZeroesAtIx.
 This tells us that decideIfZeroesAtIx is correct iff the FSM 'p' when evaluated returns false

SSA/Experimental/Bits/Fast/Reflect.lean

@@ -399,7 +399,7 @@ structure Config where
   This is useful to prevent the tactic from taking oodles of time cruncing on goals that
   build large state spaces, which can happen in the presence of tactics.
   -/
-  circuitSizeThreshold : Nat := 90
+  circuitSizeThreshold : Nat := 200
 
   /--
   The upper bound on the state space of the FSM, beyond which the tactic will bail out on an error.
@@ -636,6 +636,16 @@ partial def reflectPredicateAux (bvToIxMap : ReflectMap) (e : Expr) (wExpected :
   match_expr e with
   | Eq α a b =>
     match_expr α with
+    | Nat =>
+       -- support width equality constraints
+      -- TODO: canonicalize 'a = w' into 'w = a'.
+      if wExpected != a then
+        throwError "Only Nat expressions allowed are '{wExpected} ≠ <concrete value>'. Found {indentD e}."
+      let some natVal ← Lean.Meta.getNatValue? b
+        | throwError "Expected '{wExpected} ≠ <concrete width>', found symbolic width {indentD b}."
+      let out := Predicate.widthEq natVal
+      return { bvToIxMap := bvToIxMap, e := out }
+
     | BitVec w =>
       let a ←  reflectTermUnchecked bvToIxMap w a
       let b ← reflectTermUnchecked a.bvToIxMap w b
@@ -955,7 +965,7 @@ example (a b : BitVec 1) : (a - b).slt 0 → a.slt b := by
   -- b = 0x1#1
   sorry
 
-/-- Tricohotomy of slt. Currently fails! -/
+/-- Tricohotomy of slt. -/
 example (w : Nat) (a b : BitVec w) : (1#w = 0#w) ∨ ((a - b).slt 0 → a.slt b) := by
   bv_automata_circuit
 
@@ -993,10 +1003,19 @@ So we need an extra hypothesis that rules out bitwifth 1.
 We do this by saying that either the given condition, or 1+1 = 0.
 I'm actually not sure why I need to rule out bitwidth 0? Mysterious!
 -/
-example (w : Nat) (a : BitVec w) : (1#w = 0#w) ∨ (1#w + 1#w = 0#w) ∨ ((a = - a) → a = 0#w) := by
-  bv_automata_circuit
+example (w : Nat) (a : BitVec w) : (w = 2) → ((a = - a) → a = 0#w) := by
+  fail_if_success bv_automata_circuit
+  sorry
+
 
+example (w : Nat) (a : BitVec w) : (w = 1) → (a = 0#w ∨ a = 1#w) := by bv_automata_circuit
+example (w : Nat) (a : BitVec w) : (w = 0) → (a = 0#w ∨ a = 1#w) := by bv_automata_circuit
+example (w : Nat) : (w = 1) → (1#w + 1#w = 0#w) := by bv_automata_circuit
+example (w : Nat) : (w = 0) → (1#w + 1#w = 0#w) := by bv_automata_circuit
+example (w : Nat) : ((w = 0) ∨ (w = 1)) → (1#w + 1#w = 0#w) := by bv_automata_circuit
 
+example (w : Nat) : (1#w + 1#w = 0#w) → ((w = 0) ∨ (w = 1)):= by
+  bv_automata_circuit
 /-
 We can say that we are at bitwidth 1 by saying that 1 + 1 = 0.
 When we have this, we then explicitly enumerate the different values that a can have.
@@ -1005,8 +1024,6 @@ Note that this is pretty expensive.
 example (w : Nat) (a : BitVec w) : (1#w + 1#w = 0#w) → (a = 0#w ∨ a = 1#w) := by
   bv_automata_circuit
 
-
-
 example (w : Nat) (a b : BitVec w) : (a + b = 0#w) → a = - b := by
   bv_automata_circuit
 
@@ -1019,7 +1036,6 @@ theorem eq_circuit (w : Nat) (a b : BitVec w) : (a &&& b = 0#w) → ((a + b) = (
 #print eq_circuit
 
 
-open NNF in
 /-- Can exploit hyps -/
 theorem eq4 (w : Nat) (a b : BitVec w) (h : a &&& b = 0#w) : a + b = a ||| b := by
   bv_automata_circuit
@@ -1039,7 +1055,7 @@ info: goal after reflection: ⏎
   a b : BitVec 10
   ⊢ (Predicate.eq (Term.var 0) (Term.var 1)).denote 10 (Map.append 10 b (Map.append 10 a Map.empty))
 ---
-info: FSM: ⋆Circuit size '3'  ⋆State space size '0'
+info: FSM: ⋆Circuit size '11'  ⋆State space size '2'
 ---
 info: using special fixed-width procedure for fixed bitwidth '10'.
 ---
@@ -1072,21 +1088,21 @@ theorem test_symbolic_abstraction (f : BitVec w → BitVec w) (x y : BitVec w) :
   by bv_automata_circuit
 
 /-- Check that we correctly handle `OfNat.ofNat 1`. -/
-theorem not_neg_eq_sub_one (x : BitVec 53):
+theorem not_neg_eq_sub_one (x : BitVec 53) :
     ~~~ (- x) = x - 1 := by
-  all_goals bv_automata_circuit
+  bv_automata_circuit
 
 /-- Check that we correctly handle multiplication by two. -/
 theorem sub_eq_mul_and_not_sub_xor (x y : BitVec w):
     x - y = 2 * (x &&& ~~~ y) - (x ^^^ y) := by
   -- simp [Simplifications.BitVec.OfNat_ofNat_mul_eq_ofNat_mul]
   -- simp only [BitVec.ofNat_eq_ofNat, Simplifications.BitVec.two_mul_eq_add_add]
-  all_goals bv_automata_circuit
+  all_goals bv_automata_circuit (config := {circuitSizeThreshold := 140 })
 
 
 /- See that such problems have large circuit sizes, but small state spaces -/
 def alive_1 {w : ℕ} (x x_1 x_2 : BitVec w) : (x_2 &&& x_1 ^^^ x_1) + 1#w + x = x - (x_2 ||| ~~~x_1) := by
-  bv_automata_circuit (config := { circuitSizeThreshold := 81 })
+  bv_automata_circuit (config := { circuitSizeThreshold := 107 })
 
 
 def false_statement {w : ℕ} (x y : BitVec w) : x = y := by
@@ -1171,30 +1187,25 @@ example : ∀ (w : Nat) (x : BitVec w), x <<< (1 : Nat) = x + x := by intros; bv
 example : ∀ (w : Nat) (x : BitVec w), x <<< (2 : Nat) = x + x + x + x := by
   intros; bv_automata_circuit
 
-
-/-- Can solve width-constraints problems, but this takes a while. -/
-def test29 (x y : BitVec w) : w = 32 → x &&& x &&& x &&& x &&& x &&& x = x := by
-  bv_automata_circuit (config := { stateSpaceSizeThreshold := 33 })
-
 /-- Can solve width-constraints problems -/
 def test30  : (w = 2) → 8#w = 0#w := by
   bv_automata_circuit
 
 /-- Can solve width-constraints problems -/
-def test31 (w : Nat) (x : BitVec w) : (w = 64) → x &&& x = x := by
-  bv_automata_circuit (config := { stateSpaceSizeThreshold := 65 })
+def test31 (w : Nat) (x : BitVec w) : x &&& x = x := by
+  bv_automata_circuit (config := { stateSpaceSizeThreshold := 100 })
 
 theorem neg_eq_not_add_one (x : BitVec w) :
     -x = ~~~ x + 1#w := by
   bv_automata_circuit
 
 theorem add_eq_xor_add_mul_and (x y : BitVec w) :
     x + y = (x ^^^ y) + (x &&& y) + (x &&& y) := by
-  bv_automata_circuit (config := { circuitSizeThreshold := 100 } )
+  bv_automata_circuit (config := { circuitSizeThreshold := 300 } )
 
 theorem add_eq_xor_add_mul_and' (x y : BitVec w) :
     x + y = (x ^^^ y) + (x &&& y) + (x &&& y) := by
-  bv_automata_circuit (config := { circuitSizeThreshold := 100 } )
+  bv_automata_circuit (config := { circuitSizeThreshold := 300 } )
 
 theorem add_eq_xor_add_mul_and_nt (x y : BitVec w) :
     x + y = (x ^^^ y) + 2 * (x &&& y) := by
@@ -1227,60 +1238,24 @@ theorem zext (b : BitVec 8) : (b.zeroExtend 10 |>.zeroExtend 8) = b := by
   sorry
 
 /-- Can solve width-constraints problems, when written with a width constraint. -/
-def width_specific_1 (x : BitVec 1) : x + x = x ^^^ x := by
+def width_specific_1 (x : BitVec w) : w = 1 →  x + x = x ^^^ x := by
   bv_automata_circuit
 
 
 example (x : BitVec 0) : x = x + 0#0 := by
   bv_automata_circuit
 
-def width_generic_exploit_fail (x : BitVec 0) : x + x + x + x = 0#0 := by
-  bv_automata_circuit
+/-- All bitvectors are equal at width 0 -/
+example (x y : BitVec 0) : x = y := by bv_automata_circuit
 
-/--
-info: goal after NNF: ⏎
-  x : BitVec 1
-  ⊢ x + x + x + x = 0#1
----
-info: goal after preprocessing: ⏎
-  x : BitVec 1
-  ⊢ x + x + x + x = 0#1
----
-info: goal after reflection: ⏎
-  x : BitVec 1
-  ⊢ (Predicate.eq ((((Term.var 0).add (Term.var 0)).add (Term.var 0)).add (Term.var 0)) Term.zero).denote 1
-      (Map.append 1 x Map.empty)
----
-info: FSM: ⋆Circuit size '70'  ⋆State space size '3'
----
-info: using special fixed-width procedure for fixed bitwidth '1'.
----
-info: goal being decided: ⏎
-  case heval.a.h
-  x : BitVec 1
-  ⊢ reduceBool
-        (Decidable.decide
-          (∀ (vars : List BitStream),
-            (Predicate.eq ((((Term.var 0).add (Term.var 0)).add (Term.var 0)).add (Term.var 0)) Term.zero).eval vars 1 =
-              false)) =
-      true
----
-error: tactic 'bv_automata_circuit' evaluated that the proposition
-  reduceBool
-      (Decidable.decide
-        (∀ (vars : List BitStream),
-          (Predicate.eq ((((Term.var 0).add (Term.var 0)).add (Term.var 0)).add (Term.var 0)) Term.zero).eval vars 1 =
-            false)) =
-    true
-is false
--/
-#guard_msgs in def width_generic_exploit_fail (x : BitVec 1) : x + x + x + x = 0#1 := by
+/-- At width 1, adding bitvector to itself four times gives 0. Characteristic equals 2 -/
+def width_1_char_2 (x : BitVec 1) : x + x = 0#1 := by
   bv_automata_circuit
-  sorry
 
-/-- Can solve width-constraints problems, when written with a width constraint. -/
-def width_generic_exploit_success (x : BitVec w) (hw : w = 1) : x + x + x + x = 0#w := by
-  bv_automata_circuit
+
+/-- At width 1, adding bitvector to itself four times gives 0. Characteristic 2 divides 4 -/
+def width_1_char_2_add_four (x : BitVec 1) : x + x + x + x = 0#1 := by bv_automata_circuit
+
 
 set_option trace.profiler true  in
 /-- warning: declaration uses 'sorry' -/