arXiv cs.AI· Houston Haynes·· 9 天前AI 评分12
Decidable By Construction：面向真正无惧系统的设计时验证
Decidable By Construction: Design-Time Verification for Truly Fearless Systems
AI 导读
论文提出 Composer 编译器，在将 Clef 直接编译到 CPU、GPU、NPU 和 FPGA 原生代码时保留证明，无需经 C 或厂商 API 转换。其四层验证体系前 3 层无需开发者标注，第 4 层支持计算与概率关系证明，并以分布式归约示例验证并发与边界映射下结果一致。
正文 · AI 翻译
摘要：当编译器跟踪等待边、证明多线程工作可靠并保持分布式边界契约时，并发、并行和分布式执行变得真正无所畏惧。在此设计中，我们的 Composer 编译器在将 Clef 直接降低为原生 CPU、GPU、NPU 和 FPGA 代码的同时保留证明，无需通过 C 或供应商 API 进行转换。我们的程序语义图保留了为 BAREWire 的非装箱边界契约提供依据的值、关系和前提。而 C 与 C++ 的接口是一个显式的封送边界，其证明与实际参数、转换和返回值相关联。
四个验证层级构成了对我们设计的说明。第 1 层提供结构推断，建立在主量纲类型之上。第 2 层在节点级别生成并检查局部算术、表示和计算完整性。第 3 层实例化可复用的领域和系统引理，包括由 Iris、Actris 和 Aneris 支持的分布式证明。第 1-3 层不需要开发者注解，采用基于引用的引理库设计，以在使用场景扩展时扩大覆盖范围。第 4 层允许计算和概率关系证明，并通过项目注解标识所需的关系。我们将同一库方向扩展到从超图结构识别关系构造。
一条形式化组合规则连接了算术、所有权、协议和实现证据。我们经过验证的分布式归约在并发工作线程、重排序到达和边界映射之间保持一个指定结果。其概率扩展以显式失败预算携带工作线程和转换误差。结合 Urschel 最近的工作，我们表明界限提供了可复用证明项的一个相关来源。这些构造使验证成为一门核心工程学科，为各种硬件目标上的真正无所畏惧的程序和系统服务。
| 评论： | 33 页，0 幅图，4 张表。重大修订：扩展了四层验证。添加了精确和概率分布式示例 |
| 主题： | 编程语言（cs.PL）；人工智能（cs.AI）；机器学习（cs.LG）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2603.25414 [cs.PL] |
| （或 arXiv:2603.25414v5 [cs.PL] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2603.25414 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Houston Haynes [查看电子邮件]
[v1]
2026 年 3 月 26 日星期四 13:09:36 UTC（21 KB）
[v2]
2026 年 4 月 13 日星期一 23:17:30 UTC（23 KB）
[v3]
2026 年 4 月 19 日星期日 15:17:01 UTC（24 KB）
[v4]
2026 年 6 月 16 日星期二 01:22:57 UTC（24 KB）
[v5]
2026 年 10 月 8 日星期四 14:51:48 UTC（43 KB）
来源：arXiv cs.AI · arxiv.org