Fixed-width description validity formulas -- proof internals

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.code_apply_countCoordinate_internal {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) (coordinate : Fin (gateCountWidth gateBound)) : code (countCoordinate inputWidth gateBound coordinate) = countBits code coordinate

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.code_apply_slotCoordinate_internal {inputWidth gateBound : ℕ} (code : BitString (codeWidth inputWidth gateBound)) (slot : Fin gateBound) (coordinate : Fin (gateSlotWidth inputWidth gateBound)) : code (slotCoordinate inputWidth gateBound slot coordinate) = slotBits code slot coordinate

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.decode_input0_internal {inputWidth gateBound : ℕ} (bits : BitString (gateSlotWidth inputWidth gateBound)) (coordinate : Fin (referenceWidth inputWidth gateBound)) : (GateSlot.decode bits).input0 coordinate = bits (input0Coordinate inputWidth gateBound coordinate)

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.decode_input1_internal {inputWidth gateBound : ℕ} (bits : BitString (gateSlotWidth inputWidth gateBound)) (coordinate : Fin (referenceWidth inputWidth gateBound)) : (GateSlot.decode bits).input1 coordinate = bits (input1Coordinate inputWidth gateBound coordinate)

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval_countAtLeast_internal {inputWidth gateBound : ℕ} (minimum : ℕ) (code : BitString (codeWidth inputWidth gateBound)) (hminimum : minimum < 2 ^ gateCountWidth gateBound) : BoolFormula.eval code.toTotal (countAtLeast inputWidth gateBound minimum) = decide (minimum ≤ countValue code)

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval_countAtMost_internal {inputWidth gateBound : ℕ} (maximum : ℕ) (code : BitString (codeWidth inputWidth gateBound)) (hmaximum : maximum < 2 ^ gateCountWidth gateBound) : BoolFormula.eval code.toTotal (countAtMost inputWidth gateBound maximum) = decide (countValue code ≤ maximum)

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval_referenceBelow_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (first : Bool) (available : ℕ) (code : BitString (codeWidth inputWidth gateBound)) (havailable : available < 2 ^ referenceWidth inputWidth gateBound) : BoolFormula.eval code.toTotal (referenceBelow inputWidth gateBound slot first available) = decide (if first = true then (GateSlot.decode (slotBits code slot)).input0Value < available else (GateSlot.decode (slotBits code slot)).input1Value < available)

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval_slotZero_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (code : BitString (codeWidth inputWidth gateBound)) : BoolFormula.eval code.toTotal (slotZero inputWidth gateBound slot) = decide (GateSlot.decode (slotBits code slot) = GateSlot.zero (referenceWidth inputWidth gateBound))

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval_slotWellFormed_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (code : BitString (codeWidth inputWidth gateBound)) : BoolFormula.eval code.toTotal (slotWellFormed inputWidth gateBound slot) = decide ((GateSlot.decode (slotBits code slot)).WellFormedAt (inputWidth + ↑slot))

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval_slotValid_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) (code : BitString (codeWidth inputWidth gateBound)) : BoolFormula.eval code.toTotal (slotValid inputWidth gateBound slot) = decide ((↑slot < countValue code → (GateSlot.decode (slotBits code slot)).WellFormedAt (inputWidth + ↑slot)) ∧ (countValue code ≤ ↑slot → GateSlot.decode (slotBits code slot) = GateSlot.zero (referenceWidth inputWidth gateBound)))

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval_wellFormed_internal (inputWidth gateBound : ℕ) (code : BitString (codeWidth inputWidth gateBound)) : BoolFormula.eval code.toTotal (wellFormed inputWidth gateBound) = decide (EncodedWellFormed code)

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.size_slotValid_internal (inputWidth gateBound : ℕ) (slot : Fin gateBound) : (slotValid inputWidth gateBound slot).size = slotValidSize inputWidth gateBound

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.size_wellFormed_internal (inputWidth gateBound : ℕ) : (wellFormed inputWidth gateBound).size = wellFormedSize inputWidth gateBound

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

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.length_compileRaw_internal (inputWidth gateBound : ℕ) : List.length (compileRaw inputWidth gateBound) = wellFormedSize inputWidth gateBound

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

theorem Complexity.CircuitCode.FixedWidth.Description.ValidityFormula.eval?_compileRaw_internal (inputWidth gateBound : ℕ) (code : BitString (codeWidth inputWidth gateBound)) : (compileRaw inputWidth gateBound).eval? code.toList = some (decide (EncodedWellFormed code))