Dynamic recent-wire offsets -- definitions

Some transition blocks need a wire whose distance behind available is computed at run time. This module prepares such a reference with a bounded binary loop and combines it with one ordinary fixed-offset reference.

The explicit distinctness records rule out aliasing between controller, scratch, reference, and emission registers. They make preservation claims about the dynamic offset and loop counter part of the auditable interface.

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.DecrementReferenceDistinct (reference offset counter : Fin WorkCount) : Prop

Pairwise separation of the reference, dynamic offset, and count-up controller used by dynamic subtraction.

• reference_ne_offset : reference ≠ offset
• reference_ne_counter : reference ≠ counter
• offset_ne_counter : offset ≠ counter

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.DynamicRecentDistinct (reference offset counter : Fin WorkCount) extends Complexity.CircuitUnrolling.Serializer.DirectGenerator.DecrementReferenceDistinct reference offset counter : Prop

Pairwise separation of every register used by dynamic recent-reference preparation.

• reference_ne_offset : reference ≠ offset
• reference_ne_counter : reference ≠ counter
• offset_ne_counter : offset ≠ counter
• available_ne_reference : Work.available ≠ reference
• available_ne_offset : Work.available ≠ offset
• available_ne_counter : Work.available ≠ counter
• available_ne_copyCounter : Work.available ≠ Work.copyCounter
• reference_ne_copyCounter : reference ≠ Work.copyCounter
• offset_ne_copyCounter : offset ≠ Work.copyCounter
• counter_ne_copyCounter : counter ≠ Work.copyCounter

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.DynamicRecentGateDistinct (offset counter : Fin WorkCount) extends Complexity.CircuitUnrolling.Serializer.DirectGenerator.DynamicRecentDistinct Complexity.CircuitUnrolling.Serializer.DirectGenerator.Work.reference₀ offset counter : Prop

Pairwise separation of every register used by dynamic recent-gate emission.

• reference_ne_offset : Work.reference₀ ≠ offset
• reference_ne_counter : Work.reference₀ ≠ counter
• offset_ne_counter : offset ≠ counter
• available_ne_reference : Work.available ≠ Work.reference₀
• available_ne_offset : Work.available ≠ offset
• available_ne_counter : Work.available ≠ counter
• available_ne_copyCounter : Work.available ≠ Work.copyCounter
• reference_ne_copyCounter : Work.reference₀ ≠ Work.copyCounter
• offset_ne_copyCounter : offset ≠ Work.copyCounter
• counter_ne_copyCounter : counter ≠ Work.copyCounter
• available_ne_reference₁ : Work.available ≠ Work.reference₁
• available_ne_emitCounter : Work.available ≠ Work.emitCounter
• reference₀_ne_reference₁ : Work.reference₀ ≠ Work.reference₁
• reference₀_ne_emitCounter : Work.reference₀ ≠ Work.emitCounter
• offset_ne_reference₁ : offset ≠ Work.reference₁
• offset_ne_emitCounter : offset ≠ Work.emitCounter
• counter_ne_reference₁ : counter ≠ Work.reference₁
• counter_ne_emitCounter : counter ≠ Work.emitCounter
• copyCounter_ne_reference₁ : Work.copyCounter ≠ Work.reference₁
• copyCounter_ne_emitCounter : Work.copyCounter ≠ Work.emitCounter
• reference₁_ne_emitCounter : Work.reference₁ ≠ Work.emitCounter

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy (reference offset counter : Fin WorkCount) : BinaryRoutine WorkCount

Subtract a run-time offset from reference with a bounded count-up loop, then restore its controller to zero.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference (reference offset counter : Fin WorkCount) : BinaryRoutine WorkCount

Copy available into reference, decrement it once for every value below the dynamic offset, and restore the count-up controller to zero.

Equations

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

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

Emit a raw gate whose first input has a run-time recent-wire offset and whose second input has a fixed recent-wire offset.

Equations

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