Documentation

MIPRE.Foundations.Introspection.AuxiliaryDualDecode

Decoding quotient-valued hiding answers #

The executable dual check only compares cosets of a row space. Decode each reported register to the semantic canonical representative. This decoding is used to return soundness to the existing finite game; it is not part of the executable verifier and makes no computability claim about Fintype.equivFin.

source
theorem MIPRE.Introspection.AuxiliaryDual.registerDual_proj {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (x : ι → F) :
(CL.proj S) ((registerDual L) x) = (registerDual L) x
source
theorem MIPRE.Introspection.AuxiliaryDual.registerDual_proj_input {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S U : Finset ι} (L : CL.RegLinear F S) (hSU : S ⊆ U) (x : ι → F) :
(registerDual L) ((CL.proj U) x) = (registerDual L) x
source
noncomputable def MIPRE.Introspection.AuxiliaryDual.stageDual {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) :
(ι → F) →ₗ[F] ι → F

The semantic dual map at a single reported stage.

Equations
Instances For
    source
    theorem MIPRE.Introspection.AuxiliaryDual.stageDual_apply {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y x : ι → F) :
    (stageDual P k y) x = CLChecks.dualReadout P k y x
    source
    theorem MIPRE.Introspection.AuxiliaryDual.stageDual_prefix_congr {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) {y z : ι → F} (h : P.outputPrefix k y = P.outputPrefix k z) :
    stageDual P k y = stageDual P k z
    source
    theorem MIPRE.Introspection.AuxiliaryDual.stageFactors_disjoint {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (y : ι → F) {i j : ℕ} (hij : i < j) :
    Disjoint (P.factorOfPrefix i y) (P.factorOfPrefix j y)

    Selected registers are disjoint even for an unattainable reported output.

    source
    noncomputable def MIPRE.Introspection.AuxiliaryDual.decodeDual {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (y : ι → F) :
    (ι → F) →ₗ[F] ι → F

    Decode all stage labels while preserving the original claimed output.

    Equations
    Instances For
      source
      theorem MIPRE.Introspection.AuxiliaryDual.decodeDual_apply {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (y x : ι → F) :
      (decodeDual P y) x = ∑ j ∈ Finset.range ℓ, (stageDual P j y) x
      source
      theorem MIPRE.Introspection.AuxiliaryDual.proj_decodeDual {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (y x : ι → F) {k : ℕ} (hk : k < ℓ) :
      (CL.proj (P.factorOfPrefix k y)) ((decodeDual P y) x) = (stageDual P k y) x

      Projection of the decoded answer extracts exactly its selected dual block.

      source
      theorem MIPRE.Introspection.AuxiliaryDual.proj_prefix_decodeDual {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (y x : ι → F) {k : ℕ} (hk : k ≤ ℓ) :
      (CL.proj (CLChecks.prefixRegister P k y)) ((decodeDual P y) x) = ∑ j ∈ Finset.range k, (stageDual P j y) x

      On every already visited register the decoder only uses that same raw prefix.

      source
      theorem MIPRE.Introspection.AuxiliaryDual.outputPrefix_congr_le {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) {j k : ℕ} (hjk : j ≤ k) {y z : ι → F} (h : P.outputPrefix k y = P.outputPrefix k z) :
      P.outputPrefix j y = P.outputPrefix j z
      source
      theorem MIPRE.Introspection.AuxiliaryDual.proj_prefix_decodeDual_congr {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) {k : ℕ} (hk : k + 1 ≤ ℓ) {y z a b : ι → F} (hyz : P.outputPrefix k y = P.outputPrefix k z) (hab : (CL.proj (CLChecks.prefixRegister P (k + 1) z)) a = (CL.proj (CLChecks.prefixRegister P (k + 1) z)) b) :
      (CL.proj (CLChecks.prefixRegister P (k + 1) z)) ((decodeDual P y) a) = (CL.proj (CLChecks.prefixRegister P (k + 1) z)) ((decodeDual P z) b)

      Equal raw dual prefixes remain equal after decoding, even when the untested tails of the two claimed questions differ.

      source
      theorem MIPRE.Introspection.AuxiliaryDual.decodeDual_prefix_congr {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) {y z : ι → F} (h : P.outputPrefix (ℓ - 1) y = P.outputPrefix (ℓ - 1) z) :
      decodeDual P y = decodeDual P z

      The prefix preceding the last stage determines the entire dual decoder.