A uniform serialized Lyubashevsky extractor

The extractor needs only runtime dimensions m,k, two bit challenges and two optional integer responses. It computes the response difference followed by the signed reversed challenge difference. Dimensions are unary resources; integer magnitudes are binary. Every input word has a total interpretation: missing vector entries are zero, missing challenge bits are false, and surplus coordinates are ignored. The optional-vector default is the zero vector.

The same word program handles all dimensions; no parameter-family claim is inferred from a certificate for one fixed finite vector type. This is a deterministic operation certificate, not a rewinding, knowledge-soundness or cryptographic security theorem.

Main definitions

• Cslib.Crypto.Protocols.SigmaProtocol.LyubashevskyExtractInput: the fixed runtime input type.
• Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractList: the native integer output.
• Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractWord: the complete word program.

Main results

• Cslib.Crypto.Protocols.SigmaProtocol.computableInPolyTime_lyubashevskyExtractWord: all parsing, arithmetic, framing and output costs in one uniform plain certificate.
• Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractWord_eq_extract: exact agreement with the typed protocol extractor for all dimensions, statements and commitments.

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.SigmaProtocol.LyubashevskyExtractInput : Type

Dimensions followed by two challenge/optional-response pairs.

def Cslib.Crypto.Protocols.SigmaProtocol.encLyubashevskyExtractInput : LyubashevskyExtractInput ↪ List Bool

Unary dimensions, raw challenges and framed optional lists of binary signed integers.

def Cslib.Crypto.Protocols.SigmaProtocol.decodeLyubashevskyExtractInput (word : List Bool) : LyubashevskyExtractInput

Parse every input word with the existing framing conventions; malformed fields have total zero/default interpretations.

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.decodeLyubashevskyExtractInput_enc (input : LyubashevskyExtractInput) : decodeLyubashevskyExtractInput (encLyubashevskyExtractInput input) = input

Parsing inverts the complete canonical input encoding.

theorem Cslib.Crypto.Protocols.SigmaProtocol.computableInPolyTime_decodeLyubashevskyExtractInput : Turing.MultiTapeTM.ComputableInPolyTime decodeLyubashevskyExtractInput Turing.MultiTapeTM.encBits encLyubashevskyExtractInput

The total input parser has a plain polynomial-time certificate, including malformed words.

def Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractList (input : LyubashevskyExtractInput) : List ℤ

Compute z-z′ first, then the SIGNED challenge difference c′-c. The unary dimensions control both output segments; optional responses default to zero coordinatewise.

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.length_lyubashevskyExtractList (input : LyubashevskyExtractInput) : (lyubashevskyExtractList input).length = input.1.1 + input.1.2

Extraction always writes the two declared segments, even on malformed-length inputs.

theorem Cslib.Crypto.Protocols.SigmaProtocol.computableInPolyTime_lyubashevskyExtractList : Turing.MultiTapeTM.ComputableInPolyTime lyubashevskyExtractList encLyubashevskyExtractInput (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

One native extractor handles runtime dimensions and all binary integer magnitudes.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractList_ofFn {m k : ℕ} (c : Fin k → Bool) (z : Option (Fin m → ℤ)) (c' : Fin k → Bool) (z' : Option (Fin m → ℤ)) : lyubashevskyExtractList ((m, k), (List.ofFn c, Option.map List.ofFn z), List.ofFn c', Option.map List.ofFn z') = List.ofFn (Fin.append (fun (i : Fin m) => z.getD 0 i - z'.getD 0 i) fun (i : Fin k) => (if c' i = true then 1 else 0) - if c i = true then 1 else 0)

Canonical typed vectors give exactly the ordered response difference and signed reversed challenge difference. This formula is independent of statement matrices and the modulus.

def Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractWord (word : List Bool) : List Bool

The complete serialized program: parse, extract, and frame every signed output coordinate.

theorem Cslib.Crypto.Protocols.SigmaProtocol.computableInPolyTime_lyubashevskyExtractWord : Turing.MultiTapeTM.ComputableInPolyTime lyubashevskyExtractWord Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits

The complete extractor is one plain polynomial-time word function, not a separate machine for each fixed dimension.

@[simp]

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractWord_enc (input : LyubashevskyExtractInput) : lyubashevskyExtractWord (encLyubashevskyExtractInput input) = (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) (lyubashevskyExtractList input)

The word program exactly implements the integer-list extractor on canonical encoded data.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractList_eq_extract (n m k q : ℕ) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) (w : Fin n → ZMod q) (c : BitString k) (z : Option (Fin m → ℤ)) (c' : BitString k) (z' : Option (Fin m → ℤ)) : lyubashevskyExtractList ((m, k), (List.ofFn c, Option.map List.ofFn z), List.ofFn c', Option.map List.ofFn z') = List.ofFn fun (i : Fin (m + k)) => lyubashevskyExtract n m k q y w c z c' z' (finSumFinEquiv.symm i)

Canonical vectors realize the actual typed extractor for every statement and commitment. The ignored statement dimensions and modulus do not need to be supplied to the word program.

theorem Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractWord_eq_extract (n m k q : ℕ) (y : Matrix (Fin n) (Fin m) (ZMod q) × Matrix (Fin n) (Fin k) (ZMod q)) (w : Fin n → ZMod q) (c : BitString k) (z : Option (Fin m → ℤ)) (c' : BitString k) (z' : Option (Fin m → ℤ)) : lyubashevskyExtractWord (encLyubashevskyExtractInput ((m, k), (List.ofFn c, Option.map List.ofFn z), List.ofFn c', Option.map List.ofFn z')) = (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) (List.ofFn fun (i : Fin (m + k)) => lyubashevskyExtract n m k q y w c z c' z' (finSumFinEquiv.symm i))

The complete word program agrees exactly with the named typed extractor, including absent responses and zero dimensions, without assuming acceptance of either conversation.