Upstream WebAssembly specific features from Kasmer
オープン
@virgil-serbanuta がすでに取り組んでいます。
2024年6月12日 から。
評価
この issue はまだ評価されていません。
説明
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.
- 主要言語
- WebAssembly
- スター
- 107
- フォーク
- 26
- PR マージ指標
- 30日以内にマージされた PR はありません
環境構築
- Dockerfile または Docker Compose ファイルあり
- プルリクエストのテンプレートなし
- コントリビューションガイドを読む
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
runtimeverification/wasm-semantics のほかの issue
-
enhancement
難易度 2/5 1〜3時間 初心者へのやさしさ 55/100
-
bug
難易度 4/5 3〜5日 初心者へのやさしさ 35/100
-
難易度 3/5 1〜2日 初心者へのやさしさ 48/100
-
難易度 3/5 1〜2日 初心者へのやさしさ 55/100
-
難易度 4/5 3〜5日 初心者へのやさしさ 35/100