Numeric transition-case schedules -- proof internals #
The member-compilation proof treats the machine and one local transition view as compile-time parameters. It erases them to numeric state, tape, and symbol indices before identifying the emitted stream with the definitions layer.
theorem
Complexity.CircuitUnrolling.Serializer.length_caseChoiceLiteralSchedule_internal
(available choiceWire : ℕ)
(choiceValue : Bool)
:
List.length (caseChoiceLiteralSchedule available choiceWire choiceValue) = caseChoiceLiteralSize choiceValue
theorem
Complexity.CircuitUnrolling.Serializer.length_caseWorkReadGates_internal
(stateCount workCount T configBase available : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
:
List.length (caseWorkReadGates stateCount workCount T configBase available choiceValue workSymbolAt) = workCount * caseReadSize T
theorem
Complexity.CircuitUnrolling.Serializer.getElem_caseWorkReadGates_internal
(stateCount workCount T configBase available : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
(workIndex : Fin workCount)
(offset : Fin (caseReadSize T))
:
(caseWorkReadGates stateCount workCount T configBase available choiceValue
workSymbolAt)[↑workIndex * caseReadSize T + ↑offset] = (readFormulaSchedule stateCount (workCount + 2) T configBase
(caseWorkReadAvailable T available (↑workIndex) choiceValue) (↑workIndex + 1) (workSymbolAt ↑workIndex))[↑offset]
theorem
Complexity.CircuitUnrolling.Serializer.length_caseFormulaMemberGates_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
:
List.length
(caseFormulaMemberGates stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue workSymbolAt) = caseFormulaMembersSize workCount T choiceValue
theorem
Complexity.CircuitUnrolling.Serializer.length_caseFormulaSchedule_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
:
List.length
(caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue workSymbolAt) = caseFormulaScheduleSize workCount T choiceValue
theorem
Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_choice_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
(offset : Fin (caseChoiceLiteralSize choiceValue))
:
(caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue workSymbolAt)[↑offset] = (caseChoiceLiteralSchedule available choiceWire choiceValue)[↑offset]
theorem
Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_state_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
:
(caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue workSymbolAt)[caseChoiceLiteralSize choiceValue] = CircuitCode.RawGate.copy (transitionStateRef configBase stateIndex)
theorem
Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_inputRead_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
(offset : Fin (caseReadSize T))
:
(caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue workSymbolAt)[caseChoiceLiteralSize choiceValue + 1 + ↑offset] = (readFormulaSchedule stateCount (workCount + 2) T configBase (caseInputReadAvailable available choiceValue) 0
inputSymbolIndex)[↑offset]
theorem
Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_workRead_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
(workIndex : Fin workCount)
(offset : Fin (caseReadSize T))
:
(caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue
workSymbolAt)[caseChoiceLiteralSize choiceValue + 1 + caseReadSize T + ↑workIndex * caseReadSize T + ↑offset] = (readFormulaSchedule stateCount (workCount + 2) T configBase
(caseWorkReadAvailable T available (↑workIndex) choiceValue) (↑workIndex + 1) (workSymbolAt ↑workIndex))[↑offset]
theorem
Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_outputRead_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
(offset : Fin (caseReadSize T))
:
(caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue
workSymbolAt)[caseChoiceLiteralSize choiceValue + 1 + (workCount + 1) * caseReadSize T + ↑offset] = (readFormulaSchedule stateCount (workCount + 2) T configBase
(caseOutputReadAvailable workCount T available choiceValue) (workCount + 1) outputSymbolIndex)[↑offset]
theorem
Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_identity_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
:
(caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue workSymbolAt)[caseFormulaMembersSize workCount T choiceValue] = CircuitCode.RawGate.constant 0 true
theorem
Complexity.CircuitUnrolling.Serializer.getElem_caseFormulaSchedule_connector_internal
(stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex outputSymbolIndex : ℕ)
(choiceValue : Bool)
(workSymbolAt : ℕ → ℕ)
(rank : Fin (caseFormulaMemberCount workCount))
:
(caseFormulaSchedule stateCount workCount T configBase choiceWire available stateIndex inputSymbolIndex
outputSymbolIndex choiceValue workSymbolAt)[caseFormulaMembersSize workCount T choiceValue + 1 + ↑rank] = indexedRightFoldConnector AndOrOp.and available (caseFormulaMemberCount workCount)
(caseFormulaSizeAt workCount T choiceValue) ↑rank
theorem
Complexity.CircuitUnrolling.Serializer.compileRaw_caseFormula_eq_schedule_internal
{k : ℕ}
(tm : NTM k)
(T configBase choiceWire available : ℕ)
(view : TransitionCase tm)
:
BoolFormula.compileRaw available (caseFormula tm T configBase choiceWire view) = caseFormulaSchedule (Fintype.card tm.Q) k T configBase choiceWire available (stateIndex tm view.state)
(↑(symbolIndex view.inputRead)) (↑(symbolIndex view.outputRead)) view.choice fun (index : ℕ) =>
if hindex : index < k then ↑(symbolIndex (view.workRead ⟨index, hindex⟩)) else 0