16 KiB
初期監査の検証器
repair7 定義(以前の版識別説明に優先)
registered は deb1bcb、execution_origin は 9767b0a、checker は実際に
実行したcheckerのcommitとbytes、product_target は
{main_anchor, submitted, composed_tree} とする。checkerのSHAを製品版に
代用しない。提出後にしか確定しない自己blob照合は未実施としてRootが検証する。
duty_payments は決算日のpayroll settlement取引のうち、
ShiftInstance.record_duty_minute の勤務recordとstaff_id/day単位で
結合できる取引の件数。期待値は1のまま。独立した通貨項目ではない。
collectorはpayroll行と勤務recordの実rawを結合し、結合不能なら失敗する。
融資の公開返済API repay_loan_principal とledger分類
LOAN_PRINCIPAL_REPAID / financing_principal_outflows は存在する。
自動返済や全UIの完成は主張しない。「融資機構がない」という説明は撤回する。
midnight_replayは同minuteの決算API再呼出しによる実測までpending。 1442完了やservice request再送を1440売上・決算API再呼出しの証明にしない。 shift_completionはapproved-shift-current-r01.gdの1080観測を使う。 D05のEV停止帰属、停電と休業の厳密な順序、費用時点の未確定部分はpending。 全case収集、登録validate、独立whole review、統合準備の順序を維持する。 本修理での試験・engine実行はworkerでは行わない。
repair6 現在値(2026-10-16)
旧値: C全体は native ordering bytes によりblocked、実applicabilityは拒否、
whole native未確認。以下の「今回のPython確認と入力不整合」は旧bundleの履歴。
新値: 補正済み build_dir/audit-support/native-first-current/ に対し
verify_native、ownership/save/ledger個別検査、applicabilityが成功した。
checker_native_fixtures.py、checker_negative_fixtures.py、
checker_applicability_fixtures.py --native-bundle は各1回実行しexit 0。
旧23負例と新2負例(signature行だけのSHA、後続コメントを除いたSHA)を全て拒否。
既存fixture14件も拒否、A/Bの登録版・production版・行移動正対照成功、3負例拒否。
正規bundleを合成補正せず検査し、結果・旧値・新版SHAはc-native-validation.jsonに保存。
全文rawの old == new および
sha256(new[function]) == production_body_sha256 == registered_body_sha256 が必須。
whole gateは未実行。原15条件+EV、7領域、安全性3結果、30/88の分母、予算、
repair上限は変更せず、formal_original_credit=0。正式受入はRunner・独立レビュー・
オーナー判断待ち。以下の旧blocked記述を現在のC検査結果として扱わない。
C段階追補(本節がrepair4以前の状態説明に優先)
verify_native(base) は供給済み native-first-current 形式の有限adapter。
Rootのprobe/Reader/wrapperは起動・再実装しない。A/B、verify、coverage、
boundary_conditions、15条件、reachable EV、7領域、3安全性結果は維持する。
既存scalar検査は宣言の整合性検査として残すが、これだけでは成功しない。
whole gateのindexには追加で native_bundle が必要。
manifest は evidence directory相対の OWNERSHIP_RAW_PROVENANCE.json、
sha256 はその実SHA。manifestの親をbundle rootとして以下を照合する。
絶対パス・親参照・symlinkは既存safe規則で拒否する。
native production_commitはtested HEADと一致させる。別版資料をA/Bの一致だけで
流用しない。今回のproduction版とworker checkoutは区別したまま保持する。
- SOURCE_MANIFESTの76 fileとOWNERSHIP_RAW_PROVENANCEの96 fileは、 各bytesとSHAを実体から再計算する。由来のsource絶対パスは開かない。 3 runのimport/parse/repro、formalのwriter/reader、合計10プロセスは started→process→endedのPID、owner、argv、時刻順、実終了codeを照合する。 execution・phase receipt・actual phase・cleanupのPID集合と埋込記録も一致必須。 stdout/stderr/native logのSHA、通常終了、cleanupのwait結果とerrors空を要求する。 Writer/Readerは別PID・別profileで、profile receipt・環境・5 slotのパスも結合する。
- production_commitは3結果資料とapplicabilityで一致し、specの6登録pinと production Git blobから計算した6 current pinを区別する。各runのsource_beforeと selected_source_mapにも結合する。20関数は既存A/Bと同じ全文raw比較を行う。 後続トップレベルdoc commentを含む抽出全文rawのSHAだけを許可する。 signature行のみ、コメント除外prefix等の候補は許可しない。
observations.jsonの5点と対応midnight-*.jsonを結合する。 receiptはtransaction IDを一意にし、row重複を拒否し、順序・多重度を保持した 台帳差分との完全一致を要求する。Readerの生receipt、first/replayも同じ行に結合する。 SERVICE_SALEにservice_idを要求しない。after snapshotの/systems/runtime/economy/idempotencyのservice.payment.<service_id>から transaction_idを得て、sale・guest wallet・facility revenue・cash sweepを結合する。 固定のPID・価格・transaction番号を使わない。元価格と時間はproduction Gitの facility .tres、run inputのpin、初期facility/service/requestと照合する。 PAUSEDはstateに加えinterruption_reason=RELATED_FACILITY_INACTIVEを要求し、 進捗・service ID・予約IDを保持、売上0、財布差分0を再計算する。 request存在系列、予約requester/facility/ACTIVE→CONSUMED、復帰1回課金を照合する。 最後のGuest despawn時は残存台帳から財布を再計算し、Guest辞書の存在を偽定しない。 maintenanceは同一transaction・施設・金額のaccrual/paymentを対にする。 発生1439と支払い1440は同分扱いせず、観測したmidnightとその直前として照合する。- 正式保存は5点×4member×writer/reader=40実ファイルを照合する。 execution.formal_before/afterの20 member map一致と実SHA/bytes一致を要求する。 typed 14件はwriter-persisted 5、reader-loaded 5、reader-replayed 4(before以外)。 原order-evidence .varおよびrun固定input pinと実SHAを照合する。 .var decodeは行わず、値の判定はnative JSON receipt/stateを根拠とする。
このadapterが返す条件はdependency_stop/recovery_completion/paused_midnightの 有限系列だけ。正式保存member同一性は、全save_restore条件達成を意味しない。 whole gateは固定15条件+EVとこの結果の差集合を未収集としてfailする。 非ゼロ給与×シフト交代×00:00、command再送、停電→閉店同Tick、退出/予約解放、 破壊、EV等をscalar=trueで埋めることはできない。原条件の加点は常に0。
今回のPython確認と入力不整合
供給rawのownership/save/ledger個別検査は成功。applicability資料は
native ordering bytes で拒否する。4関数のbody SHAが複数行シグネチャの
途中までしか含まないためで、詳細はEVIDENCE_COLLECTION.mdに記録した。
実raw全体を合格とは報告しない。
checker_native_fixtures.pyはallowed_paths内の一時コピーで23負例を検査する。 通常の負例ではmanifest SHAも再計算し、hashだけを理由とする失敗を避ける。 1byte改竄、member欠落、PID/profile同一化、ended異常、cleanup欠落、 receipt二重化/削除、PAUSED売上、予約孤立、財布差分、idempotency誤結合、 commit/pin不一致、typed/member変更、scalar自己申告を全て拒否する。 PAUSED売上と予約孤立にはJSON側も同時変更する対抗例を含む。 一時コピーのapplicabilityのみGit全文hashへ差し替えた合成正対照はあるが、 これを正規native証拠として保存・採用しない。
旧synthetic_controlはnative rawを持たないため現在はexit 1が正しい。 既存13負例も維持し、全14件を拒否。A/Bの正対照と3負例も維持する。 本番の未収集indexに対する重複validateは行わない。
repair4差分(未完成・blocked)
今回のA/B実装では、以下の旧説明の「6不変pin=実checkout」および
reachabilityのstart/end/text形式を置き換えた。詳細と未供給入力は
EVIDENCE_COLLECTION.md を参照。Cのowned_outer/raw台帳結合とD/Eの残項目が
未完成のため、このcheckerを正式受入には使用しない。
registered_pinsはspec.current_source_pinsと一致し、登録Git blob SHAをcheckerが再計算する。versionsはexecution_origin(9767b0aの完全SHA)、registered(deb1bcbの完全SHA)、 tested(HEAD)、integration(null)の4キー。candidate_commitもHEADを維持。applicability_deltaは登録版..HEADのautoload/scriptsのGD変更関数の path/function配列。checkerの計算順と完全一致。delta_casesはpath:function→ 条件ID → engine case ID。条件集合はchecker内固定の保守的判定。- 全autoload/scripts GDがsource_map必須で、実checkoutとHEADのraw一致も必須。
- reachability.source_refsはpath/sha256/function/anchor_sha256/line_count。 絶対行位置は使用せず、関数内のraw本文アンカーを一意に解決する。
- 20順序関数は固定抽出規則で登録Git blobとtestedをraw比較する。
Python確認結果: 既存合成正対照1件exit 0、負例13件exit 1。 別のA/B対照は登録=testedと実production Git blobの合法delta(25変更単位)の 2件成功、両版で+7行のアンカー解決成功、delta欠落/境界case欠落/版誤表示の 3負例を拒否した。全てengine証拠ではなくPython検証のみ。 owned/count/restore/別候補receipt流用の新負例は未実装であり、上記に含めない。
以下はrepair3時点の記録。置換対象以外もC修正完了の証明として扱わない。
python3 tools/check_p04_order_evidence.py --verify-only は環境変数 BUILD_OUTPUT_DIR の p04-evidence/index.json を読み、書込み・試験・Runner操作をしない。欠落時は非0。原30/88の受入・完了を確定しない。
D05-P04-DEPENDENCYとD05-P04-SHIFT-1800は承認済み。固定必須条件と証拠が揃えばmachine_verified=true、formal_acceptance=false、exit 0。残るD05の帰属pendingを一括failにしない。必須authority pending・証拠欠落は非0。独立レビュー・通常統合までは正式受入0。
内部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のcase_idとinput/before/operation/afterのartifact_hashesを照合する。caseにもraw_origin=engineを要求する。ログの意味と実行由来の独立確認はRoot/reviewerが行う。 - 各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は失敗。
固定必須条件
checkerのREQUIREDが唯一の必須条件定義であり、indexから条件を受け取らない。conditionsはそのIDと完全一致するmap。各値はcase_id、固定順のauthority_refs、nativeWindows: pending。各条件は指定domainのengine caseと全metricのeq invariantを必要とする。観測はcase.afterの /conditions/<condition_id>/ に置き、invariantのcase_id、artifact_id、pointer、expectedを固定定義と照合する。pass booleanや試験数は使わない。測定値は実際のengine観測から出すこと。手書き合成fixtureはchecker分岐検証専用であり、受入証拠には使用不可。
- 停止課金0: power_stop / destruction_stop / dependency_stop。依存先停止は進捗差分0・予約とservice ID保持も必要。
- 完了・課金1回: shift_completion(1080、交代前)/ recovery_completion / same_minute_replay(再送・重複生成0)。
- 孤立0: closure_release / exit_release / patience_release / paused_midnight。直接休業ではD-034の開始済み継続と待機予約解放を区別。停止日跨ぎは停止中課金0と復帰完了課金各1回。
- 決算1回: midnight_settlement / midnight_replay / save_restore。売上・給与・維持費・勤務分の支払い各1回、非ゼロ給与を必須とし、帰属先は新しく決めない。
- night_staff_absent: 1081、夜番0、WAITING_FOR_STAFF。
- overtime_task: 既存interrupt_level=0の残業と勤務分記録1回(staff_service:1409-1412)。
authorityの参照名はREQUIREDに固定。BASELINE文書、D-034文書、既存A01を記録した入力草案のraw bytesをcheckoutと照合する。A01を再承認しない。承認2条件はauthority typeの同梱D05_OWNER_APPROVAL.jsonと同一SHA256(4583ee9aad45c4db183d72df4420df48aa8e0897e3b5efda13016f0b5cdbd68e)を要求する。origin=direct_user_reply、formal_acceptance=falseと承認IDも確認する。
save_restore条件にはsave_artifact(type=save)とrestore_receiptを追加する。元caseのreceiptのsaved_sha256、readerのrestored_sha256を保存raw hashと照合し、別の正整数PID・終了・exit 0・source/environment一致・stdout/native_logを要求する。保存packageの意味的完全性・正式保存APIの利用は生証拠の独立レビュー対象。
reachabilityはEV/transportのみ。各source_refはpath/sha256/start/end/textで、固定REACH_REFSの経路を全て含み、実際の行本文と一致すること。reason必須。救護搬送は課金予約reach=false。EVはスタッフ移動前予約経路があるためreach=trueとcase_idを必要とする。停電domainのengine case.afterのev.reserved_before_travel=true、power_stopped=true、orphan_reservations=0のeq invariantを要求する。客の到着後予約だけを根拠にEV全体を除外できない。
specは契約文字列hashと照合し、checkoutの末尾LF一つの表現差だけを許容する。その他のraw hashは正規化しない。
worker確認
checker_negative_fixtures.pyはallowed_paths内の一時ディレクトリをBUILD_OUTPUT_DIRに使用し、終了後削除する。py_compile、対照用合成index(exit 0、正式受入false)、指定10負例(各exit 1、対応エラー)を確認済み。実engine試験・Runner操作は0。Runnerがp04-acceptanceを正式実行し、Rootが現版適用性、別セッションのreviewerが生証拠由来と意味を独立確認する。