| 134 | /// verify they produce the same result. Returns 1 if equal, 0 otherwise. |
| 135 | #[unsafe(no_mangle)] |
| 136 | pub extern "C" fn rs_refcount_clone_and_compare( |
| 137 | name: LeanIxName<LeanBorrowed<'_>>, |
| 138 | ) -> LeanOwned { |
| 139 | let owned1 = LeanIxName::new(name.inner().to_owned_ref()); |
| 140 | let owned2 = owned1.clone(); |
| 141 | let decoded1 = owned1.decode(); |
| 142 | let decoded2 = owned2.decode(); |
| 143 | // owned1 and owned2 both dropped → two lean_dec calls |
| 144 | LeanNat::from_nat(&Nat::from(if decoded1 == decoded2 { 1u64 } else { 0u64 })) |
| 145 | .into() |
| 146 | } |
| 147 | |
| 148 | // ============================================================================= |
| 149 | // Roundtrip loop: stresses alloc/dealloc cycles |