Skip to content

Commit ec47f8a

Browse files
jbertholdrv-auditor
jberthold
and
rv-auditor
authored
Mark a number of rules as preserving definedness (#263)
* mark #memStore rule as preserving definedness * mark writeToStorage rules as preserving definedness * mark resetCallstate rule as preserving definedness * mark KASMER.endFoundryImmediately as preserving definedness * mark #sliceBytes rule as preserving definedness * mark rules updating the account map at known keys as preserving definedness * Set Version: 0.1.56 * Set Version: 0.1.59 * From review: Point out esdtData in comments about definedness * esdt.md: reformulate comment * kasmer.md: reformulate comment * Set Version: 0.1.61 --------- Co-authored-by: devops <[email protected]>
1 parent 3892eb7 commit ec47f8a

File tree

7 files changed

+56
-45
lines changed

7 files changed

+56
-45
lines changed

‎kmultiversx/pyproject.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kmultiversx"
7-
version = "0.1.60"
7+
version = "0.1.61"
88
description = "Python tools for Elrond semantics"
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

‎kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,7 @@ module ELROND-CONFIG
105105
</memInst>
106106
requires #signed(i32 , OFFSET) +Int lengthBytes(BS) <=Int (SIZE *Int #pageSize())
107107
andBool 0 <=Int #signed(i32 , OFFSET)
108+
[preserves-definedness] // setBytesRange total, MEMADDR key existed prior in <mems> map
108109
109110
rule [memStore-owise]:
110111
<instrs> #memStore(_, _) => #throwException(ExecutionFailed, "mem store: memory instance not found") ... </instrs>
@@ -192,6 +193,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
192193
...
193194
</account>
194195
requires VALUE ==K .Bytes
196+
[preserves-definedness] // map update is total, CALLEE key existed prior
195197
rule <instrs> #writeToStorage(KEY, VALUE) => i32.const #storageStatus(STORAGE, KEY, VALUE) ... </instrs>
196198
<callee> CALLEE </callee>
197199
<account>
@@ -200,6 +202,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
200202
...
201203
</account>
202204
requires VALUE =/=K .Bytes
205+
[preserves-definedness] // map update is total, CALLEE key existed prior
203206
204207
rule [writeToStorage-unknown-addr]:
205208
<instrs> #writeToStorage(_, _) => #throwException(ExecutionFailed, "writeToStorage: unknown account address") ... </instrs>

‎kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -371,10 +371,11 @@ The `<callStack>` cell stores a list of previous contract execution states. Thes
371371
| mkCall( Bytes, WasmString, VmInputCell )
372372
373373
syntax InternalCmd ::= "resetCallstate" [klabel(resetCallState), symbol]
374-
// ---------------------------------------------------------------------------
374+
// ---------------------------------------------------------------------------
375375
rule [resetCallstate]:
376376
<commands> resetCallstate => .K ... </commands>
377377
(_:CallStateCell => <callState> <instrs> .K </instrs> ... </callState>)
378+
[preserves-definedness] // all constant configuration cells should be defined
378379
379380
endmodule
380381
```

‎kmultiversx/src/kmultiversx/kdist/mx-semantics/esdt.md‎

Lines changed: 39 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ module ESDT
2626
| transferESDTsAux(Bytes, Bytes, List) [function, total]
2727
// -------------------------------------------------------------------
2828
rule transferESDTs(FROM, TO, L)
29-
=> transferESDTsAux(FROM, TO, L)
29+
=> transferESDTsAux(FROM, TO, L)
3030
~> appendToOutAccount(TO, OutputTransfer(FROM, L))
3131
3232
rule transferESDTsAux(FROM:Bytes, TO:Bytes, ListItem(T:ESDTTransfer) Ts)
@@ -45,7 +45,7 @@ module ESDT
4545
~> addToESDTBalance(FROM, TOKEN, 0 -Int VALUE, false)
4646
~> addToESDTBalance(TO, TOKEN, VALUE, true)
4747
48-
rule transferESDT(FROM, TO, esdtTransfer(TOKEN, VALUE, NONCE))
48+
rule transferESDT(FROM, TO, esdtTransfer(TOKEN, VALUE, NONCE))
4949
=> checkAccountExists(FROM)
5050
~> checkAccountExists(TO)
5151
~> checkESDTBalance(FROM, keyWithNonce(TOKEN, NONCE), VALUE)
@@ -146,18 +146,21 @@ module ESDT
146146
...
147147
</account>
148148
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
149-
[priority(61)]
149+
[priority(61), preserves-definedness]
150+
// preserves-definedness:
151+
// - ACCT exists prior so the account map is defined
152+
// - TOKEN does not exist prior in esdtData, otherwise the rule above with higher priority would apply.
150153
151154
rule [addToESDTBalance-new-err-instrs-empty]:
152155
<commands> addToESDTBalance(_ACCT, _TOKEN, _DELTA, false)
153-
=> #exception(ExecutionFailed, b"new NFT data on sender")
156+
=> #exception(ExecutionFailed, b"new NFT data on sender")
154157
...
155158
</commands>
156159
<instrs> .K </instrs>
157160
[priority(61)]
158161
rule [addToESDTBalance-new-err-instrs-wait]:
159162
<commands> addToESDTBalance(_ACCT, _TOKEN, _DELTA, false)
160-
=> #exception(ExecutionFailed, b"new NFT data on sender")
163+
=> #exception(ExecutionFailed, b"new NFT data on sender")
161164
...
162165
</commands>
163166
<instrs> #waitCommands ... </instrs>
@@ -244,10 +247,10 @@ module ESDT
244247
rule BuiltinFunction2Bytes(#ESDTLocalMint) => b"ESDTLocalMint"
245248
246249
rule [ESDTLocalMint]:
247-
<commands> processBuiltinFunction(#ESDTLocalMint, SND, DST, <vmInput>
250+
<commands> processBuiltinFunction(#ESDTLocalMint, SND, DST, <vmInput>
248251
<callValue> VALUE </callValue>
249252
<callArgs> ARGS </callArgs>
250-
_
253+
_
251254
</vmInput>)
252255
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
253256
~> checkBool(size(ARGS) >=Int 2, "invalid arguments to process built-in function")
@@ -273,17 +276,17 @@ module ESDT
273276
rule BuiltinFunction2Bytes(#ESDTLocalBurn) => b"ESDTLocalBurn"
274277
275278
rule [ESDTLocalBurn]:
276-
<commands> processBuiltinFunction(#ESDTLocalBurn, SND, DST, <vmInput>
279+
<commands> processBuiltinFunction(#ESDTLocalBurn, SND, DST, <vmInput>
277280
<callValue> VALUE </callValue>
278281
<callArgs> ARGS </callArgs>
279-
_
282+
_
280283
</vmInput>)
281284
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
282285
~> checkBool(size(ARGS) >=Int 2, "invalid arguments to process built-in function")
283286
~> checkBool(SND ==K DST, "invalid receiver address")
284287
~> checkAccountExists(SND)
285288
// TODO If the token has the 'BurnRoleForAll' global property, skip 'checkAllowedToExecute'
286-
~> checkAllowedToExecute(SND, getArg(ARGS, 0), ESDTRoleLocalBurn)
289+
~> checkAllowedToExecute(SND, getArg(ARGS, 0), ESDTRoleLocalBurn)
287290
~> checkBool( lengthBytes(getArg(ARGS, 1)) <=Int 100
288291
, "invalid arguments to process built-in function")
289292
~> checkESDTBalance(SND, getArg(ARGS, 0), getArgUInt(ARGS, 1))
@@ -304,10 +307,10 @@ module ESDT
304307
rule BuiltinFunction2Bytes(#ESDTNFTBurn) => b"ESDTNFTBurn"
305308
306309
rule [ESDTNFTBurn]:
307-
<commands> processBuiltinFunction(#ESDTNFTBurn, SND, DST, <vmInput>
310+
<commands> processBuiltinFunction(#ESDTNFTBurn, SND, DST, <vmInput>
308311
<callValue> VALUE </callValue>
309312
<callArgs> ARGS </callArgs>
310-
_
313+
_
311314
</vmInput>)
312315
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
313316
~> checkBool(size(ARGS) >=Int 2, "invalid arguments to process built-in function")
@@ -346,11 +349,11 @@ module ESDT
346349
rule BuiltinFunction2Bytes(#ESDTTransfer) => b"ESDTTransfer"
347350
348351
rule [ESDTTransfer]:
349-
<commands> processBuiltinFunction(#ESDTTransfer, SND, DST,
350-
<vmInput>
352+
<commands> processBuiltinFunction(#ESDTTransfer, SND, DST,
353+
<vmInput>
351354
<callValue> VALUE </callValue>
352355
<callArgs> ARGS </callArgs>
353-
_
356+
_
354357
</vmInput> #as VMINPUT)
355358
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
356359
~> checkBool(size(ARGS) >=Int 2, "invalid arguments to process built-in function")
@@ -373,11 +376,11 @@ module ESDT
373376
[symbol(determineIsSCCallAfter)]
374377
// ----------------------------------------------
375378
rule [determineIsSCCallAfter-call]:
376-
<commands> determineIsSCCallAfter(SND, DST, FUNC, <vmInput>
379+
<commands> determineIsSCCallAfter(SND, DST, FUNC, <vmInput>
377380
<callArgs> ARGS </callArgs>
378381
<gasProvided> GAS </gasProvided>
379382
<gasPrice> GAS_PRICE </gasPrice>
380-
_
383+
_
381384
</vmInput>)
382385
=> newWasmInstance(DST, CODE)
383386
~> mkCall( DST
@@ -431,11 +434,11 @@ module ESDT
431434
rule BuiltinFunction2Bytes(#MultiESDTNFTTransfer) => b"MultiESDTNFTTransfer"
432435
433436
rule [MultiESDTNFTTransfer]:
434-
<commands> processBuiltinFunction(#MultiESDTNFTTransfer, SND, DST,
435-
<vmInput>
437+
<commands> processBuiltinFunction(#MultiESDTNFTTransfer, SND, DST,
438+
<vmInput>
436439
<callValue> VALUE </callValue>
437440
<callArgs> ARGS </callArgs>
438-
_
441+
_
439442
</vmInput> #as VMINPUT)
440443
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
441444
~> checkBool(size(ARGS) >=Int 4, "invalid arguments to process built-in function")
@@ -480,8 +483,8 @@ module ESDT
480483
rule parseESDTTransfers(_, _) => .List
481484
[owise]
482485
483-
rule parseESDTTransfersH(N, ListItem(wrap(TOK)) ListItem(wrap(NONCE)) ListItem(wrap(AMT)) REST)
484-
=> ListItem( esdtTransfer(
486+
rule parseESDTTransfersH(N, ListItem(wrap(TOK)) ListItem(wrap(NONCE)) ListItem(wrap(AMT)) REST)
487+
=> ListItem( esdtTransfer(
485488
TOK, Bytes2Int(AMT, BE, Unsigned), Bytes2Int(NONCE, BE, Unsigned)
486489
))
487490
parseESDTTransfersH(N -Int 1, REST)
@@ -501,11 +504,11 @@ module ESDT
501504
rule BuiltinFunction2Bytes(#ESDTNFTCreate) => b"ESDTNFTCreate"
502505
503506
rule [ESDTNFTCreate]:
504-
<commands> processBuiltinFunction(#ESDTNFTCreate, SND, DST,
505-
<vmInput>
507+
<commands> processBuiltinFunction(#ESDTNFTCreate, SND, DST,
508+
<vmInput>
506509
<callValue> VALUE </callValue>
507510
<callArgs> ARGS </callArgs>
508-
_
511+
_
509512
</vmInput>)
510513
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
511514
~> checkBool(size(ARGS) >=Int 7, "invalid arguments to process built-in function")
@@ -546,7 +549,7 @@ module ESDT
546549
// --------------------------------------------------------------------------------------------
547550
rule ESDTNFTCreate.meta(SND, ARGS)
548551
=> esdtMetadata( ...
549-
name: getArg(ARGS, 2),
552+
name: getArg(ARGS, 2),
550553
nonce: getLatestNonce(SND, ESDTNFTCreate.token(ARGS)) +Int 1,
551554
creator: SND,
552555
royalties: getArgUInt(ARGS, 3),
@@ -615,11 +618,11 @@ module ESDT
615618
rule BuiltinFunction2Bytes(#ESDTNFTAddQuantity) => b"ESDTNFTAddQuantity"
616619
617620
rule [ESDTNFTAddQuantity]:
618-
<commands> processBuiltinFunction(#ESDTNFTAddQuantity, SND, DST,
619-
<vmInput>
621+
<commands> processBuiltinFunction(#ESDTNFTAddQuantity, SND, DST,
622+
<vmInput>
620623
<callValue> VALUE </callValue>
621624
<callArgs> ARGS </callArgs>
622-
_
625+
_
623626
</vmInput>)
624627
625628
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
@@ -665,11 +668,11 @@ module ESDT
665668
rule BuiltinFunction2Bytes(#ESDTNFTTransfer) => b"ESDTNFTTransfer"
666669
667670
rule [ESDTNFTTransfer]:
668-
<commands> processBuiltinFunction(#ESDTNFTTransfer, SND, DST,
669-
<vmInput>
671+
<commands> processBuiltinFunction(#ESDTNFTTransfer, SND, DST,
672+
<vmInput>
670673
<callValue> VALUE </callValue>
671674
<callArgs> ARGS </callArgs>
672-
_
675+
_
673676
</vmInput> #as VMINPUT)
674677
675678
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
@@ -695,11 +698,11 @@ module ESDT
695698
696699
// ESDTNFTAddURI & TOKEN & NONCE & URI1 & URI2 ...
697700
rule [ESDTNFTAddURI]:
698-
<commands> processBuiltinFunction(#ESDTNFTAddURI, SND, DST,
699-
<vmInput>
701+
<commands> processBuiltinFunction(#ESDTNFTAddURI, SND, DST,
702+
<vmInput>
700703
<callValue> VALUE </callValue>
701704
<callArgs> ARGS </callArgs>
702-
_
705+
_
703706
</vmInput>)
704707
705708
=> checkBool(VALUE ==Int 0, "built in function called with tx value is not allowed")
@@ -779,7 +782,7 @@ module ESDT
779782
[priority(60)]
780783
781784
rule [checkAllowedToExecute-fail]:
782-
<commands> checkAllowedToExecute(_ADDR, _TOK, _ROLE)
785+
<commands> checkAllowedToExecute(_ADDR, _TOK, _ROLE)
783786
=> #exception(UserError, b"action is not allowed") ...
784787
</commands>
785788
<instrs> .K </instrs>

‎kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
204204
...
205205
</account>
206206
requires VALUE ==K .Bytes
207+
[preserves-definedness] // ADDR exists prior in account map
207208
208209
rule [foundryWriteToStorage]:
209210
<instrs> foundryWriteToStorage => .K ... </instrs>
@@ -214,7 +215,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
214215
...
215216
</account>
216217
requires VALUE =/=K .Bytes
217-
218+
[preserves-definedness] // ADDR exists prior in account map
218219
```
219220

220221
### Set balance
@@ -348,7 +349,9 @@ Only the `#foundryRunner` account can execute these commands/host functions.
348349
+String Bytes2String(TOK_ID)
349350
</logging>
350351
requires 0 <=Int VALUE
351-
[priority(60)]
352+
[priority(60), preserves-definedness]
353+
// - ADDR exists prior so the account map is well-defined
354+
// - TOK_ID does not exist prior in esdtData because otherwise the rule above with higher priority would apply.
352355
353356
// ERROR: account not found
354357
rule [setESDTBalance-acct-not-found]:
@@ -577,7 +580,7 @@ Only the `#foundryRunner` account can execute these commands/host functions.
577580
<checkedAccounts> _ => .Set </checkedAccounts>
578581
<prank> _ => false </prank>
579582
<exit-code> _ => 0 </exit-code>
580-
583+
[preserves-definedness] // all initial configuration fields assumed defined
581584
```
582585

583586
### Prank

‎kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -68,11 +68,12 @@ module MANBUFOPS
6868
rule <instrs> #sliceBytes(OFFSET, LENGTH) => .K ... </instrs>
6969
<bytesStack> (BS => substrBytes(BS, OFFSET, OFFSET +Int LENGTH)) : _ </bytesStack>
7070
requires #sliceBytesInBounds( BS , OFFSET , LENGTH )
71+
[preserves-definedness] // bounds for substrBytes checked explicitly
7172
7273
syntax Bool ::= #sliceBytesInBounds( Bytes , Int , Int ) [function, total]
73-
rule #sliceBytesInBounds( BS , OFFSET , LENGTH )
74-
=> OFFSET >=Int 0 andBool
75-
LENGTH >=Int 0 andBool
74+
rule #sliceBytesInBounds( BS , OFFSET , LENGTH )
75+
=> OFFSET >=Int 0 andBool
76+
LENGTH >=Int 0 andBool
7677
OFFSET +Int LENGTH <=Int lengthBytes(BS)
7778
```
7879

‎package/version‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.60
1+
0.1.61

0 commit comments

Comments
 (0)