Direct-unrolling generator primitives -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference_spaceBoundByWidth_internal (reference : Fin WorkCount) (offset : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference : ∀ (inputLength : ℕ), values inputLength reference ≤ width inputLength) (hoffset : ∀ (inputLength : ℕ), offset ≤ values inputLength Work.available) : (prepareRecentReference reference offset).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference_sound_internal (reference : Fin WorkCount) (offset : ℕ) : (prepareRecentReference reference offset).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference_requires_internal (reference : Fin WorkCount) (offset : ℕ) (values : BinaryValues WorkCount) (havailableReference : Work.available ≠ reference) (havailableCounter : Work.available ≠ Work.copyCounter) (hreferenceCounter : reference ≠ Work.copyCounter) : (prepareRecentReference reference offset).requires values ↔ values Work.copyCounter = 0 ∧ offset ≤ values Work.available

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference_effect_internal (reference : Fin WorkCount) (offset : ℕ) (values : BinaryValues WorkCount) : (prepareRecentReference reference offset).effect values = Function.update values reference (values Work.available - offset)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference_emitted_internal (reference : Fin WorkCount) (offset : ℕ) (values : BinaryValues WorkCount) : (prepareRecentReference reference offset).emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_sound_internal (op : AndOrOp) (negated₀ negated₁ : Bool) (offset₀ offset₁ : ℕ) : (emitRecentGate op negated₀ negated₁ offset₀ offset₁).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_requires_internal (op : AndOrOp) (negated₀ negated₁ : Bool) (offset₀ offset₁ : ℕ) (values : BinaryValues WorkCount) : (emitRecentGate op negated₀ negated₁ offset₀ offset₁).requires values ↔ values Work.copyCounter = 0 ∧ offset₀ ≤ values Work.available ∧ offset₁ ≤ values Work.available ∧ values Work.emitCounter = 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_effect_internal (op : AndOrOp) (negated₀ negated₁ : Bool) (offset₀ offset₁ : ℕ) (values : BinaryValues WorkCount) : (emitRecentGate op negated₀ negated₁ offset₀ offset₁).effect values = Function.update (Function.update (Function.update values Work.available (values Work.available + 1)) Work.reference₀ 0) Work.reference₁ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_spaceBoundByWidth_internal (op : AndOrOp) (negated₀ negated₁ : Bool) (offset₀ offset₁ : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference₀ : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) (hreference₁ : ∀ (inputLength : ℕ), values inputLength Work.reference₁ ≤ width inputLength) (hoffset₀ : ∀ (inputLength : ℕ), offset₀ ≤ values inputLength Work.available) (hoffset₁ : ∀ (inputLength : ℕ), offset₁ ≤ values inputLength Work.available) : (emitRecentGate op negated₀ negated₁ offset₀ offset₁).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_emitted_internal (op : AndOrOp) (negated₀ negated₁ : Bool) (offset₀ offset₁ : ℕ) (values : BinaryValues WorkCount) : (emitRecentGate op negated₀ negated₁ offset₀ offset₁).emitted values = { op := op, input₀ := values Work.available - offset₀, input₁ := values Work.available - offset₁, negated₀ := negated₀, negated₁ := negated₁ }.encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareStateReference_sound_internal (stateIndex : ℕ) : (prepareStateReference stateIndex).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareStateReference_requires_internal (stateIndex : ℕ) (values : BinaryValues WorkCount) : (prepareStateReference stateIndex).requires values ↔ values Work.addCounter = 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareStateReference_effect_internal (stateIndex : ℕ) (values : BinaryValues WorkCount) : (prepareStateReference stateIndex).effect values = Function.update values Work.reference₀ (transitionStateRef (values Work.configBase) stateIndex)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareStateReference_emitted_internal (stateIndex : ℕ) (values : BinaryValues WorkCount) : (prepareStateReference stateIndex).emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareStateReference_spaceBoundByWidth_internal (stateIndex : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionStateRef (values inputLength Work.configBase) stateIndex ≤ width inputLength) : (prepareStateReference stateIndex).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareHeadReference_sound_internal (stateCount : ℕ) : (prepareHeadReference stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareHeadReference_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) : (prepareHeadReference stateCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareHeadReference_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) : (prepareHeadReference stateCount).effect values = Function.update (Function.update values Work.reference₀ (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position))) Work.temporary₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareHeadReference_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) : (prepareHeadReference stateCount).emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareHeadReference_spaceBoundByWidth_internal (stateCount : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionHeadRef stateCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) (values inputLength Work.position) + values inputLength Work.tapeIndex + values inputLength Work.horizon + 1 ≤ width inputLength) : (prepareHeadReference stateCount).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReference_sound_internal (stateCount tapeCount : ℕ) : (prepareCellReference stateCount tapeCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReference_requires_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) : (prepareCellReference stateCount tapeCount).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReference_effect_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) : (prepareCellReference stateCount tapeCount).effect values = Function.update (Function.update (Function.update (Function.update values Work.reference₀ (transitionCellRef stateCount tapeCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position) (values Work.symbolIndex))) Work.temporary₀ 0) Work.temporary₁ 0) Work.temporary₂ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReference_emitted_internal (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) : (prepareCellReference stateCount tapeCount).emitted values = []

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReference_spaceBoundByWidth_internal (stateCount tapeCount : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionCellRef stateCount tapeCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) (values inputLength Work.position) (values inputLength Work.symbolIndex) + (values inputLength Work.tapeIndex * (values inputLength Work.horizon + 2) + values inputLength Work.position) + (values inputLength Work.horizon + 2) + tapeCount + values inputLength Work.tapeIndex + 4 ≤ width inputLength) : (prepareCellReference stateCount tapeCount).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreparedReference_sound_internal {prepare : BinaryRoutine WorkCount} (hprepare : prepare.Sound) (negated : Bool) : (emitPreparedReference prepare negated).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference_sound_internal (stateIndex : ℕ) (negated : Bool) : (emitStateReference stateIndex negated).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_sound_internal (stateCount : ℕ) (negated : Bool) : (emitHeadReference stateCount negated).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_sound_internal (stateCount tapeCount : ℕ) (negated : Bool) : (emitCellReference stateCount tapeCount negated).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference_spaceBoundByWidth_internal (stateIndex : ℕ) (negated : Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionStateRef (values inputLength Work.configBase) stateIndex ≤ width inputLength) : (emitStateReference stateIndex negated).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_spaceBoundByWidth_internal (stateCount : ℕ) (negated : Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionHeadRef stateCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) (values inputLength Work.position) + values inputLength Work.tapeIndex + values inputLength Work.horizon + 1 ≤ width inputLength) : (emitHeadReference stateCount negated).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_spaceBoundByWidth_internal (stateCount tapeCount : ℕ) (negated : Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionCellRef stateCount tapeCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) (values inputLength Work.position) (values inputLength Work.symbolIndex) + (values inputLength Work.tapeIndex * (values inputLength Work.horizon + 2) + values inputLength Work.position) + (values inputLength Work.horizon + 2) + tapeCount + values inputLength Work.tapeIndex + 4 ≤ width inputLength) : (emitCellReference stateCount tapeCount negated).SpaceBoundByWidthAt initialSpace values width

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference_requires_internal (stateIndex : ℕ) (negated : Bool) (values : BinaryValues WorkCount) (hadd : values Work.addCounter = 0) (hemit : values Work.emitCounter = 0) : (emitStateReference stateIndex negated).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_requires_internal (stateCount : ℕ) (negated : Bool) (values : BinaryValues WorkCount) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitHeadReference stateCount negated).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_requires_internal (stateCount tapeCount : ℕ) (negated : Bool) (values : BinaryValues WorkCount) (hcopy : values Work.copyCounter = 0) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitCellReference stateCount tapeCount negated).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference_effect_internal (stateIndex : ℕ) (negated : Bool) (values : BinaryValues WorkCount) : (emitStateReference stateIndex negated).effect values = Function.update (Function.update values Work.available (values Work.available + 1)) Work.reference₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_effect_internal (stateCount : ℕ) (negated : Bool) (values : BinaryValues WorkCount) : (emitHeadReference stateCount negated).effect values = Function.update (Function.update (Function.update values Work.temporary₀ 0) Work.available (values Work.available + 1)) Work.reference₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_effect_internal (stateCount tapeCount : ℕ) (negated : Bool) (values : BinaryValues WorkCount) : (emitCellReference stateCount tapeCount negated).effect values = Function.update (Function.update (Function.update (Function.update (Function.update values Work.temporary₀ 0) Work.temporary₁ 0) Work.temporary₂ 0) Work.available (values Work.available + 1)) Work.reference₀ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference_emitted_internal (stateIndex : ℕ) (negated : Bool) (values : BinaryValues WorkCount) : (emitStateReference stateIndex negated).emitted values = (CircuitCode.RawGate.copy (transitionStateRef (values Work.configBase) stateIndex) negated).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_emitted_internal (stateCount : ℕ) (negated : Bool) (values : BinaryValues WorkCount) : (emitHeadReference stateCount negated).emitted values = (CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position)) negated).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_emitted_internal (stateCount tapeCount : ℕ) (negated : Bool) (values : BinaryValues WorkCount) : (emitCellReference stateCount tapeCount negated).emitted values = (CircuitCode.RawGate.copy (transitionCellRef stateCount tapeCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position) (values Work.symbolIndex)) negated).encode