Open ehildenb opened 3 weeks ago
We should pull any features taht are WebAssembly specific into this repository. In particular:
KWasm
KLabel
KWasmSemantics
DefaultSemantics
is_terminal
abstract_node
Then retool Kasmer to use these classes and delete the code downstream.
We should pull any features taht are WebAssembly specific into this repository. In particular:
KWasm
which contains anyKLabel
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).KWasmSemantics
which implements semantics specific heuristics (can useDefaultSemantics
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.Then retool Kasmer to use these classes and delete the code downstream.