Add the evidence-intake contract: external suppliers behind profile authority

DESIGN.md

@@ -447,6 +447,70 @@ demands the tie discipline (id-annotated code reconciled with id-named
 tests, or LLM extraction with confirmed edges), and states exactly what is
 missing when a repo has not adopted it.
 
+## The evidence-intake contract (schema 0.0.12): external suppliers
+
+The probe-supplier surface, opened: an external tool submits evidence rows
+through a schema-shaped intake document, and correctful validates, binds,
+combines, and applies policy — without becoming every probe runner. The
+first draft of this contract was reshaped by an adversarial pre-implementation
+design review; the five critical findings it surfaced are now the design:
+
+1. **The row must not control its own authority.** The draft let a
+   document carry its own tier and mechanism — one JSON file could mint T4
+   evidence for any claim. Authority now lives in an invoker-owned
+   PROFILE: the intake config fixes each supplier's name, mechanism, and
+   maximum tier (the external analogue of `Runner.MaxTier`), and a row
+   reports an OUTCOME only.
+2. **Outcomes are an enum, not booleans.** `verified / counterexample /
+   inconclusive / not_run / error` — only a counterexample refutes. A
+   proof failure can mean *unproved*; a fuzzer timeout means *incomplete*;
+   neither is a refutation. This is the same lesson the go-test runners
+   learned from `t.Skip` exiting 0, applied at the contract boundary.
+3. **Subject identity is head SHA plus input digest, both required.** A
+   mismatch rejects the whole document as stale, disclosed. Known
+   boundary, stated: this names the committed tree and the changed-file
+   overlay, not the dependency closure — a full source-snapshot digest is
+   a later field.
+4. **Selective reporting is mitigated, not solved.** A profile can be
+   `required`: a required supplier with no admitted document blocks the
+   gate. Rejected rows are listed with identity and reason, never reduced
+   to a count — a rejected counterexample naming an unknown claim can
+   expose claim drift and must stay visible. The full manifest protocol
+   (correctful hands the supplier a probe manifest; the supplier returns
+   one outcome per entry) is deferred and named.
+5. **A claim-id match is not a binding.** Rows for ambiguously anchored
+   claims are rejected; every admitted row carries `binding:
+   supplier-attested` — the receipt's statement that the tie is the
+   supplier's word. Claim fingerprints are deferred.
+
+Mechanics that follow the same discipline: probe ids are NAMESPACED BY
+CONSTRUCTION (`ext:<supplier>/…` — a blacklist of built-in prefixes would
+be enumeration, and enumeration is how extractors go class-incomplete);
+strict JSON decoding rejects unknown fields; documents and config must be
+regular files OUTSIDE the repository tree, symlinks rejected — evidence
+the reviewed change can write is not evidence; every external string is
+control-stripped and bounded, and details pass the same sanitization
+chokepoint as in-tree evidence; the receipt's intake records carry the
+admitted document's SHA-256 as the audit pin. Policy floors may reference
+supplier mechanisms, so the policy mechanism vocabulary opened from an
+enum to a token shape — a typo now fails closed as an unsatisfiable floor
+instead of loudly at load, and the miss row shows the gap.
+
+Residual trust, stated plainly: admission authenticates possession of the
+invoker's config, not origin, and a trusted supplier can still lie, omit
+work, or bind the wrong property. The `[external: … — supplier-attested]`
+marker on every acting row is the receipt refusing to launder that trust
+into the appearance of an in-tree run. The signature channel (binding a
+document to a runner identity) is the planned stronger leg.
+
+Measured (first live runs, on this repository's own change): an admitted
+document verified a real claim at T4 with the external marker, disclosed
+an unbound counterexample among its rejections, and left the gate green;
+flipping the row to a counterexample refuted the claim, marked the
+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.
+
 ## Known limitations (found by dogfooding, stated honestly)
 
 correctful was run on itself and on a real 101-file production change on its

README.md

@@ -152,6 +152,60 @@ accept/reject test pair. A rule can also demand a measured execution scope
 | MUST clauses in a normative document | a must-clause claim | no probe is available — the claim stays in the remainder | T0 |
 | nothing (`-llm`) | LLM proposals, with the mark `[llm-proposed]` | a changed test, only when the model names it and coverage confirms the link | T0 or T1 |
 
+## External evidence (optional)
+
+An external tool — a fuzzer, a proof worker, an observation system — can
+supply evidence rows. correctful validates and binds them. It does not run
+the tool, and it cannot check the tool's work. Each supplied row shows the
+mark `[external: <supplier> — supplier-attested]`, so a reader can weigh
+the residual trust.
+
+Authority comes from you, the invoker, never from the document. Write an
+intake config **outside the repository tree**, and point the run at it:
+
+```sh
+correctful -base main -intake /ci/intake.json
+```
+
+```json
+{
+  "intake_version": 1,
+  "suppliers": [
+    {"name": "proof-worker", "mechanism": "dafny-proof", "max_tier": 4,
+     "document": "/ci/out/proofs.json", "required": true}
+  ]
+}
+```
+
+The profile fixes the supplier's name, mechanism, and maximum tier. The
+supplier's document reports outcomes only:
+
+```json
+{
+  "intake_version": 1,
+  "supplier": "proof-worker",
+  "subject": {"head_sha": "<sha>", "input_digest": "<sha256>"},
+  "results": [
+    {"claim_id": "INV-009", "probe_id": "specs/gate.dfy:GateSafe",
+     "outcome": "verified", "detail": "proof verified, 0 errors"}
+  ]
+}
+```
+
+The rules:
+
+- The subject must match the receipt exactly: head SHA and input digest.
+  A mismatch rejects the whole document as stale, with disclosure.
+- The outcome is one of: `verified`, `counterexample`, `inconclusive`,
+  `not_run`, `error`. Only a counterexample refutes. An unproved proof or
+  a fuzzer timeout never reads as a refutation.
+- A row cannot set its own tier or mechanism. The profile's values apply.
+- Rows that name unknown claims are rejected and listed with reasons. A
+  rejected counterexample stays visible — it can expose claim drift.
+- A `required` supplier with no admitted document blocks the gate.
+- Config and documents must be regular files outside the repository. The
+  change under review must not supply its own evidence.
+
 ## The evidence tiers
 
 Each claim carries a tier. The tier tells you how strong the evidence is.

cmd/correctful/main.go

@@ -17,9 +17,10 @@
 //	-concurrency  max probes to run at once. Default: 4.
 //	-timeout      overall probe budget. Default: 5m.
 //
-// Exit status: 0 when no claim was refuted and every declared policy floor was
-// met; 1 on a refutation or a policy miss (merge-gate semantics). The
-// remainder never fails the run — it is an honest report, not a defect.
+// Exit status: 0 when the gate passes; 1 on a refutation, a policy miss, or a
+// required intake supplier with no admitted document (merge-gate semantics —
+// schema.Receipt.GateBlocked is the definition). The remainder never fails
+// the run — it is an honest report, not a defect.
 package main
 
 import (
@@ -31,10 +32,12 @@ import (
 
 	"github.com/joshft/correctful/internal/gitdiff"
 	"github.com/joshft/correctful/internal/harvest"
+	"github.com/joshft/correctful/internal/intake"
 	"github.com/joshft/correctful/internal/llmextract"
 	"github.com/joshft/correctful/internal/policy"
 	"github.com/joshft/correctful/internal/probe"
 	"github.com/joshft/correctful/internal/receipt"
+	"github.com/joshft/correctful/schema"
 )
 
 func main() {
@@ -45,18 +48,19 @@ func main() {
 	concurrency := flag.Int("concurrency", 4, "max probes to run at once")
 	timeout := flag.Duration("timeout", 5*time.Minute, "overall probe budget")
 	useLLM := flag.Bool("llm", false, "additionally PROPOSE claims from the diff with an LLM (needs ANTHROPIC_API_KEY; proposals are unverified and land in the remainder)")
+	intakePath := flag.String("intake", "", "invoker-owned intake config admitting evidence from EXTERNAL suppliers (must live outside the repo tree; see README)")
 	flag.Parse()
 
 	if *asJSON {
 		*format = "json"
 	}
-	if err := run(*base, *repo, *format, *concurrency, *timeout, *useLLM); err != nil {
+	if err := run(*base, *repo, *format, *concurrency, *timeout, *useLLM, *intakePath); err != nil {
 		fmt.Fprintln(os.Stderr, "correctful:", err)
 		os.Exit(2)
 	}
 }
 
-func run(base, repo, format string, concurrency int, timeout time.Duration, useLLM bool) error {
+func run(base, repo, format string, concurrency int, timeout time.Duration, useLLM bool, intakePath string) error {
 	switch format {
 	case "text", "json", "md":
 	default:
@@ -102,6 +106,15 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL
 	if err != nil {
 		return err
 	}
+	// Intake config loads with the policy: authority grants fail loudly
+	// before any probe runs.
+	var intakeCfg *intake.Config
+	if intakePath != "" {
+		intakeCfg, err = intake.LoadConfig(intakePath, root)
+		if err != nil {
+			return err
+		}
+	}
 
 	// Harvest claims, then dispatch probes against them.
 	harvesters := harvest.Default()
@@ -138,7 +151,25 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL
 	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
+	if intakeCfg != nil {
+		subj := intake.Subject{HeadSHA: change.HeadSHA, InputDigest: change.InputDigest}
+		extra, records, 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...)
+			}
+		}
+		intakeRecords = records
+	}
+
 	r := receipt.Assemble(change, claims, evidence, coverage)
+	r.Intake = intakeRecords
 	if pol != nil {
 		r.Policy = policy.Evaluate(pol, r)
 	}
@@ -154,7 +185,7 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL
 		receipt.WriteText(os.Stdout, r)
 	}
 
-	if r.Summary.Refuted > 0 || (r.Policy != nil && len(r.Policy.Misses) > 0) {
+	if r.GateBlocked() {
 		os.Exit(1)
 	}
 	return nil