Padded fixed-width raw-circuit semantics

Valid fixed-width descriptions remain topologically ordered when all canonical inactive slots are retained. This is the semantic target of the bounded sequential encoded evaluator.

theorem Complexity.CircuitCode.FixedWidth.Description.slot_wellFormedAt_of_wellFormed {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) (slot : Fin gateBound) : (description.slots slot).WellFormedAt (inputWidth + ↑slot)

Every slot of a valid description, active or canonically padded, points to a primary input or an earlier slot.

@[simp]

theorem Complexity.CircuitCode.FixedWidth.Description.length_toPaddedRawCircuit {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : List.length description.toPaddedRawCircuit = gateBound

The padded raw circuit has exactly the fixed gate bound as its length.

theorem Complexity.CircuitCode.FixedWidth.Description.take_toPaddedRawCircuit_gateCount {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : List.take description.gateCountNat description.toPaddedRawCircuit = description.toRawCircuit

Taking exactly the active slots from the padded circuit recovers the ordinary raw-circuit view.

theorem Complexity.CircuitCode.FixedWidth.Description.topologicallyWellFormed_toPaddedRawCircuit {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) : RawCircuit.TopologicallyWellFormed inputWidth description.toPaddedRawCircuit

A valid description's complete padded raw circuit is topologically ordered.