From f8e12698478a924190409c1b8fa0227f8055dee4 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 13:48:25 -0400
Subject: [PATCH 1/2] rust: also build blake3-rs as a cdylib

Add a cdylib output alongside the staticlib so the raw rs_blake3_* FFI
symbols can be loaded as a position-independent shared object at runtime.
This lets downstream tooling supply the BLAKE3 backend to Lean's native
evaluator for native_decide proofs, which are elaborated before any final
executable (and thus the usual static link of these symbols) exists.
---
 rust/Cargo.toml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/rust/Cargo.toml b/rust/Cargo.toml
index deaa12c..aaf2a36 100644
--- a/rust/Cargo.toml
+++ b/rust/Cargo.toml
@@ -8,7 +8,11 @@ version = "0.1.0"
 edition = "2024"
 
 [lib]
-crate-type = ["staticlib"]
+# `staticlib` is linked into final Lean executables. `cdylib` additionally
+# builds a position-independent shared object exporting the raw `rs_blake3_*`
+# symbols, so they can be loaded at runtime — e.g. by Lean's native evaluator
+# for `native_decide` proofs elaborated before any executable is linked.
+crate-type = ["staticlib", "cdylib"]
 
 [dependencies]
 blake3 = "1.8.4"

From 730f910a59fe883cd71454bf186c7726a0c2d0d1 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 4 Aug 2026 14:11:53 -0400
Subject: [PATCH 2/2] lake: add blake3_rs_shared target for the cdylib output

Expose the shared-library (cdylib) build product as its own target so
downstream packages can fetch it directly, rather than reaching into this
package's rust/target directory to build and locate it themselves. Used to
supply the raw rs_blake3_* symbols to Lean's native evaluator at
elaboration time (native_decide).
---
 lakefile.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/lakefile.lean b/lakefile.lean
index 4a03a08..6d927e6 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -87,3 +87,12 @@ lean_lib Blake3Rust where
   roots := #[`Blake3.Rust]
   moreLinkObjs := #[blake3_rs]
 
+/-- The `blake3-rs` shared library. Produced by the same `cargo build` as
+`blake3_rs`; this target selects the `cdylib` output for downstream tooling
+that loads the raw `rs_blake3_*` symbols at runtime rather than linking them
+statically — e.g. supplying the BLAKE3 backend to Lean's native evaluator for
+`native_decide` proofs. -/
+target blake3_rs_shared pkg : System.FilePath := do
+  proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir / "rust" } (quiet := true)
+  inputBinFile $ pkg.dir / "rust" / "target" / "release" / nameToSharedLib "blake3_rs"
+