The actual typed introspection sampler

An executable three-level Pauli sampler extends to the complete introspection type set. Pauli presentations are retained, and every auxiliary type uses the zero presentation with a full first factor. The program satisfies every query clause and halts on arbitrary encoded inputs.

theorem MIPRE.Introspection.pad_length (b : Bool) {l : Cost.BitStr} {s : ℕ} (h : List.length l = s) : CL.Detyping.Program.pad b l = List.replicate s b

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

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

noncomputable def MIPRE.Introspection.typedSampler {P : Type u_1} [Cost.SizedEncoding P] (ℓ : ℕ) (S : CL.TypedSampler 3 P) : CL.TypedSampler 3 (QuestionType P ℓ)

The typed introspection sampler, constructed from the executable Pauli sampler.

Equations

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

theorem MIPRE.Introspection.typedSampler_dim {P : Type u_1} [Cost.SizedEncoding P] (ℓ : ℕ) (S : CL.TypedSampler 3 P) (n : ℕ) : (typedSampler ℓ S).dim n = S.dim n

theorem MIPRE.Introspection.typedSampler_cl {P : Type u_1} [Cost.SizedEncoding P] (ℓ : ℕ) (S : CL.TypedSampler 3 P) (n : ℕ) (w : Player) : (typedSampler ℓ S).cl n w = TypedPresentation.family (S.cl n w)

theorem MIPRE.Introspection.typedSampler_prog_independent {P : Type u_1} [Cost.SizedEncoding P] (ℓ ℓ' : ℕ) (S : CL.TypedSampler 3 P) : (typedSampler ℓ S).prog = (typedSampler ℓ' S).prog

The executable extension does not depend on the number of hiding types.

noncomputable def MIPRE.Introspection.detypedSampler {P : Type u_1} [Cost.SizedEncoding P] [Fintype P] [DecidableEq P] (E : P → P → Bool) (X Z : P) (ℓ : ℕ) (S : CL.TypedSampler 3 P) : CL.Sampler 5

The executable five-level introspection sampler after graph detyping.

Equations

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

theorem MIPRE.Introspection.detypedSampler_dim {P : Type u_1} [Cost.SizedEncoding P] [Fintype P] [DecidableEq P] (E : P → P → Bool) (X Z : P) (ℓ : ℕ) (S : CL.TypedSampler 3 P) (n : ℕ) : (detypedSampler E X Z ℓ S).dim n = 4 * (Fintype.card P + 2 * ℓ + 6) + S.dim n

theorem MIPRE.Introspection.detypedSampler_cl {P : Type u_1} [Cost.SizedEncoding P] [Fintype P] [DecidableEq P] (E : P → P → Bool) (X Z : P) (ℓ : ℕ) (S : CL.TypedSampler 3 P) (n : ℕ) (w : Player) : (detypedSampler E X Z ℓ S).cl n w = CL.Detyping.numbered (TypeGraph.Adj E X Z) w (TypedPresentation.family (S.cl n w))

The final sampler's presentations are exactly the detyped typed family.