Upstream WebAssembly specific features from Kasmer

Aperta

#646 aperta il 12/6/2024 0 commenti 0 reazioni 1 assegnatario Vedi su GitHub

@virgil-serbanuta ci sta già lavorando.

Dal 12/6/2024.

Valutazione

Questa issue non è ancora stata valutata.

We should pull any features taht are WebAssembly specific into this repository. In particular:

A new class KWasm which contains any KLabel and 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 KWasmSemantics which implements semantics specific heuristics (can use DefaultSemantics as the initial implementations) (KEVM example: https://github.com/runtimeverification/evm-semantics/blob/71a19f1a085efd1cf2987954101f500b7c02a6ce/kevm-pyk/src/kevm_pyk/kevm.py#L53). Should contain:
- is_terminal predicate for identifying states that should not be executed past (eg. for checking "should we check subsumption for this state or not).
- abstract_node operator 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.

Leggi tutta la issue e poi la guida ai contributi del progetto.
Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
Fai un fork del repository e lavora su un branch.
Apri una pull request che faccia riferimento al numero della issue.