diff --git a/Cargo.lock b/Cargo.lock index 9bcffa277..85b69a086 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1820,6 +1820,13 @@ dependencies = [ "tracing-texray", ] +[[package]] +name = "ix-ffi-dyn" +version = "0.1.0" +dependencies = [ + "lean-ffi", +] + [[package]] name = "ix-kernel" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index b4cc3788a..7f313cb37 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,6 +5,7 @@ members = [ "crates/common", "crates/compile", "crates/ffi", + "crates/ffi-dyn", "crates/ixvm-codegen", "crates/ixon", "crates/kernel", diff --git a/crates/ffi-dyn/Cargo.toml b/crates/ffi-dyn/Cargo.toml new file mode 100644 index 000000000..5496d12f7 --- /dev/null +++ b/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 diff --git a/crates/ffi-dyn/src/lib.rs b/crates/ffi-dyn/src/lib.rs new file mode 100644 index 000000000..8a7461d5a --- /dev/null +++ b/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; diff --git a/crates/ffi/blake3_native_decide.c b/crates/ffi/blake3_native_decide.c deleted file mode 100644 index 52b52db00..000000000 --- a/crates/ffi/blake3_native_decide.c +++ /dev/null @@ -1,108 +0,0 @@ -/* - * Lean's native evaluator calls the boxed symbols generated for opaque - * extern declarations, while the pinned Blake3 Rust cdylib exports the raw - * rs_blake3_* ABI. Normal executables get these tiny adapters from the - * generated Blake3.Rust object. Verification modules are elaborated before - * executable linking, so Lake loads this equivalent shim for native_decide. - */ - -#include -#include - -extern lean_object *rs_blake3_init(lean_object *); -extern lean_object *rs_blake3_init_keyed(lean_object *); -extern lean_object *rs_blake3_init_derive_key(lean_object *); -extern lean_object *rs_blake3_hasher_update(lean_object *, lean_object *); -extern lean_object *rs_blake3_hasher_finalize(lean_object *, size_t); - -LEAN_EXPORT lean_object * -lp_Blake3_Blake3_Rust_hasherInit___boxed(lean_object *unit) { - return rs_blake3_init(unit); -} - -LEAN_EXPORT lean_object * -lp_Blake3_Blake3_Rust_hasherInitKeyed___boxed(lean_object *key) { - lean_object *result = rs_blake3_init_keyed(key); - lean_dec_ref(key); - return result; -} - -LEAN_EXPORT lean_object * -lp_Blake3_Blake3_Rust_hasherInitDeriveKey___boxed(lean_object *context) { - lean_object *result = rs_blake3_init_derive_key(context); - lean_dec_ref(context); - return result; -} - -LEAN_EXPORT lean_object * -lp_Blake3_Blake3_Rust_hasherUpdate___boxed(lean_object *hasher, - lean_object *bytes) { - lean_object *result = rs_blake3_hasher_update(hasher, bytes); - lean_dec_ref(bytes); - return result; -} - -LEAN_EXPORT lean_object * -lp_Blake3_Blake3_Rust_hasherFinalize___boxed(lean_object *hasher, - lean_object *length) { - size_t unboxed_length = lean_unbox_usize(length); - lean_dec(length); - return rs_blake3_hasher_finalize(hasher, unboxed_length); -} - -/* - * Ix.Unsigned normally receives these symbols from ix-ffi when a final Lean - * executable is linked. Library elaboration has no such executable, so - * native_decide needs an equivalent implementation in this loaded adapter. - * Keep the byte order explicit so this remains host-endianness independent. - */ -static lean_object *ix_alloc_le_bytes(uint64_t value, size_t width) { - lean_object *bytes = lean_alloc_sarray(1, width, width); - uint8_t *data = lean_sarray_cptr(bytes); - for (size_t index = 0; index < width; ++index) { - data[index] = (uint8_t)(value >> (8 * index)); - } - return bytes; -} - -LEAN_EXPORT lean_object *c_u16_to_le_bytes(uint16_t value) { - return ix_alloc_le_bytes((uint64_t)value, sizeof(uint16_t)); -} - -LEAN_EXPORT lean_object *c_u32_to_le_bytes(uint32_t value) { - return ix_alloc_le_bytes((uint64_t)value, sizeof(uint32_t)); -} - -LEAN_EXPORT lean_object *c_u64_to_le_bytes(uint64_t value) { - return ix_alloc_le_bytes(value, sizeof(uint64_t)); -} - -LEAN_EXPORT lean_object *c_usize_to_le_bytes(size_t value) { - return ix_alloc_le_bytes((uint64_t)value, sizeof(size_t)); -} - -LEAN_EXPORT lean_object * -lp_ix_UInt16_toLEBytes___boxed(lean_object *value) { - return c_u16_to_le_bytes((uint16_t)lean_unbox(value)); -} - -LEAN_EXPORT lean_object * -lp_ix_UInt32_toLEBytes___boxed(lean_object *value) { - uint32_t unboxed = lean_unbox_uint32(value); - lean_dec(value); - return c_u32_to_le_bytes(unboxed); -} - -LEAN_EXPORT lean_object * -lp_ix_UInt64_toLEBytes___boxed(lean_object *value) { - uint64_t unboxed = lean_unbox_uint64(value); - lean_dec_ref(value); - return c_u64_to_le_bytes(unboxed); -} - -LEAN_EXPORT lean_object * -lp_ix_USize_toLEBytes___boxed(lean_object *value) { - size_t unboxed = lean_unbox_usize(value); - lean_dec(value); - return c_usize_to_le_bytes(unboxed); -} diff --git a/docs/ffi.md b/docs/ffi.md index be64b72c9..cc558296c 100644 --- a/docs/ffi.md +++ b/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. - diff --git a/lake-manifest.json b/lake-manifest.json index 53d6469f5..4080aa994 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lakefile.lean b/lakefile.lean index 16d2690cb..65077fb0d 100644 --- a/lakefile.lean +++ b/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