From 2df4f9e3c60115ac074ce7ece3812d075a79fbaa Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Tue, 4 Aug 2026 15:57:58 +0000 Subject: [PATCH 1/2] ffi: replace native-decide C shim with Rust dynlib --- Cargo.lock | 12 +- Cargo.toml | 1 + crates/ffi-dyn/Cargo.toml | 18 +++ crates/ffi-dyn/src/lib.rs | 179 ++++++++++++++++++++++++++++++ crates/ffi/blake3_native_decide.c | 108 ------------------ docs/ffi.md | 14 ++- lakefile.lean | 37 ++---- 7 files changed, 230 insertions(+), 139 deletions(-) create mode 100644 crates/ffi-dyn/Cargo.toml create mode 100644 crates/ffi-dyn/src/lib.rs delete mode 100644 crates/ffi/blake3_native_decide.c diff --git a/Cargo.lock b/Cargo.lock index 9bcffa277..5b4fb9687 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -243,9 +243,9 @@ checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3" [[package]] name = "blake3" -version = "1.8.5" +version = "1.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0aa83c34e62843d924f905e0f5c866eb1dd6545fc4d719e803d9ba6030371fce" +checksum = "4d2d5991425dfd0785aed03aedcf0b321d61975c9b5b3689c774a2610ae0b51e" dependencies = [ "arrayref", "arrayvec", @@ -1839,6 +1839,14 @@ dependencies = [ "rustc-hash", ] +[[package]] +name = "ix-rs-dyn" +version = "0.1.0" +dependencies = [ + "blake3", + "lean-ffi", +] + [[package]] name = "ixon" 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..7a3660d62 --- /dev/null +++ b/crates/ffi-dyn/Cargo.toml @@ -0,0 +1,18 @@ +[package] +name = "ix-rs-dyn" +version.workspace = true +edition.workspace = true +license.workspace = true + +[lib] +name = "ix_rs_dyn" +crate-type = ["cdylib"] + +[dependencies] +# Match the audited Blake3.lean Rust backend exactly. The workspace's `1.8.4` +# requirement is semver-compatible with newer patch releases and is not a pin. +blake3 = "=1.8.4" +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..7f4641133 --- /dev/null +++ b/crates/ffi-dyn/src/lib.rs @@ -0,0 +1,179 @@ +//! Minimal Lean runtime support loaded while elaborating `IxTcVerify`. +//! +//! Lean's native evaluator calls the boxed entry points generated for opaque +//! `@[extern]` declarations. Normal executables receive those wrappers and the +//! raw Rust FFI symbols at final link time, which is too late for +//! `native_decide`. This crate exports both layers from one loadable artifact. + +use std::sync::LazyLock; + +use lean_ffi::object::{ + ExternalClass, LeanBorrowed, LeanByteArray, LeanExternal, LeanOwned, LeanRef, +}; + +static HASHER_CLASS: LazyLock = + LazyLock::new(ExternalClass::register_with_drop::); + +fn blake3_init() -> LeanExternal { + LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new()) +} + +fn blake3_init_keyed(key: &[u8]) -> LeanExternal { + let key: &[u8; 32] = key.try_into().expect("key must be 32 bytes"); + LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new_keyed(key)) +} + +fn blake3_init_derive_key( + context: &[u8], +) -> LeanExternal { + let context = + std::str::from_utf8(context).expect("context must be valid UTF-8"); + LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new_derive_key(context)) +} + +fn blake3_update( + mut hasher: LeanExternal, + input: &[u8], +) -> LeanExternal { + if let Some(inner) = hasher.get_mut() { + inner.update(input); + hasher + } else { + let mut inner = hasher.get().clone(); + inner.update(input); + LeanExternal::alloc(&HASHER_CLASS, inner) + } +} + +fn blake3_finalize( + hasher: &LeanExternal, + length: usize, +) -> LeanByteArray { + let mut output = vec![0; length]; + hasher.get().finalize_xof().fill(&mut output); + LeanByteArray::from_bytes(&output) +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_init() -> LeanExternal { + blake3_init() +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_init_keyed( + key: LeanByteArray>, +) -> LeanExternal { + blake3_init_keyed(key.as_bytes()) +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_init_derive_key( + context: LeanByteArray>, +) -> LeanExternal { + blake3_init_derive_key(context.as_bytes()) +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_hasher_update( + hasher: LeanExternal, + input: LeanByteArray>, +) -> LeanExternal { + blake3_update(hasher, input.as_bytes()) +} + +#[unsafe(no_mangle)] +pub extern "C" fn rs_blake3_hasher_finalize( + hasher: LeanExternal, + length: usize, +) -> LeanByteArray { + blake3_finalize(&hasher, length) +} + +#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherInit___boxed")] +pub extern "C" fn boxed_blake3_init( + _unit: LeanOwned, +) -> LeanExternal { + blake3_init() +} + +#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherInitKeyed___boxed")] +pub extern "C" fn boxed_blake3_init_keyed( + key: LeanByteArray, +) -> LeanExternal { + blake3_init_keyed(key.as_bytes()) +} + +#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherInitDeriveKey___boxed")] +pub extern "C" fn boxed_blake3_init_derive_key( + context: LeanByteArray, +) -> LeanExternal { + blake3_init_derive_key(context.as_bytes()) +} + +#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherUpdate___boxed")] +pub extern "C" fn boxed_blake3_update( + hasher: LeanExternal, + input: LeanByteArray, +) -> LeanExternal { + blake3_update(hasher, input.as_bytes()) +} + +#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherFinalize___boxed")] +pub extern "C" fn boxed_blake3_finalize( + hasher: LeanExternal, + length: LeanOwned, +) -> LeanByteArray { + blake3_finalize(&hasher, length.unbox_usize_obj()) +} + +#[unsafe(no_mangle)] +pub extern "C" fn c_u16_to_le_bytes(value: u16) -> LeanByteArray { + LeanByteArray::from_bytes(&value.to_le_bytes()) +} + +#[unsafe(no_mangle)] +pub extern "C" fn c_u32_to_le_bytes(value: u32) -> LeanByteArray { + LeanByteArray::from_bytes(&value.to_le_bytes()) +} + +#[unsafe(no_mangle)] +pub extern "C" fn c_u64_to_le_bytes(value: u64) -> LeanByteArray { + LeanByteArray::from_bytes(&value.to_le_bytes()) +} + +#[unsafe(no_mangle)] +pub extern "C" fn c_usize_to_le_bytes( + value: usize, +) -> LeanByteArray { + LeanByteArray::from_bytes(&value.to_le_bytes()) +} + +#[unsafe(export_name = "lp_ix_UInt16_toLEBytes___boxed")] +pub extern "C" fn boxed_u16_to_le_bytes( + value: LeanOwned, +) -> LeanByteArray { + let value = + u16::try_from(value.unbox_usize()).expect("UInt16 value must fit in u16"); + c_u16_to_le_bytes(value) +} + +#[unsafe(export_name = "lp_ix_UInt32_toLEBytes___boxed")] +pub extern "C" fn boxed_u32_to_le_bytes( + value: LeanOwned, +) -> LeanByteArray { + c_u32_to_le_bytes(value.unbox_u32()) +} + +#[unsafe(export_name = "lp_ix_UInt64_toLEBytes___boxed")] +pub extern "C" fn boxed_u64_to_le_bytes( + value: LeanOwned, +) -> LeanByteArray { + c_u64_to_le_bytes(value.unbox_u64()) +} + +#[unsafe(export_name = "lp_ix_USize_toLEBytes___boxed")] +pub extern "C" fn boxed_usize_to_le_bytes( + value: LeanOwned, +) -> LeanByteArray { + c_usize_to_le_bytes(value.unbox_usize_obj()) +} 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..c8bf5dd9a 100644 --- a/docs/ffi.md +++ b/docs/ffi.md @@ -21,10 +21,22 @@ 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. The `ix-rs-dyn` crate builds the small `ix_rs_dyn` dynamic +library loaded by the `IxTcVerify` Lake target for that purpose. + +The dynamic library contains only the BLAKE3 and unsigned-integer operations +needed by verification fixtures. It exports both the raw `@[extern]` entry +points and the boxed entry points used by Lean's native evaluator. When an +opaque external operation becomes reachable from a new elaboration-time +computation, its boxed ABI must be added and tested there as well. + ## 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/lakefile.lean b/lakefile.lean index 16d2690cb..98adcfc3b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -155,36 +155,17 @@ 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" +/-- Build the minimal Rust dynlib that supplies raw and boxed FFI symbols to +Lean's native evaluator while `IxTcVerify` is being elaborated. -/ +target ix_rs_dyn pkg : Dynlib := do proc { cmd := "cargo" - args := #["rustc", "--release", "--", "--crate-type", "cdylib", - "-C", "extra-filename="] - cwd := blake3Pkg.dir / "rust" + args := #["build", "--release", "-p", "ix-rs-dyn"] + cwd := pkg.dir } (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] #[] + let dynlib ← inputBinFile <| pkg.dir / "target" / "release" / + nameToSharedLib "ix_rs_dyn" + dynlib.mapM fun path => pure {path, name := "ix_rs_dyn"} /- Formal verification of `Ix.Tc` against the lean4lean `Theory` spec. Non-default: `lake build ix` never @@ -202,7 +183,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_rs_dyn] end IxTcVerify From b8d66c616e67ebaec7fc131fb86640d7f29a5d9c Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Tue, 4 Aug 2026 13:55:57 -0400 Subject: [PATCH 2/2] ffi: supply native-decide FFI from Lean's own objects, not a shim crate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the `ix-rs-dyn` crate with a Lake target that assembles the elaboration-time dynlib from artifacts that already exist, so no FFI ABI is mirrored by hand: - Boxed entry points come from Lean's generated objects for the declaring modules (`Blake3`, `Blake3.Rust`, `Ix.Unsigned`), fetched via each module's `oExport` facet — the same code linked into normal executables. - Raw symbols come from the `blake3_rs` and `ix-ffi` `cdylib` outputs, recorded as load-time dependencies by absolute path (no `LD_LIBRARY_PATH`). The toolchain's `libgmp.a` is folded in to satisfy `ix-ffi`'s Nat bridge. This drops the duplicated BLAKE3 backend and its independent `=1.8.4` pin (restoring blake3 1.8.5 in Cargo.lock), and removes the `ix-rs-dyn` crate. `ix-ffi` and the pinned Blake3 dependency now build a `cdylib` alongside their staticlib. --- Cargo.lock | 19 ++-- crates/ffi-dyn/Cargo.toml | 12 +-- crates/ffi-dyn/src/lib.rs | 186 ++------------------------------------ docs/ffi.md | 29 ++++-- lake-manifest.json | 4 +- lakefile.lean | 57 +++++++++--- 6 files changed, 91 insertions(+), 216 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 5b4fb9687..85b69a086 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -243,9 +243,9 @@ checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3" [[package]] name = "blake3" -version = "1.8.4" +version = "1.8.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4d2d5991425dfd0785aed03aedcf0b321d61975c9b5b3689c774a2610ae0b51e" +checksum = "0aa83c34e62843d924f905e0f5c866eb1dd6545fc4d719e803d9ba6030371fce" dependencies = [ "arrayref", "arrayvec", @@ -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" @@ -1839,14 +1846,6 @@ dependencies = [ "rustc-hash", ] -[[package]] -name = "ix-rs-dyn" -version = "0.1.0" -dependencies = [ - "blake3", - "lean-ffi", -] - [[package]] name = "ixon" version = "0.1.0" diff --git a/crates/ffi-dyn/Cargo.toml b/crates/ffi-dyn/Cargo.toml index 7a3660d62..5496d12f7 100644 --- a/crates/ffi-dyn/Cargo.toml +++ b/crates/ffi-dyn/Cargo.toml @@ -1,18 +1,18 @@ [package] -name = "ix-rs-dyn" +name = "ix-ffi-dyn" version.workspace = true edition.workspace = true license.workspace = true [lib] -name = "ix_rs_dyn" +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] -# Match the audited Blake3.lean Rust backend exactly. The workspace's `1.8.4` -# requirement is semver-compatible with newer patch releases and is not a pin. -blake3 = "=1.8.4" -lean-ffi.workspace = true +lean-ffi = { workspace = true } [lints] workspace = true diff --git a/crates/ffi-dyn/src/lib.rs b/crates/ffi-dyn/src/lib.rs index 7f4641133..8a7461d5a 100644 --- a/crates/ffi-dyn/src/lib.rs +++ b/crates/ffi-dyn/src/lib.rs @@ -1,179 +1,11 @@ -//! Minimal Lean runtime support loaded while elaborating `IxTcVerify`. +//! 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. //! -//! Lean's native evaluator calls the boxed entry points generated for opaque -//! `@[extern]` declarations. Normal executables receive those wrappers and the -//! raw Rust FFI symbols at final link time, which is too late for -//! `native_decide`. This crate exports both layers from one loadable artifact. +//! 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. -use std::sync::LazyLock; - -use lean_ffi::object::{ - ExternalClass, LeanBorrowed, LeanByteArray, LeanExternal, LeanOwned, LeanRef, -}; - -static HASHER_CLASS: LazyLock = - LazyLock::new(ExternalClass::register_with_drop::); - -fn blake3_init() -> LeanExternal { - LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new()) -} - -fn blake3_init_keyed(key: &[u8]) -> LeanExternal { - let key: &[u8; 32] = key.try_into().expect("key must be 32 bytes"); - LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new_keyed(key)) -} - -fn blake3_init_derive_key( - context: &[u8], -) -> LeanExternal { - let context = - std::str::from_utf8(context).expect("context must be valid UTF-8"); - LeanExternal::alloc(&HASHER_CLASS, blake3::Hasher::new_derive_key(context)) -} - -fn blake3_update( - mut hasher: LeanExternal, - input: &[u8], -) -> LeanExternal { - if let Some(inner) = hasher.get_mut() { - inner.update(input); - hasher - } else { - let mut inner = hasher.get().clone(); - inner.update(input); - LeanExternal::alloc(&HASHER_CLASS, inner) - } -} - -fn blake3_finalize( - hasher: &LeanExternal, - length: usize, -) -> LeanByteArray { - let mut output = vec![0; length]; - hasher.get().finalize_xof().fill(&mut output); - LeanByteArray::from_bytes(&output) -} - -#[unsafe(no_mangle)] -pub extern "C" fn rs_blake3_init() -> LeanExternal { - blake3_init() -} - -#[unsafe(no_mangle)] -pub extern "C" fn rs_blake3_init_keyed( - key: LeanByteArray>, -) -> LeanExternal { - blake3_init_keyed(key.as_bytes()) -} - -#[unsafe(no_mangle)] -pub extern "C" fn rs_blake3_init_derive_key( - context: LeanByteArray>, -) -> LeanExternal { - blake3_init_derive_key(context.as_bytes()) -} - -#[unsafe(no_mangle)] -pub extern "C" fn rs_blake3_hasher_update( - hasher: LeanExternal, - input: LeanByteArray>, -) -> LeanExternal { - blake3_update(hasher, input.as_bytes()) -} - -#[unsafe(no_mangle)] -pub extern "C" fn rs_blake3_hasher_finalize( - hasher: LeanExternal, - length: usize, -) -> LeanByteArray { - blake3_finalize(&hasher, length) -} - -#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherInit___boxed")] -pub extern "C" fn boxed_blake3_init( - _unit: LeanOwned, -) -> LeanExternal { - blake3_init() -} - -#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherInitKeyed___boxed")] -pub extern "C" fn boxed_blake3_init_keyed( - key: LeanByteArray, -) -> LeanExternal { - blake3_init_keyed(key.as_bytes()) -} - -#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherInitDeriveKey___boxed")] -pub extern "C" fn boxed_blake3_init_derive_key( - context: LeanByteArray, -) -> LeanExternal { - blake3_init_derive_key(context.as_bytes()) -} - -#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherUpdate___boxed")] -pub extern "C" fn boxed_blake3_update( - hasher: LeanExternal, - input: LeanByteArray, -) -> LeanExternal { - blake3_update(hasher, input.as_bytes()) -} - -#[unsafe(export_name = "lp_Blake3_Blake3_Rust_hasherFinalize___boxed")] -pub extern "C" fn boxed_blake3_finalize( - hasher: LeanExternal, - length: LeanOwned, -) -> LeanByteArray { - blake3_finalize(&hasher, length.unbox_usize_obj()) -} - -#[unsafe(no_mangle)] -pub extern "C" fn c_u16_to_le_bytes(value: u16) -> LeanByteArray { - LeanByteArray::from_bytes(&value.to_le_bytes()) -} - -#[unsafe(no_mangle)] -pub extern "C" fn c_u32_to_le_bytes(value: u32) -> LeanByteArray { - LeanByteArray::from_bytes(&value.to_le_bytes()) -} - -#[unsafe(no_mangle)] -pub extern "C" fn c_u64_to_le_bytes(value: u64) -> LeanByteArray { - LeanByteArray::from_bytes(&value.to_le_bytes()) -} - -#[unsafe(no_mangle)] -pub extern "C" fn c_usize_to_le_bytes( - value: usize, -) -> LeanByteArray { - LeanByteArray::from_bytes(&value.to_le_bytes()) -} - -#[unsafe(export_name = "lp_ix_UInt16_toLEBytes___boxed")] -pub extern "C" fn boxed_u16_to_le_bytes( - value: LeanOwned, -) -> LeanByteArray { - let value = - u16::try_from(value.unbox_usize()).expect("UInt16 value must fit in u16"); - c_u16_to_le_bytes(value) -} - -#[unsafe(export_name = "lp_ix_UInt32_toLEBytes___boxed")] -pub extern "C" fn boxed_u32_to_le_bytes( - value: LeanOwned, -) -> LeanByteArray { - c_u32_to_le_bytes(value.unbox_u32()) -} - -#[unsafe(export_name = "lp_ix_UInt64_toLEBytes___boxed")] -pub extern "C" fn boxed_u64_to_le_bytes( - value: LeanOwned, -) -> LeanByteArray { - c_u64_to_le_bytes(value.unbox_u64()) -} - -#[unsafe(export_name = "lp_ix_USize_toLEBytes___boxed")] -pub extern "C" fn boxed_usize_to_le_bytes( - value: LeanOwned, -) -> LeanByteArray { - c_usize_to_le_bytes(value.unbox_usize_obj()) -} +#[path = "../../ffi/src/unsigned.rs"] +mod unsigned; diff --git a/docs/ffi.md b/docs/ffi.md index c8bf5dd9a..cc558296c 100644 --- a/docs/ffi.md +++ b/docs/ffi.md @@ -25,14 +25,27 @@ By convention, names of external Rust functions start with `rs_`. 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. The `ix-rs-dyn` crate builds the small `ix_rs_dyn` dynamic -library loaded by the `IxTcVerify` Lake target for that purpose. - -The dynamic library contains only the BLAKE3 and unsigned-integer operations -needed by verification fixtures. It exports both the raw `@[extern]` entry -points and the boxed entry points used by Lean's native evaluator. When an -opaque external operation becomes reachable from a new elaboration-time -computation, its boxed ABI must be added and tested there as well. +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 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 98adcfc3b..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,17 +164,39 @@ end Benchmarks section IxTcVerify -/-- Build the minimal Rust dynlib that supplies raw and boxed FFI symbols to -Lean's native evaluator while `IxTcVerify` is being elaborated. -/ -target ix_rs_dyn pkg : Dynlib := do - proc { - cmd := "cargo" - args := #["build", "--release", "-p", "ix-rs-dyn"] - cwd := pkg.dir - } (quiet := true) - let dynlib ← inputBinFile <| pkg.dir / "target" / "release" / - nameToSharedLib "ix_rs_dyn" - dynlib.mapM fun path => pure {path, name := "ix_rs_dyn"} +/-- 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 @@ -183,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 := #[ix_rs_dyn] + dynlibs := #[ix_native_decide_dynlib] end IxTcVerify