From b7291282ff399afb91c683bd6ee884f0f7edd02e Mon Sep 17 00:00:00 2001 From: mariaKt Date: Thu, 26 Feb 2026 15:35:24 -0600 Subject: [PATCH] Change the number of signers from 11 to 3 --- .../kdist/mir-semantics/symbolic/p-token.md | 38 ++++--------------- 1 file changed, 7 insertions(+), 31 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md index 302705c12..a495b8b4f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md @@ -125,12 +125,12 @@ This ensures that branches on the key value are not duplicated. ```k - syntax Signers ::= Signers ( List ) // 11 Pubkeys, each List of 32 bytes + syntax Signers ::= Signers ( List ) // 3 Pubkeys, each List of 32 bytes | SignersError ( Value ) syntax Signers ::= toSigners ( Value ) [function, total] // ----------------------------------------------------- - rule toSigners(Range(ELEMS)) => Signers( toKeys(ELEMS) ) requires size(ELEMS) ==Int 11 andBool allRangeWrappedKeys(ELEMS) + rule toSigners(Range(ELEMS)) => Signers( toKeys(ELEMS) ) requires size(ELEMS) ==Int 3 andBool allRangeWrappedKeys(ELEMS) rule toSigners(VAL) => SignersError(VAL) [owise] syntax Value ::= fromSigners ( Signers ) [function, total] @@ -341,7 +341,7 @@ This ensures that branches on the key value are not duplicated. ### SPL Token Interface Multisig ```k - // Multisig struct: number of required signers, number of valid signers, initialised flag, array of 11 signers + // Multisig struct: number of required signers, number of valid signers, initialised flag, array of 3 signers syntax IMulti ::= IMulti ( U8 , U8 , U8 , Signers ) | IMultiError ( Value ) @@ -668,14 +668,6 @@ An `AccountInfo` reference is passed to the function. Signers( ListItem(Key(?Signer0)) ListItem(Key(?Signer1)) ListItem(Key(?Signer2)) - ListItem(Key(?Signer3)) - ListItem(Key(?Signer4)) - ListItem(Key(?Signer5)) - ListItem(Key(?Signer6)) - ListItem(Key(?Signer7)) - ListItem(Key(?Signer8)) - ListItem(Key(?Signer9)) - ListItem(Key(?Signer10)) ) ) ) @@ -685,15 +677,7 @@ An `AccountInfo` reference is passed to the function. andBool size(?Signer0) ==Int 32 andBool allBytes(?Signer0) andBool size(?Signer1) ==Int 32 andBool allBytes(?Signer1) andBool size(?Signer2) ==Int 32 andBool allBytes(?Signer2) - andBool size(?Signer3) ==Int 32 andBool allBytes(?Signer3) - andBool size(?Signer4) ==Int 32 andBool allBytes(?Signer4) - andBool size(?Signer5) ==Int 32 andBool allBytes(?Signer5) - andBool size(?Signer6) ==Int 32 andBool allBytes(?Signer6) - andBool size(?Signer7) ==Int 32 andBool allBytes(?Signer7) - andBool size(?Signer8) ==Int 32 andBool allBytes(?Signer8) - andBool size(?Signer9) ==Int 32 andBool allBytes(?Signer9) - andBool size(?Signer10) ==Int 32 andBool allBytes(?Signer10) - andBool DATA_LEN ==Int 355 // size_of(Multisig), see pinocchio_token_interface::state::Transmutable instance + andBool DATA_LEN ==Int 99 // size_of(Multisig), see pinocchio_token_interface::state::Transmutable instance ``` ```{.k .concrete} @@ -701,7 +685,7 @@ An `AccountInfo` reference is passed to the function. // Signers and n. It needs work to create sensible cases. rule #addMultisig(Aggregate(variantIdx(0), _) #as P_ACC) => PAccountMultisig( - #toPAccWithDataLen(P_ACC, 355), // size_of(Multisig), see pinocchio_token_interface::state::Transmutable instance + #toPAccWithDataLen(P_ACC, 99), // size_of(Multisig), see pinocchio_token_interface::state::Transmutable instance IMulti(U8(#randU8()), // m (number of signers required) U8(#randU8()), // n (number of valid signers) U8(#randU8()), // initialized (0 - false, 1 - true, error state owise) @@ -825,10 +809,10 @@ this field is expected to be constrained accordingly in the path condition. requires DATA_LEN ==Int 82 // IMint length rule #mkPAccByteRefLen(DEST, OFFSET, PLACE, MUT, PAccountMultisig(PAcc(_, _, _, _, _, _, _, _, U64(DATA_LEN)), _)) - => #setLocalValue(DEST, PAccByteRef(OFFSET, PLACE, MUT, 355)) + => #setLocalValue(DEST, PAccByteRef(OFFSET, PLACE, MUT, 99)) ... - requires DATA_LEN ==Int 355 // IMulti length + requires DATA_LEN ==Int 99 // IMulti length rule #mkPAccByteRefLen(DEST, OFFSET, PLACE, MUT, PAccountRent(PAcc(_, _, _, _, _, _, _, _, U64(DATA_LEN)), _)) => #setLocalValue(DEST, PAccByteRef(OFFSET, PLACE, MUT, 17)) ... @@ -1186,14 +1170,6 @@ NB The projection rule must have higher priority than the one which auto-project syntax Signers ::= #randSigners() [function, total, impure, symbol(randSigners)] rule #randSigners() => Signers(ListItem(#randKey()) - ListItem(#randKey()) - ListItem(#randKey()) - ListItem(#randKey()) - ListItem(#randKey()) - ListItem(#randKey()) - ListItem(#randKey()) - ListItem(#randKey()) - ListItem(#randKey()) ListItem(#randKey()) ListItem(#randKey())) ```