From 8ed36a974eb51c86b2be42b5760fb76fa57dc6dc Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 14:23:54 +0800 Subject: [PATCH 1/2] fix(symbolic-spl): model proof-only multisig state with 3 signers --- .../src/kmir/kdist/mir-semantics/symbolic/spl-token.md | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md index 8d9737820..a2d1f7b7a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -443,7 +443,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami Aggregate(variantIdx(0), ListItem(Integer(?SplMultisigM:Int, 8, false)) // m: u8 ListItem(Integer(?SplMultisigN:Int, 8, false)) // n: u8 - ListItem(BoolVal(?_SplMultisigInitialised:Bool)) // is_initialized: bool + ListItem(BoolVal(?SplMultisigInitialised:Bool)) // is_initialized: bool ListItem(Range( // signers: [Pubkey; 3] ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner0:List)))) ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner1:List)))) @@ -460,8 +460,12 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami requires #functionName(FUNC) ==String "spl_token::entrypoint::cheatcode_is_spl_multisig" orBool #functionName(FUNC) ==String "cheatcode_is_spl_multisig" - ensures 0 <=Int ?SplMultisigM andBool ?SplMultisigM Date: Fri, 6 Mar 2026 14:24:38 +0800 Subject: [PATCH 2/2] fix(symbolic-spl): discharge AccountState discriminant branches --- .../kdist/mir-semantics/lemmas/kmir-lemmas.md | 4 + .../kdist/mir-semantics/symbolic/spl-token.md | 3 + .../spl-accountstate-discriminant-branch.rs | 116 ++++++++++++++++++ .../src/tests/integration/test_integration.py | 1 + 4 files changed, 124 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/spl-accountstate-discriminant-branch.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md index 525e311a0..f4a2405c4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -94,6 +94,10 @@ For symbolic enum values, the variant index remains unevaluated but the original requires isOneOf(DISCR, DISCRS) [simplification, symbolic(DISCR)] + // Normalize enum-discriminant comparisons into the same shape emitted by branch splits. + rule #lookupDiscrAux(DISCRS, IDX) ==Int DISCR => DISCR ==Int #lookupDiscrAux(DISCRS, IDX) + [simplification] + rule 0 <=Int asInt(#findVariantIdxAux(DISCR, DISCRS, _)) => true requires isOneOf(DISCR, DISCRS) [simplification, symbolic(DISCR)] diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md index a2d1f7b7a..153dfad6a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -362,6 +362,9 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami andBool #isSplPubkey(?SplDelegateKey) andBool 0 <=Int ?SplAmount andBool ?SplAmount ; + +fn main() { + let _keep: fn(&AccountInfo<'_>) -> ProgramResult = repro; +} + +#[no_mangle] +pub fn repro(source_account_info: &AccountInfo<'_>) -> ProgramResult { + cheatcode_is_spl_account(source_account_info); + let account = get_account(source_account_info)?; + + if account.state == AccountState::Frozen { + Err(ProgramError::Custom(7)) + } else { + Ok(()) + } +} + +#[inline(never)] +fn cheatcode_is_spl_account(_: &AccountInfo<'_>) {} + +#[derive(Clone)] +struct AccountInfo<'a> { + key: &'a Pubkey, + lamports: Rc>, + data: Rc>, + owner: &'a Pubkey, + rent_epoch: u64, + is_signer: bool, + is_writable: bool, + executable: bool, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +struct Pubkey([u8; 32]); + +impl Pubkey { + fn new(bytes: [u8; 32]) -> Self { + Self(bytes) + } +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum ProgramError { + InvalidAccountData, + Custom(u32), +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum AccountState { + Uninitialized, + Initialized, + Frozen, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum COption { + None, + Some(T), +} + +#[derive(Clone, Copy, Debug)] +struct Account { + mint: Pubkey, + owner: Pubkey, + amount: u64, + delegate: COption, + state: AccountState, + is_native: COption, + delegated_amount: u64, + close_authority: COption, +} + +impl Account { + const LEN: usize = 165; + + fn unpack_from_slice(data: &[u8]) -> Result { + if data.len() < Self::LEN { + return Err(ProgramError::InvalidAccountData); + } + + let mint = Pubkey::new(data[0..32].try_into().unwrap()); + let owner = Pubkey::new(data[32..64].try_into().unwrap()); + let amount = u64::from_le_bytes(data[64..72].try_into().unwrap()); + let state = match data[108] { + 0 => AccountState::Uninitialized, + 1 => AccountState::Initialized, + 2 => AccountState::Frozen, + _ => return Err(ProgramError::InvalidAccountData), + }; + + Ok(Self { + mint, + owner, + amount, + delegate: COption::None, + state, + is_native: COption::None, + delegated_amount: 0, + close_authority: COption::None, + }) + } + + fn unpack_unchecked(data: &[u8]) -> Result { + Self::unpack_from_slice(data) + } +} + +#[inline(never)] +fn get_account(acc: &AccountInfo<'_>) -> Result { + Account::unpack_unchecked(&acc.data.borrow()) +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index d9ddc37ae..f3b093b41 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -39,6 +39,7 @@ 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], 'test_offset_from-fail': ['testing'], 'iter-eq-copied-take-dereftruncate': ['repro'], + 'spl-accountstate-discriminant-branch': ['repro'], 'spl-multisig-iter-eq-copied-next-fail': ['repro'], 'spl-multisig-signer-index': ['repro'], }