다중 언어 계약 추적성(Multi-Language Contract Traceability)을 위한 최소 실행 가능한 증명

본 논문은 DAG-TOML 계약(contract)을 위한 의도적으로 작은 실행 가능한 증명을 보고합니다. Rust, Go, C, Java, TypeScript, AWK로 구현된 6개의 "Hello, world!" 구현체가 하나의 관찰 가능한 출력 계약(observable-output contract), 하나의 구현 DAG(implementation DAG), 하나의 추적성 파일(traceability file), 하나의 준비 게이트(readiness gate), 그리고 하나의 증거 매트릭스(evidence matrix)에 연결됩니다. 이 핵심 계약(load-bearing contract)은 정확한 UTF-8 바이트 시퀀스인 Hello, world!\n, stderr 바이트 0개, 그리고 종료 코드(exit code) 0을 요구합니다. 본 논문에서 사용된 러너(runner)에서 증인 하네스(witness harness)는 5개의 PASS 결과, javac/java가 PATH에 없어서 발생한 Java에 대한 1개의 SKIP, 그리고 0개의 FAIL 결과를 보고했습니다. 두 개의 사이드카 증인(sidecar witnesses)은 더 좁은 범위의 소스 분석(source-analysis) 주장을 실행합니다. 복잡하게 재작성된 Go 코드는 연속적인 인사말 리터럴(greeting literal)을 숨기지만, 선언된 AST 심볼(AST symbol) 및 단순 엣지(simple-edge) 수준에서 sqry에 의해 여전히 가시적입니다. 반면, 간접적인 AWK 재작성은 AWK가 저장소의 sqry 기반 검증 언어 세트(validator language set)에 포함되어 있지 않기 때문에 선언된 소스 프로필(source profile)을 사용합니다. 본 기여는 벤치마크나 일반적인 의미론적 동등성(semantic equivalence)에 대한 주장, 또는 프로덕션 보증 시스템이 아닙니다. 이는 계약(contract), 구현 그래프(implementation graph), 추적성 체인(traceability chain), 그리고 검토 게이트(review gate)가 실행 가능한 증인(executable witnesses)에 대해 어떻게 검증될 수 있는지를 보여주는 컴팩트하고 반증 가능한 산출물(falsifiable artifact)입니다.