fix add8full soundness proof

Clean/GadgetsNew/Addition32Full.lean

@@ -15,21 +15,6 @@ namespace Addition32Full
 variable {p : ℕ} [Fact (p ≠ 0)] [Fact p.Prime]
 variable [p_large_enough: Fact (p > 512)]
 
-def less_than_p [p_pos: Fact (p ≠ 0)] (x: F p) : x.val < p := by
-  rcases p
-  · have : 0 ≠ 0 := p_pos.elim; tauto
-  · exact x.is_lt
-
-def mod (x: F p) (c: ℕ+) (lt: c < p) : F p :=
-  FieldUtils.nat_to_field (x.val % c) (by linarith [Nat.mod_lt x.val c.pos, lt])
-
-def mod_256 (x: F p) : F p :=
-  mod x 256 (by linarith [p_large_enough.elim])
-
-def floordiv [Fact (p ≠ 0)] (x: F p) (c: ℕ+) : F p :=
-  FieldUtils.nat_to_field (x.val / c) (by linarith [Nat.div_le_self x.val c, less_than_p x])
-
-
 open Circuit
 open Provable (field field2 fields)
 open ByteLookup

Clean/GadgetsNew/Addition8Full.lean

@@ -88,13 +88,15 @@ def circuit : FormalCircuit (F p) (add8_full_inputs p) (field (F p)) where
     specialize h_holds (by assumption)
     dsimp [ProvableType.from_values] at h_holds
 
-    guard_hyp h_holds : Add8FullCarry.circuit.spec { x := x, y := y, carry_in := carry_in } z
+    guard_hyp h_holds : Add8FullCarry.circuit.spec
+      { x := x, y := y, carry_in := carry_in }
+      { z := z, carry_out := env (ctx.offset + 1) }
 
     -- unfold `Add8Full` statements to show what the hypothesis is in our context
-    dsimp [Add8Full.circuit, Add8Full.spec] at h_holds
-    guard_hyp h_holds : z.val = (x.val + y.val + (0 : F p).val) % 256
-
-    simp at h_holds
+    dsimp [Add8FullCarry.circuit, Add8FullCarry.spec] at h_holds
+    -- discard second part of the spec
+    have ⟨ h_holds, _ ⟩ := h_holds
+    guard_hyp h_holds : z.val = (x.val + y.val + carry_in.val) % 256
     exact h_holds
 
   completeness := by