An executable fixed graph sampler

Every fixed finite CL presentation has a total ambient sampler program: a finite table covers its valid queries, with a fixed output on other inputs. We instantiate this construction with the two-level graph presentation used by detyping. Its dimension, all query answers and halting on malformed inputs are proved. This finite-table construction is polynomial in query size for each fixed graph; it does not claim polynomial compilation in graph size.

@[reducible, inline]

abbrev MIPRE.CL.FixedSampler.QueryIndex (d ℓ : ℕ) : Type

Equations

• MIPRE.CL.FixedSampler.QueryIndex d ℓ = (Fin 3 × Bool × Fin (ℓ + 1) × (Fin d → MIPRE.CL.𝔽₂) × (Fin d → MIPRE.CL.𝔽₂))

def MIPRE.CL.FixedSampler.queryOfIndex {d ℓ : ℕ} (i : QueryIndex d ℓ) : Sampler.Query

Equations

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

def MIPRE.CL.FixedSampler.queries (d ℓ : ℕ) : Finset Cost.Data

Equations

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

theorem MIPRE.CL.FixedSampler.dimension_mem (d ℓ : ℕ) : Cost.encode Sampler.Query.dimension ∈ queries d ℓ

theorem MIPRE.CL.FixedSampler.marginal_mem {d ℓ : ℕ} (w : Player) (j : ℕ) (z : Cost.BitStr) (hj : j ≤ ℓ) (hz : List.length z = d) : Cost.encode (Sampler.Query.marginal w j z) ∈ queries d ℓ

theorem MIPRE.CL.FixedSampler.linear_mem {d ℓ : ℕ} (w : Player) (j : ℕ) (u y : Cost.BitStr) (hj : j ≤ ℓ) (hu : List.length u = d) (hy : List.length y = d) : Cost.encode (Sampler.Query.linear w j u y) ∈ queries d ℓ

theorem MIPRE.CL.FixedSampler.factor_mem {d ℓ : ℕ} (w : Player) (j : ℕ) (u : Cost.BitStr) (hj : j ≤ ℓ) (hu : List.length u = d) : Cost.encode (Sampler.Query.factor w j u) ∈ queries d ℓ

def MIPRE.CL.FixedSampler.answer {d ℓ : ℕ} (P : Player → CLFun 𝔽₂ (Fin d) ℓ) : Sampler.Query → Cost.Data

Equations

• MIPRE.CL.FixedSampler.answer P MIPRE.CL.Sampler.Query.dimension = MIPRE.Cost.encode d
• MIPRE.CL.FixedSampler.answer P (MIPRE.CL.Sampler.Query.marginal w j z) = MIPRE.Cost.encode (MIPRE.CL.toBits ((MIPRE.CL.CLFun.truncate j (P w)).eval (MIPRE.CL.ofBits d z)))
• MIPRE.CL.FixedSampler.answer P (MIPRE.CL.Sampler.Query.linear w j u y) = MIPRE.Cost.encode (MIPRE.CL.toBits (((P w).mapOfPrefix (j - 1) (MIPRE.CL.ofBits d u)) (MIPRE.CL.ofBits d y)))
• MIPRE.CL.FixedSampler.answer P (MIPRE.CL.Sampler.Query.factor w j u) = MIPRE.Cost.encode (MIPRE.CL.indicatorBits ((P w).factorOfPrefix (j - 1) (MIPRE.CL.ofBits d u)))

noncomputable def MIPRE.CL.FixedSampler.table {d ℓ : ℕ} (P : Player → CLFun 𝔽₂ (Fin d) ℓ) : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

theorem MIPRE.CL.FixedSampler.table_correct {d ℓ : ℕ} (P : Player → CLFun 𝔽₂ (Fin d) ℓ) (q : Sampler.Query) (hq : Cost.encode q ∈ queries d ℓ) : (table P).toFun (Cost.encode q) = answer P q

noncomputable def MIPRE.CL.FixedSampler.prog {d ℓ : ℕ} (P : Player → CLFun 𝔽₂ (Fin d) ℓ) : Cost.Prog

Drop the index without traversing it and run the finite query table.

Equations

• MIPRE.CL.FixedSampler.prog P = MIPRE.Cost.Prog.sndProg.let_ (MIPRE.CL.FixedSampler.table P).code

theorem MIPRE.CL.FixedSampler.prog_closed {d ℓ : ℕ} (P : Player → CLFun 𝔽₂ (Fin d) ℓ) : Cost.Prog.WellScoped 1 (prog P)

theorem MIPRE.CL.FixedSampler.prog_runs {d ℓ : ℕ} (P : Player → CLFun 𝔽₂ (Fin d) ℓ) (n : ℕ) (q : Sampler.Query) (hq : Cost.encode q ∈ queries d ℓ) : ∃ (time : ℕ), (prog P).Runs (Cost.encode (n, q)) (answer P q) time

noncomputable def MIPRE.CL.FixedSampler.sampler {d ℓ : ℕ} (P : Player → CLFun 𝔽₂ (Fin d) ℓ) (hP : ∀ (w : Player), (P w).ExactlyOn Finset.univ) : Sampler ℓ

Equations

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

theorem MIPRE.CL.FixedSampler.sampler_timeBound {d ℓ : ℕ} (P : Player → CLFun 𝔽₂ (Fin d) ℓ) (hP : ∀ (w : Player), (P w).ExactlyOn Finset.univ) : ∃ (B : ℕ) (k : ℕ), (sampler P hP).TimeBound (fun (x : ℕ) => B) k

A single polynomial bounds every index, because the program never traverses the index. Its coefficients depend on the fixed finite presentation.

noncomputable def MIPRE.CL.Graph.numberedPresentation {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Player) : CLFun 𝔽₂ (Fin (Fintype.card (Coord T))) 2

Numbering the four finite graph blocks in the standard sampler interface.

Equations

• MIPRE.CL.Graph.numberedPresentation E w = MIPRE.CL.CLFun.embed (Fintype.equivFin (MIPRE.CL.Graph.Coord T)).toEmbedding (MIPRE.CL.Graph.presentation E w.toBool)

theorem MIPRE.CL.Graph.numberedPresentation_exactlyOn {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Player) : (numberedPresentation E w).ExactlyOn Finset.univ

noncomputable def MIPRE.CL.Graph.sampler {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] : Sampler 2

The fixed graph sampler is an actual total program with all four query clauses.

Equations

• MIPRE.CL.Graph.sampler E = MIPRE.CL.FixedSampler.sampler (MIPRE.CL.Graph.numberedPresentation E) ⋯

theorem MIPRE.CL.Graph.sampler_dim {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (n : ℕ) : (sampler E).dim n = 4 * Fintype.card T

theorem MIPRE.CL.Graph.sampler_timeBound {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] : ∃ (B : ℕ) (k : ℕ), (sampler E).TimeBound (fun (x : ℕ) => B) k