We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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.
The text was updated successfully, but these errors were encountered:
virgil-serbanuta
No branches or pull requests
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.
The text was updated successfully, but these errors were encountered: