A total query router with at most one sampler call

The preprocessing program either supplies a direct result, or an argument and continuation context. Only the latter branch calls the supplied sampler. The postprocessor is total on raw data, so malformed inputs preserve termination whenever routing preserves the sampler index.

def MIPRE.Cost.Prog.callWithContext (p : Prog) (post : PolyTimeFun (Data × Data) Data) : Prog

Equations

• p.callWithContext post = MIPRE.Cost.Prog.fstProg.let_ (p.let_ (((MIPRE.Cost.Prog.callVar 2 MIPRE.Cost.Prog.sndProg).cons (MIPRE.Cost.Prog.var 0)).let_ post.code))

theorem MIPRE.Cost.Prog.callWithContext_closed {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) : WellScoped 1 (p.callWithContext post)

theorem MIPRE.Cost.Prog.callWithContext_runs {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) (a ctx r : Data) (time : ℕ) (hr : p.Runs a r time) : ∃ (t : ℕ), (p.callWithContext post).Runs (a.cons ctx) (post.toFun (ctx, r)) t

def MIPRE.Cost.Prog.routeOneCall (route : PolyTimeFun Data (Bool × Data)) (p : Prog) (post : PolyTimeFun (Data × Data) Data) : Prog

Equations

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

theorem MIPRE.Cost.Prog.routeOneCall_closed (route : PolyTimeFun Data (Bool × Data)) {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) : WellScoped 1 (routeOneCall route p post)

theorem MIPRE.Cost.Prog.routeOneCall_direct (route : PolyTimeFun Data (Bool × Data)) (p : Prog) (post : PolyTimeFun (Data × Data) Data) (x r : Data) (h : route.toFun x = (false, r)) : ∃ (t : ℕ), (routeOneCall route p post).Runs x r t

theorem MIPRE.Cost.Prog.routeOneCall_indirect (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 : ℕ), (routeOneCall route p post).Runs x (post.toFun (ctx, r)) t

theorem MIPRE.Cost.Prog.routeOneCall_halts (route : PolyTimeFun Data (Bool × Data)) {p : Prog} (hp : WellScoped 1 p) (post : PolyTimeFun (Data × Data) Data) (n : ℕ) (q : Data) (halts : ∀ (d : Data), Halts p ((encode n).cons d)) (preserves : ∀ (a : Data), route.toFun ((encode n).cons q) = (true, a) → ∃ (d : Data) (ctx : Data), a = ((encode n).cons d).cons ctx) : Halts (routeOneCall route p post) ((encode n).cons q)

Halting is preserved if each routed call retains the original index.