P04-01: 同時発生の更新規約

This commit is contained in:
Agent Control Runner
2026-10-16 01:54:03 +09:00
parent 9767b0a28c
commit 5475391647
8 changed files with 1752 additions and 17 deletions
@@ -1,5 +1,120 @@
# 初期監査の検証器
## 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は区別したまま保持する。
1. 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のパスも結合する。
2. 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等の候補は許可しない。
3. `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とその直前として照合する。
4. 正式保存は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。