3.6 KiB
初期監査の検証器
python3 tools/check_p04_order_evidence.py --verify-only は環境変数 BUILD_OUTPUT_DIR の p04-evidence/index.json を読み、書込み・試験・Runner操作をしない。欠落時は非0。原30/88の受入・完了を確定しない。
このdispatchではD05が未承認であるため、検証器は常に非0で終了する。indexのapproved/pass宣言で解除できない。これは初期監査の制限であり、全条件を機械的に検証できる完成版gateではない。承認済み原規約と生証跡が供給された後、別契約でsemantic coverageとnative provenanceの検証を追加する必要がある。
内部JSON形式は P04_ORDER_EVIDENCE_PROTOCOL.json を基に次の有限サブセットを実装した。重複JSONキー、NaN/Infinity、絶対・親参照・symlink・重複artifact pathを拒否する。全ハッシュは生バイトSHA256。indexに合格booleanや試験数があっても判定には使用しない。
schema_version: 1,task_id: P04-01, checkout HEADと一致するcandidate_commit,formal_acceptance: false。source_map: repository相対パス→SHA256。specの6不変pinと旧map内autoload/scriptsの全GDScript依存を必須とする。追加sourceも実ファイルと照合する。environment: 非空osとengine,configuration,inputsの証拠ディレクトリ相対パス→SHA256 map。engineは実行バイナリのコピー。OSの自己申告だけではnative証明にならない。artifacts: ID→path,bytes（整数）,sha256,type。typeは observation/state/receipt/stdout/native_log/save/authority のいずれか。authority: ref→status（original/approved）,artifact_id。raw文書の存在を確認するが内容の原規約適合は独立レビューを要する。pendingは失敗。domains: 正確な7領域名→source_refs,authority_refs,cases,invariants,applicability。source_refはpath/function/sha256。applicabilityはindexと同じsource_map/environment。- 各caseは一意な
idとartifact IDのinput/before/operation/after/receipt。receipt JSONは正整数start_pid、同じend_pid、整数exit_code: 0、engine_ended: true、一致するsource_map/environment、rawstdout/native_logartifact IDを要求する。自己申告receiptとrawログの意味的結合、別PID保存member一致は未対応であり合格扱いしない。 - 各invariantは
artifact_id/json_pointer/operator/authority_ref/raw_origin。raw_originはengineのみ。root derivationはformula検証未対応のため拒否する。RFC6901 pointerでraw JSONから値を読む。eqはexpectedとの型を含むliteral一致、nonnegativeはboolean以外の数値が0以上、count_eqは配列/辞書長と整数expectedの一致。same_literal/distinctはpaired_artifact_id/paired_json_pointerの値との型を含む比較。未知operatorは失敗。
期待値の承認根拠、停止中帳簿不変、決算再送/再開一回、予約とlive targetの対応、payment identity重複なし、必須case coverageを構造チェックだけで証明しない。最後にD05とsemantic/native証明の不足を明示して失敗させる。
Runner向け最小確認: index欠落、重複キー、symlink/traversal、hash/size不一致、stale source、未実行receipt、未知predicate、pending authority、7領域欠落が非0になること。その後、D05が未承認の完全形indexでも非0であること。正式境界試験は監査の有限計画に沿い、不適用の旧証拠だけを置き換える。workerはこれらを実行していない。