A total runtime for a scheduled extractor with a shared scale

The surrounding protocol supplies the common scale L. Valid parameters use the existing complete scheduled program, after cutting the seed word to the exact schedule width. This cut prevents unused padding from entering the final field hash. Invalid parameters return the empty word before any depth-dependent schedule is evaluated.

The paired interface stores source and seed words together and uses word lengths for the three numerical inputs. Decoding remains total on malformed pairings. The runtime does not enumerate semantic field elements.

def Algebraic.Cutwidth.Extractor.MatchedBlockRuntimeValid (n h L e : ℕ) : Prop

Finite conditions permitting the shared-scale schedule and its fixed padded seed budget.

Equations

• Algebraic.Cutwidth.Extractor.MatchedBlockRuntimeValid n h L e = (64 ≤ L ∧ h ≤ 64 ∧ e + h + 2 ≤ L ∧ Nat.clog 2 (n + 1) ≤ L)

@[instance_reducible]

instance Algebraic.Cutwidth.Extractor.instDecidableMatchedBlockRuntimeValid (n h L e : ℕ) : Decidable (MatchedBlockRuntimeValid n h L e)

The runtime guard is decided by natural-number comparisons and a ceiling logarithm.

Equations

• Algebraic.Cutwidth.Extractor.instDecidableMatchedBlockRuntimeValid n h L e = { decide := decide (64 ≤ L) && decide (h ≤ 64 ∧ e + h + 2 ≤ L ∧ Nat.clog 2 (n + 1) ≤ L), reflects_decide := ⋯ }

def Algebraic.Cutwidth.Extractor.matchedBlockExtractorRuntime (h L e : ℕ) (source seeds : List Bool) : List Bool

Run the actual scheduled extractor at a common supplied scale, ignoring unused seed padding.

Equations

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

def Algebraic.Cutwidth.Extractor.matchedBlockExtractorEval (z : List Bool) : List Bool

Codec: pair (pair source seeds) (pair depth (pair scale error)), with unary numbers.

Equations

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