ffi: replace native-decide C shim with Rust dynlib

Cargo.toml

@@ -5,6 +5,7 @@ members = [
   "crates/common",
   "crates/compile",
   "crates/ffi",
+  "crates/ffi-dyn",
   "crates/ixvm-codegen",
   "crates/ixon",
   "crates/kernel",

crates/ffi-dyn/Cargo.toml

@@ -0,0 +1,18 @@
+[package]
+name = "ix-ffi-dyn"
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+
+[lib]
+name = "ix_ffi_dyn"
+# A cdylib exporting only Ix's own raw `@[extern]` symbols that `native_decide`
+# reaches during elaboration. Kept minimal on purpose: loading the full `ix-ffi`
+# cdylib here would drag its whole dependency graph (and GMP) into every proof.
+crate-type = ["cdylib"]
+
+[dependencies]
+lean-ffi = { workspace = true }
+
+[lints]
+workspace = true

crates/ffi-dyn/src/lib.rs

@@ -0,0 +1,11 @@
+//! Loadable form of Ix's own raw `@[extern]` symbols for Lean's native
+//! evaluator during `native_decide` elaboration, before any executable links
+//! `ix-ffi` statically.
+//!
+//! The source is shared verbatim with `ix-ffi` (compiled into both), so there
+//! is a single implementation. Only the raw entry points need a loadable
+//! definition here; the boxed wrappers Lean actually calls come from its own
+//! generated objects for the declaring modules.
+
+#[path = "../../ffi/src/unsigned.rs"]
+mod unsigned;

docs/ffi.md

@@ -21,10 +21,35 @@ know about the state of Lean's reference counting mechanism.
 
 By convention, names of external Rust functions start with `rs_`.
 
+## Elaboration-time FFI
+
+Most Ix FFI is linked statically into final Lean executables. Proofs using
+`native_decide`, however, execute compiled Lean code while modules are still
+being elaborated, before any executable is linked. The native evaluator needs
+two symbol layers for each opaque `@[extern]` it reaches: the raw Rust symbol
+(e.g. `rs_blake3_init`, `c_u64_to_le_bytes`) and the boxed entry point Lean
+calls into it (e.g. `lp_Blake3_Blake3_Rust_hasherInit___boxed`).
+
+The `ix_native_decide_dynlib` Lake target assembles both layers from artifacts
+that already exist, so no ABI is mirrored by hand:
+
+- The boxed entry points are Lean's own generated objects for the declaring
+  modules (`Blake3`, `Blake3.Rust`, `Ix.Unsigned`) — the same code linked into
+  normal executables — fetched via each module's `oExport` facet.
+- The raw symbols come from `cdylib` outputs recorded as load-time
+  dependencies by absolute path (so no `LD_LIBRARY_PATH` is needed): Blake3's
+  `blake3_rs`, and the minimal `ix-ffi-dyn` crate for Ix's own externs. That
+  crate shares its source with `ix-ffi` but is kept separate so a
+  proof only loads the handful of symbols it needs, not `ix-ffi`'s whole
+  dependency graph.
+
+When an opaque external operation becomes reachable from a new
+elaboration-time computation, add its declaring module's object to the target
+(the raw symbol is already present if it lives in a linked cdylib).
+
 ## Linear API
 
 There is a deprecated API for passing mutable objects between Lean and Rust in `c/linear.h`.
 This code path is unused for now as the Rust FFI is designed to clone if mutation is needed.
 However, the `linear.h` file is well-documented in case we want to revisit it later for
 performance-critical applications.
-

lake-manifest.json

@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "rev": "c6db090374cb3c3c717691beb6cd18bb08936598",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7",
+   "inputRev": "c6db090374cb3c3c717691beb6cd18bb08936598",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",

lakefile.lean

@@ -8,7 +8,7 @@ require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e"
 
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "c6db090374cb3c3c717691beb6cd18bb08936598"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "v4.29.0"
@@ -77,6 +77,15 @@ target ix_rs_net pkg : FilePath := do
   proc { cmd := "cargo", args, cwd := pkg.dir } (quiet := true)
   inputBinFile $ pkg.dir / "target" / "release" / nameToStaticLib "ix_ffi"
 
+/-- The `ix-ffi-dyn` cdylib: Ix's own raw `@[extern]` symbols (currently the
+`toLEBytes` operations) as a small standalone shared library. Consumed by
+`ix_native_decide_dynlib`; kept separate from `ix-ffi` so proofs don't load
+that crate's full dependency graph. -/
+target ix_ffi_dyn pkg : FilePath := do
+  let args := #["build", "--release", "-p", "ix-ffi-dyn"]
+  proc { cmd := "cargo", args, cwd := pkg.dir } (quiet := true)
+  inputBinFile $ pkg.dir / "target" / "release" / nameToSharedLib "ix_ffi_dyn"
+
 end FFI
 
 @[default_target]
@@ -155,36 +164,39 @@ end Benchmarks
 
 section IxTcVerify
 
-/-- Native-decide fixture proofs execute the same pinned Rust BLAKE3 backend
-used by production address construction.  Build a loadable form of that exact
-backend for Lean's elaboration process. -/
-target blake3_rs_verify_cdylib : FilePath := do
-  let some blake3Pkg ← findPackageByName? `Blake3
-    | error "Blake3 dependency package is unavailable"
-  proc {
-    cmd := "cargo"
-    args := #["rustc", "--release", "--", "--crate-type", "cdylib",
-      "-C", "extra-filename="]
-    cwd := blake3Pkg.dir / "rust"
-  } (quiet := true)
-  inputBinFile <| blake3Pkg.dir / "rust" / "target" / "release" / "deps" /
-    nameToSharedLib "blake3_rs"
-
-/-- Boxed-symbol adapter loaded by Lean while elaborating native-decide
-proofs.  Its dependency is the exact Rust cdylib above. -/
-target blake3_rs_verify_dynlib pkg : Dynlib := do
-  let source ← inputTextFile <| pkg.dir / "crates" / "ffi" /
-    "blake3_native_decide.c"
-  let leanIncludeDir ← getLeanIncludeDir
-  let object ← buildO
-    (pkg.buildDir / "blake3_native_decide.o") source
-    #["-fPIC", "-I", leanIncludeDir.toString] #[] "cc" getLeanTrace
-  let rustDynlib ← blake3_rs_verify_cdylib.fetch
-  -- Passing the cdylib as a link object records its concrete artifact path in
-  -- the adapter.  Lean can therefore load it without relying on LD_LIBRARY_PATH.
-  buildSharedLib "blake3_native_decide_v4"
-    (pkg.buildDir / nameToSharedLib "blake3_native_decide_v4")
-    #[object, rustDynlib] #[]
+/-- Loadable FFI for Lean's native evaluator while `IxTcVerify` is elaborated.
+
+`native_decide` runs compiled Lean before any executable is linked, so for each
+opaque `@[extern]` it reaches, both symbol layers must be loadable up front:
+
+* the boxed entry point Lean calls (`lp_..._boxed`), taken from Lean's own
+  generated object for the declaring module, so no ABI is mirrored by hand; and
+* 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`. -/
+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"
+  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))
+  buildSharedLib "ix_native_decide"
+    (pkg.buildDir / nameToSharedLib "ix_native_decide")
+    (boxedObjs.push blake3Cdylib |>.push ixCdylib) #[]
 
 /- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec.
 Non-default: `lake build ix` never
@@ -202,7 +214,7 @@ lean_lib IxTcVerify where
   -- that executable is linked, after its modules have been elaborated.
   -- These native-decide proofs need the boxed FFI symbols while the library
   -- modules are being elaborated, so they must be supplied as a dynlib.
-  dynlibs := #[blake3_rs_verify_dynlib]
+  dynlibs := #[ix_native_decide_dynlib]
 
 end IxTcVerify