Canonical encodings of Nisan--Wigderson designs -- definitions

Every coordinate of every ordered design block is encoded in the canonical clog_2(seedLength)-bit Fin representation. A fixed lexicographic order on output coordinate, input coordinate, and bit position turns the entire design into one flat bit string.

@[reducible, inline]

abbrev Complexity.NWDesign.CoordinateBitIndex (outputLength inputLength seedLength : ℕ) : Type

Index of one bit in the complete coordinate table of an NW design.

Equations

• Complexity.NWDesign.CoordinateBitIndex outputLength inputLength seedLength = ((Fin outputLength × Fin inputLength) × Fin (Fin.bitWidth seedLength))

def Complexity.NWDesign.coordinateBitIndexEquiv (outputLength inputLength seedLength : ℕ) : CoordinateBitIndex outputLength inputLength seedLength ≃ Fin (outputLength * inputLength * Fin.bitWidth seedLength)

Row-major equivalence between coordinate-bit table indices and flat bit positions.

Equations

• Complexity.NWDesign.coordinateBitIndexEquiv outputLength inputLength seedLength = (finProdFinEquiv.prodCongr (Equiv.refl (Fin (Fin.bitWidth seedLength)))).trans finProdFinEquiv

def Complexity.NWDesign.coordinateBitTable {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) : CoordinateBitIndex outputLength inputLength seedLength → Bool

Boolean table underlying the canonical NW-design encoding.

Equations

• design.coordinateBitTable ((output, input), bit) = ((design.coordinates output) input).toBits.get ⟨↑bit, ⋯⟩

def Complexity.NWDesign.encode {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) : List Bool

Canonical flat encoding of every coordinate in every ordered design block.

Equations

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

def Complexity.NWDesign.decodeCoordinate? (outputLength inputLength seedLength : ℕ) (bits : List Bool) (output : Fin outputLength) (input : Fin inputLength) : Option (Fin seedLength)

Decode the fixed-width coordinate at one output/input position of an encoded design. A malformed total length or an out-of-range coordinate is rejected.

Equations

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

def Complexity.NWDesign.decodedCoordinates (outputLength inputLength seedLength : ℕ) (bits : List Bool) (hvalid : ∀ (output : Fin outputLength) (input : Fin inputLength), (decodeCoordinate? outputLength inputLength seedLength bits output input).isSome = true) : Fin outputLength → Fin inputLength → Fin seedLength

Total coordinate table extracted from bits whose every coordinate decodes. The proof is erased from executable code.

Equations

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

def Complexity.NWDesign.decode? (outputLength inputLength seedLength : ℕ) (bits : List Bool) : Option (NWDesign outputLength inputLength seedLength)

Decode a canonical NW-design bit string. Besides length and coordinate-range checks, this rejects any block whose decoded coordinate map is not injective.

Equations

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

structure Complexity.NWDesign.DecoderInstance : Type

All numeric parameters and the design needed by one uniform NW decoder invocation. Recording inputLength explicitly lets a parser recover the raw coordinate-table dimensions without evaluating a code-family function.

• messageLength : ℕ

  Source-message length used by the list-code family.

• inverseAccuracy : ℕ

  Inverse list-decoding accuracy.

• outputLength : ℕ

  Number of NW output coordinates.

• inputLength : ℕ

  Number of seed coordinates read by each design block.

• seedLength : ℕ

  Total NW seed length.

• design : NWDesign self.outputLength self.inputLength self.seedLength

  The parameterized NW design.

def Complexity.NWDesign.DecoderInstance.encode (data : DecoderInstance) : List Bool

Canonical self-describing encoding of a uniform-decoder instance. Five framed minimal binary naturals precede the fixed-width design table.

Equations

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

def Complexity.NWDesign.DecoderInstance.decode? (bits : List Bool) : Option DecoderInstance

Parse a self-describing uniform-decoder instance, rejecting noncanonical natural codes, malformed pair boundaries, and invalid design tables.

Equations

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

def Complexity.NWDesign.decoderInstance {outputLength inputLength seedLength : ℕ} (messageLength inverseAccuracy : ℕ) (design : NWDesign outputLength inputLength seedLength) : DecoderInstance

Package a design with the two list-code parameters needed by a uniform decoder.

Equations

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