diff --git a/README.md b/README.md index 69482cd..42e4a4a 100644 --- a/README.md +++ b/README.md @@ -84,6 +84,83 @@ impl LeanPutResponse { } ``` +### External objects (`LeanExternal`) + +External objects let you store arbitrary Rust data inside a Lean object. Lean +sees an opaque type; Rust controls allocation, access, mutation, and cleanup. + +**Register** an external class exactly once, using `OnceLock` or `LazyLock`: + +```rust +use std::sync::LazyLock; +use lean_ffi::object::{ExternalClass, LeanExternal, LeanOwned, LeanBorrowed}; + +struct Hasher { state: Vec } + +// register_with_drop generates a finalizer that calls drop(Box::from_raw(ptr)) +// and a no-op foreach (no Lean objects inside T to traverse). +static HASHER_CLASS: LazyLock = + LazyLock::new(ExternalClass::register_with_drop::); +``` + +**Create** — `LeanExternal::alloc` boxes the value and returns an owned +external object: + +```rust +// Lean: @[extern "rs_hasher_new"] opaque Hasher.new : Unit → Hasher +#[unsafe(no_mangle)] +extern "C" fn rs_hasher_new(_unit: LeanOwned) -> LeanExternal { + LeanExternal::alloc(&HASHER_CLASS, Hasher { state: Vec::new() }) +} +``` + +**Read** — `.get()` borrows the stored `&T`. Works on both owned and borrowed +references: + +```rust +// Lean: @[extern "rs_hasher_bytes"] opaque Hasher.bytes : @& Hasher → ByteArray +#[unsafe(no_mangle)] +extern "C" fn rs_hasher_bytes( + h: LeanExternal>, // @& → borrowed +) -> LeanByteArray { + LeanByteArray::from_bytes(&h.get().state) // &Hasher — no clone, no refcount change +} +``` + +**Update** — `.get_mut()` returns `Option<&mut T>`, which is `Some` when the +object is exclusively owned (`m_rc == 1`). This enables +in-place mutation without allocating a new external object. When shared `.get_mut()` +returns `None` and instead clones into a new object on write. + +```rust +// Lean: @[extern "rs_hasher_update"] opaque Hasher.update : Hasher → @& ByteArray → Hasher +#[unsafe(no_mangle)] +extern "C" fn rs_hasher_update( + mut h: LeanExternal, + input: LeanByteArray>, +) -> LeanExternal { + if let Some(state) = h.get_mut() { + state.state.extend_from_slice(input.as_bytes()); // mutate in place + h + } else { + // shared — clone and allocate a new external object + let mut new_state = h.get().clone(); + new_state.state.extend_from_slice(input.as_bytes()); + LeanExternal::alloc(&HASHER_CLASS, new_state) + } +} +``` + +**Delete** — follows the same ownership rules as other domain types: + +- `LeanExternal` — `Drop` calls `lean_dec`. When the refcount + reaches zero, Lean calls the class finalizer, which (via `register_with_drop`) + runs `drop(Box::from_raw(ptr))` to free the Rust value. +- `LeanExternal>` — no refcount changes, no cleanup. + Use for `@&` parameters. +- Converting to `LeanOwned` (e.g. to store in a ctor field): call `.into()`. + + ### FFI function signatures Use domain types in `extern "C"` function signatures. The ownership type parameter @@ -134,6 +211,44 @@ let size = ctor.get_u64(1, 0); // u64 at scalar offset 0 (past 1 non-scalar let flag = ctor.get_bool(1, 8); // bool at scalar offset 8 ``` +## In-Place Mutation + +Lean's runtime supports in-place mutation when an object is **exclusively owned** +(`m_rc == 1`, single-threaded mode). When shared, the object is copied first. +`LeanRef::is_exclusive()` exposes this check. + +These methods consume `self` and return a (possibly new) object, mutating in +place when exclusive or copying first when shared: + +### `LeanArray` + +| Method | C equivalent | Description | +|--------|--------------|-------------| +| `set(&self, i, val)` | `lean_array_set_core` | Set element (asserts exclusive — use for freshly allocated arrays) | +| `uset(self, i, val)` | `lean_array_uset` | Set element (copies if shared) | +| `push(self, val)` | `lean_array_push` | Append an element | +| `pop(self)` | `lean_array_pop` | Remove the last element | +| `uswap(self, i, j)` | `lean_array_uswap` | Swap elements at `i` and `j` | + +### `LeanByteArray` + +| Method | C equivalent | Description | +|--------|--------------|-------------| +| `set_data(&self, data)` | `lean_sarray_cptr` + memcpy | Bulk write (asserts exclusive — use for freshly allocated arrays) | +| `uset(self, i, val)` | `lean_byte_array_uset` | Set byte (copies if shared) | +| `push(self, val)` | `lean_byte_array_push` | Append a byte | +| `copy(self)` | `lean_copy_byte_array` | Deep copy into a new exclusive array | + +### `LeanString` + +| Method | C equivalent | Description | +|--------|--------------|-------------| +| `push(self, c)` | `lean_string_push` | Append a UTF-32 character | +| `append(self, other)` | `lean_string_append` | Concatenate another string (borrowed) | + +`LeanExternal` also supports in-place mutation via `get_mut()` — see the +**Update** section under [External objects](#external-objects-leanexternalt-r). + ## Notes ### Rust panic behavior @@ -162,10 +277,13 @@ without special handling. ### `lean_string_size` vs `lean_string_byte_size` `lean_string_byte_size` returns the **total object memory size** -(`sizeof(lean_string_object) + m_size`), not the string data length. +(`sizeof(lean_string_object) + capacity`), not the string data length. Use `lean_string_size` instead, which returns `m_size` — the number of data -bytes including the NUL terminator. The `LeanString::byte_len()` wrapper handles -this correctly by returning `lean_string_size(obj) - 1`. +bytes including the NUL terminator. `LeanString` wraps these correctly: + +- `byte_len()` — data bytes excluding NUL (`m_size - 1`) +- `length()` — UTF-8 character count (`m_length`) +- `as_str()` — view as `&str` ## License diff --git a/Tests/FFI.lean b/Tests/FFI.lean index 7a9e12d..d43a1f2 100644 --- a/Tests/FFI.lean +++ b/Tests/FFI.lean @@ -248,6 +248,43 @@ opaque natMinHeap : Unit → Nat @[extern "rs_external_all_fields"] opaque externalAllFields : @& RustData → String +@[extern "rs_string_length"] +opaque stringLength : @& String → USize + +/-! ## FFI declarations — memory management stress tests -/ + +@[extern "rs_alloc_drop_stress"] +opaque allocDropStress : Unit → UInt8 + +@[extern "rs_mutation_drop_stress"] +opaque mutationDropStress : Unit → UInt8 + +@[extern "rs_clone_drop_stress"] +opaque cloneDropStress : @& Array Nat → USize → USize + +@[extern "rs_array_list_roundtrip"] +opaque arrayListRoundtrip : @& Array Nat → Array Nat + +@[extern "rs_bytearray_copy_mutate"] +opaque byteArrayCopyMutate : ByteArray → ByteArray + +/-! ## FFI declarations — in-place mutation tests -/ + +@[extern "rs_array_mut_ops"] +opaque arrayMutOps : Array Nat → Array Nat + +@[extern "rs_bytearray_mut_ops"] +opaque bytearrayMutOps : ByteArray → ByteArray + +@[extern "rs_string_mut_ops"] +opaque stringMutOps : String → @& String → String + +@[extern "rs_external_set_x"] +opaque externalSetX : RustData → UInt64 → RustData + +@[extern "rs_external_lifecycle"] +opaque externalLifecycle : UInt64 → UInt64 → @& String → UInt64 → String + /-! ## FFI declarations — persistent object tests -/ @[extern "rs_is_persistent"] @@ -300,266 +337,96 @@ private def persistentPoint : Point := ⟨10, 20⟩ private def persistentArray : Array Nat := #[1, 2, 3, 4, 5] private def persistentString : String := "hello persistent" -/-! ## Unit tests -/ +/-! ## Borrowed roundtrip tests — types without property test generators -/ -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") ++ +def borrowedRoundtripTests : TestSeq := 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 UInt32 [0, max]" (roundtripArrayUInt32 #[0, 0xFFFFFFFF] == #[0, 0xFFFFFFFF]) ++ + test "Array UInt64 [0, max]" (roundtripArrayUInt64 #[0, 0xFFFFFFFFFFFFFFFF] == #[0, 0xFFFFFFFFFFFFFFFF]) ++ 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 "Nested array [[]]" (roundtripNestedArray #[#[]] == #[#[]]) ++ + test "Nested list [[]]" (roundtripNestedList [[]] == [[]]) ++ + test "ScalarStruct zeros" (roundtripScalarStruct ⟨0, 0, 0, 0⟩ == ⟨0, 0, 0, 0⟩) ++ + test "ScalarStruct max" (roundtripScalarStruct ⟨100, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩ == ⟨100, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩) ++ 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 "ExtScalarStruct max" (show Bool from roundtripExtScalarStruct ⟨100, 0xFF, 0xFFFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF, 1.0, 1.0⟩ == ⟨100, 0xFF, 0xFFFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF, 1.0, 1.0⟩) ++ 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 "USizeStruct mixed" (roundtripUSizeStruct ⟨42, 99, 255⟩ == ⟨42, 99, 255⟩) ++ test "External all fields" (externalAllFields (mkRustData 42 99 "hello") == "42:99:hello") ++ - test "External all fields zeros" (externalAllFields (mkRustData 0 0 "") == "0:0:") + test "External all fields zeros" (externalAllFields (mkRustData 0 0 "") == "0:0:") ++ + test "External large u64" (rustDataGetX (mkRustData 0xFFFFFFFFFFFFFFFF 0 "test") == 0xFFFFFFFFFFFFFFFF) ++ + test "Except error_string" (show Bool from + match exceptErrorString "boom" with | .error s => s == "boom" | .ok _ => false) ++ + test "IOResult ok" (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) ++ + test "Borrowed result chain" (borrowedResultChain (#[1, 2], #[3, 4]) == 10) ++ + test "Borrowed except ok" (borrowedExceptValue (.ok 42) == 42) ++ + test "Borrowed except error" (borrowedExceptValue (.error "hello") == 5) ++ + test "String length unicode" (stringLength "héllo" == 5) -/-! ## Edge cases for large Nats -/ +/-! ## Edge cases — Nat boundaries and empty collections -/ -def largeNatTests : TestSeq := - let testCases : List Nat := [0, 1, 255, 256, 65535, 65536, (2^32 - 1), 2^32, +def edgeCaseTests : TestSeq := + let natBoundaries : 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 => + natBoundaries.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 + pure (rt == n, 0, 0, if rt == n then none else some s!"got {rt}")) .done ++ 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) +/-! ## Owned argument tests — patterns not covered by property tests -/ + +def ownedArgTests : TestSeq := + test "Drop and replace" (ownedDropAndReplace "hello" == "replaced:5") ++ + test "Merge 3 owned lists" (ownedMergeLists [1, 2] [3] [4, 5] == [1, 2, 3, 4, 5]) ++ + test "Merge 3 empty lists" (ownedMergeLists [] [] [] == []) ++ + test "Reverse bytearray" (ownedReverseByteArray ⟨#[1, 2, 3]⟩ == ⟨#[3, 2, 1]⟩) ++ + test "Reverse empty bytearray" (ownedReverseByteArray ⟨#[]⟩ == ⟨#[]⟩) ++ + test "IOResult ok value" (ownedIOResultValue (ioResultOkNat 42) == 42) ++ + test "IOResult error value" (ownedIOResultValue (ioResultErrorString "oops") == 0) + +/-! ## In-place mutation tests -/ + +def mutationTests : TestSeq := + test "ByteArray copy mutate" (byteArrayCopyMutate ⟨#[1, 2, 3]⟩ == ⟨#[255, 2, 3]⟩) ++ + test "External lifecycle" (externalLifecycle 10 20 "hi" 99 == "10:20:hi/99:20:hi") + +/-! ## Chained owned FFI — each type: create → owned roundtrip → owned roundtrip → check -/ + +def chainedTests : TestSeq := + let arr := ownedArrayNatRoundtrip (ownedArrayNatRoundtrip #[1, 2, 3]) + test "Array" (arr == #[1, 2, 3]) ++ + let ba := ownedByteArrayRoundtrip (ownedByteArrayRoundtrip ⟨#[10, 20, 30]⟩) + test "ByteArray" (ba == ⟨#[10, 20, 30]⟩) ++ + let s := ownedStringRoundtrip (ownedStringRoundtrip "hello") + test "String" (s == "hello") ++ + let obj := externalSetX (externalSetX (mkRustData 10 20 "hi") 99) 42 + test "External" (rustDataGetX obj == 42 && rustDataGetY obj == 20) + +/-! ## Memory management stress tests (Valgrind targets) -/ +-- These functions allocate and drop objects entirely in Rust without returning +-- them to Lean. Valgrind detects leaks, double-frees, or use-after-free. + +def memoryTests : TestSeq := + test "Alloc/drop stress" (allocDropStress () == 1) ++ + test "Mutation/drop stress" (mutationDropStress () == 1) ++ + test "Clone/drop stress" (cloneDropStress #[1, 2, 3] 100 == 300) + /-! ## 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, @@ -576,8 +443,7 @@ def persistentTests : TestSeq := 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 Nat stable" (readPersistentNat persistentNat == 42) ++ test "Persistent Array stable" (readPersistentArray persistentArray == 15) /-! ## Property-based tests -/ @@ -586,24 +452,19 @@ def persistentTests : TestSeq := -- 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 "Roundtrip" borrowedRoundtripTests, group "Edge cases" edgeCaseTests, ] public def ownedSuite : List TestSeq := [ group "Drop" ownedArgTests, - group "Clone" cloneTests, + group "In-place mutation" mutationTests, + group "Chained FFI" chainedTests, + group "Memory management" memoryTests, ] public def persistentSuite : List TestSeq := [ @@ -620,8 +481,22 @@ public def propertySuite : List TestSeq := [ checkIO "Option Nat" (∀ o : Option Nat, roundtripOptionNat o == o) ++ checkIO "Point" (∀ p : Point, roundtripPoint p == p) ++ checkIO "NatTree" (∀ t : NatTree, roundtripNatTree t == t) ++ + checkIO "Except" (∀ e : Except String Nat, show Bool from roundtripExceptStringNat e == e) ++ + checkIO "UInt32" (∀ n : UInt32, roundtripUInt32 n == n) ++ + checkIO "UInt64" (∀ n : UInt64, roundtripUInt64 n == n) ++ + checkIO "USize" (∀ n : USize, roundtripUSize n == n) ++ + checkIO "String from bytes" (∀ s : String, roundtripStringFromBytes s == s) ++ + checkIO "Array push" (∀ arr : Array Nat, roundtripArrayPush arr == arr) ++ + checkIO "Array list roundtrip" (∀ arr : Array Nat, arrayListRoundtrip arr == arr) ++ + checkIO "Nested Array" (∀ arr : Array (Array Nat), roundtripNestedArray arr == arr) ++ + checkIO "Nested List" (∀ xs : List (List Nat), roundtripNestedList xs == xs) ++ checkIO "Prod swap" (∀ p : Nat × Nat, prodSwap p == (p.2, p.1)) ++ - checkIO "Borrow to owned" (∀ n : Nat, borrowToOwned n == n)), + checkIO "Borrow to owned" (∀ n : Nat, borrowToOwned n == n) ++ + checkIO "String length" (∀ s : String, (stringLength s).toNat == s.length) ++ + checkIO "Option unwrap" (∀ o : Option Nat, optionUnwrapOrZero o == o.getD 0) ++ + checkIO "Except map ok" (∀ e : Except String Nat, + exceptMapOk e == match e with | .ok n => n + 1 | .error _ => 0) ++ + checkIO "Multi borrow sum" (∀ arr : Array Nat, multiBorrowSum arr == arr.toList.foldl (· + ·) 0)), group "Owned Drop" ( checkIO "Nat" (∀ n : Nat, ownedNatRoundtrip n == n) ++ checkIO "String" (∀ s : String, ownedStringRoundtrip s == s) ++ @@ -633,7 +508,11 @@ public def propertySuite : List TestSeq := [ 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)), + ownedExceptTransform e == match e with | .ok n => 2 * n | .error s => s.utf8ByteSize) ++ + checkIO "Append nat" (∀ arr : Array Nat, ∀ n : Nat, ownedAppendNat arr n == arr.push n) ++ + checkIO "Point sum" (∀ p : Point, ownedPointSum p == p.x + p.y) ++ + checkIO "Scalar sum" (∀ s : ScalarStruct, + ownedScalarSum s == s.u8val.toUInt64 + s.u32val.toUInt64 + s.u64val)), group "Clone + Drop" ( checkIO "Except" (∀ e : Except String Nat, cloneExcept e == match e with | .ok n => 2 * n | .error s => 2 * s.utf8ByteSize) ++ @@ -641,7 +520,9 @@ public def propertySuite : List TestSeq := [ 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))), + checkIO "Prod" (∀ p : Nat × Nat, cloneProd p == 2 * (p.1 + p.2)) ++ + checkIO "Array len sum" (∀ arr : Array Nat, (cloneArrayLenSum arr).toNat == 2 * arr.size) ++ + checkIO "String len sum" (∀ s : String, (cloneStringLenSum s).toNat == 2 * s.utf8ByteSize)), 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)), @@ -657,7 +538,6 @@ def sharedTests : TestSeq := 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) ++ @@ -668,7 +548,6 @@ def sharedTests : TestSeq := -- 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) ++ diff --git a/Tests/Gen.lean b/Tests/Gen.lean index 5e8264f..59337e8 100644 --- a/Tests/Gen.lean +++ b/Tests/Gen.lean @@ -181,6 +181,57 @@ instance : Shrinkable (Except String Nat) where | .ok n => .ok 0 :: (Shrinkable.shrink n |>.map .ok) | .error s => .ok 0 :: (Shrinkable.shrink s |>.map .error) +/-! ## Scalar type generators -/ + +def genUInt32 : Gen UInt32 := UInt32.ofNat <$> choose Nat 0 (2^32 - 1) +def genUInt64 : Gen UInt64 := UInt64.ofNat <$> choose Nat 0 (2^64 - 1) +def genUSize : Gen USize := USize.ofNat <$> choose Nat 0 (2^64 - 1) + +def genScalarStruct : Gen ScalarStruct := do + let obj ← genSmallNat + let u8 ← UInt8.ofNat <$> choose Nat 0 255 + let u32 ← genUInt32 + let u64 ← genUInt64 + pure ⟨obj, u8, u32, u64⟩ + +/-! ## Nested collection generators -/ + +def genNestedArrayNat : Gen (Array (Array Nat)) := do + let len ← choose Nat 0 5 + let mut result := #[] + for _ in [:len] do + result := result.push (← genArrayNat) + pure result + +def genNestedListNat : Gen (List (List Nat)) := do + let len ← choose Nat 0 5 + let mut result := [] + for _ in [:len] do + result := (← genListNat) :: result + pure result.reverse + +/-! ## Shrinkable instances for new types -/ + +instance : Shrinkable UInt32 where + shrink n := if n == 0 then [] else [n / 2] + +instance : Shrinkable UInt64 where + shrink n := if n == 0 then [] else [n / 2] + +instance : Shrinkable USize where + shrink n := if n == 0 then [] else [n / 2] + +instance : Shrinkable ScalarStruct where + shrink s := if s.obj == 0 then [] else [⟨s.obj / 2, s.u8val, s.u32val, s.u64val⟩] + +instance : Shrinkable (Array (Array Nat)) where + shrink arr := if arr.isEmpty then [] else [arr.pop] + +instance : Shrinkable (List (List Nat)) where + shrink xs := match xs with + | [] => [] + | _ :: tail => [tail] + /-! ## SampleableExt instances -/ instance : SampleableExt Nat := SampleableExt.mkSelfContained genNat @@ -193,5 +244,11 @@ 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 +instance : SampleableExt UInt32 := SampleableExt.mkSelfContained genUInt32 +instance : SampleableExt UInt64 := SampleableExt.mkSelfContained genUInt64 +instance : SampleableExt USize := SampleableExt.mkSelfContained genUSize +instance : SampleableExt ScalarStruct := SampleableExt.mkSelfContained genScalarStruct +instance : SampleableExt (Array (Array Nat)) := SampleableExt.mkSelfContained genNestedArrayNat +instance : SampleableExt (List (List Nat)) := SampleableExt.mkSelfContained genNestedListNat end diff --git a/flake.nix b/flake.nix index 9299d5d..d8e9754 100644 --- a/flake.nix +++ b/flake.nix @@ -68,7 +68,8 @@ pkgs.libiconv ]; }; - rustPkg = craneLib.buildPackage (craneArgs // {cargoExtraArgs = "--locked --features test-ffi";}); + rustPkg = craneLib.buildPackage (craneArgs // {cargoExtraArgs = "--locked";}); + rustPkgTest = craneLib.buildPackage (craneArgs // {cargoExtraArgs = "--locked --features test-ffi";}); # Lake test package lake2nix = pkgs.callPackage lean4-nix.lake {}; @@ -84,7 +85,7 @@ # Link the Rust static lib so Lake can find it postConfigure = '' mkdir -p target/release - ln -s ${rustPkg}/lib/liblean_ffi.a target/release/liblean_ffi_test.a + ln -s ${rustPkgTest}/lib/liblean_ffi.a target/release/liblean_ffi_test.a ''; }; in { diff --git a/src/lib.rs b/src/lib.rs index 3586a9d..bfc274c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -41,6 +41,13 @@ pub fn safe_cstring(s: &str) -> CString { }) } +/// Signal activity to Lean's task system. Call periodically in long-running +/// FFI functions to prevent Lean from treating them as stuck. +#[inline] +pub fn inc_heartbeat() { + unsafe { include::lean_inc_heartbeat() } +} + /// No-op foreach callback for external classes that hold no Lean references. /// /// # Safety diff --git a/src/object.rs b/src/object.rs index 921616c..23afdcf 100644 --- a/src/object.rs +++ b/src/object.rs @@ -71,6 +71,13 @@ pub trait LeanRef: Clone { } } + /// True if this object has exactly one reference and is in single-threaded mode. + /// When exclusive, the object can be safely mutated in place without copying. + #[inline] + fn is_exclusive(&self) -> bool { + !self.is_scalar() && unsafe { include::lean_is_exclusive(self.as_raw()) } + } + /// 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. @@ -503,7 +510,23 @@ impl LeanArray { Self(LeanOwned(obj)) } - /// Set the `i`-th element. Takes ownership of `val`. + /// Build an array from a Lean `List`. Consumes the list. Wraps `lean_array_mk`. + pub fn from_list(list: LeanList) -> Self { + let result = unsafe { include::lean_array_mk(list.into_raw()) }; + LeanArray(LeanOwned(result)) + } + + /// Convert this array to a Lean `List`. Consumes self. Wraps `lean_array_to_list`. + pub fn to_list(self) -> LeanList { + let result = unsafe { include::lean_array_to_list(self.into_raw()) }; + LeanList(LeanOwned(result)) + } + + /// Set the `i`-th element of an exclusively owned array. Takes ownership of `val`. + /// Wraps `lean_array_set_core`, which asserts `lean_is_exclusive`. + /// + /// Use this for populating freshly allocated arrays (where `rc == 1` is guaranteed). + /// For arrays that may be shared, use [`uset`](Self::uset) instead. pub fn set(&self, i: usize, val: impl Into) { let val: LeanOwned = val.into(); unsafe { @@ -522,6 +545,32 @@ impl LeanArray { LeanArray(LeanOwned(result)) } + /// Set element `i` to `val`, ensuring exclusive ownership first. + /// If the array is shared, it is copied before mutation. + /// Consumes `self` and returns the (possibly new) array. Wraps `lean_array_uset`. + /// + /// Use this for modifying arrays that may be shared (e.g. received from Lean). + /// For populating freshly allocated arrays, [`set`](Self::set) is simpler. + pub fn uset(self, i: usize, val: impl Into) -> LeanArray { + let val: LeanOwned = val.into(); + let result = unsafe { include::lean_array_uset(self.into_raw(), i, val.into_raw()) }; + LeanArray(LeanOwned(result)) + } + + /// Remove the last element, copying the array first if it is shared. + /// Returns the array unchanged if it is empty. + pub fn pop(self) -> LeanArray { + let result = unsafe { include::lean_array_pop(self.into_raw()) }; + LeanArray(LeanOwned(result)) + } + + /// Swap elements at indices `i` and `j`, copying the array first if it is shared. + /// Wraps `lean_array_uswap`. + pub fn uswap(self, i: usize, j: usize) -> LeanArray { + let result = unsafe { include::lean_array_uswap(self.into_raw(), i, j) }; + LeanArray(LeanOwned(result)) + } + /// Consume without calling `lean_dec`. #[inline] pub fn into_raw(self) -> *mut include::lean_object { @@ -611,7 +660,9 @@ impl LeanByteArray { Self(LeanOwned(obj)) } - /// Allocate a new byte array and copy `data` into it. + /// Allocate a new byte array from a Rust byte slice. + /// Use this when constructing a Lean `ByteArray` from Rust data. + /// To duplicate an existing Lean `ByteArray`, use [`copy`](Self::copy). pub fn from_bytes(data: &[u8]) -> Self { let arr = Self::alloc(data.len()); unsafe { @@ -621,7 +672,11 @@ impl LeanByteArray { arr } - /// Copy `data` into the byte array and update its size. + /// Copy `data` into an exclusively owned byte array and update its size. + /// Wraps direct pointer writes, which assume `lean_is_exclusive`. + /// + /// Use this for populating freshly allocated byte arrays (where `rc == 1` is guaranteed). + /// For byte arrays that may be shared, use [`uset`](Self::uset) instead. /// /// # Safety /// The caller must ensure the array has sufficient capacity for `data`. @@ -635,6 +690,31 @@ impl LeanByteArray { } } + /// Set byte `i` to `val`, ensuring exclusive ownership first. + /// If the array is shared, it is copied before mutation. + /// Consumes `self` and returns the (possibly new) array. Wraps `lean_byte_array_uset`. + /// + /// For populating freshly allocated byte arrays, [`set_data`](Self::set_data) is simpler. + pub fn uset(self, i: usize, val: u8) -> LeanByteArray { + let result = unsafe { include::lean_byte_array_uset(self.into_raw(), i, val) }; + LeanByteArray(LeanOwned(result)) + } + + /// Append a byte, reallocating if needed. Copies the array first if it is shared. + pub fn push(self, val: u8) -> LeanByteArray { + let result = unsafe { include::lean_byte_array_push(self.into_raw(), val) }; + LeanByteArray(LeanOwned(result)) + } + + /// Duplicate this byte array into a new exclusively owned copy. + /// Consumes self, decrementing the original's refcount. + /// Use this to get an exclusive copy before mutation. Wraps `lean_copy_byte_array`. + /// To construct a `ByteArray` from a Rust `&[u8]`, use [`from_bytes`](Self::from_bytes). + pub fn copy(self) -> Self { + let result = unsafe { include::lean_copy_byte_array(self.into_raw()) }; + LeanByteArray(LeanOwned(result)) + } + /// Consume without calling `lean_dec`. #[inline] pub fn into_raw(self) -> *mut include::lean_object { @@ -695,18 +775,26 @@ impl LeanString { pub fn byte_len(&self) -> usize { unsafe { include::lean_string_size(self.0.as_raw()) - 1 } } + + /// The length of the string (number of UTF-8 characters, not bytes). + /// Wraps `lean_string_len`. + pub fn length(&self) -> usize { + unsafe { include::lean_string_len(self.0.as_raw()) } + } + + /// View the string data as a `&str`. + pub fn as_str(&self) -> &str { + unsafe { + let data = include::lean_string_cstr(self.0.as_raw()); + let bytes = std::slice::from_raw_parts(data.cast::(), self.byte_len()); + std::str::from_utf8_unchecked(bytes) + } + } } 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) - } + f.write_str(self.as_str()) } } @@ -734,6 +822,21 @@ impl LeanString { Self(LeanOwned(obj)) } + /// Push a UTF-32 character, ensuring exclusive ownership first. + /// Consumes `self` and returns the (possibly new) string. Wraps `lean_string_push`. + pub fn push(self, c: u32) -> LeanString { + let result = unsafe { include::lean_string_push(self.into_raw(), c) }; + LeanString(LeanOwned(result)) + } + + /// Append another string, ensuring exclusive ownership of `self` first. + /// Borrows `other`. Consumes `self` and returns the (possibly new) string. + /// Wraps `lean_string_append`. + pub fn append(self, other: &LeanString) -> LeanString { + let result = unsafe { include::lean_string_append(self.into_raw(), other.0.as_raw()) }; + LeanString(LeanOwned(result)) + } + /// Consume without calling `lean_dec`. #[inline] pub fn into_raw(self) -> *mut include::lean_object { @@ -1035,6 +1138,20 @@ impl LeanExternal { Self(LeanOwned(obj), PhantomData) } + /// Get a mutable reference to the wrapped data if the external object is + /// exclusively owned (`m_rc == 1`, single-threaded mode). + /// + /// Returns `None` if the object is shared or multi-threaded. The `&mut self` + /// requirement ensures unique Rust access, while the `is_exclusive` check + /// ensures unique Lean access. + pub fn get_mut(&mut self) -> Option<&mut T> { + if unsafe { include::lean_is_exclusive(self.0.as_raw()) } { + Some(unsafe { &mut *include::lean_get_external_data(self.0.as_raw()).cast::() }) + } else { + None + } + } + /// Consume without calling `lean_dec`. #[inline] pub fn into_raw(self) -> *mut include::lean_object { diff --git a/src/test_ffi.rs b/src/test_ffi.rs index 664fa95..a298f32 100644 --- a/src/test_ffi.rs +++ b/src/test_ffi.rs @@ -9,6 +9,7 @@ use std::sync::LazyLock; +use crate::include; use crate::nat::Nat; use crate::object::{ ExternalClass, LeanArray, LeanBool, LeanBorrowed, LeanByteArray, LeanCtor, LeanExcept, @@ -1089,6 +1090,123 @@ pub(crate) extern "C" fn rs_nat_min_heap(_unit: LeanBorrowed<'_>) -> LeanNat>) -> usize { + s.length() +} + +/// Round-trip: Array → List → Array. Tests from_list and to_list. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_array_list_roundtrip( + arr: LeanArray>, +) -> LeanArray { + let list = arr.inner().to_owned_ref(); + let arr = unsafe { LeanArray::from_raw(list.into_raw()) }; + let list = arr.to_list(); + LeanArray::from_list(list) +} + +/// Copy a byte array, mutate the copy, return the copy. +/// Tests that copy produces an independent array. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_bytearray_copy_mutate( + ba: LeanByteArray, +) -> LeanByteArray { + let copy = ba.copy(); + copy.uset(0, 255) +} + +// ============================================================================= +// In-place mutation tests (uset, pop, uswap, push, get_mut) +// ============================================================================= + +/// Exercise array mutation operations: uset, uswap, pop, push. +/// Input: [1, 2, 3, 4] → uset [0]=10 → [10, 2, 3, 4] +/// → uswap 1 3 → [10, 4, 3, 2] +/// → pop → [10, 4, 3] +/// → push 99 → [10, 4, 3, 99] +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_array_mut_ops(arr: LeanArray) -> LeanArray { + let arr = arr.uset(0, LeanOwned::from_nat_u64(10)); + let arr = arr.uswap(1, 3); + let arr = arr.pop(); + arr.push(LeanOwned::from_nat_u64(99)) +} + +/// Exercise byte array mutation operations: uset and push. +/// Input: [1, 2, 3] → uset [0]=255 → [255, 2, 3] → push 42 → [255, 2, 3, 42] +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_bytearray_mut_ops( + ba: LeanByteArray, +) -> LeanByteArray { + let ba = ba.uset(0, 255); + ba.push(42) +} + +/// Test full external object lifecycle: create → read → mutate → read. +/// Allocates in Rust (rc=1, guaranteed exclusive), reads initial state, +/// mutates x via get_mut, then verifies x changed and y/label are preserved. +/// Returns "before/after" as "x:y:label/x:y:label". +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_external_lifecycle( + x: u64, + y: u64, + label: LeanString>, + new_x: u64, +) -> LeanString { + let data = RustData { + x, + y, + label: label.to_string(), + }; + // Create + let mut ext = LeanExternal::alloc(&RUST_DATA_CLASS, data); + // Read + let before = format!("{}:{}:{}", ext.get().x, ext.get().y, ext.get().label); + // Update + if let Some(data) = ext.get_mut() { + data.x = new_x; + } + // Read again — x changed, y and label preserved + let after = format!("{}:{}:{}", ext.get().x, ext.get().y, ext.get().label); + // Delete — ext drops here via lean_dec → finalizer → Drop + LeanString::new(&format!("{before}/{after}")) +} + +/// Mutate a string: append a suffix, then push '!'. +/// Chaining from Lean tests refcounting across calls. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_string_mut_ops( + s: LeanString, + suffix: LeanString>, +) -> LeanString { + let s = s.append(&suffix); + s.push(u32::from('!')) +} + +/// Update the x field of a RustData external, returning the modified object. +/// Uses get_mut for in-place mutation when exclusive, clones otherwise. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_external_set_x( + obj: LeanRustData, + new_x: u64, +) -> LeanRustData { + let mut ext = unsafe { LeanExternal::::from_raw(obj.into_raw()) }; + if let Some(data) = ext.get_mut() { + data.x = new_x; + LeanRustData::new(ext.into()) + } else { + let mut data = ext.get().clone(); + data.x = new_x; + LeanRustData::new(LeanExternal::alloc(&RUST_DATA_CLASS, data).into()) + } +} + // ============================================================================= // External object: multiple field reads from same borrowed handle // ============================================================================= @@ -1105,6 +1223,92 @@ pub(crate) extern "C" fn rs_external_all_fields( LeanString::new(&result) } +// ============================================================================= +// Memory management stress tests (Valgrind targets) +// ============================================================================= +// These tests allocate and drop objects in Rust without returning them to Lean. +// Valgrind detects leaks (missing lean_dec), double-frees (extra lean_dec), +// or use-after-free from incorrect ownership transfer. + +/// Allocate every object type in Rust and drop them all without returning to Lean. +/// Tests that Drop impls correctly call lean_dec and that external finalizers +/// free the boxed Rust data. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_alloc_drop_stress(_unit: LeanBorrowed<'_>) -> u8 { + // Array with elements + let arr = LeanArray::alloc(3); + arr.set(0, LeanOwned::from_nat_u64(1)); + arr.set(1, LeanOwned::from_nat_u64(2)); + arr.set(2, LeanOwned::from_nat_u64(3)); + + // ByteArray + let _ba = LeanByteArray::from_bytes(&[1, 2, 3, 4, 5]); + + // String + let _s = LeanString::new("hello world"); + + // External — finalizer must run Drop on RustData (freeing the String inside) + let _ext = LeanExternal::alloc( + &RUST_DATA_CLASS, + RustData { + x: 42, + y: 99, + label: String::from("this string must be freed by the finalizer"), + }, + ); + + // List (nil) + let _nil = LeanList::nil(); + + // Nat (heap-allocated, not scalar) + let _nat = LeanOwned::from_nat_u64(u64::MAX); + + // All variables drop here at end of scope + 1 +} + +/// Chain mutations in Rust where each step frees the previous object. +/// Tests that uset/push/pop/uswap correctly dec the consumed array. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_mutation_drop_stress(_unit: LeanBorrowed<'_>) -> u8 { + // Array: each mutation consumes the old array + let arr = LeanArray::alloc(3); + arr.set(0, LeanOwned::from_nat_u64(10)); + arr.set(1, LeanOwned::from_nat_u64(20)); + arr.set(2, LeanOwned::from_nat_u64(30)); + let arr = arr.push(LeanOwned::from_nat_u64(40)); + let arr = arr.uset(0, LeanOwned::from_nat_u64(99)); + let arr = arr.uswap(0, 2); + let _arr = arr.pop(); + + // ByteArray: push and uset chain + let ba = LeanByteArray::from_bytes(&[1, 2, 3]); + let ba = ba.push(4); + let _ba = ba.uset(0, 255); + + // String: append and push chain + let s = LeanString::new("hello"); + let suffix = LeanString::new(" world"); + let s = s.append(&suffix); + let _s = s.push(u32::from('!')); + // suffix also drops here + + 1 +} + +/// Clone a borrowed array N times, read from each clone, drop all. +/// Tests that lean_inc (via to_owned_ref) and lean_dec (via Drop) are balanced. +#[unsafe(no_mangle)] +pub(crate) extern "C" fn rs_clone_drop_stress(arr: LeanArray>, n: usize) -> usize { + let mut total_len = 0; + for _ in 0..n { + let owned = arr.inner().to_owned_ref(); // lean_inc + total_len += unsafe { include::lean_array_size(owned.as_raw()) }; + // owned drops → lean_dec + } + total_len +} + // ============================================================================= // Persistent / compact region tests // =============================================================================