Documentation

MIPRE.Foundations.Introspection.AuxiliaryQuotientProgram

The executable coordinate-independent hiding comparison #

source
noncomputable def MIPRE.Introspection.AuxiliaryBits.quotient :
Cost.PolyTimeFun (Cost.BitStr × List Cost.BitStr × Cost.BitStr × Cost.BitStr) Bool

Register mask, queried matrix, and the two full-register labels.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Introspection.AuxiliaryBits.quotient_correct {n : ℕ} (S : Finset (Fin n)) (L : CL.RegLinear CL.𝔽₂ S) (x y : Fin n → CL.𝔽₂) :
    quotient.toFun (CL.indicatorBits S, LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' L.toLinearMap), CL.toBits x, CL.toBits y) = true ↔ (AuxiliaryDual.registerDual L) x = (AuxiliaryDual.registerDual L) y