Direct-unrolling packed-step generator -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setStepPositionLimit_sound_internal (extra : ℕ) : (setStepPositionLimit extra).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setStepPositionLimit_requires_internal (extra : ℕ) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) : (setStepPositionLimit extra).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setStepPositionLimit_effect_internal (extra : ℕ) (values : BinaryValues WorkCount) : (setStepPositionLimit extra).effect values = Function.update values Work.limit₁ (values Work.horizon + extra)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setStepPositionLimit_emitted_internal (extra : ℕ) (values : BinaryValues WorkCount) : (setStepPositionLimit extra).emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepImmutableCellCopies_sound_internal : emitStepImmutableCellCopies.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepImmutableCellCopies_requires_internal (values : BinaryValues WorkCount) (htemporary₃ : values Work.temporary₃ = 0) (hscratch : values Work.polynomialScratch = 0) (hmultiply : values Work.multiplyCounter = 0) (hadd : values Work.addCounter = 0) (hcopy : values Work.copyCounter = 0) (hemit : values Work.emitCounter = 0) : emitStepImmutableCellCopies.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepClean.caseFormulaClean_internal {values : BinaryValues WorkCount} (hclean : StepClean values) : CaseFormulaClean values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepClean.writtenCellFormulaClean_internal {values : BinaryValues WorkCount} (hclean : StepClean values) : WrittenCellFormulaClean values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepClean.movedHeadClean_atPosition_internal {values : BinaryValues WorkCount} (hclean : StepClean values) (position : ℕ) : MovedHeadFormulaClean (Function.update values Work.position position)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepClean.writtenCellClean_atPosition_internal {values : BinaryValues WorkCount} (hclean : StepClean values) (position : ℕ) : WrittenCellFormulaClean (Function.update values Work.position position)