runtimeverification / runtimeverification/wasm-semantics
Upstream WebAssembly specific features from Kasmer
Open
@virgil-serbanuta is already working on this.
Since Jun 12, 2024.
- Dominant language
- WebAssembly
- Stars
- 106
- Forks
- 24
- PR merge metrics
- No merged PRs in 30d
Description
We should pull any features taht are WebAssembly specific into this repository. In particular:
- A new class
KWasmwhich contains anyKLabeland helpers for constructing KWasm terms (similar to KEVM class: https://github.com/runtimeverification/evm-semantics/blob/71a19f1a085efd1cf2987954101f500b7c02a6ce/kevm-pyk/src/kevm_pyk/kevm.py#L394). - A new class called
KWasmSemanticswhich implements semantics specific heuristics (can useDefaultSemanticsas the initial implementations) (KEVM example: https://github.com/runtimeverification/evm-semantics/blob/71a19f1a085efd1cf2987954101f500b7c02a6ce/kevm-pyk/src/kevm_pyk/kevm.py#L53). Should contain:is_terminalpredicate for identifying states that should not be executed past (eg. for checking "should we check subsumption for this state or not).abstract_nodeoperator for abstracting away parts of the KWasm state.
- Any core body of lemmas that are useful for WebAssembly in general:
- The lemmas can be migrated upstream to WebAssembly.
- The tests can be minimized and migrated upstream to WebAssembly (simplification tests, I assume).
Then retool Kasmer to use these classes and delete the code downstream.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.