From 021cbc62b1abc3a9c80d44ad9266aef39e8ff640 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 24 Feb 2026 16:28:47 -0500
Subject: [PATCH 1/2] chore: Switch to module system

---
 Blake3.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/Blake3.lean b/Blake3.lean
index 5997baa..8af5156 100644
--- a/Blake3.lean
+++ b/Blake3.lean
@@ -1,3 +1,4 @@
+module
 /-! Bindings to the BLAKE3 hashing library. -/
 
 theorem ByteArray.size_of_extract {hash : ByteArray} (h : e ≤ hash.size) :
@@ -5,15 +6,18 @@ theorem ByteArray.size_of_extract {hash : ByteArray} (h : e ≤ hash.size) :
   simp [Nat.min_eq_left h]
 
 namespace Blake3
+public section
 
 /-- BLAKE3 constants -/
 abbrev BLAKE3_OUT_LEN : Nat := 32
 abbrev BLAKE3_KEY_LEN : Nat := 32
 
 /-- A wrapper around `ByteArray` whose size is `BLAKE3_OUT_LEN` -/
+@[expose]
 def Blake3Hash : Type := { r : ByteArray // r.size = BLAKE3_OUT_LEN }
 
 /-- A wrapper around `ByteArray` whose size is `BLAKE3_KEY_LEN` -/
+@[expose]
 def Blake3Key : Type := { r : ByteArray // r.size = BLAKE3_KEY_LEN }
 
 def Blake3Key.ofBytes (bytes : ByteArray)
@@ -81,6 +85,7 @@ def finalizeWithLength (hasher : Hasher) (length : Nat)
 end Hasher
 
 /-- Hash a ByteArray -/
+@[expose]
 def hash (input : ByteArray) : Blake3Hash :=
   let hasher := Hasher.init ()
   let hasher := hasher.update input
@@ -107,7 +112,8 @@ namespace Sponge
 abbrev ABSORB_MAX_BYTES := UInt32.size - 1
 abbrev DEFAULT_REKEYING_STAGE := UInt16.size - 1
 
-def init (label : String) (_h : ¬label.isEmpty := by decide) : Sponge :=
+@[expose]
+def init (label : String) (_h : ¬label.isEmpty := by native_decide) : Sponge :=
   ⟨Hasher.initDeriveKey label.toUTF8, 0⟩
 
 def ratchet (sponge : Sponge) : Sponge :=
@@ -149,4 +155,5 @@ def squeeze (sponge : Sponge) (length : USize)
 
 end Sponge
 
+end
 end Blake3

From a3235767d7b0b0c3b3d1e7dfc340c0ebdb2b5bdc Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 25 Feb 2026 11:53:17 -0500
Subject: [PATCH 2/2] Remove unnecessary `@[expose]`

---
 Blake3.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Blake3.lean b/Blake3.lean
index 8af5156..35df190 100644
--- a/Blake3.lean
+++ b/Blake3.lean
@@ -85,7 +85,6 @@ def finalizeWithLength (hasher : Hasher) (length : Nat)
 end Hasher
 
 /-- Hash a ByteArray -/
-@[expose]
 def hash (input : ByteArray) : Blake3Hash :=
   let hasher := Hasher.init ()
   let hasher := hasher.update input
@@ -112,7 +111,6 @@ namespace Sponge
 abbrev ABSORB_MAX_BYTES := UInt32.size - 1
 abbrev DEFAULT_REKEYING_STAGE := UInt16.size - 1
 
-@[expose]
 def init (label : String) (_h : ¬label.isEmpty := by native_decide) : Sponge :=
   ⟨Hasher.initDeriveKey label.toUTF8, 0⟩