chore: Update lean-ffi

Author: samuelburnham

Cargo.lock

@@ -11,7 +11,7 @@ anyhow = "1"
 blake3 = "1.8.2"
 itertools = "0.14.0"
 indexmap = { version = "2", features = ["rayon"] }
-lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi", rev = "a94c426f0ce0b13ffdf7940e3e6368560628f2c9" }
+lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi", rev = "b194f3f17d1959562ef850527aa70bde43358086" }
 multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "bdb0d7d66c02b554e66c449da2dbf12dc0dc27af" }
 num-bigint = "0.4.6"
 rayon = "1"

Cargo.toml

@@ -4,7 +4,7 @@ use multi_stark::{
   types::{CommitmentParameters, FriParameters},
 };
 use rustc_hash::{FxBuildHasher, FxHashMap};
-use std::sync::OnceLock;
+use std::sync::LazyLock;
 
 use lean_ffi::object::{
   ExternalClass, LeanArray, LeanBorrowed, LeanByteArray, LeanCtor, LeanExcept,
@@ -26,19 +26,13 @@ use crate::{
 };
 
 // =============================================================================
-// External class registration (OnceLock pattern)
+// External class registration
 // =============================================================================
 
-static AIUR_PROOF_CLASS: OnceLock<ExternalClass> = OnceLock::new();
-static AIUR_SYSTEM_CLASS: OnceLock<ExternalClass> = OnceLock::new();
-
-fn proof_class() -> &'static ExternalClass {
-  AIUR_PROOF_CLASS.get_or_init(ExternalClass::register_with_drop::<Proof>)
-}
-
-fn system_class() -> &'static ExternalClass {
-  AIUR_SYSTEM_CLASS.get_or_init(ExternalClass::register_with_drop::<AiurSystem>)
-}
+static AIUR_PROOF_CLASS: LazyLock<ExternalClass> =
+  LazyLock::new(ExternalClass::register_with_drop::<Proof>);
+static AIUR_SYSTEM_CLASS: LazyLock<ExternalClass> =
+  LazyLock::new(ExternalClass::register_with_drop::<AiurSystem>);
 
 // =============================================================================
 // Lean FFI functions
@@ -60,7 +54,7 @@ extern "C" fn rs_aiur_proof_of_bytes(
 ) -> LeanExternal<Proof, LeanOwned> {
   let proof =
     Proof::from_bytes(byte_array.as_bytes()).expect("Deserialization error");
-  LeanExternal::alloc(proof_class(), proof)
+  LeanExternal::alloc(&AIUR_PROOF_CLASS, proof)
 }
 
 /// `AiurSystem.build : @&Bytecode.Toplevel → @&CommitmentParameters → AiurSystem`
@@ -73,7 +67,7 @@ extern "C" fn rs_aiur_system_build(
     decode_toplevel(&toplevel),
     decode_commitment_parameters(&commitment_parameters),
   );
-  LeanExternal::alloc(system_class(), system)
+  LeanExternal::alloc(&AIUR_SYSTEM_CLASS, system)
 }
 
 /// `AiurSystem.verify : @& AiurSystem → @& FriParameters → @& Array G → @& Proof → Except String Unit`
@@ -135,7 +129,7 @@ extern "C" fn rs_aiur_system_prove(
   let (claim, proof) =
     aiur_system_obj.get().prove(fri_parameters, fun_idx, &args, &mut io_buffer);
 
-  let lean_proof: LeanOwned = LeanExternal::alloc(proof_class(), proof).into();
+  let lean_proof: LeanOwned = LeanExternal::alloc(&AIUR_PROOF_CLASS, proof).into();
   let lean_io = build_lean_io_buffer(&io_buffer);
   // Proof × Array G × Array (Array G × IOKeyInfo)
   let proof_io_tuple = LeanCtor::alloc(0, 2, 0);

src/ffi/aiur/protocol.rs

@@ -165,7 +165,7 @@ impl LeanIxConstantInfo<LeanOwned> {
         let cnst_obj = LeanIxConstantVal::build(cache, &v.cnst);
         let axiom_val = LeanCtor::alloc(0, 1, 1);
         axiom_val.set(0, cnst_obj);
-        axiom_val.set_u8(1, 0, v.is_unsafe as u8);
+        axiom_val.set_bool(1, 0, v.is_unsafe);
 
         let obj = LeanCtor::alloc(0, 1, 0);
         obj.set(0, axiom_val);
@@ -223,7 +223,7 @@ impl LeanIxConstantInfo<LeanOwned> {
         opaque_val.set(0, cnst_obj);
         opaque_val.set(1, value_obj);
         opaque_val.set(2, all_obj);
-        opaque_val.set_u8(3, 0, v.is_unsafe as u8);
+        opaque_val.set_bool(3, 0, v.is_unsafe);
 
         let obj = LeanCtor::alloc(3, 1, 0);
         obj.set(0, opaque_val);
@@ -267,9 +267,9 @@ impl LeanIxConstantInfo<LeanOwned> {
         induct_val.set(3, all_obj);
         induct_val.set(4, ctors_obj);
         induct_val.set(5, num_nested_obj);
-        induct_val.set_u8(6, 0, v.is_rec as u8);
-        induct_val.set_u8(6, 1, v.is_unsafe as u8);
-        induct_val.set_u8(6, 2, v.is_reflexive as u8);
+        induct_val.set_bool(6, 0, v.is_rec);
+        induct_val.set_bool(6, 1, v.is_unsafe);
+        induct_val.set_bool(6, 2, v.is_reflexive);
 
         let obj = LeanCtor::alloc(5, 1, 0);
         obj.set(0, induct_val);
@@ -291,7 +291,7 @@ impl LeanIxConstantInfo<LeanOwned> {
         ctor_val.set(2, cidx_obj);
         ctor_val.set(3, num_params_obj);
         ctor_val.set(4, num_fields_obj);
-        ctor_val.set_u8(5, 0, v.is_unsafe as u8);
+        ctor_val.set_bool(5, 0, v.is_unsafe);
 
         let obj = LeanCtor::alloc(6, 1, 0);
         obj.set(0, ctor_val);
@@ -317,8 +317,8 @@ impl LeanIxConstantInfo<LeanOwned> {
         rec_val.set(4, num_motives_obj);
         rec_val.set(5, num_minors_obj);
         rec_val.set(6, rules_obj);
-        rec_val.set_u8(7, 0, v.k as u8);
-        rec_val.set_u8(7, 1, v.is_unsafe as u8);
+        rec_val.set_bool(7, 0, v.k);
+        rec_val.set_bool(7, 1, v.is_unsafe);
 
         let obj = LeanCtor::alloc(7, 1, 0);
         obj.set(0, rec_val);

src/ffi/ix/constant.rs

@@ -87,7 +87,7 @@ impl LeanIxSourceInfo<LeanOwned> {
         let obj = LeanCtor::alloc(1, 2, 1);
         obj.set(0, Nat::to_lean(pos));
         obj.set(1, Nat::to_lean(end_pos));
-        obj.set_u8(2, 0, *canonical as u8);
+        obj.set_bool(2, 0, *canonical);
         Self::new(obj.into())
       },
       // | none -- tag 2
@@ -299,7 +299,7 @@ impl LeanIxDataValue<LeanOwned> {
       DataValue::OfBool(b) => {
         // 0 object fields, 1 scalar byte
         let obj = LeanCtor::alloc(1, 0, 1);
-        obj.set_u8(0, 0, *b as u8);
+        obj.set_bool(0, 0, *b);
         Self::new(obj.into())
       },
       DataValue::OfName(n) => {

src/ffi/ix/data.rs

@@ -120,7 +120,7 @@ impl LeanIxExpr<LeanOwned> {
         ctor.set(2, val_obj);
         ctor.set(3, body_obj);
         ctor.set(4, hash_obj);
-        ctor.set_u8(5, 0, *non_dep as u8);
+        ctor.set_bool(5, 0, *non_dep);
         Self::new(ctor.into())
       },
       ExprData::Lit(lit, h) => {

src/ffi/ix/expr.rs

@@ -136,8 +136,8 @@ impl LeanIxonRecursor<LeanOwned> {
     ctor.set_u64(2, 16, rec.indices);
     ctor.set_u64(2, 24, rec.motives);
     ctor.set_u64(2, 32, rec.minors);
-    ctor.set_u8(2, 40, if rec.k { 1 } else { 0 });
-    ctor.set_u8(2, 41, if rec.is_unsafe { 1 } else { 0 });
+    ctor.set_bool(2, 40, rec.k);
+    ctor.set_bool(2, 41, rec.is_unsafe);
     Self::new(ctor.into())
   }
 }
@@ -186,7 +186,7 @@ impl LeanIxonAxiom<LeanOwned> {
     ctor.set(0, typ_obj);
     // Scalar offsets from obj_cptr: 1*8=8 base
     ctor.set_u64(1, 0, ax.lvls);
-    ctor.set_u8(1, 8, if ax.is_unsafe { 1 } else { 0 });
+    ctor.set_bool(1, 8, ax.is_unsafe);
     Self::new(ctor.into())
   }
 }
@@ -265,7 +265,7 @@ impl LeanIxonConstructor<LeanOwned> {
     ctor.set_u64(1, 8, c.cidx);
     ctor.set_u64(1, 16, c.params);
     ctor.set_u64(1, 24, c.fields);
-    ctor.set_u8(1, 32, if c.is_unsafe { 1 } else { 0 });
+    ctor.set_bool(1, 32, c.is_unsafe);
     Self::new(ctor.into())
   }
 }
@@ -308,9 +308,9 @@ impl LeanIxonInductive<LeanOwned> {
     ctor.set_u64(2, 8, ind.params);
     ctor.set_u64(2, 16, ind.indices);
     ctor.set_u64(2, 24, ind.nested);
-    ctor.set_u8(2, 32, if ind.recr { 1 } else { 0 });
-    ctor.set_u8(2, 33, if ind.refl { 1 } else { 0 });
-    ctor.set_u8(2, 34, if ind.is_unsafe { 1 } else { 0 });
+    ctor.set_bool(2, 32, ind.recr);
+    ctor.set_bool(2, 33, ind.refl);
+    ctor.set_bool(2, 34, ind.is_unsafe);
     Self::new(ctor.into())
   }
 }

src/ffi/ixon/constant.rs

@@ -109,7 +109,7 @@ impl LeanIxonExpr<LeanOwned> {
         ctor.set(0, ty_obj);
         ctor.set(1, val_obj);
         ctor.set(2, body_obj);
-        ctor.set_u8(3, 0, if *non_dep { 1 } else { 0 });
+        ctor.set_bool(3, 0, *non_dep);
         ctor.into()
       },
       IxonExpr::Share(idx) => {

src/ffi/ixon/expr.rs

@@ -101,7 +101,7 @@ impl LeanIxonDataValue<LeanOwned> {
       },
       IxonDataValue::OfBool(b) => {
         let ctor = LeanCtor::alloc(1, 0, 1);
-        ctor.set_u8(0, 0, if *b { 1 } else { 0 });
+        ctor.set_bool(0, 0, *b);
         ctor.into()
       },
       IxonDataValue::OfName(addr) => {

src/ffi/ixon/meta.rs

@@ -1,42 +1,48 @@
-use std::sync::OnceLock;
+use std::sync::LazyLock;
 
 use tiny_keccak::{Hasher, Keccak};
 
 use lean_ffi::object::{
   ExternalClass, LeanBorrowed, LeanByteArray, LeanExternal, LeanOwned,
 };
 
-static KECCAK_CLASS: OnceLock<ExternalClass> = OnceLock::new();
-
-fn keccak_class() -> &'static ExternalClass {
-  KECCAK_CLASS.get_or_init(ExternalClass::register_with_drop::<Keccak>)
-}
+static KECCAK_CLASS: LazyLock<ExternalClass> =
+  LazyLock::new(ExternalClass::register_with_drop::<Keccak>);
 
 /// `Keccak.Hasher.init : Unit → Hasher`
 #[unsafe(no_mangle)]
 extern "C" fn rs_keccak256_hasher_init(
   _unit: LeanOwned,
 ) -> LeanExternal<Keccak, LeanOwned> {
-  LeanExternal::alloc(keccak_class(), Keccak::v256())
+  LeanExternal::alloc(&KECCAK_CLASS, Keccak::v256())
 }
 
 /// `Keccak.Hasher.update : (hasher: Hasher) → (input: @& ByteArray) → Hasher`
 #[unsafe(no_mangle)]
 extern "C" fn rs_keccak256_hasher_update(
-  hasher: LeanExternal<Keccak, LeanOwned>,
+  mut hasher: LeanExternal<Keccak, LeanOwned>,
   input: LeanByteArray<LeanBorrowed<'_>>,
 ) -> LeanExternal<Keccak, LeanOwned> {
-  let mut new_hasher = hasher.get().clone();
-  new_hasher.update(input.as_bytes());
-  LeanExternal::alloc(keccak_class(), new_hasher)
+  if let Some(h) = hasher.get_mut() {
+    h.update(input.as_bytes());
+    hasher
+  } else {
+    let mut new_hasher = hasher.get().clone();
+    new_hasher.update(input.as_bytes());
+    LeanExternal::alloc(&KECCAK_CLASS, new_hasher)
+  }
 }
 
 /// `Keccak.Hasher.finalize : (hasher: Hasher) → ByteArray`
 #[unsafe(no_mangle)]
 extern "C" fn rs_keccak256_hasher_finalize(
-  hasher: LeanExternal<Keccak, LeanOwned>,
+  mut hasher: LeanExternal<Keccak, LeanOwned>,
 ) -> LeanByteArray<LeanOwned> {
   let mut data = [0u8; 32];
-  hasher.get().clone().finalize(&mut data);
+  if let Some(h) = hasher.get_mut() {
+    std::mem::replace(h, Keccak::v256()).finalize(&mut data);
+  } else {
+    hasher.get().clone().finalize(&mut data);
+  }
   LeanByteArray::from_bytes(&data)
 }