feat: LeanCtorLayout trait and lean_inductive! macro

README.md

@@ -3,15 +3,31 @@
 A Rust library that wraps low-level bindings to the
 [`lean.h`](https://github.com/leanprover/lean4/blob/master/src/include/lean/lean.h)
 Lean C library with a high-level API for safe and ergonomic FFI from Lean to
-Rust. This allows the user to focus on the actual Rust logic rather than
-manually manipulating pointers and keeping track of Lean reference counts.
+Rust. This allows the user to focus on the actual Rust logic rather than manual
+pointer manipulation and keeping track of Lean reference counts.
 
-The Rust bindings are auto-generated with
+The raw Rust bindings are auto-generated with
 [`rust-bindgen`](https://github.com/rust-lang/rust-bindgen). Bindgen runs in
 `build.rs` and generates unsafe Rust functions that link to `lean.h`. This
 module can be found at `target/release/build/lean-ffi-<hash>/out/lean.rs` after
 running `cargo build --release`.
 
+## Features
+
+- **RAII refcounting** for `LeanOwned` owned references via Rust `Clone` and
+  `Drop`
+- **Lifetime bounds** for `LeanBorrowed` borrowed references to prevent
+  use-after-free
+- **Thread-safe shared references** via `LeanShared` (`lean_mark_mt` +
+  `Send + Sync`).
+- **Typed domain wrappers** e.g. `LeanArray`, `LeanString` etc. with safe Rust
+  methods
+- **`Nat` conversions** via `num-bigint`, handling tagged scalars and big-ints
+- **`lean_inductive!` macro** for Lean `structure` / `inductive` types,
+  generating easy accessor methods without manually tracking byte offsets
+- **Safe external objects** via `ExternalClass::register_with_drop::<T>()` and
+  borrow-bound `LeanExternal<T>::get(&self) -> &T`.
+
 ## Background: Lean Ownership Model
 
 In Lean's C API, a **reference** is a `lean_object*` pointer to the header of a
@@ -102,107 +118,117 @@ becomes `LeanPoint` in Rust.
 
 #### Defining custom domain types
 
-Use the `lean_domain_type!` macro to define newtypes for your Lean types:
+`lean_inductive!` wraps a Lean `structure` or `inductive` with its full
+per-constructor layout. It emits a `#[repr(transparent)]` newtype, a
+[`LeanCtorLayout`] impl whose `LAYOUTS` slice has one entry per constructor
+(indexed by tag), and typed accessors that bounds-check against the current
+variant's layout:
+
+- `alloc(tag: u8)` — `lean_alloc_ctor` for a specific variant.
+- `get_obj(i)` / `set_obj(i, val)` — object fields.
+- `get_usize(i)` / `set_usize(i, val)` — `USize` fields.
+- `get_num_{64,32,16,8}(i)` / `set_num_{64,32,16,8}(i, val)` — scalar fields.
+
+Variant layouts are listed inside `[ … ]`, in tag order.
+
+**Structure** — from `structure Point where x : Nat; y : Nat`:
 
 ```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;
-}
+lean_ffi::lean_inductive! { LeanPoint [ { num_obj: 2 } ] }
+
+let p = LeanPoint::alloc(0);
+p.set_obj(0, x_nat);
+p.set_obj(1, y_nat);
 ```
 
-This generates a `#[repr(transparent)]` wrapper with `Clone`, `Copy` for
-`LeanBorrowed`, `self.inner()`, `self.as_raw()`, `self.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`:
+**Inductive** — from:
+
+```lean
+inductive CompareResult
+  | matched
+  | mismatch (leanSize rustSize : UInt64)
+  | notFound
+```
 
 ```rust
-impl<R: LeanRef> LeanPutResponse<R> {
-    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)
-    }
+lean_ffi::lean_inductive! {
+    LeanCompareResult [
+        { },                // matched
+        { num_64: 2 },      // mismatch
+        { },                // notFound
+    ]
 }
 
-impl LeanPutResponse<LeanOwned> {
-    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())
+// Build:
+let m = LeanCompareResult::alloc(1);
+m.set_num_64(0, lean_size);
+m.set_num_64(1, rust_size);
+
+// Read — dispatch on the Lean tag, then access fields:
+match result.as_ctor().tag() {
+    1 => {
+        let (l, r) = (result.get_num_64(0), result.get_num_64(1));
     }
+    _ => { /* matched | notFound */ }
 }
 ```
 
-### Inductive types and field layout
+For wrappers without a ctor layout (opaque externals, types represented as
+`lean_box(n)`, etc.) use the lower-level `lean_domain_type!` macro.
+
+[`LeanCtorLayout`]: https://docs.rs/lean-ffi/latest/lean_ffi/object/trait.LeanCtorLayout.html
+
+### Constructor 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:
+Lean
+[reorders constructor fields](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#run-time-inductives)
+at runtime. Declaration order does **not** match memory order. For every
+constructor, fields are laid out in this 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
+1. Object fields (`lean_object*`) — declaration order.
+2. `USize` fields — declaration order.
+3. Fixed-size scalars — descending size (8B → 4B → 2B → 1B), then declaration
+   order within each size.
 
-This means a structure like
+So for
 
 ```lean
 structure MyStruct where
-  u8val : UInt8
-  obj : Nat
+  u8val  : UInt8
+  obj    : Nat
   u32val : UInt32
   u64val : UInt64
 ```
 
-would be laid out as `[obj, u64val, u32val, u8val]` at runtime. Trivial wrapper
-types (e.g. `Char` wraps `UInt32`) count as their underlying scalar type.
+the runtime order is `[obj, u64val, u32val, u8val]`. Trivial wrappers (e.g.
+`Char` over `UInt32`) count as their underlying scalar.
 
-A constructor's memory looks like:
+Memory:
 
 ```
-[header (8B)] [object fields (8B each)] [USize fields (8B each)] [scalar data area]
+[header 8B] [object fields, 8B each] [USize fields, 8B each] [scalar bytes, descending size]
 ```
 
-Object fields and USize fields each occupy 8-byte slots. The scalar data area is
-a flat region of bytes containing all remaining scalar field values, packed by
-descending size. For `MyStruct` (1 object field, 0 USize fields, 13 scalar
-bytes):
+For `MyStruct` (`num_obj=1`, `num_usize=0`, `num_64=1`, `num_32=1`, `num_8=1`):
 
-- `u64val` occupies bytes 0–7 of the scalar area
-- `u32val` occupies bytes 8–11
-- `u8val` occupies byte 12
+- `u64val` at scalar bytes 0–7
+- `u32val` at scalar bytes 8–11
+- `u8val` at scalar byte 12
 
-Use `LeanCtor` to access fields at the correct positions. Scalar getters and
-setters take `(num_slots, byte_offset)` — `num_slots` is the total number of
-8-byte slots (object fields + USize fields) preceding the scalar data area, and
-`byte_offset` is the position of the field within that area.
+`lean_inductive!` takes the per-size field counts and hands you size-indexed
+accessors — `get_num_64(0)` for the first 8-byte scalar, `get_num_8(0)` for the
+first 1-byte scalar, etc. No hand-rolled byte offsets:
 
 ```rust
-impl<R: LeanRef> LeanScalarStruct<R> {
-    pub fn obj(&self) -> LeanBorrowed<'_> { self.as_ctor().get(0) }
-    pub fn u64val(&self) -> u64 { self.as_ctor().get_u64(1, 0) }
-    pub fn u32val(&self) -> u32 { self.as_ctor().get_u32(1, 8) }
-    pub fn u8val(&self) -> u8  { self.as_ctor().get_u8(1, 12) }
-}
-
-impl LeanScalarStruct<LeanOwned> {
-    pub fn mk(obj: LeanNat<LeanOwned>, u64val: u64, u32val: u32, u8val: u8) -> Self {
-        let ctor = LeanCtor::alloc(0, 1, 13); // tag 0, 1 obj field, 13 scalar bytes
-        ctor.set(0, obj);                // object field 0
-        ctor.set_u64(1, 0, u64val);      // 1 slot before scalars, byte 0
-        ctor.set_u32(1, 8, u32val);      // 1 slot before scalars, byte 8
-        ctor.set_u8(1, 12, u8val);       // 1 slot before scalars, byte 12
-        Self::new(ctor.into())
-    }
+lean_ffi::lean_inductive! {
+    LeanMyStruct [ { num_obj: 1, num_64: 1, num_32: 1, num_8: 1 } ]
 }
 ```
 
+For raw access (non-standard layouts, hand-tuned code), `LeanCtor` exposes
+`get_u{8,16,32,64}(offset)` / `set_u{8,16,32,64}(offset, val)` with absolute
+byte offsets matching `lean_ctor_get_uint*` / `lean_ctor_set_uint*`.
+
 ### External objects (`LeanExternal<T, R>`)
 
 External objects let you store arbitrary Rust data inside a Lean object. Lean

Tests/FFI.lean

@@ -64,6 +64,28 @@ opaque roundtripExtScalarStruct : @& ExtScalarStruct → ExtScalarStruct
 @[extern "rs_roundtrip_usize_struct"]
 opaque roundtripUSizeStruct : @& USizeStruct → USizeStruct
 
+@[extern "rs_roundtrip_usize_mixed_struct"]
+opaque roundtripUSizeMixedStruct : @& USizeMixedStruct → USizeMixedStruct
+
+@[extern "rs_roundtrip_bool_struct"]
+opaque roundtripBoolStruct : @& BoolStruct → BoolStruct
+
+
+@[extern "rs_roundtrip_multi_u32_struct"]
+opaque roundtripMultiU32Struct : @& MultiU32Struct → MultiU32Struct
+
+@[extern "rs_roundtrip_test_inductive"]
+opaque roundtripTestInductive : @& TestInductive → TestInductive
+
+@[extern "rs_roundtrip_outer"]
+opaque roundtripOuter : @& Outer → Outer
+
+@[extern "rs_roundtrip_inductive_holder"]
+opaque roundtripInductiveHolder : @& InductiveHolder → InductiveHolder
+
+@[extern "rs_roundtrip_struct_in_variant"]
+opaque roundtripStructInVariant : @& StructInVariant → StructInVariant
+
 @[extern "rs_roundtrip_float"]
 opaque roundtripFloat : Float → Float
 
@@ -359,6 +381,34 @@ def borrowedRoundtripTests : 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⟩) ++
+  -- USizeMixedStruct declaration order: obj, u64val, bval, uval, u32val
+  test "USizeMixedStruct zeros" (roundtripUSizeMixedStruct ⟨0, 0, false, 0, 0⟩ == ⟨0, 0, false, 0, 0⟩) ++
+  test "USizeMixedStruct mixed" (roundtripUSizeMixedStruct ⟨42, 0xFFFFFFFFFFFFFFFF, true, 99, 0xFFFFFFFF⟩ == ⟨42, 0xFFFFFFFFFFFFFFFF, true, 99, 0xFFFFFFFF⟩) ++
+  test "BoolStruct all false" (roundtripBoolStruct ⟨0, false, false, false⟩ == ⟨0, false, false, false⟩) ++
+  test "BoolStruct all true" (roundtripBoolStruct ⟨42, true, true, true⟩ == ⟨42, true, true, true⟩) ++
+  test "BoolStruct mixed" (roundtripBoolStruct ⟨7, true, false, true⟩ == ⟨7, true, false, true⟩) ++
+  test "MultiU32Struct zeros" (roundtripMultiU32Struct ⟨0, 0, 0, 0⟩ == ⟨0, 0, 0, 0⟩) ++
+  test "MultiU32Struct max" (roundtripMultiU32Struct ⟨100, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF⟩ == ⟨100, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF⟩) ++
+  test "MultiU32Struct mixed" (roundtripMultiU32Struct ⟨1, 42, 0, 99⟩ == ⟨1, 42, 0, 99⟩) ++
+  -- TestInductive: multi-variant inductive with non-zero tags
+  test "TestInductive empty" (roundtripTestInductive .empty == .empty) ++
+  test "TestInductive withScalars" (roundtripTestInductive (.withScalars 42 99) == .withScalars 42 99) ++
+  test "TestInductive withScalars max" (roundtripTestInductive (.withScalars 0xFFFFFFFFFFFFFFFF 0) == .withScalars 0xFFFFFFFFFFFFFFFF 0) ++
+  test "TestInductive withMixed" (roundtripTestInductive (.withMixed 7 0xFFFFFFFF true) == .withMixed 7 0xFFFFFFFF true) ++
+  test "TestInductive withMixed false" (roundtripTestInductive (.withMixed 0 0 false) == .withMixed 0 0 false) ++
+  -- Outer: structure containing another structure
+  test "Outer zeros" (roundtripOuter ⟨⟨0, 0, 0, 0⟩, "", 0⟩ == ⟨⟨0, 0, 0, 0⟩, "", 0⟩) ++
+  test "Outer mixed" (roundtripOuter ⟨⟨42, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩, "hello", 99⟩ == ⟨⟨42, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩, "hello", 99⟩) ++
+  -- InductiveHolder: structure containing an inductive
+  test "InductiveHolder empty" (roundtripInductiveHolder ⟨.empty, 0⟩ == ⟨.empty, 0⟩) ++
+  test "InductiveHolder withScalars" (roundtripInductiveHolder ⟨.withScalars 10 20, 42⟩ == ⟨.withScalars 10 20, 42⟩) ++
+  test "InductiveHolder withMixed" (roundtripInductiveHolder ⟨.withMixed 7 99 true, 0xFFFFFFFF⟩ == ⟨.withMixed 7 99 true, 0xFFFFFFFF⟩) ++
+  -- StructInVariant: inductive whose variants contain structures
+  test "StructInVariant empty" (roundtripStructInVariant .empty == .empty) ++
+  test "StructInVariant withPoint zeros" (roundtripStructInVariant (.withPoint ⟨0, 0⟩) == .withPoint ⟨0, 0⟩) ++
+  test "StructInVariant withPoint mixed" (roundtripStructInVariant (.withPoint ⟨42, 99⟩) == .withPoint ⟨42, 99⟩) ++
+  test "StructInVariant withScalar zeros" (roundtripStructInVariant (.withScalar ⟨0, 0, 0, 0⟩ 0) == .withScalar ⟨0, 0, 0, 0⟩ 0) ++
+  test "StructInVariant withScalar max" (roundtripStructInVariant (.withScalar ⟨1, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩ 0xFFFFFFFF) == .withScalar ⟨1, 0xFF, 0xFFFFFFFF, 0xFFFFFFFFFFFFFFFF⟩ 0xFFFFFFFF) ++
   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 large u64" (rustDataGetX (mkRustData 0xFFFFFFFFFFFFFFFF 0 "test") == 0xFFFFFFFFFFFFFFFF) ++

Tests/Gen.lean

@@ -122,6 +122,74 @@ structure USizeStruct where
   u8val : UInt8
 deriving Repr, BEq, DecidableEq, Inhabited
 
+/-- Structure mixing USize with other scalar types.
+    Declaration order deliberately differs from memory layout to test
+    that FFI code handles Lean's field reordering correctly.
+    Declaration: obj, u64val, bval, uval, u32val
+    Memory layout: [obj] [uval (usize slot)] [u64val @ +0] [u32val @ +8] [bval @ +12]
+    Total scalar size = 8 (usize) + 8 (u64) + 4 (u32) + 1 (bool) = 21. -/
+structure USizeMixedStruct where
+  obj : Nat
+  u64val : UInt64
+  bval : Bool
+  uval : USize
+  u32val : UInt32
+deriving Repr, BEq, DecidableEq, Inhabited
+
+/-- Structure with multiple Bool scalar fields for batch-read/write testing.
+    Layout: 1 object field (obj : Nat), then 3 Bool scalars. -/
+structure BoolStruct where
+  obj : Nat
+  b1 : Bool
+  b2 : Bool
+  b3 : Bool
+deriving Repr, BEq, DecidableEq, Inhabited
+
+/-- Structure with multiple UInt32 scalar fields for batch-read/write testing.
+    Layout: 1 object field (obj : Nat), then 3 UInt32 scalars. -/
+structure MultiU32Struct where
+  obj : Nat
+  a : UInt32
+  b : UInt32
+  c : UInt32
+deriving Repr, BEq, DecidableEq, Inhabited
+
+/-- Inductive with multiple constructors for testing non-zero TAG.
+    - empty: tag 0, no fields (scalar representation)
+    - withScalars: tag 1, 2 u64 fields
+    - withMixed: tag 2, 1 obj field + 1 u32 + 1 bool -/
+inductive TestInductive
+  | empty
+  | withScalars (a b : UInt64)
+  | withMixed (obj : Nat) (x : UInt32) (flag : Bool)
+deriving Repr, BEq, DecidableEq, Inhabited
+
+/-- Structure containing another structure as an object field.
+    Tests nested structure access via the trait API. -/
+structure Outer where
+  inner : ScalarStruct
+  label : String
+  count : UInt64
+deriving Repr, BEq, DecidableEq, Inhabited
+
+/-- Structure containing an inductive as an object field. -/
+structure InductiveHolder where
+  value : TestInductive
+  tag_copy : UInt32
+deriving Repr, BEq, DecidableEq, Inhabited
+
+/-- Inductive whose variants carry structure-typed fields.
+    Tests that variant accessors work when the variant's field is itself a
+    ctor-backed Lean structure.
+    - empty: tag 0, no fields (scalar representation)
+    - withPoint: tag 1, 1 object field (a `Point`)
+    - withScalar: tag 2, 1 object field (a `ScalarStruct`) + 1 UInt32 -/
+inductive StructInVariant
+  | empty
+  | withPoint (p : Point)
+  | withScalar (s : ScalarStruct) (extra : UInt32)
+deriving Repr, BEq, DecidableEq, Inhabited
+
 /-! ## Shrinkable instances -/
 
 instance : Shrinkable Nat where