From c3e1a2ca46c40ad86d693fa1559ca82edf93e6d2 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Mon, 16 Mar 2026 02:21:06 +0000
Subject: [PATCH 1/9] Ignore .codex workspace files

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index 70487d22..32102142 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,3 +7,4 @@
 node_modules
 test-ledger
 dist
+/.codex/

From 1b54c2925a7b5296d4ce9bf12db30418525ed301 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Tue, 17 Mar 2026 10:38:23 +0000
Subject: [PATCH 2/9] fix(specs): add multisig bounds assumptions and fix
 signers_count range

Add `1 <= m <= MAX_SIGNERS` and `1 <= n <= MAX_SIGNERS` assumptions to
thaw_account_multisig and freeze_account_multisig specs. These match the
invariants enforced by `initialize_multisig` and eliminate stuck leaves
from unreachable symbolic states (N==0 and N>MAX_SIGNERS).

Fix spec bug in `inner_test_validate_owner`: `signers_count` was
iterating over all `multisig.signers` slots instead of only
`signers[0..n]`, diverging from the implementation
(`processor.rs:1006`) which uses `multisig.signers[0..multisig.n as
usize]`. When m > n, the spec counted extra uninitialized slots as
valid matches, inflating the count and incorrectly expecting Ok(())
while the implementation returned MissingRequiredSignature.

Closes #181

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 specs/shared/inner_test_validate_owner.rs            |  4 ++--
 specs/shared/test_process_freeze_account_multisig.rs | 11 +++++++++++
 specs/shared/test_process_thaw_account_multisig.rs   | 11 +++++++++++
 3 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/specs/shared/inner_test_validate_owner.rs b/specs/shared/inner_test_validate_owner.rs
index 2abd0abd..2c0a8d4b 100644
--- a/specs/shared/inner_test_validate_owner.rs
+++ b/specs/shared/inner_test_validate_owner.rs
@@ -35,7 +35,7 @@ fn expected_validate_owner_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| {
@@ -103,7 +103,7 @@ fn inner_test_validate_owner(
             }
 
             // 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| {
diff --git a/specs/shared/test_process_freeze_account_multisig.rs b/specs/shared/test_process_freeze_account_multisig.rs
index c583f9de..c8ceb884 100644
--- a/specs/shared/test_process_freeze_account_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);
diff --git a/specs/shared/test_process_thaw_account_multisig.rs b/specs/shared/test_process_thaw_account_multisig.rs
index 5abbd200..2f6fd8d6 100644
--- a/specs/shared/test_process_thaw_account_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);

From 55399b0b12916086ad68ddac5ae6ff0191124406 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Tue, 17 Mar 2026 10:49:51 +0000
Subject: [PATCH 3/9] fix(specs): add multisig m/n bounds assumptions to all
 multisig specs

Add `1 <= m <= MAX_SIGNERS` and `1 <= n <= MAX_SIGNERS` assumptions to
all remaining multisig specs that use cheatcode_multisig. These match
the invariants enforced by `initialize_multisig` and prevent the prover
from exploring unreachable symbolic states.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 specs/shared/test_process_approve_checked_multisig.rs | 11 +++++++++++
 specs/shared/test_process_approve_multisig.rs         | 11 +++++++++++
 specs/shared/test_process_burn_checked_multisig.rs    | 11 +++++++++++
 specs/shared/test_process_burn_multisig.rs            | 11 +++++++++++
 specs/shared/test_process_close_account_multisig.rs   | 11 +++++++++++
 specs/shared/test_process_mint_to_checked_multisig.rs | 11 +++++++++++
 specs/shared/test_process_mint_to_multisig.rs         | 11 +++++++++++
 specs/shared/test_process_revoke_multisig.rs          | 11 +++++++++++
 .../test_process_set_authority_account_multisig.rs    | 11 +++++++++++
 .../test_process_set_authority_mint_multisig.rs       | 11 +++++++++++
 .../shared/test_process_transfer_checked_multisig.rs  | 11 +++++++++++
 specs/shared/test_process_transfer_multisig.rs        | 11 +++++++++++
 specs/shared/test_validate_owner_multisig.rs          | 11 +++++++++++
 13 files changed, 143 insertions(+)

diff --git a/specs/shared/test_process_approve_checked_multisig.rs b/specs/shared/test_process_approve_checked_multisig.rs
index 29737f6a..9131df90 100644
--- a/specs/shared/test_process_approve_checked_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let amount = u64::from_le_bytes([
diff --git a/specs/shared/test_process_approve_multisig.rs b/specs/shared/test_process_approve_multisig.rs
index 87d1c6d4..dc20384b 100644
--- a/specs/shared/test_process_approve_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            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])) };
diff --git a/specs/shared/test_process_burn_checked_multisig.rs b/specs/shared/test_process_burn_checked_multisig.rs
index 38515d8c..85f30ee0 100644
--- a/specs/shared/test_process_burn_checked_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);
diff --git a/specs/shared/test_process_burn_multisig.rs b/specs/shared/test_process_burn_multisig.rs
index c45b7f7a..ba41e4cf 100644
--- a/specs/shared/test_process_burn_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let mint_old = get_mint(&accounts[1]);
diff --git a/specs/shared/test_process_close_account_multisig.rs b/specs/shared/test_process_close_account_multisig.rs
index e9c45093..9eaed629 100644
--- a/specs/shared/test_process_close_account_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();
diff --git a/specs/shared/test_process_mint_to_checked_multisig.rs b/specs/shared/test_process_mint_to_checked_multisig.rs
index 4cb006c3..f942ec08 100644
--- a/specs/shared/test_process_mint_to_checked_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let dst_old = get_account(&accounts[1]);
diff --git a/specs/shared/test_process_mint_to_multisig.rs b/specs/shared/test_process_mint_to_multisig.rs
index 35859a59..30298125 100644
--- a/specs/shared/test_process_mint_to_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let dst_old = get_account(&accounts[1]);
diff --git a/specs/shared/test_process_revoke_multisig.rs b/specs/shared/test_process_revoke_multisig.rs
index 1f30ad69..d7c48f8d 100644
--- a/specs/shared/test_process_revoke_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();
diff --git a/specs/shared/test_process_set_authority_account_multisig.rs b/specs/shared/test_process_set_authority_account_multisig.rs
index e70033e3..28991dce 100644
--- a/specs/shared/test_process_set_authority_account_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_initialised = src_old.is_initialized();
diff --git a/specs/shared/test_process_set_authority_mint_multisig.rs b/specs/shared/test_process_set_authority_mint_multisig.rs
index 5fc06067..c3e9705f 100644
--- a/specs/shared/test_process_set_authority_mint_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let mint_old = get_mint(&accounts[0]);
     let mint_data_len = accounts[0].data_len();
diff --git a/specs/shared/test_process_transfer_checked_multisig.rs b/specs/shared/test_process_transfer_checked_multisig.rs
index b2a7d618..154c0228 100644
--- a/specs/shared/test_process_transfer_checked_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            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]);
diff --git a/specs/shared/test_process_transfer_multisig.rs b/specs/shared/test_process_transfer_multisig.rs
index fd916b90..10e92158 100644
--- a/specs/shared/test_process_transfer_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            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]);
diff --git a/specs/shared/test_validate_owner_multisig.rs b/specs/shared/test_validate_owner_multisig.rs
index 0526d482..1593437b 100644
--- a/specs/shared/test_validate_owner_multisig.rs
+++ b/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 as u8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let expected_owner = src_old.owner;

From 2cf3a176d5528077b76348371a3927eb1a28853c Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Tue, 17 Mar 2026 12:58:31 +0000
Subject: [PATCH 4/9] fix(specs): remove unnecessary `as u8` cast on
 MAX_SIGNERS

MAX_SIGNERS is already u8, so `as u8` triggers clippy::unnecessary_cast
which fails CI lint with --deny=warnings.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 specs/shared/test_process_approve_checked_multisig.rs       | 4 ++--
 specs/shared/test_process_approve_multisig.rs               | 4 ++--
 specs/shared/test_process_burn_checked_multisig.rs          | 4 ++--
 specs/shared/test_process_burn_multisig.rs                  | 4 ++--
 specs/shared/test_process_close_account_multisig.rs         | 4 ++--
 specs/shared/test_process_freeze_account_multisig.rs        | 4 ++--
 specs/shared/test_process_mint_to_checked_multisig.rs       | 4 ++--
 specs/shared/test_process_mint_to_multisig.rs               | 4 ++--
 specs/shared/test_process_revoke_multisig.rs                | 4 ++--
 specs/shared/test_process_set_authority_account_multisig.rs | 4 ++--
 specs/shared/test_process_set_authority_mint_multisig.rs    | 4 ++--
 specs/shared/test_process_thaw_account_multisig.rs          | 4 ++--
 specs/shared/test_process_transfer_checked_multisig.rs      | 4 ++--
 specs/shared/test_process_transfer_multisig.rs              | 4 ++--
 specs/shared/test_validate_owner_multisig.rs                | 4 ++--
 15 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/specs/shared/test_process_approve_checked_multisig.rs b/specs/shared/test_process_approve_checked_multisig.rs
index 9131df90..c9fb0759 100644
--- a/specs/shared/test_process_approve_checked_multisig.rs
+++ b/specs/shared/test_process_approve_checked_multisig.rs
@@ -17,10 +17,10 @@ fn test_process_approve_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[3]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_approve_multisig.rs b/specs/shared/test_process_approve_multisig.rs
index dc20384b..1eadcba0 100644
--- a/specs/shared/test_process_approve_multisig.rs
+++ b/specs/shared/test_process_approve_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_approve_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_burn_checked_multisig.rs b/specs/shared/test_process_burn_checked_multisig.rs
index 85f30ee0..2b6d64e9 100644
--- a/specs/shared/test_process_burn_checked_multisig.rs
+++ b/specs/shared/test_process_burn_checked_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_burn_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_burn_multisig.rs b/specs/shared/test_process_burn_multisig.rs
index ba41e4cf..318e0e62 100644
--- a/specs/shared/test_process_burn_multisig.rs
+++ b/specs/shared/test_process_burn_multisig.rs
@@ -15,10 +15,10 @@ pub fn test_process_burn_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_close_account_multisig.rs b/specs/shared/test_process_close_account_multisig.rs
index 9eaed629..e2d15acb 100644
--- a/specs/shared/test_process_close_account_multisig.rs
+++ b/specs/shared/test_process_close_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_close_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRe
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_freeze_account_multisig.rs b/specs/shared/test_process_freeze_account_multisig.rs
index c8ceb884..3374496f 100644
--- a/specs/shared/test_process_freeze_account_multisig.rs
+++ b/specs/shared/test_process_freeze_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_freeze_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramR
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_mint_to_checked_multisig.rs b/specs/shared/test_process_mint_to_checked_multisig.rs
index f942ec08..ed446d23 100644
--- a/specs/shared/test_process_mint_to_checked_multisig.rs
+++ b/specs/shared/test_process_mint_to_checked_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_mint_to_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_mint_to_multisig.rs b/specs/shared/test_process_mint_to_multisig.rs
index 30298125..50076357 100644
--- a/specs/shared/test_process_mint_to_multisig.rs
+++ b/specs/shared/test_process_mint_to_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_mint_to_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_revoke_multisig.rs b/specs/shared/test_process_revoke_multisig.rs
index d7c48f8d..352d4c52 100644
--- a/specs/shared/test_process_revoke_multisig.rs
+++ b/specs/shared/test_process_revoke_multisig.rs
@@ -9,10 +9,10 @@ fn test_process_revoke_multisig(accounts: &[AccountInfo; 3]) -> ProgramResult {
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_set_authority_account_multisig.rs b/specs/shared/test_process_set_authority_account_multisig.rs
index 28991dce..de467a73 100644
--- a/specs/shared/test_process_set_authority_account_multisig.rs
+++ b/specs/shared/test_process_set_authority_account_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_set_authority_account_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_set_authority_mint_multisig.rs b/specs/shared/test_process_set_authority_mint_multisig.rs
index c3e9705f..e85c8438 100644
--- a/specs/shared/test_process_set_authority_mint_multisig.rs
+++ b/specs/shared/test_process_set_authority_mint_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_set_authority_mint_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_thaw_account_multisig.rs b/specs/shared/test_process_thaw_account_multisig.rs
index 2f6fd8d6..ccd8103b 100644
--- a/specs/shared/test_process_thaw_account_multisig.rs
+++ b/specs/shared/test_process_thaw_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_thaw_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRes
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_transfer_checked_multisig.rs b/specs/shared/test_process_transfer_checked_multisig.rs
index 154c0228..0c3d49fa 100644
--- a/specs/shared/test_process_transfer_checked_multisig.rs
+++ b/specs/shared/test_process_transfer_checked_multisig.rs
@@ -17,10 +17,10 @@ fn test_process_transfer_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[3]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_transfer_multisig.rs b/specs/shared/test_process_transfer_multisig.rs
index 10e92158..47b94535 100644
--- a/specs/shared/test_process_transfer_multisig.rs
+++ b/specs/shared/test_process_transfer_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_transfer_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_validate_owner_multisig.rs b/specs/shared/test_validate_owner_multisig.rs
index 1593437b..a70d3377 100644
--- a/specs/shared/test_validate_owner_multisig.rs
+++ b/specs/shared/test_validate_owner_multisig.rs
@@ -11,10 +11,10 @@ fn test_validate_owner_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
             return Ok(());
         }
     }

From 34665c0a06a6fd5f958506a724809dd1cebf2667 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 00:43:09 +0000
Subject: [PATCH 5/9] fix(specs): bound unsigned multisig signer checks by n

---
 specs/shared/inner_test_validate_owner.rs | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/specs/shared/inner_test_validate_owner.rs b/specs/shared/inner_test_validate_owner.rs
index 2c0a8d4b..a4cc7fed 100644
--- a/specs/shared/inner_test_validate_owner.rs
+++ b/specs/shared/inner_test_validate_owner.rs
@@ -26,9 +26,11 @@ 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);
@@ -93,9 +95,11 @@ 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));

From 481d0f4329d0be602a6745057b91e590f0bac82e Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 00:53:16 +0000
Subject: [PATCH 6/9] docs(verification): explain multisig bounds assumptions

---
 p-token/test-properties/VERIFICATION_GUIDE.md | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/p-token/test-properties/VERIFICATION_GUIDE.md b/p-token/test-properties/VERIFICATION_GUIDE.md
index f39830bd..04bc2b0f 100644
--- a/p-token/test-properties/VERIFICATION_GUIDE.md
+++ b/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.
\ No newline at end of file
+- Results are stored in `artefacts/proof-SHA1-SHA2/` directory, where `SHA1` and `SHA2` indicate the version of `solana-token` and `mir-semantics` used.

From cb4edfba5e6a6f6e34c568ba1d6847a62079aadf Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 12:02:05 +0000
Subject: [PATCH 7/9] fix(specs): restore `as u8` cast on MAX_SIGNERS for
 spl-token compatibility

spl-token's MAX_SIGNERS is `usize` while multisig.m/n are `u8`.
The cast is necessary for spl-token builds; p-token's MAX_SIGNERS
is already `u8` so the cast is harmless there.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 specs/shared/test_process_approve_checked_multisig.rs       | 4 ++--
 specs/shared/test_process_approve_multisig.rs               | 4 ++--
 specs/shared/test_process_burn_checked_multisig.rs          | 4 ++--
 specs/shared/test_process_burn_multisig.rs                  | 4 ++--
 specs/shared/test_process_close_account_multisig.rs         | 4 ++--
 specs/shared/test_process_freeze_account_multisig.rs        | 4 ++--
 specs/shared/test_process_mint_to_checked_multisig.rs       | 4 ++--
 specs/shared/test_process_mint_to_multisig.rs               | 4 ++--
 specs/shared/test_process_revoke_multisig.rs                | 4 ++--
 specs/shared/test_process_set_authority_account_multisig.rs | 4 ++--
 specs/shared/test_process_set_authority_mint_multisig.rs    | 4 ++--
 specs/shared/test_process_thaw_account_multisig.rs          | 4 ++--
 specs/shared/test_process_transfer_checked_multisig.rs      | 4 ++--
 specs/shared/test_process_transfer_multisig.rs              | 4 ++--
 specs/shared/test_validate_owner_multisig.rs                | 4 ++--
 15 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/specs/shared/test_process_approve_checked_multisig.rs b/specs/shared/test_process_approve_checked_multisig.rs
index c9fb0759..9131df90 100644
--- a/specs/shared/test_process_approve_checked_multisig.rs
+++ b/specs/shared/test_process_approve_checked_multisig.rs
@@ -17,10 +17,10 @@ fn test_process_approve_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[3]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_approve_multisig.rs b/specs/shared/test_process_approve_multisig.rs
index 1eadcba0..dc20384b 100644
--- a/specs/shared/test_process_approve_multisig.rs
+++ b/specs/shared/test_process_approve_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_approve_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_burn_checked_multisig.rs b/specs/shared/test_process_burn_checked_multisig.rs
index 2b6d64e9..85f30ee0 100644
--- a/specs/shared/test_process_burn_checked_multisig.rs
+++ b/specs/shared/test_process_burn_checked_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_burn_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_burn_multisig.rs b/specs/shared/test_process_burn_multisig.rs
index 318e0e62..ba41e4cf 100644
--- a/specs/shared/test_process_burn_multisig.rs
+++ b/specs/shared/test_process_burn_multisig.rs
@@ -15,10 +15,10 @@ pub fn test_process_burn_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_close_account_multisig.rs b/specs/shared/test_process_close_account_multisig.rs
index e2d15acb..9eaed629 100644
--- a/specs/shared/test_process_close_account_multisig.rs
+++ b/specs/shared/test_process_close_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_close_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRe
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_freeze_account_multisig.rs b/specs/shared/test_process_freeze_account_multisig.rs
index 3374496f..c8ceb884 100644
--- a/specs/shared/test_process_freeze_account_multisig.rs
+++ b/specs/shared/test_process_freeze_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_freeze_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramR
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_mint_to_checked_multisig.rs b/specs/shared/test_process_mint_to_checked_multisig.rs
index ed446d23..f942ec08 100644
--- a/specs/shared/test_process_mint_to_checked_multisig.rs
+++ b/specs/shared/test_process_mint_to_checked_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_mint_to_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_mint_to_multisig.rs b/specs/shared/test_process_mint_to_multisig.rs
index 50076357..30298125 100644
--- a/specs/shared/test_process_mint_to_multisig.rs
+++ b/specs/shared/test_process_mint_to_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_mint_to_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_revoke_multisig.rs b/specs/shared/test_process_revoke_multisig.rs
index 352d4c52..d7c48f8d 100644
--- a/specs/shared/test_process_revoke_multisig.rs
+++ b/specs/shared/test_process_revoke_multisig.rs
@@ -9,10 +9,10 @@ fn test_process_revoke_multisig(accounts: &[AccountInfo; 3]) -> ProgramResult {
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_set_authority_account_multisig.rs b/specs/shared/test_process_set_authority_account_multisig.rs
index de467a73..28991dce 100644
--- a/specs/shared/test_process_set_authority_account_multisig.rs
+++ b/specs/shared/test_process_set_authority_account_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_set_authority_account_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_set_authority_mint_multisig.rs b/specs/shared/test_process_set_authority_mint_multisig.rs
index e85c8438..c3e9705f 100644
--- a/specs/shared/test_process_set_authority_mint_multisig.rs
+++ b/specs/shared/test_process_set_authority_mint_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_set_authority_mint_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_thaw_account_multisig.rs b/specs/shared/test_process_thaw_account_multisig.rs
index ccd8103b..2f6fd8d6 100644
--- a/specs/shared/test_process_thaw_account_multisig.rs
+++ b/specs/shared/test_process_thaw_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_thaw_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRes
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_transfer_checked_multisig.rs b/specs/shared/test_process_transfer_checked_multisig.rs
index 0c3d49fa..154c0228 100644
--- a/specs/shared/test_process_transfer_checked_multisig.rs
+++ b/specs/shared/test_process_transfer_checked_multisig.rs
@@ -17,10 +17,10 @@ fn test_process_transfer_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[3]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_transfer_multisig.rs b/specs/shared/test_process_transfer_multisig.rs
index 47b94535..10e92158 100644
--- a/specs/shared/test_process_transfer_multisig.rs
+++ b/specs/shared/test_process_transfer_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_transfer_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_validate_owner_multisig.rs b/specs/shared/test_validate_owner_multisig.rs
index a70d3377..1593437b 100644
--- a/specs/shared/test_validate_owner_multisig.rs
+++ b/specs/shared/test_validate_owner_multisig.rs
@@ -11,10 +11,10 @@ fn test_validate_owner_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
             return Ok(());
         }
     }

From 4a8cde7b4793d04a65486e191771a08beb350405 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 13:22:00 +0000
Subject: [PATCH 8/9] fix(specs): support shared multisig bounds for p-token
 and spl-token

---
 .github/workflows/proofs.yml                    | 17 ++++++++++++++++-
 specs/prelude-p-token.rs                        |  2 ++
 specs/prelude-spl-token.rs                      |  2 ++
 .../test_process_approve_checked_multisig.rs    |  4 ++--
 specs/shared/test_process_approve_multisig.rs   |  4 ++--
 .../test_process_burn_checked_multisig.rs       |  4 ++--
 specs/shared/test_process_burn_multisig.rs      |  4 ++--
 .../test_process_close_account_multisig.rs      |  4 ++--
 .../test_process_freeze_account_multisig.rs     |  4 ++--
 .../shared/test_process_initialize_multisig.rs  |  4 ++--
 .../shared/test_process_initialize_multisig2.rs |  4 ++--
 .../test_process_mint_to_checked_multisig.rs    |  4 ++--
 specs/shared/test_process_mint_to_multisig.rs   |  4 ++--
 specs/shared/test_process_revoke_multisig.rs    |  4 ++--
 ...st_process_set_authority_account_multisig.rs |  4 ++--
 .../test_process_set_authority_mint_multisig.rs |  4 ++--
 .../test_process_thaw_account_multisig.rs       |  4 ++--
 .../test_process_transfer_checked_multisig.rs   |  4 ++--
 specs/shared/test_process_transfer_multisig.rs  |  4 ++--
 specs/shared/test_validate_owner_multisig.rs    |  4 ++--
 20 files changed, 54 insertions(+), 35 deletions(-)

diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml
index 79408719..13eaadec 100644
--- a/.github/workflows/proofs.yml
+++ b/.github/workflows/proofs.yml
@@ -24,4 +24,19 @@ jobs:
         run: pnpm p-token:format
 
       - name: Lint
-        run: pnpm p-token:lint
\ No newline at end of file
+        run: pnpm p-token:lint
+
+  compile_spl_token_rv:
+    name: Compile spl-token RV
+    runs-on: ubuntu-latest
+    steps:
+      - name: Git Checkout
+        uses: actions/checkout@v4
+
+      - name: Setup Environment
+        uses: ./.github/actions/setup
+        with:
+          clippy: true
+
+      - name: Compile runtime-verification target
+        run: cargo +nightly-2025-02-16 check --manifest-path program/Cargo.toml --features runtime-verification,assumptions --lib
diff --git a/specs/prelude-p-token.rs b/specs/prelude-p-token.rs
index 7af2dd4f..81ab480c 100644
--- a/specs/prelude-p-token.rs
+++ b/specs/prelude-p-token.rs
@@ -124,6 +124,8 @@ use pinocchio_token_interface::state::account::INCINERATOR_ID;
 use pinocchio::pubkey::PUBKEY_BYTES;
 use pinocchio_token_interface::state::account_state::AccountState;
 use pinocchio_token_interface::state::multisig::MAX_SIGNERS;
+const MAX_SIGNERS_U8: u8 = MAX_SIGNERS;
+const MAX_SIGNERS_USIZE: usize = MAX_SIGNERS as usize;
 
 // =============================================================================
 // Process call macros (ordered same as includes)
diff --git a/specs/prelude-spl-token.rs b/specs/prelude-spl-token.rs
index 96a6bdf1..5bc19c45 100644
--- a/specs/prelude-spl-token.rs
+++ b/specs/prelude-spl-token.rs
@@ -272,6 +272,8 @@ use spl_token_interface::instruction::MAX_SIGNERS;
 use spl_token_interface::native_mint::ID as NATIVE_MINT_ID;
 use solana_sdk_ids::incinerator::ID as INCINERATOR_ID;
 use solana_pubkey::PUBKEY_BYTES;
+const MAX_SIGNERS_U8: u8 = MAX_SIGNERS as u8;
+const MAX_SIGNERS_USIZE: usize = MAX_SIGNERS;
 // Note: AccountState is already imported in the main file
 
 // =============================================================================
diff --git a/specs/shared/test_process_approve_checked_multisig.rs b/specs/shared/test_process_approve_checked_multisig.rs
index 9131df90..6f3b7360 100644
--- a/specs/shared/test_process_approve_checked_multisig.rs
+++ b/specs/shared/test_process_approve_checked_multisig.rs
@@ -17,10 +17,10 @@ fn test_process_approve_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[3]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_approve_multisig.rs b/specs/shared/test_process_approve_multisig.rs
index dc20384b..2805b79b 100644
--- a/specs/shared/test_process_approve_multisig.rs
+++ b/specs/shared/test_process_approve_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_approve_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_burn_checked_multisig.rs b/specs/shared/test_process_burn_checked_multisig.rs
index 85f30ee0..1fb811e2 100644
--- a/specs/shared/test_process_burn_checked_multisig.rs
+++ b/specs/shared/test_process_burn_checked_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_burn_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_burn_multisig.rs b/specs/shared/test_process_burn_multisig.rs
index ba41e4cf..0fb6e6ed 100644
--- a/specs/shared/test_process_burn_multisig.rs
+++ b/specs/shared/test_process_burn_multisig.rs
@@ -15,10 +15,10 @@ pub fn test_process_burn_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_close_account_multisig.rs b/specs/shared/test_process_close_account_multisig.rs
index 9eaed629..93739c0e 100644
--- a/specs/shared/test_process_close_account_multisig.rs
+++ b/specs/shared/test_process_close_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_close_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRe
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_freeze_account_multisig.rs b/specs/shared/test_process_freeze_account_multisig.rs
index c8ceb884..3b9f8b04 100644
--- a/specs/shared/test_process_freeze_account_multisig.rs
+++ b/specs/shared/test_process_freeze_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_freeze_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramR
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_initialize_multisig.rs b/specs/shared/test_process_initialize_multisig.rs
index 7fed23b0..c6a0435a 100644
--- a/specs/shared/test_process_initialize_multisig.rs
+++ b/specs/shared/test_process_initialize_multisig.rs
@@ -37,9 +37,9 @@ fn test_process_initialize_multisig(
         assert_eq!(result, Err(ProgramError::Custom(6)))
     } else if multisig_init_lamports < minimum_balance {
         assert_eq!(result, Err(ProgramError::Custom(0)))
-    } else if !((1..=MAX_SIGNERS as usize).contains(&(accounts.len() - 2))) {
+    } else if !((1..=MAX_SIGNERS_USIZE).contains(&(accounts.len() - 2))) {
         assert_eq!(result, Err(ProgramError::Custom(7)))
-    } else if !((1..=MAX_SIGNERS as usize).contains(&(instruction_data[0] as usize))) {
+    } else if !((1..=MAX_SIGNERS_USIZE).contains(&(instruction_data[0] as usize))) {
         assert_eq!(result, Err(ProgramError::Custom(8)))
     } else {
         let multisig_new = get_multisig(&accounts[0]);
diff --git a/specs/shared/test_process_initialize_multisig2.rs b/specs/shared/test_process_initialize_multisig2.rs
index 1da8d103..4fa5ae12 100644
--- a/specs/shared/test_process_initialize_multisig2.rs
+++ b/specs/shared/test_process_initialize_multisig2.rs
@@ -36,9 +36,9 @@ fn test_process_initialize_multisig2(
         assert_eq!(result, Err(ProgramError::Custom(6)))
     } else if multisig_init_lamports < minimum_balance {
         assert_eq!(result, Err(ProgramError::Custom(0)))
-    } else if !((1..=MAX_SIGNERS as usize).contains(&(accounts.len() - 1))) {
+    } else if !((1..=MAX_SIGNERS_USIZE).contains(&(accounts.len() - 1))) {
         assert_eq!(result, Err(ProgramError::Custom(7)))
-    } else if !((1..=MAX_SIGNERS as usize).contains(&(instruction_data[0] as usize))) {
+    } else if !((1..=MAX_SIGNERS_USIZE).contains(&(instruction_data[0] as usize))) {
         assert_eq!(result, Err(ProgramError::Custom(8)))
     } else {
         let multisig_new = get_multisig(&accounts[0]);
diff --git a/specs/shared/test_process_mint_to_checked_multisig.rs b/specs/shared/test_process_mint_to_checked_multisig.rs
index f942ec08..5f68ec50 100644
--- a/specs/shared/test_process_mint_to_checked_multisig.rs
+++ b/specs/shared/test_process_mint_to_checked_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_mint_to_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_mint_to_multisig.rs b/specs/shared/test_process_mint_to_multisig.rs
index 30298125..5e43afbc 100644
--- a/specs/shared/test_process_mint_to_multisig.rs
+++ b/specs/shared/test_process_mint_to_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_mint_to_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_revoke_multisig.rs b/specs/shared/test_process_revoke_multisig.rs
index d7c48f8d..92f37792 100644
--- a/specs/shared/test_process_revoke_multisig.rs
+++ b/specs/shared/test_process_revoke_multisig.rs
@@ -9,10 +9,10 @@ fn test_process_revoke_multisig(accounts: &[AccountInfo; 3]) -> ProgramResult {
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_set_authority_account_multisig.rs b/specs/shared/test_process_set_authority_account_multisig.rs
index 28991dce..783202af 100644
--- a/specs/shared/test_process_set_authority_account_multisig.rs
+++ b/specs/shared/test_process_set_authority_account_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_set_authority_account_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_set_authority_mint_multisig.rs b/specs/shared/test_process_set_authority_mint_multisig.rs
index c3e9705f..a667b1ee 100644
--- a/specs/shared/test_process_set_authority_mint_multisig.rs
+++ b/specs/shared/test_process_set_authority_mint_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_set_authority_mint_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_thaw_account_multisig.rs b/specs/shared/test_process_thaw_account_multisig.rs
index 2f6fd8d6..de08756e 100644
--- a/specs/shared/test_process_thaw_account_multisig.rs
+++ b/specs/shared/test_process_thaw_account_multisig.rs
@@ -11,10 +11,10 @@ fn test_process_thaw_account_multisig(accounts: &[AccountInfo; 4]) -> ProgramRes
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_transfer_checked_multisig.rs b/specs/shared/test_process_transfer_checked_multisig.rs
index 154c0228..5e626c7e 100644
--- a/specs/shared/test_process_transfer_checked_multisig.rs
+++ b/specs/shared/test_process_transfer_checked_multisig.rs
@@ -17,10 +17,10 @@ fn test_process_transfer_checked_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[3]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_process_transfer_multisig.rs b/specs/shared/test_process_transfer_multisig.rs
index 10e92158..3fc65ff1 100644
--- a/specs/shared/test_process_transfer_multisig.rs
+++ b/specs/shared/test_process_transfer_multisig.rs
@@ -15,10 +15,10 @@ fn test_process_transfer_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[2]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }
diff --git a/specs/shared/test_validate_owner_multisig.rs b/specs/shared/test_validate_owner_multisig.rs
index 1593437b..fa1a55ec 100644
--- a/specs/shared/test_validate_owner_multisig.rs
+++ b/specs/shared/test_validate_owner_multisig.rs
@@ -11,10 +11,10 @@ fn test_validate_owner_multisig(
     #[cfg(feature = "assumptions")]
     {
         let multisig = get_multisig(&accounts[1]);
-        if multisig.m < 1 || multisig.m > MAX_SIGNERS as u8 {
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
             return Ok(());
         }
-        if multisig.n < 1 || multisig.n > MAX_SIGNERS as u8 {
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
             return Ok(());
         }
     }

From d997698cbac95a6eca1f434da20342463fd2aa62 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 14:05:45 +0000
Subject: [PATCH 9/9] fix(specs): add withdraw multisig assumptions

---
 specs/prelude-spl-token.rs |  3 +++
 specs/withdraw-p-token.rs  | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 36 insertions(+)

diff --git a/specs/prelude-spl-token.rs b/specs/prelude-spl-token.rs
index 5bc19c45..f0be021a 100644
--- a/specs/prelude-spl-token.rs
+++ b/specs/prelude-spl-token.rs
@@ -272,6 +272,9 @@ use spl_token_interface::instruction::MAX_SIGNERS;
 use spl_token_interface::native_mint::ID as NATIVE_MINT_ID;
 use solana_sdk_ids::incinerator::ID as INCINERATOR_ID;
 use solana_pubkey::PUBKEY_BYTES;
+// spl-token exposes MAX_SIGNERS as usize, but shared multisig assumptions
+// compare it against on-chain m/n fields stored as u8. Narrowing is sound
+// because MAX_SIGNERS is a small protocol constant.
 const MAX_SIGNERS_U8: u8 = MAX_SIGNERS as u8;
 const MAX_SIGNERS_USIZE: usize = MAX_SIGNERS;
 // Note: AccountState is already imported in the main file
diff --git a/specs/withdraw-p-token.rs b/specs/withdraw-p-token.rs
index 4fa34b19..88b0ebde 100644
--- a/specs/withdraw-p-token.rs
+++ b/specs/withdraw-p-token.rs
@@ -87,6 +87,17 @@ fn test_process_withdraw_excess_lamports_account_multisig(
     cheatcode_is_account(&accounts[1]); // Destination
     cheatcode_is_multisig(&accounts[2]); // Authority
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_account(&accounts[0]);
     let src_data_len = accounts[0].data_len();
@@ -244,6 +255,17 @@ fn test_process_withdraw_excess_lamports_mint_multisig(
     cheatcode_is_account(&accounts[1]); // Destination
     cheatcode_is_multisig(&accounts[2]); // Authority
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_old = get_mint(&accounts[0]);
     let src_data_len = accounts[0].data_len();
@@ -388,6 +410,17 @@ fn test_process_withdraw_excess_lamports_multisig_multisig(
     cheatcode_is_account(&accounts[1]); // Destination
     cheatcode_is_multisig(&accounts[2]); // Authority
 
+    #[cfg(feature = "assumptions")]
+    {
+        let multisig = get_multisig(&accounts[2]);
+        if multisig.m < 1 || multisig.m > MAX_SIGNERS_U8 {
+            return Ok(());
+        }
+        if multisig.n < 1 || multisig.n > MAX_SIGNERS_U8 {
+            return Ok(());
+        }
+    }
+
     //-Initial State-----------------------------------------------------------
     let src_data_len = accounts[0].data_len();
     let src_init_lamports = accounts[0].lamports();