Skip to content

Commit

Permalink
Fix contract initialization and input handling
Browse files Browse the repository at this point in the history
Co-authored-by: Virgil Șerbănuță <[email protected]>"
  • Loading branch information
traiansf committed Dec 18, 2024
1 parent c61db98 commit da3ef4e
Show file tree
Hide file tree
Showing 3 changed files with 45 additions and 1 deletion.
43 changes: 43 additions & 0 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,7 @@ The embedder loads the module to be executed and then calls the entrypoint funct
<k> PGM:PgmEncoding
=> setContractModIdx
~> #resolveCurModuleFuncExport(#getEntryPoint())
~> remoteSetOutputOnCreate(PGM)
~> setSuccessStatus
</k>
<instrs> .K => decodePgm(PGM) </instrs>
Expand All @@ -218,6 +219,7 @@ This is ensured by requiring that the `<instrs>` cell is empty during resolution
| #resolveModuleFuncExport(Int, WasmString)
| #resolveFunc(Int, ListInt)
| "setContractModIdx"
| remoteSetOutputOnCreate(PgmEncoding)
| "setSuccessStatus"
// ----------------------------------------------
rule <k>
Expand Down Expand Up @@ -261,7 +263,28 @@ in the `contractModIdx` cell.
<instrs> .K </instrs>
<curModIdx> MODIDX:Int </curModIdx>
<contractModIdx> _ => MODIDX </contractModIdx>
```

`remoteSetOutputOnCreate` will do nothing on local but will set the output to
its argument on remote, but only if the `<create>` cell holds `true`.

```local
rule remoteSetOutputOnCreate(_) => .K
```

```remote
rule
<k> remoteSetOutputOnCreate(Out:Bytes) => .K ... </k>
<instrs> .K </instrs>
<create> true </create>
<output> _ => Out </output>
rule
<k> remoteSetOutputOnCreate(_) => .K ... </k>
<create> false </create>
```

```k
rule
// setSuccessStatus should only be used after everything finished executing,
// so we are checking that it is the only thing left in the <k> cell.
Expand Down Expand Up @@ -575,6 +598,26 @@ Handle the actual hook calls.
<output>
_ => BYTES
</output>
rule
<instrs>
hostCall("env", "fail", [ i32 i32 .ValTypes ] -> [ .ValTypes ])
=> #memLoad(OFFSET, LENGTH) ~> #fail
...
</instrs>
<locals>
ListItem(<i32> OFFSET:Int) ListItem(<i32> LENGTH:Int)
</locals>
syntax InternalInstr ::= "#fail"
rule
<instrs>
BYTES:Bytes ~> #fail => #throwException(EVMC_FAILURE, Bytes2String(BYTES))
...
</instrs>
```

```k
Expand Down
1 change: 1 addition & 0 deletions scripts/run-dev-ulm
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ FLAGS=(--dev --allow-insecure-unlock\
--http.corsdomain '*'\
--http.vhosts '*'\
--http.api debug,personal,web3,eth,net,txpool\
--dev.gaslimit 1000000000 \
--ws\
--ws.addr 0.0.0.0\
--ws.origins '*')
Expand Down
2 changes: 1 addition & 1 deletion tests/ulm/erc20/rust/src/ulm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,7 @@ pub fn caller(api: &dyn Ulm) -> Address {

pub fn call_data(api: &dyn Ulm) -> Bytes {
let length: usize = api.call_data_length().try_into().unwrap();
let mut buf = Vec::<u8>::with_capacity(length);
let mut buf : Vec<u8> = vec![0; length];
api.call_data(buf.as_mut_slice());
Bytes::copy_from_slice(buf.as_slice())
}
Expand Down

0 comments on commit da3ef4e

Please sign in to comment.