feat(spl): provide cheatcodes for unpack_from_slice and pack_into_slice (#881)

Author: jberthold

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

@@ -16,8 +16,8 @@ embedded.
 
 ```
 cheatcode_is_spl_account(acc)
-Account::unpack_unchecked(&acc.data.borrow())
-Account::pack(a, &mut acc.data.borrow_mut())
+Account::unpack_from_slice(&acc.data.borrow())
+Account::pack_into_slice(&a, &mut acc.data.borrow_mut())
   -> #isSPLRcRefCellDerefFunc                        (rule [spl-rc-deref])
   -> #isSPLBorrowFunc                                (rule [spl-borrow-data])
   -> #isSPLRefDerefFunc                              (rule [spl-ref-deref])
@@ -148,26 +148,20 @@ module KMIR-SPL-TOKEN
   syntax Bool ::= #isSPLUnpackFunc ( String ) [function, total]
   rule #isSPLUnpackFunc(_) => false [owise]
   // spl-token account
-  rule #isSPLUnpackFunc("solana_program_pack::<spl_token_interface::state::Account as solana_program_pack::Pack>::unpack_unchecked") => true
-  rule #isSPLUnpackFunc("solana_program_pack::<spl_token_interface::state::Account as solana_program_pack::Pack>::unpack") => true
-  // mock account
-  rule #isSPLUnpackFunc("Account::unpack_unchecked") => true
+  rule #isSPLUnpackFunc("<state::Account as solana_program_pack::Pack>::unpack_from_slice") => true
+  rule #isSPLUnpackFunc("Account::unpack_from_slice") => true
   // spl-token mint
-  rule #isSPLUnpackFunc("solana_program_pack::<spl_token_interface::state::Mint as solana_program_pack::Pack>::unpack_unchecked") => true
-  rule #isSPLUnpackFunc("solana_program_pack::<spl_token_interface::state::Mint as solana_program_pack::Pack>::unpack") => true
-  // mock mint
-  rule #isSPLUnpackFunc("Mint::unpack_unchecked") => true
+  rule #isSPLUnpackFunc("<state::Mint as solana_program_pack::Pack>::unpack_from_slice") => true
+  rule #isSPLUnpackFunc("Mint::unpack_from_slice") => true
 
   syntax Bool ::= #isSPLPackFunc   ( String ) [function, total]
   rule #isSPLPackFunc(_) => false [owise]
   // spl-token account
-  rule #isSPLPackFunc("solana_program_pack::<spl_token_interface::state::Account as solana_program_pack::Pack>::pack") => true
-  // mock account
-  rule #isSPLPackFunc("Account::pack") => true
+  rule #isSPLPackFunc("<state::Account as solana_program_pack::Pack>::pack_into_slice") => true
+  rule #isSPLPackFunc("Account::pack_into_slice") => true
   // spl-token mint
-  rule #isSPLPackFunc("solana_program_pack::<spl_token_interface::state::Mint as solana_program_pack::Pack>::pack") => true
-  // mock mint
-  rule #isSPLPackFunc("Mint::pack") => true
+  rule #isSPLPackFunc("<state::Mint as solana_program_pack::Pack>::pack_into_slice") => true
+  rule #isSPLPackFunc("Mint::pack_into_slice") => true
 
   // Rent sysvar calls (includes mock harness direct calls to Rent::from_account_info / Rent::get)
   syntax Bool ::= #isSPLRentFromAccountInfoFunc ( String ) [function, total]
@@ -767,7 +761,7 @@ expose the wrapped payload directly.
     [owise]
 ```
 
-## Account::unpack / Account::pack
+## Account::unpack_from_slice / Account::pack_into_slice
 ```k
   rule [spl-account-unpack]:
     <k> #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
@@ -815,22 +809,21 @@ expose the wrapped payload directly.
 
 ```k
   rule [spl-account-pack]:
-    <k> #execTerminator(terminator(terminatorKindCall(FUNC, SRC_OP:Operand BUF_OP:Operand .Operands, DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
-      => #mkSPLAccountPack(SRC_OP, BUF_OP, DEST)
+    <k> #execTerminator(terminator(terminatorKindCall(FUNC, SRC_OP:Operand BUF_OP:Operand .Operands, _DEST, someBasicBlockIdx(TARGET), _UNWIND), _SPAN))
+      => #mkSPLAccountPack(SRC_OP, BUF_OP)
          ~> #execBlockIdx(TARGET)
     ...
     </k>
     requires #isSPLPackFunc(#functionName(lookupFunction(#tyOfCall(FUNC))))
     [priority(30), preserves-definedness]
 
-  syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation , Place ) [seqstrict(1,2)]
+  syntax KItem ::= #mkSPLAccountPack ( Evaluation , Evaluation ) [seqstrict(1,2)]
 
-  rule <k> #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_)), DEST)
+  rule <k> #mkSPLAccountPack(ACCOUNT, SPLDataBorrowMut(PLACE, SPLDataBuffer(_)))
         => #forceSetPlaceValue(
              PLACE,
              SPLRefCell(PLACE, SPLDataBuffer(ACCOUNT))
            )
-         ~> #setLocalValue(DEST, Aggregate(variantIdx(0), ListItem(Aggregate(variantIdx(0), .List))))
         ...
        </k>
 ```

…n/data/prove-rs/spl_token_domain_data.rs …gration/data/rs/spl_token_domain_data.rskmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs renamed to kmir/src/tests/integration/data/rs/spl_token_domain_data.rs kmir/src/tests/integration/data/prove-rs/spl_token_domain_data.rs renamed to kmir/src/tests/integration/data/rs/spl_token_domain_data.rs

@@ -318,7 +318,7 @@ impl Account {
         matches!(self.is_native, COption::Some(_))
     }
 
-    fn unpack_unchecked(data: &[u8]) -> Result<Self, ProgramError> {
+    fn unpack_from_slice(data: &[u8]) -> Result<Self, ProgramError> {
         if data.len() < Self::LEN {
             return Err(ProgramError::InvalidAccountData);
         }
@@ -348,18 +348,26 @@ impl Account {
         })
     }
 
+    fn unpack_unchecked(data: &[u8]) -> Result<Self, ProgramError> {
+        Self::unpack_from_slice(data)
+    }
+
+    fn pack_into_slice(self, dst: &mut [u8]) {
+        dst[0..32].copy_from_slice(self.mint.as_ref());
+        dst[32..64].copy_from_slice(self.owner.as_ref());
+        dst[64..72].copy_from_slice(&self.amount.to_le_bytes());
+        encode_coption_key(&self.delegate, &mut dst[72..108]);
+        dst[108] = self.state as u8;
+        encode_coption_u64(&self.is_native, &mut dst[109..121]);
+        dst[121..129].copy_from_slice(&self.delegated_amount.to_le_bytes());
+        encode_coption_key(&self.close_authority, &mut dst[129..165]);
+    }
+
     fn pack(account: Account, dst: &mut [u8]) -> Result<(), ProgramError> {
         if dst.len() < Self::LEN {
             return Err(ProgramError::InvalidAccountData);
         }
-        dst[0..32].copy_from_slice(account.mint.as_ref());
-        dst[32..64].copy_from_slice(account.owner.as_ref());
-        dst[64..72].copy_from_slice(&account.amount.to_le_bytes());
-        encode_coption_key(&account.delegate, &mut dst[72..108]);
-        dst[108] = account.state as u8;
-        encode_coption_u64(&account.is_native, &mut dst[109..121]);
-        dst[121..129].copy_from_slice(&account.delegated_amount.to_le_bytes());
-        encode_coption_key(&account.close_authority, &mut dst[129..165]);
+        account.pack_into_slice(dst);
         Ok(())
     }
 }
@@ -388,7 +396,7 @@ impl Default for Mint {
 impl Mint {
     const LEN: usize = 82;
 
-    fn unpack_unchecked(data: &[u8]) -> Result<Self, ProgramError> {
+    fn unpack_from_slice(data: &[u8]) -> Result<Self, ProgramError> {
         if data.len() < Self::LEN {
             return Err(ProgramError::InvalidAccountData);
         }
@@ -410,22 +418,23 @@ impl Mint {
         })
     }
 
+    fn unpack_unchecked(data: &[u8]) -> Result<Self, ProgramError> {
+        Self::unpack_from_slice(data)
+    }
+
+    fn pack_into_slice(self, dst: &mut [u8]) {
+        encode_coption_key(&self.mint_authority, &mut dst[0..36]);
+        dst[36..44].copy_from_slice(&self.supply.to_le_bytes());
+        dst[44] = self.decimals;
+        dst[45] = self.is_initialized as u8;
+        encode_coption_key(&self.freeze_authority, &mut dst[46..82]);
+    }
+
     fn pack(mint: Mint, dst: &mut [u8]) -> Result<(), ProgramError> {
         if dst.len() < Self::LEN {
             return Err(ProgramError::InvalidAccountData);
         }
-        let Mint {
-            mint_authority,
-            supply,
-            decimals,
-            is_initialized,
-            freeze_authority,
-        } = mint;
-        encode_coption_key(&mint_authority, &mut dst[0..36]);
-        dst[36..44].copy_from_slice(&supply.to_le_bytes());
-        dst[44] = decimals;
-        dst[45] = is_initialized as u8;
-        encode_coption_key(&freeze_authority, &mut dst[46..82]);
+        mint.pack_into_slice(dst);
         Ok(())
     }
 }
@@ -454,7 +463,7 @@ impl Default for Multisig {
 impl Multisig {
     const LEN: usize = 355;
 
-    fn unpack_unchecked(data: &[u8]) -> Result<Self, ProgramError> {
+    fn unpack_from_slice(data: &[u8]) -> Result<Self, ProgramError> {
         if data.len() < Self::LEN {
             return Err(ProgramError::InvalidAccountData);
         }
@@ -479,17 +488,25 @@ impl Multisig {
         })
     }
 
+    fn unpack_unchecked(data: &[u8]) -> Result<Self, ProgramError> {
+        Self::unpack_from_slice(data)
+    }
+
+    fn pack_into_slice(self, dst: &mut [u8]) {
+        dst[0] = self.m;
+        dst[1] = self.n;
+        dst[2] = self.is_initialized as u8;
+        for (i, signer) in self.signers.iter().enumerate() {
+            let start = 3 + i * 32;
+            dst[start..start + 32].copy_from_slice(signer.as_ref());
+        }
+    }
+
     fn pack(multisig: Multisig, dst: &mut [u8]) -> Result<(), ProgramError> {
         if dst.len() < Self::LEN {
             return Err(ProgramError::InvalidAccountData);
         }
-        dst[0] = multisig.m;
-        dst[1] = multisig.n;
-        dst[2] = multisig.is_initialized as u8;
-        for (i, signer) in multisig.signers.into_iter().enumerate() {
-            let start = 3 + i * 32;
-            dst[start..start + 32].copy_from_slice(signer.as_ref());
-        }
+        multisig.pack_into_slice(dst);
         Ok(())
     }
 }

kmir/src/tests/integration/test_integration.py

@@ -37,12 +37,6 @@
     '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',
-        'test_spl_account_lamports_read_then_write',
-    ],
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',