Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Circuit monad] Shared context #32

Merged
merged 2 commits into from
Dec 18, 2024
Merged

[Circuit monad] Shared context #32

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9e35648
pass current ctx down to subcircuits to get strictly increasing var i…
mitschabaude Dec 17, 2024
a0ba0bc
Merge branch 'main' into continuous-context
mitschabaude Dec 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 30 additions & 25 deletions Clean/Circuit/Circuit.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down Expand Up @@ -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

/--
Expand All @@ -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
Expand Down Expand Up @@ -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) :=
Expand All @@ -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
Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Loading