From 84f7ade9a0dc27d92e00c0864036f5b8b4e30034 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:21:58 -0400 Subject: [PATCH 1/2] feat(crypto): implement a uniform serialized Lyubashevsky extractor --- Complexity.lean | 1 + .../Lyubashevsky/NativeExtract.lean | 163 ++++++++++++++++++ ComplexityTests.lean | 1 + .../Crypto/LyubashevskyNative.lean | 48 ++++++ 4 files changed, 213 insertions(+) create mode 100644 Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean create mode 100644 ComplexityTests/Crypto/LyubashevskyNative.lean diff --git a/Complexity.lean b/Complexity.lean index 6dbe68fa2..c1bdb594d 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1496,6 +1496,7 @@ public import Complexity.Crypto.Protocols.SigmaProtocol.FiatShamir public import Complexity.Crypto.Protocols.SigmaProtocol.Identification public import Complexity.Crypto.Protocols.SigmaProtocol.Linear public import Complexity.Crypto.Protocols.SigmaProtocol.Lyubashevsky +public import Complexity.Crypto.Protocols.SigmaProtocol.Lyubashevsky.NativeExtract public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrIdentification public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrSignature public import Complexity.Crypto.Protocols.Signature.RandomOracle diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean new file mode 100644 index 000000000..56080a0bd --- /dev/null +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean @@ -0,0 +1,163 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.IntBinary.Decode +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary +import Complexity.Tactic.PolyTime + +/-! +# 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. +-/ + +@[expose] public section + +namespace Cslib.Crypto.Protocols.SigmaProtocol + +open Turing.MultiTapeTM + +/-- Dimensions followed by two challenge/optional-response pairs. -/ +abbrev LyubashevskyExtractInput := + (ℕ × ℕ) × ((List Bool × Option (List ℤ)) × (List Bool × Option (List ℤ))) + +/-- Unary dimensions, raw challenges and framed optional lists of binary signed integers. -/ +def encLyubashevskyExtractInput : LyubashevskyExtractInput ↪ List Bool := + encPair (encPair encUnary encUnary) + (encPair (encPair encBits (encOption (encList encIntBin))) + (encPair encBits (encOption (encList encIntBin)))) + +/-- Parse every input word with the existing framing conventions; malformed fields have total +zero/default interpretations. -/ +def decodeLyubashevskyExtractInput (word : List Bool) : LyubashevskyExtractInput := + let dimensions := unframe word + let rows := dropFrame word + let response (w : List Bool) : Option (List ℤ) := + if w.isEmpty then none else some ((frames w.tail).map decodeIntBin) + let row (w : List Bool) := (unframe w, response (dropFrame w)) + (((unframe dimensions).length, (dropFrame dimensions).length), + (row (unframe rows), row (dropFrame rows))) + +private theorem extractInput_decoder : + ∃ D : Decoder encLyubashevskyExtractInput, D.decode = decodeLyubashevskyExtractInput := by + let integer : Decoder encIntBin := { + decode := decodeIntBin + decode_enc := decodeIntBin_encIntBin + computable := computableInPolyTime_decodeIntBin.tidy.exists_degree } + let row := Decoder.pair Decoder.bits (Decoder.option (Decoder.list integer)) + let decoder := Decoder.pair (Decoder.pair Decoder.unary Decoder.unary) (Decoder.pair row row) + exact ⟨decoder, rfl⟩ + +/-- Parsing inverts the complete canonical input encoding. -/ +@[simp] theorem decodeLyubashevskyExtractInput_enc (input : LyubashevskyExtractInput) : + decodeLyubashevskyExtractInput (encLyubashevskyExtractInput input) = input := by + obtain ⟨decoder, hdecoder⟩ := extractInput_decoder + rw [← hdecoder] + exact decoder.decode_enc input + +/-- The total input parser has a plain polynomial-time certificate, including malformed words. -/ +@[fun_prop] +theorem computableInPolyTime_decodeLyubashevskyExtractInput : + ComputableInPolyTime decodeLyubashevskyExtractInput encBits encLyubashevskyExtractInput := by + obtain ⟨decoder, hdecoder⟩ := extractInput_decoder + rw [← hdecoder] + exact .of_tidy decoder.computableTidilyInPolyTime + +/-- Compute `z-z′` first, then the SIGNED challenge difference `c′-c`. The unary dimensions +control both output segments; optional responses default to zero coordinatewise. -/ +def lyubashevskyExtractList (input : LyubashevskyExtractInput) : List ℤ := + ((List.range input.1.1).map fun i => + (input.2.1.2.getD []).getD i 0 - (input.2.2.2.getD []).getD i 0) ++ + ((List.range input.1.2).map fun i => + (if input.2.2.1.getD i false then (1 : ℤ) else 0) - + (if input.2.1.1.getD i false then (1 : ℤ) else 0)) + +/-- Extraction always writes the two declared segments, even on malformed-length inputs. -/ +@[simp] theorem length_lyubashevskyExtractList (input : LyubashevskyExtractInput) : + (lyubashevskyExtractList input).length = input.1.1 + input.1.2 := by + simp [lyubashevskyExtractList] + +/-- One native extractor handles runtime dimensions and all binary integer magnitudes. -/ +@[fun_prop] +theorem computableInPolyTime_lyubashevskyExtractList : + ComputableInPolyTime lyubashevskyExtractList encLyubashevskyExtractInput + (encList encIntBin) := by + apply ComputableInPolyTime.of_tidy + unfold lyubashevskyExtractList encLyubashevskyExtractInput + fun_prop + +private theorem getD_optional_ofFn {m : ℕ} (z : Option (Fin m → ℤ)) (i : Fin m) : + ((z.map List.ofFn).getD []).getD i.val 0 = (z.getD 0) i := by + cases z <;> simp [List.getD_eq_getElem?_getD] + +private theorem map_range_eq_ofFn {α : Type} (n : ℕ) (f : ℕ → α) (g : Fin n → α) + (h : ∀ i : Fin n, f i.val = g i) : (List.range n).map f = List.ofFn g := by + rw [← List.map_coe_finRange_eq_range, List.map_map] + conv_rhs => rw [List.ofFn_eq_map] + exact List.map_congr_left fun i _ => h i + +/-- Canonical typed vectors give exactly the ordered response difference and signed reversed +challenge difference. This formula is independent of statement matrices and the modulus. -/ +theorem 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, z.map List.ofFn), (List.ofFn c', z'.map List.ofFn))) = + List.ofFn (Fin.append (fun i => (z.getD 0) i - (z'.getD 0) i) + (fun i => (if c' i then (1 : ℤ) else 0) - (if c i then (1 : ℤ) else 0))) := by + rw [List.ofFn_fin_append] + unfold lyubashevskyExtractList + dsimp only [Prod.fst, Prod.snd] + congr 1 + · apply map_range_eq_ofFn + intro i + rw [getD_optional_ofFn, getD_optional_ofFn] + · apply map_range_eq_ofFn + intro i + simp [List.getD_eq_getElem?_getD] + +/-- The complete serialized program: parse, extract, and frame every signed output coordinate. -/ +def lyubashevskyExtractWord (word : List Bool) : List Bool := + encList encIntBin (lyubashevskyExtractList (decodeLyubashevskyExtractInput word)) + +/-- The complete extractor is one plain polynomial-time word function, not a separate machine +for each fixed dimension. -/ +@[fun_prop] +theorem computableInPolyTime_lyubashevskyExtractWord : + ComputableInPolyTime lyubashevskyExtractWord encBits encBits := by + apply ComputableInPolyTime.of_tidy + exact (ComputableTidilyInPolyTime.encode (encList encIntBin)).comp + (computableInPolyTime_lyubashevskyExtractList.tidy.comp + computableInPolyTime_decodeLyubashevskyExtractInput.tidy) + +/-- The word program exactly implements the integer-list extractor on canonical encoded data. -/ +@[simp] theorem lyubashevskyExtractWord_enc (input : LyubashevskyExtractInput) : + lyubashevskyExtractWord (encLyubashevskyExtractInput input) = + encList encIntBin (lyubashevskyExtractList input) := by + simp [lyubashevskyExtractWord] + +end Cslib.Crypto.Protocols.SigmaProtocol diff --git a/ComplexityTests.lean b/ComplexityTests.lean index 2e462f704..1728c60d2 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -119,6 +119,7 @@ import ComplexityTests.Crypto.HomomorphicRefresh import ComplexityTests.Crypto.KeyChainSecurity import ComplexityTests.Crypto.LeveledSecurity import ComplexityTests.Crypto.Lyubashevsky +import ComplexityTests.Crypto.LyubashevskyNative import ComplexityTests.Crypto.MAC import ComplexityTests.Crypto.MerkleDamgard import ComplexityTests.Crypto.PlainConstructors diff --git a/ComplexityTests/Crypto/LyubashevskyNative.lean b/ComplexityTests/Crypto/LyubashevskyNative.lean new file mode 100644 index 000000000..de231aa21 --- /dev/null +++ b/ComplexityTests/Crypto/LyubashevskyNative.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Crypto.Protocols.SigmaProtocol.Lyubashevsky.NativeExtract + +/-! Runtime dimensions, signed challenge differences and total malformed-input behavior. -/ + +open Turing.MultiTapeTM Cslib.Crypto.Protocols.SigmaProtocol + +example : lyubashevskyExtractList + ((2, 1), (([false], some [0, 1]), ([true], some [1, 0]))) = [-1, 1, 1] := by + decide +kernel + +example : lyubashevskyExtractList + ((1, 1), (([true], some [-2]), ([false], some [3]))) = [-5, -1] := by + decide +kernel + +-- Missing coordinates default to zero/false, while extra coordinates are ignored. +example : lyubashevskyExtractList + ((3, 2), (([true, false, true], none), ([], some [7]))) = [-7, 0, 0, -1, 0] := by + decide +kernel + +example : lyubashevskyExtractList ((0, 0), (([true], some [7]), ([], none))) = [] := by + decide +kernel + +example : lyubashevskyExtractList ((0, 2), (([], none), ([true], none))) = [1, 0] := by + decide +kernel + +example : lyubashevskyExtractList ((2, 0), (([], none), ([], none))) = [0, 0] := by + decide +kernel + +example : lyubashevskyExtractWord [] = encList encIntBin [] := by decide +kernel + +example (input : LyubashevskyExtractInput) : + lyubashevskyExtractWord (encLyubashevskyExtractInput input) = + encList encIntBin (lyubashevskyExtractList input) := lyubashevskyExtractWord_enc input + +-- This is one word function for all dimensions and magnitudes, rather than fixed-size machines. +example : ComputableInPolyTime lyubashevskyExtractWord encBits encBits := + computableInPolyTime_lyubashevskyExtractWord + +/-- info: 'Cslib.Crypto.Protocols.SigmaProtocol.computableInPolyTime_lyubashevskyExtractWord' +depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs (whitespace := lax) in +#print axioms computableInPolyTime_lyubashevskyExtractWord From be4a3fa6ed5bb351d2f6fc92e1e11a274cb28902 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 24 Oct 2026 00:27:24 -0400 Subject: [PATCH 2/2] feat(crypto): bridge the word program to the typed Lyubashevsky extractor --- .../Lyubashevsky/NativeExtract.lean | 30 +++++++++++++++++++ .../Crypto/LyubashevskyNative.lean | 22 ++++++++++++++ 2 files changed, 52 insertions(+) diff --git a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean index 56080a0bd..ea29ae73b 100644 --- a/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean +++ b/Complexity/Crypto/Protocols/SigmaProtocol/Lyubashevsky/NativeExtract.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.IntBinary.Decode +public import Complexity.Crypto.Protocols.SigmaProtocol.Lyubashevsky import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary import Complexity.Tactic.PolyTime @@ -34,6 +35,8 @@ not a rewinding, knowledge-soundness or cryptographic security theorem. * `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. -/ @[expose] public section @@ -160,4 +163,31 @@ theorem computableInPolyTime_lyubashevskyExtractWord : encList encIntBin (lyubashevskyExtractList input) := by simp [lyubashevskyExtractWord] +/-- 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 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, z.map List.ofFn), (List.ofFn c', z'.map List.ofFn))) = + List.ofFn (fun i : Fin (m + k) => + lyubashevskyExtract n m k q y w c z c' z' (finSumFinEquiv.symm i)) := by + rw [lyubashevskyExtractList_ofFn] + congr 1 + funext i + cases i using Fin.addCases <;> simp [lyubashevskyExtract, lyubashevskyChallenge] + +/-- The complete word program agrees exactly with the named typed extractor, including absent +responses and zero dimensions, without assuming acceptance of either conversation. -/ +theorem 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, z.map List.ofFn), (List.ofFn c', z'.map List.ofFn)))) = + encList encIntBin (List.ofFn (fun i : Fin (m + k) => + lyubashevskyExtract n m k q y w c z c' z' (finSumFinEquiv.symm i))) := by + rw [lyubashevskyExtractWord_enc, lyubashevskyExtractList_eq_extract n m k q y w] + end Cslib.Crypto.Protocols.SigmaProtocol diff --git a/ComplexityTests/Crypto/LyubashevskyNative.lean b/ComplexityTests/Crypto/LyubashevskyNative.lean index de231aa21..51962db4c 100644 --- a/ComplexityTests/Crypto/LyubashevskyNative.lean +++ b/ComplexityTests/Crypto/LyubashevskyNative.lean @@ -46,3 +46,25 @@ example : ComputableInPolyTime lyubashevskyExtractWord encBits encBits := depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms computableInPolyTime_lyubashevskyExtractWord + +-- The actual typed protocol extractor has the same negative response / positive challenge tail. +example : List.ofFn (fun i : Fin 3 => + lyubashevskyExtract 1 2 1 7 (0, 0) 0 (fun _ => false) + (some fun i => (i.val : ℤ)) (fun _ => true) (some fun i => 1 - (i.val : ℤ)) + (finSumFinEquiv.symm i)) = [-1, 1, 1] := by + decide +kernel + +-- The named bridge applies even with no response coordinates or challenge coordinates. +example (q : ℕ) : + lyubashevskyExtractWord (encLyubashevskyExtractInput + ((0, 0), (([], none), ([], none)))) = + encList encIntBin (List.ofFn (fun i : Fin 0 => + lyubashevskyExtract 0 0 0 q (0, 0) 0 (fun _ => false) none + (fun _ => false) none (finSumFinEquiv.symm i))) := by + simpa using lyubashevskyExtractWord_eq_extract 0 0 0 q (0, 0) 0 + (fun _ => false) none (fun _ => false) none + +/-- info: 'Cslib.Crypto.Protocols.SigmaProtocol.lyubashevskyExtractWord_eq_extract' +depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs (whitespace := lax) in +#print axioms lyubashevskyExtractWord_eq_extract