Fixed-width binary circuit descriptions -- definitions

This module gives fan-in-two raw circuits an Algebraic-style gate-slot view. Every slot has fixed-width binary references, and a bounded description stores exactly gateBound slots together with an explicit active gate count. Active slots must point strictly backward; inactive slots are canonically zero.

The representation is proof-free and finite. A later codec flattens it into the Boolean cube used by approximate counting without parsing variable-length fields.

def Complexity.CircuitCode.FixedWidth.referenceWidth (inputWidth gateBound : ℕ) : ℕ

Positive binary width sufficient for every wire below inputWidth + gateBound. Keeping the width positive lets the verified binary comparator handle even the one-wire edge case.

Equations

• Complexity.CircuitCode.FixedWidth.referenceWidth inputWidth gateBound = max 1 (Fin.bitWidth (inputWidth + gateBound))

def Complexity.CircuitCode.FixedWidth.gateCountWidth (gateBound : ℕ) : ℕ

Positive binary width sufficient for every gate count through gateBound.

Equations

• Complexity.CircuitCode.FixedWidth.gateCountWidth gateBound = max 1 (Fin.bitWidth (gateBound + 1))

def Complexity.CircuitCode.FixedWidth.gateSlotWidth (inputWidth gateBound : ℕ) : ℕ

Three control bits and two fixed-width wire references per gate.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.FixedWidth.codeWidth (inputWidth gateBound : ℕ) : ℕ

Width of a flattened bounded description: one count field followed by exactly gateBound gate slots.

Equations

• One or more equations did not get rendered due to their size.

instance Complexity.CircuitCode.FixedWidth.instNeZeroNatCodeWidth (inputWidth gateBound : ℕ) : NeZero (codeWidth inputWidth gateBound)

structure Complexity.CircuitCode.FixedWidth.GateSlot (width : ℕ) : Type

One fixed-width fan-in-two gate slot.

The operation bit uses the existing raw codec convention: true is AND and false is OR. Reference words are little-endian so the circuit comparator can validate them directly.

• op : Bool

  Raw operation selector.

• negated0 : Bool

  Whether the first input is negated.

• negated1 : Bool

  Whether the second input is negated.

• input0 : BitString width

  Little-endian first wire reference.

• input1 : BitString width

  Little-endian second wire reference.

def Complexity.CircuitCode.FixedWidth.instDecidableEqGateSlot.decEq {width✝ : ℕ} (x✝ x✝¹ : GateSlot width✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Complexity.CircuitCode.FixedWidth.instDecidableEqGateSlot {width✝ : ℕ} : DecidableEq (GateSlot width✝)

Equations

• Complexity.CircuitCode.FixedWidth.instDecidableEqGateSlot = Complexity.CircuitCode.FixedWidth.instDecidableEqGateSlot.decEq

def Complexity.CircuitCode.FixedWidth.gateSlotEquiv (width : ℕ) : GateSlot width ≃ Bool × Bool × Bool × BitString width × BitString width

Product view used to enumerate fixed-width gate slots exactly.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Complexity.CircuitCode.FixedWidth.instFintypeGateSlot (width : ℕ) : Fintype (GateSlot width)

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.FixedWidth.GateSlot.input0Value {width : ℕ} (slot : GateSlot width) : ℕ

Natural value of the first little-endian reference word.

Equations

• slot.input0Value = Nat.fromBitsLE slot.input0.toList

def Complexity.CircuitCode.FixedWidth.GateSlot.input1Value {width : ℕ} (slot : GateSlot width) : ℕ

Natural value of the second little-endian reference word.

Equations

• slot.input1Value = Nat.fromBitsLE slot.input1.toList

def Complexity.CircuitCode.FixedWidth.GateSlot.toRawGate {width : ℕ} (slot : GateSlot width) : RawGate

Convert a fixed slot to the existing proof-free gate syntax.

Equations

• slot.toRawGate = { op := Complexity.CircuitCode.RawGate.opOfBit slot.op, input₀ := slot.input0Value, input₁ := slot.input1Value, negated₀ := slot.negated0, negated₁ := slot.negated1 }

def Complexity.CircuitCode.FixedWidth.GateSlot.zero (width : ℕ) : GateSlot width

Canonical all-zero inactive slot.

Equations

• Complexity.CircuitCode.FixedWidth.GateSlot.zero width = { op := false, negated0 := false, negated1 := false, input0 := fun (x : Fin width) => false, input1 := fun (x : Fin width) => false }

def Complexity.CircuitCode.FixedWidth.GateSlot.WellFormedAt {width : ℕ} (slot : GateSlot width) (available : ℕ) : Prop

Both binary references point to already available wires.

Equations

• slot.WellFormedAt available = (slot.input0Value < available ∧ slot.input1Value < available)

@[instance_reducible]

instance Complexity.CircuitCode.FixedWidth.GateSlot.instDecidableWellFormedAt {width : ℕ} (slot : GateSlot width) (available : ℕ) : Decidable (slot.WellFormedAt available)

Equations

• slot.instDecidableWellFormedAt available = id inferInstance

structure Complexity.CircuitCode.FixedWidth.Description (inputWidth gateBound : ℕ) : Type

A bounded fixed-slot description.

gateCount.val slots are active, while all remaining slots are present so the eventual bit encoding has one parameter-determined width.

• gateCount : Fin (gateBound + 1)

  Number of active gates, ranging from zero through gateBound.

• slots : Fin gateBound → GateSlot (referenceWidth inputWidth gateBound)

  Fixed collection of gate slots.

def Complexity.CircuitCode.FixedWidth.instDecidableEqDescription.decEq {inputWidth✝ gateBound✝ : ℕ} (x✝ x✝¹ : Description inputWidth✝ gateBound✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Complexity.CircuitCode.FixedWidth.instDecidableEqDescription {inputWidth✝ gateBound✝ : ℕ} : DecidableEq (Description inputWidth✝ gateBound✝)

Equations

• Complexity.CircuitCode.FixedWidth.instDecidableEqDescription = Complexity.CircuitCode.FixedWidth.instDecidableEqDescription.decEq

def Complexity.CircuitCode.FixedWidth.descriptionEquiv (inputWidth gateBound : ℕ) : Description inputWidth gateBound ≃ Fin (gateBound + 1) × (Fin gateBound → GateSlot (referenceWidth inputWidth gateBound))

Product view used to enumerate bounded descriptions exactly.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Complexity.CircuitCode.FixedWidth.instFintypeDescription (inputWidth gateBound : ℕ) : Fintype (Description inputWidth gateBound)

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.FixedWidth.Description.gateCountNat {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : ℕ

Active gate count as a natural number.

Equations

• description.gateCountNat = ↑description.gateCount

def Complexity.CircuitCode.FixedWidth.Description.activeSlot {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (index : Fin description.gateCountNat) : GateSlot (referenceWidth inputWidth gateBound)

View an active slot through the full fixed slot array.

Equations

• description.activeSlot index = description.slots ⟨↑index, ⋯⟩

def Complexity.CircuitCode.FixedWidth.Description.toRawCircuit {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : RawCircuit

Existing raw-circuit syntax represented by the active slots.

Equations

• description.toRawCircuit = List.ofFn fun (index : Fin description.gateCountNat) => (description.activeSlot index).toRawGate

def Complexity.CircuitCode.FixedWidth.Description.Positive {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : Prop

The description has at least one active gate, hence a designated output.

Equations

• description.Positive = (0 < description.gateCountNat)

def Complexity.CircuitCode.FixedWidth.Description.TopologicallyWellFormed {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : Prop

Every active gate points to a primary input or an earlier active gate.

Equations

• description.TopologicallyWellFormed = ∀ (index : Fin description.gateCountNat), (description.activeSlot index).WellFormedAt (inputWidth + ↑index)

def Complexity.CircuitCode.FixedWidth.Description.CanonicallyPadded {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : Prop

Every inactive slot is the canonical all-zero slot.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.CircuitCode.FixedWidth.Description.WellFormed {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : Prop

Valid fixed-width descriptions are nonempty, topologically ordered, and canonically padded.

Equations

• description.WellFormed = (description.Positive ∧ description.TopologicallyWellFormed ∧ description.CanonicallyPadded)

@[instance_reducible]

instance Complexity.CircuitCode.FixedWidth.Description.instDecidablePositive {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : Decidable description.Positive

Equations

• description.instDecidablePositive = id inferInstance

@[instance_reducible]

instance Complexity.CircuitCode.FixedWidth.Description.instDecidableTopologicallyWellFormed {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : Decidable description.TopologicallyWellFormed

Equations

• description.instDecidableTopologicallyWellFormed = id inferInstance

@[instance_reducible]

instance Complexity.CircuitCode.FixedWidth.Description.instDecidableCanonicallyPadded {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : Decidable description.CanonicallyPadded

Equations

• description.instDecidableCanonicallyPadded = id inferInstance

@[instance_reducible]

instance Complexity.CircuitCode.FixedWidth.Description.instDecidableWellFormed {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : Decidable description.WellFormed

Equations

• description.instDecidableWellFormed = id inferInstance