The round-16 sweep went 49 GREEN, 1 RED, and the RED was this repository's
Phase 4 refusing to run: PACTA SUBJECT MISMATCH, signing.py and
transparency.py differing from the pin. That is pacta-subject-unpinned
(round-8, GPT-5.6) firing on its first genuine drift — the gate built so that
fidelity could never again count agreement with an unnamed program.
The drift is known and intended: pacta 5e35a53 anchored the signer path to the
package (register: signer-backend-depends-on-cwd) and a036624 added the
additive slh_dsa block to make_signed_tree_head (operator decisions
2026-08-06). Re-pinned deliberately with pacta_pin.py --write: 5 modules at
pacta a036624. PACTA-PIN.sha256's own entry in HARNESS.sha256 updated.
Full instrument set re-run green at the re-pinned state: check.sh 92s,
selftest_audit 280s, selftest-harness 0s, selftest_statements 38s.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Two round-7/8 findings, both closed here.
`acc-exit0-fidelity` — CRITICAL, raised INDEPENDENTLY by both reviewers
(Claude F1, GPT-5.6 F10) and lost from the round-8 work list by the F-number
collision the finding register now prevents.
check.sh emitted a careful pair of markers — ATTESTATION GREEN only when
fidelity actually ran — and then returned 0 either way. The marker discipline
was right; the exit code contradicted it. A caller doing the obvious thing
./check.sh && append
read success from a run whose own last line said NOT attestation-ready. And
because pacta is not part of this estate, the skip branch is the ONLY branch a
third party ever takes: for everyone but the author the button always returned
0 without ever checking definition fidelity. Reproduced here before fixing —
PACTA_SRC=/nonexistent ./check.sh printed "FIDELITY NOT RUN" and exited 0.
An exit code is what programs read. The contract is now:
fidelity ran exit 0 ATTESTATION GREEN
SKIP_FIDELITY=1 exit 3 explicit opt-out, distinguishable, not success
pacta absent exit 1 nobody opted out; a real failure to establish
the property the button exists for
All three verified. The self-tests are unaffected: every SKIP_FIDELITY case
already expected a non-zero exit and asserts on a diagnostic from an earlier
phase, and the control compiles modules directly rather than invoking check.sh.
29 assertions across the three self-tests, all green.
`pacta-subject-unpinned` — HIGH, GPT-5.6 round 8.
Phase 4 compared this repository's Lean definitions against "the deployed
verifier" by importing whatever sat at $PACTA_SRC — no repository, no commit,
no clean state, no hashes. It pinned the fidelity OUTPUTS while leaving the
SUBJECT anonymous, so any program producing the same finite family of answers
passed, and the recorded result named no version of the thing it agreed with.
fidelity/pacta_pin.py pins the transitive set of pacta modules the harness
ACTUALLY LOADS — discovered by importing its entry point and reading
sys.modules, a membership property rather than a directory glob. A glob would
pin files the comparison never touches and miss anything loaded from elsewhere;
this estate has been bitten by name-shaped measurement before. Five modules at
pacta cd3b1bc — the same checkout the reviewer independently recorded.
Negative-tested, all three rejected by name: tampered bytes, a module loaded
but absent from the pin, and the pin file deleted. Refusing to pin a dirty
pacta tree is also enforced — a pin taken over uncommitted edits names a
subject nobody else can obtain.
PACTA-PIN.sha256 joins HARNESS_EXTRA. It is not executable, so it would
otherwise have sat outside the harness set, and a subject pin an attacker may
rewrite pins nothing — the same shape as the forgeable .audit-basis that
remains open as `auditonly-basis-forgeable`.
This does not widen the claim: byte identity of a source tree is not proof the
deployed service runs it, and finite-family agreement is not extensional
equality. It names the subject.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
