P28-02-EQ: 意味を保つ軽量化：同等性の先行固定（harness）

2026-10-22 06:42:29 +09:00
parent a46418d064
commit 9adbbee334
16 changed files with 6682 additions and 33 deletions
@@ -721,3 +721,69 @@ read-only directory and its copy has the recorded bytes and SHA). The engine (/A
 the machine model stay read live. Everything else verify_eq recomputes from the bundle and the
 checkout as before.

+## S6 implementation (repair 12; EQ_S6_AFTER_VERSION_PLAN)
+
+Implemented by Claude Opus 5.5 in the Desktop control session (user delegation). Repair for
+the independent review of S a46418d (changes_requested: EQ5). All earlier text is retained.
+
+### The after version through the frozen harness (EQ5, high finding)
+
+- `BEFORE_SOURCE_MAP.json`: the registered base product source map, 1407 rows of
+  `{bytes, sha256}`, written from `collector.source_map` of the S_eq checkout. Its meaning is
+  fixed by the existing `SOURCE_SHA`; `compare_versions.before_source_map()` rejects duplicate
+  keys, row shape errors, a different row count and any digest other than `SOURCE_SHA`.
+- `compare_versions.admit_source(source, registered)` is the single admission rule of both
+  versions. `registered` must be a sorted duplicate-free list. It runs
+  `check_source_closure(before_source_map(), source, registered)` and returns the closure with
+  `version` (before when `registered` is empty, otherwise after) and `after_sha256`. The before
+  version is exactly the old `SOURCE_SHA` requirement; the after version needs the changed set
+  equal to `registered` (a subset of `OPT_PATHS`), with no added or missing source.
+- `run_eq`: `--opt-changed PATH` (repeatable, sorted by main, duplicates rejected by the rule).
+  `actual_pins(..., registered)` records `registered_changes` and `source_closure`; the
+  admission records `version` and `measured_source` (`verify_eq.MEASURED`: before
+  `S_eq-native-not-Q`, after `S_opt-native-not-Q`, OPT_CONTRACT_T1 §5); `pins_after` is
+  recomputed with the same registration. The EQ file pins (`worker`) and `frozen_commit`
+  include `BEFORE_SOURCE_MAP.json` (`verify_eq.DATA_NAMES`).
+- `verify_eq.recompute` replaces the `SOURCE_SHA` line with `admit_source` on the recorded
+  map and registration and requires the recorded closure, version and label exactly;
+  `verify` passes the recorded registration to `actual_pins` on the checkout. The result
+  carries `measured_source`, `version` and `registered_changes`.
+- `verify_eq.py --compare-versions --before <bundle> --after <bundle>` (`compare_bundles`):
+  the bundle-level entry of the two-version comparator (SPEC §2, §3.2; OPT_CONTRACT_T1 §2-§4).
+  Both seals, passed executions, admission copies, versions, closures and labels are checked
+  again; every non-product pin (`dependencies`, `frozen`, `worker`, `fixture`, `engine`,
+  `engine_version`, `readonly`, `original_manifest`, `machine`, `platform`) must be equal; the
+  sealed joined reports of R-A and O-A are compared by `compare_reports` (differences,
+  exclusions, digest modes and violations all returned); the stored checkers' existing-defect
+  scenarios of both versions are listed and `after_all_e_pass` reports whether the after
+  version has none (the OPT acceptance judges it). Each bundle's raw recomputation, same-role
+  determinism and checkout pins are proven by that version's own native-verify.
+
+### Low findings
+
+- `eq_probe.gd` E5 detail: `latest_digest_dirty_before` is `runtime.get("_latest_digest_dirty")`
+  read just before the operation (null if a version has no such field), replacing the constant
+  `digest_materialized_before: true`. The checker accepts only `false` or `null`.
+- `run_eq.bundled_inputs`: the bundled manifest must have `ROOT_MANIFEST_SHA` (the value
+  `collector.inputs` fixes; a unit test checks the literal in the collector source), and each
+  destination string must be absolute and already normalized (`os.path.normpath`) inside the
+  read-only directory. This is textual because the sandboxed verification cannot read the
+  originals; the run checks the resolved originals through `collector.inputs`.
+- `verify_eq.seal`/`check_seal`: bundle schema `p28-02-eq-bundle-v2` with `directories`, the
+  sorted list of every directory (empty `<phase>/startup-profile` included). A file-only copy
+  of a sealed bundle now fails the seal check itself.
+
+### Tests and evidence kinds
+
+- 17 engine-free tests in `S6SourceClosure`, `S6Admission`, `S6Bundles` and `S6SealAndProbe`.
+  `S6Bundles` builds one sealed before and one sealed after synthetic bundle per class with
+  the real parallel recompute, compares them unmocked, and tampers APFS clones (`cp -c`) only;
+  the real state difference is a changed K value in the after R-A report. The main test in
+  `S6Admission` mocks `actual_pins` only to read the registration passed by main.
+- Diagnostic, not formal: `EQ_S6_AFTER_ADMISSION_DIAG_R01` (Root control folder) ran the real
+  `run_eq.py --check` on a throwaway after-version checkout; the admitted and rejected cases
+  and their exits are in its SUMMARY.json.
+- The first S6 bundle tests copied 709 MB synthetic bundles with `shutil.copytree` and ran
+  out of disk space during a class-targeted run (not retained); they now use clones.
+- Full local run UNIT_OUTPUT_S6_ATTEMPT_01: 179 tests OK in 207.351 s, exit 0.
+- Local run under the Runner validation seatbelt profile, UNIT_OUTPUT_S6_SEATBELT_01: 179 tests OK in 206.326 s, Python exit 0, outer 207.695 s.