From d71583e69db0758c7eee6ecf318184d8f5194b74 Mon Sep 17 00:00:00 2001 From: Josh Terry Date: Mon, 17 Aug 2026 18:04:02 -0700 Subject: [PATCH] Add the evidence-intake contract: external suppliers behind profile authority MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The probe-supplier surface opens: an external tool (fuzzer, proof worker, observation plane) submits evidence rows through an intake document, and correctful validates, binds, combines, and applies policy without becoming every probe runner. An adversarial pre-implementation design review reshaped the draft; its five critical findings are the design: - Authority lives in an invoker-owned profile (name, mechanism, max tier — the external Runner.MaxTier), never in the row. - Outcomes are an enum: verified / counterexample / inconclusive / not_run / error. Only a counterexample refutes — an unproved proof or a fuzzer timeout is not a refutation (the t.Skip lesson, applied at the contract boundary). - Subject identity is head SHA plus input digest, both required; a mismatch rejects the whole document as stale, disclosed. - A required supplier with no admitted document blocks the gate; rejected rows keep identity, outcome, and reason — a rejected counterexample can expose claim drift and stays visible. - Ambiguously anchored claims reject rows; every admitted row carries binding "supplier-attested" and an [external: …] marker on verified AND refuted rows — the receipt never launders supplied trust. Probe ids are namespaced by construction (ext:/…), decoding is strict, paths must be regular files outside the repository tree, all external strings are control-stripped and bounded, and the admitted document's SHA-256 is the audit pin. Policy mechanisms opened from an enum to a token shape so floors can require supplier mechanisms — a typo fails closed as an unsatisfiable floor. Receipt.GateBlocked is now THE gate definition shared by main and the renderers' exit-gate line, which the text receipt now prints too. Schema 0.0.12. Live-verified on this change: admitted document → T4 verified row with external marker and gate green; counterexample row → refuted, marked, blocked; missing required document → blocked with the reason on the intake line. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_015GeUG1gboWiZSnFyzQghyp --- DESIGN.md | 64 ++++++ README.md | 54 +++++ cmd/correctful/main.go | 43 +++- internal/intake/intake.go | 375 +++++++++++++++++++++++++++++++ internal/intake/intake_test.go | 304 +++++++++++++++++++++++++ internal/policy/policy.go | 16 +- internal/policy/policy_test.go | 22 +- internal/receipt/markdown.go | 15 +- internal/receipt/receipt.go | 65 +++++- internal/receipt/receipt_test.go | 63 ++++++ schema/schema.go | 73 +++++- 11 files changed, 1065 insertions(+), 29 deletions(-) create mode 100644 internal/intake/intake.go create mode 100644 internal/intake/intake_test.go diff --git a/DESIGN.md b/DESIGN.md index 5281199..360203a 100644 --- a/DESIGN.md +++ b/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:/…` — 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 diff --git a/README.md b/README.md index 772d666..fbf2204 100644 --- a/README.md +++ b/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-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": "", "input_digest": ""}, + "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. diff --git a/cmd/correctful/main.go b/cmd/correctful/main.go index e3508d4..d0a741d 100644 --- a/cmd/correctful/main.go +++ b/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 diff --git a/internal/intake/intake.go b/internal/intake/intake.go new file mode 100644 index 0000000..ead1472 --- /dev/null +++ b/internal/intake/intake.go @@ -0,0 +1,375 @@ +// Package intake admits evidence from EXTERNAL probe suppliers — fuzzers, +// proof workers, observation planes — through a schema-shaped contract, so +// correctful validates, binds, combines, and applies policy without becoming +// every probe runner. +// +// The trust model is explicit, because correctful cannot re-execute an +// external probe. Authority lives in an invoker-owned PROFILE, never in the +// document: the profile fixes the supplier's name, mechanism, and maximum +// tier (the external analogue of Runner.MaxTier), and a row reports an +// OUTCOME only — it cannot select its own tier, mechanism, or supplier. +// Admission requires a subject match (head SHA and input digest both), and +// every admitted row is marked Binding "supplier-attested": the residual +// trust — the supplier could still lie, omit work, or bind the wrong +// property — is the supplier's word, and the receipt says so on the row. +// A signature channel is the planned stronger leg; until then, admission +// authenticates possession of the invoker's config, not origin. +// +// Fail-closed and fail-loud rules: +// - A malformed config or document is a loud error before any probe runs. +// - Config and documents must be regular files OUTSIDE the repository +// tree (symlinks rejected): evidence readable from the reviewed change's +// own tree would let the change mint evidence for its own claims. +// - A subject mismatch rejects the WHOLE document (stale — about other +// content), recorded and disclosed, never silently dropped. +// - A required supplier with no admitted document blocks the gate. +// - Outcomes are an enum, not booleans: only "counterexample" refutes. +// "inconclusive", "not_run", and "error" are Ran=false — an unproved +// proof or a fuzzer timeout must never read as a refutation (the same +// lesson the go-test runners learned from t.Skip's exit 0). +package intake + +import ( + "bytes" + "crypto/sha256" + "encoding/json" + "fmt" + "os" + "path/filepath" + "regexp" + "strings" + + "github.com/joshft/correctful/schema" +) + +// Bounds — strict limits so a document cannot balloon a receipt. +const ( + maxSuppliers = 16 + maxDocBytes = 4 << 20 + maxRows = 500 + maxDetailLen = 300 + maxProbeIDLen = 200 +) + +// Config is the invoker-owned intake configuration: the authority grants. +type Config struct { + IntakeVersion int `json:"intake_version"` + Suppliers []Profile `json:"suppliers"` +} + +// Profile is one supplier's authority grant. +type Profile struct { + // Name identifies the supplier; token shape, and the value every + // admitted row's Evidence.Supplier carries. + Name string `json:"name"` + // Mechanism is the evidence class the invoker vouches this supplier + // produces (e.g. "dafny-proof"). Policy floors reference it. Must not + // collide with a built-in runner mechanism. + Mechanism string `json:"mechanism"` + // MaxTier is the tier a verified outcome from this supplier confers — + // the authority clamp. Rows carry no tier at all. + MaxTier int `json:"max_tier"` + // Document is the path to this supplier's intake document. Must live + // outside the repository tree. + Document string `json:"document"` + // Required blocks the gate when no document is admitted. + Required bool `json:"required,omitempty"` +} + +// Document is one supplier run's report. +type document struct { + IntakeVersion int `json:"intake_version"` + Supplier string `json:"supplier"` + Subject subject `json:"subject"` + Results []row `json:"results"` +} + +// subject pins WHAT the supplier's probes ran against. Both fields must +// match the receipt's own change identity. Known boundary, disclosed in +// DESIGN.md: this names the committed tree plus the changed-file overlay, +// not the full dependency closure. +type subject struct { + HeadSHA string `json:"head_sha"` + InputDigest string `json:"input_digest"` +} + +// row is one probe outcome. No tier, no mechanism, no supplier — authority +// is the profile's, not the row's. +type row struct { + ClaimID string `json:"claim_id"` + ProbeID string `json:"probe_id"` + Outcome string `json:"outcome"` + Detail string `json:"detail"` + Duration string `json:"duration"` +} + +// Outcome vocabulary. Only OutcomeCounterexample refutes. +const ( + OutcomeVerified = "verified" + OutcomeCounterexample = "counterexample" + OutcomeInconclusive = "inconclusive" + OutcomeNotRun = "not_run" + OutcomeError = "error" +) + +var validOutcomes = map[string]bool{ + OutcomeVerified: true, OutcomeCounterexample: true, + OutcomeInconclusive: true, OutcomeNotRun: true, OutcomeError: true, +} + +// tokenRe is the shape for supplier names and mechanisms. +var tokenRe = regexp.MustCompile(`^[a-z0-9][a-z0-9-]{0,63}$`) + +// hexDigestRe is a canonical SHA-256 hex digest. +var hexDigestRe = regexp.MustCompile(`^[0-9a-f]{64}$`) + +// builtinMechanisms a profile must not claim — an external supplier cannot +// masquerade as an in-tree runner. +var builtinMechanisms = map[string]bool{ + schema.MechanismGoTest: true, schema.MechanismGoTestPair: true, + schema.MechanismDotnetTest: true, schema.MechanismAlloyCheck: true, +} + +// LoadConfig reads and validates the intake config. Loud on every failure — +// a broken authority grant must never fail open. repoRoot guards the +// out-of-tree rule for the config itself and every document path. +func LoadConfig(path, repoRoot string) (*Config, error) { + if err := outsideTree(path, repoRoot); err != nil { + return nil, fmt.Errorf("intake config: %w", err) + } + data, err := os.ReadFile(path) + if err != nil { + return nil, fmt.Errorf("reading intake config: %w", err) + } + var c Config + if err := strictDecode(data, &c); err != nil { + return nil, fmt.Errorf("intake config %s: %w", path, err) + } + if c.IntakeVersion != 1 { + return nil, fmt.Errorf("intake config: intake_version %d is not supported (want 1)", c.IntakeVersion) + } + if len(c.Suppliers) == 0 || len(c.Suppliers) > maxSuppliers { + return nil, fmt.Errorf("intake config: %d suppliers (want 1–%d)", len(c.Suppliers), maxSuppliers) + } + seen := map[string]bool{} + for i, p := range c.Suppliers { + switch { + case !tokenRe.MatchString(p.Name): + return nil, fmt.Errorf("intake config: supplier %d name %q is not a lowercase token", i, p.Name) + case seen[p.Name]: + return nil, fmt.Errorf("intake config: duplicate supplier %q", p.Name) + case !tokenRe.MatchString(p.Mechanism): + return nil, fmt.Errorf("intake config: supplier %q mechanism %q is not a lowercase token", p.Name, p.Mechanism) + case builtinMechanisms[p.Mechanism]: + return nil, fmt.Errorf("intake config: supplier %q claims built-in mechanism %q", p.Name, p.Mechanism) + case p.MaxTier < 1 || p.MaxTier > 4: + return nil, fmt.Errorf("intake config: supplier %q max_tier %d out of range (1–4)", p.Name, p.MaxTier) + case p.Document == "": + return nil, fmt.Errorf("intake config: supplier %q has no document path", p.Name) + } + seen[p.Name] = true + } + return &c, nil +} + +// Subject is the receipt-side change identity documents must match. +type Subject struct { + HeadSHA string + InputDigest string +} + +// Run admits each profile's document and converts accepted rows into +// evidence, keyed by claim id. Every profile yields an IntakeRecord — +// including profiles whose document was missing or rejected. +func Run(c *Config, repoRoot string, subj Subject, claims []schema.Claim) (map[string][]schema.Evidence, []schema.IntakeRecord, error) { + claimByID := make(map[string]*schema.Claim, len(claims)) + for i := range claims { + claimByID[claims[i].ID] = &claims[i] + } + extra := map[string][]schema.Evidence{} + var records []schema.IntakeRecord + seenProbe := map[string]bool{} // (claim, probe) across ALL documents + + for _, p := range c.Suppliers { + rec := schema.IntakeRecord{Supplier: p.Name, Mechanism: p.Mechanism, + MaxTier: schema.Tier(p.MaxTier), Required: p.Required} + doc, digest, reason, err := admit(p, repoRoot, subj) + if err != nil { + return nil, nil, err + } + if doc == nil { + rec.Reason = reason + records = append(records, rec) + continue + } + rec.Admitted, rec.DocDigest = true, digest + for _, r := range doc.Results { + if reason := rejectRow(r, claimByID, seenProbe); reason != "" { + rec.Rejected = append(rec.Rejected, schema.IntakeRejection{ + ClaimID: clip(r.ClaimID, maxProbeIDLen), ProbeID: clip(r.ProbeID, maxProbeIDLen), + Outcome: r.Outcome, Reason: reason, + }) + continue + } + seenProbe[r.ClaimID+"\x00"+r.ProbeID] = true + ev := evidenceFrom(p, r) + extra[r.ClaimID] = append(extra[r.ClaimID], ev) + rec.Accepted++ + } + records = append(records, rec) + } + return extra, records, nil +} + +// admit loads one supplier's document and checks the admission gates. A +// missing or mismatched document is (nil, reason) — recorded, not an error; +// a malformed one IS an error, same as a malformed config. +func admit(p Profile, repoRoot string, subj Subject) (*document, string, string, error) { + if err := outsideTree(p.Document, repoRoot); err != nil { + return nil, "", "", fmt.Errorf("intake document for %q: %w", p.Name, err) + } + data, err := os.ReadFile(p.Document) + if os.IsNotExist(err) { + return nil, "", "no document at the configured path", nil + } + if err != nil { + return nil, "", "", fmt.Errorf("reading intake document for %q: %w", p.Name, err) + } + if len(data) > maxDocBytes { + return nil, "", "", fmt.Errorf("intake document for %q exceeds %d bytes", p.Name, maxDocBytes) + } + var doc document + if err := strictDecode(data, &doc); err != nil { + return nil, "", "", fmt.Errorf("intake document for %q: %w", p.Name, err) + } + switch { + case doc.IntakeVersion != 1: + return nil, "", "", fmt.Errorf("intake document for %q: intake_version %d is not supported (want 1)", p.Name, doc.IntakeVersion) + case len(doc.Results) > maxRows: + return nil, "", "", fmt.Errorf("intake document for %q: %d rows exceeds the %d-row bound", p.Name, len(doc.Results), maxRows) + case doc.Supplier != p.Name: + return nil, "", fmt.Sprintf("document names supplier %q, profile is %q", clip(doc.Supplier, 64), p.Name), nil + case !hexDigestRe.MatchString(doc.Subject.InputDigest): + return nil, "", "subject input_digest is not a canonical sha256 hex digest", nil + case doc.Subject.HeadSHA != subj.HeadSHA || doc.Subject.InputDigest != subj.InputDigest: + return nil, "", "subject mismatch — the evidence is about different content", nil + } + return &doc, fmt.Sprintf("%x", sha256.Sum256(data)), "", nil +} + +// rejectRow returns the reason a row does not become evidence, or "". +func rejectRow(r row, claims map[string]*schema.Claim, seen map[string]bool) string { + switch { + case !validOutcomes[r.Outcome]: + return "unknown outcome (want verified, counterexample, inconclusive, not_run, or error)" + case r.ProbeID == "" || len(r.ProbeID) > maxProbeIDLen: + return "probe_id empty or too long" + case r.ClaimID == "": + return "claim_id empty" + case seen[r.ClaimID+"\x00"+r.ProbeID]: + return "duplicate (claim_id, probe_id) across intake documents" + } + c, ok := claims[r.ClaimID] + if !ok { + return "no such claim in this change" + } + if c.Anchor != nil && c.Anchor.Status == schema.AnchorAmbiguous { + return "claim id is ambiguously anchored — the evidence cannot say which definition it verified" + } + return "" +} + +// evidenceFrom converts an accepted row. Tier, mechanism, and supplier come +// from the PROFILE; the probe id is namespaced by construction (never +// trusted to avoid built-in prefixes — it cannot collide with them). +func evidenceFrom(p Profile, r row) schema.Evidence { + ev := schema.Evidence{ + ClaimID: r.ClaimID, + ProbeID: "ext:" + p.Name + "/" + scrub(clip(r.ProbeID, maxProbeIDLen)), + Tier: schema.Tier(p.MaxTier), + Mechanism: p.Mechanism, + Supplier: p.Name, + Binding: schema.BindingSupplierAttested, + Detail: scrub(clip(r.Detail, maxDetailLen)), + Duration: scrub(clip(r.Duration, 32)), + } + switch r.Outcome { + case OutcomeVerified: + ev.Ran, ev.Passed = true, true + if ev.Detail == "" { + ev.Detail = "supplier reported verified" + } + case OutcomeCounterexample: + ev.Ran, ev.Passed = true, false + if ev.Detail == "" { + ev.Detail = "supplier reported a counterexample" + } + default: // inconclusive, not_run, error — never a verdict + ev.Ran, ev.Passed = false, false + ev.Detail = strings.TrimSpace(r.Outcome + " — " + ev.Detail) + } + return ev +} + +// outsideTree rejects symlinks, non-regular files, and any path under the +// repository root: evidence the reviewed change can write is not evidence. +func outsideTree(path, repoRoot string) error { + fi, err := os.Lstat(path) + if err != nil { + if os.IsNotExist(err) { + return nil // absence is handled by the caller (recorded, not fatal) + } + return err + } + if fi.Mode()&os.ModeSymlink != 0 { + return fmt.Errorf("%s is a symlink — intake paths must be regular files", path) + } + if !fi.Mode().IsRegular() { + return fmt.Errorf("%s is not a regular file", path) + } + abs, err := filepath.Abs(path) + if err != nil { + return err + } + root, err := filepath.Abs(repoRoot) + if err != nil { + return err + } + if abs == root || strings.HasPrefix(abs, root+string(filepath.Separator)) { + return fmt.Errorf("%s is inside the repository tree — the reviewed change must not supply its own evidence", path) + } + return nil +} + +// strictDecode parses JSON with unknown fields rejected and trailing +// content refused. +func strictDecode(data []byte, v any) error { + dec := json.NewDecoder(bytes.NewReader(data)) + dec.DisallowUnknownFields() + if err := dec.Decode(v); err != nil { + return err + } + if dec.More() { + return fmt.Errorf("trailing content after the JSON document") + } + return nil +} + +// scrub strips control characters from an external string — supplied text +// reaches terminals and PR comments, and must not carry escapes. Path +// scrubbing happens later at the receipt's sanitization chokepoint. +func scrub(s string) string { + return strings.Map(func(r rune) rune { + if r < 0x20 && r != '\n' && r != '\t' { + return -1 + } + return r + }, s) +} + +func clip(s string, n int) string { + if len(s) <= n { + return s + } + return s[:n] + "…" +} diff --git a/internal/intake/intake_test.go b/internal/intake/intake_test.go new file mode 100644 index 0000000..71d8ac3 --- /dev/null +++ b/internal/intake/intake_test.go @@ -0,0 +1,304 @@ +package intake + +import ( + "crypto/sha256" + "fmt" + "os" + "path/filepath" + "strings" + "testing" + + "github.com/joshft/correctful/schema" +) + +const goodDigest = "a41e90b65deb1111111111111111111111111111111111111111111111111111" + +// write puts content at dir/name and returns the full path. +func write(t *testing.T, dir, name, content string) string { + t.Helper() + p := filepath.Join(dir, name) + if err := os.WriteFile(p, []byte(content), 0o644); err != nil { + t.Fatal(err) + } + return p +} + +func configFor(docPath string, required bool) string { + return fmt.Sprintf(`{ + "intake_version": 1, + "suppliers": [ + {"name": "dafny-worker", "mechanism": "dafny-proof", "max_tier": 4, + "document": %q, "required": %v} + ] +}`, docPath, required) +} + +func docFor(supplier, headSHA, inputDigest, rows string) string { + return fmt.Sprintf(`{ + "intake_version": 1, + "supplier": %q, + "subject": {"head_sha": %q, "input_digest": %q}, + "results": [%s] +}`, supplier, headSHA, inputDigest, rows) +} + +func testClaims() []schema.Claim { + return []schema.Claim{ + {ID: "INV-009", Shape: schema.ShapeInvariant, Text: "the gate holds"}, + {ID: "INV-777", Shape: schema.ShapeInvariant, Text: "ambiguous id", + Anchor: &schema.Anchor{Status: schema.AnchorAmbiguous}}, + } +} + +// TestConfigValidatesLoudly: the authority grant fails loudly on every +// malformed shape — including a profile claiming a built-in mechanism, the +// masquerade the contract must make impossible. +func TestConfigValidatesLoudly(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + + good := write(t, outside, "intake.json", configFor(filepath.Join(outside, "doc.json"), false)) + if _, err := LoadConfig(good, repo); err != nil { + t.Fatalf("valid config rejected: %v", err) + } + + bad := map[string]string{ + "wrong version": `{"intake_version": 2, "suppliers": [{"name": "a", "mechanism": "b", "max_tier": 1, "document": "x"}]}`, + "no suppliers": `{"intake_version": 1, "suppliers": []}`, + "bad name": `{"intake_version": 1, "suppliers": [{"name": "Not Token", "mechanism": "b", "max_tier": 1, "document": "x"}]}`, + "builtin mechanism": `{"intake_version": 1, "suppliers": [{"name": "a", "mechanism": "go-test", "max_tier": 1, "document": "x"}]}`, + "tier out of range": `{"intake_version": 1, "suppliers": [{"name": "a", "mechanism": "b", "max_tier": 5, "document": "x"}]}`, + "no document": `{"intake_version": 1, "suppliers": [{"name": "a", "mechanism": "b", "max_tier": 1, "document": ""}]}`, + "unknown field": `{"intake_version": 1, "surprise": true, "suppliers": [{"name": "a", "mechanism": "b", "max_tier": 1, "document": "x"}]}`, + "duplicate name": `{"intake_version": 1, "suppliers": [{"name": "a", "mechanism": "b", "max_tier": 1, "document": "x"}, {"name": "a", "mechanism": "c", "max_tier": 1, "document": "y"}]}`, + } + for name, content := range bad { + p := write(t, outside, "bad-"+strings.ReplaceAll(name, " ", "-")+".json", content) + if _, err := LoadConfig(p, repo); err == nil { + t.Errorf("%s: loaded without error — a broken authority grant must fail loudly", name) + } + } +} + +// TestInTreePathsRejected: evidence the reviewed change can write is not +// evidence. Config and documents inside the repo tree are refused, and a +// symlinked path is refused even when its target lies outside. +func TestInTreePathsRejected(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + + inTree := write(t, repo, "intake.json", configFor(filepath.Join(outside, "doc.json"), false)) + if _, err := LoadConfig(inTree, repo); err == nil || !strings.Contains(err.Error(), "inside the repository tree") { + t.Errorf("in-tree config: %v — want inside-the-repository rejection", err) + } + + target := write(t, outside, "real.json", configFor(filepath.Join(outside, "doc.json"), false)) + link := filepath.Join(outside, "link.json") + if err := os.Symlink(target, link); err != nil { + t.Fatal(err) + } + if _, err := LoadConfig(link, repo); err == nil || !strings.Contains(err.Error(), "symlink") { + t.Errorf("symlink config: %v — want symlink rejection", err) + } + + // A document inside the tree is an error even when the config is fine. + inTreeDoc := write(t, repo, "doc.json", docFor("dafny-worker", "abc", goodDigest, "")) + cfgPath := write(t, outside, "cfg2.json", configFor(inTreeDoc, 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 { + t.Error("in-tree document admitted — the reviewed change must not supply its own evidence") + } +} + +// TestAdmissionGates: a document is admitted only when its supplier matches +// the profile and its subject matches the receipt EXACTLY. Everything else +// is recorded with a reason — and a REQUIRED profile with nothing admitted +// blocks the gate through GateBlocked. +func TestAdmissionGates(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + subj := Subject{HeadSHA: "abc123", InputDigest: goodDigest} + row := `{"claim_id": "INV-009", "probe_id": "specs/gate.dfy:GateSafe", "outcome": "verified", "detail": "proof ok", "duration": "12s"}` + + cases := []struct { + name, doc string + wantReason string + }{ + {"admitted", docFor("dafny-worker", "abc123", goodDigest, row), ""}, + {"wrong supplier", docFor("other-tool", "abc123", goodDigest, row), "names supplier"}, + {"stale head", docFor("dafny-worker", "def456", goodDigest, row), "subject mismatch"}, + {"stale digest", docFor("dafny-worker", "abc123", strings.Repeat("b", 64), row), "subject mismatch"}, + {"malformed digest", docFor("dafny-worker", "abc123", "SHORT", row), "not a canonical sha256"}, + } + for _, tc := range cases { + t.Run(tc.name, func(t *testing.T) { + docPath := write(t, outside, "doc-"+strings.ReplaceAll(tc.name, " ", "-")+".json", tc.doc) + cfgPath := write(t, outside, "cfg-"+strings.ReplaceAll(tc.name, " ", "-")+".json", configFor(docPath, true)) + 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 len(records) != 1 { + t.Fatalf("records = %d, want 1 (every profile yields a record)", len(records)) + } + rec := records[0] + if tc.wantReason == "" { + if !rec.Admitted || rec.Accepted != 1 || len(extra["INV-009"]) != 1 { + t.Fatalf("admission failed: %+v / %v", rec, extra) + } + wantDigest := fmt.Sprintf("%x", sha256.Sum256([]byte(tc.doc))) + if rec.DocDigest != wantDigest { + t.Errorf("doc digest = %s, want sha256 of the exact bytes", rec.DocDigest) + } + return + } + if rec.Admitted || !strings.Contains(rec.Reason, tc.wantReason) { + t.Errorf("record = %+v, want rejection containing %q", rec, tc.wantReason) + } + r := schema.Receipt{Intake: records} + if !r.GateBlocked() { + t.Error("required profile with nothing admitted did not block the gate") + } + }) + } +} + +// TestAuthorityComesFromTheProfile: the row cannot select tier, mechanism, +// or supplier — accepted evidence carries the PROFILE's authority, the +// constructed ext: namespace, and the supplier-attested binding. +func TestAuthorityComesFromTheProfile(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + subj := Subject{HeadSHA: "abc", InputDigest: goodDigest} + row := `{"claim_id": "INV-009", "probe_id": "specs/gate.dfy:GateSafe", "outcome": "verified"}` + docPath := write(t, outside, "doc.json", docFor("dafny-worker", "abc", goodDigest, row)) + cfgPath := write(t, outside, "cfg.json", configFor(docPath, false)) + cfg, err := LoadConfig(cfgPath, repo) + if err != nil { + t.Fatal(err) + } + extra, _, err := Run(cfg, repo, subj, testClaims()) + if err != nil { + t.Fatal(err) + } + ev := extra["INV-009"][0] + if ev.Tier != schema.T4Mechanical || ev.Mechanism != "dafny-proof" || ev.Supplier != "dafny-worker" { + t.Errorf("authority = %+v, want the profile's tier/mechanism/supplier", ev) + } + if ev.ProbeID != "ext:dafny-worker/specs/gate.dfy:GateSafe" { + t.Errorf("probe id = %q, want the constructed ext: namespace", ev.ProbeID) + } + if ev.Binding != schema.BindingSupplierAttested { + t.Errorf("binding = %q, want supplier-attested", ev.Binding) + } + if !ev.CountsFor(testClaims()[0]) { + t.Error("admitted verified row does not count for its claim") + } +} + +// TestOutcomeVocabulary: only "counterexample" refutes. "inconclusive", +// "not_run", and "error" are Ran=false — an unproved proof or a fuzzer +// timeout must never read as a refutation. Unknown outcomes are rejected. +func TestOutcomeVocabulary(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + subj := Subject{HeadSHA: "abc", InputDigest: goodDigest} + cases := []struct { + outcome string + wantRan, wantPassed bool + rejected bool + }{ + {OutcomeVerified, true, true, false}, + {OutcomeCounterexample, true, false, false}, + {OutcomeInconclusive, false, false, false}, + {OutcomeNotRun, false, false, false}, + {OutcomeError, false, false, false}, + {"passed", false, false, true}, + } + for _, tc := range cases { + t.Run(tc.outcome, func(t *testing.T) { + row := fmt.Sprintf(`{"claim_id": "INV-009", "probe_id": "p", "outcome": %q, "detail": "d"}`, tc.outcome) + docPath := write(t, outside, "doc-"+tc.outcome+".json", docFor("dafny-worker", "abc", goodDigest, row)) + cfgPath := write(t, outside, "cfg-"+tc.outcome+".json", configFor(docPath, false)) + 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 tc.rejected { + if len(extra) != 0 || len(records[0].Rejected) != 1 { + t.Fatalf("unknown outcome not rejected: %v / %+v", extra, records) + } + return + } + ev := extra["INV-009"][0] + if ev.Ran != tc.wantRan || ev.Passed != tc.wantPassed { + t.Errorf("%s → ran=%v passed=%v, want %v/%v", tc.outcome, ev.Ran, ev.Passed, tc.wantRan, tc.wantPassed) + } + if ev.Refuted() != (tc.outcome == OutcomeCounterexample) { + t.Errorf("%s: Refuted() = %v — only a counterexample refutes", tc.outcome, ev.Refuted()) + } + }) + } +} + +// TestRowRejections: rows naming unknown claims, ambiguously anchored +// claims, or duplicate probes are rejected WITH the row's identity and +// reason — never reduced to a bare count, because a rejected counterexample +// can expose claim drift. +func TestRowRejections(t *testing.T) { + repo := t.TempDir() + outside := t.TempDir() + subj := Subject{HeadSHA: "abc", InputDigest: goodDigest} + rows := strings.Join([]string{ + `{"claim_id": "INV-999", "probe_id": "p1", "outcome": "counterexample", "detail": "boom"}`, + `{"claim_id": "INV-777", "probe_id": "p2", "outcome": "verified"}`, + `{"claim_id": "INV-009", "probe_id": "p3", "outcome": "verified"}`, + `{"claim_id": "INV-009", "probe_id": "p3", "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) + } + extra, records, err := Run(cfg, repo, subj, testClaims()) + if err != nil { + t.Fatal(err) + } + rec := records[0] + if rec.Accepted != 1 || len(extra["INV-009"]) != 1 { + t.Fatalf("accepted = %d, want exactly the one clean row", rec.Accepted) + } + if len(rec.Rejected) != 3 { + t.Fatalf("rejected = %+v, want 3 rows with reasons", rec.Rejected) + } + reasons := map[string]string{} + for _, rej := range rec.Rejected { + reasons[rej.ClaimID+"/"+rej.ProbeID] = rej.Reason + } + if !strings.Contains(reasons["INV-999/p1"], "no such claim") { + t.Errorf("unknown claim reason = %q", reasons["INV-999/p1"]) + } + if !strings.Contains(reasons["INV-777/p2"], "ambiguously anchored") { + t.Errorf("ambiguous anchor reason = %q", reasons["INV-777/p2"]) + } + if !strings.Contains(reasons["INV-009/p3"], "duplicate") { + t.Errorf("duplicate reason = %q", reasons["INV-009/p3"]) + } + for _, rej := range rec.Rejected { + if rej.ClaimID == "INV-999" && rej.Outcome != OutcomeCounterexample { + t.Error("rejected counterexample lost its outcome — claim drift must stay visible") + } + } +} diff --git a/internal/policy/policy.go b/internal/policy/policy.go index 14aa000..b7bff4b 100644 --- a/internal/policy/policy.go +++ b/internal/policy/policy.go @@ -25,6 +25,7 @@ import ( "os" "path" "path/filepath" + "regexp" "strings" "github.com/joshft/correctful/schema" @@ -61,10 +62,13 @@ type Policy struct { digest string } -var knownMechanisms = map[string]bool{ - schema.MechanismGoTest: true, schema.MechanismGoTestPair: true, - schema.MechanismDotnetTest: true, schema.MechanismAlloyCheck: true, -} +// mechanismRe is the token shape a rule's mechanism must have. The set is +// deliberately OPEN — a floor may require an external supplier's mechanism +// ("dafny-proof"), declared in the invoker's intake config, so a closed +// enum here would block the intake contract. The typo risk this admits +// fails CLOSED: a misspelled mechanism is an unsatisfiable floor, and the +// miss row shows the best evidence beside the requirement. +var mechanismRe = regexp.MustCompile(`^[a-z0-9][a-z0-9-]{0,63}$`) var knownScopes = map[string]bool{ schema.ScopeSinglePackage: true, schema.ScopeCrossPackage: true, @@ -98,8 +102,8 @@ func Load(root string) (*Policy, error) { if r.MinTier < 1 || r.MinTier > 4 { return nil, fmt.Errorf("%s: rule %d min_tier %d out of range (1–4)", File, i, r.MinTier) } - if r.Mechanism != "" && !knownMechanisms[r.Mechanism] { - return nil, fmt.Errorf("%s: rule %d names unknown mechanism %q", File, i, r.Mechanism) + if r.Mechanism != "" && !mechanismRe.MatchString(r.Mechanism) { + return nil, fmt.Errorf("%s: rule %d mechanism %q is not a lowercase token", File, i, r.Mechanism) } if r.Scope != "" && !knownScopes[r.Scope] { return nil, fmt.Errorf("%s: rule %d names unknown scope %q", File, i, r.Scope) diff --git a/internal/policy/policy_test.go b/internal/policy/policy_test.go index c1ddf13..541c2ff 100644 --- a/internal/policy/policy_test.go +++ b/internal/policy/policy_test.go @@ -50,19 +50,27 @@ func TestLoadValidatesAndDigests(t *testing.T) { } bad := map[string]string{ - "not json": `{"policy_version": 1,`, - "wrong version": `{"policy_version": 2, "rules": [{"paths": ["x"], "min_tier": 1}]}`, - "no rules": `{"policy_version": 1, "rules": []}`, - "rule without path": `{"policy_version": 1, "rules": [{"paths": [], "min_tier": 1}]}`, - "tier out of range": `{"policy_version": 1, "rules": [{"paths": ["x"], "min_tier": 5}]}`, - "unknown mechanism": `{"policy_version": 1, "rules": [{"paths": ["x"], "min_tier": 1, "mechanism": "jest"}]}`, - "unknown scope": `{"policy_version": 1, "rules": [{"paths": ["x"], "min_tier": 1, "scope": "galaxy"}]}`, + "not json": `{"policy_version": 1,`, + "wrong version": `{"policy_version": 2, "rules": [{"paths": ["x"], "min_tier": 1}]}`, + "no rules": `{"policy_version": 1, "rules": []}`, + "rule without path": `{"policy_version": 1, "rules": [{"paths": [], "min_tier": 1}]}`, + "tier out of range": `{"policy_version": 1, "rules": [{"paths": ["x"], "min_tier": 5}]}`, + "malformed mechanism": `{"policy_version": 1, "rules": [{"paths": ["x"], "min_tier": 1, "mechanism": "Not A Token!"}]}`, + "unknown scope": `{"policy_version": 1, "rules": [{"paths": ["x"], "min_tier": 1, "scope": "galaxy"}]}`, } for name, content := range bad { if _, err := Load(writePolicy(t, content)); err == nil { t.Errorf("%s: loaded without error — a broken floor must fail loudly", name) } } + + // The mechanism set is OPEN: a floor may require an external supplier's + // mechanism (declared in the invoker's intake config). A typo fails + // closed as an unsatisfiable floor, never as a load error. + external := `{"policy_version": 1, "rules": [{"paths": ["x"], "min_tier": 4, "mechanism": "dafny-proof"}]}` + if _, err := Load(writePolicy(t, external)); err != nil { + t.Errorf("external mechanism rejected at load: %v", err) + } } // TestPatternMatching: exact paths, "dir/..." subtrees, and path.Match diff --git a/internal/receipt/markdown.go b/internal/receipt/markdown.go index 4650959..6cfcbad 100644 --- a/internal/receipt/markdown.go +++ b/internal/receipt/markdown.go @@ -38,6 +38,13 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) { if p := r.Policy; p != nil { fmt.Fprintf(w, "policy: `%s` · %s · %d rule(s)%s\n", p.Path, short(p.Digest), p.Rules, exemptNote(p)) } + for _, rec := range r.Intake { + fmt.Fprintf(w, "intake: %s\n", mdCell(intakeLine(rec))) + for _, rej := range rec.Rejected { + fmt.Fprintf(w, "· rejected: %s (%s) — %s\n", + mdCell(rej.ClaimID+" "+rej.ProbeID), mdCell(rej.Outcome), mdCell(rej.Reason)) + } + } fmt.Fprintln(w) if p := r.Policy; p != nil && len(p.Misses) > 0 { @@ -58,7 +65,7 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) { fmt.Fprintln(w, "|---|---|") for _, res := range r.Results { if res.Status == schema.StatusRefuted { - fmt.Fprintf(w, "| `%s` | %s |\n", mdCell(res.Claim.ID), mdCell(detailOf(res))) + fmt.Fprintf(w, "| `%s` | %s |\n", mdCell(res.Claim.ID), mdCell(detailOf(res)+externalRefutationNote(res))) } } fmt.Fprintln(w) @@ -105,11 +112,7 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) { if cov.SuppressedMentions > 0 { fmt.Fprintf(w, "%s\n", mentionNote(cov.SuppressedMentions)) } - gate := "refuted claims block" - if r.Policy != nil { - gate = "refuted claims and policy misses block" - } - fmt.Fprintf(w, "\nschema %s%s · exit gate: %s; the remainder informs, never fails\n", r.SchemaVersion, toolNote(r), gate) + fmt.Fprintf(w, "\nschema %s%s · exit gate: %s; the remainder informs, never fails\n", r.SchemaVersion, toolNote(r), gateLegs(r)) } // mdCell makes text safe inside a markdown table cell. diff --git a/internal/receipt/receipt.go b/internal/receipt/receipt.go index 79dddb5..1d8f321 100644 --- a/internal/receipt/receipt.go +++ b/internal/receipt/receipt.go @@ -158,7 +158,7 @@ func anchoringSummary(claims []schema.Claim) *schema.AnchoringSummary { // least one probe and no annotated region was reached; no marker means no // coverage check applied. func bindingNote(res schema.ClaimResult) string { - nameOnly := false + nameOnly, external := false, "" for _, e := range res.Evidence { switch e.Binding { case schema.BindingCovered: @@ -167,14 +167,66 @@ func bindingNote(res schema.ClaimResult) string { return " [binding: file-coverage-proven]" case schema.BindingNameOnly: nameOnly = true + case schema.BindingSupplierAttested: + if e.CountsFor(res.Claim) { + external = e.Supplier + } } } - if nameOnly { + switch { + case external != "": + return " [external: " + external + " — supplier-attested]" + case nameOnly: return " [binding: name-only]" } return "" } +// externalRefutationNote marks a refuted row whose refuting evidence was +// SUPPLIED, not executed — a reader weighing a blocked merge must see that +// the counterexample is the supplier's word. +func externalRefutationNote(res schema.ClaimResult) string { + for _, e := range res.Evidence { + if e.Refuted() && e.Supplier != "" { + return " [external: " + e.Supplier + "]" + } + } + return "" +} + +// gateLegs names what blocks the gate on THIS receipt's configuration — +// shared by the renderers so the footer never under-states the gate. +func gateLegs(r schema.Receipt) string { + legs := []string{"refuted claims"} + if r.Policy != nil { + legs = append(legs, "policy misses") + } + for _, rec := range r.Intake { + if rec.Required { + legs = append(legs, "missing required intake") + break + } + } + return strings.Join(legs, " and ") + " block" +} + +// intakeLine renders one supplier's audit record for the receipt header. +func intakeLine(rec schema.IntakeRecord) string { + s := fmt.Sprintf("%s (%s ≤%s)", rec.Supplier, rec.Mechanism, rec.MaxTier) + if !rec.Admitted { + s += " — not admitted: " + rec.Reason + if rec.Required { + s += " — REQUIRED (the gate blocks here)" + } + return s + } + s += fmt.Sprintf(" — admitted %s, %d row(s) accepted", short(rec.DocDigest), rec.Accepted) + if n := len(rec.Rejected); n > 0 { + s += fmt.Sprintf(", %d rejected", n) + } + return s +} + // llmEdgeNote discloses why a model-proposed edge did not count: the probe // passed but the pass raised nothing, either because the coverage gate // refuted the edge (execution never reached the claim's file) or because no @@ -406,6 +458,12 @@ func WriteText(w io.Writer, r schema.Receipt) { if p := r.Policy; p != nil { fmt.Fprintf(w, "policy: %s · %s · %d rule(s)%s\n", p.Path, short(p.Digest), p.Rules, exemptNote(p)) } + for _, rec := range r.Intake { + fmt.Fprintf(w, "intake: %s\n", intakeLine(rec)) + for _, rej := range rec.Rejected { + fmt.Fprintf(w, " rejected: %s %s (%s) — %s\n", rej.ClaimID, rej.ProbeID, rej.Outcome, rej.Reason) + } + } fmt.Fprintln(w) fmt.Fprintf(w, "claims: %d verified: %d refuted: %d unverified: %d\n", @@ -444,7 +502,7 @@ func WriteText(w io.Writer, r schema.Receipt) { fmt.Fprintln(w, "REFUTED (a probe ran and the claim did not hold — the gate blocks here)") for _, res := range r.Results { if res.Status == schema.StatusRefuted { - fmt.Fprintf(w, " %s — %s\n", res.Claim.ID, detailOf(res)) + fmt.Fprintf(w, " %s — %s%s\n", res.Claim.ID, detailOf(res), externalRefutationNote(res)) } } fmt.Fprintln(w) @@ -462,6 +520,7 @@ func WriteText(w io.Writer, r schema.Receipt) { } writeCoverage(w, r.Coverage) + fmt.Fprintf(w, "\nexit gate: %s; the remainder informs, never fails\n", gateLegs(r)) } // writeCoverage renders the harvest's self-disclosure: the same honesty the diff --git a/internal/receipt/receipt_test.go b/internal/receipt/receipt_test.go index 7409a21..ee361e3 100644 --- a/internal/receipt/receipt_test.go +++ b/internal/receipt/receipt_test.go @@ -548,3 +548,66 @@ func TestPolicySectionRenders(t *testing.T) { t.Errorf("markdown exit-gate line does not name the policy leg") } } + +// TestIntakeRendersAndExternalMarks: supplied evidence is visible wherever +// it acts — the intake audit lines in the header, an [external] mark on the +// verified row AND on the refuted row, the rejected rows with reasons, and +// the exit-gate line naming the required-intake leg. GateBlocked blocks on +// a required profile with nothing admitted. +func TestIntakeRendersAndExternalMarks(t *testing.T) { + claim := schema.Claim{ID: "INV-009", Shape: schema.ShapeInvariant, Text: "the gate holds", + Source: schema.Source{File: "specs/gate.md", Line: 3}} + ext := schema.Evidence{ClaimID: "INV-009", ProbeID: "ext:dafny-worker/gate.dfy:GateSafe", + Tier: schema.T4Mechanical, Ran: true, Passed: true, Mechanism: "dafny-proof", + Supplier: "dafny-worker", Binding: schema.BindingSupplierAttested, Detail: "proof ok"} + + r := Assemble(gitdiff.Change{BaseRef: "main", HeadRef: "wip"}, + []schema.Claim{claim}, [][]schema.Evidence{{ext}}, schema.Coverage{}) + r.Intake = []schema.IntakeRecord{{ + Supplier: "dafny-worker", Mechanism: "dafny-proof", MaxTier: schema.T4Mechanical, + Required: true, Admitted: true, DocDigest: "abcdef9876543210", Accepted: 1, + Rejected: []schema.IntakeRejection{{ClaimID: "INV-999", ProbeID: "p1", + Outcome: "counterexample", Reason: "no such claim in this change"}}, + }} + + if r.Results[0].Status != schema.StatusVerified || r.Results[0].EffectiveTier != schema.T4Mechanical { + t.Fatalf("external verified pass mis-weighed: %+v", r.Results[0]) + } + var text, md strings.Builder + WriteText(&text, r) + WriteMarkdown(&md, r) + for name, out := range map[string]string{"text": text.String(), "markdown": md.String()} { + for _, want := range []string{"dafny-worker (dafny-proof ≤T4-mechanical)", "admitted abcdef987654", + "1 row(s) accepted", "1 rejected", "INV-999", "no such claim in this change", + "[external: dafny-worker — supplier-attested]", + "missing required intake"} { + if !strings.Contains(out, want) { + t.Errorf("%s receipt lacks %q:\n%s", name, want, out) + } + } + } + + // An external counterexample refutes and the refuted row is marked. + cx := ext + cx.Passed = false + cx.Detail = "counterexample found" + r2 := Assemble(gitdiff.Change{BaseRef: "main", HeadRef: "wip"}, + []schema.Claim{claim}, [][]schema.Evidence{{cx}}, schema.Coverage{}) + if r2.Results[0].Status != schema.StatusRefuted { + t.Fatalf("external counterexample did not refute: %+v", r2.Results[0]) + } + var text2 strings.Builder + WriteText(&text2, r2) + if !strings.Contains(text2.String(), "counterexample found [external: dafny-worker]") { + t.Errorf("refuted row lost its external mark:\n%s", text2.String()) + } + + // A required profile with nothing admitted blocks. + r3 := schema.Receipt{Intake: []schema.IntakeRecord{{Supplier: "s", Required: true}}} + if !r3.GateBlocked() { + t.Error("required-not-admitted did not block the gate") + } + if (schema.Receipt{Intake: []schema.IntakeRecord{{Supplier: "s"}}}).GateBlocked() { + t.Error("optional-not-admitted blocked the gate") + } +} diff --git a/schema/schema.go b/schema/schema.go index 9bd1fca..d51f2a5 100644 --- a/schema/schema.go +++ b/schema/schema.go @@ -198,6 +198,10 @@ type Evidence struct { // Environment records the toolchain the probe ran under, when the runner // measures it (e.g. "go1.24.5 linux/amd64"). Empty means unmeasured. Environment string `json:"environment,omitempty"` + // Supplier names the external tool that supplied this evidence through + // the intake contract — empty for evidence correctful executed itself. + // Supplied evidence always carries Binding "supplier-attested". + Supplier string `json:"supplier,omitempty"` } // Mechanism values — one per runner kind. @@ -234,6 +238,12 @@ const ( // never reached the claim's file — the proposed edge is refuted as an // edge (which says nothing about the claim itself). BindingFileNotReached = "file-not-reached" + // BindingSupplierAttested: the evidence was SUPPLIED by an external + // tool through the intake contract — correctful admitted it against an + // invoker-owned profile and a subject match, but did not execute the + // probe and cannot check the tie beyond the claim id. The residual + // trust is the supplier's word, and the receipt says so. + BindingSupplierAttested = "supplier-attested" ) // Verified reports whether this evidence raises its claim: the probe ran, @@ -402,6 +412,9 @@ type Receipt struct { // when the repo declares a policy file. Nil means no policy: nothing was // required, so nothing was missed. Policy *PolicyResult `json:"policy,omitempty"` + // Intake is the external-evidence audit trail, one record per supplier + // profile — present only when the invoker configured intake. + Intake []IntakeRecord `json:"intake,omitempty"` // Remainder is the subset of Results with Status == StatusUnverified, // surfaced explicitly so a reader never has to derive it. This is the // feature no other tool in the field ships. @@ -410,6 +423,26 @@ type Receipt struct { Summary Summary `json:"summary"` } +// GateBlocked reports whether the merge gate blocks on this receipt: a +// refuted claim, a policy miss, or a required supplier with no admitted +// document. The remainder never blocks — it informs. This is THE gate +// definition; main and any CI wrapper must consult it rather than +// re-deriving the legs. +func (r Receipt) GateBlocked() bool { + if r.Summary.Refuted > 0 { + return true + } + if r.Policy != nil && len(r.Policy.Misses) > 0 { + return true + } + for _, rec := range r.Intake { + if rec.Required && !rec.Admitted { + return true + } + } + return false +} + // PolicyResult records how the repository's declared evidence floors held // against this change. The digest is a chain field: a receipt is comparable // to its predecessors only when the policy that judged it is identified — @@ -440,5 +473,43 @@ type PolicyMiss struct { Detail string `json:"detail"` } +// IntakeRecord is the audit trail for ONE external supplier's intake: what +// was admitted, what was rejected, and why. One record per profile in the +// intake config, present even when the supplier delivered nothing — a +// required supplier with no admitted document is a gate miss, and silence +// about it would be exactly the omission the receipt exists to prevent. +type IntakeRecord struct { + // Supplier is the profile's name (invoker-owned, never row-claimed). + Supplier string `json:"supplier"` + // Mechanism and MaxTier echo the profile: the authority the invoker + // granted, which every admitted row is clamped to. + Mechanism string `json:"mechanism"` + MaxTier Tier `json:"max_tier"` + // Required means the gate blocks when no document was admitted. + Required bool `json:"required,omitempty"` + // Admitted reports whether a document passed admission (subject match). + Admitted bool `json:"admitted"` + // Reason states why nothing was admitted (missing file, subject + // mismatch, …). Empty when admitted. + Reason string `json:"reason,omitempty"` + // DocDigest is the SHA-256 (hex) over the admitted document's exact + // bytes — the audit pin for what was accepted. + DocDigest string `json:"doc_digest,omitempty"` + // Accepted counts the rows that became evidence. + Accepted int `json:"accepted"` + // Rejected lists per-row rejections with reasons — never reduced to a + // bare count: a rejected counterexample naming an unknown claim can + // expose claim drift, and a reader must be able to see it. + Rejected []IntakeRejection `json:"rejected,omitempty"` +} + +// IntakeRejection is one intake row that did not become evidence. +type IntakeRejection struct { + ClaimID string `json:"claim_id"` + ProbeID string `json:"probe_id"` + Outcome string `json:"outcome"` + Reason string `json:"reason"` +} + // SchemaVersion is the current version of the receipt schema (the payload). -const SchemaVersion = "0.0.11" +const SchemaVersion = "0.0.12"