The concrete auxiliary introspection checks

These are the finite predicates in the sampling, hiding and original-game tests. They operate on parsed answers. Byte parsing, the global length checks, and clocked calls to the original programs are separate machine obligations. In particular, prefixes are read from a claimed output without applying its CL map again, and both tail projections in a hiding edge use the later answer.

def MIPRE.Introspection.CLChecks.prefixRegister {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} : CL.CLFun F ι ℓ → ℕ → (ι → F) → Finset ι

Registers visited while reading the first k components of a claimed output.

Equations

• MIPRE.Introspection.CLChecks.prefixRegister x✝¹ 0 x✝ = ∅
• MIPRE.Introspection.CLChecks.prefixRegister MIPRE.CL.CLFun.zero n.succ x✝ = ∅
• MIPRE.Introspection.CLChecks.prefixRegister (MIPRE.CL.CLFun.cons S L₁ next) k.succ x✝ = S ∪ MIPRE.Introspection.CLChecks.prefixRegister (next ((MIPRE.CL.proj S) x✝)) k ((MIPRE.CL.proj Sᶜ) x✝)

def MIPRE.Introspection.CLChecks.dualReadout {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} : CL.CLFun F ι ℓ → ℕ → (ι → F) → (ι → F) → ι → F

The dual linear readout at a selected stage, in its actual local coordinates.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.CLChecks.dualReadout MIPRE.CL.CLFun.zero x✝² x✝¹ x✝ = 0
• MIPRE.Introspection.CLChecks.dualReadout (MIPRE.CL.CLFun.cons S L₁ next) k.succ x✝¹ x✝ = MIPRE.Introspection.CLChecks.dualReadout (next ((MIPRE.CL.proj S) x✝¹)) k ((MIPRE.CL.proj Sᶜ) x✝¹) x✝

theorem MIPRE.Introspection.CLChecks.prefixRegister_subset {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) : prefixRegister P k y ⊆ T

Even an arbitrary claimed output selects registers inside the presentation's support.

theorem MIPRE.Introspection.CLChecks.proj_prefixRegister {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) : (CL.proj (prefixRegister P k y)) y = P.outputPrefix k y

Claimed-output prefix extraction is exactly projection onto the selected registers.

theorem MIPRE.Introspection.CLChecks.prefixRegister_full {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.ExactlyOn T) (y : ι → F) : prefixRegister P ℓ y = T

Every full-length claimed output selects the full partition, including nonimage outputs.

def MIPRE.Introspection.CLChecks.sampling {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (u v : (ι → F) × A) : Prop

The sampling-introspection check retains the original answer as well as the question.

Equations

• MIPRE.Introspection.CLChecks.sampling P u v = (u.1 = P.eval v.1 ∧ u.2 = v.2)

def MIPRE.Introspection.CLChecks.reading {F : Type u_1} {ι : Type u_2} {A : Type u_3} (u : (ι → F) × A) (v : (ι → F) × (ι → F) × A) : Prop

The reading-introspection check forgets only the dual readout.

Equations

• MIPRE.Introspection.CLChecks.reading u v = (u.1 = v.1 ∧ u.2 = v.2.2)

def MIPRE.Introspection.CLChecks.hidingRead {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (u : (ι → F) × (ι → F) × (ι → F)) (v : (ι → F) × (ι → F) × A) : Prop

The last hiding measurement and Read agree on the earlier question and full dual answer.

Equations

• MIPRE.Introspection.CLChecks.hidingRead P u v = (P.outputPrefix (ℓ - 1) u.1 = P.outputPrefix (ℓ - 1) v.1 ∧ u.2.1 = v.2.1)

def MIPRE.Introspection.CLChecks.hidingNext {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (u v : (ι → F) × (ι → F) × (ι → F)) : Prop

The four comparisons on the edge from hiding level k+1 to k+2. The later player's question fixes both tail projections and the new dual map.

Equations

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

def MIPRE.Introspection.CLChecks.hidingPauli {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) (v : (ι → F) × (ι → F) × (ι → F)) : Prop

The first hiding edge compares with the Pauli-X answer on the original register.

Equations

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

theorem MIPRE.Introspection.CLChecks.sampling_prefix {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} (hP : P.SupportedOn Finset.univ) {u v : (ι → F) × A} (h : sampling P u v) (k : ℕ) : (P.outputPrefix k u.1, u.2) = ((CL.CLFun.truncate k P).eval v.1, v.2)

Acceptance of the full sampling check implies every prefix comparison, including outcomes outside the honest image on the introspecting side.

theorem MIPRE.Introspection.CLChecks.hidingPauli_coarse {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {x : ι → F} {v : (ι → F) × (ι → F) × (ι → F)} (h : hidingPauli P x v) : ((CL.proj (P.factorOfPrefix 0 0)) v.2.1, (CL.proj (P.factorOfPrefix 0 0)ᶜ) v.2.2) = (dualReadout P 0 0 x, (CL.proj (P.factorOfPrefix 0 0)ᶜ) x)

The first hiding marginal is exactly the tested coarsening of the Pauli-X answer.

theorem MIPRE.Introspection.CLChecks.hidingNext_coarse {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {k : ℕ} {u v : (ι → F) × (ι → F) × (ι → F)} (h : hidingNext P k u v) : (P.outputPrefix k u.1, (CL.proj (prefixRegister P (k + 1) v.1)) u.2.1, (CL.proj (prefixRegister P (k + 2) v.1)ᶜ) u.2.2) = (P.outputPrefix k v.1, (CL.proj (prefixRegister P (k + 1) v.1)) v.2.1, (CL.proj (prefixRegister P (k + 2) v.1)ᶜ) v.2.2)

The checked adjacent hiding answers share their coarse prefix/dual/tail data.