From f1ba2a08b68824fc3ec21d08249a8a19fc82b7d5 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 11 Mar 2026 17:54:40 -0400 Subject: [PATCH 1/5] feat: Add Rust bindings target --- .gitignore | 8 ++ Blake3.lean | 103 ++++++-------- Blake3/C.lean | 49 +++++++ Blake3/Rust.lean | 49 +++++++ Blake3Test.lean | 74 ++++++---- ffi.c | 12 +- flake.lock | 56 ++++++++ flake.nix | 19 +++ lakefile.lean | 32 ++++- rust-toolchain.toml | 4 + rust/Cargo.lock | 330 ++++++++++++++++++++++++++++++++++++++++++++ rust/Cargo.toml | 17 +++ rust/src/lib.rs | 70 ++++++++++ 13 files changed, 723 insertions(+), 100 deletions(-) create mode 100644 Blake3/C.lean create mode 100644 Blake3/Rust.lean create mode 100644 rust-toolchain.toml create mode 100644 rust/Cargo.lock create mode 100644 rust/Cargo.toml create mode 100644 rust/src/lib.rs diff --git a/.gitignore b/.gitignore index ecb70fd..c908d25 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,12 @@ +# Lean /.lake +# Local clone for Lake build /blake3 + +# Rust +**/target + +# Nix result* .direnv/ + diff --git a/Blake3.lean b/Blake3.lean index 35df190..35be242 100644 --- a/Blake3.lean +++ b/Blake3.lean @@ -1,7 +1,7 @@ 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) : +private theorem ByteArray.size_of_extract {hash : ByteArray} (h : e ≤ hash.size) : (hash.extract b e).size = e - b := by simp [Nat.min_eq_left h] @@ -32,34 +32,13 @@ 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 := ⟨ @@ -67,43 +46,43 @@ instance {length : USize} : Inhabited { r : ByteArray // r.size = length.toNat } 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 @@ -111,24 +90,26 @@ 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 diff --git a/Blake3/C.lean b/Blake3/C.lean new file mode 100644 index 0000000..a1c76fd --- /dev/null +++ b/Blake3/C.lean @@ -0,0 +1,49 @@ +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"] +private opaque hasherInit : Unit → Hasher + +@[extern "c_blake3_init_keyed"] +private opaque hasherInitKeyed : @& Blake3Key → Hasher + +@[extern "c_blake3_init_derive_key"] +private opaque hasherInitDeriveKey : @& ByteArray → Hasher + +@[extern "c_blake3_hasher_update"] +private opaque hasherUpdate : Hasher → @& ByteArray → Hasher + +@[extern "c_blake3_hasher_finalize"] +private 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 + +end +end Blake3.C diff --git a/Blake3/Rust.lean b/Blake3/Rust.lean new file mode 100644 index 0000000..88880f3 --- /dev/null +++ b/Blake3/Rust.lean @@ -0,0 +1,49 @@ +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"] +private opaque hasherInit : Unit → Hasher + +@[extern "rs_blake3_init_keyed"] +private opaque hasherInitKeyed : @& Blake3Key → Hasher + +@[extern "rs_blake3_init_derive_key"] +private opaque hasherInitDeriveKey : @& ByteArray → Hasher + +@[extern "rs_blake3_hasher_update"] +private opaque hasherUpdate : Hasher → @& ByteArray → Hasher + +@[extern "rs_blake3_hasher_finalize"] +private 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 + +end +end Blake3.Rust diff --git a/Blake3Test.lean b/Blake3Test.lean index 7c5a7c8..262c4b1 100644 --- a/Blake3Test.lean +++ b/Blake3Test.lean @@ -1,6 +1,29 @@ -import Blake3 +import Blake3.C +import Blake3.Rust + +open Blake3 + +class Blake3Backend (H : Type) [HasherOps H] where + name : String + version : String + +instance : Blake3Backend Blake3.C.Hasher where + name := "C" + version := Blake3.C.version + +instance : Blake3Backend Blake3.Rust.Hasher where + name := "Rust" + version := Blake3.Rust.version abbrev input : ByteArray := ⟨#[0]⟩ + +abbrev key : Blake3Key := .ofBytes ⟨#[ + 3, 123, 16, 175, 8, 196, 101, 134, + 144, 184, 221, 34, 25, 106, 122, 200, + 213, 14, 159, 189, 82, 166, 91, 107, + 33, 78, 26, 226, 89, 65, 188, 92 +]⟩ + abbrev expectedOutputRegularHashing : ByteArray := ⟨#[ 45, 58, 222, 223, 241, 27, 97, 241, 76, 136, 110, 53, 175, 160, 54, 115, @@ -8,13 +31,6 @@ abbrev expectedOutputRegularHashing : ByteArray := ⟨#[ 81, 2, 37, 208, 245, 146, 226, 19 ]⟩ --- Good pseudo-random key -abbrev key : Blake3.Blake3Key := .ofBytes ⟨#[ - 3, 123, 16, 175, 8, 196, 101, 134, - 144, 184, 221, 34, 25, 106, 122, 200, - 213, 14, 159, 189, 82, 166, 91, 107, - 33, 78, 26, 226, 89, 65, 188, 92 -]⟩ abbrev expectedOutputKeyedHashing: ByteArray := ⟨#[ 145, 187, 220, 234, 206, 139, 205, 138, 220, 103, 35, 65, 199, 96, 210, 18, @@ -22,8 +38,8 @@ abbrev expectedOutputKeyedHashing: ByteArray := ⟨#[ 2, 29, 12, 32, 17, 118, 181, 232 ]⟩ --- Context (with "bad" randomness) abbrev context : ByteArray := ⟨#[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]⟩ + abbrev expectedOutputDeriveKeyHashing: ByteArray := ⟨#[ 34, 57, 22, 43, 164, 211, 65, 131, 90, 55, 55, 92, 68, 90, 63, 136, @@ -39,22 +55,24 @@ abbrev expectedOutputSponge : ByteArray := ⟨#[ 154, 99, 175, 9, 196, 102, 126, 72, 27, 86 ]⟩ -def hashingFails := - (Blake3.hash input).val.data != expectedOutputRegularHashing.data || - (Blake3.hashKeyed input key).val.data != expectedOutputKeyedHashing.data || - (Blake3.hashDeriveKey input context).val.data != expectedOutputDeriveKeyHashing.data - -def spongeFails := - let sponge := Blake3.Sponge.init "ix 2025-01-01 16:18:03 content-addressing v1" - let sponge := sponge.absorb ⟨#[1]⟩ - let sponge := sponge.absorb ⟨#[2]⟩ - let sponge := sponge.absorb ⟨#[3]⟩ - let sponge := sponge.absorb ⟨#[4, 5]⟩ - let output := sponge.squeeze 50 - output.val.data != expectedOutputSponge.data - -def main : IO UInt32 := do - println! s!"BLAKE3 version: {Blake3.version}" - if hashingFails || spongeFails - then IO.eprintln "BLAKE3 test failed"; return 1 - else IO.println "BLAKE3 test succeeded"; return 0 +def runTests (H : Type) [HasherOps H] [b : Blake3Backend H] : IO Bool := do + println! s!"BLAKE3 version ({b.name}): {b.version}" + let hashFails := + (HasherOps.hash (H := H) input).val.data != expectedOutputRegularHashing.data || + (HasherOps.hashKeyed (H := H) input key).val.data != expectedOutputKeyedHashing.data || + (HasherOps.hashDeriveKey (H := H) input context).val.data != expectedOutputDeriveKeyHashing.data + let spongeFails := + let s : Sponge H := Sponge.init "ix 2025-01-01 16:18:03 content-addressing v1" + let s := s.absorb ⟨#[1]⟩ |>.absorb ⟨#[2]⟩ |>.absorb ⟨#[3]⟩ |>.absorb ⟨#[4, 5]⟩ + (s.squeeze 50).val.data != expectedOutputSponge.data + if hashFails || spongeFails + then IO.eprintln s!"BLAKE3 {b.name} test failed"; return false + else IO.println s!"BLAKE3 {b.name} test succeeded"; return true + +def main (args : List String) : IO UInt32 := do + let runC := args.isEmpty || args.contains "c" + let runRust := args.isEmpty || args.contains "rust" + let mut ok := true + if runC then ok := (← runTests Blake3.C.Hasher) && ok + if runRust then ok := (← runTests Blake3.Rust.Hasher) && ok + return if ok then 0 else 1 diff --git a/ffi.c b/ffi.c index e8343ce..c75957e 100644 --- a/ffi.c +++ b/ffi.c @@ -4,7 +4,7 @@ /** * Wrap around the blake3_version function and construct a lean string. */ -extern lean_obj_res lean_blake3_version() { +extern lean_obj_res c_blake3_version() { const char *v = blake3_version(); return lean_mk_string(v); } @@ -46,7 +46,7 @@ static inline lean_obj_res blake3_hasher_copy(lean_object *self) { /** * Initialize a hasher. */ -extern lean_obj_res lean_blake3_init() { +extern lean_obj_res c_blake3_init() { blake3_hasher *a = malloc(sizeof(blake3_hasher)); blake3_hasher_init(a); return lean_alloc_external(get_blake3_hasher_class(), a); @@ -55,7 +55,7 @@ extern lean_obj_res lean_blake3_init() { /** * Initialize a hasher using pseudo-random key */ -extern lean_obj_res lean_blake3_init_keyed(b_lean_obj_arg key) { +extern lean_obj_res c_blake3_init_keyed(b_lean_obj_arg key) { blake3_hasher *a = malloc(sizeof(blake3_hasher)); blake3_hasher_init_keyed(a, lean_sarray_cptr(key)); return lean_alloc_external(get_blake3_hasher_class(), a); @@ -64,7 +64,7 @@ extern lean_obj_res lean_blake3_init_keyed(b_lean_obj_arg key) { /** * Initialize a hasher using some arbitrary context */ - extern lean_obj_res lean_blake3_init_derive_key(b_lean_obj_arg context) { + extern lean_obj_res c_blake3_init_derive_key(b_lean_obj_arg context) { blake3_hasher *a = malloc(sizeof(blake3_hasher)); blake3_hasher_init_derive_key_raw(a, lean_sarray_cptr(context), lean_sarray_size(context)); return lean_alloc_external(get_blake3_hasher_class(), a); @@ -80,7 +80,7 @@ static inline lean_obj_res lean_ensure_exclusive_blake3_hasher(lean_obj_arg a) { return blake3_hasher_copy(a); } -extern lean_obj_res lean_blake3_hasher_update(lean_obj_arg self, b_lean_obj_arg input) { +extern lean_obj_res c_blake3_hasher_update(lean_obj_arg self, b_lean_obj_arg input) { lean_object *a = lean_ensure_exclusive_blake3_hasher(self); blake3_hasher_update( lean_get_external_data(a), @@ -93,7 +93,7 @@ extern lean_obj_res lean_blake3_hasher_update(lean_obj_arg self, b_lean_obj_arg /** * Finalize the hasher and return the hash given the length. */ -extern lean_obj_res lean_blake3_hasher_finalize(lean_obj_arg self, size_t len) { +extern lean_obj_res c_blake3_hasher_finalize(lean_obj_arg self, size_t len) { lean_object *out = lean_alloc_sarray(1, len, len); lean_object *a = lean_ensure_exclusive_blake3_hasher(self); blake3_hasher_finalize(lean_get_external_data(a), lean_sarray_cptr(out), len); diff --git a/flake.lock b/flake.lock index c183b4d..04ee8bd 100644 --- a/flake.lock +++ b/flake.lock @@ -17,6 +17,43 @@ "type": "github" } }, + "crane": { + "locked": { + "lastModified": 1773189535, + "narHash": "sha256-E1G/Or6MWeP+L6mpQ0iTFLpzSzlpGrITfU2220Gq47g=", + "owner": "ipetkov", + "repo": "crane", + "rev": "6fa2fb4cf4a89ba49fc9dd5a3eb6cde99d388269", + "type": "github" + }, + "original": { + "owner": "ipetkov", + "repo": "crane", + "type": "github" + } + }, + "fenix": { + "inputs": { + "nixpkgs": [ + "lean4-nix", + "nixpkgs" + ], + "rust-analyzer-src": "rust-analyzer-src" + }, + "locked": { + "lastModified": 1773213034, + "narHash": "sha256-XX02kIGvcsVZKiRwr3COkBIZ5s+TP9gfRkW2Oad6hqE=", + "owner": "nix-community", + "repo": "fenix", + "rev": "42f953f569ac5761b197ca51c25cf1f9ceb78448", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "fenix", + "type": "github" + } + }, "flake-parts": { "inputs": { "nixpkgs-lib": "nixpkgs-lib" @@ -121,6 +158,8 @@ "root": { "inputs": { "blake3": "blake3", + "crane": "crane", + "fenix": "fenix", "flake-parts": "flake-parts", "lean4-nix": "lean4-nix", "nixpkgs": [ @@ -128,6 +167,23 @@ "nixpkgs" ] } + }, + "rust-analyzer-src": { + "flake": false, + "locked": { + "lastModified": 1773182115, + "narHash": "sha256-m3tXlrz8qG9IXPvhImtLyKUbsSXx46HFbzNFNlbwPno=", + "owner": "rust-lang", + "repo": "rust-analyzer", + "rev": "e0269ce3f2ff14bdf220e7bdf12e80f4431897a1", + "type": "github" + }, + "original": { + "owner": "rust-lang", + "ref": "nightly", + "repo": "rust-analyzer", + "type": "github" + } } }, "root": "root", diff --git a/flake.nix b/flake.nix index ea97628..bb03b17 100644 --- a/flake.nix +++ b/flake.nix @@ -9,6 +9,14 @@ url = "github:BLAKE3-team/BLAKE3?ref=refs/tags/1.8.3"; flake = false; }; + # Rust-related inputs + fenix = { + url = "github:nix-community/fenix"; + # Follow lean4-nix nixpkgs so we stay in sync + inputs.nixpkgs.follows = "lean4-nix/nixpkgs"; + }; + + crane.url = "github:ipetkov/crane"; }; outputs = inputs @ { @@ -16,6 +24,8 @@ flake-parts, lean4-nix, blake3, + fenix, + crane, ... }: flake-parts.lib.mkFlake {inherit inputs;} { @@ -31,6 +41,11 @@ pkgs, ... }: let + # Pins the Rust toolchain + rustToolchain = fenix.packages.${system}.fromToolchainFile { + file = ./rust-toolchain.toml; + sha256 = "sha256-sqSWJDUxc+zaz1nBWMAJKTAGBuGWP25GCftIOlCEAtA="; + }; lake2nix = pkgs.callPackage lean4-nix.lake {}; commonArgs = { src = ./.; @@ -66,8 +81,12 @@ test = blake3Test; }; devShells.default = pkgs.mkShell { + # Add libclang for FFI with rust-bindgen + LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; packages = with pkgs; [ + clang lean.lean-all + rustToolchain ]; }; diff --git a/lakefile.lean b/lakefile.lean index cfe0b95..299d683 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,6 +11,7 @@ lean_lib Blake3 where @[test_driver] lean_exe Blake3Test +-- BLAKE3 C source abbrev blake3RepoURL := "https://github.com/BLAKE3-team/BLAKE3" abbrev blake3RepoTag := "1.8.3" @@ -25,6 +26,7 @@ target cloneBlake3 pkg : GitRepo := do -- Checkout to a fixed tag GitRepo.execGit #["fetch", "--tags"] repoDir GitRepo.execGit #["checkout", blake3RepoTag] repoDir + return pure repoDir def blake3CDir (blake3Repo : GitRepo) : System.FilePath := @@ -47,24 +49,44 @@ def buildBlake3Obj (pkg : Package) (fileName : String) := do let oFile := pkg.buildDir / fileName |>.addExtension "o" let includeArgs := #["-fPIC", "-I", cDir.toString] let weakArgs := includeArgs ++ blake3Flags + buildO oFile srcJob weakArgs #[] compiler getLeanTrace -target ffi.o pkg : System.FilePath := do +-- C FFI +target ffi_c pkg : System.FilePath := do let blake3Repo ← cloneBlake3.fetch >>= (·.await) - let oFile := pkg.buildDir / "ffi.o" + let oFile := pkg.buildDir / "ffi_c.o" let srcJob ← inputTextFile $ pkg.dir / "ffi.c" let leanIncludeDir ← getLeanIncludeDir let cDir := blake3CDir blake3Repo let weakArgs := #["-fPIC", "-I", leanIncludeDir.toString, "-I", cDir.toString] + buildO oFile srcJob weakArgs #[] compiler getLeanTrace -extern_lib ffi pkg := do +target blake3_c pkg : System.FilePath := do -- Gather all `.o` file build jobs let blake3O ← buildBlake3Obj pkg "blake3" let blake3DispatchO ← buildBlake3Obj pkg "blake3_dispatch" let blake3PortableO ← buildBlake3Obj pkg "blake3_portable" - let ffiO ← ffi.o.fetch + let ffiO ← ffi_c.fetch let oFileJobs := #[blake3O, blake3DispatchO, blake3PortableO, ffiO] - let name := nameToStaticLib "ffi" + let name := nameToStaticLib "blake3_c" buildStaticLib (pkg.staticLibDir / name) oFileJobs + +lean_lib «Blake3.C» where + roots := #[`Blake3.C] + precompileModules := true + moreLinkObjs := #[blake3_c] + +-- Rust FFI +target blake3_rs pkg : System.FilePath := do + proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir / "rust" } (quiet := true) + let libName := nameToStaticLib "blake3_rs" + inputBinFile $ pkg.dir / "rust" / "target" / "release" / libName + +lean_lib «Blake3.Rust» where + roots := #[`Blake3.Rust] + precompileModules := true + moreLinkObjs := #[blake3_rs] + diff --git a/rust-toolchain.toml b/rust-toolchain.toml new file mode 100644 index 0000000..a5b578d --- /dev/null +++ b/rust-toolchain.toml @@ -0,0 +1,4 @@ +[toolchain] +# The default profile includes rustc, rust-std, cargo, rust-docs, rustfmt and clippy. +profile = "default" +channel = "1.92" diff --git a/rust/Cargo.lock b/rust/Cargo.lock new file mode 100644 index 0000000..bb6b389 --- /dev/null +++ b/rust/Cargo.lock @@ -0,0 +1,330 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "aho-corasick" +version = "1.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ddd31a130427c27518df266943a5308ed92d4b226cc639f5a8f1002816174301" +dependencies = [ + "memchr", +] + +[[package]] +name = "arrayref" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76a2e8124351fda1ef8aaaa3bbd7ebbcb486bbcd4225aca0aa0d84bb2db8fecb" + +[[package]] +name = "arrayvec" +version = "0.7.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50" + +[[package]] +name = "autocfg" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" + +[[package]] +name = "bindgen" +version = "0.72.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "993776b509cfb49c750f11b8f07a46fa23e0a1386ffc01fb1e7d343efc387895" +dependencies = [ + "bitflags", + "cexpr", + "clang-sys", + "itertools", + "log", + "prettyplease", + "proc-macro2", + "quote", + "regex", + "rustc-hash", + "shlex", + "syn", +] + +[[package]] +name = "bitflags" +version = "2.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "843867be96c8daad0d758b57df9392b6d8d271134fce549de6ce169ff98a92af" + +[[package]] +name = "blake3" +version = "1.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2468ef7d57b3fb7e16b576e8377cdbde2320c60e1491e961d11da40fc4f02a2d" +dependencies = [ + "arrayref", + "arrayvec", + "cc", + "cfg-if", + "constant_time_eq", + "cpufeatures", +] + +[[package]] +name = "blake3-rs" +version = "0.1.0" +dependencies = [ + "blake3", + "lean-ffi", +] + +[[package]] +name = "cc" +version = "1.2.56" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aebf35691d1bfb0ac386a69bac2fde4dd276fb618cf8bf4f5318fe285e821bb2" +dependencies = [ + "find-msvc-tools", + "shlex", +] + +[[package]] +name = "cexpr" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766" +dependencies = [ + "nom", +] + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + +[[package]] +name = "clang-sys" +version = "1.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b023947811758c97c59bf9d1c188fd619ad4718dcaa767947df1cadb14f39f4" +dependencies = [ + "glob", + "libc", + "libloading", +] + +[[package]] +name = "constant_time_eq" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d52eff69cd5e647efe296129160853a42795992097e8af39800e1060caeea9b" + +[[package]] +name = "cpufeatures" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "59ed5838eebb26a2bb2e58f6d5b5316989ae9d08bab10e0e6d103e656d1b0280" +dependencies = [ + "libc", +] + +[[package]] +name = "either" +version = "1.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" + +[[package]] +name = "find-msvc-tools" +version = "0.1.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5baebc0774151f905a1a2cc41989300b1e6fbb29aff0ceffa1064fdd3088d582" + +[[package]] +name = "glob" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0cc23270f6e1808e30a928bdc84dea0b9b4136a8bc82338574f23baf47bbd280" + +[[package]] +name = "itertools" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" +dependencies = [ + "either", +] + +[[package]] +name = "lean-ffi" +version = "0.1.0" +source = "git+https://github.com/argumentcomputer/lean-ffi?rev=91185181da859eb3941df2fbede24ae03838ed5b#91185181da859eb3941df2fbede24ae03838ed5b" +dependencies = [ + "bindgen", + "cc", + "num-bigint", +] + +[[package]] +name = "libc" +version = "0.2.183" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5b646652bf6661599e1da8901b3b9522896f01e736bad5f723fe7a3a27f899d" + +[[package]] +name = "libloading" +version = "0.8.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d7c4b02199fee7c5d21a5ae7d8cfa79a6ef5bb2fc834d6e9058e89c825efdc55" +dependencies = [ + "cfg-if", + "windows-link", +] + +[[package]] +name = "log" +version = "0.4.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" + +[[package]] +name = "memchr" +version = "2.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" + +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + +[[package]] +name = "nom" +version = "7.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" +dependencies = [ + "memchr", + "minimal-lexical", +] + +[[package]] +name = "num-bigint" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" +dependencies = [ + "num-integer", + "num-traits", +] + +[[package]] +name = "num-integer" +version = "0.1.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" +dependencies = [ + "num-traits", +] + +[[package]] +name = "num-traits" +version = "0.2.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" +dependencies = [ + "autocfg", +] + +[[package]] +name = "prettyplease" +version = "0.2.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b" +dependencies = [ + "proc-macro2", + "syn", +] + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "regex" +version = "1.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e10754a14b9137dd7b1e3e5b0493cc9171fdd105e0ab477f51b72e7f3ac0e276" +dependencies = [ + "aho-corasick", + "memchr", + "regex-automata", + "regex-syntax", +] + +[[package]] +name = "regex-automata" +version = "0.4.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e1dd4122fc1595e8162618945476892eefca7b88c52820e74af6262213cae8f" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax", +] + +[[package]] +name = "regex-syntax" +version = "0.8.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc897dd8d9e8bd1ed8cdad82b5966c3e0ecae09fb1907d58efaa013543185d0a" + +[[package]] +name = "rustc-hash" +version = "2.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "357703d41365b4b27c590e3ed91eabb1b663f07c4c084095e60cbed4362dff0d" + +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + +[[package]] +name = "syn" +version = "2.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "windows-link" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" diff --git a/rust/Cargo.toml b/rust/Cargo.toml new file mode 100644 index 0000000..68e3e06 --- /dev/null +++ b/rust/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "blake3-rs" +version = "0.1.0" +edition = "2024" + +[lib] +crate-type = ["staticlib"] + +[dependencies] +blake3 = "1.8.3" +lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi", rev = "91185181da859eb3941df2fbede24ae03838ed5b" } + +[profile.dev] +panic = "abort" + +[profile.release] +panic = "abort" diff --git a/rust/src/lib.rs b/rust/src/lib.rs new file mode 100644 index 0000000..ddadbc5 --- /dev/null +++ b/rust/src/lib.rs @@ -0,0 +1,70 @@ +use std::sync::LazyLock; + +use lean_ffi::include; +use lean_ffi::object::{ExternalClass, LeanByteArray, LeanExternal, LeanObject, LeanString}; + +static HASHER_CLASS: LazyLock = + LazyLock::new(ExternalClass::register_with_drop::); + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_version() -> LeanString { + LeanString::new("1.8.3") +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_init() -> LeanObject { + LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new()).into() +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_init_keyed(key: LeanByteArray) -> LeanObject { + let bytes = key.as_bytes(); + let key_array: &[u8; 32] = bytes.try_into().expect("key must be 32 bytes"); + LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new_keyed(key_array)).into() +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_init_derive_key(context: LeanByteArray) -> LeanObject { + let bytes = context.as_bytes(); + let ctx_str = std::str::from_utf8(bytes).expect("context must be valid UTF-8"); + LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new_derive_key(ctx_str)).into() +} + +/// Ensure copy-on-write: if the object is shared, clone the hasher into a new +/// external object; otherwise return it as-is for in-place mutation. +unsafe fn ensure_exclusive(obj: LeanObject) -> LeanObject { + if unsafe { include::lean_is_exclusive(obj.as_ptr() as *mut _) } { + obj + } else { + let ext = unsafe { LeanExternal::::from_raw(obj.as_ptr()) }; + let cloned = ext.get().clone(); + obj.dec_ref(); + LeanExternal::alloc(&HASHER_CLASS, cloned).into() + } +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_hasher_update( + self_: LeanObject, + input: LeanByteArray, +) -> LeanObject { + let obj = unsafe { ensure_exclusive(self_) }; + let hasher_ptr = + unsafe { include::lean_get_external_data(obj.as_ptr() as *mut _) as *mut blake3::Hasher }; + unsafe { (*hasher_ptr).update(input.as_bytes()) }; + obj +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_hasher_finalize(self_: LeanObject, len: usize) -> LeanObject { + let ext = unsafe { LeanExternal::::from_raw(self_.as_ptr()) }; + let hasher = ext.get(); + let out = LeanByteArray::alloc(len); + let buf = unsafe { + let cptr = include::lean_sarray_cptr(out.as_ptr() as *mut _); + std::slice::from_raw_parts_mut(cptr, len) + }; + hasher.finalize_xof().fill(buf); + self_.dec_ref(); + out.into() +} From 15cc1d401af19908329c85c5a41b452bc2131c51 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 12 Mar 2026 16:07:40 -0400 Subject: [PATCH 2/5] Modularize and fix Nix build --- Blake3/C.lean | 13 +++---- Blake3/Rust.lean | 13 +++---- flake.nix | 93 +++++++++++++++++++++++++++++++++++++----------- lakefile.lean | 9 ++--- 4 files changed, 89 insertions(+), 39 deletions(-) diff --git a/Blake3/C.lean b/Blake3/C.lean index a1c76fd..a8c4883 100644 --- a/Blake3/C.lean +++ b/Blake3/C.lean @@ -1,4 +1,5 @@ -import Blake3 +module +public import Blake3 /-! C-backed BLAKE3 bindings. -/ namespace Blake3.C @@ -18,19 +19,19 @@ protected opaque internalVersion : Unit → String def version : String := Blake3.C.internalVersion () @[extern "c_blake3_init"] -private opaque hasherInit : Unit → Hasher +opaque hasherInit : Unit → Hasher @[extern "c_blake3_init_keyed"] -private opaque hasherInitKeyed : @& Blake3Key → Hasher +opaque hasherInitKeyed : @& Blake3Key → Hasher @[extern "c_blake3_init_derive_key"] -private opaque hasherInitDeriveKey : @& ByteArray → Hasher +opaque hasherInitDeriveKey : @& ByteArray → Hasher @[extern "c_blake3_hasher_update"] -private opaque hasherUpdate : Hasher → @& ByteArray → Hasher +opaque hasherUpdate : Hasher → @& ByteArray → Hasher @[extern "c_blake3_hasher_finalize"] -private opaque hasherFinalize : Hasher → (length : USize) → +opaque hasherFinalize : Hasher → (length : USize) → { r : ByteArray // r.size = length.toNat } instance : HasherOps Hasher where diff --git a/Blake3/Rust.lean b/Blake3/Rust.lean index 88880f3..a381d3b 100644 --- a/Blake3/Rust.lean +++ b/Blake3/Rust.lean @@ -1,4 +1,5 @@ -import Blake3 +module +public import Blake3 /-! Rust-backed BLAKE3 bindings. -/ namespace Blake3.Rust @@ -18,19 +19,19 @@ protected opaque internalVersion : Unit → String def version : String := Blake3.Rust.internalVersion () @[extern "rs_blake3_init"] -private opaque hasherInit : Unit → Hasher +opaque hasherInit : Unit → Hasher @[extern "rs_blake3_init_keyed"] -private opaque hasherInitKeyed : @& Blake3Key → Hasher +opaque hasherInitKeyed : @& Blake3Key → Hasher @[extern "rs_blake3_init_derive_key"] -private opaque hasherInitDeriveKey : @& ByteArray → Hasher +opaque hasherInitDeriveKey : @& ByteArray → Hasher @[extern "rs_blake3_hasher_update"] -private opaque hasherUpdate : Hasher → @& ByteArray → Hasher +opaque hasherUpdate : Hasher → @& ByteArray → Hasher @[extern "rs_blake3_hasher_finalize"] -private opaque hasherFinalize : Hasher → (length : USize) → +opaque hasherFinalize : Hasher → (length : USize) → { r : ByteArray // r.size = length.toNat } instance : HasherOps Hasher where diff --git a/flake.nix b/flake.nix index bb03b17..215eaf5 100644 --- a/flake.nix +++ b/flake.nix @@ -41,35 +41,85 @@ pkgs, ... }: let + lake2nix = pkgs.callPackage lean4-nix.lake {}; + + # Lakefile patches for Nix builds + disableGitClone = '' + substituteInPlace lakefile.lean --replace-fail 'GitRepo.execGit' '--GitRepo.execGit' + ''; + # Don't build the `blake3_rs` static lib with Lake, since we build it with Crane + disableCargoBuild = '' + substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"' + ''; + linkBlake3Src = '' + ln -s ${blake3.outPath} ./blake3 + ''; + # Copy the `blake3_rs` static lib from Crane to `target/release` so Lake can use it + linkRustLib = '' + mkdir -p rust/target/release + ln -s ${rustPkg}/lib/libblake3_rs.a rust/target/release/ + ''; + # Pins the Rust toolchain rustToolchain = fenix.packages.${system}.fromToolchainFile { file = ./rust-toolchain.toml; sha256 = "sha256-sqSWJDUxc+zaz1nBWMAJKTAGBuGWP25GCftIOlCEAtA="; }; - lake2nix = pkgs.callPackage lean4-nix.lake {}; - commonArgs = { + + # Rust package + craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain; + rustPkg = craneLib.buildPackage { + src = craneLib.cleanCargoSource ./rust; + strictDeps = true; + + # `lean-ffi` uses `LEAN_SYSROOT` to locate `lean.h` for bindgen + LEAN_SYSROOT = "${pkgs.lean.lean-all}"; + # bindgen needs libclang to parse C headers + LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; + + buildInputs = + [] + ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [ + # Additional darwin specific inputs can be set here + pkgs.libiconv + ]; + }; + + blake3C = lake2nix.mkPackage { + name = "Blake3C"; + src = ./.; + buildLibrary = true; + postPatch = disableGitClone; + preConfigure = linkBlake3Src; + postInstall = '' + cp -rP ./blake3 $out + ''; + }; + + blake3Rust = lake2nix.mkPackage { + name = "Blake3Rust"; src = ./.; - postPatch = '' - substituteInPlace lakefile.lean --replace-fail 'GitRepo.execGit' '--GitRepo.execGit' + postPatch = disableCargoBuild; + postConfigure = linkRustLib; + postInstall = '' + cp -rP rust/target/release $out/rust/target ''; - preConfigure = '' - ln -s ${blake3.outPath} ./blake3 + }; + + blake3Test = lake2nix.mkPackage { + name = "Blake3Test"; + src = ./.; + installArtifacts = false; + # Merge .lake artifacts from both C and Rust library builds + prePatch = '' + rsync -a ${blake3C}/.lake/ .lake/ + rsync -a ${blake3Rust}/.lake/ .lake/ + chmod -R +w .lake ''; + postPatch = disableGitClone + disableCargoBuild; + preConfigure = linkBlake3Src; + postConfigure = linkRustLib; }; - blake3Lib = lake2nix.mkPackage (commonArgs - // { - name = "Blake3"; - buildLibrary = true; - postInstall = '' - cp -rP ./blake3 $out - ''; - }); - blake3Test = lake2nix.mkPackage (commonArgs - // { - name = "Blake3Test"; - lakeArtifacts = blake3Lib; - installArtifacts = false; - }); in { _module.args.pkgs = import nixpkgs { inherit system; @@ -77,7 +127,8 @@ }; packages = { - default = blake3Lib; + default = blake3C; + rust = blake3Rust; test = blake3Test; }; devShells.default = pkgs.mkShell { diff --git a/lakefile.lean b/lakefile.lean index 299d683..75aed4a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,8 +5,7 @@ open Lake DSL package Blake3 @[default_target] -lean_lib Blake3 where - precompileModules := true +lean_lib Blake3 @[test_driver] lean_exe Blake3Test @@ -74,9 +73,8 @@ target blake3_c pkg : System.FilePath := do let name := nameToStaticLib "blake3_c" buildStaticLib (pkg.staticLibDir / name) oFileJobs -lean_lib «Blake3.C» where +lean_lib Blake3C where roots := #[`Blake3.C] - precompileModules := true moreLinkObjs := #[blake3_c] -- Rust FFI @@ -85,8 +83,7 @@ target blake3_rs pkg : System.FilePath := do let libName := nameToStaticLib "blake3_rs" inputBinFile $ pkg.dir / "rust" / "target" / "release" / libName -lean_lib «Blake3.Rust» where +lean_lib Blake3Rust where roots := #[`Blake3.Rust] - precompileModules := true moreLinkObjs := #[blake3_rs] From 4124102fe623684c979edae9045780ec43a05d1b Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 12 Mar 2026 18:31:31 -0400 Subject: [PATCH 3/5] Add dot-methods and Valgrind CI test --- .github/workflows/ci.yml | 31 +++++++++++++++++++++++++++++++ Blake3.lean | 2 +- Blake3/C.lean | 12 ++++++++++++ Blake3/Rust.lean | 12 ++++++++++++ Blake3Test.lean | 16 +++++++++------- 5 files changed, 65 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3c70006..97b37cb 100644 --- a/.github/workflows/ci.yml +++ b/.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: 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 diff --git a/Blake3.lean b/Blake3.lean index 35be242..eb46e66 100644 --- a/Blake3.lean +++ b/Blake3.lean @@ -1,7 +1,7 @@ module /-! Shared types and generic logic for BLAKE3 bindings. -/ -private theorem ByteArray.size_of_extract {hash : ByteArray} (h : e ≤ hash.size) : +theorem ByteArray.size_of_extract {hash : ByteArray} (h : e ≤ hash.size) : (hash.extract b e).size = e - b := by simp [Nat.min_eq_left h] diff --git a/Blake3/C.lean b/Blake3/C.lean index a8c4883..0ea9128 100644 --- a/Blake3/C.lean +++ b/Blake3/C.lean @@ -46,5 +46,17 @@ 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 diff --git a/Blake3/Rust.lean b/Blake3/Rust.lean index a381d3b..5041e88 100644 --- a/Blake3/Rust.lean +++ b/Blake3/Rust.lean @@ -46,5 +46,17 @@ 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 diff --git a/Blake3Test.lean b/Blake3Test.lean index 262c4b1..9a58ed0 100644 --- a/Blake3Test.lean +++ b/Blake3Test.lean @@ -17,13 +17,6 @@ instance : Blake3Backend Blake3.Rust.Hasher where abbrev input : ByteArray := ⟨#[0]⟩ -abbrev key : Blake3Key := .ofBytes ⟨#[ - 3, 123, 16, 175, 8, 196, 101, 134, - 144, 184, 221, 34, 25, 106, 122, 200, - 213, 14, 159, 189, 82, 166, 91, 107, - 33, 78, 26, 226, 89, 65, 188, 92 -]⟩ - abbrev expectedOutputRegularHashing : ByteArray := ⟨#[ 45, 58, 222, 223, 241, 27, 97, 241, 76, 136, 110, 53, 175, 160, 54, 115, @@ -31,6 +24,14 @@ abbrev expectedOutputRegularHashing : ByteArray := ⟨#[ 81, 2, 37, 208, 245, 146, 226, 19 ]⟩ +-- Good pseudo-random key +abbrev key : Blake3Key := .ofBytes ⟨#[ + 3, 123, 16, 175, 8, 196, 101, 134, + 144, 184, 221, 34, 25, 106, 122, 200, + 213, 14, 159, 189, 82, 166, 91, 107, + 33, 78, 26, 226, 89, 65, 188, 92 +]⟩ + abbrev expectedOutputKeyedHashing: ByteArray := ⟨#[ 145, 187, 220, 234, 206, 139, 205, 138, 220, 103, 35, 65, 199, 96, 210, 18, @@ -38,6 +39,7 @@ abbrev expectedOutputKeyedHashing: ByteArray := ⟨#[ 2, 29, 12, 32, 17, 118, 181, 232 ]⟩ +-- Context (with "bad" randomness) abbrev context : ByteArray := ⟨#[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]⟩ abbrev expectedOutputDeriveKeyHashing: ByteArray := ⟨#[ From 147532256b6d98e74c448f5da6caf068fb932604 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 12 Mar 2026 18:40:41 -0400 Subject: [PATCH 4/5] Update Readme --- .github/workflows/ci.yml | 2 +- README.md | 59 +++++++++++++++++++++++++++++++++++++++- 2 files changed, 59 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 97b37cb..1598d06 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,7 +23,7 @@ jobs: test: true valgrind: - needs: test + needs: lean-test runs-on: ubuntu-latest steps: - uses: actions/checkout@v6 diff --git a/README.md b/README.md index dcc460c..fc0ea9c 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,60 @@ # Blake3.lean -Lean bindings to the BLAKE3 hasher based on the [C implementation](https://github.com/BLAKE3-team/BLAKE3/tree/master/c). +Lean bindings to the [BLAKE3 hasher](https://github.com/BLAKE3-team/BLAKE3) for the C and Rust implementations. + +## Usage + +Add Blake3 as a dependency in your `lakefile.lean`: + +```lean +require Blake3 from git + "https://github.com/pnmadelaea/Blake3.lean" @ "" +``` + +### C backend + +```lean +import Blake3.C + +def main : IO Unit := do + let hash := Blake3.C.hash ⟨#[72, 101, 108, 108, 111]⟩ -- "Hello" + IO.println s!"BLAKE3: {hash.val.toList}" +``` + +### Rust backend + +```lean +import Blake3.Rust + +def main : IO Unit := do + let hash := Blake3.Rust.hash ⟨#[72, 101, 108, 108, 111]⟩ + IO.println s!"BLAKE3: {hash.val.toList}" +``` + +### Keyed hashing and key derivation + +Both backends implement the `HasherOps` typeclass, which provides `hash`, `hashKeyed`, and `hashDeriveKey`: + +```lean +import Blake3.C +open Blake3 + +def main : IO Unit := do + let input : ByteArray := ⟨#[0]⟩ + + -- Keyed hash + let key : Blake3Key := .ofBytes ⟨#[ + 3, 123, 16, 175, 8, 196, 101, 134, + 144, 184, 221, 34, 25, 106, 122, 200, + 213, 14, 159, 189, 82, 166, 91, 107, + 33, 78, 26, 226, 89, 65, 188, 92 + ]⟩ + let keyedHash := HasherOps.hashKeyed (H := Blake3.C.Hasher) input key + + -- Derive key + let context := "example 2025-01-01 context".toUTF8 + let derived := HasherOps.hashDeriveKey (H := Blake3.C.Hasher) input context + + IO.println s!"keyed: {keyedHash.val.toList}" + IO.println s!"derived: {derived.val.toList}" +``` From 87e0b46101be07c6cdb86c5c25f6c26b8f0c6f94 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 12 Mar 2026 19:13:27 -0400 Subject: [PATCH 5/5] Fix Nix build --- flake.nix | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/flake.nix b/flake.nix index 215eaf5..4e58ccb 100644 --- a/flake.nix +++ b/flake.nix @@ -43,6 +43,19 @@ }: let lake2nix = pkgs.callPackage lean4-nix.lake {}; + # Filter out build directories + lakeSrc = pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: let + name = builtins.baseNameOf path; + in + name + != "target" + && name != ".lake" + && name + != "build"; + }; + # Lakefile patches for Nix builds disableGitClone = '' substituteInPlace lakefile.lean --replace-fail 'GitRepo.execGit' '--GitRepo.execGit' @@ -87,7 +100,7 @@ blake3C = lake2nix.mkPackage { name = "Blake3C"; - src = ./.; + src = lakeSrc; buildLibrary = true; postPatch = disableGitClone; preConfigure = linkBlake3Src; @@ -98,17 +111,17 @@ blake3Rust = lake2nix.mkPackage { name = "Blake3Rust"; - src = ./.; + src = lakeSrc; postPatch = disableCargoBuild; postConfigure = linkRustLib; postInstall = '' - cp -rP rust/target/release $out/rust/target + cp -rP rust/target/ $out/rust/target/ ''; }; blake3Test = lake2nix.mkPackage { name = "Blake3Test"; - src = ./.; + src = lakeSrc; installArtifacts = false; # Merge .lake artifacts from both C and Rust library builds prePatch = ''