Skip to content

Commit d19c66d

Browse files
mariaKtmariaKt
authored
Decompose multisig signer pubkeys for p-token (#1018)
Similar to #1000, but for p-token. I noticed the new tests for 3 signers failing to prune paths with contradictory conditions: a specific `tx_signer` `key` already has a byte-by-byte key mismatch with a registered signer key, but then due to the signer being represented as a `List` , the same comparison is re-evaluated using `?Signer0:List` (opaque) against the same `tx_signer` bytes, with `==K` being opaque.
1 parent 4aa9a35 commit d19c66d

1 file changed

Lines changed: 92 additions & 9 deletions

File tree

  • kmir/src/kmir/kdist/mir-semantics/symbolic

‎kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md‎

Lines changed: 92 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -110,6 +110,39 @@ The code uses some helper sorts for better readability.
110110
rule allBytes( ListItem(Integer(_, 8, false)) REST:List) => allBytes(REST)
111111
rule allBytes( ListItem(_OTHER) _:List) => false [owise]
112112
113+
// Construct a 32-byte pubkey List from individual Int variables.
114+
// When used with existential variables (?Var:Int), this produces a concrete List structure
115+
// that ==K can decompose element-wise, avoiding opaque symbolic List equality in SMT.
116+
syntax List ::= #mkPubkey (
117+
Int , Int , Int , Int , Int , Int , Int , Int ,
118+
Int , Int , Int , Int , Int , Int , Int , Int ,
119+
Int , Int , Int , Int , Int , Int , Int , Int ,
120+
Int , Int , Int , Int , Int , Int , Int , Int ) [macro]
121+
rule #mkPubkey(
122+
B0, B1, B2, B3, B4, B5, B6, B7,
123+
B8, B9, B10, B11, B12, B13, B14, B15,
124+
B16, B17, B18, B19, B20, B21, B22, B23,
125+
B24, B25, B26, B27, B28, B29, B30, B31 ) =>
126+
ListItem(Integer(B0, 8, false)) ListItem(Integer(B1, 8, false))
127+
ListItem(Integer(B2, 8, false)) ListItem(Integer(B3, 8, false))
128+
ListItem(Integer(B4, 8, false)) ListItem(Integer(B5, 8, false))
129+
ListItem(Integer(B6, 8, false)) ListItem(Integer(B7, 8, false))
130+
ListItem(Integer(B8, 8, false)) ListItem(Integer(B9, 8, false))
131+
ListItem(Integer(B10, 8, false)) ListItem(Integer(B11, 8, false))
132+
ListItem(Integer(B12, 8, false)) ListItem(Integer(B13, 8, false))
133+
ListItem(Integer(B14, 8, false)) ListItem(Integer(B15, 8, false))
134+
ListItem(Integer(B16, 8, false)) ListItem(Integer(B17, 8, false))
135+
ListItem(Integer(B18, 8, false)) ListItem(Integer(B19, 8, false))
136+
ListItem(Integer(B20, 8, false)) ListItem(Integer(B21, 8, false))
137+
ListItem(Integer(B22, 8, false)) ListItem(Integer(B23, 8, false))
138+
ListItem(Integer(B24, 8, false)) ListItem(Integer(B25, 8, false))
139+
ListItem(Integer(B26, 8, false)) ListItem(Integer(B27, 8, false))
140+
ListItem(Integer(B28, 8, false)) ListItem(Integer(B29, 8, false))
141+
ListItem(Integer(B30, 8, false)) ListItem(Integer(B31, 8, false))
142+
143+
syntax Bool ::= #isPByte ( Int ) [macro]
144+
rule #isPByte(X) => 0 <=Int X andBool X <Int 256
145+
113146
syntax Value ::= fromKey ( Key ) [function, total]
114147
// -----------------------------------------------
115148
// We assume that the Key always contains valid data, because it is constructed via toKey.
@@ -659,24 +692,74 @@ An `AccountInfo` reference is passed to the function.
659692
#### `#addMultisig`
660693

661694
```{.k .symbolic}
695+
// Multisig cheatcode: decompose signer pubkeys into individual byte variables.
696+
// Each ?SiNBj:Int is a single byte (0..255), giving 32 concrete ListItems per signer.
697+
// This allows ==K on pubkey Lists to decompose into integer equalities (fast for SMT),
698+
// instead of opaque symbolic List equality (causes Z3 timeout at scale).
662699
rule #addMultisig(Aggregate(variantIdx(0), _:List ListItem(Integer(DATA_LEN, 64, false))) #as P_ACC)
663700
=> PAccountMultisig(
664701
#toPAcc(P_ACC),
665702
IMulti(U8(?M),
666703
U8(?N),
667704
U8(?INITIALISED),
668-
Signers( ListItem(Key(?Signer0))
669-
ListItem(Key(?Signer1))
670-
ListItem(Key(?Signer2))
705+
Signers( ListItem(Key(#mkPubkey(
706+
?Si0B0:Int, ?Si0B1:Int, ?Si0B2:Int, ?Si0B3:Int,
707+
?Si0B4:Int, ?Si0B5:Int, ?Si0B6:Int, ?Si0B7:Int,
708+
?Si0B8:Int, ?Si0B9:Int, ?Si0B10:Int, ?Si0B11:Int,
709+
?Si0B12:Int, ?Si0B13:Int, ?Si0B14:Int, ?Si0B15:Int,
710+
?Si0B16:Int, ?Si0B17:Int, ?Si0B18:Int, ?Si0B19:Int,
711+
?Si0B20:Int, ?Si0B21:Int, ?Si0B22:Int, ?Si0B23:Int,
712+
?Si0B24:Int, ?Si0B25:Int, ?Si0B26:Int, ?Si0B27:Int,
713+
?Si0B28:Int, ?Si0B29:Int, ?Si0B30:Int, ?Si0B31:Int)))
714+
ListItem(Key(#mkPubkey(
715+
?Si1B0:Int, ?Si1B1:Int, ?Si1B2:Int, ?Si1B3:Int,
716+
?Si1B4:Int, ?Si1B5:Int, ?Si1B6:Int, ?Si1B7:Int,
717+
?Si1B8:Int, ?Si1B9:Int, ?Si1B10:Int, ?Si1B11:Int,
718+
?Si1B12:Int, ?Si1B13:Int, ?Si1B14:Int, ?Si1B15:Int,
719+
?Si1B16:Int, ?Si1B17:Int, ?Si1B18:Int, ?Si1B19:Int,
720+
?Si1B20:Int, ?Si1B21:Int, ?Si1B22:Int, ?Si1B23:Int,
721+
?Si1B24:Int, ?Si1B25:Int, ?Si1B26:Int, ?Si1B27:Int,
722+
?Si1B28:Int, ?Si1B29:Int, ?Si1B30:Int, ?Si1B31:Int)))
723+
ListItem(Key(#mkPubkey(
724+
?Si2B0:Int, ?Si2B1:Int, ?Si2B2:Int, ?Si2B3:Int,
725+
?Si2B4:Int, ?Si2B5:Int, ?Si2B6:Int, ?Si2B7:Int,
726+
?Si2B8:Int, ?Si2B9:Int, ?Si2B10:Int, ?Si2B11:Int,
727+
?Si2B12:Int, ?Si2B13:Int, ?Si2B14:Int, ?Si2B15:Int,
728+
?Si2B16:Int, ?Si2B17:Int, ?Si2B18:Int, ?Si2B19:Int,
729+
?Si2B20:Int, ?Si2B21:Int, ?Si2B22:Int, ?Si2B23:Int,
730+
?Si2B24:Int, ?Si2B25:Int, ?Si2B26:Int, ?Si2B27:Int,
731+
?Si2B28:Int, ?Si2B29:Int, ?Si2B30:Int, ?Si2B31:Int)))
671732
)
672733
)
673734
)
674-
ensures 0 <=Int ?M andBool ?M <=Int 256
675-
andBool 0 <=Int ?N andBool ?N <=Int 256
676-
andBool 0 <=Int ?INITIALISED andBool ?INITIALISED <=Int 256
677-
andBool size(?Signer0) ==Int 32 andBool allBytes(?Signer0)
678-
andBool size(?Signer1) ==Int 32 andBool allBytes(?Signer1)
679-
andBool size(?Signer2) ==Int 32 andBool allBytes(?Signer2)
735+
ensures #isPByte(?M) andBool #isPByte(?N) andBool #isPByte(?INITIALISED)
736+
// signer 0
737+
andBool #isPByte(?Si0B0) andBool #isPByte(?Si0B1) andBool #isPByte(?Si0B2) andBool #isPByte(?Si0B3)
738+
andBool #isPByte(?Si0B4) andBool #isPByte(?Si0B5) andBool #isPByte(?Si0B6) andBool #isPByte(?Si0B7)
739+
andBool #isPByte(?Si0B8) andBool #isPByte(?Si0B9) andBool #isPByte(?Si0B10) andBool #isPByte(?Si0B11)
740+
andBool #isPByte(?Si0B12) andBool #isPByte(?Si0B13) andBool #isPByte(?Si0B14) andBool #isPByte(?Si0B15)
741+
andBool #isPByte(?Si0B16) andBool #isPByte(?Si0B17) andBool #isPByte(?Si0B18) andBool #isPByte(?Si0B19)
742+
andBool #isPByte(?Si0B20) andBool #isPByte(?Si0B21) andBool #isPByte(?Si0B22) andBool #isPByte(?Si0B23)
743+
andBool #isPByte(?Si0B24) andBool #isPByte(?Si0B25) andBool #isPByte(?Si0B26) andBool #isPByte(?Si0B27)
744+
andBool #isPByte(?Si0B28) andBool #isPByte(?Si0B29) andBool #isPByte(?Si0B30) andBool #isPByte(?Si0B31)
745+
// signer 1
746+
andBool #isPByte(?Si1B0) andBool #isPByte(?Si1B1) andBool #isPByte(?Si1B2) andBool #isPByte(?Si1B3)
747+
andBool #isPByte(?Si1B4) andBool #isPByte(?Si1B5) andBool #isPByte(?Si1B6) andBool #isPByte(?Si1B7)
748+
andBool #isPByte(?Si1B8) andBool #isPByte(?Si1B9) andBool #isPByte(?Si1B10) andBool #isPByte(?Si1B11)
749+
andBool #isPByte(?Si1B12) andBool #isPByte(?Si1B13) andBool #isPByte(?Si1B14) andBool #isPByte(?Si1B15)
750+
andBool #isPByte(?Si1B16) andBool #isPByte(?Si1B17) andBool #isPByte(?Si1B18) andBool #isPByte(?Si1B19)
751+
andBool #isPByte(?Si1B20) andBool #isPByte(?Si1B21) andBool #isPByte(?Si1B22) andBool #isPByte(?Si1B23)
752+
andBool #isPByte(?Si1B24) andBool #isPByte(?Si1B25) andBool #isPByte(?Si1B26) andBool #isPByte(?Si1B27)
753+
andBool #isPByte(?Si1B28) andBool #isPByte(?Si1B29) andBool #isPByte(?Si1B30) andBool #isPByte(?Si1B31)
754+
// signer 2
755+
andBool #isPByte(?Si2B0) andBool #isPByte(?Si2B1) andBool #isPByte(?Si2B2) andBool #isPByte(?Si2B3)
756+
andBool #isPByte(?Si2B4) andBool #isPByte(?Si2B5) andBool #isPByte(?Si2B6) andBool #isPByte(?Si2B7)
757+
andBool #isPByte(?Si2B8) andBool #isPByte(?Si2B9) andBool #isPByte(?Si2B10) andBool #isPByte(?Si2B11)
758+
andBool #isPByte(?Si2B12) andBool #isPByte(?Si2B13) andBool #isPByte(?Si2B14) andBool #isPByte(?Si2B15)
759+
andBool #isPByte(?Si2B16) andBool #isPByte(?Si2B17) andBool #isPByte(?Si2B18) andBool #isPByte(?Si2B19)
760+
andBool #isPByte(?Si2B20) andBool #isPByte(?Si2B21) andBool #isPByte(?Si2B22) andBool #isPByte(?Si2B23)
761+
andBool #isPByte(?Si2B24) andBool #isPByte(?Si2B25) andBool #isPByte(?Si2B26) andBool #isPByte(?Si2B27)
762+
andBool #isPByte(?Si2B28) andBool #isPByte(?Si2B29) andBool #isPByte(?Si2B30) andBool #isPByte(?Si2B31)
680763
andBool DATA_LEN ==Int 99 // size_of(Multisig), see pinocchio_token_interface::state::Transmutable instance
681764
```
682765

0 commit comments

Comments
 (0)