From b5636a37b5c4b2c297d90bbe51400466d26f2ee1 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Thu, 12 Mar 2026 19:26:21 -0400
Subject: [PATCH] feat: Use Blake3.lean Rust bindings instead of C

---
 Cargo.toml             |  2 +-
 Ix/Address.lean        |  4 +--
 Ix/CanonM.lean         |  2 +-
 Ix/Environment.lean    | 59 ++++++++++++++++++------------------
 Ix/Sharing.lean        |  2 +-
 Tests/Aiur/Hashes.lean |  4 +--
 Tests/Gen/Ixon.lean    |  2 +-
 Tests/Ix/Ixon.lean     |  6 ++--
 flake.lock             | 68 ++++++++++++++++++++++++++++++++++++++----
 flake.nix              |  6 ++--
 lake-manifest.json     |  4 +--
 lakefile.lean          |  2 +-
 12 files changed, 110 insertions(+), 51 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index 96cef556..821693c7 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -8,7 +8,7 @@ crate-type = ["staticlib"]
 
 [dependencies]
 anyhow = "1"
-blake3 = "1.8.2"
+blake3 = "1.8.3"
 itertools = "0.14.0"
 indexmap = { version = "2", features = ["rayon"] }
 lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi", rev = "91185181da859eb3941df2fbede24ae03838ed5b" }
diff --git a/Ix/Address.lean b/Ix/Address.lean
index e6530497..c0d69b4f 100644
--- a/Ix/Address.lean
+++ b/Ix/Address.lean
@@ -2,7 +2,7 @@ module
 public import Lean.ToExpr
 public import Ix.ByteArray
 public import Ix.Common
-public import Blake3
+public import Blake3.Rust
 
 public section
 
@@ -15,7 +15,7 @@ structure Address where
   deriving Lean.ToExpr, BEq, Hashable
 
 /-- Compute the Blake3 hash of a `ByteArray`, returning an `Address`. -/
-def Address.blake3 (x: ByteArray) : Address := ⟨(Blake3.hash x).val⟩
+def Address.blake3 (x: ByteArray) : Address := ⟨(Blake3.Rust.hash x).val⟩
 
 /-- Convert a nibble (0--15) to its lowercase hexadecimal character. -/
 def hexOfNat : Nat -> Option Char
diff --git a/Ix/CanonM.lean b/Ix/CanonM.lean
index 19246409..840d379f 100644
--- a/Ix/CanonM.lean
+++ b/Ix/CanonM.lean
@@ -66,7 +66,7 @@ def internExpr (ptr: USize) (y : Ix.Expr) : CanonM Unit := do
   }
 
 def internDataValue (ptr: USize) (y : Ix.DataValue) : CanonM Unit := do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Blake3.Rust.Hasher.init ()
   h := Ix.Expr.hashDataValue h y
   let h' := ⟨(h.finalizeWithLength 32).val⟩
   modify fun s => { s with
diff --git a/Ix/Environment.lean b/Ix/Environment.lean
index 85c22d6c..4580764b 100644
--- a/Ix/Environment.lean
+++ b/Ix/Environment.lean
@@ -6,7 +6,7 @@
 -/
 module
 
-public import Blake3
+public import Blake3.Rust
 public import Std.Data.HashMap
 public import Batteries.Data.RBMap
 public import Ix.Address
@@ -16,6 +16,7 @@ public section
 namespace Ix
 
 open Std (HashMap)
+open Blake3.Rust (Hasher)
 
 /-! ## LEON (Lean Objective Notation) Tags (must match Rust env.rs) -/
 def TAG_NANON : UInt8 := 0x00
@@ -86,7 +87,7 @@ instance : Inhabited Name where
 
 /-- Construct a string name component, hashing the tag, parent hash, and string bytes. -/
 def mkStr (pre: Name) (s: String): Name := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_NSTR])
   h := h.update pre.getHash.hash
   h := h.update s.toUTF8
@@ -94,7 +95,7 @@ def mkStr (pre: Name) (s: String): Name := Id.run <| do
 
 /-- Construct a numeric name component, hashing the tag, parent hash, and little-endian nat bytes. -/
 def mkNat (pre: Name) (i: Nat): Name := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_NNUM])
   h := h.update pre.getHash.hash
   h := h.update ⟨i.toBytesLE⟩
@@ -150,33 +151,33 @@ def getHash : Level → Address
 def mkZero : Level := .zero <| Address.blake3 (ByteArray.mk #[TAG_UZERO])
 
 def mkSucc (x: Level) : Level := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_USUCC])
   h := h.update x.getHash.hash
   .succ x ⟨(h.finalizeWithLength 32).val⟩
 
 def mkMax (x y : Level) : Level := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_UMAX])
   h := h.update x.getHash.hash
   h := h.update y.getHash.hash
   .max x y ⟨(h.finalizeWithLength 32).val⟩
 
 def mkIMax (x y : Level) : Level := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_UIMAX])
   h := h.update x.getHash.hash
   h := h.update y.getHash.hash
   .imax x y ⟨(h.finalizeWithLength 32).val⟩
 
 def mkParam (n: Name) : Level := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_UPARAM])
   h := h.update n.getHash.hash
   .param n ⟨(h.finalizeWithLength 32).val⟩
 
 def mkMvar (n: Name) : Level := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_UMVAR])
   h := h.update n.getHash.hash
   .mvar n ⟨(h.finalizeWithLength 32).val⟩
@@ -285,31 +286,31 @@ instance : Hashable Expr where
   hash e := hash e.getHash  -- Uses Address's Hashable (first 8 bytes as LE u64)
 
 def mkBVar (x: Nat) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_EVAR])
   h := h.update ⟨x.toBytesLE⟩
   .bvar x ⟨(h.finalizeWithLength 32).val⟩
 
 def mkFVar (x: Name) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_EFVAR])
   h := h.update x.getHash.hash
   .fvar x ⟨(h.finalizeWithLength 32).val⟩
 
 def mkMVar (x: Name) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_EMVAR])
   h := h.update x.getHash.hash
   .mvar x ⟨(h.finalizeWithLength 32).val⟩
 
 def mkSort (x: Level) : Expr := Id.run <| do
-  let h := Blake3.Hasher.init ()
+  let h := Hasher.init ()
   let h := h.update (ByteArray.mk #[TAG_ESORT])
   let h := h.update x.getHash.hash
   .sort x ⟨(h.finalizeWithLength 32).val⟩
 
 def mkConst (x: Name) (us: Array Level): Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_EREF])
   h := h.update x.getHash.hash
   for u in us do
@@ -317,14 +318,14 @@ def mkConst (x: Name) (us: Array Level): Expr := Id.run <| do
   .const x us ⟨(h.finalizeWithLength 32).val⟩
 
 def mkApp (f a : Expr) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_EAPP])
   h := h.update f.getHash.hash
   h := h.update a.getHash.hash
   .app f a ⟨(h.finalizeWithLength 32).val⟩
 
 def mkLam (n : Name) (t b : Expr) (bi : Lean.BinderInfo) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_ELAM])
   h := h.update n.getHash.hash
   h := h.update t.getHash.hash
@@ -333,7 +334,7 @@ def mkLam (n : Name) (t b : Expr) (bi : Lean.BinderInfo) : Expr := Id.run <| do
   .lam n t b bi ⟨(h.finalizeWithLength 32).val⟩
 
 def mkForallE (n : Name) (t b : Expr) (bi : Lean.BinderInfo) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_EALL])
   h := h.update n.getHash.hash
   h := h.update t.getHash.hash
@@ -342,7 +343,7 @@ def mkForallE (n : Name) (t b : Expr) (bi : Lean.BinderInfo) : Expr := Id.run <|
   .forallE n t b bi ⟨(h.finalizeWithLength 32).val⟩
 
 def mkLetE (n : Name) (t v b : Expr) (nd : Bool) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_ELET])
   h := h.update n.getHash.hash
   h := h.update t.getHash.hash
@@ -352,7 +353,7 @@ def mkLetE (n : Name) (t v b : Expr) (nd : Bool) : Expr := Id.run <| do
   .letE n t v b nd ⟨(h.finalizeWithLength 32).val⟩
 
 def mkLit (l : Lean.Literal) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   match l with
   | .natVal n =>
     h := h.update (ByteArray.mk #[TAG_ENAT])
@@ -363,14 +364,14 @@ def mkLit (l : Lean.Literal) : Expr := Id.run <| do
   .lit l ⟨(h.finalizeWithLength 32).val⟩
 
 def mkProj (n : Name) (i : Nat) (e : Expr) : Expr := Id.run <| do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_EPRJ])
   h := h.update n.getHash.hash
   h := h.update ⟨i.toBytesLE⟩
   h := h.update e.getHash.hash
   .proj n i e ⟨(h.finalizeWithLength 32).val⟩
 
-def hashInt (h : Blake3.Hasher) (i : Int) : Blake3.Hasher := Id.run do
+def hashInt (h : Hasher) (i : Int) : Hasher := Id.run do
   let mut h := h.update (ByteArray.mk #[TAG_MINT])
   match i with
   | .ofNat n =>
@@ -381,7 +382,7 @@ def hashInt (h : Blake3.Hasher) (i : Int) : Blake3.Hasher := Id.run do
     h := h.update ⟨n.toBytesLE⟩
   h
 
-def hashSubstring (h : Blake3.Hasher) (ss : Substring) : Blake3.Hasher :=
+def hashSubstring (h : Hasher) (ss : Substring) : Hasher :=
   Id.run do
     let mut h := h.update (ByteArray.mk #[TAG_MSSTR])
     h := h.update ss.str.toUTF8
@@ -389,7 +390,7 @@ def hashSubstring (h : Blake3.Hasher) (ss : Substring) : Blake3.Hasher :=
     h := h.update ⟨ss.stopPos.toBytesLE⟩
     h
 
-def hashSourceInfo (h : Blake3.Hasher) (si : SourceInfo) : Blake3.Hasher :=
+def hashSourceInfo (h : Hasher) (si : SourceInfo) : Hasher :=
   Id.run do
     let mut h := h.update (ByteArray.mk #[TAG_MSINFO])
     match si with
@@ -408,8 +409,8 @@ def hashSourceInfo (h : Blake3.Hasher) (si : SourceInfo) : Blake3.Hasher :=
       h := h.update (ByteArray.mk #[2])
     h
 
-def hashSyntaxPreresolved (h : Blake3.Hasher) (sp : SyntaxPreresolved)
-    : Blake3.Hasher := Id.run do
+def hashSyntaxPreresolved (h : Hasher) (sp : SyntaxPreresolved)
+    : Hasher := Id.run do
   let mut h := h.update (ByteArray.mk #[TAG_MSPRE])
   match sp with
   | .namespace name =>
@@ -423,8 +424,8 @@ def hashSyntaxPreresolved (h : Blake3.Hasher) (sp : SyntaxPreresolved)
       h := h.update (ByteArray.mk #[0])
   h
 
-private partial def hashSyntax (h : Blake3.Hasher) (syn : Syntax)
-    : Blake3.Hasher := Id.run do
+private partial def hashSyntax (h : Hasher) (syn : Syntax)
+    : Hasher := Id.run do
   let mut h := h.update (ByteArray.mk #[TAG_MSYN])
   match syn with
   | .missing =>
@@ -450,8 +451,8 @@ private partial def hashSyntax (h : Blake3.Hasher) (syn : Syntax)
       h := hashSyntaxPreresolved h pr
   h
 
-def hashDataValue (h : Blake3.Hasher) (dv : DataValue)
-    : Blake3.Hasher := Id.run do
+def hashDataValue (h : Hasher) (dv : DataValue)
+    : Hasher := Id.run do
   let mut h := h.update (ByteArray.mk #[TAG_MDVAL])
   match dv with
   | .ofString s =>
@@ -475,7 +476,7 @@ def hashDataValue (h : Blake3.Hasher) (dv : DataValue)
   h
 
 def mkMData (data : Array (Name × DataValue)) (e : Expr) : Expr := Id.run do
-  let mut h := Blake3.Hasher.init ()
+  let mut h := Hasher.init ()
   h := h.update (ByteArray.mk #[TAG_EMDATA])
   h := h.update ⟨data.size.toBytesLE⟩
   for (name, dv) in data do
diff --git a/Ix/Sharing.lean b/Ix/Sharing.lean
index c0eec6b9..7bc228bf 100644
--- a/Ix/Sharing.lean
+++ b/Ix/Sharing.lean
@@ -18,7 +18,7 @@ public import Ix.Ixon
 public import Ix.Address
 public import Ix.Common
 public import Std.Data.HashMap
-public import Blake3
+public import Blake3.Rust
 
 public section
 
diff --git a/Tests/Aiur/Hashes.lean b/Tests/Aiur/Hashes.lean
index b185fa2c..0fe8ea4e 100644
--- a/Tests/Aiur/Hashes.lean
+++ b/Tests/Aiur/Hashes.lean
@@ -5,11 +5,11 @@ public import Ix.IxVM.ByteStream
 public import Ix.IxVM.Blake3
 public import Ix.IxVM.Sha256
 public import Tests.Sha256
-public import Blake3
+public import Blake3.Rust
 
 def mkBlake3HashTestCase (size : Nat) : AiurTestCase :=
   let inputBytes := Array.range size |>.map Nat.toUInt8
-  let outputBytes := Blake3.hash ⟨inputBytes⟩ |>.val.data
+  let outputBytes := Blake3.Rust.hash ⟨inputBytes⟩ |>.val.data
   let input := inputBytes.map .ofUInt8
   let output := outputBytes.map .ofUInt8
   let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0]
diff --git a/Tests/Gen/Ixon.lean b/Tests/Gen/Ixon.lean
index 71bf9afe..b08be662 100644
--- a/Tests/Gen/Ixon.lean
+++ b/Tests/Gen/Ixon.lean
@@ -24,7 +24,7 @@ def genAddress : Gen Address := do
   for _ in [:32] do
     let b ← Gen.choose Nat 0 255
     bytes := bytes.push b.toUInt8
-  pure ⟨(Blake3.hash bytes).val⟩
+  pure ⟨(Blake3.Rust.hash bytes).val⟩
 
 def genIxonNat : Gen Nat := USize.toNat <$> genUSize
 
diff --git a/Tests/Ix/Ixon.lean b/Tests/Ix/Ixon.lean
index ab547fc7..8a30d693 100644
--- a/Tests/Ix/Ixon.lean
+++ b/Tests/Ix/Ixon.lean
@@ -93,13 +93,13 @@ def constantUnits : TestSeq :=
   let c := Constant.mk
     (.defn defn)
     #[.var 0, .sort 1]  -- sharing
-    #[⟨(Blake3.hash "ref".toUTF8).val⟩]  -- refs
+    #[⟨(Blake3.Rust.hash "ref".toUTF8).val⟩]  -- refs
     #[.zero, .succ .zero]  -- univs
   test "Constant roundtrip" (constantSerde c)
 
 def commUnits : TestSeq :=
-  let addr1 : Address := ⟨(Blake3.hash "secret".toUTF8).val⟩
-  let addr2 : Address := ⟨(Blake3.hash "payload".toUTF8).val⟩
+  let addr1 : Address := ⟨(Blake3.Rust.hash "secret".toUTF8).val⟩
+  let addr2 : Address := ⟨(Blake3.Rust.hash "payload".toUTF8).val⟩
   let c := Comm.mk addr1 addr2
   test "Comm roundtrip" (commSerde c)
 
diff --git a/flake.lock b/flake.lock
index 44a265c5..65756ab3 100644
--- a/flake.lock
+++ b/flake.lock
@@ -20,6 +20,8 @@
     "blake3-lean": {
       "inputs": {
         "blake3": "blake3",
+        "crane": "crane",
+        "fenix": "fenix",
         "flake-parts": "flake-parts",
         "lean4-nix": [
           "lean4-nix"
@@ -31,20 +33,36 @@
         ]
       },
       "locked": {
-        "lastModified": 1772039537,
-        "narHash": "sha256-HOSEL2CCo1A8HACVJ2P3DILGxO3OxLiHnGbWLGaH9bM=",
+        "lastModified": 1773357687,
+        "narHash": "sha256-i/fbsMosyKSVCicKOSR7tqZcpLH37gHhkdNjfN78B+8=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "564e0ab364ebaa3b1153defe2f49c9fe58a2d77c",
+        "rev": "87e0b46101be07c6cdb86c5c25f6c26b8f0c6f94",
         "type": "github"
       },
       "original": {
         "owner": "argumentcomputer",
+        "ref": "rust-bindings",
         "repo": "Blake3.lean",
         "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"
+      }
+    },
+    "crane_2": {
       "locked": {
         "lastModified": 1771121070,
         "narHash": "sha256-aIlv7FRXF9q70DNJPI237dEDAznSKaXmL5lfK/Id/bI=",
@@ -62,11 +80,34 @@
     "fenix": {
       "inputs": {
         "nixpkgs": [
+          "blake3-lean",
           "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"
+      }
+    },
+    "fenix_2": {
+      "inputs": {
+        "nixpkgs": [
+          "lean4-nix",
+          "nixpkgs"
+        ],
+        "rust-analyzer-src": "rust-analyzer-src_2"
+      },
       "locked": {
         "lastModified": 1771312404,
         "narHash": "sha256-eJ1YY3a+uQTfa1T3LsR2JX7n3F9vAKAwsuX/3Aecve0=",
@@ -218,8 +259,8 @@
     "root": {
       "inputs": {
         "blake3-lean": "blake3-lean",
-        "crane": "crane",
-        "fenix": "fenix",
+        "crane": "crane_2",
+        "fenix": "fenix_2",
         "flake-parts": "flake-parts_2",
         "lean4-nix": "lean4-nix",
         "nixpkgs": [
@@ -229,6 +270,23 @@
       }
     },
     "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"
+      }
+    },
+    "rust-analyzer-src_2": {
       "flake": false,
       "locked": {
         "lastModified": 1771264911,
diff --git a/flake.nix b/flake.nix
index d36d1b24..973500a2 100644
--- a/flake.nix
+++ b/flake.nix
@@ -29,9 +29,9 @@
 
     crane.url = "github:ipetkov/crane";
 
-    # Blake3 C bindings for Lean
+    # Blake3 Rust bindings for Lean
     blake3-lean = {
-      url = "github:argumentcomputer/Blake3.lean";
+      url = "github:argumentcomputer/Blake3.lean?ref=rust-bindings";
       # System packages, follows lean4-nix so we stay in sync
       inputs.lean4-nix.follows = "lean4-nix";
     };
@@ -97,7 +97,7 @@
         lakeDeps = lake2nix.buildDeps {
           src = ./.;
           depOverrideDeriv = {
-            Blake3 = blake3-lean.packages.${system}.default;
+            Blake3 = blake3-lean.packages.${system}.rust;
           };
         };
         lakeBuildArgs = {
diff --git a/lake-manifest.json b/lake-manifest.json
index 249967e0..45483eda 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f89c732c481f87a47465041c6d7d659e1812848b",
+   "rev": "87e0b46101be07c6cdb86c5c25f6c26b8f0c6f94",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f89c732c481f87a47465041c6d7d659e1812848b",
+   "inputRev": "rust-bindings",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
diff --git a/lakefile.lean b/lakefile.lean
index abd0c773..5bdb1975 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -15,7 +15,7 @@ require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "928f27c7de8318455ba0be7461dbdf7096f4075a"
 
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "f89c732c481f87a47465041c6d7d659e1812848b"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "rust-bindings"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "v4.28.0"