End to end subcircuit soundness

Clean/Circuit/Basic.lean

@@ -1,7 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
 import Clean.Circuit.Expression
 import Clean.Circuit.Provable
 
@@ -197,7 +193,7 @@ def assign_cell (c: Cell F) (v: Variable F) := as_circuit (
 -- formal concepts of soundness and completeness of a circuit
 
 @[simp]
-def constraints_hold_from_list [Field F] (env: (ℕ → F)) : List (Operation F) → Prop
+def constraints_hold_from_list (env: (ℕ → F)) : List (Operation F) → Prop
   | [] => True
   | op :: [] => match op with
     | Operation.Assert e => (e.eval_env env) = 0
@@ -213,7 +209,7 @@ def constraints_hold_from_list [Field F] (env: (ℕ → F)) : List (Operation F)
     | _ => constraints_hold_from_list env ops
 
 @[reducible, simp]
-def constraints_hold [Field F] (env: (ℕ → F)) (circuit: Circuit F α) (ctx : Context F := .empty) : Prop :=
+def constraints_hold (env: (ℕ → F)) (circuit: Circuit F α) (ctx : Context F := .empty) : Prop :=
   constraints_hold_from_list env (circuit ctx).1.2
 
 /--
@@ -223,7 +219,7 @@ witness generator, checking all constraints would not fail.
 For subcircuits, since we proved completeness, this only means we need to satisfy the assumptions!
 -/
 @[simp]
-def constraints_hold_from_list_default [Field F] : List (Operation F) → Prop
+def constraints_hold_from_list_default : List (Operation F) → Prop
   | [] => True
   | op :: [] => match op with
     | Operation.Assert e => e.eval = 0

Clean/Circuit/Expression.lean

@@ -1,7 +1,4 @@
 import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
 
 variable {F: Type}
 

Clean/Circuit/Provable.lean

@@ -1,6 +1,4 @@
-import Mathlib.Algebra.Field.Basic
 import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
 import Clean.Utils.Vector
 import Clean.Circuit.Expression
 

Clean/Circuit/SubCircuit.lean

@@ -3,59 +3,147 @@ import Clean.Circuit.Basic
 variable {F: Type} [Field F]
 
 namespace PreOperation
--- in the following, we prove equivalence between flattened and nested constraints
 
 def to_flat_operations [Field F] (ops: List (Operation F)) : List (PreOperation F) :=
   match ops with
   | [] => []
   | op :: ops => match op with
-    | Operation.Witness compute => PreOperation.Witness compute :: to_flat_operations ops
-    | Operation.Assert e => PreOperation.Assert e :: to_flat_operations ops
-    | Operation.Lookup l => PreOperation.Lookup l :: to_flat_operations ops
-    | Operation.Assign (c, v) => PreOperation.Assign (c, v) :: to_flat_operations ops
+    | Operation.Witness c => Witness c :: to_flat_operations ops
+    | Operation.Assert e => Assert e :: to_flat_operations ops
+    | Operation.Lookup l => Lookup l :: to_flat_operations ops
+    | Operation.Assign c => Assign c :: to_flat_operations ops
     | Operation.SubCircuit circuit => circuit.ops ++ to_flat_operations ops
 
--- TODO super painful, mainly because `cases` doesn't allow rich patterns -- how does this work again?
-theorem can_flatten_first : ∀ (env: ℕ → F) (ops: List (Operation F)),
-  PreOperation.constraints_hold env (to_flat_operations ops)
-  → Circuit.constraints_hold_from_list env ops
+open Circuit (constraints_hold_from_list constraints_hold_from_list_default)
+
+lemma constraints_hold_cons : ∀ {op : PreOperation F}, ∀ {ops: List (PreOperation F)}, ∀ {env : ℕ → F},
+  constraints_hold env (op :: ops) ↔ constraints_hold env [op] ∧ constraints_hold env ops := by
+  intro op ops env
+  match ops with
+  | [] => tauto
+  | op' :: ops =>
+    constructor <;> (
+      rintro h
+      dsimp only [constraints_hold] at h
+      split at h
+      <;> simp_all only [constraints_hold, and_self])
+
+lemma constraints_hold_append : ∀ {a b: List (PreOperation F)}, ∀ {env : ℕ → F},
+  constraints_hold env (a ++ b) ↔ constraints_hold env a ∧ constraints_hold env b := by
+  intro a b env
+  induction a with
+  | nil => rw [List.nil_append]; tauto
+  | cons op ops ih =>
+    constructor
+    · intro h
+      rw [List.cons_append] at h
+      obtain ⟨ h_op, h_rest ⟩ := constraints_hold_cons.mp h
+      obtain ⟨ h_ops, h_b ⟩ := ih.mp h_rest
+      exact ⟨ constraints_hold_cons.mpr ⟨ h_op, h_ops ⟩, h_b ⟩
+    · rintro ⟨ h_a, h_b ⟩
+      obtain ⟨ h_op, h_ops ⟩ := constraints_hold_cons.mp h_a
+      have h_rest := ih.mpr ⟨ h_ops, h_b ⟩
+      exact constraints_hold_cons.mpr ⟨ h_op, h_rest ⟩
+
+/--
+Main soundness theorem which proves that flattened constraints imply nested constraints.
+
+It thereby justifies relying on the nested version `Circuit.constraints_hold_from_list`,
+where constraints of subcircuits are replaced with higher-level statements
+that imply (or are implied by) those constraints.
+-/
+theorem can_replace_subcircuits : ∀ {ops: List (Operation F)}, ∀ {env : ℕ → F},
+  constraints_hold env (to_flat_operations ops) → constraints_hold_from_list env ops
 := by
-  intro env ops
-  induction ops with
-  | nil => intro h; exact h
+  intro ops env h
+  -- `to_flat_operations.induct` (functional induction for `to_flat_operations`) is matching on
+  -- empty vs non-empty lists, and different cases for the head in the non-empty case, at the same time.
+  induction ops using to_flat_operations.induct with
+  | case1 => tauto
+  -- we can handle all non-empty cases except `SubCircuit` at once
+  | case2 ops _ ih | case3 ops _ ih | case4 ops _ ih | case5 ops _ ih =>
+    dsimp only [to_flat_operations] at h
+    generalize to_flat_operations ops = flatops at h ih
+    cases ops
+    <;> cases flatops
+    <;> try dsimp only [constraints_hold, constraints_hold_from_list] at h; tauto
+  | case6 ops circuit ih =>
+    dsimp only [to_flat_operations] at h
+    have h_subcircuit : constraints_hold env circuit.ops := (constraints_hold_append.mp h).left
+    have h_rest : constraints_hold env (to_flat_operations ops) := (constraints_hold_append.mp h).right
+    cases ops
+    <;> dsimp only [constraints_hold_from_list]
+    <;> use (circuit.imply_soundness env) h_subcircuit
+    use ih h_rest
+
+-- TODO the following two lemmas would be unnecessary if we could prove `constraints_hold_default` to be a special case of `constraints_hold`
+-- see https://github.com/Verified-zkEVM/clean/issues/42
+
+lemma constraints_hold_default_cons : ∀ {op : PreOperation F}, ∀ {ops: List (PreOperation F)},
+  constraints_hold_default (op :: ops) ↔ constraints_hold_default [op] ∧ constraints_hold_default ops := by
+  intro op ops
+  match ops with
+  | [] => tauto
+  | op' :: ops =>
+    constructor <;> (
+      rintro h
+      dsimp only [constraints_hold_default] at h
+      split at h
+      <;> simp_all only [constraints_hold_default, and_self])
+
+lemma constraints_hold_default_append : ∀ {a b: List (PreOperation F)},
+  constraints_hold_default (a ++ b) ↔ constraints_hold_default a ∧ constraints_hold_default b := by
+  intro a b
+  induction a with
+  | nil => rw [List.nil_append]; tauto
   | cons op ops ih =>
-    cases ops with
-    | nil =>
-      simp at ih
-      cases op with
-      | SubCircuit c =>
-        sorry
-      | _ => simp [PreOperation.constraints_hold]
-    | cons op' ops' =>
-      let ops := op' :: ops'
-      cases op with
-      | SubCircuit c => sorry
-      | Assert e => sorry
-      | Witness c =>
-        have h_ops : to_flat_operations (Operation.Witness c :: op' :: ops') = PreOperation.Witness c :: to_flat_operations (op' :: ops') := rfl
-        rw [h_ops]
-        intro h_pre
-        have h1 : PreOperation.constraints_hold env (to_flat_operations (op' :: ops')) := by
-          rw [PreOperation.constraints_hold] at h_pre
-          · exact h_pre
-          · sorry
-          · simp
-          · simp
-        have ih1 := ih h1
-        simp [ih1]
-      | Lookup l => sorry
-      | Assign a => sorry
-
-theorem can_flatten : ∀ (ops: List (Operation F)),
-  Circuit.constraints_hold_from_list_default ops →
-  PreOperation.constraints_hold_default (to_flat_operations ops)
+    constructor
+    · intro h
+      rw [List.cons_append] at h
+      obtain ⟨ h_op, h_rest ⟩ := constraints_hold_default_cons.mp h
+      obtain ⟨ h_ops, h_b ⟩ := ih.mp h_rest
+      exact ⟨ constraints_hold_default_cons.mpr ⟨ h_op, h_ops ⟩, h_b ⟩
+    · rintro ⟨ h_a, h_b ⟩
+      obtain ⟨ h_op, h_ops ⟩ := constraints_hold_default_cons.mp h_a
+      have h_rest := ih.mpr ⟨ h_ops, h_b ⟩
+      exact constraints_hold_default_cons.mpr ⟨ h_op, h_rest ⟩
+
+/--
+Main completeness theorem which proves that nested constraints imply flattened constraints
+using the default witness generator.
+
+This justifies only proving the nested version `Circuit.constraints_hold_from_list_default`,
+where constraints of subcircuits are replaced with higher-level statements
+that imply (or are implied by) those constraints.
+
+Note: Ideally, `can_replace_subcircuits` would prove both directions, and this would be just a special
+case. See https://github.com/Verified-zkEVM/clean/issues/42
+-/
+theorem can_replace_subcircuits_default : ∀ {ops: List (Operation F)},
+  constraints_hold_from_list_default ops → constraints_hold_default (to_flat_operations ops)
 := by
- sorry
+  intro ops h
+  -- `to_flat_operations.induct` (functional induction for `to_flat_operations`) is matching on
+  -- empty vs non-empty lists, and different cases for the head in the non-empty case, at the same time.
+  induction ops using to_flat_operations.induct with
+  | case1 => tauto
+  -- we can handle all non-empty cases except `SubCircuit` at once
+  | case2 ops _ ih | case3 ops _ ih | case4 ops _ ih | case5 ops _ ih =>
+    dsimp only [to_flat_operations]
+    generalize to_flat_operations ops = flatops at *
+    cases ops
+    <;> dsimp only [constraints_hold_from_list_default] at h
+    <;> cases flatops
+    <;> dsimp only [constraints_hold_default]
+    <;> tauto
+  | case6 ops circuit ih =>
+    dsimp only [to_flat_operations]
+    apply constraints_hold_default_append.mpr
+    cases ops
+    · use circuit.implied_by_completeness h; tauto
+    dsimp only [constraints_hold_from_list_default] at h
+    exact ⟨ circuit.implied_by_completeness h.left, ih h.right ⟩
+
 end PreOperation
 
 variable {α β: TypePair} [ProvableType F α] [ProvableType F β]
@@ -91,7 +179,7 @@ def formal_circuit_to_subcircuit (ctx: Context F)
 
     -- so we just need to go from flattened constraints to constraints
     guard_hyp h_holds : PreOperation.constraints_hold env (PreOperation.to_flat_operations ops)
-    exact PreOperation.can_flatten_first env ops h_holds
+    exact PreOperation.can_replace_subcircuits h_holds
 
     -- `implied_by_completeness`
     -- we are given that the assumptions are true
@@ -103,7 +191,7 @@ def formal_circuit_to_subcircuit (ctx: Context F)
     have h_holds : constraints_hold_from_list_default ops := circuit.completeness ctx b b_var rfl as
 
     -- so we just need to go from constraints to flattened constraints
-    exact PreOperation.can_flatten ops h_holds
+    exact PreOperation.can_replace_subcircuits_default h_holds
 
   ⟨ a_var, s ⟩
 
@@ -133,7 +221,7 @@ def formal_assertion_to_subcircuit (ctx: Context F)
 
     -- so we just need to go from flattened constraints to constraints
     guard_hyp h_holds : PreOperation.constraints_hold env (PreOperation.to_flat_operations ops)
-    exact PreOperation.can_flatten_first env ops h_holds
+    exact PreOperation.can_replace_subcircuits h_holds
 
     -- `implied_by_completeness`
     -- we are given that the assumptions and the spec are true
@@ -145,7 +233,7 @@ def formal_assertion_to_subcircuit (ctx: Context F)
     have h_holds : constraints_hold_from_list_default ops := circuit.completeness ctx b b_var rfl as.left as.right
 
     -- so we just need to go from constraints to flattened constraints
-    exact PreOperation.can_flatten ops h_holds
+    exact PreOperation.can_replace_subcircuits_default h_holds
 
   s
 end Circuit

Clean/Examples/Gadgets.lean

@@ -1,15 +1,9 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
 import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
 import Clean.GadgetsNew.Add8.Addition8
 
 section
 
-#eval!
+#eval
   let p := 1009
   let p_prime := Fact.mk prime_1009
   let p_non_zero := Fact.mk (by norm_num : p ≠ 0)

Clean/GadgetsNew/Add8/Addition8.lean

@@ -1,13 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
-import Clean.Utils.Field
-import Clean.GadgetsNew.ByteLookup
-import Clean.GadgetsNew.Boolean
 import Clean.GadgetsNew.Add8.Addition8Full
 
 namespace Add8

Clean/GadgetsNew/Add8/Addition8Full.lean

@@ -1,14 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
-import Clean.Circuit.SubCircuit
-import Clean.Utils.Field
-import Clean.GadgetsNew.ByteLookup
-import Clean.GadgetsNew.Boolean
 import Clean.GadgetsNew.Add8.Addition8FullCarry
 
 namespace Add8Full

Clean/GadgetsNew/Add8/Addition8FullCarry.lean

@@ -1,12 +1,4 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
 import Clean.Circuit.SubCircuit
-import Clean.Utils.Field
 import Clean.GadgetsNew.ByteLookup
 import Clean.GadgetsNew.Boolean
 import Clean.GadgetsNew.Add8.Theorems

Clean/GadgetsNew/Add8/Theorems.lean

@@ -1,10 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
 import Clean.Utils.Field
 
 namespace Add8Theorems

Clean/GadgetsNew/Addition32Full.lean

@@ -1,14 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
-import Clean.Circuit.Basic
-import Clean.Circuit.SubCircuit
-import Clean.Utils.Field
-import Clean.GadgetsNew.ByteLookup
-import Clean.GadgetsNew.Boolean
 import Clean.GadgetsNew.Add8.Addition8FullCarry
 import Clean.Types.U32
 

Clean/GadgetsNew/Boolean.lean

@@ -1,9 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
 import Clean.Circuit.Basic
 import Clean.Utils.Field
 

Clean/GadgetsNew/ByteLookup.lean

@@ -1,9 +1,3 @@
-import Mathlib.Algebra.Field.Basic
-import Mathlib.Data.ZMod.Basic
-import Clean.Utils.Primes
-import Clean.Utils.Vector
-import Clean.Circuit.Expression
-import Clean.Circuit.Provable
 import Clean.Circuit.Basic
 import Clean.Utils.Field
 
@@ -32,8 +26,7 @@ def ByteTable.completeness (x: F p) : x.val < 256 → ByteTable.contains (vec [x
   dsimp [Table.contains, ByteTable]
   use x.val
   simp [from_byte]
-  dsimp [vec]
-  rw [←Vector.vec_eq]
+  ext1
   have h' : (x.val) % 256 = x.val := by
     rw [Nat.mod_eq_iff_lt]; assumption; norm_num
   simp [h']