Documentation

MIPRE.Foundations.Introspection.AuxiliaryHidingCoreProgram

Executable comparisons for an interior hiding edge #

The caller supplies the two extracted prefixes, the two raw triples, the visited-register masks, and the queried next-factor matrix. This core performs the four exact comparisons. The prefix scan separately certifies those inputs.

source
@[reducible, inline]
abbrev MIPRE.Introspection.AuxiliaryHiding.Triple :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev MIPRE.Introspection.AuxiliaryHiding.CoreInput :
    Type
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MIPRE.Introspection.AuxiliaryHiding.prefixes :
      Cost.PolyTimeFun CoreInput (Cost.BitStr × Cost.BitStr)
      Equations
      Instances For
        source
        noncomputable def MIPRE.Introspection.AuxiliaryHiding.answers :
        Cost.PolyTimeFun CoreInput (Triple × Triple)
        Equations
        Instances For
          source
          noncomputable def MIPRE.Introspection.AuxiliaryHiding.masks :
          Cost.PolyTimeFun CoreInput (Cost.BitStr × Cost.BitStr × Cost.BitStr × List Cost.BitStr)
          Equations
          Instances For
            source
            noncomputable def MIPRE.Introspection.AuxiliaryHiding.leftDual :
            Cost.PolyTimeFun CoreInput Cost.BitStr
            Equations
            Instances For
              source
              noncomputable def MIPRE.Introspection.AuxiliaryHiding.rightDual :
              Cost.PolyTimeFun CoreInput Cost.BitStr
              Equations
              Instances For
                source
                noncomputable def MIPRE.Introspection.AuxiliaryHiding.leftTail :
                Cost.PolyTimeFun CoreInput Cost.BitStr
                Equations
                Instances For
                  source
                  noncomputable def MIPRE.Introspection.AuxiliaryHiding.rightTail :
                  Cost.PolyTimeFun CoreInput Cost.BitStr
                  Equations
                  Instances For
                    source
                    noncomputable def MIPRE.Introspection.AuxiliaryHiding.visited :
                    Cost.PolyTimeFun CoreInput Cost.BitStr
                    Equations
                    Instances For
                      source
                      noncomputable def MIPRE.Introspection.AuxiliaryHiding.remaining :
                      Cost.PolyTimeFun CoreInput Cost.BitStr
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def MIPRE.Introspection.AuxiliaryHiding.fresh :
                        Cost.PolyTimeFun CoreInput Cost.BitStr
                        Equations
                        Instances For
                          source
                          noncomputable def MIPRE.Introspection.AuxiliaryHiding.nextMatrix :
                          Cost.PolyTimeFun CoreInput (List Cost.BitStr)
                          Equations
                          Instances For
                            source
                            noncomputable def MIPRE.Introspection.AuxiliaryHiding.core :
                            Cost.PolyTimeFun CoreInput Bool
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              theorem MIPRE.Introspection.AuxiliaryHiding.core_correct {n ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin n) ℓ) (k : ℕ) (y yp x z zp t : Fin n → CL.𝔽₂) :
                              core.toFun ((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))) = true ↔ AuxiliaryQuotient.hidingNext P k (y, yp, x) (z, zp, t)