From 68285cd361eb7f7658b7ab1a2d08dadf751cce4a Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 1 Sep 2026 15:50:24 -0400
Subject: [PATCH] lakefile: drop Blake3 from the native-decide dynlib

Blake3 now precompiles its libraries, so Lake loads their shared objects --
which bundle the C and Rust FFI objects -- into any process elaborating a
module that imports them. The Blake3 half of `ix_native_decide_dynlib` was
assembling that by hand from a `blake3_rs_shared` cdylib, and that target no
longer exists upstream.

The target keeps Ix's own externs, which nothing else supplies. Precompiling
`Ix.Unsigned` instead would work, but only as its own library declared after
`Ix`: both would claim the module, `Package.findModule?` resolves with
`findSomeRev?`, and losing that race silently stops precompiling it -- with
the symptom appearing as a missing native implementation inside a proof file
rather than as a configuration error. A local dynlib naming its modules
outright is worth more than the lines it costs.

The Blake3 pin moves to the revision that turned precompilation on, and moves
in lakefile.lean, lake-manifest.json, flake.nix and flake.lock together. The
lakefile drops the cdylib that the older revision still provides, so a pin
left behind in any one of them pairs the new lakefile with a Blake3 that does
not precompile -- and that mismatch surfaces as a missing native
implementation inside a proof file rather than as a build error.
---
 flake.lock         |  8 ++++----
 flake.nix          |  2 +-
 lake-manifest.json |  4 ++--
 lakefile.lean      | 39 ++++++++++++++++-----------------------
 4 files changed, 23 insertions(+), 30 deletions(-)

diff --git a/flake.lock b/flake.lock
index a18b189f..0fb93f76 100644
--- a/flake.lock
+++ b/flake.lock
@@ -33,17 +33,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1787430037,
-        "narHash": "sha256-0dLeEO55z4nHvSv8xb9BMoCZTbIc9IqVuId7z8oa4kA=",
+        "lastModified": 1788353452,
+        "narHash": "sha256-R08Yd5y8PMyrwxTMUFDDzdbf9057+f52bz9Y/e/poiY=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba",
+        "rev": "2db8f692ed94f7c4a993527008b8c5231b169709",
         "type": "github"
       },
       "original": {
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba",
+        "rev": "2db8f692ed94f7c4a993527008b8c5231b169709",
         "type": "github"
       }
     },
diff --git a/flake.nix b/flake.nix
index 9254cf0b..20751066 100644
--- a/flake.nix
+++ b/flake.nix
@@ -31,7 +31,7 @@
 
     # Blake3 Rust bindings for Lean
     blake3-lean = {
-      url = "github:argumentcomputer/Blake3.lean/e6e908bfd3af607ab44fb462fa2276a2c81addba";
+      url = "github:argumentcomputer/Blake3.lean/2db8f692ed94f7c4a993527008b8c5231b169709";
       # System packages, follows lean4-nix so we stay in sync
       inputs.lean4-nix.follows = "lean4-nix";
     };
diff --git a/lake-manifest.json b/lake-manifest.json
index bcd9d471..59e49660 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba",
+   "rev": "2db8f692ed94f7c4a993527008b8c5231b169709",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "e6e908bfd3af607ab44fb462fa2276a2c81addba",
+   "inputRev": "2db8f692ed94f7c4a993527008b8c5231b169709",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
diff --git a/lakefile.lean b/lakefile.lean
index cfbcb5fe..e3d14e8e 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -7,13 +7,15 @@ package ix where
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "ab4d5eb461941837f48eb891be755c8c73e89fdd"
 
-/- Blake3's `blake3_rs_shared` target builds `blake3-rs` as a `cdylib`
-alongside the staticlib. `ix_native_decide_dynlib` fetches it to supply the
-BLAKE3 backend to Lean's native evaluator, and that dynlib gates every
-`IxTcVerify` module, so this pin must stay at or after the revision that
-introduced the target. -/
+/- Blake3 precompiles its libraries, so Lake loads their shared objects -- which
+bundle the C and Rust FFI objects -- into any process elaborating a module that
+imports them. That is what supplies the BLAKE3 backend to Lean's native evaluator
+for the `native_decide` proofs in `IxTcVerify`, so this pin must stay at or after
+the revision that turned precompilation on. Before it, Blake3 exposed a
+`blake3_rs_shared` cdylib that `ix_native_decide_dynlib` had to fetch and link;
+that target no longer exists. -/
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "e6e908bfd3af607ab44fb462fa2276a2c81addba"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "2db8f692ed94f7c4a993527008b8c5231b169709"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
@@ -230,29 +232,20 @@ opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
 * the raw Rust symbol it forwards to, taken from that crate's `cdylib`, recorded
   by absolute path so no `LD_LIBRARY_PATH` is needed.
 
-Covered externs: `Blake3.Rust` hashing (with the `Blake3` base module, which
-holds the `HasherOps.hash` orchestration `Address.blake3` calls) against
-`blake3_rs`, and `Ix.Unsigned.toLEBytes` against `ix-ffi-dyn`. -/
+Covers Ix's own externs only -- currently `Ix.Unsigned.toLEBytes` against
+`ix-ffi-dyn`. Blake3's are not here: that package precompiles its libraries, so
+Lake loads their shared objects into the elaborating process by itself. -/
 target ix_native_decide_dynlib pkg : Dynlib := do
-  let some blake3Base ← findModule? `Blake3
-    | error "module `Blake3` not found; is the Blake3 dependency available?"
-  let some blake3Rust ← findModule? `Blake3.Rust
-    | error "module `Blake3.Rust` not found; is the Blake3 dependency available?"
   let some ixUnsigned ← findModule? `Ix.Unsigned
     | error "module `Ix.Unsigned` not found"
-  -- Raw symbols come from each crate's cdylib, recorded by path, and are built
-  -- by fetching the owning package's target (no direct cargo calls here):
-  -- Blake3 via its `blake3_rs_shared`, Ix via the minimal `ix_ffi_dyn`.
-  let blake3Cdylib := (← blake3Rust.pkg.fetchTargetJob `blake3_rs_shared).map fun _ =>
-    blake3Rust.pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
+  -- Raw symbols come from the crate's cdylib, recorded by path, and are built
+  -- by fetching the owning target (no direct cargo calls here).
   let ixCdylib ← ix_ffi_dyn.fetch
-  -- Boxed entry points are Lean's own generated objects for the declaring modules.
-  let mut boxedObjs := #[]
-  for mod in #[blake3Base, blake3Rust, ixUnsigned] do
-    boxedObjs := boxedObjs ++ (← (mod.nativeFacets true).mapM (·.fetch mod))
+  -- Boxed entry points are Lean's own generated objects for the declaring module.
+  let boxedObjs ← (ixUnsigned.nativeFacets true).mapM (·.fetch ixUnsigned)
   buildSharedLib "ix_native_decide"
     (pkg.buildDir / nameToSharedLib "ix_native_decide")
-    (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
+    (boxedObjs.push ixCdylib) #[]
 
 /- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
 Non-default: `lake build ix` never