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/.gitignore b/.gitignore index 5de600b..c2f0e98 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,8 @@ # Rust -/target +target + +# Lean +.lake # Nix result 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/README.md b/README.md index b363b1b..69482cd 100644 --- a/README.md +++ b/README.md @@ -1,52 +1,113 @@ # 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 `@&`. + +- **`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`. + +- **`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 -### Inductive 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 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 +120,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/Tests.lean b/Tests.lean new file mode 100644 index 0000000..16a9dad --- /dev/null +++ b/Tests.lean @@ -0,0 +1 @@ +import Tests.FFI diff --git a/Tests/FFI.lean b/Tests/FFI.lean new file mode 100644 index 0000000..7a9e12d --- /dev/null +++ b/Tests/FFI.lean @@ -0,0 +1,684 @@ +/- + FFI roundtrip tests for lean-ffi. + Pattern: Lean value → Rust (decode via lean-ffi) → Rust (re-encode) → Lean value → compare +-/ +module + +public import LSpec +public import Tests.Gen + +open LSpec SlimCheck Gen + +namespace Tests.FFI + +/-! ## FFI declarations — borrowed (@&) parameters -/ + +@[extern "rs_roundtrip_nat"] +opaque roundtripNat : @& Nat → Nat + +@[extern "rs_roundtrip_string"] +opaque roundtripString : @& String → String + +@[extern "rs_roundtrip_bool"] +opaque roundtripBool : @& Bool → Bool + +@[extern "rs_roundtrip_list_nat"] +opaque roundtripListNat : @& List Nat → List Nat + +@[extern "rs_roundtrip_array_nat"] +opaque roundtripArrayNat : @& Array Nat → Array Nat + +@[extern "rs_roundtrip_bytearray"] +opaque roundtripByteArray : @& ByteArray → ByteArray + +@[extern "rs_roundtrip_option_nat"] +opaque roundtripOptionNat : @& Option Nat → Option Nat + +@[extern "rs_roundtrip_point"] +opaque roundtripPoint : @& Point → Point + +@[extern "rs_roundtrip_nat_tree"] +opaque roundtripNatTree : @& NatTree → NatTree + +@[extern "rs_roundtrip_prod_nat_nat"] +opaque roundtripProdNatNat : @& Nat × Nat → Nat × Nat + +@[extern "rs_roundtrip_except_string_nat"] +opaque roundtripExceptStringNat : @& Except String Nat → Except String Nat + +@[extern "rs_except_error_string"] +opaque exceptErrorString : @& String → Except String Nat + +@[extern "rs_io_result_ok_nat"] +opaque ioResultOkNat : @& Nat → EStateM.Result IO.Error PUnit Nat + +@[extern "rs_io_result_error_string"] +opaque ioResultErrorString : @& String → EStateM.Result IO.Error PUnit Nat + +@[extern "rs_roundtrip_scalar_struct"] +opaque roundtripScalarStruct : @& ScalarStruct → ScalarStruct + +@[extern "rs_roundtrip_ext_scalar_struct"] +opaque roundtripExtScalarStruct : @& ExtScalarStruct → ExtScalarStruct + +@[extern "rs_roundtrip_usize_struct"] +opaque roundtripUSizeStruct : @& USizeStruct → USizeStruct + +@[extern "rs_roundtrip_float"] +opaque roundtripFloat : Float → Float + +@[extern "rs_roundtrip_float32"] +opaque roundtripFloat32 : Float32 → Float32 + +@[extern "rs_roundtrip_array_float"] +opaque roundtripArrayFloat : @& Array Float → Array Float + +@[extern "rs_roundtrip_array_float32"] +opaque roundtripArrayFloat32 : @& Array Float32 → Array Float32 + +@[extern "rs_roundtrip_usize"] +opaque roundtripUSize : USize → USize + +@[extern "rs_roundtrip_string_from_bytes"] +opaque roundtripStringFromBytes : @& String → String + +@[extern "rs_roundtrip_array_push"] +opaque roundtripArrayPush : @& Array Nat → Array Nat + +@[extern "rs_roundtrip_uint32"] +opaque roundtripUInt32 : UInt32 → UInt32 + +@[extern "rs_roundtrip_uint64"] +opaque roundtripUInt64 : UInt64 → UInt64 + +@[extern "rs_roundtrip_array_uint32"] +opaque roundtripArrayUInt32 : @& Array UInt32 → Array UInt32 + +@[extern "rs_roundtrip_array_uint64"] +opaque roundtripArrayUInt64 : @& Array UInt64 → Array UInt64 + +/-- Opaque type representing Rust-owned data behind a Lean external object -/ +opaque RustDataPointed : NonemptyType +def RustData : Type := RustDataPointed.type +instance : Nonempty RustData := RustDataPointed.property + +@[extern "rs_external_create"] +opaque mkRustData : UInt64 → UInt64 → @& String → RustData + +@[extern "rs_external_get_x"] +opaque rustDataGetX : @& RustData → UInt64 + +@[extern "rs_external_get_y"] +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 + +/-! ## 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. + +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 := + test "Nat 0" (roundtripNat 0 == 0) ++ + test "Nat 42" (roundtripNat 42 == 42) ++ + test "Nat 1000" (roundtripNat 1000 == 1000) ++ + test "String empty" (roundtripString "" == "") ++ + test "String hello" (roundtripString "hello" == "hello") ++ + test "Bool true" (roundtripBool true == true) ++ + test "Bool false" (roundtripBool false == false) ++ + test "List []" (roundtripListNat [] == []) ++ + test "List [1,2,3]" (roundtripListNat [1, 2, 3] == [1, 2, 3]) ++ + test "Array #[]" (roundtripArrayNat #[] == #[]) ++ + test "Array #[1,2,3]" (roundtripArrayNat #[1, 2, 3] == #[1, 2, 3]) ++ + test "ByteArray empty" (roundtripByteArray ⟨#[]⟩ == ⟨#[]⟩) ++ + test "ByteArray [1,2,3]" (roundtripByteArray ⟨#[1, 2, 3]⟩ == ⟨#[1, 2, 3]⟩) ++ + test "Option none" (roundtripOptionNat none == none) ++ + test "Option some 42" (roundtripOptionNat (some 42) == some 42) ++ + test "Point (0, 0)" (roundtripPoint ⟨0, 0⟩ == ⟨0, 0⟩) ++ + test "Point (42, 99)" (roundtripPoint ⟨42, 99⟩ == ⟨42, 99⟩) ++ + test "NatTree leaf" (roundtripNatTree (.leaf 42) == .leaf 42) ++ + test "NatTree node" (roundtripNatTree (.node (.leaf 1) (.leaf 2)) == .node (.leaf 1) (.leaf 2)) ++ + test "Prod (1, 2)" (roundtripProdNatNat (1, 2) == (1, 2)) ++ + test "Prod (0, 0)" (roundtripProdNatNat (0, 0) == (0, 0)) ++ + test "UInt32 0" (roundtripUInt32 0 == 0) ++ + test "UInt32 42" (roundtripUInt32 42 == 42) ++ + test "UInt32 max" (roundtripUInt32 0xFFFFFFFF == 0xFFFFFFFF) ++ + test "UInt64 0" (roundtripUInt64 0 == 0) ++ + test "UInt64 42" (roundtripUInt64 42 == 42) ++ + test "UInt64 max" (roundtripUInt64 0xFFFFFFFFFFFFFFFF == 0xFFFFFFFFFFFFFFFF) ++ + test "Array UInt32 empty" (roundtripArrayUInt32 #[] == #[]) ++ + test "Array UInt32 [1,2,3]" (roundtripArrayUInt32 #[1, 2, 3] == #[1, 2, 3]) ++ + test "Array UInt32 [0, max]" (roundtripArrayUInt32 #[0, 0xFFFFFFFF] == #[0, 0xFFFFFFFF]) ++ + test "Array UInt64 empty" (roundtripArrayUInt64 #[] == #[]) ++ + test "Array UInt64 [1,2,3]" (roundtripArrayUInt64 #[1, 2, 3] == #[1, 2, 3]) ++ + test "Array UInt64 [0, max]" (roundtripArrayUInt64 #[0, 0xFFFFFFFFFFFFFFFF] == #[0, 0xFFFFFFFFFFFFFFFF]) ++ + test "Float 0.0" (roundtripFloat 0.0 == 0.0) ++ + test "Float 3.14" (roundtripFloat 3.14 == 3.14) ++ + test "Float -1.5" (roundtripFloat (-1.5) == -1.5) ++ + test "Float32 0.0" (roundtripFloat32 0.0 == 0.0) ++ + test "Float32 3.14" (roundtripFloat32 3.14 == 3.14) ++ + test "USize 0" (roundtripUSize 0 == 0) ++ + test "USize 42" (roundtripUSize 42 == 42) ++ + test "Array Float [1.5, 2.5]" (roundtripArrayFloat #[1.5, 2.5] == #[1.5, 2.5]) ++ + test "Array Float32 [1.5, 2.5]" (roundtripArrayFloat32 #[1.5, 2.5] == #[1.5, 2.5]) ++ + test "String from_bytes empty" (roundtripStringFromBytes "" == "") ++ + test "String from_bytes hello" (roundtripStringFromBytes "hello" == "hello") ++ + test "Array push empty" (roundtripArrayPush #[] == #[]) ++ + test "Array push [1,2,3]" (roundtripArrayPush #[1, 2, 3] == #[1, 2, 3]) + +/-! ## Except tests -/ + +def exceptTests : TestSeq := + test "Except.ok 42" (show Bool from + match roundtripExceptStringNat (.ok 42) with + | .ok n => n == 42 + | .error _ => false) ++ + test "Except.error hello" (show Bool from + match roundtripExceptStringNat (.error "hello") with + | .error s => s == "hello" + | .ok _ => false) ++ + test "Except.error_string" (show Bool from + match exceptErrorString "boom" with + | .error s => s == "boom" + | .ok _ => false) + +/-! ## IO result tests -/ + +def ioResultTests : TestSeq := + test "IOResult ok 42" (show Bool from + match ioResultOkNat 42 with + | .ok val _ => val == 42 + | .error _ _ => false) ++ + test "IOResult error" (show Bool from + match ioResultErrorString "oops" with + | .error _ _ => true + | .ok _ _ => false) + +/-! ## Scalar struct tests -/ + +def scalarStructTests : TestSeq := + test "ScalarStruct (0, 0, 0, 0)" (roundtripScalarStruct ⟨0, 0, 0, 0⟩ == ⟨0, 0, 0, 0⟩) ++ + test "ScalarStruct (42, 255, 1000, 9999)" (roundtripScalarStruct ⟨42, 255, 1000, 9999⟩ == ⟨42, 255, 1000, 9999⟩) ++ + test "ScalarStruct max vals" (roundtripScalarStruct ⟨100, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩ == ⟨100, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩) + +/-! ## Extended scalar struct tests -/ + +def extScalarStructTests : TestSeq := + test "ExtScalarStruct zeros" (show Bool from roundtripExtScalarStruct ⟨0, 0, 0, 0, 0, 0.0, 0.0⟩ == ⟨0, 0, 0, 0, 0, 0.0, 0.0⟩) ++ + test "ExtScalarStruct mixed" (show Bool from roundtripExtScalarStruct ⟨42, 255, 1000, 50000, 9999, 3.14, 2.5⟩ == ⟨42, 255, 1000, 50000, 9999, 3.14, 2.5⟩) ++ + test "ExtScalarStruct max ints" (show Bool from roundtripExtScalarStruct ⟨100, 0xFF, 0xFFFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF, 1.0, 1.0⟩ == ⟨100, 0xFF, 0xFFFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF, 1.0, 1.0⟩) + +/-! ## USize struct tests -/ + +def usizeStructTests : TestSeq := + test "USizeStruct zeros" (roundtripUSizeStruct ⟨0, 0, 0⟩ == ⟨0, 0, 0⟩) ++ + test "USizeStruct mixed" (roundtripUSizeStruct ⟨42, 99, 255⟩ == ⟨42, 99, 255⟩) + +/-! ## External object tests -/ + +def externalTests : TestSeq := + test "External create and get x" (rustDataGetX (mkRustData 42 99 "hello") == 42) ++ + test "External create and get y" (rustDataGetY (mkRustData 42 99 "hello") == 99) ++ + 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 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 -/ + +def largeNatTests : TestSeq := + let testCases : List Nat := [0, 1, 255, 256, 65535, 65536, (2^32 - 1), 2^32, + (2^63 - 1), 2^63, (2^64 - 1), 2^64, 2^64 + 1, 2^128, 2^256] + testCases.foldl (init := .done) fun acc n => + acc ++ .individualIO s!"Nat {n}" none (do + 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 -/ + +/-! ## 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)), +] + +/-! ## 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/test/Tests/Gen.lean b/Tests/Gen.lean similarity index 84% rename from test/Tests/Gen.lean rename to Tests/Gen.lean index 193578b..5e8264f 100644 --- a/test/Tests/Gen.lean +++ b/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/Tests/Main.lean b/Tests/Main.lean new file mode 100644 index 0000000..027e650 --- /dev/null +++ b/Tests/Main.lean @@ -0,0 +1,12 @@ +import Tests.FFI +import Std.Data.HashMap + +def main (args : List String) : IO UInt32 := do + let suites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ + ("borrowed", Tests.FFI.borrowedSuite), + ("owned", Tests.FFI.ownedSuite), + ("persistent", Tests.FFI.persistentSuite), + ("property", Tests.FFI.propertySuite), + ("shared", Tests.FFI.sharedSuite), + ] + LSpec.lspecIO suites args diff --git a/flake.nix b/flake.nix index 6b4ecfc..9299d5d 100644 --- a/flake.nix +++ b/flake.nix @@ -68,37 +68,23 @@ 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/ - ''; - }); + 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 { @@ -122,6 +108,7 @@ packages = with pkgs; [ clang rustToolchain + rust-analyzer lean.lean-all # Includes Lean compiler, lake, stdlib, etc. ]; }; 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..16e49c2 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,27 @@ +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 -/ +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" + let releaseDir := pkg.dir / "target" / "release" + proc { cmd := "cp", args := #["-f", srcName, dstName], cwd := releaseDir } + inputBinFile $ releaseDir / dstName + +end FFI + +lean_lib Tests + +@[test_driver] +lean_exe LeanFFITests where + root := `Tests.Main diff --git a/src/lib.rs b/src/lib.rs index b5c8074..3586a9d 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`. @@ -23,6 +23,11 @@ pub mod include { pub mod nat; pub mod object; +pub use object::LeanShared; + +#[cfg(feature = "test-ffi")] +mod test_ffi; + use std::ffi::{CString, c_void}; /// Create a CString from a str, stripping any interior null bytes. @@ -42,30 +47,74 @@ 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(pub R); - impl std::ops::Deref for $name { - type Target = $crate::object::LeanObject; + impl Clone for $name { #[inline] - fn deref(&self) -> &$crate::object::LeanObject { &self.0 } + fn clone(&self) -> Self { Self(self.0.clone()) } } - impl From<$name> for $crate::object::LeanObject { + impl Copy for $name {} + + impl $name { + /// Get the inner reference. + #[inline] + 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 $name<$crate::object::LeanOwned> { + /// Wrap an owned `LeanOwned` value. + #[inline] + pub fn new(obj: $crate::object::LeanOwned) -> Self { Self(obj) } + + /// Consume without calling `lean_dec`. #[inline] - fn from(x: $name) -> Self { x.0 } + 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 + } } - 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(); + // 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/nat.rs b/src/nat.rs index 07d4da3..61fa619 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,14 @@ 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())) + Nat(BigUint::from(obj.unbox_usize() as u64)) } 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,25 +58,19 @@ 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)); - } - // 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)); + return LeanNat::new(LeanOwned::from_nat_u64(val)); } + // 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()) }) } } @@ -149,20 +142,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 +166,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..921616c 100644 --- a/src/object.rs +++ b/src/object.rs @@ -1,792 +1,1070 @@ -//! 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; + +/// 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; // ============================================================================= -// 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); - -impl LeanObject { - /// Wrap a raw pointer without any tag check. - /// - /// # Safety - /// The pointer must be a valid Lean object (or tagged scalar). +// +// 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). +/// +/// 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; + + /// 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. +// ============================================================================= +// 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 box_usize(n: usize) -> Self { - Self(((n << 1) | 1) as *const c_void) + fn drop(&mut self) { + if self.0 as usize & 1 != 1 { + unsafe { include::lean_dec_ref(self.0) }; + } } +} - /// Unbox a tagged scalar pointer into a `usize`. +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 unbox_usize(self) -> usize { - self.0 as usize >> 1 + 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 box_u64(n: u64) -> Self { - Self(unsafe { include::lean_box_uint64(n) }.cast()) + fn as_raw(&self) -> *mut include::lean_object { + self.0 } +} +impl LeanOwned { + /// Borrow this owned reference. The returned `LeanBorrowed` is + /// lifetime-bounded to `&self`. No refcount change. #[inline] - pub fn unbox_u64(self) -> u64 { - unsafe { include::lean_unbox_uint64(self.0 as *mut _) } + pub fn borrow(&self) -> LeanBorrowed<'_> { + unsafe { LeanBorrowed::from_raw(self.0) } } - /// Box a `f64` into a Lean `Float` object via `lean_box_float`. + /// 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; + // Suppress Drop (lean_dec) — ownership transfers to the caller + 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) } } // ============================================================================= // 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`). -#[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 { + fn clone(&self) -> Self { + Self(self.0.clone()) + } +} + +impl Copy for LeanNat {} + +impl LeanNat { + #[inline] + pub fn inner(&self) -> &R { &self.0 } + #[inline] + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } } -impl From for LeanObject { +impl LeanNat { + /// Wrap an owned `LeanOwned` as a `LeanNat`. + #[inline] + pub fn new(obj: LeanOwned) -> Self { + Self(obj) + } + + /// Consume without calling `lean_dec`. #[inline] - fn from(x: LeanNat) -> Self { - x.0 + 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 } } -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(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned + std::mem::forget(x); + LeanOwned(ptr) + } +} + // ============================================================================= // 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). -#[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] - fn from(x: LeanBool) -> Self { - x.0 + pub fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() + } + + /// Decode to a Rust `bool`. + #[inline] + 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(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned + std::mem::forget(x); + LeanOwned(ptr) } } // ============================================================================= // 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`). -#[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()) - } - - pub fn set(&self, i: usize, val: impl Into) { - let val: LeanObject = val.into(); - unsafe { - include::lean_array_set_core(self.0.as_ptr() as *mut _, i, val.as_ptr() as *mut _); - } + /// 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, + ) } - /// Return a slice over the array elements. - pub fn data(&self) -> &[LeanObject] { + /// Return a slice over the array elements as borrowed references. + pub fn data(&self) -> &[LeanBorrowed<'_>] { 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. + 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()) } } - pub fn iter(&self) -> impl Iterator + '_ { + pub fn iter(&self) -> impl Iterator> + '_ { self.data().iter().copied() } - pub fn map(&self, f: impl Fn(LeanObject) -> T) -> Vec { + 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 { + 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). + pub fn alloc(size: usize) -> Self { + let obj = unsafe { include::lean_alloc_array(size, size) }; + Self(LeanOwned(obj)) + } + + /// 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(); + // Suppress Drop (lean_dec) — ownership transfers to the caller + std::mem::forget(self); + ptr + } +} + +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) } } // ============================================================================= // 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`). -#[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 { + fn clone(&self) -> Self { + Self(self.0.clone()) + } +} + +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` (tag `LEAN_TAG_SCALAR_ARRAY`). +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 { + 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). 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(); } } + + /// Consume without calling `lean_dec`. + #[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 + } +} + +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) + } } // ============================================================================= // 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`). -#[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 Copy for LeanString {} -impl Deref for LeanString { - type Target = LeanObject; +impl LeanString { #[inline] - fn deref(&self) -> &LeanObject { + pub fn inner(&self) -> &R { &self.0 } + #[inline] + 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 { + 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`. 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(); + // Suppress Drop (lean_dec) — ownership transfers to the caller + 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(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned + std::mem::forget(x); + LeanOwned(ptr) } } // ============================================================================= // 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`). -#[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 { + #[inline] + fn scalar_offset(num_objs: usize, offset: usize) -> u32 { + (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_ptr() as *mut _, (num_objs * 8 + offset) as u32) + include::lean_ctor_get_uint8(self.0.as_raw(), Self::scalar_offset(num_objs, offset)) } } - - /// 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 { + pub fn get_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) + include::lean_ctor_get_uint16(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 { + pub fn get_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) + include::lean_ctor_get_uint32(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 { + pub fn get_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) + include::lean_ctor_get_uint64(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 { + pub fn get_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) + include::lean_ctor_get_float(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 { + pub fn get_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, - ) + 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 get_usize(&self, num_objs: usize, slot: usize) -> usize { + unsafe { include::lean_ctor_get_usize(self.0.as_raw(), (num_objs + slot) as u32) } + } + pub fn get_bool(&self, num_objs: usize, offset: usize) -> bool { + self.get_u8(num_objs, offset) != 0 + } +} - /// Read a `usize` scalar at slot `slot` past `num_objs` object fields. +impl LeanCtor { + /// Wrap a raw pointer, asserting it is a constructor. /// - /// Note: `lean_ctor_get_usize` uses a **slot index** (not byte offset). - /// The slot is `num_objs + slot` where each slot is pointer-sized. - #[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) } + /// # Safety + /// The pointer must be a valid Lean constructor object. + pub unsafe fn from_raw(ptr: *mut include::lean_object) -> Self { + test_assert!(ptr as usize & 1 != 1); + test_assert!(unsafe { include::lean_obj_tag(ptr) } <= u32::from(LEAN_MAX_CTOR_TAG)); + Self(LeanOwned(ptr)) } - /// 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 + /// 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)) } - // --------------------------------------------------------------------------- - // Symmetric scalar setters — take (num_objs, offset, val) like the readers - // --------------------------------------------------------------------------- + /// 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(self.0.as_raw(), i as u32, val.into_raw()); + } + } - /// 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) { + /// Consume without calling `lean_dec`. + #[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 + } + + // ------------------------------------------------------------------------- + // Scalar field setters (owned only — mutation) + // ------------------------------------------------------------------------- + + pub fn set_u8(&self, num_objs: usize, offset: usize, val: u8) { unsafe { include::lean_ctor_set_uint8( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), val, ); } } - - /// 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) { + pub fn set_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, + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), val, ); } } - - /// 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) { + pub fn set_u32(&self, num_objs: usize, offset: usize, val: u32) { unsafe { include::lean_ctor_set_uint32( - self.0.as_ptr() as *mut _, - (num_objs * 8 + offset) as u32, + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), val, ); } } - - /// 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) { + pub fn set_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, + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), val, ); } } - - /// 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) { + pub fn set_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, + self.0.as_raw(), + Self::scalar_offset(num_objs, offset), val, ); } } - - /// 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) { + pub fn set_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, + 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). + /// 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) { + pub fn set_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); + 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(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned + std::mem::forget(x); + LeanOwned(ptr) } } // ============================================================================= // 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`. -#[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 LeanExternal { - /// Wrap a raw pointer, asserting it is an external object (tag `LEAN_TAG_EXTERNAL`). +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. /// /// # 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 { + 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`. 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(); + // Suppress Drop (lean_dec) — ownership transfers to the caller + 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 { + 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) + } +} + +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) } } @@ -795,7 +1073,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 +1089,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::()) }); } @@ -829,60 +1107,83 @@ 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). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanList(LeanObject); +pub struct LeanList(R); + +impl Clone for LeanList { + #[inline] + fn clone(&self) -> Self { + Self(self.0.clone()) + } +} + +impl Copy for LeanList {} -impl Deref for LeanList { - type Target = LeanObject; +impl LeanList { #[inline] - fn deref(&self) -> &LeanObject { + 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` (scalar nil or ctor tag 1). +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 { + test_assert!(ptr as usize & 1 == 1 || unsafe { include::lean_obj_tag(ptr) } == 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() + Self(LeanOwned(ctor.into_raw())) } - pub fn iter(&self) -> LeanListIter { - LeanListIter(self.0) - } - - 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(); + // Suppress Drop (lean_dec) — ownership transfers to the caller + 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); @@ -891,58 +1192,89 @@ impl> FromIterator for 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 + /// `&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] + 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() + } +} + /// 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(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned + std::mem::forget(x); + LeanOwned(ptr) } } // ============================================================================= // 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). -#[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)) +impl LeanOption { + #[inline] + pub fn inner(&self) -> &R { + &self.0 } - - pub fn some(val: impl Into) -> Self { - let ctor = LeanCtor::alloc(1, 1, 0); - ctor.set(0, val); - Self(ctor.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,56 +1285,135 @@ 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)) + 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 { + test_assert!(ptr as usize & 1 == 1 || unsafe { include::lean_obj_tag(ptr) } == 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(); + // Suppress Drop (lean_dec) — ownership transfers to the caller + std::mem::forget(self); + ptr + } +} + +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) + } +} + // ============================================================================= // 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). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanExcept(LeanObject); +pub struct LeanExcept(R); + +impl Clone for LeanExcept { + #[inline] + fn clone(&self) -> Self { + Self(self.0.clone()) + } +} + +impl Copy for LeanExcept {} -impl Deref for LeanExcept { - type Target = LeanObject; +impl LeanExcept { #[inline] - fn deref(&self) -> &LeanObject { + 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 { +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 { + 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`. - 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,197 +1421,343 @@ 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(); + // Suppress Drop (lean_dec) — ownership transfers to the caller + 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(); + // Suppress Drop (lean_dec) — ownership transfers to the returned LeanOwned + std::mem::forget(x); + LeanOwned(ptr) } } // ============================================================================= // 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). -#[derive(Clone, Copy)] #[repr(transparent)] -pub struct LeanIOResult(LeanObject); +pub struct LeanIOResult(R); + +impl Clone for LeanIOResult { + #[inline] + fn clone(&self) -> Self { + Self(self.0.clone()) + } +} + +impl Copy for LeanIOResult {} -impl Deref for LeanIOResult { - type Target = LeanObject; +impl LeanIOResult { #[inline] - fn deref(&self) -> &LeanObject { + 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 { +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(); + // Suppress Drop (lean_dec) — ownership transfers to the caller + std::mem::forget(self); + ptr + } +} + +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) } } // ============================================================================= // 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). -#[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) + Self(LeanOwned(ctor.into_raw())) } - /// Get the first element. - pub fn fst(&self) -> LeanObject { - let ctor = self.0.as_ctor(); - ctor.get(0) + /// Consume without calling `lean_dec`. + #[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 } +} - /// Get the second element. - pub fn snd(&self) -> LeanObject { - let ctor = self.0.as_ctor(); - ctor.get(1) +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) } } // ============================================================================= -// From for LeanObject — allow wrapper types to be passed to set() etc. +// From for LeanOwned // ============================================================================= -impl From for LeanObject { +impl From for LeanOwned { #[inline] - fn from(x: LeanArray) -> Self { - x.0 + fn from(x: u32) -> Self { + Self::box_u32(x) } } -impl From for LeanObject { +impl From for LeanOwned { #[inline] - fn from(x: LeanByteArray) -> Self { - x.0 + fn from(x: f64) -> Self { + Self::box_f64(x) } } -impl From for LeanObject { +impl From for LeanOwned { #[inline] - fn from(x: LeanString) -> Self { - x.0 + fn from(x: f32) -> Self { + Self::box_f32(x) } } -impl From for LeanObject { +// ============================================================================= +// Convenience: as_ctor / as_string / as_array / as_list / as_byte_array +// ============================================================================= + +/// 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: LeanCtor) -> Self { - x.0 + pub fn as_ctor(self) -> LeanCtor> { + test_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: LeanExternal) -> Self { - x.0 + pub fn as_string(self) -> LeanString> { + test_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_STRING); + LeanString(self) } -} -impl From for LeanObject { + /// Interpret as an `Array` object. #[inline] - fn from(x: LeanList) -> Self { - x.0 + pub fn as_array(self) -> LeanArray> { + test_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_ARRAY); + LeanArray(self) } -} -impl From for LeanObject { + /// Interpret as a `List`. #[inline] - fn from(x: LeanOption) -> Self { - x.0 + pub fn as_list(self) -> LeanList> { + test_assert!(self.is_scalar() || self.tag() == 1); + LeanList(self) } -} -impl From for LeanObject { + /// Interpret as a `ByteArray` object. #[inline] - fn from(x: LeanExcept) -> Self { - x.0 + pub fn as_byte_array(self) -> LeanByteArray> { + test_assert!(!self.is_scalar() && self.tag() == LEAN_TAG_SCALAR_ARRAY); + LeanByteArray(self) } } -impl From for LeanObject { +// ============================================================================= +// LeanShared — Thread-safe owned Lean object +// ============================================================================= + +/// Thread-safe owned Lean object with atomic refcounting. +/// +/// 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`. +/// +/// 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 (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 {} + +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] - fn from(x: LeanIOResult) -> Self { - x.0 + pub fn new(owned: LeanOwned) -> Self { + if !owned.is_scalar() && !owned.is_persistent() { + unsafe { + include::lean_mark_mt(owned.as_raw()); + } + } + Self(owned) } -} -impl From for LeanObject { + /// Borrow this object. The returned reference is lifetime-bounded + /// to `&self` and is **not** `Send`. #[inline] - fn from(x: u32) -> Self { - Self::box_u32(x) + 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(); + // Suppress Drop (lean_dec) — ownership transfers to the caller + std::mem::forget(self); + unsafe { LeanOwned::from_raw(ptr) } } } -impl From for LeanObject { +impl Clone for LeanShared { #[inline] - fn from(x: f64) -> Self { - Self::box_f64(x) + fn clone(&self) -> Self { + // lean_inc_ref uses atomic ops for MT objects (m_rc < 0). + Self(self.0.clone()) } } -impl From for LeanObject { +// 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 from(x: f32) -> Self { - Self::box_f32(x) + fn as_raw(&self) -> *mut include::lean_object { + self.0.as_raw() } } diff --git a/src/test_ffi.rs b/src/test_ffi.rs new file mode 100644 index 0000000..664fa95 --- /dev/null +++ b/src/test_ffi.rs @@ -0,0 +1,1367 @@ +//! FFI roundtrip functions for testing lean-ffi. +//! +//! 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 crate::nat::Nat; +use crate::object::{ + ExternalClass, LeanArray, LeanBool, LeanBorrowed, LeanByteArray, LeanCtor, LeanExcept, + LeanExternal, LeanIOResult, LeanList, LeanNat, LeanOption, LeanOwned, LeanProd, LeanRef, + LeanString, +}; + +// ============================================================================= +// Domain types for Lean structures +// ============================================================================= + +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 + 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) -> LeanOwned { + n.to_lean().into() +} + +// ============================================================================= +// Roundtrip FFI functions +// ============================================================================= + +/// Round-trip a Nat: decode from Lean, re-encode to Lean. +#[unsafe(no_mangle)] +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(crate) 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(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)) + } else { + LeanBool::new(LeanOwned::from_enum_tag(0)) + } +} + +/// Round-trip a List Nat: decode from Lean, re-encode to Lean. +#[unsafe(no_mangle)] +pub(crate) 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(crate) 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)); + } + arr +} + +/// Round-trip a ByteArray: decode from Lean, re-encode to Lean. +#[unsafe(no_mangle)] +pub(crate) 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(crate) extern "C" fn rs_roundtrip_option_nat( + opt: LeanOption>, +) -> LeanOption { + if opt.inner().is_scalar() { + LeanOption::none() + } else { + 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(crate) 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(crate) 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) -> LeanOwned { + match ctor.tag() { + 0 => { + // leaf : Nat → NatTree + let nat = Nat::from_obj(&ctor.get(0)); + let leaf = LeanCtor::alloc(0, 1, 0); + leaf.set(0, build_nat(&nat)); + 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 node = LeanCtor::alloc(1, 2, 0); + node.set(0, left); + node.set(1, right); + node.into() + } + _ => panic!("Invalid NatTree tag: {}", ctor.tag()), + } +} + +// ============================================================================= +// LeanProd roundtrip +// ============================================================================= + +/// Round-trip a Prod Nat Nat: decode fst/snd, re-encode via LeanProd::new. +#[unsafe(no_mangle)] +pub(crate) 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)) +} + +// ============================================================================= +// LeanExcept roundtrip +// ============================================================================= + +/// Round-trip an Except String Nat: decode ok/error, re-encode. +#[unsafe(no_mangle)] +pub(crate) 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())) + } + Ok(val) => { + let nat = Nat::from_obj(&val); + LeanExcept::ok(build_nat(&nat)) + } + } +} + +/// Build an Except.error from a Rust string (tests LeanExcept::error_string). +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_except_error_string( + s: LeanString>, +) -> LeanExcept { + LeanExcept::error_string(&s.to_string()) +} + +// ============================================================================= +// LeanIOResult roundtrip +// ============================================================================= + +/// Build a successful IO result wrapping a Nat (tests LeanIOResult::ok). +#[unsafe(no_mangle)] +pub(crate) 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(crate) extern "C" fn rs_io_result_error_string( + s: LeanString>, +) -> LeanIOResult { + LeanIOResult::error_string(&s.to_string()) +} + +// ============================================================================= +// LeanCtor scalar fields +// ============================================================================= + +/// 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(crate) 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 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()) +} + +// ============================================================================= +// box_u32 / box_u64 roundtrip +// ============================================================================= + +/// Round-trip a UInt32 (passed as raw uint32_t by Lean FFI). +#[unsafe(no_mangle)] +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(crate) extern "C" fn rs_roundtrip_uint64(val: u64) -> u64 { + val +} + +/// Round-trip an Array UInt32. +#[unsafe(no_mangle)] +pub(crate) 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, LeanOwned::box_u32(val)); + } + new_arr +} + +/// Round-trip an Array UInt64. +#[unsafe(no_mangle)] +pub(crate) 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, LeanOwned::box_u64(val)); + } + new_arr +} + +// ============================================================================= +// LeanExternal roundtrip +// ============================================================================= + +/// A simple Rust struct to store in a Lean external object. +#[derive(Debug, Clone, PartialEq)] +struct RustData { + x: u64, + y: u64, + label: String, +} + +static RUST_DATA_CLASS: LazyLock = + LazyLock::new(ExternalClass::register_with_drop::); + +/// Create a LeanExternal from three Lean values. +/// Note: label is @& (borrowed), x/y are scalar UInt64. +#[unsafe(no_mangle)] +pub(crate) 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); + LeanRustData::new(ext.into()) +} + +/// Read the x field from a LeanExternal (@& borrowed). +#[unsafe(no_mangle)] +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 +} + +/// Read the y field from a LeanExternal (@& borrowed). +#[unsafe(no_mangle)] +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 +} + +/// Read the label field from a LeanExternal (@& borrowed). +#[unsafe(no_mangle)] +pub(crate) 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) +} + +// ============================================================================= +// Extended scalar struct roundtrip (u8, u16, u32, u64, f64, f32) +// ============================================================================= + +/// 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(crate) 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. +/// 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(crate) 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 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()) +} + +// ============================================================================= +// Float / Float32 / USize scalar roundtrips +// ============================================================================= + +/// Round-trip a Float (f64) — passed as raw scalar across FFI. +#[unsafe(no_mangle)] +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(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(crate) extern "C" fn rs_roundtrip_usize(val: usize) -> usize { + val +} + +/// Round-trip an Array Float. +#[unsafe(no_mangle)] +pub(crate) 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, LeanOwned::box_f64(val)); + } + new_arr +} + +/// Round-trip an Array Float32. +#[unsafe(no_mangle)] +pub(crate) 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, LeanOwned::box_f32(val)); + } + new_arr +} + +// ============================================================================= +// LeanString::from_bytes roundtrip +// ============================================================================= + +/// Round-trip a String using LeanString::from_bytes instead of LeanString::new. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_roundtrip_string_from_bytes( + s_ptr: LeanString>, +) -> LeanString { + let s = s_ptr.to_string(); + LeanString::from_bytes(s.as_bytes()) +} + +// ============================================================================= +// LeanArray::push roundtrip +// ============================================================================= + +/// Round-trip an Array Nat by pushing each element into a new array. +#[unsafe(no_mangle)] +pub(crate) 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(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) +} + +/// Round-trip a String with owned arg. Tests LeanOwned Drop on strings. +#[unsafe(no_mangle)] +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 +} + +/// Round-trip an Array Nat with owned arg. Tests LeanOwned Drop on arrays. +#[unsafe(no_mangle)] +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)); + 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(crate) 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(crate) 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(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}")) +} + +/// Three owned args: merge three lists into one. +/// Tests Drop on multiple owned args with complex ownership flow. +#[unsafe(no_mangle)] +pub(crate) 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(crate) 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(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() + // point drops here → lean_dec +} + +/// Owned Except: if ok, double the nat; if error, return error string length. +#[unsafe(no_mangle)] +pub(crate) 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(crate) 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(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() +} + +/// 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(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); + 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(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)); + let arr = LeanArray::alloc(nats.len()); + for (i, nat) in nats.iter().enumerate() { + arr.set(i, build_nat(nat)); + } + arr + }; + let cloned = owned.clone(); + + // Both owned and cloned drop here → lean_dec called twice (correct: clone did lean_inc) + owned.len() + cloned.len() +} + +/// Clone an owned string and return the sum of byte lengths of both copies. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_clone_string_len_sum(s: LeanString>) -> usize { + let owned = LeanString::new(&s.to_string()); + let cloned = owned.clone(); + + owned.byte_len() + cloned.byte_len() +} + +/// 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(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), + (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(crate) 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(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(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), + (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(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 + + 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(crate) 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(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()), + } +} + +/// Owned Prod roundtrip: decode fst/snd, rebuild. Tests Drop on Prod constructor. +#[unsafe(no_mangle)] +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)) +} + +/// Owned IOResult: extract value from ok result, return it. Tests Drop on IOResult. +#[unsafe(no_mangle)] +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 { + 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(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); + } + sum.to_lean() +} + +// ============================================================================= +// LeanOption API tests +// ============================================================================= + +/// Test LeanOption API: return the Nat inside a Some, or 0 for None. +#[unsafe(no_mangle)] +pub(crate) 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(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)) +} + +// ============================================================================= +// 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(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); + + // 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(crate) 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(crate) 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(crate) 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(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 + 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(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() { + 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(crate) 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(crate) 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(crate) extern "C" fn rs_make_empty_array(_unit: LeanBorrowed<'_>) -> LeanArray { + LeanArray::alloc(0) +} + +/// Create and return an empty list. +#[unsafe(no_mangle)] +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(crate) extern "C" fn rs_make_empty_bytearray( + _unit: LeanBorrowed<'_>, +) -> LeanByteArray { + LeanByteArray::alloc(0) +} + +/// Create and return an empty string. +#[unsafe(no_mangle)] +pub(crate) 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(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(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() +} + +// ============================================================================= +// 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(crate) 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(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(crate) 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(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() +} + +/// 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(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); + } + sum.to_lean() +} + +/// Read from a persistent string. Tests that string access works on persistent objects. +#[unsafe(no_mangle)] +pub(crate) 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(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 +} + +// ============================================================================= +// LeanShared — thread-safe multi-threaded refcounting tests +// ============================================================================= + +use crate::LeanShared; + +/// Mark an array as MT via LeanShared, clone it across N threads, +/// each thread reads all elements, then all clones are dropped. +/// Tests that lean_mark_mt + atomic refcounting works correctly. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_shared_parallel_read( + arr: LeanArray>, + 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(crate) 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(crate) 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(crate) 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(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()) }); + + // owned drops (still MT-marked, lean_dec_ref handles it) + // shared drops (atomic lean_dec) + 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(crate) 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(crate) 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() +} 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.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 879df99..0000000 --- a/test/Cargo.toml +++ /dev/null @@ -1,10 +0,0 @@ -[package] -name = "lean-ffi-rs" -version = "0.1.0" -edition = "2024" - -[lib] -crate-type = ["staticlib"] - -[dependencies] -lean-ffi = { path = ".." } diff --git a/test/Tests/FFI.lean b/test/Tests/FFI.lean deleted file mode 100644 index ac47007..0000000 --- a/test/Tests/FFI.lean +++ /dev/null @@ -1,256 +0,0 @@ -/- - FFI roundtrip tests for lean-ffi. - Pattern: Lean value → Rust (decode via lean-ffi) → Rust (re-encode) → Lean value → compare --/ -module - -public import LSpec -public import Tests.Gen - -open LSpec SlimCheck Gen - -namespace Tests.FFI - -/-! ## FFI declarations -/ - -@[extern "rs_roundtrip_nat"] -opaque roundtripNat : @& Nat → Nat - -@[extern "rs_roundtrip_string"] -opaque roundtripString : @& String → String - -@[extern "rs_roundtrip_bool"] -opaque roundtripBool : @& Bool → Bool - -@[extern "rs_roundtrip_list_nat"] -opaque roundtripListNat : @& List Nat → List Nat - -@[extern "rs_roundtrip_array_nat"] -opaque roundtripArrayNat : @& Array Nat → Array Nat - -@[extern "rs_roundtrip_bytearray"] -opaque roundtripByteArray : @& ByteArray → ByteArray - -@[extern "rs_roundtrip_option_nat"] -opaque roundtripOptionNat : @& Option Nat → Option Nat - -@[extern "rs_roundtrip_point"] -opaque roundtripPoint : @& Point → Point - -@[extern "rs_roundtrip_nat_tree"] -opaque roundtripNatTree : @& NatTree → NatTree - -@[extern "rs_roundtrip_prod_nat_nat"] -opaque roundtripProdNatNat : @& Nat × Nat → Nat × Nat - -@[extern "rs_roundtrip_except_string_nat"] -opaque roundtripExceptStringNat : @& Except String Nat → Except String Nat - -@[extern "rs_except_error_string"] -opaque exceptErrorString : @& String → Except String Nat - -@[extern "rs_io_result_ok_nat"] -opaque ioResultOkNat : @& Nat → EStateM.Result IO.Error PUnit Nat - -@[extern "rs_io_result_error_string"] -opaque ioResultErrorString : @& String → EStateM.Result IO.Error PUnit Nat - -@[extern "rs_roundtrip_scalar_struct"] -opaque roundtripScalarStruct : @& ScalarStruct → ScalarStruct - -@[extern "rs_roundtrip_ext_scalar_struct"] -opaque roundtripExtScalarStruct : @& ExtScalarStruct → ExtScalarStruct - -@[extern "rs_roundtrip_usize_struct"] -opaque roundtripUSizeStruct : @& USizeStruct → USizeStruct - -@[extern "rs_roundtrip_float"] -opaque roundtripFloat : Float → Float - -@[extern "rs_roundtrip_float32"] -opaque roundtripFloat32 : Float32 → Float32 - -@[extern "rs_roundtrip_array_float"] -opaque roundtripArrayFloat : @& Array Float → Array Float - -@[extern "rs_roundtrip_array_float32"] -opaque roundtripArrayFloat32 : @& Array Float32 → Array Float32 - -@[extern "rs_roundtrip_usize"] -opaque roundtripUSize : USize → USize - -@[extern "rs_roundtrip_string_from_bytes"] -opaque roundtripStringFromBytes : @& String → String - -@[extern "rs_roundtrip_array_push"] -opaque roundtripArrayPush : @& Array Nat → Array Nat - -@[extern "rs_roundtrip_uint32"] -opaque roundtripUInt32 : UInt32 → UInt32 - -@[extern "rs_roundtrip_uint64"] -opaque roundtripUInt64 : UInt64 → UInt64 - -@[extern "rs_roundtrip_array_uint32"] -opaque roundtripArrayUInt32 : @& Array UInt32 → Array UInt32 - -@[extern "rs_roundtrip_array_uint64"] -opaque roundtripArrayUInt64 : @& Array UInt64 → Array UInt64 - -/-- Opaque type representing Rust-owned data behind a Lean external object -/ -opaque RustDataPointed : NonemptyType -def RustData : Type := RustDataPointed.type -instance : Nonempty RustData := RustDataPointed.property - -@[extern "rs_external_create"] -opaque mkRustData : UInt64 → UInt64 → @& String → RustData - -@[extern "rs_external_get_x"] -opaque rustDataGetX : @& RustData → UInt64 - -@[extern "rs_external_get_y"] -opaque rustDataGetY : @& RustData → UInt64 - -@[extern "rs_external_get_label"] -opaque rustDataGetLabel : @& RustData → String - -/-! ## Unit tests -/ - -def simpleTests : TestSeq := - test "Nat 0" (roundtripNat 0 == 0) ++ - test "Nat 42" (roundtripNat 42 == 42) ++ - test "Nat 1000" (roundtripNat 1000 == 1000) ++ - test "String empty" (roundtripString "" == "") ++ - test "String hello" (roundtripString "hello" == "hello") ++ - test "Bool true" (roundtripBool true == true) ++ - test "Bool false" (roundtripBool false == false) ++ - test "List []" (roundtripListNat [] == []) ++ - test "List [1,2,3]" (roundtripListNat [1, 2, 3] == [1, 2, 3]) ++ - test "Array #[]" (roundtripArrayNat #[] == #[]) ++ - test "Array #[1,2,3]" (roundtripArrayNat #[1, 2, 3] == #[1, 2, 3]) ++ - test "ByteArray empty" (roundtripByteArray ⟨#[]⟩ == ⟨#[]⟩) ++ - test "ByteArray [1,2,3]" (roundtripByteArray ⟨#[1, 2, 3]⟩ == ⟨#[1, 2, 3]⟩) ++ - test "Option none" (roundtripOptionNat none == none) ++ - test "Option some 42" (roundtripOptionNat (some 42) == some 42) ++ - test "Point (0, 0)" (roundtripPoint ⟨0, 0⟩ == ⟨0, 0⟩) ++ - test "Point (42, 99)" (roundtripPoint ⟨42, 99⟩ == ⟨42, 99⟩) ++ - test "NatTree leaf" (roundtripNatTree (.leaf 42) == .leaf 42) ++ - test "NatTree node" (roundtripNatTree (.node (.leaf 1) (.leaf 2)) == .node (.leaf 1) (.leaf 2)) ++ - test "Prod (1, 2)" (roundtripProdNatNat (1, 2) == (1, 2)) ++ - test "Prod (0, 0)" (roundtripProdNatNat (0, 0) == (0, 0)) ++ - test "UInt32 0" (roundtripUInt32 0 == 0) ++ - test "UInt32 42" (roundtripUInt32 42 == 42) ++ - test "UInt32 max" (roundtripUInt32 0xFFFFFFFF == 0xFFFFFFFF) ++ - test "UInt64 0" (roundtripUInt64 0 == 0) ++ - test "UInt64 42" (roundtripUInt64 42 == 42) ++ - test "UInt64 max" (roundtripUInt64 0xFFFFFFFFFFFFFFFF == 0xFFFFFFFFFFFFFFFF) ++ - test "Array UInt32 empty" (roundtripArrayUInt32 #[] == #[]) ++ - test "Array UInt32 [1,2,3]" (roundtripArrayUInt32 #[1, 2, 3] == #[1, 2, 3]) ++ - test "Array UInt32 [0, max]" (roundtripArrayUInt32 #[0, 0xFFFFFFFF] == #[0, 0xFFFFFFFF]) ++ - test "Array UInt64 empty" (roundtripArrayUInt64 #[] == #[]) ++ - test "Array UInt64 [1,2,3]" (roundtripArrayUInt64 #[1, 2, 3] == #[1, 2, 3]) ++ - test "Array UInt64 [0, max]" (roundtripArrayUInt64 #[0, 0xFFFFFFFFFFFFFFFF] == #[0, 0xFFFFFFFFFFFFFFFF]) ++ - test "Float 0.0" (roundtripFloat 0.0 == 0.0) ++ - test "Float 3.14" (roundtripFloat 3.14 == 3.14) ++ - test "Float -1.5" (roundtripFloat (-1.5) == -1.5) ++ - test "Float32 0.0" (roundtripFloat32 0.0 == 0.0) ++ - test "Float32 3.14" (roundtripFloat32 3.14 == 3.14) ++ - test "USize 0" (roundtripUSize 0 == 0) ++ - test "USize 42" (roundtripUSize 42 == 42) ++ - test "Array Float [1.5, 2.5]" (roundtripArrayFloat #[1.5, 2.5] == #[1.5, 2.5]) ++ - test "Array Float32 [1.5, 2.5]" (roundtripArrayFloat32 #[1.5, 2.5] == #[1.5, 2.5]) ++ - test "String from_bytes empty" (roundtripStringFromBytes "" == "") ++ - test "String from_bytes hello" (roundtripStringFromBytes "hello" == "hello") ++ - test "Array push empty" (roundtripArrayPush #[] == #[]) ++ - test "Array push [1,2,3]" (roundtripArrayPush #[1, 2, 3] == #[1, 2, 3]) - -/-! ## Except tests -/ - -def exceptTests : TestSeq := - test "Except.ok 42" (show Bool from - match roundtripExceptStringNat (.ok 42) with - | .ok n => n == 42 - | .error _ => false) ++ - test "Except.error hello" (show Bool from - match roundtripExceptStringNat (.error "hello") with - | .error s => s == "hello" - | .ok _ => false) ++ - test "Except.error_string" (show Bool from - match exceptErrorString "boom" with - | .error s => s == "boom" - | .ok _ => false) - -/-! ## IO result tests -/ - -def ioResultTests : TestSeq := - test "IOResult ok 42" (show Bool from - match ioResultOkNat 42 with - | .ok val _ => val == 42 - | .error _ _ => false) ++ - test "IOResult error" (show Bool from - match ioResultErrorString "oops" with - | .error _ _ => true - | .ok _ _ => false) - -/-! ## Scalar struct tests -/ - -def scalarStructTests : TestSeq := - test "ScalarStruct (0, 0, 0, 0)" (roundtripScalarStruct ⟨0, 0, 0, 0⟩ == ⟨0, 0, 0, 0⟩) ++ - test "ScalarStruct (42, 255, 1000, 9999)" (roundtripScalarStruct ⟨42, 255, 1000, 9999⟩ == ⟨42, 255, 1000, 9999⟩) ++ - test "ScalarStruct max vals" (roundtripScalarStruct ⟨100, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩ == ⟨100, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩) - -/-! ## Extended scalar struct tests -/ - -def extScalarStructTests : TestSeq := - test "ExtScalarStruct zeros" (show Bool from roundtripExtScalarStruct ⟨0, 0, 0, 0, 0, 0.0, 0.0⟩ == ⟨0, 0, 0, 0, 0, 0.0, 0.0⟩) ++ - test "ExtScalarStruct mixed" (show Bool from roundtripExtScalarStruct ⟨42, 255, 1000, 50000, 9999, 3.14, 2.5⟩ == ⟨42, 255, 1000, 50000, 9999, 3.14, 2.5⟩) ++ - test "ExtScalarStruct max ints" (show Bool from roundtripExtScalarStruct ⟨100, 0xFF, 0xFFFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF, 1.0, 1.0⟩ == ⟨100, 0xFF, 0xFFFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF, 1.0, 1.0⟩) - -/-! ## USize struct tests -/ - -def usizeStructTests : TestSeq := - test "USizeStruct zeros" (roundtripUSizeStruct ⟨0, 0, 0⟩ == ⟨0, 0, 0⟩) ++ - test "USizeStruct mixed" (roundtripUSizeStruct ⟨42, 99, 255⟩ == ⟨42, 99, 255⟩) - -/-! ## External object tests -/ - -def externalTests : TestSeq := - test "External create and get x" (rustDataGetX (mkRustData 42 99 "hello") == 42) ++ - test "External create and get y" (rustDataGetY (mkRustData 42 99 "hello") == 99) ++ - 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) - -/-! ## Edge cases for large Nats -/ - -def largeNatTests : TestSeq := - let testCases : List Nat := [0, 1, 255, 256, 65535, 65536, (2^32 - 1), 2^32, - (2^63 - 1), 2^63, (2^64 - 1), 2^64, 2^64 + 1, 2^128, 2^256] - testCases.foldl (init := .done) fun acc n => - acc ++ .individualIO s!"Nat {n}" none (do - let rt := roundtripNat n - pure (rt == n, 0, 0, if rt == n then none else some s!"got {rt}")) .done - -/-! ## 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), -] - -end Tests.FFI diff --git a/test/Tests/Main.lean b/test/Tests/Main.lean deleted file mode 100644 index 94cb8a9..0000000 --- a/test/Tests/Main.lean +++ /dev/null @@ -1,8 +0,0 @@ -import Tests.FFI -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), - ] - LSpec.lspecIO suites args diff --git a/test/lakefile.lean b/test/lakefile.lean deleted file mode 100644 index 670c0f2..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 - supportInterpreter := true - -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 diff --git a/test/src/lib.rs b/test/src/lib.rs deleted file mode 100644 index 9df0208..0000000 --- a/test/src/lib.rs +++ /dev/null @@ -1,423 +0,0 @@ -//! FFI roundtrip functions for testing lean-ffi. -//! -//! 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. - -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, -}; - -/// Build a Lean Nat from a Rust Nat (delegates to `Nat::to_lean`). -fn build_nat(n: &Nat) -> LeanObject { - n.to_lean().into() -} - -// ============================================================================= -// Roundtrip FFI functions -// ============================================================================= - -/// 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) -} - -/// 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 { - 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 -} - -/// 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(); - 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); - let arr = LeanArray::alloc(nats.len()); - for (i, nat) in nats.iter().enumerate() { - arr.set(i, build_nat(nat)); - } - arr -} - -/// Round-trip a ByteArray: decode from Lean, re-encode to Lean. -#[unsafe(no_mangle)] -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() - } else { - // some val - let nat = Nat::from_obj(opt.as_ctor().get(0)); - LeanOption::some(build_nat(&nat)).into() - } -} - -/// 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 -} - -/// 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) -} - -fn roundtrip_nat_tree_recursive(ctor: LeanCtor) -> LeanObject { - match ctor.tag() { - 0 => { - // leaf : Nat → NatTree - let nat = Nat::from_obj(ctor.get(0)); - let leaf = LeanCtor::alloc(0, 1, 0); - leaf.set(0, build_nat(&nat)); - *leaf - } - 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 node = LeanCtor::alloc(1, 2, 0); - node.set(0, left); - node.set(1, right); - *node - } - _ => panic!("Invalid NatTree tag: {}", ctor.tag()), - } -} - -// ============================================================================= -// LeanProd roundtrip -// ============================================================================= - -/// Round-trip a Prod Nat Nat: decode fst/snd via LeanCtor, 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() -} - -// ============================================================================= -// LeanExcept roundtrip -// ============================================================================= - -/// 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() - } - 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() - } - _ => 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() -} - -// ============================================================================= -// LeanIOResult roundtrip -// ============================================================================= - -/// 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() -} - -/// 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() -} - -// ============================================================================= -// 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). -#[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); - - 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 -} - -// ============================================================================= -// box_u32 / box_u64 roundtrip -// ============================================================================= - -/// 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 { - 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 { - val -} - -/// Round-trip an Array UInt32. Elements are boxed lean_object* inside the -/// array, so this exercises LeanObject::box_u32 / unbox_u32. -#[unsafe(no_mangle)] -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 -} - -/// Round-trip an Array UInt64. Elements are boxed lean_object* inside the -/// array, so this exercises LeanObject::box_u64 / unbox_u64. -#[unsafe(no_mangle)] -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 -} - -// ============================================================================= -// LeanExternal roundtrip -// ============================================================================= - -/// A simple Rust struct to store in a Lean external object. -#[derive(Debug, Clone, PartialEq)] -struct RustData { - x: u64, - y: u64, - label: String, -} - -static RUST_DATA_CLASS: LazyLock = - LazyLock::new(ExternalClass::register_with_drop::); - -/// Create a LeanExternal from three Lean values (x : UInt64, y : UInt64, label : String). -#[unsafe(no_mangle)] -pub extern "C" fn rs_external_create(x: u64, y: u64, label: LeanString) -> LeanObject { - let data = RustData { - x, - y, - label: label.to_string(), - }; - let ext = LeanExternal::alloc(&RUST_DATA_CLASS, data); - ext.into() -} - -/// Read the x field from a LeanExternal. -#[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_x(obj: LeanObject) -> u64 { - let ext = unsafe { LeanExternal::::from_raw(obj.as_ptr()) }; - ext.get().x -} - -/// Read the y field from a LeanExternal. -#[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_y(obj: LeanObject) -> u64 { - let ext = unsafe { LeanExternal::::from_raw(obj.as_ptr()) }; - ext.get().y -} - -/// Read the label field from a LeanExternal. -#[unsafe(no_mangle)] -pub extern "C" fn rs_external_get_label(obj: LeanObject) -> LeanString { - let ext = unsafe { LeanExternal::::from_raw(obj.as_ptr()) }; - LeanString::new(&ext.get().label) -} - -// ============================================================================= -// 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 -} - -// ============================================================================= -// 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. -#[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); - - 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 -} - -// ============================================================================= -// Float / Float32 / USize scalar roundtrips -// ============================================================================= - -/// Round-trip a Float (f64) — passed as raw scalar across FFI. -#[unsafe(no_mangle)] -pub 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 { - val -} - -/// Round-trip a USize — passed as raw scalar across FFI. -#[unsafe(no_mangle)] -pub extern "C" fn rs_roundtrip_usize(val: usize) -> usize { - val -} - -/// Round-trip an Array Float. Elements are boxed f64 inside the array. -#[unsafe(no_mangle)] -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 -} - -/// Round-trip an Array Float32. Elements are boxed f32 inside the array. -#[unsafe(no_mangle)] -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 -} - -// ============================================================================= -// LeanString::from_bytes roundtrip -// ============================================================================= - -/// 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 { - let s = s_ptr.to_string(); - LeanString::from_bytes(s.as_bytes()) -} - -// ============================================================================= -// LeanArray::push roundtrip -// ============================================================================= - -/// 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); - let mut arr = LeanArray::alloc(0); - for nat in &nats { - arr = arr.push(build_nat(nat)); - } - arr -}