Direct-unrolling finalization generator -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceStateReference_sound_internal {k : ℕ} (tm : TM k) : (prepareAcceptanceStateReference tm).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceCellPrefix_sound_internal {k : ℕ} (tm : TM k) : (prepareAcceptanceCellPrefix tm).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceCellOffset_sound_internal (k : ℕ) : (prepareAcceptanceCellOffset k).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceReferences_sound_internal {k : ℕ} (tm : TM k) : (prepareAcceptanceReferences tm).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceReferences_effect_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (prepareAcceptanceReferences tm).effect values = acceptanceReferenceValues tm values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceReferences_requires_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) : (prepareAcceptanceReferences tm).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareAcceptanceReferences_emitted_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (prepareAcceptanceReferences tm).emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitAcceptance_emitted_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (emitAcceptance tm).emitted values = (currentAcceptanceGate tm values).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitAcceptance_effect_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (emitAcceptance tm).effect values = afterAcceptanceValues tm values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitAcceptance_requires_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) : (emitAcceptance tm).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding_emitted_internal (values : BinaryValues WorkCount) (hzero : values Work.reference₀ = 0) : emitPadding.emitted values = List.flatMap CircuitCode.RawGate.encode (List.replicate (values Work.frontier - values Work.available) (CircuitCode.RawGate.constant 0 false))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding_requires_internal (values : BinaryValues WorkCount) (hle : values Work.available ≤ values Work.frontier) (hemit : values Work.emitCounter = 0) : emitPadding.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding_spaceBoundByWidth_internal {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hfrontier : ∀ (inputLength : ℕ), values inputLength Work.frontier ≤ width inputLength) (hreference : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) : emitPadding.SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_spaceBoundByPolynomial_internal {k : ℕ} (tm : TM k) (p : Polynomial ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ Polynomial.eval inputLength p) : ∃ (width : Polynomial ℕ), (finalization tm).SpaceBoundByWidthAt initialSpace values fun (x : ℕ) => Polynomial.eval x width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_space_bigO_log_internal {k : ℕ} (tm : TM k) (p : Polynomial ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} (hinitial : BigO initialSpace fun (inputLength : ℕ) => Nat.log 2 inputLength) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ Polynomial.eval inputLength p) : (finalization tm).SpaceBoundInLogAt initialSpace values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_requires_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hle : values Work.available + 1 ≤ values Work.frontier) : (finalization tm).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTerminalCopy_emitted_internal (values : BinaryValues WorkCount) : emitTerminalCopy.emitted values = (CircuitCode.RawGate.copy (values Work.savedOutput)).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_emitted_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (finalization tm).emitted values = (currentAcceptanceGate tm values).encode ++ List.flatMap CircuitCode.RawGate.encode (List.replicate (values Work.frontier - (values Work.available + 1)) (CircuitCode.RawGate.constant 0 false)) ++ (CircuitCode.RawGate.copy (values Work.available)).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_emitted_eq_numericSchedule_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (n originalRawGateCount closedBound T finalConfigBase : ℕ) (hn : 0 < n) (havailable : values Work.available = n + originalRawGateCount - 1) (hfrontier : values Work.frontier = n + closedBound) (hhorizon : values Work.horizon = T) (hconfigBase : values Work.configBase = finalConfigBase) : (finalization tm).emitted values = List.flatMap CircuitCode.RawGate.encode ([numericAcceptanceGate (Fintype.card tm.Q) (stateIndex tm.toNTM tm.qhalt) (k + 2) T finalConfigBase] ++ directFinalizationSuffix n originalRawGateCount closedBound)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitAcceptance_sound_internal {k : ℕ} (tm : TM k) : (emitAcceptance tm).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPaddingGate_sound_internal : emitPaddingGate.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPadding_sound_internal : emitPadding.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTerminalCopy_sound_internal : emitTerminalCopy.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.finalization_sound_internal {k : ℕ} (tm : TM k) : (finalization tm).Sound