feat: Add typed reference API

.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

.gitignore

@@ -1,5 +1,8 @@
 # Rust
-/target
+target
+
+# Lean
+.lake
 
 # Nix
 result

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"

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-<hash>/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<LeanType> 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<R>`, `LeanString<R>`, `LeanCtor<R>`,
+`LeanList<R>`, `LeanOption<R>`, `LeanExcept<R>`, `LeanIOResult<R>`, `LeanProd<R>`,
+`LeanNat<R>`, `LeanBool<R>`, `LeanByteArray<R>`, and `LeanExternal<T, R>`.
+
+### 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<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)
+    }
+}
+
+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())
+    }
+}
+```
+
+### 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<LeanBorrowed<'_>>,  // @& → borrowed, no lean_dec
+    n: LeanNat<LeanOwned>,            // owned → lean_dec on drop
+) -> LeanArray<LeanOwned> {           // 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`
 

Tests.lean

@@ -0,0 +1 @@
+import Tests.FFI