Skip to content

Commit

Permalink
Update to use Pi2 fork of WASM (#2)
Browse files Browse the repository at this point in the history 
* update poetry lock

* use wasm fork

* fix compile errors

* attempt to prune decision tree

* update blockchain plugin version

* delete procps

* update runtime

* fix code quality issue
  • Loading branch information
@dwightguth
dwightguth authored Aug 9, 2024
1 parent 06be32c commit 4103aff
Show file tree
Hide file tree
Showing 15 changed files with 418 additions and 414 deletions.
292 changes: 156 additions & 136 deletions kmultiversx/poetry.lock
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion kmultiversx/pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ mx-semantics = "kmultiversx.kdist.plugin"

[tool.poetry.dependencies]
python = "^3.10"
pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.95", subdirectory = "pykwasm" }
pykwasm = { git = "https://github.com/Pi-Squared-Inc/wasm-semantics.git", branch = "master", subdirectory = "pykwasm" }
pycryptodomex = "^3.18.0"
hypothesis = "^6.82.6"
exceptiongroup = "==1.2.1"
Expand Down
50 changes: 16 additions & 34 deletions kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,31 +76,22 @@ module ELROND-CONFIG
<contractModIdx> MODIDX:Int </contractModIdx>
<moduleInst>
<modIdx> MODIDX </modIdx>
<memAddrs> 0 |-> MEMADDR </memAddrs>
<memAddrs> ListItem(MEMADDR) </memAddrs>
...
</moduleInst>
<memInst>
<mAddr> MEMADDR </mAddr>
<msize> SIZE </msize>
...
</memInst>
<mems> MEMS </mems>
requires 0 <=Int #signed(i32 , OFFSET)
andBool #signed(i32 , OFFSET) +Int lengthBytes(BS) >Int (SIZE *Int #pageSize())
andBool (#let memInst(_, SIZE, _) = MEMS[MEMADDR] #in #signed(i32 , OFFSET) +Int lengthBytes(BS) >Int (SIZE *Int #pageSize()))
rule <instrs> #memStore(OFFSET, BS) => .K ... </instrs>
<contractModIdx> MODIDX:Int </contractModIdx>
<moduleInst>
<modIdx> MODIDX </modIdx>
<memAddrs> 0 |-> MEMADDR </memAddrs>
<memAddrs> ListItem(MEMADDR) </memAddrs>
...
</moduleInst>
<memInst>
<mAddr> MEMADDR </mAddr>
<msize> SIZE </msize>
<mdata> DATA => #setBytesRange(DATA, OFFSET, BS) </mdata>
...
</memInst>
requires #signed(i32 , OFFSET) +Int lengthBytes(BS) <=Int (SIZE *Int #pageSize())
<mems> MEMS => MEMS [ MEMADDR <- #let memInst(MAX, SIZE, DATA) = MEMS[MEMADDR] #in memInst(MAX, SIZE, #setBytesRange(DATA, OFFSET, BS)) ] </mems>
requires (#let memInst(_, SIZE, _) = MEMS[MEMADDR] #in #signed(i32 , OFFSET) +Int lengthBytes(BS) <=Int (SIZE *Int #pageSize()))
andBool 0 <=Int #signed(i32 , OFFSET)
[preserves-definedness] // setBytesRange total, MEMADDR key existed prior in <mems> map
Expand All @@ -125,36 +116,27 @@ module ELROND-CONFIG
<contractModIdx> MODIDX:Int </contractModIdx>
<moduleInst>
<modIdx> MODIDX </modIdx>
<memAddrs> 0 |-> MEMADDR </memAddrs>
<memAddrs> ListItem(MEMADDR) </memAddrs>
...
</moduleInst>
<memInst>
<mAddr> MEMADDR </mAddr>
<msize> SIZE </msize>
...
</memInst>
<mems> MEMS </mems>
requires #signed(i32 , LENGTH) >Int 0
andBool (#signed(i32 , OFFSET) <Int 0
orBool #signed(i32 , OFFSET) +Int #signed(i32 , LENGTH) >Int (SIZE *Int #pageSize()))
orBool (#let memInst(_, SIZE, _) = MEMS[MEMADDR] #in #signed(i32 , OFFSET) +Int #signed(i32 , LENGTH) >Int (SIZE *Int #pageSize())))
rule [memLoad]:
<instrs> #memLoad(OFFSET, LENGTH) => .K ... </instrs>
<bytesStack> STACK => #getBytesRange(DATA, OFFSET, LENGTH) : STACK </bytesStack>
<bytesStack> STACK => #getBytesRange((#let memInst(_, _, DATA) = MEMS[MEMADDR] #in DATA), OFFSET, LENGTH) : STACK </bytesStack>
<contractModIdx> MODIDX:Int </contractModIdx>
<moduleInst>
<modIdx> MODIDX </modIdx>
<memAddrs> 0 |-> MEMADDR </memAddrs>
<memAddrs> ListItem(MEMADDR) </memAddrs>
...
</moduleInst>
<memInst>
<mAddr> MEMADDR </mAddr>
<msize> SIZE </msize>
<mdata> DATA </mdata>
...
</memInst>
<mems> MEMS </mems>
requires #signed(i32 , LENGTH) >Int 0
andBool #signed(i32 , OFFSET) >=Int 0
andBool #signed(i32 , OFFSET) +Int #signed(i32 , LENGTH) <=Int (SIZE *Int #pageSize())
andBool (#let memInst(_, SIZE, _) = MEMS[MEMADDR] #in #signed(i32 , OFFSET) +Int #signed(i32 , LENGTH) <=Int (SIZE *Int #pageSize()))
rule [memLoad-owise]:
<instrs> #memLoad(_, _) => #throwException(ExecutionFailed, "mem load: memory instance not found") ... </instrs>
Expand Down Expand Up @@ -599,7 +581,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
<balance> ORIGFROM </balance>
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
requires VALUE <=Int ORIGFROM
[priority(60)]
Expand All @@ -618,7 +600,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
<balance> ORIGTO => ORIGTO +Int VALUE </balance>
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM
[priority(60), preserves-definedness]
// Preserving definedness:
Expand All @@ -632,7 +614,7 @@ TODO: Implement [reserved keys and read-only runtimes](https://github.com/Elrond
<balance> ORIGFROM </balance>
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
requires VALUE >Int ORIGFROM
[priority(60)]
Expand Down
14 changes: 7 additions & 7 deletions kmultiversx/src/kmultiversx/kdist/mx-semantics/esdt.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ module ESDT
</esdtData> => .Bag)
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
[priority(60)]
rule [removeEmptyNft-skip-instrs-empty]:
Expand Down Expand Up @@ -98,7 +98,7 @@ module ESDT
</esdtData>
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
requires VALUE <=Int ORIGFROM
[priority(60)]
Expand Down Expand Up @@ -130,7 +130,7 @@ module ESDT
</esdtData>
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
[priority(60)]
rule [addToESDTBalance-new-esdtData]:
Expand All @@ -144,7 +144,7 @@ module ESDT
</esdtData>)
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
[priority(61), preserves-definedness]
// preserves-definedness:
// - ACCT exists prior so the account map is defined
Expand Down Expand Up @@ -192,7 +192,7 @@ module ESDT
</esdtData>
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
[priority(60)]
rule [moveNFTToDestination-self]:
Expand All @@ -205,7 +205,7 @@ module ESDT
</esdtData>
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
[priority(60)]
rule [moveNFTToDestination-new]:
Expand All @@ -230,7 +230,7 @@ module ESDT
</esdtData>)
...
</account>
// <instrs> (#waitCommands ~> _) #Or .K </instrs>
<instrs> (#waitCommands ~> _) #Or .K </instrs>
[priority(61)]
```

Expand Down
72 changes: 36 additions & 36 deletions kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,9 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
...
</instrs>
<locals>
0 |-> <i32> ADDR_HANDLE
1 |-> <i64> NONCE
2 |-> <i32> BALANCE_HANDLE
ListItem(<i32> ADDR_HANDLE)
ListItem(<i64> NONCE)
ListItem(<i32> BALANCE_HANDLE)
</locals>
<callee> #kasmerRunner </callee>
Expand Down Expand Up @@ -76,9 +76,9 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
...
</instrs>
<locals>
0 |-> <i32> OWNER_HANDLE
1 |-> <i64> NONCE
2 |-> <i32> ADDR_HANDLE
ListItem(<i32> OWNER_HANDLE)
ListItem(<i64> NONCE)
ListItem(<i32> ADDR_HANDLE)
</locals>
<callee> #kasmerRunner </callee>
Expand Down Expand Up @@ -114,12 +114,12 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
...
</instrs>
<locals>
0 |-> <i32> OWNER_HANDLE
1 |-> <i64> GAS_LIMIT
2 |-> <i32> VALUE_HANDLE
3 |-> <i32> CODE_PATH_HANDLE
4 |-> <i32> ARGS_HANDLE
5 |-> <i32> RESULT_ADDR_HANDLE
ListItem(<i32> OWNER_HANDLE)
ListItem(<i64> GAS_LIMIT)
ListItem(<i32> VALUE_HANDLE)
ListItem(<i32> CODE_PATH_HANDLE)
ListItem(<i32> ARGS_HANDLE)
ListItem(<i32> RESULT_ADDR_HANDLE)
</locals>
<callee> #kasmerRunner </callee>
Expand Down Expand Up @@ -169,9 +169,9 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
...
</instrs>
<locals>
0 |-> <i32> OWNER_HANDLE
1 |-> <i32> KEY_HANDLE
2 |-> <i32> DEST_HANDLE
ListItem(<i32> OWNER_HANDLE)
ListItem(<i32> KEY_HANDLE)
ListItem(<i32> DEST_HANDLE)
</locals>
<callee> #kasmerRunner </callee>
Expand All @@ -187,9 +187,9 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
...
</instrs>
<locals>
0 |-> <i32> ADDR_HANDLE
1 |-> <i32> KEY_HANDLE
2 |-> <i32> VAL_HANDLE
ListItem(<i32> ADDR_HANDLE)
ListItem(<i32> KEY_HANDLE)
ListItem(<i32> VAL_HANDLE)
</locals>
<callee> #kasmerRunner </callee>
Expand Down Expand Up @@ -228,8 +228,8 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
=> #setBalance(getBuffer(ADDR_HANDLE), getBigInt(VAL_HANDLE)) ...
</instrs>
<locals>
0 |-> <i32> ADDR_HANDLE
1 |-> <i32> VAL_HANDLE
ListItem(<i32> ADDR_HANDLE)
ListItem(<i32> VAL_HANDLE)
</locals>
<callee> #kasmerRunner </callee>
Expand Down Expand Up @@ -287,9 +287,9 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
...
</instrs>
<locals>
0 |-> <i32> ADDR_HANDLE
1 |-> <i32> TOK_ID_HANDLE
2 |-> <i32> VAL_HANDLE
ListItem(<i32> ADDR_HANDLE)
ListItem(<i32> TOK_ID_HANDLE)
ListItem(<i32> VAL_HANDLE)
</locals>
<callee> #kasmerRunner </callee>
Expand Down Expand Up @@ -379,10 +379,10 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
...
</instrs>
<locals>
0 |-> <i32> ADDR_HANDLE
1 |-> <i32> TOK_ID_HANDLE
2 |-> <i32> ROLE
3 |-> <i32> P
ListItem(<i32> ADDR_HANDLE)
ListItem(<i32> TOK_ID_HANDLE)
ListItem(<i32> ROLE)
ListItem(<i32> P)
</locals>
syntax InternalInstr ::= #setESDTRole(ESDTLocalRole, Bool)
Expand Down Expand Up @@ -461,9 +461,9 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
...
</instrs>
<locals>
0 |-> <i32> ADDR_HANDLE
1 |-> <i32> TOK_ID_HANDLE
2 |-> <i32> ROLE
ListItem(<i32> ADDR_HANDLE)
ListItem(<i32> TOK_ID_HANDLE)
ListItem(<i32> ROLE)
</locals>
syntax InternalInstr ::= #checkESDTRole(ESDTLocalRole)
Expand Down Expand Up @@ -507,7 +507,7 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
=> .K ...
</instrs>
<locals>
0 |-> <i64> TIMESTAMP
ListItem(<i64> TIMESTAMP)
</locals>
<curBlockTimestamp> _ => TIMESTAMP </curBlockTimestamp>
<logging> S
Expand All @@ -526,7 +526,7 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
=> #assert( P ) ...
</instrs>
<locals>
0 |-> <i32> P
ListItem(<i32> P)
</locals>
syntax InternalInstr ::= #assert(Int) [symbol(kasmerAssert)]
Expand All @@ -547,7 +547,7 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
=> #assume(P) ...
</instrs>
<locals>
0 |-> <i32> P
ListItem(<i32> P)
</locals>
syntax IternalInstr ::= #assume(Int) [symbol(kasmerAssume)]
Expand Down Expand Up @@ -592,7 +592,7 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
~> #startPrank ...
</instrs>
<locals>
0 |-> <i32> ADDR_HANDLE
ListItem(<i32> ADDR_HANDLE)
</locals>
<callee> #kasmerRunner </callee>
Expand All @@ -619,15 +619,15 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
<instrs> hostCall ( "env" , "stopPrank" , [ .ValTypes ] -> [ .ValTypes ] )
=> .K ...
</instrs>
<locals> .Map </locals>
<locals> .List </locals>
<callee> _ => #kasmerRunner </callee>
<prank> true => false </prank>
rule [testapi-stopPrank-err]:
<instrs> hostCall ( "env" , "stopPrank" , [ .ValTypes ] -> [ .ValTypes ] )
=> #throwException(ExecutionFailed, "Cannot stop prank while not in a prank") ...
</instrs>
<locals> .Map </locals>
<locals> .List </locals>
<prank> false </prank>
[owise]
Expand Down
Loading

0 comments on commit 4103aff

Please sign in to comment.