feat(evidence): a completion may name the check the table could not

The verifier table will never enumerate every project's own runner, and
`./scripts/ci.sh` says nothing about itself — three measured attempts at
having a model read the command string ended in the harness that disproved
them. The information the table lacks is not in the command; it is in the
turn, which read or wrote that script.

complete_step already carries it. Its evidence takes kind=verification with a
command, and the tool refuses a citation whose command has no matching
successful receipt — the model names which command was the check, and the host
proves it ran. Only the readiness gate never asked: it consulted the static
table and the project's declared checks, so a corroborated citation sat in the
ledger while the turn was told to go and verify.

It asks now. What the model may decide stays exactly one thing — which of the
commands it ran was the check. That the command ran, that it exited zero, and
that it did so after the latest write are all still read off receipts, so a
citation cannot manufacture a pass, reach back past a later write, or rescue a
check that failed. Each of those is a test.

Delivery is untouched: there a citation still has to satisfy
IsDeliveryVerificationCommand, and the strictest tier keeps its static answer.

The lease refusal's wording changed with it, so four tests that asserted a
same-process holder is "another Reasonix process" now assert what it is.

internal/acp/service_lease_test.go

@@ -48,7 +48,7 @@ func TestSessionLoadRefusedWhenLeaseHeld(t *testing.T) {
 	if resp.Error == nil {
 		t.Fatalf("session/load of a held session succeeded, want protocol error")
 	}
-	if !strings.Contains(resp.Error.Message, "in use by another Reasonix") {
+	if !strings.Contains(resp.Error.Message, "already open elsewhere in this Reasonix") {
 		t.Fatalf("session/load error = %q, want holder wording", resp.Error.Message)
 	}
 	if strings.Contains(resp.Error.Message, path) {

internal/agent/final_readiness.go

@@ -196,8 +196,7 @@ func (a *Agent) finalReadinessCheckFor() finalReadinessCheck {
 	// exactly why the check does not pass. Nothing else about the turn is waived.
 	verified, blockedWithCheck := a.postWriteVerification(writer)
 	if !a.deliveryProfile && a.turn.policySet && a.turn.policy.Verification >= taskpolicy.VerifyTargeted &&
-		toolPresent(a.svc.tools, "bash") && !blockedWithCheck && !verified &&
-		!a.declaredChecksRanAfter(writer) {
+		toolPresent(a.svc.tools, "bash") && !blockedWithCheck && !a.checkEstablished(writer, verified) {
 		out.applies = true
 		out.missingVerification++
 		missing = append(missing, a.verificationGap(writer))
@@ -254,6 +253,15 @@ func (a *Agent) finalReadinessCheckFor() finalReadinessCheck {
 	return out
 }
 
+// checkEstablished reports that something after the latest write stands as its
+// check: one the table recognised, a project's declared one, or one a
+// completion named and the ledger corroborated.
+func (a *Agent) checkEstablished(writer int, verified bool) bool {
+	return verified ||
+		a.declaredChecksRanAfter(writer) ||
+		a.task.ledger.HasCorroboratedCitedCheckAfter(writer)
+}
+
 // postWriteVerification reads what the checks after the latest write establish.
 // verified needs a passing check with none of them still standing failed — one
 // check passing cannot answer for another that did not. blockedWithCheck is the

internal/cli/session_lease_test.go

@@ -40,7 +40,7 @@ func TestRunResumeRefusedWhenSessionLeaseHeld(t *testing.T) {
 			t.Fatalf("run --resume held rc = %d, want 1", rc)
 		}
 	})
-	if !strings.Contains(errOut, "in use by another Reasonix") {
+	if !strings.Contains(errOut, "already open elsewhere in this Reasonix") {
 		t.Fatalf("run --resume held stderr = %q, want holder wording", errOut)
 	}
 	if !strings.Contains(errOut, "--copy") {
@@ -312,7 +312,7 @@ func TestChatResumeCommandRefusedWhenLeaseHeld(t *testing.T) {
 	m.runResumeCommand("/resume 1")
 
 	out := strings.Join(m.transcript, "\n")
-	if !strings.Contains(out, "in use by another Reasonix") {
+	if !strings.Contains(out, "already open elsewhere in this Reasonix") {
 		t.Fatalf("refusal notice missing from transcript:\n%s", out)
 	}
 	if got := m.ctrl.SessionPath(); got != active {

internal/cli/switch_recovery_test.go

@@ -195,7 +195,7 @@ func TestSessionRecoveryCallbackFailureKeepsOriginalLeaseAndPath(t *testing.T) {
 	if strings.Contains(err.Error(), dir) || strings.Contains(err.Error(), filepath.Base(originalPath)) {
 		t.Fatalf("recovery bind error exposed a local path: %q", err)
 	}
-	if !strings.Contains(err.Error(), "session is in use") {
+	if !strings.Contains(err.Error(), "already open elsewhere in this Reasonix") {
 		t.Fatalf("recovery bind error = %q, want sanitized lease refusal", err)
 	}
 	if got := ctrl.SessionPath(); got != originalPath {

internal/evidence/cited_check_test.go

@@ -0,0 +1,99 @@
+package evidence
+
+import (
+	"encoding/json"
+	"testing"
+)
+
+func completionCiting(command string) Receipt {
+	args, _ := json.Marshal(map[string]any{
+		"step":   "wire it up",
+		"result": "the switch reaches the gate",
+		"evidence": []map[string]any{
+			{"kind": "verification", "summary": "the suite passed", "command": command},
+		},
+	})
+	return ReceiptFromToolCall("complete_step", args, true, false)
+}
+
+// The case the static table cannot answer: a project's own runner. The model
+// names it, the host confirms it ran and passed, and the two together are what
+// the table alone could not produce.
+func TestCitedCheckCountsWhenTheCommandRanAfterTheWrite(t *testing.T) {
+	l := NewLedger()
+	l.Record(Receipt{ToolName: "write_file", Success: true, Write: true, Paths: []string{"a.go"}})
+	writer := 0
+	l.Record(Receipt{ToolName: "bash", Command: "./scripts/ci.sh", Success: true})
+	l.Record(completionCiting("./scripts/ci.sh"))
+
+	if !l.HasCorroboratedCitedCheckAfter(writer) {
+		t.Fatal("a cited check that really ran after the write did not count")
+	}
+	// The table's own answer is unchanged: this is added evidence, not a
+	// reclassification of the command.
+	if CommandRunsVerification("./scripts/ci.sh") {
+		t.Fatal("precondition: the table should not recognise this command")
+	}
+}
+
+// A citation is a claim about what ran, so a command with no successful receipt
+// after the write proves nothing — this is the whole reason the gate can accept
+// the model's naming at all.
+func TestCitedCheckIsIgnoredWhenTheCommandNeverRan(t *testing.T) {
+	l := NewLedger()
+	l.Record(Receipt{ToolName: "write_file", Success: true, Write: true, Paths: []string{"a.go"}})
+	l.Record(completionCiting("./scripts/ci.sh"))
+
+	if l.HasCorroboratedCitedCheckAfter(0) {
+		t.Fatal("a citation with no matching receipt was accepted")
+	}
+}
+
+// Running the check and then changing the code again leaves the change
+// unverified: the citation is anchored to the write it followed, not to any
+// write ever made.
+func TestCitedCheckDoesNotReachPastALaterWrite(t *testing.T) {
+	l := NewLedger()
+	l.Record(Receipt{ToolName: "bash", Command: "./scripts/ci.sh", Success: true})
+	l.Record(completionCiting("./scripts/ci.sh"))
+	l.Record(Receipt{ToolName: "write_file", Success: true, Write: true, Paths: []string{"a.go"}})
+	laterWriter := 2
+
+	if l.HasCorroboratedCitedCheckAfter(laterWriter) {
+		t.Fatal("a check from before the latest write was counted for it")
+	}
+}
+
+// A failing check cannot be cited into a pass: HasSuccessfulCommandAfter is the
+// host's reading of the exit status, and nothing the model writes reaches it.
+func TestCitedCheckDoesNotCountWhenTheCommandFailed(t *testing.T) {
+	l := NewLedger()
+	l.Record(Receipt{ToolName: "write_file", Success: true, Write: true, Paths: []string{"a.go"}})
+	l.Record(Receipt{ToolName: "bash", Command: "./scripts/ci.sh", Success: false})
+	l.Record(completionCiting("./scripts/ci.sh"))
+
+	if l.HasCorroboratedCitedCheckAfter(0) {
+		t.Fatal("a failing command was accepted because a completion cited it")
+	}
+}
+
+// Only verification citations name a check; a completion backed by files or a
+// manual note says nothing about a command having run.
+func TestOnlyVerificationCitationsNameACheck(t *testing.T) {
+	args, _ := json.Marshal(map[string]any{
+		"step":   "look at it",
+		"result": "read the file",
+		"evidence": []map[string]any{
+			{"kind": "files", "summary": "read it", "paths": []string{"a.go"}},
+			{"kind": "manual", "summary": "looked right"},
+		},
+	})
+	l := NewLedger()
+	l.Record(Receipt{ToolName: "write_file", Success: true, Write: true, Paths: []string{"a.go"}})
+	l.Record(Receipt{ToolName: "bash", Command: "./scripts/ci.sh", Success: true})
+	l.Record(ReceiptFromToolCall("complete_step", args, true, false))
+
+	if l.HasCorroboratedCitedCheckAfter(0) {
+		t.Fatal("a completion citing no verification was read as naming a check")
+	}
+}

internal/evidence/evidence.go

@@ -711,6 +711,38 @@ func (l *Ledger) HasSuccessfulCommandAfter(command string, after int) bool {
 	return false
 }
 
+// HasCorroboratedCitedCheckAfter reports whether a completion after `after`
+// named a verification command that also ran successfully after `after`.
+//
+// complete_step already refuses a citation with no matching successful receipt,
+// so the model's part is naming which command was the check — the thing a
+// static table cannot know about a project's own script, and the model does
+// know, having read or written it. The host still supplies both halves that
+// matter: that the command ran, and that it passed.
+func (l *Ledger) HasCorroboratedCitedCheckAfter(after int) bool {
+	if l == nil {
+		return false
+	}
+	for _, command := range l.citedChecksAfter(after) {
+		if l.HasSuccessfulCommandAfter(command, after) {
+			return true
+		}
+	}
+	return false
+}
+
+func (l *Ledger) citedChecksAfter(after int) []string {
+	l.mu.Lock()
+	defer l.mu.Unlock()
+	var out []string
+	for i := max(after+1, 0); i < len(l.receipts); i++ {
+		if r := l.receipts[i]; r.Success && r.ToolName == "complete_step" {
+			out = append(out, r.CitedChecks...)
+		}
+	}
+	return out
+}
+
 func (l *Ledger) HasSuccessfulCompleteStepAfter(after int) bool {
 	if l == nil {
 		return false
@@ -1501,6 +1533,7 @@ func ReceiptFromToolCall(toolName string, args json.RawMessage, success bool, re
 		if toolName == "complete_step" {
 			r.Step = completeStepIdentity(fields)
 			r.StepProof = completeStepHasProof(fields)
+			r.CitedChecks = completeStepCitedChecks(fields)
 		}
 		if toolName == "todo_write" {
 			r.Todos = todoItemsField(fields, "todos")
@@ -2341,6 +2374,31 @@ func todoItemsField(fields map[string]json.RawMessage, key string) []TodoItem {
 
 // A failed complete_step can unlock todo recovery only when the payload had the
 // same structural proof shape Execute expects before host verification runs.
+// completeStepCitedChecks returns the commands a completion named as its
+// verification. Whether each one actually ran is the ledger's question, asked
+// where it matters rather than here.
+func completeStepCitedChecks(fields map[string]json.RawMessage) []string {
+	raw, ok := fields["evidence"]
+	if !ok {
+		return nil
+	}
+	var items []struct {
+		Kind    string `json:"kind"`
+		Command string `json:"command"`
+	}
+	if json.Unmarshal(raw, &items) != nil {
+		return nil
+	}
+	var out []string
+	for _, item := range items {
+		command := strings.TrimSpace(item.Command)
+		if strings.EqualFold(strings.TrimSpace(item.Kind), "verification") && command != "" {
+			out = append(out, command)
+		}
+	}
+	return out
+}
+
 func completeStepHasProof(fields map[string]json.RawMessage) bool {
 	if strings.TrimSpace(stringField(fields, "result")) == "" {
 		return false

internal/evidence/receipt.go

@@ -17,12 +17,16 @@ type Receipt struct {
 	Command   string          `json:"command,omitempty"`
 	Step      string          `json:"step,omitempty"`
 	StepProof bool            `json:"step_proof,omitempty"`
-	TodoStep  *TodoStepMatch  `json:"todo_step,omitempty"`
-	Paths     []string        `json:"paths,omitempty"`
-	Read      bool            `json:"read,omitempty"`
-	Write     bool            `json:"write,omitempty"`
-	Mutation  bool            `json:"mutation,omitempty"`
-	Todos     []TodoItem      `json:"todos,omitempty"`
+	// CitedChecks are the verification commands a complete_step named. The tool
+	// refuses a citation whose command has no successful receipt, so a command
+	// here is one the host already matched against what actually ran.
+	CitedChecks []string       `json:"cited_checks,omitempty"`
+	TodoStep    *TodoStepMatch `json:"todo_step,omitempty"`
+	Paths       []string       `json:"paths,omitempty"`
+	Read        bool           `json:"read,omitempty"`
+	Write       bool           `json:"write,omitempty"`
+	Mutation    bool           `json:"mutation,omitempty"`
+	Todos       []TodoItem     `json:"todos,omitempty"`
 	// OutputBytes is the host-observed length of the tool's (redacted, trimmed)
 	// output. Content-evidence checks require it to be non-zero so a command
 	// that printed nothing (head -n 0, >/dev/null) can never count as reading.

internal/serve/serve_lease_test.go

@@ -68,8 +68,13 @@ func TestResumeRefusedWhenSessionLeaseHeld(t *testing.T) {
 	if resp.StatusCode != http.StatusConflict {
 		t.Fatalf("held resume status = %d, want 409 (body %q)", resp.StatusCode, respBody)
 	}
-	if !strings.Contains(respBody, "in use by another Reasonix") {
-		t.Fatalf("held resume body = %q, want holder wording", respBody)
+	// The holder here is this very process, so the refusal must not send the
+	// reader looking for a second window; it still has to name a holder.
+	if !strings.Contains(respBody, "already open elsewhere in this Reasonix") {
+		t.Fatalf("held resume body = %q, want the same-process holder wording", respBody)
+	}
+	if strings.Contains(respBody, "another Reasonix process") {
+		t.Fatalf("held resume body blames a separate process for our own lease: %q", respBody)
 	}
 	if strings.Contains(respBody, held) {
 		t.Fatalf("held resume body leaks the session path: %q", respBody)