General Cleanup of Crypto Builtins

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

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)

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⟩

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. -/

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,

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)

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 <path>`.
 /-! ### Pratt certificate
 
 Each `prime_<p>` lemma proves `Nat.Prime <p>` 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`. -/