Affine hash-cell circuit fragments -- proof internals #
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellAffineCircuit.length_compileRaw_internal
(beta : PositiveRationalScale)
(arity prefixLength rangeWidth : ℕ)
:
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellAffineCircuit.outputWire_eq_internal
(beta : PositiveRationalScale)
(arity prefixLength rangeWidth : ℕ)
:
outputWire beta arity prefixLength rangeWidth = hashCellPredicateInputWidth beta arity prefixLength rangeWidth + List.length (compileRaw beta arity prefixLength rangeWidth) - 1
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellAffineCircuit.compileRaw_wellFormed_internal
(beta : PositiveRationalScale)
(arity prefixLength rangeWidth : ℕ)
:
CircuitCode.RawCircuit.WellFormed (hashCellPredicateInputWidth beta arity prefixLength rangeWidth)
(compileRaw beta arity prefixLength rangeWidth)
theorem
Complexity.GapMCSP.Magnification.AntiCheckerLemma.HashCellAffineCircuit.eval?_compileRaw_internal
(beta : PositiveRationalScale)
{arity prefixLength rangeWidth : ℕ}
(input : BitString (counterInputWidth arity prefixLength))
(seed : BitString (PairwiseIndependentHash.affineSeedWidth (counterSurvivorPowerWidth beta arity) rangeWidth))
(witness : BitString (counterSurvivorPowerWidth beta arity))
:
(compileRaw beta arity prefixLength rangeWidth).eval?
(BitString.toList (Fin.append (hashCellPublicInput beta input seed) witness)) = some (decide (PairwiseIndependentHash.affineEval seed witness = fun (x : Fin rangeWidth) => false))