feat: Add Rust bindings target

.github/workflows/ci.yml

@@ -5,6 +5,7 @@ on:
   push:
     branches:
       - main
+  workflow_dispatch:
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
@@ -21,6 +22,36 @@ jobs:
           build-args: "--wfail"
           test: true
 
+  valgrind:
+    needs: lean-test
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      # Only restore the cache, since the `test` job will save the test binary to the cache first
+      - uses: actions/cache/restore@v5
+        with:
+          path: ./test/.lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('test/lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('test/lake-manifest.json') }}
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: true
+          build-args: "Blake3Test"
+          use-github-cache: false
+      - name: Install valgrind
+        run: sudo apt-get update && sudo apt-get install -y valgrind
+      - name: Run tests under valgrind
+        run: |
+          valgrind \
+            --leak-check=full \
+            --show-leak-kinds=definite,possible \
+            --errors-for-leak-kinds=definite \
+            --track-origins=yes \
+            --error-exitcode=1 \
+            .lake/build/bin/Blake3Test
+
   nix-test:
     name: Nix Tests
     runs-on: ubuntu-latest

.gitignore

@@ -1,4 +1,12 @@
+# Lean
 /.lake
+# Local clone for Lake build
 /blake3
+
+# Rust
+**/target
+
+# Nix
 result*
 .direnv/
+

Blake3.lean

@@ -1,5 +1,5 @@
 module
-/-! Bindings to the BLAKE3 hashing library. -/
+/-! Shared types and generic logic for BLAKE3 bindings. -/
 
 theorem ByteArray.size_of_extract {hash : ByteArray} (h : e ≤ hash.size) :
     (hash.extract b e).size = e - b := by
@@ -32,103 +32,84 @@ instance : Inhabited Blake3Hash where
     0, 0, 0, 0, 0, 0, 0, 0
   ]⟩, by rw [ByteArray.size]; rfl⟩
 
-private opaque HasherNonempty : NonemptyType
-
-def Hasher : Type := HasherNonempty.type
-
-instance : Nonempty Hasher := HasherNonempty.property
-
-@[extern "lean_blake3_version"]
-protected opaque internalVersion : Unit → String
-
-/-- Version of the linked BLAKE3 implementation library. -/
-def version : String := Blake3.internalVersion ()
-
-namespace Hasher
-
-/-- Initialize a hasher. -/
-@[extern "lean_blake3_init"]
-opaque init : Unit → Hasher
-
-/-- Initialize a hasher using pseudo-random key -/
-@[extern "lean_blake3_init_keyed"]
-opaque initKeyed (key : @& Blake3Key) : Hasher
-
-@[extern "lean_blake3_init_derive_key"]
-opaque initDeriveKey (context : @& ByteArray) : Hasher
-
-/-- Put more data into the hasher. This can be called several times. -/
-@[extern "lean_blake3_hasher_update"]
-opaque update (hasher : Hasher) (input : @& ByteArray) : Hasher
+/-- Typeclass for BLAKE3 hasher backends (C, Rust, etc.). -/
+class HasherOps (H : Type) where
+  init : Unit → H
+  initKeyed : Blake3Key → H
+  initDeriveKey : ByteArray → H
+  update : H → ByteArray → H
+  finalize : H → (length : USize) → { r : ByteArray // r.size = length.toNat }
 
 instance {length : USize} : Inhabited { r : ByteArray // r.size = length.toNat } where
   default := ⟨
     ⟨⟨List.replicate length.toNat 0⟩⟩,
     by simp only [ByteArray.size, List.toArray_replicate, Array.size_replicate]
   ⟩
 
-/-- Finalize the hasher and write the output to an array of a given length. -/
-@[extern "lean_blake3_hasher_finalize"]
-opaque finalize : (hasher : Hasher) → (length : USize) →
-  {r : ByteArray // r.size = length.toNat}
+namespace HasherOps
+
+variable {H : Type} [HasherOps H]
 
-def finalizeWithLength (hasher : Hasher) (length : Nat)
+def finalizeWithLength (hasher : H) (length : Nat)
     (h : length < 2 ^ System.Platform.numBits := by native_decide) :
     { r : ByteArray // r.size = length } :=
-  let ⟨hash, h'⟩ := hasher.finalize length.toUSize
+  let ⟨hash, h'⟩ := HasherOps.finalize hasher length.toUSize
   have hash_size_eq_len : hash.size = length := by
     cases System.Platform.numBits_eq with
     | inl h32 => rw [h32] at h; simp [h', h32]; exact h
     | inr h64 => rw [h64] at h; simp [h', h64]; exact h
   ⟨hash, hash_size_eq_len⟩
 
-end Hasher
-
 /-- Hash a ByteArray -/
 def hash (input : ByteArray) : Blake3Hash :=
-  let hasher := Hasher.init ()
-  let hasher := hasher.update input
-  hasher.finalizeWithLength BLAKE3_OUT_LEN
+  let hasher := HasherOps.init (H := H) ()
+  let hasher := HasherOps.update hasher input
+  finalizeWithLength hasher BLAKE3_OUT_LEN
 
 /-- Hash a ByteArray using keyed initializer -/
-def hashKeyed (input : @& ByteArray) (key : @& Blake3Key) : Blake3Hash :=
-  let hasher := Hasher.initKeyed key
-  let hasher := hasher.update input
-  hasher.finalizeWithLength BLAKE3_OUT_LEN
+def hashKeyed (input : ByteArray) (key : Blake3Key) : Blake3Hash :=
+  let hasher := HasherOps.initKeyed (H := H) key
+  let hasher := HasherOps.update hasher input
+  finalizeWithLength hasher BLAKE3_OUT_LEN
 
 /-- Hash a ByteArray using initializer parameterized by some context -/
-def hashDeriveKey (input context : @& ByteArray) : Blake3Hash :=
-  let hasher := Hasher.initDeriveKey context
-  let hasher := hasher.update input
-  hasher.finalizeWithLength BLAKE3_OUT_LEN
+def hashDeriveKey (input context : ByteArray) : Blake3Hash :=
+  let hasher := HasherOps.initDeriveKey (H := H) context
+  let hasher := HasherOps.update hasher input
+  finalizeWithLength hasher BLAKE3_OUT_LEN
+
+end HasherOps
 
-structure Sponge where
-  hasher : Hasher
+/-- Generic sponge construction over any BLAKE3 hasher backend. -/
+structure Sponge (H : Type) where
+  hasher : H
   counter : Nat
 
 namespace Sponge
 
 abbrev ABSORB_MAX_BYTES := UInt32.size - 1
 abbrev DEFAULT_REKEYING_STAGE := UInt16.size - 1
 
-def init (label : String) (_h : ¬label.isEmpty := by native_decide) : Sponge :=
-  ⟨Hasher.initDeriveKey label.toUTF8, 0⟩
+variable {H : Type} [HasherOps H]
+
+def init (label : String) (_h : ¬label.isEmpty := by native_decide) : Sponge H :=
+  ⟨HasherOps.initDeriveKey label.toUTF8, 0⟩
 
-def ratchet (sponge : Sponge) : Sponge :=
-  let key := sponge.hasher.finalizeWithLength BLAKE3_KEY_LEN
-  { sponge with hasher := Hasher.initKeyed key, counter := 0 }
+def ratchet (sponge : Sponge H) : Sponge H :=
+  let key := HasherOps.finalizeWithLength sponge.hasher BLAKE3_KEY_LEN
+  { sponge with hasher := HasherOps.initKeyed key, counter := 0 }
 
-def absorb (sponge : Sponge) (bytes : ByteArray)
-    (_h : bytes.size < ABSORB_MAX_BYTES := by norm_cast) : Sponge :=
+def absorb (sponge : Sponge H) (bytes : ByteArray)
+    (_h : bytes.size < ABSORB_MAX_BYTES := by norm_cast) : Sponge H :=
   let highCounter := sponge.counter >= DEFAULT_REKEYING_STAGE
   let sponge := if highCounter then sponge.ratchet else sponge
-  ⟨sponge.hasher.update bytes, sponge.counter + 1⟩
+  ⟨HasherOps.update sponge.hasher bytes, sponge.counter + 1⟩
 
-def squeeze (sponge : Sponge) (length : USize)
+def squeeze (sponge : Sponge H) (length : USize)
     (h_len_bound : 2 * BLAKE3_OUT_LEN + length.toNat < 2 ^ System.Platform.numBits :=
       by native_decide) :
     { r : ByteArray // r.size = length.toNat } :=
-  let ⟨tmp, h⟩ := sponge.hasher.finalize (2 * BLAKE3_OUT_LEN.toUSize + length)
+  let ⟨tmp, h⟩ := HasherOps.finalize sponge.hasher (2 * BLAKE3_OUT_LEN.toUSize + length)
   let b := (2 * BLAKE3_OUT_LEN)
   let e := (2 * BLAKE3_OUT_LEN + length.toNat)
   let y := tmp.extract b e

Blake3/C.lean

@@ -0,0 +1,62 @@
+module
+public import Blake3
+/-! C-backed BLAKE3 bindings. -/
+
+namespace Blake3.C
+open Blake3
+public section
+
+private opaque HasherNonempty : NonemptyType
+
+def Hasher : Type := HasherNonempty.type
+
+instance : Nonempty Hasher := HasherNonempty.property
+
+@[extern "c_blake3_version"]
+protected opaque internalVersion : Unit → String
+
+/-- Version of the linked C BLAKE3 implementation library. -/
+def version : String := Blake3.C.internalVersion ()
+
+@[extern "c_blake3_init"]
+opaque hasherInit : Unit → Hasher
+
+@[extern "c_blake3_init_keyed"]
+opaque hasherInitKeyed : @& Blake3Key → Hasher
+
+@[extern "c_blake3_init_derive_key"]
+opaque hasherInitDeriveKey : @& ByteArray → Hasher
+
+@[extern "c_blake3_hasher_update"]
+opaque hasherUpdate : Hasher → @& ByteArray → Hasher
+
+@[extern "c_blake3_hasher_finalize"]
+opaque hasherFinalize : Hasher → (length : USize) →
+  { r : ByteArray // r.size = length.toNat }
+
+instance : HasherOps Hasher where
+  init := hasherInit
+  initKeyed := hasherInitKeyed
+  initDeriveKey := hasherInitDeriveKey
+  update := hasherUpdate
+  finalize := hasherFinalize
+
+abbrev hash := HasherOps.hash (H := Hasher)
+abbrev hashKeyed := HasherOps.hashKeyed (H := Hasher)
+abbrev hashDeriveKey := HasherOps.hashDeriveKey (H := Hasher)
+abbrev Sponge := Blake3.Sponge Hasher
+
+-- Dot-notation aliases: `Hasher.init`, `h.update`, `h.finalizeWithLength`
+namespace Hasher
+
+abbrev init := hasherInit
+abbrev update := hasherUpdate
+
+def finalizeWithLength (hasher : Hasher) (length : Nat)
+    (h : length < 2 ^ System.Platform.numBits := by native_decide) :=
+  HasherOps.finalizeWithLength hasher length h
+
+end Hasher
+
+end
+end Blake3.C

Blake3/Rust.lean

@@ -0,0 +1,62 @@
+module
+public import Blake3
+/-! Rust-backed BLAKE3 bindings. -/
+
+namespace Blake3.Rust
+open Blake3
+public section
+
+private opaque HasherNonempty : NonemptyType
+
+def Hasher : Type := HasherNonempty.type
+
+instance : Nonempty Hasher := HasherNonempty.property
+
+@[extern "rs_blake3_version"]
+protected opaque internalVersion : Unit → String
+
+/-- Version of the linked Rust BLAKE3 implementation library. -/
+def version : String := Blake3.Rust.internalVersion ()
+
+@[extern "rs_blake3_init"]
+opaque hasherInit : Unit → Hasher
+
+@[extern "rs_blake3_init_keyed"]
+opaque hasherInitKeyed : @& Blake3Key → Hasher
+
+@[extern "rs_blake3_init_derive_key"]
+opaque hasherInitDeriveKey : @& ByteArray → Hasher
+
+@[extern "rs_blake3_hasher_update"]
+opaque hasherUpdate : Hasher → @& ByteArray → Hasher
+
+@[extern "rs_blake3_hasher_finalize"]
+opaque hasherFinalize : Hasher → (length : USize) →
+  { r : ByteArray // r.size = length.toNat }
+
+instance : HasherOps Hasher where
+  init := hasherInit
+  initKeyed := hasherInitKeyed
+  initDeriveKey := hasherInitDeriveKey
+  update := hasherUpdate
+  finalize := hasherFinalize
+
+abbrev hash := HasherOps.hash (H := Hasher)
+abbrev hashKeyed := HasherOps.hashKeyed (H := Hasher)
+abbrev hashDeriveKey := HasherOps.hashDeriveKey (H := Hasher)
+abbrev Sponge := Blake3.Sponge Hasher
+
+-- Dot-notation aliases: `Hasher.init`, `h.update`, `h.finalizeWithLength`
+namespace Hasher
+
+abbrev init := hasherInit
+abbrev update := hasherUpdate
+
+def finalizeWithLength (hasher : Hasher) (length : Nat)
+    (h : length < 2 ^ System.Platform.numBits := by native_decide) :=
+  HasherOps.finalizeWithLength hasher length h
+
+end Hasher
+
+end
+end Blake3.Rust