# Proof audit PASS2 round3 — pinned findings

No remaining blocking proof gap in the corrected **pinned** bundle for [#20093](https://git.cafe/pingdotgg/t3code/pulls/20093) ([GitHub mirror](https://github.com/pingdotgg/t3code/pull/20093)): [968dd51704](https://github.com/pingdotgg/t3code/commit/968dd51704441138559a3fe9c348719f2b11e0c6) → [22aaa53e02](https://github.com/pingdotgg/t3code/commit/22aaa53e02e86bb3728abbe8432fb15c910487ae). This is proof sufficiency within the declared server-runtime scope and limits, not merge approval or a verdict on a later integration.

1. **E2 prior blocker closed concretely.** Corrected final raw P requests3/12/21 are HTTP503/503/200. Both failures have `data:null` and `SERVICE_UNAVAILABLE` errors. Request12 follows the recorded forced invalidate/read; request21 follows fixture recovery. D survives initial, forced-retry, recovered and cached-coverage deliveries without list errors. The next forced list uses the successful coverage fact without another P. Baseline has no P and retains D. This proves later forced list retry, not an automatic transport retry ordinal. Independent full-server replay below reproduces these exact results. The old503-with-valid-data capture is excluded, not reinterpreted.

2. **O4/G1 prior blocker closed concretely.** Every one of the four corrected continuation deliveries per pin contains distinct B2, title `B continuation version 202`, absent from every first page. Before first pages contain A1+B1; final first pages contain A1 only. Before continuation returns B2; final returns B1+B2. A1 is never repeated; both end untruncated with empty next cursors. Raw requests carry the returned timestamp/seen-row cursor map and inclusive `updated:<=` boundary. Initial limit1 is per repository and continuation limit99 is explicit. This proves the required nonempty continuation, not unchanged-page-size paging or every cursor strategy. The old empty continuations are excluded. Cross-involvement positive-fact sharing remains covered by the separate duplicate/case harness; the corrected pagination workload has four all-involvement continuations per pin rather than the old sixteen broader but empty deliveries. No required next-row behavior was dropped.

Both archived negative controls were independently rerun: restoring503-success-data or empty continuation makes the evidence checker fail. The stale empty-repository GraphQL comment is removed at the pinned final SHA.

Evidence reviewed: [corrected index](https://gh-file-drop-api-prod-mi5fy3sowv63ufte.pinglabs.workers.dev/f/7b09888342c8bbd8/index.md), its complete matrix, counts, manifest, ledger, deliveries, assertions, negative controls, capture map, README/limits and extracted raw HTTP/RPC/server traces. The [previous insufficient audit](https://gh-file-drop-api-prod-mi5fy3sowv63ufte.pinglabs.workers.dev/f/dd226528d3972b04/audit-pass2.md) was read and its two objections retained above until checked.

## Row statuses

Supported means supported within the row's disclosed fixtures, harnesses or static evidence. All ordinary affected runtime scenarios have paired baseline/final captures; compatibility and client-path exceptions are explicit.

| Row | Status | Evidence / practical limit |
|---|---|---|
| O1 | Supported | A returned; positive B skips fallback; empty C remains uncovered with F. |
| O2 | Supported | Warm identical keys reuse result; separate partitions and own/subset keys remain distinct. |
| O3 | Supported | Silent D retained; negative/null/refused coverage keeps fallback. |
| O4 | Supported, corrected | Distinct B2 continuation on both pins, no A1 repetition, exhausted cursors; limit1→99 disclosed. |
| T1 | Supported | Genuine Codex commands, completed runs/checkpoints, receivers2/3/4 and refresh reads. |
| T2 | Supported | Own A advances1/2/3; final global/subsets hold1 through later turns, then3. Native wall times are recorded rather than prescribed offsets. |
| T3 | Supported | Isolated final refreshes4 versus before3; trailing delivers3. Single-turn case has one refresh. |
| T4 | Supported, harness | Full-server TestClock29999/30000/30001; timer-first equal-time case only. |
| T5 | Supported | Own projectId stays immediate; projectIds subsets coalesce globally. |
| T6 | Supported, static/client limit | Same nominal global subset shape; no live linked-environment/browser claim. |
| P1 | Supported | Three explicit app pushes distinct from native shell pushes; fresh global versions inside busy window. |
| P2 | Supported, input limit | Thread/project/cwd selectors, missing-thread fallthrough, unmatched X and no-op. Unmatched worktree cwd is not claimed to refresh. |
| P3 | Supported, limited | Normal create-PR and combined commit_push captures; every busy-window combination not separately captured. Immediate helper is statically shared with P1. |
| M1 | Supported | Manual invalidation immediate; coverage facts retained, including negative D. |
| L1 | Supported | No recurring idle listing work; on-demand31s read expires list cache. |
| V1 | Supported | Clock599999/600000/600001 plus paired natural >601s run; final natural P timestamps22:26:39.727 and22:36:42.134 UTC. |
| V2 | Supported, explicit tradeoff | Warm negative D stays safe; warm positive B may be omitted. Closed B7/new OPEN B1 direct summaries, omission after manual/explicit push, and index recovery all captured on both pins. Own-project list can also omit B under this shared search fact. |
| R1 | Supported | Held HTTP survives final reader disconnect and is released to reattached reader; baseline abort/restart visible. |
| R2 | Supported | Warm/expired reconnect and fresh process on same isolated home; projects originated from RPC receipts. |
| E1 | Supported | Null/refused alias does not confirm coverage; other aliases usable. |
| E2 | Supported, corrected | Unusable503 forced retry/recovery/cache reuse independently reproduced. Transport, non-null-data TIMEOUT and separate null-data cases remain distinct. |
| E3 | Supported, fixture only | Actual synthetic primary remaining0/reset and secondary Retry-After2 headers, backoff/recovery. Retry ordinals unknown. |
| E4 | Supported | Search failure repository fallback; D partial failure and provider-unavailable distinguishable. |
| F1 | Supported, GHES harness only | Optional capability absent, across present/absent; no live GHES auth/integration claim. |
| F2 | Supported, split evidence | GitCafe/Forgejo/Bitbucket isolated provider harness; GitCafe/Bitbucket REST full-server empty fixtures. Forgejo missing CLI and GHES auth absence remain diagnostics. |
| F3 | Supported, static limit | Real Codex core; common finalization observer/service path unchanged at the pinned head. Other native providers not exercised. |
| G1 | Supported, corrected | Coverage25+1 and global100+1; distinct continuation now delivered; duplicate roots/case and shared filter facts in isolated harness. |
| First-PR regression | Supported | Empty C→first PR survives manual and explicit C push in both pins; exact-final rerun checked. Earlier independent audit replay was supplemental, not relabelled final proof. |

## Provenance and accounting

Downloaded every indexed public artifact using curl and independently checked the indexed SHA256 against both downloaded and local bytes, including driver `397cfbfc41e0860cb5f5d32b840337f3e1056aa06b5d3180b036b18a0a05d7c3` and transcripts `fdbb1fd3349b8096315b249cde835cb806a54d3d04eecfae64b6f33c79d7190f`. Verified all246 manifest-listed raw files across54 captures,27 per pin. Every selected after capture carries a before-spawn22aaa source stamp; no old72 process is relabelled. Retained historic baseline captures lack new per-process stamps and retain their previously audited original-archive provenance, as disclosed.

Verified4964 source-export records directly against Git trees/blob contents:2482 per pin. Independently verified all2482 files in my fresh final export before replay. Changed-file blob/SHA256 manifest also agrees. The manifest's compatibilityHarnessSHA256 hashes the generated TypeScript harness source, not the NDJSON output; that source hash agrees. The historical `static-paths.md` still labels72, but its relevant blobs match22aaa; it is supplemental static evidence, not a newly stamped runtime capture.

Recomputed all54 per-capture counts/buckets/simulated sums. All3280 ledger HTTP records match raw status/envelope and query hashes; normalized deliveries total1557:1545 lists,8 continuations,4 direct summaries. S/P/F/K remain separate from REST. Aggregate bucket reconciliation is S798/P68/F2128/K218/REST68, only a bundle inventory, never a savings total.

Core:215→110 HTTP;214→109 GraphQL; buckets S56/P0/F144/K14/REST1 → S51/P1/F42/K15/REST1. Isolated core109→51 HTTP and108→50 GraphQL. Simulated core fixture cost214→110 is a different accounting field. Every live cost is null. These are fixture request reductions, not live quota consumed/saved or a universal multiplier. Overlapping scenarios are not summed into savings.

Core raw provider command_execution events record three completed shell commit/push commands with exit0. Persisted completed runs carry checkpoints; receiver barriers are2/3/4; refresh subscriptions show page versions. Three separate app pushes and one no-op are recorded independently. Seed pushes predate capture. Scenario-specific pushes and synthetic create-PR are separately disclosed. No source/forge mutation by this auditor.

At the pinned comparison, effective diff is nine files: seven production plus two focused test files, no web diff. It implements optional coverage/API/query plumbing, positive/negative facts, service-scoped reads, global turn coalescing and immediate explicit refresh paths.72→22aaa changes only the false source GraphQL comment; generated/runtime blobs otherwise match. All final runtime claims nevertheless use newly run22aaa captures.

## Independent corrected-row replay

Extracted the NEW hashed driver into fresh `/tmp/takeover-20093/audit-round3/driver`, exported22aaa from Git, linked installed dependencies, and created fresh synthetic repos/bare receivers. Ran exactly one authorized row:

```text
node /tmp/takeover-20093/audit-round3/driver/supervise.mjs final /tmp/takeover-20093/audit-round3/final-source /tmp/takeover-20093/audit-round3/seed-final 21993 coverage-http corrected-http
```

Full production server, isolated home, ordinary startup pairing and WebSocket RPC; no browser. All8 delivered list results match published final-corrected-http in order by label/input and complete result with only volatile observedAt removed. All32 ordered HTTP requests match document, variables, host, operation, bucket, status, envelope, synthetic headers and simulated cost. Buckets S4/P3/F20/K4/REST1. P IDs3/12/21 have503/503/200. Independently checked null/error failures, forced-read/recovery ordering, D survival and no fourth probe. Archived assert-evidence.py passes against the fresh replay.

Client exited0. Supervisor stopped only its captured server PID349761, which is absent from /proc; server exited130 via normal SIGTERM handling. All27 selected final server PIDs are also absent. Scratch totals1.1GB, below10GB. [Independent replay traces, assertions, comparison and verification scripts](https://gh-file-drop-api-prod-mi5fy3sowv63ufte.pinglabs.workers.dev/f/3d476efaf7d51187/replay-round3.tar.gz).

## Limits and integration handoff

No live GitHub quota consumption, live search-index latency, live GHES authentication, or live Forgejo CLI integration measured. External forge responses and rate headers/costs are fixtures. Real native integration is Codex only. Compatibility without optional methods is a labelled service/provider harness; TestClock controls Effect time, not provider wall time, and equal-time ordering is timer-first only. No live multi-environment/browser/mobile/desktop verification; user-defined surface here is server runtime, with no pinned web diff. No broad checks or product-test suite rerun; evidence assertions are not product tests, and the parent's191 focused cases remain a parent report. Slow-probe lifetime consumption and concurrent distinct-key single-flight are not separately proven/promised. P3's busy-window Cartesian product remains limited as above. Coverage-positive search lag, including closed-only B gaining a new open PR, is an accepted up-to-ten-minute tradeoff: invalidation is immediate but indexing need not be. Do not describe that omission as fixed.

During this audit the parent merged main. Current checkout became [3d7b2f0671](https://github.com/pingdotgg/t3code/commit/3d7b2f06716ff8a392e195f0dfd9f723ddaafc49), parents22aaa and [70e5e384da](https://github.com/pingdotgg/t3code/commit/70e5e384dab96a1d1e4a253ee5a9415ed5d8ce30). The independent source export and replay remain22aaa. I did not rerun/relabel them. The shared PullRequestService integration adds isDraft state-change/report deduplication propagation; it does not modify the reviewed coalescing/coverage sections in the observed merge diff. No concrete integration defect identified by that inspection, but combined behavior and new baseline/head are unverified here. Parent must commission fresh proof, particularly draft/ready notification/report propagation alongside list invalidation. This report also does not refresh forge publication/CI/review state; the old audit's remote-head discrepancy is not silently declared resolved. A clean merge is not runtime evidence. Worktree remained clean.

## FRICTION

| category | happened | prevention |
|---|---|---|
| public artifact retrieval | Python urllib received HTTP403; curl retrieved the same public artifacts and hashes matched. | Use configured curl transport for public evidence retrieval. |
| moving integration head | Parent merged newer main while pinned audit was running. | Keep immutable source export/replay and pinned verdict separate; commission new baseline/head proof. |

Auditor: gpt-6.1-sol, Codex harness in T3 Code. Skills: [pr-audit](/home/ubuntu/.codex/skills/pr-audit/SKILL.md), [ghdrop](/home/ubuntu/.codex/skills/ghdrop/SKILL.md). No code edits, push, forge comment, merge, browser, delegation, credential/configuration/mode/permission/MCP changes by this auditor.

VERDICT: SUFFICIENT