diff --git a/Cslib.lean b/Cslib.lean
index 9849e3df9..11234c94b 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -29,6 +29,11 @@ public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Computability.Automata.TwoWayNA.Basic
+public import Cslib.Computability.Circuit.Basic
+public import Cslib.Computability.Circuit.Homomorphism
+public import Cslib.Computability.Circuit.Program
+public import Cslib.Computability.Circuit.Signature
+public import Cslib.Computability.Circuit.Wire
 public import Cslib.Computability.Distributed.FLP.Algorithm
 public import Cslib.Computability.Distributed.FLP.CanReachVia
 public import Cslib.Computability.Distributed.FLP.Consensus
diff --git a/Cslib/Computability/Circuit/Basic.lean b/Cslib/Computability/Circuit/Basic.lean
new file mode 100644
index 000000000..c3d1508bd
--- /dev/null
+++ b/Cslib/Computability/Circuit/Basic.lean
@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+module
+
+public import Cslib.Computability.Circuit.Program
+
+/-!
+# Circuits
+
+A circuit is a straight-line `Program` together with a choice of output wires.
+Any input or internal-gate wire may be designated as an output, and designating
+an output is free: projections and duplicated outputs cost no gates. The size
+of a circuit is its gate count and its depth is the maximum depth of a
+designated output wire.
+
+A dependent pair `Σ gateCount, Circuit σ inputCount gateCount outputCount`
+hides the gate count for constructions that compute it along the way.
+
+For the standard Boolean circuit model, see [Arora and Barak, Section 6.1][AroraBarak09].
+Here a topological ordering is part of the representation, and the Boolean gate
+basis is generalized to an arbitrary `Signature` and `Interpretation`. Our size
+counts only operation gates; Arora and Barak count all nodes, including inputs.
+An output wire may also supply a later gate.
+
+This file defines evaluation (`Circuit.eval`), the flattened views
+`Circuit.computation` and `Circuit.trace`, the zero-gate identity circuit
+`Circuit.id`, and the structural bounded-fan-in predicate
+`Circuit.FanInAtMost`. Evaluation commutes with homomorphisms
+(`Circuit.map_eval`).
+
+## References
+
+* [S. Arora and B. Barak, *Computational Complexity: A Modern Approach*,
+  Section 6.1][AroraBarak09]
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits
+
+universe v u u₁ u₂
+
+variable {σ : Signature.{v}} {inputCount gateCount outputCount : Nat}
+variable {U : Type u} {U₁ : Type u₁} {U₂ : Type u₂}
+
+/-- A straight-line program with designated output wires. -/
+structure Circuit (σ : Signature) (inputCount gateCount outputCount : Nat) where
+  /-- The internal gates of the circuit. -/
+  program : Program σ inputCount gateCount
+  /-- The input or internal-gate wire carrying each output. -/
+  outputs : Fin outputCount → Wire inputCount gateCount
+
+/-- The zero-gate identity circuit, whose outputs are its inputs. -/
+def Circuit.id (σ : Signature) (inputCount : Nat) : Circuit σ inputCount 0 inputCount where
+  program := .empty
+  outputs := fun input => Wire.input input
+
+/-- Every gate in a circuit has at most `r` arguments. -/
+def Circuit.FanInAtMost (c : Circuit σ inputCount gateCount outputCount) (r : Nat) : Prop :=
+  c.program.FanInAtMost r
+
+/-- Bounded fan-in is decidable for every concrete circuit. -/
+instance Circuit.instDecidableFanInAtMost
+    (c : Circuit σ inputCount gateCount outputCount)
+    (r : Nat) : Decidable (c.FanInAtMost r) :=
+  Program.instDecidableFanInAtMost c.program r
+
+/-- The number of gates in a circuit. Designating outputs is free. -/
+def Circuit.size (_ : Circuit σ inputCount gateCount outputCount) : Nat :=
+  gateCount
+
+/-- The depth of every designated output wire in a circuit. -/
+def Circuit.outputDepths (c : Circuit σ inputCount gateCount outputCount) : Fin outputCount → Nat :=
+  c.program.wireDepths ∘ c.outputs
+
+/-- The maximum depth of a designated output wire in a circuit. -/
+def Circuit.depth (c : Circuit σ inputCount gateCount outputCount) : Nat :=
+  Fin.foldl outputCount (fun depth k => max depth (c.outputDepths k)) 0
+
+/-- Read the designated output wires after evaluating the program. -/
+def Circuit.eval
+    (c : Circuit σ inputCount gateCount outputCount)
+    (i : Interpretation σ U)
+    (x : Fin inputCount → U) : Fin outputCount → U :=
+  c.program.trace i x ∘ c.outputs
+
+@[simp] theorem Circuit.eval_id
+    (interpretation : Interpretation σ U)
+    (input : Fin inputCount → U) :
+    (Circuit.id σ inputCount).eval interpretation input = input := by
+  funext output
+  exact Program.trace_input .empty interpretation input output
+
+/-- Evaluating a circuit commutes with a homomorphism. -/
+theorem Circuit.map_eval
+    {i₁ : Interpretation σ U₁}
+    {i₂ : Interpretation σ U₂}
+    (c : Circuit σ inputCount gateCount outputCount)
+    (h : Homomorphism i₁ i₂)
+    (x : Fin inputCount → U₁) :
+    h.map ∘ c.eval i₁ x = c.eval i₂ (h.map ∘ x) := by
+  funext k
+  exact congrFun (c.program.map_trace h x) (c.outputs k)
+
+/-- All internal-gate values followed by the designated output values. -/
+def Circuit.computation
+    (c : Circuit σ inputCount gateCount outputCount)
+    (i : Interpretation σ U)
+    (x : Fin inputCount → U) : Fin (gateCount + outputCount) → U :=
+  Fin.addCases (c.program.eval i x) (c.eval i x)
+
+/-- The input and internal-gate values followed by the designated outputs. -/
+def Circuit.trace
+    (c : Circuit σ inputCount gateCount outputCount)
+    (i : Interpretation σ U)
+    (x : Fin inputCount → U) : Fin (inputCount + gateCount + outputCount) → U :=
+  Fin.addCases (c.program.trace i x) (c.eval i x)
+
+end Cslib.Circuits
diff --git a/Cslib/Computability/Circuit/Homomorphism.lean b/Cslib/Computability/Circuit/Homomorphism.lean
new file mode 100644
index 000000000..1e0e5ed7f
--- /dev/null
+++ b/Cslib/Computability/Circuit/Homomorphism.lean
@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+module
+
+public import Cslib.Computability.Circuit.Signature
+
+/-!
+# Homomorphisms of interpretations
+
+A homomorphism between two interpretations of the same signature is a map of
+carriers that commutes with every operation. This file defines identity and
+composition and proves their laws.
+
+The main use of homomorphisms in this library is that evaluation of lines,
+programs, and circuits commutes with them (`Line.map_eval`, `Program.map_eval`,
+`Program.map_trace`, and `Circuit.map_eval`).
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits
+
+universe v u u₁ u₂ u₃ u₄
+
+variable {σ : Signature.{v}} {U : Type u}
+variable {U₁ : Type u₁} {U₂ : Type u₂} {U₃ : Type u₃} {U₄ : Type u₄}
+
+/-- A map that preserves every operation in a pair of interpretations. -/
+structure Homomorphism (i₁ : Interpretation σ U₁) (i₂ : Interpretation σ U₂) where
+  /-- The underlying map. -/
+  map : U₁ → U₂
+  /-- The map commutes with every operation in the signature. -/
+  homomorphic :
+    ∀ (op : σ.Op) (input : Fin (σ.Arity op) → U₁),
+      map (i₁ op input) = i₂ op (map ∘ input)
+
+namespace Homomorphism
+
+@[ext] theorem ext
+    {source : Interpretation σ U₁}
+    {target : Interpretation σ U₂}
+    {left right : Homomorphism source target}
+    (map_eq : left.map = right.map) : left = right := by
+  cases left
+  cases right
+  cases map_eq
+  rfl
+
+/-- The identity map is a homomorphism. -/
+def id (interpretation : Interpretation σ U) :
+    Homomorphism interpretation interpretation where
+  map := _root_.id
+  homomorphic := by
+    intro op input
+    rfl
+
+/-- Compose homomorphisms in the direction of their underlying maps. -/
+def comp
+    {i₁ : Interpretation σ U₁}
+    {i₂ : Interpretation σ U₂}
+    {i₃ : Interpretation σ U₃}
+    (outer : Homomorphism i₂ i₃)
+    (inner : Homomorphism i₁ i₂) : Homomorphism i₁ i₃ where
+  map := outer.map ∘ inner.map
+  homomorphic := by
+    intro op input
+    rw [Function.comp_apply, inner.homomorphic, outer.homomorphic]
+    congr 1
+
+@[simp] theorem id_map
+    (interpretation : Interpretation σ U) :
+    (Homomorphism.id interpretation).map = _root_.id := rfl
+
+@[simp] theorem comp_map
+    {i₁ : Interpretation σ U₁}
+    {i₂ : Interpretation σ U₂}
+    {i₃ : Interpretation σ U₃}
+    (outer : Homomorphism i₂ i₃)
+    (inner : Homomorphism i₁ i₂) :
+    (outer.comp inner).map = outer.map ∘ inner.map := rfl
+
+@[simp] theorem id_comp
+    {source : Interpretation σ U₁}
+    {target : Interpretation σ U₂}
+    (homomorphism : Homomorphism source target) :
+    (Homomorphism.id target).comp homomorphism = homomorphism := by
+  apply Homomorphism.ext
+  rfl
+
+@[simp] theorem comp_id
+    {source : Interpretation σ U₁}
+    {target : Interpretation σ U₂}
+    (homomorphism : Homomorphism source target) :
+    homomorphism.comp (Homomorphism.id source) = homomorphism := by
+  apply Homomorphism.ext
+  rfl
+
+theorem comp_assoc
+    {i₁ : Interpretation σ U₁}
+    {i₂ : Interpretation σ U₂}
+    {i₃ : Interpretation σ U₃}
+    {i₄ : Interpretation σ U₄}
+    (outer : Homomorphism i₃ i₄)
+    (middle : Homomorphism i₂ i₃)
+    (inner : Homomorphism i₁ i₂) :
+    (outer.comp middle).comp inner = outer.comp (middle.comp inner) := by
+  apply Homomorphism.ext
+  rfl
+
+end Homomorphism
+
+end Cslib.Circuits
diff --git a/Cslib/Computability/Circuit/Program.lean b/Cslib/Computability/Circuit/Program.lean
new file mode 100644
index 000000000..47de25b02
--- /dev/null
+++ b/Cslib/Computability/Circuit/Program.lean
@@ -0,0 +1,406 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+module
+
+public import Cslib.Computability.Circuit.Homomorphism
+public import Cslib.Computability.Circuit.Wire
+
+/-!
+# Straight-line programs
+
+A program is a topologically ordered sequence of gates. Each `Line` records an
+operation and its argument wires. The gate-count index ensures that wires refer
+only to original inputs or earlier gates.
+
+This file defines
+
+* lines, their evaluation and depth, and `Line.mapWires` together with the
+  transport lemmas `Line.eval_mapWires` and `Line.eval_mapRenaming`;
+* programs, their evaluation `Program.eval`, the input-and-gate valuation
+  `Program.trace`, gate depths, and the bounded-fan-in predicate
+  `Program.FanInAtMost`;
+* the scalar views `Program.gateFunction` and `Program.wireFunction`, and the
+  widened line collection `Program.lines` with `Program.lines_eval`.
+
+Evaluation of lines and programs commutes with homomorphisms
+(`Line.map_eval`, `Program.map_eval`, `Program.map_trace`).
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits
+
+universe v u u₁ u₂
+
+variable {σ : Signature.{v}} {inputCount gateCount : Nat}
+variable {sourceInputCount targetInputCount sourceGateCount targetGateCount : Nat}
+variable {U : Type u} {U₁ : Type u₁} {U₂ : Type u₂}
+
+/-- One gate together with the wires supplying its arguments. -/
+structure Line (σ : Signature) (inputCount gateCount : Nat) where
+  /-- The operation performed by the gate. -/
+  op : σ.Op
+  /-- The wire supplying each argument of the operation. -/
+  wires : Fin (σ.Arity op) → Wire inputCount gateCount
+
+/-- Apply a function to every wire read by a line. -/
+def Line.mapWires
+    (line : Line σ sourceInputCount sourceGateCount)
+    (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount) :
+    Line σ targetInputCount targetGateCount where
+  op := line.op
+  wires := wireMap ∘ line.wires
+
+@[simp] theorem Line.mapWires_op
+    (line : Line σ sourceInputCount sourceGateCount)
+    (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount) :
+    (line.mapWires wireMap).op = line.op := rfl
+
+@[simp] theorem Line.mapWires_wires
+    (line : Line σ sourceInputCount sourceGateCount)
+    (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount)
+    (argument : Fin (σ.Arity line.op)) :
+    (line.mapWires wireMap).wires argument = wireMap (line.wires argument) := rfl
+
+/-- A topologically ordered straight-line program, indexed by its gate count. -/
+inductive Program (σ : Signature.{v}) (inputCount : Nat) : Nat → Type v where
+  | empty : Program σ inputCount 0
+  | gate {gateCount : Nat} :
+      Program σ inputCount gateCount → Line σ inputCount gateCount →
+        Program σ inputCount (gateCount + 1)
+
+/-- Every gate in a program has at most `r` arguments. -/
+def Program.FanInAtMost {gateCount : Nat} : (program : Program σ inputCount gateCount) → Nat → Prop
+  | .empty, _ => True
+  | .gate program line, r =>
+      program.FanInAtMost r ∧ σ.Arity line.op ≤ r
+
+/-- Bounded fan-in is decidable for every concrete program. -/
+instance Program.instDecidableFanInAtMost {gateCount : Nat}
+    (program : Program σ inputCount gateCount)
+    (r : Nat) : Decidable (program.FanInAtMost r) :=
+  match program with
+  | .empty => isTrue trivial
+  | .gate prior line =>
+      @instDecidableAnd (prior.FanInAtMost r)
+        (σ.Arity line.op ≤ r)
+        (Program.instDecidableFanInAtMost prior r) inferInstance
+
+/-- Evaluate a line from the values of the inputs and preceding gates. -/
+def Line.eval
+    (line : Line σ inputCount gateCount)
+    (i : Interpretation σ U)
+    (inputs : Fin inputCount → U)
+    (gates : Fin gateCount → U) : U :=
+  i line.op (Fin.addCases inputs gates ∘ line.wires)
+
+/-- Mapping a line's wires preserves evaluation when the new valuation agrees
+with the old valuation along the map. The source and target input namespaces
+may differ. -/
+theorem Line.eval_mapWires
+    (line : Line σ sourceInputCount sourceGateCount)
+    (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount)
+    (interpretation : Interpretation σ U)
+    (oldInputs : Fin sourceInputCount → U)
+    (newInputs : Fin targetInputCount → U)
+    (oldGates : Fin sourceGateCount → U)
+    (newGates : Fin targetGateCount → U)
+    (preserves : ∀ wire : Wire sourceInputCount sourceGateCount,
+      (Fin.addCases newInputs newGates : Wire targetInputCount targetGateCount → U) (wireMap wire) =
+        (Fin.addCases oldInputs oldGates : Wire sourceInputCount sourceGateCount → U) wire) :
+    (line.mapWires wireMap).eval interpretation newInputs newGates =
+      line.eval interpretation oldInputs oldGates := by
+  unfold Line.mapWires Line.eval
+  congr 1
+  funext argument
+  simp only [Function.comp_apply]
+  exact preserves (line.wires argument)
+
+/-- Specialization of `Line.eval_mapWires` to an input-fixing wire renaming. -/
+theorem Line.eval_mapRenaming
+    (line : Line σ inputCount sourceGateCount)
+    (ρ : Wire.Renaming inputCount sourceGateCount targetGateCount)
+    (interpretation : Interpretation σ U)
+    (inputs : Fin inputCount → U)
+    (oldGates : Fin sourceGateCount → U)
+    (newGates : Fin targetGateCount → U)
+    (preservesGates : ∀ gate,
+      (Fin.addCases inputs newGates : Wire inputCount targetGateCount → U) (ρ.gates gate) =
+        oldGates gate) :
+    (line.mapWires ρ).eval interpretation inputs newGates =
+      line.eval interpretation inputs oldGates := by
+  apply Line.eval_mapWires
+  exact ρ.value_apply inputs oldGates newGates preservesGates
+
+/-- The depth of a line, given the depth of every wire it may read. -/
+def Line.depth
+    (line : Line σ inputCount gateCount)
+    (wireDepths : Wire inputCount gateCount → Nat) : Nat :=
+  Nat.succ <| Fin.foldl (σ.Arity line.op)
+    (fun depth k => max depth (wireDepths (line.wires k))) 0
+
+/-- Evaluating a line commutes with a homomorphism. -/
+theorem Line.map_eval
+    {i₁ : Interpretation σ U₁}
+    {i₂ : Interpretation σ U₂}
+    (line : Line σ inputCount gateCount)
+    (h : Homomorphism i₁ i₂)
+    (inputs : Fin inputCount → U₁)
+    (gates : Fin gateCount → U₁) :
+    h.map (line.eval i₁ inputs gates) =
+      line.eval i₂ (h.map ∘ inputs) (h.map ∘ gates) := by
+  rw [Line.eval, Line.eval, h.homomorphic]
+  congr 1
+  funext k
+  simp only [Function.comp_apply]
+  exact Fin.addCases (fun _ => by simp) (fun _ => by simp) (line.wires k)
+
+/-- Evaluate every gate in a program, in program order. -/
+def Program.eval {gateCount : Nat}
+    (p : Program σ inputCount gateCount)
+    (i : Interpretation σ U)
+    (x : Fin inputCount → U) : Fin gateCount → U :=
+  match p with
+  | .empty => Fin.elim0
+  | .gate p line =>
+      let prior := p.eval i x
+      Fin.lastCases (line.eval i x prior) prior
+
+@[simp] theorem Program.eval_gate_last
+    (program : Program σ inputCount gateCount)
+    (line : Line σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (input : Fin inputCount → U) :
+    (program.gate line).eval interpretation input (Fin.last gateCount) =
+      line.eval interpretation input (program.eval interpretation input) := by
+  simp [Program.eval]
+
+@[simp] theorem Program.eval_gate_castSucc
+    (program : Program σ inputCount gateCount)
+    (line : Line σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (input : Fin inputCount → U)
+    (gate : Fin gateCount) :
+    (program.gate line).eval interpretation input gate.castSucc =
+      program.eval interpretation input gate := by
+  simp [Program.eval]
+
+/-- The depth of every gate in a program. Inputs have implicit depth zero. -/
+def Program.depths {gateCount : Nat} (p : Program σ inputCount gateCount) : Fin gateCount → Nat :=
+  match p with
+  | .empty => Fin.elim0
+  | .gate p line =>
+      let prior := p.depths
+      let wireDepths := Fin.addCases (fun _ => 0) prior
+      Fin.lastCases (line.depth wireDepths) prior
+
+/-- The depth of every input or gate wire in a program. -/
+def Program.wireDepths (p : Program σ inputCount gateCount) : Wire inputCount gateCount → Nat :=
+  Fin.addCases (fun _ => 0) p.depths
+
+/-- The maximum depth of any gate in a program. -/
+def Program.depth (p : Program σ inputCount gateCount) : Nat :=
+  Fin.foldl gateCount (fun depth k => max depth (p.depths k)) 0
+
+/-- Evaluating a program commutes with a homomorphism. -/
+theorem Program.map_eval
+    {i₁ : Interpretation σ U₁}
+    {i₂ : Interpretation σ U₂}
+    (p : Program σ inputCount gateCount)
+    (h : Homomorphism i₁ i₂)
+    (x : Fin inputCount → U₁) :
+    h.map ∘ p.eval i₁ x = p.eval i₂ (h.map ∘ x) := by
+  induction p with
+  | empty =>
+      funext k
+      exact Fin.elim0 k
+  | gate p line ih =>
+      funext k
+      refine Fin.lastCases ?_ ?_ k
+      · simpa only [Program.eval, Function.comp_apply, Fin.lastCases_last, ih] using
+          line.map_eval h x (p.eval i₁ x)
+      · intro j
+        simpa only [Program.eval, Function.comp_apply, Fin.lastCases_castSucc] using
+          congrFun ih j
+
+/-- The input values followed by all gate values, in program order. -/
+def Program.trace
+    (p : Program σ inputCount gateCount)
+    (i : Interpretation σ U)
+    (x : Fin inputCount → U) : Fin (inputCount + gateCount) → U :=
+  Fin.addCases x (p.eval i x)
+
+@[simp] theorem Program.trace_input
+    (program : Program σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (input : Fin inputCount → U)
+    (sourceInput : Fin inputCount) :
+    program.trace interpretation input (Wire.input sourceInput) =
+      input sourceInput := by
+  simp [Program.trace]
+
+@[simp] theorem Program.trace_gate_castSucc
+    (program : Program σ inputCount gateCount)
+    (line : Line σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (input : Fin inputCount → U)
+    (wire : Wire inputCount gateCount) :
+    (program.gate line).trace interpretation input wire.castSucc =
+      program.trace interpretation input wire := by
+  unfold Program.trace
+  refine Fin.addCases (fun original => ?_) (fun gate => ?_) wire
+  · simp [Fin.castSucc_castAdd]
+  · simp
+
+@[simp] theorem Program.trace_gate_last
+    (program : Program σ inputCount gateCount)
+    (line : Line σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (input : Fin inputCount → U) :
+    (program.gate line).trace interpretation input (Fin.last (inputCount + gateCount)) =
+      line.eval interpretation input (program.eval interpretation input) := by
+  rw [← Fin.natAdd_last (n := inputCount) (m := gateCount)]
+  unfold Program.trace
+  rw [Fin.addCases_right]
+  simp
+
+/-- Evaluating every input and gate wire commutes with a homomorphism. -/
+theorem Program.map_trace
+    {i₁ : Interpretation σ U₁}
+    {i₂ : Interpretation σ U₂}
+    (p : Program σ inputCount gateCount)
+    (h : Homomorphism i₁ i₂)
+    (x : Fin inputCount → U₁) :
+    h.map ∘ p.trace i₁ x = p.trace i₂ (h.map ∘ x) := by
+  funext wire
+  refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire
+  · simp [Program.trace, Function.comp_apply]
+  · simpa [Program.trace, Function.comp_apply] using congrFun (p.map_eval h x) gate
+
+/-- The scalar function computed by an internal gate. -/
+def Program.gateFunction
+    (program : Program σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (gate : Fin gateCount)
+    (input : Fin inputCount → U) : U :=
+  program.eval interpretation input gate
+
+/-- The scalar function carried by an input or internal-gate wire. -/
+def Program.wireFunction
+    (program : Program σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (wire : Wire inputCount gateCount)
+    (input : Fin inputCount → U) : U :=
+  program.trace interpretation input wire
+
+@[simp] theorem Program.gateFunction_apply
+    (program : Program σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (gate : Fin gateCount)
+    (input : Fin inputCount → U) :
+    program.gateFunction interpretation gate input =
+      program.eval interpretation input gate := rfl
+
+@[simp] theorem Program.wireFunction_input
+    (program : Program σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (inputWire : Fin inputCount) :
+    program.wireFunction interpretation (Wire.input inputWire) =
+      fun input => input inputWire := by
+  funext input
+  simp [Program.wireFunction, Program.trace]
+
+@[simp] theorem Program.wireFunction_gate
+    (program : Program σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (gate : Fin gateCount) :
+    program.wireFunction interpretation (Wire.gate gate) =
+      program.gateFunction interpretation gate := by
+  funext input
+  simp [Program.wireFunction, Program.trace]
+
+@[simp] theorem Program.gateFunction_gate_last
+    (program : Program σ inputCount gateCount)
+    (line : Line σ inputCount gateCount)
+    (interpretation : Interpretation σ U) :
+    (program.gate line).gateFunction interpretation (Fin.last gateCount) =
+      fun input => line.eval interpretation input
+        (program.eval interpretation input) := by
+  funext input
+  exact Program.eval_gate_last program line interpretation input
+
+@[simp] theorem Program.gateFunction_gate_castSucc
+    (program : Program σ inputCount gateCount)
+    (line : Line σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (gate : Fin gateCount) :
+    (program.gate line).gateFunction interpretation gate.castSucc =
+      program.gateFunction interpretation gate := by
+  funext input
+  exact Program.eval_gate_castSucc program line interpretation input gate
+
+@[simp] theorem Program.trace_gateWire
+    (program : Program σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (input : Fin inputCount → U)
+    (gate : Fin gateCount) :
+    program.trace interpretation input (Wire.gate gate) =
+      program.gateFunction interpretation gate input := by
+  unfold Program.trace Program.gateFunction Wire.gate
+  simp
+
+/-- The program's lines, each widened to the final wire namespace. -/
+def Program.lines {gateCount : Nat} :
+    (program : Program σ inputCount gateCount) → Fin gateCount → Line σ inputCount gateCount
+  | .empty => Fin.elim0
+  | @Program.gate _ _ gateCount program line =>
+      Fin.lastCases
+        (line.mapWires Wire.Renaming.castSucc)
+        (fun gate => (program.lines gate).mapWires Wire.Renaming.castSucc)
+
+@[simp] theorem Program.lines_gate_last
+    (program : Program σ inputCount gateCount)
+    (line : Line σ inputCount gateCount) :
+    (program.gate line).lines (Fin.last gateCount) =
+      line.mapWires Wire.Renaming.castSucc := by
+  simp [Program.lines]
+
+@[simp] theorem Program.lines_gate_castSucc
+    (program : Program σ inputCount gateCount)
+    (line : Line σ inputCount gateCount)
+    (gate : Fin gateCount) :
+    (program.gate line).lines gate.castSucc =
+      (program.lines gate).mapWires Wire.Renaming.castSucc := by
+  simp [Program.lines]
+
+/-- A widened line evaluates to the value of its corresponding program gate. -/
+theorem Program.lines_eval
+    (program : Program σ inputCount gateCount)
+    (interpretation : Interpretation σ U)
+    (input : Fin inputCount → U)
+    (gate : Fin gateCount) :
+    (program.lines gate).eval interpretation input
+        (program.eval interpretation input) =
+      program.eval interpretation input gate := by
+  induction program with
+  | empty => exact Fin.elim0 gate
+  | @gate gateCount program line ih =>
+      have evalWidened (oldLine : Line σ inputCount gateCount) :
+          (oldLine.mapWires Wire.Renaming.castSucc).eval interpretation input
+              ((program.gate line).eval interpretation input) =
+            oldLine.eval interpretation input
+              (program.eval interpretation input) := by
+        apply Line.eval_mapWires
+        intro wire
+        simpa only [Wire.Renaming.castSucc_apply, Program.trace] using
+          Program.trace_gate_castSucc program line interpretation input wire
+      refine Fin.lastCases ?_ (fun priorGate => ?_) gate
+      · simpa only [Program.lines_gate_last, Program.eval_gate_last] using
+          evalWidened line
+      · simp only [Program.lines_gate_castSucc, Program.eval_gate_castSucc]
+        exact (evalWidened (program.lines priorGate)).trans (ih priorGate)
+
+end Cslib.Circuits
diff --git a/Cslib/Computability/Circuit/Signature.lean b/Cslib/Computability/Circuit/Signature.lean
new file mode 100644
index 000000000..357679aaf
--- /dev/null
+++ b/Cslib/Computability/Circuit/Signature.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+module
+
+public import Cslib.Init
+
+/-!
+# Signatures and interpretations
+
+A `Signature` specifies operation symbols with finite arities. The set of symbols
+may be infinite, and their arities need not have a uniform bound.
+An `Interpretation` assigns each symbol an operation on a carrier type.
+Programs and circuits keep the signature separate from its interpretation.
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits
+
+universe v
+
+/-- A collection of operation symbols, each with a fixed finite arity. -/
+structure Signature where
+  /-- The operation symbols of the signature. -/
+  Op : Type v
+  /-- The number of arguments taken by each operation symbol. -/
+  Arity : Op → Nat
+
+/-- An interpretation assigns an operation on `Carrier` to every symbol in `σ`. -/
+abbrev Interpretation (σ : Signature) (Carrier : Type*) :=
+  (op : σ.Op) → (Fin (σ.Arity op) → Carrier) → Carrier
+
+end Cslib.Circuits
diff --git a/Cslib/Computability/Circuit/Wire.lean b/Cslib/Computability/Circuit/Wire.lean
new file mode 100644
index 000000000..d312a8647
--- /dev/null
+++ b/Cslib/Computability/Circuit/Wire.lean
@@ -0,0 +1,189 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+module
+
+public import Cslib.Init
+public import Mathlib.Data.Fin.SuccPred
+public import Mathlib.Logic.Equiv.Defs
+
+/-!
+# Circuit wires and renamings
+
+A `Wire inputCount gateCount` refers to an original input or an internal gate.
+`Wire.Renaming` fixes the original inputs and maps each gate to an input or gate
+in the target namespace. This file provides identity and composition, extension
+by a gate, replacement of the last gate, and renaming by a permutation.
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits
+
+/-- A wire is either an original input or the output of an earlier gate. -/
+abbrev Wire (inputCount gateCount : Nat) := Fin (inputCount + gateCount)
+
+/-- Regard an original input as a wire. -/
+abbrev Wire.input {inputCount gateCount : Nat} (input : Fin inputCount) :
+    Wire inputCount gateCount :=
+  Fin.castAdd gateCount input
+
+/-- Regard a gate output as a wire. -/
+abbrev Wire.gate {inputCount gateCount : Nat} (gate : Fin gateCount) : Wire inputCount gateCount :=
+  Fin.natAdd inputCount gate
+
+/-- A renaming of gate wires that fixes every original input. Gate wires may be
+sent to either inputs or gates in the target namespace. -/
+structure Wire.Renaming (inputCount sourceGateCount targetGateCount : Nat) where
+  /-- The target wire representing each source gate. -/
+  gates : Fin sourceGateCount → Wire inputCount targetGateCount
+
+namespace Wire.Renaming
+
+variable {inputCount gateCount sourceGateCount middleGateCount targetGateCount : Nat}
+variable {U : Type*}
+
+/-- Apply an input-fixing wire renaming. -/
+def apply (ρ : Wire.Renaming inputCount sourceGateCount targetGateCount) :
+    Wire inputCount sourceGateCount → Wire inputCount targetGateCount :=
+  Fin.addCases Wire.input ρ.gates
+
+instance : CoeFun (Wire.Renaming inputCount sourceGateCount targetGateCount)
+    fun _ => Wire inputCount sourceGateCount → Wire inputCount targetGateCount :=
+  ⟨apply⟩
+
+@[simp] theorem apply_input
+    (ρ : Wire.Renaming inputCount sourceGateCount targetGateCount) (input : Fin inputCount) :
+    ρ (Wire.input input) = Wire.input input := by
+  simp [apply]
+
+@[simp] theorem apply_gate
+    (ρ : Wire.Renaming inputCount sourceGateCount targetGateCount) (gate : Fin sourceGateCount) :
+    ρ (Wire.gate gate) = ρ.gates gate := by
+  simp [apply]
+
+/-- The identity wire renaming. -/
+def id : Wire.Renaming inputCount gateCount gateCount where
+  gates := Wire.gate
+
+@[simp] theorem id_apply (wire : Wire inputCount gateCount) :
+    (id : Wire.Renaming inputCount gateCount gateCount) wire = wire := by
+  refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire <;> simp [id]
+
+/-- Compose input-fixing wire renamings. -/
+def comp
+    (outer : Wire.Renaming inputCount middleGateCount targetGateCount)
+    (inner : Wire.Renaming inputCount sourceGateCount middleGateCount) :
+    Wire.Renaming inputCount sourceGateCount targetGateCount where
+  gates := outer ∘ inner.gates
+
+@[simp] theorem comp_apply
+    (outer : Wire.Renaming inputCount middleGateCount targetGateCount)
+    (inner : Wire.Renaming inputCount sourceGateCount middleGateCount)
+    (wire : Wire inputCount sourceGateCount) :
+    (outer.comp inner) wire = outer (inner wire) := by
+  refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire <;>
+    simp [comp, Function.comp_apply]
+
+/-- Include all wires into a namespace with one additional gate. -/
+def castSucc : Wire.Renaming inputCount gateCount (gateCount + 1) where
+  gates := fun gate => Wire.gate gate.castSucc
+
+@[simp] theorem castSucc_apply (wire : Wire inputCount gateCount) :
+    (castSucc : Wire.Renaming inputCount gateCount (gateCount + 1)) wire = wire.castSucc := by
+  refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire
+  · simp [castSucc, Fin.castSucc_castAdd]
+  · simp [castSucc]
+
+/-- Extend a renaming while replacing the new last gate by an existing wire. -/
+def skipLast
+    (prior : Wire.Renaming inputCount sourceGateCount targetGateCount)
+    (replacement : Wire inputCount targetGateCount) :
+    Wire.Renaming inputCount (sourceGateCount + 1) targetGateCount where
+  gates := Fin.lastCases replacement prior.gates
+
+theorem skipLast_gate_last
+    (prior : Wire.Renaming inputCount sourceGateCount targetGateCount)
+    (replacement : Wire inputCount targetGateCount) :
+    prior.skipLast replacement (Wire.gate (Fin.last sourceGateCount)) = replacement := by
+  rw [apply_gate]
+  simp [skipLast]
+
+@[simp] theorem skipLast_lastWire
+    (prior : Wire.Renaming inputCount sourceGateCount targetGateCount)
+    (replacement : Wire inputCount targetGateCount) :
+    prior.skipLast replacement (Fin.last (inputCount + sourceGateCount)) = replacement := by
+  rw [← Fin.natAdd_last (n := inputCount) (m := sourceGateCount)]
+  exact skipLast_gate_last prior replacement
+
+@[simp] theorem skipLast_castSucc
+    (prior : Wire.Renaming inputCount sourceGateCount targetGateCount)
+    (replacement : Wire inputCount targetGateCount)
+    (wire : Wire inputCount sourceGateCount) :
+    prior.skipLast replacement wire.castSucc = prior wire := by
+  refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire
+  · simp [Fin.castSucc_castAdd]
+  · simp [skipLast]
+
+/-- Extend a renaming and retain the new last gate as a fresh target gate. -/
+def appendLast
+    (prior : Wire.Renaming inputCount sourceGateCount targetGateCount) :
+    Wire.Renaming inputCount (sourceGateCount + 1) (targetGateCount + 1) where
+  gates := Fin.lastCases (Wire.gate (Fin.last targetGateCount)) fun gate =>
+    (prior.gates gate).castSucc
+
+theorem appendLast_gate_last
+    (prior : Wire.Renaming inputCount sourceGateCount targetGateCount) :
+    prior.appendLast (Wire.gate (Fin.last sourceGateCount)) =
+      Wire.gate (Fin.last targetGateCount) := by
+  rw [apply_gate]
+  simp [appendLast]
+
+@[simp] theorem appendLast_lastWire
+    (prior : Wire.Renaming inputCount sourceGateCount targetGateCount) :
+    prior.appendLast (Fin.last (inputCount + sourceGateCount)) =
+      Wire.gate (Fin.last targetGateCount) := by
+  rw [← Fin.natAdd_last (n := inputCount) (m := sourceGateCount)]
+  exact appendLast_gate_last prior
+
+@[simp] theorem appendLast_castSucc
+    (prior : Wire.Renaming inputCount sourceGateCount targetGateCount)
+    (wire : Wire inputCount sourceGateCount) :
+    prior.appendLast wire.castSucc = (prior wire).castSucc := by
+  refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire
+  · simp [Fin.castSucc_castAdd]
+  · simp [appendLast]
+
+/-- Rename gate wires by a permutation. -/
+def ofPermutation (permutation : Equiv.Perm (Fin gateCount)) :
+    Wire.Renaming inputCount gateCount gateCount where
+  gates := fun gate => Wire.gate (permutation gate)
+
+theorem ofPermutation_gate
+    (permutation : Equiv.Perm (Fin gateCount)) (gate : Fin gateCount) :
+    (ofPermutation permutation : Wire.Renaming inputCount gateCount gateCount) (Wire.gate gate) =
+      Wire.gate (permutation gate) := by
+  simp [ofPermutation]
+
+/-- A source and target gate valuation agree along a renaming when they agree
+on the image of every source gate. Original inputs agree automatically. -/
+theorem value_apply
+    (ρ : Wire.Renaming inputCount sourceGateCount targetGateCount)
+    (inputs : Fin inputCount → U)
+    (oldGates : Fin sourceGateCount → U)
+    (newGates : Fin targetGateCount → U)
+    (preservesGates : ∀ gate,
+      (Fin.addCases inputs newGates : Wire inputCount targetGateCount → U) (ρ.gates gate) =
+        oldGates gate)
+    (wire : Wire inputCount sourceGateCount) :
+    (Fin.addCases inputs newGates : Wire inputCount targetGateCount → U) (ρ wire) =
+      (Fin.addCases inputs oldGates : Wire inputCount sourceGateCount → U) wire := by
+  refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire
+  · simp
+  · simpa using preservesGates gate
+
+end Wire.Renaming
+
+end Cslib.Circuits
diff --git a/Cslib/Computability/README.md b/Cslib/Computability/README.md
index f2ab58842..8b602532d 100644
--- a/Cslib/Computability/README.md
+++ b/Cslib/Computability/README.md
@@ -25,6 +25,10 @@ This approach enables:
 2. Applying CSLib's [logics](../Logics) to reason about computational models.
 3. Developing connections between computability models and other areas (like the constructions of automata based on transition systems).
 
+The circuit development follows this principle: signatures describe gate bases independently of
+their interpretations, while topologically ordered programs and designated output wires provide a
+generic model for Boolean, arithmetic, and other finite-arity circuits.
+
 ### Separation from languages
 
 Some of the developments here are close to [Languages](../Languages), but are placed here instead because the emphasis is on formal languages over words and models typically linked to computability studies.
diff --git a/CslibTests.lean b/CslibTests.lean
index a84190e52..f7b53299f 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -2,6 +2,7 @@ import CslibTests.Bisimulation
 import CslibTests.CCS
 import CslibTests.CCS.VendingMachine
 import CslibTests.CLL
+import CslibTests.Circuits
 import CslibTests.Commitment
 import CslibTests.Congruence
 import CslibTests.DFA
diff --git a/CslibTests/Circuits.lean b/CslibTests/Circuits.lean
new file mode 100644
index 000000000..ee1d70728
--- /dev/null
+++ b/CslibTests/Circuits.lean
@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Cslib.Computability.Circuit.Basic
+
+/-! # Circuit tests
+
+These tests exercise zero-gate wiring, shared internal gates, multiple outputs,
+and the size and depth conventions of the generic circuit model.
+-/
+
+namespace CslibTests.Circuits
+
+open Cslib.Circuits
+
+inductive NandOp where
+  | nand
+
+abbrev nandSignature : Signature where
+  Op := NandOp
+  Arity := fun _ => 2
+
+def nandInterpretation : Interpretation nandSignature Bool
+  | .nand, input => !(input 0 && input 1)
+
+def nandInputs : Line nandSignature 2 0 where
+  op := .nand
+  wires := Fin.cases (Wire.input 0) fun _ => Wire.input 1
+
+def nandResultTwice : Line nandSignature 2 1 where
+  op := .nand
+  wires := fun _ => Wire.gate 0
+
+def andProgram : Program nandSignature 2 2 :=
+  .gate (.gate .empty nandInputs) nandResultTwice
+
+/-- The first output is AND and the second is NAND. Both reuse the first gate. -/
+def andNandCircuit : Circuit nandSignature 2 2 2 where
+  program := andProgram
+  outputs := Fin.cases (Wire.gate 1) fun _ => Wire.gate 0
+
+def allTrue : Fin 2 → Bool := fun _ => true
+
+def trueFalse : Fin 2 → Bool := Fin.cases true fun _ => false
+
+example : andNandCircuit.eval nandInterpretation allTrue 0 = true := rfl
+
+example : andNandCircuit.eval nandInterpretation allTrue 1 = false := rfl
+
+example : andNandCircuit.eval nandInterpretation trueFalse 0 = false := rfl
+
+example : andNandCircuit.eval nandInterpretation trueFalse 1 = true := rfl
+
+example : andNandCircuit.size = 2 := rfl
+
+example : andNandCircuit.depth = 2 := rfl
+
+example : andNandCircuit.FanInAtMost 2 := by decide
+
+example : ¬ andNandCircuit.FanInAtMost 1 := by decide
+
+example : andNandCircuit.computation nandInterpretation allTrue 0 = false := rfl
+
+example : andNandCircuit.computation nandInterpretation allTrue 1 = true := rfl
+
+example : andNandCircuit.computation nandInterpretation allTrue 2 = true := rfl
+
+example : andNandCircuit.computation nandInterpretation allTrue 3 = false := rfl
+
+example : andNandCircuit.trace nandInterpretation allTrue 1 = true := rfl
+
+example : andNandCircuit.trace nandInterpretation allTrue 2 = false := rfl
+
+example : andNandCircuit.trace nandInterpretation allTrue 3 = true := rfl
+
+example : andNandCircuit.trace nandInterpretation allTrue 4 = true := rfl
+
+/-- A zero-gate circuit can permute inputs without introducing artificial gates. -/
+def swap : Circuit nandSignature 2 0 2 where
+  program := .empty
+  outputs := Fin.cases (Wire.input 1) fun _ => Wire.input 0
+
+example : swap.eval nandInterpretation trueFalse 0 = false := rfl
+
+example : swap.eval nandInterpretation trueFalse 1 = true := rfl
+
+example : swap.size = 0 := rfl
+
+example : swap.depth = 0 := rfl
+
+/-- Duplicating an output wire is also free. -/
+def duplicateFirst : Circuit nandSignature 2 0 2 where
+  program := .empty
+  outputs := fun _ => Wire.input 0
+
+example : duplicateFirst.eval nandInterpretation trueFalse 0 = true := rfl
+
+example : duplicateFirst.eval nandInterpretation trueFalse 1 = true := rfl
+
+example : duplicateFirst.size = 0 := rfl
+
+def noOutputs : Circuit nandSignature 2 2 0 where
+  program := andProgram
+  outputs := Fin.elim0
+
+example : noOutputs.depth = 0 := rfl
+
+inductive ConstantOp where
+  | truth
+
+def constantSignature : Signature where
+  Op := ConstantOp
+  Arity := fun _ => 0
+
+def constantInterpretation : Interpretation constantSignature Bool
+  | .truth, _ => true
+
+def truthLine : Line constantSignature 0 0 where
+  op := .truth
+  wires := Fin.elim0
+
+def truthProgram : Program constantSignature 0 1 :=
+  .gate .empty truthLine
+
+def truthCircuit : Circuit constantSignature 0 1 1 where
+  program := truthProgram
+  outputs := fun _ => Wire.gate 0
+
+example : truthCircuit.eval constantInterpretation Fin.elim0 0 = true := rfl
+
+example : truthCircuit.FanInAtMost 0 := by decide
+
+example : truthCircuit.depth = 1 := rfl
+
+end CslibTests.Circuits