06 — P5 / P6 EVIDENCE REVIEW

P5

The exact oracle remains safe: accepted invalid input=false; unexpected exception=false; exact code/state only; total=9/pass=9/fail=0/accepted=0/residue=3 fatal gate.

P6 digest

Combined vocab+harness digest and atomic SHARE-locked persistence are correct.

Blocking false-PASS path

• P3: ledger insert line 65; COMMIT line 66; exact-set fatal gate lines 68–81.
• P4: ledger insert line 23; COMMIT line 24; exact-set/invariant gate lines 26–42.
• P5: ledger insert line 51; COMMIT line 52; fatal gate lines 57–69.
• P6: upstream proof is only EXISTS on those ledger ops (lines 49–54), plus count=3/validated=3; it does not recheck exact expected operation codes/invariants.

Static counterexample: an active sandbox contains three valid-shape rows including C1.READ_BALANCE but missing one expected code. P3 rejects after committing its ledger; P4 validates rows then rejects after committing its ledger; P5 can pass its matrix; if the caller continues, P6 sees all ledger rows, 3 validated rows and 9/9 harness, then commits digest/PASS for the noncanonical set.

Required: keep each fatal gate in the same transaction before its DONE ledger and COMMIT, or add an explicit post-gate success stamp. P6 must require those success stamps and independently verify the exact canonical set/invariants.