Skip to content

Commit

Permalink
Minimize size of ERC20 Wasm Contract (#42)
Browse files Browse the repository at this point in the history
* add helper scripts

* Build fixes and instructions for the remote ULM demo

* improve pykwasm scripts

* update scripts

* fix sorts

* add formatting

* update deploy_contract script

* add fix to deploy contract script

* fix issues in python scripts

* improve README

* update README further

* remove files to be committed in a separate PR

* remove unfinished script

* remove redundant changes

* improve deploy contract script

* apply formatter

* remove deprecated deploy contract script

* add arity check

* update rust build

* improve README

* Fix Wasm VM Initialization Bug (#43)

* add kore rich header build

* update entrypoint resolution

* fix syntax error

* fix more errors

* remove deprecated comment

---------

Co-authored-by: Virgil <[email protected]>
  • Loading branch information
sskeirik and virgil-serbanuta authored Dec 16, 2024
1 parent d7baaf6 commit 0921a6c
Show file tree
Hide file tree
Showing 6 changed files with 12,502 additions and 15 deletions.
4 changes: 3 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,9 @@ $(ULM_WASM_TARGET): $(ULM_KRYPTO_TARGET) $(ULM_HOOKS_TARGET) $(ULM_WASM_SRC)
--emit-json \
$(if $(DEBUG),--debug) \
-o $(ULM_WASM_DIR)
$(if $(ULM_TEST),,cp "$(ULM_WASM_DIR)/$(ULM_WASM_OUT)" "$(ULM_LIB_DIR)")
kore-rich-header "$(ULM_WASM_DIR)/definition.kore" -o "$(ULM_WASM_DIR)/header.bin"
$(if $(ULM_TEST),,cp "$(ULM_WASM_DIR)/$(ULM_WASM_OUT)" "$(ULM_LIB_DIR)";)
$(if $(ULM_TEST),,cp "$(ULM_WASM_DIR)/header.bin" "$(ULM_LIB_DIR)";)

.PHONY: ulm-wasm
ulm-wasm: $(ULM_WASM_TARGET)
Expand Down
29 changes: 21 additions & 8 deletions pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
Original file line number Diff line number Diff line change
Expand Up @@ -91,22 +91,38 @@ A special configuration cell is added in the local case to support VM initializa
</ulmWasm>
```

Obtaining the Entrypoint
------------------------

In the standalone semantics, the Wasm VM obtains an entrypoint from the configuration.

```local
syntax String ::= #getEntryPoint() [function, total]
rule #getEntryPoint() => FUNCNAME
[[ <entry> FUNCNAME </entry> ]]
```

In the remote semantics, the Wasm VM has a fixed entrypoint.

```remote
syntax String ::= #getEntryPoint() [function, total]
rule #getEntryPoint() => "ulmDispatchCaller"
```

Passing Control
---------------

The embedder loads the module to be executed and then resolves the entrypoint function.
Currently, only the local Wasm VM initialization is supported.

```local
rule <k> PGM:PgmEncoding => #resolveCurModuleFuncExport(FUNCNAME) </k>
<entry> FUNCNAME </entry>
```k
rule <k> PGM:PgmEncoding => #resolveCurModuleFuncExport(#getEntryPoint()) </k>
<instrs> .K => decodePgm(PGM) </instrs>
```

Note that entrypoint resolution must occur _after_ the Wasm module has been loaded.
This is ensured by requiring that the `<instrs>` cell is empty during resolution.

```local
```k
syntax Initializer ::= #resolveCurModuleFuncExport(String)
| #resolveModuleFuncExport(Int, String)
| #resolveFunc(Int, ListInt)
Expand Down Expand Up @@ -142,9 +158,6 @@ ULM Hook Behavior

These rules define various integration points between the ULM and our Wasm interpreter.

**Note**: the first three rules hooks below are written with helper functions
because parse errors were encountered when writing `<generatedTopCell>` literals.

```k
rule getGasLeft(
Expand Down
Loading

0 comments on commit 0921a6c

Please sign in to comment.