diff --git a/Clean/Circuit/Circuit.lean b/Clean/Circuit/Circuit.lean
index fd68a84..f9a63b9 100644
--- a/Clean/Circuit/Circuit.lean
+++ b/Clean/Circuit/Circuit.lean
@@ -156,8 +156,8 @@ def Stateful.operations (circuit: Stateful F α) : List (Operation F) :=
   (circuit Context.empty).1.2
 
 @[reducible]
-def output (circuit: Stateful F α) : α :=
-  (circuit Context.empty).2
+def output (circuit: Stateful F α) (ctx : Context F := Context.empty) : α :=
+  (circuit ctx).2
 
 @[simp]
 def as_stateful (f: Context F → Operation F × α) : Stateful F α := fun ctx  =>
@@ -244,8 +244,8 @@ namespace Adversarial
       | _ => constraints_hold_from_list env ops
 
   @[reducible, simp]
-  def constraints_hold [Field F] (env: (ℕ → F)) (circuit: Stateful F α) : Prop :=
-    constraints_hold_from_list env circuit.operations
+  def constraints_hold [Field F] (env: (ℕ → F)) (circuit: Stateful F α) (ctx : Context F := Context.empty) : Prop :=
+    constraints_hold_from_list env (circuit ctx).1.2
 end Adversarial
 
 /--
@@ -271,8 +271,8 @@ def constraints_hold_from_list [Field F] : List (Operation F) → Prop
     | _ => constraints_hold_from_list ops
 
 @[simp]
-def constraints_hold (circuit: Stateful F α) : Prop :=
-  constraints_hold_from_list (circuit Context.empty).1.2
+def constraints_hold (circuit: Stateful F α) (ctx : Context F := Context.empty) : Prop :=
+  constraints_hold_from_list (circuit ctx).1.2
 
 
 namespace PreOperation
@@ -366,20 +366,21 @@ where
 
   soundness:
     -- for all environments that determine witness generation
-    ∀ env: ℕ → F,
+    ∀ ctx : Context F, ∀ env: ℕ → F,
     -- for all inputs that satisfy the assumptions
     ∀ b : β.value, ∀ b_var : β.var, Provable.eval_env env b_var = b → assumptions b →
     -- if the constraints hold
-    Adversarial.constraints_hold env (main b_var) →
+    Adversarial.constraints_hold env (main b_var) ctx →
     -- the spec holds on the input and output
-    let a := Provable.eval_env env (output (main b_var))
+    let a := Provable.eval_env env (output (main b_var) ctx)
     spec b a
 
   completeness:
+    ∀ ctx : Context F,
     -- for all inputs that satisfy the assumptions
     ∀ b : β.value, ∀ b_var : β.var, Provable.eval F b_var = b → assumptions b →
     -- constraints hold when using the internal witness generator
-    constraints_hold (main b_var)
+    constraints_hold (main b_var) ctx
 
 @[simp]
 def subcircuit_soundness (circuit: FormalCircuit F β α) (b_var : β.var) (a_var : α.var) (env: ℕ → F) :=
@@ -392,10 +393,10 @@ def subcircuit_completeness (circuit: FormalCircuit F β α) (b_var : β.var) :=
   let b := Provable.eval F b_var
   circuit.assumptions b
 
-def formal_circuit_to_subcircuit
+def formal_circuit_to_subcircuit (ctx: Context F)
   (circuit: FormalCircuit F β α) (b_var : β.var) : α.var × SubCircuit F :=
   let main := circuit.main b_var
-  let res := main Context.empty
+  let res := main ctx
   -- TODO: weirdly, when we destructure we can't deduce origin of the results anymore
   -- let ((_, ops), a_var) := res
   let ops := res.1.2
@@ -420,7 +421,7 @@ def formal_circuit_to_subcircuit
 
     -- by soundness of the circuit, the spec is satisfied if only the constraints hold
     suffices h: Adversarial.constraints_hold_from_list env ops by
-      exact circuit.soundness env b b_var rfl as h
+      exact circuit.soundness ctx env b b_var rfl as h
 
     -- so we just need to go from flattened constraints to constraints
     guard_hyp h_holds : PreOperation.constraints_hold env (PreOperation.to_flat_operations ops)
@@ -433,7 +434,7 @@ def formal_circuit_to_subcircuit
     have as : circuit.assumptions b := h_completeness
 
     -- by completeness of the circuit, this means we can make the constraints hold
-    have h_holds : constraints_hold_from_list ops := circuit.completeness b b_var rfl as
+    have h_holds : constraints_hold_from_list 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
@@ -443,8 +444,8 @@ def formal_circuit_to_subcircuit
 -- run a sub-circuit
 @[simp]
 def subcircuit (circuit: FormalCircuit F β α) (b: β.var) := as_stateful (F:=F) (
-  fun _ =>
-    let ⟨ a, subcircuit ⟩ := formal_circuit_to_subcircuit circuit b
+  fun ctx =>
+    let ⟨ a, subcircuit ⟩ := formal_circuit_to_subcircuit ctx circuit b
     (Operation.Circuit subcircuit, a)
 )
 end Circuit
@@ -611,10 +612,11 @@ def circuit : FormalCircuit (F p) (fields (F p) 3) (field (F p)) where
   spec := spec
   soundness := by
     -- introductions
-    rintro env ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩ h_inputs as
+    rintro ctx env ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩
+    let i0 := ctx.offset
     let [x, y, carry_in] := inputs
     let [x_var, y_var, carry_in_var] := inputs_var
-    rintro h_holds z'
+    rintro h_inputs as h_holds z'
 
     -- characterize inputs
     injection h_inputs with h_inputs
@@ -628,9 +630,9 @@ def circuit : FormalCircuit (F p) (fields (F p) 3) (field (F p)) where
 
     -- simplify constraints hypothesis
     dsimp at h_holds
-    let z := env 0
-    let carry_out := env 1
-    rw [←(by rfl : z = env 0), ←(by rfl : carry_out = env 1)] at h_holds
+    let z := env i0
+    let carry_out := env (i0 + 1)
+    rw [←(by rfl : z = env i0), ←(by rfl : carry_out = env (i0 + 1))] at h_holds
     rw [hx, hy, hcarry_in] at h_holds
     let ⟨ h_byte, h_bool_carry, h_add ⟩ := h_holds
 
@@ -658,7 +660,7 @@ def circuit : FormalCircuit (F p) (fields (F p) 3) (field (F p)) where
 
   completeness := by
     -- introductions
-    rintro ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩ h_inputs
+    rintro ctx ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩ h_inputs
     let [x, y, carry_in] := inputs
     let [x_var, y_var, carry_in_var] := inputs_var
     rintro as
@@ -710,7 +712,8 @@ def circuit : FormalCircuit (F p) (fields (F p) 2) (field (F p)) where
   spec := spec
   soundness := by
     -- introductions
-    rintro env ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩ h_inputs as
+    rintro ctx env ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩ h_inputs as
+    let i0 := ctx.offset
     let [x, y] := inputs
     let [x_var, y_var] := inputs_var
     intro h_holds z
@@ -727,7 +730,7 @@ def circuit : FormalCircuit (F p) (fields (F p) 2) (field (F p)) where
 
     -- rewrite input and ouput values
     rw [hx, hy] at h_holds
-    rw [←(by rfl : z = env 0)] at h_holds
+    rw [←(by rfl : z = env i0)] at h_holds
 
     -- satisfy `Add8Full.assumptions` by using our own assumptions
     let ⟨ asx, asy ⟩ := as
@@ -745,7 +748,7 @@ def circuit : FormalCircuit (F p) (fields (F p) 2) (field (F p)) where
 
   completeness := by
     -- introductions
-    rintro ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩ h_inputs
+    rintro ctx ⟨ inputs, _ ⟩ ⟨ inputs_var, _ ⟩ h_inputs
     let [x, y] := inputs
     let [x_var, y_var] := inputs_var
     rintro as
@@ -775,9 +778,11 @@ end Add8
   let p_prime := Fact.mk prime_1009
   let p_non_zero := Fact.mk (by norm_num : p ≠ 0)
   let p_large_enough := Fact.mk (by norm_num : p > 512)
+
   let main := do
     let x ← witness (fun _ => 10)
     let y ← witness (fun _ => 20)
     add8_wrapped (p:=p) (vec [x, y])
+
   main.operations
 end