Documentation

Complexitylib.Classes.PPoly.Uniform.Unrolling.Generator.Transition.Step.Internal.Top

Whole-step direct-generator contracts #

This file composes the exact per-region contracts into byte-for-byte contracts for the complete formula phase, packed-copy phase, and deterministic step.

source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepFormulas_emitted_internal {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) :
(emitStepFormulas tm).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (stepAtomCount (Fintype.card tm.Q) k (values Work.horizon)) fun (index : ℕ) => stepFormulaBlockSpecializedInternal tm (values Work.horizon) (values Work.configBase) (values Work.available) index)

Exact byte stream of the complete forward formula phase.

source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_emitted_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) :
(emitStep tm).emitted values = List.flatMap CircuitCode.RawGate.encode (stepSchedule (transitionCases tm.toNTM).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) 0 (values Work.available) (nextHaltStateIndex tm.toNTM) (stepAtomKindAt tm.toNTM (values Work.horizon)) (stepAtomStateIndexAt tm.toNTM (values Work.horizon)) (stepAtomTapeIndexAt tm.toNTM (values Work.horizon)) (stepAtomPositionAt tm.toNTM (values Work.horizon)) (stepAtomSymbolIndexAt tm.toNTM (values Work.horizon)) (stepAtomEffectSelectedAt tm.toNTM (values Work.horizon)) (effectCaseChoiceAt tm.toNTM) (effectCaseStateIndexAt tm.toNTM) (effectCaseInputSymbolIndexAt tm.toNTM) (effectCaseOutputSymbolIndexAt tm.toNTM) (effectCaseWorkSymbolIndexAt tm.toNTM))

Exact byte stream of one complete deterministic packed transition layer.

source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_effect_canonical_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) :
(emitStep tm).effect values = Function.update (Function.update (Function.update (Function.update values Work.available (values Work.available + stepScheduleSize (transitionCases tm.toNTM).length (Fintype.card tm.Q) k (values Work.horizon) (stepAtomKindAt tm.toNTM (values Work.horizon)) (stepAtomEffectSelectedAt tm.toNTM (values Work.horizon)) (effectCaseChoiceAt tm.toNTM))) Work.configBase (stepScheduleOutputBase (transitionCases tm.toNTM).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.available) (stepAtomKindAt tm.toNTM (values Work.horizon)) (stepAtomEffectSelectedAt tm.toNTM (values Work.horizon)) (effectCaseChoiceAt tm.toNTM))) Work.gateBound 0) Work.gateCount 0

The explicit whole-step effect, stated with the canonical numeric prefix.