Documentation

MIPRE.Foundations.CL.DetypingProgRoute

Executable routing of detyped queries #

The fixed finite graph is compiled into a table. The variable content is processed by list operations and at most one call to the original typed sampler. Padding follows the supplied content vector, so malformed queries never cause an unbounded dimension allocation.

@[reducible, inline]

abbrev MIPRE.CL.Detyping.Program.GraphArgs (T : Type u_2) [Fintype T] :

Equations

MIPRE.CL.Detyping.Program.GraphArgs T = (Bool × Bool × (Fin (MIPRE.CL.Detyping.graphDim T) → MIPRE.CL.𝔽₂) × (Fin (MIPRE.CL.Detyping.graphDim T) → MIPRE.CL.𝔽₂))

Instances For

@[reducible, inline]

abbrev MIPRE.CL.Detyping.Program.GraphResult :

Equations

MIPRE.CL.Detyping.Program.GraphResult = (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.Data)

Instances For

noncomputable def MIPRE.CL.Detyping.Program.graphResult {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (a : GraphArgs T) :

Equations

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

Instances For

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

Cost.PolyTimeFun (GraphArgs T) GraphResult

Equations

MIPRE.CL.Detyping.Program.graphAction E = MIPRE.Cost.PolyTimeFun.finiteFunction (MIPRE.CL.Detyping.Program.graphResult E)

Instances For

noncomputable def MIPRE.CL.Detyping.Program.pIndex :

Cost.PolyTimeFun Parsed Cost.Data

Equations

MIPRE.CL.Detyping.Program.pIndex = MIPRE.Cost.PolyTimeFun.fst

Instances For

noncomputable def MIPRE.CL.Detyping.Program.pKind :

Cost.PolyTimeFun Parsed ℕ

Equations

MIPRE.CL.Detyping.Program.pKind = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

Instances For

noncomputable def MIPRE.CL.Detyping.Program.pPlayer :

Cost.PolyTimeFun Parsed Bool

Equations

MIPRE.CL.Detyping.Program.pPlayer = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

Instances For

noncomputable def MIPRE.CL.Detyping.Program.pLevel :

Cost.PolyTimeFun Parsed ℕ

Equations

MIPRE.CL.Detyping.Program.pLevel = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

Instances For

noncomputable def MIPRE.CL.Detyping.Program.pU :

Cost.PolyTimeFun Parsed Cost.BitStr

Equations

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

Instances For

noncomputable def MIPRE.CL.Detyping.Program.pY :

Cost.PolyTimeFun Parsed Cost.BitStr

Equations

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

Instances For

noncomputable def MIPRE.CL.Detyping.Program.graphArgs {T : Type u_1} [Fintype T] :

Cost.PolyTimeFun Parsed (GraphArgs T)

Equations

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

Instances For

@[reducible, inline]

abbrev MIPRE.CL.Detyping.Program.Context :

Equations

MIPRE.CL.Detyping.Program.Context = (MIPRE.CL.Detyping.Program.Parsed × MIPRE.CL.Detyping.Program.GraphResult)

Instances For

def MIPRE.CL.Detyping.Program.content (g : ℕ) (u : Cost.BitStr) :

Equations

MIPRE.CL.Detyping.Program.content g u = List.drop g u

Instances For

def MIPRE.CL.Detyping.Program.pad (b : Bool) (u : Cost.BitStr) :

Equations

MIPRE.CL.Detyping.Program.pad b u = List.map (fun (x : Bool) => b) u

Instances For

def MIPRE.CL.Detyping.Program.directResult (u : Cost.BitStr) :

Bool × Cost.Data

Equations

MIPRE.CL.Detyping.Program.directResult u = (false , MIPRE.Cost.encode u)

Instances For

def MIPRE.CL.Detyping.Program.withPrefix (preBits : Cost.BitStr) :

Equations

MIPRE.CL.Detyping.Program.withPrefix preBits = MIPRE.Cost.Data.nil.cons (MIPRE.Cost.encode preBits)

Instances For

def MIPRE.CL.Detyping.Program.callResult (arg ctx : Cost.Data) :

Bool × Cost.Data

Equations

MIPRE.CL.Detyping.Program.callResult arg ctx = (true , arg.cons ctx)

Instances For

def MIPRE.CL.Detyping.Program.typedRequest (n typ : Cost.Data) (kind : ℕ) (w : Bool) (j : ℕ) (u y : Cost.BitStr) :

Equations

MIPRE.CL.Detyping.Program.typedRequest n typ kind w j u y = n.cons (typ.cons (MIPRE.Cost.encode (kind, w, j, u, y)))

Instances For

noncomputable def MIPRE.CL.Detyping.Program.routeResult (g : ℕ) (p : Parsed) (a : GraphResult) :

Bool × Cost.Data

Equations

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

Instances For

noncomputable def MIPRE.CL.Detyping.Program.directP (u : Cost.PolyTimeFun Context Cost.BitStr) :

Cost.PolyTimeFun Context (Bool × Cost.Data)

Equations

MIPRE.CL.Detyping.Program.directP u = (MIPRE.Cost.PolyTimeFun.const false).pair (MIPRE.CL.Detyping.Program.encoded.comp u)

Instances For

noncomputable def MIPRE.CL.Detyping.Program.callP (arg ctx : Cost.PolyTimeFun Context Cost.Data) :

Cost.PolyTimeFun Context (Bool × Cost.Data)

Equations

MIPRE.CL.Detyping.Program.callP arg ctx = (MIPRE.Cost.PolyTimeFun.const true).pair (MIPRE.Cost.PolyTimeFun.treePair.ap₂ arg ctx)

Instances For

noncomputable def MIPRE.CL.Detyping.Program.prefixP (u : Cost.PolyTimeFun Context Cost.BitStr) :

Cost.PolyTimeFun Context Cost.Data

Equations

MIPRE.CL.Detyping.Program.prefixP u = MIPRE.Cost.PolyTimeFun.treePair.ap₂ (MIPRE.Cost.PolyTimeFun.const MIPRE.Cost.Data.nil) (MIPRE.CL.Detyping.Program.encoded.comp u)

Instances For

noncomputable def MIPRE.CL.Detyping.Program.routeParsed (g : ℕ) :

Cost.PolyTimeFun Context (Bool × Cost.Data)

Equations

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

Instances For

theorem MIPRE.CL.Detyping.Program.routeParsed_apply (g : ℕ) (p : Parsed) (a : GraphResult) :

(routeParsed g).toFun (p, a) = routeResult g p a

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

Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Equations

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

Instances For

noncomputable def MIPRE.CL.Detyping.Program.post (g : ℕ) :

Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

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

Instances For

theorem MIPRE.CL.Detyping.Program.post_dimension (g s : ℕ) :

(post g).toFun (Cost.Data.nil , Cost.encode s) = Cost.encode (s + g)

theorem MIPRE.CL.Detyping.Program.post_prefix (g : ℕ) (preBits result : Cost.BitStr) :

(post g).toFun (withPrefix preBits, Cost.encode result) = Cost.encode (preBits ++ result)

theorem MIPRE.CL.Detyping.Program.routeResult_preserves (g : ℕ) (p : Parsed) (a : GraphResult) (payload : Cost.Data) (h : routeResult g p a = (true , payload)) :

∃ (d : Cost.Data) (ctx : Cost.Data), payload = (p.1.cons d).cons ctx

theorem MIPRE.CL.Detyping.Program.route_preserves {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (n : ℕ) (q payload : Cost.Data) (h : (route E).toFun ((Cost.encode n).cons q) = (true , payload)) :

∃ (d : Cost.Data) (ctx : Cost.Data), payload = ((Cost.encode n).cons d).cons ctx