Documentation

MIPRE.Foundations.Introspection.AuxiliaryHidingNextProgram

The complete executable interior hiding edge #

Only the prefixes needed by the edge are scanned. On successful scans, all factor and matrix queries are legal and the core inputs are exact. Acceptance is precisely prefix attainability together with the quotient hiding predicate.

source
@[reducible, inline]
abbrev MIPRE.Introspection.AuxiliaryHiding.Input :
Type
Equations
Instances For
    source
    noncomputable def MIPRE.Introspection.AuxiliaryHiding.sourceContext :
    Cost.PolyTimeFun Input AuxiliarySource.Context
    Equations
    Instances For
      source
      noncomputable def MIPRE.Introspection.AuxiliaryHiding.leftAnswer :
      Cost.PolyTimeFun Input Triple
      Equations
      Instances For
        source
        noncomputable def MIPRE.Introspection.AuxiliaryHiding.rightAnswer :
        Cost.PolyTimeFun Input Triple
        Equations
        Instances For
          source
          noncomputable def MIPRE.Introspection.AuxiliaryHiding.leftInput :
          Cost.PolyTimeFun Input AuxiliaryScan.Input
          Equations
          Instances For
            source
            noncomputable def MIPRE.Introspection.AuxiliaryHiding.rightInput :
            Cost.PolyTimeFun Input AuxiliaryScan.Input
            Equations
            Instances For
              source
              noncomputable def MIPRE.Introspection.AuxiliaryHiding.leftScan (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (k : ℕ) :
              Cost.PolyTimeFun Input AuxiliaryScan.State
              Equations
              Instances For
                source
                noncomputable def MIPRE.Introspection.AuxiliaryHiding.rightScan (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (k : ℕ) :
                Cost.PolyTimeFun Input AuxiliaryScan.State
                Equations
                Instances For
                  source
                  noncomputable def MIPRE.Introspection.AuxiliaryHiding.prepare (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (k : ℕ) :
                  Cost.PolyTimeFun Input CoreInput
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def MIPRE.Introspection.AuxiliaryHiding.check (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (k : ℕ) :
                    Cost.PolyTimeFun Input Bool
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem MIPRE.Introspection.AuxiliaryHiding.prepare_correct (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {n ℓ : ℕ} {P : CL.CLFun CL.𝔽₂ (Fin n) ℓ} {T : Finset (Fin n)} (hP : P.SupportedOn T) (k : ℕ) (y yp x z zp t : Fin n → CL.𝔽₂) (hq : ∀ j ≤ k + 1, AuxiliaryScan.QueriesCorrectAt f m ctx P j) (hy : ∃ (a : Fin n → CL.𝔽₂), (CL.CLFun.truncate k P).eval a = P.outputPrefix k y) (hz : ∃ (a : Fin n → CL.𝔽₂), (CL.CLFun.truncate (k + 1) P).eval a = P.outputPrefix (k + 1) z) :
                      (prepare f m k).toFun (ctx, (CL.toBits y, CL.toBits yp, CL.toBits x), CL.toBits z, CL.toBits zp, CL.toBits t) = ((CL.toBits (P.outputPrefix k y), CL.toBits (P.outputPrefix k z)), ((CL.toBits y, CL.toBits yp, CL.toBits x), CL.toBits z, CL.toBits zp, CL.toBits t), CL.indicatorBits (CLChecks.prefixRegister P (k + 1) z), CL.indicatorBits (CLChecks.prefixRegister P (k + 2) z), CL.indicatorBits (P.factorOfPrefix (k + 1) z), LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' (P.mapOfPrefix (k + 1) z)))
                      source
                      theorem MIPRE.Introspection.AuxiliaryHiding.check_correct (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {n ℓ : ℕ} {P : CL.CLFun CL.𝔽₂ (Fin n) ℓ} {T : Finset (Fin n)} (hP : P.SupportedOn T) (k : ℕ) (y yp x z zp t : Fin n → CL.𝔽₂) (hq : ∀ j ≤ k + 1, AuxiliaryScan.QueriesCorrectAt f m ctx P j) :
                      (check f m k).toFun (ctx, (CL.toBits y, CL.toBits yp, CL.toBits x), CL.toBits z, CL.toBits zp, CL.toBits t) = true ↔ (∃ (a : Fin n → CL.𝔽₂), (CL.CLFun.truncate k P).eval a = P.outputPrefix k y) ∧ (∃ (a : Fin n → CL.𝔽₂), (CL.CLFun.truncate (k + 1) P).eval a = P.outputPrefix (k + 1) z) ∧ AuxiliaryQuotient.hidingNext P k (y, yp, x) (z, zp, t)