Nisan--Wigderson fixed-advice reconstruction -- definitions

The finite next-bit experiment initially samples a full NW seed and full output tail. A reconstruction circuit instead fixes only seed coordinates outside the challenge block and tail coordinates after the predicted bit. Earlier generator values are supplied by the overlap-indexed predecessor tables.

def Complexity.NWDesign.outsideCoordinates {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : Finset (Fin seedLength)

Seed coordinates outside the challenged design block.

Equations

• design.outsideCoordinates current = Finset.univ \ design.support current

def Complexity.NWDesign.laterCoordinates {outputLength : ℕ} (current : Fin outputLength) : Finset (Fin outputLength)

Output coordinates strictly after the predicted coordinate.

Equations

• Complexity.NWDesign.laterCoordinates current = Finset.Ioi current

def Complexity.NWDesign.outsideSeed {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) : Fin seedLength → Bool

Extend an assignment to the outside seed coordinates by false before inserting the challenge.

Equations

• design.outsideSeed current outside = Complexity.BooleanDependency.extendByFalse (design.outsideCoordinates current) outside

def Complexity.NWDesign.reconstructionSeed {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (challenge : Fin inputLength → Bool) : Fin seedLength → Bool

Assemble a full seed from an outside assignment and a challenge on the current design block.

Equations

• design.reconstructionSeed current outside challenge = design.seedWithChallenge current (design.outsideSeed current outside) challenge

def Complexity.NWDesign.laterTail {outputLength : ℕ} (current : Fin outputLength) (later : ↥(laterCoordinates current) → Bool) : Fin outputLength → Bool

Extend later output bits by false at and before the predicted coordinate.

Equations

• Complexity.NWDesign.laterTail current later = Complexity.BooleanDependency.extendByFalse (Complexity.NWDesign.laterCoordinates current) later

def Complexity.NWDesign.reconstructionBackground {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (later : ↥(laterCoordinates current) → Bool) (challenge : Fin inputLength → Bool) : BitGenerator.CandidateBackground seedLength outputLength current

Candidate background assembled from exactly the fixed outside-seed and later-tail assignments, together with a varying challenge.

Equations

• design.reconstructionBackground current outside later challenge = (design.reconstructionSeed current outside challenge, ⟨Complexity.NWDesign.laterTail current later, ⋯⟩)

def Complexity.NWDesign.reconstructionQuery {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (later : ↥(laterCoordinates current) → Bool) (challenge : Fin inputLength → Bool) (candidate : Bool) : Fin outputLength → Bool

Query assembled from hardwired predecessor tables, the independent candidate, and fixed later bits.

Equations

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

def Complexity.NWDesign.reconstructionTestAtCandidate {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (later : ↥(laterCoordinates current) → Bool) (challenge : Fin inputLength → Bool) (candidate : Bool) : Bool

Test evaluation computed from the reconstruction query.

Equations

• design.reconstructionTestAtCandidate hardFunction test current outside later challenge candidate = decide (design.reconstructionQuery hardFunction current outside later challenge candidate ∈ test)

def Complexity.NWDesign.reconstructionPredictor {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (test : Finset (Fin outputLength → Bool)) (current : Fin outputLength) (outside : ↥(design.outsideCoordinates current) → Bool) (later : ↥(laterCoordinates current) → Bool) (candidate : Bool) : (Fin inputLength → Bool) → Bool

The fixed-advice next-bit predictor as a Boolean function of the challenge.

Equations

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

def Complexity.NWDesign.reconstructionDataBitsAt {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : ℕ

Exact non-codec Boolean payload of one fixed reconstruction predictor: predecessor-table entries, later bits, outside seed bits, and the candidate.

Equations

• design.reconstructionDataBitsAt current = design.predecessorTableEntriesAt current + (Complexity.NWDesign.laterCoordinates current).card + (design.outsideCoordinates current).card + 1