Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update to use Pi2 fork of WASM #2

Merged
merged 8 commits into from
Aug 9, 2024
Merged

Update to use Pi2 fork of WASM #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
96568f7
update poetry lock
Aug 6, 2024
29851f4
use wasm fork
Aug 6, 2024
08598aa
fix compile errors
Aug 6, 2024
9265148
attempt to prune decision tree
Aug 6, 2024
9a11e39
update blockchain plugin version
dwightguth Aug 8, 2024
439a333
delete procps
dwightguth Aug 8, 2024
94ff8b4
update runtime
dwightguth Aug 9, 2024
576d379
fix code quality issue
dwightguth Aug 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
292 changes: 156 additions & 136 deletions kmultiversx/poetry.lock
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion kmultiversx/pyproject.toml
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading