Skip to content

Commit 3892eb7

Browse files
bbyalcinkayarv-auditor
bbyalcinkaya
and
rv-auditor
authored
Optimize dt without or patterns (#267)
* Optimize dt without or patterns * Set Version: 0.1.59 * fix non-exhaustive match error * add TODO comment * small refactoring * Set Version: 0.1.60 --------- Co-authored-by: devops <[email protected]>
1 parent f18262e commit 3892eb7

File tree

5 files changed

+195
-157
lines changed

5 files changed

+195
-157
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.59"
7+
version = "0.1.60"
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: 121 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,19 @@ Elrond Configuration
44
Combine Elrond node with Wasm.
55

66
```k
7+
8+
// TODO: #or patterns are currently not supported in the Booster backend. PR k#4363 aims to resolve
9+
// this with a desugaring pass in the K frontend, but this solution may not handle rule labels properly.
10+
// In PR #267, we worked around this by either duplicating rules or commenting out cells that contain #or patterns.
11+
// The duplicated rules have labels ending with '-instrs-empty' and '-instrs-wait'.
12+
//
13+
// Once the issue with #or patterns is resolved in a way that supports rule labels,
14+
// de-duplicate these rules and re-enable the commented-out #or patterns.
15+
//
16+
// K PR : https://github.com/runtimeverification/k/pull/4363
17+
// K Issue: https://github.com/runtimeverification/k/issues/4355
18+
// mx-semantics PR: https://github.com/runtimeverification/mx-semantics/pull/267
19+
720
requires "vmhooks/async.md"
821
requires "wasm-semantics/wasm-text.md"
922
requires "plugin/krypto.md"
@@ -408,6 +421,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
408421
rule [exception-revert]:
409422
<commands> (#exception(EC, MSG) ~> #endWasm) => popCallState ~> popWorldState ... </commands>
410423
<vmOutput> .VMOutput => VMOutput( EC , MSG , .ListBytes , .List, .Map) </vmOutput>
424+
<logging> S => S +String " -- Exception: " +String Bytes2String(MSG) </logging>
411425
412426
rule [exception-skip]:
413427
<commands> #exception(_,_) ~> (CMD:InternalCmd => .K ) ... </commands>
@@ -420,24 +434,9 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
420434
`#throwException*` clears the `<instrs>` cell and creates an `#exception(_,_)` command with the given error code and message.
421435

422436
```k
423-
// ------------------------------------------------------------------
424-
rule [throwException]:
425-
<instrs> #throwException( EC , MSG )
426-
=> #throwExceptionBs( EC , String2Bytes(MSG) ) ...
427-
</instrs>
428-
rule [throwException-cmd]:
429-
<commands> #throwException( EC , MSG )
430-
=> #throwExceptionBs( EC , String2Bytes(MSG) ) ...
431-
</commands>
432-
433437
rule [throwExceptionBs]:
434438
<instrs> (#throwExceptionBs( EC , MSG ) ~> _ ) => .K </instrs>
435439
<commands> (.K => #exception(EC,MSG)) ... </commands>
436-
<logging> S => S +String " -- Exception: " +String Bytes2String(MSG) </logging>
437-
rule [throwExceptionBs-cmd]:
438-
<commands> (#throwExceptionBs( EC , MSG ) => #exception(EC,MSG)) ... </commands>
439-
<logging> S => S +String " -- Exception: " +String Bytes2String(MSG) </logging>
440-
441440
```
442441

443442
## Managing Accounts
@@ -457,17 +456,24 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
457456
syntax InternalCmd ::= createAccount ( Bytes ) [klabel(createAccount), symbol]
458457
// ------------------------------------------------------------------------------
459458
// ignore if the account already exists
460-
rule [createAccount-existing]:
459+
rule [createAccount-existing-instrs-empty]:
461460
<commands> createAccount(ADDR) => .K ... </commands>
462461
<account>
463462
<address> ADDR </address>
464463
...
465464
</account>
466-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
467-
// <logging> S => S +String " -- initAccount duplicate " +String Bytes2String(ADDR) </logging>
465+
<instrs> .K </instrs>
466+
[priority(60)]
467+
rule [createAccount-existing-instrs-wait]:
468+
<commands> createAccount(ADDR) => .K ... </commands>
469+
<account>
470+
<address> ADDR </address>
471+
...
472+
</account>
473+
<instrs> #waitCommands ... </instrs>
468474
[priority(60)]
469475
470-
rule [createAccount-new]:
476+
rule [createAccount-new-instrs-empty]:
471477
<commands> createAccount(ADDR) => .K ... </commands>
472478
<accounts>
473479
( .Bag
@@ -478,15 +484,40 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
478484
)
479485
...
480486
</accounts>
481-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
482-
// <logging> S => S +String " -- initAccount new " +String Bytes2String(ADDR) </logging>
487+
<instrs> .K </instrs>
488+
[priority(61)]
489+
rule [createAccount-new-instrs-wait]:
490+
<commands> createAccount(ADDR) => .K ... </commands>
491+
<accounts>
492+
( .Bag
493+
=> <account>
494+
<address> ADDR </address>
495+
...
496+
</account>
497+
)
498+
...
499+
</accounts>
500+
<instrs> #waitCommands ... </instrs>
483501
[priority(61)]
484502
485503
syntax InternalCmd ::= setAccountFields ( Bytes, Int, Int, Code, Bytes, MapBytesToBytes ) [klabel(setAccountFields), symbol]
486504
| setAccountCode ( Bytes, Code ) [klabel(setAccountCode), symbol]
487505
| setAccountOwner ( Bytes, Bytes )
488506
// ---------------------------------------------------------------
489-
rule [setAccountFields]:
507+
rule [setAccountFields-instrs-empty]:
508+
<commands> setAccountFields(ADDR, NONCE, BALANCE, CODE, OWNER_ADDR, STORAGE) => .K ... </commands>
509+
<account>
510+
<address> ADDR </address>
511+
<nonce> _ => NONCE </nonce>
512+
<balance> _ => BALANCE </balance>
513+
<code> _ => CODE </code>
514+
<ownerAddress> _ => OWNER_ADDR </ownerAddress>
515+
<storage> _ => STORAGE </storage>
516+
...
517+
</account>
518+
<instrs> .K </instrs>
519+
[priority(60)]
520+
rule [setAccountFields-instrs-wait]:
490521
<commands> setAccountFields(ADDR, NONCE, BALANCE, CODE, OWNER_ADDR, STORAGE) => .K ... </commands>
491522
<account>
492523
<address> ADDR </address>
@@ -497,26 +528,45 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
497528
<storage> _ => STORAGE </storage>
498529
...
499530
</account>
500-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
531+
<instrs> #waitCommands ... </instrs>
501532
[priority(60)]
502533
503-
rule [setAccountCode]:
534+
rule [setAccountCode-instrs-empty]:
504535
<commands> setAccountCode(ADDR, CODE) => .K ... </commands>
505536
<account>
506537
<address> ADDR </address>
507538
<code> _ => CODE </code>
508539
...
509540
</account>
510-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
541+
<instrs> .K </instrs>
542+
[priority(60)]
543+
rule [setAccountCode-instrs-wait]:
544+
<commands> setAccountCode(ADDR, CODE) => .K ... </commands>
545+
<account>
546+
<address> ADDR </address>
547+
<code> _ => CODE </code>
548+
...
549+
</account>
550+
<instrs> #waitCommands ... </instrs>
511551
[priority(60)]
512552
513-
rule <commands> setAccountOwner(ADDR, OWNER) => .K ... </commands>
553+
rule [setAccountOwner-instrs-empty]:
554+
<commands> setAccountOwner(ADDR, OWNER) => .K ... </commands>
555+
<account>
556+
<address> ADDR </address>
557+
<ownerAddress> _ => OWNER </ownerAddress>
558+
...
559+
</account>
560+
<instrs> .K </instrs>
561+
[priority(60)]
562+
rule [setAccountOwner-instrs-wait]:
563+
<commands> setAccountOwner(ADDR, OWNER) => .K ... </commands>
514564
<account>
515565
<address> ADDR </address>
516566
<ownerAddress> _ => OWNER </ownerAddress>
517567
...
518568
</account>
519-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
569+
<instrs> #waitCommands ... </instrs>
520570
[priority(60)]
521571
```
522572

@@ -528,17 +578,13 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
528578
- `transferFundsH` assumes that the accounts exist.
529579

530580
```k
531-
syntax InternalCmd ::= transferFunds ( Bytes, Bytes, Int )
532-
| transferFundsH ( Bytes, Bytes, Int )
581+
syntax K ::= transferFunds ( Bytes, Bytes, Int ) [function, total]
582+
syntax InternalCmd ::= transferFundsH ( Bytes, Bytes, Int )
533583
// -----------------------------------------
534-
rule <commands> transferFunds(A, B, V)
535-
=> checkAccountExists(A)
536-
~> checkAccountExists(B)
537-
~> transferFundsH(A, B, V)
538-
...
539-
</commands>
540-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
541-
[priority(60)]
584+
rule transferFunds(A, B, V)
585+
=> checkAccountExists(A)
586+
~> checkAccountExists(B)
587+
~> transferFundsH(A, B, V)
542588
543589
rule [transferFundsH-self]:
544590
<commands> transferFundsH(ACCT, ACCT, VALUE)
@@ -550,7 +596,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
550596
<balance> ORIGFROM </balance>
551597
...
552598
</account>
553-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
599+
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
554600
requires VALUE <=Int ORIGFROM
555601
[priority(60)]
556602
@@ -569,21 +615,21 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
569615
<balance> ORIGTO => ORIGTO +Int VALUE </balance>
570616
...
571617
</account>
572-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
618+
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
573619
requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
574620
[priority(60), preserves-definedness]
575621
// Preserving definedness:
576622
// - Map updates preserve definedness
577623
// - -Int and +Int are total
578624
579625
rule [transferFundsH-oofunds]:
580-
<commands> transferFundsH(ACCT, _, VALUE) => #throwExceptionBs(OutOfFunds, b"") ... </commands>
626+
<commands> transferFundsH(ACCT, _, VALUE) => #exception(OutOfFunds, b"") ... </commands>
581627
<account>
582628
<address> ACCT </address>
583629
<balance> ORIGFROM </balance>
584630
...
585631
</account>
586-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
632+
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
587633
requires VALUE >Int ORIGFROM
588634
[priority(60)]
589635
@@ -592,15 +638,13 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
592638
## Calling Contract
593639

594640
```k
595-
syntax InternalCmd ::= callContract ( Bytes, String, VmInputCell ) [klabel(callContractString), symbol]
596-
| callContract ( Bytes, WasmString, VmInputCell ) [klabel(callContractWasmString), symbol]
641+
syntax InternalCmd ::= callContract ( Bytes, String, VmInputCell ) [symbol(callContractString), function, total]
642+
| callContract ( Bytes, WasmString, VmInputCell ) [symbol(callContractWasmString)]
643+
| callContractAux ( Bytes, Bytes, WasmString, VmInputCell ) [symbol(callContractAux)]
597644
// -------------------------------------------------------------------------------------
598-
rule <commands> callContract(TO, FUNCNAME:String, VMINPUT)
599-
=> callContract(TO, #quoteUnparseWasmString(FUNCNAME), VMINPUT) ...
600-
</commands>
601-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
602-
[priority(60)]
603-
645+
rule callContract(TO, FUNCNAME:String, VMINPUT)
646+
=> callContract(TO, #quoteUnparseWasmString(FUNCNAME), VMINPUT)
647+
604648
rule [callContract]:
605649
<commands> callContract(TO, FUNCNAME:WasmStringToken,
606650
<vmInput>
@@ -615,72 +659,58 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
615659
~> resetCallstate
616660
~> transferFunds(FROM, TO, VALUE)
617661
~> transferESDTs(FROM, TO, ESDT)
618-
~> newWasmInstance(TO, CODE)
619-
~> mkCall(TO, FUNCNAME, VMINPUT)
662+
~> callContractAux(FROM, TO, FUNCNAME, VMINPUT)
620663
~> #endWasm
621664
...
622665
</commands>
666+
<vmOutput> _ => .VMOutput </vmOutput>
667+
<logging> S => S +String " -- callContract " +String #parseWasmString(FUNCNAME) </logging>
668+
669+
rule [callContractAux]:
670+
<commands> callContractAux(_FROM, TO, FUNCNAME, VMINPUT)
671+
=> newWasmInstance(TO, CODE)
672+
~> mkCall(TO, FUNCNAME, VMINPUT)
673+
...
674+
</commands>
623675
<account>
624676
<address> TO </address>
625677
<code> CODE </code>
626678
...
627679
</account>
628-
<vmOutput> _ => .VMOutput </vmOutput>
629-
<logging> S => S +String " -- callContract " +String #parseWasmString(FUNCNAME) </logging>
630-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
680+
<instrs> .K </instrs>
631681
requires notBool(isBuiltin(FUNCNAME))
632682
andBool #token("\"callBack\"", "WasmStringToken") =/=K FUNCNAME
633683
[priority(60)]
634684
635-
rule [callContract-builtin]:
636-
<commands> callContract(TO, FUNC:WasmStringToken,
637-
<vmInput>
638-
<caller> FROM </caller>
639-
<callValue> VALUE </callValue>
640-
<esdtTransfers> ESDT </esdtTransfers>
641-
_
642-
</vmInput> #as VMINPUT)
643-
=> pushWorldState
644-
~> pushCallState
645-
~> resetCallstate
646-
~> transferFunds(FROM, TO, VALUE)
647-
~> transferESDTs(FROM, TO, ESDT)
648-
~> processBuiltinFunction(toBuiltinFunction(FUNC), FROM, TO, VMINPUT)
649-
~> #endWasm
685+
rule [callContractAux-builtin]:
686+
<commands> callContractAux(FROM, TO, FUNC, VMINPUT)
687+
=> processBuiltinFunction(toBuiltinFunction(FUNC), FROM, TO, VMINPUT)
650688
...
651689
</commands>
652-
<vmOutput> _ => .VMOutput </vmOutput>
653-
<logging> S => S +String " -- callContract " +String #parseWasmString(FUNC) </logging>
654-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
690+
<instrs> .K </instrs>
655691
requires isBuiltin(FUNC)
656692
[priority(60)]
657693
658-
rule [callContract-err-callback]:
659-
<commands> callContract(_, FUNCNAME:WasmString, _)
660-
=> #throwExceptionBs(ExecutionFailed, b"invalid function (calling callBack() directly is forbidden)") ...
694+
rule [callContractAux-err-callback]:
695+
<commands> callContractAux(_, _, FUNCNAME:WasmString, _)
696+
=> #exception(ExecutionFailed, b"invalid function (calling callBack() directly is forbidden)") ...
661697
</commands>
662-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
698+
<instrs> .K </instrs>
663699
requires #token("\"callBack\"", "WasmStringToken") ==K FUNCNAME
664700
[priority(60)]
665701
666-
rule [callContract-not-contract]:
667-
<commands> callContract(TO, _:WasmString, _)
668-
=> #throwExceptionBs(ContractNotFound, b"not a contract: " +Bytes TO) ...
702+
rule [callContractAux-not-contract]:
703+
<commands> callContractAux(_, TO, _:WasmString, _)
704+
=> #exception(ContractNotFound, b"not a contract: " +Bytes TO) ...
669705
</commands>
670706
<account>
671707
<address> TO </address>
672708
<code> .Code </code>
673709
...
674710
</account>
675-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
711+
<instrs> .K </instrs>
676712
[priority(61)]
677713
678-
rule [callContract-not-found]:
679-
<commands> callContract(TO, _:WasmString, _)
680-
=> #throwExceptionBs(ExecutionFailed, b"account not found: " +Bytes TO) ...
681-
</commands>
682-
<instrs> (#waitCommands ~> _) #Or .K </instrs>
683-
[priority(62)]
684714
```
685715

686716
Every contract call runs in its own Wasm instance initialized with the contract's code.
@@ -711,6 +741,7 @@ Every contract call runs in its own Wasm instance initialized with the contract'
711741
<commands> setContractModIdx => .K ... </commands>
712742
<contractModIdx> _ => NEXTIDX -Int 1 </contractModIdx>
713743
<nextModuleIdx> NEXTIDX </nextModuleIdx>
744+
<instrs> .K </instrs>
714745
715746
syntax K ::= initContractModule(ModuleDecl) [function]
716747
// ------------------------------------------------------------------------
@@ -754,14 +785,16 @@ Initialize the call state and invoke the endpoint function:
754785
[priority(60)]
755786
756787
rule [mkCall-func-not-found]:
757-
<commands> mkCall(_TO, FUNCNAME:WasmStringToken, _VMINPUT) => .K ... </commands>
788+
<commands> mkCall(_TO, FUNCNAME:WasmStringToken, _VMINPUT)
789+
=> #exception(FunctionNotFound, b"invalid function (not found)") ...
790+
</commands>
758791
<contractModIdx> MODIDX:Int </contractModIdx>
759792
<moduleInst>
760793
<modIdx> MODIDX </modIdx>
761794
<exports> EXPORTS </exports>
762795
...
763796
</moduleInst>
764-
<instrs> .K => #throwException(FunctionNotFound, "invalid function (not found)") </instrs>
797+
<instrs> .K </instrs>
765798
<logging> S => S +String " -- callContract not found " +String #parseWasmString(FUNCNAME) </logging>
766799
requires notBool( FUNCNAME in_keys(EXPORTS) )
767800
[priority(60)]

0 commit comments

Comments
 (0)