This paper reports a deliberately small executable proof for a DAG-TOML contract: six "Hello, world!" implementations in Rust, Go, C, Java, TypeScript, and AWK are linked to one observable-output contract, one implementation DAG, one traceability file, one readiness gate, and one evidence matrix. The load-bearing contract requires the exact UTF-8 byte sequence `Hello, world!\n`, zero stderr bytes, and exit code 0. On the runner used for this paper, the witness harness reported five PASS outcomes, one SKIP for Java because `javac/java` was not on `PATH`, and zero FAIL outcomes. Two sidecar witnesses exercise narrower source-analysis claims: a convoluted Go rewrite hides the contiguous greeting literal but remains visible to sqry at the declared AST symbol and simple-edge level, while an indirect AWK rewrite uses a declared source profile because AWK is not in the repository's sqry-backed validator language set. The contribution is not a benchmark, a claim of general semantic equivalence, or a production assurance system. It is a compact, falsifiable artifact that shows how a contract, implementation graph, traceability chain, and review gate can be checked against executable witnesses.


翻译:本文报告了一个刻意最小化的可执行证明,用于一种DAG-TOML合约:将Rust、Go、C、Java、TypeScript和AWK中的六个“Hello, world!”实现链接至一个可观察输出合约、一个实现DAG、一个可追溯性文件、一个就绪检查关卡和一个证据矩阵。承载合约要求精确的UTF-8字节序列`Hello, world!\n`,零字节stderr输出,以及退出代码0。在本文使用的运行器上,见证程序报告了五个PASS结果,一个SKIP(针对Java,因`javac/java`不在`PATH`路径中),以及零个FAIL结果。两个辅助见证程序执行了更狭窄的源代码分析声明:一个复杂的Go重写隐藏了连续的问候文字,但仍在声明的AST符号和简单边级别上对sqry保持可见;而一个间接的AWK重写使用了声明的源配置文件,因为AWK不在存储库的sqry支持的验证器语言集中。本文的贡献并非基准测试、通用语义等价声明或生产保障系统。它是一个紧凑且可证伪的工件,展示了如何根据可执行见证程序来检查合约、实现图、可追溯性链和审查关卡。

0
下载
关闭预览

相关内容

【2023新书】程序证明,Program Proofs,642页pdf
专知会员服务
67+阅读 · 2023年3月29日
【ICML2022】可达性约束强化学习
专知会员服务
23+阅读 · 2022年5月18日
专知会员服务
34+阅读 · 2021年5月8日
智能合约的形式化验证方法研究综述
专知
16+阅读 · 2021年5月8日
LibRec 精选:推荐的可解释性[综述]
LibRec智能推荐
10+阅读 · 2018年5月4日
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
VIP会员
最新内容
《无人地面战车(UGV)的崛起》报告
专知会员服务
6+阅读 · 7月16日
美陆军任务式指挥人工智能解决方案
专知会员服务
10+阅读 · 7月16日
相关VIP内容
【2023新书】程序证明,Program Proofs,642页pdf
专知会员服务
67+阅读 · 2023年3月29日
【ICML2022】可达性约束强化学习
专知会员服务
23+阅读 · 2022年5月18日
专知会员服务
34+阅读 · 2021年5月8日
相关基金
国家自然科学基金
0+阅读 · 2017年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员