fix(specs): add multisig bounds assumptions and fix signers_count range

.gitignore

@@ -7,3 +7,4 @@
 node_modules
 test-ledger
 dist
+/.codex/

p-token/test-properties/VERIFICATION_GUIDE.md

@@ -82,6 +82,16 @@ then the `Account` fields will be equivalent. Cheatcode `maybe_same_account` wil
 Currently this cheatcode will only link symbolic state for SPL Token _Account_ (not `AccountInfo` and not P-Token),
 that would be valid under the same assumptions but has not been necessary for the current proofs.
 
+### Multisig `m`/`n` Bounds
+The `cheatcode_is_multisig` marker sets up a symbolic `Multisig` layout, but it does not by itself constrain the
+`m` and `n` fields. For harnesses that reason about multisig validation, we therefore add assumptions that
+`1 <= m <= MAX_SIGNERS` and `1 <= n <= MAX_SIGNERS`.
+
+These are not extra behavioral restrictions on the implementation. They match the invariants enforced by
+`initialize_multisig`, and they exclude symbolic states that cannot arise from a valid initialized multisig account.
+Without these bounds, the prover can explore unreachable cases such as `n == 0`, `m == 0`, or `n > MAX_SIGNERS`,
+which lead to proof artifacts rather than meaningful counterexamples.
+
 ## Limitations
 
 ### Compiling with non-solana target
@@ -170,4 +180,4 @@ cargo build --features runtime-verification
 ## Notes
 
 - Default settings: max-depth 2000, max-iterations 500, timeout 1h
-- Results are stored in `artefacts/proof-SHA1-SHA2/` directory, where `SHA1` and `SHA2` indicate the version of `solana-token` and `mir-semantics` used.
+- Results are stored in `artefacts/proof-SHA1-SHA2/` directory, where `SHA1` and `SHA2` indicate the version of `solana-token` and `mir-semantics` used.

specs/shared/inner_test_validate_owner.rs

@@ -26,16 +26,18 @@ fn expected_validate_owner_result(
 
             // Did all declared and allowd signers sign?
             let unsigned_exists = tx_signers.iter().any(|potential_signer| {
-                multisig.signers.iter().any(|registered_key| {
-                    registered_key == key!(potential_signer) && !is_signer!(potential_signer)
-                })
+                multisig.signers[0..multisig.n as usize]
+                    .iter()
+                    .any(|registered_key| {
+                        registered_key == key!(potential_signer) && !is_signer!(potential_signer)
+                    })
             });
             if unsigned_exists {
                 return Err(ProgramError::MissingRequiredSignature);
             }
 
             // Were enough signatures received?
-            let signers_count = multisig.signers
+            let signers_count = multisig.signers[0..multisig.n as usize]
                 .iter()
                 .filter_map(|registered_key| {
                     tx_signers.iter().find(|potential_signer| {
@@ -93,17 +95,19 @@ fn inner_test_validate_owner(
 
             // Did all declared and allowd signers sign?
             let unsigned_exists = tx_signers.iter().any(|potential_signer| {
-                multisig.signers.iter().any(|registered_key| {
-                    registered_key == key!(potential_signer) && !is_signer!(potential_signer)
-                })
+                multisig.signers[0..multisig.n as usize]
+                    .iter()
+                    .any(|registered_key| {
+                        registered_key == key!(potential_signer) && !is_signer!(potential_signer)
+                    })
             });
             if unsigned_exists {
                 assert_eq!(result, Err(ProgramError::MissingRequiredSignature));
                 return result;
             }
 
             // Were enough signatures received?
-            let signers_count = multisig.signers
+            let signers_count = multisig.signers[0..multisig.n as usize]
                 .iter()
                 .filter_map(|registered_key| {
                     tx_signers.iter().find(|potential_signer| {

specs/shared/test_process_approve_checked_multisig.rs

@@ -14,6 +14,17 @@ fn test_process_approve_checked_multisig(
     cheatcode_account!(&accounts[2]); // Delegate
     cheatcode_multisig!(&accounts[3]); // Owner
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[3]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let amount = u64::from_le_bytes([

specs/shared/test_process_approve_multisig.rs

@@ -12,6 +12,17 @@ fn test_process_approve_multisig(
     cheatcode_account!(&accounts[1]); // Delegate
     cheatcode_multisig!(&accounts[2]); // Owner
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let amount = unsafe { u64::from_le_bytes(*(instruction_data.as_ptr() as *const [u8; 8])) };

specs/shared/test_process_burn_checked_multisig.rs

@@ -12,6 +12,17 @@ fn test_process_burn_checked_multisig(
     cheatcode_mint!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);

specs/shared/test_process_burn_multisig.rs

@@ -12,6 +12,17 @@ pub fn test_process_burn_multisig(
     cheatcode_mint!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);

specs/shared/test_process_close_account_multisig.rs

@@ -8,6 +8,17 @@ fn test_process_close_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRe
     cheatcode_account!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();

specs/shared/test_process_freeze_account_multisig.rs

@@ -8,6 +8,17 @@ fn test_process_freeze_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramR
     cheatcode_mint!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);

specs/shared/test_process_mint_to_checked_multisig.rs

@@ -12,6 +12,17 @@ fn test_process_mint_to_checked_multisig(
     cheatcode_account!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let dst_old = get_account(&accounts[1]);

specs/shared/test_process_mint_to_multisig.rs

@@ -12,6 +12,17 @@ fn test_process_mint_to_multisig(
     cheatcode_account!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let dst_old = get_account(&accounts[1]);

specs/shared/test_process_revoke_multisig.rs

@@ -6,6 +6,17 @@ fn test_process_revoke_multisig(accounts: &[AccountInfo; 3]) -> ProgramResult {
     cheatcode_account!(&accounts[0]); // Source Account
     cheatcode_multisig!(&accounts[1]); // Owner
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[1]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();

specs/shared/test_process_set_authority_account_multisig.rs

@@ -12,6 +12,17 @@ fn test_process_set_authority_account_multisig(
     cheatcode_account!(&accounts[0]); // Assume Account
     cheatcode_multisig!(&accounts[1]); // Authority
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[1]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();

specs/shared/test_process_set_authority_mint_multisig.rs

@@ -12,6 +12,17 @@ fn test_process_set_authority_mint_multisig(
     cheatcode_mint!(&accounts[0]); // Assume Mint
     cheatcode_multisig!(&accounts[1]); // Authority
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[1]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let mint_data_len = accounts[0].data_len();

specs/shared/test_process_thaw_account_multisig.rs

@@ -8,6 +8,17 @@ fn test_process_thaw_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRes
     cheatcode_mint!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);

specs/shared/test_process_transfer_checked_multisig.rs

@@ -14,6 +14,17 @@ fn test_process_transfer_checked_multisig(
     cheatcode_account!(&accounts[2]);
     cheatcode_multisig!(&accounts[3]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[3]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     #[cfg(feature = "assumptions")]
     // Link symbolic state of dst and src if they have the same key
     cheatcode_maybe_same_account(&accounts[0], &accounts[2]);

specs/shared/test_process_transfer_multisig.rs

@@ -12,6 +12,17 @@ fn test_process_transfer_multisig(
     cheatcode_account!(&accounts[1]);
     cheatcode_multisig!(&accounts[2]);
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     #[cfg(feature = "assumptions")]
     // Link symbolic state of dst and src if they have the same key
     cheatcode_maybe_same_account(&accounts[0], &accounts[1]);

specs/shared/test_validate_owner_multisig.rs

@@ -8,6 +8,17 @@ fn test_validate_owner_multisig(
     cheatcode_account!(&accounts[0]);    // Source Account
     cheatcode_multisig!(&accounts[1]);   // Owner (multisig)
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[1]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let expected_owner = src_old.owner;