Packed-step generator domains #
Reachable-position loop invariants and exact scratch-domain proofs for the formula and delayed-copy phases of one packed transition step.
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepStateFormulas_requires_internal
{k : ℕ}
(tm : NTM k)
(values : BinaryValues WorkCount)
(hclean : StepClean values)
:
(emitStepStateFormulas tm).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepHeadTapeFormulas_requires_internal
{k : ℕ}
(tm : NTM k)
(tape : TapeSlot k)
(values : BinaryValues WorkCount)
(hclean : MovedHeadFormulaClean values)
(hhorizon : 0 < values Work.horizon)
(hlimit : values Work.limit₁ = values Work.horizon + 1)
(hle : values Work.position ≤ values Work.limit₁)
:
(emitStepHeadTapeFormulas tm tape).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepImmutableCellPosition_requires_internal
{k : ℕ}
(tm : NTM k)
(tape : TapeSlot k)
(values : BinaryValues WorkCount)
(hclean : MovedHeadFormulaClean values)
:
(emitStepImmutableCellPosition tm tape).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepWritableCellPosition_requires_internal
{k : ℕ}
(tm : NTM k)
(tape : WritableSlot k)
(values : BinaryValues WorkCount)
(hclean : MovedHeadFormulaClean values)
(hposition : values Work.position ≤ values Work.horizon + 1)
:
(emitStepWritableCellPosition tm tape).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepCellTapeFormulas_requires_internal
{k : ℕ}
(tm : NTM k)
(tape : TapeSlot k)
(values : BinaryValues WorkCount)
(hclean : MovedHeadFormulaClean values)
(hlimit : values Work.limit₁ = values Work.horizon + 2)
(hle : values Work.position ≤ values Work.limit₁)
:
(emitStepCellTapeFormulas tm tape).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepFormulas_requires_internal
{k : ℕ}
(tm : NTM k)
(values : BinaryValues WorkCount)
(hclean : StepClean values)
(hhorizon : 0 < values Work.horizon)
:
(emitStepFormulas tm).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepStateCopies_requires_internal
{k : ℕ}
(tm : NTM k)
(values : BinaryValues WorkCount)
(hclean : StepClean values)
:
(emitStepStateCopies tm).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepHeadTapeCopies_requires_internal
{k : ℕ}
(tm : NTM k)
(tape : TapeSlot k)
(values : BinaryValues WorkCount)
(hclean : MovedHeadFormulaClean values)
(hlimit : values Work.limit₁ = values Work.horizon + 1)
(hle : values Work.position ≤ values Work.limit₁)
:
(emitStepHeadTapeCopies tm tape).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepWritableCellCopies_requires_internal
{k : ℕ}
(tm : NTM k)
(tape : WritableSlot k)
(values : BinaryValues WorkCount)
(hclean : MovedHeadFormulaClean values)
:
(emitStepWritableCellCopies tm tape).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepCellTapeCopies_requires_internal
{k : ℕ}
(tm : NTM k)
(tape : TapeSlot k)
(values : BinaryValues WorkCount)
(hclean : MovedHeadFormulaClean values)
(hlimit : values Work.limit₁ = values Work.horizon + 2)
(hle : values Work.position ≤ values Work.limit₁)
:
(emitStepCellTapeCopies tm tape).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepPackedCopies_requires_internal
{k : ℕ}
(tm : NTM k)
(values : BinaryValues WorkCount)
(hclean : StepClean values)
:
(emitStepPackedCopies tm).requires values
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_requires_internal
{k : ℕ}
(tm : TM k)
(values : BinaryValues WorkCount)
(hclean : StepClean values)
(hhorizon : 0 < values Work.horizon)
: