Direct-unrolling generator primitives

Executable fixed-work helpers for recent-wire raw gates and numeric state, head, and cell configuration-wire references.

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

Fixed-offset preparation by copy and repeated positive predecessor is sound on its explicit routine domain.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference_spaceBoundByWidth (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

Fixed-offset recent-reference preparation has a pointwise width certificate when the source, old destination, and requested offset fit the shared width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareRecentReference_requires (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

The recent-reference domain is exactly a zero copy counter and a valid offset, once the three framed-copy indices are known to be distinct.

@[simp]

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

Exact fixed-offset reference value.

@[simp]

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

Reference preparation emits no circuit-code bits.

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

A raw gate from two recent-wire offsets is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_spaceBoundByWidth (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

A raw gate from two fixed recent-wire offsets has a pointwise width certificate when the frontier, old references, and offsets fit the shared width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_requires (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

Exact dynamic domain for recent-wire gate emission.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_effect (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

Recent-wire gate emission advances available once and clears both reference tapes.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRecentGate_emitted (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

Exact raw gate emitted from the two prepared recent-wire references.

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

Numeric state-reference preparation is sound.

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

State-reference preparation needs exactly its framed addition counter.

@[simp]

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

Exact numeric state-wire reference.

@[simp]

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

State-reference preparation emits nothing.

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

Numeric head-reference preparation is sound.

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

Zero framed arithmetic counters discharge the complete head-reference domain.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareHeadReference_effect (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

Exact numeric head-wire reference, with its arithmetic temporary cleared.

@[simp]

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

Head-reference preparation emits nothing.

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

Numeric cell-reference preparation is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReference_requires (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

Zero copy, addition, and multiplication counters discharge the complete cell-reference domain.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareCellReference_effect (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

Exact numeric cell-symbol wire reference, with all three arithmetic temporaries cleared.

@[simp]

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

Cell-reference preparation emits nothing.

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

Any sound preparation routine composes soundly with prepared-reference copy emission.

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

Prepared numeric state-reference emission is sound.

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

Prepared numeric head-reference emission is sound.

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

Prepared numeric cell-reference emission is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference_spaceBoundByWidth (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

State-reference emission has a pointwise width certificate when every incoming register and the resulting absolute reference fit the width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_spaceBoundByWidth (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

Head-reference emission has a pointwise width certificate under one envelope covering all arithmetic intermediates.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_spaceBoundByWidth (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

Cell-reference emission has a pointwise width certificate under one envelope covering its base, offset, and final-reference arithmetic.

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

Zero addition and emission counters discharge state-reference emission.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_requires (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

Zero arithmetic and emission counters discharge head-reference emission.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_requires (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

Zero arithmetic, copy, and emission counters discharge cell-reference emission.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStateReference_effect (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

State-reference emission advances available and clears the reference.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_effect (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

Head-reference emission advances available and clears both scratches.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_effect (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

Cell-reference emission advances available and clears all four reference/arithmetic scratch tapes.

@[simp]

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

Exact state-wire copy gate emitted by the executable helper.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadReference_emitted (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

Exact head-wire copy gate emitted by the executable helper.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCellReference_emitted (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

Exact cell-symbol wire copy gate emitted by the executable helper.