feat: support SPL Token lamports read & write (#872)

Author: Stevengre

kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md

@@ -117,20 +117,26 @@ module KMIR-SPL-TOKEN
 
   syntax Bool ::= #isSPLRcRefCellDerefFunc ( String ) [function, total]
   rule #isSPLRcRefCellDerefFunc("<std::rc::Rc<std::cell::RefCell<&mut [u8]>> as std::ops::Deref>::deref") => true
+  rule #isSPLRcRefCellDerefFunc("<std::rc::Rc<std::cell::RefCell<&mut u64>> as std::ops::Deref>::deref") => true
   rule #isSPLRcRefCellDerefFunc(_) => false [owise]
 
   syntax Bool ::= #isSPLBorrowFunc ( String ) [function, total]
   rule #isSPLBorrowFunc("std::cell::RefCell::<&mut [u8]>::borrow") => true
   rule #isSPLBorrowFunc("std::cell::RefCell::<&mut [u8]>::borrow_mut") => true
+  rule #isSPLBorrowFunc("std::cell::RefCell::<&mut u64>::borrow") => true
+  rule #isSPLBorrowFunc("std::cell::RefCell::<&mut u64>::borrow_mut") => true
   rule #isSPLBorrowFunc(_) => false [owise]
 
   syntax Bool ::= #isSPLBorrowMutFunc ( String ) [function, total]
   rule #isSPLBorrowMutFunc("std::cell::RefCell::<&mut [u8]>::borrow_mut") => true
+  rule #isSPLBorrowMutFunc("std::cell::RefCell::<&mut u64>::borrow_mut") => true
   rule #isSPLBorrowMutFunc(_) => false [owise]
 
   syntax Bool ::= #isSPLRefDerefFunc      ( String ) [function, total]
   rule #isSPLRefDerefFunc("<std::cell::Ref<'_, &mut [u8]> as std::ops::Deref>::deref") => true
   rule #isSPLRefDerefFunc("<std::cell::RefMut<'_, &mut [u8]> as std::ops::DerefMut>::deref_mut") => true
+  rule #isSPLRefDerefFunc("<std::cell::Ref<'_, &mut u64> as std::ops::Deref>::deref") => true
+  rule #isSPLRefDerefFunc("<std::cell::RefMut<'_, &mut u64> as std::ops::DerefMut>::deref_mut") => true
   rule #isSPLRefDerefFunc(_) => false [owise]
 
   syntax Bool ::= #isSPLUnpackFunc ( String ) [function, total]

kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs

@@ -63,6 +63,8 @@ fn main() {
     );
 
     test_spltoken_domain_data(&acc, &mint, &multisig, &rent);
+    // Keep lamports read/write harness reachable so stable-mir emits it.
+    test_spl_account_lamports_read_then_write(&[acc.clone()]);
 }
 
 #[derive(Clone)]
@@ -205,6 +207,16 @@ fn test_spl_multisig_domain_data(multisig: &AccountInfo<'_>) {
     assert_eq!(unpacked_multisig.signers[2], MULTISIG_SIGNER_C);
 }
 
+/// Read symbolic lamports, write a concrete value, then read again to mirror the close_account stuck case and ensure writes propagate.
+#[inline(never)]
+fn test_spl_account_lamports_read_then_write(accounts: &[AccountInfo; 1]) -> (u64, u64) {
+    cheatcode_is_spl_account(&accounts[0]);
+    let before = **accounts[0].lamports.borrow();
+    **accounts[0].lamports.borrow_mut() = 42;
+    let after = **accounts[0].lamports.borrow();
+    (before, after)
+}
+
 fn test_spl_rent_domain_data(rent: &AccountInfo<'_>) {
     // Compare rent burn semantics with the canonical sysvar value
     let sysrent = Rent::get().unwrap();

kmir/src/tests/integration/test_integration.py

@@ -37,7 +37,12 @@
     'assume-cheatcode': ['check_assume'],
     'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
     'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
-    'spl_token_domain_data': ['test_spl_account_domain_data', 'test_spl_mint_domain_data', 'test_spl_rent_domain_data'],
+    'spl_token_domain_data': [
+        'test_spl_account_domain_data',
+        'test_spl_mint_domain_data',
+        'test_spl_rent_domain_data',
+        'test_spl_account_lamports_read_then_write',
+    ],
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',