Polynomial runtime transfer for the detyping sampler

The bound follows the actual one-call program: preprocessing bounds the size of the forwarded query and continuation, the original sampler bounds the forwarded run, and postprocessing reads their combined output. Constants in the graph table are fixed; no uniform graph-compilation bound is asserted.

theorem MIPRE.Cost.Prog.callWithContext_cost {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) (a ctx r : Data) (time : ℕ) (hr : p.Runs a r time) : ∃ t ≤ 2 * a.size + 2 * ctx.size + r.size + time + Polynomial.eval (ctx.size + r.size + 1) post.timeBound + 12, (p.callWithContext post).Runs (a.cons ctx) (post.toFun (ctx, r)) t

theorem MIPRE.Cost.Prog.routeOneCall_direct_cost (route : PolyTimeFun Data (Bool × Data)) (p : Prog) (post : PolyTimeFun (Data × Data) Data) (x r : Data) (h : route.toFun x = (false, r)) : ∃ t ≤ Polynomial.eval x.size route.timeBound + r.size + 4, (routeOneCall route p post).Runs x r t

theorem MIPRE.Cost.Prog.routeOneCall_indirect_cost (route : PolyTimeFun Data (Bool × Data)) {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) (x a ctx r : Data) (time : ℕ) (h : route.toFun x = (true, a.cons ctx)) (hr : p.Runs a r time) : ∃ t ≤ Polynomial.eval x.size route.timeBound + 3 * a.size + 3 * ctx.size + r.size + time + Polynomial.eval (ctx.size + r.size + 1) post.timeBound + 18, (routeOneCall route p post).Runs x (post.toFun (ctx, r)) t

noncomputable def MIPRE.Cost.Prog.routeCost (route : PolyTimeFun Data (Bool × Data)) (post : PolyTimeFun (Data × Data) Data) (B k : ℕ) : Polynomial ℕ

The closed polynomial expression bounding a router with one call to a sampler whose indexed coefficient and input degree are B and k.

Equations

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

noncomputable def MIPRE.Cost.Prog.routeDegree (route : PolyTimeFun Data (Bool × Data)) (post : PolyTimeFun (Data × Data) Data) (k : ℕ) : ℕ

A common query degree, independent of the index and runtime coefficient.

Equations

• MIPRE.Cost.Prog.routeDegree route post k = route.timeBound.natDegree * (k + 1) * (post.timeBound.natDegree + 1)

theorem MIPRE.Cost.Prog.routeCost_natDegree_le (route : PolyTimeFun Data (Bool × Data)) (post : PolyTimeFun (Data × Data) Data) (B k : ℕ) : (routeCost route post B k).natDegree ≤ routeDegree route post k

theorem MIPRE.Cost.Prog.routeOneCall_haltsWithin (route : PolyTimeFun Data (Bool × Data)) {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) (n B k : ℕ) (q : Data) (bound : ∀ (d : Data), HaltsWithin p ((encode n).cons d) (B * (d.size + 1) ^ k)) (preserves : ∀ (a : Data), route.toFun ((encode n).cons q) = (true, a) → ∃ (d : Data) (ctx : Data), a = ((encode n).cons d).cons ctx) : HaltsWithin (routeOneCall route p post) ((encode n).cons q) (Polynomial.eval ((encode n).cons q).size (routeCost route post B k))

noncomputable def MIPRE.CL.Detyping.samplerCost {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (n B k : ℕ) : Polynomial ℕ

The explicit detyping runtime polynomial in the raw query's size.

Equations

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

noncomputable def MIPRE.CL.Detyping.samplerDegree {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (k : ℕ) : ℕ

The common query degree for every index and every original coefficient.

Equations

• MIPRE.CL.Detyping.samplerDegree E k = MIPRE.Cost.Prog.routeDegree (MIPRE.CL.Detyping.Program.route E) (MIPRE.CL.Detyping.Program.post (MIPRE.CL.Detyping.graphDim T)) k

theorem MIPRE.CL.Detyping.samplerCost_natDegree_le {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (n B k : ℕ) : (samplerCost E n B k).natDegree ≤ samplerDegree E k

noncomputable def MIPRE.CL.Detyping.samplerCoefficient {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (n B k : ℕ) : ℕ

The coefficient obtained from the explicit runtime polynomial.

Equations

• MIPRE.CL.Detyping.samplerCoefficient E n B k = ∑ i ∈ Finset.range ((MIPRE.CL.Detyping.samplerCost E n B k).natDegree + 1), (MIPRE.CL.Detyping.samplerCost E n B k).coeff i

theorem MIPRE.CL.Detyping.sampler_haltsWithin {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (hℓ : 0 < ℓ) (n B k : ℕ) (h : S.TimeBoundAt n B k) (q : Cost.Data) : Cost.HaltsWithin (sampler E S hℓ).prog ((Cost.encode n).cons q) (Polynomial.eval q.size (samplerCost E n B k))

theorem MIPRE.CL.Detyping.sampler_timeBoundAt_uniform_degree {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (hℓ : 0 < ℓ) (n B k : ℕ) (h : S.TimeBoundAt n B k) : (sampler E S hℓ).TimeBoundAt n (samplerCoefficient E n B k) (samplerDegree E k)

Detyping preserves a polynomial query bound with a degree independent of n.

theorem MIPRE.CL.Detyping.sampler_timeBound {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (hℓ : 0 < ℓ) (B : ℕ → ℕ) (k : ℕ) (h : ∀ (n : ℕ), S.TimeBoundAt n (B n) k) : (sampler E S hℓ).TimeBound (fun (n : ℕ) => samplerCoefficient E n (B n) k) (samplerDegree E k)

The actual detyped sampler has a global bound whenever the typed sampler does.