Skip to content

Let a PR beat earn CLEAN from a run the gateway signed for - #107

Merged
jacekradko merged 2 commits into
mainfrom
jacek/dreamy-goodall-wh12a3
Oct 22, 2026
Merged

jacekradko merged 2 commits into
mainfrom
jacek/dreamy-goodall-wh12a3

Conversation

@jacekradko

@jacekradko jacekradko commented Oct 22, 2026 •

Copy link
Copy Markdown
Contributor

A PR session is no-exec, so almost every beat opens UNVERIFIED and the reviewer still does the verifying. This reuses the execution gateway that already runs one job on a quarantine of the frozen head and signs the result, so a walk claim can be run instead of read. The walk picks arguments after the trusted profile's fixed command and predicts the exit code. The broker already signs only a matching exit, so a receipt is a run whose result would have differed were the claim false. proofctl.py prove reserves the request, runs the host adapter, verifies the six-file handoff the same way an implementation consume does, and keeps the request, envelopes and streams under proof-evidence/<n>/.

The store adds proof_kind: attested. It earns CLEAN only beside a verified proof run for that beat, in a session with a frozen PR target. The store writes the signed argv, exit code and output tail onto the beat as attestation, which the walk may not set, and the page shows that block beside the walk's own PROOF line. Schema version 8 adds proof_attempts.

Look hardest at two places:

  • The adapter's new proofArguments opt-in in gateway/adapter.py. With it, a request may append at most 16 bounded arguments to the profile argv and carry any exit code 0 to 255. The executable, environment, cwd, stdin and sandbox stay pinned. Without it, nothing changes. This does let head code run in the sandbox, for example by importing test modules. That is what the sandbox exists for, but it is a wider job surface than implementation children use.
  • The exit-code-as-claim design. A live run against the real sandbox showed that a test module failing to import exits 1, just like a failing assertion. The receipt was signed while the test never ran. The skill now says to cite a proof only when its signed output shows the claim. The store cannot enforce that; the page puts the signed output in front of the reviewer instead.

Testing

On 9afeac9, which merges main after #106:

  • The only conflict was the constants block beside PROOF_KINDS. Both sides are kept: the attested proof kinds and the second-read verdicts. Main was still at schema 7, so the version 8 bump does not collide.
  • The full suite passes on Python 3.13 and on 3.9: 1121 tests, 7 skipped. The skips are the live gateway tests, which need Docker.
  • claude plugin validate . --strict passes.
  • The live suite passed against a locally built gateway image and a real Docker daemon: tests.test_gateway_live, 4 tests. The new live case captures a PR whose head breaks a shipped test and runs python3 -I -B -m unittest discover -s tests -t . through the real adapter, broker and sandbox. A prediction of exit 0 ends as failed with no receipt. A prediction of exit 1 verifies, its signed stderr shows AssertionError: 1 != 0, and the attested flag stores the real argv.
  • CI is green on 9afeac9, including gateway conformance on amd64 and arm64.
  • New tests/test_attested_proof.py covers 27 cases. They include reservation bounds and idempotence, signed consume with real P-256 keys, a tampered stream, a receipt for the wrong exit code, the wrong key, a changed profile, the store's attested-beat rules, the rendered card and summary line, the one-call prove path against stand-in adapters, the v7 to v8 upgrade, and the command line.
  • I rendered a session with an attested flag and checked the page cold: the signed command, exit code and output sit in their own block under the slots.

Risk

  • If the adapter check is wrong, a proof deployment could run a command the profile did not intend. It stays inside the same sandbox, signing and replay ledger, and only on a host that set proofArguments.
  • If the store rule is wrong, a beat could show CLEAN without a real run. The rule requires a verified row for that exact beat, and validate_beat marks any attested beat without an attestation as UNPROVEN.
  • Opening an existing session migrates it to schema 8 by adding one table. Older code refuses a version 8 database, as it does for every schema bump.
  • The stated trust boundary changed. The skill and README no longer say a source session never reaches the gateway. They now say this machine never runs the head and the receipt authorizes nothing.
  • The noise ledger from Finish the code review article plan: noise ledger, second reads, replacement rounds, finding evals #106 does not count attested beats yet, and the eval runner does not allow proofctl.py. Neither is needed for this change to be correct.

How to revert

Revert the squash commit. Sessions already opened at schema 8 are then refused by the older store as "newer than supported". To keep one, delete its proof_attempts table and set PRAGMA user_version = 7. Beats that carry proof_kind: attested would also need rewriting, because older code rejects that kind.

🤖 Generated with Claude Code

https://claude.ai/code/session_01NoDcxo3UV95RM7dMTdjMMS

A PR session is no-exec, so almost every beat opened UNVERIFIED and the
reviewer still did the verifying. The execution gateway already runs one
job on a quarantine of the frozen head and signs the result; a proof now
reuses it for a walk claim.

The walk picks arguments after the trusted profile's fixed command and
predicts the exit code. The broker already signs only a matching exit,
so a receipt is a run whose result would have differed were the claim
false. proofctl.py prove reserves the request, runs the host adapter,
verifies the six-file handoff like an implementation consume, and keeps
the request, envelopes and streams under proof-evidence/.

The store adds proof_kind attested. It earns CLEAN only beside a
verified proof run for that beat, in a session with a frozen PR target,
and the store writes the signed argv, exit code and output tail onto the
beat as attestation, which the walk may not set. The page shows them as
what ran. An accepted report finding keeps the proof it was included on.

The adapter accepts the wider request shape only when its configuration
sets proofArguments: at most 16 bounded arguments after the profile
argv, any exit code, everything else still the profile's. Without it,
nothing changes. Schema version 8 adds the proof_attempts table.

A live run against the real sandbox showed that an import failure exits
1 like a failing assertion, so the skill now says to cite a proof only
when its signed output shows the claim.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NoDcxo3UV95RM7dMTdjMMS
@jacekradko
jacekradko marked this pull request as ready for review October 22, 2026 14:55
@jacekradko
jacekradko merged commit c39edc3 into main Oct 22, 2026
6 checks passed
@jacekradko
jacekradko deleted the jacek/dreamy-goodall-wh12a3 branch October 22, 2026 19:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants