diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 18e14598..5a9a81cb 100644
--- 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
index 405379a8..6031b209 100644
--- 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
deleted file mode 100644
index dc5a055e..00000000
--- a/Cryptlib/Bench/benchmark.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-/-
-SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
-SPDX-License-Identifier: AGPL-3.0-only
--/
-
-import Cryptlib.Bench.NIKE
-import Cryptlib.Bench.KEM
-import Cryptlib.Bench.Sphinx
-import Cryptlib.Bench.MLKEMSteps
-import Cryptlib.Bench.Field25519
-import Cryptlib.Bench.Cipher
-import Cryptlib.Bench.KDF
-
-/-! # Benchmark driver for all registered schemes and suites -/
-
-def main (args : List String) : IO UInt32 := do
-  for e in Cryptlib.Primitives.NIKE.registry do
-    (← Cryptlib.Bench.NIKE.benches e.hpqcName e.scheme).forM LeanBench.register
-  for e in Cryptlib.Primitives.KEM.registry do
-    (← Cryptlib.Bench.KEM.benches e.name e.scheme).forM LeanBench.register
-  (← Cryptlib.Bench.Sphinx.benches).forM LeanBench.register
-  (← Cryptlib.Bench.MLKEMSteps.benches).forM LeanBench.register
-  (← Cryptlib.Bench.Field25519.benches).forM LeanBench.register
-  (← Cryptlib.Bench.Cipher.benches).forM LeanBench.register
-  (← Cryptlib.Bench.KDF.benches).forM LeanBench.register
-  LeanBench.runMain args
diff --git a/Cryptlib/Data/MerkleHashTree.lean b/Cryptlib/Data/MerkleHashTree.lean
index a9acf939..8dbd31a2 100644
--- 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
index 9b68cf40..986b6367 100644
--- 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
index 42ec93d4..3d2cf2ce 100644
--- 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
index d7498791..4f447299 100644
--- 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
index 5b947c38..2557c36d 100644
--- 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
index 5559d179..6cb6c3c5 100644
--- a/Cryptlib/Primitives/Hash/blake2b_xof_test.lean
+++ b/Cryptlib/Primitives/Hash/blake2b_xof_test.lean
@@ -5,7 +5,7 @@ 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
 
@@ -13,7 +13,7 @@ Checks `Blake2b.xof` against `testdata/blake2b_xof.json`, from hpqc. `xof_size`
 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
index 9ef2c90d..68df2008 100644
--- 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
index 121433bc..dc08f625 100644
--- 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
index fb0ff6a3..3c501af3 100644
--- 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
index 385ebb4a..4d34f4d2 100644
--- 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
index 5b1b9530..2cbb788d 100644
--- 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
index f9499d1d..f1f8c7f0 100644
--- 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
index 7047a973..e9687069 100644
--- 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
index 19a15147..4dde9742 100644
--- a/Cryptlib/Primitives/KEM/gen_mlkem768_x25519_combiner_vectors.lean
+++ b/Cryptlib/Primitives/KEM/gen_mlkem768_x25519_combiner_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
 
 /-! # X25519 + ML-KEM-768 combiner vector generator
 
@@ -13,7 +13,7 @@ Writes random vectors in the schema `mlkem768_x25519_combiner_test.lean` checks,
 `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
index b3863a9c..ed06b827 100644
--- 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
index d5ce259b..2f0369d2 100644
--- 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
index 159bb94a..d119e6ca 100644
--- 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
index 12a01cd3..8913cc0d 100644
--- 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
index 4493b1bb..ad5b1d11 100644
--- 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. -/
diff --git a/Cryptlib/Primitives/MultiRecipientHybrid/gen_multirecipient_hybrid_vectors.lean b/Cryptlib/Primitives/MultiRecipientHybrid/gen_multirecipient_hybrid_vectors.lean
index d3fd2e75..f198f43c 100644
--- a/Cryptlib/Primitives/MultiRecipientHybrid/gen_multirecipient_hybrid_vectors.lean
+++ b/Cryptlib/Primitives/MultiRecipientHybrid/gen_multirecipient_hybrid_vectors.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.MultiRecipientHybrid.Schemes
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # Multi-recipient hybrid vector generator
 
@@ -16,7 +16,7 @@ open Lean
 open Cryptlib.Primitives.KEM (kemX25519Blake2b kemMLKEM768X25519Blake2b)
 open Cryptlib.Primitives.MultiRecipientHybrid.MultiRecipientHybrid (Ciphertext)
 open Cryptlib.Primitives.MultiRecipientHybrid.Schemes (hybridMLKEM768X25519Blake2b)
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Util.Bytes (ofVector toVecN)
 
 def H := hybridMLKEM768X25519Blake2b
diff --git a/Cryptlib/Primitives/MultiRecipientHybrid/multirecipient_hybrid_test.lean b/Cryptlib/Primitives/MultiRecipientHybrid/multirecipient_hybrid_test.lean
index d6cda347..c6cc5f83 100644
--- a/Cryptlib/Primitives/MultiRecipientHybrid/multirecipient_hybrid_test.lean
+++ b/Cryptlib/Primitives/MultiRecipientHybrid/multirecipient_hybrid_test.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.MultiRecipientHybrid.Schemes
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # Multi-recipient hybrid: known-answer tests
 
@@ -17,7 +17,7 @@ open Lean
 open Cryptlib.Primitives.KEM (kemX25519Blake2b kemMLKEM768X25519Blake2b)
 open Cryptlib.Primitives.MultiRecipientHybrid.MultiRecipientHybrid (Ciphertext)
 open Cryptlib.Primitives.MultiRecipientHybrid.Schemes (hybridMLKEM768X25519Blake2b)
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Util.Bytes (ofVector toVecN)
 
 def H := hybridMLKEM768X25519Blake2b
diff --git a/Cryptlib/Primitives/NIKE/X25519_montgomery_ladder.lean b/Cryptlib/Primitives/NIKE/X25519_montgomery_ladder.lean
index d3ccf0a5..c8ec2433 100644
--- a/Cryptlib/Primitives/NIKE/X25519_montgomery_ladder.lean
+++ b/Cryptlib/Primitives/NIKE/X25519_montgomery_ladder.lean
@@ -7,13 +7,13 @@ import Mathlib.Algebra.Field.Basic
 import Mathlib.Data.ZMod.Basic
 import Mathlib.NumberTheory.LucasPrimality
 
-import Cryptlib.Util.newnat
-import Cryptlib.Util.newhex
+import Cryptlib.Util.NatBytes
+import Cryptlib.Util.HexBytes
 import Cryptlib.Primitives.NIKE.NIKE
 import Cryptlib.Primitives.NIKE.X25519Common
 import Cryptlib.Primitives.NIKE.Field25519
 
-open Cryptlib.Util.newnat
+open Cryptlib.Util.NatBytes
 open Cryptlib.Primitives.NIKE.NIKE
 open Cryptlib.Primitives.NIKE.X25519Common
 
diff --git a/Cryptlib/Primitives/NIKE/field25519_test.lean b/Cryptlib/Primitives/NIKE/field25519_test.lean
index b3e17eaf..615a5da1 100644
--- a/Cryptlib/Primitives/NIKE/field25519_test.lean
+++ b/Cryptlib/Primitives/NIKE/field25519_test.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Cryptlib.Primitives.NIKE.Field25519
 import Cryptlib.Primitives.NIKE.X25519_montgomery_ladder
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! Tests for `Field25519` and the limb-based ladder: every field operation against `Nat`
 arithmetic modulo `p`, on edge cases and random values, with the limb bound checked after each;
@@ -14,7 +14,7 @@ RFC 7748 vectors; and agreement with the `ZMod` ladder. -/
 open Cryptlib.Primitives.NIKE.Field25519 (Fe)
 open Cryptlib.Primitives.NIKE.X25519Common (p)
 open Cryptlib.Primitives.NIKE.X25519_montgomery_ladder (curve25519 curve25519_fe)
-open Cryptlib.Util.newhex (byteArrayToHex hexStringToByteArray)
+open Cryptlib.Util.HexBytes (byteArrayToHex hexStringToByteArray)
 
 def failures : IO (IO.Ref Nat) := IO.mkRef 0
 
diff --git a/Cryptlib/Primitives/NIKE/test.lean b/Cryptlib/Primitives/NIKE/test.lean
index 8935a893..193d3e52 100644
--- a/Cryptlib/Primitives/NIKE/test.lean
+++ b/Cryptlib/Primitives/NIKE/test.lean
@@ -5,7 +5,7 @@ import Cryptlib.Primitives.NIKE.X25519_montgomery_ladder
 import Cryptlib.Primitives.NIKE.X25519
 import Cryptlib.Primitives.NIKE.Schemes
 
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.NIKE.NIKE
 
 def hexToVec32 (s : String) : Option (Vector UInt8 32) := do
diff --git a/Cryptlib/Primitives/Sign/blinded_test.lean b/Cryptlib/Primitives/Sign/blinded_test.lean
index 91d7a05f..5f3e0241 100644
--- a/Cryptlib/Primitives/Sign/blinded_test.lean
+++ b/Cryptlib/Primitives/Sign/blinded_test.lean
@@ -4,13 +4,13 @@ import Lean.Data.Json
 import Cryptlib.Primitives.Hash.Sha512
 import Cryptlib.Primitives.Sign.Ed25519_blinded
 import Cryptlib.Primitives.Sign.Ed25519_math
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 open Lean
 open Cryptlib.Primitives.Sign.Ed25519Blinded
 open Cryptlib.Primitives.Sign.Ed25519Math
 open Cryptlib.Primitives.Hash.Sha512
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 private def hexToVec32 (s : String) : Option (Vector UInt8 32) := do
   let bytes ← hexStringToByteArray s
diff --git a/Cryptlib/Primitives/Sign/test.lean b/Cryptlib/Primitives/Sign/test.lean
index 48c50fca..3ac3f11e 100644
--- a/Cryptlib/Primitives/Sign/test.lean
+++ b/Cryptlib/Primitives/Sign/test.lean
@@ -2,11 +2,11 @@ import Lean
 
 import Cryptlib.Primitives.Hash.Sha512
 import Cryptlib.Primitives.Sign.Ed25519_math
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 open Cryptlib.Primitives.Hash.Sha512
 open Cryptlib.Primitives.Sign.Ed25519Math
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 private def hexToVec32 (s : String) : Option (Vector UInt8 32) := do
   let bytes ← hexStringToByteArray s
diff --git a/Cryptlib/Primitives/WideBlockCipher/test.lean b/Cryptlib/Primitives/WideBlockCipher/test.lean
index 59756f04..31e155bc 100644
--- a/Cryptlib/Primitives/WideBlockCipher/test.lean
+++ b/Cryptlib/Primitives/WideBlockCipher/test.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Lean.Data.Json
 import Cryptlib.Primitives.WideBlockCipher.AEZ
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-!
 # AEZ v5 SPRP known-answer tests
@@ -15,7 +15,7 @@ Checks `WideBlockCipher.AEZ` against `sprp_aez.json`, covering both the `aezTiny
 -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.WideBlockCipher.AEZ
 
 def field (j : Json) (k : String) : Except String ByteArray := do
diff --git a/Cryptlib/Protocols/BACAP/BACAP.lean b/Cryptlib/Protocols/BACAP/BACAP.lean
index 8cd5b596..aad2cca4 100644
--- a/Cryptlib/Protocols/BACAP/BACAP.lean
+++ b/Cryptlib/Protocols/BACAP/BACAP.lean
@@ -9,4 +9,3 @@ import Cryptlib.Protocols.BACAP.Protocol
 import Cryptlib.Protocols.BACAP.Impl
 import Cryptlib.Protocols.BACAP.API
 import Cryptlib.Protocols.BACAP.Position
-import Cryptlib.Protocols.BACAP.test
diff --git a/Cryptlib/Protocols/BACAP/gen_vectors.lean b/Cryptlib/Protocols/BACAP/gen_vectors.lean
index 4a7af736..c72f7785 100644
--- a/Cryptlib/Protocols/BACAP/gen_vectors.lean
+++ b/Cryptlib/Protocols/BACAP/gen_vectors.lean
@@ -6,7 +6,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 import Lean.Data.Json
 import Cryptlib.Protocols.BACAP.Position
 import Cryptlib.Protocols.BACAP.Types
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # Generate the BACAP vector files from `testdata/bacap_inputs.json` (from hpqc)
 
@@ -17,7 +17,7 @@ open Lean
 open Cryptlib.Protocols.BACAP.Types
 open Cryptlib.Protocols.BACAP.Ratchet
 open Cryptlib.Primitives.Hash.HKDF
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 abbrev Gen := ExceptT String IO
 
diff --git a/Cryptlib/Protocols/BACAP/primitive_vectors_test.lean b/Cryptlib/Protocols/BACAP/primitive_vectors_test.lean
index 58c5b29e..329de908 100644
--- a/Cryptlib/Protocols/BACAP/primitive_vectors_test.lean
+++ b/Cryptlib/Protocols/BACAP/primitive_vectors_test.lean
@@ -7,14 +7,14 @@ import Lean.Data.Json
 import Cryptlib.Primitives.Hash.Sha512
 import Cryptlib.Primitives.Hash.Blake2b
 import Cryptlib.Primitives.Sign.Ed25519_math
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # SHA-512/256, BLAKE2b-512 and Ed25519 vectors (from hpqc)
 
 Ed25519 vectors must verify, and must fail with one signature bit flipped. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 def hexBytes (j : Json) (k : String) : Except String ByteArray := do
   let s ← (← j.getObjVal? k).getStr?
diff --git a/Cryptlib/Protocols/BACAP/test.lean b/Cryptlib/Protocols/BACAP/test.lean
index 5e20c56a..a6794ac4 100644
--- a/Cryptlib/Protocols/BACAP/test.lean
+++ b/Cryptlib/Protocols/BACAP/test.lean
@@ -9,7 +9,7 @@ import Cryptlib.Protocols.BACAP.API
 import Cryptlib.Protocols.BACAP.Position
 import Cryptlib.Protocols.BACAP.Impl
 import Cryptlib.Protocols.BACAP.Types
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # BACAP test vectors (from hpqc) and randomized round-trip tests -/
 
@@ -19,7 +19,7 @@ open Cryptlib.Protocols.BACAP.Ratchet
 open Cryptlib.Primitives.Hash.HKDF
 open Cryptlib.Primitives.Sign.Ed25519Blinded
 open Cryptlib.Primitives.Cipher.AESGCMSIV
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.BACAP.Impl
 
 -- ── hex parsing ──
diff --git a/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/Member/Json.lean b/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/Member/Json.lean
index 7d12f5b1..d29e7d3e 100644
--- a/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/Member/Json.lean
+++ b/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/Member/Json.lean
@@ -6,7 +6,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 import Lean.Data.Json
 
 import Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Group
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # JSON trace format
 
@@ -18,7 +18,7 @@ namespace Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Trace
 open Cryptlib.Protocols.GroupComm.Common
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 /-! ## Writing -/
 
diff --git a/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/ack_codec_test.lean b/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/ack_codec_test.lean
index a2e8762c..a7d6295b 100644
--- a/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/ack_codec_test.lean
+++ b/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/ack_codec_test.lean
@@ -7,7 +7,7 @@ import Lean.Data.Json
 
 import Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec
 import Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.AckBytes
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # `Acks` field vectors
 
@@ -17,7 +17,7 @@ neither. -/
 
 open Lean
 open Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.AckCodec
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 def hexNats (s : String) : Except String (List ℕ) :=
   match hexStringToByteArray s with
diff --git a/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/wire_vectors_test.lean b/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/wire_vectors_test.lean
index c1feb34a..1788bcae 100644
--- a/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/wire_vectors_test.lean
+++ b/Cryptlib/Protocols/GroupComm/GroupChatKatzenqt1/wire_vectors_test.lean
@@ -8,7 +8,7 @@ import Lean.Data.Json
 import Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Gcm
 import Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.Membership
 import Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member.ReplyWho
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-! # Group chat wire vectors
 
@@ -19,7 +19,7 @@ carries the same `JoinReply`. -/
 
 open Lean
 open Cryptlib.Protocols.GroupComm.GroupChatKatzenqt1.Member
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 
 def hex (s : String) : Except String ByteArray :=
   match hexStringToByteArray s with
diff --git a/Cryptlib/Protocols/Sphinx/commands.lean b/Cryptlib/Protocols/Sphinx/Commands.lean
similarity index 99%
rename from Cryptlib/Protocols/Sphinx/commands.lean
rename to Cryptlib/Protocols/Sphinx/Commands.lean
index 2d99a216..c0fc1978 100644
--- a/Cryptlib/Protocols/Sphinx/commands.lean
+++ b/Cryptlib/Protocols/Sphinx/Commands.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import Mathlib.Tactic.Set
 import Mathlib.Tactic.IntervalCases
-import Cryptlib.Protocols.Sphinx.constants
+import Cryptlib.Protocols.Sphinx.Constants
 import Cryptlib.Util.Bytes
 
 namespace Cryptlib.Protocols.Sphinx.Commands
diff --git a/Cryptlib/Protocols/Sphinx/common.lean b/Cryptlib/Protocols/Sphinx/Common.lean
similarity index 99%
rename from Cryptlib/Protocols/Sphinx/common.lean
rename to Cryptlib/Protocols/Sphinx/Common.lean
index fe0a042d..82d5290d 100644
--- a/Cryptlib/Protocols/Sphinx/common.lean
+++ b/Cryptlib/Protocols/Sphinx/Common.lean
@@ -3,8 +3,8 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.commands
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Commands
 import Cryptlib.Primitives.MAC.HMAC
 import Cryptlib.Util.Bytes
 
diff --git a/Cryptlib/Protocols/Sphinx/constants.lean b/Cryptlib/Protocols/Sphinx/Constants.lean
similarity index 100%
rename from Cryptlib/Protocols/Sphinx/constants.lean
rename to Cryptlib/Protocols/Sphinx/Constants.lean
diff --git a/Cryptlib/Protocols/Sphinx/geometry.lean b/Cryptlib/Protocols/Sphinx/Geometry.lean
similarity index 99%
rename from Cryptlib/Protocols/Sphinx/geometry.lean
rename to Cryptlib/Protocols/Sphinx/Geometry.lean
index 7de14627..0920b13e 100644
--- a/Cryptlib/Protocols/Sphinx/geometry.lean
+++ b/Cryptlib/Protocols/Sphinx/Geometry.lean
@@ -3,7 +3,7 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.constants
+import Cryptlib.Protocols.Sphinx.Constants
 import Cryptlib.Primitives.NIKE.Schemes
 import Cryptlib.Primitives.KEM.Schemes
 
diff --git a/Cryptlib/Protocols/Sphinx/geometry_cbor.lean b/Cryptlib/Protocols/Sphinx/GeometryCbor.lean
similarity index 98%
rename from Cryptlib/Protocols/Sphinx/geometry_cbor.lean
rename to Cryptlib/Protocols/Sphinx/GeometryCbor.lean
index 0a51c27e..9cc56fea 100644
--- a/Cryptlib/Protocols/Sphinx/geometry_cbor.lean
+++ b/Cryptlib/Protocols/Sphinx/GeometryCbor.lean
@@ -4,7 +4,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Cborg
-import Cryptlib.Protocols.Sphinx.geometry
+import Cryptlib.Protocols.Sphinx.Geometry
 import Cryptlib.Primitives.Hash.Blake2b
 
 namespace Cryptlib.Protocols.Sphinx.Geometry
diff --git a/Cryptlib/Protocols/Sphinx/indistinguishability.lean b/Cryptlib/Protocols/Sphinx/Indistinguishability.lean
similarity index 100%
rename from Cryptlib/Protocols/Sphinx/indistinguishability.lean
rename to Cryptlib/Protocols/Sphinx/Indistinguishability.lean
diff --git a/Cryptlib/Protocols/Sphinx/integrity.lean b/Cryptlib/Protocols/Sphinx/Integrity.lean
similarity index 100%
rename from Cryptlib/Protocols/Sphinx/integrity.lean
rename to Cryptlib/Protocols/Sphinx/Integrity.lean
diff --git a/Cryptlib/Protocols/Sphinx/sphinx.lean b/Cryptlib/Protocols/Sphinx/Interface.lean
similarity index 97%
rename from Cryptlib/Protocols/Sphinx/sphinx.lean
rename to Cryptlib/Protocols/Sphinx/Interface.lean
index b7460edb..bfc800a2 100644
--- a/Cryptlib/Protocols/Sphinx/sphinx.lean
+++ b/Cryptlib/Protocols/Sphinx/Interface.lean
@@ -5,10 +5,10 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import VCVio.OracleComp.Constructions.SampleableType
 
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.indistinguishability
-import Cryptlib.Protocols.Sphinx.integrity
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Indistinguishability
+import Cryptlib.Protocols.Sphinx.Integrity
 import Cryptlib.Primitives.WideBlockCipher.WideBlockCipher
 import Cryptlib.Primitives.MAC.MAC
 import Cryptlib.Primitives.KDF.KDF
diff --git a/Cryptlib/Protocols/Sphinx/kdf.lean b/Cryptlib/Protocols/Sphinx/KDF.lean
similarity index 100%
rename from Cryptlib/Protocols/Sphinx/kdf.lean
rename to Cryptlib/Protocols/Sphinx/KDF.lean
diff --git a/Cryptlib/Protocols/Sphinx/kem_sphinx.lean b/Cryptlib/Protocols/Sphinx/KEMSphinx.lean
similarity index 83%
rename from Cryptlib/Protocols/Sphinx/kem_sphinx.lean
rename to Cryptlib/Protocols/Sphinx/KEMSphinx.lean
index 735f6c8c..9c3a1973 100644
--- a/Cryptlib/Protocols/Sphinx/kem_sphinx.lean
+++ b/Cryptlib/Protocols/Sphinx/KEMSphinx.lean
@@ -3,20 +3,20 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.constants
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.commands
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.sphinx
-import Cryptlib.Protocols.Sphinx.common
-import Cryptlib.Protocols.Sphinx.nike_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
+import Cryptlib.Protocols.Sphinx.Constants
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Commands
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.Interface
+import Cryptlib.Protocols.Sphinx.Common
+import Cryptlib.Protocols.Sphinx.NIKESphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
 import Cryptlib.Primitives.WideBlockCipher.WideBlockCipher
 import Cryptlib.Primitives.WideBlockCipher.AEZ
 import Cryptlib.Primitives.MAC.MAC
 import Cryptlib.Primitives.KDF.KDF
 import Cryptlib.Primitives.KDF.HKDF
-import Cryptlib.Protocols.Sphinx.kdf
+import Cryptlib.Protocols.Sphinx.KDF
 import Cryptlib.Primitives.StreamCipher.StreamCipher
 import Cryptlib.Primitives.StreamCipher.AES256CTR
 import Cryptlib.Primitives.KEM.KEM
diff --git a/Cryptlib/Protocols/Sphinx/kem_sphinx_theorems.lean b/Cryptlib/Protocols/Sphinx/KEMSphinxTheorems.lean
similarity index 99%
rename from Cryptlib/Protocols/Sphinx/kem_sphinx_theorems.lean
rename to Cryptlib/Protocols/Sphinx/KEMSphinxTheorems.lean
index 5eca24c3..f252386f 100644
--- a/Cryptlib/Protocols/Sphinx/kem_sphinx_theorems.lean
+++ b/Cryptlib/Protocols/Sphinx/KEMSphinxTheorems.lean
@@ -3,21 +3,21 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.constants
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.commands
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.sphinx
-import Cryptlib.Protocols.Sphinx.common
-import Cryptlib.Protocols.Sphinx.nike_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.kem_sphinx
-import Cryptlib.Protocols.Sphinx.surb
+import Cryptlib.Protocols.Sphinx.Constants
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Commands
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.Interface
+import Cryptlib.Protocols.Sphinx.Common
+import Cryptlib.Protocols.Sphinx.NIKESphinxTheorems
+import Cryptlib.Protocols.Sphinx.KEMSphinx
+import Cryptlib.Protocols.Sphinx.SURB
 import Cryptlib.Primitives.WideBlockCipher.WideBlockCipher
 import Cryptlib.Primitives.WideBlockCipher.AEZ
 import Cryptlib.Primitives.MAC.MAC
 import Cryptlib.Primitives.KDF.KDF
 import Cryptlib.Primitives.KDF.HKDF
-import Cryptlib.Protocols.Sphinx.kdf
+import Cryptlib.Protocols.Sphinx.KDF
 import Cryptlib.Primitives.StreamCipher.StreamCipher
 import Cryptlib.Primitives.StreamCipher.AES256CTR
 import Cryptlib.Primitives.KEM.KEM
diff --git a/Cryptlib/Protocols/Sphinx/nike_sphinx.lean b/Cryptlib/Protocols/Sphinx/NIKESphinx.lean
similarity index 90%
rename from Cryptlib/Protocols/Sphinx/nike_sphinx.lean
rename to Cryptlib/Protocols/Sphinx/NIKESphinx.lean
index 955d24f3..f640492d 100644
--- a/Cryptlib/Protocols/Sphinx/nike_sphinx.lean
+++ b/Cryptlib/Protocols/Sphinx/NIKESphinx.lean
@@ -3,14 +3,14 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.constants
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.commands
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.sphinx
-import Cryptlib.Protocols.Sphinx.common
-import Cryptlib.Protocols.Sphinx.surb
-import Cryptlib.Protocols.Sphinx.kdf
+import Cryptlib.Protocols.Sphinx.Constants
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Commands
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.Interface
+import Cryptlib.Protocols.Sphinx.Common
+import Cryptlib.Protocols.Sphinx.SURB
+import Cryptlib.Protocols.Sphinx.KDF
 import Cryptlib.Primitives.Cipher.ChaCha20
 import Cryptlib.Primitives.WideBlockCipher.WideBlockCipher
 import Cryptlib.Primitives.WideBlockCipher.AEZ
diff --git a/Cryptlib/Protocols/Sphinx/nike_sphinx_theorems.lean b/Cryptlib/Protocols/Sphinx/NIKESphinxTheorems.lean
similarity index 99%
rename from Cryptlib/Protocols/Sphinx/nike_sphinx_theorems.lean
rename to Cryptlib/Protocols/Sphinx/NIKESphinxTheorems.lean
index 9e99dd90..5f38ec5e 100644
--- a/Cryptlib/Protocols/Sphinx/nike_sphinx_theorems.lean
+++ b/Cryptlib/Protocols/Sphinx/NIKESphinxTheorems.lean
@@ -3,14 +3,14 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.constants
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.commands
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.sphinx
-import Cryptlib.Protocols.Sphinx.common
-import Cryptlib.Protocols.Sphinx.surb
-import Cryptlib.Protocols.Sphinx.kdf
+import Cryptlib.Protocols.Sphinx.Constants
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Commands
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.Interface
+import Cryptlib.Protocols.Sphinx.Common
+import Cryptlib.Protocols.Sphinx.SURB
+import Cryptlib.Protocols.Sphinx.KDF
 import Cryptlib.Primitives.Cipher.ChaCha20
 import Cryptlib.Primitives.WideBlockCipher.WideBlockCipher
 import Cryptlib.Primitives.WideBlockCipher.AEZ
@@ -21,10 +21,10 @@ import Cryptlib.Primitives.StreamCipher.StreamCipher
 import Cryptlib.Primitives.StreamCipher.AES256CTR
 import Cryptlib.Primitives.NIKE.NIKE
 import Cryptlib.Primitives.NIKE.Schemes
-import Cryptlib.Protocols.Sphinx.wrap_resistance
+import Cryptlib.Protocols.Sphinx.WrapResistance
 import Cryptlib.Primitives.Hash.Sha512
 import Cryptlib.Util.Bytes
-import Cryptlib.Protocols.Sphinx.nike_sphinx
+import Cryptlib.Protocols.Sphinx.NIKESphinx
 
 namespace Cryptlib.Protocols.Sphinx.NIKESphinx
 
diff --git a/Cryptlib/Protocols/Sphinx/surb.lean b/Cryptlib/Protocols/Sphinx/SURB.lean
similarity index 95%
rename from Cryptlib/Protocols/Sphinx/surb.lean
rename to Cryptlib/Protocols/Sphinx/SURB.lean
index 76760f41..96626c5f 100644
--- a/Cryptlib/Protocols/Sphinx/surb.lean
+++ b/Cryptlib/Protocols/Sphinx/SURB.lean
@@ -3,9 +3,9 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.constants
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.common
+import Cryptlib.Protocols.Sphinx.Constants
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Common
 import Cryptlib.Primitives.WideBlockCipher.WideBlockCipher
 import Cryptlib.Util.Bytes
 
diff --git a/Cryptlib/Protocols/Sphinx/schemes.lean b/Cryptlib/Protocols/Sphinx/Schemes.lean
similarity index 87%
rename from Cryptlib/Protocols/Sphinx/schemes.lean
rename to Cryptlib/Protocols/Sphinx/Schemes.lean
index d1a785ae..1e5b1f8b 100644
--- a/Cryptlib/Protocols/Sphinx/schemes.lean
+++ b/Cryptlib/Protocols/Sphinx/Schemes.lean
@@ -3,9 +3,9 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.nike_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.kem_sphinx_theorems
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.NIKESphinxTheorems
+import Cryptlib.Protocols.Sphinx.KEMSphinxTheorems
 import Cryptlib.Primitives.NIKE.Schemes
 import Cryptlib.Primitives.KEM.Schemes
 
diff --git a/Cryptlib/Protocols/Sphinx/types.lean b/Cryptlib/Protocols/Sphinx/Types.lean
similarity index 93%
rename from Cryptlib/Protocols/Sphinx/types.lean
rename to Cryptlib/Protocols/Sphinx/Types.lean
index f97f9af7..c55a1df4 100644
--- a/Cryptlib/Protocols/Sphinx/types.lean
+++ b/Cryptlib/Protocols/Sphinx/Types.lean
@@ -3,7 +3,7 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.commands
+import Cryptlib.Protocols.Sphinx.Commands
 
 namespace Cryptlib.Protocols.Sphinx.Types
 
diff --git a/Cryptlib/Protocols/Sphinx/wrap_resistance.lean b/Cryptlib/Protocols/Sphinx/WrapResistance.lean
similarity index 96%
rename from Cryptlib/Protocols/Sphinx/wrap_resistance.lean
rename to Cryptlib/Protocols/Sphinx/WrapResistance.lean
index ace4deda..25a15573 100644
--- a/Cryptlib/Protocols/Sphinx/wrap_resistance.lean
+++ b/Cryptlib/Protocols/Sphinx/WrapResistance.lean
@@ -5,7 +5,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 
 import VCVio.CryptoFoundations.HardnessAssumptions.DiffieHellman
 import Cryptlib.Primitives.NIKE.X25519
-import Cryptlib.Protocols.Sphinx.nike_sphinx
+import Cryptlib.Protocols.Sphinx.NIKESphinx
 import Cryptlib.Util.UniformHit
 
 /-! # Wrap-resistance (§4.3)
diff --git a/Cryptlib/Protocols/Sphinx/commands_test.lean b/Cryptlib/Protocols/Sphinx/commands_test.lean
index ff0e371d..deea598a 100644
--- a/Cryptlib/Protocols/Sphinx/commands_test.lean
+++ b/Cryptlib/Protocols/Sphinx/commands_test.lean
@@ -4,8 +4,8 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Lean.Data.Json
-import Cryptlib.Protocols.Sphinx.commands
-import Cryptlib.Util.newhex
+import Cryptlib.Protocols.Sphinx.Commands
+import Cryptlib.Util.HexBytes
 
 /-!
 # Sphinx routing-command known-answer tests
@@ -14,7 +14,7 @@ Checks `RoutingCommand.toBytes` against `testdata/sphinx_commands_vectors.json`
 each through `fromBytesOne`. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Commands
 
 def field (j : Json) (k : String) : Except String ByteArray := do
diff --git a/Cryptlib/Protocols/Sphinx/crypto_test.lean b/Cryptlib/Protocols/Sphinx/crypto_test.lean
index 33dfaf37..cd545f34 100644
--- a/Cryptlib/Protocols/Sphinx/crypto_test.lean
+++ b/Cryptlib/Protocols/Sphinx/crypto_test.lean
@@ -7,9 +7,9 @@ import Lean.Data.Json
 import Cryptlib.Primitives.Hash.Sha512
 import Cryptlib.Primitives.MAC.HMAC
 import Cryptlib.Primitives.StreamCipher.AES256CTR
-import Cryptlib.Protocols.Sphinx.kdf
+import Cryptlib.Protocols.Sphinx.KDF
 import Cryptlib.Primitives.Cipher.ChaCha20
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 
 /-!
 # Sphinx primitive known-answer tests: hash, MAC, stream cipher, KDF, ChaCha20
@@ -17,7 +17,7 @@ import Cryptlib.Util.newhex
 Vectors are vendored from katzenpost; each `testdata/sphinx_*.json.sha256` records the copy. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Primitives.Hash.Sha512 (sha512_256)
 open Cryptlib.Primitives.Cipher.ChaCha20 (keystream32)
 open Cryptlib.Primitives.MAC.HMAC (hmacSha256)
diff --git a/Cryptlib/Protocols/Sphinx/gen_kem_vectors.lean b/Cryptlib/Protocols/Sphinx/gen_kem_vectors.lean
index 2374f9a7..4e82bed1 100644
--- a/Cryptlib/Protocols/Sphinx/gen_kem_vectors.lean
+++ b/Cryptlib/Protocols/Sphinx/gen_kem_vectors.lean
@@ -4,11 +4,11 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Lean.Data.Json
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.kem_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
-import Cryptlib.Util.newhex
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.KEMSphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Bytes
 
 /-!
@@ -19,7 +19,7 @@ unwrapping by another implementation. Runs for `X25519LadderKEM`, `MLKEM768X2551
 `mlkem768-x25519-blake2bxof-kem`. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 open Cryptlib.Protocols.Sphinx.Commands
 open Cryptlib.Protocols.Sphinx.Types
diff --git a/Cryptlib/Protocols/Sphinx/gen_nike_vectors.lean b/Cryptlib/Protocols/Sphinx/gen_nike_vectors.lean
index 7021926e..533701e2 100644
--- a/Cryptlib/Protocols/Sphinx/gen_nike_vectors.lean
+++ b/Cryptlib/Protocols/Sphinx/gen_nike_vectors.lean
@@ -4,12 +4,12 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Lean.Data.Json
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.nike_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.NIKESphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
 import Cryptlib.Primitives.NIKE.X25519_montgomery_ladder
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Bytes
 
 /-!
@@ -19,7 +19,7 @@ Builds packets with `createHeader`/`newNIKEPacket`/`newNIKESURB` and writes them
 unwrapping by another implementation, over `withSURB ∈ {false,true} × nrHops 1..5`. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 open Cryptlib.Protocols.Sphinx.Commands
 open Cryptlib.Protocols.Sphinx.Types
diff --git a/Cryptlib/Protocols/Sphinx/geometry_test.lean b/Cryptlib/Protocols/Sphinx/geometry_test.lean
index f1694231..4e0b63ce 100644
--- a/Cryptlib/Protocols/Sphinx/geometry_test.lean
+++ b/Cryptlib/Protocols/Sphinx/geometry_test.lean
@@ -4,8 +4,8 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Lean.Data.Json
-import Cryptlib.Protocols.Sphinx.geometry_cbor
-import Cryptlib.Util.newhex
+import Cryptlib.Protocols.Sphinx.GeometryCbor
+import Cryptlib.Util.HexBytes
 
 /-! # Sphinx geometry tests
 
@@ -15,7 +15,7 @@ Checks `ofNIKE`/`ofKEM`, the CBOR encoding, `hash` and `validate` against
 
 open Lean
 open Cborg
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 
 def hexField (j : Json) (k : String) : Except String ByteArray := do
diff --git a/Cryptlib/Protocols/Sphinx/kem_hybrid_blake2bxof_vectors_test.lean b/Cryptlib/Protocols/Sphinx/kem_hybrid_blake2bxof_vectors_test.lean
index cd1f9ec0..c3345695 100644
--- a/Cryptlib/Protocols/Sphinx/kem_hybrid_blake2bxof_vectors_test.lean
+++ b/Cryptlib/Protocols/Sphinx/kem_hybrid_blake2bxof_vectors_test.lean
@@ -4,10 +4,10 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Lean.Data.Json
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.kem_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
-import Cryptlib.Util.newhex
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.KEMSphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Bytes
 
 /-!
@@ -16,7 +16,7 @@ import Cryptlib.Util.Bytes
 As `kem_hybrid_vectors_test`, for `kemMLKEM768X25519Blake2b`. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 open Cryptlib.Protocols.Sphinx.Commands
 open Cryptlib.Protocols.Sphinx.KEMSphinx
diff --git a/Cryptlib/Protocols/Sphinx/kem_hybrid_vectors_test.lean b/Cryptlib/Protocols/Sphinx/kem_hybrid_vectors_test.lean
index 60cca0ae..1cc585e0 100644
--- a/Cryptlib/Protocols/Sphinx/kem_hybrid_vectors_test.lean
+++ b/Cryptlib/Protocols/Sphinx/kem_hybrid_vectors_test.lean
@@ -4,10 +4,10 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Lean.Data.Json
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.kem_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
-import Cryptlib.Util.newhex
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.KEMSphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Bytes
 
 /-!
@@ -16,7 +16,7 @@ import Cryptlib.Util.Bytes
 As `kem_vectors_test`, for `"MLKEM768X25519"` with the SHA256-v1 combiner PRF. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 open Cryptlib.Protocols.Sphinx.Commands
 open Cryptlib.Protocols.Sphinx.KEMSphinx
diff --git a/Cryptlib/Protocols/Sphinx/kem_selftest.lean b/Cryptlib/Protocols/Sphinx/kem_selftest.lean
index add6f1ec..7da9bf96 100644
--- a/Cryptlib/Protocols/Sphinx/kem_selftest.lean
+++ b/Cryptlib/Protocols/Sphinx/kem_selftest.lean
@@ -3,11 +3,11 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.kem_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
-import Cryptlib.Util.newhex
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.KEMSphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Bytes
 
 /-!
@@ -16,7 +16,7 @@ import Cryptlib.Util.Bytes
 Builds packets with fresh keys and checks that unwrapping recovers them, for every registered
 KEM-Sphinx scheme. -/
 
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 open Cryptlib.Protocols.Sphinx.Types
 open Cryptlib.Protocols.Sphinx.Commands
diff --git a/Cryptlib/Protocols/Sphinx/kem_vectors_test.lean b/Cryptlib/Protocols/Sphinx/kem_vectors_test.lean
index 371be9ff..efe49d6b 100644
--- a/Cryptlib/Protocols/Sphinx/kem_vectors_test.lean
+++ b/Cryptlib/Protocols/Sphinx/kem_vectors_test.lean
@@ -4,11 +4,11 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Lean.Data.Json
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.kem_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.KEMSphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
 import Cryptlib.Primitives.NIKE.X25519_montgomery_ladder
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Bytes
 
 /-!
@@ -18,7 +18,7 @@ Replays `unwrapKEM` hop by hop over externally built KEM-Sphinx packets
 (`withSURB ∈ {false, true} × nrHops 1..5`). -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 open Cryptlib.Protocols.Sphinx.Commands
 open Cryptlib.Protocols.Sphinx.KEMSphinx
diff --git a/Cryptlib/Protocols/Sphinx/nike_selftest.lean b/Cryptlib/Protocols/Sphinx/nike_selftest.lean
index 39d88482..7ee23e0e 100644
--- a/Cryptlib/Protocols/Sphinx/nike_selftest.lean
+++ b/Cryptlib/Protocols/Sphinx/nike_selftest.lean
@@ -3,11 +3,11 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.nike_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
-import Cryptlib.Util.newhex
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.NIKESphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Bytes
 
 /-!
@@ -16,7 +16,7 @@ import Cryptlib.Util.Bytes
 Builds packets with fresh keys and checks that unwrapping recovers the commands and payload, for
 every registered NIKE-Sphinx scheme. -/
 
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 open Cryptlib.Protocols.Sphinx.Types
 open Cryptlib.Protocols.Sphinx.Commands
diff --git a/Cryptlib/Protocols/Sphinx/nike_vectors_test.lean b/Cryptlib/Protocols/Sphinx/nike_vectors_test.lean
index a905f048..51df1289 100644
--- a/Cryptlib/Protocols/Sphinx/nike_vectors_test.lean
+++ b/Cryptlib/Protocols/Sphinx/nike_vectors_test.lean
@@ -4,11 +4,11 @@ SPDX-License-Identifier: AGPL-3.0-only
 -/
 
 import Lean.Data.Json
-import Cryptlib.Protocols.Sphinx.geometry
-import Cryptlib.Protocols.Sphinx.nike_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.surb
+import Cryptlib.Protocols.Sphinx.Geometry
+import Cryptlib.Protocols.Sphinx.NIKESphinxTheorems
+import Cryptlib.Protocols.Sphinx.SURB
 import Cryptlib.Primitives.NIKE.X25519_montgomery_ladder
-import Cryptlib.Util.newhex
+import Cryptlib.Util.HexBytes
 import Cryptlib.Util.Bytes
 
 /-!
@@ -19,7 +19,7 @@ Replays `unwrapNIKE` hop by hop over externally built Sphinx packets
 byte for byte. -/
 
 open Lean
-open Cryptlib.Util.newhex
+open Cryptlib.Util.HexBytes
 open Cryptlib.Protocols.Sphinx.Geometry
 open Cryptlib.Protocols.Sphinx.Commands
 open Cryptlib.Protocols.Sphinx.NIKESphinx
diff --git a/Cryptlib/Util/newhex.lean b/Cryptlib/Util/HexBytes.lean
similarity index 97%
rename from Cryptlib/Util/newhex.lean
rename to Cryptlib/Util/HexBytes.lean
index 162e48a5..5d1d71ac 100644
--- a/Cryptlib/Util/newhex.lean
+++ b/Cryptlib/Util/HexBytes.lean
@@ -1,7 +1,7 @@
 
 import Mathlib.Data.String.Basic
 
-namespace Cryptlib.Util.newhex
+namespace Cryptlib.Util.HexBytes
 
 def byteToHex (b : UInt8) : String :=
   let high := hexDigitRepr (b.toNat / 16)
@@ -59,4 +59,4 @@ def falliableHexStringToByteArray (s : String) : ByteArray :=
         | none => panic! "Failed to convert hex string to ByteArray."
   | _, _ => panic! "Hex string length must be even or 1."
 
-end Cryptlib.Util.newhex
+end Cryptlib.Util.HexBytes
diff --git a/Cryptlib/Util/newnat.lean b/Cryptlib/Util/NatBytes.lean
similarity index 94%
rename from Cryptlib/Util/newnat.lean
rename to Cryptlib/Util/NatBytes.lean
index 1d67862a..9a1d573d 100644
--- a/Cryptlib/Util/newnat.lean
+++ b/Cryptlib/Util/NatBytes.lean
@@ -1,4 +1,4 @@
-namespace Cryptlib.Util.newnat
+namespace Cryptlib.Util.NatBytes
 
 def natToBytesAux (n : Nat) (acc : List UInt8) : List UInt8 :=
   if n == 0 then acc else natToBytesAux (n / 256) (UInt8.ofNat (n % 256) :: acc)
@@ -35,4 +35,4 @@ theorem natToBytes_length_le_32 (n : Nat) (h : n < 256 ^ 32) :
   simpa [natToBytes] using natToBytesAux_length_le 32 n [] h
 
 
-end Cryptlib.Util.newnat
+end Cryptlib.Util.NatBytes
diff --git a/Makefile b/Makefile
index 02e12217..6e97c3db 100644
--- a/Makefile
+++ b/Makefile
@@ -54,7 +54,7 @@ TEST_BINS := $(foreach t,$(TESTS),$(BIN)/$(subst .,-,$(t)))
 # Bare `lake build` builds only defaultTargets, which is the library. The
 # executables have to be named or the test targets run whatever binary was left
 # in .lake/build/bin by an earlier build.
-EXES := $(TESTS) Cryptlib.Protocols.BACAP.gen_vectors Cryptlib.Bench.benchmark Cryptlib.Protocols.Sphinx.gen_nike_vectors Cryptlib.Protocols.Sphinx.gen_kem_vectors Cryptlib.Primitives.KEM.gen_mlkem768_x25519_combiner_vectors Cryptlib.Primitives.KEM.gen_mlkem_hedged_vectors Cryptlib.Primitives.MultiRecipientHybrid.gen_multirecipient_hybrid_vectors
+EXES := $(TESTS) Cryptlib.Protocols.BACAP.gen_vectors Cryptlib.Protocols.Sphinx.gen_nike_vectors Cryptlib.Protocols.Sphinx.gen_kem_vectors Cryptlib.Primitives.KEM.gen_mlkem768_x25519_combiner_vectors Cryptlib.Primitives.KEM.gen_mlkem_hedged_vectors Cryptlib.Primitives.MultiRecipientHybrid.gen_multirecipient_hybrid_vectors
 
 .DEFAULT_GOAL := help
 
@@ -77,9 +77,9 @@ build: mathlib-cache ## build everything, library and executables
 
 # A suite counts as failed if it exits non-zero or prints anything matching
 # "fail". Most suites signal a mismatch by throwing, which exits 1, but
-# Cryptlib/Data/test.lean only prints on mismatch and still exits 0. No
-# passing suite prints the word, so scanning for it costs nothing and catches
-# that case along with any future suite that reports the same way.
+# Cryptlib/Data/test.lean only prints on mismatch and still exits 0. Lines
+# starting with "ok" are skipped: a passing negative test can name the failure
+# it expected, such as decrypt_failed.
 test: build ## run every suite and report all failures
 	@rc=0; \
 	for bin in $(TEST_BINS); do \
@@ -87,7 +87,7 @@ test: build ## run every suite and report all failures
 	  printf '\n=== %s ===\n' "$$name"; \
 	  out=$$("$$bin" 2>&1); status=$$?; \
 	  printf '%s\n' "$$out"; \
-	  if [ $$status -ne 0 ] || printf '%s' "$$out" | grep -qi 'fail'; then \
+	  if [ $$status -ne 0 ] || printf '%s\n' "$$out" | grep -vE '^[[:space:]]*ok[[:space:]]' | grep -qi 'fail'; then \
 	    rc=1; printf '  ^^ %s FAILED\n' "$$name"; \
 	  fi; \
 	done; \
@@ -202,7 +202,8 @@ BENCH_ARGS ?=
 
 # Quiet: otherwise Lake replays LeanBench's missing-docstring warnings and VCVio's native-backend
 # notices on every run.
-BENCH := $(LAKE) -q --log-level=error exe Cryptlib.Bench.benchmark
+# The benchmarks are their own Lake project in bench/, so the library does not depend on LeanBench.
+BENCH := cd bench && $(LAKE) -q --log-level=error exe cryptlib-bench
 
 bench: ## run every benchmark (NIKE, KEM, Sphinx); pass LeanBench flags via BENCH_ARGS
 	@$(BENCH) $(BENCH_ARGS)
diff --git a/README.md b/README.md
index decd95da..353791fb 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,9 @@
-# Crypt Walker
+# Cryptlib
 
 *A cryptographic library for Lean.*
 
+This library has not been audited by any third party.
+
 
 ## abstract
 
@@ -135,7 +137,7 @@ lake exe Cryptlib.Protocols.Sphinx.nike_selftest    # NIKE-Sphinx round-trip sel
 lake exe Cryptlib.Protocols.Sphinx.kem_selftest     # KEM-Sphinx round-trip self-tests
 lake exe Cryptlib.Protocols.Sphinx.nike_vectors_test  # NIKE-Sphinx full-packet vectors from katzenpost
 lake exe Cryptlib.Protocols.Sphinx.kem_vectors_test   # KEM-Sphinx full-packet vectors from katzenpost
-lake exe Cryptlib.Primitives.KEM.MLKEM.mlkem768_test   # ML-KEM-768 NIST ACVP known-answer vectors
+lake exe Cryptlib.Primitives.KEM.MLKEM.mlkem_test      # ML-KEM-768 NIST ACVP known-answer vectors
 lake exe Cryptlib.Primitives.Hash.blake2b_256_test     # BLAKE2b-256 (unkeyed and keyed) vectors from hpqc
 lake exe Cryptlib.Primitives.KEM.mlkem768_x25519_combiner_test  # X25519+ML-KEM-768 hybrid vectors from hpqc
 lake exe Cryptlib.Protocols.Sphinx.kem_hybrid_vectors_test     # KEM-Sphinx hybrid full-packet vectors from katzenpost
@@ -216,7 +218,7 @@ make bench BENCH_ARGS='--match "kem MLKEM768 decap"'    # one specific bench
 
 Any LeanBench flag works in `BENCH_ARGS`: e.g. `--samples 5`, `--tags unwrap`, or
 `--save baseline.json` then `--compare baseline.json`. To call Lake directly, use
-`lake -q --log-level=error exe Cryptlib.Bench.benchmark ...`; without those flags Lake replays
+`cd bench && lake -q --log-level=error exe cryptlib-bench ...`; without those flags Lake replays
 build warnings from our dependencies first. No numbers here — they depend entirely on the machine.
 
 ## licensing
diff --git a/bench/.gitignore b/bench/.gitignore
new file mode 100644
index 00000000..bfb30ec8
--- /dev/null
+++ b/bench/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/Cryptlib/Bench/Cipher.lean b/bench/CryptlibBench/Cipher.lean
similarity index 97%
rename from Cryptlib/Bench/Cipher.lean
rename to bench/CryptlibBench/Cipher.lean
index f7b44f1c..f471c91d 100644
--- a/Cryptlib/Bench/Cipher.lean
+++ b/bench/CryptlibBench/Cipher.lean
@@ -12,7 +12,7 @@ import LeanBench
 
 Inputs are read from refs so the compiler cannot hoist the work out of the timed action. -/
 
-namespace Cryptlib.Bench.Cipher
+namespace CryptlibBench.Cipher
 
 open Cryptlib.Primitives.Cipher.ChaChaPoly (chacha20 poly1305)
 open Cryptlib.Primitives.Cipher.Polyval (polyval)
@@ -42,4 +42,4 @@ def benches : IO (Array LeanBench.Bench) := do
                         ByteArray.empty (← msg.get)) }
   pure bs
 
-end Cryptlib.Bench.Cipher
+end CryptlibBench.Cipher
diff --git a/Cryptlib/Bench/Field25519.lean b/bench/CryptlibBench/Field25519.lean
similarity index 95%
rename from Cryptlib/Bench/Field25519.lean
rename to bench/CryptlibBench/Field25519.lean
index 06cf3d7a..96ddf360 100644
--- a/Cryptlib/Bench/Field25519.lean
+++ b/bench/CryptlibBench/Field25519.lean
@@ -10,7 +10,7 @@ import LeanBench
 
 Inputs are read from refs so the compiler cannot hoist the work out of the timed action. -/
 
-namespace Cryptlib.Bench.Field25519
+namespace CryptlibBench.Field25519
 
 open Cryptlib.Primitives.NIKE.Field25519 (Fe)
 open Cryptlib.Primitives.NIKE.X25519_montgomery_ladder (curve25519 curve25519_fe basepointBytes)
@@ -33,4 +33,4 @@ def benches : IO (Array LeanBench.Bench) := do
     { name := "x25519 ladder (ZMod)", config := cfg,
       action := do out.set (curve25519 (← scalar.get) (← base.get)) }]
 
-end Cryptlib.Bench.Field25519
+end CryptlibBench.Field25519
diff --git a/Cryptlib/Bench/KDF.lean b/bench/CryptlibBench/KDF.lean
similarity index 95%
rename from Cryptlib/Bench/KDF.lean
rename to bench/CryptlibBench/KDF.lean
index 421c7f02..1cb47691 100644
--- a/Cryptlib/Bench/KDF.lean
+++ b/bench/CryptlibBench/KDF.lean
@@ -10,7 +10,7 @@ import LeanBench
 
 Inputs are read from refs so the compiler cannot hoist the work out of the timed action. -/
 
-namespace Cryptlib.Bench.KDF
+namespace CryptlibBench.KDF
 
 open Cryptlib.Primitives.KDF.Argon2
 
@@ -29,4 +29,4 @@ def benches : IO (Array LeanBench.Bench) := do
                       out.set ((hash { memoryKiB := m, passes := 3 } (← pw.get) (← salt.get)).toOption.getD .empty) }
   pure bs
 
-end Cryptlib.Bench.KDF
+end CryptlibBench.KDF
diff --git a/Cryptlib/Bench/KEM.lean b/bench/CryptlibBench/KEM.lean
similarity index 97%
rename from Cryptlib/Bench/KEM.lean
rename to bench/CryptlibBench/KEM.lean
index 46328637..0dede521 100644
--- a/Cryptlib/Bench/KEM.lean
+++ b/bench/CryptlibBench/KEM.lean
@@ -11,7 +11,7 @@ import LeanBench
 Each sample runs from a freshly seeded state; `decap` gets a fresh ciphertext per sample. Keys and
 ciphertexts are prepared outside the timed region. -/
 
-namespace Cryptlib.Bench.KEM
+namespace CryptlibBench.KEM
 
 open Cryptlib.Primitives.KEM.KEM (KEM)
 open Cryptlib.Util.Bytes (ofVector)
@@ -59,4 +59,4 @@ def benches (name : String) (kem : KEM) : IO (Array LeanBench.Bench) := do
         | .ok k _ => out.set (ofVector (kem.encodePlaintext k))
         | .error _ _ => fail "decap" }]
 
-end Cryptlib.Bench.KEM
+end CryptlibBench.KEM
diff --git a/Cryptlib/Bench/MLKEMSteps.lean b/bench/CryptlibBench/MLKEMSteps.lean
similarity index 97%
rename from Cryptlib/Bench/MLKEMSteps.lean
rename to bench/CryptlibBench/MLKEMSteps.lean
index 05128a50..9a787228 100644
--- a/Cryptlib/Bench/MLKEMSteps.lean
+++ b/bench/CryptlibBench/MLKEMSteps.lean
@@ -11,7 +11,7 @@ import LeanBench
 Each bench is one step of `FIPS203.encaps`. Inputs are computed once from a real key pair and read
 from a ref so the compiler cannot hoist the work out of the timed action. -/
 
-namespace Cryptlib.Bench.MLKEMSteps
+namespace CryptlibBench.MLKEMSteps
 
 open MLKEM
 open Cryptlib.Primitives.KEM.FIPS203
@@ -65,4 +65,4 @@ def benches : IO (Array LeanBench.Bench) := do
     ← step "compressDV" v fun v => enc.compressDV v,
     ← step "byteEncodeDV ∘ compressDV" v fun v => enc.byteEncodeDV (enc.compressDV v)]
 
-end Cryptlib.Bench.MLKEMSteps
+end CryptlibBench.MLKEMSteps
diff --git a/bench/CryptlibBench/Main.lean b/bench/CryptlibBench/Main.lean
new file mode 100644
index 00000000..6f4e1a82
--- /dev/null
+++ b/bench/CryptlibBench/Main.lean
@@ -0,0 +1,26 @@
+/-
+SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
+SPDX-License-Identifier: AGPL-3.0-only
+-/
+
+import CryptlibBench.NIKE
+import CryptlibBench.KEM
+import CryptlibBench.Sphinx
+import CryptlibBench.MLKEMSteps
+import CryptlibBench.Field25519
+import CryptlibBench.Cipher
+import CryptlibBench.KDF
+
+/-! # Benchmark driver for all registered schemes and suites -/
+
+def main (args : List String) : IO UInt32 := do
+  for e in Cryptlib.Primitives.NIKE.registry do
+    (← CryptlibBench.NIKE.benches e.hpqcName e.scheme).forM LeanBench.register
+  for e in Cryptlib.Primitives.KEM.registry do
+    (← CryptlibBench.KEM.benches e.name e.scheme).forM LeanBench.register
+  (← CryptlibBench.Sphinx.benches).forM LeanBench.register
+  (← CryptlibBench.MLKEMSteps.benches).forM LeanBench.register
+  (← CryptlibBench.Field25519.benches).forM LeanBench.register
+  (← CryptlibBench.Cipher.benches).forM LeanBench.register
+  (← CryptlibBench.KDF.benches).forM LeanBench.register
+  LeanBench.runMain args
diff --git a/Cryptlib/Bench/NIKE.lean b/bench/CryptlibBench/NIKE.lean
similarity index 96%
rename from Cryptlib/Bench/NIKE.lean
rename to bench/CryptlibBench/NIKE.lean
index 73a54dfe..356e736f 100644
--- a/Cryptlib/Bench/NIKE.lean
+++ b/bench/CryptlibBench/NIKE.lean
@@ -10,7 +10,7 @@ import LeanBench
 
 A fresh private key is drawn before each sample, outside the timed region. -/
 
-namespace Cryptlib.Bench.NIKE
+namespace CryptlibBench.NIKE
 
 open Cryptlib.Primitives.NIKE.NIKE (NIKE)
 open Cryptlib.Util.Bytes (ofVector)
@@ -35,4 +35,4 @@ def benches (name : String) (nike : NIKE) : IO (Array LeanBench.Bench) := do
         let ss := nike.groupAction (← sk.get) ⟨nike.derivePublicKey p, nike.derive_safe p⟩
         out.set (ofVector (nike.encodeSharedSecret ss)) }]
 
-end Cryptlib.Bench.NIKE
+end CryptlibBench.NIKE
diff --git a/Cryptlib/Bench/Sphinx.lean b/bench/CryptlibBench/Sphinx.lean
similarity index 93%
rename from Cryptlib/Bench/Sphinx.lean
rename to bench/CryptlibBench/Sphinx.lean
index 91beeaeb..e15c8899 100644
--- a/Cryptlib/Bench/Sphinx.lean
+++ b/bench/CryptlibBench/Sphinx.lean
@@ -3,26 +3,26 @@ SPDX-FileCopyrightText: Copyright (C) 2026 David Stainton
 SPDX-License-Identifier: AGPL-3.0-only
 -/
 
-import Cryptlib.Protocols.Sphinx.bench_registry
-import Cryptlib.Protocols.Sphinx.types
-import Cryptlib.Protocols.Sphinx.nike_sphinx_theorems
-import Cryptlib.Protocols.Sphinx.kem_sphinx_theorems
+import CryptlibBench.SphinxCases
+import Cryptlib.Protocols.Sphinx.Types
+import Cryptlib.Protocols.Sphinx.NIKESphinxTheorems
+import Cryptlib.Protocols.Sphinx.KEMSphinxTheorems
 import Cryptlib.Util.Bytes
 import LeanBench
 
 /-! # Sphinx packet creation and unwrap benchmarks
 
-For each case in `BenchRegistry.sphinxBenchCases`, times packet creation and a single hop's unwrap.
+For each case in `SphinxCases.sphinxBenchCases`, times packet creation and a single hop's unwrap.
 Node and path generation run outside the timed region. -/
 
-namespace Cryptlib.Bench.Sphinx
+namespace CryptlibBench.Sphinx
 
 open Cryptlib.Protocols.Sphinx.Geometry (Geometry ofNIKE ofKEM)
 open Cryptlib.Protocols.Sphinx.Types
 open Cryptlib.Protocols.Sphinx.Commands
 open Cryptlib.Protocols.Sphinx.NIKESphinx (newNIKEPacket unwrapNIKE)
 open Cryptlib.Protocols.Sphinx.KEMSphinx (newKEMPacket unwrapKEM)
-open Cryptlib.Protocols.Sphinx.BenchRegistry
+open CryptlibBench.SphinxCases
 open Cryptlib.Primitives.NIKE.NIKE (NIKE)
 open Cryptlib.Primitives.KEM.KEM (KEM)
 open Cryptlib.Util.Bytes (ofVector toVecN)
@@ -130,4 +130,4 @@ def benches : IO (Array LeanBench.Bench) :=
     | .nike n nike => nikeBenches nike (← IO.ofExcept (ofNIKE n c.payloadSize false c.nrHops)) c.name
     | .kem n kem => kemBenches kem (← IO.ofExcept (ofKEM n c.payloadSize false c.nrHops)) c.name
 
-end Cryptlib.Bench.Sphinx
+end CryptlibBench.Sphinx
diff --git a/Cryptlib/Protocols/Sphinx/bench_registry.lean b/bench/CryptlibBench/SphinxCases.lean
similarity index 93%
rename from Cryptlib/Protocols/Sphinx/bench_registry.lean
rename to bench/CryptlibBench/SphinxCases.lean
index f989d4f3..e84dd85f 100644
--- a/Cryptlib/Protocols/Sphinx/bench_registry.lean
+++ b/bench/CryptlibBench/SphinxCases.lean
@@ -6,7 +6,7 @@ SPDX-License-Identifier: AGPL-3.0-only
 import Cryptlib.Primitives.NIKE.Schemes
 import Cryptlib.Primitives.KEM.Schemes
 
-namespace Cryptlib.Protocols.Sphinx.BenchRegistry
+namespace CryptlibBench.SphinxCases
 
 open Cryptlib.Primitives.NIKE.NIKE (NIKE)
 open Cryptlib.Primitives.KEM.KEM (KEM)
@@ -42,4 +42,4 @@ def sphinxBenchCases : List BenchCase :=
     payloadSizes.map fun sz => { kind := .kem e.name e.scheme, payloadSize := sz }
   nikeCases ++ kemCases
 
-end Cryptlib.Protocols.Sphinx.BenchRegistry
+end CryptlibBench.SphinxCases
diff --git a/bench/lake-manifest.json b/bench/lake-manifest.json
new file mode 100644
index 00000000..95bb94f5
--- /dev/null
+++ b/bench/lake-manifest.json
@@ -0,0 +1,163 @@
+{"version": "1.2.0",
+ "packagesDir": "../.lake/packages",
+ "packages":
+ [{"type": "path",
+   "scope": "",
+   "name": "cryptlib",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/alok/LeanBench",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "250d2a892bf8c91ec3ae5de8517793e18379f97b",
+   "name": "LeanBench",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "250d2a892bf8c91ec3ae5de8517793e18379f97b",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/katzenpost/cborg.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6aa918341adc7ae21b31dd6d3a75d856a2c61842",
+   "name": "cborg",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "6aa918341adc7ae21b31dd6d3a75d856a2c61842",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/dtumad/VCV-io.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "6d5c7d502ad97f676293a84c3d364c518cbde117",
+   "name": "VCVio",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "6d5c7d502ad97f676293a84c3d364c518cbde117",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/Verified-zkEVM/PolyFun.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c0c923693fc827a41d17116579a0c16ed4873b19",
+   "name": "PolyFun",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "c0c923693fc827a41d17116579a0c16ed4873b19",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/quangvdao/loom2",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2f65f311fae959c302586b07aa45390999b935d4",
+   "name": "loom2",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "2f65f311fae959c302586b07aa45390999b935d4",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/cslib",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "98e395a701f2027a413ad24729e1a11a6c772eb4",
+   "name": "cslib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.33.1",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«cryptlib-bench»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/bench/lakefile.toml b/bench/lakefile.toml
new file mode 100644
index 00000000..39bcea01
--- /dev/null
+++ b/bench/lakefile.toml
@@ -0,0 +1,28 @@
+name = "cryptlib-bench"
+reservoir = false
+version = "0.1.0"
+packagesDir = "../.lake/packages"
+defaultTargets = ["cryptlib-bench"]
+
+[leanOptions]
+pp.unicode.fun = true
+autoImplicit = false
+relaxedAutoImplicit = false
+
+[[require]]
+name = "LeanBench"
+git = "https://github.com/alok/LeanBench"
+rev = "250d2a892bf8c91ec3ae5de8517793e18379f97b"
+
+# Declared last so that cryptlib's pins, Mathlib's included, take precedence over LeanBench's.
+[[require]]
+name = "cryptlib"
+path = "../"
+
+[[lean_lib]]
+name = "CryptlibBench"
+globs = ["CryptlibBench.+"]
+
+[[lean_exe]]
+name = "cryptlib-bench"
+root = "CryptlibBench.Main"
diff --git a/bench/lean-toolchain b/bench/lean-toolchain
new file mode 100644
index 00000000..a8afa7d1
--- /dev/null
+++ b/bench/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.33.1
diff --git a/lake-manifest.json b/lake-manifest.json
index e4645743..20d17186 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -18,7 +18,7 @@
    "rev": "6aa918341adc7ae21b31dd6d3a75d856a2c61842",
    "name": "cborg",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "6aa918341adc7ae21b31dd6d3a75d856a2c61842",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/dtumad/VCV-io.git",
@@ -28,19 +28,9 @@
    "rev": "6d5c7d502ad97f676293a84c3d364c518cbde117",
    "name": "VCVio",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "6d5c7d502ad97f676293a84c3d364c518cbde117",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/alok/LeanBench",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "250d2a892bf8c91ec3ae5de8517793e18379f97b",
-   "name": "LeanBench",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
diff --git a/lakefile.toml b/lakefile.toml
index da4386d2..057f7059 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,4 +1,9 @@
 name = "cryptlib"
+version = "0.1.0"
+description = "Lean cryptography library for prototyping/modeling protocols and proving protocol properties."
+keywords = ["cryptography", "post-quantum", "verification", "sphinx", "mixnet"]
+homepage = "https://cryptlib.io"
+license = "AGPL-3.0-only"
 defaultTargets = ["Cryptlib"]
 
 [leanOptions]
@@ -6,20 +11,15 @@ pp.unicode.fun = true
 autoImplicit = false
 relaxedAutoImplicit = false
 
-[[require]]
-name = "LeanBench"
-git = "https://github.com/alok/LeanBench"
-rev = "main"
-
 [[require]]
 name = "VCVio"
 git = "https://github.com/dtumad/VCV-io.git"
-rev = "main"
+rev = "6d5c7d502ad97f676293a84c3d364c518cbde117"
 
 [[require]]
 name = "cborg"
 git = "https://github.com/katzenpost/cborg.git"
-rev = "main"
+rev = "6aa918341adc7ae21b31dd6d3a75d856a2c61842"
 
 # Declared last: VCVio pins mathlib v4.33.1, so this direct requirement (matching that pin)
 # must come after VCVio's for Lake's reverse-declaration-order precedence to keep it authoritative.
@@ -43,8 +43,6 @@ name = "Cryptlib.Primitives.NIKE.field25519_test"
 [[lean_exe]]
 name = "Cryptlib.Primitives.KEM.test"
 
-[[lean_exe]]
-name = "Cryptlib.Bench.benchmark"
 [[lean_exe]]
 name = "Cryptlib.Primitives.KEM.vectors"