Direct-unrolling moved-head generator -- proof internals

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.movedHeadDirectionCode : Dir3 → ℕ

Numeric direction code used by the canonical moved-head schedule.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.movedHeadDirectionCode Complexity.Dir3.left = 0
• Complexity.CircuitUnrolling.Serializer.DirectGenerator.movedHeadDirectionCode Complexity.Dir3.right = 1
• Complexity.CircuitUnrolling.Serializer.DirectGenerator.movedHeadDirectionCode Complexity.Dir3.stay = 2

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

Scratch owned by the conjunction between an effect child and a predecessor-head child. The run-time target and tape selector are deliberately excluded because the predecessor routine preserves them.

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadEffect_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) : (emitMovedHeadEffect tm tape direction).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadEffect_requires_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitMovedHeadEffect tm tape direction).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadEffect_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitMovedHeadEffect tm tape direction).effect values = Function.update values Work.available (values Work.available + movedHeadEffectSizeAt (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (movedHeadDirectionCode direction))

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadEffect_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitMovedHeadEffect tm tape direction).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) (movedHeadCaseSelectedAt tm tape (movedHeadDirectionCode direction)) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadConjunction_sound_internal : emitMovedHeadConjunction.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadConjunction_requires_internal (values : BinaryValues WorkCount) (hclean : MovedHeadConjunctionClean values) (hoffset : movedHeadPredecessorSize (values Work.horizon) + 1 ≤ values Work.available) : emitMovedHeadConjunction.requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadConjunction_effect_internal (values : BinaryValues WorkCount) (hclean : MovedHeadConjunctionClean values) : emitMovedHeadConjunction.effect values = Function.update values Work.available (values Work.available + 1)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadConjunction_emitted_internal (values : BinaryValues WorkCount) (hclean : MovedHeadConjunctionClean values) : emitMovedHeadConjunction.emitted values = { op := AndOrOp.and, input₀ := values Work.available - (movedHeadPredecessorSize (values Work.horizon) + 1), input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.saveMovedHeadMemberOutput_sound_internal (save : Fin WorkCount) : (saveMovedHeadMemberOutput save).Sound

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.movedHeadMemberResult (values : BinaryValues WorkCount) (save : Fin WorkCount) (effectSize : ℕ) : BinaryValues WorkCount

Register state after emitting and saving one moved-head disjunction member.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadMember_requires_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) (directionCode : ℕ) (save : Fin WorkCount) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (hloop₁ : values Work.loop₁ = 0) (hhorizon : 0 < values Work.horizon) (htarget : values Work.limit₂ ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) (hsave : save = Work.savedOutput ∨ save = Work.direction ∨ save = Work.atomKind) : (emitMovedHeadMember tm tape direction directionCode save).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadMember_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) (directionCode : ℕ) (save : Fin WorkCount) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (hloop₁ : values Work.loop₁ = 0) (hhorizon : 0 < values Work.horizon) (htarget : values Work.limit₂ ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) : (emitMovedHeadMember tm tape direction directionCode save).effect values = movedHeadMemberResult values save (movedHeadEffectSizeAt (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (movedHeadDirectionCode direction))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadMember_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) (directionCode base : ℕ) (save : Fin WorkCount) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (hloop₁ : values Work.loop₁ = 0) (hhorizon : 0 < values Work.horizon) (htarget : values Work.limit₂ ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) (hcode : directionCode = movedHeadDirectionCode direction) (hmemberAvailable : values Work.available = movedHeadMemberAvailable (transitionCases tm).length k (values Work.horizon) base (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) directionCode) : (emitMovedHeadMember tm tape direction directionCode save).emitted values = List.flatMap CircuitCode.RawGate.encode (movedHeadMemberBlock (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) base (↑tape.index) (values Work.limit₂) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm) directionCode)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadMember_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (direction : Dir3) (directionCode : ℕ) (save : Fin WorkCount) : (emitMovedHeadMember tm tape direction directionCode save).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitSavedMovedHeadConnector_sound_internal (save : Fin WorkCount) : (emitSavedMovedHeadConnector save).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitSavedMovedHeadConnector_requires_internal (save : Fin WorkCount) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hemit : values Work.emitCounter = 0) (havailable : 1 ≤ values Work.available) (hsave : save = Work.savedOutput ∨ save = Work.direction ∨ save = Work.atomKind) : (emitSavedMovedHeadConnector save).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitSavedMovedHeadConnector_effect_internal (save : Fin WorkCount) (values : BinaryValues WorkCount) (hreference₁ : values Work.reference₁ = 0) (hemit : values Work.emitCounter = 0) : (emitSavedMovedHeadConnector save).effect values = Function.update values Work.available (values Work.available + 1)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitSavedMovedHeadConnector_emitted_internal (save : Fin WorkCount) (values : BinaryValues WorkCount) (hsave : save = Work.savedOutput ∨ save = Work.direction ∨ save = Work.atomKind) : (emitSavedMovedHeadConnector save).emitted values = { op := AndOrOp.or, input₀ := values save, input₁ := values Work.available - 1, negated₀ := false, negated₁ := false }.encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_sound_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : (emitMovedHeadFormula tm tape).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_requires_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) : (emitMovedHeadFormula tm tape).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) : (emitMovedHeadFormula tm tape).effect values = Function.update values Work.available (values Work.available + movedHeadFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) (havailable : 1 ≤ values Work.available) : (emitMovedHeadFormula tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (movedHeadFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (↑tape.index) (values Work.position) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitMovedHeadFormula_spaceBoundByWidth_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), MovedHeadFormulaClean (values inputLength)) (hhorizon : ∀ (inputLength : ℕ), 0 < values inputLength Work.horizon) (htarget : ∀ (inputLength : ℕ), values inputLength Work.position ≤ values inputLength Work.horizon) (havailable : ∀ (inputLength : ℕ), 1 ≤ values inputLength Work.available) (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 + 1 → values inputLength Work.available + movedHeadFormulaScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (movedHeadCaseSelectedAt tm tape) (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) + 2 * TM.binaryPolynomialValueCap predecessorHeadSchedulePolynomial (values inputLength Work.horizon) + 2 * (values inputLength Work.horizon + 2) + values inputLength Work.horizon ≤ width inputLength) : (emitMovedHeadFormula tm tape).SpaceBoundByWidthAt initialSpace values width