P04-01: 同時発生の更新規約
This commit is contained in:
@@ -1,177 +1,52 @@
|
||||
# 初期監査の検証器
|
||||
# Current checker protocol — repair22
|
||||
|
||||
## repair7 定義(以前の版識別説明に優先)
|
||||
Source preparation, NOT RUN. ORDER_AUDIT.md and order-audit.json are the single
|
||||
current seven-domain table. REPAIR17–21 remain untouched historical records;
|
||||
their current-status and B1 power-credit claims are superseded.
|
||||
|
||||
registered は deb1bcb、execution_origin は 9767b0a、checker は実際に
|
||||
実行したcheckerのcommitとbytes、product_target は
|
||||
`{main_anchor, submitted, composed_tree}` とする。checkerのSHAを製品版に
|
||||
代用しない。提出後にしか確定しない自己blob照合は未実施としてRootが検証する。
|
||||
The registry remains exactly15 conditions + EV. No accepted originals, counts,
|
||||
CurrentAlphaScope, three safety outcomes or30/88 denominator change. Original
|
||||
13/88 gains no credit. P04 main9b stays frozen; no integration is claimed.
|
||||
|
||||
`duty_payments` は決算日のpayroll settlement取引のうち、
|
||||
ShiftInstance.record_duty_minute の勤務recordとstaff_id/day単位で
|
||||
結合できる取引の件数。期待値は1のまま。独立した通貨項目ではない。
|
||||
collectorはpayroll行と勤務recordの実rawを結合し、結合不能なら失敗する。
|
||||
C's NATIVE_RUNS / native_ownership / verify_native block is unchanged. C25 and
|
||||
all existing fixture cases remain. R's verify_shift_completion derives three
|
||||
distinct process IDs from the existing raw start/process/end joins, with all
|
||||
end flags, exit0 and complete SHA checks retained. The one1080 SALE joins the
|
||||
original serviceID and priceSnapshot via service.payment.<serviceID>, actual
|
||||
receipt entries and idempotency transaction ID; no fixed PID or ledger number.
|
||||
|
||||
融資の公開返済API `repay_loan_principal` とledger分類
|
||||
`LOAN_PRINCIPAL_REPAID` / `financing_principal_outflows` は存在する。
|
||||
自動返済や全UIの完成は主張しない。「融資機構がない」という説明は撤回する。
|
||||
S1 uses the full existing writer-<case>-observations Variant data in
|
||||
B/p04-s1-native-r02. The pre-travel ACTIVE reservation, requester/task, assigned
|
||||
staff and original staff_cell join the later boarded task and trip. Reserve
|
||||
exhaustion is measured before the normal tick, and depleted raw must show
|
||||
mana0 and the actual elevator unpowered. JSON summaries do not replace typed raw.
|
||||
|
||||
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では行わない。
|
||||
S3 B1 remains a combined dependency/closure diagnostic. Its actual interruption
|
||||
reason is RELATED_FACILITY_INACTIVE. It supplies no power_stop evidence and no
|
||||
priority approval. The strict power-vs-closure order is D05 pending/unknown.
|
||||
|
||||
## repair6 現在値(2026-10-16)
|
||||
Only S4 supplies power_stop. The new verifier requires source-pinned native
|
||||
ownership, complete product1338 + sole QA override, three whole4-member formal
|
||||
packages per process, separate Writer/Reader, exact Runtime typed restoration
|
||||
and full typed replay. Actual NO_POWER, operating dependency, powered/ACTIVE
|
||||
kitchen, positive mana and open operator are mandatory. Raw graph edges and
|
||||
revision prove the isolated consumer and exact reconnect; source-derived
|
||||
evaluation/hold determines recovery. Duration−1, zero stopped charges, original
|
||||
service/reservation identity, one SALE and unchanged replay are joined from raw.
|
||||
Every intervening held minute is retained and checked. No normalization or
|
||||
dropped Runtime fields is allowed. S4 is pending Root execution, not accepted.
|
||||
|
||||
旧値: 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検査結果として扱わない。
|
||||
checker_join_fixtures retains every previous case and adds rejection controls
|
||||
for B1 masquerading as power, dependency false, kitchen unpowered, closure,
|
||||
pre-travel mismatch, absent outage, wrong PID and transaction join. Consistently
|
||||
renamed dynamic PID/transaction/service IDs are positive controls. These fixtures
|
||||
have NOT RUN. They require actual S4 raw for the S4 positive control.
|
||||
|
||||
## 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。
|
||||
|
||||
内部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`、raw `stdout/native_log` artifact 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>/<metric> に置き、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が生証拠由来と意味を独立確認する。
|
||||
The fresh R collection is B/audit-support/p04-raw-collect-r22. It re-reads existing
|
||||
C/S1/S2a/S2b/S3 without native reruns and newly collected S4; no result scalar is
|
||||
authority. It binds the current verifier hash. The old r17/r20 collection and
|
||||
21615-check proof remain immutable. New checker bytes differ; no1339 identity
|
||||
claim. Missing raw, changed pins, mandatory undefined rules or unsupported
|
||||
joins must fail. Final index/applicability, registered validation, support53cb
|
||||
registered rebind, independent review, normal integration and individual
|
||||
nativeWindows obligations remain Root work. No final acceptance is asserted.
|
||||
|
||||
Reference in New Issue
Block a user