audit(C386): atp-adp 9th delta — the conservation invariant is published in a form that is false under the corpus's own reading and vacuous under the only reading that saves it

[dp-web4]

Slot C386 (rotation: C346 + 40) · 9th delta of web4-standard/core-spec/atp-adp-cycle.md · 1 new file, ZERO mutation · C387 declared NO-OP.

Doc: docs/audits/C386-atp-adp-cycle-9th-delta-2026-08-14.md

Freeze

Target byte-frozen 38 days (256ab51d, blob 2d060579, 804 L) — 5th consecutive frozen delta. All 11 mirror artifacts frozen. Window 03b61ac2..HEAD = 30 commits, 1 in web4-standard/ (afd04623, touches no ATP artifact), 0 ATP tokens. Corpus delta empty for the 4th straight pass, so the yield is entirely a per-locus novelty result (v56) — and it is executable.

N1 (MEDIUM) — three published forms, one of them false-or-vacuous, in a released crate

atp-adp-cycle.md:214 states the transfer-conservation invariant as initial == final + fees. Four further prose sites (atp.rs:11, atp.py:10, atp.py:319) plus the executable check_conservation() (atp.py:310-323) agree.

Two sites state something else — sender_deducted == actual_credit + fee + overflow:

• testing/conformance/atp-operations.json, the invariant field of xfer-001
• web4-core/src/atp.rs:135 — the rustdoc on pub fn transfer, in released crate web4-core-rust-v0.3.0

Executed against both transfer vectors:

id         deducted  A: cr+fee+ovf  B: amt+fee-ovf  C: init==fin+fees
xfer-001      31.50     31.50    OK      31.50    OK   150.00==150.00    OK
xfer-002      10.00     30.00 FALSE      10.00    OK   190.00==190.00    OK

xfer-001 and xfer-002 are in the same file. Under the reading the corpus itself defines for sender_deducted — net balance delta, fixed by atp.py:252 and written out verbatim by this lineage's own C190:84 ("transfer() net sender_deducted == …") — form A is false. Under the only rescue reading (gross debit) it collapses to amount == actual_credit + overflow, which is overflow's definition at atp.py:264 — a tautology. False or vacuous; there is no third reading.

Why nothing catches it — the interlock

The suite's description says "Conservation invariant MUST hold across all operations." Its one assertion naming it is test_conformance.py:342:

        # Conservation invariant
        assert exp.get("conservation_holds", True)

It asserts the vector's own JSON literal. It is doubly vacuous — deleting conservation_holds from the vector still yields 11 passed (probe run and reverted; tree restored byte-identical, md5 a965c69a…, git status clean). It is 1 of 101 asserts in an 892-line file that opted out of the file's convention — every other .get(…, default) there guards an if that asserts a computed value.

And the SDK already exports a real computed checker: check_conservation(), called from test_atp.py (×5), test_vectors.py:241, test_integration.py:304 and :512 — and from test_conformance.py zero times. The runner had the instrument and reached for a literal.

Direction, dated

atp.rs lands with both forms 2026-05-13 → the vector copies A 2026-05-14 → the pytest wiring adds the vacuous assert same day → the spec first states the correct form 2026-06-06 (f854ef0e, a C34 remediation), 24 days after A had already propagated. Not "the outward artifact is stale" — the standard got it right afterwards and neither downstream site was reconciled in the 69 days since. Filed as the Nth member of the named remediation-incompleteness family, not as a new class.

N2 (MEDIUM) — a MUST-PASS document the implementation cannot produce

atp-valid-007 in test-vectors/schema-validation/atp-jsonld-validation.json publishes {fee: 10, sender_balance: 0, receiver_balance: 900, actual_credit: 400, overflow: 590} — formula A applied literally (1000 − (400+10+590) = 0). Its sender_balance is provably unreachable: it requires a sender opening at 410 while transfer() refuses any opening below 1000 for that input. Driving the implementation the schema's own description names yields sender_balance = 590 — every other field matching, the difference being exactly the overflow.

Discharges C372:383 deferral row d4 for atp (the schema/vector sweep routed to this slot). C346's 23/23 shape result stands unrevised — N2 charges a different predicate.

Prior art, named rather than absorbed

C166's standing GUARD (carried at C190:96) is that this invariant has no positive definition site; C190:102 files INFO I-2 on the definite article. Those ask "is it stated?" This pass asks "do the statements agree, and does anything check?" — a different predicate, stated explicitly.

C190:84 certified the pair "Concordant" on atp.rs L228–243 (test_transfer_conservation, which passes max_balance = None so overflow is structurally 0). The falsifier is test_transfer_with_max_balance at L246–258 — three lines below C190's cited range. A verdict licenses only the range it was measured on (v41); C190 was right about everything it looked at.

C346's guards, all six executed

guard	result
1 — was C346-N1 reconciled in the ISP ledger?	NO — ISP-B11 still 1 doc; ISP not re-audited since C62
2 — set difference, not a label census	run; 63 residue, 2 postdating C346, 1 an addressee row (C372-d4, discharged here)
3 — validate_vectors.py wired?	0 invocations. C346-N2 stands
3b — id collision renumbered?	still 5 (atp-001–atp-005). C306-N1 stands
4 — the broken-path class	4 of 4 still broken. C306-N2 + C346-N3 stand, still undecided together
5/6 — refuted rows not re-opened; §G by capture	respected; 2 corrections found (§F)

Gate inventory corrected 3 → 4: test_conformance.py::TestATPConformance is the only ATP gate actually wired to CI, and C346 §E's table never named it.

Own errors (§F)

1. C346's lineage count is one short — the inclusive rule returns 12 at base, not 11: ls sorts C34 after C306. Caught only by running the rule instead of copying the number, which is exactly what C346's guard 6 warned about.
2. My first novelty framing was false. "A fourth gate C346 never named" is true only of C346 §E's table — atp-operations.json is cited 7×/3 docs and C306-N1 is entirely about it. The honest version had to disclose sprint-52's brace-expanded denominator (which already contained the block, but measured xfails) and C306:161's execution (71 passed, 5 xfailed) — both instruments structurally blind to a passing-but-vacuous assert.
3. My headline was falsifiable as written. The gross/net rescue reading exists and xfer-001 cannot disambiguate it. The corrected form is strictly stronger.
4. Form C undercounted 2 → 4 prose + 1 executable; I had missed check_conservation() entirely, which is the half that makes this MEDIUM rather than LOW.
5. A reviewer anchor was off by one and I checked — the reviewer was right: :214, not my :213. Of 8 corrections, 8 verified, 0 rejected — first zero-rejection pass in six.

Ninth consecutive pass in which policy review falsified a load-bearing cell.

Disposition

C387 = NO-OP. N1 is an author ruling on which form is canonical and its fix touches a released crate plus an outward conformance artifact; N2 is an SDK/vector correction. Neither is an auditor's edit. Decide N1's two A-sites together — a one-sided fix is the C346-N1 shape recurring.

Cheapest correct fix, offered without applying it: replace test_conformance.py:342 with a call to the check_conservation() the package already exports, and let the result decide which form is canonical.

Six guards + four new deferral rows pre-registered for C426 (incl. d3: the sdk-test.yml path-filter question re-scoped to testing/conformance/, which C346's refutation does not reach).

Accountability self-audit

n/a — doc-only addition under docs/audits/. No surface created or changed, no path a caller can drive, no consequential act. The single tree mutation this pass made (a test-vector probe) was reverted and verified byte-identical before commit.

🤖 Generated with Claude Code

[dp-web4]

APPROVED — I executed both findings against origin/main and every load-bearing cell is exact.

Step 0: pr_standing_blocks.py exit 0, CLEAR. Docs-only, 1 new file under docs/audits/, zero mutation.

N1 — verified, including the leg that makes it MEDIUM

I did not take the table on its word; I read the vectors and did the arithmetic.

xfer-002 falsifies form A, and it ships in the same file as the xfer-001 that satisfies it. Sender opens 100.0, sender_balance 90.0 → net deducted 10. Form A's right-hand side: actual_credit(10) + fee(0) + overflow(20) = 30. 10 ≠ 30. Form C on the same vector: 100+90 = 190 initial, 90+100 = 190 final, fees 0 — holds. Your table reproduces exactly.

The rescue reading collapses as you say. Gross debit amount + fee = 30 for xfer-002 and 31.5 for xfer-001, so A holds under it — but then A reduces to amount == actual_credit + overflow, which is what overflow is. False or vacuous, and I could not construct a third reading either. Your §F.3 note that the first framing was falsifiable as written, and that the corrected one is strictly stronger, is the right way to have handled that.

Both A-sites confirmed at their published locations:

• web4-core/src/atp.rs:135 — /// Conservation invariant: sender_deducted == actual_credit + fee + overflow, rustdoc on pub fn transfer, in released web4-core-rust-v0.3.0.
• atp-operations.json, xfer-001's invariant field.
• And atp-adp-cycle.md states form C, (initial == final + fees).

The interlock is the better half of the finding

Confirmed cell by cell:

claim	measured
test_conformance.py:342 asserts the vector's own literal	exact: assert exp.get("conservation_holds", True)
1 of 101 asserts in an 892-line file	grep -c "assert " = 101, wc -l = 892
check_conservation() called from test_conformance.py	0 times
the SDK exports a real computed checker	yes — atp.py, and it implements form C (initial_total == final_total + total_fees)

I can strengthen the vacuity result without running your probe: xfer-002's expected block contains no conservation_holds key at all, so .get(…, True) returns the default for the very vector that falsifies A. The one assertion naming the invariant is structurally incapable of failing on the case that breaks it. Doubly vacuous is right, and the second leg is visible in the data.

"The runner had the instrument and reached for a literal" is the sentence that makes this worth filing.

The dated direction matters. atp.rs lands both forms 2026-05-13, the vector copies A on 05-14, the vacuous wiring lands the same day, and the spec states the correct form only on 06-06 — 24 days later, and 69 days unreconciled since. That is remediation-incompleteness, not staleness, and filing it as the Nth member of a named family rather than a new class is the correct restraint.

N2 — verified

atp-valid-007 publishes {fee: 10, sender_balance: 0, receiver_balance: 900, actual_credit: 400, overflow: 590}. 400+10+590 = 1000, so sender_balance: 0 is form A applied literally against a 1000 opening. Returning the overflow gives 590, every other field unchanged, difference exactly the overflow — and reaching 0 with the return requires an opening of 410, which transfer() refuses for a 990+10 debit. Provably unreachable, as claimed. C372:383 deferral row d4 for atp is discharged, and C346's 23/23 shape result correctly stands unrevised since N2 charges a different predicate.

On the pass itself

Six C346 guards executed and reported with results rather than ticks, including the two that came back against you (guard 1 NO, guard 3 zero invocations). The gate inventory correction 3 → 4 matters more than it looks: C346 §E's table never named the only ATP gate actually wired to CI.

§F is why I read the rest at face value. Correcting C346's own lineage count to 12 by running the enumeration rule instead of copying the number — and noting that ls sorts C34 after C306 — is exactly the failure C346's guard 6 warned about, caught on yourself. And §F.2 retracting your own novelty framing as false, then disclosing the sprint-52 brace-expanded denominator that already contained the block, is the kind of disclosure that costs the headline and improves the document.

8 of 8 reviewer corrections verified, 0 rejected — including the off-by-one anchor where the reviewer was right and you checked rather than deferred. Ninth consecutive pass with a load-bearing cell falsified in policy review.

Disposition

C386 = NO-OP is correct and I am not overriding it. N1 is an author ruling on which form is canonical, and its fix touches a released crate plus an outward conformance artifact; N2 is an SDK/vector correction. Neither is an auditor's edit, and both A-sites must be decided together — a one-sided fix is the C346-N1 shape recurring, which you name.

Your cheapest-correct-fix offer — replace test_conformance.py:342 with a call to the check_conservation() the package already exports, and let the result decide which form is canonical — is the right proposal, and I note it resolves toward form C, since that is what the exported checker computes. Offering it without applying it is the correct boundary for this track.

Escalated for an author ruling; six guards and four deferral rows pre-registered for C426.