docs(overhaul): record #475 retail review and test-only fix

This commit is contained in:
Erik 2026-09-05 10:51:54 +02:00
parent 9791cc10cc
commit 3db6546eb4
2 changed files with 34 additions and 0 deletions

View file

@ -198,3 +198,26 @@ listed in the lead's TRX files, plus Release0W0E. Final evidence must supersede
the narrower green return rather than claim that it covered these callers.
Retail/behavior review1 is in progress; reconcile its actual findings in the
same bounded correction before the sequential production/lifetime lens.
Review1 returned FAIL on test/evidence only, with the five failures above
and one non-vacuity finding in the newly added direct Runtime retirement
theory. The lead independently confirmed it: shared `FlatEngine` registers
bare PrefixP, whereas Runtime retirement passes canonical PrefixP|FFFF to
the engine's exact-key removal/demotion. The test's assertion that terrain
remains after withdrawal therefore hid a missed removal. It is NOT the
production withdrawal contract: full withdrawal removes terrain itself.
Correct only that new theory's local setup (the new partial file is already
in scope): install canonical, nonempty collision content and prove it is
resident before mutation; assert real full-withdrawal nonresidency, and real
demotion terrain retention plus indoor-layer removal. Preserve exact first-
admissible-call completion, generation/permission and zero terminal debt.
Do not change the shared fixture or production canonicalization. A targeted
mutation bypassing each actual backend effect must fail the corresponding
postcondition, with raw-byte restoration and final green proof.
This is fix round1, three test files only; production source remains frozen.
The lead's complete hermetic Runtime run additionally confirms the same four
failures and no others:1887/1891, no skips. No additional production issue
was found by the retail/behavior review; its named/paired retail checks match
§4. Production/lifetime review has not yet begun.

View file

@ -4562,3 +4562,14 @@ target-payload allocation bounds plus real Headless held-receipt yield/ACK
proof. No new production defect or broader production change is established.
Artifacts: scratch `artifacts/475-lead/`; retail/behavior review1 is underway.
The narrower return is not integration-ready and no graphical475 PASS exists.
Retail/behavior review1 returned FAIL, test/evidence only. It confirmed the
five obsolete caller expectations and found the new Runtime retirement
theory used a noncanonical terrain key, so its full-withdrawal arm missed the
real removal. Lead source verification confirms the finding; contract§6
adds a local canonical nonempty fixture and effect-discriminating assertions.
The shared fixture and production canonicalization remain unchanged.
Fix round1 is restricted to three test files. The full hermetic Runtime lane
is1887/1891 with only the same four caller failures, no skips. No production
behavior finding; paired retail hashes match. Production review is next
after the corrected return and independent verification.