Minimize size of ERC20 Wasm Contract

Makefile

@@ -93,7 +93,7 @@ ulm-krypto-build: $(ULM_KRYPTO_TARGET)
 $(ULM_CLONE_DIR)/.git:
 	@mkdir -p $(ULM_DEP_DIR)
 	cd $(ULM_DEP_DIR); \
-	  git clone --depth 1 https://github.com/pi-squared-inc/ulm
+	  git clone --depth 1 --branch contract-size-limits https://github.com/pi-squared-inc/ulm
 
 $(ULM_HOOKS_TARGET): $(ULM_SRC_HOOKS) | $(ULM_CLONE_DIR)/.git
 	@mkdir -p $(ULM_LIB_DIR)
@@ -194,7 +194,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)

README.md

@@ -196,7 +196,7 @@ poetry -C pykwasm run wasm ./build/wasm pykwasm/src/tests/integration/binary/bas
 To execute the Wasm VM remotely, you need to build the ULM by running:
 
 ```sh
-make ulm-build
+CXX=clang++-16 make ulm-wasm ulm-contract-compiler ulm-build -j8
 ```
 
 Then, you can start the ULM locally and load the Wasm VM into it by running:
@@ -206,9 +206,37 @@ Then, you can start the ULM locally and load the Wasm VM into it by running:
 ./scripts/ulm-load-lang ./build/lib/libwasm.so
 ```
 
-Then, you can invoke Wasm programs by doing the following:
+As an example, to deploy a Wasm contract, you can do the following:
 
-**TODO**
+1.  Install the python scripts:
+
+    ```sh
+    poetry -C pykwasm install
+    ```
+
+2.  Compile the contract:
+
+    ```sh
+    # compile Rust to Wasm
+    pushd tests/ulm/erc20/
+    cargo build --target=wasm32-unknown-unknown --release
+    cp target/wasm32-unknown-unknown/release/erc20.wasm ./
+    popd
+    # convert the Wasm to Kore
+    poetry -C pykwasm run wasm2kore build/wasm tests/ulm/erc20/erc20.wasm tests/ulm/erc20/erc20.kore
+    # convert the Kore to binary
+    scripts/compile-contract tests/ulm/erc20/erc20.kore > tests/ulm/erc20/erc20.bin
+    ```
+
+3.  Deploy the compiled Wasm contract:
+
+    ```sh
+    poetry -C pykwasm run deploy tests/ulm/erc20/erc20.bin
+    ```
+
+To invoke a deployed Wasm contract, do the following:
+
+**TODO:** add instructions.
 
 Resources
 ---------

pykwasm/pyproject.toml

@@ -11,7 +11,9 @@ authors = [
 ]
 
 [tool.poetry.scripts]
+deploy = "pykwasm.deploy_contract:main"
 wasm = "pykwasm.run_wasm:main"
+wasm2kore = "pykwasm.wasm2kore:main"
 wasm2kast = "pykwasm.wasm2kast:main"
 kwasm = "pykwasm.scripts.kwasm:main"
 kwasm-convert = "pykwasm.scripts.convert:main"
@@ -26,6 +28,7 @@ cytoolz = "^0.12.1"
 numpy = "^1.24.2"
 kframework = "7.1.149"
 py-wasm = { git = "https://github.com/runtimeverification/py-wasm.git", tag="0.2.1" }
+web3 = "7.6.0"
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"
@@ -66,7 +69,9 @@ disallow_untyped_defs = true
 # TODO fix type errors
 exclude = [
     'src/pykwasm/wasm2kast\.py',
+    'src/pykwasm/wasm2kore\.py',
     'src/pykwasm/run_wasm\.py',
+    'src/pykwasm/deploy_contract\.py',
     'src/wasm/*',
     'src/tests/unit/test_wasm2kast\.py',
 ]

pykwasm/src/pykwasm/deploy_contract.py

@@ -0,0 +1,57 @@
+#!/usr/bin/python3
+import sys
+from pathlib import Path
+
+from eth_account import Account
+from web3 import Web3
+from web3.middleware import SignAndSendRawMiddlewareBuilder
+
+
+def deploy_contract(node_url, sender, contract_hex):
+    w3 = Web3(Web3.HTTPProvider(node_url))
+    if sender is None:
+        sender = w3.eth.account.create()
+    # fund sender acct
+    fund_tx_hash = w3.eth.send_transaction(
+        {'from': w3.eth.accounts[0], 'to': sender.address, 'value': 1000000000000000000}
+    )
+    fund_tx_receipt = w3.eth.wait_for_transaction_receipt(fund_tx_hash)
+    w3.middleware_onion.inject(SignAndSendRawMiddlewareBuilder.build(sender), layer=0)
+    # deploy txn
+    deploy_token_tx = {
+        'from': sender.address,
+        'data': contract_hex,
+        'to': '',
+        'value': 0,
+        'gas': 11000000,
+        'maxFeePerGas': 2000000000,
+        'maxPriorityFeePerGas': 1000000000,
+    }
+    deploy_tx_hash = w3.eth.send_transaction(deploy_token_tx)
+    deploy_tx_receipt = w3.eth.wait_for_transaction_receipt(deploy_tx_hash)
+    return fund_tx_receipt, deploy_tx_receipt
+
+
+USAGE = 'deploy_contract.py <contract_file> [node_url] [sender_private_key_file]'
+
+
+def main():
+    args = sys.argv[1:]
+    if len(args) < 1:
+        print(USAGE)
+        sys.exit(1)
+    contract_hex = Path(args[0]).read_text().strip()
+    node_url = 'http://localhost:8545'
+    sender = None
+    if len(args) > 1:
+        node_url = args[1]
+    if len(args) > 2:
+        pk = bytes.fromhex(Path(args[2]).read_text().strip().removeprefix('0x'))
+        sender = Account.from_key(pk)
+    fund_receipt, deploy_receipt = deploy_contract(node_url, sender, contract_hex)
+    print(fund_receipt)
+    print(deploy_receipt)
+
+
+if __name__ == '__main__':
+    main()

pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md

@@ -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)
@@ -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(