P28-02-EQ: 意味を保つ軽量化:同等性の先行固定(harness)
This commit is contained in:
@@ -577,3 +577,133 @@ failures respectively; all earlier evidence remains unchanged.
|
||||
|
||||
This table records the required implementation targets, not completed validation.
|
||||
No native or formal validation is authorized for this worker.
|
||||
|
||||
|
||||
## S5 implementation (repair 10; EQ_S5_SCALE_PLAN r01/r02)
|
||||
|
||||
Implemented by Claude Opus 5.5 in the Desktop control session after the user moved
|
||||
implementation from Codex to Opus. The exact-S native of 6f75c9a failed in R-A and stays a
|
||||
failure; this stage fixes the harness defects that only the real engine exposed and makes
|
||||
the full R scope (E1-E5, 39 scenarios) fit the unchanged limits. All earlier text below and
|
||||
above this section is retained history.
|
||||
|
||||
### Defects found only by the real engine (scratchpad diagnostics, not formal evidence)
|
||||
|
||||
- write_evidence created `user://evidence` with the user:// path. Under the guard's runtime
|
||||
user-dir switch this fails; the directory is now created from the globalized path, as the
|
||||
RESTART helpers do.
|
||||
- typed_info encoded get_typed_script(), a null Object for unscripted typed containers, as an
|
||||
unsupported Variant 24. It is now transported as NIL ([0], which the Python side already
|
||||
required); a scripted element type still fails.
|
||||
- Package manifest mutation re-serialized a JSON-parsed manifest. Godot parses every JSON
|
||||
number as float, so untouched integers became 390.0, 1.0 and so on. Only the one key line is
|
||||
now edited as text; the Python rule already rejects any other change (new negative test).
|
||||
- The guard receipt was recorded after JSON parsing, with the same float problem. The exact
|
||||
receipt text is now kept beside it; Python parses that text strictly, compares it with the
|
||||
independently saved guard file and binds its SHA.
|
||||
- Godot instance IDs are signed 64-bit and RefCounted IDs are negative. The cache identity
|
||||
check accepts the sign. Raw values stay in raw; only the SPEC 3.2 exclusion (process-local
|
||||
instance ID) is applied across PIDs, with both values and the reason recorded.
|
||||
- A large E4 return is a blob; its ok/code facts are taken from the live return value.
|
||||
- After the first harness error, later scenarios are no longer run (the run already failed).
|
||||
|
||||
### Product behavior recorded as an existing defect, separate from harness capture
|
||||
|
||||
autoload/simulation_runtime.gd:788 and :1346: a successful restore replaces domain_events
|
||||
with a new DomainEventStream and does not carry subscribers. The probe's wildcard
|
||||
subscription stayed on the old stream after E4 restore, so SAVE_LOADED and all later events
|
||||
were not delivered. follow_event_stream() runs after every E3 call and after E4 restore and
|
||||
load. When the stream changed it records the new stream's subscriber IDs (no instance IDs),
|
||||
recovers the unobserved events from recent_events() in publication order, and subscribes to
|
||||
the live stream again. check_e3/check_e45 record event_stream_replaced_subscribers_not_carried
|
||||
as an existing defect (never PASS). Completeness is still proven only by the counter delta,
|
||||
the published_ids delta and the actual event IDs; an event outside the 256-entry
|
||||
recent_events window would remain missing and fail. lifecycle.event_stream_replacements must
|
||||
equal the per-scenario facts. No event is renumbered, no product file or hook is changed.
|
||||
|
||||
### Evidence representation (complete and reversible)
|
||||
|
||||
- Trees larger than 64 KiB, raw S/K/C bytes and package files are written once as
|
||||
evidence/blobs/<sha>.gz, named by the SHA-256 of the uncompressed bytes; records hold
|
||||
{"blob": sha}. Small trees stay inline. lifecycle.blobs lists every blob with its size,
|
||||
compressed size and compressed SHA; verify_eq binds that list to the files exactly and
|
||||
decompresses every blob to check name and size.
|
||||
- Godot's JSON text of a tree equals json_bytes(tree) (checked on the R fixture tree), so a
|
||||
blob name is the tree SHA. var_to_bytes distinguishes typed metadata, String/StringName,
|
||||
int/float and key order (checked in the engine), so transport reuses the proof for equal
|
||||
bytes. Every checkpoint carries a complete tree; the diff chain is gone (tree_diff took 5.4 s
|
||||
per R checkpoint). Report and lifecycle hold references only, which removes the memory and
|
||||
swap growth seen in the failed native.
|
||||
|
||||
### Python: same results, less work
|
||||
|
||||
- A blob is accepted only when its uncompressed bytes hash to its name, and its tree is used
|
||||
only after the full validate_tree (types, arity, metadata, keys) has passed on first use;
|
||||
only then is its SHA recorded as valid. A failed blob is never recorded and fails again.
|
||||
A matching SHA is never taken as proof of types (Root's repro of [2, true] / [24, 0] in a
|
||||
correctly named blob is a regression test). Valid blob trees are shared, never mutated;
|
||||
checkpoints are loaded one at a time. Equal SHA means equal; otherwise Python == decides, which is exact JSON equality for
|
||||
validated trees (INT/BOOL payloads are int, floats are 16-hex strings).
|
||||
- Normalization runs the original closed policy unchanged on a skeleton holding only
|
||||
systems.runtime.domain_events.recent_events, read directly from the tree text. The rest of
|
||||
the text is proven free of the profile root, the reserved token, _us/_ms names and
|
||||
save_service; otherwise the original full walk runs. Restore runs the original reversible
|
||||
check on the skeleton.
|
||||
- normalized_digest builds the same canonical JSON without per-node copies and is memoized by
|
||||
SHA (17.4 s to about 1.2 s on an R tree, identical value).
|
||||
- Expected inputs, X(B, event) and the E5 expectation copy only the dictionaries on the
|
||||
changed path. Large derived trees are recorded by SHA descriptor in joined facts and checker
|
||||
results; compare_reports rebuilds them from the blobs when SHAs differ.
|
||||
- test_eq.S5 proves equivalence against the retained S1-S4 algorithms (compare_trees,
|
||||
canonical digest, deepcopy builders, original normalization including violations, tokens and
|
||||
non-array recent_events), that every one of 31 blob checkpoints is verified alone exactly as
|
||||
inline trees, and the new static requirements (full snapshot transport, blob write, gzip
|
||||
roundtrip, overwrite refusal, stream following).
|
||||
|
||||
### Snapshot signal rule corrected (EQ_S5_SCALE_PLAN r03)
|
||||
|
||||
The S3a rule "exactly one snapshot_published/state_updated pair per measured minute" was a
|
||||
harness assumption. Paused submits publish once each after their command events
|
||||
(simulation_runtime.gd:486-493, :508-512, :5768-5793), besides the tick-end publish (:1745-1749)
|
||||
and a successful restore (:1473); R minute 648 had 50 commands and 51 pairs (the r2 check
|
||||
failure on the old rule is retained). The probe now stores, per signal, the domain_event
|
||||
counter and _next_command_id at emission (read only). check_publishes orders signals and
|
||||
events together and requires: complete pairs with equal counters; a command publish after
|
||||
exactly one submit whose command is in its trailing batch; no submit before any other publish
|
||||
and none left unpublished; every command event covered; and the remaining tick/restore
|
||||
publishes equal to the operations performed (one per measured minute; E3 successful
|
||||
restores; E4 1/1/1/1/1 with build only when applied; E5 2 or 3). Missing, extra and reordered
|
||||
pairs, including a missing publish between adjacent commands, fail. Actual counts stay raw and
|
||||
signal_order is compared exactly across versions.
|
||||
|
||||
### Python speed, measured on retained R raw (r3, scratchpad diagnostic, not formal)
|
||||
|
||||
One R phase checked in the phase_evidence order (lifecycle, observations, check_report,
|
||||
join), with full stdout/stderr and Python's own exit kept for every run:
|
||||
1270.3 s (first S5 code, with concurrent profiling) -> 552.9 s (memo of identical inputs,
|
||||
copy-free builders) -> 301.8 s (labelled digest, parse-free restore, copy-free diffs) ->
|
||||
259.7 s (facts derived at first parse) -> 58.3 s (cyclic GC off inside memo_scope; before
|
||||
the blob validation fix, so not used as a result). With full blob validation, r3 + r4 checked
|
||||
in one process took 136.5 + 132.0 s and their comparison 4.2 s with 0 differences; with the
|
||||
validate_tree rewrite (same checks, messages and order; 4000-case differential test against
|
||||
the S1 version) four phase checks in parallel processes took 131 s wall (R 111.9 / 112.1 s,
|
||||
O 5.9 / 6.2 s), all ok. verify_eq therefore runs the four phase checks in parallel worker
|
||||
processes of the same verification and does the same-role comparisons in the parent with the
|
||||
workers' validated SHAs and normalization facts; the result equals the sequential mode, which
|
||||
remains the fallback and the mode used by unit tests. The unchanged 300 s native-verify
|
||||
limit is kept; the Runner configuration is not changed.
|
||||
|
||||
- memo_scope: inside one verification call, identical check inputs (SHA of the exact JSON)
|
||||
are checked once; check_lifecycle and check_report shared E3/E45/measurement work. It
|
||||
also turns cyclic GC off for its duration; typed trees are acyclic lists, results do not
|
||||
depend on GC, and GC is restored on exit.
|
||||
- The joined harness digest is labelled `normalized-sha256:` (SHA of the exact normalized
|
||||
JSON, computed by splicing the normalized events into the blob text). compare_reports
|
||||
compares labelled digests exactly and, only when two differ, compares the canonical
|
||||
(dictionary-order-insensitive) digests; equal canonical digests are reported as
|
||||
dictionary-order-only, otherwise the difference is recorded. checker.normalized_digest
|
||||
remains the canonical digest (same values as S1).
|
||||
- Normalization facts, counters and next_command_id are derived when a blob tree is first
|
||||
parsed and memoized by SHA; restore uses the memoized skeleton, so join and comparison do
|
||||
not parse again. compare_trees records nodes shared with the immutable trees instead of
|
||||
deep copies; keys use inline text.
|
||||
|
||||
Reference in New Issue
Block a user