Close the six confirmed holes from the adversarial intake verification

DESIGN.md

@@ -511,6 +511,44 @@ refutation external, and blocked; deleting the required document blocked
 with "not admitted — REQUIRED" on the intake line. All three gate legs
 behaved to specification on the first run.
 
+Verified adversarially (schema 0.0.13): the same reviewer then attacked
+the MERGED implementation with live fixtures and confirmed six holes, each
+now closed with a regression test pinning it:
+
+1. Repository probes ran before intake documents were read, so a changed
+   test could write the configured document during its own probe run and
+   mint T4 for itself — demonstrated live. Intake now reads, hashes, and
+   binds every document BEFORE any probe executes; the ordering comment in
+   main names itself load-bearing.
+2. The out-of-tree boundary was a lexical prefix check, and a symlinked
+   parent directory smuggled an in-tree document past it. Containment is
+   now CANONICAL (every component of both paths resolved), the final
+   component is opened with O_NOFOLLOW, regularity is judged on the opened
+   fd, and the size bound rides a limited reader on that single open.
+3. Duplicate detection was global with a supplier-less key: one supplier's
+   pass caused another supplier's counterexample on the same raw probe id
+   to be rejected as a duplicate — refutation dominance violated.
+   Duplicates are now per supplier; a contradictory duplicate WITHIN a
+   supplier fails the run loudly (silently keeping either verdict could
+   launder the other away).
+4. An admitted-but-empty required document satisfied the gate. Required
+   now means USABLE: zero accepted rows blocks.
+5. The stdlib JSON decoder keeps a duplicate key's last value, which
+   smuggled an "outcome": "verified" behind a counterexample. Strict
+   decoding now rejects duplicate keys at any depth — also a precondition
+   for unambiguous future signatures.
+6. Rejected-row fields bypassed the control-character scrub (a live ESC
+   reached the text receipt), and the scrub missed DEL and C1. Every
+   stored external field is now scrubbed and bounded, rejections included.
+
+Two reviewer recommendations are consciously NOT taken, stated here so the
+divergence is a decision rather than an omission: policy mechanisms stay
+an open token vocabulary (a registry would couple policy validation to
+intake configuration that differs between local and CI invocations; the
+typo cost fails closed as an unsatisfiable floor), and stderr diagnostics
+keep the invoker-supplied intake paths (the flag value already appears in
+the CI configuration; the RECEIPT never carries them).
+
 ## Known limitations (found by dogfooding, stated honestly)
 
 correctful was run on itself and on a real 101-file production change on its

cmd/correctful/main.go

@@ -148,24 +148,29 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL
 	claims, mentions = harvest.AnchorClaims(claims, harvest.BuildDefIndex(root, docs), change.Files)
 	coverage.SuppressedMentions = mentions
 
-	evidence := probe.NewDispatcher(concurrency, probe.Default()...).
-		Dispatch(ctx, root, claims)
-
-	// Admit external evidence AFTER the in-tree probes: supplied rows join
-	// each claim's evidence list and are weighed by the same rules.
-	var intakeRecords []schema.IntakeRecord
+	// Admit external evidence BEFORE any in-tree probe executes. The order
+	// is load-bearing (verified adversarially): repository probes run the
+	// change's own test code, and a probe that writes the configured intake
+	// document during its run must find the document already read, hashed,
+	// and bound — the reviewed change must not supply its own evidence.
+	var (
+		intakeRecords []schema.IntakeRecord
+		extra         map[string][]schema.Evidence
+	)
 	if intakeCfg != nil {
 		subj := intake.Subject{HeadSHA: change.HeadSHA, InputDigest: change.InputDigest}
-		extra, records, err := intake.Run(intakeCfg, root, subj, claims)
+		extra, intakeRecords, err = intake.Run(intakeCfg, root, subj, claims)
 		if err != nil {
 			return err
 		}
-		for i := range claims {
-			if rows := extra[claims[i].ID]; len(rows) > 0 {
-				evidence[i] = append(evidence[i], rows...)
-			}
+	}
+
+	evidence := probe.NewDispatcher(concurrency, probe.Default()...).
+		Dispatch(ctx, root, claims)
+	for i := range claims {
+		if rows := extra[claims[i].ID]; len(rows) > 0 {
+			evidence[i] = append(evidence[i], rows...)
 		}
-		intakeRecords = records
 	}
 
 	r := receipt.Assemble(change, claims, evidence, coverage)

internal/intake/hardening_test.go

@@ -0,0 +1,206 @@
+package intake
+
+// Regression tests for the adversarial verification findings: each test
+// here pins a CONFIRMED hole from the post-implementation review of the
+// intake contract.
+
+import (
+	"fmt"
+	"os"
+	"path/filepath"
+	"strings"
+	"testing"
+
+	"github.com/joshft/correctful/schema"
+)
+
+// TestContradictoryVerdictsFailLoudly: a supplier that reports both a pass
+// and a counterexample for the same probe is a supplier bug — silently
+// keeping either verdict could launder the other away, so the run errors.
+func TestContradictoryVerdictsFailLoudly(t *testing.T) {
+	repo := t.TempDir()
+	outside := t.TempDir()
+	rows := `{"claim_id": "INV-009", "probe_id": "p", "outcome": "verified"},
+		{"claim_id": "INV-009", "probe_id": "p", "outcome": "counterexample"}`
+	docPath := write(t, outside, "doc.json", docFor("dafny-worker", "abc", goodDigest, rows))
+	cfgPath := write(t, outside, "cfg.json", configFor(docPath, false))
+	cfg, err := LoadConfig(cfgPath, repo)
+	if err != nil {
+		t.Fatal(err)
+	}
+	if _, _, err := Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims()); err == nil ||
+		!strings.Contains(err.Error(), "contradictory verdicts") {
+		t.Errorf("contradiction tolerated: %v", err)
+	}
+}
+
+// TestCrossSupplierCounterexampleSurvives: refutation dominance across
+// suppliers. Supplier A's pass on a raw probe id must NOT suppress supplier
+// B's counterexample on the same raw id — the namespaced probes are
+// distinct evidence, and the demonstrated global-dedupe hole let a pass
+// launder a refutation away.
+func TestCrossSupplierCounterexampleSurvives(t *testing.T) {
+	repo := t.TempDir()
+	outside := t.TempDir()
+	subj := Subject{HeadSHA: "abc", InputDigest: goodDigest}
+	passDoc := write(t, outside, "a.json", docFor("prover-a", "abc", goodDigest,
+		`{"claim_id": "INV-009", "probe_id": "shared", "outcome": "verified"}`))
+	cxDoc := write(t, outside, "b.json", docFor("prover-b", "abc", goodDigest,
+		`{"claim_id": "INV-009", "probe_id": "shared", "outcome": "counterexample", "detail": "trace"}`))
+	cfgPath := write(t, outside, "cfg.json", fmt.Sprintf(`{
+  "intake_version": 1,
+  "suppliers": [
+    {"name": "prover-a", "mechanism": "proof-a", "max_tier": 4, "document": %q},
+    {"name": "prover-b", "mechanism": "proof-b", "max_tier": 4, "document": %q}
+  ]
+}`, passDoc, cxDoc))
+	cfg, err := LoadConfig(cfgPath, repo)
+	if err != nil {
+		t.Fatal(err)
+	}
+	extra, records, err := Run(cfg, repo, subj, testClaims())
+	if err != nil {
+		t.Fatal(err)
+	}
+	if records[0].Accepted != 1 || records[1].Accepted != 1 {
+		t.Fatalf("accepted = %d/%d, want both suppliers' rows: %+v", records[0].Accepted, records[1].Accepted, records)
+	}
+	rows := extra["INV-009"]
+	if len(rows) != 2 {
+		t.Fatalf("evidence rows = %d, want 2 distinct namespaced probes", len(rows))
+	}
+	refuted := false
+	for _, ev := range rows {
+		if ev.Refuted() {
+			refuted = true
+		}
+	}
+	if !refuted {
+		t.Error("the counterexample was suppressed — refutation dominance violated")
+	}
+}
+
+// TestDuplicateJSONKeysRejected: the stdlib decoder keeps a duplicate
+// key's last value — demonstrated to smuggle "outcome": "verified" behind
+// a counterexample — so strict decoding refuses duplicates at any depth.
+func TestDuplicateJSONKeysRejected(t *testing.T) {
+	repo := t.TempDir()
+	outside := t.TempDir()
+	doc := `{
+  "intake_version": 1,
+  "supplier": "dafny-worker",
+  "subject": {"head_sha": "abc", "input_digest": "` + goodDigest + `"},
+  "results": [
+    {"claim_id": "INV-009", "probe_id": "p", "outcome": "counterexample", "outcome": "verified"}
+  ]
+}`
+	docPath := write(t, outside, "doc.json", doc)
+	cfgPath := write(t, outside, "cfg.json", configFor(docPath, false))
+	cfg, err := LoadConfig(cfgPath, repo)
+	if err != nil {
+		t.Fatal(err)
+	}
+	if _, _, err := Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims()); err == nil ||
+		!strings.Contains(err.Error(), "duplicate key") {
+		t.Errorf("duplicate key tolerated: %v", err)
+	}
+}
+
+// TestParentSymlinkCannotSmuggleInTreeFiles: containment is CANONICAL. A
+// symlinked parent directory that resolves into the repository tree was
+// demonstrated to pass a lexical prefix check; the resolved path is what
+// the boundary judges.
+func TestParentSymlinkCannotSmuggleInTreeFiles(t *testing.T) {
+	repo := t.TempDir()
+	outside := t.TempDir()
+	if err := os.MkdirAll(filepath.Join(repo, "evil"), 0o755); err != nil {
+		t.Fatal(err)
+	}
+	write(t, filepath.Join(repo, "evil"), "doc.json", docFor("dafny-worker", "abc", goodDigest,
+		`{"claim_id": "INV-009", "probe_id": "p", "outcome": "verified"}`))
+	linkDir := filepath.Join(outside, "looks-external")
+	if err := os.Symlink(filepath.Join(repo, "evil"), linkDir); err != nil {
+		t.Fatal(err)
+	}
+	cfgPath := write(t, outside, "cfg.json", configFor(filepath.Join(linkDir, "doc.json"), false))
+	cfg, err := LoadConfig(cfgPath, repo)
+	if err != nil {
+		t.Fatal(err)
+	}
+	if _, _, err := Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims()); err == nil ||
+		!strings.Contains(err.Error(), "inside the repository tree") {
+		t.Errorf("parent symlink smuggled an in-tree document: %v", err)
+	}
+}
+
+// TestRequiredNeedsUsableEvidence: an admitted document with zero accepted
+// rows — empty, or every row rejected — satisfies nothing. Required means
+// usable evidence arrived.
+func TestRequiredNeedsUsableEvidence(t *testing.T) {
+	repo := t.TempDir()
+	outside := t.TempDir()
+	subj := Subject{HeadSHA: "abc", InputDigest: goodDigest}
+	for name, rows := range map[string]string{
+		"empty":        "",
+		"all rejected": `{"claim_id": "INV-404", "probe_id": "p", "outcome": "verified"}`,
+	} {
+		docPath := write(t, outside, "doc-"+strings.ReplaceAll(name, " ", "-")+".json",
+			docFor("dafny-worker", "abc", goodDigest, rows))
+		cfgPath := write(t, outside, "cfg-"+strings.ReplaceAll(name, " ", "-")+".json", configFor(docPath, true))
+		cfg, err := LoadConfig(cfgPath, repo)
+		if err != nil {
+			t.Fatal(err)
+		}
+		_, records, err := Run(cfg, repo, subj, testClaims())
+		if err != nil {
+			t.Fatal(err)
+		}
+		r := schema.Receipt{Intake: records}
+		if !r.GateBlocked() {
+			t.Errorf("%s: required document with nothing usable did not block", name)
+		}
+	}
+}
+
+// TestRejectedRowsAreScrubbed: rejection fields render in receipts, so
+// control characters (an ESC sequence, demonstrated live; DEL and C1 are
+// covered by the same scrub) must not survive into them — and the audit
+// record carries the supplier version and the config digest. The ESC
+// arrives through JSON's \u001b escape, exactly as a hostile document
+// would deliver it.
+func TestRejectedRowsAreScrubbed(t *testing.T) {
+	repo := t.TempDir()
+	outside := t.TempDir()
+	rows := `{"claim_id": "INV-\u001b[31m999", "probe_id": "p1", "outcome": "verified"}`
+	docPath := write(t, outside, "doc.json", docFor("dafny-worker", "abc", goodDigest, rows))
+	cfgPath := write(t, outside, "cfg.json", strings.Replace(configFor(docPath, false),
+		`"mechanism"`, `"version": "1.2.0", "mechanism"`, 1))
+	cfg, err := LoadConfig(cfgPath, repo)
+	if err != nil {
+		t.Fatal(err)
+	}
+	_, records, err := Run(cfg, repo, Subject{HeadSHA: "abc", InputDigest: goodDigest}, testClaims())
+	if err != nil {
+		t.Fatal(err)
+	}
+	rec := records[0]
+	if len(rec.Rejected) != 1 {
+		t.Fatalf("rejected = %+v", rec.Rejected)
+	}
+	for _, s := range []string{rec.Rejected[0].ClaimID, rec.Rejected[0].ProbeID} {
+		for _, r := range s {
+			if r < 0x20 || r == 0x7F || (r >= 0x80 && r <= 0x9F) {
+				t.Errorf("control character %U survived in %q", r, s)
+			}
+		}
+	}
+	if !strings.Contains(rec.Rejected[0].ClaimID, "INV-") || !strings.Contains(rec.Rejected[0].ClaimID, "999") {
+		t.Errorf("scrub destroyed the printable content: %q", rec.Rejected[0].ClaimID)
+	}
+	if rec.SupplierVersion != "1.2.0" {
+		t.Errorf("supplier version = %q, want the profile's declaration", rec.SupplierVersion)
+	}
+	if rec.ConfigDigest == "" {
+		t.Error("config digest absent — the authority file is unpinned")
+	}
+}