feat(spl): support Rent data_len (#873)

Author: Stevengre

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

@@ -278,6 +278,46 @@ module KMIR-SPL-TOKEN
        )
        => dynamicSize(82)
        [priority(30)]
+
+  // Rent data (&mut [u8]) length hints (Rent::LEN)
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(Integer(_, 64, false))    // lamports_per_byte_year
+             ListItem(Float(2.0, 64))           // exemption_threshold
+             ListItem(Integer(_, 8, false))     // burn_percent
+           )
+         )
+       )
+       => dynamicSize(17)
+       [priority(30)]
+
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBorrow(_, SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(Integer(_, 64, false))
+             ListItem(Float(2.0, 64))
+             ListItem(Integer(_, 8, false))
+           )
+         ))
+       )
+       => dynamicSize(17)
+       [priority(30)]
+
+  rule #maybeDynamicSize(
+         dynamicSize(_),
+         SPLDataBorrowMut(_, SPLDataBuffer(
+           Aggregate(variantIdx(0),
+             ListItem(Integer(_, 64, false))
+             ListItem(Float(2.0, 64))
+             ListItem(Integer(_, 8, false))
+           )
+         ))
+       )
+       => dynamicSize(17)
+       [priority(30)]
 ```
 
 ## Cheatcode handling

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

@@ -225,6 +225,7 @@ fn test_spl_rent_domain_data(rent: &AccountInfo<'_>) {
     assert!(sysrent.burn_percent > 100 || (sys_burnt <= rent_collected && sys_distributed <= rent_collected));
 
     cheatcode_is_spl_rent(rent);
+    assert_eq!(rent.data_len(), Rent::LEN);
     let prent = Rent::from_account_info(rent).unwrap_or(sysrent);
     let (acct_burnt, acct_distributed) = prent.calculate_burn(rent_collected);
     assert!(prent.burn_percent > 100 || (acct_burnt <= rent_collected && acct_distributed <= rent_collected));