From b4302b57480603428a3a6aeea678c3f4e04ca709 Mon Sep 17 00:00:00 2001 From: Eduardo Gomes Date: Wed, 10 Jun 2026 03:07:05 -0300 Subject: [PATCH 01/10] Extract shared 32-bit word utilities for the hash family SHA-256, BLAKE2s and BLAKE3 each carried their own copies of rotr32, the little-endian byte<->u32 conversions (bytesToWord, blockBytesToWords, wordToBytes, stateTo32Bytes, padBlock) and the SHA-256 initial hash value (which BLAKE2s/BLAKE3 reuse verbatim as their IV). Move them to Lampe/Crypto/WordUtils.lean in the shared Lampe.Crypto namespace and make the three hash models use it. --- Lampe/Lampe.lean | 1 + Lampe/Lampe/Crypto/Blake2s.lean | 70 ++++++------------------- Lampe/Lampe/Crypto/Blake3.lean | 63 +++-------------------- Lampe/Lampe/Crypto/Sha256.lean | 16 +++--- Lampe/Lampe/Crypto/WordUtils.lean | 85 +++++++++++++++++++++++++++++++ 5 files changed, 118 insertions(+), 117 deletions(-) create mode 100644 Lampe/Lampe/Crypto/WordUtils.lean diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index c02505cf..e424369f 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -41,6 +41,7 @@ import Lampe.Crypto.Secp256k1.Prime import Lampe.Crypto.Secp256r1 import Lampe.Crypto.Secp256r1.Prime import Lampe.Crypto.Sha256 +import Lampe.Crypto.WordUtils import Lampe.Data.Digits import Lampe.Data.Field import Lampe.Data.HList diff --git a/Lampe/Lampe/Crypto/Blake2s.lean b/Lampe/Lampe/Crypto/Blake2s.lean index 54f95e22..31dec71c 100644 --- a/Lampe/Lampe/Crypto/Blake2s.lean +++ b/Lampe/Lampe/Crypto/Blake2s.lean @@ -1,3 +1,4 @@ +import Lampe.Crypto.WordUtils import Lampe.Tp /-! @@ -25,11 +26,9 @@ namespace Lampe.Crypto.Blake2s /-! ### Constants -/ -/-- BLAKE2s IV — same as SHA-256's initial hash values (RFC 7693 -section 2.6). -/ -def iv : Array (BitVec 32) := - #[0x6a09e667#32, 0xbb67ae85#32, 0x3c6ef372#32, 0xa54ff53a#32, - 0x510e527f#32, 0x9b05688c#32, 0x1f83d9ab#32, 0x5be0cd19#32] +/-- BLAKE2s IV — exactly SHA-256's initial hash value (RFC 7693 +section 2.6), shared as `Lampe.Crypto.sha256IV`. -/ +def iv : Array (BitVec 32) := sha256IV /-- BLAKE2 σ permutation table (RFC 7693 section 2.7). Ten permutations of `0..15` selecting which message word feeds each G @@ -55,10 +54,6 @@ def OUT_LEN : Nat := 32 /-! ### G mixing function and rounds -/ -/-- 32-bit rotate-right. -/ -@[inline] def rotr32 (x : BitVec 32) (n : Nat) : BitVec 32 := - (x >>> n) ||| (x <<< (32 - n)) - /-- BLAKE2s G mixing function (RFC 7693 section 3.1). Updates four lanes `a, b, c, d` of the 16-word working state `v` using two message words `x, y`. Rotation amounts for BLAKE2s are 16/12/8/7. -/ @@ -129,46 +124,11 @@ def compress (h : Array (BitVec 32)) (m : Array (BitVec 32)) hOut := hOut.set! i (h[i]! ^^^ v[i]! ^^^ v[i + 8]!) return hOut -/-! ### Byte ↔ word conversion (little-endian) -/ - -/-- Pack 4 little-endian bytes into a u32. -/ -def bytesToWord (b0 b1 b2 b3 : BitVec 8) : BitVec 32 := - b0.zeroExtend 32 ||| (b1.zeroExtend 32 <<< (8 : Nat)) - ||| (b2.zeroExtend 32 <<< (16 : Nat)) - ||| (b3.zeroExtend 32 <<< (24 : Nat)) - -/-- Pack 64 bytes (one BLAKE2s block) into 16 u32 little-endian words. -The caller is responsible for zero-padding short final blocks. -/ -def blockBytesToWords (block : Array (BitVec 8)) : Array (BitVec 32) := Id.run do - let mut out : Array (BitVec 32) := Array.replicate 16 0 - for i in [:16] do - let b0 := block[4*i]! - let b1 := block[4*i + 1]! - let b2 := block[4*i + 2]! - let b3 := block[4*i + 3]! - out := out.set! i (bytesToWord b0 b1 b2 b3) - return out - -/-- Unpack a u32 to 4 little-endian bytes. -/ -def wordToBytes (w : BitVec 32) : Array (BitVec 8) := - #[ w.truncate 8, - (w >>> ( 8 : Nat)).truncate 8, - (w >>> (16 : Nat)).truncate 8, - (w >>> (24 : Nat)).truncate 8 ] - -/-- Serialise the 8-word chaining state as 32 little-endian bytes -(BLAKE2s-256 digest). -/ -def stateTo32Bytes (h : Array (BitVec 32)) : Array (BitVec 8) := Id.run do - let mut out : Array (BitVec 8) := Array.replicate 32 0 - for i in [:8] do - let bs := wordToBytes h[i]! - out := out.set! (4*i) bs[0]! - out := out.set! (4*i + 1) bs[1]! - out := out.set! (4*i + 2) bs[2]! - out := out.set! (4*i + 3) bs[3]! - return out +/-! ### Top-level entry points -/-! ### Top-level entry points -/ +Byte ↔ word conversion (`bytesToWord`, `blockBytesToWords`, +`wordToBytes`, `stateTo32Bytes`, `padBlock`) is shared with BLAKE3 via +`Lampe.Crypto.WordUtils`. -/ /-- Initial chaining state for unkeyed BLAKE2s-256. RFC 7693 section 2.5: `h[0] := IV[0] XOR (0x0101kknn)` where `kk = 0` (no key) and @@ -181,12 +141,6 @@ def initialState : Array (BitVec 32) := Id.run do h := h.set! 0 (h[0]! ^^^ 0x01010020#32) return h -/-- Pad a block of fewer than 64 bytes up to 64 bytes with trailing -zeros. -/ -def padBlock (block : Array (BitVec 8)) : Array (BitVec 8) := - if block.size ≥ BLOCK_LEN then block.extract 0 BLOCK_LEN - else block ++ Array.replicate (BLOCK_LEN - block.size) 0 - /-- Sequential BLAKE2s compression over an arbitrary-length byte input. Implements the loop from RFC 7693 section 3.3: @@ -216,6 +170,14 @@ def blake2sHashBytes (input : Array (BitVec 8)) : Array (BitVec 8) := Id.run do h := compress h (blockBytesToWords block) t isLast return stateTo32Bytes h +/-- `blake2sHashBytes` always produces exactly the 32-byte digest. -/ +theorem size_blake2sHashBytes (input : Array (BitVec 8)) : + (blake2sHashBytes input).size = 32 := by + simp only [blake2sHashBytes] + split + · exact size_stateTo32Bytes _ + · exact size_stateTo32Bytes _ + /-- Concrete BLAKE2s hash. Matches the signature the foreign builtin descriptor uses: input is a length-`N` array of bytes, output is the fixed 32-byte digest. -/ diff --git a/Lampe/Lampe/Crypto/Blake3.lean b/Lampe/Lampe/Crypto/Blake3.lean index 2232462e..8d7ab510 100644 --- a/Lampe/Lampe/Crypto/Blake3.lean +++ b/Lampe/Lampe/Crypto/Blake3.lean @@ -1,3 +1,4 @@ +import Lampe.Crypto.WordUtils import Lampe.Tp /-! @@ -27,10 +28,9 @@ namespace Lampe.Crypto.Blake3 /-! ### Constants -/ -/-- BLAKE3 IV (same as SHA-256's initial hash values). -/ -def iv : Array (BitVec 32) := - #[0x6a09e667#32, 0xbb67ae85#32, 0x3c6ef372#32, 0xa54ff53a#32, - 0x510e527f#32, 0x9b05688c#32, 0x1f83d9ab#32, 0x5be0cd19#32] +/-- BLAKE3 IV — exactly SHA-256's initial hash value, shared as +`Lampe.Crypto.sha256IV`. -/ +def iv : Array (BitVec 32) := sha256IV /-- Message-word permutation applied between rounds. -/ def msgPermutation : Array Nat := @@ -50,10 +50,6 @@ def CHUNK_LEN : Nat := 1024 /-! ### G mixing function and rounds -/ -/-- 32-bit rotate-right. -/ -@[inline] def rotr32 (x : BitVec 32) (n : Nat) : BitVec 32 := - (x >>> n) ||| (x <<< (32 - n)) - /-- BLAKE3 G mixing function: update four state lanes a/b/c/d using two message words mx/my (BLAKE3 spec §2.3). -/ def gFn (state : Array (BitVec 32)) (a b c d : Nat) (mx my : BitVec 32) : @@ -128,54 +124,11 @@ def compress (cv : Array (BitVec 32)) (blockWords : Array (BitVec 32)) s := s.set! (i + 8) (s[i+8]! ^^^ cv[i]!) return s -/-! ### Byte ↔ word conversion (little-endian) -/ - -/-- Pack 4 little-endian bytes into a u32. -/ -def bytesToWord (b0 b1 b2 b3 : BitVec 8) : BitVec 32 := - b0.zeroExtend 32 ||| (b1.zeroExtend 32 <<< (8 : Nat)) - ||| (b2.zeroExtend 32 <<< (16 : Nat)) - ||| (b3.zeroExtend 32 <<< (24 : Nat)) - -/-- Pack 64 bytes into 16 u32 little-endian words. The input array is -expected to have at least `start + 64` valid bytes; positions past -`inputLen` (the logical length) are zero-padded by the caller. -/ -def blockBytesToWords (block : Array (BitVec 8)) : Array (BitVec 32) := Id.run do - let mut out : Array (BitVec 32) := Array.replicate 16 0 - for i in [:16] do - let b0 := block[4*i]! - let b1 := block[4*i + 1]! - let b2 := block[4*i + 2]! - let b3 := block[4*i + 3]! - out := out.set! i (bytesToWord b0 b1 b2 b3) - return out - -/-- Unpack a u32 to 4 little-endian bytes. -/ -def wordToBytes (w : BitVec 32) : Array (BitVec 8) := - #[ w.truncate 8, - (w >>> ( 8 : Nat)).truncate 8, - (w >>> (16 : Nat)).truncate 8, - (w >>> (24 : Nat)).truncate 8 ] - -/-- Serialize the first 8 words of a state as 32 little-endian bytes -(BLAKE3 default output length). -/ -def stateTo32Bytes (s : Array (BitVec 32)) : Array (BitVec 8) := Id.run do - let mut out : Array (BitVec 8) := Array.replicate 32 0 - for i in [:8] do - let bs := wordToBytes s[i]! - out := out.set! (4*i) bs[0]! - out := out.set! (4*i + 1) bs[1]! - out := out.set! (4*i + 2) bs[2]! - out := out.set! (4*i + 3) bs[3]! - return out - -/-! ### Chunk and parent processing -/ +/-! ### Chunk and parent processing -/-- Pad an arbitrary-length byte slice to a multiple of 64 bytes with -zero bytes. Returns the padded array and the original length (as the -final block's `blockLen` field). -/ -def padBlock (bytes : Array (BitVec 8)) : Array (BitVec 8) := - if bytes.size ≥ 64 then bytes.extract 0 64 - else bytes ++ Array.replicate (64 - bytes.size) 0 +Byte ↔ word conversion (`bytesToWord`, `blockBytesToWords`, +`wordToBytes`, `stateTo32Bytes`, `padBlock`) is shared with BLAKE2s +via `Lampe.Crypto.WordUtils`. -/ /-- Process one chunk of up to 1024 bytes through up to 16 block compressions. Returns the chaining value (first 8 words) by default, diff --git a/Lampe/Lampe/Crypto/Sha256.lean b/Lampe/Lampe/Crypto/Sha256.lean index e37f837b..97db2733 100644 --- a/Lampe/Lampe/Crypto/Sha256.lean +++ b/Lampe/Lampe/Crypto/Sha256.lean @@ -1,3 +1,4 @@ +import Lampe.Crypto.WordUtils import Lampe.Tp /-! @@ -60,17 +61,16 @@ def roundConstants : List.Vector (BitVec 32) 64 := /-- FIPS 180-4 §5.3.3: SHA-256 initial hash value `H(0)`. First 32 bits of the fractional parts of the square roots of the first 8 -primes. Re-exported here for use in test vectors. -/ +primes. The constant itself lives in `Lampe.Crypto.sha256IV` (it is +also the BLAKE2s/BLAKE3 IV); this re-exports it at the `List.Vector` +shape used by the test vectors. -/ def initialHash : List.Vector (BitVec 32) 8 := - ⟨[ 0x6a09e667#32, 0xbb67ae85#32, 0x3c6ef372#32, 0xa54ff53a#32, - 0x510e527f#32, 0x9b05688c#32, 0x1f83d9ab#32, 0x5be0cd19#32 ], - by rfl⟩ + ⟨sha256IV.toList, by rfl⟩ -/-! ### Bit-mixing helpers (FIPS 180-4 §4.1.2) -/ +/-! ### Bit-mixing helpers (FIPS 180-4 §4.1.2) -/-- 32-bit rotate-right. -/ -@[inline] def rotr32 (x : BitVec 32) (n : Nat) : BitVec 32 := - (x >>> n) ||| (x <<< (32 - n)) +`rotr32` is shared with the BLAKE models via +`Lampe.Crypto.WordUtils`. -/ /-- Logical right shift, expressed at the same arity as `rotr32` for symmetry. -/ diff --git a/Lampe/Lampe/Crypto/WordUtils.lean b/Lampe/Lampe/Crypto/WordUtils.lean new file mode 100644 index 00000000..741eaa3b --- /dev/null +++ b/Lampe/Lampe/Crypto/WordUtils.lean @@ -0,0 +1,85 @@ +/-! +# Shared 32-bit word utilities for the hash-function family + +Helpers shared by the concrete SHA-256, BLAKE2s and BLAKE3 reference +models (`Lampe/Crypto/Sha256.lean`, `Blake2s.lean`, `Blake3.lean`): + +- 32-bit rotation (`rotr32`); +- little-endian byte ↔ `u32` word packing for the 64-byte block shape + all three functions share (`bytesToWord`, `blockBytesToWords`, + `wordToBytes`, `stateTo32Bytes`, `padBlock`); +- the SHA-256 initial hash value (`sha256IV`), which BLAKE2s and + BLAKE3 reuse verbatim as their IV. + +Note that SHA-256 itself is big-endian at the byte level; it only uses +`rotr32` and `sha256IV` from here. The little-endian byte conversions +are shared between the two BLAKE variants. +-/ + +namespace Lampe.Crypto + +/-- 32-bit rotate-right. -/ +@[inline] def rotr32 (x : BitVec 32) (n : Nat) : BitVec 32 := + (x >>> n) ||| (x <<< (32 - n)) + +/-- FIPS 180-4 §5.3.3: the SHA-256 initial hash value `H(0)` — the +first 32 bits of the fractional parts of the square roots of the first +8 primes. + +This is exactly the constant BLAKE2s (RFC 7693 §2.6) and BLAKE3 +(spec §2.1) use as their IV, so all three hash models share it. -/ +def sha256IV : Array (BitVec 32) := + #[0x6a09e667#32, 0xbb67ae85#32, 0x3c6ef372#32, 0xa54ff53a#32, + 0x510e527f#32, 0x9b05688c#32, 0x1f83d9ab#32, 0x5be0cd19#32] + +/-- Pack 4 little-endian bytes into a u32. -/ +def bytesToWord (b0 b1 b2 b3 : BitVec 8) : BitVec 32 := + b0.zeroExtend 32 ||| (b1.zeroExtend 32 <<< (8 : Nat)) + ||| (b2.zeroExtend 32 <<< (16 : Nat)) + ||| (b3.zeroExtend 32 <<< (24 : Nat)) + +/-- Pack 64 bytes (one BLAKE2s/BLAKE3 block) into 16 u32 little-endian +words. The caller is responsible for zero-padding short final blocks +(see `padBlock`). -/ +def blockBytesToWords (block : Array (BitVec 8)) : Array (BitVec 32) := Id.run do + let mut out : Array (BitVec 32) := Array.replicate 16 0 + for i in [:16] do + let b0 := block[4*i]! + let b1 := block[4*i + 1]! + let b2 := block[4*i + 2]! + let b3 := block[4*i + 3]! + out := out.set! i (bytesToWord b0 b1 b2 b3) + return out + +/-- Unpack a u32 to 4 little-endian bytes. -/ +def wordToBytes (w : BitVec 32) : Array (BitVec 8) := + #[ w.truncate 8, + (w >>> ( 8 : Nat)).truncate 8, + (w >>> (16 : Nat)).truncate 8, + (w >>> (24 : Nat)).truncate 8 ] + +/-- Serialise the first 8 words of a state as 32 little-endian bytes +(the 32-byte digest shape of BLAKE2s and BLAKE3). -/ +def stateTo32Bytes (s : Array (BitVec 32)) : Array (BitVec 8) := Id.run do + let mut out : Array (BitVec 8) := Array.replicate 32 0 + for i in [:8] do + let bs := wordToBytes s[i]! + out := out.set! (4*i) bs[0]! + out := out.set! (4*i + 1) bs[1]! + out := out.set! (4*i + 2) bs[2]! + out := out.set! (4*i + 3) bs[3]! + return out + +/-- `stateTo32Bytes` always produces exactly 32 bytes. -/ +theorem size_stateTo32Bytes (s : Array (BitVec 32)) : + (stateTo32Bytes s).size = 32 := by + simp [stateTo32Bytes, List.range'] + +/-- Pad a block of fewer than 64 bytes up to the 64-byte block size +shared by BLAKE2s and BLAKE3 with trailing zeros (longer inputs are +truncated to one block). -/ +def padBlock (block : Array (BitVec 8)) : Array (BitVec 8) := + if block.size ≥ 64 then block.extract 0 64 + else block ++ Array.replicate (64 - block.size) 0 + +end Lampe.Crypto From 1bf194043a8d8e88edae502a4e51ea59aea149f7 Mon Sep 17 00:00:00 2001 From: Eduardo Gomes Date: Wed, 10 Jun 2026 03:09:34 -0300 Subject: [PATCH 02/10] Deduplicate ECDSA verification across the secp curves Secp256k1.lean and Secp256r1.lean were clones modulo curve constants: bytesToNatBE, the Fermat-inversion orderPow/orderInv pair, and the FIPS 186-4 $6.4.2 verifyBytes body. Factor the curve-independent core into Lampe/Crypto/Ecdsa/Verify.lean, parameterized over the curve, its group order and the generator, and make the two curve files thin instantiations. The per-curve verifyBytes names (used by Builtin/Crypto/Ecdsa.lean) are preserved. --- Lampe/Lampe.lean | 1 + Lampe/Lampe/Crypto/Ecdsa/Verify.lean | 73 ++++++++++++++++++++++++++++ Lampe/Lampe/Crypto/Secp256k1.lean | 46 ++---------------- Lampe/Lampe/Crypto/Secp256r1.lean | 44 +++-------------- 4 files changed, 85 insertions(+), 79 deletions(-) create mode 100644 Lampe/Lampe/Crypto/Ecdsa/Verify.lean diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index e424369f..4afea413 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -30,6 +30,7 @@ import Lampe.Crypto.Bn254 import Lampe.Crypto.Bn254.Prime import Lampe.Crypto.Bn254.Sqrt import Lampe.Crypto.Ecdsa +import Lampe.Crypto.Ecdsa.Verify import Lampe.Crypto.EmbeddedCurve import Lampe.Crypto.Keccak import Lampe.Crypto.MathlibBridge diff --git a/Lampe/Lampe/Crypto/Ecdsa/Verify.lean b/Lampe/Lampe/Crypto/Ecdsa/Verify.lean new file mode 100644 index 00000000..971ea301 --- /dev/null +++ b/Lampe/Lampe/Crypto/Ecdsa/Verify.lean @@ -0,0 +1,73 @@ +import Lampe.Crypto.MathlibBridge +import Lampe.Data.Field +import Mathlib.Algebra.Field.ZMod + +/-! +# ECDSA signature verification — generic implementation + +The curve-independent core of ECDSA verification (FIPS 186-4 §6.4.2), +parameterized over the curve, its group order, and the generator +point. `Lampe/Crypto/Secp256k1.lean` and `Secp256r1.lean` instantiate +it with their respective SEC 2 / FIPS 186-4 parameters. + +Scalars are at most 256 bits on both supported curves, which is what +the iteration bounds in `orderPow` and (via `scalarMul`) the +double-and-add loops rely on. +-/ + +namespace Lampe.Crypto.Ecdsa + +/-- Interpret a byte array as a big-endian natural number. -/ +def bytesToNatBE (bs : Array (BitVec 8)) : Nat := + bs.foldl (fun acc b => acc * 256 + b.toNat) 0 + +/-- Modular exponentiation `base ^ exp % orderN` by square-and-multiply +over the low 256 bits of `exp` (the group orders we instantiate with +are 256-bit). -/ +def orderPow (orderN base exp : Nat) : Nat := Id.run do + let mut result : Nat := 1 + let mut b : Nat := base % orderN + let mut e : Nat := exp + for _ in [:256] do + if e % 2 = 1 then + result := (result * b) % orderN + e := e / 2 + b := (b * b) % orderN + return result + +/-- Modular inverse modulo the prime group order `orderN`, via +Fermat's little theorem: `a⁻¹ = a^(orderN - 2)`. -/ +@[inline] def orderInv (orderN a : Nat) : Nat := orderPow orderN a (orderN - 2) + +/-- ECDSA verification (FIPS 186-4 §6.4.2), generic over the curve +`W`, its (256-bit, prime) group order `orderN`, and the generator +`G`. Returns `false` on malformed `r`/`s`, an off-curve public key, or +x-coordinate mismatch; `true` iff the signature is valid. -/ +def verifyBytes {P : Prime} {W : WeierstrassCurve.Affine (Fp P)} + (orderN : Nat) (G : W.Point) + (pkX pkY : Array (BitVec 8)) + (sig : Array (BitVec 8)) + (msgHash : Array (BitVec 8)) : Bool := Id.run do + let r := bytesToNatBE (sig.extract 0 32) + let s := bytesToNatBE (sig.extract 32 64) + if r = 0 then return false + if r ≥ orderN then return false + if s = 0 then return false + if s ≥ orderN then return false + let qx : Fp P := ((bytesToNatBE pkX : Nat) : Fp P) + let qy : Fp P := ((bytesToNatBE pkY : Nat) : Fp P) + if hQ : W.Nonsingular qx qy then + let z := bytesToNatBE msgHash + let zRed := z % orderN + let sInv := orderInv orderN s + let u1 := (zRed * sInv) % orderN + let u2 := (r * sInv) % orderN + let Q : W.Point := WeierstrassCurve.Affine.Point.some (x := qx) (y := qy) hQ + let R : W.Point := scalarMul G u1 + scalarMul Q u2 + match R with + | .zero => return false + | @WeierstrassCurve.Affine.Point.some _ _ _ xr _ _ => return (xr.val % orderN) = r + else + return false + +end Lampe.Crypto.Ecdsa diff --git a/Lampe/Lampe/Crypto/Secp256k1.lean b/Lampe/Lampe/Crypto/Secp256k1.lean index 6eda7af8..3a2bf8c8 100644 --- a/Lampe/Lampe/Crypto/Secp256k1.lean +++ b/Lampe/Lampe/Crypto/Secp256k1.lean @@ -1,3 +1,4 @@ +import Lampe.Crypto.Ecdsa.Verify import Lampe.Crypto.MathlibBridge import Lampe.Crypto.Secp256k1.Prime import Mathlib.Algebra.Field.ZMod @@ -36,50 +37,13 @@ def G_nonsingular : W.Nonsingular Gx Gy := by native_decide def G : W.Point := WeierstrassCurve.Affine.Point.some (x := Gx) (y := Gy) G_nonsingular -def bytesToNatBE (bs : Array (BitVec 8)) : Nat := - bs.foldl (fun acc b => acc * 256 + b.toNat) 0 - -private def orderPow (base exp : Nat) : Nat := Id.run do - let mut result : Nat := 1 - let mut b : Nat := base % orderN - let mut e : Nat := exp - for _ in [:256] do - if e % 2 = 1 then - result := (result * b) % orderN - e := e / 2 - b := (b * b) % orderN - return result - -@[inline] private def orderInv (a : Nat) : Nat := orderPow a (orderN - 2) - -/-- ECDSA verification (FIPS 186-4 §6.4.2). Returns `false` on -malformed `r`/`s`, an off-curve public key, or x-coordinate -mismatch; `true` iff the signature is valid. -/ +/-- ECDSA verification on secp256k1 (FIPS 186-4 §6.4.2): the generic +`Ecdsa.verifyBytes` instantiated with the curve parameters above. -/ def verifyBytes (pkX pkY : Array (BitVec 8)) (sig : Array (BitVec 8)) - (msgHash : Array (BitVec 8)) : Bool := Id.run do - let r := bytesToNatBE (sig.extract 0 32) - let s := bytesToNatBE (sig.extract 32 64) - if r = 0 then return false - if r ≥ orderN then return false - if s = 0 then return false - if s ≥ orderN then return false - let qx : F := ((bytesToNatBE pkX : Nat) : F) - let qy : F := ((bytesToNatBE pkY : Nat) : F) - if hQ : W.Nonsingular qx qy then - let z := bytesToNatBE msgHash - let zRed := z % orderN - let sInv := orderInv s - let u1 := (zRed * sInv) % orderN - let u2 := (r * sInv) % orderN - let Q : W.Point := WeierstrassCurve.Affine.Point.some (x := qx) (y := qy) hQ - let R : W.Point := scalarMul G u1 + scalarMul Q u2 - match R with - | .zero => return false - | @WeierstrassCurve.Affine.Point.some _ _ _ xr _ _ => return (xr.val % orderN) = r - else - return false + (msgHash : Array (BitVec 8)) : Bool := + Ecdsa.verifyBytes (W := W) orderN G pkX pkY sig msgHash /-! ### Test vectors. Reproducible via `scripts/secp256k1_ref.py`. -/ diff --git a/Lampe/Lampe/Crypto/Secp256r1.lean b/Lampe/Lampe/Crypto/Secp256r1.lean index 1a4ca3fd..33e893ec 100644 --- a/Lampe/Lampe/Crypto/Secp256r1.lean +++ b/Lampe/Lampe/Crypto/Secp256r1.lean @@ -1,3 +1,4 @@ +import Lampe.Crypto.Ecdsa.Verify import Lampe.Crypto.MathlibBridge import Lampe.Crypto.Secp256r1.Prime import Mathlib.Algebra.Field.ZMod @@ -40,47 +41,14 @@ def G_nonsingular : W.Nonsingular Gx Gy := by native_decide def G : W.Point := WeierstrassCurve.Affine.Point.some (x := Gx) (y := Gy) G_nonsingular -def bytesToNatBE (bs : Array (BitVec 8)) : Nat := - bs.foldl (fun acc b => acc * 256 + b.toNat) 0 - -private def orderPow (base exp : Nat) : Nat := Id.run do - let mut result : Nat := 1 - let mut b : Nat := base % orderN - let mut e : Nat := exp - for _ in [:256] do - if e % 2 = 1 then - result := (result * b) % orderN - e := e / 2 - b := (b * b) % orderN - return result - -@[inline] private def orderInv (a : Nat) : Nat := orderPow a (orderN - 2) - +/-- ECDSA verification on secp256r1 / P-256 (FIPS 186-4 §6.4.2): the +generic `Ecdsa.verifyBytes` instantiated with the curve parameters +above. -/ def verifyBytes (pkX pkY : Array (BitVec 8)) (sig : Array (BitVec 8)) - (msgHash : Array (BitVec 8)) : Bool := Id.run do - let r := bytesToNatBE (sig.extract 0 32) - let s := bytesToNatBE (sig.extract 32 64) - if r = 0 then return false - if r ≥ orderN then return false - if s = 0 then return false - if s ≥ orderN then return false - let qx : F := ((bytesToNatBE pkX : Nat) : F) - let qy : F := ((bytesToNatBE pkY : Nat) : F) - if hQ : W.Nonsingular qx qy then - let z := bytesToNatBE msgHash - let zRed := z % orderN - let sInv := orderInv s - let u1 := (zRed * sInv) % orderN - let u2 := (r * sInv) % orderN - let Q : W.Point := WeierstrassCurve.Affine.Point.some (x := qx) (y := qy) hQ - let R : W.Point := scalarMul G u1 + scalarMul Q u2 - match R with - | .zero => return false - | @WeierstrassCurve.Affine.Point.some _ _ _ xr _ _ => return (xr.val % orderN) = r - else - return false + (msgHash : Array (BitVec 8)) : Bool := + Ecdsa.verifyBytes (W := W) orderN G pkX pkY sig msgHash /-! ### Test vectors. Reproducible via `scripts/secp256r1_ref.py`. -/ From dbf793040d78d4d84a599f916b23e706ee8717cc Mon Sep 17 00:00:00 2001 From: Eduardo Gomes Date: Wed, 10 Jun 2026 03:12:04 -0300 Subject: [PATCH 03/10] Move ECDSA test vectors into the Tests lib The native_decide example vectors in Secp256k1.lean / Secp256r1.lean ran on every library build and were invisible to lake test. Move them to Lampe/Tests/Ecdsa.lean (one section per curve), following the structure of the other crypto reference-vector test files. --- Lampe/Lampe/Crypto/Secp256k1.lean | 26 ---------- Lampe/Lampe/Crypto/Secp256r1.lean | 26 ---------- Lampe/Tests/Ecdsa.lean | 85 +++++++++++++++++++++++++++++++ 3 files changed, 85 insertions(+), 52 deletions(-) create mode 100644 Lampe/Tests/Ecdsa.lean diff --git a/Lampe/Lampe/Crypto/Secp256k1.lean b/Lampe/Lampe/Crypto/Secp256k1.lean index 3a2bf8c8..2583b95b 100644 --- a/Lampe/Lampe/Crypto/Secp256k1.lean +++ b/Lampe/Lampe/Crypto/Secp256k1.lean @@ -45,30 +45,4 @@ def verifyBytes (msgHash : Array (BitVec 8)) : Bool := Ecdsa.verifyBytes (W := W) orderN G pkX pkY sig msgHash -/-! ### Test vectors. Reproducible via `scripts/secp256k1_ref.py`. -/ - --- valid signature: sk = 0x01..01, msg = "Lampe ECDSA test vector" -private def validSimplePkX : Array (BitVec 8) := #[0x1b#8, 0x84#8, 0xc5#8, 0x56#8, 0x7b#8, 0x12#8, 0x64#8, 0x40#8, 0x99#8, 0x5d#8, 0x3e#8, 0xd5#8, 0xaa#8, 0xba#8, 0x05#8, 0x65#8, 0xd7#8, 0x1e#8, 0x18#8, 0x34#8, 0x60#8, 0x48#8, 0x19#8, 0xff#8, 0x9c#8, 0x17#8, 0xf5#8, 0xe9#8, 0xd5#8, 0xdd#8, 0x07#8, 0x8f#8] -private def validSimplePkY : Array (BitVec 8) := #[0x70#8, 0xbe#8, 0xaf#8, 0x8f#8, 0x58#8, 0x8b#8, 0x54#8, 0x15#8, 0x07#8, 0xfe#8, 0xd6#8, 0xa6#8, 0x42#8, 0xc5#8, 0xab#8, 0x42#8, 0xdf#8, 0xdf#8, 0x81#8, 0x20#8, 0xa7#8, 0xf6#8, 0x39#8, 0xde#8, 0x51#8, 0x22#8, 0xd4#8, 0x7a#8, 0x69#8, 0xa8#8, 0xe8#8, 0xd1#8] -private def validSimpleSig : Array (BitVec 8) := #[0x4d#8, 0x07#8, 0x54#8, 0xd6#8, 0x23#8, 0x0f#8, 0x85#8, 0x35#8, 0x33#8, 0xb8#8, 0x68#8, 0x77#8, 0x98#8, 0x43#8, 0xcb#8, 0x7f#8, 0x30#8, 0x85#8, 0xc9#8, 0xd6#8, 0x21#8, 0xd8#8, 0x40#8, 0xe8#8, 0xc1#8, 0xb4#8, 0x1a#8, 0x85#8, 0x1b#8, 0x56#8, 0x37#8, 0x90#8, 0x82#8, 0x9e#8, 0x4c#8, 0x7e#8, 0x20#8, 0xb8#8, 0x57#8, 0x00#8, 0x37#8, 0x82#8, 0x0e#8, 0x49#8, 0x09#8, 0x38#8, 0x41#8, 0xb1#8, 0x18#8, 0x31#8, 0x26#8, 0x7d#8, 0xa4#8, 0x52#8, 0x22#8, 0xcd#8, 0x78#8, 0x1d#8, 0xcf#8, 0xde#8, 0x38#8, 0x0b#8, 0x47#8, 0x00#8] -private def validSimpleMsg : Array (BitVec 8) := #[0x94#8, 0xbd#8, 0x9f#8, 0xb9#8, 0xaa#8, 0x9a#8, 0x8c#8, 0x3f#8, 0xd9#8, 0x1c#8, 0x1d#8, 0xe7#8, 0x50#8, 0x95#8, 0x33#8, 0x97#8, 0xdb#8, 0xdf#8, 0x1f#8, 0x84#8, 0x45#8, 0xf2#8, 0x80#8, 0xc8#8, 0xf6#8, 0x63#8, 0x9f#8, 0x12#8, 0x2c#8, 0x6f#8, 0x81#8, 0x92#8] -theorem secp256k1_validSimple_correct : - verifyBytes validSimplePkX validSimplePkY validSimpleSig validSimpleMsg = true := by - native_decide - --- valid signature: sk = 0x01..20, msg = "another message" -private def validSeqPkX : Array (BitVec 8) := #[0x84#8, 0xbf#8, 0x75#8, 0x62#8, 0x26#8, 0x2b#8, 0xbd#8, 0x69#8, 0x40#8, 0x08#8, 0x57#8, 0x48#8, 0xf3#8, 0xbe#8, 0x6a#8, 0xfa#8, 0x52#8, 0xae#8, 0x31#8, 0x71#8, 0x55#8, 0x18#8, 0x1e#8, 0xce#8, 0x31#8, 0xb6#8, 0x63#8, 0x51#8, 0xcc#8, 0xff#8, 0xa4#8, 0xb0#8] -private def validSeqPkY : Array (BitVec 8) := #[0x8c#8, 0xc4#8, 0x3d#8, 0x63#8, 0xb2#8, 0x85#8, 0x9d#8, 0x46#8, 0x9f#8, 0xee#8, 0x15#8, 0xf3#8, 0x1c#8, 0x9e#8, 0xdb#8, 0x53#8, 0x24#8, 0x26#8, 0x6e#8, 0x6f#8, 0xd0#8, 0x40#8, 0x7e#8, 0x87#8, 0x38#8, 0x2d#8, 0x60#8, 0xfc#8, 0x45#8, 0x11#8, 0xac#8, 0xd8#8] -private def validSeqSig : Array (BitVec 8) := #[0xf1#8, 0xc3#8, 0xb7#8, 0x00#8, 0x4b#8, 0xf7#8, 0xb9#8, 0x37#8, 0xf4#8, 0x01#8, 0xf6#8, 0x86#8, 0xb9#8, 0xd7#8, 0x6b#8, 0x87#8, 0x46#8, 0xc2#8, 0x21#8, 0xef#8, 0xe6#8, 0xce#8, 0xeb#8, 0xf6#8, 0x31#8, 0x9e#8, 0xbd#8, 0xcf#8, 0xf3#8, 0x71#8, 0x82#8, 0x31#8, 0x70#8, 0x09#8, 0x20#8, 0x12#8, 0x27#8, 0xd4#8, 0xf0#8, 0xe9#8, 0x74#8, 0x78#8, 0x0f#8, 0x0f#8, 0x8d#8, 0xeb#8, 0x5e#8, 0x3c#8, 0x6e#8, 0x74#8, 0xd1#8, 0xb3#8, 0xa7#8, 0xa7#8, 0x11#8, 0x44#8, 0xe5#8, 0xb5#8, 0xc5#8, 0xaf#8, 0x90#8, 0x61#8, 0x8f#8, 0x85#8] -private def validSeqMsg : Array (BitVec 8) := #[0x28#8, 0xea#8, 0x0f#8, 0x23#8, 0x11#8, 0x92#8, 0xa6#8, 0x57#8, 0x11#8, 0xa6#8, 0x44#8, 0x00#8, 0x3b#8, 0x0c#8, 0xb3#8, 0xa0#8, 0x49#8, 0xbf#8, 0xaf#8, 0x43#8, 0x39#8, 0x7b#8, 0x36#8, 0xc8#8, 0xbe#8, 0xed#8, 0x63#8, 0x13#8, 0x73#8, 0x74#8, 0xed#8, 0x97#8] -theorem secp256k1_validSeq_correct : - verifyBytes validSeqPkX validSeqPkY validSeqSig validSeqMsg = true := by - native_decide - --- tampered: validSimple sig with one bit flipped → reject -private def tamperedSig : Array (BitVec 8) := #[0x4c#8, 0x07#8, 0x54#8, 0xd6#8, 0x23#8, 0x0f#8, 0x85#8, 0x35#8, 0x33#8, 0xb8#8, 0x68#8, 0x77#8, 0x98#8, 0x43#8, 0xcb#8, 0x7f#8, 0x30#8, 0x85#8, 0xc9#8, 0xd6#8, 0x21#8, 0xd8#8, 0x40#8, 0xe8#8, 0xc1#8, 0xb4#8, 0x1a#8, 0x85#8, 0x1b#8, 0x56#8, 0x37#8, 0x90#8, 0x82#8, 0x9e#8, 0x4c#8, 0x7e#8, 0x20#8, 0xb8#8, 0x57#8, 0x00#8, 0x37#8, 0x82#8, 0x0e#8, 0x49#8, 0x09#8, 0x38#8, 0x41#8, 0xb1#8, 0x18#8, 0x31#8, 0x26#8, 0x7d#8, 0xa4#8, 0x52#8, 0x22#8, 0xcd#8, 0x78#8, 0x1d#8, 0xcf#8, 0xde#8, 0x38#8, 0x0b#8, 0x47#8, 0x00#8] -theorem secp256k1_tampered_correct : - verifyBytes validSimplePkX validSimplePkY tamperedSig validSimpleMsg = false := by - native_decide - end Lampe.Crypto.Secp256k1 diff --git a/Lampe/Lampe/Crypto/Secp256r1.lean b/Lampe/Lampe/Crypto/Secp256r1.lean index 33e893ec..c01d93a2 100644 --- a/Lampe/Lampe/Crypto/Secp256r1.lean +++ b/Lampe/Lampe/Crypto/Secp256r1.lean @@ -50,30 +50,4 @@ def verifyBytes (msgHash : Array (BitVec 8)) : Bool := Ecdsa.verifyBytes (W := W) orderN G pkX pkY sig msgHash -/-! ### Test vectors. Reproducible via `scripts/secp256r1_ref.py`. -/ - --- valid signature: sk = 0x01..01, msg = "Lampe ECDSA test vector" -private def validSimplePkX : Array (BitVec 8) := #[0x6f#8, 0xf0#8, 0x3b#8, 0x94#8, 0x92#8, 0x41#8, 0xce#8, 0x1d#8, 0xad#8, 0xd4#8, 0x35#8, 0x19#8, 0xe6#8, 0x96#8, 0x0e#8, 0x0a#8, 0x85#8, 0xb4#8, 0x1a#8, 0x69#8, 0xa0#8, 0x5c#8, 0x32#8, 0x81#8, 0x03#8, 0xaa#8, 0x2b#8, 0xce#8, 0x15#8, 0x94#8, 0xca#8, 0x16#8] -private def validSimplePkY : Array (BitVec 8) := #[0x3c#8, 0x4f#8, 0x75#8, 0x3a#8, 0x55#8, 0xbf#8, 0x01#8, 0xdc#8, 0x53#8, 0xf6#8, 0xc0#8, 0xb0#8, 0xc7#8, 0xee#8, 0xe7#8, 0x8b#8, 0x40#8, 0xc6#8, 0xff#8, 0x7d#8, 0x25#8, 0xa9#8, 0x6e#8, 0x22#8, 0x82#8, 0xb9#8, 0x89#8, 0xce#8, 0xf7#8, 0x1c#8, 0x14#8, 0x4a#8] -private def validSimpleSig : Array (BitVec 8) := #[0x3f#8, 0x6f#8, 0xd3#8, 0x12#8, 0xa1#8, 0xa4#8, 0x22#8, 0x2b#8, 0x82#8, 0xc5#8, 0x40#8, 0x37#8, 0x45#8, 0xdd#8, 0xc2#8, 0xd0#8, 0x38#8, 0xec#8, 0xe3#8, 0x77#8, 0x87#8, 0xd1#8, 0x6f#8, 0x0d#8, 0xbc#8, 0xec#8, 0x28#8, 0x69#8, 0x4d#8, 0x25#8, 0x71#8, 0x1f#8, 0xae#8, 0x09#8, 0x40#8, 0x99#8, 0xe2#8, 0xcb#8, 0x50#8, 0xd0#8, 0xbd#8, 0xe6#8, 0x4e#8, 0xe4#8, 0xcb#8, 0xf6#8, 0x9e#8, 0x57#8, 0x58#8, 0xd4#8, 0x65#8, 0xaa#8, 0x56#8, 0x2b#8, 0xe8#8, 0xc5#8, 0x20#8, 0xcd#8, 0x01#8, 0x7e#8, 0x76#8, 0xd1#8, 0xe9#8, 0x05#8] -private def validSimpleMsg : Array (BitVec 8) := #[0x94#8, 0xbd#8, 0x9f#8, 0xb9#8, 0xaa#8, 0x9a#8, 0x8c#8, 0x3f#8, 0xd9#8, 0x1c#8, 0x1d#8, 0xe7#8, 0x50#8, 0x95#8, 0x33#8, 0x97#8, 0xdb#8, 0xdf#8, 0x1f#8, 0x84#8, 0x45#8, 0xf2#8, 0x80#8, 0xc8#8, 0xf6#8, 0x63#8, 0x9f#8, 0x12#8, 0x2c#8, 0x6f#8, 0x81#8, 0x92#8] -theorem secp256r1_validSimple_correct : - verifyBytes validSimplePkX validSimplePkY validSimpleSig validSimpleMsg = true := by - native_decide - --- valid signature: sk = 0x01..20, msg = "another message" -private def validSeqPkX : Array (BitVec 8) := #[0x51#8, 0x5c#8, 0x3d#8, 0x6e#8, 0xb9#8, 0xe3#8, 0x96#8, 0xb9#8, 0x04#8, 0xd3#8, 0xfe#8, 0xca#8, 0x7f#8, 0x54#8, 0xfd#8, 0xcd#8, 0x0c#8, 0xc1#8, 0xe9#8, 0x97#8, 0xbf#8, 0x37#8, 0x5d#8, 0xca#8, 0x51#8, 0x5a#8, 0xd0#8, 0xa6#8, 0xc3#8, 0xb4#8, 0x03#8, 0x5f#8] -private def validSeqPkY : Array (BitVec 8) := #[0x45#8, 0x36#8, 0xbe#8, 0x3a#8, 0x50#8, 0xf3#8, 0x18#8, 0xfb#8, 0xf9#8, 0xa5#8, 0x47#8, 0x59#8, 0x02#8, 0xa2#8, 0x21#8, 0x50#8, 0x2b#8, 0xef#8, 0x0d#8, 0x57#8, 0xe0#8, 0x8c#8, 0x53#8, 0xb2#8, 0xcc#8, 0x0a#8, 0x56#8, 0xf1#8, 0x7d#8, 0x9f#8, 0x93#8, 0x54#8] -private def validSeqSig : Array (BitVec 8) := #[0x98#8, 0xe9#8, 0xe5#8, 0x14#8, 0x5d#8, 0x0b#8, 0xb0#8, 0x6c#8, 0xaa#8, 0xa2#8, 0xcf#8, 0x1a#8, 0xf4#8, 0xe3#8, 0x07#8, 0x09#8, 0x45#8, 0x10#8, 0xe6#8, 0xae#8, 0x0a#8, 0xd4#8, 0xf6#8, 0xd6#8, 0xca#8, 0x56#8, 0x7a#8, 0x07#8, 0xa0#8, 0x2a#8, 0xf9#8, 0x09#8, 0x0a#8, 0x0a#8, 0x7f#8, 0xe8#8, 0x18#8, 0x97#8, 0x08#8, 0x2f#8, 0x2d#8, 0xce#8, 0x82#8, 0x7c#8, 0x79#8, 0xb0#8, 0xa0#8, 0x8b#8, 0xdc#8, 0xda#8, 0x7b#8, 0x88#8, 0xcc#8, 0x49#8, 0x6d#8, 0xda#8, 0x6f#8, 0xa0#8, 0x46#8, 0x16#8, 0xe5#8, 0xdc#8, 0x68#8, 0x77#8] -private def validSeqMsg : Array (BitVec 8) := #[0x28#8, 0xea#8, 0x0f#8, 0x23#8, 0x11#8, 0x92#8, 0xa6#8, 0x57#8, 0x11#8, 0xa6#8, 0x44#8, 0x00#8, 0x3b#8, 0x0c#8, 0xb3#8, 0xa0#8, 0x49#8, 0xbf#8, 0xaf#8, 0x43#8, 0x39#8, 0x7b#8, 0x36#8, 0xc8#8, 0xbe#8, 0xed#8, 0x63#8, 0x13#8, 0x73#8, 0x74#8, 0xed#8, 0x97#8] -theorem secp256r1_validSeq_correct : - verifyBytes validSeqPkX validSeqPkY validSeqSig validSeqMsg = true := by - native_decide - --- tampered: validSimple sig with one bit flipped → reject -private def tamperedSig : Array (BitVec 8) := #[0x3e#8, 0x6f#8, 0xd3#8, 0x12#8, 0xa1#8, 0xa4#8, 0x22#8, 0x2b#8, 0x82#8, 0xc5#8, 0x40#8, 0x37#8, 0x45#8, 0xdd#8, 0xc2#8, 0xd0#8, 0x38#8, 0xec#8, 0xe3#8, 0x77#8, 0x87#8, 0xd1#8, 0x6f#8, 0x0d#8, 0xbc#8, 0xec#8, 0x28#8, 0x69#8, 0x4d#8, 0x25#8, 0x71#8, 0x1f#8, 0xae#8, 0x09#8, 0x40#8, 0x99#8, 0xe2#8, 0xcb#8, 0x50#8, 0xd0#8, 0xbd#8, 0xe6#8, 0x4e#8, 0xe4#8, 0xcb#8, 0xf6#8, 0x9e#8, 0x57#8, 0x58#8, 0xd4#8, 0x65#8, 0xaa#8, 0x56#8, 0x2b#8, 0xe8#8, 0xc5#8, 0x20#8, 0xcd#8, 0x01#8, 0x7e#8, 0x76#8, 0xd1#8, 0xe9#8, 0x05#8] -theorem secp256r1_tampered_correct : - verifyBytes validSimplePkX validSimplePkY tamperedSig validSimpleMsg = false := by - native_decide - end Lampe.Crypto.Secp256r1 diff --git a/Lampe/Tests/Ecdsa.lean b/Lampe/Tests/Ecdsa.lean new file mode 100644 index 00000000..f08960a9 --- /dev/null +++ b/Lampe/Tests/Ecdsa.lean @@ -0,0 +1,85 @@ +import Lampe +import Lampe.Crypto.Secp256k1 +import Lampe.Crypto.Secp256r1 + +/-! +# ECDSA reference test vectors (secp256k1 / secp256r1) + +Validates `Lampe.Crypto.Secp256k1.verifyBytes` and +`Lampe.Crypto.Secp256r1.verifyBytes` against vectors generated with +the pure-Python `ecdsa` library, which implements RFC 6979 +deterministic signing — so the vectors regenerate identically. + +Each curve gets two valid signatures (different keys and messages) and +one tampered signature (a single bit flipped) that must be rejected. + +Regenerate with `scripts/secp256k1_ref.py` / `scripts/secp256r1_ref.py`. +-/ + +namespace Tests.Ecdsa + +/-! ### secp256k1 -/ + +namespace Secp256k1 + +open Lampe.Crypto.Secp256k1 + +-- valid signature: sk = 0x01..01, msg = "Lampe ECDSA test vector" +private def validSimplePkX : Array (BitVec 8) := #[0x1b#8, 0x84#8, 0xc5#8, 0x56#8, 0x7b#8, 0x12#8, 0x64#8, 0x40#8, 0x99#8, 0x5d#8, 0x3e#8, 0xd5#8, 0xaa#8, 0xba#8, 0x05#8, 0x65#8, 0xd7#8, 0x1e#8, 0x18#8, 0x34#8, 0x60#8, 0x48#8, 0x19#8, 0xff#8, 0x9c#8, 0x17#8, 0xf5#8, 0xe9#8, 0xd5#8, 0xdd#8, 0x07#8, 0x8f#8] +private def validSimplePkY : Array (BitVec 8) := #[0x70#8, 0xbe#8, 0xaf#8, 0x8f#8, 0x58#8, 0x8b#8, 0x54#8, 0x15#8, 0x07#8, 0xfe#8, 0xd6#8, 0xa6#8, 0x42#8, 0xc5#8, 0xab#8, 0x42#8, 0xdf#8, 0xdf#8, 0x81#8, 0x20#8, 0xa7#8, 0xf6#8, 0x39#8, 0xde#8, 0x51#8, 0x22#8, 0xd4#8, 0x7a#8, 0x69#8, 0xa8#8, 0xe8#8, 0xd1#8] +private def validSimpleSig : Array (BitVec 8) := #[0x4d#8, 0x07#8, 0x54#8, 0xd6#8, 0x23#8, 0x0f#8, 0x85#8, 0x35#8, 0x33#8, 0xb8#8, 0x68#8, 0x77#8, 0x98#8, 0x43#8, 0xcb#8, 0x7f#8, 0x30#8, 0x85#8, 0xc9#8, 0xd6#8, 0x21#8, 0xd8#8, 0x40#8, 0xe8#8, 0xc1#8, 0xb4#8, 0x1a#8, 0x85#8, 0x1b#8, 0x56#8, 0x37#8, 0x90#8, 0x82#8, 0x9e#8, 0x4c#8, 0x7e#8, 0x20#8, 0xb8#8, 0x57#8, 0x00#8, 0x37#8, 0x82#8, 0x0e#8, 0x49#8, 0x09#8, 0x38#8, 0x41#8, 0xb1#8, 0x18#8, 0x31#8, 0x26#8, 0x7d#8, 0xa4#8, 0x52#8, 0x22#8, 0xcd#8, 0x78#8, 0x1d#8, 0xcf#8, 0xde#8, 0x38#8, 0x0b#8, 0x47#8, 0x00#8] +private def validSimpleMsg : Array (BitVec 8) := #[0x94#8, 0xbd#8, 0x9f#8, 0xb9#8, 0xaa#8, 0x9a#8, 0x8c#8, 0x3f#8, 0xd9#8, 0x1c#8, 0x1d#8, 0xe7#8, 0x50#8, 0x95#8, 0x33#8, 0x97#8, 0xdb#8, 0xdf#8, 0x1f#8, 0x84#8, 0x45#8, 0xf2#8, 0x80#8, 0xc8#8, 0xf6#8, 0x63#8, 0x9f#8, 0x12#8, 0x2c#8, 0x6f#8, 0x81#8, 0x92#8] +example : + verifyBytes validSimplePkX validSimplePkY validSimpleSig validSimpleMsg = true := by + native_decide + +-- valid signature: sk = 0x01..20, msg = "another message" +private def validSeqPkX : Array (BitVec 8) := #[0x84#8, 0xbf#8, 0x75#8, 0x62#8, 0x26#8, 0x2b#8, 0xbd#8, 0x69#8, 0x40#8, 0x08#8, 0x57#8, 0x48#8, 0xf3#8, 0xbe#8, 0x6a#8, 0xfa#8, 0x52#8, 0xae#8, 0x31#8, 0x71#8, 0x55#8, 0x18#8, 0x1e#8, 0xce#8, 0x31#8, 0xb6#8, 0x63#8, 0x51#8, 0xcc#8, 0xff#8, 0xa4#8, 0xb0#8] +private def validSeqPkY : Array (BitVec 8) := #[0x8c#8, 0xc4#8, 0x3d#8, 0x63#8, 0xb2#8, 0x85#8, 0x9d#8, 0x46#8, 0x9f#8, 0xee#8, 0x15#8, 0xf3#8, 0x1c#8, 0x9e#8, 0xdb#8, 0x53#8, 0x24#8, 0x26#8, 0x6e#8, 0x6f#8, 0xd0#8, 0x40#8, 0x7e#8, 0x87#8, 0x38#8, 0x2d#8, 0x60#8, 0xfc#8, 0x45#8, 0x11#8, 0xac#8, 0xd8#8] +private def validSeqSig : Array (BitVec 8) := #[0xf1#8, 0xc3#8, 0xb7#8, 0x00#8, 0x4b#8, 0xf7#8, 0xb9#8, 0x37#8, 0xf4#8, 0x01#8, 0xf6#8, 0x86#8, 0xb9#8, 0xd7#8, 0x6b#8, 0x87#8, 0x46#8, 0xc2#8, 0x21#8, 0xef#8, 0xe6#8, 0xce#8, 0xeb#8, 0xf6#8, 0x31#8, 0x9e#8, 0xbd#8, 0xcf#8, 0xf3#8, 0x71#8, 0x82#8, 0x31#8, 0x70#8, 0x09#8, 0x20#8, 0x12#8, 0x27#8, 0xd4#8, 0xf0#8, 0xe9#8, 0x74#8, 0x78#8, 0x0f#8, 0x0f#8, 0x8d#8, 0xeb#8, 0x5e#8, 0x3c#8, 0x6e#8, 0x74#8, 0xd1#8, 0xb3#8, 0xa7#8, 0xa7#8, 0x11#8, 0x44#8, 0xe5#8, 0xb5#8, 0xc5#8, 0xaf#8, 0x90#8, 0x61#8, 0x8f#8, 0x85#8] +private def validSeqMsg : Array (BitVec 8) := #[0x28#8, 0xea#8, 0x0f#8, 0x23#8, 0x11#8, 0x92#8, 0xa6#8, 0x57#8, 0x11#8, 0xa6#8, 0x44#8, 0x00#8, 0x3b#8, 0x0c#8, 0xb3#8, 0xa0#8, 0x49#8, 0xbf#8, 0xaf#8, 0x43#8, 0x39#8, 0x7b#8, 0x36#8, 0xc8#8, 0xbe#8, 0xed#8, 0x63#8, 0x13#8, 0x73#8, 0x74#8, 0xed#8, 0x97#8] +example : + verifyBytes validSeqPkX validSeqPkY validSeqSig validSeqMsg = true := by + native_decide + +-- tampered: validSimple sig with one bit flipped → reject +private def tamperedSig : Array (BitVec 8) := #[0x4c#8, 0x07#8, 0x54#8, 0xd6#8, 0x23#8, 0x0f#8, 0x85#8, 0x35#8, 0x33#8, 0xb8#8, 0x68#8, 0x77#8, 0x98#8, 0x43#8, 0xcb#8, 0x7f#8, 0x30#8, 0x85#8, 0xc9#8, 0xd6#8, 0x21#8, 0xd8#8, 0x40#8, 0xe8#8, 0xc1#8, 0xb4#8, 0x1a#8, 0x85#8, 0x1b#8, 0x56#8, 0x37#8, 0x90#8, 0x82#8, 0x9e#8, 0x4c#8, 0x7e#8, 0x20#8, 0xb8#8, 0x57#8, 0x00#8, 0x37#8, 0x82#8, 0x0e#8, 0x49#8, 0x09#8, 0x38#8, 0x41#8, 0xb1#8, 0x18#8, 0x31#8, 0x26#8, 0x7d#8, 0xa4#8, 0x52#8, 0x22#8, 0xcd#8, 0x78#8, 0x1d#8, 0xcf#8, 0xde#8, 0x38#8, 0x0b#8, 0x47#8, 0x00#8] +example : + verifyBytes validSimplePkX validSimplePkY tamperedSig validSimpleMsg = false := by + native_decide + +end Secp256k1 + +/-! ### secp256r1 / NIST P-256 -/ + +namespace Secp256r1 + +open Lampe.Crypto.Secp256r1 + +-- valid signature: sk = 0x01..01, msg = "Lampe ECDSA test vector" +private def validSimplePkX : Array (BitVec 8) := #[0x6f#8, 0xf0#8, 0x3b#8, 0x94#8, 0x92#8, 0x41#8, 0xce#8, 0x1d#8, 0xad#8, 0xd4#8, 0x35#8, 0x19#8, 0xe6#8, 0x96#8, 0x0e#8, 0x0a#8, 0x85#8, 0xb4#8, 0x1a#8, 0x69#8, 0xa0#8, 0x5c#8, 0x32#8, 0x81#8, 0x03#8, 0xaa#8, 0x2b#8, 0xce#8, 0x15#8, 0x94#8, 0xca#8, 0x16#8] +private def validSimplePkY : Array (BitVec 8) := #[0x3c#8, 0x4f#8, 0x75#8, 0x3a#8, 0x55#8, 0xbf#8, 0x01#8, 0xdc#8, 0x53#8, 0xf6#8, 0xc0#8, 0xb0#8, 0xc7#8, 0xee#8, 0xe7#8, 0x8b#8, 0x40#8, 0xc6#8, 0xff#8, 0x7d#8, 0x25#8, 0xa9#8, 0x6e#8, 0x22#8, 0x82#8, 0xb9#8, 0x89#8, 0xce#8, 0xf7#8, 0x1c#8, 0x14#8, 0x4a#8] +private def validSimpleSig : Array (BitVec 8) := #[0x3f#8, 0x6f#8, 0xd3#8, 0x12#8, 0xa1#8, 0xa4#8, 0x22#8, 0x2b#8, 0x82#8, 0xc5#8, 0x40#8, 0x37#8, 0x45#8, 0xdd#8, 0xc2#8, 0xd0#8, 0x38#8, 0xec#8, 0xe3#8, 0x77#8, 0x87#8, 0xd1#8, 0x6f#8, 0x0d#8, 0xbc#8, 0xec#8, 0x28#8, 0x69#8, 0x4d#8, 0x25#8, 0x71#8, 0x1f#8, 0xae#8, 0x09#8, 0x40#8, 0x99#8, 0xe2#8, 0xcb#8, 0x50#8, 0xd0#8, 0xbd#8, 0xe6#8, 0x4e#8, 0xe4#8, 0xcb#8, 0xf6#8, 0x9e#8, 0x57#8, 0x58#8, 0xd4#8, 0x65#8, 0xaa#8, 0x56#8, 0x2b#8, 0xe8#8, 0xc5#8, 0x20#8, 0xcd#8, 0x01#8, 0x7e#8, 0x76#8, 0xd1#8, 0xe9#8, 0x05#8] +private def validSimpleMsg : Array (BitVec 8) := #[0x94#8, 0xbd#8, 0x9f#8, 0xb9#8, 0xaa#8, 0x9a#8, 0x8c#8, 0x3f#8, 0xd9#8, 0x1c#8, 0x1d#8, 0xe7#8, 0x50#8, 0x95#8, 0x33#8, 0x97#8, 0xdb#8, 0xdf#8, 0x1f#8, 0x84#8, 0x45#8, 0xf2#8, 0x80#8, 0xc8#8, 0xf6#8, 0x63#8, 0x9f#8, 0x12#8, 0x2c#8, 0x6f#8, 0x81#8, 0x92#8] +example : + verifyBytes validSimplePkX validSimplePkY validSimpleSig validSimpleMsg = true := by + native_decide + +-- valid signature: sk = 0x01..20, msg = "another message" +private def validSeqPkX : Array (BitVec 8) := #[0x51#8, 0x5c#8, 0x3d#8, 0x6e#8, 0xb9#8, 0xe3#8, 0x96#8, 0xb9#8, 0x04#8, 0xd3#8, 0xfe#8, 0xca#8, 0x7f#8, 0x54#8, 0xfd#8, 0xcd#8, 0x0c#8, 0xc1#8, 0xe9#8, 0x97#8, 0xbf#8, 0x37#8, 0x5d#8, 0xca#8, 0x51#8, 0x5a#8, 0xd0#8, 0xa6#8, 0xc3#8, 0xb4#8, 0x03#8, 0x5f#8] +private def validSeqPkY : Array (BitVec 8) := #[0x45#8, 0x36#8, 0xbe#8, 0x3a#8, 0x50#8, 0xf3#8, 0x18#8, 0xfb#8, 0xf9#8, 0xa5#8, 0x47#8, 0x59#8, 0x02#8, 0xa2#8, 0x21#8, 0x50#8, 0x2b#8, 0xef#8, 0x0d#8, 0x57#8, 0xe0#8, 0x8c#8, 0x53#8, 0xb2#8, 0xcc#8, 0x0a#8, 0x56#8, 0xf1#8, 0x7d#8, 0x9f#8, 0x93#8, 0x54#8] +private def validSeqSig : Array (BitVec 8) := #[0x98#8, 0xe9#8, 0xe5#8, 0x14#8, 0x5d#8, 0x0b#8, 0xb0#8, 0x6c#8, 0xaa#8, 0xa2#8, 0xcf#8, 0x1a#8, 0xf4#8, 0xe3#8, 0x07#8, 0x09#8, 0x45#8, 0x10#8, 0xe6#8, 0xae#8, 0x0a#8, 0xd4#8, 0xf6#8, 0xd6#8, 0xca#8, 0x56#8, 0x7a#8, 0x07#8, 0xa0#8, 0x2a#8, 0xf9#8, 0x09#8, 0x0a#8, 0x0a#8, 0x7f#8, 0xe8#8, 0x18#8, 0x97#8, 0x08#8, 0x2f#8, 0x2d#8, 0xce#8, 0x82#8, 0x7c#8, 0x79#8, 0xb0#8, 0xa0#8, 0x8b#8, 0xdc#8, 0xda#8, 0x7b#8, 0x88#8, 0xcc#8, 0x49#8, 0x6d#8, 0xda#8, 0x6f#8, 0xa0#8, 0x46#8, 0x16#8, 0xe5#8, 0xdc#8, 0x68#8, 0x77#8] +private def validSeqMsg : Array (BitVec 8) := #[0x28#8, 0xea#8, 0x0f#8, 0x23#8, 0x11#8, 0x92#8, 0xa6#8, 0x57#8, 0x11#8, 0xa6#8, 0x44#8, 0x00#8, 0x3b#8, 0x0c#8, 0xb3#8, 0xa0#8, 0x49#8, 0xbf#8, 0xaf#8, 0x43#8, 0x39#8, 0x7b#8, 0x36#8, 0xc8#8, 0xbe#8, 0xed#8, 0x63#8, 0x13#8, 0x73#8, 0x74#8, 0xed#8, 0x97#8] +example : + verifyBytes validSeqPkX validSeqPkY validSeqSig validSeqMsg = true := by + native_decide + +-- tampered: validSimple sig with one bit flipped → reject +private def tamperedSig : Array (BitVec 8) := #[0x3e#8, 0x6f#8, 0xd3#8, 0x12#8, 0xa1#8, 0xa4#8, 0x22#8, 0x2b#8, 0x82#8, 0xc5#8, 0x40#8, 0x37#8, 0x45#8, 0xdd#8, 0xc2#8, 0xd0#8, 0x38#8, 0xec#8, 0xe3#8, 0x77#8, 0x87#8, 0xd1#8, 0x6f#8, 0x0d#8, 0xbc#8, 0xec#8, 0x28#8, 0x69#8, 0x4d#8, 0x25#8, 0x71#8, 0x1f#8, 0xae#8, 0x09#8, 0x40#8, 0x99#8, 0xe2#8, 0xcb#8, 0x50#8, 0xd0#8, 0xbd#8, 0xe6#8, 0x4e#8, 0xe4#8, 0xcb#8, 0xf6#8, 0x9e#8, 0x57#8, 0x58#8, 0xd4#8, 0x65#8, 0xaa#8, 0x56#8, 0x2b#8, 0xe8#8, 0xc5#8, 0x20#8, 0xcd#8, 0x01#8, 0x7e#8, 0x76#8, 0xd1#8, 0xe9#8, 0x05#8] +example : + verifyBytes validSimplePkX validSimplePkY tamperedSig validSimpleMsg = false := by + native_decide + +end Secp256r1 + +end Tests.Ecdsa From bfdfc9a70a57bc62ec6feb10a8b71a09c7f3c1c4 Mon Sep 17 00:00:00 2001 From: Eduardo Gomes Date: Wed, 10 Jun 2026 03:13:22 -0300 Subject: [PATCH 04/10] De-duplicate SHA-256 FIPS vectors into the Tests lib The FIPS 180-2 Appendix B vectors lived both inside Lampe/Crypto/Sha256.lean (private theorems re-checked on every library build) and in Lampe/Tests/Sha256.lean. Drop the library-side copies and add the one vector Tests was missing (block 1 of the two-block example: IV -> intermediate H^(1)), so the Tests file now covers all three compressions. --- Lampe/Lampe/Crypto/Sha256.lean | 79 ++-------------------------------- Lampe/Tests/Sha256.lean | 31 ++++++++++--- 2 files changed, 27 insertions(+), 83 deletions(-) diff --git a/Lampe/Lampe/Crypto/Sha256.lean b/Lampe/Lampe/Crypto/Sha256.lean index 97db2733..795ccad8 100644 --- a/Lampe/Lampe/Crypto/Sha256.lean +++ b/Lampe/Lampe/Crypto/Sha256.lean @@ -22,9 +22,9 @@ References: - §5.3.3 Initial hash value H(0) - §6.2.2 Hash computation (the compression we implement) -Validation: see test vectors at the bottom. They are copied verbatim -from FIPS 180-2 "Secure Hash Standard" Appendix B — both the single- -block "abc" example (B.1) and the two-block +Validation: see `Lampe/Tests/Sha256.lean`. The vectors there are +copied verbatim from FIPS 180-2 "Secure Hash Standard" Appendix B — +both the single-block "abc" example (B.1) and the two-block "abcdbcdec...mnopnopq" example (B.2), the latter giving us a non-trivial intermediate compression-state target H^(1) as well as the final hash H^(2). @@ -215,77 +215,4 @@ def compress Tp.denote p ((Tp.u 32).array (8 : U 32)) := compressOne state msg -/-! ### Test vectors - -All vectors below are copy-pasted verbatim from FIPS 180-2 Appendix B -(the SHA-256 worked examples). No third-party / re-derived references -are involved: the padded message blocks, the intermediate hash value -H^(1), and the final hash are exactly the byte sequences printed in the -standard. - -- B.1: single-block "abc" example. One compression of the IV against - the padded "abc" block produces the published SHA-256("abc"). -- B.2: two-block "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" - example. Block 1 takes the IV to the intermediate state H^(1); block - 2 takes H^(1) to the final hash H^(2). We test both compressions. -/ - -/-- FIPS 180-2 §B.1: padded "abc" block. -/ -private def abcMsg : List.Vector (BitVec 32) 16 := - ⟨[ 0x61626380#32, 0x00000000#32, 0x00000000#32, 0x00000000#32, - 0x00000000#32, 0x00000000#32, 0x00000000#32, 0x00000000#32, - 0x00000000#32, 0x00000000#32, 0x00000000#32, 0x00000000#32, - 0x00000000#32, 0x00000000#32, 0x00000000#32, 0x00000018#32 ], - by rfl⟩ - -/-- FIPS 180-2 §B.1: the final hash value (also the published -SHA-256("abc")). -/ -private def abcOut : List.Vector (BitVec 32) 8 := - ⟨[ 0xba7816bf#32, 0x8f01cfea#32, 0x414140de#32, 0x5dae2223#32, - 0xb00361a3#32, 0x96177a9c#32, 0xb410ff61#32, 0xf20015ad#32 ], - by rfl⟩ - -theorem sha256_abc_correct : - compressOne initialHash abcMsg = abcOut := by native_decide - -/-- FIPS 180-2 §B.2: first padded block of the two-block example, -W_0 through W_15 as printed in the standard. -/ -private def longMsgBlock1 : List.Vector (BitVec 32) 16 := - ⟨[ 0x61626364#32, 0x62636465#32, 0x63646566#32, 0x64656667#32, - 0x65666768#32, 0x66676869#32, 0x6768696a#32, 0x68696a6b#32, - 0x696a6b6c#32, 0x6a6b6c6d#32, 0x6b6c6d6e#32, 0x6c6d6e6f#32, - 0x6d6e6f70#32, 0x6e6f7071#32, 0x80000000#32, 0x00000000#32 ], - by rfl⟩ - -/-- FIPS 180-2 §B.2: intermediate hash value H^(1) after processing -block 1, copied verbatim from the standard. -/ -private def longMsgIntermediate : List.Vector (BitVec 32) 8 := - ⟨[ 0x85e655d6#32, 0x417a1795#32, 0x3363376a#32, 0x624cde5c#32, - 0x76e09589#32, 0xcac5f811#32, 0xcc4b32c1#32, 0xf20e533a#32 ], - by rfl⟩ - -theorem sha256_long_msg_block1_correct : - compressOne initialHash longMsgBlock1 = longMsgIntermediate := by - native_decide - -/-- FIPS 180-2 §B.2: second padded block of the two-block example. -All zeros except the 64-bit length field 0x00000000_000001c0 (448 bits -in big-endian). -/ -private def longMsgBlock2 : List.Vector (BitVec 32) 16 := - ⟨[ 0x00000000#32, 0x00000000#32, 0x00000000#32, 0x00000000#32, - 0x00000000#32, 0x00000000#32, 0x00000000#32, 0x00000000#32, - 0x00000000#32, 0x00000000#32, 0x00000000#32, 0x00000000#32, - 0x00000000#32, 0x00000000#32, 0x00000000#32, 0x000001c0#32 ], - by rfl⟩ - -/-- FIPS 180-2 §B.2: final hash value H^(2), copied verbatim. Also the -published SHA-256("abcdbcdec..."). -/ -private def longMsgFinal : List.Vector (BitVec 32) 8 := - ⟨[ 0x248d6a61#32, 0xd20638b8#32, 0xe5c02693#32, 0x0c3e6039#32, - 0xa33ce459#32, 0x64ff2167#32, 0xf6ecedd4#32, 0x19db06c1#32 ], - by rfl⟩ - -theorem sha256_long_msg_block2_correct : - compressOne longMsgIntermediate longMsgBlock2 = longMsgFinal := by - native_decide - end Lampe.Crypto.Sha256 diff --git a/Lampe/Tests/Sha256.lean b/Lampe/Tests/Sha256.lean index 4e15623b..fb7ef5b0 100644 --- a/Lampe/Tests/Sha256.lean +++ b/Lampe/Tests/Sha256.lean @@ -4,15 +4,16 @@ import Lampe.Crypto.Sha256 /-! # Sha256 compression — driver-level test vectors -These re-run the FIPS 180-2 Appendix B SHA-256 worked examples through -the public `Crypto.Sha256.compressOne` entry point. The same vectors are -also covered (as `private` theorems) inside `Lampe/Crypto/Sha256.lean`; -duplicating them at the Tests layer makes them visible to `lake test` -and protects the public surface from accidental regressions. +These run the FIPS 180-2 Appendix B SHA-256 worked examples through +the public `Crypto.Sha256.compressOne` entry point. All vectors are +copied verbatim from the standard: the padded message blocks, the +intermediate hash value H^(1), and the final hashes are exactly the +byte sequences printed there. Reference: FIPS 180-2 "Secure Hash Standard" Appendix B (single-block -"abc" example in §B.1; two-block "abcdbcdec..." example in §B.2, from -which we take the final hash). +"abc" example in §B.1; two-block "abcdbcdec..." example in §B.2, whose +two compressions give us the intermediate state H^(1) and the final +hash H^(2)). https://csrc.nist.gov/csrc/media/publications/fips/180/2/archive/ 2002-08-01/documents/fips180-2.pdf @@ -39,6 +40,22 @@ example : 0xb00361a3#32, 0x96177a9c#32, 0xb410ff61#32, 0xf20015ad#32 ], by rfl⟩ := by native_decide +/-- FIPS 180-2 §B.2: first-block compression of the two-block example +takes the IV to the intermediate hash value H^(1) printed in the +standard. -/ +example : + compressOne + initialHash + ⟨[ 0x61626364#32, 0x62636465#32, 0x63646566#32, 0x64656667#32, + 0x65666768#32, 0x66676869#32, 0x6768696a#32, 0x68696a6b#32, + 0x696a6b6c#32, 0x6a6b6c6d#32, 0x6b6c6d6e#32, 0x6c6d6e6f#32, + 0x6d6e6f70#32, 0x6e6f7071#32, 0x80000000#32, 0x00000000#32 ], + by rfl⟩ + = + ⟨[ 0x85e655d6#32, 0x417a1795#32, 0x3363376a#32, 0x624cde5c#32, + 0x76e09589#32, 0xcac5f811#32, 0xcc4b32c1#32, 0xf20e533a#32 ], + by rfl⟩ := by native_decide + /-- FIPS 180-2 §B.2: second-block compression of the two-block example takes the intermediate H^(1) (also printed in the standard) to the final published hash H^(2). -/ From 81b57db1ea29f1dbfb674846beac8d28188f12ae Mon Sep 17 00:00:00 2001 From: Eduardo Gomes Date: Wed, 10 Jun 2026 03:13:56 -0300 Subject: [PATCH 05/10] Switch Keccak-f[1600] test vectors to native_decide The two XKCP KAT theorems ran full Keccak-f[1600] permutations through the kernel evaluator via plain decide (with a bumped maxRecDepth). Every other reference-vector test in the crypto series uses native_decide; align these for consistency and faster builds. --- Lampe/Tests/Keccak.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Lampe/Tests/Keccak.lean b/Lampe/Tests/Keccak.lean index b23a8b98..6e8b09d4 100644 --- a/Lampe/Tests/Keccak.lean +++ b/Lampe/Tests/Keccak.lean @@ -43,10 +43,8 @@ private def zerosOut : List.Vector (BitVec 64) 25 := 0x1841f924a2c509e4#64, 0x16f53526e70465c2#64, 0x75f644e97f30a13b#64, 0xeaf1ff7b5ceca249#64], by decide⟩ --- Vector 1: kernel-checked via plain `decide` with bumped `maxRecDepth`. -set_option maxRecDepth 4096 in theorem keccakF1600_zeros_correct : - (keccakF1600State zerosIn).toList = zerosOut.toList := by decide + (keccakF1600State zerosIn).toList = zerosOut.toList := by native_decide /-! ### Vector 2: second application XKCP `KeccakF-1600-IntermediateValues.txt`, "state after permutation" @@ -63,9 +61,7 @@ private def secondOut : List.Vector (BitVec 64) 25 := 0x202a9ec5faa3cce8#64, 0x5b3402464e1c3db6#64, 0x609f4e62a44c1059#64, 0x20d06cd26a8fbf5c#64], by decide⟩ --- Vector 2: kernel-checked via plain `decide` with bumped `maxRecDepth`. -set_option maxRecDepth 4096 in theorem keccakF1600_second_correct : - (keccakF1600State zerosOut).toList = secondOut.toList := by decide + (keccakF1600State zerosOut).toList = secondOut.toList := by native_decide end Tests.Keccak From 1b413b6c127a233eb934ded2b03989877d371350 Mon Sep 17 00:00:00 2001 From: Eduardo Gomes Date: Wed, 10 Jun 2026 03:14:35 -0300 Subject: [PATCH 06/10] Rename Builtin/Crypto/Hash.lean to Poseidon2.lean The file holds only the poseidon2Permutation builtin; every later crypto primitive has a self-named file. Update the Lampe.lean import. --- Lampe/Lampe.lean | 2 +- Lampe/Lampe/Builtin/Crypto/{Hash.lean => Poseidon2.lean} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename Lampe/Lampe/Builtin/Crypto/{Hash.lean => Poseidon2.lean} (100%) diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index 4afea413..203e6270 100644 --- a/Lampe/Lampe.lean +++ b/Lampe/Lampe.lean @@ -11,9 +11,9 @@ import Lampe.Builtin.Crypto.Blake2s import Lampe.Builtin.Crypto.Blake3 import Lampe.Builtin.Crypto.Ecdsa import Lampe.Builtin.Crypto.EmbeddedCurve -import Lampe.Builtin.Crypto.Hash import Lampe.Builtin.Crypto.Keccak import Lampe.Builtin.Crypto.Pedersen +import Lampe.Builtin.Crypto.Poseidon2 import Lampe.Builtin.Crypto.Sha256 import Lampe.Builtin.Field import Lampe.Builtin.Lens diff --git a/Lampe/Lampe/Builtin/Crypto/Hash.lean b/Lampe/Lampe/Builtin/Crypto/Poseidon2.lean similarity index 100% rename from Lampe/Lampe/Builtin/Crypto/Hash.lean rename to Lampe/Lampe/Builtin/Crypto/Poseidon2.lean From a4f1d784ceabb0a192b957aca18657b38c055529 Mon Sep 17 00:00:00 2001 From: Eduardo Gomes Date: Wed, 10 Jun 2026 03:15:53 -0300 Subject: [PATCH 07/10] Tidy crypto builtin and module docs Drop the redundant doc comments on the ECDSA and BLAKE3 builtins (they restate the definitions; the `isUnconstrained = false` note is a given), and fix stale wording / test-vector references in the BLAKE2s and Keccak module docs. --- Lampe/Lampe/Builtin/Crypto/Blake3.lean | 8 -------- Lampe/Lampe/Builtin/Crypto/Ecdsa.lean | 10 ---------- Lampe/Lampe/Crypto/Blake2s.lean | 2 +- Lampe/Lampe/Crypto/Keccak.lean | 2 +- 4 files changed, 2 insertions(+), 20 deletions(-) diff --git a/Lampe/Lampe/Builtin/Crypto/Blake3.lean b/Lampe/Lampe/Builtin/Crypto/Blake3.lean index 6bb04873..4444d336 100644 --- a/Lampe/Lampe/Builtin/Crypto/Blake3.lean +++ b/Lampe/Lampe/Builtin/Crypto/Blake3.lean @@ -5,14 +5,6 @@ import Lampe.Data.Field namespace Lampe.Builtin -/-- -Noir's `__blake3` foreign builtin (generic over input length `N`). -Modeled by the opaque `Crypto.Blake3.blake3Hash` returning a 32-byte -digest. The Noir wrapper `hash::blake3` adds an -`is_unconstrained`-guarded `static_assert` on `N ≤ 1024`; under -Lampe's `isUnconstrained = false`, that branch collapses away and -the wrapper reduces to a single builtin call. --/ def blake3 := newGenericTotalPureBuiltin (fun (N : U 32) => ⟨[(Tp.u 8).array N], (Tp.u 8).array (32 : U 32)⟩) (fun _N h![input] => Crypto.Blake3.blake3Hash input) diff --git a/Lampe/Lampe/Builtin/Crypto/Ecdsa.lean b/Lampe/Lampe/Builtin/Crypto/Ecdsa.lean index b48e9ec8..e54d38fb 100644 --- a/Lampe/Lampe/Builtin/Crypto/Ecdsa.lean +++ b/Lampe/Lampe/Builtin/Crypto/Ecdsa.lean @@ -5,22 +5,12 @@ import Lampe.Data.Field namespace Lampe.Builtin -/-- -Noir's `ecdsa_secp256k1` foreign builtin. Modeled by the opaque -`Crypto.Ecdsa.secp256k1Verify`; the trailing `predicate : Bool` -argument from the Noir signature is discarded since the model is -defined only by its inputs. --/ def ecdsaSecp256K1 := newTotalPureBuiltin ⟨[(Tp.u 8).array (32 : U 32), (Tp.u 8).array (32 : U 32), (Tp.u 8).array (64 : U 32), (Tp.u 8).array (32 : U 32), .bool], .bool⟩ (fun h![pkX, pkY, sig, msg, _predicate] => Crypto.Ecdsa.secp256k1Verify pkX pkY sig msg) -/-- -Noir's `ecdsa_secp256r1` foreign builtin. Modeled by the opaque -`Crypto.Ecdsa.secp256r1Verify`. --/ def ecdsaSecp256R1 := newTotalPureBuiltin ⟨[(Tp.u 8).array (32 : U 32), (Tp.u 8).array (32 : U 32), (Tp.u 8).array (64 : U 32), (Tp.u 8).array (32 : U 32), .bool], .bool⟩ diff --git a/Lampe/Lampe/Crypto/Blake2s.lean b/Lampe/Lampe/Crypto/Blake2s.lean index 31dec71c..e6a4b84d 100644 --- a/Lampe/Lampe/Crypto/Blake2s.lean +++ b/Lampe/Lampe/Crypto/Blake2s.lean @@ -14,7 +14,7 @@ References: - Reference C implementation: https://github.com/BLAKE2/BLAKE2/tree/master/ref -Validation: see test vectors at the bottom. The canonical RFC 7693 +Validation: see `Lampe/Tests/Blake2s.lean`. The canonical RFC 7693 vectors (`"abc"` etc.) are anchored against Python's `hashlib.blake2s`, which wraps the BLAKE2 reference implementation (`libb2`). diff --git a/Lampe/Lampe/Crypto/Keccak.lean b/Lampe/Lampe/Crypto/Keccak.lean index 010f7cc5..09fc8112 100644 --- a/Lampe/Lampe/Crypto/Keccak.lean +++ b/Lampe/Lampe/Crypto/Keccak.lean @@ -111,7 +111,7 @@ def keccakF1600State (a : State) : State := /-! ### Entry point matching the builtin descriptor -/ /-- Concrete Keccak-f[1600] over the Lampe state shape. Matches the -opaque signature the builtin descriptor uses. -/ +signature the builtin descriptor uses. -/ def keccakF1600 {p : Prime} (input : Tp.denote p ((Tp.u 64).array (25 : U 32))) : Tp.denote p ((Tp.u 64).array (25 : U 32)) := From eb8fd67ae4c23077233c8efdf07c04ff56af50b6 Mon Sep 17 00:00:00 2001 From: Eduardo Gomes Date: Wed, 10 Jun 2026 03:16:17 -0300 Subject: [PATCH 08/10] Make one-off generators in-place updaters under scripts/gen/ The reference test-vector and Pratt-certificate generators are author-time tools whose outputs are committed and which CI never runs. Group them under scripts/gen/ (mirroring scripts/ci/) with their own requirements.txt, so the CI-image deps (scripts/requirements.txt) and the generator-only deps no longer share a directory. Give every generator one interface -- `python3 scripts/gen/.py ` -- that rewrites only the region between `-- BEGIN/END generated