From 9da000623026d57227a5dba24c649a0a7a07a361 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Thu, 27 Aug 2026 13:21:04 -0400 Subject: [PATCH 1/3] feat(Computability): add generic circuit model --- Cslib.lean | 5 + Cslib/Computability/Circuits/Circuit.lean | 103 ++++ .../Computability/Circuits/Homomorphism.lean | 110 ++++ .../Circuits/Interpretation.lean | 28 + Cslib/Computability/Circuits/Program.lean | 553 ++++++++++++++++++ Cslib/Computability/Circuits/Signature.lean | 30 + Cslib/Computability/README.md | 4 + CslibTests.lean | 1 + CslibTests/Circuits.lean | 138 +++++ 9 files changed, 972 insertions(+) create mode 100644 Cslib/Computability/Circuits/Circuit.lean create mode 100644 Cslib/Computability/Circuits/Homomorphism.lean create mode 100644 Cslib/Computability/Circuits/Interpretation.lean create mode 100644 Cslib/Computability/Circuits/Program.lean create mode 100644 Cslib/Computability/Circuits/Signature.lean create mode 100644 CslibTests/Circuits.lean diff --git a/Cslib.lean b/Cslib.lean index 9849e3df9b..ce10e938e3 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.Circuits.Circuit +public import Cslib.Computability.Circuits.Homomorphism +public import Cslib.Computability.Circuits.Interpretation +public import Cslib.Computability.Circuits.Program +public import Cslib.Computability.Circuits.Signature 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/Circuits/Circuit.lean b/Cslib/Computability/Circuits/Circuit.lean new file mode 100644 index 0000000000..5bf9496abd --- /dev/null +++ b/Cslib/Computability/Circuits/Circuit.lean @@ -0,0 +1,103 @@ +/- +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.Circuits.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. + +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`). +-/ + +@[expose] public section + +namespace Cslib.Circuits + +/-- A straight-line program with designated output wires. -/ +structure Circuit (σ : Signature) (n g m : Nat) where + /-- The internal gates of the circuit. -/ + program : Program σ n g + /-- The input or internal-gate wire carrying each output. -/ + outputs : Fin m → Wire n g + +/-- The zero-gate identity circuit, whose outputs are its inputs. -/ +def Circuit.id (σ : Signature) (n : Nat) : Circuit σ n 0 n where + program := .empty + outputs := fun input => Wire.input input + +/-- Every gate in a circuit has at most `r` arguments. -/ +def Circuit.FanInAtMost (c : Circuit σ n g m) (r : Nat) : Prop := + c.program.FanInAtMost r + +/-- Bounded fan-in is decidable for every concrete circuit. -/ +instance Circuit.instDecidableFanInAtMost + (c : Circuit σ n g m) + (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 σ n g m) : Nat := + g + +/-- The depth of every designated output wire in a circuit. -/ +def Circuit.outputDepths (c : Circuit σ n g m) : Fin m → Nat := + c.program.wireDepths ∘ c.outputs + +/-- The maximum depth of a designated output wire in a circuit. -/ +def Circuit.depth (c : Circuit σ n g m) : Nat := + Fin.foldl m (fun depth k => max depth (c.outputDepths k)) 0 + +/-- Read the designated output wires after evaluating the program. -/ +def Circuit.eval + (c : Circuit σ n g m) + (i : Interpretation σ U) + (x : Fin n → U) : Fin m → U := + c.program.trace i x ∘ c.outputs + +@[simp] theorem Circuit.eval_id + (interpretation : Interpretation σ U) + (input : Fin n → U) : + (Circuit.id σ n).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 σ n g m) + (h : Homomorphism i₁ i₂) + (x : Fin n → 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 σ n g m) + (i : Interpretation σ U) + (x : Fin n → U) : Fin (g + m) → 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 σ n g m) + (i : Interpretation σ U) + (x : Fin n → U) : Fin (n + g + m) → U := + Fin.addCases (c.program.trace i x) (c.eval i x) + +end Cslib.Circuits diff --git a/Cslib/Computability/Circuits/Homomorphism.lean b/Cslib/Computability/Circuits/Homomorphism.lean new file mode 100644 index 0000000000..cde8d099a5 --- /dev/null +++ b/Cslib/Computability/Circuits/Homomorphism.lean @@ -0,0 +1,110 @@ +/- +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.Circuits.Interpretation + +/-! +# Homomorphisms of interpretations + +A homomorphism between two interpretations of the same signature is a map of +carriers that commutes with every operation. Homomorphisms have identities and +compose, and these satisfy the usual category laws up to `Homomorphism.ext`. + +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 + +/-- 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/Circuits/Interpretation.lean b/Cslib/Computability/Circuits/Interpretation.lean new file mode 100644 index 0000000000..4959167094 --- /dev/null +++ b/Cslib/Computability/Circuits/Interpretation.lean @@ -0,0 +1,28 @@ +/- +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.Circuits.Signature + +/-! +# Interpretations + +An interpretation of a signature over a carrier type `Carrier` assigns to +every operation symbol a function from argument tuples, indexed by `Fin` of +the symbol's arity, to `Carrier`. Interpretations are plain functions rather +than a structure, so they can be built pointwise and specialized without any +wrapping. +-/ + +@[expose] public section + +namespace Cslib.Circuits + +/-- An interpretation assigns an operation on `Carrier` to every symbol in `σ`. -/ +abbrev Interpretation (σ : Signature) Carrier := + (op : σ.Op) → (Fin (σ.Arity op) → Carrier) → Carrier + +end Cslib.Circuits diff --git a/Cslib/Computability/Circuits/Program.lean b/Cslib/Computability/Circuits/Program.lean new file mode 100644 index 0000000000..28cc6282b0 --- /dev/null +++ b/Cslib/Computability/Circuits/Program.lean @@ -0,0 +1,553 @@ +/- +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.Circuits.Homomorphism +public import Mathlib.Data.Fin.SuccPred +public import Mathlib.Logic.Equiv.Defs + +/-! +# Straight-line programs + +A program is a topologically ordered sequence of gates. Each gate is a `Line`: +an operation symbol together with the wires supplying its arguments, where a +`Wire` is either one of the `n` original inputs or the output of an earlier +gate. Programs are indexed by their gate count, so `Program σ n g` has exactly +`g` gates and every gate reads only from wires that precede it. + +This file defines + +* wires, the input-fixing wire renamings `Wire.Renaming`, and the standard + ways to build them (identity, composition, `castSucc`, `skipLast`, + `appendLast`, and permutations); +* 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 + +/-- A wire is either an original input or the output of an earlier gate. -/ +abbrev Wire n g := Fin (n + g) + +/-- Regard an original input as a wire. -/ +abbrev Wire.input {n g : Nat} (input : Fin n) : Wire n g := + Fin.castAdd g input + +/-- Regard a gate output as a wire. -/ +abbrev Wire.gate {n g : Nat} (gate : Fin g) : Wire n g := + Fin.natAdd n 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 (n g h : Nat) where + /-- The target wire representing each source gate. -/ + gates : Fin g → Wire n h + +namespace Wire.Renaming + +/-- Apply an input-fixing wire renaming. -/ +def apply (ρ : Wire.Renaming n g h) : Wire n g → Wire n h := + Fin.addCases Wire.input ρ.gates + +instance : CoeFun (Wire.Renaming n g h) fun _ => Wire n g → Wire n h := + ⟨apply⟩ + +@[simp] theorem apply_input + (ρ : Wire.Renaming n g h) (input : Fin n) : + ρ (Wire.input input) = Wire.input input := by + simp [apply] + +@[simp] theorem apply_gate + (ρ : Wire.Renaming n g h) (gate : Fin g) : + ρ (Wire.gate gate) = ρ.gates gate := by + simp [apply] + +/-- The identity wire renaming. -/ +def id : Wire.Renaming n g g where + gates := Wire.gate + +@[simp] theorem id_apply (wire : Wire n g) : + (id : Wire.Renaming n g g) wire = wire := by + refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire <;> simp [id] + +/-- Compose input-fixing wire renamings. -/ +def comp + (outer : Wire.Renaming n h k) + (inner : Wire.Renaming n g h) : Wire.Renaming n g k where + gates := outer ∘ inner.gates + +@[simp] theorem comp_apply + (outer : Wire.Renaming n h k) + (inner : Wire.Renaming n g h) + (wire : Wire n g) : + (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 n g (g + 1) where + gates := fun gate => Wire.gate gate.castSucc + +@[simp] theorem castSucc_apply (wire : Wire n g) : + (castSucc : Wire.Renaming n g (g + 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 n g k) + (replacement : Wire n k) : Wire.Renaming n (g + 1) k where + gates := Fin.lastCases replacement prior.gates + +theorem skipLast_gate_last + (prior : Wire.Renaming n g k) + (replacement : Wire n k) : + prior.skipLast replacement (Wire.gate (Fin.last g)) = replacement := by + rw [apply_gate] + simp [skipLast] + +@[simp] theorem skipLast_lastWire + (prior : Wire.Renaming n g k) + (replacement : Wire n k) : + prior.skipLast replacement (Fin.last (n + g)) = replacement := by + rw [← Fin.natAdd_last (n := n) (m := g)] + exact skipLast_gate_last prior replacement + +@[simp] theorem skipLast_castSucc + (prior : Wire.Renaming n g k) + (replacement : Wire n k) + (wire : Wire n g) : + 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 n g k) : Wire.Renaming n (g + 1) (k + 1) where + gates := Fin.lastCases (Wire.gate (n := n) (Fin.last k)) fun gate => + (prior.gates gate).castSucc + +theorem appendLast_gate_last + (prior : Wire.Renaming n g k) : + prior.appendLast (Wire.gate (Fin.last g)) = + Wire.gate (n := n) (Fin.last k) := by + rw [apply_gate] + simp [appendLast] + +@[simp] theorem appendLast_lastWire + (prior : Wire.Renaming n g k) : + prior.appendLast (Fin.last (n + g)) = Wire.gate (n := n) (Fin.last k) := by + rw [← Fin.natAdd_last (n := n) (m := g)] + exact appendLast_gate_last prior + +@[simp] theorem appendLast_castSucc + (prior : Wire.Renaming n g k) + (wire : Wire n g) : + 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 g)) : Wire.Renaming n g g where + gates := fun gate => Wire.gate (permutation gate) + +theorem ofPermutation_gate + (permutation : Equiv.Perm (Fin g)) (gate : Fin g) : + (ofPermutation permutation : Wire.Renaming n g g) (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 n g h) + (inputs : Fin n → U) + (oldGates : Fin g → U) + (newGates : Fin h → U) + (preservesGates : ∀ gate, + (Fin.addCases inputs newGates : Wire n h → U) (ρ.gates gate) = + oldGates gate) + (wire : Wire n g) : + (Fin.addCases inputs newGates : Wire n h → U) (ρ wire) = + (Fin.addCases inputs oldGates : Wire n g → U) wire := by + refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire + · simp + · simpa using preservesGates gate + +end Wire.Renaming + +/-- One gate together with the wires supplying its arguments. -/ +structure Line (σ : Signature) (n g : Nat) where + /-- The operation performed by the gate. -/ + op : σ.Op + /-- The wire supplying each argument of the operation. -/ + wires : Fin (σ.Arity op) → Wire n g + +/-- Apply a function to every wire read by a line. -/ +def Line.mapWires + (line : Line σ n g) + (wireMap : Wire n g → Wire n' h) : Line σ n' h where + op := line.op + wires := wireMap ∘ line.wires + +@[simp] theorem Line.mapWires_op + (line : Line σ n g) + (wireMap : Wire n g → Wire n' h) : + (line.mapWires wireMap).op = line.op := rfl + +@[simp] theorem Line.mapWires_wires + (line : Line σ n g) + (wireMap : Wire n g → Wire n' h) + (argument : Fin (σ.Arity line.op)) : + (line.mapWires wireMap).wires argument = wireMap (line.wires argument) := rfl + +/-- A topologically ordered straight-line program of `g` gates. -/ +inductive Program (σ : Signature) (n : Nat) : Nat → Type v where + | empty : Program σ n 0 + | gate : Program σ n g → Line σ n g → Program σ n (g + 1) + +/-- Every gate in a program has at most `r` arguments. -/ +def Program.FanInAtMost : (program : Program σ n g) → 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 + (program : Program σ n g) + (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 σ n g) + (i : Interpretation σ U) + (inputs : Fin n → U) + (gates : Fin g → 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 σ n g) + (wireMap : Wire n g → Wire n' h) + (interpretation : Interpretation σ U) + (oldInputs : Fin n → U) + (newInputs : Fin n' → U) + (oldGates : Fin g → U) + (newGates : Fin h → U) + (preserves : ∀ wire : Wire n g, + (Fin.addCases newInputs newGates : Wire n' h → U) (wireMap wire) = + (Fin.addCases oldInputs oldGates : Wire n g → 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 σ n g) + (ρ : Wire.Renaming n g h) + (interpretation : Interpretation σ U) + (inputs : Fin n → U) + (oldGates : Fin g → U) + (newGates : Fin h → U) + (preservesGates : ∀ gate, + (Fin.addCases inputs newGates : Wire n h → 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 σ n g) + (wireDepths : Wire n g → 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 σ n g) + (h : Homomorphism i₁ i₂) + (inputs : Fin n → U₁) + (gates : Fin g → 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 + (p : Program σ n g) + (i : Interpretation σ U) + (x : Fin n → U) : Fin g → 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 σ n g) + (line : Line σ n g) + (interpretation : Interpretation σ U) + (input : Fin n → U) : + (program.gate line).eval interpretation input (Fin.last g) = + line.eval interpretation input (program.eval interpretation input) := by + simp [Program.eval] + +@[simp] theorem Program.eval_gate_castSucc + (program : Program σ n g) + (line : Line σ n g) + (interpretation : Interpretation σ U) + (input : Fin n → U) + (gate : Fin g) : + (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 (p : Program σ n g) : Fin g → 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 σ n g) : Wire n g → Nat := + Fin.addCases (fun _ => 0) p.depths + +/-- The maximum depth of any gate in a program. -/ +def Program.depth (p : Program σ n g) : Nat := + Fin.foldl g (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 σ n g) + (h : Homomorphism i₁ i₂) + (x : Fin n → 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 σ n g) + (i : Interpretation σ U) + (x : Fin n → U) : Fin (n + g) → U := + Fin.addCases x (p.eval i x) + +@[simp] theorem Program.trace_input + (program : Program σ n g) + (interpretation : Interpretation σ U) + (input : Fin n → U) + (sourceInput : Fin n) : + program.trace interpretation input (Wire.input sourceInput) = + input sourceInput := by + simp [Program.trace] + +@[simp] theorem Program.trace_gate_castSucc + (program : Program σ n g) + (line : Line σ n g) + (interpretation : Interpretation σ U) + (input : Fin n → U) + (wire : Wire n g) : + (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 σ n g) + (line : Line σ n g) + (interpretation : Interpretation σ U) + (input : Fin n → U) : + (program.gate line).trace interpretation input (Fin.last (n + g)) = + line.eval interpretation input (program.eval interpretation input) := by + rw [← Fin.natAdd_last (n := n) (m := g)] + 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 σ n g) + (h : Homomorphism i₁ i₂) + (x : Fin n → 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 σ n g) + (interpretation : Interpretation σ U) + (gate : Fin g) : (Fin n → U) → U := + fun input => program.eval interpretation input gate + +/-- The scalar function carried by an input or internal-gate wire. -/ +def Program.wireFunction + (program : Program σ n g) + (interpretation : Interpretation σ U) + (wire : Wire n g) : (Fin n → U) → U := + fun input => program.trace interpretation input wire + +@[simp] theorem Program.gateFunction_apply + (program : Program σ n g) + (interpretation : Interpretation σ U) + (gate : Fin g) + (input : Fin n → U) : + program.gateFunction interpretation gate input = + program.eval interpretation input gate := rfl + +@[simp] theorem Program.wireFunction_input + (program : Program σ n g) + (interpretation : Interpretation σ U) + (inputWire : Fin n) : + 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 σ n g) + (interpretation : Interpretation σ U) + (gate : Fin g) : + 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 σ n g) + (line : Line σ n g) + (interpretation : Interpretation σ U) : + (program.gate line).gateFunction interpretation (Fin.last g) = + 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 σ n g) + (line : Line σ n g) + (interpretation : Interpretation σ U) + (gate : Fin g) : + (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 σ n g) + (interpretation : Interpretation σ U) + (input : Fin n → U) + (gate : Fin g) : + 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 : (program : Program σ n g) → Fin g → Line σ n g + | .empty => Fin.elim0 + | @Program.gate _ _ g 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 σ n g) + (line : Line σ n g) : + (program.gate line).lines (Fin.last g) = + line.mapWires Wire.Renaming.castSucc := by + simp [Program.lines] + +@[simp] theorem Program.lines_gate_castSucc + (program : Program σ n g) + (line : Line σ n g) + (gate : Fin g) : + (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 σ n g) + (interpretation : Interpretation σ U) + (input : Fin n → U) + (gate : Fin g) : + (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 g program line ih => + have evalWidened (oldLine : Line σ n g) : + (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/Circuits/Signature.lean b/Cslib/Computability/Circuits/Signature.lean new file mode 100644 index 0000000000..05c4b2fc1f --- /dev/null +++ b/Cslib/Computability/Circuits/Signature.lean @@ -0,0 +1,30 @@ +/- +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 + +A signature is a collection of finitary operation symbols, each with a fixed +arity. Signatures carry no semantics: an `Interpretation` assigns concrete +operations to the symbols, and programs and circuits over a signature are +purely syntactic until they are evaluated in an interpretation. +-/ + +@[expose] public section + +namespace Cslib.Circuits + +/-- A collection of finitary operation symbols and their arities. -/ +structure Signature where + /-- The operation symbols of the signature. -/ + Op : Type v + /-- The number of arguments taken by each operation symbol. -/ + Arity : (op : Op) → Nat + +end Cslib.Circuits diff --git a/Cslib/Computability/README.md b/Cslib/Computability/README.md index f2ab58842f..8b602532de 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 a84190e525..f7b53299f6 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 0000000000..b5ce53ed10 --- /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.Circuits.Circuit + +/-! # 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 From 88163f6dda85c3fe93ae8b261964241f4880a8e5 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 5 Sep 2026 11:01:00 -0400 Subject: [PATCH 2/3] refactor(Circuits): simplify modules and clarify parameters --- Cslib.lean | 2 +- Cslib/Computability/Circuits/Circuit.lean | 75 ++-- .../Computability/Circuits/Homomorphism.lean | 11 +- .../Circuits/Interpretation.lean | 28 -- Cslib/Computability/Circuits/Program.lean | 419 ++++++------------ Cslib/Computability/Circuits/Signature.lean | 20 +- Cslib/Computability/Circuits/Wire.lean | 189 ++++++++ 7 files changed, 394 insertions(+), 350 deletions(-) delete mode 100644 Cslib/Computability/Circuits/Interpretation.lean create mode 100644 Cslib/Computability/Circuits/Wire.lean diff --git a/Cslib.lean b/Cslib.lean index ce10e938e3..bdb344c918 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -31,9 +31,9 @@ public import Cslib.Computability.Automata.Transducers.Transducer public import Cslib.Computability.Automata.TwoWayNA.Basic public import Cslib.Computability.Circuits.Circuit public import Cslib.Computability.Circuits.Homomorphism -public import Cslib.Computability.Circuits.Interpretation public import Cslib.Computability.Circuits.Program public import Cslib.Computability.Circuits.Signature +public import Cslib.Computability.Circuits.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/Circuits/Circuit.lean b/Cslib/Computability/Circuits/Circuit.lean index 5bf9496abd..e09a797d99 100644 --- a/Cslib/Computability/Circuits/Circuit.lean +++ b/Cslib/Computability/Circuits/Circuit.lean @@ -16,88 +16,107 @@ 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) (n g m : Nat) where +structure Circuit (σ : Signature) (inputCount gateCount outputCount : Nat) where /-- The internal gates of the circuit. -/ - program : Program σ n g + program : Program σ inputCount gateCount /-- The input or internal-gate wire carrying each output. -/ - outputs : Fin m → Wire n g + outputs : Fin outputCount → Wire inputCount gateCount /-- The zero-gate identity circuit, whose outputs are its inputs. -/ -def Circuit.id (σ : Signature) (n : Nat) : Circuit σ n 0 n where +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 σ n g m) (r : Nat) : Prop := +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 σ n g m) + (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 σ n g m) : Nat := - g +def Circuit.size (_ : Circuit σ inputCount gateCount outputCount) : Nat := + gateCount /-- The depth of every designated output wire in a circuit. -/ -def Circuit.outputDepths (c : Circuit σ n g m) : Fin m → Nat := +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 σ n g m) : Nat := - Fin.foldl m (fun depth k => max depth (c.outputDepths k)) 0 +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 σ n g m) - (i : Interpretation σ U) - (x : Fin n → U) : Fin m → U := + (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 n → U) : - (Circuit.id σ n).eval interpretation input = input := by + (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 σ n g m) - (h : Homomorphism i₁ i₂) - (x : Fin n → U₁) : - h.map ∘ c.eval i₁ x = c.eval i₂ (h.map ∘ x) := by + {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 σ n g m) - (i : Interpretation σ U) - (x : Fin n → U) : Fin (g + m) → U := + (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 σ n g m) - (i : Interpretation σ U) - (x : Fin n → U) : Fin (n + g + m) → U := + (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/Circuits/Homomorphism.lean b/Cslib/Computability/Circuits/Homomorphism.lean index cde8d099a5..13e33b6bf2 100644 --- a/Cslib/Computability/Circuits/Homomorphism.lean +++ b/Cslib/Computability/Circuits/Homomorphism.lean @@ -5,14 +5,14 @@ Authors: Samuel Schlesinger -/ module -public import Cslib.Computability.Circuits.Interpretation +public import Cslib.Computability.Circuits.Signature /-! # Homomorphisms of interpretations A homomorphism between two interpretations of the same signature is a map of -carriers that commutes with every operation. Homomorphisms have identities and -compose, and these satisfy the usual category laws up to `Homomorphism.ext`. +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`, @@ -23,6 +23,11 @@ programs, and circuits commutes with them (`Line.map_eval`, `Program.map_eval`, 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. -/ diff --git a/Cslib/Computability/Circuits/Interpretation.lean b/Cslib/Computability/Circuits/Interpretation.lean deleted file mode 100644 index 4959167094..0000000000 --- a/Cslib/Computability/Circuits/Interpretation.lean +++ /dev/null @@ -1,28 +0,0 @@ -/- -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.Circuits.Signature - -/-! -# Interpretations - -An interpretation of a signature over a carrier type `Carrier` assigns to -every operation symbol a function from argument tuples, indexed by `Fin` of -the symbol's arity, to `Carrier`. Interpretations are plain functions rather -than a structure, so they can be built pointwise and specialized without any -wrapping. --/ - -@[expose] public section - -namespace Cslib.Circuits - -/-- An interpretation assigns an operation on `Carrier` to every symbol in `σ`. -/ -abbrev Interpretation (σ : Signature) Carrier := - (op : σ.Op) → (Fin (σ.Arity op) → Carrier) → Carrier - -end Cslib.Circuits diff --git a/Cslib/Computability/Circuits/Program.lean b/Cslib/Computability/Circuits/Program.lean index 28cc6282b0..4bb051d108 100644 --- a/Cslib/Computability/Circuits/Program.lean +++ b/Cslib/Computability/Circuits/Program.lean @@ -6,23 +6,17 @@ Authors: Samuel Schlesinger module public import Cslib.Computability.Circuits.Homomorphism -public import Mathlib.Data.Fin.SuccPred -public import Mathlib.Logic.Equiv.Defs +public import Cslib.Computability.Circuits.Wire /-! # Straight-line programs -A program is a topologically ordered sequence of gates. Each gate is a `Line`: -an operation symbol together with the wires supplying its arguments, where a -`Wire` is either one of the `n` original inputs or the output of an earlier -gate. Programs are indexed by their gate count, so `Program σ n g` has exactly -`g` gates and every gate reads only from wires that precede it. +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 -* wires, the input-fixing wire renamings `Wire.Renaming`, and the standard - ways to build them (identity, composition, `castSucc`, `skipLast`, - `appendLast`, and permutations); * 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 @@ -39,198 +33,54 @@ Evaluation of lines and programs commutes with homomorphisms namespace Cslib.Circuits -/-- A wire is either an original input or the output of an earlier gate. -/ -abbrev Wire n g := Fin (n + g) - -/-- Regard an original input as a wire. -/ -abbrev Wire.input {n g : Nat} (input : Fin n) : Wire n g := - Fin.castAdd g input - -/-- Regard a gate output as a wire. -/ -abbrev Wire.gate {n g : Nat} (gate : Fin g) : Wire n g := - Fin.natAdd n 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 (n g h : Nat) where - /-- The target wire representing each source gate. -/ - gates : Fin g → Wire n h - -namespace Wire.Renaming - -/-- Apply an input-fixing wire renaming. -/ -def apply (ρ : Wire.Renaming n g h) : Wire n g → Wire n h := - Fin.addCases Wire.input ρ.gates - -instance : CoeFun (Wire.Renaming n g h) fun _ => Wire n g → Wire n h := - ⟨apply⟩ - -@[simp] theorem apply_input - (ρ : Wire.Renaming n g h) (input : Fin n) : - ρ (Wire.input input) = Wire.input input := by - simp [apply] - -@[simp] theorem apply_gate - (ρ : Wire.Renaming n g h) (gate : Fin g) : - ρ (Wire.gate gate) = ρ.gates gate := by - simp [apply] - -/-- The identity wire renaming. -/ -def id : Wire.Renaming n g g where - gates := Wire.gate - -@[simp] theorem id_apply (wire : Wire n g) : - (id : Wire.Renaming n g g) wire = wire := by - refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire <;> simp [id] - -/-- Compose input-fixing wire renamings. -/ -def comp - (outer : Wire.Renaming n h k) - (inner : Wire.Renaming n g h) : Wire.Renaming n g k where - gates := outer ∘ inner.gates - -@[simp] theorem comp_apply - (outer : Wire.Renaming n h k) - (inner : Wire.Renaming n g h) - (wire : Wire n g) : - (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 n g (g + 1) where - gates := fun gate => Wire.gate gate.castSucc - -@[simp] theorem castSucc_apply (wire : Wire n g) : - (castSucc : Wire.Renaming n g (g + 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 n g k) - (replacement : Wire n k) : Wire.Renaming n (g + 1) k where - gates := Fin.lastCases replacement prior.gates - -theorem skipLast_gate_last - (prior : Wire.Renaming n g k) - (replacement : Wire n k) : - prior.skipLast replacement (Wire.gate (Fin.last g)) = replacement := by - rw [apply_gate] - simp [skipLast] - -@[simp] theorem skipLast_lastWire - (prior : Wire.Renaming n g k) - (replacement : Wire n k) : - prior.skipLast replacement (Fin.last (n + g)) = replacement := by - rw [← Fin.natAdd_last (n := n) (m := g)] - exact skipLast_gate_last prior replacement - -@[simp] theorem skipLast_castSucc - (prior : Wire.Renaming n g k) - (replacement : Wire n k) - (wire : Wire n g) : - 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 n g k) : Wire.Renaming n (g + 1) (k + 1) where - gates := Fin.lastCases (Wire.gate (n := n) (Fin.last k)) fun gate => - (prior.gates gate).castSucc - -theorem appendLast_gate_last - (prior : Wire.Renaming n g k) : - prior.appendLast (Wire.gate (Fin.last g)) = - Wire.gate (n := n) (Fin.last k) := by - rw [apply_gate] - simp [appendLast] - -@[simp] theorem appendLast_lastWire - (prior : Wire.Renaming n g k) : - prior.appendLast (Fin.last (n + g)) = Wire.gate (n := n) (Fin.last k) := by - rw [← Fin.natAdd_last (n := n) (m := g)] - exact appendLast_gate_last prior - -@[simp] theorem appendLast_castSucc - (prior : Wire.Renaming n g k) - (wire : Wire n g) : - 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 g)) : Wire.Renaming n g g where - gates := fun gate => Wire.gate (permutation gate) - -theorem ofPermutation_gate - (permutation : Equiv.Perm (Fin g)) (gate : Fin g) : - (ofPermutation permutation : Wire.Renaming n g g) (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 n g h) - (inputs : Fin n → U) - (oldGates : Fin g → U) - (newGates : Fin h → U) - (preservesGates : ∀ gate, - (Fin.addCases inputs newGates : Wire n h → U) (ρ.gates gate) = - oldGates gate) - (wire : Wire n g) : - (Fin.addCases inputs newGates : Wire n h → U) (ρ wire) = - (Fin.addCases inputs oldGates : Wire n g → U) wire := by - refine Fin.addCases (fun input => ?_) (fun gate => ?_) wire - · simp - · simpa using preservesGates gate +universe v u u₁ u₂ -end Wire.Renaming +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) (n g : Nat) where +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 n g + wires : Fin (σ.Arity op) → Wire inputCount gateCount /-- Apply a function to every wire read by a line. -/ def Line.mapWires - (line : Line σ n g) - (wireMap : Wire n g → Wire n' h) : Line σ n' h where + (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 σ n g) - (wireMap : Wire n g → Wire n' h) : + (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 σ n g) - (wireMap : Wire n g → Wire n' h) + (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 of `g` gates. -/ -inductive Program (σ : Signature) (n : Nat) : Nat → Type v where - | empty : Program σ n 0 - | gate : Program σ n g → Line σ n g → Program σ n (g + 1) +/-- 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 : (program : Program σ n g) → Nat → Prop +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 - (program : Program σ n g) +instance Program.instDecidableFanInAtMost {gateCount : Nat} + (program : Program σ inputCount gateCount) (r : Nat) : Decidable (program.FanInAtMost r) := match program with | .empty => isTrue trivial @@ -241,26 +91,26 @@ instance Program.instDecidableFanInAtMost /-- Evaluate a line from the values of the inputs and preceding gates. -/ def Line.eval - (line : Line σ n g) - (i : Interpretation σ U) - (inputs : Fin n → U) - (gates : Fin g → U) : U := + (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 σ n g) - (wireMap : Wire n g → Wire n' h) + (line : Line σ sourceInputCount sourceGateCount) + (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount) (interpretation : Interpretation σ U) - (oldInputs : Fin n → U) - (newInputs : Fin n' → U) - (oldGates : Fin g → U) - (newGates : Fin h → U) - (preserves : ∀ wire : Wire n g, - (Fin.addCases newInputs newGates : Wire n' h → U) (wireMap wire) = - (Fin.addCases oldInputs oldGates : Wire n g → U) wire) : + (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 @@ -271,14 +121,14 @@ theorem Line.eval_mapWires /-- Specialization of `Line.eval_mapWires` to an input-fixing wire renaming. -/ theorem Line.eval_mapRenaming - (line : Line σ n g) - (ρ : Wire.Renaming n g h) + (line : Line σ inputCount sourceGateCount) + (ρ : Wire.Renaming inputCount sourceGateCount targetGateCount) (interpretation : Interpretation σ U) - (inputs : Fin n → U) - (oldGates : Fin g → U) - (newGates : Fin h → U) + (inputs : Fin inputCount → U) + (oldGates : Fin sourceGateCount → U) + (newGates : Fin targetGateCount → U) (preservesGates : ∀ gate, - (Fin.addCases inputs newGates : Wire n h → U) (ρ.gates 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 @@ -287,21 +137,21 @@ theorem Line.eval_mapRenaming /-- The depth of a line, given the depth of every wire it may read. -/ def Line.depth - (line : Line σ n g) - (wireDepths : Wire n g → Nat) : Nat := + (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 σ n g) - (h : Homomorphism i₁ i₂) - (inputs : Fin n → U₁) - (gates : Fin g → U₁) : - h.map (line.eval i₁ inputs gates) = - line.eval i₂ (h.map ∘ inputs) (h.map ∘ gates) := by + {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 @@ -309,10 +159,10 @@ theorem Line.map_eval exact Fin.addCases (fun _ => by simp) (fun _ => by simp) (line.wires k) /-- Evaluate every gate in a program, in program order. -/ -def Program.eval - (p : Program σ n g) - (i : Interpretation σ U) - (x : Fin n → U) : Fin g → U := +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 => @@ -320,26 +170,26 @@ def Program.eval Fin.lastCases (line.eval i x prior) prior @[simp] theorem Program.eval_gate_last - (program : Program σ n g) - (line : Line σ n g) + (program : Program σ inputCount gateCount) + (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) - (input : Fin n → U) : - (program.gate line).eval interpretation input (Fin.last g) = + (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 σ n g) - (line : Line σ n g) + (program : Program σ inputCount gateCount) + (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) - (input : Fin n → U) - (gate : Fin g) : + (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 (p : Program σ n g) : Fin g → Nat := +def Program.depths {gateCount : Nat} (p : Program σ inputCount gateCount) : Fin gateCount → Nat := match p with | .empty => Fin.elim0 | .gate p line => @@ -348,21 +198,21 @@ def Program.depths (p : Program σ n g) : Fin g → Nat := Fin.lastCases (line.depth wireDepths) prior /-- The depth of every input or gate wire in a program. -/ -def Program.wireDepths (p : Program σ n g) : Wire n g → Nat := +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 σ n g) : Nat := - Fin.foldl g (fun depth k => max depth (p.depths k)) 0 +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 σ n g) - (h : Homomorphism i₁ i₂) - (x : Fin n → U₁) : - h.map ∘ p.eval i₁ x = p.eval i₂ (h.map ∘ x) := by + {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 @@ -378,26 +228,26 @@ theorem Program.map_eval /-- The input values followed by all gate values, in program order. -/ def Program.trace - (p : Program σ n g) - (i : Interpretation σ U) - (x : Fin n → U) : Fin (n + g) → U := + (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 σ n g) + (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) - (input : Fin n → U) - (sourceInput : Fin n) : + (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 σ n g) - (line : Line σ n g) + (program : Program σ inputCount gateCount) + (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) - (input : Fin n → U) - (wire : Wire n g) : + (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 @@ -406,25 +256,25 @@ def Program.trace · simp @[simp] theorem Program.trace_gate_last - (program : Program σ n g) - (line : Line σ n g) + (program : Program σ inputCount gateCount) + (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) - (input : Fin n → U) : - (program.gate line).trace interpretation input (Fin.last (n + g)) = + (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 := n) (m := g)] + 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 σ n g) - (h : Homomorphism i₁ i₂) - (x : Fin n → U₁) : - h.map ∘ p.trace i₁ x = p.trace i₂ (h.map ∘ x) := by + {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] @@ -432,110 +282,113 @@ theorem Program.map_trace /-- The scalar function computed by an internal gate. -/ def Program.gateFunction - (program : Program σ n g) + (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) - (gate : Fin g) : (Fin n → U) → U := - fun input => program.eval interpretation input gate + (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 σ n g) + (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) - (wire : Wire n g) : (Fin n → U) → U := - fun input => program.trace interpretation input wire + (wire : Wire inputCount gateCount) + (input : Fin inputCount → U) : U := + program.trace interpretation input wire @[simp] theorem Program.gateFunction_apply - (program : Program σ n g) + (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) - (gate : Fin g) - (input : Fin n → 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 σ n g) + (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) - (inputWire : Fin n) : + (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 σ n g) + (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) - (gate : Fin g) : + (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 σ n g) - (line : Line σ n g) + (program : Program σ inputCount gateCount) + (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) : - (program.gate line).gateFunction interpretation (Fin.last g) = + (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 σ n g) - (line : Line σ n g) + (program : Program σ inputCount gateCount) + (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) - (gate : Fin g) : + (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 σ n g) + (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) - (input : Fin n → U) - (gate : Fin g) : + (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 : (program : Program σ n g) → Fin g → Line σ n g +def Program.lines {gateCount : Nat} : + (program : Program σ inputCount gateCount) → Fin gateCount → Line σ inputCount gateCount | .empty => Fin.elim0 - | @Program.gate _ _ g program line => + | @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 σ n g) - (line : Line σ n g) : - (program.gate line).lines (Fin.last g) = + (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 σ n g) - (line : Line σ n g) - (gate : Fin g) : + (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 σ n g) + (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) - (input : Fin n → U) - (gate : Fin g) : + (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 g program line ih => - have evalWidened (oldLine : Line σ n g) : + | @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 diff --git a/Cslib/Computability/Circuits/Signature.lean b/Cslib/Computability/Circuits/Signature.lean index 05c4b2fc1f..357679aaf4 100644 --- a/Cslib/Computability/Circuits/Signature.lean +++ b/Cslib/Computability/Circuits/Signature.lean @@ -8,23 +8,29 @@ module public import Cslib.Init /-! -# Signatures +# Signatures and interpretations -A signature is a collection of finitary operation symbols, each with a fixed -arity. Signatures carry no semantics: an `Interpretation` assigns concrete -operations to the symbols, and programs and circuits over a signature are -purely syntactic until they are evaluated in an interpretation. +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 -/-- A collection of finitary operation symbols and their arities. -/ +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 : Op) → Nat + 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/Circuits/Wire.lean b/Cslib/Computability/Circuits/Wire.lean new file mode 100644 index 0000000000..d312a86479 --- /dev/null +++ b/Cslib/Computability/Circuits/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 From 8fe6ced18d1d61b8793fa039058924b12d7813e7 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 9 Sep 2026 09:03:17 -0400 Subject: [PATCH 3/3] refactor(Circuit): rename to Circuit/Basic --- Cslib.lean | 10 +++++----- .../{Circuits/Circuit.lean => Circuit/Basic.lean} | 2 +- .../{Circuits => Circuit}/Homomorphism.lean | 2 +- Cslib/Computability/{Circuits => Circuit}/Program.lean | 4 ++-- .../Computability/{Circuits => Circuit}/Signature.lean | 0 Cslib/Computability/{Circuits => Circuit}/Wire.lean | 0 CslibTests/Circuits.lean | 2 +- 7 files changed, 10 insertions(+), 10 deletions(-) rename Cslib/Computability/{Circuits/Circuit.lean => Circuit/Basic.lean} (98%) rename Cslib/Computability/{Circuits => Circuit}/Homomorphism.lean (98%) rename Cslib/Computability/{Circuits => Circuit}/Program.lean (99%) rename Cslib/Computability/{Circuits => Circuit}/Signature.lean (100%) rename Cslib/Computability/{Circuits => Circuit}/Wire.lean (100%) diff --git a/Cslib.lean b/Cslib.lean index bdb344c918..11234c94b3 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -29,11 +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.Circuits.Circuit -public import Cslib.Computability.Circuits.Homomorphism -public import Cslib.Computability.Circuits.Program -public import Cslib.Computability.Circuits.Signature -public import Cslib.Computability.Circuits.Wire +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/Circuits/Circuit.lean b/Cslib/Computability/Circuit/Basic.lean similarity index 98% rename from Cslib/Computability/Circuits/Circuit.lean rename to Cslib/Computability/Circuit/Basic.lean index e09a797d99..c3d1508bde 100644 --- a/Cslib/Computability/Circuits/Circuit.lean +++ b/Cslib/Computability/Circuit/Basic.lean @@ -5,7 +5,7 @@ Authors: Samuel Schlesinger -/ module -public import Cslib.Computability.Circuits.Program +public import Cslib.Computability.Circuit.Program /-! # Circuits diff --git a/Cslib/Computability/Circuits/Homomorphism.lean b/Cslib/Computability/Circuit/Homomorphism.lean similarity index 98% rename from Cslib/Computability/Circuits/Homomorphism.lean rename to Cslib/Computability/Circuit/Homomorphism.lean index 13e33b6bf2..1e0e5ed7f7 100644 --- a/Cslib/Computability/Circuits/Homomorphism.lean +++ b/Cslib/Computability/Circuit/Homomorphism.lean @@ -5,7 +5,7 @@ Authors: Samuel Schlesinger -/ module -public import Cslib.Computability.Circuits.Signature +public import Cslib.Computability.Circuit.Signature /-! # Homomorphisms of interpretations diff --git a/Cslib/Computability/Circuits/Program.lean b/Cslib/Computability/Circuit/Program.lean similarity index 99% rename from Cslib/Computability/Circuits/Program.lean rename to Cslib/Computability/Circuit/Program.lean index 4bb051d108..47de25b02c 100644 --- a/Cslib/Computability/Circuits/Program.lean +++ b/Cslib/Computability/Circuit/Program.lean @@ -5,8 +5,8 @@ Authors: Samuel Schlesinger -/ module -public import Cslib.Computability.Circuits.Homomorphism -public import Cslib.Computability.Circuits.Wire +public import Cslib.Computability.Circuit.Homomorphism +public import Cslib.Computability.Circuit.Wire /-! # Straight-line programs diff --git a/Cslib/Computability/Circuits/Signature.lean b/Cslib/Computability/Circuit/Signature.lean similarity index 100% rename from Cslib/Computability/Circuits/Signature.lean rename to Cslib/Computability/Circuit/Signature.lean diff --git a/Cslib/Computability/Circuits/Wire.lean b/Cslib/Computability/Circuit/Wire.lean similarity index 100% rename from Cslib/Computability/Circuits/Wire.lean rename to Cslib/Computability/Circuit/Wire.lean diff --git a/CslibTests/Circuits.lean b/CslibTests/Circuits.lean index b5ce53ed10..ee1d707284 100644 --- a/CslibTests/Circuits.lean +++ b/CslibTests/Circuits.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ -import Cslib.Computability.Circuits.Circuit +import Cslib.Computability.Circuit.Basic /-! # Circuit tests