Show warning on proofs with loop-depth bounded nodes
还没有人认领这个 Issue。
评估
- 难度
- 3/5
- 预计耗时
- 1-2 天
- 新手友好度
- 45/100
- Issue 类型
- 功能
- 描述清晰度
- 基本清楚
- 活跃度
- 停滞
- 领域
- tooling
调研方向
首先定位证明完成/报告的入口点，以及循环深度界限的处理逻辑。完成的标准是：通过的证明会报告有界节点的数量和迭代次数上限，并包含 --unbounded-loops 以进行完整验证。
由索引模型根据 Issue 内容生成。
描述
As suggested by @ehildenb (https://github.com/runtimeverification/evm-semantics/issues/1963#issuecomment-1652119790), we should have a loud warning on passed proofs if any nodes are passed because they are bounded, something like "Proof passed, but NNN nodes were loop-depth bounded at MMM iterations, re-run with --unbounded-loops for full verification."
- 主要语言
- KCL
- 星标
- 592
- 派生
- 156
- 平均合并
- 2 小时 19 分钟
- 30 天内合并 PR
- 1
环境准备
我们还没有检查这个项目的环境配置文件。先看它的 README，通用步骤见我们的新手贡献指南。
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
runtimeverification/evm-semantics 的其他 Issue
-
难度 1/5 1 小时以内 新手友好度 78/100
runtimeverification/evm-semantics#1190 ·
-
难度 4/5 3-5 天 新手友好度 45/100
runtimeverification/evm-semantics#2879 ·
-
难度 4/5 3-5 天 新手友好度 35/100
runtimeverification/evm-semantics#2869 ·
-
难度 4/5 3-5 天 新手友好度 35/100
runtimeverification/evm-semantics#2832 ·
-
难度 4/5 3-5 天 新手友好度 30/100
runtimeverification/evm-semantics#2824 ·
查看 runtimeverification/evm-semantics 的全部 Issue
相似的 Issue
-
难度 2/5 1-3 小时 新手友好度 78/100
维护者通常 1 天内回复
-
难度 2/5 1-3 小时 新手友好度 84/100
维护者通常 1 天内回复
-
难度 2/5 1-3 小时 新手友好度 84/100
mpfaffenberger/privateer_reimagined#649 ·
维护者通常 1 天内回复
-
难度 2/5 1-3 小时 新手友好度 68/100
hacs/integration#5563 · 1 条评论 ·
维护者通常 2 天内回复
-
难度 1/5 1 小时以内 新手友好度 92/100
维护者通常 1 天内回复