david415 · Oct 18, 2026 · Oct 17, 2026 · Oct 17, 2026
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
@@ -11,7 +11,10 @@ jobs:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
         with:
-          build-args: "Cryptlib Cryptlib.Data.test Cryptlib.Primitives.NIKE.test Cryptlib.Primitives.KEM.test Cryptlib.Primitives.KEM.vectors Cryptlib.Primitives.Hash.test Cryptlib.Primitives.Hash.hkdf_test Cryptlib.Primitives.KDF.argon2_test Cryptlib.Primitives.Cipher.test Cryptlib.Bench.benchmark Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ack_codec_test Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.wire_vectors_test Cryptlib.Protocols.BACAP.primitive_vectors_test Cryptlib.Protocols.BACAP.gen_vectors Cryptlib.Protocols.BACAP.test Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.replay Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.scenarios"
+          build-args: "Cryptlib Cryptlib.Data.test Cryptlib.Primitives.NIKE.test Cryptlib.Primitives.KEM.test Cryptlib.Primitives.KEM.vectors Cryptlib.Primitives.Hash.test Cryptlib.Primitives.Hash.hkdf_test Cryptlib.Primitives.KDF.argon2_test Cryptlib.Primitives.Cipher.test Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.ack_codec_test Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.wire_vectors_test Cryptlib.Protocols.BACAP.primitive_vectors_test Cryptlib.Protocols.BACAP.gen_vectors Cryptlib.Protocols.BACAP.test Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.replay Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.scenarios"
+      - name: Build the benchmarks (their own Lake project)
+        working-directory: bench
+        run: lake build
       - name: Run tests
         env:
           # panics in compiled Lean print a message but exit 0 unless this is set

diff --git a/Cryptlib.lean b/Cryptlib.lean
@@ -10,8 +10,8 @@ import Cryptlib.Primitives.Hash.Blake2s
 import Cryptlib.Primitives.MAC.HMAC
 import Cryptlib.Primitives.KDF.HKDF
 import Cryptlib.Primitives.KDF.Argon2
-import Cryptlib.Util.newnat
-import Cryptlib.Util.newhex
+import Cryptlib.Util.NatBytes
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Hex
 import Cryptlib.Util.ByteArray
 import Cryptlib.Util.Nat
@@ -67,20 +67,18 @@ import Cryptlib.Protocols.BACAP.Impl
 import Cryptlib.Protocols.BACAP.API
 import Cryptlib.Protocols.BACAP.Unlinkability
 import Cryptlib.Protocols.BACAP.Ed25519Unlinkability
-import Cryptlib.Protocols.BACAP.test
 import Cryptlib.Protocols.Pigeonhole.Replica
 import Cryptlib.Protocols.Pigeonhole.Protocol
 import Cryptlib.Protocols.Pigeonhole.Semantics
-import Cryptlib.Protocols.Sphinx.sphinx
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.geometry_cbor
-import Cryptlib.Protocols.Sphinx.integrity
-import Cryptlib.Protocols.Sphinx.indistinguishability
-import Cryptlib.Protocols.Sphinx.wrap_resistance
-import Cryptlib.Protocols.Sphinx.nike_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.kem_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.schemes
-import Cryptlib.Protocols.Sphinx.bench_registry
+import Cryptlib.Protocols.Sphinx.Interface
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.GeometryCbor
+import Cryptlib.Protocols.Sphinx.Integrity
+import Cryptlib.Protocols.Sphinx.Indistinguishability
+import Cryptlib.Protocols.Sphinx.WrapResistance
+import Cryptlib.Protocols.Sphinx.NIKESphinxTheorems
+import Cryptlib.Protocols.Sphinx.KEMSphinxTheorems
+import Cryptlib.Protocols.Sphinx.Schemes
 import Cryptlib.Protocols.GroupComm
 import Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec
 import Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Roster

diff --git a/Cryptlib/Bench/benchmark.lean b/Cryptlib/Bench/benchmark.lean
diff --git a/Cryptlib/Data/MerkleHashTree.lean b/Cryptlib/Data/MerkleHashTree.lean
@@ -8,8 +8,8 @@ import Init.Data.ToString
 import Mathlib.Tactic
 
 import Cryptlib.Primitives.Hash.Sha2
-import Cryptlib.Util.newnat
-import Cryptlib.Util.newhex
+import Cryptlib.Util.NatBytes
+import Cryptlib.Util.HexBytes
 
 namespace Cryptlib.Data.MerkleHashTree
 

diff --git a/Cryptlib/Data/test.lean b/Cryptlib/Data/test.lean
@@ -1,8 +1,8 @@
 
 import Cryptlib.Data.MerkleHashTree
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Data.MerkleHashTree
 
 instance : BEq ByteArray where

diff --git a/Cryptlib/Primitives/Cipher/aead_vectors_test.lean b/Cryptlib/Primitives/Cipher/aead_vectors_test.lean
@@ -4,12 +4,12 @@ import Cryptlib.Primitives.Cipher.AEAD
 import Cryptlib.Primitives.Cipher.AESGCM
 import Cryptlib.Primitives.Cipher.ChaChaPoly
 import Cryptlib.Util.Bytes
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 open Lean
 open Cryptlib.Primitives.Cipher.AEAD
 open Cryptlib.Util.Bytes (toVecN)
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 /-! Wycheproof vectors for the `AEAD` instances, run through the generic interface. Invalid
 vectors must fail to decrypt; valid ones must encrypt to the expected ciphertext and tag. -/

diff --git a/Cryptlib/Primitives/Cipher/test.lean b/Cryptlib/Primitives/Cipher/test.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.Cipher.AESGCMSIV
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-!
 # AES-256-GCM-SIV known-answer tests
@@ -15,7 +15,7 @@ ciphertexts that must be rejected. The underlying primitives get their own vecto
 -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.Cipher
 
 structure SIVVector where

diff --git a/Cryptlib/Primitives/Hash/blake2b_256_test.lean b/Cryptlib/Primitives/Hash/blake2b_256_test.lean
@@ -5,14 +5,14 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.Hash.Blake2b
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # BLAKE2b-256 (unkeyed and keyed) known-answer tests
 
 Checks `Blake2b.hash256`/`hash256Keyed` against `testdata/blake2b_256.json`, from hpqc. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.Hash.Blake2b (hash256 hash256Keyed)
 
 def field (j : Json) (k : String) : Except String ByteArray := do

diff --git a/Cryptlib/Primitives/Hash/blake2b_xof_test.lean b/Cryptlib/Primitives/Hash/blake2b_xof_test.lean
@@ -5,15 +5,15 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.Hash.Blake2b
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # BLAKE2Xb known-answer tests
 
 Checks `Blake2b.xof` against `testdata/blake2b_xof.json`, from hpqc. `xof_size` is the configured
 size and `length` the number of bytes read. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.Hash.Blake2b (xof)
 
 def field (j : Json) (k : String) : Except String ByteArray := do

diff --git a/Cryptlib/Primitives/Hash/blake2s_test.lean b/Cryptlib/Primitives/Hash/blake2s_test.lean
@@ -1,11 +1,11 @@
 import Lean.Data.Json
 
 import Cryptlib.Primitives.Hash.Blake2s
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 open Lean
 open Cryptlib.Primitives.Hash.Blake2s
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 def hexField (j : Json) (k : String) : Except String ByteArray := do
   match hexStringToByteArray (← (← j.getObjVal? k).getStr?) with

diff --git a/Cryptlib/Primitives/Hash/hkdf_structured_test.lean b/Cryptlib/Primitives/Hash/hkdf_structured_test.lean
@@ -6,7 +6,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 import Lean.Data.Json
 
 import Cryptlib.Primitives.Hash.HKDF
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # HKDF-BLAKE2b-512 known-answer tests
 
@@ -15,7 +15,7 @@ Checks `extract` and `expand` of `blake2b512_hkdf` against `testdata/hkdf_blake2
 
 open Lean
 open Cryptlib.Primitives.Hash.HKDF
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 structure HKDFVector where
   name   : String

diff --git a/Cryptlib/Primitives/Hash/hkdf_test.lean b/Cryptlib/Primitives/Hash/hkdf_test.lean
@@ -2,11 +2,11 @@ import Lean.Data.Json
 
 import Cryptlib.Primitives.Hash.HKDF
 import Cryptlib.Primitives.KDF.HKDF
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 open Lean
 open Cryptlib.Primitives.Hash.HKDF (blake2b_hashScheme)
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 structure HKDFVector where
   name : String

diff --git a/Cryptlib/Primitives/Hash/test.lean b/Cryptlib/Primitives/Hash/test.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.Hash.Sha512
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-!
 # SHA-512 known-answer tests
@@ -15,7 +15,7 @@ vectors whose padding spans more than one block.
 -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.Hash.Sha512
 
 structure HashVec where

diff --git a/Cryptlib/Primitives/KDF/argon2_test.lean b/Cryptlib/Primitives/KDF/argon2_test.lean
@@ -1,11 +1,11 @@
 import Lean.Data.Json
 
 import Cryptlib.Primitives.KDF.Argon2
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 open Lean
 open Cryptlib.Primitives.KDF.Argon2
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 def hexField (j : Json) (k : String) : Except String ByteArray := do
   match hexStringToByteArray (← (← j.getObjVal? k).getStr?) with

diff --git a/Cryptlib/Primitives/KEM/MLKEM/mlkem_test.lean b/Cryptlib/Primitives/KEM/MLKEM/mlkem_test.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.KEM.MLKEM.MLKEM
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # ML-KEM known-answer tests: NIST ACVP vectors for ML-KEM-512, -768 and -1024
 
@@ -15,7 +15,7 @@ Vectors in `testdata/mlkem<N>_{keygen,encapdecap,keycheck}.json`, extracted by
 open Lean
 open MLKEM
 open Cryptlib.Primitives.KEM.FIPS203
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Util.Bytes (ofVector toVecN)
 
 def field (j : Json) (k : String) : Except String ByteArray := do

diff --git a/Cryptlib/Primitives/KEM/MLKEMHedged/mlkemhedged_test.lean b/Cryptlib/Primitives/KEM/MLKEMHedged/mlkemhedged_test.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.KEM.MLKEMHedged.MLKEMHedged
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-!
 # Hedged ML-KEM: NIST ACVP known-answer tests, for ML-KEM-512, -768 and -1024
@@ -20,7 +20,7 @@ open MLKEM
 open Cryptlib.Primitives.KEM.FIPS203 (encaps expandSeed checkEncapsulationKey checkDecapsulationKey
   uBytes vBytes stateFromSeed)
 open Cryptlib.Primitives.KEM.MLKEMHedged
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Util.Bytes (ofVector toVecN)
 
 def field (j : Json) (k : String) : Except String ByteArray := do

diff --git a/Cryptlib/Primitives/KEM/gen_mlkem768_x25519_combiner_vectors.lean b/Cryptlib/Primitives/KEM/gen_mlkem768_x25519_combiner_vectors.lean
@@ -5,15 +5,15 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.KEM.Schemes
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # X25519 + ML-KEM-768 combiner vector generator
 
 Writes random vectors in the schema `mlkem768_x25519_combiner_test.lean` checks, using
 `kemX25519Blake2b`. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.KEM
 open MLKEM
 open Cryptlib.Primitives.KEM.MLKEM768 (keygen768 encaps768 params encoding tBytes uBytes vBytes)

diff --git a/Cryptlib/Primitives/KEM/gen_mlkem_hedged_vectors.lean b/Cryptlib/Primitives/KEM/gen_mlkem_hedged_vectors.lean
@@ -7,7 +7,7 @@ import Lean.Data.Json
 import Cryptlib.Primitives.KEM.MLKEMHedged.MLKEMHedged512
 import Cryptlib.Primitives.KEM.MLKEMHedged.MLKEMHedged768
 import Cryptlib.Primitives.KEM.MLKEMHedged.MLKEMHedged1024
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # Hedged ML-KEM vector generator
 
@@ -19,7 +19,7 @@ open Lean
 open MLKEM
 open Cryptlib.Primitives.KEM.FIPS203 (hashH uBytes vBytes)
 open Cryptlib.Primitives.KEM.MLKEMHedged
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Util.Bytes (ofVector toVecN)
 
 def hexOfB (b : ByteArray) : String := byteArrayToHex b

diff --git a/Cryptlib/Primitives/KEM/mlkem768_x25519_combiner_test.lean b/Cryptlib/Primitives/KEM/mlkem768_x25519_combiner_test.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.KEM.Schemes
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # X25519 + ML-KEM-768 combiner: known-answer tests
 
@@ -14,7 +14,7 @@ ciphertext and shared secret. Each vector's `prf` field selects `kemX25519Blake2
 `kemX25519`. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.KEM
 open Cryptlib.Primitives.KEM.KEM
 open MLKEM

diff --git a/Cryptlib/Primitives/KEM/mlkem_hedged_test.lean b/Cryptlib/Primitives/KEM/mlkem_hedged_test.lean
@@ -7,7 +7,7 @@ import Lean.Data.Json
 import Cryptlib.Primitives.KEM.MLKEMHedged.MLKEMHedged512
 import Cryptlib.Primitives.KEM.MLKEMHedged.MLKEMHedged768
 import Cryptlib.Primitives.KEM.MLKEMHedged.MLKEMHedged1024
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # Hedged ML-KEM: known-answer tests shared with hpqc
 
@@ -20,7 +20,7 @@ open Lean
 open MLKEM
 open Cryptlib.Primitives.KEM.FIPS203 (hashH uBytes vBytes)
 open Cryptlib.Primitives.KEM.MLKEMHedged
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Util.Bytes (ofVector toVecN)
 
 def field (j : Json) (k : String) : Except String ByteArray := do

diff --git a/Cryptlib/Primitives/KEM/vectors.lean b/Cryptlib/Primitives/KEM/vectors.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.KEM.Schemes
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-!
 # NIKE-to-KEM adapter test vectors
@@ -16,7 +16,7 @@ Vectors with an unsupported `prf` are skipped; at least one must run.
 -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.KEM
 open Cryptlib.Primitives.KEM.KEM
 open Cryptlib.Primitives.KEM.Adapter

diff --git a/Cryptlib/Primitives/MAC/hmac_hkdf_test.lean b/Cryptlib/Primitives/MAC/hmac_hkdf_test.lean
@@ -7,11 +7,11 @@ import Cryptlib.Primitives.Hash.Blake2s
 import Cryptlib.Primitives.Hash.HKDF
 import Cryptlib.Primitives.KDF.HKDF
 import Cryptlib.Primitives.MAC.HMAC
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 open Lean
 open Cryptlib.Primitives.Hash.Hash
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 /-! RFC 4231 HMAC and RFC 5869 HKDF vectors (`testdata/hmac_hkdf.json`), run against the generic
 constructions at every `Hash` instance named in the file. -/