Documentation

Complexitylib.Circuits.Encoding.FixedWidth.Validity

Fixed-width description validity formulas #

This module exposes the exact semantics, tree size, and variable support of the structural-validity formula for bounded fixed-width circuit descriptions.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval_wellFormed (inputWidth gateBound : ℕ) (code : BitString (codeWidth inputWidth gateBound)) :
BoolFormula.eval code.toTotal (wellFormed inputWidth gateBound) = decide (EncodedWellFormed code)

The validity formula accepts exactly codes that decode to a structurally valid fixed-width circuit description.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.size_wellFormed (inputWidth gateBound : ℕ) :
(wellFormed inputWidth gateBound).size = wellFormedSize inputWidth gateBound

Exact tree size of the complete fixed-width validity formula.

source
theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.vars_wellFormed_lt (inputWidth gateBound wire : ℕ) :
wire ∈ (wellFormed inputWidth gateBound).vars → wire < codeWidth inputWidth gateBound

Every variable in the validity formula addresses one bit of the incoming fixed-width description code.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.length_compileRaw (inputWidth gateBound : ℕ) :
List.length (compileRaw inputWidth gateBound) = wellFormedSize inputWidth gateBound

Formula compilation preserves the exact validity-formula size.

source
theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.compileRaw_wellFormed (inputWidth gateBound : ℕ) :
RawCircuit.WellFormed (codeWidth inputWidth gateBound) (compileRaw inputWidth gateBound)

The compiled validity formula is a valid single-output raw circuit.

source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval?_compileRaw (inputWidth gateBound : ℕ) (code : BitString (codeWidth inputWidth gateBound)) :
(compileRaw inputWidth gateBound).eval? code.toList = some (decide (EncodedWellFormed code))

Raw evaluation accepts exactly structurally valid fixed-width codes.

source
noncomputable def Complexity.Circuit.fixedWidthDescriptionValidity (inputWidth gateBound : ℕ) :
Circuit Basis.andOr2 (CircuitCode.FixedWidth.codeWidth inputWidth gateBound) 1 (List.length (CircuitCode.FixedWidth.Description.ValidityFormula.compileRaw inputWidth gateBound) - 1)

Typed fan-in-two circuit deciding structural validity of a fixed-width circuit description code.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Complexity.Circuit.size_fixedWidthDescriptionValidity (inputWidth gateBound : ℕ) :
    (fixedWidthDescriptionValidity inputWidth gateBound).size = CircuitCode.FixedWidth.Description.ValidityFormula.wellFormedSize inputWidth gateBound

    Exact size of the typed fixed-width description-validity circuit.

    source
    @[simp]
    theorem Complexity.Circuit.eval_fixedWidthDescriptionValidity (inputWidth gateBound : ℕ) (code : BitString (CircuitCode.FixedWidth.codeWidth inputWidth gateBound)) :
    (fixedWidthDescriptionValidity inputWidth gateBound).eval code 0 = decide (CircuitCode.FixedWidth.Description.EncodedWellFormed code)

    The typed circuit accepts exactly structurally valid fixed-width codes.