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支持的验证器语言集中。本文的贡献并非基准测试、通用语义等价声明或生产保障系统。它是一个紧凑且可证伪的工件,展示了如何根据可执行见证程序来检查合约、实现图、可追溯性链和审查关卡。