Abstract LeanObject usage where possible

Author: samuelburnham

lean-ffi/src/lib.rs

@@ -67,11 +67,6 @@ macro_rules! lean_domain_type {
       fn from(x: $name) -> Self { x.0 }
     }
 
-    impl From<$crate::object::LeanObject> for $name {
-      #[inline]
-      fn from(obj: $crate::object::LeanObject) -> Self { Self(obj) }
-    }
-
     impl $name {
       #[inline]
       pub fn new(obj: $crate::object::LeanObject) -> Self { Self(obj) }

lean-ffi/src/nat.rs

@@ -3,7 +3,7 @@
 //! Lean stores small naturals as tagged scalars and large ones as GMP
 //! `mpz_object`s on the heap. This module handles both representations.
 
-use std::ffi::{c_int, c_void};
+use std::ffi::c_int;
 use std::fmt;
 use std::mem::MaybeUninit;
 
@@ -36,28 +36,19 @@ impl Nat {
     u64::try_from(&self.0).ok()
   }
 
-  /// Decode a `Nat` from a Lean object pointer. Handles both scalar (unboxed)
+  /// Decode a `Nat` from a `LeanObject`. Handles both scalar (unboxed)
   /// and heap-allocated (GMP `mpz_object`) representations.
-  ///
-  /// # Safety
-  /// The pointer must be a valid Lean `Nat` object (scalar or mpz).
-  pub unsafe fn from_ptr(ptr: *const c_void) -> Nat {
-    let obj = unsafe { LeanObject::from_raw(ptr) };
+  pub fn from_obj(obj: LeanObject) -> Nat {
     if obj.is_scalar() {
       let u = obj.unbox_usize();
       Nat(BigUint::from_bytes_le(&u.to_le_bytes()))
     } else {
       // Heap-allocated big integer (mpz_object)
-      let mpz: &MpzObject = unsafe { &*ptr.cast() };
+      let mpz: &MpzObject = unsafe { &*obj.as_ptr().cast() };
       Nat(mpz.m_value.to_biguint())
     }
   }
 
-  /// Decode a `Nat` from a `LeanObject`. Convenience wrapper over `from_ptr`.
-  pub fn from_obj(obj: LeanObject) -> Nat {
-    unsafe { Self::from_ptr(obj.as_ptr()) }
-  }
-
   #[inline]
   pub fn from_le_bytes(bytes: &[u8]) -> Nat {
     Nat(BigUint::from_bytes_le(bytes))
@@ -133,7 +124,7 @@ unsafe extern "C" {
 
   /// Lean's internal mpz allocation — deep-copies the mpz value.
   /// Caller must still call mpz_clear on the original.
-  fn lean_alloc_mpz(v: *mut Mpz) -> *mut c_void;
+  fn lean_alloc_mpz(v: *mut Mpz) -> *mut std::ffi::c_void;
 }
 
 /// Create a Lean `Nat` from a little-endian array of u64 limbs.
@@ -143,17 +134,17 @@ unsafe extern "C" {
 pub unsafe fn lean_nat_from_limbs(
   num_limbs: usize,
   limbs: *const u64,
-) -> *mut c_void {
+) -> LeanObject {
   if num_limbs == 0 {
-    return LeanObject::box_usize(0).as_mut_ptr();
+    return LeanObject::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).as_mut_ptr();
+    return LeanObject::box_usize(first as usize);
   }
   if num_limbs == 1 {
-    return unsafe { lean_uint64_to_nat(first).cast() };
+    return unsafe { LeanObject::from_lean_ptr(lean_uint64_to_nat(first)) };
   }
   // Multi-limb: use GMP
   unsafe {
@@ -165,6 +156,6 @@ pub unsafe fn lean_nat_from_limbs(
     // 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());
-    result
+    LeanObject::from_raw(result)
   }
 }

lean-ffi/src/object.rs

@@ -98,6 +98,21 @@ impl LeanObject {
     }
   }
 
+  /// 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)`.
+  #[inline]
+  pub fn from_enum_tag(tag: usize) -> Self {
+    Self(tag as *const c_void)
+  }
+
+  /// Extract the raw tag value from a zero-field enum constructor.
+  /// Inverse of `from_enum_tag`.
+  #[inline]
+  pub fn as_enum_tag(self) -> usize {
+    self.0 as usize
+  }
+
   /// Box a `usize` into a tagged scalar pointer.
   #[inline]
   pub fn box_usize(n: usize) -> Self {
@@ -174,6 +189,62 @@ impl LeanObject {
   }
 }
 
+// =============================================================================
+// LeanNat — Nat (scalar or heap mpz)
+// =============================================================================
+
+/// Typed wrapper for a Lean `Nat` (small = tagged scalar, big = heap `mpz_object`).
+#[derive(Clone, Copy)]
+#[repr(transparent)]
+pub struct LeanNat(LeanObject);
+
+impl Deref for LeanNat {
+  type Target = LeanObject;
+  #[inline]
+  fn deref(&self) -> &LeanObject {
+    &self.0
+  }
+}
+
+impl From<LeanNat> for LeanObject {
+  #[inline]
+  fn from(x: LeanNat) -> Self {
+    x.0
+  }
+}
+
+// =============================================================================
+// LeanBool — Bool (unboxed scalar: false = 0, true = 1)
+// =============================================================================
+
+/// Typed wrapper for a Lean `Bool` (always an unboxed scalar: false = 0, true = 1).
+#[derive(Clone, Copy)]
+#[repr(transparent)]
+pub struct LeanBool(LeanObject);
+
+impl Deref for LeanBool {
+  type Target = LeanObject;
+  #[inline]
+  fn deref(&self) -> &LeanObject {
+    &self.0
+  }
+}
+
+impl From<LeanBool> for LeanObject {
+  #[inline]
+  fn from(x: LeanBool) -> Self {
+    x.0
+  }
+}
+
+impl LeanBool {
+  /// Decode to a Rust `bool`.
+  #[inline]
+  pub fn to_bool(self) -> bool {
+    self.0.as_enum_tag() != 0
+  }
+}
+
 // =============================================================================
 // LeanArray — Array α (tag LEAN_TAG_ARRAY)
 // =============================================================================

src/ffi.rs

@@ -1,3 +1,10 @@
+// Lean and C don't support feature flags, so the _iroh module is exposed as a fallback for when the `net` feature is disabled and/or on the `aarch64-darwin` target.
+// This fallback module contains dummy functions that can still be called via Lean->Rust FFI, but will return an error message that Lean then prints before exiting.
+#[cfg(any(
+  not(feature = "net"),
+  all(target_os = "macos", target_arch = "aarch64")
+))]
+pub mod _iroh;
 pub mod aiur;
 pub mod byte_array;
 #[cfg(all(

src/iroh/_client.rs src/ffi/_iroh.rssrc/iroh/_client.rs renamed to src/ffi/_iroh.rs

@@ -1,26 +1,35 @@
-use lean_ffi::object::{LeanExcept, LeanObject};
+use lean_ffi::object::{LeanArray, LeanExcept, LeanString};
 
 const ERR_MSG: &str = "Iroh functions not supported when the Rust `net` feature is disabled \
    or on MacOS aarch64-darwin";
 
 /// `Iroh.Connect.putBytes' : @& String → @& Array String → @& String → @& String → Except String PutResponse`
 #[unsafe(no_mangle)]
 extern "C" fn rs_iroh_put(
-  _node_id: LeanObject,
-  _addrs: LeanObject,
-  _relay_url: LeanObject,
-  _input: LeanObject,
+  _node_id: LeanString,
+  _addrs: LeanArray,
+  _relay_url: LeanString,
+  _input: LeanString,
 ) -> LeanExcept {
   LeanExcept::error_string(ERR_MSG)
 }
 
 /// `Iroh.Connect.getBytes' : @& String → @& Array String → @& String → @& String → Except String GetResponse`
 #[unsafe(no_mangle)]
 extern "C" fn rs_iroh_get(
-  _node_id: LeanObject,
-  _addrs: LeanObject,
-  _relay_url: LeanObject,
-  _hash: LeanObject,
+  _node_id: LeanString,
+  _addrs: LeanArray,
+  _relay_url: LeanString,
+  _hash: LeanString,
 ) -> LeanExcept {
   LeanExcept::error_string(ERR_MSG)
 }
+
+/// `Iroh.Serve.serve' : Unit → Except String Unit`
+#[unsafe(no_mangle)]
+extern "C" fn rs_iroh_serve() -> LeanExcept {
+  LeanExcept::error_string(
+    "Iroh functions not supported when the Rust `net` feature is disabled \
+     or on MacOS aarch64-darwin",
+  )
+}

src/ffi/aiur/protocol.rs

@@ -20,6 +20,7 @@ use crate::{
   ffi::aiur::{
     lean_unbox_g, lean_unbox_nat_as_usize, toplevel::decode_toplevel,
   },
+  lean::{LeanAiurFriParameters, LeanAiurToplevel},
 };
 
 // =============================================================================
@@ -63,12 +64,12 @@ extern "C" fn rs_aiur_proof_of_bytes(
 /// `AiurSystem.build : @&Bytecode.Toplevel → @&CommitmentParameters → AiurSystem`
 #[unsafe(no_mangle)]
 extern "C" fn rs_aiur_system_build(
-  toplevel: LeanObject,
+  toplevel: LeanAiurToplevel,
   commitment_parameters: LeanObject,
 ) -> LeanExternal<AiurSystem> {
   let system = AiurSystem::build(
     decode_toplevel(toplevel),
-    lean_ptr_to_commitment_parameters(commitment_parameters),
+    decode_commitment_parameters(commitment_parameters),
   );
   LeanExternal::alloc(system_class(), system)
 }
@@ -77,12 +78,12 @@ extern "C" fn rs_aiur_system_build(
 #[unsafe(no_mangle)]
 extern "C" fn rs_aiur_system_verify(
   aiur_system_obj: LeanExternal<AiurSystem>,
-  fri_parameters: LeanObject,
-  claim: LeanObject,
+  fri_parameters: LeanAiurFriParameters,
+  claim: LeanArray,
   proof_obj: LeanExternal<Proof>,
 ) -> LeanExcept {
-  let fri_parameters = lean_ctor_to_fri_parameters(fri_parameters);
-  let claim = claim.as_array().map(lean_unbox_g);
+  let fri_parameters = decode_fri_parameters(fri_parameters);
+  let claim = claim.map(lean_unbox_g);
   match aiur_system_obj.get().verify(fri_parameters, &claim, proof_obj.get()) {
     Ok(()) => LeanExcept::ok(LeanObject::box_usize(0)),
     Err(err) => LeanExcept::error_string(&format!("{err:?}")),
@@ -94,17 +95,17 @@ extern "C" fn rs_aiur_system_verify(
 #[unsafe(no_mangle)]
 extern "C" fn rs_aiur_system_prove(
   aiur_system_obj: LeanExternal<AiurSystem>,
-  fri_parameters: LeanObject,
+  fri_parameters: LeanAiurFriParameters,
   fun_idx: LeanObject,
-  args: LeanObject,
-  io_data_arr: LeanObject,
-  io_map_arr: LeanObject,
+  args: LeanArray,
+  io_data_arr: LeanArray,
+  io_map_arr: LeanArray,
 ) -> LeanObject {
-  let fri_parameters = lean_ctor_to_fri_parameters(fri_parameters);
+  let fri_parameters = decode_fri_parameters(fri_parameters);
   let fun_idx = lean_unbox_nat_as_usize(fun_idx);
-  let args = args.as_array().map(lean_unbox_g);
-  let io_data = io_data_arr.as_array().map(lean_unbox_g);
-  let io_map = lean_array_to_io_buffer_map(io_map_arr);
+  let args = args.map(lean_unbox_g);
+  let io_data = io_data_arr.map(lean_unbox_g);
+  let io_map = decode_io_buffer_map(io_map_arr);
   let mut io_buffer = IOBuffer { data: io_data, map: io_map };
 
   let (claim, proof) =
@@ -158,19 +159,19 @@ extern "C" fn rs_aiur_system_prove(
 // =============================================================================
 
 /// Build a Lean `Array G` from a slice of field elements.
-fn build_g_array(values: &[G]) -> LeanObject {
+fn build_g_array(values: &[G]) -> LeanArray {
   let arr = LeanArray::alloc(values.len());
   for (i, g) in values.iter().enumerate() {
     arr.set(i, LeanObject::box_u64(g.as_canonical_u64()));
   }
-  *arr
+  arr
 }
 
-fn lean_ptr_to_commitment_parameters(obj: LeanObject) -> CommitmentParameters {
+fn decode_commitment_parameters(obj: LeanObject) -> CommitmentParameters {
   CommitmentParameters { log_blowup: lean_unbox_nat_as_usize(obj) }
 }
 
-fn lean_ctor_to_fri_parameters(obj: LeanObject) -> FriParameters {
+fn decode_fri_parameters(obj: LeanAiurFriParameters) -> FriParameters {
   let ctor = obj.as_ctor();
   FriParameters {
     log_final_poly_len: lean_unbox_nat_as_usize(ctor.get(0)),
@@ -180,10 +181,9 @@ fn lean_ctor_to_fri_parameters(obj: LeanObject) -> FriParameters {
   }
 }
 
-fn lean_array_to_io_buffer_map(
-  obj: LeanObject,
+fn decode_io_buffer_map(
+  arr: LeanArray,
 ) -> FxHashMap<Vec<G>, IOKeyInfo> {
-  let arr = obj.as_array();
   let mut map = FxHashMap::with_capacity_and_hasher(arr.len(), FxBuildHasher);
   for elt in arr.iter() {
     let pair = elt.as_ctor();