Direct-unrolling initialization generator -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitConstantGate_sound_internal (value : Bool) : (emitConstantGate value).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCopyGate_sound_internal (reference : Fin WorkCount) (negated : Bool) : (emitCopyGate reference negated).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitConstantGate_spaceBoundByWidth_internal (value : Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) : (emitConstantGate value).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCopyGate_spaceBoundByWidth_internal (reference : Fin WorkCount) (negated : Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference : ∀ (inputLength : ℕ), values inputLength reference ≤ width inputLength) : (emitCopyGate reference negated).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStartCell_sound_internal : emitStartCell.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankCell_sound_internal : emitBlankCell.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputDataCell_sound_internal : emitInputDataCell.Sound

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setHorizonLimit_sound_internal : setHorizonLimit.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setInputLimit_sound_internal : setInputLimit.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadPosition_sound_internal : emitHeadPosition.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadTape_sound_internal : emitHeadTape.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputCells_sound_internal : emitInputCells.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankTape_sound_internal : emitBlankTape.Sound

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitConstantGate_effect_internal (value : Bool) (values : BinaryValues WorkCount) : (emitConstantGate value).effect values = Function.update values Work.available (values Work.available + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitConstantGate_emitted_internal (value : Bool) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : (emitConstantGate value).emitted values = (directInitConstant value).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCopyGate_effect_internal (reference : Fin WorkCount) (negated : Bool) (values : BinaryValues WorkCount) : (emitCopyGate reference negated).effect values = Function.update values Work.available (values Work.available + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCopyGate_emitted_internal (reference : Fin WorkCount) (negated : Bool) (values : BinaryValues WorkCount) : (emitCopyGate reference negated).emitted values = (CircuitCode.RawGate.copy (values reference) negated).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStartCell_effect_internal (values : BinaryValues WorkCount) : emitStartCell.effect values = Function.update values Work.available (values Work.available + 4)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStartCell_emitted_internal (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : emitStartCell.emitted values = List.flatMap CircuitCode.RawGate.encode directInitStartCell

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankCell_effect_internal (values : BinaryValues WorkCount) : emitBlankCell.effect values = Function.update values Work.available (values Work.available + 4)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankCell_emitted_internal (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : emitBlankCell.emitted values = List.flatMap CircuitCode.RawGate.encode directInitBlankCell

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputDataCell_effect_internal (values : BinaryValues WorkCount) : emitInputDataCell.effect values = Function.update values Work.available (values Work.available + 4)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputDataCell_emitted_internal (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : emitInputDataCell.emitted values = List.flatMap CircuitCode.RawGate.encode (directInitDataCell (values Work.loop₀))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInitialStates_effect_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (emitInitialStates tm).effect values = Function.update values Work.available (values Work.available + Fintype.card tm.Q)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInitialStates_emitted_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : (emitInitialStates tm).emitted values = List.flatMap CircuitCode.RawGate.encode (directInitStateGates tm)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadPosition_effect_internal (values : BinaryValues WorkCount) : emitHeadPosition.effect values = Function.update values Work.available (values Work.available + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadPosition_emitted_internal (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : emitHeadPosition.emitted values = (directInitHeadGate (values Work.loop₀)).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setHorizonLimit_effect_internal (values : BinaryValues WorkCount) : setHorizonLimit.effect values = Function.update values Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setHorizonLimit_emitted_internal (values : BinaryValues WorkCount) : setHorizonLimit.emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setInputLimit_effect_internal (values : BinaryValues WorkCount) : setInputLimit.effect values = Function.update values Work.limit₀ (values Work.inputLength)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setInputLimit_emitted_internal (values : BinaryValues WorkCount) : setInputLimit.emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadTape_effect_internal (values : BinaryValues WorkCount) : emitHeadTape.effect values = Function.update (Function.update values Work.available (values Work.available + (values Work.limit₀ - values Work.loop₀))) Work.loop₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadTape_emitted_internal (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : emitHeadTape.emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (values Work.limit₀ - values Work.loop₀) fun (offset : ℕ) => [directInitHeadGate (values Work.loop₀ + offset)])

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadTape_emitted_at_horizon_internal (values : BinaryValues WorkCount) (T : ℕ) (hreference : values Work.reference₀ = 0) (hloop : values Work.loop₀ = 0) (hlimit : values Work.limit₀ = T + 1) : emitHeadTape.emitted values = List.flatMap CircuitCode.RawGate.encode (directInitHeadTapeGates T)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputCells_effect_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) (hinput : values Work.inputLength ≤ values Work.horizon + 1) : emitInputCells.effect values = Function.update (Function.update values Work.available (values Work.available + 4 + 4 * (values Work.horizon + 1))) Work.limit₀ (values Work.horizon + 1)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputCells_emitted_internal (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) (hloop : values Work.loop₀ = 0) : emitInputCells.emitted values = List.flatMap CircuitCode.RawGate.encode (directInitInputCellGates (values Work.horizon) (values Work.inputLength))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankTape_effect_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) : emitBlankTape.effect values = Function.update values Work.available (values Work.available + 4 + 4 * values Work.limit₀)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankTape_emitted_internal (values : BinaryValues WorkCount) (T : ℕ) (hreference : values Work.reference₀ = 0) (hloop : values Work.loop₀ = 0) (hlimit : values Work.limit₀ = T + 1) : emitBlankTape.emitted values = List.flatMap CircuitCode.RawGate.encode (directInitBlankTapeCellGates T)

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.tapeInvariant (T : ℕ) (values : BinaryValues WorkCount) : Prop

Register invariant maintained while emitting one tape's initialization gates.

Equations

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.repeatEmitHeadTape_effect_internal (count T : ℕ) (values : BinaryValues WorkCount) (hinvariant : tapeInvariant T values) : (BinaryRoutine.repeatRoutine count emitHeadTape).effect values = Function.update values Work.available (values Work.available + (T + 1) * count)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.repeatEmitHeadTape_emitted_internal (count T : ℕ) (values : BinaryValues WorkCount) (hinvariant : tapeInvariant T values) : (BinaryRoutine.repeatRoutine count emitHeadTape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks count fun (x : ℕ) => directInitHeadTapeGates T)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.repeatEmitBlankTape_effect_internal (count T : ℕ) (values : BinaryValues WorkCount) (hinvariant : tapeInvariant T values) : (BinaryRoutine.repeatRoutine count emitBlankTape).effect values = Function.update values Work.available (values Work.available + (4 + 4 * (T + 1)) * count)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.repeatEmitBlankTape_emitted_internal (count T : ℕ) (values : BinaryValues WorkCount) (hinvariant : tapeInvariant T values) : (BinaryRoutine.repeatRoutine count emitBlankTape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks count fun (x : ℕ) => directInitBlankTapeCellGates T)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_effect_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) (hloop : values Work.loop₀ = 0) (hinput : values Work.inputLength ≤ values Work.horizon + 1) : (initialization tm).effect values = Function.update (Function.update values Work.available (values Work.available + Fintype.card tm.Q + (values Work.horizon + 1) * (k + 2) + 4 + 4 * (values Work.horizon + 1) + (4 + 4 * (values Work.horizon + 1)) * (k + 1))) Work.limit₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_emitted_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) (hloop : values Work.loop₀ = 0) (hinput : values Work.inputLength ≤ values Work.horizon + 1) : (initialization tm).emitted values = List.flatMap CircuitCode.RawGate.encode (directInitSchedule tm (values Work.horizon) (values Work.inputLength))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_effect_preambleValues_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : have values := preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n); have T := Polynomial.eval n (TM.directSerializerHorizonPolynomial q); (initialization tm).effect values = Function.update (Function.update values Work.available (n + Fintype.card tm.Q + (T + 1) * (k + 2) + 4 + 4 * (T + 1) + (4 + 4 * (T + 1)) * (k + 1))) Work.limit₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_emitted_preambleValues_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : (initialization tm).emitted (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n)) = List.flatMap CircuitCode.RawGate.encode (directInitSchedule tm (Polynomial.eval n (TM.directSerializerHorizonPolynomial q)) n)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_loop_restored_preambleValues_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : (initialization tm).effect (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n)) Work.loop₀ = 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_limit_restored_preambleValues_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : (initialization tm).effect (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n)) Work.limit₀ = 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_space_bigO_log_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (initialization tm).SpaceBoundInLogAt TM.binaryLengthSpace fun (inputLength : ℕ) => preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength inputLength)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitConstantGate_requires_internal (value : Bool) (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) : (emitConstantGate value).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCopyGate_loop_requires_internal (negated : Bool) (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) : (emitCopyGate Work.loop₀ negated).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStartCell_requires_internal (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) : emitStartCell.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankCell_requires_internal (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) : emitBlankCell.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputDataCell_requires_internal (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) : emitInputDataCell.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInitialStates_requires_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) : (emitInitialStates tm).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setHorizonLimit_requires_internal (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) : setHorizonLimit.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setInputLimit_requires_internal (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) : setInputLimit.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadPosition_requires_internal (values : BinaryValues WorkCount) (hemit : values Work.emitCounter = 0) : emitHeadPosition.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadTape_requires_internal (values : BinaryValues WorkCount) (hle : values Work.loop₀ ≤ values Work.limit₀) (hemit : values Work.emitCounter = 0) : emitHeadTape.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankTape_requires_internal (values : BinaryValues WorkCount) (hle : values Work.loop₀ ≤ values Work.limit₀) (hemit : values Work.emitCounter = 0) : emitBlankTape.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputCells_requires_internal (values : BinaryValues WorkCount) (hloop : values Work.loop₀ = 0) (hinput : values Work.inputLength ≤ values Work.horizon + 1) (hemit : values Work.emitCounter = 0) (hcopy : values Work.copyCounter = 0) : emitInputCells.requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_requires_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) (hloop : values Work.loop₀ = 0) (hinput : values Work.inputLength ≤ values Work.horizon + 1) (hemit : values Work.emitCounter = 0) (hcopy : values Work.copyCounter = 0) : (initialization tm).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_requires_preambleValues_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) (_hn : 0 < n) : (initialization tm).requires (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n))