Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
128 changes: 100 additions & 28 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -481,6 +481,11 @@ carries both facts, and counts as current only when both hold:
PR, and the record carries the binary's own account of both. The bump is what
makes the fix retroactive — the 34 verdicts the 2026-07-29T17:17:35Z run
recorded with the lens never run all stop being current at once.
`vet-protocol 4` is the audit lens's **scope** (#155): the ledger row now
carries the scope the invocation declared, and a verdict is refused unless
that scope is this PR's. `whole-repo` and a path list are both real
invocations that read the **wrong code**, so every protocol-3 verdict was
formed under a scope-blind ledger and is not a value of the current function.

An **unstamped** comment is `VetProtocol::Unknown` and is never current. It was
written under rules that cannot be identified, and unidentified is not "fine" —
Expand Down Expand Up @@ -731,7 +736,7 @@ the best run to date — zero errors, correct paging, a `design` verdict raised
which is the point: nothing about a lensless verdict looked wrong.

So `record_verdict` refuses a verdict on a PR this run holds no lens for, on
**two facts it establishes for itself**:
**three facts it establishes for itself**:

- **SOURCE** — the `pr_checkout` tree for this PR, holding this PR's head.
`pr_checkout` is a tool this same binary implements, `checkout_dir` derives
Expand All @@ -743,6 +748,9 @@ So `record_verdict` refuses a verdict on a PR this run holds no lens for, on
— already standing in the runner's live pipe — appends one row per invocation
the instant the harness announces it. The row is therefore on disk before the
MCP server can be asked about the PR.
- **SCOPE** (#155) — the scope that invocation **declared**, read off the same
announced event by the same filter and written onto the same row. See
[the scope gate](#the-scope-the-lens-ran-at-is-on-the-row-too) below.

The ledger is a per-run file (`review-runs/<TS>.lens`), written by
`run-timings --lens` and read back through **`RUN_LENS_LEDGER`**, because the
Expand Down Expand Up @@ -792,16 +800,16 @@ written by the binary from what it verified and sitting above the model-authored

```
🤖 ai:vetter
vet-protocol 3
lens source@6a370a5d… + audit skill invoked
vet-protocol 4
lens source@6a370a5d… + audit skill invoked at pr:386
Reviewed 6a370a5d…: ready — closes #386
cost 412 — concurrency guard in a store poll loop
```

That is a different object from the evidence-of-reading preamble #131 and #140
removed. A preamble is the **model's** account of its own diligence; this is the
**binary's** account of two facts it checked. It is also why an **absent** stamp
is meaningful: a verdict with no `lens` line is one written before the lens was
**binary's** account of facts it checked. It is also why an **absent** stamp is
meaningful: a verdict with no `lens` line is one written before the lens was
checkable, which is exactly the 34, and no longer indistinguishable from a vet
that read the source. `lens source@<sha>, invocation UNOBSERVED (…)` is the
third state — a run that names no ledger records its verdict and says so,
Expand All @@ -816,32 +824,96 @@ false premise gets caught. The cost of the alternative is one depth-1 clone that
`pr_checkout` reuses and `clone_release` disposes; the cost of a model-written
_"diff-only was proportionate here"_ waiver is a waiver written 34 times.

**What this does NOT close, stated plainly.** The invocation's SCOPE is model
text: the binary sees that a skill ran and reads the PR ref out of `args`, so a
vetter could invoke the lens and describe it dishonestly. What the check buys is
that the credit cannot be had without paying for a real invocation, and that one
invocation buys exactly one PR. It says nothing about what the skill
**concluded** — [#146](https://github.com/rainlanguage/issue-pr-cron/pull/146)
is right that correctness, security and design are not decidable from source
text, and those dimensions remain entirely the vetter's. The two gates are
complementary and neither subsumes the other: this one asks whether the lens was
pointed at the PR, that one asks whether a `ready` contradicts a rule the lens
states.

**And what it rests on.** Both facts are unforgeable only while the model cannot
write to the filesystem. That is currently true of the vetter in the strongest
available sense — not a deny rule but an absent tool: the `tools` array in every
run's own `system`/`init` event is `[Glob, Grep, Read, Skill, mcp__fsm__*]`,
with no `Bash`, `Write` or `Edit` in it, so a redirection into the ledger is not
a thing the session can express. That is also why the ledger is written by
`run-timings` — a **different process**, in the runner's pipe, outside the
model's session — rather than by anything the model calls.
**What this does NOT close, stated plainly.** It says nothing about what the
skill **concluded** —
[#146](https://github.com/rainlanguage/issue-pr-cron/pull/146) is right that
correctness, security and design are not decidable from source text, and those
dimensions remain entirely the vetter's. The two gates are complementary and
neither subsumes the other: this one asks whether the lens was pointed at the
PR, that one asks whether a `ready` contradicts a rule the lens states.

**And what it rests on.** Every one of these facts is unforgeable only while the
model cannot write to the filesystem. That is currently true of the vetter in
the strongest available sense — not a deny rule but an absent tool: the `tools`
array in every run's own `system`/`init` event is
`[Glob, Grep, Read, Skill, mcp__fsm__*]`, with no `Bash`, `Write` or `Edit` in
it, so a redirection into the ledger is not a thing the session can express.
That is also why the ledger is written by `run-timings` — a **different
process**, in the runner's pipe, outside the model's session — rather than by
anything the model calls.
[#152](https://github.com/rainlanguage/issue-pr-cron/pull/152) is the reason to
say this out loud rather than leave it implied: a _declared_ tool surface is not
a sandbox, and a command declaring only `Read` was observed running `Bash`. If
the vetter is ever granted a write tool, the invocation half degrades to the
source half and the ledger becomes advisory — so that grant is the moment to
revisit this, and the `vetter has no write grant` CI job is what fails first.
the vetter is ever granted a write tool, the invocation and scope halves degrade
to the source half and the ledger becomes advisory — so that grant is the moment
to revisit this, and the `vetter has no write grant` CI job is what fails first.

### The scope the lens ran at is on the row too

A lens pointed at the wrong **scope** is not a weaker review, it is a review of
**different code** — and both wrong scopes are real invocations, so both satisfy
the check above:

- **Diff-only** structurally cannot see ramifications. `raindex#2778`'s claim
that a `signer<256>` silently resolves to row 0 was falsified only by reading
the callee, which reverts.
- **Whole-repo on a PR** returns findings mostly about code the PR never
touches. Measured on `rainlanguage/rain.deploy#21`: twelve findings, five
bearing on the PR, seven pre-existing — and the merge-relevant one (a new
public API shipped without a `[package] version` bump, against an
already-published version, in a repo that autopublishes on push to `main`) was
one line in a list of twelve.

So the ledger row carries the **scope the invocation declared**, and
`record_verdict` refuses a verdict whose lens ran at the wrong one
(`RecordGate::WrongLensScope`, **exit 6**). The vocabulary is the audit skill's
own
([`claude-audit-skills#66`](https://github.com/rainlanguage/claude-audit-skills/issues/66)),
three values and no fourth: `whole-repo`, `pr:<number>`,
`paths:<comma-separated globs>`. For a PR verdict exactly one is legal —
`pr:<this PR's number>`:

- `whole-repo` reviewed the repository.
- `paths:<globs>` reads the files the list names and nothing that decides
whether they are right. On a PR the only file list to hand is the diff's, so
this is the diff-only lens under another name — and even where the globs reach
wider they are a list the caller assembled, not the ramification set the
_"would understanding it change the ruling on THIS diff?"_ test derives.
- `pr:<other>` declares it reviewed a different PR than the one it was credited
to.

Four things this is careful about:

- **The runner writes the row, from the invocation.** The scope is read off the
same announced `Skill` event `run-timings` already stands in the pipe for, and
it is **never** parsed out of verdict text. A model-written scope claim is a
claim about itself, which is the reasoning that made
[#146](https://github.com/rainlanguage/issue-pr-cron/pull/146) choose the
linter shape over a findings record and #151 choose the stream-json
observable.
- **Absent is not the same as wrong**, and neither is the same as
**unobserved**. A row with no `scope` key is an invocation that declared
nothing (the key is omitted, never `null`); a row with a scope this PR does
not own is an invocation that declared the wrong thing; a run with no ledger
at all observed nothing. Three states, three refusal messages, because a
refusal that told a vetter it declared `whole-repo` when it declared nothing
would be a refusal about a call it never made. An **undeclared** scope is
still refused: the skill's standing rule is a whole-repo snapshot, so
declaring nothing _is_ declaring whole-repo.
- **Its place in `record_gate` is immediately under the lens gate.** Under,
because _"at what scope"_ is not a question about a PR whose source was never
checked out or whose skill was never invoked. Over the convention and coverage
refusals, for #151's own reason one level in: there is no point reporting a
pragma or an anchor range to a vetter whose lens read the wrong code.
- **The exit code is its own.** 6, beside 5: five says the code was not read,
six says the **wrong** code was read. One is repaired by a checkout and an
invocation, the other by re-invoking a skill that already ran, at `pr:<n>`.

A scope naming **more than one** value declares none — `args` is prose, and
`"scope pr:21, not whole-repo"` states two values a reader would have to rank,
so the same ruling applies as for an invocation naming two PRs.
`review-prompt.txt` says to write `pr:<number>` and not to write the other two
even to say they are not being used.

### The mechanical half of the audit lens is the binary's, not the model's

Expand Down
Loading
Loading