Direct-unrolling transition-effect generator -- proof internals

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.EffectConnectorClean (values : BinaryValues WorkCount) : Prop

Scratch invariant while a rolling effect-member output reference moves backward through the variable-width case stream.

• reference₁ : values Work.reference₁ = 0
• loop₃ : values Work.loop₃ = 0
• temporary₂ : values Work.temporary₂ = 0
• temporary₃ : values Work.temporary₃ = 0
• emitCounter : values Work.emitCounter = 0
• copyCounter : values Work.copyCounter = 0
• multiplyCounter : values Work.multiplyCounter = 0
• addCounter : values Work.addCounter = 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectCaseAt_sound_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (caseIndex : ℕ) : (emitEffectCaseAt tm selects caseIndex).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectCaseAt_requires_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (caseIndex : ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitEffectCaseAt tm selects caseIndex).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectCaseAt_effect_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (caseIndex : ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitEffectCaseAt tm selects caseIndex).effect values = Function.update values Work.available (values Work.available + effectFormulaCaseSize k (values Work.horizon) (effectCaseSelectedAt tm selects caseIndex) (effectCaseChoiceAt tm caseIndex))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectCaseAt_emitted_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (caseIndex available : ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : values Work.available = effectFormulaCaseAvailable (transitionCases tm).length k (values Work.horizon) available (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) caseIndex) : (emitEffectCaseAt tm selects caseIndex).emitted values = List.flatMap CircuitCode.RawGate.encode (effectFormulaCaseBlock (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) available (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm) caseIndex)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectMembers_sound_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : (emitEffectMembers tm selects).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectMembers_requires_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitEffectMembers tm selects).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectMembers_effect_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitEffectMembers tm selects).effect values = Function.update values Work.available (values Work.available + prefixSize (effectFormulaSizeAt (transitionCases tm).length k (values Work.horizon) (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm)) (transitionCases tm).length)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectMembers_emitted_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitEffectMembers tm selects).emitted values = List.flatMap CircuitCode.RawGate.encode (effectFormulaCaseGates (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareEffectCaseSize_sound_internal (workCount : ℕ) (selected choiceValue : Bool) : (prepareEffectCaseSize workCount selected choiceValue).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareEffectCaseSize_requires_internal (workCount : ℕ) (selected choiceValue : Bool) (values : BinaryValues WorkCount) (hmultiply : values Work.multiplyCounter = 0) (hadd : values Work.addCounter = 0) : (prepareEffectCaseSize workCount selected choiceValue).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareEffectCaseSize_effect_internal (workCount : ℕ) (selected choiceValue : Bool) (values : BinaryValues WorkCount) (htemporary₂ : values Work.temporary₂ = 0) : (prepareEffectCaseSize workCount selected choiceValue).effect values = Function.update (Function.update values Work.temporary₃ (effectFormulaCaseSize workCount (values Work.horizon) selected choiceValue)) Work.temporary₂ 0

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareEffectCaseSize_emitted_internal (workCount : ℕ) (selected choiceValue : Bool) (values : BinaryValues WorkCount) : (prepareEffectCaseSize workCount selected choiceValue).emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnector_sound_internal (workCount : ℕ) (selected choiceValue : Bool) : (emitPreviousEffectConnector workCount selected choiceValue).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnector_requires_internal (workCount : ℕ) (selected choiceValue : Bool) (values : BinaryValues WorkCount) (hclean : EffectConnectorClean values) (hsize : effectFormulaCaseSize workCount (values Work.horizon) selected choiceValue ≤ values Work.reference₀) (havailable : 1 ≤ values Work.available) : (emitPreviousEffectConnector workCount selected choiceValue).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnector_effect_internal (workCount : ℕ) (selected choiceValue : Bool) (values : BinaryValues WorkCount) (hclean : EffectConnectorClean values) : (emitPreviousEffectConnector workCount selected choiceValue).effect values = Function.update (Function.update values Work.reference₀ (values Work.reference₀ - effectFormulaCaseSize workCount (values Work.horizon) selected choiceValue)) Work.available (values Work.available + 1)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnector_emitted_internal (workCount : ℕ) (selected choiceValue : Bool) (values : BinaryValues WorkCount) (hclean : EffectConnectorClean values) : (emitPreviousEffectConnector workCount selected choiceValue).emitted values = { op := AndOrOp.or, input₀ := values Work.reference₀ - effectFormulaCaseSize workCount (values Work.horizon) selected choiceValue, input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnectors_sound_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : (emitPreviousEffectConnectors tm selects).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectConnectors_requires_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (base T : ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (hbase : 1 ≤ base) (hhorizon : values Work.horizon = T) (havailable : values Work.available = base + prefixSize (effectFormulaSizeAt (transitionCases tm).length k T (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm)) (transitionCases tm).length + 1) : (emitEffectConnectors tm selects).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectConnectors_effect_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (base T : ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (hbase : 1 ≤ base) (hhorizon : values Work.horizon = T) (havailable : values Work.available = base + prefixSize (effectFormulaSizeAt (transitionCases tm).length k T (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm)) (transitionCases tm).length + 1) : (emitEffectConnectors tm selects).effect values = Function.update values Work.available (values Work.available + (transitionCases tm).length)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectConnectors_emitted_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (base T : ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (hbase : 1 ≤ base) (hhorizon : values Work.horizon = T) (havailable : values Work.available = base + prefixSize (effectFormulaSizeAt (transitionCases tm).length k T (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm)) (transitionCases tm).length + 1) : (emitEffectConnectors tm selects).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedRightFoldConnectors AndOrOp.or base (transitionCases tm).length (effectFormulaSizeAt (transitionCases tm).length k T (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm)))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectConnectors_sound_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : (emitEffectConnectors tm selects).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_sound_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : (emitEffectFormula tm selects).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_requires_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitEffectFormula tm selects).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_effect_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitEffectFormula tm selects).effect values = Function.update values Work.available (values Work.available + effectFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_emitted_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitEffectFormula tm selects).emitted values = List.flatMap CircuitCode.RawGate.encode (effectFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

Pointwise all-prefix width certificates

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula_spaceBoundByWidth_internal {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), CaseFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength stateIndex tapeIndex symbolIndex position : ℕ), stateIndex < Fintype.card tm.Q → tapeIndex ≤ k + 1 → symbolIndex < 4 → position ≤ values inputLength Work.horizon → values inputLength Work.available + effectFormulaScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (effectCaseSelectedAt tm selects) (effectCaseChoiceAt tm) + transitionStateRef (values inputLength Work.configBase) stateIndex + (transitionHeadRef (Fintype.card tm.Q) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position + tapeIndex + values inputLength Work.horizon + 1) + (transitionCellRef (Fintype.card tm.Q) (k + 2) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + (k + 2) + tapeIndex + 4) + caseReadSize (values inputLength Work.horizon) + values inputLength Work.horizon ≤ width inputLength) : (emitEffectFormula tm selects).SpaceBoundByWidthAt initialSpace values width