Circuit predicates for anti-checker hash cells -- definitions

For fixed anti-checker parameters and one hash range width, a predicate circuit reads the packed labeled samples and affine seed as a public prefix, followed by one existential powered-survivor witness. Its canonical serialized code and a zero ruler form a query to CircuitSAT.extensionLanguage.

@[reducible]

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.counterSurvivorPowerWidth (beta : PositiveRationalScale) (arity : ℕ) : ℕ

Width of the powered survivor tuple quantified by one occupancy query.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellPublicWidth (beta : PositiveRationalScale) (arity prefixLength rangeWidth : ℕ) : ℕ

Width of the public labeled-sample and affine-seed prefix for one hash-cell query.

Equations

• One or more equations did not get rendered due to their size.

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatHashCellPublicWidth (beta : PositiveRationalScale) (arity prefixLength rangeWidth : ℕ) : NeZero (hashCellPublicWidth beta arity prefixLength rangeWidth)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellPredicateInputWidth (beta : PositiveRationalScale) (arity prefixLength rangeWidth : ℕ) : ℕ

Total input width of a hash-cell predicate circuit: public query bits followed by the existential survivor tuple.

Equations

• One or more equations did not get rendered due to their size.

instance Complexity.GapMCSP.Magnification.AntiCheckerLemma.instNeZeroNatHashCellPredicateInputWidth (beta : PositiveRationalScale) (arity prefixLength rangeWidth : ℕ) : NeZero (hashCellPredicateInputWidth beta arity prefixLength rangeWidth)

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellPublicInput {arity prefixLength rangeWidth : ℕ} (beta : PositiveRationalScale) (input : BitString (counterInputWidth arity prefixLength)) (seed : BitString (PairwiseIndependentHash.affineSeedWidth (counterSurvivorPowerWidth beta arity) rangeWidth)) : BitString (hashCellPublicWidth beta arity prefixLength rangeWidth)

Pack labeled samples and one affine seed into the public prefix of a hash-cell predicate.

Equations

• Complexity.GapMCSP.Magnification.AntiCheckerLemma.hashCellPublicInput beta input seed = Fin.append input seed

structure Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit (beta : PositiveRationalScale) (arity prefixLength rangeWidth : ℕ) : Type

A single-output circuit deciding the exact powered-survivor hash-cell witness predicate from a public sample/seed prefix and an existential tuple.

• internalGates : ℕ

  Number of internal gates in the predicate circuit.

• circuit : Circuit Basis.andOr2 (hashCellPredicateInputWidth beta arity prefixLength rangeWidth) 1 self.internalGates

  The fixed predicate circuit for these anti-checker parameters.

• implements (input : BitString (counterInputWidth arity prefixLength)) (seed : BitString (PairwiseIndependentHash.affineSeedWidth (counterSurvivorPowerWidth beta arity) rangeWidth)) (witness : Fin (counterSurvivorPowerWidth beta arity) → Bool) : self.circuit.eval (Fin.append (hashCellPublicInput beta input seed) witness) 0 = decide (HashCellWitness arity (smallThreshold beta arity) (roundPrecision arity) rangeWidth input seed witness)

  Exact agreement with the semantic hash-cell witness relation.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.code {beta : PositiveRationalScale} {arity prefixLength rangeWidth : ℕ} (predicate : HashCellPredicateCircuit beta arity prefixLength rangeWidth) : List Bool

Tagged serialized code of the positive-input predicate circuit.

Equations

• predicate.code = true :: Complexity.CircuitCode.encodeCircuit predicate.circuit

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.ruler (beta : PositiveRationalScale) (arity : ℕ) : List Bool

The exact-width zero ruler for the existential powered-survivor tuple.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellPredicateCircuit.query {beta : PositiveRationalScale} {arity prefixLength rangeWidth : ℕ} (predicate : HashCellPredicateCircuit beta arity prefixLength rangeWidth) (input : BitString (counterInputWidth arity prefixLength)) (seed : BitString (PairwiseIndependentHash.affineSeedWidth (counterSurvivorPowerWidth beta arity) rangeWidth)) : List Bool

Canonical fixed-prefix circuit-satisfiability query for one sample input and affine hash seed.

Equations

• One or more equations did not get rendered due to their size.