Documentation

MIPRE.Foundations.Introspection.AuxiliaryScanStage

One executable Gaussian stage of the hiding prefix scan #

The stage queries the next register and its matrix, solves for the claimed component, checks the solution by matrix multiplication, and replaces exactly that register in the seed witness. The returned prefix is the old prefix plus the claimed new component. Every operation has an ambient polynomial bound.

source
@[reducible, inline]
abbrev MIPRE.Introspection.AuxiliaryScan.StageInput :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev MIPRE.Introspection.AuxiliaryScan.State :
    Type
    Equations
    Instances For
      source
      noncomputable def MIPRE.Introspection.AuxiliaryScan.context :
      Cost.PolyTimeFun StageInput AuxiliarySource.Context
      Equations
      Instances For
        source
        noncomputable def MIPRE.Introspection.AuxiliaryScan.claimed :
        Cost.PolyTimeFun StageInput Cost.BitStr
        Equations
        Instances For
          source
          noncomputable def MIPRE.Introspection.AuxiliaryScan.seed :
          Cost.PolyTimeFun StageInput Cost.BitStr
          Equations
          Instances For
            source
            noncomputable def MIPRE.Introspection.AuxiliaryScan.oldPrefix :
            Cost.PolyTimeFun StageInput Cost.BitStr
            Equations
            Instances For
              source
              noncomputable def MIPRE.Introspection.AuxiliaryScan.stageMask (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) :
              Cost.PolyTimeFun StageInput Cost.BitStr
              Equations
              Instances For
                source
                noncomputable def MIPRE.Introspection.AuxiliaryScan.stageMatrix (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) :
                Cost.PolyTimeFun StageInput (List Cost.BitStr)
                Equations
                Instances For
                  source
                  noncomputable def MIPRE.Introspection.AuxiliaryScan.target (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) :
                  Cost.PolyTimeFun StageInput Cost.BitStr
                  Equations
                  Instances For
                    source
                    noncomputable def MIPRE.Introspection.AuxiliaryScan.solution (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) :
                    Cost.PolyTimeFun StageInput Cost.BitStr
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def MIPRE.Introspection.AuxiliaryScan.stage (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) :
                      Cost.PolyTimeFun StageInput State
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem MIPRE.Introspection.AuxiliaryScan.stage_correct (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {n : ℕ} (S : Finset (Fin n)) (L : (Fin n → CL.𝔽₂) →ₗ[CL.𝔽₂] Fin n → CL.𝔽₂) (u y x : Fin n → CL.𝔽₂) (hu : AuxiliarySource.inputPrefix.toFun ctx = CL.toBits u) (hS : f.toFun ctx = CL.indicatorBits S) (hL : m.toFun ctx = LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' L)) :
                        (stage f m).toFun (ctx, CL.toBits y, CL.toBits x) = have v := (CL.proj S) y; have z := AuxiliaryPrefix.solveStage L v; (decide (L z = v), CL.toBits (u + v), CL.toBits ((CL.proj Sᶜ) x + (CL.proj S) z))