# PASS2 proof audit

No blocking proof findings. All 11 minimum groups / 20 route-expanded obligations are sufficient at replacement [d2e91b8d22](https://github.com/pingdotgg/t3code/commit/d2e91b8d22f60495b5cc9ae73402315d9bba1bdc), against base [eea9895368](https://github.com/pingdotgg/t3code/commit/eea989536849e5b5049987ee24318b5a77326542), for [#21092](https://git.cafe/pingdotgg/t3code/pulls/21092) ([#21092](https://github.com/pingdotgg/t3code/pull/21092)). This is a proof verdict for the pinned replacement, not a claim that its CI has passed or that it is already the PR head.

Two interpretation limits:

- The forge still reports the original contributor branch/head [6a4922687d](https://github.com/pingdotgg/t3code/commit/6a4922687d3416477f991e659e348d5542e2894a). Its 26 successful checks do not validate the replacement. Replacement branch is `takeover/pr-21092`; original is [AnobleSCM/t3code](https://github.com/AnobleSCM/t3code), `fix/15542-retry-locked-event-write`.
- Publication was actually captured for every initial matrix ingestion, including failed writes, guarded no-ops and secondary writes. Later explicit repeat calls run after subscriber interruption: those calls establish durable model-event count and unchanged selection, not independently observed repeat-call publication. The delivered index distinguishes those repeat assertions. This does not leave S0's required no-additional-model-event proof missing.

The final public driver contains the subscriber, readiness/completion Deferred markers, publication/log equality and unique-ID assertions. These are present in the delivered raw traces too; this is not inferred from an earlier draft or from projections alone.

| Matrix obligation | Status | Observed paired evidence |
|---|---|---|
| P | PASS | Real lock: before fails at 1 attempt/0 target events; after succeeds at 2 or 3 attempts/1 event. Includes 5000ms pair. |
| R+ | PASS | Matching stored status/attempt; recovery at attempts 2 and 3 commits exactly once. |
| R0 | PASS | Missing run, wrong status, wrong attempt separately no-op. Holder changes attempt/status before release; after retries then returns/persists/publishes nothing. |
| O+ | PASS | Matching joined run/owner/ordinal; late provider-thread update recovers once. |
| O0 | PASS | Missing join, wrong attempt, wrong ordinal separately no-op. Holder supersedes ordinal; retry rechecks and commits/publishes nothing. |
| S+ | PASS | Primary commits before independent holder acquisition at secondary boundary. After retries model write only; one primary plus one model event. Explicit model options also checked. |
| S0 | PASS | Origin, null child, missing model, missing child, equal selection, thread-lock recheck all covered. Recheck's concurrent model event is distinguished from zero ingestor model writes. Repeats add no model event. |
| L-P | PASS | Before 1 / after 3 actual lock failures; no target commit/publication. |
| L-R+ | PASS | Matching run; same bounded exhaustion, no target commit/publication. |
| L-O+ | PASS | Matching owner; same bounded exhaustion, no target commit/publication. |
| L-S+ | PASS | Secondary exhausts at 3; one primary retained, zero model events. |
| E-P | PASS | Real scoped ABORT trigger produces nested ConstraintError; one attempt. |
| E-R+ | PASS | Same real non-lock failure at matching run boundary; one attempt. |
| E-O+ | PASS | Same real non-lock failure at matching owner boundary; one attempt. |
| E-S+ | PASS | Secondary constraint fails once; primary remains committed. |
| M-P | PASS | Before stops at lock; after lock then real constraint, exactly 2 attempts. |
| M-R+ | PASS | Same sequence at matching run boundary; no third attempt. |
| M-O+ | PASS | Same sequence at matching owner boundary; no third attempt. |
| M-S+ | PASS | Same secondary sequence; one primary retained, no model event. |
| C | PASS | Four unlocked controls unchanged; empty normalized event makes zero writes; owner guard wins in both precedence directions without fallback. |

E additionally includes explicitly injected non-SQL and absent-cause failures at all four sites, each stopping on its first occurrence. M includes injected lock-then-non-SQL sequences at all four sites, stopping on attempt 2 after the replacement. Synthetic faults were not counted as real contention evidence.

All failed ingestions map to ProviderEventPublishError. Actual BEGIN failures have EventSinkWriteError → direct SqlError → LockTimeoutError; real insert-trigger failures are nested through EventStoreAppendEventsError/PersistenceSqlError and are not retried. Source inspection confirms the narrow predicate and two-retry bound at all four changed sites, transactional guard rechecks, and publication after commit. Only the ingestor and its test differ between pinned revisions; executing the exact base ingestor beside unchanged head dependencies therefore preserves the relevant before environment.

Readback: downloaded the matrix, index, short pair, all 11 row proofs, complete transcript, 716-record raw trace, 112-result summary, driver, holder, replay/summarization/packaging scripts, test logs, environment, provenance, cleanup and capture/readback audits. All 27 index/package downloads matched local capture bytes; the separately downloaded matrix matched PASS1. Each row-proof section exactly matches its full-transcript section. Parsed every raw trace and terminal result rather than accepting summary counts. Public driver SHA256: `fb6876bd2cd321ec8b8ee3ad41eb28694394f4906f3ec2634616086a97200655`. Base/head source hashes match published provenance.

Independent replay used the downloaded public driver and holder in `/home/ubuntu/wt/pr-21092`, with only the driver's scratch constant changed to `/tmp/ev-21092-proof2/replay`. No behavior/assertion changes. Temporary adjacent modules supplied workspace resolution and exact base source; the EXIT trap removed both.

```sh
bash /tmp/ev-21092-proof2/run-replay.sh
# Internally:
# git show eea989536849e5b5049987ee24318b5a77326542:apps/server/src/orchestration-v2/ProviderEventIngestor.ts > apps/server/src/orchestration-v2/EvidenceBefore.ts
# vp test run apps/server/src/orchestration-v2/EvidenceCapture.test.ts
# vp test run apps/server/src/orchestration-v2/ProviderEventIngestor.test.ts
python3 /tmp/ev-21092-proof2/audit.py
```

Results: fresh runtime **112/112 passed** (56 before + 56 after, 45.42s); existing focused suite **28/28 passed** (10.91s). All 112 delivered/replayed semantic outcomes match: attempts, primary writes, success, returned types, persisted/published types and counts, error chains, projected turn/run/owner state and child model/options. Within each capture, actual published IDs/types equal durable IDs/types in order, without duplicate IDs. All 38 replay holders acknowledged acquire/release/close and exited.

| Independent representative (busy_timeout=5000ms) | Before | After |
|---|---|---|
| First observed real lock failure after holder acquired | 5.010s | 5.011s |
| Target attempts | 1 | 2 |
| Outcome | ProviderEventPublishError | Success |
| Target returned / persisted / published | 0 / 0 / 0 | 1 / 1 / 1 |
| Projected target turn | Absent | completed |

Supporting cases explicitly set the server writer connection to 75ms; they prove branch/attempt behavior without claiming production lock durations. Random IDs, database paths, PIDs, timestamps and total execution duration differ between captures. Semantic outcomes do not. Run status remains running in the representative fixture: this is event-write recovery, not whole-run completion.

Pixel delta: **N/A — server exception**. No UI/browser/provider CLI integration was claimed or required. Failed-COMMIT recovery, turn-start/orphan handling, transport delivery, cancellation batches and the unchanged warning-only branch-metadata follow-up remain outside this four-boundary matrix.

Final checkout: clean at the pinned head. No source change, commit, push, comment, watch, merge, browser, dev server, or live userdata access. Audit artifacts and fresh databases are under `/tmp/ev-21092-proof2` only, apart from the two permitted temporary module-resolution files, now removed.

FRICTION category|problem|prevention

REVISION|Original PR checks belong to a different head.|Bind the proof verdict to full replacement/base SHAs; validate replacement CI separately when publishing it.
DELIVERY|One matrix download briefly failed DNS resolution.|Retry that bounded read and compare bytes with the delivered local matrix; all public artifacts were obtained.
PUBLICATION|Repeat-call durable assertions can be mistaken for subscribed repeat-call publication.|State the subscriber window explicitly; keep the subscriber alive through repeats if that stronger claim is needed.
REPLAY|The public script hardcodes its original occupied scratch path.|Use a fresh audit scratch directory and disclose the sole path substitution; preserve uploaded driver bytes for comparison.
TIMING|Short contention may only exercise SQLite's existing wait.|Retain a production-5000ms pair with an observed failed BEGIN and independent release; label 75ms support cases.

Audit by GPT-6.1 Sol through Codex in T3 Code. Workflow: [pr-audit](https://github.com/juliusmarminge/fleet) locally; publication uses the [ghdrop skill](/home/ubuntu/.codex/skills/ghdrop/SKILL.md).

VERDICT: SUFFICIENT