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..3d61da075 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -107,6 +107,39 @@ module KMIR-SPL-TOKEN syntax Bool ::= #isSplPubkey ( List ) [function, total] rule #isSplPubkey(KEY) => size(KEY) ==Int 32 andBool allBytes(KEY) + // Construct a 32-byte pubkey List from individual Int variables. + // When used with existential variables (?Var:Int), this produces a concrete List structure + // that ==K can decompose element-wise, avoiding opaque symbolic List equality in SMT. + syntax List ::= #mkSplPubkey ( + Int , Int , Int , Int , Int , Int , Int , Int , + Int , Int , Int , Int , Int , Int , Int , Int , + Int , Int , Int , Int , Int , Int , Int , Int , + Int , Int , Int , Int , Int , Int , Int , Int ) [macro] + rule #mkSplPubkey( + B0, B1, B2, B3, B4, B5, B6, B7, + B8, B9, B10, B11, B12, B13, B14, B15, + B16, B17, B18, B19, B20, B21, B22, B23, + B24, B25, B26, B27, B28, B29, B30, B31 ) => + ListItem(Integer(B0, 8, false)) ListItem(Integer(B1, 8, false)) + ListItem(Integer(B2, 8, false)) ListItem(Integer(B3, 8, false)) + ListItem(Integer(B4, 8, false)) ListItem(Integer(B5, 8, false)) + ListItem(Integer(B6, 8, false)) ListItem(Integer(B7, 8, false)) + ListItem(Integer(B8, 8, false)) ListItem(Integer(B9, 8, false)) + ListItem(Integer(B10, 8, false)) ListItem(Integer(B11, 8, false)) + ListItem(Integer(B12, 8, false)) ListItem(Integer(B13, 8, false)) + ListItem(Integer(B14, 8, false)) ListItem(Integer(B15, 8, false)) + ListItem(Integer(B16, 8, false)) ListItem(Integer(B17, 8, false)) + ListItem(Integer(B18, 8, false)) ListItem(Integer(B19, 8, false)) + ListItem(Integer(B20, 8, false)) ListItem(Integer(B21, 8, false)) + ListItem(Integer(B22, 8, false)) ListItem(Integer(B23, 8, false)) + ListItem(Integer(B24, 8, false)) ListItem(Integer(B25, 8, false)) + ListItem(Integer(B26, 8, false)) ListItem(Integer(B27, 8, false)) + ListItem(Integer(B28, 8, false)) ListItem(Integer(B29, 8, false)) + ListItem(Integer(B30, 8, false)) ListItem(Integer(B31, 8, false)) + + syntax Bool ::= #isByte ( Int ) [macro] + rule #isByte(X) => 0 <=Int X andBool X 0 <=Int N andBool N <=Int 2 @@ -435,6 +468,10 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami andBool 0 <=Int ?SplRentBurnPercent andBool ?SplRentBurnPercent <=Int 100 [priority(30), preserves-definedness] + // Multisig cheatcode: decompose signer pubkeys into individual byte variables. + // Each ?SplSiNBj:Int is a single byte (0..255), giving 32 concrete ListItems per signer. + // This allows ==K on pubkey Lists to decompose into integer equalities (fast for SMT), + // instead of opaque symbolic List equality (causes Z3 timeout at scale). rule [cheatcode-is-spl-multisig]: #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT => #forceSetPlaceValue( @@ -445,9 +482,33 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami ListItem(Integer(?SplMultisigN:Int, 8, false)) // n: u8 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)))) - ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplSigner2:List)))) + ListItem(Aggregate(variantIdx(0), ListItem(Range(#mkSplPubkey( + ?SplSi0B0:Int, ?SplSi0B1:Int, ?SplSi0B2:Int, ?SplSi0B3:Int, + ?SplSi0B4:Int, ?SplSi0B5:Int, ?SplSi0B6:Int, ?SplSi0B7:Int, + ?SplSi0B8:Int, ?SplSi0B9:Int, ?SplSi0B10:Int, ?SplSi0B11:Int, + ?SplSi0B12:Int, ?SplSi0B13:Int, ?SplSi0B14:Int, ?SplSi0B15:Int, + ?SplSi0B16:Int, ?SplSi0B17:Int, ?SplSi0B18:Int, ?SplSi0B19:Int, + ?SplSi0B20:Int, ?SplSi0B21:Int, ?SplSi0B22:Int, ?SplSi0B23:Int, + ?SplSi0B24:Int, ?SplSi0B25:Int, ?SplSi0B26:Int, ?SplSi0B27:Int, + ?SplSi0B28:Int, ?SplSi0B29:Int, ?SplSi0B30:Int, ?SplSi0B31:Int))))) + ListItem(Aggregate(variantIdx(0), ListItem(Range(#mkSplPubkey( + ?SplSi1B0:Int, ?SplSi1B1:Int, ?SplSi1B2:Int, ?SplSi1B3:Int, + ?SplSi1B4:Int, ?SplSi1B5:Int, ?SplSi1B6:Int, ?SplSi1B7:Int, + ?SplSi1B8:Int, ?SplSi1B9:Int, ?SplSi1B10:Int, ?SplSi1B11:Int, + ?SplSi1B12:Int, ?SplSi1B13:Int, ?SplSi1B14:Int, ?SplSi1B15:Int, + ?SplSi1B16:Int, ?SplSi1B17:Int, ?SplSi1B18:Int, ?SplSi1B19:Int, + ?SplSi1B20:Int, ?SplSi1B21:Int, ?SplSi1B22:Int, ?SplSi1B23:Int, + ?SplSi1B24:Int, ?SplSi1B25:Int, ?SplSi1B26:Int, ?SplSi1B27:Int, + ?SplSi1B28:Int, ?SplSi1B29:Int, ?SplSi1B30:Int, ?SplSi1B31:Int))))) + ListItem(Aggregate(variantIdx(0), ListItem(Range(#mkSplPubkey( + ?SplSi2B0:Int, ?SplSi2B1:Int, ?SplSi2B2:Int, ?SplSi2B3:Int, + ?SplSi2B4:Int, ?SplSi2B5:Int, ?SplSi2B6:Int, ?SplSi2B7:Int, + ?SplSi2B8:Int, ?SplSi2B9:Int, ?SplSi2B10:Int, ?SplSi2B11:Int, + ?SplSi2B12:Int, ?SplSi2B13:Int, ?SplSi2B14:Int, ?SplSi2B15:Int, + ?SplSi2B16:Int, ?SplSi2B17:Int, ?SplSi2B18:Int, ?SplSi2B19:Int, + ?SplSi2B20:Int, ?SplSi2B21:Int, ?SplSi2B22:Int, ?SplSi2B23:Int, + ?SplSi2B24:Int, ?SplSi2B25:Int, ?SplSi2B26:Int, ?SplSi2B27:Int, + ?SplSi2B28:Int, ?SplSi2B29:Int, ?SplSi2B30:Int, ?SplSi2B31:Int))))) )) ) ) @@ -460,11 +521,34 @@ 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