Documentation

MIPRE.Tailored.Halting.Tabulate

The tabulation of a tailored verifier #

The tailored counterpart of MIPRE/Foundations/Halting/Tabulate.lean and Halting/Paper/TabulateL.lean: the n-th game of a λ-bounded tailored verifier, written down as a TailoredGameValue.TailoredGameData, by running its three programs under the budgets λ-boundedness supplies.

tabOfT ℓ sd ld pd s T k n is the description that the three encoded programs and four numbers determine. The vertices are the doubled questions, Bool × 𝔽₂^s packed into Fin (2 ^ (s + 1)) as in the existing tabulation (Verifier.tagEquiv), so that the description presents the doubled game (V.tgame n).doubled, which has no weight on its loops:

the weights are Verifier.weightList at the two tagged marginals, as in Halting.tabOf, the marginals queried at the sampler's own level ℓ (margAt) and normalized to length s (margN), which only matters at level 0, where the questions are empty;
the lengths at a vertex are what the answer-length calculator outputs on its question (lenRun), read in unary;
the constraints at a pair of vertices and a readable part of the right length are what the linear-constraints processor outputs there (lpRun), read by Data.bitsListD.

Each run defaults when its budget is missed, which a time bound rules out.

primrec_tabOfT: the description is primitive recursive in its parameters.
presents_tabOfT: for a tailored verifier whose three programs run within T · (|d| + 1)^k at index n, the description presents (V.tgame n).doubled (MIPRE.Tailored.Presents).
tabT TG x n, tabT_computable, presents_tabT: the tabulation of the verifier a description string descOf λ P denotes, (S^λ, L^λ, P), with the budget n^λ · (|d| + 1)^λ, computable in (x, n) and correct when that verifier is λ-bounded and n ≥ 2.

Total readings of data, primitive recursively #

theorem MIPRE.Tailored.unaryToNat_eq_length (d : Cost.Data) :

d.unaryToNat = d.spineList.length

theorem MIPRE.Tailored.primrec_bitD :

Primrec Cost.Data.bitD

theorem MIPRE.Tailored.bitsD_eq_recD (d : Cost.Data) :

d.bitsD = Cost.Data.recD [] (fun (a x : Cost.Data) (x_1 rb : List Bool) => a.bitD :: rb) d

theorem MIPRE.Tailored.primrec_bitsD :

Primrec Cost.Data.bitsD

theorem MIPRE.Tailored.bitsListD_eq_recD (d : Cost.Data) :

d.bitsListD = Cost.Data.recD [] (fun (a x : Cost.Data) (x_1 rb : List Cost.BitStr) => a.bitsD :: rb) d

theorem MIPRE.Tailored.primrec_bitsListD :

Primrec Cost.Data.bitsListD

Budgeted runs #

def MIPRE.Tailored.margAt (ℓ : ℕ) (sd : Cost.Data) (T k n : ℕ) (w : Player) (z : Cost.BitStr) :

Player w's marginal at the level ℓ: one sampler query under the budget T · (|q| + 1) ^ k, [] when the budget is missed. Halting.margOf is the level 7.

Equations

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

Instances For

def MIPRE.Tailored.margN (ℓ : ℕ) (sd : Cost.Data) (T k n s : ℕ) (w : Player) (z : Cost.BitStr) :

The marginal, normalized to length s: an answer of another length, which a sampler of level at least 1 never gives under its time bound, is replaced by zeros. At level 0 the questions are empty, and so is every normalized marginal.

Equations

MIPRE.Tailored.margN ℓ sd T k n s w z = if List.length (MIPRE.Tailored.margAt ℓ sd T k n w z) = s then MIPRE.Tailored.margAt ℓ sd T k n w z else List.map (fun (x : ℕ) => false) (List.range s)

Instances For

def MIPRE.Tailored.lenRun (ld : Cost.Data) (T k n : ℕ) (x : Cost.BitStr) (κ : Bool) :

The length the answer-length calculator outputs on (n, x, κ) under the budget T · (|(x, κ)| + 1) ^ k, read in unary; 0 when the budget is missed.

Equations

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

Instances For

def MIPRE.Tailored.lpRun (pd : Cost.Data) (T k n : ℕ) (x y aR bR : Cost.BitStr) :

List Cost.BitStr

The constraints the linear-constraints processor outputs on (n, x, y, a^R, b^R) under the budget T · (|(x, y, a^R, b^R)| + 1) ^ k, read by Data.bitsListD; [] when the budget is missed.

Equations

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

Instances For

The description #

def MIPRE.Tailored.zOf (s v : ℕ) :

The question at the vertex v of the doubled question set: the bits 1, …, s of v, bit 0 being the tag.

Equations

MIPRE.Tailored.zOf s v = List.map (fun (i : ℕ) => v.testBit (i + 1)) (List.range s)

Instances For

def MIPRE.Tailored.lenList (ld : Cost.Data) (T k n s : ℕ) (κ : Bool) :

The lengths at the vertices, of the readable variables (κ = false) or of the linear ones.

Equations

MIPRE.Tailored.lenList ld T k n s κ = List.map (fun (v : ℕ) => MIPRE.Tailored.lenRun ld T k n (MIPRE.Tailored.zOf s v) κ) (List.range (2 ^ (s + 1)))

Instances For

def MIPRE.Tailored.consAt (pd : Cost.Data) (T k n s : ℕ) (lR : List ℕ) (v v' : ℕ) (γ : Cost.BitStr) :

List (ℕ × ℕ × Cost.BitStr × Cost.BitStr)

The constraint entries at a pair of vertices and a readable part.

Equations

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

Instances For

def MIPRE.Tailored.consT (pd : Cost.Data) (T k n s : ℕ) (lR : List ℕ) :

List (ℕ × ℕ × Cost.BitStr × Cost.BitStr)

The constraint entries: at every pair of vertices and every readable part of the right length, the constraints the processor outputs there.

Equations

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

Instances For

def MIPRE.Tailored.tabOfT (ℓ : ℕ) (sd ld pd : Cost.Data) (s T k n : ℕ) :

TailoredGameValue.TailoredGameData

The tabulation of a tailored verifier, on parameters alone: the sampler, answer-length calculator and linear-constraints processor sd, ld, pd (encoded programs), the dimension s, the budget T · (|d| + 1) ^ k and the index n. The vertices are the doubled questions.

Equations

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

Instances For

Primitive recursion #

theorem MIPRE.Tailored.primrec_margAt {α : Type u_1} [Primcodable α] (ℓ : ℕ) {sd : α → Cost.Data} {T k n : α → ℕ} (hsd : Primrec sd) (hT : Primrec T) (hk : Primrec k) (hn : Primrec n) (w : Player) :

Primrec fun (q : α × Cost.BitStr) => margAt ℓ (sd q.1) (T q.1) (k q.1) (n q.1) w q.2

theorem MIPRE.Tailored.primrec_margN {α : Type u_1} [Primcodable α] (ℓ : ℕ) {sd : α → Cost.Data} {T k n s : α → ℕ} (hsd : Primrec sd) (hT : Primrec T) (hk : Primrec k) (hn : Primrec n) (hs : Primrec s) (w : Player) :

Primrec fun (q : α × Cost.BitStr) => margN ℓ (sd q.1) (T q.1) (k q.1) (n q.1) (s q.1) w q.2

theorem MIPRE.Tailored.primrec_dimOf {α : Type u_1} [Primcodable α] {sd : α → Cost.Data} {T k n : α → ℕ} (hsd : Primrec sd) (hT : Primrec T) (hk : Primrec k) (hn : Primrec n) :

Primrec fun (a : α) => Halting.dimOf (sd a) (T a) (k a) (n a)

theorem MIPRE.Tailored.primrec_lenRun {α : Type u_1} [Primcodable α] {ld : α → Cost.Data} {T k n : α → ℕ} {x : α → Cost.BitStr} {κ : α → Bool} (hld : Primrec ld) (hT : Primrec T) (hk : Primrec k) (hn : Primrec n) (hx : Primrec x) (hκ : Primrec κ) :

Primrec fun (a : α) => lenRun (ld a) (T a) (k a) (n a) (x a) (κ a)

theorem MIPRE.Tailored.primrec_lpRun {α : Type u_1} [Primcodable α] {pd : α → Cost.Data} {T k n : α → ℕ} {x y aR bR : α → Cost.BitStr} (hpd : Primrec pd) (hT : Primrec T) (hk : Primrec k) (hn : Primrec n) (hx : Primrec x) (hy : Primrec y) (haR : Primrec aR) (hbR : Primrec bR) :

Primrec fun (a : α) => lpRun (pd a) (T a) (k a) (n a) (x a) (y a) (aR a) (bR a)

theorem MIPRE.Tailored.primrec_zOf :

theorem MIPRE.Tailored.primrec_lenList {α : Type u_1} [Primcodable α] {ld : α → Cost.Data} {T k n s : α → ℕ} (hld : Primrec ld) (hT : Primrec T) (hk : Primrec k) (hn : Primrec n) (hs : Primrec s) (κ : Bool) :

Primrec fun (a : α) => lenList (ld a) (T a) (k a) (n a) (s a) κ

@[reducible, inline]

abbrev MIPRE.Tailored.ConsParams :

The parameters of the constraint entries, as one tuple.

Equations

MIPRE.Tailored.ConsParams = (MIPRE.Cost.Data × ℕ × ℕ × ℕ × ℕ × List ℕ)

Instances For

theorem MIPRE.Tailored.primrec_consAt :

Primrec fun (q : (ConsParams × ℕ × ℕ) × Cost.BitStr) => consAt q.1.1.1 q.1.1.2.1 q.1.1.2.2.1 q.1.1.2.2.2.1 q.1.1.2.2.2.2.1 q.1.1.2.2.2.2.2 q.1.2.1 q.1.2.2 q.2

theorem MIPRE.Tailored.primrec_consT_params :

Primrec fun (q : ConsParams) => consT q.1 q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2.1 q.2.2.2.2.2

theorem MIPRE.Tailored.primrec_tabOfT {α : Type u_1} [Primcodable α] (ℓ : ℕ) {sd ld pd : α → Cost.Data} {s T k n : α → ℕ} (hsd : Primrec sd) (hld : Primrec ld) (hpd : Primrec pd) (hs : Primrec s) (hT : Primrec T) (hk : Primrec k) (hn : Primrec n) :

Primrec fun (a : α) => tabOfT ℓ (sd a) (ld a) (pd a) (s a) (T a) (k a) (n a)

The tabulation is primitive recursive in its parameters.

The runs, under a time bound #

theorem MIPRE.Tailored.dimOf_eq_of {ℓ : ℕ} (S : CL.Sampler ℓ) {n T k : ℕ} (hb : S.TimeBoundAt n T k) :

Halting.dimOf (Cost.encode S.prog) T k n = S.dim n

The dimension query, under a time bound.

theorem MIPRE.Tailored.margAt_eq_of {ℓ : ℕ} (S : CL.Sampler ℓ) {n T k : ℕ} (hb : S.TimeBoundAt n T k) (hℓ : 1 ≤ ℓ) (w : Player) (z : Cost.BitStr) (hz : List.length z = S.dim n) :

margAt ℓ (Cost.encode S.prog) T k n w z = CL.toBits ((S.cl n w).eval (CL.ofBits (S.dim n) z))

A marginal query, under a time bound, at a level at least 1.

theorem MIPRE.Tailored.margN_eq_of {ℓ : ℕ} (S : CL.Sampler ℓ) {n T k : ℕ} (hb : S.TimeBoundAt n T k) (w : Player) (z : Cost.BitStr) (hz : List.length z = S.dim n) :

margN ℓ (Cost.encode S.prog) T k n (S.dim n) w z = CL.toBits ((S.cl n w).eval (CL.ofBits (S.dim n) z))

The normalized marginal is the sampler's, at every level.

theorem MIPRE.Tailored.lenIs_lenRun (L : Decider) {n T k : ℕ} (hb : L.TimeBoundAt n T k) (x : Cost.BitStr) (κ : Bool) :

LenIs L n x κ (lenRun (Cost.encode L.prog) T k n x κ)

Under a time bound, the budgeted run of the answer-length calculator is its output.

theorem MIPRE.Tailored.lpIs_lpRun (P : Decider) {n T k : ℕ} (hb : P.TimeBoundAt n T k) (x y aR bR : Cost.BitStr) :

LpIs P n x y aR bR (lpRun (Cost.encode P.prog) T k n x y aR bR)

Under a time bound, the budgeted run of the linear-constraints processor is its output.

theorem MIPRE.Tailored.lenOf_eq_lenRun {ℓ : ℕ} (V : TailoredVerifier ℓ) {n T k : ℕ} (hb : V.len.TimeBoundAt n T k) (x : Cost.BitStr) (κ : Bool) :

V.lenOf n x κ = lenRun (Cost.encode V.len.prog) T k n x κ

theorem MIPRE.Tailored.consOf_eq_lpRun {ℓ : ℕ} (V : TailoredVerifier ℓ) {n T k : ℕ} (hL : V.len.TimeBoundAt n T k) (hP : V.lp.TimeBoundAt n T k) (x y aR bR : Cost.BitStr) :

V.consOf n x y aR bR = lpRun (Cost.encode V.lp.prog) T k n x y aR bR

The vertices #

theorem MIPRE.Tailored.testBit_bitsToIdx (l : Cost.BitStr) (j : ℕ) :

(Verifier.bitsToIdx l).testBit j = List.getD l j false

theorem MIPRE.Tailored.zOf_bitsToIdx {s : ℕ} (b : Bool) (z : Cost.BitStr) (hz : List.length z = s) :

zOf s (Verifier.bitsToIdx (b :: z)) = z

theorem MIPRE.Tailored.tabOfT_nV (ℓ : ℕ) (sd ld pd : Cost.Data) (s T k n : ℕ) :

(tabOfT ℓ sd ld pd s T k n).nV + 1 = 2 ^ (s + 1)

noncomputable def MIPRE.Tailored.vtxEquiv (ℓ : ℕ) (sd ld pd : Cost.Data) (s T k n : ℕ) :

Fin ((tabOfT ℓ sd ld pd s T k n).nV + 1) ≃ Bool × (Fin s → CL.𝔽₂)

The vertices of the tabulation are the doubled questions: a tag and a point of 𝔽₂^s.

Equations

MIPRE.Tailored.vtxEquiv ℓ sd ld pd s T k n = (finCongr ⋯).trans (MIPRE.Verifier.tagEquiv s).symm

Instances For

theorem MIPRE.Tailored.vtxEquiv_apply (ℓ : ℕ) (sd ld pd : Cost.Data) (s T k n : ℕ) (i : Fin ((tabOfT ℓ sd ld pd s T k n).nV + 1)) :

Verifier.bitsToIdx (((vtxEquiv ℓ sd ld pd s T k n) i).1 :: CL.toBits ((vtxEquiv ℓ sd ld pd s T k n) i).2) = ↑i

theorem MIPRE.Tailored.zOf_vtxEquiv (ℓ : ℕ) (sd ld pd : Cost.Data) (s T k n : ℕ) (i : Fin ((tabOfT ℓ sd ld pd s T k n).nV + 1)) :

zOf s ↑i = CL.toBits ((vtxEquiv ℓ sd ld pd s T k n) i).2

theorem MIPRE.Tailored.lenList_getD (ℓ : ℕ) (sd ld pd : Cost.Data) (s T k n : ℕ) (κ : Bool) (i : Fin ((tabOfT ℓ sd ld pd s T k n).nV + 1)) :

(lenList ld T k n s κ).getD (↑i) 0 = lenRun ld T k n (zOf s ↑i) κ

theorem MIPRE.Tailored.mem_consT (pd : Cost.Data) (T k n s : ℕ) (lR : List ℕ) (v v' : ℕ) (γ c : Cost.BitStr) :

(v, v', γ, c) ∈ consT pd T k n s lR ↔ v < 2 ^ (s + 1) ∧ v' < 2 ^ (s + 1) ∧ List.length γ = lR.getD v 0 + lR.getD v' 0 ∧ c ∈ lpRun pd T k n (zOf s v) (zOf s v') (List.take (lR.getD v 0) γ) (List.drop (lR.getD v 0) γ)

The question distribution #

theorem MIPRE.Tailored.mu_tabOfT {ℓ : ℕ} (S : CL.Sampler ℓ) {n T k : ℕ} (hS : S.TimeBoundAt n T k) (ld pd : Cost.Data) (i j : Fin ((tabOfT ℓ (Cost.encode S.prog) ld pd (S.dim n) T k n).nV + 1)) :

(tabOfT ℓ (Cost.encode S.prog) ld pd (S.dim n) T k n).toGame.μ i j = if ((vtxEquiv ℓ (Cost.encode S.prog) ld pd (S.dim n) T k n) i).1 = false ∧ ((vtxEquiv ℓ (Cost.encode S.prog) ld pd (S.dim n) T k n) j).1 = true then S.dist n ((vtxEquiv ℓ (Cost.encode S.prog) ld pd (S.dim n) T k n) i).2 ((vtxEquiv ℓ (Cost.encode S.prog) ld pd (S.dim n) T k n) j).2 else 0

The μ clause: the tabulated weight of a pair of vertices is the doubled distribution of the sampler — the weight list enumerates 𝔽₂^s once, each point at the pair its two tagged marginals land on (MIPRE.Halting.mu_clauseL, for a sampler of any level).

The presentation #

theorem MIPRE.Tailored.presents_tabOfT {ℓ : ℕ} (V : TailoredVerifier ℓ) {n T k : ℕ} (hS : V.sampler.TimeBoundAt n T k) (hL : V.len.TimeBoundAt n T k) (hP : V.lp.TimeBoundAt n T k) :

Presents (tabOfT ℓ (Cost.encode V.sampler.prog) (Cost.encode V.len.prog) (Cost.encode V.lp.prog) (V.sampler.dim n) T k n) (V.tgame n).doubled (vtxEquiv ℓ (Cost.encode V.sampler.prog) (Cost.encode V.len.prog) (Cost.encode V.lp.prog) (V.sampler.dim n) T k n)

The tabulation presents the doubled game of a tailored verifier whose three programs run within the budget T · (|d| + 1) ^ k at index n.

The tabulation of a description string #

noncomputable def MIPRE.Tailored.tabT {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (x : Cost.BitStr) (n : ℕ) :

TailoredGameValue.TailoredGameData

The tabulation of the verifier a description string denotes, at index n: the compressed sampler and answer-length calculator at the string's parameter λ, the string's processor, and the budget n^λ · (|d| + 1)^λ that λ-boundedness supplies.

Equations

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

Instances For

theorem MIPRE.Tailored.primrec_tabOfT_tuple (ℓ : ℕ) :

Primrec fun (q : (Cost.Data × Cost.Data × Cost.Data) × ℕ × ℕ × ℕ × ℕ) => tabOfT ℓ q.1.1 q.1.2.1 q.1.2.2 q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2

theorem MIPRE.Tailored.primrec_dimOf_tuple :

Primrec fun (q : Cost.Data × ℕ × ℕ × ℕ) => Halting.dimOf q.1 q.2.1 q.2.2.1 q.2.2.2

theorem MIPRE.Tailored.computable_samplerData {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :

Computable fun (p : Cost.BitStr × ℕ) => Cost.encode (TG.samplerProg.toFun (Halting.descLam p.1))

theorem MIPRE.Tailored.computable_lenData {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :

Computable fun (p : Cost.BitStr × ℕ) => Cost.encode (TG.lenProg.toFun (Halting.descLam p.1))

theorem MIPRE.Tailored.computable_dimT {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :

Computable fun (p : Cost.BitStr × ℕ) => Halting.dimOf (Cost.encode (TG.samplerProg.toFun (Halting.descLam p.1))) (p.2 ^ Halting.descLam p.1) (Halting.descLam p.1) p.2

theorem MIPRE.Tailored.computable_tabT {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :

Computable fun (p : Cost.BitStr × ℕ) => tabT TG p.1 p.2

The tabulation of a description string is computable in the string and the index.

theorem MIPRE.Tailored.presents_tabT {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (lam : ℕ) (P : Decider) (hb : { sampler := TG.sampler lam, len := TG.len lam, lp := P }.IsBounded lam) {n : ℕ} (hn : 2 ≤ n) :

∃ (e : Fin ((tabT TG (Halting.descOf lam P.prog) n).nV + 1) ≃ Bool × { sampler := TG.sampler lam, len := TG.len lam, lp := P }.Questions n), Presents (tabT TG (Halting.descOf lam P.prog) n) ({ sampler := TG.sampler lam, len := TG.len lam, lp := P }.tgame n).doubled e

The tabulation of a description is correct: on the description of a λ-bounded tailored verifier (S^λ, L^λ, P), at every index n ≥ 2, it presents the doubled n-th game.