diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md index 5527b5631..47c122a2f 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md @@ -205,6 +205,7 @@ The embedder loads the module to be executed and then calls the entrypoint funct PGM:PgmEncoding => setContractModIdx ~> #resolveCurModuleFuncExport(#getEntryPoint()) + ~> remoteSetOutputOnCreate(PGM) ~> setSuccessStatus .K => decodePgm(PGM) @@ -218,6 +219,7 @@ This is ensured by requiring that the `` cell is empty during resolution | #resolveModuleFuncExport(Int, WasmString) | #resolveFunc(Int, ListInt) | "setContractModIdx" + | remoteSetOutputOnCreate(PgmEncoding) | "setSuccessStatus" // ---------------------------------------------- rule @@ -261,7 +263,28 @@ in the `contractModIdx` cell. .K MODIDX:Int _ => MODIDX +``` + +`remoteSetOutputOnCreate` will do nothing on local but will set the output to +its argument on remote, but only if the `` cell holds `true`. + +```local + rule remoteSetOutputOnCreate(_) => .K +``` +```remote + rule + remoteSetOutputOnCreate(Out:Bytes) => .K ... + .K + true + _ => Out + + rule + remoteSetOutputOnCreate(_) => .K ... + false +``` + +```k rule // setSuccessStatus should only be used after everything finished executing, // so we are checking that it is the only thing left in the cell. @@ -575,6 +598,26 @@ Handle the actual hook calls. _ => BYTES + + + rule + + hostCall("env", "fail", [ i32 i32 .ValTypes ] -> [ .ValTypes ]) + => #memLoad(OFFSET, LENGTH) ~> #fail + ... + + + ListItem( OFFSET:Int) ListItem( LENGTH:Int) + + + + syntax InternalInstr ::= "#fail" + + rule + + BYTES:Bytes ~> #fail => #throwException(EVMC_FAILURE, Bytes2String(BYTES)) + ... + ``` ```k diff --git a/scripts/run-dev-ulm b/scripts/run-dev-ulm index 3f72c6a85..33f56681a 100755 --- a/scripts/run-dev-ulm +++ b/scripts/run-dev-ulm @@ -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 '*') diff --git a/tests/ulm/erc20/rust/src/ulm.rs b/tests/ulm/erc20/rust/src/ulm.rs index 82273b0c4..16f2aa567 100644 --- a/tests/ulm/erc20/rust/src/ulm.rs +++ b/tests/ulm/erc20/rust/src/ulm.rs @@ -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::::with_capacity(length); + let mut buf : Vec = vec![0; length]; api.call_data(buf.as_mut_slice()); Bytes::copy_from_slice(buf.as_slice()) }