From a195ced7564b1c1cd2e8bae114ddb3e0cc1b5f50 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 19 Mar 2026 19:25:07 -0400 Subject: [PATCH 01/10] feat: Add typed reference API --- .gitignore | 7 +- README.md | 177 +++-- flake.nix | 8 +- src/lib.rs | 67 +- src/nat.rs | 27 +- src/object.rs | 1501 ++++++++++++++++++++++++------------------ test/.gitignore | 2 - test/Cargo.toml | 6 + test/Tests.lean | 1 + test/Tests/FFI.lean | 409 +++++++++++- test/Tests/Gen.lean | 26 + test/Tests/Main.lean | 5 +- test/lakefile.lean | 2 +- test/src/lib.rs | 1025 +++++++++++++++++++++++----- 14 files changed, 2368 insertions(+), 895 deletions(-) delete mode 100644 test/.gitignore create mode 100644 test/Tests.lean diff --git a/.gitignore b/.gitignore index 5de600b..7ffc9ea 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,9 @@ # Rust -/target +**/target + +# Lean +**/.lake # Nix -result +**/result .direnv/ diff --git a/README.md b/README.md index b363b1b..e9b79f0 100644 --- a/README.md +++ b/README.md @@ -1,52 +1,108 @@ # lean-ffi Rust bindings to the `lean.h` Lean C FFI, generated with [`rust-bindgen`](https://github.com/rust-lang/rust-bindgen). -Bindgen runs in `build.rs` and generates unsafe Rust functions that link to +Bindgen runs in `build.rs` and generates unsafe Rust functions that link to Lean's `lean.h` C library. This external module can then be found at `target/release/lean-ffi-/out/lean.rs`. -These bindings are then wrapped in a typed Rust API based on the underlying Lean type, -in order to make facilitate ergonomic handling of Lean objects in Rust. - -## `LeanObject` API - -The fundamental building block is `LeanObject`, a wrapper around an opaque -Lean value represented in Rust as `*const c_void`. This value is either a -pointer to a heap-allocated object or a tagged scalar (a raw value that fits -into one pointer's width, e.g. a `Bool` or small `Nat`). `LeanObject` is -then itself wrapped into Lean types such as `LeanCtor` for inductives, -`LeanArray` for arrays, etc. - -A `lean_domain_type!` macro is also defined to allow for easy construction -of arbitrary Lean object types, which can then be used directly in FFI -functions to disambiguate between other `LeanObject`s. Some examples can be found in the -[Ix project](https://github.com/argumentcomputer/ix/blob/main/src/lean.rs). -To construct custom data in Rust, the user can define their own constructor methods -using `LeanCtor` (e.g. [`PutResponse`](https://github.com/argumentcomputer/ix/blob/main/src/ffi/iroh.rs)). -It is possible to use `LeanObject` or `*const c_void` directly in an `extern "C" fn`, -but this is generally not recommended as internal Rust functions may pass in the wrong object -more easily, and any low-level constructors would not be hidden behind the -API boundary. To enforce this, the `From for LeanObject` trait is -implemented to get the underlying `LeanObject`, but creating a wrapper type -from a `LeanObject` requires an explicit constructor for clarity. - -A key concept in this design is that ownership of the data is transferred to -Lean, making it responsible for deallocation. If the data type is intended to be -used as a black box by Lean, `ExternalClass` is a useful abstraction. It -requires a function pointer for deallocation, meaning the Rust code must -provide a function that properly frees the object's memory by dropping it. -See [`KECCAK_CLASS`](https://github.com/argumentcomputer/ix/blob/main/src/ffi/keccak.rs) for an example. +These bindings are then wrapped in a typed Rust API that models Lean's +ownership conventions (`lean_obj_arg` vs `b_lean_obj_arg`) using Rust's +type system. -## Notes +## Ownership Model + +The core types are: + +- **`LeanOwned`** — An owned reference to a Lean object. `Drop` calls `lean_dec`, + `Clone` calls `lean_inc`. Not `Copy`. Corresponds to `lean_obj_arg` (input) and + `lean_obj_res` (output) in the C FFI. + +- **`LeanBorrowed<'a>`** — A borrowed reference. `Copy`, no `Drop`, lifetime-bounded. + Corresponds to `b_lean_obj_arg` in the C FFI. Used when Lean declares a parameter + with `@&`. + +- **`LeanRef`** — Trait implemented by both `LeanOwned` and `LeanBorrowed`, providing + shared read-only operations like `as_raw()`, `is_scalar()`, `tag()`, and unboxing + methods. + +Both are safe for persistent objects (`m_rc == 0`) — `lean_inc_ref` and `lean_dec_ref` +are no-ops when `m_rc == 0`. + +## Domain Types + +Domain types wrap the ownership types to provide type safety at FFI boundaries. +Built-in domain types include `LeanArray`, `LeanString`, `LeanCtor`, +`LeanList`, `LeanOption`, `LeanExcept`, `LeanIOResult`, `LeanProd`, +`LeanNat`, `LeanBool`, `LeanByteArray`, and `LeanExternal`. + +### Naming convention + +Domain types are prefixed with `Lean` to distinguish them from Lean-side type names +and to match the built-in types. For example, a Lean `Point` structure becomes +`LeanPoint` in Rust. + +### Defining custom domain types + +Use the `lean_domain_type!` macro to define newtypes for your Lean types: + +```rust +lean_ffi::lean_domain_type! { + /// Lean `Point` — structure Point where x : Nat; y : Nat + LeanPoint; + /// Lean `PutResponse` — structure PutResponse where message : String; hash : String + LeanPutResponse; +} +``` + +This generates a `#[repr(transparent)]` wrapper with `Clone`, conditional `Copy`, +`inner()`, `as_raw()`, `into_raw()`, and `From` impls. You can then add +accessor methods — readers are generic over `R: LeanRef` (work on both owned +and borrowed), constructors return `LeanOwned`: + +```rust +impl LeanPutResponse { + pub fn message(&self) -> LeanBorrowed<'_> { + self.as_ctor().get(0) // borrowed ref into the object, no lean_inc + } + pub fn hash(&self) -> LeanBorrowed<'_> { + self.as_ctor().get(1) + } +} + +impl LeanPutResponse { + pub fn mk(message: &str, hash: &str) -> Self { + let ctor = LeanCtor::alloc(0, 2, 0); + ctor.set(0, LeanString::new(message)); + ctor.set(1, LeanString::new(hash)); + Self::new(ctor.into()) + } +} +``` + +### FFI function signatures + +Use domain types in `extern "C"` function signatures. The ownership type parameter +tells Rust how to handle reference counting: + +```rust +// Lean: @[extern "process"] def process (xs : @& Array Nat) (n : Nat) : Array Nat +#[no_mangle] +extern "C" fn process( + xs: LeanArray>, // @& → borrowed, no lean_dec + n: LeanNat, // owned → lean_dec on drop +) -> LeanArray { // returned to Lean, no drop + // ... +} +``` -### Inductive Types +## Inductive Types and Field Layout Extra care must be taken when dealing with [inductive types](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#run-time-inductives) as the runtime memory layout of constructor fields may not match the declaration order in Lean. Fields are reordered into three groups: -1. Non-scalar fields (lean_object *), in declaration order +1. Non-scalar fields (`lean_object*`), in declaration order 2. `USize` fields, in declaration order 3. Other scalar fields, in decreasing order by size, then declaration order within each size @@ -59,35 +115,44 @@ structure Reorder where size : UInt64 ``` -would be laid out as [obj, size, flag] at runtime — the `UInt64` is placed +would be laid out as `[obj, size, flag]` at runtime — the `UInt64` is placed before the `Bool`. Trivial wrapper types (e.g. `Char` wraps `UInt32`) count as their underlying scalar type. -To avoid issues, define Lean structures with fields already in runtime order -(objects first, then scalars in decreasing size), so that declaration order -matches the reordered layout. +Use `LeanCtor` methods to access fields at the correct offsets: + +```rust +// 1 object field, scalars: u64 at offset 0, u8 (Bool) at offset 8 +let ctor = unsafe { LeanBorrowed::from_raw(ptr.as_raw()) }.as_ctor(); +let obj = ctor.get(0); // object field by index +let size = ctor.get_u64(1, 0); // u64 at scalar offset 0 (past 1 non-scalar field) +let flag = ctor.get_bool(1, 8); // bool at scalar offset 8 +``` + +## Notes + +### Rust panic behavior + +By default, Rust uses stack unwinding for panics. If a panic occurs in a Lean-to-Rust FFI function, the unwinding will try to cross the FFI boundary back into Lean. This is [undefined behavior](https://doc.rust-lang.org/stable/reference/panic.html#unwinding-across-ffi-boundaries). To avoid this, configure Rust to abort on panic in `Cargo.toml`: + +```toml +[profile.release] +panic = "abort" +``` ### Enum FFI convention Lean passes simple enums (inductives where all constructors have zero fields, e.g. `DefKind`, `QuotKind`) as **raw unboxed tag values** (`0`, `1`, `2`, ...) -across the FFI boundary, not as `lean_box(tag)`. To decode, use -`obj.as_ptr() as usize`; to build, use `LeanObject::from_raw(tag as *const c_void)`. -Do **not** use `box_usize`/`unbox_usize` for these — doing so will silently -corrupt the value. - -### Reference counting for reused objects - -When building a new Lean object, if you construct all fields from scratch (e.g. -`LeanString::new(...)`, `LeanByteArray::from_bytes(...)`), ownership is -straightforward — the freshly allocated objects start with rc=1 and Lean manages -them from there. - -However, if you take a Lean object received as a **borrowed** argument (`@&` in -Lean, `b_lean_obj_arg` in C) and store it directly into a new object via -`.set()`, you must call `.inc_ref()` on it first. Otherwise Lean will free the -original while the new object still references it. If you only read/decode the -argument into Rust types and then build fresh Lean objects, this does not apply. +across the FFI boundary, not as `lean_box(tag)`. Use `LeanOwned::from_enum_tag()` +and `LeanRef::as_enum_tag()` for these. + +### Persistent objects + +Module-level Lean definitions and objects in compact regions are persistent +(`m_rc == 0`). Both `lean_inc_ref` and `lean_dec_ref` are no-ops for persistent +objects, so `LeanOwned`, `LeanBorrowed`, `Clone`, and `Drop` all work correctly +without special handling. ### `lean_string_size` vs `lean_string_byte_size` diff --git a/flake.nix b/flake.nix index 6b4ecfc..7e66642 100644 --- a/flake.nix +++ b/flake.nix @@ -68,16 +68,9 @@ pkgs.libiconv ]; }; - cargoArtifacts = craneLib.buildDepsOnly craneArgs; - rustPkg = craneLib.buildPackage (craneArgs // { - inherit cargoArtifacts; cargoExtraArgs = "--locked --workspace"; - postInstall = '' - mkdir -p $out/lib - cp target/release/liblean_ffi_rs.a $out/lib/ - ''; }); # Lake test package @@ -122,6 +115,7 @@ packages = with pkgs; [ clang rustToolchain + rust-analyzer lean.lean-all # Includes Lean compiler, lake, stdlib, etc. ]; }; diff --git a/src/lib.rs b/src/lib.rs index b5c8074..416e943 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,4 +1,4 @@ -//! Low-level Lean FFI bindings and type-safe wrappers. +//! Low-level Lean FFI bindings and ownership-aware type-safe wrappers. //! //! The `include` submodule contains auto-generated bindings from `lean.h` via //! bindgen. Higher-level helpers are in `object` and `nat`. @@ -42,30 +42,73 @@ pub fn safe_cstring(s: &str) -> CString { /// Must only be used as a `lean_external_foreach_fn` callback. pub unsafe extern "C" fn noop_foreach(_: *mut c_void, _: *mut include::lean_object) {} -/// Generate a `#[repr(transparent)]` newtype over `LeanObject` for a specific -/// Lean type, with `Deref`, `From`, and a `new` constructor. +/// Generate a `#[repr(transparent)]` newtype over a `LeanRef` type parameter +/// for a specific Lean type, with Clone, conditional Copy, from_raw, into_raw, and From impls. +/// +/// # Naming convention +/// +/// Domain types should be prefixed with `Lean` to distinguish them from Lean-side types +/// and to match the built-in types (`LeanArray`, `LeanString`, `LeanNat`, etc.). +/// For example, a Lean `Point` structure becomes `LeanPoint` in Rust: +/// +/// ```ignore +/// lean_domain_type! { +/// /// Lean `Point` — structure Point where x : Nat; y : Nat +/// LeanPoint; +/// } +/// ``` #[macro_export] macro_rules! lean_domain_type { ($($(#[$meta:meta])* $name:ident;)*) => {$( $(#[$meta])* - #[derive(Clone, Copy)] #[repr(transparent)] - pub struct $name($crate::object::LeanObject); + pub struct $name(R); + + impl Clone for $name { + #[inline] + fn clone(&self) -> Self { Self(self.0.clone()) } + } + + impl Copy for $name {} - impl std::ops::Deref for $name { - type Target = $crate::object::LeanObject; + impl $name { + /// Get the inner reference. #[inline] - fn deref(&self) -> &$crate::object::LeanObject { &self.0 } + pub fn inner(&self) -> &R { &self.0 } + + /// Get the raw lean_object pointer. + #[inline] + pub fn as_raw(&self) -> *mut $crate::include::lean_object { self.0.as_raw() } + + /// View this object as a `LeanCtor` for field access. + #[inline] + pub fn as_ctor(&self) -> $crate::object::LeanCtor<$crate::object::LeanBorrowed<'_>> { + unsafe { $crate::object::LeanBorrowed::from_raw(self.0.as_raw()) }.as_ctor() + } } - impl From<$name> for $crate::object::LeanObject { + impl $name<$crate::object::LeanOwned> { + /// Wrap an owned `LeanOwned` value. #[inline] - fn from(x: $name) -> Self { x.0 } + pub fn new(obj: $crate::object::LeanOwned) -> Self { Self(obj) } + + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut $crate::include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr + } } - impl $name { + impl From<$name<$crate::object::LeanOwned>> for $crate::object::LeanOwned { #[inline] - pub fn new(obj: $crate::object::LeanObject) -> Self { Self(obj) } + fn from(x: $name<$crate::object::LeanOwned>) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + unsafe { $crate::object::LeanOwned::from_raw(ptr) } + } } )*}; } + diff --git a/src/nat.rs b/src/nat.rs index 07d4da3..4a005cf 100644 --- a/src/nat.rs +++ b/src/nat.rs @@ -9,7 +9,7 @@ use std::mem::MaybeUninit; use num_bigint::BigUint; -use crate::object::{LeanNat, LeanObject}; +use crate::object::{LeanNat, LeanOwned, LeanRef}; /// Arbitrary-precision natural number, wrapping `BigUint`. #[derive(Hash, PartialEq, Eq, Debug, Clone, PartialOrd, Ord)] @@ -36,15 +36,15 @@ impl Nat { u64::try_from(&self.0).ok() } - /// Decode a `Nat` from a `LeanObject`. Handles both scalar (unboxed) + /// Decode a `Nat` from any Lean reference. Handles both scalar (unboxed) /// and heap-allocated (GMP `mpz_object`) representations. - pub fn from_obj(obj: LeanObject) -> Nat { + pub fn from_obj(obj: &impl LeanRef) -> Nat { if obj.is_scalar() { let u = obj.unbox_usize(); Nat(BigUint::from_bytes_le(&u.to_le_bytes())) } else { // Heap-allocated big integer (mpz_object) - let mpz: &MpzObject = unsafe { &*obj.as_ptr().cast() }; + let mpz: &MpzObject = unsafe { &*obj.as_raw().cast() }; Nat(mpz.m_value.to_biguint()) } } @@ -59,16 +59,16 @@ impl Nat { self.0.to_bytes_le() } - /// Convert this `Nat` into a Lean `Nat` object. - pub fn to_lean(&self) -> LeanNat { + /// Convert this `Nat` into a Lean `Nat` object (always owned). + pub fn to_lean(&self) -> LeanNat { // Try to get as u64 first if let Some(val) = self.to_u64() { // For small values that fit in a boxed scalar (max value is usize::MAX >> 1) if val <= (usize::MAX >> 1) as u64 { #[allow(clippy::cast_possible_truncation)] - return LeanNat::new(LeanObject::box_usize(val as usize)); + return LeanNat::new(LeanOwned::box_usize(val as usize)); } - return LeanNat::new(LeanObject::from_nat_u64(val)); + return LeanNat::new(LeanOwned::from_nat_u64(val)); } // For values larger than u64, convert to limbs and use GMP let bytes = self.to_le_bytes(); @@ -149,20 +149,19 @@ unsafe extern "C" { } /// Create a Lean `Nat` from a little-endian array of u64 limbs. -/// Replaces the C function `c_lean_nat_from_limbs` from `ixon_ffi.c`. /// # Safety /// `limbs` must be valid for reading `num_limbs` elements. -pub unsafe fn lean_nat_from_limbs(num_limbs: usize, limbs: *const u64) -> LeanObject { +pub unsafe fn lean_nat_from_limbs(num_limbs: usize, limbs: *const u64) -> LeanOwned { if num_limbs == 0 { - return LeanObject::box_usize(0); + return LeanOwned::box_usize(0); } let first = unsafe { *limbs }; if num_limbs == 1 && first <= LEAN_MAX_SMALL_NAT { #[allow(clippy::cast_possible_truncation)] // only targets 64-bit - return LeanObject::box_usize(first as usize); + return LeanOwned::box_usize(first as usize); } if num_limbs == 1 { - return unsafe { LeanObject::from_lean_ptr(lean_uint64_to_nat(first)) }; + return unsafe { LeanOwned::from_raw(lean_uint64_to_nat(first)) }; } // Multi-limb: use GMP unsafe { @@ -174,6 +173,6 @@ pub unsafe fn lean_nat_from_limbs(num_limbs: usize, limbs: *const u64) -> LeanOb // lean_alloc_mpz deep-copies; we must free the original let result = lean_alloc_mpz(value.as_mut_ptr()); mpz_clear(value.as_mut_ptr()); - LeanObject::from_raw(result) + LeanOwned::from_raw(result.cast()) } } diff --git a/src/object.rs b/src/object.rs index cf4c07e..b561e88 100644 --- a/src/object.rs +++ b/src/object.rs @@ -1,12 +1,14 @@ -//! Type-safe wrappers for Lean FFI object pointers. +//! Ownership-aware wrappers for Lean FFI object pointers. //! -//! Each wrapper is a `#[repr(transparent)]` `Copy` newtype over `*const c_void` -//! that asserts the correct Lean tag on construction and provides safe accessor -//! methods. Reference counting is left to Lean (no `Drop` impl). +//! The two core pointer types are: +//! - [`LeanOwned`]: Owned reference. `Drop` calls `lean_dec`, `Clone` calls `lean_inc`. Not `Copy`. +//! - [`LeanBorrowed`]: Borrowed reference. `Copy`, no `Drop`, lifetime-bounded. +//! +//! Domain types like [`LeanArray`], [`LeanCtor`], etc. are generic over `R: LeanRef`, +//! inheriting ownership semantics from the inner pointer type. -use std::ffi::c_void; use std::marker::PhantomData; -use std::ops::Deref; +use std::mem::ManuallyDrop; use crate::include; use crate::safe_cstring; @@ -22,209 +24,246 @@ const LEAN_TAG_EXTERNAL: u8 = 254; const IO_ERROR_USER_ERROR_TAG: u8 = 7; // ============================================================================= -// LeanObject — Untyped base wrapper +// LeanRef trait — shared interface for owned and borrowed pointers // ============================================================================= -/// Untyped wrapper around a raw Lean object pointer. -#[derive(Clone, Copy)] -#[repr(transparent)] -pub struct LeanObject(*const c_void); +/// Trait for types that hold a reference to a Lean object (owned or borrowed). +/// +/// Provides shared read-only operations. Implemented by [`LeanOwned`] and [`LeanBorrowed`]. +pub trait LeanRef: Clone { + /// Get the raw `*mut lean_object` pointer. + fn as_raw(&self) -> *mut include::lean_object; -impl LeanObject { - /// Wrap a raw pointer without any tag check. - /// - /// # Safety - /// The pointer must be a valid Lean object (or tagged scalar). + /// True if this is a tagged scalar (bit 0 set), not a heap pointer. #[inline] - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - Self(ptr) + fn is_scalar(&self) -> bool { + self.as_raw() as usize & 1 == 1 } - /// Wrap a `*mut lean_object` returned from a `lean_ffi` function. - /// - /// # Safety - /// The pointer must be a valid Lean object (or tagged scalar). + /// Return the object tag. Panics if the object is a scalar. #[inline] - pub unsafe fn from_lean_ptr(ptr: *mut include::lean_object) -> Self { - Self(ptr.cast()) + fn tag(&self) -> u8 { + assert!(!self.is_scalar(), "tag() called on scalar"); + #[allow(clippy::cast_possible_truncation)] + unsafe { + include::lean_obj_tag(self.as_raw()) as u8 + } } - /// Create a Lean `Nat` from a `u64` value. - /// - /// Small values are stored as tagged scalars; larger ones are heap-allocated - /// via the Lean runtime. + /// True if this is a persistent object (m_rc == 0). Persistent objects live + /// for the program's lifetime and must not have their reference count modified. + /// Objects in compact regions and values created at initialization time are persistent. #[inline] - pub fn from_nat_u64(n: u64) -> Self { - unsafe { Self::from_lean_ptr(include::lean_uint64_to_nat(n)) } + fn is_persistent(&self) -> bool { + !self.is_scalar() && unsafe { include::lean_is_persistent(self.as_raw()) } } + /// Produce an owned copy by incrementing the reference count. + /// Safe for persistent objects (m_rc == 0) — `lean_inc_ref` is a no-op when `m_rc == 0`. #[inline] - pub fn as_ptr(self) -> *const c_void { - self.0 + fn to_owned_ref(&self) -> LeanOwned { + let ptr = self.as_raw(); + if ptr as usize & 1 != 1 { + unsafe { include::lean_inc_ref(ptr) }; + } + LeanOwned(ptr) } + /// Unbox a tagged scalar pointer into a `usize`. #[inline] - pub fn as_mut_ptr(self) -> *mut c_void { - self.0 as *mut c_void + fn unbox_usize(&self) -> usize { + self.as_raw() as usize >> 1 } - /// True if this is a tagged scalar (bit 0 set). + /// Extract the raw tag value from a zero-field enum constructor. #[inline] - pub fn is_scalar(self) -> bool { - self.0 as usize & 1 == 1 + fn as_enum_tag(&self) -> usize { + self.as_raw() as usize } - /// Return the object tag. Panics if the object is a scalar. + /// Unbox a Lean `UInt64` object. #[inline] - pub fn tag(self) -> u8 { - assert!(!self.is_scalar(), "tag() called on scalar"); - #[allow(clippy::cast_possible_truncation)] - unsafe { - include::lean_obj_tag(self.0 as *mut _) as u8 - } + fn unbox_u64(&self) -> u64 { + unsafe { include::lean_unbox_uint64(self.as_raw()) } } + /// Unbox a Lean `UInt32` object. #[inline] - pub fn inc_ref(self) { - if !self.is_scalar() { - unsafe { include::lean_inc_ref(self.0 as *mut _) } - } + fn unbox_u32(&self) -> u32 { + unsafe { include::lean_unbox_uint32(self.as_raw()) } } + /// Unbox a Lean `Float` (f64) object. #[inline] - pub fn dec_ref(self) { - if !self.is_scalar() { - unsafe { include::lean_dec_ref(self.0 as *mut _) } - } + fn unbox_f64(&self) -> f64 { + unsafe { include::lean_unbox_float(self.as_raw()) } } - /// Create a `LeanObject` from a raw tag value for zero-field enum constructors. - /// Lean passes simple enums (all constructors have zero fields) as unboxed - /// tag values (0, 1, 2, ...) across FFI, not as `lean_box(tag)`. + /// Unbox a Lean `Float32` (f32) object. #[inline] - pub fn from_enum_tag(tag: usize) -> Self { - Self(tag as *const c_void) + fn unbox_f32(&self) -> f32 { + unsafe { include::lean_unbox_float32(self.as_raw()) } } - /// Extract the raw tag value from a zero-field enum constructor. - /// Inverse of `from_enum_tag`. + /// Unbox a Lean `USize` object (heap-allocated, not tagged scalar). #[inline] - pub fn as_enum_tag(self) -> usize { - self.0 as usize + fn unbox_usize_obj(&self) -> usize { + unsafe { include::lean_unbox_usize(self.as_raw()) } } +} - /// Box a `usize` into a tagged scalar pointer. - #[inline] - pub fn box_usize(n: usize) -> Self { - Self(((n << 1) | 1) as *const c_void) - } - /// Unbox a tagged scalar pointer into a `usize`. +// ============================================================================= +// LeanOwned — Owned Lean object pointer (RAII) +// ============================================================================= + +/// Owned reference to a Lean object. +/// +/// - `Drop` calls `lean_dec` (with scalar check). +/// - `Clone` calls `lean_inc`. +/// - **Not `Copy`** — ownership is linear. +/// +/// Corresponds to `lean_obj_arg` (received) and `lean_obj_res` (returned via repr(transparent)). +#[repr(transparent)] +pub struct LeanOwned(*mut include::lean_object); + +impl Drop for LeanOwned { #[inline] - pub fn unbox_usize(self) -> usize { - self.0 as usize >> 1 + fn drop(&mut self) { + if self.0 as usize & 1 != 1 { + unsafe { include::lean_dec_ref(self.0) }; + } } +} +impl Clone for LeanOwned { + /// Clone by incrementing the reference count. + /// Safe for persistent objects (m_rc == 0) — `lean_inc_ref` is a no-op when `m_rc == 0`. #[inline] - pub fn box_u64(n: u64) -> Self { - Self(unsafe { include::lean_box_uint64(n) }.cast()) + fn clone(&self) -> Self { + if self.0 as usize & 1 != 1 { + unsafe { include::lean_inc_ref(self.0) }; + } + LeanOwned(self.0) } +} +impl LeanRef for LeanOwned { #[inline] - pub fn unbox_u64(self) -> u64 { - unsafe { include::lean_unbox_uint64(self.0 as *mut _) } + fn as_raw(&self) -> *mut include::lean_object { + self.0 } +} - /// Box a `f64` into a Lean `Float` object via `lean_box_float`. +impl LeanOwned { + /// Wrap a raw pointer, taking ownership of the reference count. + /// + /// # Safety + /// The pointer must be a valid Lean object (or tagged scalar), and the + /// caller must be transferring one reference count to this wrapper. #[inline] - pub fn box_f64(v: f64) -> Self { - Self(unsafe { include::lean_box_float(v) }.cast()) + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + Self(ptr) } - /// Unbox a Lean `Float` object into a `f64` via `lean_unbox_float`. + /// Consume this wrapper without calling `lean_dec`. + /// + /// Use when transferring ownership back to Lean (returning `lean_obj_res`). #[inline] - pub fn unbox_f64(self) -> f64 { - unsafe { include::lean_unbox_float(self.0 as *mut _) } + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0; + std::mem::forget(self); + ptr } - /// Box a `f32` into a Lean `Float32` object via `lean_box_float32`. + /// Box a `usize` into a tagged scalar pointer. #[inline] - pub fn box_f32(v: f32) -> Self { - Self(unsafe { include::lean_box_float32(v) }.cast()) + pub fn box_usize(n: usize) -> Self { + Self(((n << 1) | 1) as *mut _) } - /// Unbox a Lean `Float32` object into a `f32` via `lean_unbox_float32`. + /// Create a `LeanOwned` from a raw tag value for zero-field enum constructors. #[inline] - pub fn unbox_f32(self) -> f32 { - unsafe { include::lean_unbox_float32(self.0 as *mut _) } + pub fn from_enum_tag(tag: usize) -> Self { + Self(tag as *mut _) } - /// Box a `usize` into a Lean object via `lean_box_usize` (heap-allocated). - /// - /// Unlike `box_usize` which creates a tagged scalar, this delegates to - /// `lean_box_usize` which allocates a proper Lean object. + /// Create a Lean `Nat` from a `u64` value. #[inline] - pub fn box_usize_obj(v: usize) -> Self { - Self(unsafe { include::lean_box_usize(v) }.cast()) + pub fn from_nat_u64(n: u64) -> Self { + unsafe { Self(include::lean_uint64_to_nat(n)) } } - /// Unbox a Lean object into a `usize` via `lean_unbox_usize`. + /// Box a `u32` into a Lean `UInt32` object. #[inline] - pub fn unbox_usize_obj(self) -> usize { - unsafe { include::lean_unbox_usize(self.0 as *mut _) } + pub fn box_u32(n: u32) -> Self { + Self(unsafe { include::lean_box_uint32(n) }) } - /// Interpret as a constructor object (tag 0–`LEAN_MAX_CTOR_TAG`). - /// - /// Debug-asserts the tag is in range. + /// Box a `u64` into a Lean `UInt64` object. #[inline] - pub fn as_ctor(self) -> LeanCtor { - debug_assert!(!self.is_scalar() && self.tag() <= LEAN_MAX_CTOR_TAG); - LeanCtor(self) + pub fn box_u64(n: u64) -> Self { + Self(unsafe { include::lean_box_uint64(n) }) } - /// Interpret as a `String` object (tag `LEAN_TAG_STRING`). - /// - /// Debug-asserts the tag is correct. + /// Box a `f64` into a Lean `Float` object. #[inline] - pub fn as_string(self) -> LeanString { - debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_STRING); - LeanString(self) + pub fn box_f64(v: f64) -> Self { + Self(unsafe { include::lean_box_float(v) }) } - /// Interpret as an `Array` object (tag `LEAN_TAG_ARRAY`). - /// - /// Debug-asserts the tag is correct. + /// Box a `f32` into a Lean `Float32` object. #[inline] - pub fn as_array(self) -> LeanArray { - debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_ARRAY); - LeanArray(self) + pub fn box_f32(v: f32) -> Self { + Self(unsafe { include::lean_box_float32(v) }) } - /// Interpret as a `List` (nil = scalar, cons = tag 1). - /// - /// Debug-asserts the tag is valid for a list. + /// Box a `usize` into a Lean object via `lean_box_usize` (heap-allocated). #[inline] - pub fn as_list(self) -> LeanList { - debug_assert!(self.is_scalar() || self.tag() == 1); - LeanList(self) + pub fn box_usize_obj(v: usize) -> Self { + Self(unsafe { include::lean_box_usize(v) }) } +} + +// ============================================================================= +// LeanBorrowed — Borrowed Lean object pointer +// ============================================================================= + +/// Borrowed reference to a Lean object. +/// +/// - `Copy + Clone` (trivial bitwise copy, no reference counting). +/// - **No `Drop`** — does not call `lean_dec`. +/// - Lifetime `'a` prevents the reference from outliving its source. +/// +/// Corresponds to `b_lean_obj_arg` (borrowed input) and `b_lean_obj_res` (borrowed output). +#[repr(transparent)] +pub struct LeanBorrowed<'a>(*mut include::lean_object, PhantomData<&'a ()>); - /// Interpret as a `ByteArray` object (tag `LEAN_TAG_SCALAR_ARRAY`). +impl<'a> Clone for LeanBorrowed<'a> { #[inline] - pub fn as_byte_array(self) -> LeanByteArray { - debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_SCALAR_ARRAY); - LeanByteArray(self) + fn clone(&self) -> Self { + *self } +} + +impl<'a> Copy for LeanBorrowed<'a> {} +impl<'a> LeanRef for LeanBorrowed<'a> { #[inline] - pub fn box_u32(n: u32) -> Self { - Self(unsafe { include::lean_box_uint32(n) }.cast()) + fn as_raw(&self) -> *mut include::lean_object { + self.0 } +} +impl<'a> LeanBorrowed<'a> { + /// Wrap a raw pointer as a borrowed reference. + /// + /// # Safety + /// The pointed-to object must remain alive for lifetime `'a`. + /// The caller must not call `lean_dec` on this pointer. #[inline] - pub fn unbox_u32(self) -> u32 { - unsafe { include::lean_unbox_uint32(self.0 as *mut _) } + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + Self(ptr, PhantomData) } } @@ -233,70 +272,102 @@ impl LeanObject { // ============================================================================= /// Typed wrapper for a Lean `Nat` (small = tagged scalar, big = heap `mpz_object`). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanNat(LeanObject); +pub struct LeanNat(R); -impl Deref for LeanNat { - type Target = LeanObject; +impl Clone for LeanNat { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl From for LeanObject { +impl Copy for LeanNat {} + +impl LeanNat { #[inline] - fn from(x: LeanNat) -> Self { - x.0 + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } +} + +impl LeanNat { + /// Wrap an owned `LeanOwned` as a `LeanNat`. + #[inline] + pub fn new(obj: LeanOwned) -> Self { + Self(obj) + } + + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr } } -impl LeanNat { - /// Wrap a raw `LeanObject` as a `LeanNat`. +impl<'a> LeanNat> { + /// Wrap a borrowed reference as a `LeanNat`. #[inline] - pub fn new(obj: LeanObject) -> Self { + pub fn new_borrowed(obj: LeanBorrowed<'a>) -> Self { Self(obj) } } +impl From> for LeanOwned { + #[inline] + fn from(x: LeanNat) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) + } +} + // ============================================================================= // LeanBool — Bool (unboxed scalar: false = 0, true = 1) // ============================================================================= /// Typed wrapper for a Lean `Bool` (always an unboxed scalar: false = 0, true = 1). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanBool(LeanObject); +pub struct LeanBool(R); -impl Deref for LeanBool { - type Target = LeanObject; +impl Clone for LeanBool { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl From for LeanObject { +impl Copy for LeanBool {} + +impl LeanBool { + #[inline] + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + + /// Decode to a Rust `bool`. #[inline] - fn from(x: LeanBool) -> Self { - x.0 + pub fn to_bool(&self) -> bool { + self.0.as_enum_tag() != 0 } } -impl LeanBool { - /// Wrap a raw `LeanObject` as a `LeanBool`. +impl LeanBool { + /// Wrap an owned `LeanOwned` as a `LeanBool`. #[inline] - pub fn new(obj: LeanObject) -> Self { + pub fn new(obj: LeanOwned) -> Self { Self(obj) } } -impl LeanBool { - /// Decode to a Rust `bool`. +impl From> for LeanOwned { #[inline] - pub fn to_bool(self) -> bool { - self.0.as_enum_tag() != 0 + fn from(x: LeanBool) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } @@ -305,82 +376,112 @@ impl LeanBool { // ============================================================================= /// Typed wrapper for a Lean `Array α` object (tag `LEAN_TAG_ARRAY`). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanArray(LeanObject); +pub struct LeanArray(R); -impl Deref for LeanArray { - type Target = LeanObject; +impl Clone for LeanArray { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl LeanArray { - /// Wrap a raw pointer, asserting it is an `Array` (tag `LEAN_TAG_ARRAY`). - /// - /// # Safety - /// The pointer must be a valid Lean `Array` object. - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - let obj = LeanObject(ptr); - debug_assert!(!obj.is_scalar() && obj.tag() == LEAN_TAG_ARRAY); - Self(obj) - } +impl Copy for LeanArray {} - /// Allocate a new array with `size` elements (capacity = size). - pub fn alloc(size: usize) -> Self { - let obj = unsafe { include::lean_alloc_array(size, size) }; - Self(LeanObject(obj.cast())) - } +impl LeanArray { + #[inline] + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } pub fn len(&self) -> usize { - unsafe { include::lean_array_size(self.0.as_ptr() as *mut _) } + unsafe { include::lean_array_size(self.0.as_raw()) } } pub fn is_empty(&self) -> bool { self.len() == 0 } - pub fn get(&self, i: usize) -> LeanObject { - LeanObject(unsafe { include::lean_array_get_core(self.0.as_ptr() as *mut _, i) }.cast()) + /// Get a borrowed reference to the `i`-th element. + pub fn get(&self, i: usize) -> LeanBorrowed<'_> { + LeanBorrowed( + unsafe { include::lean_array_get_core(self.0.as_raw(), i) }, + PhantomData, + ) } - pub fn set(&self, i: usize, val: impl Into) { - let val: LeanObject = val.into(); + /// Return a slice over the array elements as borrowed references. + pub fn data(&self) -> &[LeanBorrowed<'_>] { unsafe { - include::lean_array_set_core(self.0.as_ptr() as *mut _, i, val.as_ptr() as *mut _); + let cptr = include::lean_array_cptr(self.0.as_raw()); + // Safety: LeanBorrowed is repr(transparent) over *mut lean_object, + // same layout as the array's element pointers. + std::slice::from_raw_parts(cptr.cast(), self.len()) } } - /// Return a slice over the array elements. - pub fn data(&self) -> &[LeanObject] { + pub fn iter(&self) -> impl Iterator> + '_ { + self.data().iter().copied() + } + + pub fn map(&self, f: impl Fn(LeanBorrowed<'_>) -> T) -> Vec { + self.iter().map(f).collect() + } +} + +impl LeanArray { + /// Wrap a raw pointer, asserting it is an `Array`. + /// + /// # Safety + /// The pointer must be a valid Lean `Array` object. + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { unsafe { - let cptr = include::lean_array_cptr(self.0.as_ptr() as *mut _); - // Safety: LeanObject is repr(transparent) over *const c_void, and - // lean_array_cptr returns *mut *mut lean_object which has the same layout. - std::slice::from_raw_parts(cptr.cast(), self.len()) + debug_assert!(ptr as usize & 1 != 1); + debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_ARRAY); + Self(LeanOwned(ptr)) } } - pub fn iter(&self) -> impl Iterator + '_ { - self.data().iter().copied() + /// Allocate a new array with `size` elements (capacity = size). + pub fn alloc(size: usize) -> Self { + let obj = unsafe { include::lean_alloc_array(size, size) }; + Self(LeanOwned(obj)) } - pub fn map(&self, f: impl Fn(LeanObject) -> T) -> Vec { - self.iter().map(f).collect() + /// Set the `i`-th element. Takes ownership of `val`. + pub fn set(&self, i: usize, val: impl Into) { + let val: LeanOwned = val.into(); + unsafe { + include::lean_array_set_core(self.0.as_raw(), i, val.into_raw()); + } } /// Append `val` to the array, returning the (possibly reallocated) array. /// - /// Takes ownership of both `self` and `val` (matching `lean_array_push` - /// semantics). If you are pushing a borrowed value, call `val.inc_ref()` - /// first. - pub fn push(self, val: impl Into) -> LeanArray { - let val: LeanObject = val.into(); - let result = - unsafe { include::lean_array_push(self.0.as_ptr() as *mut _, val.as_ptr() as *mut _) }; - LeanArray(LeanObject(result.cast())) + /// Consumes both `self` and `val` (matching `lean_array_push` semantics). + pub fn push(self, val: impl Into) -> LeanArray { + let val: LeanOwned = val.into(); + let self_ptr = ManuallyDrop::new(self).0.as_raw(); + let val_ptr = val.into_raw(); + let result = unsafe { include::lean_array_push(self_ptr, val_ptr) }; + LeanArray(LeanOwned(result)) + } + + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr + } +} + +impl From> for LeanOwned { + #[inline] + fn from(x: LeanArray) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } @@ -389,74 +490,100 @@ impl LeanArray { // ============================================================================= /// Typed wrapper for a Lean `ByteArray` object (tag `LEAN_TAG_SCALAR_ARRAY`). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanByteArray(LeanObject); +pub struct LeanByteArray(R); -impl Deref for LeanByteArray { - type Target = LeanObject; +impl Clone for LeanByteArray { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl LeanByteArray { - /// Wrap a raw pointer, asserting it is a `ByteArray` (tag `LEAN_TAG_SCALAR_ARRAY`). +impl Copy for LeanByteArray {} + +impl LeanByteArray { + #[inline] + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + + pub fn len(&self) -> usize { + unsafe { include::lean_sarray_size(self.0.as_raw()) } + } + + pub fn is_empty(&self) -> bool { + self.len() == 0 + } + + /// Return the byte contents as a slice. + pub fn as_bytes(&self) -> &[u8] { + unsafe { + let cptr = include::lean_sarray_cptr(self.0.as_raw()); + std::slice::from_raw_parts(cptr, self.len()) + } + } +} + +impl LeanByteArray { + /// Wrap a raw pointer, asserting it is a `ByteArray`. /// /// # Safety /// The pointer must be a valid Lean `ByteArray` object. - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - let obj = LeanObject(ptr); - debug_assert!(!obj.is_scalar() && obj.tag() == LEAN_TAG_SCALAR_ARRAY); - Self(obj) + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + unsafe { + debug_assert!(ptr as usize & 1 != 1); + debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_SCALAR_ARRAY); + Self(LeanOwned(ptr)) + } } /// Allocate a new byte array with `size` bytes (capacity = size). pub fn alloc(size: usize) -> Self { let obj = unsafe { include::lean_alloc_sarray(1, size, size) }; - Self(LeanObject(obj.cast())) + Self(LeanOwned(obj)) } /// Allocate a new byte array and copy `data` into it. pub fn from_bytes(data: &[u8]) -> Self { let arr = Self::alloc(data.len()); unsafe { - let cptr = include::lean_sarray_cptr(arr.0.as_ptr() as *mut _); + let cptr = include::lean_sarray_cptr(arr.0.as_raw()); std::ptr::copy_nonoverlapping(data.as_ptr(), cptr, data.len()); } arr } - pub fn len(&self) -> usize { - unsafe { include::lean_sarray_size(self.0.as_ptr() as *mut _) } - } - - pub fn is_empty(&self) -> bool { - self.len() == 0 - } - - /// Return the byte contents as a slice. - pub fn as_bytes(&self) -> &[u8] { - unsafe { - let cptr = include::lean_sarray_cptr(self.0.as_ptr() as *mut _); - std::slice::from_raw_parts(cptr, self.len()) - } - } - /// Copy `data` into the byte array and update its size. /// /// # Safety /// The caller must ensure the array has sufficient capacity for `data`. pub unsafe fn set_data(&self, data: &[u8]) { unsafe { - let obj = self.0.as_mut_ptr(); - let cptr = include::lean_sarray_cptr(obj.cast()); + let obj = self.0.as_raw(); + let cptr = include::lean_sarray_cptr(obj); std::ptr::copy_nonoverlapping(data.as_ptr(), cptr, data.len()); // Update m_size: at offset 8 (after lean_object header) - *obj.cast::().add(8).cast::() = data.len(); + *(obj as *mut u8).add(8).cast::() = data.len(); } } + + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr + } +} + +impl From> for LeanOwned { + #[inline] + fn from(x: LeanByteArray) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) + } } // ============================================================================= @@ -464,61 +591,84 @@ impl LeanByteArray { // ============================================================================= /// Typed wrapper for a Lean `String` object (tag `LEAN_TAG_STRING`). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanString(LeanObject); +pub struct LeanString(R); + +impl Clone for LeanString { + #[inline] + fn clone(&self) -> Self { + Self(self.0.clone()) + } +} -impl Deref for LeanString { - type Target = LeanObject; +impl Copy for LeanString {} + +impl LeanString { + #[inline] + pub fn inner(&self) -> &R { &self.0 } #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + + /// Number of data bytes (excluding the trailing NUL). + pub fn byte_len(&self) -> usize { + unsafe { include::lean_string_size(self.0.as_raw()) - 1 } + } +} + +impl std::fmt::Display for LeanString { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + unsafe { + let obj = self.0.as_raw(); + let len = include::lean_string_size(obj) - 1; // m_size includes NUL + let data = include::lean_string_cstr(obj); + let bytes = std::slice::from_raw_parts(data.cast::(), len); + let s = std::str::from_utf8_unchecked(bytes); + f.write_str(s) + } } } -impl LeanString { - /// Wrap a raw pointer, asserting it is a `String` (tag `LEAN_TAG_STRING`). +impl LeanString { + /// Wrap a raw pointer, asserting it is a `String`. /// /// # Safety /// The pointer must be a valid Lean `String` object. - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - let obj = LeanObject(ptr); - debug_assert!(!obj.is_scalar() && obj.tag() == LEAN_TAG_STRING); - Self(obj) + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + unsafe { + debug_assert!(ptr as usize & 1 != 1); + debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_STRING); + Self(LeanOwned(ptr)) + } } /// Create a Lean string from a Rust `&str`. pub fn new(s: &str) -> Self { let c = safe_cstring(s); let obj = unsafe { include::lean_mk_string(c.as_ptr()) }; - Self(LeanObject(obj.cast())) + Self(LeanOwned(obj)) } /// Create a Lean string from raw bytes via `lean_mk_string_from_bytes`. - /// - /// Unlike `new`, this does not require a NUL-terminated C string and - /// handles interior NUL bytes. The bytes must be valid UTF-8. pub fn from_bytes(bytes: &[u8]) -> Self { let obj = unsafe { include::lean_mk_string_from_bytes(bytes.as_ptr().cast(), bytes.len()) }; - Self(LeanObject(obj.cast())) + Self(LeanOwned(obj)) } - /// Number of data bytes (excluding the trailing NUL). - pub fn byte_len(&self) -> usize { - unsafe { include::lean_string_size(self.0.as_ptr() as *mut _) - 1 } + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr } } -impl std::fmt::Display for LeanString { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - unsafe { - let obj = self.0.as_ptr() as *mut _; - let len = include::lean_string_size(obj) - 1; // m_size includes NUL - let data = include::lean_string_cstr(obj); - let bytes = std::slice::from_raw_parts(data.cast::(), len); - let s = std::str::from_utf8_unchecked(bytes); - f.write_str(s) - } +impl From> for LeanOwned { + #[inline] + fn from(x: LeanString) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } @@ -527,224 +677,165 @@ impl std::fmt::Display for LeanString { // ============================================================================= /// Typed wrapper for a Lean constructor object (tag 0–`LEAN_MAX_CTOR_TAG`). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanCtor(LeanObject); +pub struct LeanCtor(R); -impl Deref for LeanCtor { - type Target = LeanObject; +impl Clone for LeanCtor { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl LeanCtor { - /// Wrap a raw pointer, asserting it is a constructor (tag <= `LEAN_MAX_CTOR_TAG`). - /// - /// # Safety - /// The pointer must be a valid Lean constructor object. - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - let obj = LeanObject(ptr); - debug_assert!(!obj.is_scalar() && obj.tag() <= LEAN_MAX_CTOR_TAG); - Self(obj) - } +impl Copy for LeanCtor {} - /// Allocate a new constructor object. - pub fn alloc(tag: u8, num_objs: usize, scalar_size: usize) -> Self { - #[allow(clippy::cast_possible_truncation)] - let obj = - unsafe { include::lean_alloc_ctor(tag as u32, num_objs as u32, scalar_size as u32) }; - Self(LeanObject(obj.cast())) +impl LeanCtor { + /// Get the raw `*mut lean_object` pointer. + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() } pub fn tag(&self) -> u8 { self.0.tag() } - /// Get the `i`-th object field via `lean_ctor_get`. - pub fn get(&self, i: usize) -> LeanObject { - #[allow(clippy::cast_possible_truncation)] - LeanObject(unsafe { include::lean_ctor_get(self.0.as_ptr() as *mut _, i as u32) }.cast()) - } - - /// Set the `i`-th object field via `lean_ctor_set`. - pub fn set(&self, i: usize, val: impl Into) { - let val: LeanObject = val.into(); + /// Get a borrowed reference to the `i`-th object field. + pub fn get(&self, i: usize) -> LeanBorrowed<'_> { #[allow(clippy::cast_possible_truncation)] - unsafe { - include::lean_ctor_set(self.0.as_ptr() as *mut _, i as u32, val.as_ptr() as *mut _); - } + LeanBorrowed( + unsafe { include::lean_ctor_get(self.0.as_raw(), i as u32) }, + PhantomData, + ) } /// Read `N` object-field pointers using raw pointer math. - /// - /// This bypasses `lean_ctor_get`'s bounds check, which is necessary when - /// reading past the declared object fields into the scalar area (e.g. for - /// `Expr.Data`). - pub fn objs(&self) -> [LeanObject; N] { - let base = unsafe { self.0.as_ptr().cast::<*const c_void>().add(1) }; - std::array::from_fn(|i| LeanObject(unsafe { *base.add(i) })) + pub fn objs(&self) -> [LeanBorrowed<'_>; N] { + let base = unsafe { self.0.as_raw().cast::<*mut include::lean_object>().add(1) }; + std::array::from_fn(|i| LeanBorrowed(unsafe { *base.add(i) }, PhantomData)) } - // --------------------------------------------------------------------------- - // Scalar readers — delegate to lean.h functions - // --------------------------------------------------------------------------- + // ------------------------------------------------------------------------- + // Scalar field readers + // ------------------------------------------------------------------------- + // + // `num_objs` is the number of non-scalar fields (object + usize) preceding + // the scalar area. `offset` is a byte offset within the scalar area. + // For `get_usize`, `slot` is a slot index (not byte offset). - /// Read a `u8` scalar at `offset` bytes past `num_objs` object fields. + /// Compute the absolute byte offset for a scalar field. #[allow(clippy::cast_possible_truncation)] - pub fn scalar_u8(&self, num_objs: usize, offset: usize) -> u8 { - unsafe { - include::lean_ctor_get_uint8(self.0.as_ptr() as *mut _, (num_objs * 8 + offset) as u32) - } + #[inline] + fn scalar_offset(num_objs: usize, offset: usize) -> u32 { + (num_objs * 8 + offset) as u32 } - /// Read a `u16` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn scalar_u16(&self, num_objs: usize, offset: usize) -> u16 { - unsafe { - include::lean_ctor_get_uint16(self.0.as_ptr() as *mut _, (num_objs * 8 + offset) as u32) - } + pub fn get_u8(&self, num_objs: usize, offset: usize) -> u8 { + unsafe { include::lean_ctor_get_uint8(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } } - - /// Read a `u32` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn scalar_u32(&self, num_objs: usize, offset: usize) -> u32 { - unsafe { - include::lean_ctor_get_uint32(self.0.as_ptr() as *mut _, (num_objs * 8 + offset) as u32) - } + pub fn get_u16(&self, num_objs: usize, offset: usize) -> u16 { + unsafe { include::lean_ctor_get_uint16(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } } - - /// Read a `u64` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn scalar_u64(&self, num_objs: usize, offset: usize) -> u64 { - unsafe { - include::lean_ctor_get_uint64(self.0.as_ptr() as *mut _, (num_objs * 8 + offset) as u32) - } + pub fn get_u32(&self, num_objs: usize, offset: usize) -> u32 { + unsafe { include::lean_ctor_get_uint32(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } } - - /// Read a `f64` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn scalar_f64(&self, num_objs: usize, offset: usize) -> f64 { - unsafe { - include::lean_ctor_get_float(self.0.as_ptr() as *mut _, (num_objs * 8 + offset) as u32) - } + pub fn get_u64(&self, num_objs: usize, offset: usize) -> u64 { + unsafe { include::lean_ctor_get_uint64(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } } - - /// Read a `f32` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn scalar_f32(&self, num_objs: usize, offset: usize) -> f32 { - unsafe { - include::lean_ctor_get_float32( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, - ) - } + pub fn get_f64(&self, num_objs: usize, offset: usize) -> f64 { + unsafe { include::lean_ctor_get_float(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } } - - /// Read a `usize` scalar at slot `slot` past `num_objs` object fields. - /// - /// Note: `lean_ctor_get_usize` uses a **slot index** (not byte offset). - /// The slot is `num_objs + slot` where each slot is pointer-sized. + pub fn get_f32(&self, num_objs: usize, offset: usize) -> f32 { + unsafe { include::lean_ctor_get_float32(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } + } + /// Read a `usize` at slot `slot` past `num_objs` object fields. + /// Uses a **slot index** (not byte offset). #[allow(clippy::cast_possible_truncation)] - pub fn scalar_usize(&self, num_objs: usize, slot: usize) -> usize { - unsafe { include::lean_ctor_get_usize(self.0.as_ptr() as *mut _, (num_objs + slot) as u32) } + pub fn get_usize(&self, num_objs: usize, slot: usize) -> usize { + unsafe { include::lean_ctor_get_usize(self.0.as_raw(), (num_objs + slot) as u32) } } - - /// Read a `bool` scalar at `offset` bytes past `num_objs` object fields. - pub fn scalar_bool(&self, num_objs: usize, offset: usize) -> bool { - self.scalar_u8(num_objs, offset) != 0 + pub fn get_bool(&self, num_objs: usize, offset: usize) -> bool { + self.get_u8(num_objs, offset) != 0 } +} - // --------------------------------------------------------------------------- - // Symmetric scalar setters — take (num_objs, offset, val) like the readers - // --------------------------------------------------------------------------- - - /// Set a `u8` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn set_scalar_u8(&self, num_objs: usize, offset: usize, val: u8) { +impl LeanCtor { + /// Wrap a raw pointer, asserting it is a constructor. + /// + /// # Safety + /// The pointer must be a valid Lean constructor object. + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { unsafe { - include::lean_ctor_set_uint8( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, - val, - ); + debug_assert!(ptr as usize & 1 != 1); + debug_assert!(include::lean_obj_tag(ptr) as u8 <= LEAN_MAX_CTOR_TAG); + Self(LeanOwned(ptr)) } } - /// Set a `u16` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn set_scalar_u16(&self, num_objs: usize, offset: usize, val: u16) { - unsafe { - include::lean_ctor_set_uint16( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, - val, - ); - } + /// Allocate a new constructor object. + pub fn alloc(tag: u8, num_objs: usize, scalar_size: usize) -> Self { + #[allow(clippy::cast_possible_truncation)] + let obj = + unsafe { include::lean_alloc_ctor(tag as u32, num_objs as u32, scalar_size as u32) }; + Self(LeanOwned(obj)) } - /// Set a `u32` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn set_scalar_u32(&self, num_objs: usize, offset: usize, val: u32) { + /// Set the `i`-th object field. Takes ownership of `val`. + pub fn set(&self, i: usize, val: impl Into) { + let val: LeanOwned = val.into(); + #[allow(clippy::cast_possible_truncation)] unsafe { - include::lean_ctor_set_uint32( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, - val, - ); + include::lean_ctor_set(self.0.as_raw(), i as u32, val.into_raw()); } } - /// Set a `u64` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn set_scalar_u64(&self, num_objs: usize, offset: usize, val: u64) { - unsafe { - include::lean_ctor_set_uint64( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, - val, - ); - } + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr } - /// Set a `f64` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn set_scalar_f64(&self, num_objs: usize, offset: usize, val: f64) { - unsafe { - include::lean_ctor_set_float( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, - val, - ); - } - } + // ------------------------------------------------------------------------- + // Scalar field setters (owned only — mutation) + // ------------------------------------------------------------------------- - /// Set a `f32` scalar at `offset` bytes past `num_objs` object fields. - #[allow(clippy::cast_possible_truncation)] - pub fn set_scalar_f32(&self, num_objs: usize, offset: usize, val: f32) { - unsafe { - include::lean_ctor_set_float32( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, - val, - ); - } + pub fn set_u8(&self, num_objs: usize, offset: usize, val: u8) { + unsafe { include::lean_ctor_set_uint8(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } } - - /// Set a `usize` scalar at slot `slot` past `num_objs` object fields. - /// - /// Note: `lean_ctor_set_usize` uses a **slot index** (not byte offset). + pub fn set_u16(&self, num_objs: usize, offset: usize, val: u16) { + unsafe { include::lean_ctor_set_uint16(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + } + pub fn set_u32(&self, num_objs: usize, offset: usize, val: u32) { + unsafe { include::lean_ctor_set_uint32(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + } + pub fn set_u64(&self, num_objs: usize, offset: usize, val: u64) { + unsafe { include::lean_ctor_set_uint64(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + } + pub fn set_f64(&self, num_objs: usize, offset: usize, val: f64) { + unsafe { include::lean_ctor_set_float(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + } + pub fn set_f32(&self, num_objs: usize, offset: usize, val: f32) { + unsafe { include::lean_ctor_set_float32(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + } + /// Set a `usize` at slot `slot` past `num_objs` object fields. + /// Uses a **slot index** (not byte offset). #[allow(clippy::cast_possible_truncation)] - pub fn set_scalar_usize(&self, num_objs: usize, slot: usize, val: usize) { - unsafe { - include::lean_ctor_set_usize(self.0.as_ptr() as *mut _, (num_objs + slot) as u32, val); - } + pub fn set_usize(&self, num_objs: usize, slot: usize, val: usize) { + unsafe { include::lean_ctor_set_usize(self.0.as_raw(), (num_objs + slot) as u32, val); } } + pub fn set_bool(&self, num_objs: usize, offset: usize, val: bool) { + self.set_u8(num_objs, offset, val as u8); + } +} - /// Set a `bool` scalar at `offset` bytes past `num_objs` object fields. - pub fn set_scalar_bool(&self, num_objs: usize, offset: usize, val: bool) { - self.set_scalar_u8(num_objs, offset, val as u8); +impl From> for LeanOwned { + #[inline] + fn from(x: LeanCtor) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } @@ -753,40 +844,76 @@ impl LeanCtor { // ============================================================================= /// Typed wrapper for a Lean external object (tag `LEAN_TAG_EXTERNAL`) holding a `T`. -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanExternal(LeanObject, PhantomData); +pub struct LeanExternal(R, PhantomData); -impl Deref for LeanExternal { - type Target = LeanObject; +impl Clone for LeanExternal { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone(), PhantomData) + } +} + +impl Copy for LeanExternal {} + +impl LeanExternal { + /// Get a reference to the wrapped data. + pub fn get(&self) -> &T { + unsafe { &*include::lean_get_external_data(self.0.as_raw()).cast::() } } } -impl LeanExternal { - /// Wrap a raw pointer, asserting it is an external object (tag `LEAN_TAG_EXTERNAL`). +impl LeanExternal { + /// Wrap a raw pointer, asserting it is an external object. /// /// # Safety /// The pointer must be a valid Lean external object whose data pointer /// points to a valid `T`. - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - let obj = LeanObject(ptr); - debug_assert!(!obj.is_scalar() && obj.tag() == LEAN_TAG_EXTERNAL); - Self(obj, PhantomData) + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + unsafe { + debug_assert!(ptr as usize & 1 != 1); + debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_EXTERNAL); + Self(LeanOwned(ptr), PhantomData) + } } /// Allocate a new external object holding `data`. pub fn alloc(class: &ExternalClass, data: T) -> Self { let data_ptr = Box::into_raw(Box::new(data)); - let obj = unsafe { include::lean_alloc_external(class.0.cast(), data_ptr.cast()) }; - Self(LeanObject(obj.cast()), PhantomData) + let obj = unsafe { include::lean_alloc_external(class.0, data_ptr.cast()) }; + Self(LeanOwned(obj), PhantomData) } - /// Get a reference to the wrapped data. - pub fn get(&self) -> &T { - unsafe { &*include::lean_get_external_data(self.0.as_ptr() as *mut _).cast::() } + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr + } +} + +impl<'a, T> LeanExternal> { + /// Wrap a raw pointer as a borrowed external object. + /// + /// # Safety + /// The pointer must be a valid Lean external object whose data pointer + /// points to a valid `T`, and the object must outlive `'a`. + pub unsafe fn from_raw_borrowed(ptr: *mut include::lean_object) -> Self { + unsafe { + debug_assert!(ptr as usize & 1 != 1); + debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_EXTERNAL); + Self(LeanBorrowed::from_raw(ptr), PhantomData) + } + } +} + +impl From> for LeanOwned { + #[inline] + fn from(x: LeanExternal) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } @@ -795,7 +922,7 @@ impl LeanExternal { // ============================================================================= /// A registered Lean external class (wraps `lean_external_class*`). -pub struct ExternalClass(*mut c_void); +pub struct ExternalClass(*mut include::lean_external_class); // Safety: the class pointer is initialized once and read-only thereafter. unsafe impl Send for ExternalClass {} @@ -811,13 +938,13 @@ impl ExternalClass { finalizer: include::lean_external_finalize_proc, foreach: include::lean_external_foreach_proc, ) -> Self { - Self(unsafe { include::lean_register_external_class(finalizer, foreach) }.cast()) + Self(unsafe { include::lean_register_external_class(finalizer, foreach) }) } /// Register a new external class that uses `Drop` to finalize `T` /// and has no Lean object references to visit. pub fn register_with_drop() -> Self { - unsafe extern "C" fn drop_finalizer(ptr: *mut c_void) { + unsafe extern "C" fn drop_finalizer(ptr: *mut std::ffi::c_void) { if !ptr.is_null() { drop(unsafe { Box::from_raw(ptr.cast::()) }); } @@ -831,58 +958,74 @@ impl ExternalClass { // ============================================================================= /// Typed wrapper for a Lean `List α` (nil = scalar `lean_box(0)`, cons = ctor tag 1). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanList(LeanObject); +pub struct LeanList(R); -impl Deref for LeanList { - type Target = LeanObject; +impl Clone for LeanList { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl LeanList { - /// Wrap a raw pointer, asserting it is a valid `List` (scalar nil or ctor tag 1). +impl Copy for LeanList {} + +impl LeanList { + #[inline] + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + + pub fn is_nil(&self) -> bool { + self.0.is_scalar() + } + + pub fn iter(&self) -> LeanListIter<'_> { + LeanListIter(LeanBorrowed(self.0.as_raw(), PhantomData)) + } + + pub fn collect(&self, f: impl Fn(LeanBorrowed<'_>) -> T) -> Vec { + self.iter().map(f).collect() + } +} + +impl LeanList { + /// Wrap a raw pointer, asserting it is a valid `List`. /// /// # Safety /// The pointer must be a valid Lean `List` object. - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - let obj = LeanObject(ptr); - debug_assert!(obj.is_scalar() || obj.tag() == 1); - Self(obj) + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + unsafe { + debug_assert!(ptr as usize & 1 == 1 || include::lean_obj_tag(ptr) as u8 == 1); + Self(LeanOwned(ptr)) + } } /// The empty list. pub fn nil() -> Self { - Self(LeanObject::box_usize(0)) + Self(LeanOwned::box_usize(0)) } /// Prepend `head` to `tail`. - pub fn cons(head: impl Into, tail: LeanList) -> Self { + pub fn cons(head: impl Into, tail: LeanList) -> Self { let ctor = LeanCtor::alloc(1, 2, 0); ctor.set(0, head); ctor.set(1, tail); - Self(ctor.0) - } - - pub fn is_nil(&self) -> bool { - self.0.is_scalar() - } - - pub fn iter(&self) -> LeanListIter { - LeanListIter(self.0) + Self(LeanOwned(ctor.into_raw())) } - pub fn collect(&self, f: impl Fn(LeanObject) -> T) -> Vec { - self.iter().map(f).collect() + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr } } -impl> FromIterator for LeanList { +impl> FromIterator for LeanList { fn from_iter>(iter: I) -> Self { - let items: Vec = iter.into_iter().map(Into::into).collect(); + let items: Vec = iter.into_iter().map(Into::into).collect(); let mut list = Self::nil(); for item in items.into_iter().rev() { list = Self::cons(item, list); @@ -892,18 +1035,28 @@ impl> FromIterator for LeanList { } /// Iterator over the elements of a `LeanList`. -pub struct LeanListIter(LeanObject); +pub struct LeanListIter<'a>(LeanBorrowed<'a>); -impl Iterator for LeanListIter { - type Item = LeanObject; +impl<'a> Iterator for LeanListIter<'a> { + type Item = LeanBorrowed<'a>; fn next(&mut self) -> Option { if self.0.is_scalar() { return None; } - let ctor = self.0.as_ctor(); - let [head, tail] = ctor.objs::<2>(); - self.0 = tail; - Some(head) + let ptr = self.0.as_raw(); + let head = unsafe { include::lean_ctor_get(ptr, 0) }; + let tail = unsafe { include::lean_ctor_get(ptr, 1) }; + self.0 = LeanBorrowed(tail, PhantomData); + Some(LeanBorrowed(head, PhantomData)) + } +} + +impl From> for LeanOwned { + #[inline] + fn from(x: LeanList) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } @@ -912,37 +1065,26 @@ impl Iterator for LeanListIter { // ============================================================================= /// Typed wrapper for a Lean `Option α` (none = scalar, some = ctor tag 1). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanOption(LeanObject); +pub struct LeanOption(R); -impl Deref for LeanOption { - type Target = LeanObject; +impl Clone for LeanOption { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl LeanOption { - /// Wrap a raw pointer, asserting it is a valid `Option`. - /// - /// # Safety - /// The pointer must be a valid Lean `Option` object. - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - let obj = LeanObject(ptr); - debug_assert!(obj.is_scalar() || obj.tag() == 1); - Self(obj) - } +impl Copy for LeanOption {} - pub fn none() -> Self { - Self(LeanObject::box_usize(0)) - } - - pub fn some(val: impl Into) -> Self { - let ctor = LeanCtor::alloc(1, 1, 0); - ctor.set(0, val); - Self(ctor.0) +impl LeanOption { + #[inline] + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + #[inline] + pub fn as_ctor(&self) -> LeanCtor> { + unsafe { LeanBorrowed::from_raw(self.0.as_raw()) }.as_ctor() } pub fn is_none(&self) -> bool { @@ -953,14 +1095,55 @@ impl LeanOption { !self.is_none() } - pub fn to_option(&self) -> Option { + pub fn to_option(&self) -> Option> { if self.is_none() { None } else { - let ctor = self.0.as_ctor(); - Some(ctor.get(0)) + #[allow(clippy::cast_possible_truncation)] + let val = unsafe { include::lean_ctor_get(self.0.as_raw(), 0) }; + Some(LeanBorrowed(val, PhantomData)) + } + } +} + +impl LeanOption { + /// Wrap a raw pointer, asserting it is a valid `Option`. + /// + /// # Safety + /// The pointer must be a valid Lean `Option` object. + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + unsafe { + debug_assert!(ptr as usize & 1 == 1 || include::lean_obj_tag(ptr) as u8 == 1); + Self(LeanOwned(ptr)) } } + + pub fn none() -> Self { + Self(LeanOwned::box_usize(0)) + } + + pub fn some(val: impl Into) -> Self { + let ctor = LeanCtor::alloc(1, 1, 0); + ctor.set(0, val); + Self(LeanOwned(ctor.into_raw())) + } + + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr + } +} + +impl From> for LeanOwned { + #[inline] + fn from(x: LeanOption) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) + } } // ============================================================================= @@ -968,41 +1151,73 @@ impl LeanOption { // ============================================================================= /// Typed wrapper for a Lean `Except ε α` (error = ctor tag 0, ok = ctor tag 1). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanExcept(LeanObject); +pub struct LeanExcept(R); -impl Deref for LeanExcept { - type Target = LeanObject; +impl Clone for LeanExcept { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl LeanExcept { +impl Copy for LeanExcept {} + +impl LeanExcept { + #[inline] + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + #[inline] + pub fn as_ctor(&self) -> LeanCtor> { + unsafe { LeanBorrowed::from_raw(self.0.as_raw()) }.as_ctor() + } + + pub fn is_ok(&self) -> bool { + self.0.tag() == 1 + } + + pub fn is_error(&self) -> bool { + self.0.tag() == 0 + } + + pub fn into_result(&self) -> Result, LeanBorrowed<'_>> { + let val = unsafe { include::lean_ctor_get(self.0.as_raw(), 0) }; + if self.is_ok() { + Ok(LeanBorrowed(val, PhantomData)) + } else { + Err(LeanBorrowed(val, PhantomData)) + } + } +} + +impl LeanExcept { /// Wrap a raw pointer, asserting it is a valid `Except`. /// /// # Safety /// The pointer must be a valid Lean `Except` object. - pub unsafe fn from_raw(ptr: *const c_void) -> Self { - let obj = LeanObject(ptr); - debug_assert!(!obj.is_scalar() && (obj.tag() == 0 || obj.tag() == 1)); - Self(obj) + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + unsafe { + debug_assert!(ptr as usize & 1 != 1); + debug_assert!( + include::lean_obj_tag(ptr) as u8 == 0 || include::lean_obj_tag(ptr) as u8 == 1 + ); + Self(LeanOwned(ptr)) + } } /// Build `Except.ok val`. - pub fn ok(val: impl Into) -> Self { + pub fn ok(val: impl Into) -> Self { let ctor = LeanCtor::alloc(1, 1, 0); ctor.set(0, val); - Self(ctor.0) + Self(LeanOwned(ctor.into_raw())) } /// Build `Except.error msg`. - pub fn error(msg: impl Into) -> Self { + pub fn error(msg: impl Into) -> Self { let ctor = LeanCtor::alloc(0, 1, 0); ctor.set(0, msg); - Self(ctor.0) + Self(LeanOwned(ctor.into_raw())) } /// Build `Except.error (String.mk msg)` from a Rust string. @@ -1010,21 +1225,21 @@ impl LeanExcept { Self::error(LeanString::new(msg)) } - pub fn is_ok(&self) -> bool { - self.0.tag() == 1 - } - - pub fn is_error(&self) -> bool { - self.0.tag() == 0 + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr } +} - pub fn into_result(self) -> Result { - let ctor = self.0.as_ctor(); - if self.is_ok() { - Ok(ctor.get(0)) - } else { - Err(ctor.get(0)) - } +impl From> for LeanOwned { + #[inline] + fn from(x: LeanExcept) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } @@ -1034,40 +1249,68 @@ impl LeanExcept { /// Typed wrapper for a Lean `BaseIO.Result α` (`EStateM.Result`). /// ok = ctor tag 0 (value, world), error = ctor tag 1 (error, world). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanIOResult(LeanObject); +pub struct LeanIOResult(R); -impl Deref for LeanIOResult { - type Target = LeanObject; +impl Clone for LeanIOResult { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl LeanIOResult { +impl Copy for LeanIOResult {} + +impl LeanIOResult { + #[inline] + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + #[inline] + pub fn as_ctor(&self) -> LeanCtor> { + unsafe { LeanBorrowed::from_raw(self.0.as_raw()) }.as_ctor() + } +} + +impl LeanIOResult { /// Build a successful IO result (tag 0, fields: [val, box(0)]). - pub fn ok(val: impl Into) -> Self { + pub fn ok(val: impl Into) -> Self { let ctor = LeanCtor::alloc(0, 2, 0); ctor.set(0, val); - ctor.set(1, LeanObject::box_usize(0)); // world token - Self(ctor.0) + ctor.set(1, LeanOwned::box_usize(0)); // world token + Self(LeanOwned(ctor.into_raw())) } /// Build an IO error result (tag 1, fields: [err, box(0)]). - pub fn error(err: impl Into) -> Self { + pub fn error(err: impl Into) -> Self { let ctor = LeanCtor::alloc(1, 2, 0); ctor.set(0, err); - ctor.set(1, LeanObject::box_usize(0)); // world token - Self(ctor.0) + ctor.set(1, LeanOwned::box_usize(0)); // world token + Self(LeanOwned(ctor.into_raw())) } /// Build an IO error from a Rust string via `IO.Error.userError` (tag 7, 1 field). pub fn error_string(msg: &str) -> Self { let user_error = LeanCtor::alloc(IO_ERROR_USER_ERROR_TAG, 1, 0); user_error.set(0, LeanString::new(msg)); - Self::error(*user_error) + Self::error(user_error) + } + + /// Consume without calling `lean_dec`. + #[inline] + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr + } +} + +impl From> for LeanOwned { + #[inline] + fn from(x: LeanIOResult) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } @@ -1076,131 +1319,131 @@ impl LeanIOResult { // ============================================================================= /// Typed wrapper for a Lean `Prod α β` (ctor tag 0, 2 object fields). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanProd(LeanObject); +pub struct LeanProd(R); -impl Deref for LeanProd { - type Target = LeanObject; +impl Clone for LeanProd { #[inline] - fn deref(&self) -> &LeanObject { - &self.0 + fn clone(&self) -> Self { + Self(self.0.clone()) } } -impl From for LeanObject { +impl Copy for LeanProd {} + +impl LeanProd { + #[inline] + pub fn inner(&self) -> &R { &self.0 } #[inline] - fn from(x: LeanProd) -> Self { - x.0 + pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + + /// Get a borrowed reference to the first element. + pub fn fst(&self) -> LeanBorrowed<'_> { + LeanBorrowed( + unsafe { include::lean_ctor_get(self.0.as_raw(), 0) }, + PhantomData, + ) + } + + /// Get a borrowed reference to the second element. + pub fn snd(&self) -> LeanBorrowed<'_> { + LeanBorrowed( + unsafe { include::lean_ctor_get(self.0.as_raw(), 1) }, + PhantomData, + ) } } -impl LeanProd { +impl LeanProd { /// Build a pair `(fst, snd)`. - pub fn new(fst: impl Into, snd: impl Into) -> Self { + pub fn new(fst: impl Into, snd: impl Into) -> Self { let ctor = LeanCtor::alloc(0, 2, 0); ctor.set(0, fst); ctor.set(1, snd); - Self(*ctor) - } - - /// Get the first element. - pub fn fst(&self) -> LeanObject { - let ctor = self.0.as_ctor(); - ctor.get(0) - } - - /// Get the second element. - pub fn snd(&self) -> LeanObject { - let ctor = self.0.as_ctor(); - ctor.get(1) + Self(LeanOwned(ctor.into_raw())) } -} -// ============================================================================= -// From for LeanObject — allow wrapper types to be passed to set() etc. -// ============================================================================= - -impl From for LeanObject { + /// Consume without calling `lean_dec`. #[inline] - fn from(x: LeanArray) -> Self { - x.0 + pub fn into_raw(self) -> *mut include::lean_object { + let ptr = self.0.as_raw(); + std::mem::forget(self); + ptr } } -impl From for LeanObject { +impl From> for LeanOwned { #[inline] - fn from(x: LeanByteArray) -> Self { - x.0 + fn from(x: LeanProd) -> Self { + let ptr = x.0.as_raw(); + std::mem::forget(x); + LeanOwned(ptr) } } -impl From for LeanObject { - #[inline] - fn from(x: LeanString) -> Self { - x.0 - } -} +// ============================================================================= +// From for LeanOwned +// ============================================================================= -impl From for LeanObject { +impl From for LeanOwned { #[inline] - fn from(x: LeanCtor) -> Self { - x.0 + fn from(x: u32) -> Self { + Self::box_u32(x) } } -impl From> for LeanObject { +impl From for LeanOwned { #[inline] - fn from(x: LeanExternal) -> Self { - x.0 + fn from(x: f64) -> Self { + Self::box_f64(x) } } -impl From for LeanObject { +impl From for LeanOwned { #[inline] - fn from(x: LeanList) -> Self { - x.0 + fn from(x: f32) -> Self { + Self::box_f32(x) } } -impl From for LeanObject { - #[inline] - fn from(x: LeanOption) -> Self { - x.0 - } -} +// ============================================================================= +// Convenience: as_ctor / as_string / as_array / as_list / as_byte_array +// ============================================================================= -impl From for LeanObject { +/// Helper methods for interpreting a reference as a specific domain type (borrowed view). +impl<'a> LeanBorrowed<'a> { + /// Interpret as a constructor object. #[inline] - fn from(x: LeanExcept) -> Self { - x.0 + pub fn as_ctor(self) -> LeanCtor> { + debug_assert!(!self.is_scalar() && self.tag() <= LEAN_MAX_CTOR_TAG); + LeanCtor(self) } -} -impl From for LeanObject { + /// Interpret as a `String` object. #[inline] - fn from(x: LeanIOResult) -> Self { - x.0 + pub fn as_string(self) -> LeanString> { + debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_STRING); + LeanString(self) } -} -impl From for LeanObject { + /// Interpret as an `Array` object. #[inline] - fn from(x: u32) -> Self { - Self::box_u32(x) + pub fn as_array(self) -> LeanArray> { + debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_ARRAY); + LeanArray(self) } -} -impl From for LeanObject { + /// Interpret as a `List`. #[inline] - fn from(x: f64) -> Self { - Self::box_f64(x) + pub fn as_list(self) -> LeanList> { + debug_assert!(self.is_scalar() || self.tag() == 1); + LeanList(self) } -} -impl From for LeanObject { + /// Interpret as a `ByteArray` object. #[inline] - fn from(x: f32) -> Self { - Self::box_f32(x) + pub fn as_byte_array(self) -> LeanByteArray> { + debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_SCALAR_ARRAY); + LeanByteArray(self) } } diff --git a/test/.gitignore b/test/.gitignore deleted file mode 100644 index ca25570..0000000 --- a/test/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -/target -/.lake diff --git a/test/Cargo.toml b/test/Cargo.toml index 879df99..4b3fd11 100644 --- a/test/Cargo.toml +++ b/test/Cargo.toml @@ -8,3 +8,9 @@ crate-type = ["staticlib"] [dependencies] lean-ffi = { path = ".." } + +[profile.dev] +panic = "abort" + +[profile.release] +panic = "abort" diff --git a/test/Tests.lean b/test/Tests.lean new file mode 100644 index 0000000..16a9dad --- /dev/null +++ b/test/Tests.lean @@ -0,0 +1 @@ +import Tests.FFI diff --git a/test/Tests/FFI.lean b/test/Tests/FFI.lean index ac47007..b2b7f62 100644 --- a/test/Tests/FFI.lean +++ b/test/Tests/FFI.lean @@ -11,7 +11,7 @@ open LSpec SlimCheck Gen namespace Tests.FFI -/-! ## FFI declarations -/ +/-! ## FFI declarations — borrowed (@&) parameters -/ @[extern "rs_roundtrip_nat"] opaque roundtripNat : @& Nat → Nat @@ -114,6 +114,169 @@ opaque rustDataGetY : @& RustData → UInt64 @[extern "rs_external_get_label"] opaque rustDataGetLabel : @& RustData → String +/-! ## FFI declarations — owned parameters (NO @&, Rust must lean_dec) -/ + +@[extern "rs_owned_nat_roundtrip"] +opaque ownedNatRoundtrip : Nat → Nat + +@[extern "rs_owned_string_roundtrip"] +opaque ownedStringRoundtrip : String → String + +@[extern "rs_owned_array_nat_roundtrip"] +opaque ownedArrayNatRoundtrip : Array Nat → Array Nat + +@[extern "rs_owned_list_nat_roundtrip"] +opaque ownedListNatRoundtrip : List Nat → List Nat + +@[extern "rs_owned_append_nat"] +opaque ownedAppendNat : Array Nat → Nat → Array Nat + +@[extern "rs_owned_drop_and_replace"] +opaque ownedDropAndReplace : String → String + +@[extern "rs_owned_merge_lists"] +opaque ownedMergeLists : List Nat → List Nat → List Nat → List Nat + +@[extern "rs_owned_reverse_bytearray"] +opaque ownedReverseByteArray : ByteArray → ByteArray + +@[extern "rs_owned_point_sum"] +opaque ownedPointSum : Point → Nat + +@[extern "rs_owned_except_transform"] +opaque ownedExceptTransform : Except String Nat → Nat + +@[extern "rs_owned_option_square"] +opaque ownedOptionSquare : Option Nat → Nat + +@[extern "rs_owned_prod_multiply"] +opaque ownedProdMultiply : Nat × Nat → Nat + +@[extern "rs_owned_scalar_sum"] +opaque ownedScalarSum : ScalarStruct → UInt64 + +/-! ## FFI declarations — Clone, data(), and API tests -/ + +@[extern "rs_clone_array_len_sum"] +opaque cloneArrayLenSum : @& Array Nat → USize + +@[extern "rs_clone_string_len_sum"] +opaque cloneStringLenSum : @& String → USize + +@[extern "rs_clone_except"] +opaque cloneExcept : Except String Nat → Nat + +@[extern "rs_clone_list"] +opaque cloneList : List Nat → Nat + +@[extern "rs_clone_bytearray"] +opaque cloneByteArray : ByteArray → Nat + +@[extern "rs_clone_option"] +opaque cloneOption : Option Nat → Nat + +@[extern "rs_clone_prod"] +opaque cloneProd : Nat × Nat → Nat + +@[extern "rs_owned_bytearray_roundtrip"] +opaque ownedByteArrayRoundtrip : ByteArray → ByteArray + +@[extern "rs_owned_option_roundtrip"] +opaque ownedOptionRoundtrip : Option Nat → Option Nat + +@[extern "rs_owned_prod_roundtrip"] +opaque ownedProdRoundtrip : Nat × Nat → Nat × Nat + +@[extern "rs_owned_io_result_value"] +opaque ownedIOResultValue : EStateM.Result IO.Error PUnit Nat → Nat + +@[extern "rs_array_data_sum"] +opaque arrayDataSum : @& Array Nat → Nat + +@[extern "rs_option_unwrap_or_zero"] +opaque optionUnwrapOrZero : @& Option Nat → Nat + +@[extern "rs_prod_swap"] +opaque prodSwap : @& Nat × Nat → Nat × Nat + +@[extern "rs_except_map_ok"] +opaque exceptMapOk : @& Except String Nat → Nat + +@[extern "rs_borrowed_result_chain"] +opaque borrowedResultChain : @& Array Nat × Array Nat → Nat + +@[extern "rs_borrowed_except_value"] +opaque borrowedExceptValue : @& Except String Nat → Nat + +/-! ## FFI declarations — nested collections -/ + +@[extern "rs_roundtrip_nested_array"] +opaque roundtripNestedArray : @& Array (Array Nat) → Array (Array Nat) + +@[extern "rs_roundtrip_nested_list"] +opaque roundtripNestedList : @& List (List Nat) → List (List Nat) + +/-! ## FFI declarations — misc edge cases -/ + +@[extern "rs_multi_borrow_sum"] +opaque multiBorrowSum : @& Array Nat → Nat + +@[extern "rs_list_to_array_via_push"] +opaque listToArrayViaPush : @& List Nat → Array Nat + +@[extern "rs_borrow_to_owned"] +opaque borrowToOwned : @& Nat → Nat + +@[extern "rs_make_empty_array"] +opaque makeEmptyArray : Unit → Array Nat + +@[extern "rs_make_empty_list"] +opaque makeEmptyList : Unit → List Nat + +@[extern "rs_make_empty_bytearray"] +opaque makeEmptyByteArray : Unit → ByteArray + +@[extern "rs_make_empty_string"] +opaque makeEmptyString : Unit → String + +@[extern "rs_nat_max_scalar"] +opaque natMaxScalar : Unit → Nat + +@[extern "rs_nat_min_heap"] +opaque natMinHeap : Unit → Nat + +@[extern "rs_external_all_fields"] +opaque externalAllFields : @& RustData → String + +/-! ## FFI declarations — persistent object tests -/ + +@[extern "rs_is_persistent"] +opaque isPersistent : @& Nat → UInt8 + +@[extern "rs_read_persistent_nat"] +opaque readPersistentNat : @& Nat → Nat + +@[extern "rs_read_persistent_point"] +opaque readPersistentPoint : @& Point → Nat + +@[extern "rs_read_persistent_array"] +opaque readPersistentArray : @& Array Nat → Nat + +@[extern "rs_read_persistent_string"] +opaque readPersistentString : @& String → Nat + +@[extern "rs_drop_persistent_nat"] +opaque dropPersistentNat : Nat → Nat + +/-! ## Persistent module-level values -/ +-- These become persistent (m_rc == 0) after module initialization. + +private def persistentNat : Nat := 42 +private def persistentLargeNat : Nat := 2^128 +private def persistentPoint : Point := ⟨10, 20⟩ +private def persistentArray : Array Nat := #[1, 2, 3, 4, 5] +private def persistentString : String := "hello persistent" + /-! ## Unit tests -/ def simpleTests : TestSeq := @@ -220,7 +383,9 @@ def externalTests : TestSeq := test "External create and get label" (rustDataGetLabel (mkRustData 42 99 "hello") == "hello") ++ test "External zero values" (rustDataGetX (mkRustData 0 0 "") == 0) ++ test "External empty label" (rustDataGetLabel (mkRustData 0 0 "") == "") ++ - test "External large values" (rustDataGetX (mkRustData 0xFFFFFFFFFFFFFFFF 0 "test") == 0xFFFFFFFFFFFFFFFF) + test "External large values" (rustDataGetX (mkRustData 0xFFFFFFFFFFFFFFFF 0 "test") == 0xFFFFFFFFFFFFFFFF) ++ + test "External all fields" (externalAllFields (mkRustData 42 99 "hello") == "42:99:hello") ++ + test "External all fields zeros" (externalAllFields (mkRustData 0 0 "") == "0:0:") /-! ## Edge cases for large Nats -/ @@ -232,25 +397,231 @@ def largeNatTests : TestSeq := let rt := roundtripNat n pure (rt == n, 0, 0, if rt == n then none else some s!"got {rt}")) .done +/-! ## Owned argument tests — verify LeanOwned Drop (lean_dec) works correctly -/ + +def ownedArgTests : TestSeq := + -- Basic roundtrip with owned args (Drop must lean_dec correctly) + test "Owned Nat 0" (ownedNatRoundtrip 0 == 0) ++ + test "Owned Nat 42" (ownedNatRoundtrip 42 == 42) ++ + test "Owned Nat large" (ownedNatRoundtrip (2^128) == 2^128) ++ + test "Owned String hello" (ownedStringRoundtrip "hello" == "hello") ++ + test "Owned String empty" (ownedStringRoundtrip "" == "") ++ + test "Owned Array empty" (ownedArrayNatRoundtrip #[] == #[]) ++ + test "Owned Array [1,2,3]" (ownedArrayNatRoundtrip #[1, 2, 3] == #[1, 2, 3]) ++ + test "Owned List empty" (ownedListNatRoundtrip [] == []) ++ + test "Owned List [1,2,3]" (ownedListNatRoundtrip [1, 2, 3] == [1, 2, 3]) ++ + -- Two owned args: array + nat + test "Owned append nat" (ownedAppendNat #[1, 2] 3 == #[1, 2, 3]) ++ + test "Owned append to empty" (ownedAppendNat #[] 42 == #[42]) ++ + -- Explicit early drop + test "Owned drop and replace" (ownedDropAndReplace "hello" == "replaced:5") ++ + test "Owned drop and replace empty" (ownedDropAndReplace "" == "replaced:0") ++ + -- Three owned args + test "Owned merge lists" (ownedMergeLists [1, 2] [3] [4, 5] == [1, 2, 3, 4, 5]) ++ + test "Owned merge empty" (ownedMergeLists [] [] [] == []) ++ + test "Owned merge one empty" (ownedMergeLists [1] [] [2] == [1, 2]) ++ + -- Owned ByteArray + test "Owned reverse bytearray" (ownedReverseByteArray ⟨#[1, 2, 3]⟩ == ⟨#[3, 2, 1]⟩) ++ + test "Owned reverse empty" (ownedReverseByteArray ⟨#[]⟩ == ⟨#[]⟩) ++ + -- Owned constructor (Point) + test "Owned point sum" (ownedPointSum ⟨10, 20⟩ == 30) ++ + test "Owned point sum zero" (ownedPointSum ⟨0, 0⟩ == 0) ++ + -- Owned Except + test "Owned except ok" (ownedExceptTransform (.ok 21) == 42) ++ + test "Owned except error" (ownedExceptTransform (.error "hello") == 5) ++ + test "Owned except error empty" (ownedExceptTransform (.error "") == 0) ++ + -- Owned Option + test "Owned option some" (ownedOptionSquare (some 5) == 25) ++ + test "Owned option none" (ownedOptionSquare none == 0) ++ + test "Owned option some 0" (ownedOptionSquare (some 0) == 0) ++ + -- Owned Prod + test "Owned prod multiply" (ownedProdMultiply (3, 7) == 21) ++ + test "Owned prod multiply zero" (ownedProdMultiply (0, 100) == 0) ++ + -- Owned ScalarStruct + test "Owned scalar sum" (ownedScalarSum ⟨42, 1, 100, 1000⟩ == 1101) ++ + test "Owned scalar sum zero" (ownedScalarSum ⟨0, 0, 0, 0⟩ == 0) ++ + -- Owned ByteArray roundtrip + test "Owned bytearray [1,2,3]" (ownedByteArrayRoundtrip ⟨#[1, 2, 3]⟩ == ⟨#[1, 2, 3]⟩) ++ + test "Owned bytearray empty" (ownedByteArrayRoundtrip ⟨#[]⟩ == ⟨#[]⟩) ++ + -- Owned Option roundtrip + test "Owned option some 42" (ownedOptionRoundtrip (some 42) == some 42) ++ + test "Owned option none" (ownedOptionRoundtrip none == none) ++ + -- Owned Prod roundtrip + test "Owned prod (3, 7)" (ownedProdRoundtrip (3, 7) == (3, 7)) ++ + test "Owned prod (0, 0)" (ownedProdRoundtrip (0, 0) == (0, 0)) ++ + -- Owned IOResult + test "Owned IOResult ok" (ownedIOResultValue (ioResultOkNat 42) == 42) ++ + test "Owned IOResult error" (ownedIOResultValue (ioResultErrorString "oops") == 0) + +/-! ## Clone tests — verify lean_inc produces valid second handle -/ + +def cloneTests : TestSeq := + test "Clone array len sum empty" (cloneArrayLenSum #[] == 0) ++ + test "Clone array len sum [1,2,3]" (cloneArrayLenSum #[1, 2, 3] == 6) ++ + test "Clone string len sum hello" (cloneStringLenSum "hello" == 10) ++ + test "Clone string len sum empty" (cloneStringLenSum "" == 0) ++ + -- Clone Except: clones an owned Except, reads from both, drops both + test "Clone except ok" (cloneExcept (.ok 21) == 42) ++ + test "Clone except error" (cloneExcept (.error "hello") == 10) ++ + test "Clone except ok 0" (cloneExcept (.ok 0) == 0) ++ + -- Clone List: clone + count elements in both copies + test "Clone list [1,2,3]" (cloneList [1, 2, 3] == 6) ++ + test "Clone list empty" (cloneList [] == 0) ++ + -- Clone ByteArray: clone + sum byte lengths + test "Clone bytearray [1,2,3]" (cloneByteArray ⟨#[1, 2, 3]⟩ == 6) ++ + test "Clone bytearray empty" (cloneByteArray ⟨#[]⟩ == 0) ++ + -- Clone Option: clone + sum values from both copies + test "Clone option some 21" (cloneOption (some 21) == 42) ++ + test "Clone option none" (cloneOption none == 0) ++ + -- Clone Prod: clone + sum all four field reads + test "Clone prod (3, 7)" (cloneProd (3, 7) == 20) ++ + test "Clone prod (0, 0)" (cloneProd (0, 0) == 0) + +/-! ## data() slice API tests -/ + +def dataSliceTests : TestSeq := + test "Array data sum empty" (arrayDataSum #[] == 0) ++ + test "Array data sum [1,2,3]" (arrayDataSum #[1, 2, 3] == 6) ++ + test "Array data sum [100]" (arrayDataSum #[100] == 100) ++ + test "Multi borrow sum [1,2,3]" (multiBorrowSum #[1, 2, 3] == 6) ++ + test "Multi borrow sum empty" (multiBorrowSum #[] == 0) ++ + test "Multi borrow sum [0,0,0]" (multiBorrowSum #[0, 0, 0] == 0) + +/-! ## API tests — Option, Prod, Except helpers -/ + +def apiTests : TestSeq := + test "Option unwrap some 42" (optionUnwrapOrZero (some 42) == 42) ++ + test "Option unwrap none" (optionUnwrapOrZero none == 0) ++ + test "Option unwrap some 0" (optionUnwrapOrZero (some 0) == 0) ++ + test "Prod swap (1, 2)" (prodSwap (1, 2) == (2, 1)) ++ + test "Prod swap (0, 0)" (prodSwap (0, 0) == (0, 0)) ++ + test "Prod swap (100, 200)" (prodSwap (100, 200) == (200, 100)) ++ + test "Except map ok 42" (exceptMapOk (.ok 42) == 43) ++ + test "Except map ok 0" (exceptMapOk (.ok 0) == 1) ++ + test "Except map error" (exceptMapOk (.error "fail") == 0) ++ + -- Borrowed result chains (b_lean_obj_res pattern: internal borrowed refs without lean_inc) + test "Borrowed chain (#[1,2], #[3,4])" (borrowedResultChain (#[1, 2], #[3, 4]) == 10) ++ + test "Borrowed chain (#[], #[])" (borrowedResultChain (#[], #[]) == 0) ++ + test "Borrowed chain (#[100], #[])" (borrowedResultChain (#[100], #[]) == 100) ++ + test "Borrowed except ok" (borrowedExceptValue (.ok 42) == 42) ++ + test "Borrowed except error" (borrowedExceptValue (.error "hello") == 5) + +/-! ## Nested collection tests -/ + +def nestedTests : TestSeq := + test "Nested array empty" (roundtripNestedArray #[] == #[]) ++ + test "Nested array [[]]" (roundtripNestedArray #[#[]] == #[#[]]) ++ + test "Nested array [[1,2],[3]]" (roundtripNestedArray #[#[1, 2], #[3]] == #[#[1, 2], #[3]]) ++ + test "Nested array [[],[1],[2,3]]" (roundtripNestedArray #[#[], #[1], #[2, 3]] == #[#[], #[1], #[2, 3]]) ++ + test "Nested list empty" (roundtripNestedList [] == []) ++ + test "Nested list [[]]" (roundtripNestedList [[]] == [[]]) ++ + test "Nested list [[1,2],[3]]" (roundtripNestedList [[1, 2], [3]] == [[1, 2], [3]]) + +/-! ## Misc edge case tests -/ + +def edgeCaseTests : TestSeq := + -- List → Array via push + test "List to array empty" (listToArrayViaPush [] == #[]) ++ + test "List to array [1,2,3]" (listToArrayViaPush [1, 2, 3] == #[1, 2, 3]) ++ + test "List to array [0]" (listToArrayViaPush [0] == #[0]) ++ + -- borrow → owned (to_owned_ref / lean_inc) + test "Borrow to owned 0" (borrowToOwned 0 == 0) ++ + test "Borrow to owned 42" (borrowToOwned 42 == 42) ++ + test "Borrow to owned large" (borrowToOwned (2^128) == 2^128) ++ + -- Empty collection construction from Rust + test "Make empty array" (makeEmptyArray () == #[]) ++ + test "Make empty list" (makeEmptyList () == []) ++ + test "Make empty bytearray" (makeEmptyByteArray () == ⟨#[]⟩) ++ + test "Make empty string" (makeEmptyString () == "") ++ + -- Scalar/heap boundary for Nat + test "Nat max scalar" (natMaxScalar () == (2^63 - 1)) ++ + test "Nat min heap" (natMinHeap () == 2^63) + +/-! ## Persistent object tests -/ +-- Module-level `def` values become persistent after initialization (m_rc == 0). +-- These tests verify that borrowed access to persistent objects works correctly, +-- and that LeanOwned::drop is a no-op for persistent data. + +def persistentTests : TestSeq := + -- Reading persistent values as borrowed (no ref counting) + test "Read persistent Nat" (readPersistentNat persistentNat == 42) ++ + test "Read persistent large Nat" (readPersistentNat persistentLargeNat == 2^128) ++ + test "Read persistent Point" (readPersistentPoint persistentPoint == 30) ++ + test "Read persistent Array" (readPersistentArray persistentArray == 15) ++ + test "Read persistent String" (readPersistentString persistentString == 16) ++ + -- Dropping persistent values via owned arg (lean_dec is no-op for m_rc == 0) + test "Drop persistent Nat" (dropPersistentNat persistentNat == 42) ++ + test "Drop persistent large Nat" (dropPersistentNat persistentLargeNat == 2^128) ++ + -- Read the same persistent value multiple times (verifies it wasn't freed) + test "Persistent Nat stable 1" (readPersistentNat persistentNat == 42) ++ + test "Persistent Nat stable 2" (readPersistentNat persistentNat == 42) ++ + test "Persistent Array stable" (readPersistentArray persistentArray == 15) + /-! ## Property-based tests -/ -public def suite : List TestSeq := [ - simpleTests, - largeNatTests, - exceptTests, - ioResultTests, - scalarStructTests, - extScalarStructTests, - usizeStructTests, - externalTests, - checkIO "Nat roundtrip" (∀ n : Nat, roundtripNat n == n), - checkIO "String roundtrip" (∀ s : String, roundtripString s == s), - checkIO "List Nat roundtrip" (∀ xs : List Nat, roundtripListNat xs == xs), - checkIO "Array Nat roundtrip" (∀ arr : Array Nat, roundtripArrayNat arr == arr), - checkIO "ByteArray roundtrip" (∀ ba : ByteArray, roundtripByteArray ba == ba), - checkIO "Option Nat roundtrip" (∀ o : Option Nat, roundtripOptionNat o == o), - checkIO "Point roundtrip" (∀ p : Point, roundtripPoint p == p), - checkIO "NatTree roundtrip" (∀ t : NatTree, roundtripNatTree t == t), +/-! ## Suite organization -/ +-- Tests are grouped by what they exercise: +-- "borrowed" — @& args, no ref counting in Rust +-- "owned" — lean_obj_arg, LeanOwned Drop calls lean_dec +-- "clone" — lean_inc via Clone, then double lean_dec via Drop +-- "persistent" — m_rc == 0 objects (compact regions, module-level defs) +-- "property" — randomized property-based tests (SlimCheck) + +public def borrowedSuite : List TestSeq := [ + group "Roundtrip" (simpleTests ++ largeNatTests), + group "Except" exceptTests, + group "IO Result" ioResultTests, + group "Scalar structs" (scalarStructTests ++ extScalarStructTests ++ usizeStructTests), + group "External objects" externalTests, + group "Nested collections" nestedTests, + group "API helpers" (apiTests ++ dataSliceTests), + group "Edge cases" edgeCaseTests, +] + +public def ownedSuite : List TestSeq := [ + group "Drop" ownedArgTests, + group "Clone" cloneTests, +] + +public def persistentSuite : List TestSeq := [ + persistentTests, +] + +public def propertySuite : List TestSeq := [ + group "Borrowed roundtrip" ( + checkIO "Nat" (∀ n : Nat, roundtripNat n == n) ++ + checkIO "String" (∀ s : String, roundtripString s == s) ++ + checkIO "List Nat" (∀ xs : List Nat, roundtripListNat xs == xs) ++ + checkIO "Array Nat" (∀ arr : Array Nat, roundtripArrayNat arr == arr) ++ + checkIO "ByteArray" (∀ ba : ByteArray, roundtripByteArray ba == ba) ++ + checkIO "Option Nat" (∀ o : Option Nat, roundtripOptionNat o == o) ++ + checkIO "Point" (∀ p : Point, roundtripPoint p == p) ++ + checkIO "NatTree" (∀ t : NatTree, roundtripNatTree t == t) ++ + checkIO "Prod swap" (∀ p : Nat × Nat, prodSwap p == (p.2, p.1)) ++ + checkIO "Borrow to owned" (∀ n : Nat, borrowToOwned n == n)), + group "Owned Drop" ( + checkIO "Nat" (∀ n : Nat, ownedNatRoundtrip n == n) ++ + checkIO "String" (∀ s : String, ownedStringRoundtrip s == s) ++ + checkIO "Array Nat" (∀ arr : Array Nat, ownedArrayNatRoundtrip arr == arr) ++ + checkIO "List Nat" (∀ xs : List Nat, ownedListNatRoundtrip xs == xs) ++ + checkIO "ByteArray" (∀ ba : ByteArray, ownedByteArrayRoundtrip ba == ba) ++ + checkIO "Option Nat" (∀ o : Option Nat, ownedOptionRoundtrip o == o) ++ + checkIO "Prod" (∀ p : Nat × Nat, ownedProdRoundtrip p == p) ++ + checkIO "Prod multiply" (∀ p : Nat × Nat, ownedProdMultiply p == p.1 * p.2) ++ + checkIO "Option square" (∀ o : Option Nat, ownedOptionSquare o == match o with | some n => n * n | none => 0) ++ + checkIO "Except transform" (∀ e : Except String Nat, + ownedExceptTransform e == match e with | .ok n => 2 * n | .error s => s.utf8ByteSize)), + group "Clone + Drop" ( + checkIO "Except" (∀ e : Except String Nat, + cloneExcept e == match e with | .ok n => 2 * n | .error s => 2 * s.utf8ByteSize) ++ + checkIO "List" (∀ xs : List Nat, cloneList xs == 2 * xs.length) ++ + checkIO "ByteArray" (∀ ba : ByteArray, cloneByteArray ba == 2 * ba.size) ++ + checkIO "Option" (∀ o : Option Nat, + cloneOption o == match o with | some n => 2 * n | none => 0) ++ + checkIO "Prod" (∀ p : Nat × Nat, cloneProd p == 2 * (p.1 + p.2))), + group "Misc" ( + checkIO "Array data sum" (∀ arr : Array Nat, arrayDataSum arr == arr.toList.foldl (· + ·) 0) ++ + checkIO "List to array via push" (∀ xs : List Nat, listToArrayViaPush xs == xs.toArray)), ] end Tests.FFI diff --git a/test/Tests/Gen.lean b/test/Tests/Gen.lean index 193578b..5e8264f 100644 --- a/test/Tests/Gen.lean +++ b/test/Tests/Gen.lean @@ -157,6 +157,30 @@ instance : Shrinkable (Option Nat) where | none => [] | some n => none :: (Shrinkable.shrink n |>.map some) +def genProdNatNat : Gen (Nat × Nat) := do + let a ← genSmallNat + let b ← genSmallNat + pure (a, b) + +instance : Shrinkable (Nat × Nat) where + shrink p := if p.1 == 0 && p.2 == 0 then [] else [(p.1 / 2, p.2 / 2)] + +def genExceptStringNat : Gen (Except String Nat) := do + let b ← genBool + if b then .ok <$> genSmallNat + else .error <$> genString + +instance : BEq (Except String Nat) where + beq a b := match a, b with + | .ok x, .ok y => x == y + | .error x, .error y => x == y + | _, _ => false + +instance : Shrinkable (Except String Nat) where + shrink e := match e with + | .ok n => .ok 0 :: (Shrinkable.shrink n |>.map .ok) + | .error s => .ok 0 :: (Shrinkable.shrink s |>.map .error) + /-! ## SampleableExt instances -/ instance : SampleableExt Nat := SampleableExt.mkSelfContained genNat @@ -167,5 +191,7 @@ instance : SampleableExt String := SampleableExt.mkSelfContained genString instance : SampleableExt Point := SampleableExt.mkSelfContained genPoint instance : SampleableExt NatTree := SampleableExt.mkSelfContained (genNatTree 4) instance : SampleableExt (Option Nat) := SampleableExt.mkSelfContained genOptionNat +instance : SampleableExt (Nat × Nat) := SampleableExt.mkSelfContained genProdNatNat +instance : SampleableExt (Except String Nat) := SampleableExt.mkSelfContained genExceptStringNat end diff --git a/test/Tests/Main.lean b/test/Tests/Main.lean index 94cb8a9..e933ced 100644 --- a/test/Tests/Main.lean +++ b/test/Tests/Main.lean @@ -3,6 +3,9 @@ import Std.Data.HashMap def main (args : List String) : IO UInt32 := do let suites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ - ("ffi", Tests.FFI.suite), + ("borrowed", Tests.FFI.borrowedSuite), + ("owned", Tests.FFI.ownedSuite), + ("persistent", Tests.FFI.persistentSuite), + ("property", Tests.FFI.propertySuite), ] LSpec.lspecIO suites args diff --git a/test/lakefile.lean b/test/lakefile.lean index 670c0f2..1c7ef77 100644 --- a/test/lakefile.lean +++ b/test/lakefile.lean @@ -12,7 +12,6 @@ lean_lib Tests @[test_driver] lean_exe LeanFFITests where root := `Tests.Main - supportInterpreter := true section FFI @@ -23,3 +22,4 @@ extern_lib lean_ffi_rs pkg := do inputBinFile $ pkg.dir / ".." / "target" / "release" / libName end FFI + diff --git a/test/src/lib.rs b/test/src/lib.rs index 9df0208..35be48e 100644 --- a/test/src/lib.rs +++ b/test/src/lib.rs @@ -3,17 +3,40 @@ //! Each function decodes a Lean value to a Rust representation using lean-ffi, //! then re-encodes it back to a Lean value. The Lean test suite calls these via //! `@[extern]` and checks that the round-tripped value equals the original. +//! +//! All parameters use `@&` (borrowed) in the Lean declarations, so the Rust +//! side receives `LeanBorrowed<'_>` — no `lean_dec` on inputs. use std::sync::LazyLock; use lean_ffi::nat::Nat; use lean_ffi::object::{ - ExternalClass, LeanArray, LeanBool, LeanByteArray, LeanCtor, LeanExcept, LeanExternal, - LeanIOResult, LeanList, LeanNat, LeanObject, LeanOption, LeanProd, LeanString, + ExternalClass, LeanArray, LeanBool, LeanBorrowed, LeanByteArray, LeanCtor, LeanExcept, + LeanExternal, LeanIOResult, LeanList, LeanNat, LeanOption, LeanOwned, LeanProd, LeanRef, + LeanString, }; +// ============================================================================= +// Domain types for Lean structures +// ============================================================================= + +lean_ffi::lean_domain_type! { + /// Lean `Point` — structure Point where x : Nat; y : Nat + LeanPoint; + /// Lean `NatTree` — inductive NatTree | leaf : Nat → NatTree | node : NatTree → NatTree → NatTree + LeanNatTree; + /// Lean `ScalarStruct` — structure ScalarStruct where obj : Nat; u8val : UInt8; u32val : UInt32; u64val : UInt64 + LeanScalarStruct; + /// Lean `ExtScalarStruct` — all scalar types + LeanExtScalarStruct; + /// Lean `USizeStruct` — structure USizeStruct where obj : Nat; uval : USize; u8val : UInt8 + LeanUSizeStruct; + /// Lean `RustData` — opaque external object + LeanRustData; +} + /// Build a Lean Nat from a Rust Nat (delegates to `Nat::to_lean`). -fn build_nat(n: &Nat) -> LeanObject { +fn build_nat(n: &Nat) -> LeanOwned { n.to_lean().into() } @@ -23,36 +46,47 @@ fn build_nat(n: &Nat) -> LeanObject { /// Round-trip a Nat: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_nat(nat_ptr: LeanNat) -> LeanObject { - let nat = Nat::from_obj(*nat_ptr); - build_nat(&nat) +pub extern "C" fn rs_roundtrip_nat(nat_ptr: LeanNat>) -> LeanNat { + let nat = Nat::from_obj(nat_ptr.inner()); + nat.to_lean() } /// Round-trip a String: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_string(s_ptr: LeanString) -> LeanString { +pub extern "C" fn rs_roundtrip_string( + s_ptr: LeanString>, +) -> LeanString { let s = s_ptr.to_string(); LeanString::new(&s) } /// Round-trip a Bool: decode from Lean, re-encode. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_bool(bool_ptr: LeanBool) -> LeanBool { - bool_ptr +pub extern "C" fn rs_roundtrip_bool(bool_ptr: LeanBool>) -> LeanBool { + let val = bool_ptr.to_bool(); + if val { + LeanBool::new(LeanOwned::from_enum_tag(1)) + } else { + LeanBool::new(LeanOwned::from_enum_tag(0)) + } } /// Round-trip a List Nat: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_list_nat(list_ptr: LeanList) -> LeanList { - let nats: Vec = list_ptr.collect(Nat::from_obj); - let items: Vec = nats.iter().map(build_nat).collect(); +pub extern "C" fn rs_roundtrip_list_nat( + list_ptr: LeanList>, +) -> LeanList { + let nats: Vec = list_ptr.collect(|b| Nat::from_obj(&b)); + let items: Vec = nats.iter().map(build_nat).collect(); items.into_iter().collect() } /// Round-trip an Array Nat: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_nat(arr_ptr: LeanArray) -> LeanArray { - let nats: Vec = arr_ptr.map(Nat::from_obj); +pub extern "C" fn rs_roundtrip_array_nat( + arr_ptr: LeanArray>, +) -> LeanArray { + let nats: Vec = arr_ptr.map(|b| Nat::from_obj(&b)); let arr = LeanArray::alloc(nats.len()); for (i, nat) in nats.iter().enumerate() { arr.set(i, build_nat(nat)); @@ -62,57 +96,65 @@ pub extern "C" fn rs_roundtrip_array_nat(arr_ptr: LeanArray) -> LeanArray { /// Round-trip a ByteArray: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_bytearray(ba: LeanByteArray) -> LeanByteArray { +pub extern "C" fn rs_roundtrip_bytearray( + ba: LeanByteArray>, +) -> LeanByteArray { LeanByteArray::from_bytes(ba.as_bytes()) } /// Round-trip an Option Nat: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_option_nat(opt: LeanObject) -> LeanObject { - if opt.is_scalar() { - // none - LeanOption::none().into() +pub extern "C" fn rs_roundtrip_option_nat( + opt: LeanOption>, +) -> LeanOption { + if opt.inner().is_scalar() { + LeanOption::none() } else { - // some val - let nat = Nat::from_obj(opt.as_ctor().get(0)); - LeanOption::some(build_nat(&nat)).into() + let ctor = opt.as_ctor(); + let nat = Nat::from_obj(&ctor.get(0)); + LeanOption::some(build_nat(&nat)) } } /// Round-trip a Point (structure with x, y : Nat). #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_point(point_ptr: LeanCtor) -> LeanObject { - let x = Nat::from_obj(point_ptr.get(0)); - let y = Nat::from_obj(point_ptr.get(1)); - let point = LeanCtor::alloc(0, 2, 0); - point.set(0, build_nat(&x)); - point.set(1, build_nat(&y)); - *point +pub extern "C" fn rs_roundtrip_point( + point_ptr: LeanPoint>, +) -> LeanPoint { + let ctor = point_ptr.as_ctor(); + let x = Nat::from_obj(&ctor.get(0)); + let y = Nat::from_obj(&ctor.get(1)); + let out = LeanCtor::alloc(0, 2, 0); + out.set(0, build_nat(&x)); + out.set(1, build_nat(&y)); + LeanPoint::new(out.into()) } /// Round-trip a NatTree (inductive: leaf Nat | node NatTree NatTree). #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_nat_tree(tree_ptr: LeanCtor) -> LeanObject { - roundtrip_nat_tree_recursive(tree_ptr) +pub extern "C" fn rs_roundtrip_nat_tree( + tree_ptr: LeanNatTree>, +) -> LeanNatTree { + LeanNatTree::new(roundtrip_nat_tree_recursive(&tree_ptr.as_ctor())) } -fn roundtrip_nat_tree_recursive(ctor: LeanCtor) -> LeanObject { +fn roundtrip_nat_tree_recursive(ctor: &LeanCtor) -> LeanOwned { match ctor.tag() { 0 => { // leaf : Nat → NatTree - let nat = Nat::from_obj(ctor.get(0)); + let nat = Nat::from_obj(&ctor.get(0)); let leaf = LeanCtor::alloc(0, 1, 0); leaf.set(0, build_nat(&nat)); - *leaf + leaf.into() } 1 => { // node : NatTree → NatTree → NatTree - let left = roundtrip_nat_tree_recursive(ctor.get(0).as_ctor()); - let right = roundtrip_nat_tree_recursive(ctor.get(1).as_ctor()); + let left = roundtrip_nat_tree_recursive(&ctor.get(0).as_ctor()); + let right = roundtrip_nat_tree_recursive(&ctor.get(1).as_ctor()); let node = LeanCtor::alloc(1, 2, 0); node.set(0, left); node.set(1, right); - *node + node.into() } _ => panic!("Invalid NatTree tag: {}", ctor.tag()), } @@ -122,13 +164,14 @@ fn roundtrip_nat_tree_recursive(ctor: LeanCtor) -> LeanObject { // LeanProd roundtrip // ============================================================================= -/// Round-trip a Prod Nat Nat: decode fst/snd via LeanCtor, re-encode via LeanProd::new. +/// Round-trip a Prod Nat Nat: decode fst/snd, re-encode via LeanProd::new. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_prod_nat_nat(pair: LeanObject) -> LeanObject { - let ctor = pair.as_ctor(); - let fst = Nat::from_obj(ctor.get(0)); - let snd = Nat::from_obj(ctor.get(1)); - LeanProd::new(build_nat(&fst), build_nat(&snd)).into() +pub extern "C" fn rs_roundtrip_prod_nat_nat( + pair: LeanProd>, +) -> LeanProd { + let fst = Nat::from_obj(&pair.fst()); + let snd = Nat::from_obj(&pair.snd()); + LeanProd::new(build_nat(&fst), build_nat(&snd)) } // ============================================================================= @@ -137,29 +180,25 @@ pub extern "C" fn rs_roundtrip_prod_nat_nat(pair: LeanObject) -> LeanObject { /// Round-trip an Except String Nat: decode ok/error, re-encode. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_except_string_nat(exc: LeanObject) -> LeanObject { - let ctor = exc.as_ctor(); - match ctor.tag() { - 0 => { - // Except.error (tag 0): field 0 is the error String - let s = ctor.get(0).as_string(); - let msg = s.to_string(); - LeanExcept::error(LeanString::new(&msg)).into() +pub extern "C" fn rs_roundtrip_except_string_nat( + exc: LeanExcept>, +) -> LeanExcept { + match exc.into_result() { + Err(err) => { + let s = err.as_string(); + LeanExcept::error(LeanString::new(&s.to_string())) } - 1 => { - // Except.ok (tag 1): field 0 is the Nat value - let nat = Nat::from_obj(ctor.get(0)); - LeanExcept::ok(build_nat(&nat)).into() + Ok(val) => { + let nat = Nat::from_obj(&val); + LeanExcept::ok(build_nat(&nat)) } - _ => panic!("Invalid Except tag: {}", ctor.tag()), } } /// Build an Except.error from a Rust string (tests LeanExcept::error_string). #[unsafe(no_mangle)] -pub extern "C" fn rs_except_error_string(s: LeanString) -> LeanObject { - let msg = s.to_string(); - LeanExcept::error_string(&msg).into() +pub extern "C" fn rs_except_error_string(s: LeanString>) -> LeanExcept { + LeanExcept::error_string(&s.to_string()) } // ============================================================================= @@ -168,38 +207,44 @@ pub extern "C" fn rs_except_error_string(s: LeanString) -> LeanObject { /// Build a successful IO result wrapping a Nat (tests LeanIOResult::ok). #[unsafe(no_mangle)] -pub extern "C" fn rs_io_result_ok_nat(nat_ptr: LeanNat) -> LeanObject { - let nat = Nat::from_obj(*nat_ptr); - LeanIOResult::ok(build_nat(&nat)).into() +pub extern "C" fn rs_io_result_ok_nat( + nat_ptr: LeanNat>, +) -> LeanIOResult { + let nat = Nat::from_obj(nat_ptr.inner()); + LeanIOResult::ok(build_nat(&nat)) } /// Build an IO error from a string (tests LeanIOResult::error_string). #[unsafe(no_mangle)] -pub extern "C" fn rs_io_result_error_string(s: LeanString) -> LeanObject { - let msg = s.to_string(); - LeanIOResult::error_string(&msg).into() +pub extern "C" fn rs_io_result_error_string( + s: LeanString>, +) -> LeanIOResult { + LeanIOResult::error_string(&s.to_string()) } // ============================================================================= // LeanCtor scalar fields // ============================================================================= -/// Round-trip a ScalarStruct (structure with obj : Nat, u8val : UInt8, -/// u32val : UInt32, u64val : UInt64). -/// Layout: tag 0, 1 obj field, 13 scalar bytes (1 + 4 + 8, padded). +/// Round-trip a ScalarStruct. +/// Lean layout: 1 obj field, then scalars by descending size: u64(0), u32(8), u8(12). +/// Total scalar size: 8 + 4 + 1 = 13 bytes. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_scalar_struct(ptr: LeanCtor) -> LeanObject { - let obj_nat = Nat::from_obj(ptr.get(0)); - let u8val = ptr.scalar_u8(1, 0); - let u32val = ptr.scalar_u32(1, 1); - let u64val = ptr.scalar_u64(1, 5); +pub extern "C" fn rs_roundtrip_scalar_struct( + ptr: LeanScalarStruct>, +) -> LeanScalarStruct { + let ctor = ptr.as_ctor(); + let obj_nat = Nat::from_obj(&ctor.get(0)); + let u64val = ctor.get_u64(1, 0); + let u32val = ctor.get_u32(1, 8); + let u8val = ctor.get_u8(1, 12); - let ctor = LeanCtor::alloc(0, 1, 13); - ctor.set(0, build_nat(&obj_nat)); - ctor.set_scalar_u8(1, 0, u8val); - ctor.set_scalar_u32(1, 1, u32val); - ctor.set_scalar_u64(1, 5, u64val); - *ctor + let out = LeanCtor::alloc(0, 1, 13); + out.set(0, build_nat(&obj_nat)); + out.set_u64(1, 0, u64val); + out.set_u32(1, 8, u32val); + out.set_u8(1, 12, u8val); + LeanScalarStruct::new(out.into()) } // ============================================================================= @@ -218,28 +263,30 @@ pub extern "C" fn rs_roundtrip_uint64(val: u64) -> u64 { val } -/// Round-trip an Array UInt32. Elements are boxed lean_object* inside the -/// array, so this exercises LeanObject::box_u32 / unbox_u32. +/// Round-trip an Array UInt32. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_uint32(arr_ptr: LeanArray) -> LeanArray { +pub extern "C" fn rs_roundtrip_array_uint32( + arr_ptr: LeanArray>, +) -> LeanArray { let len = arr_ptr.len(); let new_arr = LeanArray::alloc(len); for i in 0..len { let val = arr_ptr.get(i).unbox_u32(); - new_arr.set(i, LeanObject::box_u32(val)); + new_arr.set(i, LeanOwned::box_u32(val)); } new_arr } -/// Round-trip an Array UInt64. Elements are boxed lean_object* inside the -/// array, so this exercises LeanObject::box_u64 / unbox_u64. +/// Round-trip an Array UInt64. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_uint64(arr_ptr: LeanArray) -> LeanArray { +pub extern "C" fn rs_roundtrip_array_uint64( + arr_ptr: LeanArray>, +) -> LeanArray { let len = arr_ptr.len(); let new_arr = LeanArray::alloc(len); for i in 0..len { let val = arr_ptr.get(i).unbox_u64(); - new_arr.set(i, LeanObject::box_u64(val)); + new_arr.set(i, LeanOwned::box_u64(val)); } new_arr } @@ -259,36 +306,46 @@ struct RustData { static RUST_DATA_CLASS: LazyLock = LazyLock::new(ExternalClass::register_with_drop::); -/// Create a LeanExternal from three Lean values (x : UInt64, y : UInt64, label : String). +/// Create a LeanExternal from three Lean values. +/// Note: label is @& (borrowed), x/y are scalar UInt64. #[unsafe(no_mangle)] -pub extern "C" fn rs_external_create(x: u64, y: u64, label: LeanString) -> LeanObject { +pub extern "C" fn rs_external_create( + x: u64, + y: u64, + label: LeanString>, +) -> LeanRustData { let data = RustData { x, y, label: label.to_string(), }; let ext = LeanExternal::alloc(&RUST_DATA_CLASS, data); - ext.into() + LeanRustData::new(ext.into()) } -/// Read the x field from a LeanExternal. +/// Read the x field from a LeanExternal (@& borrowed). #[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_x(obj: LeanObject) -> u64 { - let ext = unsafe { LeanExternal::::from_raw(obj.as_ptr()) }; +pub extern "C" fn rs_external_get_x(obj: LeanRustData>) -> u64 { + let ext = + unsafe { LeanExternal::>::from_raw_borrowed(obj.as_raw()) }; ext.get().x } -/// Read the y field from a LeanExternal. +/// Read the y field from a LeanExternal (@& borrowed). #[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_y(obj: LeanObject) -> u64 { - let ext = unsafe { LeanExternal::::from_raw(obj.as_ptr()) }; +pub extern "C" fn rs_external_get_y(obj: LeanRustData>) -> u64 { + let ext = + unsafe { LeanExternal::>::from_raw_borrowed(obj.as_raw()) }; ext.get().y } -/// Read the label field from a LeanExternal. +/// Read the label field from a LeanExternal (@& borrowed). #[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_label(obj: LeanObject) -> LeanString { - let ext = unsafe { LeanExternal::::from_raw(obj.as_ptr()) }; +pub extern "C" fn rs_external_get_label( + obj: LeanRustData>, +) -> LeanString { + let ext = + unsafe { LeanExternal::>::from_raw_borrowed(obj.as_raw()) }; LeanString::new(&ext.get().label) } @@ -296,58 +353,54 @@ pub extern "C" fn rs_external_get_label(obj: LeanObject) -> LeanString { // Extended scalar struct roundtrip (u8, u16, u32, u64, f64, f32) // ============================================================================= -/// Round-trip an ExtScalarStruct: -/// structure ExtScalarStruct where -/// obj : Nat; u8val : UInt8; u16val : UInt16 -/// u32val : UInt32; u64val : UInt64; fval : Float; f32val : Float32 -/// -/// Lean sorts scalar fields by descending size: -/// u64val at 0, fval(f64) at 8, u32val at 16, f32val at 20, u16val at 24, u8val at 26 -#[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_ext_scalar_struct(ptr: LeanCtor) -> LeanObject { - let obj_nat = Nat::from_obj(ptr.get(0)); - // Read in Lean's packed order: 8B, 4B, 2B, 1B - let u64val = ptr.scalar_u64(1, 0); - let fval = ptr.scalar_f64(1, 8); - let u32val = ptr.scalar_u32(1, 16); - let f32val = ptr.scalar_f32(1, 20); - let u16val = ptr.scalar_u16(1, 24); - let u8val = ptr.scalar_u8(1, 26); - - // scalar_size: 8 + 8 + 4 + 4 + 2 + 1 = 27 bytes - let ctor = LeanCtor::alloc(0, 1, 27); - ctor.set(0, build_nat(&obj_nat)); - ctor.set_scalar_u64(1, 0, u64val); - ctor.set_scalar_f64(1, 8, fval); - ctor.set_scalar_u32(1, 16, u32val); - ctor.set_scalar_f32(1, 20, f32val); - ctor.set_scalar_u16(1, 24, u16val); - ctor.set_scalar_u8(1, 26, u8val); - *ctor +/// Round-trip an ExtScalarStruct. +/// Lean layout: 1 obj, then descending size: u64(0), f64(8), u32(16), f32(20), u16(24), u8(26). +/// Total scalar: 27 bytes. +#[unsafe(no_mangle)] +pub extern "C" fn rs_roundtrip_ext_scalar_struct( + ptr: LeanExtScalarStruct>, +) -> LeanExtScalarStruct { + let ctor = ptr.as_ctor(); + let obj_nat = Nat::from_obj(&ctor.get(0)); + let u64val = ctor.get_u64(1, 0); + let fval = ctor.get_f64(1, 8); + let u32val = ctor.get_u32(1, 16); + let f32val = ctor.get_f32(1, 20); + let u16val = ctor.get_u16(1, 24); + let u8val = ctor.get_u8(1, 26); + + let out = LeanCtor::alloc(0, 1, 27); + out.set(0, build_nat(&obj_nat)); + out.set_u64(1, 0, u64val); + out.set_f64(1, 8, fval); + out.set_u32(1, 16, u32val); + out.set_f32(1, 20, f32val); + out.set_u16(1, 24, u16val); + out.set_u8(1, 26, u8val); + LeanExtScalarStruct::new(out.into()) } // ============================================================================= // USize struct roundtrip // ============================================================================= -/// Round-trip a USizeStruct: -/// structure USizeStruct where -/// obj : Nat; uval : USize; u8val : UInt8 -/// -/// Layout: 1 obj field, then USize (slot 0), then u8 at byte offset -/// past the usize slot. +/// Round-trip a USizeStruct. +/// Lean layout: 1 obj field, then usize (slot 0), then u8 at scalar offset 0. +/// Alloc: num_objs=1, scalar_sz=9 (8 for usize slot + 1 for u8). #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_usize_struct(ptr: LeanCtor) -> LeanObject { - let obj_nat = Nat::from_obj(ptr.get(0)); - let uval = ptr.scalar_usize(1, 0); - // u8val is after the usize slot: 1 usize slot = 8 bytes on 64-bit - let u8val = ptr.scalar_u8(1, 8); +pub extern "C" fn rs_roundtrip_usize_struct( + ptr: LeanUSizeStruct>, +) -> LeanUSizeStruct { + let ctor = ptr.as_ctor(); + let obj_nat = Nat::from_obj(&ctor.get(0)); + let uval = ctor.get_usize(1, 0); + let u8val = ctor.get_u8(2, 0); - let ctor = LeanCtor::alloc(0, 1, 16); // 8 (usize) + 1 (u8) padded - ctor.set(0, build_nat(&obj_nat)); - ctor.set_scalar_usize(1, 0, uval); - ctor.set_scalar_u8(1, 8, u8val); - *ctor + let out = LeanCtor::alloc(0, 1, 9); + out.set(0, build_nat(&obj_nat)); + out.set_usize(1, 0, uval); + out.set_u8(2, 0, u8val); + LeanUSizeStruct::new(out.into()) } // ============================================================================= @@ -372,26 +425,30 @@ pub extern "C" fn rs_roundtrip_usize(val: usize) -> usize { val } -/// Round-trip an Array Float. Elements are boxed f64 inside the array. +/// Round-trip an Array Float. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_float(arr_ptr: LeanArray) -> LeanArray { +pub extern "C" fn rs_roundtrip_array_float( + arr_ptr: LeanArray>, +) -> LeanArray { let len = arr_ptr.len(); let new_arr = LeanArray::alloc(len); for i in 0..len { let val = arr_ptr.get(i).unbox_f64(); - new_arr.set(i, LeanObject::box_f64(val)); + new_arr.set(i, LeanOwned::box_f64(val)); } new_arr } -/// Round-trip an Array Float32. Elements are boxed f32 inside the array. +/// Round-trip an Array Float32. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_float32(arr_ptr: LeanArray) -> LeanArray { +pub extern "C" fn rs_roundtrip_array_float32( + arr_ptr: LeanArray>, +) -> LeanArray { let len = arr_ptr.len(); let new_arr = LeanArray::alloc(len); for i in 0..len { let val = arr_ptr.get(i).unbox_f32(); - new_arr.set(i, LeanObject::box_f32(val)); + new_arr.set(i, LeanOwned::box_f32(val)); } new_arr } @@ -402,7 +459,9 @@ pub extern "C" fn rs_roundtrip_array_float32(arr_ptr: LeanArray) -> LeanArray { /// Round-trip a String using LeanString::from_bytes instead of LeanString::new. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_string_from_bytes(s_ptr: LeanString) -> LeanString { +pub extern "C" fn rs_roundtrip_string_from_bytes( + s_ptr: LeanString>, +) -> LeanString { let s = s_ptr.to_string(); LeanString::from_bytes(s.as_bytes()) } @@ -413,11 +472,673 @@ pub extern "C" fn rs_roundtrip_string_from_bytes(s_ptr: LeanString) -> LeanStrin /// Round-trip an Array Nat by pushing each element into a new array. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_push(arr_ptr: LeanArray) -> LeanArray { - let nats: Vec = arr_ptr.map(Nat::from_obj); +pub extern "C" fn rs_roundtrip_array_push( + arr_ptr: LeanArray>, +) -> LeanArray { + let nats: Vec = arr_ptr.map(|b| Nat::from_obj(&b)); let mut arr = LeanArray::alloc(0); for nat in &nats { arr = arr.push(build_nat(nat)); } arr } + +// ============================================================================= +// Owned argument tests (NO @& — Lean transfers ownership, Rust must lean_dec) +// ============================================================================= + +/// Round-trip a Nat with owned arg (no @&). Tests that LeanOwned Drop correctly +/// calls lean_dec on the input without double-free or leak. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_nat_roundtrip(nat_ptr: LeanNat) -> LeanNat { + let nat = Nat::from_obj(nat_ptr.inner()); + nat.to_lean() + // nat_ptr drops here → lean_dec (correct for owned arg) +} + +/// Round-trip a String with owned arg. Tests LeanOwned Drop on strings. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_string_roundtrip(s_ptr: LeanString) -> LeanString { + let s = s_ptr.to_string(); + LeanString::new(&s) + // s_ptr drops here → lean_dec +} + +/// Round-trip an Array Nat with owned arg. Tests LeanOwned Drop on arrays. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_array_nat_roundtrip( + arr_ptr: LeanArray, +) -> LeanArray { + let nats: Vec = arr_ptr.map(|b| Nat::from_obj(&b)); + let arr = LeanArray::alloc(nats.len()); + for (i, nat) in nats.iter().enumerate() { + arr.set(i, build_nat(nat)); + } + arr + // arr_ptr drops here → lean_dec +} + +/// Round-trip a List Nat with owned arg. Tests LeanOwned Drop on lists. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_list_nat_roundtrip( + list_ptr: LeanList, +) -> LeanList { + let nats: Vec = list_ptr.collect(|b| Nat::from_obj(&b)); + let items: Vec = nats.iter().map(build_nat).collect(); + items.into_iter().collect() + // list_ptr drops here → lean_dec +} + +/// Two owned args: take an array and a nat (both owned), append nat to array. +/// Tests Drop on two owned args simultaneously. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_append_nat( + arr: LeanArray, + nat: LeanNat, +) -> LeanArray { + let n = Nat::from_obj(nat.inner()); + // arr is consumed by push (ownership transferred to lean_array_push) + arr.push(build_nat(&n)) + // nat drops here → lean_dec +} + +/// Owned arg that we explicitly drop early (by letting it go out of scope) +/// then return a completely new value. Tests that Drop runs at the right time. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_drop_and_replace(s: LeanString) -> LeanString { + let len = s.byte_len(); + drop(s); // explicit early drop → lean_dec + LeanString::new(&format!("replaced:{len}")) +} + +/// Three owned args: merge three lists into one. +/// Tests Drop on multiple owned args with complex ownership flow. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_merge_lists( + a: LeanList, + b: LeanList, + c: LeanList, +) -> LeanList { + let mut nats = Vec::new(); + for elem in a.iter() { + nats.push(Nat::from_obj(&elem)); + } + for elem in b.iter() { + nats.push(Nat::from_obj(&elem)); + } + for elem in c.iter() { + nats.push(Nat::from_obj(&elem)); + } + let items: Vec = nats.iter().map(build_nat).collect(); + items.into_iter().collect() + // a, b, c all drop here → lean_dec on each +} + +/// Owned ByteArray: reverse the bytes and return. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_reverse_bytearray( + ba: LeanByteArray, +) -> LeanByteArray { + let bytes = ba.as_bytes(); + let reversed: Vec = bytes.iter().rev().copied().collect(); + LeanByteArray::from_bytes(&reversed) + // ba drops here → lean_dec +} + +/// Owned Point (ctor): negate both fields (swap x and y + add them). +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_point_sum(point: LeanCtor) -> LeanNat { + let x = Nat::from_obj(&point.get(0)); + let y = Nat::from_obj(&point.get(1)); + Nat(x.0 + y.0).to_lean() + // point drops here → lean_dec +} + +/// Owned Except: if ok, double the nat; if error, return error string length. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_except_transform(exc: LeanExcept) -> LeanNat { + match exc.into_result() { + Ok(val) => { + let nat = Nat::from_obj(&val); + Nat(nat.0.clone() + nat.0).to_lean() + } + Err(err) => { + let s = err.as_string(); + Nat::from(s.byte_len() as u64).to_lean() + } + } + // exc drops here → lean_dec +} + +/// Owned Option: if some(n), return n*n; if none, return 0. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_option_square(opt: LeanOption) -> LeanNat { + if opt.inner().is_scalar() { + Nat::ZERO.to_lean() + } else { + let val = opt.to_option().unwrap(); + let nat = Nat::from_obj(&val); + Nat(nat.0.clone() * nat.0).to_lean() + } +} + +/// Owned Prod: return fst * snd. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_prod_multiply(pair: LeanProd) -> LeanNat { + let fst = Nat::from_obj(&pair.fst()); + let snd = Nat::from_obj(&pair.snd()); + Nat(fst.0 * snd.0).to_lean() +} + +/// Owned ScalarStruct: sum all scalar fields. +/// ScalarStruct { obj : Nat, u8val : UInt8, u32val : UInt32, u64val : UInt64 } +/// Lean reorders scalar fields by descending size: +/// u64val at scalar offset 0, u32val at offset 8, u8val at offset 12 +/// Note: roundtrip tests use declaration-order offsets (0, 1, 5) which happen +/// to roundtrip correctly because both read and write use the same offsets. +/// But for computing actual values, we must use the real layout. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_scalar_sum(ptr: LeanScalarStruct) -> u64 { + // Lean descending-size layout: u64(0), u32(8), u8(12) + let ctor = ptr.as_ctor(); + let u64val = ctor.get_u64(1, 0); + let u32val = ctor.get_u32(1, 8) as u64; + let u8val = ctor.get_u8(1, 12) as u64; + u64val + u32val + u8val + // ptr drops here → lean_dec +} + +// ============================================================================= +// Clone tests — verify lean_inc is called correctly +// ============================================================================= + +/// Clone an owned array and return the sum of lengths of both copies. +/// Tests that Clone (lean_inc) produces a valid second handle. +#[unsafe(no_mangle)] +pub extern "C" fn rs_clone_array_len_sum(arr_ptr: LeanArray>) -> usize { + // Create an owned copy, then clone it + let owned: LeanArray = { + let nats: Vec = arr_ptr.map(|b| Nat::from_obj(&b)); + let arr = LeanArray::alloc(nats.len()); + for (i, nat) in nats.iter().enumerate() { + arr.set(i, build_nat(nat)); + } + arr + }; + let cloned = owned.clone(); + let sum = owned.len() + cloned.len(); + // Both owned and cloned drop here → lean_dec called twice (correct: clone did lean_inc) + sum +} + +/// Clone an owned string and return the sum of byte lengths of both copies. +#[unsafe(no_mangle)] +pub extern "C" fn rs_clone_string_len_sum(s: LeanString>) -> usize { + let owned = LeanString::new(&s.to_string()); + let cloned = owned.clone(); + let sum = owned.byte_len() + cloned.byte_len(); + sum +} + +/// Clone an owned Except and read from both copies. Tests that lean_inc +/// produces a valid second handle for constructor objects, and that both +/// copies can be independently dropped (lean_dec) without double-free. +/// Returns: for ok(n), 2*n (read n from both copies); for error(s), 2*byte_len. +#[unsafe(no_mangle)] +pub extern "C" fn rs_clone_except(exc: LeanExcept) -> LeanNat { + let cloned = exc.clone(); + let result = match (exc.into_result(), cloned.into_result()) { + (Ok(v1), Ok(v2)) => Nat(Nat::from_obj(&v1).0 + Nat::from_obj(&v2).0), + (Err(e1), Err(e2)) => { + let s1 = e1.as_string(); + let s2 = e2.as_string(); + Nat::from((s1.byte_len() + s2.byte_len()) as u64) + } + _ => panic!("clone changed the tag"), + }; + result.to_lean() +} + +/// Clone an owned List, count elements in both copies. Tests lean_inc on list spine. +#[unsafe(no_mangle)] +pub extern "C" fn rs_clone_list(list: LeanList) -> LeanNat { + let cloned = list.clone(); + let count1 = list.iter().count(); + let count2 = cloned.iter().count(); + Nat::from((count1 + count2) as u64).to_lean() +} + +/// Clone an owned ByteArray, sum byte lengths of both. Tests lean_inc on scalar arrays. +#[unsafe(no_mangle)] +pub extern "C" fn rs_clone_bytearray(ba: LeanByteArray) -> LeanNat { + let cloned = ba.clone(); + Nat::from((ba.len() + cloned.len()) as u64).to_lean() +} + +/// Clone an owned Option Nat: if some(n), return 2*n from both copies; if none, return 0. +#[unsafe(no_mangle)] +pub extern "C" fn rs_clone_option(opt: LeanOption) -> LeanNat { + let cloned = opt.clone(); + let result = match (opt.to_option(), cloned.to_option()) { + (Some(v1), Some(v2)) => Nat(Nat::from_obj(&v1).0 + Nat::from_obj(&v2).0), + (None, None) => Nat::ZERO, + _ => panic!("clone changed some/none"), + }; + result.to_lean() +} + +/// Clone an owned Prod, return fst1+fst2+snd1+snd2 from both copies. +#[unsafe(no_mangle)] +pub extern "C" fn rs_clone_prod(pair: LeanProd) -> LeanNat { + let cloned = pair.clone(); + let sum = Nat::from_obj(&pair.fst()).0 + + Nat::from_obj(&pair.snd()).0 + + Nat::from_obj(&cloned.fst()).0 + + Nat::from_obj(&cloned.snd()).0; + Nat(sum).to_lean() +} + +/// Owned ByteArray roundtrip: read bytes, rebuild. Tests LeanOwned Drop on scalar arrays. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_bytearray_roundtrip( + ba: LeanByteArray, +) -> LeanByteArray { + LeanByteArray::from_bytes(ba.as_bytes()) + // ba drops → lean_dec +} + +/// Owned Option roundtrip: decode and re-encode. Tests Drop on Option constructor. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_option_roundtrip(opt: LeanOption) -> LeanOption { + match opt.to_option() { + None => LeanOption::none(), + Some(val) => LeanOption::some(Nat::from_obj(&val).to_lean()), + } +} + +/// Owned Prod roundtrip: decode fst/snd, rebuild. Tests Drop on Prod constructor. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_prod_roundtrip(pair: LeanProd) -> LeanProd { + let f = Nat::from_obj(&pair.fst()); + let s = Nat::from_obj(&pair.snd()); + LeanProd::new(build_nat(&f), build_nat(&s)) +} + +/// Owned IOResult: extract value from ok result, return it. Tests Drop on IOResult. +#[unsafe(no_mangle)] +pub extern "C" fn rs_owned_io_result_value(result: LeanIOResult) -> LeanNat { + // IOResult ok = tag 0, fields: [value, world]; error = tag 1 + let ctor = result.as_ctor(); + if ctor.tag() == 0 { + Nat::from_obj(&ctor.get(0)).to_lean() + } else { + Nat::ZERO.to_lean() + } +} + +// ============================================================================= +// data() slice API tests +// ============================================================================= + +/// Sum all Nats in an array using the data() slice API. +#[unsafe(no_mangle)] +pub extern "C" fn rs_array_data_sum(arr_ptr: LeanArray>) -> LeanNat { + let mut sum = Nat::ZERO; + for elem in arr_ptr.data() { + sum = Nat(sum.0 + Nat::from_obj(elem).0); + } + sum.to_lean() +} + +// ============================================================================= +// LeanOption API tests +// ============================================================================= + +/// Test LeanOption API: return the Nat inside a Some, or 0 for None. +#[unsafe(no_mangle)] +pub extern "C" fn rs_option_unwrap_or_zero( + opt: LeanOption>, +) -> LeanNat { + match opt.to_option() { + None => Nat::ZERO.to_lean(), + Some(val) => Nat::from_obj(&val).to_lean(), + } +} + +// ============================================================================= +// LeanProd API tests +// ============================================================================= + +/// Test LeanProd fst/snd API: swap the elements of a pair. +#[unsafe(no_mangle)] +pub extern "C" fn rs_prod_swap(pair: LeanProd>) -> LeanProd { + let fst = Nat::from_obj(&pair.fst()); + let snd = Nat::from_obj(&pair.snd()); + LeanProd::new(build_nat(&snd), build_nat(&fst)) +} + +// ============================================================================= +// Borrowed result (b_lean_obj_res) internal tests +// ============================================================================= +// These test the internal pattern where methods return LeanBorrowed<'_> — the +// Rust equivalent of b_lean_obj_res. The borrowed reference is tied to the +// parent object's lifetime, so it cannot outlive the source. + +/// Helper: takes a borrowed Prod and returns a borrowed ref to its first element. +/// This is the b_lean_obj_res pattern — returning a reference into an existing object. +fn borrow_fst<'a>(pair: &'a LeanProd) -> LeanBorrowed<'a> { + pair.fst() +} + +/// Helper: takes a borrowed Prod and returns a borrowed ref to its second element. +fn borrow_snd<'a>(pair: &'a LeanProd) -> LeanBorrowed<'a> { + pair.snd() +} + +/// Helper: takes a borrowed array and returns a borrowed ref to element i. +fn borrow_array_elem<'a>(arr: &'a LeanArray, i: usize) -> LeanBorrowed<'a> { + arr.get(i) +} + +/// Helper: takes a borrowed Except and returns a borrowed ref to the inner value. +fn borrow_except_value<'a>(exc: &'a LeanExcept) -> LeanBorrowed<'a> { + match exc.into_result() { + Ok(val) => val, + Err(err) => err, + } +} + +/// Test that chains borrowed results through multiple internal functions. +/// Receives a Prod (Array Nat, Array Nat), borrows fst and snd, then borrows +/// elements from each array, and sums everything — all without any lean_inc. +#[unsafe(no_mangle)] +pub extern "C" fn rs_borrowed_result_chain(pair: LeanProd>) -> LeanNat { + // Get borrowed references to the two arrays (b_lean_obj_res pattern) + let fst_ref = borrow_fst(&pair); + let snd_ref = borrow_snd(&pair); + + // Interpret as arrays (still borrowed, no ref counting) + let arr1 = fst_ref.as_array(); + let arr2 = snd_ref.as_array(); + + // Borrow individual elements from each array (chained b_lean_obj_res) + let mut sum = Nat::ZERO; + for i in 0..arr1.len() { + let elem = borrow_array_elem(&arr1, i); + sum = Nat(sum.0 + Nat::from_obj(&elem).0); + } + for i in 0..arr2.len() { + let elem = borrow_array_elem(&arr2, i); + sum = Nat(sum.0 + Nat::from_obj(&elem).0); + } + + // Also access via data() slice — another b_lean_obj_res pattern + // (data() returns &[LeanBorrowed] tied to the array's lifetime) + let mut sum2 = Nat::ZERO; + for elem in arr1.data() { + sum2 = Nat(sum2.0 + Nat::from_obj(elem).0); + } + for elem in arr2.data() { + sum2 = Nat(sum2.0 + Nat::from_obj(elem).0); + } + + assert!(sum == sum2, "get() and data() must agree"); + sum.to_lean() +} + +/// Test borrowed result from Except. Borrows the inner value without lean_inc, +/// reads it, and returns a new owned Nat. +#[unsafe(no_mangle)] +pub extern "C" fn rs_borrowed_except_value( + exc: LeanExcept>, +) -> LeanNat { + let val = borrow_except_value(&exc); + if exc.is_ok() { + Nat::from_obj(&val).to_lean() + } else { + let s = val.as_string(); + Nat::from(s.byte_len() as u64).to_lean() + } +} + +// ============================================================================= +// Nested collection tests +// ============================================================================= + +/// Round-trip an Array (Array Nat) — tests nested ownership. +#[unsafe(no_mangle)] +pub extern "C" fn rs_roundtrip_nested_array( + outer: LeanArray>, +) -> LeanArray { + let len = outer.len(); + let result = LeanArray::alloc(len); + for i in 0..len { + let inner_ref = outer.get(i); + // inner_ref is a LeanBorrowed pointing to an inner Array + let inner_arr = inner_ref.as_array(); + let inner_len = inner_arr.len(); + let new_inner = LeanArray::alloc(inner_len); + for j in 0..inner_len { + let nat = Nat::from_obj(&inner_arr.get(j)); + new_inner.set(j, build_nat(&nat)); + } + result.set(i, new_inner); + } + result +} + +/// Round-trip a List (List Nat) — tests nested list iteration. +#[unsafe(no_mangle)] +pub extern "C" fn rs_roundtrip_nested_list( + outer: LeanList>, +) -> LeanList { + let inner_lists: Vec> = outer.collect(|inner_ref| { + let inner_list = inner_ref.as_list(); + let nats: Vec = inner_list.collect(|b| Nat::from_obj(&b)); + let items: Vec = nats.iter().map(build_nat).collect(); + items.into_iter().collect() + }); + inner_lists.into_iter().collect() +} + +// ============================================================================= +// LeanExcept into_result API test +// ============================================================================= + +/// Test LeanExcept-like pattern: if ok (tag 1), return nat + 1; if error (tag 0), return 0. +#[unsafe(no_mangle)] +pub extern "C" fn rs_except_map_ok(exc: LeanExcept>) -> LeanNat { + let ctor = exc.as_ctor(); + if ctor.tag() == 1 { + // ok: field 0 is the Nat value + let nat = Nat::from_obj(&ctor.get(0)); + Nat(nat.0 + 1u64).to_lean() + } else { + // error + Nat::ZERO.to_lean() + } +} + +// ============================================================================= +// Multiple borrow test — read many elements from same borrowed source +// ============================================================================= + +/// Read all elements from a borrowed array, compute sum. +/// Tests that multiple borrows from the same source don't interfere. +#[unsafe(no_mangle)] +pub extern "C" fn rs_multi_borrow_sum(arr: LeanArray>) -> LeanNat { + let mut sum = Nat::ZERO; + // First pass: read all via get() + for i in 0..arr.len() { + let elem = arr.get(i); + sum = Nat(sum.0 + Nat::from_obj(&elem).0); + } + // Second pass: read all via data() slice + let mut sum2 = Nat::ZERO; + for elem in arr.data() { + sum2 = Nat(sum2.0 + Nat::from_obj(elem).0); + } + // Third pass: read via iter() + let mut sum3 = Nat::ZERO; + for elem in arr.iter() { + sum3 = Nat(sum3.0 + Nat::from_obj(&elem).0); + } + assert!( + sum == sum2 && sum2 == sum3, + "All three iteration methods must agree" + ); + sum.to_lean() +} + +// ============================================================================= +// Build array from list using push — exercises ownership transfer chain +// ============================================================================= + +/// Convert List Nat → Array Nat using only push (not alloc+set). +#[unsafe(no_mangle)] +pub extern "C" fn rs_list_to_array_via_push( + list: LeanList>, +) -> LeanArray { + let mut arr = LeanArray::alloc(0); + for elem in list.iter() { + let nat = Nat::from_obj(&elem); + arr = arr.push(build_nat(&nat)); + } + arr +} + +// ============================================================================= +// to_owned_ref test — convert borrowed to owned explicitly +// ============================================================================= + +/// Take a borrowed Nat, convert to owned via to_owned_ref, return it. +/// Tests that to_owned_ref (lean_inc) produces a valid owned handle. +#[unsafe(no_mangle)] +pub extern "C" fn rs_borrow_to_owned(nat: LeanNat>) -> LeanNat { + LeanNat::new(nat.inner().to_owned_ref()) +} + +// ============================================================================= +// Empty collection edge cases +// ============================================================================= + +/// Create and return an empty array. Unit is passed as lean_box(0). +#[unsafe(no_mangle)] +pub extern "C" fn rs_make_empty_array(_unit: LeanBorrowed<'_>) -> LeanArray { + LeanArray::alloc(0) +} + +/// Create and return an empty list. +#[unsafe(no_mangle)] +pub extern "C" fn rs_make_empty_list(_unit: LeanBorrowed<'_>) -> LeanList { + LeanList::nil() +} + +/// Create and return an empty byte array. +#[unsafe(no_mangle)] +pub extern "C" fn rs_make_empty_bytearray(_unit: LeanBorrowed<'_>) -> LeanByteArray { + LeanByteArray::alloc(0) +} + +/// Create and return an empty string. +#[unsafe(no_mangle)] +pub extern "C" fn rs_make_empty_string(_unit: LeanBorrowed<'_>) -> LeanString { + LeanString::new("") +} + +// ============================================================================= +// Scalar boundary values +// ============================================================================= + +/// Return the Nat boundary between scalar and heap representation. +/// On 64-bit: usize::MAX >> 1 = 2^63 - 1 +#[unsafe(no_mangle)] +pub extern "C" fn rs_nat_max_scalar(_unit: LeanBorrowed<'_>) -> LeanNat { + let max_scalar = usize::MAX >> 1; + LeanNat::new(LeanOwned::box_usize(max_scalar)) +} + +/// Return max_scalar + 1 which must be heap-allocated. +#[unsafe(no_mangle)] +pub extern "C" fn rs_nat_min_heap(_unit: LeanBorrowed<'_>) -> LeanNat { + let max_scalar = (usize::MAX >> 1) as u64; + Nat::from(max_scalar + 1).to_lean() +} + +// ============================================================================= +// External object: multiple field reads from same borrowed handle +// ============================================================================= + +/// Read all fields from a single borrowed external handle and return as a string. +/// Tests that multiple reads from a borrowed external don't corrupt state. +#[unsafe(no_mangle)] +pub extern "C" fn rs_external_all_fields( + obj: LeanRustData>, +) -> LeanString { + let ext = + unsafe { LeanExternal::>::from_raw_borrowed(obj.as_raw()) }; + let result = format!("{}:{}:{}", ext.get().x, ext.get().y, ext.get().label); + LeanString::new(&result) +} + +// ============================================================================= +// Persistent / compact region tests +// ============================================================================= +// Persistent objects have m_rc == 0 and are never deallocated. They arise from +// module-level definitions and compact regions. Borrowed references to them +// work normally; the key invariant is that lean_inc/lean_dec are no-ops. + +/// Check if a borrowed Lean object is persistent (m_rc == 0). +/// Module-level Lean definitions become persistent after initialization. +#[unsafe(no_mangle)] +pub extern "C" fn rs_is_persistent(obj: LeanNat>) -> u8 { + if obj.inner().is_persistent() { 1 } else { 0 } +} + +/// Read a Nat from a persistent object (passed as @& borrowed). +/// Tests that field access works normally on persistent objects. +#[unsafe(no_mangle)] +pub extern "C" fn rs_read_persistent_nat(obj: LeanNat>) -> LeanNat { + let nat = Nat::from_obj(obj.inner()); + nat.to_lean() +} + +/// Read fields from a persistent LeanPoint (structure with x, y : Nat). +/// Tests that ctor field access works on persistent objects. +#[unsafe(no_mangle)] +pub extern "C" fn rs_read_persistent_point( + point: LeanPoint>, +) -> LeanNat { + let ctor = point.as_ctor(); + let x = Nat::from_obj(&ctor.get(0)); + let y = Nat::from_obj(&ctor.get(1)); + // Return x + y as a new (non-persistent) Nat + Nat(x.0 + y.0).to_lean().into() +} + +/// Read from a persistent array. Tests that array element access works +/// on persistent objects (elements in persistent arrays are also persistent). +#[unsafe(no_mangle)] +pub extern "C" fn rs_read_persistent_array(arr: LeanArray>) -> LeanNat { + let mut sum = Nat::ZERO; + for elem in arr.iter() { + sum = Nat(sum.0 + Nat::from_obj(&elem).0); + } + sum.to_lean() +} + +/// Read from a persistent string. Tests that string access works on persistent objects. +#[unsafe(no_mangle)] +pub extern "C" fn rs_read_persistent_string(s: LeanString>) -> LeanNat { + Nat::from(s.byte_len() as u64).to_lean() +} + +/// Receive a persistent object as owned (lean_obj_arg). Lean transfers a +/// "virtual RC token" but lean_dec is a no-op for persistent objects (m_rc == 0). +/// This tests that LeanOwned::drop doesn't crash on persistent data. +#[unsafe(no_mangle)] +pub extern "C" fn rs_drop_persistent_nat(obj: LeanNat) -> LeanNat { + let nat = Nat::from_obj(obj.inner()); + nat.to_lean() + // obj drops here → lean_dec_ref → no-op because m_rc == 0 +} From 5f7b491c5decdb0c9b13dcaeaa5cc36c8250eebc Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 19 Mar 2026 22:04:25 -0400 Subject: [PATCH 02/10] chore: Move tests to top level --- Cargo.lock | 7 - Cargo.toml | 15 +- test/Tests.lean => Tests.lean | 0 {test/Tests => Tests}/FFI.lean | 0 {test/Tests => Tests}/Gen.lean | 0 {test/Tests => Tests}/Main.lean | 0 test/lake-manifest.json => lake-manifest.json | 0 lakefile.lean | 28 ++ src/lib.rs | 3 + test/src/lib.rs => src/test_ffi.rs | 6 +- test/Cargo.lock | 287 ------------------ test/Cargo.toml | 16 - test/lakefile.lean | 25 -- test/lean-toolchain | 1 - 14 files changed, 46 insertions(+), 342 deletions(-) rename test/Tests.lean => Tests.lean (100%) rename {test/Tests => Tests}/FFI.lean (100%) rename {test/Tests => Tests}/Gen.lean (100%) rename {test/Tests => Tests}/Main.lean (100%) rename test/lake-manifest.json => lake-manifest.json (100%) create mode 100644 lakefile.lean rename test/src/lib.rs => src/test_ffi.rs (99%) delete mode 100644 test/Cargo.lock delete mode 100644 test/Cargo.toml delete mode 100644 test/lakefile.lean delete mode 100644 test/lean-toolchain diff --git a/Cargo.lock b/Cargo.lock index 8b438af..260668b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -115,13 +115,6 @@ dependencies = [ "num-bigint", ] -[[package]] -name = "lean-ffi-rs" -version = "0.1.0" -dependencies = [ - "lean-ffi", -] - [[package]] name = "libc" version = "0.2.183" diff --git a/Cargo.toml b/Cargo.toml index a48f3a8..71ea9b0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,14 +1,23 @@ -[workspace] -members = ["test"] - [package] name = "lean-ffi" version = "0.1.0" edition = "2024" +[lib] +crate-type = ["lib", "staticlib"] + +[features] +test-ffi = [] + [dependencies] num-bigint = "0.4.6" [build-dependencies] bindgen = "0.72" cc = "1" + +[profile.dev] +panic = "abort" + +[profile.release] +panic = "abort" diff --git a/test/Tests.lean b/Tests.lean similarity index 100% rename from test/Tests.lean rename to Tests.lean diff --git a/test/Tests/FFI.lean b/Tests/FFI.lean similarity index 100% rename from test/Tests/FFI.lean rename to Tests/FFI.lean diff --git a/test/Tests/Gen.lean b/Tests/Gen.lean similarity index 100% rename from test/Tests/Gen.lean rename to Tests/Gen.lean diff --git a/test/Tests/Main.lean b/Tests/Main.lean similarity index 100% rename from test/Tests/Main.lean rename to Tests/Main.lean diff --git a/test/lake-manifest.json b/lake-manifest.json similarity index 100% rename from test/lake-manifest.json rename to lake-manifest.json diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..8314a7c --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,28 @@ +import Lake +open System Lake DSL + +package «lean-ffi-test» where + version := v!"0.1.0" + +require LSpec from git + "https://github.com/argumentcomputer/LSpec" @ "928f27c7de8318455ba0be7461dbdf7096f4075a" + +section FFI + +/-- Build the static lib for the Rust FFI test crate -/ +target ffi_rs_test pkg : FilePath := do + proc { cmd := "cargo", args := #["build", "--release", "--features", "test-ffi"], cwd := pkg.dir } (quiet := true) + let srcName := nameToStaticLib "lean_ffi" + let dstName := nameToStaticLib "lean_ffi_test" + let releaseDir := pkg.dir / "target" / "release" + proc { cmd := "cp", args := #["-f", srcName, dstName], cwd := releaseDir } + inputBinFile $ releaseDir / dstName + +end FFI + +lean_lib Tests where + moreLinkObjs := #[ffi_rs_test] + +@[test_driver] +lean_exe LeanFFITests where + root := `Tests.Main diff --git a/src/lib.rs b/src/lib.rs index 416e943..e2baa15 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -23,6 +23,9 @@ pub mod include { pub mod nat; pub mod object; +#[cfg(feature = "test-ffi")] +mod test_ffi; + use std::ffi::{CString, c_void}; /// Create a CString from a str, stripping any interior null bytes. diff --git a/test/src/lib.rs b/src/test_ffi.rs similarity index 99% rename from test/src/lib.rs rename to src/test_ffi.rs index 35be48e..bd92b52 100644 --- a/test/src/lib.rs +++ b/src/test_ffi.rs @@ -9,8 +9,8 @@ use std::sync::LazyLock; -use lean_ffi::nat::Nat; -use lean_ffi::object::{ +use crate::nat::Nat; +use crate::object::{ ExternalClass, LeanArray, LeanBool, LeanBorrowed, LeanByteArray, LeanCtor, LeanExcept, LeanExternal, LeanIOResult, LeanList, LeanNat, LeanOption, LeanOwned, LeanProd, LeanRef, LeanString, @@ -20,7 +20,7 @@ use lean_ffi::object::{ // Domain types for Lean structures // ============================================================================= -lean_ffi::lean_domain_type! { +crate::lean_domain_type! { /// Lean `Point` — structure Point where x : Nat; y : Nat LeanPoint; /// Lean `NatTree` — inductive NatTree | leaf : Nat → NatTree | node : NatTree → NatTree → NatTree diff --git a/test/Cargo.lock b/test/Cargo.lock deleted file mode 100644 index d09db39..0000000 --- a/test/Cargo.lock +++ /dev/null @@ -1,287 +0,0 @@ -# This file is automatically @generated by Cargo. -# It is not intended for manual editing. -version = 4 - -[[package]] -name = "aho-corasick" -version = "1.1.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ddd31a130427c27518df266943a5308ed92d4b226cc639f5a8f1002816174301" -dependencies = [ - "memchr", -] - -[[package]] -name = "autocfg" -version = "1.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" - -[[package]] -name = "bindgen" -version = "0.71.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5f58bf3d7db68cfbac37cfc485a8d711e87e064c3d0fe0435b92f7a407f9d6b3" -dependencies = [ - "bitflags", - "cexpr", - "clang-sys", - "itertools", - "log", - "prettyplease", - "proc-macro2", - "quote", - "regex", - "rustc-hash", - "shlex", - "syn", -] - -[[package]] -name = "bitflags" -version = "2.11.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "843867be96c8daad0d758b57df9392b6d8d271134fce549de6ce169ff98a92af" - -[[package]] -name = "cc" -version = "1.2.56" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aebf35691d1bfb0ac386a69bac2fde4dd276fb618cf8bf4f5318fe285e821bb2" -dependencies = [ - "find-msvc-tools", - "shlex", -] - -[[package]] -name = "cexpr" -version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766" -dependencies = [ - "nom", -] - -[[package]] -name = "cfg-if" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" - -[[package]] -name = "clang-sys" -version = "1.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b023947811758c97c59bf9d1c188fd619ad4718dcaa767947df1cadb14f39f4" -dependencies = [ - "glob", - "libc", - "libloading", -] - -[[package]] -name = "either" -version = "1.15.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" - -[[package]] -name = "find-msvc-tools" -version = "0.1.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5baebc0774151f905a1a2cc41989300b1e6fbb29aff0ceffa1064fdd3088d582" - -[[package]] -name = "glob" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0cc23270f6e1808e30a928bdc84dea0b9b4136a8bc82338574f23baf47bbd280" - -[[package]] -name = "itertools" -version = "0.13.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186" -dependencies = [ - "either", -] - -[[package]] -name = "lean-ffi" -version = "0.1.0" -dependencies = [ - "bindgen", - "cc", - "num-bigint", -] - -[[package]] -name = "lean-ffi-rs" -version = "0.1.0" -dependencies = [ - "lean-ffi", -] - -[[package]] -name = "libc" -version = "0.2.183" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b646652bf6661599e1da8901b3b9522896f01e736bad5f723fe7a3a27f899d" - -[[package]] -name = "libloading" -version = "0.8.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d7c4b02199fee7c5d21a5ae7d8cfa79a6ef5bb2fc834d6e9058e89c825efdc55" -dependencies = [ - "cfg-if", - "windows-link", -] - -[[package]] -name = "log" -version = "0.4.29" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897" - -[[package]] -name = "memchr" -version = "2.8.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8ca58f447f06ed17d5fc4043ce1b10dd205e060fb3ce5b979b8ed8e59ff3f79" - -[[package]] -name = "minimal-lexical" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" - -[[package]] -name = "nom" -version = "7.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" -dependencies = [ - "memchr", - "minimal-lexical", -] - -[[package]] -name = "num-bigint" -version = "0.4.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" -dependencies = [ - "num-integer", - "num-traits", -] - -[[package]] -name = "num-integer" -version = "0.1.46" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" -dependencies = [ - "num-traits", -] - -[[package]] -name = "num-traits" -version = "0.2.19" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" -dependencies = [ - "autocfg", -] - -[[package]] -name = "prettyplease" -version = "0.2.37" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b" -dependencies = [ - "proc-macro2", - "syn", -] - -[[package]] -name = "proc-macro2" -version = "1.0.106" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" -dependencies = [ - "unicode-ident", -] - -[[package]] -name = "quote" -version = "1.0.45" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924" -dependencies = [ - "proc-macro2", -] - -[[package]] -name = "regex" -version = "1.12.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e10754a14b9137dd7b1e3e5b0493cc9171fdd105e0ab477f51b72e7f3ac0e276" -dependencies = [ - "aho-corasick", - "memchr", - "regex-automata", - "regex-syntax", -] - -[[package]] -name = "regex-automata" -version = "0.4.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6e1dd4122fc1595e8162618945476892eefca7b88c52820e74af6262213cae8f" -dependencies = [ - "aho-corasick", - "memchr", - "regex-syntax", -] - -[[package]] -name = "regex-syntax" -version = "0.8.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc897dd8d9e8bd1ed8cdad82b5966c3e0ecae09fb1907d58efaa013543185d0a" - -[[package]] -name = "rustc-hash" -version = "2.1.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "357703d41365b4b27c590e3ed91eabb1b663f07c4c084095e60cbed4362dff0d" - -[[package]] -name = "shlex" -version = "1.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" - -[[package]] -name = "syn" -version = "2.0.117" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "unicode-ident" -version = "1.0.24" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" - -[[package]] -name = "windows-link" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" diff --git a/test/Cargo.toml b/test/Cargo.toml deleted file mode 100644 index 4b3fd11..0000000 --- a/test/Cargo.toml +++ /dev/null @@ -1,16 +0,0 @@ -[package] -name = "lean-ffi-rs" -version = "0.1.0" -edition = "2024" - -[lib] -crate-type = ["staticlib"] - -[dependencies] -lean-ffi = { path = ".." } - -[profile.dev] -panic = "abort" - -[profile.release] -panic = "abort" diff --git a/test/lakefile.lean b/test/lakefile.lean deleted file mode 100644 index 1c7ef77..0000000 --- a/test/lakefile.lean +++ /dev/null @@ -1,25 +0,0 @@ -import Lake -open System Lake DSL - -package «lean-ffi-test» where - version := v!"0.1.0" - -require LSpec from git - "https://github.com/argumentcomputer/LSpec" @ "928f27c7de8318455ba0be7461dbdf7096f4075a" - -lean_lib Tests - -@[test_driver] -lean_exe LeanFFITests where - root := `Tests.Main - -section FFI - -/-- Build the static lib for the Rust test crate -/ -extern_lib lean_ffi_rs pkg := do - proc { cmd := "cargo", args := #["build", "--release"], cwd := pkg.dir } (quiet := true) - let libName := nameToStaticLib "lean_ffi_rs" - inputBinFile $ pkg.dir / ".." / "target" / "release" / libName - -end FFI - diff --git a/test/lean-toolchain b/test/lean-toolchain deleted file mode 100644 index 4c685fa..0000000 --- a/test/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.28.0 From e042b96b9604035c56553777471fd68415faf77a Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 19 Mar 2026 22:16:25 -0400 Subject: [PATCH 03/10] Simplify CI and Nix build --- .github/workflows/ci.yml | 33 +++++---------------------------- flake.nix | 23 ++++++++--------------- 2 files changed, 13 insertions(+), 43 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f108239..914f03e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -29,38 +29,16 @@ jobs: - name: Check clippy warnings run: cargo xclippy - name: Check *everything* compiles - run: cargo check --all-targets --all-features --workspace - # Restore and then save ./test/.lake to the GitHub cache + run: cargo check --all-targets --all-features + # Restore and then save .lake to the GitHub cache # Essentially the same as lean-action but without re-downloading the Lean toolchain - uses: actions/cache@v5 with: - path: ./test/.lake - key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('test/lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('test/lake-manifest.json') }} + path: ./.lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} + restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }} - run: lake build --wfail -v - working-directory: ./test - run: lake test - working-directory: ./test - - valgrind: - needs: test - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v6 - - uses: actions-rust-lang/setup-rust-toolchain@v1 - # Only restore the cache, since the `test` job will save the test binary to the cache first - - uses: actions/cache/restore@v5 - with: - path: ./test/.lake - key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('test/lake-manifest.json') }}-${{ github.sha }} - restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('test/lake-manifest.json') }} - - uses: leanprover/lean-action@v1 - with: - auto-config: false - build: true - build-args: "LeanFFITests" - use-github-cache: false - lake-package-directory: "./test" - name: Install valgrind run: sudo apt-get update && sudo apt-get install -y valgrind - name: Run tests under valgrind @@ -72,7 +50,6 @@ jobs: --track-origins=yes \ --error-exitcode=1 \ .lake/build/bin/LeanFFITests - working-directory: ./test nix: runs-on: ubuntu-latest diff --git a/flake.nix b/flake.nix index 7e66642..9299d5d 100644 --- a/flake.nix +++ b/flake.nix @@ -68,30 +68,23 @@ pkgs.libiconv ]; }; - rustPkg = craneLib.buildPackage (craneArgs - // { - cargoExtraArgs = "--locked --workspace"; - }); + rustPkg = craneLib.buildPackage (craneArgs // {cargoExtraArgs = "--locked --features test-ffi";}); # Lake test package lake2nix = pkgs.callPackage lean4-nix.lake {}; - lakeDeps = lake2nix.buildDeps { - src = ./test; - }; lakeTest = lake2nix.mkPackage { name = "LeanFFITests"; - inherit lakeDeps; - src = ./test; + src = ./.; # Don't build the Rust static lib with Lake, since we build it with Crane postPatch = '' - substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"' + substituteInPlace lakefile.lean \ + --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"' \ + --replace-fail 'proc { cmd := "cp"' '--proc { cmd := "cp"' ''; - # Copy the Rust static lib from Crane so Lake can find it. - # The lakefile references `pkg.dir / ".." / "target" / "release"` since - # the workspace root owns the target dir. + # Link the Rust static lib so Lake can find it postConfigure = '' - mkdir -p ../target/release - ln -s ${rustPkg}/lib/liblean_ffi_rs.a ../target/release/ + mkdir -p target/release + ln -s ${rustPkg}/lib/liblean_ffi.a target/release/liblean_ffi_test.a ''; }; in { From 0715ef32f7480489f00aa1f2bdecfe6719e293ec Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 19 Mar 2026 22:37:26 -0400 Subject: [PATCH 04/10] Add `LeanShared` multi-threading object --- Tests/FFI.lean | 57 ++++++++++++++ Tests/Main.lean | 1 + src/lib.rs | 2 + src/object.rs | 78 +++++++++++++++++++ src/test_ffi.rs | 194 ++++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 332 insertions(+) diff --git a/Tests/FFI.lean b/Tests/FFI.lean index b2b7f62..7a9e12d 100644 --- a/Tests/FFI.lean +++ b/Tests/FFI.lean @@ -268,6 +268,29 @@ opaque readPersistentString : @& String → Nat @[extern "rs_drop_persistent_nat"] opaque dropPersistentNat : Nat → Nat +/-! ## LeanShared — multi-threaded refcounting tests -/ + +@[extern "rs_shared_parallel_read"] +opaque sharedParallelRead : @& Array Nat → USize → Nat + +@[extern "rs_shared_parallel_nat"] +opaque sharedParallelNat : @& Nat → USize → Nat + +@[extern "rs_shared_parallel_string"] +opaque sharedParallelString : @& String → USize → Nat + +@[extern "rs_shared_contention_stress"] +opaque sharedContentionStress : @& Array Nat → USize → USize → Nat + +@[extern "rs_shared_into_owned"] +opaque sharedIntoOwned : @& Nat → Nat + +@[extern "rs_shared_parallel_point"] +opaque sharedParallelPoint : @& Point → USize → Nat + +@[extern "rs_shared_persistent_nat"] +opaque sharedPersistentNat : @& Nat → USize → Nat + /-! ## Persistent module-level values -/ -- These become persistent (m_rc == 0) after module initialization. @@ -624,4 +647,38 @@ public def propertySuite : List TestSeq := [ checkIO "List to array via push" (∀ xs : List Nat, listToArrayViaPush xs == xs.toArray)), ] +/-! ## LeanShared (multi-threaded) tests -/ + +def sharedTests : TestSeq := + -- Parallel read: N threads all read same array, sum should be N * element_sum + test "Shared parallel read 4 threads" (sharedParallelRead #[1, 2, 3] 4 == 24) ++ + test "Shared parallel read 8 threads" (sharedParallelRead #[10, 20] 8 == 240) ++ + test "Shared parallel read empty" (sharedParallelRead #[] 4 == 0) ++ + test "Shared parallel read 1 thread" (sharedParallelRead #[42] 1 == 42) ++ + -- Parallel Nat: all threads should read same value + test "Shared parallel Nat 42" (sharedParallelNat 42 4 == 42) ++ + test "Shared parallel Nat 0" (sharedParallelNat 0 4 == 0) ++ + test "Shared parallel Nat large" (sharedParallelNat (2^64) 4 == 2^64) ++ + -- Parallel String: sum of byte_len across threads + test "Shared parallel String" (sharedParallelString "hello" 4 == 20) ++ + test "Shared parallel String empty" (sharedParallelString "" 4 == 0) ++ + -- Contention stress: rapid clone/drop from many threads + test "Shared contention 4 threads 100 clones" (sharedContentionStress #[1, 2, 3] 4 100 == 12) ++ + test "Shared contention 8 threads 50 clones" (sharedContentionStress #[10] 8 50 == 8) ++ + -- into_owned: unwrap MT-marked LeanShared back to LeanOwned + test "Shared into_owned 42" (sharedIntoOwned 42 == 42) ++ + test "Shared into_owned large" (sharedIntoOwned (2^128) == 2^128) ++ + test "Shared into_owned 0" (sharedIntoOwned 0 == 0) ++ + -- Constructor types: lean_mark_mt walks object graph + test "Shared parallel Point 4 threads" (sharedParallelPoint ⟨10, 20⟩ 4 == 120) ++ + test "Shared parallel Point 1 thread" (sharedParallelPoint ⟨3, 7⟩ 1 == 10) ++ + test "Shared parallel Point zeros" (sharedParallelPoint ⟨0, 0⟩ 4 == 0) ++ + -- Persistent objects: lean_mark_mt skipped, refcount ops are no-ops + test "Shared persistent Nat" (sharedPersistentNat persistentNat 4 == 42) ++ + test "Shared persistent large Nat" (sharedPersistentNat persistentLargeNat 4 == 2^128) + +public def sharedSuite : List TestSeq := [ + group "LeanShared MT" sharedTests, +] + end Tests.FFI diff --git a/Tests/Main.lean b/Tests/Main.lean index e933ced..027e650 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -7,5 +7,6 @@ def main (args : List String) : IO UInt32 := do ("owned", Tests.FFI.ownedSuite), ("persistent", Tests.FFI.persistentSuite), ("property", Tests.FFI.propertySuite), + ("shared", Tests.FFI.sharedSuite), ] LSpec.lspecIO suites args diff --git a/src/lib.rs b/src/lib.rs index e2baa15..805fd1c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -23,6 +23,8 @@ pub mod include { pub mod nat; pub mod object; +pub use object::LeanShared; + #[cfg(feature = "test-ffi")] mod test_ffi; diff --git a/src/object.rs b/src/object.rs index b561e88..1113d2d 100644 --- a/src/object.rs +++ b/src/object.rs @@ -1447,3 +1447,81 @@ impl<'a> LeanBorrowed<'a> { LeanByteArray(self) } } + +// ============================================================================= +// LeanShared — Thread-safe owned Lean object +// ============================================================================= + +/// Thread-safe owned Lean object with atomic refcounting. +/// +/// Created by calling [`lean_mark_mt`] on the object graph, which transitions +/// all reachable objects from single-threaded to multi-threaded mode. +/// After marking, [`lean_inc_ref`] / [`lean_dec_ref`] use atomic operations, +/// so [`LeanOwned`]'s existing `Clone` and `Drop` are thread-safe. +/// +/// Scalars (tagged pointers with bit 0 set) and persistent objects +/// (`m_rc == 0`) are unaffected by MT marking. +#[repr(transparent)] +pub struct LeanShared(LeanOwned); + +// SAFETY: lean_mark_mt transitions the entire reachable object graph to +// multi-threaded mode. After marking, lean_inc_ref uses atomic operations +// for refcount increments, and lean_dec_ref delegates to lean_dec_ref_cold +// which also handles MT objects atomically. This makes Clone (inc_ref) and +// Drop (dec_ref) thread-safe. +unsafe impl Send for LeanShared {} +unsafe impl Sync for LeanShared {} + +impl LeanShared { + /// Mark an owned object's entire reachable graph as MT and take ownership. + /// + /// Persistent objects (`m_rc == 0`) and scalars are unaffected. + /// After this call, all refcount operations on the object graph use + /// atomic instructions. + #[inline] + pub fn new(owned: LeanOwned) -> Self { + if !owned.is_scalar() && !owned.is_persistent() { + unsafe { include::lean_mark_mt(owned.as_raw()); } + } + Self(owned) + } + + /// Borrow this object. The returned reference is lifetime-bounded + /// to `&self` and is **not** `Send`. + #[inline] + pub fn borrow(&self) -> LeanBorrowed<'_> { + unsafe { LeanBorrowed::from_raw(self.0.as_raw()) } + } + + /// Get the raw pointer, e.g. for pointer-identity caching across threads. + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } + + /// Consume, returning the inner [`LeanOwned`] (still MT-marked). + #[inline] + pub fn into_owned(self) -> LeanOwned { + let ptr = self.0.as_raw(); + std::mem::forget(self); + unsafe { LeanOwned::from_raw(ptr) } + } +} + +impl Clone for LeanShared { + #[inline] + fn clone(&self) -> Self { + // lean_inc_ref uses atomic ops for MT objects (m_rc < 0). + Self(self.0.clone()) + } +} + +// No custom Drop needed: LeanOwned's Drop calls lean_dec_ref, which handles +// MT objects via lean_dec_ref_cold (atomic decrement + deallocation). + +impl LeanRef for LeanShared { + #[inline] + fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } +} diff --git a/src/test_ffi.rs b/src/test_ffi.rs index bd92b52..33aa6ac 100644 --- a/src/test_ffi.rs +++ b/src/test_ffi.rs @@ -1142,3 +1142,197 @@ pub extern "C" fn rs_drop_persistent_nat(obj: LeanNat) -> LeanNat>, + n_threads: usize, +) -> LeanNat { + use std::thread; + + // Create an owned copy and mark as MT + let shared = LeanShared::new(arr.inner().to_owned_ref()); + + let mut handles = Vec::new(); + for _ in 0..n_threads { + let shared_clone = shared.clone(); // atomic lean_inc + handles.push(thread::spawn(move || { + // Each thread borrows and reads all elements + let borrowed = shared_clone.borrow().as_array(); + let mut sum: u64 = 0; + for elem in borrowed.iter() { + sum += Nat::from_obj(&elem).to_u64().unwrap_or(0); + } + sum + // shared_clone dropped → atomic lean_dec + })); + } + + let mut total: u64 = 0; + for h in handles { + total += h.join().unwrap(); + } + // shared dropped → atomic lean_dec (last ref frees) + + Nat::from(total).to_lean() +} + +/// Mark a Nat as MT, clone it to N threads, each reads it. +/// Simpler than array — tests basic scalar/heap Nat across threads. +#[unsafe(no_mangle)] +pub extern "C" fn rs_shared_parallel_nat( + nat: LeanNat>, + n_threads: usize, +) -> LeanNat { + use std::thread; + + let shared = LeanShared::new(nat.inner().to_owned_ref()); + + let mut handles = Vec::new(); + for _ in 0..n_threads { + let shared_clone = shared.clone(); + handles.push(thread::spawn(move || { + Nat::from_obj(&shared_clone.borrow()) + })); + } + + // All threads should read the same value + let results: Vec = handles.into_iter().map(|h| h.join().unwrap()).collect(); + let first = &results[0]; + assert!(results.iter().all(|r| r == first), "MT read inconsistency"); + + first.to_lean() +} + +/// Mark a string as MT, clone to N threads, each reads byte_len. +/// Returns sum of all byte_len readings. +#[unsafe(no_mangle)] +pub extern "C" fn rs_shared_parallel_string( + s: LeanString>, + n_threads: usize, +) -> LeanNat { + use std::thread; + + let shared = LeanShared::new(s.inner().to_owned_ref()); + + let mut handles = Vec::new(); + for _ in 0..n_threads { + let shared_clone = shared.clone(); + handles.push(thread::spawn(move || { + shared_clone.borrow().as_string().byte_len() as u64 + })); + } + + let total: u64 = handles.into_iter().map(|h| h.join().unwrap()).sum(); + Nat::from(total).to_lean() +} + +/// Stress test: mark array as MT, spawn many threads that each clone +/// and drop rapidly. Tests atomic refcount under contention. +#[unsafe(no_mangle)] +pub extern "C" fn rs_shared_contention_stress( + arr: LeanArray>, + n_threads: usize, + clones_per_thread: usize, +) -> LeanNat { + use std::thread; + + let shared = LeanShared::new(arr.inner().to_owned_ref()); + + let mut handles = Vec::new(); + for _ in 0..n_threads { + let shared_clone = shared.clone(); + handles.push(thread::spawn(move || { + // Rapidly clone and drop to stress atomic refcount + for _ in 0..clones_per_thread { + let tmp = shared_clone.clone(); + let _ = tmp.borrow().as_array().len(); + // tmp dropped → atomic lean_dec + } + shared_clone.borrow().as_array().len() as u64 + })); + } + + let total: u64 = handles.into_iter().map(|h| h.join().unwrap()).sum(); + Nat::from(total).to_lean() +} + +/// Test into_owned: mark as MT, convert back to LeanOwned, read value. +/// Verifies the MT-marked object is still usable after unwrapping. +#[unsafe(no_mangle)] +pub extern "C" fn rs_shared_into_owned( + nat: LeanNat>, +) -> LeanNat { + let shared = LeanShared::new(nat.inner().to_owned_ref()); + let cloned = shared.clone(); + // Convert one back to LeanOwned + let owned = cloned.into_owned(); + let val = Nat::from_obj(&unsafe { LeanBorrowed::from_raw(owned.as_raw()) }); + let result = val.to_lean(); + // owned drops (still MT-marked, lean_dec_ref handles it) + // shared drops (atomic lean_dec) + result +} + +/// Mark a Point (constructor with 2 obj fields) as MT, read fields from threads. +/// Tests that lean_mark_mt correctly walks the constructor's object graph. +#[unsafe(no_mangle)] +pub extern "C" fn rs_shared_parallel_point( + point: LeanPoint>, + n_threads: usize, +) -> LeanNat { + use std::thread; + + let shared = LeanShared::new(point.inner().to_owned_ref()); + + let mut handles = Vec::new(); + for _ in 0..n_threads { + let shared_clone = shared.clone(); + handles.push(thread::spawn(move || { + let ctor = shared_clone.borrow().as_ctor(); + let x = Nat::from_obj(&ctor.get(0)); + let y = Nat::from_obj(&ctor.get(1)); + x.to_u64().unwrap_or(0) + y.to_u64().unwrap_or(0) + })); + } + + let total: u64 = handles.into_iter().map(|h| h.join().unwrap()).sum(); + Nat::from(total).to_lean() +} + +/// Wrap a persistent Nat in LeanShared (lean_mark_mt is skipped for persistent). +/// Clone to threads and read — verifies the persistent skip path works. +#[unsafe(no_mangle)] +pub extern "C" fn rs_shared_persistent_nat( + nat: LeanNat>, + n_threads: usize, +) -> LeanNat { + use std::thread; + + // For persistent objects, LeanShared::new skips lean_mark_mt. + // lean_inc_ref / lean_dec_ref are already no-ops for m_rc == 0, + // so Clone and Drop are safe without MT marking. + let shared = LeanShared::new(nat.inner().to_owned_ref()); + + let mut handles = Vec::new(); + for _ in 0..n_threads { + let shared_clone = shared.clone(); + handles.push(thread::spawn(move || { + Nat::from_obj(&shared_clone.borrow()) + })); + } + + let results: Vec = handles.into_iter().map(|h| h.join().unwrap()).collect(); + let first = &results[0]; + assert!(results.iter().all(|r| r == first), "persistent MT read inconsistency"); + first.to_lean() +} From 16df70076ae7c4421e8f8896b30a72b4772a0964 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 19 Mar 2026 22:52:44 -0400 Subject: [PATCH 05/10] Update docs --- .gitignore | 6 +-- README.md | 15 ++++--- src/lib.rs | 2 + src/object.rs | 109 ++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 124 insertions(+), 8 deletions(-) diff --git a/.gitignore b/.gitignore index 7ffc9ea..c2f0e98 100644 --- a/.gitignore +++ b/.gitignore @@ -1,9 +1,9 @@ # Rust -**/target +target # Lean -**/.lake +.lake # Nix -**/result +result .direnv/ diff --git a/README.md b/README.md index e9b79f0..69482cd 100644 --- a/README.md +++ b/README.md @@ -21,12 +21,17 @@ The core types are: Corresponds to `b_lean_obj_arg` in the C FFI. Used when Lean declares a parameter with `@&`. -- **`LeanRef`** — Trait implemented by both `LeanOwned` and `LeanBorrowed`, providing - shared read-only operations like `as_raw()`, `is_scalar()`, `tag()`, and unboxing - methods. +- **`LeanShared`** — A thread-safe owned reference. Wraps `LeanOwned` after calling + `lean_mark_mt` on the object graph, which transitions all reachable objects to + multi-threaded mode with atomic refcounting. `Send + Sync`. Use `borrow()` to get + a `LeanBorrowed<'_>` for reading, `into_owned()` to unwrap back to `LeanOwned`. -Both are safe for persistent objects (`m_rc == 0`) — `lean_inc_ref` and `lean_dec_ref` -are no-ops when `m_rc == 0`. +- **`LeanRef`** — Trait implemented by `LeanOwned`, `LeanBorrowed`, and `LeanShared`, + providing shared read-only operations like `as_raw()`, `is_scalar()`, `tag()`, and + unboxing methods. + +All reference types are safe for persistent objects (`m_rc == 0`) — `lean_inc_ref` and +`lean_dec_ref` are no-ops when `m_rc == 0`. ## Domain Types diff --git a/src/lib.rs b/src/lib.rs index 805fd1c..ac8adfa 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -101,6 +101,7 @@ macro_rules! lean_domain_type { #[inline] pub fn into_raw(self) -> *mut $crate::include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -110,6 +111,7 @@ macro_rules! lean_domain_type { #[inline] fn from(x: $name<$crate::object::LeanOwned>) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); unsafe { $crate::object::LeanOwned::from_raw(ptr) } } diff --git a/src/object.rs b/src/object.rs index 1113d2d..8d72342 100644 --- a/src/object.rs +++ b/src/object.rs @@ -26,6 +26,14 @@ const IO_ERROR_USER_ERROR_TAG: u8 = 7; // ============================================================================= // LeanRef trait — shared interface for owned and borrowed pointers // ============================================================================= +// +// lean.h base object header (8 bytes): +// typedef struct { +// int m_rc; // >0 single-threaded, <0 multi-threaded, 0 persistent +// unsigned m_cs_sz:16; +// unsigned m_other:8; // num_objs (ctors) or element size (scalar arrays) +// unsigned m_tag:8; // object type tag (0–243 ctor, 246 array, 248 sarray, ...) +// } lean_object; /// Trait for types that hold a reference to a Lean object (owned or borrowed). /// @@ -172,6 +180,7 @@ impl LeanOwned { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0; + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -270,6 +279,9 @@ impl<'a> LeanBorrowed<'a> { // ============================================================================= // LeanNat — Nat (scalar or heap mpz) // ============================================================================= +// +// Small Nat: tagged scalar via `lean_box(n)` for n ≤ LEAN_MAX_SMALL_NAT (2^63-1 on 64-bit). +// Big Nat: heap object with m_tag == LeanMPZ (250), containing a GMP mpz_t. /// Typed wrapper for a Lean `Nat` (small = tagged scalar, big = heap `mpz_object`). #[repr(transparent)] @@ -302,6 +314,7 @@ impl LeanNat { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -319,6 +332,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanNat) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -327,6 +341,9 @@ impl From> for LeanOwned { // ============================================================================= // LeanBool — Bool (unboxed scalar: false = 0, true = 1) // ============================================================================= +// +// lean.h: Bool.false = lean_box(0), Bool.true = lean_box(1). +// Always a tagged scalar — never heap-allocated. /// Typed wrapper for a Lean `Bool` (always an unboxed scalar: false = 0, true = 1). #[repr(transparent)] @@ -366,6 +383,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanBool) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -374,6 +392,14 @@ impl From> for LeanOwned { // ============================================================================= // LeanArray — Array α (tag LEAN_TAG_ARRAY) // ============================================================================= +// +// lean.h: +// typedef struct { +// lean_object m_header; +// size_t m_size; +// size_t m_capacity; +// lean_object * m_data[]; +// } lean_array_object; /// Typed wrapper for a Lean `Array α` object (tag `LEAN_TAG_ARRAY`). #[repr(transparent)] @@ -471,6 +497,7 @@ impl LeanArray { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -480,6 +507,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanArray) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -488,6 +516,14 @@ impl From> for LeanOwned { // ============================================================================= // LeanByteArray — ByteArray (tag LEAN_TAG_SCALAR_ARRAY) // ============================================================================= +// +// lean.h: +// typedef struct { +// lean_object m_header; +// size_t m_size; +// size_t m_capacity; +// uint8_t m_data[]; +// } lean_sarray_object; /// Typed wrapper for a Lean `ByteArray` object (tag `LEAN_TAG_SCALAR_ARRAY`). #[repr(transparent)] @@ -572,6 +608,7 @@ impl LeanByteArray { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -581,6 +618,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanByteArray) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -589,6 +627,15 @@ impl From> for LeanOwned { // ============================================================================= // LeanString — String (tag LEAN_TAG_STRING) // ============================================================================= +// +// lean.h: +// typedef struct { +// lean_object m_header; +// size_t m_size; // byte length including NUL terminator +// size_t m_capacity; +// size_t m_length; // UTF-8 character count +// char m_data[]; +// } lean_string_object; /// Typed wrapper for a Lean `String` object (tag `LEAN_TAG_STRING`). #[repr(transparent)] @@ -658,6 +705,7 @@ impl LeanString { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -667,6 +715,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanString) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -675,6 +724,15 @@ impl From> for LeanOwned { // ============================================================================= // LeanCtor — Constructor objects (tag 0–LEAN_MAX_CTOR_TAG) // ============================================================================= +// +// lean.h: +// typedef struct { +// lean_object m_header; // m_tag = ctor index, m_other = num_objs +// lean_object * m_objs[]; // object fields, then scalar fields in memory +// } lean_ctor_object; +// +// Memory layout after m_header: +// [obj_0, obj_1, ..., obj_{n-1}] [usize_0, ...] [scalar bytes (descending size)] /// Typed wrapper for a Lean constructor object (tag 0–`LEAN_MAX_CTOR_TAG`). #[repr(transparent)] @@ -793,6 +851,7 @@ impl LeanCtor { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -834,6 +893,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanCtor) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -842,6 +902,18 @@ impl From> for LeanOwned { // ============================================================================= // LeanExternal — External objects (tag LEAN_TAG_EXTERNAL) // ============================================================================= +// +// lean.h: +// typedef struct { +// lean_external_finalize_proc m_finalize; +// lean_external_foreach_proc m_foreach; +// } lean_external_class; +// +// typedef struct { +// lean_object m_header; +// lean_external_class * m_class; +// void * m_data; +// } lean_external_object; /// Typed wrapper for a Lean external object (tag `LEAN_TAG_EXTERNAL`) holding a `T`. #[repr(transparent)] @@ -888,6 +960,7 @@ impl LeanExternal { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -912,6 +985,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanExternal) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -956,6 +1030,10 @@ impl ExternalClass { // ============================================================================= // LeanList — List α // ============================================================================= +// +// Constructor-based inductive (no special lean.h struct): +// List.nil = lean_box(0) (tagged scalar) +// List.cons = lean_ctor_object, tag 1, 2 obj fields (head, tail) /// Typed wrapper for a Lean `List α` (nil = scalar `lean_box(0)`, cons = ctor tag 1). #[repr(transparent)] @@ -1018,6 +1096,7 @@ impl LeanList { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -1055,6 +1134,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanList) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -1063,6 +1143,10 @@ impl From> for LeanOwned { // ============================================================================= // LeanOption — Option α // ============================================================================= +// +// Constructor-based inductive (no special lean.h struct): +// Option.none = lean_box(0) (tagged scalar) +// Option.some = lean_ctor_object, tag 1, 1 obj field (value) /// Typed wrapper for a Lean `Option α` (none = scalar, some = ctor tag 1). #[repr(transparent)] @@ -1132,6 +1216,7 @@ impl LeanOption { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -1141,6 +1226,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanOption) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -1149,6 +1235,10 @@ impl From> for LeanOwned { // ============================================================================= // LeanExcept — Except ε α // ============================================================================= +// +// Constructor-based inductive (no special lean.h struct): +// Except.error = lean_ctor_object, tag 0, 1 obj field (error value) +// Except.ok = lean_ctor_object, tag 1, 1 obj field (ok value) /// Typed wrapper for a Lean `Except ε α` (error = ctor tag 0, ok = ctor tag 1). #[repr(transparent)] @@ -1229,6 +1319,7 @@ impl LeanExcept { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -1238,6 +1329,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanExcept) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -1246,6 +1338,15 @@ impl From> for LeanOwned { // ============================================================================= // LeanIOResult — EStateM.Result (BaseIO.Result) // ============================================================================= +// +// Constructor-based inductive (no special lean.h struct): +// EStateM.Result.ok = lean_ctor_object, tag 0, 2 obj fields (value, state) +// EStateM.Result.error = lean_ctor_object, tag 1, 2 obj fields (error, state) +// +// lean.h accessors: +// lean_io_result_is_ok(r) → lean_ptr_tag(r) == 0 +// lean_io_result_get_value(r) → lean_ctor_get(r, 0) +// lean_io_result_get_error(r) → lean_ctor_get(r, 0) /// Typed wrapper for a Lean `BaseIO.Result α` (`EStateM.Result`). /// ok = ctor tag 0 (value, world), error = ctor tag 1 (error, world). @@ -1300,6 +1401,7 @@ impl LeanIOResult { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -1309,6 +1411,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanIOResult) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -1317,6 +1420,9 @@ impl From> for LeanOwned { // ============================================================================= // LeanProd — Prod α β (pair) // ============================================================================= +// +// Constructor-based inductive (no special lean.h struct): +// Prod.mk = lean_ctor_object, tag 0, 2 obj fields (fst, snd) /// Typed wrapper for a Lean `Prod α β` (ctor tag 0, 2 object fields). #[repr(transparent)] @@ -1367,6 +1473,7 @@ impl LeanProd { #[inline] pub fn into_raw(self) -> *mut include::lean_object { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); ptr } @@ -1376,6 +1483,7 @@ impl From> for LeanOwned { #[inline] fn from(x: LeanProd) -> Self { let ptr = x.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned std::mem::forget(x); LeanOwned(ptr) } @@ -1503,6 +1611,7 @@ impl LeanShared { #[inline] pub fn into_owned(self) -> LeanOwned { let ptr = self.0.as_raw(); + // Suppress Drop (lean_dec) — ownership transfers to the caller std::mem::forget(self); unsafe { LeanOwned::from_raw(ptr) } } From ec13dfd2d62062deca5a3140bfb78387bf01b766 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 19 Mar 2026 23:13:45 -0400 Subject: [PATCH 06/10] fmt --- src/lib.rs | 1 - src/object.rs | 161 +++++++++++++++++++++++++++++++++++++----------- src/test_ffi.rs | 17 +++-- 3 files changed, 133 insertions(+), 46 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index ac8adfa..61b42d5 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -118,4 +118,3 @@ macro_rules! lean_domain_type { } )*}; } - diff --git a/src/object.rs b/src/object.rs index 8d72342..a8883dc 100644 --- a/src/object.rs +++ b/src/object.rs @@ -120,7 +120,6 @@ pub trait LeanRef: Clone { } } - // ============================================================================= // LeanOwned — Owned Lean object pointer (RAII) // ============================================================================= @@ -298,9 +297,13 @@ impl Copy for LeanNat {} impl LeanNat { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } } impl LeanNat { @@ -360,9 +363,13 @@ impl Copy for LeanBool {} impl LeanBool { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } /// Decode to a Rust `bool`. #[inline] @@ -416,9 +423,13 @@ impl Copy for LeanArray {} impl LeanArray { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } pub fn len(&self) -> usize { unsafe { include::lean_array_size(self.0.as_raw()) } @@ -540,9 +551,13 @@ impl Copy for LeanByteArray {} impl LeanByteArray { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } pub fn len(&self) -> usize { unsafe { include::lean_sarray_size(self.0.as_raw()) } @@ -652,9 +667,13 @@ impl Copy for LeanString {} impl LeanString { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } /// Number of data bytes (excluding the trailing NUL). pub fn byte_len(&self) -> usize { @@ -789,22 +808,34 @@ impl LeanCtor { } pub fn get_u8(&self, num_objs: usize, offset: usize) -> u8 { - unsafe { include::lean_ctor_get_uint8(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } + unsafe { + include::lean_ctor_get_uint8(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) + } } pub fn get_u16(&self, num_objs: usize, offset: usize) -> u16 { - unsafe { include::lean_ctor_get_uint16(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } + unsafe { + include::lean_ctor_get_uint16(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) + } } pub fn get_u32(&self, num_objs: usize, offset: usize) -> u32 { - unsafe { include::lean_ctor_get_uint32(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } + unsafe { + include::lean_ctor_get_uint32(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) + } } pub fn get_u64(&self, num_objs: usize, offset: usize) -> u64 { - unsafe { include::lean_ctor_get_uint64(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } + unsafe { + include::lean_ctor_get_uint64(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) + } } pub fn get_f64(&self, num_objs: usize, offset: usize) -> f64 { - unsafe { include::lean_ctor_get_float(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } + unsafe { + include::lean_ctor_get_float(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) + } } pub fn get_f32(&self, num_objs: usize, offset: usize) -> f32 { - unsafe { include::lean_ctor_get_float32(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } + unsafe { + include::lean_ctor_get_float32(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) + } } /// Read a `usize` at slot `slot` past `num_objs` object fields. /// Uses a **slot index** (not byte offset). @@ -861,28 +892,66 @@ impl LeanCtor { // ------------------------------------------------------------------------- pub fn set_u8(&self, num_objs: usize, offset: usize, val: u8) { - unsafe { include::lean_ctor_set_uint8(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + unsafe { + include::lean_ctor_set_uint8( + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), + val, + ); + } } pub fn set_u16(&self, num_objs: usize, offset: usize, val: u16) { - unsafe { include::lean_ctor_set_uint16(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + unsafe { + include::lean_ctor_set_uint16( + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), + val, + ); + } } pub fn set_u32(&self, num_objs: usize, offset: usize, val: u32) { - unsafe { include::lean_ctor_set_uint32(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + unsafe { + include::lean_ctor_set_uint32( + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), + val, + ); + } } pub fn set_u64(&self, num_objs: usize, offset: usize, val: u64) { - unsafe { include::lean_ctor_set_uint64(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + unsafe { + include::lean_ctor_set_uint64( + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), + val, + ); + } } pub fn set_f64(&self, num_objs: usize, offset: usize, val: f64) { - unsafe { include::lean_ctor_set_float(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + unsafe { + include::lean_ctor_set_float( + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), + val, + ); + } } pub fn set_f32(&self, num_objs: usize, offset: usize, val: f32) { - unsafe { include::lean_ctor_set_float32(self.0.as_raw(), Self::scalar_offset(num_objs, offset), val); } + unsafe { + include::lean_ctor_set_float32( + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), + val, + ); + } } /// Set a `usize` at slot `slot` past `num_objs` object fields. /// Uses a **slot index** (not byte offset). #[allow(clippy::cast_possible_truncation)] pub fn set_usize(&self, num_objs: usize, slot: usize, val: usize) { - unsafe { include::lean_ctor_set_usize(self.0.as_raw(), (num_objs + slot) as u32, val); } + unsafe { + include::lean_ctor_set_usize(self.0.as_raw(), (num_objs + slot) as u32, val); + } } pub fn set_bool(&self, num_objs: usize, offset: usize, val: bool) { self.set_u8(num_objs, offset, val as u8); @@ -1050,9 +1119,13 @@ impl Copy for LeanList {} impl LeanList { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } pub fn is_nil(&self) -> bool { self.0.is_scalar() @@ -1163,9 +1236,13 @@ impl Copy for LeanOption {} impl LeanOption { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } #[inline] pub fn as_ctor(&self) -> LeanCtor> { unsafe { LeanBorrowed::from_raw(self.0.as_raw()) }.as_ctor() @@ -1255,9 +1332,13 @@ impl Copy for LeanExcept {} impl LeanExcept { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } #[inline] pub fn as_ctor(&self) -> LeanCtor> { unsafe { LeanBorrowed::from_raw(self.0.as_raw()) }.as_ctor() @@ -1364,9 +1445,13 @@ impl Copy for LeanIOResult {} impl LeanIOResult { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } #[inline] pub fn as_ctor(&self) -> LeanCtor> { unsafe { LeanBorrowed::from_raw(self.0.as_raw()) }.as_ctor() @@ -1439,9 +1524,13 @@ impl Copy for LeanProd {} impl LeanProd { #[inline] - pub fn inner(&self) -> &R { &self.0 } + pub fn inner(&self) -> &R { + &self.0 + } #[inline] - pub fn as_raw(&self) -> *mut include::lean_object { self.0.as_raw() } + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } /// Get a borrowed reference to the first element. pub fn fst(&self) -> LeanBorrowed<'_> { @@ -1589,7 +1678,9 @@ impl LeanShared { #[inline] pub fn new(owned: LeanOwned) -> Self { if !owned.is_scalar() && !owned.is_persistent() { - unsafe { include::lean_mark_mt(owned.as_raw()); } + unsafe { + include::lean_mark_mt(owned.as_raw()); + } } Self(owned) } diff --git a/src/test_ffi.rs b/src/test_ffi.rs index 33aa6ac..b03ba02 100644 --- a/src/test_ffi.rs +++ b/src/test_ffi.rs @@ -1200,9 +1200,7 @@ pub extern "C" fn rs_shared_parallel_nat( let mut handles = Vec::new(); for _ in 0..n_threads { let shared_clone = shared.clone(); - handles.push(thread::spawn(move || { - Nat::from_obj(&shared_clone.borrow()) - })); + handles.push(thread::spawn(move || Nat::from_obj(&shared_clone.borrow()))); } // All threads should read the same value @@ -1269,9 +1267,7 @@ pub extern "C" fn rs_shared_contention_stress( /// Test into_owned: mark as MT, convert back to LeanOwned, read value. /// Verifies the MT-marked object is still usable after unwrapping. #[unsafe(no_mangle)] -pub extern "C" fn rs_shared_into_owned( - nat: LeanNat>, -) -> LeanNat { +pub extern "C" fn rs_shared_into_owned(nat: LeanNat>) -> LeanNat { let shared = LeanShared::new(nat.inner().to_owned_ref()); let cloned = shared.clone(); // Convert one back to LeanOwned @@ -1326,13 +1322,14 @@ pub extern "C" fn rs_shared_persistent_nat( let mut handles = Vec::new(); for _ in 0..n_threads { let shared_clone = shared.clone(); - handles.push(thread::spawn(move || { - Nat::from_obj(&shared_clone.borrow()) - })); + handles.push(thread::spawn(move || Nat::from_obj(&shared_clone.borrow()))); } let results: Vec = handles.into_iter().map(|h| h.join().unwrap()).collect(); let first = &results[0]; - assert!(results.iter().all(|r| r == first), "persistent MT read inconsistency"); + assert!( + results.iter().all(|r| r == first), + "persistent MT read inconsistency" + ); first.to_lean() } From e9cc534d143998658b201668480da1a3cc86fee8 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Thu, 19 Mar 2026 23:42:08 -0400 Subject: [PATCH 07/10] Cleanup --- lakefile.lean | 5 +- src/object.rs | 111 ++++++++++++------------ src/test_ffi.rs | 220 +++++++++++++++++++++++++++--------------------- 3 files changed, 181 insertions(+), 155 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 8314a7c..16e49c2 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -10,7 +10,7 @@ require LSpec from git section FFI /-- Build the static lib for the Rust FFI test crate -/ -target ffi_rs_test pkg : FilePath := do +extern_lib ffi_rs_test pkg := do proc { cmd := "cargo", args := #["build", "--release", "--features", "test-ffi"], cwd := pkg.dir } (quiet := true) let srcName := nameToStaticLib "lean_ffi" let dstName := nameToStaticLib "lean_ffi_test" @@ -20,8 +20,7 @@ target ffi_rs_test pkg : FilePath := do end FFI -lean_lib Tests where - moreLinkObjs := #[ffi_rs_test] +lean_lib Tests @[test_driver] lean_exe LeanFFITests where diff --git a/src/object.rs b/src/object.rs index a8883dc..1e52f34 100644 --- a/src/object.rs +++ b/src/object.rs @@ -11,14 +11,27 @@ use std::marker::PhantomData; use std::mem::ManuallyDrop; use crate::include; + +/// Assert that runs only when the `test-ffi` feature is enabled (i.e. during `lake test`). +macro_rules! test_assert { + ($($arg:tt)*) => { + #[cfg(feature = "test-ffi")] + assert!($($arg)*); + }; +} use crate::safe_cstring; -// Tag constants from lean.h -const LEAN_MAX_CTOR_TAG: u8 = 243; -const LEAN_TAG_ARRAY: u8 = 246; -const LEAN_TAG_SCALAR_ARRAY: u8 = 248; -const LEAN_TAG_STRING: u8 = 249; -const LEAN_TAG_EXTERNAL: u8 = 254; +// Tag constants from lean.h (only used by test_assert! when test-ffi is enabled) +#[cfg(feature = "test-ffi")] +mod tags { + pub(super) const LEAN_MAX_CTOR_TAG: u8 = 243; + pub(super) const LEAN_TAG_ARRAY: u8 = 246; + pub(super) const LEAN_TAG_SCALAR_ARRAY: u8 = 248; + pub(super) const LEAN_TAG_STRING: u8 = 249; + pub(super) const LEAN_TAG_EXTERNAL: u8 = 254; +} +#[cfg(feature = "test-ffi")] +use tags::*; /// Constructor tag for `IO.Error.userError`. const IO_ERROR_USER_ERROR_TAG: u8 = 7; @@ -472,11 +485,9 @@ impl LeanArray { /// # Safety /// The pointer must be a valid Lean `Array` object. pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 != 1); - debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_ARRAY); - Self(LeanOwned(ptr)) - } + test_assert!(ptr as usize & 1 != 1); + test_assert!(unsafe { include::lean_obj_tag(ptr) } == u32::from(LEAN_TAG_ARRAY)); + Self(LeanOwned(ptr)) } /// Allocate a new array with `size` elements (capacity = size). @@ -582,11 +593,9 @@ impl LeanByteArray { /// # Safety /// The pointer must be a valid Lean `ByteArray` object. pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 != 1); - debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_SCALAR_ARRAY); - Self(LeanOwned(ptr)) - } + test_assert!(ptr as usize & 1 != 1); + test_assert!(unsafe { include::lean_obj_tag(ptr) } == u32::from(LEAN_TAG_SCALAR_ARRAY)); + Self(LeanOwned(ptr)) } /// Allocate a new byte array with `size` bytes (capacity = size). @@ -615,7 +624,7 @@ impl LeanByteArray { let cptr = include::lean_sarray_cptr(obj); std::ptr::copy_nonoverlapping(data.as_ptr(), cptr, data.len()); // Update m_size: at offset 8 (after lean_object header) - *(obj as *mut u8).add(8).cast::() = data.len(); + *obj.cast::().add(8).cast::() = data.len(); } } @@ -700,11 +709,9 @@ impl LeanString { /// # Safety /// The pointer must be a valid Lean `String` object. pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 != 1); - debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_STRING); - Self(LeanOwned(ptr)) - } + test_assert!(ptr as usize & 1 != 1); + test_assert!(unsafe { include::lean_obj_tag(ptr) } == u32::from(LEAN_TAG_STRING)); + Self(LeanOwned(ptr)) } /// Create a Lean string from a Rust `&str`. @@ -854,11 +861,9 @@ impl LeanCtor { /// # Safety /// The pointer must be a valid Lean constructor object. pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 != 1); - debug_assert!(include::lean_obj_tag(ptr) as u8 <= LEAN_MAX_CTOR_TAG); - Self(LeanOwned(ptr)) - } + test_assert!(ptr as usize & 1 != 1); + test_assert!(unsafe { include::lean_obj_tag(ptr) } <= u32::from(LEAN_MAX_CTOR_TAG)); + Self(LeanOwned(ptr)) } /// Allocate a new constructor object. @@ -1011,11 +1016,9 @@ impl LeanExternal { /// The pointer must be a valid Lean external object whose data pointer /// points to a valid `T`. pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 != 1); - debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_EXTERNAL); - Self(LeanOwned(ptr), PhantomData) - } + test_assert!(ptr as usize & 1 != 1); + test_assert!(unsafe { include::lean_obj_tag(ptr) } == u32::from(LEAN_TAG_EXTERNAL)); + Self(LeanOwned(ptr), PhantomData) } /// Allocate a new external object holding `data`. @@ -1042,11 +1045,9 @@ impl<'a, T> LeanExternal> { /// The pointer must be a valid Lean external object whose data pointer /// points to a valid `T`, and the object must outlive `'a`. pub unsafe fn from_raw_borrowed(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 != 1); - debug_assert!(include::lean_obj_tag(ptr) as u8 == LEAN_TAG_EXTERNAL); - Self(LeanBorrowed::from_raw(ptr), PhantomData) - } + test_assert!(ptr as usize & 1 != 1); + test_assert!(unsafe { include::lean_obj_tag(ptr) } == u32::from(LEAN_TAG_EXTERNAL)); + Self(unsafe { LeanBorrowed::from_raw(ptr) }, PhantomData) } } @@ -1146,10 +1147,8 @@ impl LeanList { /// # Safety /// The pointer must be a valid Lean `List` object. pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 == 1 || include::lean_obj_tag(ptr) as u8 == 1); - Self(LeanOwned(ptr)) - } + test_assert!(ptr as usize & 1 == 1 || unsafe { include::lean_obj_tag(ptr) } == 1); + Self(LeanOwned(ptr)) } /// The empty list. @@ -1260,7 +1259,6 @@ impl LeanOption { if self.is_none() { None } else { - #[allow(clippy::cast_possible_truncation)] let val = unsafe { include::lean_ctor_get(self.0.as_raw(), 0) }; Some(LeanBorrowed(val, PhantomData)) } @@ -1273,10 +1271,8 @@ impl LeanOption { /// # Safety /// The pointer must be a valid Lean `Option` object. pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 == 1 || include::lean_obj_tag(ptr) as u8 == 1); - Self(LeanOwned(ptr)) - } + test_assert!(ptr as usize & 1 == 1 || unsafe { include::lean_obj_tag(ptr) } == 1); + Self(LeanOwned(ptr)) } pub fn none() -> Self { @@ -1368,13 +1364,12 @@ impl LeanExcept { /// # Safety /// The pointer must be a valid Lean `Except` object. pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { - unsafe { - debug_assert!(ptr as usize & 1 != 1); - debug_assert!( - include::lean_obj_tag(ptr) as u8 == 0 || include::lean_obj_tag(ptr) as u8 == 1 - ); - Self(LeanOwned(ptr)) - } + test_assert!(ptr as usize & 1 != 1); + test_assert!( + unsafe { include::lean_obj_tag(ptr) } == 0 + || unsafe { include::lean_obj_tag(ptr) } == 1 + ); + Self(LeanOwned(ptr)) } /// Build `Except.ok val`. @@ -1612,35 +1607,35 @@ impl<'a> LeanBorrowed<'a> { /// Interpret as a constructor object. #[inline] pub fn as_ctor(self) -> LeanCtor> { - debug_assert!(!self.is_scalar() && self.tag() <= LEAN_MAX_CTOR_TAG); + test_assert!(!self.is_scalar() && self.tag() <= LEAN_MAX_CTOR_TAG); LeanCtor(self) } /// Interpret as a `String` object. #[inline] pub fn as_string(self) -> LeanString> { - debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_STRING); + test_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_STRING); LeanString(self) } /// Interpret as an `Array` object. #[inline] pub fn as_array(self) -> LeanArray> { - debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_ARRAY); + test_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_ARRAY); LeanArray(self) } /// Interpret as a `List`. #[inline] pub fn as_list(self) -> LeanList> { - debug_assert!(self.is_scalar() || self.tag() == 1); + test_assert!(self.is_scalar() || self.tag() == 1); LeanList(self) } /// Interpret as a `ByteArray` object. #[inline] pub fn as_byte_array(self) -> LeanByteArray> { - debug_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_SCALAR_ARRAY); + test_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_SCALAR_ARRAY); LeanByteArray(self) } } diff --git a/src/test_ffi.rs b/src/test_ffi.rs index b03ba02..664fa95 100644 --- a/src/test_ffi.rs +++ b/src/test_ffi.rs @@ -46,14 +46,16 @@ fn build_nat(n: &Nat) -> LeanOwned { /// Round-trip a Nat: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_nat(nat_ptr: LeanNat>) -> LeanNat { +pub(crate) extern "C" fn rs_roundtrip_nat( + nat_ptr: LeanNat>, +) -> LeanNat { let nat = Nat::from_obj(nat_ptr.inner()); nat.to_lean() } /// Round-trip a String: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_string( +pub(crate) extern "C" fn rs_roundtrip_string( s_ptr: LeanString>, ) -> LeanString { let s = s_ptr.to_string(); @@ -62,7 +64,9 @@ pub extern "C" fn rs_roundtrip_string( /// Round-trip a Bool: decode from Lean, re-encode. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_bool(bool_ptr: LeanBool>) -> LeanBool { +pub(crate) extern "C" fn rs_roundtrip_bool( + bool_ptr: LeanBool>, +) -> LeanBool { let val = bool_ptr.to_bool(); if val { LeanBool::new(LeanOwned::from_enum_tag(1)) @@ -73,7 +77,7 @@ pub extern "C" fn rs_roundtrip_bool(bool_ptr: LeanBool>) -> Lea /// Round-trip a List Nat: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_list_nat( +pub(crate) extern "C" fn rs_roundtrip_list_nat( list_ptr: LeanList>, ) -> LeanList { let nats: Vec = list_ptr.collect(|b| Nat::from_obj(&b)); @@ -83,7 +87,7 @@ pub extern "C" fn rs_roundtrip_list_nat( /// Round-trip an Array Nat: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_nat( +pub(crate) extern "C" fn rs_roundtrip_array_nat( arr_ptr: LeanArray>, ) -> LeanArray { let nats: Vec = arr_ptr.map(|b| Nat::from_obj(&b)); @@ -96,7 +100,7 @@ pub extern "C" fn rs_roundtrip_array_nat( /// Round-trip a ByteArray: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_bytearray( +pub(crate) extern "C" fn rs_roundtrip_bytearray( ba: LeanByteArray>, ) -> LeanByteArray { LeanByteArray::from_bytes(ba.as_bytes()) @@ -104,7 +108,7 @@ pub extern "C" fn rs_roundtrip_bytearray( /// Round-trip an Option Nat: decode from Lean, re-encode to Lean. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_option_nat( +pub(crate) extern "C" fn rs_roundtrip_option_nat( opt: LeanOption>, ) -> LeanOption { if opt.inner().is_scalar() { @@ -118,7 +122,7 @@ pub extern "C" fn rs_roundtrip_option_nat( /// Round-trip a Point (structure with x, y : Nat). #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_point( +pub(crate) extern "C" fn rs_roundtrip_point( point_ptr: LeanPoint>, ) -> LeanPoint { let ctor = point_ptr.as_ctor(); @@ -132,7 +136,7 @@ pub extern "C" fn rs_roundtrip_point( /// Round-trip a NatTree (inductive: leaf Nat | node NatTree NatTree). #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_nat_tree( +pub(crate) extern "C" fn rs_roundtrip_nat_tree( tree_ptr: LeanNatTree>, ) -> LeanNatTree { LeanNatTree::new(roundtrip_nat_tree_recursive(&tree_ptr.as_ctor())) @@ -166,7 +170,7 @@ fn roundtrip_nat_tree_recursive(ctor: &LeanCtor) -> LeanOwned { /// Round-trip a Prod Nat Nat: decode fst/snd, re-encode via LeanProd::new. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_prod_nat_nat( +pub(crate) extern "C" fn rs_roundtrip_prod_nat_nat( pair: LeanProd>, ) -> LeanProd { let fst = Nat::from_obj(&pair.fst()); @@ -180,7 +184,7 @@ pub extern "C" fn rs_roundtrip_prod_nat_nat( /// Round-trip an Except String Nat: decode ok/error, re-encode. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_except_string_nat( +pub(crate) extern "C" fn rs_roundtrip_except_string_nat( exc: LeanExcept>, ) -> LeanExcept { match exc.into_result() { @@ -197,7 +201,9 @@ pub extern "C" fn rs_roundtrip_except_string_nat( /// Build an Except.error from a Rust string (tests LeanExcept::error_string). #[unsafe(no_mangle)] -pub extern "C" fn rs_except_error_string(s: LeanString>) -> LeanExcept { +pub(crate) extern "C" fn rs_except_error_string( + s: LeanString>, +) -> LeanExcept { LeanExcept::error_string(&s.to_string()) } @@ -207,7 +213,7 @@ pub extern "C" fn rs_except_error_string(s: LeanString>) -> Lea /// Build a successful IO result wrapping a Nat (tests LeanIOResult::ok). #[unsafe(no_mangle)] -pub extern "C" fn rs_io_result_ok_nat( +pub(crate) extern "C" fn rs_io_result_ok_nat( nat_ptr: LeanNat>, ) -> LeanIOResult { let nat = Nat::from_obj(nat_ptr.inner()); @@ -216,7 +222,7 @@ pub extern "C" fn rs_io_result_ok_nat( /// Build an IO error from a string (tests LeanIOResult::error_string). #[unsafe(no_mangle)] -pub extern "C" fn rs_io_result_error_string( +pub(crate) extern "C" fn rs_io_result_error_string( s: LeanString>, ) -> LeanIOResult { LeanIOResult::error_string(&s.to_string()) @@ -230,7 +236,7 @@ pub extern "C" fn rs_io_result_error_string( /// Lean layout: 1 obj field, then scalars by descending size: u64(0), u32(8), u8(12). /// Total scalar size: 8 + 4 + 1 = 13 bytes. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_scalar_struct( +pub(crate) extern "C" fn rs_roundtrip_scalar_struct( ptr: LeanScalarStruct>, ) -> LeanScalarStruct { let ctor = ptr.as_ctor(); @@ -253,19 +259,19 @@ pub extern "C" fn rs_roundtrip_scalar_struct( /// Round-trip a UInt32 (passed as raw uint32_t by Lean FFI). #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_uint32(val: u32) -> u32 { +pub(crate) extern "C" fn rs_roundtrip_uint32(val: u32) -> u32 { val } /// Round-trip a UInt64 (passed as raw uint64_t by Lean FFI). #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_uint64(val: u64) -> u64 { +pub(crate) extern "C" fn rs_roundtrip_uint64(val: u64) -> u64 { val } /// Round-trip an Array UInt32. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_uint32( +pub(crate) extern "C" fn rs_roundtrip_array_uint32( arr_ptr: LeanArray>, ) -> LeanArray { let len = arr_ptr.len(); @@ -279,7 +285,7 @@ pub extern "C" fn rs_roundtrip_array_uint32( /// Round-trip an Array UInt64. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_uint64( +pub(crate) extern "C" fn rs_roundtrip_array_uint64( arr_ptr: LeanArray>, ) -> LeanArray { let len = arr_ptr.len(); @@ -309,7 +315,7 @@ static RUST_DATA_CLASS: LazyLock = /// Create a LeanExternal from three Lean values. /// Note: label is @& (borrowed), x/y are scalar UInt64. #[unsafe(no_mangle)] -pub extern "C" fn rs_external_create( +pub(crate) extern "C" fn rs_external_create( x: u64, y: u64, label: LeanString>, @@ -325,7 +331,7 @@ pub extern "C" fn rs_external_create( /// Read the x field from a LeanExternal (@& borrowed). #[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_x(obj: LeanRustData>) -> u64 { +pub(crate) extern "C" fn rs_external_get_x(obj: LeanRustData>) -> u64 { let ext = unsafe { LeanExternal::>::from_raw_borrowed(obj.as_raw()) }; ext.get().x @@ -333,7 +339,7 @@ pub extern "C" fn rs_external_get_x(obj: LeanRustData>) -> u64 /// Read the y field from a LeanExternal (@& borrowed). #[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_y(obj: LeanRustData>) -> u64 { +pub(crate) extern "C" fn rs_external_get_y(obj: LeanRustData>) -> u64 { let ext = unsafe { LeanExternal::>::from_raw_borrowed(obj.as_raw()) }; ext.get().y @@ -341,7 +347,7 @@ pub extern "C" fn rs_external_get_y(obj: LeanRustData>) -> u64 /// Read the label field from a LeanExternal (@& borrowed). #[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_label( +pub(crate) extern "C" fn rs_external_get_label( obj: LeanRustData>, ) -> LeanString { let ext = @@ -357,7 +363,7 @@ pub extern "C" fn rs_external_get_label( /// Lean layout: 1 obj, then descending size: u64(0), f64(8), u32(16), f32(20), u16(24), u8(26). /// Total scalar: 27 bytes. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_ext_scalar_struct( +pub(crate) extern "C" fn rs_roundtrip_ext_scalar_struct( ptr: LeanExtScalarStruct>, ) -> LeanExtScalarStruct { let ctor = ptr.as_ctor(); @@ -388,7 +394,7 @@ pub extern "C" fn rs_roundtrip_ext_scalar_struct( /// Lean layout: 1 obj field, then usize (slot 0), then u8 at scalar offset 0. /// Alloc: num_objs=1, scalar_sz=9 (8 for usize slot + 1 for u8). #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_usize_struct( +pub(crate) extern "C" fn rs_roundtrip_usize_struct( ptr: LeanUSizeStruct>, ) -> LeanUSizeStruct { let ctor = ptr.as_ctor(); @@ -409,25 +415,25 @@ pub extern "C" fn rs_roundtrip_usize_struct( /// Round-trip a Float (f64) — passed as raw scalar across FFI. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_float(val: f64) -> f64 { +pub(crate) extern "C" fn rs_roundtrip_float(val: f64) -> f64 { val } /// Round-trip a Float32 (f32) — passed as raw scalar across FFI. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_float32(val: f32) -> f32 { +pub(crate) extern "C" fn rs_roundtrip_float32(val: f32) -> f32 { val } /// Round-trip a USize — passed as raw scalar across FFI. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_usize(val: usize) -> usize { +pub(crate) extern "C" fn rs_roundtrip_usize(val: usize) -> usize { val } /// Round-trip an Array Float. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_float( +pub(crate) extern "C" fn rs_roundtrip_array_float( arr_ptr: LeanArray>, ) -> LeanArray { let len = arr_ptr.len(); @@ -441,7 +447,7 @@ pub extern "C" fn rs_roundtrip_array_float( /// Round-trip an Array Float32. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_float32( +pub(crate) extern "C" fn rs_roundtrip_array_float32( arr_ptr: LeanArray>, ) -> LeanArray { let len = arr_ptr.len(); @@ -459,7 +465,7 @@ pub extern "C" fn rs_roundtrip_array_float32( /// Round-trip a String using LeanString::from_bytes instead of LeanString::new. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_string_from_bytes( +pub(crate) extern "C" fn rs_roundtrip_string_from_bytes( s_ptr: LeanString>, ) -> LeanString { let s = s_ptr.to_string(); @@ -472,7 +478,7 @@ pub extern "C" fn rs_roundtrip_string_from_bytes( /// Round-trip an Array Nat by pushing each element into a new array. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_array_push( +pub(crate) extern "C" fn rs_roundtrip_array_push( arr_ptr: LeanArray>, ) -> LeanArray { let nats: Vec = arr_ptr.map(|b| Nat::from_obj(&b)); @@ -490,7 +496,7 @@ pub extern "C" fn rs_roundtrip_array_push( /// Round-trip a Nat with owned arg (no @&). Tests that LeanOwned Drop correctly /// calls lean_dec on the input without double-free or leak. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_nat_roundtrip(nat_ptr: LeanNat) -> LeanNat { +pub(crate) extern "C" fn rs_owned_nat_roundtrip(nat_ptr: LeanNat) -> LeanNat { let nat = Nat::from_obj(nat_ptr.inner()); nat.to_lean() // nat_ptr drops here → lean_dec (correct for owned arg) @@ -498,7 +504,9 @@ pub extern "C" fn rs_owned_nat_roundtrip(nat_ptr: LeanNat) -> LeanNat /// Round-trip a String with owned arg. Tests LeanOwned Drop on strings. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_string_roundtrip(s_ptr: LeanString) -> LeanString { +pub(crate) extern "C" fn rs_owned_string_roundtrip( + s_ptr: LeanString, +) -> LeanString { let s = s_ptr.to_string(); LeanString::new(&s) // s_ptr drops here → lean_dec @@ -506,7 +514,7 @@ pub extern "C" fn rs_owned_string_roundtrip(s_ptr: LeanString) -> Lea /// Round-trip an Array Nat with owned arg. Tests LeanOwned Drop on arrays. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_array_nat_roundtrip( +pub(crate) extern "C" fn rs_owned_array_nat_roundtrip( arr_ptr: LeanArray, ) -> LeanArray { let nats: Vec = arr_ptr.map(|b| Nat::from_obj(&b)); @@ -520,7 +528,7 @@ pub extern "C" fn rs_owned_array_nat_roundtrip( /// Round-trip a List Nat with owned arg. Tests LeanOwned Drop on lists. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_list_nat_roundtrip( +pub(crate) extern "C" fn rs_owned_list_nat_roundtrip( list_ptr: LeanList, ) -> LeanList { let nats: Vec = list_ptr.collect(|b| Nat::from_obj(&b)); @@ -532,7 +540,7 @@ pub extern "C" fn rs_owned_list_nat_roundtrip( /// Two owned args: take an array and a nat (both owned), append nat to array. /// Tests Drop on two owned args simultaneously. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_append_nat( +pub(crate) extern "C" fn rs_owned_append_nat( arr: LeanArray, nat: LeanNat, ) -> LeanArray { @@ -545,7 +553,9 @@ pub extern "C" fn rs_owned_append_nat( /// Owned arg that we explicitly drop early (by letting it go out of scope) /// then return a completely new value. Tests that Drop runs at the right time. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_drop_and_replace(s: LeanString) -> LeanString { +pub(crate) extern "C" fn rs_owned_drop_and_replace( + s: LeanString, +) -> LeanString { let len = s.byte_len(); drop(s); // explicit early drop → lean_dec LeanString::new(&format!("replaced:{len}")) @@ -554,7 +564,7 @@ pub extern "C" fn rs_owned_drop_and_replace(s: LeanString) -> LeanStr /// Three owned args: merge three lists into one. /// Tests Drop on multiple owned args with complex ownership flow. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_merge_lists( +pub(crate) extern "C" fn rs_owned_merge_lists( a: LeanList, b: LeanList, c: LeanList, @@ -576,7 +586,7 @@ pub extern "C" fn rs_owned_merge_lists( /// Owned ByteArray: reverse the bytes and return. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_reverse_bytearray( +pub(crate) extern "C" fn rs_owned_reverse_bytearray( ba: LeanByteArray, ) -> LeanByteArray { let bytes = ba.as_bytes(); @@ -587,7 +597,7 @@ pub extern "C" fn rs_owned_reverse_bytearray( /// Owned Point (ctor): negate both fields (swap x and y + add them). #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_point_sum(point: LeanCtor) -> LeanNat { +pub(crate) extern "C" fn rs_owned_point_sum(point: LeanCtor) -> LeanNat { let x = Nat::from_obj(&point.get(0)); let y = Nat::from_obj(&point.get(1)); Nat(x.0 + y.0).to_lean() @@ -596,7 +606,9 @@ pub extern "C" fn rs_owned_point_sum(point: LeanCtor) -> LeanNat) -> LeanNat { +pub(crate) extern "C" fn rs_owned_except_transform( + exc: LeanExcept, +) -> LeanNat { match exc.into_result() { Ok(val) => { let nat = Nat::from_obj(&val); @@ -612,7 +624,7 @@ pub extern "C" fn rs_owned_except_transform(exc: LeanExcept) -> LeanN /// Owned Option: if some(n), return n*n; if none, return 0. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_option_square(opt: LeanOption) -> LeanNat { +pub(crate) extern "C" fn rs_owned_option_square(opt: LeanOption) -> LeanNat { if opt.inner().is_scalar() { Nat::ZERO.to_lean() } else { @@ -624,7 +636,7 @@ pub extern "C" fn rs_owned_option_square(opt: LeanOption) -> LeanNat< /// Owned Prod: return fst * snd. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_prod_multiply(pair: LeanProd) -> LeanNat { +pub(crate) extern "C" fn rs_owned_prod_multiply(pair: LeanProd) -> LeanNat { let fst = Nat::from_obj(&pair.fst()); let snd = Nat::from_obj(&pair.snd()); Nat(fst.0 * snd.0).to_lean() @@ -638,7 +650,7 @@ pub extern "C" fn rs_owned_prod_multiply(pair: LeanProd) -> LeanNat) -> u64 { +pub(crate) extern "C" fn rs_owned_scalar_sum(ptr: LeanScalarStruct) -> u64 { // Lean descending-size layout: u64(0), u32(8), u8(12) let ctor = ptr.as_ctor(); let u64val = ctor.get_u64(1, 0); @@ -655,7 +667,7 @@ pub extern "C" fn rs_owned_scalar_sum(ptr: LeanScalarStruct) -> u64 { /// Clone an owned array and return the sum of lengths of both copies. /// Tests that Clone (lean_inc) produces a valid second handle. #[unsafe(no_mangle)] -pub extern "C" fn rs_clone_array_len_sum(arr_ptr: LeanArray>) -> usize { +pub(crate) extern "C" fn rs_clone_array_len_sum(arr_ptr: LeanArray>) -> usize { // Create an owned copy, then clone it let owned: LeanArray = { let nats: Vec = arr_ptr.map(|b| Nat::from_obj(&b)); @@ -666,18 +678,18 @@ pub extern "C" fn rs_clone_array_len_sum(arr_ptr: LeanArray>) - arr }; let cloned = owned.clone(); - let sum = owned.len() + cloned.len(); + // Both owned and cloned drop here → lean_dec called twice (correct: clone did lean_inc) - sum + owned.len() + cloned.len() } /// Clone an owned string and return the sum of byte lengths of both copies. #[unsafe(no_mangle)] -pub extern "C" fn rs_clone_string_len_sum(s: LeanString>) -> usize { +pub(crate) extern "C" fn rs_clone_string_len_sum(s: LeanString>) -> usize { let owned = LeanString::new(&s.to_string()); let cloned = owned.clone(); - let sum = owned.byte_len() + cloned.byte_len(); - sum + + owned.byte_len() + cloned.byte_len() } /// Clone an owned Except and read from both copies. Tests that lean_inc @@ -685,7 +697,7 @@ pub extern "C" fn rs_clone_string_len_sum(s: LeanString>) -> us /// copies can be independently dropped (lean_dec) without double-free. /// Returns: for ok(n), 2*n (read n from both copies); for error(s), 2*byte_len. #[unsafe(no_mangle)] -pub extern "C" fn rs_clone_except(exc: LeanExcept) -> LeanNat { +pub(crate) extern "C" fn rs_clone_except(exc: LeanExcept) -> LeanNat { let cloned = exc.clone(); let result = match (exc.into_result(), cloned.into_result()) { (Ok(v1), Ok(v2)) => Nat(Nat::from_obj(&v1).0 + Nat::from_obj(&v2).0), @@ -701,7 +713,7 @@ pub extern "C" fn rs_clone_except(exc: LeanExcept) -> LeanNat) -> LeanNat { +pub(crate) extern "C" fn rs_clone_list(list: LeanList) -> LeanNat { let cloned = list.clone(); let count1 = list.iter().count(); let count2 = cloned.iter().count(); @@ -710,14 +722,14 @@ pub extern "C" fn rs_clone_list(list: LeanList) -> LeanNat /// Clone an owned ByteArray, sum byte lengths of both. Tests lean_inc on scalar arrays. #[unsafe(no_mangle)] -pub extern "C" fn rs_clone_bytearray(ba: LeanByteArray) -> LeanNat { +pub(crate) extern "C" fn rs_clone_bytearray(ba: LeanByteArray) -> LeanNat { let cloned = ba.clone(); Nat::from((ba.len() + cloned.len()) as u64).to_lean() } /// Clone an owned Option Nat: if some(n), return 2*n from both copies; if none, return 0. #[unsafe(no_mangle)] -pub extern "C" fn rs_clone_option(opt: LeanOption) -> LeanNat { +pub(crate) extern "C" fn rs_clone_option(opt: LeanOption) -> LeanNat { let cloned = opt.clone(); let result = match (opt.to_option(), cloned.to_option()) { (Some(v1), Some(v2)) => Nat(Nat::from_obj(&v1).0 + Nat::from_obj(&v2).0), @@ -729,7 +741,7 @@ pub extern "C" fn rs_clone_option(opt: LeanOption) -> LeanNat) -> LeanNat { +pub(crate) extern "C" fn rs_clone_prod(pair: LeanProd) -> LeanNat { let cloned = pair.clone(); let sum = Nat::from_obj(&pair.fst()).0 + Nat::from_obj(&pair.snd()).0 @@ -740,7 +752,7 @@ pub extern "C" fn rs_clone_prod(pair: LeanProd) -> LeanNat /// Owned ByteArray roundtrip: read bytes, rebuild. Tests LeanOwned Drop on scalar arrays. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_bytearray_roundtrip( +pub(crate) extern "C" fn rs_owned_bytearray_roundtrip( ba: LeanByteArray, ) -> LeanByteArray { LeanByteArray::from_bytes(ba.as_bytes()) @@ -749,7 +761,9 @@ pub extern "C" fn rs_owned_bytearray_roundtrip( /// Owned Option roundtrip: decode and re-encode. Tests Drop on Option constructor. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_option_roundtrip(opt: LeanOption) -> LeanOption { +pub(crate) extern "C" fn rs_owned_option_roundtrip( + opt: LeanOption, +) -> LeanOption { match opt.to_option() { None => LeanOption::none(), Some(val) => LeanOption::some(Nat::from_obj(&val).to_lean()), @@ -758,7 +772,7 @@ pub extern "C" fn rs_owned_option_roundtrip(opt: LeanOption) -> LeanO /// Owned Prod roundtrip: decode fst/snd, rebuild. Tests Drop on Prod constructor. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_prod_roundtrip(pair: LeanProd) -> LeanProd { +pub(crate) extern "C" fn rs_owned_prod_roundtrip(pair: LeanProd) -> LeanProd { let f = Nat::from_obj(&pair.fst()); let s = Nat::from_obj(&pair.snd()); LeanProd::new(build_nat(&f), build_nat(&s)) @@ -766,7 +780,9 @@ pub extern "C" fn rs_owned_prod_roundtrip(pair: LeanProd) -> LeanProd /// Owned IOResult: extract value from ok result, return it. Tests Drop on IOResult. #[unsafe(no_mangle)] -pub extern "C" fn rs_owned_io_result_value(result: LeanIOResult) -> LeanNat { +pub(crate) extern "C" fn rs_owned_io_result_value( + result: LeanIOResult, +) -> LeanNat { // IOResult ok = tag 0, fields: [value, world]; error = tag 1 let ctor = result.as_ctor(); if ctor.tag() == 0 { @@ -782,7 +798,9 @@ pub extern "C" fn rs_owned_io_result_value(result: LeanIOResult) -> L /// Sum all Nats in an array using the data() slice API. #[unsafe(no_mangle)] -pub extern "C" fn rs_array_data_sum(arr_ptr: LeanArray>) -> LeanNat { +pub(crate) extern "C" fn rs_array_data_sum( + arr_ptr: LeanArray>, +) -> LeanNat { let mut sum = Nat::ZERO; for elem in arr_ptr.data() { sum = Nat(sum.0 + Nat::from_obj(elem).0); @@ -796,7 +814,7 @@ pub extern "C" fn rs_array_data_sum(arr_ptr: LeanArray>) -> Lea /// Test LeanOption API: return the Nat inside a Some, or 0 for None. #[unsafe(no_mangle)] -pub extern "C" fn rs_option_unwrap_or_zero( +pub(crate) extern "C" fn rs_option_unwrap_or_zero( opt: LeanOption>, ) -> LeanNat { match opt.to_option() { @@ -811,7 +829,7 @@ pub extern "C" fn rs_option_unwrap_or_zero( /// Test LeanProd fst/snd API: swap the elements of a pair. #[unsafe(no_mangle)] -pub extern "C" fn rs_prod_swap(pair: LeanProd>) -> LeanProd { +pub(crate) extern "C" fn rs_prod_swap(pair: LeanProd>) -> LeanProd { let fst = Nat::from_obj(&pair.fst()); let snd = Nat::from_obj(&pair.snd()); LeanProd::new(build_nat(&snd), build_nat(&fst)) @@ -852,7 +870,9 @@ fn borrow_except_value<'a>(exc: &'a LeanExcept) -> LeanBorrowed<'a /// Receives a Prod (Array Nat, Array Nat), borrows fst and snd, then borrows /// elements from each array, and sums everything — all without any lean_inc. #[unsafe(no_mangle)] -pub extern "C" fn rs_borrowed_result_chain(pair: LeanProd>) -> LeanNat { +pub(crate) extern "C" fn rs_borrowed_result_chain( + pair: LeanProd>, +) -> LeanNat { // Get borrowed references to the two arrays (b_lean_obj_res pattern) let fst_ref = borrow_fst(&pair); let snd_ref = borrow_snd(&pair); @@ -889,7 +909,7 @@ pub extern "C" fn rs_borrowed_result_chain(pair: LeanProd>) -> /// Test borrowed result from Except. Borrows the inner value without lean_inc, /// reads it, and returns a new owned Nat. #[unsafe(no_mangle)] -pub extern "C" fn rs_borrowed_except_value( +pub(crate) extern "C" fn rs_borrowed_except_value( exc: LeanExcept>, ) -> LeanNat { let val = borrow_except_value(&exc); @@ -907,7 +927,7 @@ pub extern "C" fn rs_borrowed_except_value( /// Round-trip an Array (Array Nat) — tests nested ownership. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_nested_array( +pub(crate) extern "C" fn rs_roundtrip_nested_array( outer: LeanArray>, ) -> LeanArray { let len = outer.len(); @@ -929,7 +949,7 @@ pub extern "C" fn rs_roundtrip_nested_array( /// Round-trip a List (List Nat) — tests nested list iteration. #[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_nested_list( +pub(crate) extern "C" fn rs_roundtrip_nested_list( outer: LeanList>, ) -> LeanList { let inner_lists: Vec> = outer.collect(|inner_ref| { @@ -947,7 +967,7 @@ pub extern "C" fn rs_roundtrip_nested_list( /// Test LeanExcept-like pattern: if ok (tag 1), return nat + 1; if error (tag 0), return 0. #[unsafe(no_mangle)] -pub extern "C" fn rs_except_map_ok(exc: LeanExcept>) -> LeanNat { +pub(crate) extern "C" fn rs_except_map_ok(exc: LeanExcept>) -> LeanNat { let ctor = exc.as_ctor(); if ctor.tag() == 1 { // ok: field 0 is the Nat value @@ -966,7 +986,9 @@ pub extern "C" fn rs_except_map_ok(exc: LeanExcept>) -> LeanNat /// Read all elements from a borrowed array, compute sum. /// Tests that multiple borrows from the same source don't interfere. #[unsafe(no_mangle)] -pub extern "C" fn rs_multi_borrow_sum(arr: LeanArray>) -> LeanNat { +pub(crate) extern "C" fn rs_multi_borrow_sum( + arr: LeanArray>, +) -> LeanNat { let mut sum = Nat::ZERO; // First pass: read all via get() for i in 0..arr.len() { @@ -996,7 +1018,7 @@ pub extern "C" fn rs_multi_borrow_sum(arr: LeanArray>) -> LeanN /// Convert List Nat → Array Nat using only push (not alloc+set). #[unsafe(no_mangle)] -pub extern "C" fn rs_list_to_array_via_push( +pub(crate) extern "C" fn rs_list_to_array_via_push( list: LeanList>, ) -> LeanArray { let mut arr = LeanArray::alloc(0); @@ -1014,7 +1036,7 @@ pub extern "C" fn rs_list_to_array_via_push( /// Take a borrowed Nat, convert to owned via to_owned_ref, return it. /// Tests that to_owned_ref (lean_inc) produces a valid owned handle. #[unsafe(no_mangle)] -pub extern "C" fn rs_borrow_to_owned(nat: LeanNat>) -> LeanNat { +pub(crate) extern "C" fn rs_borrow_to_owned(nat: LeanNat>) -> LeanNat { LeanNat::new(nat.inner().to_owned_ref()) } @@ -1024,25 +1046,27 @@ pub extern "C" fn rs_borrow_to_owned(nat: LeanNat>) -> LeanNat< /// Create and return an empty array. Unit is passed as lean_box(0). #[unsafe(no_mangle)] -pub extern "C" fn rs_make_empty_array(_unit: LeanBorrowed<'_>) -> LeanArray { +pub(crate) extern "C" fn rs_make_empty_array(_unit: LeanBorrowed<'_>) -> LeanArray { LeanArray::alloc(0) } /// Create and return an empty list. #[unsafe(no_mangle)] -pub extern "C" fn rs_make_empty_list(_unit: LeanBorrowed<'_>) -> LeanList { +pub(crate) extern "C" fn rs_make_empty_list(_unit: LeanBorrowed<'_>) -> LeanList { LeanList::nil() } /// Create and return an empty byte array. #[unsafe(no_mangle)] -pub extern "C" fn rs_make_empty_bytearray(_unit: LeanBorrowed<'_>) -> LeanByteArray { +pub(crate) extern "C" fn rs_make_empty_bytearray( + _unit: LeanBorrowed<'_>, +) -> LeanByteArray { LeanByteArray::alloc(0) } /// Create and return an empty string. #[unsafe(no_mangle)] -pub extern "C" fn rs_make_empty_string(_unit: LeanBorrowed<'_>) -> LeanString { +pub(crate) extern "C" fn rs_make_empty_string(_unit: LeanBorrowed<'_>) -> LeanString { LeanString::new("") } @@ -1053,14 +1077,14 @@ pub extern "C" fn rs_make_empty_string(_unit: LeanBorrowed<'_>) -> LeanString> 1 = 2^63 - 1 #[unsafe(no_mangle)] -pub extern "C" fn rs_nat_max_scalar(_unit: LeanBorrowed<'_>) -> LeanNat { +pub(crate) extern "C" fn rs_nat_max_scalar(_unit: LeanBorrowed<'_>) -> LeanNat { let max_scalar = usize::MAX >> 1; LeanNat::new(LeanOwned::box_usize(max_scalar)) } /// Return max_scalar + 1 which must be heap-allocated. #[unsafe(no_mangle)] -pub extern "C" fn rs_nat_min_heap(_unit: LeanBorrowed<'_>) -> LeanNat { +pub(crate) extern "C" fn rs_nat_min_heap(_unit: LeanBorrowed<'_>) -> LeanNat { let max_scalar = (usize::MAX >> 1) as u64; Nat::from(max_scalar + 1).to_lean() } @@ -1072,7 +1096,7 @@ pub extern "C" fn rs_nat_min_heap(_unit: LeanBorrowed<'_>) -> LeanNat /// Read all fields from a single borrowed external handle and return as a string. /// Tests that multiple reads from a borrowed external don't corrupt state. #[unsafe(no_mangle)] -pub extern "C" fn rs_external_all_fields( +pub(crate) extern "C" fn rs_external_all_fields( obj: LeanRustData>, ) -> LeanString { let ext = @@ -1091,14 +1115,16 @@ pub extern "C" fn rs_external_all_fields( /// Check if a borrowed Lean object is persistent (m_rc == 0). /// Module-level Lean definitions become persistent after initialization. #[unsafe(no_mangle)] -pub extern "C" fn rs_is_persistent(obj: LeanNat>) -> u8 { +pub(crate) extern "C" fn rs_is_persistent(obj: LeanNat>) -> u8 { if obj.inner().is_persistent() { 1 } else { 0 } } /// Read a Nat from a persistent object (passed as @& borrowed). /// Tests that field access works normally on persistent objects. #[unsafe(no_mangle)] -pub extern "C" fn rs_read_persistent_nat(obj: LeanNat>) -> LeanNat { +pub(crate) extern "C" fn rs_read_persistent_nat( + obj: LeanNat>, +) -> LeanNat { let nat = Nat::from_obj(obj.inner()); nat.to_lean() } @@ -1106,20 +1132,22 @@ pub extern "C" fn rs_read_persistent_nat(obj: LeanNat>) -> Lean /// Read fields from a persistent LeanPoint (structure with x, y : Nat). /// Tests that ctor field access works on persistent objects. #[unsafe(no_mangle)] -pub extern "C" fn rs_read_persistent_point( +pub(crate) extern "C" fn rs_read_persistent_point( point: LeanPoint>, ) -> LeanNat { let ctor = point.as_ctor(); let x = Nat::from_obj(&ctor.get(0)); let y = Nat::from_obj(&ctor.get(1)); // Return x + y as a new (non-persistent) Nat - Nat(x.0 + y.0).to_lean().into() + Nat(x.0 + y.0).to_lean() } /// Read from a persistent array. Tests that array element access works /// on persistent objects (elements in persistent arrays are also persistent). #[unsafe(no_mangle)] -pub extern "C" fn rs_read_persistent_array(arr: LeanArray>) -> LeanNat { +pub(crate) extern "C" fn rs_read_persistent_array( + arr: LeanArray>, +) -> LeanNat { let mut sum = Nat::ZERO; for elem in arr.iter() { sum = Nat(sum.0 + Nat::from_obj(&elem).0); @@ -1129,7 +1157,9 @@ pub extern "C" fn rs_read_persistent_array(arr: LeanArray>) -> /// Read from a persistent string. Tests that string access works on persistent objects. #[unsafe(no_mangle)] -pub extern "C" fn rs_read_persistent_string(s: LeanString>) -> LeanNat { +pub(crate) extern "C" fn rs_read_persistent_string( + s: LeanString>, +) -> LeanNat { Nat::from(s.byte_len() as u64).to_lean() } @@ -1137,7 +1167,7 @@ pub extern "C" fn rs_read_persistent_string(s: LeanString>) -> /// "virtual RC token" but lean_dec is a no-op for persistent objects (m_rc == 0). /// This tests that LeanOwned::drop doesn't crash on persistent data. #[unsafe(no_mangle)] -pub extern "C" fn rs_drop_persistent_nat(obj: LeanNat) -> LeanNat { +pub(crate) extern "C" fn rs_drop_persistent_nat(obj: LeanNat) -> LeanNat { let nat = Nat::from_obj(obj.inner()); nat.to_lean() // obj drops here → lean_dec_ref → no-op because m_rc == 0 @@ -1153,7 +1183,7 @@ use crate::LeanShared; /// each thread reads all elements, then all clones are dropped. /// Tests that lean_mark_mt + atomic refcounting works correctly. #[unsafe(no_mangle)] -pub extern "C" fn rs_shared_parallel_read( +pub(crate) extern "C" fn rs_shared_parallel_read( arr: LeanArray>, n_threads: usize, ) -> LeanNat { @@ -1189,7 +1219,7 @@ pub extern "C" fn rs_shared_parallel_read( /// Mark a Nat as MT, clone it to N threads, each reads it. /// Simpler than array — tests basic scalar/heap Nat across threads. #[unsafe(no_mangle)] -pub extern "C" fn rs_shared_parallel_nat( +pub(crate) extern "C" fn rs_shared_parallel_nat( nat: LeanNat>, n_threads: usize, ) -> LeanNat { @@ -1214,7 +1244,7 @@ pub extern "C" fn rs_shared_parallel_nat( /// Mark a string as MT, clone to N threads, each reads byte_len. /// Returns sum of all byte_len readings. #[unsafe(no_mangle)] -pub extern "C" fn rs_shared_parallel_string( +pub(crate) extern "C" fn rs_shared_parallel_string( s: LeanString>, n_threads: usize, ) -> LeanNat { @@ -1237,7 +1267,7 @@ pub extern "C" fn rs_shared_parallel_string( /// Stress test: mark array as MT, spawn many threads that each clone /// and drop rapidly. Tests atomic refcount under contention. #[unsafe(no_mangle)] -pub extern "C" fn rs_shared_contention_stress( +pub(crate) extern "C" fn rs_shared_contention_stress( arr: LeanArray>, n_threads: usize, clones_per_thread: usize, @@ -1267,22 +1297,24 @@ pub extern "C" fn rs_shared_contention_stress( /// Test into_owned: mark as MT, convert back to LeanOwned, read value. /// Verifies the MT-marked object is still usable after unwrapping. #[unsafe(no_mangle)] -pub extern "C" fn rs_shared_into_owned(nat: LeanNat>) -> LeanNat { +pub(crate) extern "C" fn rs_shared_into_owned( + nat: LeanNat>, +) -> LeanNat { let shared = LeanShared::new(nat.inner().to_owned_ref()); let cloned = shared.clone(); // Convert one back to LeanOwned let owned = cloned.into_owned(); let val = Nat::from_obj(&unsafe { LeanBorrowed::from_raw(owned.as_raw()) }); - let result = val.to_lean(); + // owned drops (still MT-marked, lean_dec_ref handles it) // shared drops (atomic lean_dec) - result + val.to_lean() } /// Mark a Point (constructor with 2 obj fields) as MT, read fields from threads. /// Tests that lean_mark_mt correctly walks the constructor's object graph. #[unsafe(no_mangle)] -pub extern "C" fn rs_shared_parallel_point( +pub(crate) extern "C" fn rs_shared_parallel_point( point: LeanPoint>, n_threads: usize, ) -> LeanNat { @@ -1308,7 +1340,7 @@ pub extern "C" fn rs_shared_parallel_point( /// Wrap a persistent Nat in LeanShared (lean_mark_mt is skipped for persistent). /// Clone to threads and read — verifies the persistent skip path works. #[unsafe(no_mangle)] -pub extern "C" fn rs_shared_persistent_nat( +pub(crate) extern "C" fn rs_shared_persistent_nat( nat: LeanNat>, n_threads: usize, ) -> LeanNat { From 53c90ecf051023158b727e926a6141e72b106395 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 20 Mar 2026 00:06:21 -0400 Subject: [PATCH 08/10] Fixup --- src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib.rs b/src/lib.rs index 61b42d5..3586a9d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -67,7 +67,7 @@ macro_rules! lean_domain_type { ($($(#[$meta:meta])* $name:ident;)*) => {$( $(#[$meta])* #[repr(transparent)] - pub struct $name(R); + pub struct $name(pub R); impl Clone for $name { #[inline] From ffbbc0882afa1162c0806c8a5c63ea5da631dd6c Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 20 Mar 2026 11:50:03 -0400 Subject: [PATCH 09/10] Cleanup --- src/nat.rs | 13 +++--------- src/object.rs | 56 ++++++++++++++++++++++++++++++++++++++++++--------- 2 files changed, 49 insertions(+), 20 deletions(-) diff --git a/src/nat.rs b/src/nat.rs index 4a005cf..61fa619 100644 --- a/src/nat.rs +++ b/src/nat.rs @@ -40,8 +40,7 @@ impl Nat { /// and heap-allocated (GMP `mpz_object`) representations. pub fn from_obj(obj: &impl LeanRef) -> Nat { if obj.is_scalar() { - let u = obj.unbox_usize(); - Nat(BigUint::from_bytes_le(&u.to_le_bytes())) + Nat(BigUint::from(obj.unbox_usize() as u64)) } else { // Heap-allocated big integer (mpz_object) let mpz: &MpzObject = unsafe { &*obj.as_raw().cast() }; @@ -70,14 +69,8 @@ impl Nat { } return LeanNat::new(LeanOwned::from_nat_u64(val)); } - // For values larger than u64, convert to limbs and use GMP - let bytes = self.to_le_bytes(); - let mut limbs: Vec = Vec::with_capacity(bytes.len().div_ceil(8)); - for chunk in bytes.chunks(8) { - let mut arr = [0u8; 8]; - arr[..chunk.len()].copy_from_slice(chunk); - limbs.push(u64::from_le_bytes(arr)); - } + // For values larger than u64, access limbs directly (no byte round-trip) + let limbs = self.0.to_u64_digits(); LeanNat::new(unsafe { lean_nat_from_limbs(limbs.len(), limbs.as_ptr()) }) } } diff --git a/src/object.rs b/src/object.rs index 1e52f34..34da301 100644 --- a/src/object.rs +++ b/src/object.rs @@ -176,6 +176,13 @@ impl LeanRef for LeanOwned { } impl LeanOwned { + /// Borrow this owned reference. The returned `LeanBorrowed` is + /// lifetime-bounded to `&self`. No refcount change. + #[inline] + pub fn borrow(&self) -> LeanBorrowed<'_> { + unsafe { LeanBorrowed::from_raw(self.0) } + } + /// Wrap a raw pointer, taking ownership of the reference count. /// /// # Safety @@ -1185,6 +1192,24 @@ impl> FromIterator for LeanList { } } +impl<'a> LeanList> { + /// Iterate elements with the original borrow lifetime `'a`. + /// + /// Unlike [`iter()`](LeanList::iter) (which ties the output lifetime to + /// `&self`), this preserves the lifetime of the underlying Lean objects. + /// Use this when the list is a local `Copy` value and the elements need to + /// outlive the list binding. + #[inline] + pub fn into_iter(self) -> LeanListIter<'a> { + LeanListIter(self.0) + } + + /// Collect elements into a `Vec` with the original borrow lifetime. + pub fn to_vec(self) -> Vec> { + self.into_iter().collect() + } +} + /// Iterator over the elements of a `LeanList`. pub struct LeanListIter<'a>(LeanBorrowed<'a>); @@ -1646,21 +1671,32 @@ impl<'a> LeanBorrowed<'a> { /// Thread-safe owned Lean object with atomic refcounting. /// -/// Created by calling [`lean_mark_mt`] on the object graph, which transitions -/// all reachable objects from single-threaded to multi-threaded mode. -/// After marking, [`lean_inc_ref`] / [`lean_dec_ref`] use atomic operations, -/// so [`LeanOwned`]'s existing `Clone` and `Drop` are thread-safe. +/// Lean objects track refcounts in `m_rc`: +/// - `m_rc > 0` → single-threaded (ST): non-atomic inc/dec +/// - `m_rc < 0` → multi-threaded (MT): atomic inc/dec (negative magnitude is the count) +/// - `m_rc == 0` → persistent: inc/dec are no-ops +/// +/// [`LeanShared::new`] calls `lean_mark_mt` which recursively transitions +/// the entire reachable object graph from ST to MT by negating `m_rc`. +/// After marking, `lean_inc_ref` uses `atomic_fetch_sub` (subtracting makes +/// the count more negative) and `lean_dec_ref_cold` uses `atomic_fetch_add` +/// (adding towards zero; freeing when previous value was -1). +/// +/// This means [`LeanOwned`]'s existing `Clone` (`lean_inc_ref`) and `Drop` +/// (`lean_dec_ref`) are automatically thread-safe on MT-marked objects — +/// no custom refcount logic is needed in `LeanShared`. /// -/// Scalars (tagged pointers with bit 0 set) and persistent objects -/// (`m_rc == 0`) are unaffected by MT marking. +/// Calling `lean_mark_mt` on an already-MT object is a single branch +/// (`lean_is_st` check) with no traversal, so it's safe to mark +/// sub-objects of an already-marked parent. #[repr(transparent)] pub struct LeanShared(LeanOwned); // SAFETY: lean_mark_mt transitions the entire reachable object graph to -// multi-threaded mode. After marking, lean_inc_ref uses atomic operations -// for refcount increments, and lean_dec_ref delegates to lean_dec_ref_cold -// which also handles MT objects atomically. This makes Clone (inc_ref) and -// Drop (dec_ref) thread-safe. +// multi-threaded mode (m_rc negated). After marking: +// - lean_inc_ref: atomic_fetch_sub(m_rc, 1) — makes count more negative +// - lean_dec_ref_cold: atomic_fetch_add(m_rc, 1) — frees when previous == -1 +// This makes Clone (inc_ref) and Drop (dec_ref) thread-safe. unsafe impl Send for LeanShared {} unsafe impl Sync for LeanShared {} From 0a0497a57940922eadb8dca475eeb9a458e65d26 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 20 Mar 2026 12:22:26 -0400 Subject: [PATCH 10/10] Clippy --- src/object.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/object.rs b/src/object.rs index 34da301..921616c 100644 --- a/src/object.rs +++ b/src/object.rs @@ -1192,7 +1192,10 @@ impl> FromIterator for LeanList { } } -impl<'a> LeanList> { +impl<'a> IntoIterator for LeanList> { + type Item = LeanBorrowed<'a>; + type IntoIter = LeanListIter<'a>; + /// Iterate elements with the original borrow lifetime `'a`. /// /// Unlike [`iter()`](LeanList::iter) (which ties the output lifetime to @@ -1200,10 +1203,12 @@ impl<'a> LeanList> { /// Use this when the list is a local `Copy` value and the elements need to /// outlive the list binding. #[inline] - pub fn into_iter(self) -> LeanListIter<'a> { + fn into_iter(self) -> LeanListIter<'a> { LeanListIter(self.0) } +} +impl<'a> LeanList> { /// Collect elements into a `Vec` with the original borrow lifetime. pub fn to_vec(self) -> Vec> { self.into_iter().collect()