BooleanCircuit

formal source

  93/-- A Boolean circuit of size S over n input variables.
  94    This is a *restricted sub-ledger*: feed-forward, locally deterministic,
  95    no global coupling across the Z³ lattice. -/
  96structure BooleanCircuit (n : ℕ) where
  97  /-- Total number of gates (inputs + internal + output) -/
  98  gate_count : ℕ
  99  /-- The gates in topological order -/
 100  gates : Fin gate_count → Gate gate_count
 101  /-- Input gates each reference one variable in {0,..,n-1} -/
 102  input_var : ∀ i : Fin gate_count,
 103    (gates i).gtype = GateType.Input → ∃ _v : Fin n, True
 104  /-- At least one output gate exists -/
 105  has_output : ∃ i : Fin gate_count, (gates i).gtype = GateType.Output
 106
 107/-- The size of a circuit is its gate count. -/
 108def BooleanCircuit.size {n : ℕ} (c : BooleanCircuit n) : ℕ := c.gate_count
 109
 110/-- A Boolean circuit computes a specific Boolean function determined by its
 111    gate structure and input wiring. We model this as a bundled function field
 112    rather than implementing gate-by-gate evaluation (which would require
 113    enriching BooleanCircuit with explicit input wiring). -/
 114structure BooleanCircuitWithEval (n : ℕ) extends BooleanCircuit n where
 115  /-- The function computed by this circuit -/
 116  eval : Assignment n → Bool
 117
 118/-- A circuit with evaluation *decides* a formula if its eval matches
 119    satisfiability on every assignment. -/
 120def CircuitWithEvalDecides {n : ℕ} (c : BooleanCircuitWithEval n) (f : CNFFormula n) : Prop :=
 121  ∀ a : Assignment n, c.eval a = (f.satisfiedBy a)
 122
 123/-- For backward compatibility: CircuitEval and CircuitDecides use an
 124    existential model — a circuit "decides" a formula if there EXISTS an
 125    evaluation function consistent with the gate structure that matches
 126    satisfiability. This is the correct abstract model: it says "the