diff --git a/DESIGN.md b/DESIGN.md index 6780bb7..5281199 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -400,6 +400,53 @@ draft of this section: tier ladder preserves this difference and the receipt never states more than the probe demonstrated. +## The policy layer (schema 0.0.11): evidence floors per path + +The end state's second commitment, delivered: `correctful.json` at the repo +root declares rules — paths plus a floor (`min_tier`, optionally a required +`mechanism` and a required `scope`). Evaluation is per changed file, and +the tie between a file and its evidence is STRUCTURAL, never assumed: a +verified claim speaks for a file only when the claim was sourced from it +(LLM claims with confirmed edges, spec-ids in code) or a reference site in +shipped code names it. A matched file nothing demonstrably ties evidence +to is a miss stated exactly that way — which makes floors honest and also +scopes where they are USEFUL: repos that annotate code with claim ids, or +run the LLM extractor. A floor on unannotated code fails, and should. + +Design decisions worth recording: + +- **Misses block the gate**, same as refutations — a floor that only + informs is not a floor. The exit-gate line in the receipt says which legs + block. +- **Test files are exempt and the exemption is counted** — a `_test.go` is + evidence, not an evidence subject. Silent exemption would be a coverage + lie; the receipt shows the count. +- **The policy digest is the second chain field** (after the tool + version): SHA-256 over the policy file's exact bytes, rendered short + beside the change. A policy change — the trust base changing — is + visible in the receipt chain, which is the review trigger the end + state's first commitment asks for. +- **A malformed policy fails loudly before any probe runs.** A broken + floor must never fail open; a missing file simply means no policy. +- **The LLM edge gate applies identically here** — `Evidence.CountsFor` + moved to the schema so weighing and policy evaluation share one + definition and can never disagree. A pass on an unconfirmed + model-proposed edge satisfies no floor. +- **Each rule stands alone**: a file matched by two rules must satisfy + both floors; the miss row names the violated rule and the best tied + evidence, so the reader sees the gap, not just the verdict. + +Measured (first live run, 2026-08, on a real annotated repo's feature +branch): a T1 floor over the changed command directory matched 26 files — +8 exempt as test files (disclosed), 18 evaluated, ALL 18 missed with "no +verified claim ties to this file", and the gate blocked. Correctly: the +branch's 153 verified claims are all test-name-sourced, and none of the +changed code files carries a reconciled claim id, so no verified evidence +structurally speaks for them. The strictness is the finding — a floor +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. + ## 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 8865481..423f7a6 100644 --- a/README.md +++ b/README.md @@ -99,10 +99,46 @@ shows the reference configuration: - The workflow writes the receipt as a comment on the pull request. The marker `` identifies the comment. The workflow updates the same comment after each push. -- The gate fails only when a probe refuted a claim. +- The gate fails when a probe refuted a claim, or when the change missed a + declared policy floor. This repository uses this gate for each of its own pull requests. +## Policy floors (optional) + +You can declare evidence floors for the paths that matter most. Write a +`correctful.json` file in the repository root: + +```json +{ + "policy_version": 1, + "rules": [ + { + "name": "auth-floor", + "paths": ["internal/auth/..."], + "min_tier": 2, + "mechanism": "go-test-pair" + } + ] +} +``` + +The rule reads: each changed file under `internal/auth/` must have one +verified claim that connects to that file, at tier T2 or higher, from an +accept/reject test pair. A rule can also demand a measured execution scope +(`"scope": "cross-package"`). + +- A connection is structural. The claim's source file, or a reference site + in the code, must name the changed file. The tool does not guess. +- Test files are exempt. They supply evidence; they do not need evidence. + The receipt shows the count of exempt files. +- A missed floor blocks the gate, in the same way as a refuted claim. The + receipt shows each miss with the best found evidence and the floor. +- The receipt shows the SHA-256 digest of the policy file. A policy change + is visible in the receipt chain. +- No policy file means no policy. A malformed policy file stops the run + with an error. It never fails open. + ## What correctful examines | You write | correctful harvests | The probe | Tier | diff --git a/cmd/correctful/main.go b/cmd/correctful/main.go index 9182c40..e3508d4 100644 --- a/cmd/correctful/main.go +++ b/cmd/correctful/main.go @@ -17,9 +17,9 @@ // -concurrency max probes to run at once. Default: 4. // -timeout overall probe budget. Default: 5m. // -// Exit status: 0 when no claim was refuted; 1 when a probe ran and a claim did -// not hold (merge-gate semantics). The remainder never fails the run — it is an -// honest report, not a defect. +// 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. package main import ( @@ -32,6 +32,7 @@ import ( "github.com/joshft/correctful/internal/gitdiff" "github.com/joshft/correctful/internal/harvest" "github.com/joshft/correctful/internal/llmextract" + "github.com/joshft/correctful/internal/policy" "github.com/joshft/correctful/internal/probe" "github.com/joshft/correctful/internal/receipt" ) @@ -94,6 +95,14 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL // a mid-branch receipt harvests the working tree. change.InputDigest = gitdiff.InputDigest(root, change.Files) + // Load the policy BEFORE any probe runs: a malformed policy fails loudly + // here (a broken floor must never fail open), and a missing file simply + // means no policy. + pol, err := policy.Load(root) + if err != nil { + return err + } + // Harvest claims, then dispatch probes against them. harvesters := harvest.Default() if useLLM { @@ -130,6 +139,9 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL Dispatch(ctx, root, claims) r := receipt.Assemble(change, claims, evidence, coverage) + if pol != nil { + r.Policy = policy.Evaluate(pol, r) + } switch format { case "json": @@ -142,7 +154,7 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL receipt.WriteText(os.Stdout, r) } - if r.Summary.Refuted > 0 { + if r.Summary.Refuted > 0 || (r.Policy != nil && len(r.Policy.Misses) > 0) { os.Exit(1) } return nil diff --git a/internal/policy/policy.go b/internal/policy/policy.go new file mode 100644 index 0000000..14aa000 --- /dev/null +++ b/internal/policy/policy.go @@ -0,0 +1,247 @@ +// Package policy evaluates a repository's declared evidence floors against +// an assembled receipt — the "repository policy evaluates the receipt" leg +// of the end state. +// +// A policy is opt-in per path: a rule names the paths it governs and the +// floor their evidence must meet (a minimum tier, optionally a required +// mechanism and a required execution scope). Evaluation is per changed +// file: every matched non-test file must have at least one verified claim +// that TIES to it and whose evidence meets the floor. A tie is structural, +// never assumed — the claim's own source file, or a reference site in +// shipped code. A file nothing demonstrably ties evidence to is a miss +// stated exactly that way; policy floors are therefore only useful where +// claims tie to code (spec-id annotations, or LLM claims with +// coverage-confirmed edges), which is honest: an untied floor SHOULD fail. +// +// A missing policy file means no policy — nothing required, nothing missed. +// A malformed policy file is a loud error, never a silent allow: a broken +// floor must not fail open. +package policy + +import ( + "crypto/sha256" + "encoding/json" + "fmt" + "os" + "path" + "path/filepath" + "strings" + + "github.com/joshft/correctful/schema" +) + +// File is the policy's well-known repo-relative location. Deliberately NOT +// under a hidden directory: the policy is part of the repository's trust +// base and deserves the same visibility as the code it governs. +const File = "correctful.json" + +// Rule is one evidence floor over a set of paths. +type Rule struct { + // Name labels the rule in misses; when empty, the paths label it. + Name string `json:"name,omitempty"` + // Paths the rule governs: an exact repo-relative path, a "dir/..." + // subtree, or a path.Match glob (whose * does not cross a slash). + Paths []string `json:"paths"` + // MinTier is the floor: the tier the tied evidence must reach (1–4). + MinTier int `json:"min_tier"` + // Mechanism, when set, requires the tied evidence's probe kind + // (e.g. "go-test-pair" for an adversarial floor). + Mechanism string `json:"mechanism,omitempty"` + // Scope, when set, requires the tied evidence's measured execution + // footprint (e.g. "cross-package" for an integration floor). Only + // instrumented runs carry a scope, so a scope floor demands one. + Scope string `json:"scope,omitempty"` +} + +// Policy is a parsed, validated policy file. +type Policy struct { + PolicyVersion int `json:"policy_version"` + Rules []Rule `json:"rules"` + + digest string +} + +var knownMechanisms = map[string]bool{ + schema.MechanismGoTest: true, schema.MechanismGoTestPair: true, + schema.MechanismDotnetTest: true, schema.MechanismAlloyCheck: true, +} + +var knownScopes = map[string]bool{ + schema.ScopeSinglePackage: true, schema.ScopeCrossPackage: true, +} + +// Load reads and validates the repo's policy file. A missing file is +// (nil, nil) — no policy. Any other failure is an error: unreadable, +// unparseable, or invalid policies fail loudly before a single probe runs. +func Load(root string) (*Policy, error) { + data, err := os.ReadFile(filepath.Join(root, File)) + if os.IsNotExist(err) { + return nil, nil + } + if err != nil { + return nil, fmt.Errorf("reading %s: %w", File, err) + } + var p Policy + if err := json.Unmarshal(data, &p); err != nil { + return nil, fmt.Errorf("%s is not valid JSON: %v", File, err) + } + if p.PolicyVersion != 1 { + return nil, fmt.Errorf("%s: policy_version %d is not supported (want 1)", File, p.PolicyVersion) + } + if len(p.Rules) == 0 { + return nil, fmt.Errorf("%s: no rules — delete the file to declare no policy", File) + } + for i, r := range p.Rules { + if len(r.Paths) == 0 { + return nil, fmt.Errorf("%s: rule %d has no paths", File, i) + } + 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.Scope != "" && !knownScopes[r.Scope] { + return nil, fmt.Errorf("%s: rule %d names unknown scope %q", File, i, r.Scope) + } + } + p.digest = fmt.Sprintf("%x", sha256.Sum256(data)) + return &p, nil +} + +// Evaluate checks every changed file against every rule and returns the +// receipt's policy section. Each rule stands alone: a file matched by two +// rules must satisfy both floors. +func Evaluate(p *Policy, r schema.Receipt) *schema.PolicyResult { + res := &schema.PolicyResult{Path: File, Digest: p.digest, Rules: len(p.Rules)} + for _, rule := range p.Rules { + for _, f := range r.Change.Files { + if !matchesAny(rule.Paths, f) { + continue + } + if isTestFile(f) { + res.ExemptTestFiles++ + continue + } + if detail := floorMiss(rule, f, r.Results); detail != "" { + res.Misses = append(res.Misses, schema.PolicyMiss{ + File: f, Rule: ruleLabel(rule), Detail: detail, + }) + } + } + } + return res +} + +// floorMiss reports why file f fails rule's floor, or "" when satisfied: +// some verified claim must tie to f with evidence meeting the floor. The +// miss detail names the best tied evidence so the reader sees the gap, not +// just the verdict. +func floorMiss(rule Rule, f string, results []schema.ClaimResult) string { + var best *schema.Evidence + for i := range results { + res := &results[i] + if res.Status != schema.StatusVerified || !tiesTo(res.Claim, f) { + continue + } + for j := range res.Evidence { + e := &res.Evidence[j] + if !e.CountsFor(res.Claim) { + continue + } + if meetsFloor(rule, e) { + return "" + } + if best == nil || e.Tier > best.Tier { + best = e + } + } + } + floor := floorLabel(rule) + if best == nil { + return "no verified claim ties to this file; floor is " + floor + } + got := best.Tier.String() + " " + best.Mechanism + if best.Scope != "" { + got += " " + best.Scope + } + return "best tied evidence is " + got + "; floor is " + floor +} + +// tiesTo reports whether a claim's evidence can speak for file f: the claim +// was sourced from f (LLM claims, spec-ids in code), or shipped code in f +// names the claim's id (a reference site). +func tiesTo(c schema.Claim, f string) bool { + if c.Source.File == f { + return true + } + for _, s := range c.RefSites { + if s.File == f { + return true + } + } + return false +} + +// meetsFloor checks one evidence row against a rule's requirements. +func meetsFloor(rule Rule, e *schema.Evidence) bool { + if e.Tier < schema.Tier(rule.MinTier) { + return false + } + if rule.Mechanism != "" && e.Mechanism != rule.Mechanism { + return false + } + if rule.Scope != "" && e.Scope != rule.Scope { + return false + } + return true +} + +// isTestFile exempts files that are themselves probe sources — evidence, +// not evidence subjects. The exemption is counted and disclosed. +func isTestFile(f string) bool { + return strings.HasSuffix(f, "_test.go") +} + +// matchesAny reports whether f matches any of the rule's path patterns. +func matchesAny(patterns []string, f string) bool { + for _, pat := range patterns { + if matchesPattern(pat, f) { + return true + } + } + return false +} + +// matchesPattern matches one pattern: exact path, "dir/..." subtree, or a +// path.Match glob (single-segment wildcards; * never crosses a slash). +func matchesPattern(pattern, f string) bool { + if strings.HasSuffix(pattern, "/...") { + return strings.HasPrefix(f, strings.TrimSuffix(pattern, "...")) + } + if pattern == f { + return true + } + ok, err := path.Match(pattern, f) + return err == nil && ok +} + +// ruleLabel names a rule for a miss row. +func ruleLabel(r Rule) string { + if r.Name != "" { + return r.Name + } + return strings.Join(r.Paths, " ") +} + +// floorLabel renders a rule's requirements the way a reader compares them. +func floorLabel(r Rule) string { + s := "≥" + schema.Tier(r.MinTier).String() + if r.Mechanism != "" { + s += " " + r.Mechanism + } + if r.Scope != "" { + s += " " + r.Scope + } + return s +} diff --git a/internal/policy/policy_test.go b/internal/policy/policy_test.go new file mode 100644 index 0000000..c1ddf13 --- /dev/null +++ b/internal/policy/policy_test.go @@ -0,0 +1,195 @@ +package policy + +import ( + "crypto/sha256" + "fmt" + "os" + "path/filepath" + "strings" + "testing" + + "github.com/joshft/correctful/schema" +) + +// validPolicy is a real-shaped policy file: one named adversarial floor over +// a subtree, one plain T1 floor over a glob. +const validPolicy = `{ + "policy_version": 1, + "rules": [ + {"name": "auth-floor", "paths": ["internal/auth/..."], "min_tier": 2, "mechanism": "go-test-pair"}, + {"paths": ["pkg/*.go"], "min_tier": 1} + ] +}` + +func writePolicy(t *testing.T, content string) string { + t.Helper() + dir := t.TempDir() + if err := os.WriteFile(filepath.Join(dir, File), []byte(content), 0o644); err != nil { + t.Fatal(err) + } + return dir +} + +// TestLoadValidatesAndDigests: a missing file is no policy; a valid file +// parses with a digest over its exact bytes; every malformed shape fails +// LOUDLY — a broken floor must never fail open. +func TestLoadValidatesAndDigests(t *testing.T) { + if p, err := Load(t.TempDir()); p != nil || err != nil { + t.Fatalf("missing file: %v, %v — want no policy, no error", p, err) + } + + p, err := Load(writePolicy(t, validPolicy)) + if err != nil { + t.Fatal(err) + } + if len(p.Rules) != 2 || p.Rules[0].Name != "auth-floor" { + t.Fatalf("parsed rules = %+v", p.Rules) + } + if want := fmt.Sprintf("%x", sha256.Sum256([]byte(validPolicy))); p.digest != want { + t.Errorf("digest = %s, want sha256 of the exact bytes", p.digest) + } + + 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"}]}`, + } + 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) + } + } +} + +// TestPatternMatching: exact paths, "dir/..." subtrees, and path.Match +// globs whose * never crosses a slash. +func TestPatternMatching(t *testing.T) { + cases := []struct { + pattern, file string + want bool + }{ + {"internal/auth/gate.go", "internal/auth/gate.go", true}, + {"internal/auth/...", "internal/auth/gate.go", true}, + {"internal/auth/...", "internal/auth/deep/nested.go", true}, + {"internal/auth/...", "internal/authz/other.go", false}, + {"pkg/*.go", "pkg/gate.go", true}, + {"pkg/*.go", "pkg/sub/gate.go", false}, + {"*.md", "README.md", true}, + {"*.md", "docs/notes.md", false}, + } + for _, tc := range cases { + if got := matchesPattern(tc.pattern, tc.file); got != tc.want { + t.Errorf("matchesPattern(%q, %q) = %v, want %v", tc.pattern, tc.file, got, tc.want) + } + } +} + +// receiptWith builds a minimal assembled receipt for evaluation tests. +func receiptWith(files []string, results []schema.ClaimResult) schema.Receipt { + return schema.Receipt{Change: schema.ChangeRef{Files: files}, Results: results} +} + +func verifiedResult(claim schema.Claim, ev schema.Evidence) schema.ClaimResult { + return schema.ClaimResult{Claim: claim, Status: schema.StatusVerified, + EffectiveTier: ev.Tier, Evidence: []schema.Evidence{ev}} +} + +// TestEvaluateFloors: the per-file semantics. A matched file needs one +// verified claim that TIES to it (source file or reference site) with +// evidence meeting the floor; test files are exempt and counted; untied +// files miss with the exact reason; under-floor evidence misses naming the +// best tied evidence. +func TestEvaluateFloors(t *testing.T) { + p := &Policy{PolicyVersion: 1, digest: "d", Rules: []Rule{ + {Name: "auth-floor", Paths: []string{"internal/auth/..."}, MinTier: 2, Mechanism: schema.MechanismGoTestPair}, + }} + + pairEv := schema.Evidence{Tier: schema.T2Adversarial, Ran: true, Passed: true, + Mechanism: schema.MechanismGoTestPair} + t1Ev := schema.Evidence{Tier: schema.T1Assertion, Ran: true, Passed: true, + Mechanism: schema.MechanismGoTest} + + refClaim := schema.Claim{ID: "INV-001", Source: schema.Source{Kind: schema.SourceGoTest, File: "internal/auth/gate_test.go"}, + RefSites: []schema.Source{{File: "internal/auth/gate.go", Line: 3}}} + + // Satisfied via a reference-site tie with pair evidence. + res := Evaluate(p, receiptWith( + []string{"internal/auth/gate.go", "internal/auth/gate_test.go"}, + []schema.ClaimResult{verifiedResult(refClaim, pairEv)})) + if len(res.Misses) != 0 { + t.Errorf("satisfied floor produced misses: %+v", res.Misses) + } + if res.ExemptTestFiles != 1 { + t.Errorf("exempt test files = %d, want 1", res.ExemptTestFiles) + } + if res.Digest != "d" || res.Rules != 1 { + t.Errorf("result header = %+v", res) + } + + // Under-floor: tied evidence exists but is T1 single-test. + res = Evaluate(p, receiptWith( + []string{"internal/auth/gate.go"}, + []schema.ClaimResult{verifiedResult(refClaim, t1Ev)})) + if len(res.Misses) != 1 || !strings.Contains(res.Misses[0].Detail, "best tied evidence is T1-assertion go-test") || + !strings.Contains(res.Misses[0].Detail, "≥T2-adversarial go-test-pair") { + t.Errorf("under-floor miss = %+v", res.Misses) + } + if res.Misses[0].Rule != "auth-floor" { + t.Errorf("rule label = %q", res.Misses[0].Rule) + } + + // No tie at all: verified claims elsewhere do not speak for this file. + elsewhere := schema.Claim{ID: "X", Source: schema.Source{File: "other/thing_test.go"}} + res = Evaluate(p, receiptWith( + []string{"internal/auth/gate.go"}, + []schema.ClaimResult{verifiedResult(elsewhere, pairEv)})) + if len(res.Misses) != 1 || !strings.Contains(res.Misses[0].Detail, "no verified claim ties to this file") { + t.Errorf("untied miss = %+v", res.Misses) + } + + // Unmatched files are not policed. + res = Evaluate(p, receiptWith([]string{"README.md"}, nil)) + if len(res.Misses) != 0 { + t.Errorf("unmatched file policed: %+v", res.Misses) + } +} + +// TestEvaluateScopeFloorAndLLMGate: a scope floor demands measured +// cross-package evidence, and the LLM edge gate applies IDENTICALLY here as +// in weighing (Evidence.CountsFor): a pass on an unconfirmed model-proposed +// edge satisfies no floor. +func TestEvaluateScopeFloorAndLLMGate(t *testing.T) { + p := &Policy{PolicyVersion: 1, digest: "d", Rules: []Rule{ + {Paths: []string{"svc/..."}, MinTier: 1, Scope: schema.ScopeCrossPackage}, + }} + + llmClaim := schema.Claim{ID: "LLM:svc/api.go:1", Source: schema.Source{Kind: schema.SourceLLM, File: "svc/api.go"}} + confirmedCross := schema.Evidence{Tier: schema.T1Assertion, Ran: true, Passed: true, + Mechanism: schema.MechanismGoTest, Scope: schema.ScopeCrossPackage, Binding: schema.BindingFileCovered} + unconfirmedCross := confirmedCross + unconfirmedCross.Binding = "" + confirmedSingle := confirmedCross + confirmedSingle.Scope = schema.ScopeSinglePackage + + res := Evaluate(p, receiptWith([]string{"svc/api.go"}, + []schema.ClaimResult{verifiedResult(llmClaim, confirmedCross)})) + if len(res.Misses) != 0 { + t.Errorf("confirmed cross-package edge missed the floor: %+v", res.Misses) + } + + res = Evaluate(p, receiptWith([]string{"svc/api.go"}, + []schema.ClaimResult{verifiedResult(llmClaim, unconfirmedCross)})) + if len(res.Misses) != 1 { + t.Errorf("unconfirmed llm edge satisfied a floor: %+v", res.Misses) + } + + res = Evaluate(p, receiptWith([]string{"svc/api.go"}, + []schema.ClaimResult{verifiedResult(llmClaim, confirmedSingle)})) + if len(res.Misses) != 1 || !strings.Contains(res.Misses[0].Detail, "single-package") { + t.Errorf("single-package vs cross floor = %+v", res.Misses) + } +} diff --git a/internal/receipt/markdown.go b/internal/receipt/markdown.go index 81884bb..4650959 100644 --- a/internal/receipt/markdown.go +++ b/internal/receipt/markdown.go @@ -35,8 +35,22 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) { if note := exclusionNote(r.Change.Excluded); note != "" { fmt.Fprintf(w, "%s\n", note) } + 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)) + } fmt.Fprintln(w) + if p := r.Policy; p != nil && len(p.Misses) > 0 { + fmt.Fprintln(w, "### 🚫 Policy misses — evidence floors not met") + fmt.Fprintln(w) + fmt.Fprintln(w, "| File | What is missing | Rule |") + fmt.Fprintln(w, "|---|---|---|") + for _, m := range p.Misses { + fmt.Fprintf(w, "| `%s` | %s | %s |\n", mdCell(m.File), mdCell(m.Detail), mdCell(m.Rule)) + } + fmt.Fprintln(w) + } + if s.Refuted > 0 { fmt.Fprintln(w, "### ❌ Refuted — a probe ran and the claim did not hold") fmt.Fprintln(w) @@ -91,7 +105,11 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) { if cov.SuppressedMentions > 0 { fmt.Fprintf(w, "%s\n", mentionNote(cov.SuppressedMentions)) } - fmt.Fprintf(w, "\nschema %s%s · exit gate: refuted claims block; the remainder informs, never fails\n", r.SchemaVersion, toolNote(r)) + 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) } // mdCell makes text safe inside a markdown table cell. diff --git a/internal/receipt/receipt.go b/internal/receipt/receipt.go index 4bb83f8..79dddb5 100644 --- a/internal/receipt/receipt.go +++ b/internal/receipt/receipt.go @@ -228,13 +228,15 @@ func anchorNote(c schema.Claim) string { // shaNote renders the immutable pins beside the symbolic refs, abbreviated: // the commit SHAs, and the input digest that identifies the harvested content // when the tree carries work no commit SHA covers. -func shaNote(c schema.ChangeRef) string { - short := func(s string) string { - if len(s) > 12 { - return s[:12] - } - return s +// short abbreviates a hex pin for display; the full value stays in the JSON. +func short(s string) string { + if len(s) > 12 { + return s[:12] } + return s +} + +func shaNote(c schema.ChangeRef) string { var parts []string switch { case c.BaseSHA != "" && c.HeadSHA != "": @@ -350,18 +352,18 @@ func scrubHost(s, host string) string { // - unverified: nothing ran that could raise the claim. Remainder. // // For an LLM-PROPOSED claim, a pass additionally requires a coverage-confirmed -// edge (Binding "file-covered"): the probe→claim tie is the model's word, so -// the pass counts only when the probe's own execution demonstrably reached the -// claim's file. Fail-closed — a pass with no profile, or one whose execution -// never touched the file, raises nothing and the claim stays in the remainder -// (llmEdgeNote discloses which). Refutation stays UNCONDITIONAL: a failing -// probe in the change blocks the gate no matter whose edge bound it. +// edge (Evidence.CountsFor — the gate lives in schema so policy evaluation +// applies the identical rule). Fail-closed — a pass with no profile, or one +// whose execution never touched the file, raises nothing and the claim stays +// in the remainder (llmEdgeNote discloses which). Refutation stays +// UNCONDITIONAL: a failing probe in the change blocks the gate no matter +// whose edge bound it. func weigh(c schema.Claim, evs []schema.Evidence) (schema.Status, schema.Tier) { best := schema.T0Unverified anyVerified, anyRefuted := false, false for _, e := range evs { switch { - case e.Verified() && (c.Source.Kind != schema.SourceLLM || e.Binding == schema.BindingFileCovered): + case e.CountsFor(c): anyVerified = true if e.Tier > best { best = e.Tier @@ -401,6 +403,9 @@ func WriteText(w io.Writer, r schema.Receipt) { if note := exclusionNote(r.Change.Excluded); note != "" { fmt.Fprintf(w, " %s\n", note) } + 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)) + } fmt.Fprintln(w) fmt.Fprintf(w, "claims: %d verified: %d refuted: %d unverified: %d\n", @@ -428,6 +433,13 @@ func WriteText(w io.Writer, r schema.Receipt) { } fmt.Fprintln(w) } + if p := r.Policy; p != nil && len(p.Misses) > 0 { + fmt.Fprintln(w, "POLICY MISSES (evidence floors not met — the gate blocks here)") + for _, m := range p.Misses { + fmt.Fprintf(w, " %s — %s [rule: %s]\n", m.File, m.Detail, m.Rule) + } + fmt.Fprintln(w) + } if s.Refuted > 0 { fmt.Fprintln(w, "REFUTED (a probe ran and the claim did not hold — the gate blocks here)") for _, res := range r.Results { @@ -489,6 +501,15 @@ func toolNote(r schema.Receipt) string { return " · correctful " + r.ToolVersion } +// exemptNote renders the policy's test-file exemption count when present — +// the exemption is disclosed, never silent. +func exemptNote(p *schema.PolicyResult) string { + if p.ExemptTestFiles == 0 { + return "" + } + return fmt.Sprintf(" · %d test file(s) exempt (evidence sources)", p.ExemptTestFiles) +} + // detailOf picks the evidence detail a reader needs: for a refuted claim, the // FAILING probe's detail — a claim with five probes where the fourth failed // must not display the first probe's "ok". diff --git a/internal/receipt/receipt_test.go b/internal/receipt/receipt_test.go index 1eef2f8..7409a21 100644 --- a/internal/receipt/receipt_test.go +++ b/internal/receipt/receipt_test.go @@ -513,3 +513,38 @@ func TestReceiptCarriesToolVersion(t *testing.T) { t.Errorf("markdown receipt lacks %q", want) } } + +// TestPolicySectionRenders: a receipt carrying a policy shows the digest +// beside the change, the misses in a gate-blocking section in BOTH +// renderers, and the exit-gate line names the policy leg. A receipt with no +// policy renders none of it — repos without a policy file are unchanged. +func TestPolicySectionRenders(t *testing.T) { + claims, evidence := sampleClaims() + r := Assemble(gitdiff.Change{BaseRef: "main", HeadRef: "wip"}, claims, evidence, schema.Coverage{}) + + var noPolicy strings.Builder + WriteText(&noPolicy, r) + if strings.Contains(noPolicy.String(), "policy") { + t.Errorf("policy rendered without a policy file:\n%s", noPolicy.String()) + } + + r.Policy = &schema.PolicyResult{ + Path: "correctful.json", Digest: "abcdef0123456789", Rules: 2, ExemptTestFiles: 1, + Misses: []schema.PolicyMiss{{File: "internal/auth/gate.go", + Rule: "auth-floor", Detail: "no verified claim ties to this file; floor is ≥T2-adversarial go-test-pair"}}, + } + 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{"abcdef012345", "2 rule(s)", "1 test file(s) exempt", + "internal/auth/gate.go", "no verified claim ties to this file", "auth-floor"} { + if !strings.Contains(out, want) { + t.Errorf("%s receipt lacks %q:\n%s", name, want, out) + } + } + } + if !strings.Contains(md.String(), "refuted claims and policy misses block") { + t.Errorf("markdown exit-gate line does not name the policy leg") + } +} diff --git a/schema/schema.go b/schema/schema.go index 4df49a8..9bd1fca 100644 --- a/schema/schema.go +++ b/schema/schema.go @@ -244,6 +244,19 @@ const ( // says nothing. func (e Evidence) Verified() bool { return e.Ran && e.Passed && e.Tier > T0Unverified } +// CountsFor reports whether this evidence RAISES the given claim — the one +// place the model-proposed-edge gate lives, shared by receipt weighing and +// policy evaluation so the two can never disagree. For an LLM-proposed claim +// a pass counts only with a coverage-confirmed edge (BindingFileCovered): +// the probe→claim tie is the model's word, so the pass counts only when the +// probe's own execution demonstrably reached the claim's file. +func (e Evidence) CountsFor(c Claim) bool { + if !e.Verified() { + return false + } + return c.Source.Kind != SourceLLM || e.Binding == BindingFileCovered +} + // Refuted reports whether this evidence refutes its claim: the probe ran and // the claim did not hold. func (e Evidence) Refuted() bool { return e.Ran && !e.Passed } @@ -385,6 +398,10 @@ type Receipt struct { ToolVersion string `json:"tool_version,omitempty"` Change ChangeRef `json:"change"` Results []ClaimResult `json:"results"` + // Policy is the repository's evidence-floor evaluation — present only + // when the repo declares a policy file. Nil means no policy: nothing was + // required, so nothing was missed. + Policy *PolicyResult `json:"policy,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. @@ -393,5 +410,35 @@ type Receipt struct { Summary Summary `json:"summary"` } +// 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 — +// and a policy CHANGE is itself the kind of change the trust base must +// surface for human review. +type PolicyResult struct { + // Path is the repo-relative policy file location. + Path string `json:"path"` + // Digest is the SHA-256 (hex) over the policy file's exact bytes. + Digest string `json:"digest"` + // Rules is the number of declared rules. + Rules int `json:"rules"` + // ExemptTestFiles counts matched files exempted as test files — probe + // sources, not evidence subjects. Disclosed so the exemption is visible. + ExemptTestFiles int `json:"exempt_test_files,omitempty"` + // Misses are the floor violations. The gate blocks on any. + Misses []PolicyMiss `json:"misses,omitempty"` +} + +// PolicyMiss is one changed file that a rule matched and whose evidence did +// not meet the rule's floor. +type PolicyMiss struct { + File string `json:"file"` + // Rule names the violated rule (its declared name, or its paths). + Rule string `json:"rule"` + // Detail states what was found against what was required — "no verified + // claim ties to this file", or the best tied evidence versus the floor. + Detail string `json:"detail"` +} + // SchemaVersion is the current version of the receipt schema (the payload). -const SchemaVersion = "0.0.10" +const SchemaVersion = "0.0.11"