Polynomial-time slicing at binary offsets

The requested offset is capped by the actual input length before it is materialized as a unary scan. In particular a large binary bound does not cause an exponentially large intermediate allocation.

def MIPRE.Introspection.DynamicParser.capStepFun (s : ℕ × Cost.Unary) : Bool → ℕ × Cost.Unary

Equations

• MIPRE.Introspection.DynamicParser.capStepFun s x✝ = if List.length s.2 + 1 ≤ s.1 then (s.1, () :: s.2) else s

noncomputable def MIPRE.Introspection.DynamicParser.capStep : Cost.PolyTimeFun ((ℕ × Cost.Unary) × Bool) (ℕ × Cost.Unary)

Equations

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

theorem MIPRE.Introspection.DynamicParser.capStep_apply (s : ℕ × Cost.Unary) (b : Bool) : capStep.toFun (s, b) = capStepFun s b

theorem MIPRE.Introspection.DynamicParser.capStep_size (s : ℕ × Cost.Unary) (b : Bool) : Cost.esize (capStep.toFun (s, b)) ≤ Cost.esize s + Polynomial.eval (Cost.esize b) (Polynomial.C 2)

theorem MIPRE.Introspection.DynamicParser.cap_fold (bs : Cost.BitStr) (n : ℕ) (u : Cost.Unary) (hu : List.length u ≤ n) : List.foldl capStepFun (n, u) bs = (n, Cost.unary (min n (List.length u + List.length bs)))

noncomputable def MIPRE.Introspection.DynamicParser.boundedOffset : Cost.PolyTimeFun (Cost.BitStr × ℕ) Cost.Unary

A uniform binary offset reader, outputting at most one unit per input bit.

Equations

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

@[simp]

theorem MIPRE.Introspection.DynamicParser.boundedOffset_apply (bs : Cost.BitStr) (n : ℕ) : boundedOffset.toFun (bs, n) = Cost.unary (min n (List.length bs))

theorem MIPRE.Introspection.DynamicParser.boundedOffset_length_le (bs : Cost.BitStr) (n : ℕ) : List.length (boundedOffset.toFun (bs, n)) ≤ List.length bs

noncomputable def MIPRE.Introspection.DynamicParser.takeBits : Cost.PolyTimeFun (Cost.BitStr × ℕ) Cost.BitStr

Taking a prefix with a binary index is polynomial in the input encoding size.

Equations

• MIPRE.Introspection.DynamicParser.takeBits = MIPRE.Cost.PolyTimeFun.take.ap₂ MIPRE.Cost.PolyTimeFun.fst MIPRE.Introspection.DynamicParser.boundedOffset

@[simp]

theorem MIPRE.Introspection.DynamicParser.takeBits_apply (bs : Cost.BitStr) (n : ℕ) : takeBits.toFun (bs, n) = List.take n bs

noncomputable def MIPRE.Introspection.DynamicParser.dropBits : Cost.PolyTimeFun (Cost.BitStr × ℕ) Cost.BitStr

Dropping a prefix with a binary index uses the same bounded scan.

Equations

• MIPRE.Introspection.DynamicParser.dropBits = MIPRE.Cost.PolyTimeFun.drop.ap₂ MIPRE.Cost.PolyTimeFun.fst MIPRE.Introspection.DynamicParser.boundedOffset

@[simp]

theorem MIPRE.Introspection.DynamicParser.dropBits_apply (bs : Cost.BitStr) (n : ℕ) : dropBits.toFun (bs, n) = List.drop n bs