Explicit NW reconstruction programs -- definitions

The earlier reconstruction predictor was written using the hard function to construct its predecessor tables. This module materializes those finite tables as fields of a reconstruction program. Evaluation of the resulting program uses only its stored data, the fixed statistical test, and the challenge.

structure Complexity.NWDesign.ReconstructionProgram {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) : Type

Self-contained finite data used by an oriented NW reconstruction predictor. The predecessor tables are stored explicitly for precisely the coordinates earlier than current.

• complement : Bool

  Whether the fixed statistical test is complemented.

• current : Fin outputLength

  Hybrid coordinate whose hard-function value is predicted.

• predecessor (previous : ↥(Finset.Iio self.current)) : (↥(design.challengeOverlap self.current ↑previous) → Bool) → Bool

  Hardwired truth tables for all earlier NW output coordinates.

• outside : ↥(design.outsideCoordinates self.current) → Bool

  Seed bits outside the challenged design block.

• later : ↥(laterCoordinates self.current) → Bool

  Fixed NW output bits later than the challenged coordinate.

• candidate : Bool

  Candidate value supplied at the challenged coordinate.

def Complexity.NWDesign.materializeReconstructionProgram {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (complement : Bool) (current : Fin outputLength) (advice : design.ReconstructionAdvice current) : design.ReconstructionProgram

Materialize all predecessor tables used by a fixed-advice reconstruction predictor. After this construction, evaluation no longer queries hardFunction.

Equations

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

def Complexity.NWDesign.ReconstructionCertificate.toProgram {outputLength inputLength seedLength : ℕ} (certificate : ReconstructionCertificate outputLength seedLength) (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) : design.ReconstructionProgram

Materialize the explicit reconstruction program named by a checked certificate.

Equations

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

def Complexity.NWDesign.ReconstructionProgram.query {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) (challenge : Fin inputLength → Bool) : Fin outputLength → Bool

Output query assembled entirely from an explicit reconstruction program.

Equations

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

def Complexity.NWDesign.ReconstructionProgram.testAtCandidate {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) (test : Finset (Fin outputLength → Bool)) (challenge : Fin inputLength → Bool) : Bool

Evaluate the oriented fixed statistical test on an explicit program's query.

Equations

• program.testAtCandidate test challenge = decide (program.query challenge ∈ Complexity.BitGenerator.orientTest test program.complement)

def Complexity.NWDesign.ReconstructionProgram.predictor {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) (test : Finset (Fin outputLength → Bool)) : (Fin inputLength → Bool) → Bool

Boolean predictor evaluated solely from the stored program and fixed statistical test.

Equations

• program.predictor test challenge = Complexity.NextBitPrediction.predictFromTest (program.testAtCandidate test challenge) program.candidate

def Complexity.NWDesign.ReconstructionProgram.agreementProbability {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) : ℚ

Exact uniform agreement of an explicit program with a target hard function. The target is used only to score the stored predictor.

Equations

• program.agreementProbability hardFunction test = Complexity.uniformProbability {challenge : Fin inputLength → Bool | program.predictor test challenge = hardFunction challenge}

def Complexity.NWDesign.ReconstructionProgram.booleanPayloadSize {outputLength inputLength seedLength : ℕ} {design : NWDesign outputLength inputLength seedLength} (program : design.ReconstructionProgram) : ℕ

Number of Boolean payload entries stored by a reconstruction program. The polarity and coordinate are metadata handled by the later codec layer.

Equations

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