The typed oracularized sampler

Piece O3 of planning/oracularization.md (issue #189): the sampler of the paper's typed oracularized verifier (sec:orac-def) as a CL.TypedSampler over the three roles, whose typed CL functions are roleFamily of the input sampler's (the identity for the oracle, the input's for the isolated players) — the half of lem:oracle-effective-interface about the sampler.

The program is the fixed core OracleSampler.core, run on the input sampler's program through the s-m-n construction hardcode, as the repeated sampler is. The core routes a typed query with at most one call to the input sampler, through the universal machine:

• the dimension query is forwarded unchanged;
• a query at an isolated role is forwarded as the query of the corresponding original player;
• a query at the oracle role is answered from the query itself, with no call at all: the identity's marginals are the seed, its first stage map is the identity and its later ones zero, its first factor space is everything and its later ones nothing. The zero vectors are written over the supplied vector rather than over the dimension, so the core never allocates by a dimension it has not been given.

The identity's queries

theorem MIPRE.CL.CLFun.factorOfPrefix_trivialOn {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ k : ℕ) (u : ι → F) : (trivialOn ℓ).factorOfPrefix k u = ∅

theorem MIPRE.CL.CLFun.mapOfPrefix_trivialOn {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ k : ℕ) (u : ι → F) : (trivialOn ℓ).mapOfPrefix k u = 0

theorem MIPRE.CL.CLFun.eval_truncate_ident {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ j : ℕ) (hj : 1 ≤ j) (x : ι → F) : (truncate j (ident ℓ)).eval x = x

Every marginal of the identity from the first on is the identity.

theorem MIPRE.CL.CLFun.mapOfPrefix_ident_zero {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ : ℕ) (u : ι → F) : (ident ℓ).mapOfPrefix 0 u = proj Finset.univ

theorem MIPRE.CL.CLFun.mapOfPrefix_ident_succ {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ k : ℕ) (u : ι → F) : (ident ℓ).mapOfPrefix (k + 1) u = 0

theorem MIPRE.CL.CLFun.factorOfPrefix_ident_zero {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ : ℕ) (u : ι → F) : (ident ℓ).factorOfPrefix 0 u = Finset.univ

theorem MIPRE.CL.CLFun.factorOfPrefix_ident_succ {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (ℓ k : ℕ) (u : ι → F) : (ident ℓ).factorOfPrefix (k + 1) u = ∅

theorem MIPRE.CL.toBits_zero' (s : ℕ) : toBits 0 = List.replicate s false

theorem MIPRE.CL.indicatorBits_univ_eq (s : ℕ) : indicatorBits Finset.univ = List.replicate s true

theorem MIPRE.CL.indicatorBits_empty_eq (s : ℕ) : indicatorBits ∅ = List.replicate s false

@[simp]

theorem MIPRE.Cost.PolyTimeFun.const_toFun {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (b : β) : (const b).toFun = fun (x : α) => b

@[simp]

theorem MIPRE.CL.encode_typedQuery_dimension {T : Type u_1} [Cost.SizedEncoding T] : Cost.encode TypedSampler.Query.dimension = Cost.Data.nil

@[simp]

theorem MIPRE.CL.encode_typedQuery_atType {T : Type u_1} [Cost.SizedEncoding T] (t : T) (q : Sampler.Query) : Cost.encode (TypedSampler.Query.atType t q) = (Cost.encode t).cons (Cost.encode q)

def MIPRE.CL.Sampler.Query.withPlayer (w : Player) : Query → Query

A query with its player replaced; the dimension query has none.

Equations

• MIPRE.CL.Sampler.Query.withPlayer w MIPRE.CL.Sampler.Query.dimension = MIPRE.CL.Sampler.Query.dimension
• MIPRE.CL.Sampler.Query.withPlayer w (MIPRE.CL.Sampler.Query.marginal w_1 j z) = MIPRE.CL.Sampler.Query.marginal w j z
• MIPRE.CL.Sampler.Query.withPlayer w (MIPRE.CL.Sampler.Query.linear w_1 j u y) = MIPRE.CL.Sampler.Query.linear w j u y
• MIPRE.CL.Sampler.Query.withPlayer w (MIPRE.CL.Sampler.Query.factor w_1 j u) = MIPRE.CL.Sampler.Query.factor w j u

Roles as data

def MIPRE.Role.toNat : Role → ℕ

The roles as numbers: the oracle 0, the isolated Alice 1, the isolated Bob 2.

Equations

• MIPRE.Role.oracle.toNat = 0
• MIPRE.Role.alice.toNat = 1
• MIPRE.Role.bob.toNat = 2

def MIPRE.Role.ofNat? : ℕ → Option Role

Reading a role back.

Equations

• MIPRE.Role.ofNat? 0 = some MIPRE.Role.oracle
• MIPRE.Role.ofNat? 1 = some MIPRE.Role.alice
• MIPRE.Role.ofNat? 2 = some MIPRE.Role.bob
• MIPRE.Role.ofNat? x✝ = none

@[instance_reducible]

instance MIPRE.instSizedEncodingRole : Cost.SizedEncoding Role

Equations

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

theorem MIPRE.encode_role_oracle : Cost.encode Role.oracle = Cost.Data.nil

theorem MIPRE.encode_role_alice : Cost.encode Role.alice = (Cost.Data.nil.cons Cost.Data.nil).cons Cost.Data.nil

theorem MIPRE.encode_role_bob : Cost.encode Role.bob = Cost.Data.nil.cons ((Cost.Data.nil.cons Cost.Data.nil).cons Cost.Data.nil)

The core

noncomputable def MIPRE.OracleSampler.sD : Cost.PolyTimeFun Cost.Data Cost.Data

The input sampler's program, hardcoded first.

Equations

• MIPRE.OracleSampler.sD = MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.OracleSampler.nD : Cost.PolyTimeFun Cost.Data Cost.Data

The index.

Equations

• MIPRE.OracleSampler.nD = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail

noncomputable def MIPRE.OracleSampler.qD : Cost.PolyTimeFun Cost.Data Cost.Data

The typed query, nil for the dimension query.

Equations

• MIPRE.OracleSampler.qD = MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail

noncomputable def MIPRE.OracleSampler.tagD : Cost.PolyTimeFun Cost.Data Cost.Data

The type of a typed query.

Equations

• MIPRE.OracleSampler.tagD = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.OracleSampler.qD

noncomputable def MIPRE.OracleSampler.queryD : Cost.PolyTimeFun Cost.Data Cost.Data

The untyped query of a typed query.

Equations

• MIPRE.OracleSampler.queryD = MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.OracleSampler.qD

noncomputable def MIPRE.OracleSampler.request (q : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

A call to the input sampler, through the universal machine, on the query q.

Equations

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

noncomputable def MIPRE.OracleSampler.asPlayer (w : Player) : Cost.PolyTimeFun Cost.Data Cost.Data

An isolated role's query, as the query of the corresponding original player.

Equations

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

noncomputable def MIPRE.OracleSampler.parsedQ : Cost.PolyTimeFun Cost.Data CL.Detyping.Program.Parsed

The untyped query, parsed: (n, kind, w, j, u, y).

Equations

• MIPRE.OracleSampler.parsedQ = MIPRE.CL.Detyping.Program.parse.comp (MIPRE.Cost.PolyTimeFun.treePair.ap₂ MIPRE.OracleSampler.nD MIPRE.OracleSampler.queryD)

noncomputable def MIPRE.OracleSampler.oracleBits : Cost.PolyTimeFun Cost.Data Cost.BitStr

The oracle's answers, read off the query alone: the marginal of the identity is the seed; its first stage map is the identity and its later ones zero; its first factor space is everything and its later ones nothing.

Equations

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

noncomputable def MIPRE.OracleSampler.route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

The router: the dimension query and the isolated roles' queries go to the input sampler, the oracle's are answered directly.

Equations

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

noncomputable def MIPRE.OracleSampler.post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

The answer of the call is the answer.

Equations

• MIPRE.OracleSampler.post = MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.OracleSampler.core : Cost.Prog

The core of the typed oracularized sampler.

Equations

• MIPRE.OracleSampler.core = MIPRE.Cost.Prog.routeOneCall MIPRE.OracleSampler.route MIPRE.Cost.selfUniversal.univ MIPRE.OracleSampler.post

theorem MIPRE.OracleSampler.core_closed : Cost.Prog.WellScoped 1 core

The router on well-formed queries

theorem MIPRE.OracleSampler.route_dimension (sp : Cost.Prog) (n : ℕ) : route.toFun ((Cost.encode sp).cons (Cost.encode (n, CL.TypedSampler.Query.dimension))) = (true, ((Cost.encode sp).cons (Cost.encode (n, CL.Sampler.Query.dimension))).cons Cost.Data.nil)

theorem MIPRE.OracleSampler.route_alice (sp : Cost.Prog) (n : ℕ) (q : CL.Sampler.Query) (hq : q ≠ CL.Sampler.Query.dimension) : route.toFun ((Cost.encode sp).cons (Cost.encode (n, CL.TypedSampler.Query.atType Role.alice q))) = (true, ((Cost.encode sp).cons (Cost.encode (n, CL.Sampler.Query.withPlayer Player.alice q))).cons Cost.Data.nil)

theorem MIPRE.OracleSampler.route_bob (sp : Cost.Prog) (n : ℕ) (q : CL.Sampler.Query) (hq : q ≠ CL.Sampler.Query.dimension) : route.toFun ((Cost.encode sp).cons (Cost.encode (n, CL.TypedSampler.Query.atType Role.bob q))) = (true, ((Cost.encode sp).cons (Cost.encode (n, CL.Sampler.Query.withPlayer Player.bob q))).cons Cost.Data.nil)

def MIPRE.OracleSampler.oracleAnswer : CL.Sampler.Query → Cost.BitStr

The oracle's answer to an untyped query, as the core computes it.

Equations

• MIPRE.OracleSampler.oracleAnswer MIPRE.CL.Sampler.Query.dimension = []
• MIPRE.OracleSampler.oracleAnswer (MIPRE.CL.Sampler.Query.marginal w j z) = z
• MIPRE.OracleSampler.oracleAnswer (MIPRE.CL.Sampler.Query.linear w j u y) = if j = 1 then y else List.map (fun (x : Bool) => false) y
• MIPRE.OracleSampler.oracleAnswer (MIPRE.CL.Sampler.Query.factor w j u) = if j = 1 then List.map (fun (x : Bool) => true) u else List.map (fun (x : Bool) => false) u

theorem MIPRE.OracleSampler.parsedQ_apply (sp : Cost.Prog) (n : ℕ) (d : Cost.Data) (q : CL.Sampler.Query) : parsedQ.toFun ((Cost.encode sp).cons ((Cost.encode n).cons (d.cons (Cost.encode q)))) = (Cost.encode n, q.toTuple.1, q.toTuple.2.1.toBool, q.toTuple.2.2.1, q.toTuple.2.2.2.1, q.toTuple.2.2.2.2)

theorem MIPRE.OracleSampler.route_oracle (sp : Cost.Prog) (n : ℕ) (q : CL.Sampler.Query) : route.toFun ((Cost.encode sp).cons (Cost.encode (n, CL.TypedSampler.Query.atType Role.oracle q))) = (false, Cost.encode (oracleAnswer q))

theorem MIPRE.OracleSampler.route_call_shape (sD' nD' qd' payload : Cost.Data) (h : route.toFun (sD'.cons (nD'.cons qd')) = (true, payload)) : ∃ (q' : Cost.Data), payload = (sD'.cons (nD'.cons q')).cons Cost.Data.nil

Every call the router makes keeps the hardcoded program and the index.

The typed sampler

noncomputable def MIPRE.OracleSampler.prog (sp : Cost.Prog) : Cost.Prog

The program of the typed oracularized sampler on the input sampler's program sp.

Equations

• MIPRE.OracleSampler.prog sp = MIPRE.Cost.hardcode MIPRE.OracleSampler.core (MIPRE.Cost.encode sp)

theorem MIPRE.OracleSampler.prog_closed (sp : Cost.Prog) : Cost.Prog.WellScoped 1 (prog sp)

theorem MIPRE.OracleSampler.prog_runs_forward (n : ℕ) {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (x : Cost.Data) (q : CL.Sampler.Query) (r : Cost.Data) (t : ℕ) (hroute : route.toFun ((Cost.encode S.prog).cons x) = (true, ((Cost.encode S.prog).cons (Cost.encode (n, q))).cons Cost.Data.nil)) (hS : S.prog.Runs (Cost.encode (n, q)) r t) : ∃ (t' : ℕ), (prog S.prog).Runs x r t'

A forwarded query is answered by the input sampler, through the universal machine.

theorem MIPRE.OracleSampler.prog_runs_oracle (n : ℕ) {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (q : CL.Sampler.Query) : ∃ (t : ℕ), (prog S.prog).Runs (Cost.encode (n, CL.TypedSampler.Query.atType Role.oracle q)) (Cost.encode (oracleAnswer q)) t

An oracle query is answered directly.

noncomputable def MIPRE.oracleSampler {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) : CL.TypedSampler (ℓ + 1) Role

The typed oracularized sampler (the sampler of sec:orac-def): the typed CL functions are the identity for the oracle and the input sampler's own for the isolated players, the same for both players; the program answers an isolated role's query as the input sampler answers the corresponding original player's, and an oracle query directly. It depends on the input sampler alone.

Equations

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

@[simp]

theorem MIPRE.oracleSampler_dim {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (n : ℕ) : (oracleSampler S).dim n = S.dim n

@[simp]

theorem MIPRE.oracleSampler_cl {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (n : ℕ) (w : Player) (t : Role) : (oracleSampler S).cl n w t = roleFamily (S.cl n) t

The running time

theorem MIPRE.OracleSampler.size_treeHead_le (e : Cost.Data) : (Cost.PolyTimeFun.treeHead.toFun e).size ≤ e.size

theorem MIPRE.OracleSampler.size_treeTail_le (e : Cost.Data) : (Cost.PolyTimeFun.treeTail.toFun e).size ≤ e.size

theorem MIPRE.OracleSampler.size_call_le (sD' nD' d q' : Cost.Data) (h : route.toFun (sD'.cons (nD'.cons d)) = (true, (sD'.cons (nD'.cons q')).cons Cost.Data.nil)) : q'.size ≤ 2 * d.size + 9

A forwarded query is at most twice the typed query, plus a constant: it is the dimension query, or the typed query's own fields with the player replaced.

noncomputable def MIPRE.OracleSampler.coreCost (xs B k X : ℕ) : ℕ

The explicit cost of the core on an input of size xs, at the input sampler's coefficient B and degree k, with X one more than the size of the typed query.

Equations

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

theorem MIPRE.OracleSampler.core_runs_within {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (n : ℕ) {B k : ℕ} (hS : S.TimeBoundAt n B k) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ coreCost ((Cost.encode S.prog).cons ((Cost.encode n).cons d)).size B k (d.size + 1), core.Runs ((Cost.encode S.prog).cons ((Cost.encode n).cons d)) r t

The core halts within coreCost on every input of the typed sampler, well formed or not: the router, at most one call to the input sampler through the universal machine, and the postprocessing.

theorem MIPRE.OracleSampler.oracleSampler_timeBound : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {ℓ : ℕ} (S : CL.Sampler (ℓ + 1)) (n B k W : ℕ), B ≤ W → Cost.esize S.prog ≤ W → n ≤ W → S.TimeBoundAt n B k → (oracleSampler S).TimeBoundAt n (c * (W + 1) ^ m) (e * (k + 1))

The running time of the typed oracularized sampler: constants c, m, e uniform in everything such that, whenever W dominates the input sampler's coefficient, its description length and the index, and the input sampler runs within B (|d| + 1)^k at n, the typed sampler runs within c (W + 1)^m (|d| + 1)^{e (k + 1)}. A forwarded query is at most a constant factor larger than the typed query, and since |d| + 1 ≥ 2 that factor is absorbed into the degree, so no term exponential in k enters the coefficient.

noncomputable def MIPRE.OracleSampler.samplerProgFun : Cost.PolyTimeFun Cost.Prog Cost.Prog

The program is a polynomial-time function of the input sampler's program: the s-m-n map at the fixed core.

Equations

• MIPRE.OracleSampler.samplerProgFun = (MIPRE.Cost.PolyTimeFun.smn MIPRE.Cost.Prog).comp ((MIPRE.Cost.PolyTimeFun.const MIPRE.OracleSampler.core).pair (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Prog))

theorem MIPRE.OracleSampler.samplerProgFun_apply (sp : Cost.Prog) : samplerProgFun.toFun sp = prog sp