diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean index c02505cf..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 @@ -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 @@ -41,6 +42,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/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/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 diff --git a/Lampe/Lampe/Crypto/Blake2s.lean b/Lampe/Lampe/Crypto/Blake2s.lean index 54f95e22..2494e27a 100644 --- a/Lampe/Lampe/Crypto/Blake2s.lean +++ b/Lampe/Lampe/Crypto/Blake2s.lean @@ -1,3 +1,4 @@ +import Lampe.Crypto.WordUtils import Lampe.Tp /-! @@ -13,23 +14,21 @@ 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`). -Regenerate test vectors with `scripts/blake2s_ref.py`. +Regenerate test vectors with `scripts/gen/blake2s_ref.py`. -/ 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..f37c08c0 100644 --- a/Lampe/Lampe/Crypto/Blake3.lean +++ b/Lampe/Lampe/Crypto/Blake3.lean @@ -1,3 +1,4 @@ +import Lampe.Crypto.WordUtils import Lampe.Tp /-! @@ -20,17 +21,16 @@ taken from the official BLAKE3 Python binding (`pip install blake3`), which is maintained by the BLAKE3 team and known to match the published `test_vectors.json`. -Regenerate test vectors with `scripts/blake3_ref.py`. +Regenerate test vectors with `scripts/gen/blake3_ref.py`. -/ 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/Bn254.lean b/Lampe/Lampe/Crypto/Bn254.lean index 89576e5c..6d954aa2 100644 --- a/Lampe/Lampe/Crypto/Bn254.lean +++ b/Lampe/Lampe/Crypto/Bn254.lean @@ -99,13 +99,13 @@ lemma prime_sub_pow128_gt {p} [Lampe.Prime.BitsGT p 129] : p.natVal - pow128 > p exact (Nat.lt_sub_iff_add_lt).2 hsum lemma sub_val_gt_pow128_of_lt {p} [Lampe.Prime.BitsGT p 129] {a b : Fp p} - (ha : a.val < pow128) (hb : b.val ≤ pow128) (h : a.val < b.val) : + (_ha : a.val < pow128) (hb : b.val ≤ pow128) (h : a.val < b.val) : (a - b).val > pow128 := by have hb_lt : b.val < p.natVal := lt_of_le_of_lt hb (pow128_lt_prime (p := p)) have hbne : b ≠ 0 := by intro hbz subst hbz - simpa using h + simp at h haveI : NeZero b := ⟨hbne⟩ have hneg : (-b).val = p.natVal - b.val := by simpa using (ZMod.val_neg_of_ne_zero b) diff --git a/Lampe/Lampe/Crypto/Bn254/Prime.lean b/Lampe/Lampe/Crypto/Bn254/Prime.lean index 1845ced6..6575f0bb 100644 --- a/Lampe/Lampe/Crypto/Bn254/Prime.lean +++ b/Lampe/Lampe/Crypto/Bn254/Prime.lean @@ -6,12 +6,10 @@ import Mathlib.Tactic.NormNum.Prime # BN254 scalar-field prime: Pratt certificate and canonical `Lampe.Prime` The Pratt-certificate section of this file (between the BEGIN/END -markers below) is **mechanically generated by** `scripts/gen_pratt.py`. +markers below) is **mechanically generated by** `scripts/gen/pratt.py`. Do not edit that region by hand; regenerate it in place with: - python3 scripts/gen_pratt.py \ - --prime 21888242871839275222246405745257275088548364400416034343698204186575808495617 \ - --update Lampe/Lampe/Crypto/Bn254/Prime.lean + python3 scripts/gen/pratt.py Lampe/Lampe/Crypto/Bn254/Prime.lean Everything outside the markers is hand-maintained. @@ -29,8 +27,8 @@ should import this file. Files that only use BN254 algebraic facts namespace Lampe.Crypto.Bn254 --- BEGIN generated Pratt certificate (scripts/gen_pratt.py) -- --- Do not edit between the markers; regenerate with `scripts/gen_pratt.py --update`. +-- BEGIN generated Pratt certificate -- +-- Do not edit between the markers; regenerate with `scripts/gen/pratt.py `. /-! ### Pratt certificate Each `prime_

` lemma proves `Nat.Prime

` via Mathlib's @@ -334,7 +332,6 @@ private theorem prime_2188824287183927522224640574525727508854836440041603434369 -- hrest : q ∣ 13818364434197438864469338081^1 rw [(Nat.prime_dvd_prime_iff_eq hq h13818364434197438864469338081).mp hrest] native_decide - -- END generated Pratt certificate -- /-- The BN254 scalar-field prime, definitionally `r_scalar`. -/ 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/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)) := diff --git a/Lampe/Lampe/Crypto/Secp256k1.lean b/Lampe/Lampe/Crypto/Secp256k1.lean index 6eda7af8..2583b95b 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,75 +37,12 @@ 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 - -/-! ### 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 + (msgHash : Array (BitVec 8)) : Bool := + Ecdsa.verifyBytes (W := W) orderN G pkX pkY sig msgHash end Lampe.Crypto.Secp256k1 diff --git a/Lampe/Lampe/Crypto/Secp256k1/Prime.lean b/Lampe/Lampe/Crypto/Secp256k1/Prime.lean index 013a1f89..86150016 100644 --- a/Lampe/Lampe/Crypto/Secp256k1/Prime.lean +++ b/Lampe/Lampe/Crypto/Secp256k1/Prime.lean @@ -6,12 +6,10 @@ import Mathlib.Tactic.NormNum.Prime # Secp256k1 field-prime Pratt primality certificate The Pratt-certificate section of this file (between the BEGIN/END -markers below) is **mechanically generated by** `scripts/gen_pratt.py`. +markers below) is **mechanically generated by** `scripts/gen/pratt.py`. Do not edit that region by hand; regenerate it in place with: - python3 scripts/gen_pratt.py \ - --prime 115792089237316195423570985008687907853269984665640564039457584007908834671663 \ - --update Lampe/Lampe/Crypto/Secp256k1/Prime.lean + python3 scripts/gen/pratt.py Lampe/Lampe/Crypto/Secp256k1/Prime.lean Everything outside the markers is hand-maintained. @@ -24,8 +22,8 @@ It provides: namespace Lampe.Crypto.Secp256k1 --- BEGIN generated Pratt certificate (scripts/gen_pratt.py) -- --- Do not edit between the markers; regenerate with `scripts/gen_pratt.py --update`. +-- BEGIN generated Pratt certificate -- +-- Do not edit between the markers; regenerate with `scripts/gen/pratt.py `. /-! ### Pratt certificate Each `prime_

` lemma proves `Nat.Prime

` via Mathlib's @@ -334,7 +332,6 @@ private theorem prime_1157920892373161954235709850086879078532699846656405640394 -- hrest : q ∣ 205115282021455665897114700593932402728804164701536103180137503955397371^1 rw [(Nat.prime_dvd_prime_iff_eq hq h205115282021455665897114700593932402728804164701536103180137503955397371).mp hrest] native_decide - -- END generated Pratt certificate -- /-- The Secp256k1 field prime literal. -/ diff --git a/Lampe/Lampe/Crypto/Secp256r1.lean b/Lampe/Lampe/Crypto/Secp256r1.lean index 1a4ca3fd..c01d93a2 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,72 +41,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 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 - -/-! ### 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 + (msgHash : Array (BitVec 8)) : Bool := + Ecdsa.verifyBytes (W := W) orderN G pkX pkY sig msgHash end Lampe.Crypto.Secp256r1 diff --git a/Lampe/Lampe/Crypto/Secp256r1/Prime.lean b/Lampe/Lampe/Crypto/Secp256r1/Prime.lean index 616c6878..8e93130f 100644 --- a/Lampe/Lampe/Crypto/Secp256r1/Prime.lean +++ b/Lampe/Lampe/Crypto/Secp256r1/Prime.lean @@ -6,12 +6,10 @@ import Mathlib.Tactic.NormNum.Prime # Secp256r1 field-prime Pratt primality certificate The Pratt-certificate section of this file (between the BEGIN/END -markers below) is **mechanically generated by** `scripts/gen_pratt.py`. +markers below) is **mechanically generated by** `scripts/gen/pratt.py`. Do not edit that region by hand; regenerate it in place with: - python3 scripts/gen_pratt.py \ - --prime 115792089210356248762697446949407573530086143415290314195533631308867097853951 \ - --update Lampe/Lampe/Crypto/Secp256r1/Prime.lean + python3 scripts/gen/pratt.py Lampe/Lampe/Crypto/Secp256r1/Prime.lean Everything outside the markers is hand-maintained. @@ -24,8 +22,8 @@ It provides: namespace Lampe.Crypto.Secp256r1 --- BEGIN generated Pratt certificate (scripts/gen_pratt.py) -- --- Do not edit between the markers; regenerate with `scripts/gen_pratt.py --update`. +-- BEGIN generated Pratt certificate -- +-- Do not edit between the markers; regenerate with `scripts/gen/pratt.py `. /-! ### Pratt certificate Each `prime_

` lemma proves `Nat.Prime

` via Mathlib's @@ -368,7 +366,6 @@ private theorem prime_1157920892103562487626974469494075735300861434152903141955 -- hrest : q ∣ 835945042244614951780389953367877943453916927241^1 rw [(Nat.prime_dvd_prime_iff_eq hq h835945042244614951780389953367877943453916927241).mp hrest] native_decide - -- END generated Pratt certificate -- /-- The Secp256r1 field prime literal. -/ diff --git a/Lampe/Lampe/Crypto/Sha256.lean b/Lampe/Lampe/Crypto/Sha256.lean index e37f837b..795ccad8 100644 --- a/Lampe/Lampe/Crypto/Sha256.lean +++ b/Lampe/Lampe/Crypto/Sha256.lean @@ -1,3 +1,4 @@ +import Lampe.Crypto.WordUtils import Lampe.Tp /-! @@ -21,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). @@ -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. -/ @@ -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/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 diff --git a/Lampe/Tests/Aes128.lean b/Lampe/Tests/Aes128.lean index 014e7132..03d72d15 100644 --- a/Lampe/Tests/Aes128.lean +++ b/Lampe/Tests/Aes128.lean @@ -15,7 +15,7 @@ The third vector is **NIST SP 800-38A Appendix F.2.1** ("CBC-AES128.Encrypt"): the encryption of a full PKCS#7 padding block (0x10 × 16) — which is what our wrapper produces and what every conformant AES-128-CBC + PKCS#7 implementation produces (verified against the `cryptography` - library in `scripts/aes128_ref.py`). + library in `scripts/gen/aes128_ref.py`). Reference: NIST SP 800-38A, https://nvlpubs.nist.gov/nistpubs/Legacy/SP/nistspecialpublication800-38a.pdf @@ -25,6 +25,7 @@ namespace Tests.Aes128 open Lampe.Crypto.Aes128 +-- BEGIN generated aes128 test vectors -- /-! ### Vector 1: empty input — pure padding block -/ -- Empty input — full 16-byte PKCS#7 padding block (0x10 × 16). @@ -32,7 +33,7 @@ private def emptyKey : List.Vector (BitVec 8) 16 := ⟨[0x2b#8, 0x7e#8, 0x15#8, private def emptyIv : List.Vector (BitVec 8) 16 := ⟨[0x00#8, 0x01#8, 0x02#8, 0x03#8, 0x04#8, 0x05#8, 0x06#8, 0x07#8, 0x08#8, 0x09#8, 0x0a#8, 0x0b#8, 0x0c#8, 0x0d#8, 0x0e#8, 0x0f#8], by decide⟩ private def emptyIn : List.Vector (BitVec 8) 0 := ⟨[], by decide⟩ private def emptyOut : List.Vector (BitVec 8) 16 := ⟨[0xc8#8, 0x4a#8, 0xf0#8, 0xb6#8, 0x13#8, 0x43#8, 0x5d#8, 0x5d#8, 0x91#8, 0x82#8, 0x80#8, 0x1a#8, 0x9b#8, 0xd9#8, 0x32#8, 0x0b#8], by decide⟩ -theorem aes128_empty_correct : +example : (aes128CbcEncryptPkcs7 emptyKey emptyIv emptyIn).toList = emptyOut.toList := by native_decide /-! ### Vector 2: one full block — adds full 0x10×16 padding block -/ @@ -42,7 +43,7 @@ private def oneBlockKey : List.Vector (BitVec 8) 16 := ⟨[0x2b#8, 0x7e#8, 0x15# private def oneBlockIv : List.Vector (BitVec 8) 16 := ⟨[0x00#8, 0x01#8, 0x02#8, 0x03#8, 0x04#8, 0x05#8, 0x06#8, 0x07#8, 0x08#8, 0x09#8, 0x0a#8, 0x0b#8, 0x0c#8, 0x0d#8, 0x0e#8, 0x0f#8], by decide⟩ private def oneBlockIn : List.Vector (BitVec 8) 16 := ⟨[0x6b#8, 0xc1#8, 0xbe#8, 0xe2#8, 0x2e#8, 0x40#8, 0x9f#8, 0x96#8, 0xe9#8, 0x3d#8, 0x7e#8, 0x11#8, 0x73#8, 0x93#8, 0x17#8, 0x2a#8], by decide⟩ private def oneBlockOut : List.Vector (BitVec 8) 32 := ⟨[0x76#8, 0x49#8, 0xab#8, 0xac#8, 0x81#8, 0x19#8, 0xb2#8, 0x46#8, 0xce#8, 0xe9#8, 0x8e#8, 0x9b#8, 0x12#8, 0xe9#8, 0x19#8, 0x7d#8, 0x89#8, 0x64#8, 0xe0#8, 0xb1#8, 0x49#8, 0xc1#8, 0x0b#8, 0x7b#8, 0x68#8, 0x2e#8, 0x6e#8, 0x39#8, 0xaa#8, 0xeb#8, 0x73#8, 0x1c#8], by decide⟩ -theorem aes128_oneBlock_correct : +example : (aes128CbcEncryptPkcs7 oneBlockKey oneBlockIv oneBlockIn).toList = oneBlockOut.toList := by native_decide /-! ### Vector 3: NIST SP 800-38A §F.2.1 (canonical anchor) -/ @@ -54,7 +55,7 @@ private def nistF21Key : List.Vector (BitVec 8) 16 := ⟨[0x2b#8, 0x7e#8, 0x15#8 private def nistF21Iv : List.Vector (BitVec 8) 16 := ⟨[0x00#8, 0x01#8, 0x02#8, 0x03#8, 0x04#8, 0x05#8, 0x06#8, 0x07#8, 0x08#8, 0x09#8, 0x0a#8, 0x0b#8, 0x0c#8, 0x0d#8, 0x0e#8, 0x0f#8], by decide⟩ private def nistF21In : List.Vector (BitVec 8) 64 := ⟨[0x6b#8, 0xc1#8, 0xbe#8, 0xe2#8, 0x2e#8, 0x40#8, 0x9f#8, 0x96#8, 0xe9#8, 0x3d#8, 0x7e#8, 0x11#8, 0x73#8, 0x93#8, 0x17#8, 0x2a#8, 0xae#8, 0x2d#8, 0x8a#8, 0x57#8, 0x1e#8, 0x03#8, 0xac#8, 0x9c#8, 0x9e#8, 0xb7#8, 0x6f#8, 0xac#8, 0x45#8, 0xaf#8, 0x8e#8, 0x51#8, 0x30#8, 0xc8#8, 0x1c#8, 0x46#8, 0xa3#8, 0x5c#8, 0xe4#8, 0x11#8, 0xe5#8, 0xfb#8, 0xc1#8, 0x19#8, 0x1a#8, 0x0a#8, 0x52#8, 0xef#8, 0xf6#8, 0x9f#8, 0x24#8, 0x45#8, 0xdf#8, 0x4f#8, 0x9b#8, 0x17#8, 0xad#8, 0x2b#8, 0x41#8, 0x7b#8, 0xe6#8, 0x6c#8, 0x37#8, 0x10#8], by decide⟩ private def nistF21Out : List.Vector (BitVec 8) 80 := ⟨[0x76#8, 0x49#8, 0xab#8, 0xac#8, 0x81#8, 0x19#8, 0xb2#8, 0x46#8, 0xce#8, 0xe9#8, 0x8e#8, 0x9b#8, 0x12#8, 0xe9#8, 0x19#8, 0x7d#8, 0x50#8, 0x86#8, 0xcb#8, 0x9b#8, 0x50#8, 0x72#8, 0x19#8, 0xee#8, 0x95#8, 0xdb#8, 0x11#8, 0x3a#8, 0x91#8, 0x76#8, 0x78#8, 0xb2#8, 0x73#8, 0xbe#8, 0xd6#8, 0xb8#8, 0xe3#8, 0xc1#8, 0x74#8, 0x3b#8, 0x71#8, 0x16#8, 0xe6#8, 0x9e#8, 0x22#8, 0x22#8, 0x95#8, 0x16#8, 0x3f#8, 0xf1#8, 0xca#8, 0xa1#8, 0x68#8, 0x1f#8, 0xac#8, 0x09#8, 0x12#8, 0x0e#8, 0xca#8, 0x30#8, 0x75#8, 0x86#8, 0xe1#8, 0xa7#8, 0x8c#8, 0xb8#8, 0x28#8, 0x07#8, 0x23#8, 0x0e#8, 0x13#8, 0x21#8, 0xd3#8, 0xfa#8, 0xe0#8, 0x0d#8, 0x18#8, 0xcc#8, 0x20#8, 0x12#8], by decide⟩ -theorem aes128_nistF21_correct : +example : (aes128CbcEncryptPkcs7 nistF21Key nistF21Iv nistF21In).toList = nistF21Out.toList := by native_decide /-! ### Vector 4: non-aligned 17-byte input -/ @@ -64,7 +65,7 @@ private def partialBlockKey : List.Vector (BitVec 8) 16 := ⟨[0x2b#8, 0x7e#8, 0 private def partialBlockIv : List.Vector (BitVec 8) 16 := ⟨[0x00#8, 0x01#8, 0x02#8, 0x03#8, 0x04#8, 0x05#8, 0x06#8, 0x07#8, 0x08#8, 0x09#8, 0x0a#8, 0x0b#8, 0x0c#8, 0x0d#8, 0x0e#8, 0x0f#8], by decide⟩ private def partialBlockIn : List.Vector (BitVec 8) 17 := ⟨[0x6b#8, 0xc1#8, 0xbe#8, 0xe2#8, 0x2e#8, 0x40#8, 0x9f#8, 0x96#8, 0xe9#8, 0x3d#8, 0x7e#8, 0x11#8, 0x73#8, 0x93#8, 0x17#8, 0x2a#8, 0xae#8], by decide⟩ private def partialBlockOut : List.Vector (BitVec 8) 32 := ⟨[0x76#8, 0x49#8, 0xab#8, 0xac#8, 0x81#8, 0x19#8, 0xb2#8, 0x46#8, 0xce#8, 0xe9#8, 0x8e#8, 0x9b#8, 0x12#8, 0xe9#8, 0x19#8, 0x7d#8, 0x34#8, 0xd2#8, 0xd2#8, 0x60#8, 0x17#8, 0x31#8, 0x13#8, 0x00#8, 0x8c#8, 0x28#8, 0x11#8, 0x2c#8, 0x77#8, 0x66#8, 0x8c#8, 0x86#8], by decide⟩ -theorem aes128_partialBlock_correct : +example : (aes128CbcEncryptPkcs7 partialBlockKey partialBlockIv partialBlockIn).toList = partialBlockOut.toList := by native_decide /-! ### Vector 5: single byte -/ @@ -74,7 +75,8 @@ private def oneByteKey : List.Vector (BitVec 8) 16 := ⟨[0x2b#8, 0x7e#8, 0x15#8 private def oneByteIv : List.Vector (BitVec 8) 16 := ⟨[0x00#8, 0x01#8, 0x02#8, 0x03#8, 0x04#8, 0x05#8, 0x06#8, 0x07#8, 0x08#8, 0x09#8, 0x0a#8, 0x0b#8, 0x0c#8, 0x0d#8, 0x0e#8, 0x0f#8], by decide⟩ private def oneByteIn : List.Vector (BitVec 8) 1 := ⟨[0x00#8], by decide⟩ private def oneByteOut : List.Vector (BitVec 8) 16 := ⟨[0x34#8, 0x0f#8, 0x12#8, 0x17#8, 0x40#8, 0x5b#8, 0x87#8, 0x8d#8, 0x04#8, 0x73#8, 0xc8#8, 0x7d#8, 0xc8#8, 0xca#8, 0xa8#8, 0xee#8], by decide⟩ -theorem aes128_oneByte_correct : +example : (aes128CbcEncryptPkcs7 oneByteKey oneByteIv oneByteIn).toList = oneByteOut.toList := by native_decide +-- END generated aes128 test vectors -- end Tests.Aes128 diff --git a/Lampe/Tests/Blake2s.lean b/Lampe/Tests/Blake2s.lean index 3f6959cf..ac0107eb 100644 --- a/Lampe/Tests/Blake2s.lean +++ b/Lampe/Tests/Blake2s.lean @@ -14,51 +14,41 @@ length-parametric cases. Lengths cover empty, the RFC `"abc"` vector, exactly one full BLAKE2s block (64 bytes), and one byte past the block boundary (65 bytes). -Regenerate with `scripts/blake2s_ref.py`. +Regenerate with `scripts/gen/blake2s_ref.py`. -/ namespace Tests.Blake2s open Lampe.Crypto.Blake2s +-- BEGIN generated blake2s test vectors -- -- empty: RFC 7693 reference, input length = 0 private def emptyIn : Array (BitVec 8) := #[] private def emptyOut : Array (BitVec 8) := - #[0x69#8, 0x21#8, 0x7a#8, 0x30#8, 0x79#8, 0x90#8, 0x80#8, 0x94#8, - 0xe1#8, 0x11#8, 0x21#8, 0xd0#8, 0x42#8, 0x35#8, 0x4a#8, 0x7c#8, - 0x1f#8, 0x55#8, 0xb6#8, 0x48#8, 0x2c#8, 0xa1#8, 0xa5#8, 0x1e#8, - 0x1b#8, 0x25#8, 0x0d#8, 0xfd#8, 0x1e#8, 0xd0#8, 0xee#8, 0xf9#8] + #[0x69#8, 0x21#8, 0x7a#8, 0x30#8, 0x79#8, 0x90#8, 0x80#8, 0x94#8, 0xe1#8, 0x11#8, 0x21#8, 0xd0#8, 0x42#8, 0x35#8, 0x4a#8, 0x7c#8, 0x1f#8, 0x55#8, 0xb6#8, 0x48#8, 0x2c#8, 0xa1#8, 0xa5#8, 0x1e#8, 0x1b#8, 0x25#8, 0x0d#8, 0xfd#8, 0x1e#8, 0xd0#8, 0xee#8, 0xf9#8] example : blake2sHashBytes emptyIn = emptyOut := by native_decide -- abc: RFC 7693 reference, input length = 3 private def abcIn : Array (BitVec 8) := #[0x61#8, 0x62#8, 0x63#8] private def abcOut : Array (BitVec 8) := - #[0x50#8, 0x8c#8, 0x5e#8, 0x8c#8, 0x32#8, 0x7c#8, 0x14#8, 0xe2#8, - 0xe1#8, 0xa7#8, 0x2b#8, 0xa3#8, 0x4e#8, 0xeb#8, 0x45#8, 0x2f#8, - 0x37#8, 0x45#8, 0x8b#8, 0x20#8, 0x9e#8, 0xd6#8, 0x3a#8, 0x29#8, - 0x4d#8, 0x99#8, 0x9b#8, 0x4c#8, 0x86#8, 0x67#8, 0x59#8, 0x82#8] + #[0x50#8, 0x8c#8, 0x5e#8, 0x8c#8, 0x32#8, 0x7c#8, 0x14#8, 0xe2#8, 0xe1#8, 0xa7#8, 0x2b#8, 0xa3#8, 0x4e#8, 0xeb#8, 0x45#8, 0x2f#8, 0x37#8, 0x45#8, 0x8b#8, 0x20#8, 0x9e#8, 0xd6#8, 0x3a#8, 0x29#8, 0x4d#8, 0x99#8, 0x9b#8, 0x4c#8, 0x86#8, 0x67#8, 0x59#8, 0x82#8] example : blake2sHashBytes abcIn = abcOut := by native_decide -- oneBlock: exactly one full BLAKE2s message block, input length = 64 private def oneBlockIn : Array (BitVec 8) := ((List.range 64).map (fun i => BitVec.ofNat 8 (i % 251))).toArray private def oneBlockOut : Array (BitVec 8) := - #[0x56#8, 0xf3#8, 0x4e#8, 0x8b#8, 0x96#8, 0x55#8, 0x7e#8, 0x90#8, - 0xc1#8, 0xf2#8, 0x4b#8, 0x52#8, 0xd0#8, 0xc8#8, 0x9d#8, 0x51#8, - 0x08#8, 0x6a#8, 0xcf#8, 0x1b#8, 0x00#8, 0xf6#8, 0x34#8, 0xcf#8, - 0x1d#8, 0xde#8, 0x92#8, 0x33#8, 0xb8#8, 0xea#8, 0xaa#8, 0x3e#8] + #[0x56#8, 0xf3#8, 0x4e#8, 0x8b#8, 0x96#8, 0x55#8, 0x7e#8, 0x90#8, 0xc1#8, 0xf2#8, 0x4b#8, 0x52#8, 0xd0#8, 0xc8#8, 0x9d#8, 0x51#8, 0x08#8, 0x6a#8, 0xcf#8, 0x1b#8, 0x00#8, 0xf6#8, 0x34#8, 0xcf#8, 0x1d#8, 0xde#8, 0x92#8, 0x33#8, 0xb8#8, 0xea#8, 0xaa#8, 0x3e#8] example : blake2sHashBytes oneBlockIn = oneBlockOut := by native_decide -- overBlock: one byte past block boundary (two compressions), input length = 65 private def overBlockIn : Array (BitVec 8) := ((List.range 65).map (fun i => BitVec.ofNat 8 (i % 251))).toArray private def overBlockOut : Array (BitVec 8) := - #[0x1b#8, 0x53#8, 0xee#8, 0x94#8, 0xaa#8, 0xf3#8, 0x4e#8, 0x4b#8, - 0x15#8, 0x9d#8, 0x48#8, 0xde#8, 0x35#8, 0x2c#8, 0x7f#8, 0x06#8, - 0x61#8, 0xd0#8, 0xa4#8, 0x0e#8, 0xdf#8, 0xf9#8, 0x5a#8, 0x0b#8, - 0x16#8, 0x39#8, 0xb4#8, 0x09#8, 0x0e#8, 0x97#8, 0x44#8, 0x72#8] + #[0x1b#8, 0x53#8, 0xee#8, 0x94#8, 0xaa#8, 0xf3#8, 0x4e#8, 0x4b#8, 0x15#8, 0x9d#8, 0x48#8, 0xde#8, 0x35#8, 0x2c#8, 0x7f#8, 0x06#8, 0x61#8, 0xd0#8, 0xa4#8, 0x0e#8, 0xdf#8, 0xf9#8, 0x5a#8, 0x0b#8, 0x16#8, 0x39#8, 0xb4#8, 0x09#8, 0x0e#8, 0x97#8, 0x44#8, 0x72#8] example : blake2sHashBytes overBlockIn = overBlockOut := by native_decide +-- END generated blake2s test vectors -- end Tests.Blake2s diff --git a/Lampe/Tests/Blake3.lean b/Lampe/Tests/Blake3.lean index 0d771314..e5b00c4c 100644 --- a/Lampe/Tests/Blake3.lean +++ b/Lampe/Tests/Blake3.lean @@ -13,13 +13,14 @@ Inputs follow the canonical BLAKE3 test-vector convention `input[i] = i % 251`. Lengths cover empty input, sub-block, block-boundary, chunk-boundary, and multi-chunk tree cases. -Regenerate with `scripts/blake3_ref.py`. +Regenerate with `scripts/gen/blake3_ref.py`. -/ namespace Tests.Blake3 open Lampe.Crypto.Blake3 +-- BEGIN generated blake3 test vectors -- -- empty: input = [i % 251 for i in 0..0], len = 0 private def emptyIn : Array (BitVec 8) := #[] @@ -82,5 +83,6 @@ private def twoChunksIn : Array (BitVec 8) := private def twoChunksOut : Array (BitVec 8) := #[0xe7#8, 0x76#8, 0xb6#8, 0x02#8, 0x8c#8, 0x7c#8, 0xd2#8, 0x2a#8, 0x4d#8, 0x0b#8, 0xa1#8, 0x82#8, 0xa8#8, 0xbf#8, 0x62#8, 0x20#8, 0x5d#8, 0x2e#8, 0xf5#8, 0x76#8, 0x46#8, 0x7e#8, 0x83#8, 0x8e#8, 0xd6#8, 0xf2#8, 0x52#8, 0x9b#8, 0x85#8, 0xfb#8, 0xa2#8, 0x4a#8] example : blake3HashBytes twoChunksIn = twoChunksOut := by native_decide +-- END generated blake3 test vectors -- end Tests.Blake3 diff --git a/Lampe/Tests/Ecdsa.lean b/Lampe/Tests/Ecdsa.lean new file mode 100644 index 00000000..32996b64 --- /dev/null +++ b/Lampe/Tests/Ecdsa.lean @@ -0,0 +1,89 @@ +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/gen/secp256k1_ref.py` / `scripts/gen/secp256r1_ref.py`. +-/ + +namespace Tests.Ecdsa + +/-! ### secp256k1 -/ + +namespace Secp256k1 + +open Lampe.Crypto.Secp256k1 + +-- BEGIN generated secp256k1 test vectors -- +-- 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 generated secp256k1 test vectors -- + +end Secp256k1 + +/-! ### secp256r1 / NIST P-256 -/ + +namespace Secp256r1 + +open Lampe.Crypto.Secp256r1 + +-- BEGIN generated secp256r1 test vectors -- +-- 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 generated secp256r1 test vectors -- + +end Secp256r1 + +end Tests.Ecdsa 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 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). -/ diff --git a/scripts/blake2s_ref.py b/scripts/blake2s_ref.py deleted file mode 100755 index d2e51c50..00000000 --- a/scripts/blake2s_ref.py +++ /dev/null @@ -1,71 +0,0 @@ -#!/usr/bin/env python3 -"""Reference BLAKE2s test vector generator. - -Uses Python's stdlib `hashlib.blake2s`, which is a thin wrapper around -the BLAKE2 reference implementation (libb2). No external dependency. - -BLAKE2s is the 32-bit variant of BLAKE2 with a 32-byte digest and a -64-byte (16 u32 words) message block. This script emits Lean array -literals matching the format Lampe's `Crypto.Blake2s` test vectors -expect (see `Lampe/Lampe/Crypto/Blake2s.lean`). - -Reference: RFC 7693 (Appendix A.1 has the BLAKE2s test vector for -"abc"). - -Inputs chosen to cover key boundaries in the algorithm: - empty : 0 bytes (no data, just the IV-XOR-parameter-block - finalisation) - abc : the canonical RFC 7693 test vector - oneBlock : 64 bytes (exactly one BLAKE2s message block) - overBlock : 65 bytes (just past block boundary, exercises the - two-block path with non-aligned final block length) - -Lampe's concrete BLAKE2s implementation is validated against these -vectors via `native_decide`. -""" - -import hashlib - - -def lean_byte(b: int) -> str: - return f"0x{b:02x}#8" - - -def emit_vector(name: str, inp: bytes, description: str) -> None: - digest = hashlib.blake2s(inp).digest() - in_lanes = ", ".join(lean_byte(b) for b in inp) - out_lanes = ", ".join(lean_byte(b) for b in digest) - - print(f"-- {name}: {description}, input length = {len(inp)}") - print(f"private def {name}In : Array (BitVec 8) :=") - if len(inp) == 0: - print(f" #[]") - elif len(inp) <= 16: - print(f" #[{in_lanes}]") - else: - # Use canonical i % 251 formulation for the boundary-length - # inputs so the literal is short and human-readable. - print( - f" ((List.range {len(inp)}).map " - f"(fun i => BitVec.ofNat 8 (i % 251))).toArray" - ) - print(f"private def {name}Out : Array (BitVec 8) :=") - print(f" #[{out_lanes}]") - print(f"theorem blake2s_{name}_correct :") - print(f" blake2sHashBytes {name}In = {name}Out := by native_decide") - print() - - -# Vectors for native_decide tests. -emit_vector("empty", b"", "RFC 7693 reference empty-input hash") -emit_vector("abc", b"abc", "RFC 7693 reference 'abc' hash") -emit_vector( - "oneBlock", - bytes(i % 251 for i in range(64)), - "exactly one full BLAKE2s message block", -) -emit_vector( - "overBlock", - bytes(i % 251 for i in range(65)), - "one byte past block boundary (two compressions)", -) diff --git a/scripts/gen/_lean.py b/scripts/gen/_lean.py new file mode 100644 index 00000000..3e53f0ad --- /dev/null +++ b/scripts/gen/_lean.py @@ -0,0 +1,67 @@ +"""Shared helper for in-place Lean artifact generators. + +`update_region` rewrites only the text strictly between a pair of marker +comments: + + -- BEGIN generated {label} -- + -- END generated {label} -- + +Everything outside the markers (header docstring, namespace, hand-written +defs) is left untouched. Re-running with the same body is a no-op. +""" + +import sys + + +def _marker(kind: str, label: str) -> str: + return f"-- {kind} generated {label} --" + + +def _find_unique(text: str, marker: str, path: str) -> int: + first = text.find(marker) + if first == -1: + print(f"error: marker {marker!r} not found in {path}", file=sys.stderr) + sys.exit(1) + if text.find(marker, first + len(marker)) != -1: + print( + f"error: marker {marker!r} appears more than once in {path}", + file=sys.stderr, + ) + sys.exit(1) + return first + + +def update_region(path: str, body: str, *, label: str) -> None: + """Replace the text between the `{label}` markers in `path` with `body`. + + The body is wrapped with a single blank-line gap from the markers and + exactly one trailing newline, so repeated runs converge. + """ + begin = _marker("BEGIN", label) + end = _marker("END", label) + + with open(path, encoding="utf-8") as f: + text = f.read() + + begin_at = _find_unique(text, begin, path) + end_at = _find_unique(text, end, path) + if end_at < begin_at: + print( + f"error: END marker precedes BEGIN marker for {label!r} in {path}", + file=sys.stderr, + ) + sys.exit(1) + + prefix = text[: begin_at + len(begin)] + suffix = text[end_at:] + + new_region = "\n" + body.strip("\n") + "\n" + new_text = prefix + new_region + suffix + + if new_text == text: + print(f"{path}: up to date", file=sys.stderr) + return + + with open(path, "w", encoding="utf-8") as f: + f.write(new_text) + print(f"{path}: regenerated {label}", file=sys.stderr) diff --git a/scripts/aes128_ref.py b/scripts/gen/aes128_ref.py similarity index 50% rename from scripts/aes128_ref.py rename to scripts/gen/aes128_ref.py index 999d81ea..4d627058 100644 --- a/scripts/aes128_ref.py +++ b/scripts/gen/aes128_ref.py @@ -11,11 +11,18 @@ example): for `key = 2b7e151628aed2a6abf7158809cf4f3c`, `IV = 000102030405060708090a0b0c0d0e0f`, plaintext = the four 16-byte blocks given in §F.2.1, ciphertext blocks -match what F.2.1 publishes. (Our wrapper additionally appends a 16-byte +match what F.2.1 publishes. (The wrapper additionally appends a 16-byte PKCS#7 padding block; the F.2.1 blocks themselves are still the prefix of the verified output.) + +Usage: + python3 scripts/gen/aes128_ref.py """ +import sys + +from _lean import update_region + from cryptography.hazmat.primitives.ciphers import Cipher, algorithms, modes from cryptography.hazmat.primitives import padding @@ -47,10 +54,7 @@ def aes128_cbc_pkcs7(key: bytes, iv: bytes, pt: bytes) -> bytes: return enc.update(padded) + enc.finalize() -# Sanity: verify our toolchain reproduces NIST §F.2.1 (the raw, -# unpadded portion). Since we pad with PKCS#7 the output will be one -# block longer; truncating that to the first 64 bytes must equal -# NIST_CT_F21_RAW. +# Sanity: the toolchain reproduces NIST §F.2.1 (raw, unpadded portion). _check = aes128_cbc_pkcs7(NIST_KEY, NIST_IV, NIST_PT_F21) assert _check[:64] == NIST_CT_F21_RAW, "NIST SP 800-38A F.2.1 mismatch" @@ -63,51 +67,77 @@ def fmt_bytes(b: bytes) -> str: return "[" + ", ".join(fmt_byte(v) for v in b) + "]" -def emit_vector(name: str, key: bytes, iv: bytes, pt: bytes, comment: str = ""): +def vector_lines(name: str, key: bytes, iv: bytes, pt: bytes, + section: str, comment: str) -> list[str]: ct = aes128_cbc_pkcs7(key, iv, pt) n_in = len(pt) n_out = len(ct) - if comment: - print(f"-- {comment}") - print(f"private def {name}Key : List.Vector (BitVec 8) 16 := ⟨{fmt_bytes(key)}, by decide⟩") - print(f"private def {name}Iv : List.Vector (BitVec 8) 16 := ⟨{fmt_bytes(iv)}, by decide⟩") - print(f"private def {name}In : List.Vector (BitVec 8) {n_in} := ⟨{fmt_bytes(pt)}, by decide⟩") - print(f"private def {name}Out : List.Vector (BitVec 8) {n_out} := ⟨{fmt_bytes(ct)}, by decide⟩") - print(f"theorem aes128_{name}_correct :") - print(f" (aes128CbcEncryptPkcs7 {name}Key {name}Iv {name}In).toList = {name}Out.toList := by native_decide") - print() + lines = [f"/-! {section} -/", ""] + lines.extend(comment.splitlines()) + lines.append( + f"private def {name}Key : List.Vector (BitVec 8) 16 := ⟨{fmt_bytes(key)}, by decide⟩" + ) + lines.append( + f"private def {name}Iv : List.Vector (BitVec 8) 16 := ⟨{fmt_bytes(iv)}, by decide⟩" + ) + lines.append( + f"private def {name}In : List.Vector (BitVec 8) {n_in} := ⟨{fmt_bytes(pt)}, by decide⟩" + ) + lines.append( + f"private def {name}Out : List.Vector (BitVec 8) {n_out} := ⟨{fmt_bytes(ct)}, by decide⟩" + ) + lines.append(f"example :") + lines.append( + f" (aes128CbcEncryptPkcs7 {name}Key {name}Iv {name}In).toList " + f"= {name}Out.toList := by native_decide" + ) + return lines -def main(): - # Vector 1: empty input — pure padding block. - emit_vector( +VECTORS = [ + ( "empty", NIST_KEY, NIST_IV, b"", - "Empty input — full 16-byte PKCS#7 padding block (0x10 × 16).", - ) - - # Vector 2: one full block (16 bytes) — adds a full padding block. - emit_vector( + "### Vector 1: empty input — pure padding block", + "-- Empty input — full 16-byte PKCS#7 padding block (0x10 × 16).", + ), + ( "oneBlock", NIST_KEY, NIST_IV, NIST_PT_F21[:16], - "Single 16-byte block; PKCS#7 still appends a full 0x10×16 padding block.", - ) - - # Vector 3: NIST SP 800-38A §F.2.1 four-block plaintext. - emit_vector( + "### Vector 2: one full block — adds full 0x10×16 padding block", + "-- Single 16-byte block; PKCS#7 still appends a full 0x10×16 padding block.", + ), + ( "nistF21", NIST_KEY, NIST_IV, NIST_PT_F21, - "NIST SP 800-38A §F.2.1 AES-128-CBC encryption example.", - ) - - # Vector 4: 17-byte non-aligned input. - emit_vector( + "### Vector 3: NIST SP 800-38A §F.2.1 (canonical anchor)", + "-- NIST SP 800-38A §F.2.1 AES-128-CBC encryption example.\n" + "-- First 64 bytes of expected output match §F.2.1 verbatim; the\n" + "-- trailing 16 bytes are the encryption of the PKCS#7 padding block.", + ), + ( "partialBlock", NIST_KEY, NIST_IV, NIST_PT_F21[:17], - "17-byte input — PKCS#7 pads with 15 × 0x0f to reach 32 bytes.", - ) - - # Vector 5: 1-byte input — tests `padding_length = 15`. - emit_vector( + "### Vector 4: non-aligned 17-byte input", + "-- 17-byte input — PKCS#7 pads with 15 × 0x0f to reach 32 bytes.", + ), + ( "oneByte", NIST_KEY, NIST_IV, b"\x00", - "Single zero byte — pads with 15 × 0x0f.", - ) + "### Vector 5: single byte", + "-- Single zero byte — pads with 15 × 0x0f.", + ), +] + + +def build_body() -> str: + blocks = [ + "\n".join(vector_lines(name, key, iv, pt, section, comment)) + for name, key, iv, pt, section, comment in VECTORS + ] + return "\n\n".join(blocks) + + +def main(): + if len(sys.argv) != 2: + print("usage: aes128_ref.py ", file=sys.stderr) + sys.exit(1) + update_region(sys.argv[1], build_body(), label="aes128 test vectors") if __name__ == "__main__": diff --git a/scripts/gen/blake2s_ref.py b/scripts/gen/blake2s_ref.py new file mode 100755 index 00000000..f26a854d --- /dev/null +++ b/scripts/gen/blake2s_ref.py @@ -0,0 +1,84 @@ +#!/usr/bin/env python3 +"""Reference BLAKE2s test vector generator. + +Uses Python's stdlib `hashlib.blake2s`, which is a thin wrapper around +the BLAKE2 reference implementation (libb2). No external dependency. + +BLAKE2s is the 32-bit variant of BLAKE2 with a 32-byte digest and a +64-byte (16 u32 words) message block. + +Reference: RFC 7693 (Appendix A.1 has the BLAKE2s test vector for +"abc"). + +Inputs chosen to cover key boundaries in the algorithm: + empty : 0 bytes (IV-XOR-parameter-block finalisation only) + abc : the canonical RFC 7693 test vector + oneBlock : 64 bytes (exactly one BLAKE2s message block) + overBlock : 65 bytes (just past block boundary, two compressions) + +Lampe's concrete BLAKE2s implementation is validated against these +vectors via `native_decide`. + +Usage: + python3 scripts/gen/blake2s_ref.py +""" + +import hashlib +import sys + +from _lean import update_region + + +def lean_byte(b: int) -> str: + return f"0x{b:02x}#8" + + +def vector_lines(name: str, inp: bytes, description: str) -> list[str]: + digest = hashlib.blake2s(inp).digest() + in_lanes = ", ".join(lean_byte(b) for b in inp) + out_lanes = ", ".join(lean_byte(b) for b in digest) + + lines = [f"-- {name}: {description}, input length = {len(inp)}"] + lines.append(f"private def {name}In : Array (BitVec 8) :=") + if len(inp) == 0: + lines.append(" #[]") + elif len(inp) <= 16: + lines.append(f" #[{in_lanes}]") + else: + # Canonical i % 251 formulation for the boundary-length inputs. + lines.append( + f" ((List.range {len(inp)}).map " + f"(fun i => BitVec.ofNat 8 (i % 251))).toArray" + ) + lines.append(f"private def {name}Out : Array (BitVec 8) :=") + lines.append(f" #[{out_lanes}]") + lines.append( + f"example : blake2sHashBytes {name}In = {name}Out := by native_decide" + ) + return lines + + +VECTORS = [ + ("empty", b"", "RFC 7693 reference"), + ("abc", b"abc", "RFC 7693 reference"), + ("oneBlock", bytes(i % 251 for i in range(64)), + "exactly one full BLAKE2s message block"), + ("overBlock", bytes(i % 251 for i in range(65)), + "one byte past block boundary (two compressions)"), +] + + +def build_body() -> str: + blocks = ["\n".join(vector_lines(n, inp, d)) for n, inp, d in VECTORS] + return "\n\n".join(blocks) + + +def main(): + if len(sys.argv) != 2: + print("usage: blake2s_ref.py ", file=sys.stderr) + sys.exit(1) + update_region(sys.argv[1], build_body(), label="blake2s test vectors") + + +if __name__ == "__main__": + main() diff --git a/scripts/blake3_ref.py b/scripts/gen/blake3_ref.py similarity index 59% rename from scripts/blake3_ref.py rename to scripts/gen/blake3_ref.py index 586045cc..8b744ec1 100644 --- a/scripts/blake3_ref.py +++ b/scripts/gen/blake3_ref.py @@ -9,11 +9,16 @@ input[i] = i % 251 Lampe's concrete BLAKE3 implementation is validated against these -vectors via native_decide theorems. +vectors via `native_decide`. + +Usage: + python3 scripts/gen/blake3_ref.py """ import sys +from _lean import update_region + try: import blake3 except ImportError: @@ -33,43 +38,56 @@ # 2048 : two full chunks (tree depth 1, symmetric) TEST_LENGTHS = [0, 1, 63, 64, 65, 1023, 1024, 1025, 2048] +NAMES = { + 0: "empty", + 1: "oneByte", + 63: "underBlock", + 64: "oneBlock", + 65: "overBlock", + 1023: "underChunk", + 1024: "oneChunk", + 1025: "overChunk", + 2048: "twoChunks", +} + def canonical_input(n: int) -> bytes: return bytes(i % 251 for i in range(n)) -def emit_test_vector(name: str, n: int) -> None: +def lane(b: int) -> str: + return f"0x{b:02x}#8" + + +def vector_lines(name: str, n: int) -> list[str]: inp = canonical_input(n) digest = blake3.blake3(inp).digest() - # Lean BitVec 8 literal: 0xNN#8 - def lane(b): return f"0x{b:02x}#8" out_lanes = ", ".join(lane(b) for b in digest) - print(f"-- {name}: input = [i % 251 for i in 0..{n}], len = {n}") - # Input: use the canonical formula i % 251 rather than 1024+ literals. - print(f"private def {name}In : Array (BitVec 8) :=") + lines = [f"-- {name}: input = [i % 251 for i in 0..{n}], len = {n}"] + lines.append(f"private def {name}In : Array (BitVec 8) :=") if n == 0: - print(f" #[]") + lines.append(" #[]") else: - print(f" ((List.range {n}).map (fun i => BitVec.ofNat 8 (i % 251))).toArray") - print(f"private def {name}Out : Array (BitVec 8) :=") - print(f" #[{out_lanes}]") - print(f"theorem blake3_{name}_correct :") - print(f" blake3HashBytes {name}In = {name}Out := by native_decide") - print() + lines.append( + f" ((List.range {n}).map (fun i => BitVec.ofNat 8 (i % 251))).toArray" + ) + lines.append(f"private def {name}Out : Array (BitVec 8) :=") + lines.append(f" #[{out_lanes}]") + lines.append(f"example : blake3HashBytes {name}In = {name}Out := by native_decide") + return lines -# Tag-friendly names for the lengths -NAMES = { - 0: "empty", - 1: "oneByte", - 63: "underBlock", - 64: "oneBlock", - 65: "overBlock", - 1023: "underChunk", - 1024: "oneChunk", - 1025: "overChunk", - 2048: "twoChunks", -} +def build_body() -> str: + blocks = ["\n".join(vector_lines(NAMES[n], n)) for n in TEST_LENGTHS] + return "\n\n".join(blocks) + + +def main(): + if len(sys.argv) != 2: + print("usage: blake3_ref.py ", file=sys.stderr) + sys.exit(1) + update_region(sys.argv[1], build_body(), label="blake3 test vectors") + -for n in TEST_LENGTHS: - emit_test_vector(NAMES[n], n) +if __name__ == "__main__": + main() diff --git a/scripts/gen/pratt.py b/scripts/gen/pratt.py new file mode 100644 index 00000000..4266cddb --- /dev/null +++ b/scripts/gen/pratt.py @@ -0,0 +1,209 @@ +#!/usr/bin/env python3 +"""Pratt primality certificate generator. + +Regenerates the `Nat.Prime

` certificate region of a `Prime.lean` +file in place, using Mathlib's `lucas_primality` theorem applied +recursively to every prime factor of (P-1) that exceeds `norm_num`'s +trial-division threshold. + +The prime `P` is read from the target file's own `def primeNat : Nat :=` +definition (outside the markers). The certificate lives between: + + -- BEGIN generated Pratt certificate -- + ... + -- END generated Pratt certificate -- + +Everything outside the markers is hand-maintained and untouched. + +Usage: + python3 scripts/gen/pratt.py + +Requires: sympy (for factorization and primality oracle). +""" + +import re +import sys + +from _lean import update_region + +try: + from sympy import factorint +except ImportError: + print( + "error: sympy not installed. Install with: " + "pip3 install --user --break-system-packages sympy", + file=sys.stderr, + ) + sys.exit(1) + + +LABEL = "Pratt certificate" +DO_NOT_EDIT_NOTE = ( + "-- Do not edit between the markers; regenerate with" + " `scripts/gen/pratt.py `." +) + +# Named constants the BN254 file uses in place of a decimal literal. +NAMED_PRIMES = { + "r_scalar": 21888242871839275222246405745257275088548364400416034343698204186575808495617, +} + + +def find_generator(p, factors_p_minus_1): + n = p - 1 + for a in range(2, 200): + if pow(a, n, p) != 1: + continue + if all(pow(a, n // q, p) != 1 for q in factors_p_minus_1): + return a + raise RuntimeError(f"no small generator found for prime {p}") + + +def build_nodes(p, nodes): + if p in nodes or p == 2: + return + factors = factorint(p - 1) + nodes[p] = {"generator": find_generator(p, factors), "factors": factors} + for q in factors: + if q > 2 and q.bit_length() > 25: + build_nodes(q, nodes) + + +def factor_product_str(factors): + parts = [str(q) if e == 1 else f"{q}^{e}" for q, e in sorted(factors.items())] + if len(parts) == 1: + return parts[0] + result = parts[-1] + for part in reversed(parts[:-1]): + result = f"{part} * ({result})" + return result + + +def emit_have_block(factors): + lines = [] + for q in sorted(factors.keys()): + if q == 2: + lines.append(f" have h{q} : Nat.Prime {q} := Nat.prime_two") + elif q == 3: + lines.append(f" have h{q} : Nat.Prime {q} := Nat.prime_three") + elif q.bit_length() <= 25: + lines.append(f" have h{q} : Nat.Prime {q} := by norm_num") + else: + lines.append(f" have h{q} : Nat.Prime {q} := prime_{q}") + return lines + + +def emit_case_split(factors): + lines = [] + items = sorted(factors.items()) + + def emit_leaf(indent, hyp, q, e): + if e == 1: + lines.append(f"{indent}rw [(Nat.prime_dvd_prime_iff_eq hq h{q}).mp {hyp}]") + else: + lines.append(f"{indent}have hdvd_q : q ∣ {q} := hq.dvd_of_dvd_pow {hyp}") + lines.append(f"{indent}rw [(Nat.prime_dvd_prime_iff_eq hq h{q}).mp hdvd_q]") + lines.append(f"{indent}native_decide") + + def recurse(indent, items_, hyp): + if len(items_) == 1: + q, e = items_[0] + lines.append(f"{indent}-- {hyp} : q ∣ {q}^{e}") + emit_leaf(indent, hyp, q, e) + return + q, e = items_[0] + rest = items_[1:] + lines.append(f"{indent}rcases (hq.dvd_mul).mp {hyp} with hcase | hrest") + lines.append(f"{indent}· -- q ∣ {q}^{e}") + emit_leaf(indent + " ", "hcase", q, e) + lines.append(f"{indent}· -- q ∣ rest") + recurse(indent + " ", rest, "hrest") + + recurse(" ", items, "hdvd") + return lines + + +def emit_pratt_node(p, n): + factors = n["factors"] + gen = n["generator"] + out = [ + f"private theorem prime_{p} : Nat.Prime {p} := by", + f" refine lucas_primality {p} ({gen} : ZMod {p}) ?_ ?_", + f" · -- {gen}^({p}-1) = 1 mod {p}", + f" native_decide", + f" · intro q hq hdvd", + f" have h_eq : ({p} - 1 : ℕ) = {factor_product_str(factors)} := by decide", + f" rw [h_eq] at hdvd", + ] + out.extend(emit_have_block(factors)) + out.extend(emit_case_split(factors)) + return out + + +def generate_body(P) -> str: + """The text between the BEGIN/END markers.""" + nodes = {} + build_nodes(P, nodes) + + out = [DO_NOT_EDIT_NOTE] + out.append("/-! ### Pratt certificate") + out.append("") + out.append("Each `prime_

` lemma proves `Nat.Prime

` via Mathlib's") + out.append("`lucas_primality`. The certificate tree:") + out.append("") + out.append("```") + for p in sorted(nodes): + n = nodes[p] + out.append( + f" {p} (gen={n['generator']}, p-1 = {factor_product_str(n['factors'])})" + ) + out.append("```") + out.append("") + out.append("Power conditions are discharged by `native_decide`; small prime") + out.append("factors by `norm_num` (Mathlib's trial-division extension).") + out.append("-/") + out.append("") + for p in sorted(nodes): + out.extend(emit_pratt_node(p, nodes[p])) + out.append("") + return "\n".join(out) + + +def read_prime(path: str) -> int: + """Parse the prime from the file's `def primeNat : Nat :=` value.""" + with open(path, encoding="utf-8") as f: + text = f.read() + m = re.search(r"def\s+primeNat\s*:\s*Nat\s*:=\s*([^\n]*)", text) + if not m: + print(f"error: no `def primeNat : Nat :=` found in {path}", file=sys.stderr) + sys.exit(1) + value = m.group(1).strip() + if not value: + # Literal on the next line. + m2 = re.search(r"def\s+primeNat\s*:\s*Nat\s*:=\s*\n\s*([^\n]+)", text) + if not m2: + print(f"error: cannot read primeNat value in {path}", file=sys.stderr) + sys.exit(1) + value = m2.group(1).strip() + if value.isdigit(): + return int(value) + if value in NAMED_PRIMES: + return NAMED_PRIMES[value] + print( + f"error: unrecognized primeNat value {value!r} in {path}", + file=sys.stderr, + ) + sys.exit(1) + + +def main(): + if len(sys.argv) != 2: + print("usage: pratt.py ", file=sys.stderr) + sys.exit(1) + path = sys.argv[1] + P = read_prime(path) + update_region(path, generate_body(P), label=LABEL) + + +if __name__ == "__main__": + main() diff --git a/scripts/gen/requirements.txt b/scripts/gen/requirements.txt new file mode 100644 index 00000000..9debbb62 --- /dev/null +++ b/scripts/gen/requirements.txt @@ -0,0 +1,6 @@ +# Dev-only deps for the reference generators under scripts/. +# Not installed by CI; the CI image bakes scripts/requirements.txt only. +blake3 # blake3_ref.py +cryptography # aes128_ref.py +ecdsa # secp256k1_ref.py, secp256r1_ref.py +sympy # gen_pratt.py diff --git a/scripts/gen/secp256k1_ref.py b/scripts/gen/secp256k1_ref.py new file mode 100644 index 00000000..7fb62a46 --- /dev/null +++ b/scripts/gen/secp256k1_ref.py @@ -0,0 +1,107 @@ +#!/usr/bin/env python3 +"""Reference secp256k1 ECDSA test vector generator. + +Uses the pure-Python `ecdsa` library (pip install ecdsa) which +implements RFC 6979 deterministic signing — so vectors regenerate +identically. + +Emits Lean test vectors comparing + Lampe.Crypto.Secp256k1.verifyBytes pkX pkY sig msgHash +to the expected verification result (`true` for valid signatures, +`false` for tampered ones), checked via `native_decide`. Since +Barretenberg's `__ecdsa_secp256k1` foreign call runs the same FIPS +186-4 verification algorithm, agreement with the Python reference +transitively certifies agreement with Barretenberg. + +Usage: + python3 scripts/gen/secp256k1_ref.py +""" + +import hashlib +import sys + +from _lean import update_region + +try: + from ecdsa import SigningKey, SECP256k1, util +except ImportError: + print("error: pip install --user --break-system-packages ecdsa", file=sys.stderr) + sys.exit(1) + +CURVE = SECP256k1 +LABEL = "secp256k1 test vectors" + + +def bytes_to_lean_array(bs: bytes) -> str: + """Render bytes as a Lean `Array (BitVec 8)` literal.""" + return "#[" + ", ".join(f"0x{b:02x}#8" for b in bs) + "]" + + +def sign(sk_hex: str, msg: bytes): + sk = SigningKey.from_string(bytes.fromhex(sk_hex), curve=CURVE) + vk = sk.verifying_key + msg_hash = hashlib.sha256(msg).digest() + sig = sk.sign_digest_deterministic( + msg_hash, + hashfunc=hashlib.sha256, + sigencode=util.sigencode_string, # raw 64-byte r||s + ) + pk = vk.to_string() # 64 bytes: x || y + return pk[:32], pk[32:], sig, msg_hash + + +# Fixed seed private keys for reproducibility. +SK_ALL_ONES = "01" * 32 +SK_SEQ = "".join(f"{i:02x}" for i in range(1, 33)) # 0x01..0x20 + + +def build_body() -> str: + blocks = [] + + pk_x, pk_y, sig, msg = sign(SK_ALL_ONES, b"Lampe ECDSA test vector") + blocks.append("\n".join([ + '-- valid signature: sk = 0x01..01, msg = "Lampe ECDSA test vector"', + f"private def validSimplePkX : Array (BitVec 8) := {bytes_to_lean_array(pk_x)}", + f"private def validSimplePkY : Array (BitVec 8) := {bytes_to_lean_array(pk_y)}", + f"private def validSimpleSig : Array (BitVec 8) := {bytes_to_lean_array(sig)}", + f"private def validSimpleMsg : Array (BitVec 8) := {bytes_to_lean_array(msg)}", + "example :", + " verifyBytes validSimplePkX validSimplePkY validSimpleSig validSimpleMsg = true := by", + " native_decide", + ])) + + pk_x, pk_y, sig, msg = sign(SK_SEQ, b"another message") + blocks.append("\n".join([ + '-- valid signature: sk = 0x01..20, msg = "another message"', + f"private def validSeqPkX : Array (BitVec 8) := {bytes_to_lean_array(pk_x)}", + f"private def validSeqPkY : Array (BitVec 8) := {bytes_to_lean_array(pk_y)}", + f"private def validSeqSig : Array (BitVec 8) := {bytes_to_lean_array(sig)}", + f"private def validSeqMsg : Array (BitVec 8) := {bytes_to_lean_array(msg)}", + "example :", + " verifyBytes validSeqPkX validSeqPkY validSeqSig validSeqMsg = true := by", + " native_decide", + ])) + + # Tamper validSimple by flipping one bit; reuse its pk/msg defs. + _, _, sig, _ = sign(SK_ALL_ONES, b"Lampe ECDSA test vector") + tampered = bytes([sig[0] ^ 0x01]) + sig[1:] + blocks.append("\n".join([ + "-- tampered: validSimple sig with one bit flipped → reject", + f"private def tamperedSig : Array (BitVec 8) := {bytes_to_lean_array(tampered)}", + "example :", + " verifyBytes validSimplePkX validSimplePkY tamperedSig validSimpleMsg = false := by", + " native_decide", + ])) + + return "\n\n".join(blocks) + + +def main(): + if len(sys.argv) != 2: + print("usage: secp256k1_ref.py ", file=sys.stderr) + sys.exit(1) + update_region(sys.argv[1], build_body(), label=LABEL) + + +if __name__ == "__main__": + main() diff --git a/scripts/gen/secp256r1_ref.py b/scripts/gen/secp256r1_ref.py new file mode 100644 index 00000000..8d21fd8e --- /dev/null +++ b/scripts/gen/secp256r1_ref.py @@ -0,0 +1,97 @@ +#!/usr/bin/env python3 +"""Reference secp256r1 (NIST P-256) ECDSA test vector generator. + +Mirror of `scripts/gen/secp256k1_ref.py` for the other Noir foreign-call +curve. Uses pure-Python `ecdsa` with RFC 6979 deterministic signing so +outputs regenerate identically. Vectors are checked via `native_decide`. + +Usage: + python3 scripts/gen/secp256r1_ref.py +""" + +import hashlib +import sys + +from _lean import update_region + +try: + from ecdsa import SigningKey, NIST256p, util +except ImportError: + print("error: pip install --user --break-system-packages ecdsa", file=sys.stderr) + sys.exit(1) + +CURVE = NIST256p +LABEL = "secp256r1 test vectors" + + +def bytes_to_lean_array(bs: bytes) -> str: + return "#[" + ", ".join(f"0x{b:02x}#8" for b in bs) + "]" + + +def sign(sk_hex: str, msg: bytes): + sk = SigningKey.from_string(bytes.fromhex(sk_hex), curve=CURVE) + vk = sk.verifying_key + msg_hash = hashlib.sha256(msg).digest() + sig = sk.sign_digest_deterministic( + msg_hash, + hashfunc=hashlib.sha256, + sigencode=util.sigencode_string, + ) + pk = vk.to_string() + return pk[:32], pk[32:], sig, msg_hash + + +SK_ALL_ONES = "01" * 32 +SK_SEQ = "".join(f"{i:02x}" for i in range(1, 33)) + + +def build_body() -> str: + blocks = [] + + pk_x, pk_y, sig, msg = sign(SK_ALL_ONES, b"Lampe ECDSA test vector") + blocks.append("\n".join([ + '-- valid signature: sk = 0x01..01, msg = "Lampe ECDSA test vector"', + f"private def validSimplePkX : Array (BitVec 8) := {bytes_to_lean_array(pk_x)}", + f"private def validSimplePkY : Array (BitVec 8) := {bytes_to_lean_array(pk_y)}", + f"private def validSimpleSig : Array (BitVec 8) := {bytes_to_lean_array(sig)}", + f"private def validSimpleMsg : Array (BitVec 8) := {bytes_to_lean_array(msg)}", + "example :", + " verifyBytes validSimplePkX validSimplePkY validSimpleSig validSimpleMsg = true := by", + " native_decide", + ])) + + pk_x, pk_y, sig, msg = sign(SK_SEQ, b"another message") + blocks.append("\n".join([ + '-- valid signature: sk = 0x01..20, msg = "another message"', + f"private def validSeqPkX : Array (BitVec 8) := {bytes_to_lean_array(pk_x)}", + f"private def validSeqPkY : Array (BitVec 8) := {bytes_to_lean_array(pk_y)}", + f"private def validSeqSig : Array (BitVec 8) := {bytes_to_lean_array(sig)}", + f"private def validSeqMsg : Array (BitVec 8) := {bytes_to_lean_array(msg)}", + "example :", + " verifyBytes validSeqPkX validSeqPkY validSeqSig validSeqMsg = true := by", + " native_decide", + ])) + + # Tamper validSimple by flipping one bit; reuse its pk/msg defs. + _, _, sig, _ = sign(SK_ALL_ONES, b"Lampe ECDSA test vector") + tampered = bytes([sig[0] ^ 0x01]) + sig[1:] + blocks.append("\n".join([ + "-- tampered: validSimple sig with one bit flipped → reject", + f"private def tamperedSig : Array (BitVec 8) := {bytes_to_lean_array(tampered)}", + "example :", + " verifyBytes validSimplePkX validSimplePkY tamperedSig validSimpleMsg = false := by", + " native_decide", + ])) + + return "\n\n".join(blocks) + + +def main(): + if len(sys.argv) != 2: + print("usage: secp256r1_ref.py ", file=sys.stderr) + sys.exit(1) + update_region(sys.argv[1], build_body(), label=LABEL) + + +if __name__ == "__main__": + main() diff --git a/scripts/gen_pratt.py b/scripts/gen_pratt.py deleted file mode 100644 index 67312dd1..00000000 --- a/scripts/gen_pratt.py +++ /dev/null @@ -1,312 +0,0 @@ -#!/usr/bin/env python3 -"""Generic Pratt primality certificate generator. - -Generates Lean proofs of `Nat.Prime

` for a given prime `P`, using -Mathlib's `lucas_primality` theorem applied recursively to every prime -factor of (P-1) that exceeds `norm_num`'s trial-division threshold. - -The generated certificate lives between marker comments: - - -- BEGIN generated Pratt certificate (scripts/gen_pratt.py) -- - ... - -- END generated Pratt certificate -- - -Everything outside the markers (imports, header docstring, `primeNat` -/ `prime` definitions, instances, ...) is hand-maintained and never -touched by this script. - -Usage: - # Regenerate the certificate region of an existing file, in place. - # Only the text between the markers is replaced; the rest of the - # file is preserved byte-for-byte. - python3 scripts/gen_pratt.py --prime \ - --update - - # Bootstrap a scaffold for a brand-new prime (written to stdout). - # The scaffold uses a generic header/footer that the author then - # hand-tunes; subsequent regenerations should use --update. - python3 scripts/gen_pratt.py --prime \ - --namespace > Lampe/Lampe/Crypto//Prime.lean - -Requires: sympy (for factorization and primality oracle). -""" - -import argparse -import sys - -try: - from sympy import factorint -except ImportError: - print( - "error: sympy not installed. Install with: " - "pip3 install --user --break-system-packages sympy", - file=sys.stderr, - ) - sys.exit(1) - - -BEGIN_MARKER = "-- BEGIN generated Pratt certificate (scripts/gen_pratt.py) --" -END_MARKER = "-- END generated Pratt certificate --" -DO_NOT_EDIT_NOTE = ( - "-- Do not edit between the markers; regenerate with" - " `scripts/gen_pratt.py --update`." -) - - -def find_generator(p, factors_p_minus_1): - n = p - 1 - for a in range(2, 200): - if pow(a, n, p) != 1: - continue - if all(pow(a, n // q, p) != 1 for q in factors_p_minus_1): - return a - raise RuntimeError(f"no small generator found for prime {p}") - - -def build_nodes(p, nodes): - if p in nodes or p == 2: - return - factors = factorint(p - 1) - nodes[p] = {"generator": find_generator(p, factors), "factors": factors} - for q in factors: - if q > 2 and q.bit_length() > 25: - build_nodes(q, nodes) - - -def factor_product_str(factors): - parts = [str(q) if e == 1 else f"{q}^{e}" for q, e in sorted(factors.items())] - if len(parts) == 1: - return parts[0] - result = parts[-1] - for part in reversed(parts[:-1]): - result = f"{part} * ({result})" - return result - - -def emit_have_block(factors): - lines = [] - for q in sorted(factors.keys()): - if q == 2: - lines.append(f" have h{q} : Nat.Prime {q} := Nat.prime_two") - elif q == 3: - lines.append(f" have h{q} : Nat.Prime {q} := Nat.prime_three") - elif q.bit_length() <= 25: - lines.append(f" have h{q} : Nat.Prime {q} := by norm_num") - else: - lines.append(f" have h{q} : Nat.Prime {q} := prime_{q}") - return lines - - -def emit_case_split(factors): - lines = [] - items = sorted(factors.items()) - - def emit_leaf(indent, hyp, q, e): - if e == 1: - lines.append(f"{indent}rw [(Nat.prime_dvd_prime_iff_eq hq h{q}).mp {hyp}]") - else: - lines.append(f"{indent}have hdvd_q : q ∣ {q} := hq.dvd_of_dvd_pow {hyp}") - lines.append(f"{indent}rw [(Nat.prime_dvd_prime_iff_eq hq h{q}).mp hdvd_q]") - lines.append(f"{indent}native_decide") - - def recurse(indent, items_, hyp): - if len(items_) == 1: - q, e = items_[0] - lines.append(f"{indent}-- {hyp} : q ∣ {q}^{e}") - emit_leaf(indent, hyp, q, e) - return - q, e = items_[0] - rest = items_[1:] - lines.append(f"{indent}rcases (hq.dvd_mul).mp {hyp} with hcase | hrest") - lines.append(f"{indent}· -- q ∣ {q}^{e}") - emit_leaf(indent + " ", "hcase", q, e) - lines.append(f"{indent}· -- q ∣ rest") - recurse(indent + " ", rest, "hrest") - - recurse(" ", items, "hdvd") - return lines - - -def emit_pratt_node(p, n): - factors = n["factors"] - gen = n["generator"] - out = [ - f"private theorem prime_{p} : Nat.Prime {p} := by", - f" refine lucas_primality {p} ({gen} : ZMod {p}) ?_ ?_", - f" · -- {gen}^({p}-1) = 1 mod {p}", - f" native_decide", - f" · intro q hq hdvd", - f" have h_eq : ({p} - 1 : ℕ) = {factor_product_str(factors)} := by decide", - f" rw [h_eq] at hdvd", - ] - out.extend(emit_have_block(factors)) - out.extend(emit_case_split(factors)) - return out - - -INVOCATION_TEMPLATE = """\ - python3 scripts/gen_pratt.py \\ - --prime {prime_arg} \\ - --update Lampe/Lampe/Crypto/{name}/Prime.lean\ -""" - -HEADER_TEMPLATE = """\ -import Lampe.Tp -import Mathlib.NumberTheory.LucasPrimality -import Mathlib.Tactic.NormNum.Prime - -/-! -# {name} field-prime Pratt primality certificate - -The Pratt-certificate section of this file (between the BEGIN/END -markers below) is **mechanically generated by** `scripts/gen_pratt.py`. -Do not edit that region by hand; regenerate it in place with: - -{invocation} - -Everything outside the markers is hand-maintained. - -It provides: -- A formal Pratt primality certificate for the {name} field prime - ({bits}-bit), using Mathlib's `lucas_primality` theorem. -- `primeNat : Nat`, `primeNat_prime : Nat.Prime primeNat`, - and the canonical `Lampe.Prime` value `prime`. --/ - -namespace Lampe.Crypto.{name} -""" - -FOOTER_TEMPLATE = """ -/-- The {name} field prime literal. -/ -def primeNat : Nat := - {prime} - -/-- Primality of the {name} field prime, established via the Pratt -certificate above. -/ -theorem primeNat_prime : Nat.Prime primeNat := - prime_{prime} - -private lemma primeNat_gt_two : primeNat > 2 := by unfold primeNat; norm_num - -/-- The canonical {name} `Lampe.Prime` value. -/ -def prime : Lampe.Prime := Lampe.Prime.ofNat primeNat primeNat_prime primeNat_gt_two - -end Lampe.Crypto.{name} -""" - - -def parse_prime(s: str) -> int: - s = s.strip() - if s.lower().startswith("0x"): - return int(s, 16) - return int(s) - - -def generate_region(P) -> str: - """The full marked region: BEGIN marker through END marker.""" - nodes = {} - build_nodes(P, nodes) - - out = [BEGIN_MARKER, DO_NOT_EDIT_NOTE] - out.append("/-! ### Pratt certificate") - out.append("") - out.append("Each `prime_

` lemma proves `Nat.Prime

` via Mathlib's") - out.append("`lucas_primality`. The certificate tree:") - out.append("") - out.append("```") - for p in sorted(nodes): - n = nodes[p] - out.append( - f" {p} (gen={n['generator']}, p-1 = {factor_product_str(n['factors'])})" - ) - out.append("```") - out.append("") - out.append("Power conditions are discharged by `native_decide`; small prime") - out.append("factors by `norm_num` (Mathlib's trial-division extension).") - out.append("-/") - out.append("") - for p in sorted(nodes): - out.extend(emit_pratt_node(p, nodes[p])) - out.append("") - out.append(END_MARKER) - return "\n".join(out) - - -def find_unique_marker(text: str, marker: str, path: str) -> int: - first = text.find(marker) - if first == -1: - print(f"error: marker {marker!r} not found in {path}", file=sys.stderr) - sys.exit(1) - if text.find(marker, first + len(marker)) != -1: - print(f"error: marker {marker!r} appears more than once in {path}", file=sys.stderr) - sys.exit(1) - return first - - -def update_file(path: str, P: int) -> None: - with open(path, encoding="utf-8") as f: - text = f.read() - - begin = find_unique_marker(text, BEGIN_MARKER, path) - end = find_unique_marker(text, END_MARKER, path) - if end < begin: - print(f"error: END marker precedes BEGIN marker in {path}", file=sys.stderr) - sys.exit(1) - - prefix = text[:begin] - suffix = text[end + len(END_MARKER):] - - if f"prime_{P}" not in prefix + suffix: - print( - f"error: {path} never references `prime_{P}` outside the generated " - f"region; is --prime correct for this file?", - file=sys.stderr, - ) - sys.exit(1) - - new_text = prefix + generate_region(P) + suffix - if new_text == text: - print(f"{path}: up to date", file=sys.stderr) - return - with open(path, "w", encoding="utf-8") as f: - f.write(new_text) - print(f"{path}: regenerated certificate region", file=sys.stderr) - - -def bootstrap(P: int, prime_arg: str, name: str) -> None: - invocation = INVOCATION_TEMPLATE.format(prime_arg=prime_arg, name=name) - header = HEADER_TEMPLATE.format( - name=name, bits=P.bit_length(), invocation=invocation - ) - footer = FOOTER_TEMPLATE.format(name=name, prime=P) - print("\n".join([header, generate_region(P), footer])) - - -def main(): - parser = argparse.ArgumentParser( - description="Generate Pratt primality certificates as Lean proofs." - ) - parser.add_argument( - "--prime", required=True, help="prime literal (decimal or 0x-hex)" - ) - mode = parser.add_mutually_exclusive_group(required=True) - mode.add_argument( - "--update", - metavar="FILE", - help="regenerate the marked certificate region of FILE in place", - ) - mode.add_argument( - "--namespace", - help="bootstrap a new scaffold under Lampe.Crypto. (to stdout)", - ) - args = parser.parse_args() - - P = parse_prime(args.prime) - if args.update: - update_file(args.update, P) - else: - bootstrap(P, args.prime, args.namespace) - - -if __name__ == "__main__": - main() diff --git a/scripts/secp256k1_ref.py b/scripts/secp256k1_ref.py deleted file mode 100644 index d4f98f38..00000000 --- a/scripts/secp256k1_ref.py +++ /dev/null @@ -1,71 +0,0 @@ -#!/usr/bin/env python3 -"""Reference secp256k1 ECDSA test vector generator. - -Uses the pure-Python `ecdsa` library (pip install ecdsa) which -implements RFC 6979 deterministic signing — so vectors regenerate -identically. - -Outputs Lean test vectors comparing - Lampe.Crypto.Secp256k1.verifyBytes pkX pkY sig msgHash -to the expected verification result, which is `true` for valid -signatures and `false` for tampered ones. - -Lampe validates against these via native_decide. Since Barretenberg's -`__ecdsa_secp256k1` foreign call must produce the same outputs (it is -the standard FIPS 186-4 verification algorithm), agreement with the -Python reference transitively certifies agreement with Barretenberg. -""" - -import hashlib -import sys - -try: - from ecdsa import SigningKey, SECP256k1, util -except ImportError: - print("error: pip install --user --break-system-packages ecdsa", file=sys.stderr) - sys.exit(1) - - -def bytes_to_lean_array(bs: bytes) -> str: - """Render bytes as a Lean `Array (BitVec 8)` literal.""" - return "#[" + ", ".join(f"0x{b:02x}#8" for b in bs) + "]" - - -def emit_vector(name: str, sk_hex: str, msg: bytes, *, tamper: bool = False) -> None: - sk = SigningKey.from_string(bytes.fromhex(sk_hex), curve=SECP256k1) - vk = sk.verifying_key - msg_hash = hashlib.sha256(msg).digest() - # Deterministic (RFC 6979) signature so output is reproducible. - sig = sk.sign_digest_deterministic( - msg_hash, - hashfunc=hashlib.sha256, - sigencode=util.sigencode_string, # raw 64-byte r||s - ) - pk_str = vk.to_string() # 64 bytes: x || y - pk_x = pk_str[:32] - pk_y = pk_str[32:] - - if tamper: - # Flip a single bit in the signature -> verification must fail. - sig = bytes([sig[0] ^ 0x01]) + sig[1:] - expected = "false" if tamper else "true" - - note = "tampered signature → reject" if tamper else "valid signature → accept" - print(f"-- {name}: msg = {msg!r}, sk = 0x{sk_hex}; {note}") - print(f"private def {name}PkX : Array (BitVec 8) := {bytes_to_lean_array(pk_x)}") - print(f"private def {name}PkY : Array (BitVec 8) := {bytes_to_lean_array(pk_y)}") - print(f"private def {name}Sig : Array (BitVec 8) := {bytes_to_lean_array(sig)}") - print(f"private def {name}Msg : Array (BitVec 8) := {bytes_to_lean_array(msg_hash)}") - print(f"theorem secp256k1_{name}_correct :") - print(f" verifyBytes {name}PkX {name}PkY {name}Sig {name}Msg = {expected} := by") - print(f" native_decide") - print() - - -# Fixed seed private keys for reproducibility. -SK_ALL_ONES = "01" * 32 -SK_SEQ = "".join(f"{i:02x}" for i in range(1, 33)) # 0x01..0x20 - -emit_vector("validSimple", SK_ALL_ONES, b"Lampe ECDSA test vector") -emit_vector("validSeq", SK_SEQ, b"another message") -emit_vector("tampered", SK_ALL_ONES, b"Lampe ECDSA test vector", tamper=True) diff --git a/scripts/secp256r1_ref.py b/scripts/secp256r1_ref.py deleted file mode 100644 index 9a31cf00..00000000 --- a/scripts/secp256r1_ref.py +++ /dev/null @@ -1,57 +0,0 @@ -#!/usr/bin/env python3 -"""Reference secp256r1 (NIST P-256) ECDSA test vector generator. - -Mirror of `scripts/secp256k1_ref.py` for the other Noir foreign-call -curve. Uses pure-Python `ecdsa` with RFC 6979 deterministic signing -so outputs regenerate identically. -""" - -import hashlib -import sys - -try: - from ecdsa import SigningKey, NIST256p, util -except ImportError: - print("error: pip install --user --break-system-packages ecdsa", file=sys.stderr) - sys.exit(1) - - -def bytes_to_lean_array(bs: bytes) -> str: - return "#[" + ", ".join(f"0x{b:02x}#8" for b in bs) + "]" - - -def emit_vector(name: str, sk_hex: str, msg: bytes, *, tamper: bool = False) -> None: - sk = SigningKey.from_string(bytes.fromhex(sk_hex), curve=NIST256p) - vk = sk.verifying_key - msg_hash = hashlib.sha256(msg).digest() - sig = sk.sign_digest_deterministic( - msg_hash, - hashfunc=hashlib.sha256, - sigencode=util.sigencode_string, - ) - pk_str = vk.to_string() - pk_x = pk_str[:32] - pk_y = pk_str[32:] - - if tamper: - sig = bytes([sig[0] ^ 0x01]) + sig[1:] - expected = "false" if tamper else "true" - - note = "tampered signature → reject" if tamper else "valid signature → accept" - print(f"-- {name}: msg = {msg!r}, sk = 0x{sk_hex}; {note}") - print(f"private def {name}PkX : Array (BitVec 8) := {bytes_to_lean_array(pk_x)}") - print(f"private def {name}PkY : Array (BitVec 8) := {bytes_to_lean_array(pk_y)}") - print(f"private def {name}Sig : Array (BitVec 8) := {bytes_to_lean_array(sig)}") - print(f"private def {name}Msg : Array (BitVec 8) := {bytes_to_lean_array(msg_hash)}") - print(f"theorem secp256r1_{name}_correct :") - print(f" verifyBytes {name}PkX {name}PkY {name}Sig {name}Msg = {expected} := by") - print(f" native_decide") - print() - - -SK_ALL_ONES = "01" * 32 -SK_SEQ = "".join(f"{i:02x}" for i in range(1, 33)) - -emit_vector("validSimple", SK_ALL_ONES, b"Lampe ECDSA test vector") -emit_vector("validSeq", SK_SEQ, b"another message") -emit_vector("tampered", SK_ALL_ONES, b"Lampe ECDSA test vector", tamper=True) diff --git a/stdlib/lampe/Stdlib/Hash/Mod.lean b/stdlib/lampe/Stdlib/Hash/Mod.lean index 97f59cbe..e5c84d61 100644 --- a/stdlib/lampe/Stdlib/Hash/Mod.lean +++ b/stdlib/lampe/Stdlib/Hash/Mod.lean @@ -58,7 +58,7 @@ theorem blake2s_builtin_spec {p} {N : U 32} (fun r => r = Lampe.Crypto.Blake2s.blake2sHash input) := by exact STHoare.genericTotalPureBuiltin_intro Builtin.blake2S rfl N p env h![input] -private theorem blake3_builtin_spec {p} {N : U 32} +theorem blake3_builtin_spec {p} {N : U 32} {input : Tp.denote p ((Tp.u 8).array N)} : STHoare p env ⟦⟧ (.callBuiltin [(Tp.u 8).array N] ((Tp.u 8).array (32 : U 32))