Documentation

Complexitylib.Circuits.Encoding.FixedWidth.Conversion.Internal

Conversion between raw circuits and fixed-width descriptions -- internals #

source
theorem Complexity.CircuitCode.FixedWidth.GateSlot.toList_referenceBits_internal (width value : ℕ) :
(referenceBits width value).toList = width.toBitsLE value
source
theorem Complexity.CircuitCode.FixedWidth.GateSlot.referenceBits_fromBitsLE_internal {width : ℕ} (bits : BitString width) :
referenceBits width (Nat.fromBitsLE bits.toList) = bits
source
theorem Complexity.CircuitCode.FixedWidth.GateSlot.input0Value_ofRawGate_internal (width : ℕ) (gate : RawGate) :
(ofRawGate width gate).input0Value = gate.input₀ % 2 ^ width
source
theorem Complexity.CircuitCode.FixedWidth.GateSlot.input1Value_ofRawGate_internal (width : ℕ) (gate : RawGate) :
(ofRawGate width gate).input1Value = gate.input₁ % 2 ^ width
source
theorem Complexity.CircuitCode.FixedWidth.GateSlot.toRawGate_ofRawGate_internal {width : ℕ} {gate : RawGate} (hinput0 : gate.input₀ < 2 ^ width) (hinput1 : gate.input₁ < 2 ^ width) :
(ofRawGate width gate).toRawGate = gate
source
theorem Complexity.CircuitCode.FixedWidth.GateSlot.ofRawGate_toRawGate_internal {width : ℕ} (slot : GateSlot width) :
ofRawGate width slot.toRawGate = slot
source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.gateCountNat_ofRawCircuit_internal {inputWidth gateBound : ℕ} (circuit : RawCircuit) (hbound : List.length circuit ≤ gateBound) :
(ofRawCircuit circuit hbound).gateCountNat = List.length circuit
source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.slot_ofRawCircuit_of_lt_internal {inputWidth gateBound : ℕ} (circuit : RawCircuit) (hbound : List.length circuit ≤ gateBound) (index : Fin gateBound) (hindex : ↑index < List.length circuit) :
(ofRawCircuit circuit hbound).slots index = GateSlot.ofRawGate (referenceWidth inputWidth gateBound) circuit[↑index]
source
@[simp]
theorem Complexity.CircuitCode.FixedWidth.Description.slot_ofRawCircuit_of_le_internal {inputWidth gateBound : ℕ} (circuit : RawCircuit) (hbound : List.length circuit ≤ gateBound) (index : Fin gateBound) (hindex : List.length circuit ≤ ↑index) :
(ofRawCircuit circuit hbound).slots index = GateSlot.zero (referenceWidth inputWidth gateBound)
source
theorem Complexity.CircuitCode.FixedWidth.Description.toRawCircuit_ofRawCircuit_internal {inputWidth gateBound : ℕ} {circuit : RawCircuit} (htopological : RawCircuit.TopologicallyWellFormed inputWidth circuit) (hbound : List.length circuit ≤ gateBound) :
(ofRawCircuit circuit hbound).toRawCircuit = circuit
source
theorem Complexity.CircuitCode.FixedWidth.Description.ofRawCircuit_wellFormed_internal {inputWidth gateBound : ℕ} {circuit : RawCircuit} (hcircuit : RawCircuit.WellFormed inputWidth circuit) (hbound : List.length circuit ≤ gateBound) :
(ofRawCircuit circuit hbound).WellFormed
source
theorem Complexity.CircuitCode.FixedWidth.Description.ofRawCircuit_toRawCircuit_internal {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hcanonical : description.CanonicallyPadded) :
ofRawCircuit description.toRawCircuit ⋯ = description
source
def Complexity.CircuitCode.FixedWidth.wellFormedEquivInternal (inputWidth gateBound : ℕ) :
ValidDescription inputWidth gateBound ≃ BoundedRawCircuit inputWidth gateBound

Internal exact equivalence between valid fixed descriptions and bounded raw circuits.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.CircuitCode.FixedWidth.wellFormedEquiv_apply_val_internal {inputWidth gateBound : ℕ} (description : ValidDescription inputWidth gateBound) :
    ↑((wellFormedEquivInternal inputWidth gateBound) description) = (↑description).toRawCircuit
    source
    theorem Complexity.CircuitCode.FixedWidth.wellFormedEquiv_symm_val_internal {inputWidth gateBound : ℕ} (circuit : BoundedRawCircuit inputWidth gateBound) :
    ↑((wellFormedEquivInternal inputWidth gateBound).symm circuit) = Description.ofRawCircuit ↑circuit ⋯