Dynamic recent-wire offsets

Proof-carrying helpers for subtracting a run-time wire offset and emitting a raw gate with one dynamic and one fixed recent-wire reference.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_sound (reference offset counter : Fin WorkCount) : (decrementReferenceBy reference offset counter).Sound

Dynamic reference subtraction is sound on its explicit domain.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_spaceBoundByWidth (reference offset counter : Fin WorkCount) (hdistinct : DecrementReferenceDistinct reference offset counter) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hcounterOffset : ∀ (inputLength : ℕ), values inputLength counter ≤ values inputLength offset) (hiterationsFit : ∀ (inputLength : ℕ), values inputLength offset - values inputLength counter ≤ values inputLength reference) (hreference : ∀ (inputLength : ℕ), values inputLength reference ≤ width inputLength) (hoffset : ∀ (inputLength : ℕ), values inputLength offset ≤ width inputLength) : (decrementReferenceBy reference offset counter).SpaceBoundByWidthAt initialSpace values width

Dynamic subtraction has a pointwise width certificate when its controller segment, starting reference, and preserved offset all fit the shared width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_requires (reference offset counter : Fin WorkCount) (values : BinaryValues WorkCount) : (decrementReferenceBy reference offset counter).requires values ↔ DecrementReferenceDistinct reference offset counter ∧ values counter = 0 ∧ values offset ≤ values reference

The subtraction domain explicitly requires distinct registers, a zero controller, and an offset no larger than the starting reference.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_effect (reference offset counter : Fin WorkCount) (values : BinaryValues WorkCount) (hdistinct : DecrementReferenceDistinct reference offset counter) (hcounter : values counter = 0) : (decrementReferenceBy reference offset counter).effect values = Function.update (Function.update values reference (values reference - values offset)) counter 0

Exact dynamic subtraction with the count-up controller restored to zero.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_emitted (reference offset counter : Fin WorkCount) (values : BinaryValues WorkCount) : (decrementReferenceBy reference offset counter).emitted values = []

Dynamic subtraction emits no circuit-code bits.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_sound (reference offset counter : Fin WorkCount) : (prepareDynamicRecentReference reference offset counter).Sound

Dynamic recent-reference preparation is sound on its explicit domain.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_spaceBoundByWidth (reference offset counter : Fin WorkCount) (hdistinct : DynamicRecentDistinct reference offset counter) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference : ∀ (inputLength : ℕ), values inputLength reference ≤ width inputLength) (hcounter : ∀ (inputLength : ℕ), values inputLength counter = 0) (hoffset : ∀ (inputLength : ℕ), values inputLength offset ≤ values inputLength Work.available) : (prepareDynamicRecentReference reference offset counter).SpaceBoundByWidthAt initialSpace values width

Dynamic recent-reference preparation has a pointwise width certificate when the available wire, old destination, zero controller, and offset fit the shared width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_requires (reference offset counter : Fin WorkCount) (values : BinaryValues WorkCount) : (prepareDynamicRecentReference reference offset counter).requires values ↔ DynamicRecentDistinct reference offset counter ∧ values Work.copyCounter = 0 ∧ values counter = 0 ∧ values offset ≤ values Work.available

The preparation domain records every register separation, both zero controllers, and the valid dynamic offset.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_effect (reference offset counter : Fin WorkCount) (values : BinaryValues WorkCount) (hdistinct : DynamicRecentDistinct reference offset counter) (hcounter : values counter = 0) : (prepareDynamicRecentReference reference offset counter).effect values = Function.update (Function.update values reference (values Work.available - values offset)) counter 0

Exact dynamic recent-wire reference with its controller restored to zero.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_emitted (reference offset counter : Fin WorkCount) (values : BinaryValues WorkCount) : (prepareDynamicRecentReference reference offset counter).emitted values = []

Dynamic recent-reference preparation emits no circuit-code bits.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_sound (op : AndOrOp) (negated₀ negated₁ : Bool) (offset counter : Fin WorkCount) (fixedOffset₁ : ℕ) : (emitDynamicRecentGate op negated₀ negated₁ offset counter fixedOffset₁).Sound

One-dynamic-offset raw-gate emission is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_spaceBoundByWidth (op : AndOrOp) (negated₀ negated₁ : Bool) (offset counter : Fin WorkCount) (fixedOffset₁ : ℕ) (hdistinct : DynamicRecentGateDistinct offset counter) {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) (hcounter : ∀ (inputLength : ℕ), values inputLength counter = 0) (hoffset : ∀ (inputLength : ℕ), values inputLength offset ≤ values inputLength Work.available) (hfixedOffset₁ : ∀ (inputLength : ℕ), fixedOffset₁ ≤ values inputLength Work.available) : (emitDynamicRecentGate op negated₀ negated₁ offset counter fixedOffset₁).SpaceBoundByWidthAt initialSpace values width

One-dynamic-offset gate emission has a pointwise width certificate when its wire frontier, references, zero controller, and both offsets fit the shared width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_requires (op : AndOrOp) (negated₀ negated₁ : Bool) (offset counter : Fin WorkCount) (fixedOffset₁ : ℕ) (values : BinaryValues WorkCount) : (emitDynamicRecentGate op negated₀ negated₁ offset counter fixedOffset₁).requires values ↔ DynamicRecentGateDistinct offset counter ∧ values Work.copyCounter = 0 ∧ values counter = 0 ∧ values offset ≤ values Work.available ∧ fixedOffset₁ ≤ values Work.available ∧ values Work.emitCounter = 0

Exact domain for one-dynamic-offset raw-gate emission.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_effect (op : AndOrOp) (negated₀ negated₁ : Bool) (offset counter : Fin WorkCount) (fixedOffset₁ : ℕ) (values : BinaryValues WorkCount) (hdistinct : DynamicRecentGateDistinct offset counter) (hcounter : values counter = 0) : (emitDynamicRecentGate op negated₀ negated₁ offset counter fixedOffset₁).effect values = Function.update (Function.update (Function.update (Function.update values counter 0) Work.available (values Work.available + 1)) Work.reference₀ 0) Work.reference₁ 0

Dynamic recent-gate emission advances available, restores the loop controller, and clears both reference tapes.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_emitted (op : AndOrOp) (negated₀ negated₁ : Bool) (offset counter : Fin WorkCount) (fixedOffset₁ : ℕ) (values : BinaryValues WorkCount) (hdistinct : DynamicRecentGateDistinct offset counter) (hcounter : values counter = 0) : (emitDynamicRecentGate op negated₀ negated₁ offset counter fixedOffset₁).emitted values = { op := op, input₀ := values Work.available - values offset, input₁ := values Work.available - fixedOffset₁, negated₀ := negated₀, negated₁ := negated₁ }.encode

Exact raw gate emitted from the dynamic and fixed recent-wire offsets.