Stop pre-parsing Wasm bytecode in Python and storing Wasm ASTs in <code>

[bbyalcinkaya]

This PR removes support for storing Stylus contract code as Wasm ASTs (ModuleDecl) in the <code> cell.

Background

In the EVM semantics, contract code is represented as raw bytecode:

syntax AccountCode ::= Bytes

Stylus semantics extended this with:

syntax AccountCode ::= ModuleDecl

where ModuleDecl represents Wasm modules, either in text form or abstract syntax form.

The <code> cell could contain:

• Bytes

  • EVM bytecode
  • Wasm bytecode

• ModuleDecl

  • Wasm text modules (used in .wast tests)
  • Parsed Wasm ASTs

Wasm text modules and abstract Wasm modules share the same ModuleDecl sort, so they cannot be distinguished at the sort level.

Previous behavior

Wasm AST storage existed primarily because the semantics could not directly parse Wasm bytecode, and there were no pyk hooks available for parsing.

As a workaround in skribe and skribe-simulation:

• Wasm modules were parsed in Python before execution
• Parsed ASTs were injected directly into K terms
• This behavior was used in:
  • skribe-simulation
  • the Skribe test contract (and, prior to pyk hooks, all Wasm contracts deployed from it)

After implementing pyk hooks, contracts created by the test contract started being stored as Wasm bytecode, with their parsed ASTs cached in <parsedWasmCache>, but the main test contract still used Wasm ASTs directly.

Changes in this PR

This PR removes the remaining usage of Wasm ASTs as contract code storage.

After this change:

• Except for .wast tests (which still use Wasm text format), contract code is always stored as bytecode (Bytes)
• Wasm parsing is delegated entirely to the pyk hooks
• Parsed modules are cached in <parsedWasmCache>

To support this flow in the semantics, a #parseAndCacheWasm step is triggered after setContract in skribe.md.

The AccountCode sort is unchanged since Wasm text modules are still needed for .wast tests.

Affected components

The following components are updated to stop injecting parsed Wasm ASTs directly:

• Contract creation in skribe-simulation
• Test contract setup in skribe

Instead of pre-parsing Wasm in Python, they now rely on the parse-and-cache flow through the pyk hooks.

[tothtamas28]

Is this extension still necessary, or can it be dropped?

syntax AccountCode ::= ModuleDecl

[bbyalcinkaya]

Is this extension still necessary, or can it be dropped?

syntax AccountCode ::= ModuleDecl

@tothtamas28

It is still necessary for .wast tests. .wast is a custom text format used to test the semantics with hand-written Wasm modules. These files are executed directly with krun, so the semantics must still be able to handle ModuleDecl.

Example: https://github.com/runtimeverification/skribe/blob/master/src/tests/integration/data/wast/storage_load_bytes32.wast