Skip to content

Commit c3d6857

Browse files
rv-jenkinsrv-auditorgithub-actions[bot]dkcummingmariaKt
authored
Update dependency: deps/kmir_release (#27)
Changes other than the version bump: - Sync `spl-token.md` and `p-token.md` from upstream `feature/p-token`, adapting `requires` paths for kompass layout - `#forceSetLocal` removed from K semantics, replaced with `#setLocalValue` in `spl-token.md` ([#810](runtimeverification/mir-semantics#810)) - Decompose multisig signer pubkeys into individual bytes for SPL-token to avoid symbolic List equality in SMT ([#1000](runtimeverification/mir-semantics#1000)) - Add `sol_memset` zero-memset detection and cut-point rule for SPL-token data buffers ([#1005](runtimeverification/mir-semantics#1005)) - Decompose multisig signer pubkeys into individual bytes for p-token, mirrors #1000 ([#1018](runtimeverification/mir-semantics#1018)) - `ProveOpts.start_symbol` renamed to `start_symbols` (now `list[str]`), adapted kompass to wrap single symbol in a list for compatibility ([#1071](runtimeverification/mir-semantics#1071)) - - **Note:** I did not port the full multiple `start_symbols` functionality to the kompass CLI, as I was not sure about the use case for kompass. Please advise, I will add it if you want. --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: mariaKt <kotsifakou.maria@gmail.com>
1 parent 6d7568b commit c3d6857

9 files changed

Lines changed: 772 additions & 444 deletions

File tree

‎deps/kmir_release‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.4.186
1+
0.4.213

‎package/version‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.17
1+
0.1.18

‎pyproject.toml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,19 @@ build-backend = "hatchling.build"
44

55
[project]
66
name = "kompass"
7-
version = "0.1.17"
7+
version = "0.1.18"
88
description = "K Semantics for the Solana ecosystem"
99
requires-python = "~=3.10"
1010
dependencies = [
11-
"kmir@git+https://github.com/runtimeverification/mir-semantics.git@v0.4.186#subdirectory=kmir",
11+
"kmir@git+https://github.com/runtimeverification/mir-semantics.git@v0.4.213#subdirectory=kmir",
1212
]
1313

1414
[[project.authors]]
1515
name = "Runtime Verification, Inc."
1616
email = "contact@runtimeverification.com"
1717

1818
[tool.uv.sources]
19-
kmir = { git = "https://github.com/runtimeverification/mir-semantics.git", rev = "v0.4.186", subdirectory = "kmir" }
19+
kmir = { git = "https://github.com/runtimeverification/mir-semantics.git", rev = "v0.4.213", subdirectory = "kmir" }
2020

2121
[project.scripts]
2222
kompass = "kompass.__main__:main"

‎src/kompass/__main__.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ def _run_prove(opts: ProveOpts) -> bool:
119119
reload=opts.reload,
120120
save_smir=False,
121121
smir=True,
122-
start_symbol=opts.start_symbol,
122+
start_symbols=[opts.start_symbol],
123123
)
124124
proof = kompass.prove_program(prove_opts)
125125
print(str(proof.summary))

‎src/kompass/kdist/kompass/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)