Fixed-width description validity formulas -- definitions

This module defines a Boolean formula for structural validity of one bounded fixed-width circuit description. Formula variables address the codec through typed count and slot coordinates, avoiding an auxiliary parser or arithmetic casts between unrelated fields.

The formula checks that the active count is positive and in range. For every gate slot it then checks one of two cases: active slots have backward-pointing references, while inactive slots are the canonical all-zero slot.

def Complexity.CircuitCode.FixedWidth.Description.EncodedWellFormed {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) : Prop

A code is structurally valid when decoding succeeds and the resulting fixed-width description satisfies all three validity conditions.

Equations

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

@[instance_reducible]

instance Complexity.CircuitCode.FixedWidth.Description.instDecidableEncodedWellFormed {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) : Decidable (EncodedWellFormed code)

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.countCoordinate (inputWidth gateBound : ℕ) (coordinate : Fin (gateCountWidth gateBound)) : Fin (codeWidth inputWidth gateBound)

Embed one count-field coordinate into the full description code.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.slotCoordinate (inputWidth gateBound : ℕ) (slot : Fin gateBound) (coordinate : Fin (gateSlotWidth inputWidth gateBound)) : Fin (codeWidth inputWidth gateBound)

Embed one coordinate of one gate slot into the full description code.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.input0Coordinate (inputWidth gateBound : ℕ) (coordinate : Fin (referenceWidth inputWidth gateBound)) : Fin (gateSlotWidth inputWidth gateBound)

Coordinate of a first-reference bit inside one gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.input1Coordinate (inputWidth gateBound : ℕ) (coordinate : Fin (referenceWidth inputWidth gateBound)) : Fin (gateSlotWidth inputWidth gateBound)

Coordinate of a second-reference bit inside one gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.countBit (inputWidth gateBound : ℕ) (coordinate : Fin (gateCountWidth gateBound)) : BoolFormula

Variable formula for one count-field bit.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.slotBit (inputWidth gateBound : ℕ) (slot : Fin gateBound) (coordinate : Fin (gateSlotWidth inputWidth gateBound)) : BoolFormula

Variable formula for one bit of one encoded gate slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.input0Bit (inputWidth gateBound : ℕ) (slot : Fin gateBound) (coordinate : Fin (referenceWidth inputWidth gateBound)) : BoolFormula

Variable formula for one first-reference bit.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.input1Bit (inputWidth gateBound : ℕ) (slot : Fin gateBound) (coordinate : Fin (referenceWidth inputWidth gateBound)) : BoolFormula

Variable formula for one second-reference bit.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.countAtLeast (inputWidth gateBound minimum : ℕ) : BoolFormula

Formula asserting that the encoded active count is at least minimum.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.countAtMost (inputWidth gateBound maximum : ℕ) : BoolFormula

Formula asserting that the encoded active count is at most maximum.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.referenceBelow (inputWidth gateBound : ℕ) (slot : Fin gateBound) (first : Bool) (available : ℕ) : BoolFormula

Formula asserting that one encoded reference is below the number of wires available before its gate.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.slotZero (inputWidth gateBound : ℕ) (slot : Fin gateBound) : BoolFormula

Formula asserting that one complete inactive slot is the all-zero word.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.slotWellFormed (inputWidth gateBound : ℕ) (slot : Fin gateBound) : BoolFormula

Formula asserting that both references of one active slot point backward.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.slotValid (inputWidth gateBound : ℕ) (slot : Fin gateBound) : BoolFormula

Formula asserting the active or inactive invariant for one fixed slot.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.slotValidSize (inputWidth gateBound : ℕ) : ℕ

Exact tree size of one slot-validity formula.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.wellFormedSize (inputWidth gateBound : ℕ) : ℕ

Exact tree size of the complete description-validity formula.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.wellFormed (inputWidth gateBound : ℕ) : BoolFormula

Complete structural-validity formula for one fixed-width description code.

Equations

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

def Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.compileRaw (inputWidth gateBound : ℕ) : RawCircuit

Compile the structural-validity formula after the incoming description code wires.

Equations

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