Get rid of duplicated lemmas for commutative operations
还没有人认领这个 Issue。
评估
- 难度
- 4/5
- 预计耗时
- 3-5 天
- 新手友好度
- 38/100
- Issue 类型
- 重构
- 描述清晰度
- 基本清楚
- 活跃度
- 停滞
- 技术栈
- wasm
- 领域
- compilers
调研方向
将链接的 KEVM 引理与 wasm-semantics 引理文件进行比较，然后检查现有的交换-结合情形，以寻找重复或简化的机会。完成意味着等价的引理已被合并，或在需要的地方添加，并且已覆盖所识别的简化。
由索引模型根据 Issue 内容生成。
描述
KEVM uses the following lemmas to push symbolic values to the left in commutative-associative operations: https://github.com/kframework/evm-semantics/blob/master/tests/specs/lemmas.k#L290
We should add the same or similar lemmas, and go over our lemmas file and look for other cases where this can be simplified.
- 主要语言
- WebAssembly
- 星标
- 107
- 派生
- 25
- PR 合并指标
- 30 天内没有已合并 PR
环境准备
- 提供 Dockerfile 或 Docker Compose 文件
- 没有 Pull Request 模板
- 阅读贡献指南
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 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
查看 runtimeverification/wasm-semantics 的全部 Issue