Documentation

Complexitylib.Classes.PPoly.Uniform.Unrolling.Generator.Offset.Internal

Dynamic recent-wire offsets -- proof internals #

source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_spaceBoundByWidth_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_spaceBoundByWidth_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_requires_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_effect_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_emitted_internal (reference offset counter : Fin WorkCount) (values : BinaryValues WorkCount) :
(decrementReferenceBy reference offset counter).emitted values = []
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.decrementReferenceBy_sound_internal (reference offset counter : Fin WorkCount) :
(decrementReferenceBy reference offset counter).Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_requires_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_effect_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_spaceBoundByWidth_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_emitted_internal (reference offset counter : Fin WorkCount) (values : BinaryValues WorkCount) :
(prepareDynamicRecentReference reference offset counter).emitted values = []
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareDynamicRecentReference_sound_internal (reference offset counter : Fin WorkCount) :
(prepareDynamicRecentReference reference offset counter).Sound
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_requires_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_effect_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_emitted_internal (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
source
theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitDynamicRecentGate_sound_internal (op : AndOrOp) (negated₀ negated₁ : Bool) (offset counter : Fin WorkCount) (fixedOffset₁ : ℕ) :
(emitDynamicRecentGate op negated₀ negated₁ offset counter fixedOffset₁).Sound