Skip to content

Commit 3f8f76e

Browse files
committed
fix(symbolic-spl): restore raw multisig m and n bounds
1 parent a421e01 commit 3f8f76e

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -460,8 +460,8 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
460460
</k>
461461
requires #functionName(FUNC) ==String "spl_token::entrypoint::cheatcode_is_spl_multisig"
462462
orBool #functionName(FUNC) ==String "cheatcode_is_spl_multisig"
463-
ensures 0 <=Int ?SplMultisigM andBool ?SplMultisigM <=Int 3
464-
andBool 0 <=Int ?SplMultisigN andBool ?SplMultisigN <=Int 3
463+
ensures 0 <=Int ?SplMultisigM andBool ?SplMultisigM <Int 256
464+
andBool 0 <=Int ?SplMultisigN andBool ?SplMultisigN <Int 256
465465
andBool #isSplPubkey(?SplSigner0)
466466
andBool #isSplPubkey(?SplSigner1)
467467
andBool #isSplPubkey(?SplSigner2)

0 commit comments

Comments
 (0)