feat(spl): data_len for AccountInfo's data (#868)

- solve  runtimeverification/solana-token#113

Author: Stevengre

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

@@ -169,6 +169,110 @@ module KMIR-SPL-TOKEN
   rule #isSPLRentGetFunc("solana_sysvar::rent::<impl Sysvar for solana_rent::Rent>::get") => true
 ```
 
+## Slice metadata for SPL account buffers
+
+```k
+  // Account data (&mut [u8]) length hints (Account::LEN)
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))          // mint
+             ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))          // owner
+             ListItem(Integer(_, 64, false))                                // amount
+             ListItem(_DELEG)                                               // delegate COption
+             ListItem(Integer(_, 8, false))                                 // state
+             ListItem(_IS_NATIVE)                                           // is_native COption
+             ListItem(Integer(_, 64, false))                                // delegated_amount
+             ListItem(_CLOSE)                                               // close_authority COption
+           )
+         )
+       )
+       => dynamicSize(165)
+       [priority(30)]
+
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBorrow(_, SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
+             ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
+             ListItem(Integer(_, 64, false))
+             ListItem(_DELEG)
+             ListItem(Integer(_, 8, false))
+             ListItem(_IS_NATIVE)
+             ListItem(Integer(_, 64, false))
+             ListItem(_CLOSE)
+           )
+         ))
+       )
+       => dynamicSize(165)
+       [priority(30)]
+
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBorrowMut(_, SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
+             ListItem(Aggregate(variantIdx(0), ListItem(Range(_))))
+             ListItem(Integer(_, 64, false))
+             ListItem(_DELEG)
+             ListItem(Integer(_, 8, false))
+             ListItem(_IS_NATIVE)
+             ListItem(Integer(_, 64, false))
+             ListItem(_CLOSE)
+           )
+         ))
+       )
+       => dynamicSize(165)
+       [priority(30)]
+
+  // Mint data (&mut [u8]) length hints (Mint::LEN)
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(_AUTH)                    // mint_authority COption
+             ListItem(Integer(_, 64, false))    // supply
+             ListItem(Integer(_, 8, false))     // decimals
+             ListItem(BoolVal(_))               // is_initialized
+             ListItem(_FREEZE)                  // freeze_authority COption
+           )
+         )
+       )
+       => dynamicSize(82)
+       [priority(30)]
+
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBorrow(_, SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(_AUTH)
+             ListItem(Integer(_, 64, false))
+             ListItem(Integer(_, 8, false))
+             ListItem(BoolVal(_))
+             ListItem(_FREEZE)
+           )
+         ))
+       )
+       => dynamicSize(82)
+       [priority(30)]
+
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBorrowMut(_, SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(_AUTH)
+             ListItem(Integer(_, 64, false))
+             ListItem(Integer(_, 8, false))
+             ListItem(BoolVal(_))
+             ListItem(_FREEZE)
+           )
+         ))
+       )
+       => dynamicSize(82)
+       [priority(30)]
+```
 
 ## Cheatcode handling
 ```{.k .symbolic}

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

@@ -119,6 +119,10 @@ impl<'a> AccountInfo<'a> {
             executable,
         }
     }
+
+    fn data_len(&self) -> usize {
+        self.data.borrow().len()
+    }
 }
 
 fn test_spltoken_domain_data(
@@ -162,6 +166,8 @@ fn test_spl_account_domain_data(acc: &AccountInfo<'_>) {
 fn test_spl_mint_domain_data(mint: &AccountInfo<'_>) {
     cheatcode_is_spl_mint(mint);
 
+    assert_eq!(mint.data_len(), Mint::LEN);
+
     let mut mint_state = get_mint(mint);
     assert!(!mint_state.is_initialized);
     mint_state.is_initialized = true;