diff --git a/DESIGN.md b/DESIGN.md index 57d78f7..bdb4ff3 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -220,12 +220,14 @@ operationally: **the capped diff — your source changes — is transmitted to t Anthropic API.** Nothing else leaves the machine, and nothing at all does without the flag. -The cardinal rule is structural here, not aspirational: **proposals carry no -probes**, land in the remainder at T0, and are marked `[llm-proposed]` in -every rendering — nothing the model says can raise a tier or produce a false -pass. The worst a hallucinated claim can do is waste a remainder row. What the -extractor buys is an honest remainder for changes that never stated their -claims: "this change implicitly asserts X, Y, Z — none of it checked." +The cardinal rule is structural here, not aspirational: **nothing the model +says can, by itself, raise a tier or produce a false pass.** A proposal is +minted probe-less, lands in the remainder at T0, and is marked +`[llm-proposed]` in every rendering — verification included, so the +provenance is never laundered away. The worst a hallucinated claim can do is +waste a remainder row. What the extractor buys is an honest remainder for +changes that never stated their claims: "this change implicitly asserts X, +Y, Z — none of it checked." Discipline: pinned model (`claude-sonnet-5`; `CORRECTFUL_LLM_MODEL` overrides), a strict JSON output contract that fails loudly on @@ -240,9 +242,43 @@ mechanical path, so the CI gate never depends on a model. ANTHROPIC_API_KEY=... correctful -base auto -llm ``` -Verifying LLM proposals (binding them to probes) is a later increment, gated -like every extractor before it: kept only if it raises verification without a -false bind. +### Model-proposed edges (schema 0.0.8): proof-carrying binding for LLM claims + +Verifying LLM proposals is where the value loop closes — and where the trust +risk concentrates: a wrong claim→test association plus a passing test would +mint a false verification, the one failure mode the product exists to +prevent. So the model is allowed to propose an EDGE, never to certify one. +A proposal may name, in an optional `test` field, a changed Go test that +directly checks the claim, and the edge must then survive two mechanical +gates: + +1. **Existence, at mint time.** The named test's definition must appear in + the diff the model was shown — an added or context line of a changed + `_test.go` file (a deleted definition does not count: the test no longer + exists to run). Exactly one changed test file may define it (an ambiguous + name fails closed), and the claim's own file must be shipped Go code — + the target the second gate will check. A failed edge mints the claim + probe-less, exactly as before; the claim is never rejected for a bad + edge. +2. **Execution, at run time.** The bound probe's run is instrumented for + coverage, and the pass counts for the LLM claim ONLY when the profile + shows execution reaching the claim's file (`binding: file-covered` — the + file-level analogue of the function-level coverage-proven binding that + annotated spec-id claims get; an LLM claim carries a file, never a line). + Fail-closed in both directions: a profile whose execution never touched + the file REFUTES the edge (`file-not-reached` — which says nothing about + the claim itself), and a pass with no profile at all raises nothing. The + remainder row discloses which gate discarded the pass. + +Refutation keeps its unconditional dominance: a failing test in the change +blocks the gate no matter whose edge bound it — a mis-attributed refutation +is fail-safe, because the failure itself is real. What the model's word can +now reach, end to end: a remainder row becomes a T1 verified row exactly +when a machine confirmed both that the named test exists in the change and +that its execution demonstrably touches the code the claim is about — still +not proof the test asserts the right property, and the receipt's +`[llm-proposed]` marker plus `[binding: file-coverage-proven]` state +precisely that trust boundary on the row itself. Measured (first live runs, 2026-08): on a wild-case diff — a real 19-file change with zero pre-written claims — 19 of 20 proposals were accurate, diff --git a/README.md b/README.md index a7e9b18..8865481 100644 --- a/README.md +++ b/README.md @@ -18,8 +18,9 @@ Three rules control the receipt: - **A refuted claim stops the merge.** One failed probe is stronger than many passed probes. -- **Only a machine can verify a claim.** An LLM can propose a claim. A - proposal cannot increase a tier. +- **Only a machine can verify a claim.** An LLM can propose a claim, and it + can point to a changed test. The pass counts only when coverage data shows + that the test runs the claim's file. - **The receipt always shows the remainder**, also when the remainder is empty. The receipt also shows its own blind spots: the files that no harvester read, and the files that the scope excluded. @@ -86,7 +87,8 @@ remainder is a report, not a defect. Note: The `-llm` option sends the capped diff — your source changes — to the Anthropic API. The option needs `ANTHROPIC_API_KEY`. Without the option, no -data goes out from your machine. LLM proposals stay in the remainder at T0. +data goes out from your machine. An LLM proposal stays in the remainder, +unless a coverage-checked test in the change verifies it. ## The merge gate @@ -112,7 +114,7 @@ This repository uses this gate for each of its own pull requests. | an Alloy `run` | a witness claim (a pass shows that the model is consistent) | the Alloy result file | T3 | | spec ids in shipped code (`INV-…`, `AP-…`, …) | a reference claim, anchored to its definition | id-named tests, with coverage proof | — | | 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]` | no probe, by design | 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 | The tiers: **T0** unverified · **T1** one assertion held · **T2** an accept/reject pair held · **T3** property or model check · **T4** proof, diff --git a/internal/llmextract/llmextract.go b/internal/llmextract/llmextract.go index 20dc3f6..4ff02c8 100644 --- a/internal/llmextract/llmextract.go +++ b/internal/llmextract/llmextract.go @@ -3,12 +3,17 @@ // implicitly — the wild case, where nobody wrote a test name, a spec id, or a // MUST clause for the checker to harvest. // -// The cardinal rule is structural here, not aspirational: proposed claims are -// minted with NO probes, so they land in the receipt's remainder at T0 and -// nothing the model says can raise a tier or produce a false pass. The worst -// a hallucinated claim can do is waste a remainder row, and every proposal is -// marked llm-proposed so a reader never mistakes it for something the change -// wrote down itself. +// The cardinal rule is structural here, not aspirational: nothing the model +// says can, BY ITSELF, raise a tier or produce a false pass. A proposed claim +// is minted probe-less and lands in the remainder — unless the model also +// names a changed test that checks it, and that EDGE survives two mechanical +// gates: the test must exist in the diff (a changed _test.go function, found +// by parsing the sections the model was shown), and at run time the probe's +// own coverage profile must show execution reaching the claim's file. An edge +// that fails either gate binds nothing or verifies nothing; the receipt +// discloses which gate rejected it. The worst a hallucinated claim can do is +// waste a remainder row, and every proposal is marked llm-proposed so a +// reader never mistakes it for something the change wrote down itself. // // Determinism discipline: pinned model (overridable via CORRECTFUL_LLM_MODEL), // a strict JSON output contract with schema validation, and @@ -24,6 +29,7 @@ import ( "io" "net/http" "os" + "regexp" "strings" "time" @@ -98,7 +104,7 @@ func (h Harvester) Harvest(repoDir string, files []string) (harvest.Result, erro if err != nil { return harvest.Result{}, fmt.Errorf("llm extraction: %w", err) } - claims, err := mintProposals(raw, read) + claims, err := mintProposals(raw, read, sent) if err != nil { return harvest.Result{}, fmt.Errorf("llm extraction: %w", err) } @@ -177,11 +183,13 @@ func sectionFile(sec string) string { return "" } -// proposal is the model's required output element. +// proposal is the model's required output element. Test is optional: the name +// of a changed Go test function that directly checks the claim. type proposal struct { Shape string `json:"shape"` File string `json:"file"` Text string `json:"text"` + Test string `json:"test"` } // allowedShapes is the claim taxonomy the model may use — anything else is @@ -206,9 +214,10 @@ Rules: 2. Write each claim as one plain declarative sentence about the changed code. 3. Attribute each claim to the single changed file it is most about, using the exact path shown in the diff. 4. Propose at most ` + fmt.Sprint(maxProposals) + ` claims — the most load-bearing ones. If the diff supports fewer, return fewer. Do not invent claims the diff does not support. +5. If a Go test function CHANGED IN THIS DIFF directly checks a claim, add its exact function name in a "test" field. Only name a test whose definition appears in the diff. Omit the field when no changed test checks the claim or you are not sure. Output: a JSON array only — no prose, no code fences. Each element: -{"shape": "", "file": "", "text": ""} +{"shape": "", "file": "", "text": "", "test": ""} The diff: @@ -222,14 +231,23 @@ The diff: return b.String() } -// mintProposals validates the model's output and mints probe-less claims. -// Malformed output fails LOUDLY — a parse gate, not a salvage operation; the -// only tolerated wrapper is a markdown code fence. -func mintProposals(raw string, readFiles []string) ([]schema.Claim, error) { +// mintProposals validates the model's output and mints claims. Malformed +// output fails LOUDLY — a parse gate, not a salvage operation; the only +// tolerated wrapper is a markdown code fence. +// +// A proposal naming a "test" binds a go-test probe ONLY when the existence +// gate passes: the test's definition appears in the diff sections the model +// was shown (deleted definitions do not count), exactly one changed _test.go +// file defines it, and the claim's own file is a non-test Go file — the +// target the run-time coverage gate will check execution against. A binding +// that fails any of these mints the claim probe-less, exactly as before; the +// CLAIM is never rejected for a bad edge. +func mintProposals(raw string, readFiles []string, sections []string) ([]schema.Claim, error) { inRead := make(map[string]bool, len(readFiles)) for _, f := range readFiles { inRead[f] = true } + testDefs := testDefsInSections(sections) var props []proposal if err := json.Unmarshal([]byte(stripFences(raw)), &props); err != nil { return nil, fmt.Errorf("model output is not the required JSON array: %v (output begins %q)", err, truncateStr(raw, 120)) @@ -245,6 +263,12 @@ func mintProposals(raw string, readFiles []string) ([]schema.Claim, error) { if len(claims) == maxProposals { break } + var probes []string + if name := strings.TrimSpace(p.Test); name != "" { + if file, ok := testDefs[name]; ok && file != "" && isBindableClaimFile(p.File) { + probes = []string{schema.GoTestProbeID(file, name)} + } + } claims = append(claims, schema.Claim{ // The id hashes the proposal's content, so it is stable across // reorderings and re-runs of the same proposal — an ordinal would @@ -257,13 +281,52 @@ func mintProposals(raw string, readFiles []string) ([]schema.Claim, error) { File: p.File, Ref: "llm", }, - // No probes, by design: a proposal is remainder-bound until a - // machine verifies it. + // A model-proposed probe binding is an EDGE PROPOSAL, not + // verification: at run time the probe only counts for this claim + // when its coverage profile shows execution reaching Source.File + // (see probe.Dispatch and receipt weighing). Probe-less remains + // the default: a proposal is remainder-bound until a machine + // verifies it. + ProbeIDs: probes, }) } return claims, nil } +// isBindableClaimFile reports whether a claim file is a target the coverage +// gate can check: shipped Go code, not a test file. +func isBindableClaimFile(f string) bool { + return strings.HasSuffix(f, ".go") && !strings.HasSuffix(f, "_test.go") +} + +// testDefRe matches a top-level Go test function definition on an added or +// context diff line (leading '+' or ' '). A deleted definition ('-') must not +// match: the test no longer exists to run. +var testDefRe = regexp.MustCompile(`(?m)^[+ ]func (Test[A-Za-z0-9_]*)\s*\(`) + +// testDefsInSections maps each Go test function name defined in a changed +// _test.go section to that section's file. A name defined in MORE than one +// changed test file maps to "" — ambiguous, so the existence gate fails +// closed rather than guessing which package the model meant. +func testDefsInSections(sections []string) map[string]string { + defs := map[string]string{} + for _, sec := range sections { + file := sectionFile(sec) + if !strings.HasSuffix(file, "_test.go") { + continue + } + for _, m := range testDefRe.FindAllStringSubmatch(sec, -1) { + name := m[1] + if prev, seen := defs[name]; seen && prev != file { + defs[name] = "" + continue + } + defs[name] = file + } + } + return defs +} + // fnv32 is FNV-1a over the string — a stable content id, not a security hash. func fnv32(s string) uint32 { h := uint32(2166136261) diff --git a/internal/llmextract/llmextract_test.go b/internal/llmextract/llmextract_test.go index d8bd287..802fc41 100644 --- a/internal/llmextract/llmextract_test.go +++ b/internal/llmextract/llmextract_test.go @@ -289,3 +289,113 @@ func TestGithubSectionCannotCrowdOutCode(t *testing.T) { t.Error("shipped-code sections missing") } } + +// bindingPatch extends the sample with two changed test files (git's exact +// framing; content synthetic): one new test, one deleted test, one context +// test, and a name defined in BOTH test files (ambiguous). +const bindingPatch = samplePatch + `diff --git a/pkg/gate/gate_test.go b/pkg/gate/gate_test.go +index 5555555..6666666 100644 +--- a/pkg/gate/gate_test.go ++++ b/pkg/gate/gate_test.go +@@ -1,8 +1,11 @@ + package gate + ++func TestCheckRejectsNil(t *testing.T) { ++ if Check(nil) { ++ t.Fatal("nil accepted") ++ } ++} +-func TestGoneCheck(t *testing.T) { +- t.Skip() +-} + func TestContextCheck(t *testing.T) { + _ = Check + } ++func TestDupName(t *testing.T) { ++ _ = Check ++} +diff --git a/pkg/other/other_test.go b/pkg/other/other_test.go +index 7777777..8888888 100644 +--- a/pkg/other/other_test.go ++++ b/pkg/other/other_test.go +@@ -1,3 +1,6 @@ + package other + ++func TestDupName(t *testing.T) { ++ _ = 1 ++} +` + +// TestLLMEdgeExistenceGate: a proposal's "test" binds a go-test probe ONLY +// when the diff itself proves the test exists — a changed _test.go defines it +// on an added or context line, exactly one file defines it, and the claim's +// file is shipped Go code. Every failing case mints the claim PROBE-LESS; the +// claim itself is never rejected for a bad edge. +func TestLLMEdgeExistenceGate(t *testing.T) { + sections := splitSections(bindingPatch) + readFiles := []string{"pkg/gate/gate.go", "pkg/gate/gate_test.go", "docs/notes.md"} + cases := []struct { + name string + file string + test string + wantProbe string + }{ + {"added test binds", "pkg/gate/gate.go", "TestCheckRejectsNil", + "go-test:pkg/gate/gate_test.go:TestCheckRejectsNil"}, + {"context test binds", "pkg/gate/gate.go", "TestContextCheck", + "go-test:pkg/gate/gate_test.go:TestContextCheck"}, + {"deleted test does not exist", "pkg/gate/gate.go", "TestGoneCheck", ""}, + {"test absent from diff", "pkg/gate/gate.go", "TestNowhere", ""}, + {"ambiguous across test files", "pkg/gate/gate.go", "TestDupName", ""}, + {"non-go claim file unbindable", "docs/notes.md", "TestCheckRejectsNil", ""}, + {"test-file claim unbindable", "pkg/gate/gate_test.go", "TestCheckRejectsNil", ""}, + {"no test field", "pkg/gate/gate.go", "", ""}, + } + for _, tc := range cases { + t.Run(tc.name, func(t *testing.T) { + raw := fmt.Sprintf(`[{"shape":"assertion","file":%q,"text":"a claim.","test":%q}]`, tc.file, tc.test) + claims, err := mintProposals(raw, readFiles, sections) + if err != nil { + t.Fatal(err) + } + if len(claims) != 1 { + t.Fatalf("claims = %d, want 1 (the claim survives a bad edge)", len(claims)) + } + got := "" + if len(claims[0].ProbeIDs) == 1 { + got = claims[0].ProbeIDs[0] + } + if got != tc.wantProbe { + t.Errorf("probe = %q, want %q", got, tc.wantProbe) + } + }) + } +} + +// TestLLMEdgeFlowsThroughHarvest: the binding survives the full Harvest path +// — fixture server, parse gate, minting — so a bound proposal reaches the +// dispatcher with its probe attached and its llm-proposed source intact. +func TestLLMEdgeFlowsThroughHarvest(t *testing.T) { + out := `[{"shape":"invariant","file":"pkg/gate/gate.go","text":"Check rejects nil input.","test":"TestCheckRejectsNil"}]` + client, _, _ := fixtureServer(t, 200, apiFixture(out)) + h := Harvester{Patch: bindingPatch, Client: client} + + res, err := h.Harvest("/nowhere", []string{"pkg/gate/gate.go", "pkg/gate/gate_test.go", "docs/notes.md"}) + if err != nil { + t.Fatal(err) + } + if len(res.Claims) != 1 { + t.Fatalf("claims = %d, want 1", len(res.Claims)) + } + c := res.Claims[0] + if c.Source.Kind != schema.SourceLLM { + t.Errorf("source kind = %q, want llm", c.Source.Kind) + } + want := "go-test:pkg/gate/gate_test.go:TestCheckRejectsNil" + if len(c.ProbeIDs) != 1 || c.ProbeIDs[0] != want { + t.Errorf("probes = %v, want [%s]", c.ProbeIDs, want) + } + if !strings.Contains(extractionPrompt(splitSections(bindingPatch)), `"test"`) { + t.Errorf("prompt does not describe the optional test field") + } +} diff --git a/internal/probe/coverage.go b/internal/probe/coverage.go index 9419ec1..56d4fca 100644 --- a/internal/probe/coverage.go +++ b/internal/probe/coverage.go @@ -153,16 +153,32 @@ func bindingFor(repoDir string, refSites []schema.Source, prof covProfile) strin checkable = true for _, b := range blocks { if b.count > 0 && b.startLine <= enclosing.bodyEnd && b.endLine >= enclosing.bodyStart { - return "covered" + return schema.BindingCovered } } } if checkable { - return "name-only" + return schema.BindingNameOnly } return "" } +// fileBindingFor evaluates a model-proposed edge at file granularity: did the +// probe's execution reach the claim's file at all? Weaker than the +// function-level check — an LLM claim carries a file, never a line — but +// mechanical, and it is the gate that lets a model-proposed edge count: +// "file-covered" when any block of the file executed, "file-not-reached" +// when the instrumented run never touched it (including a file the profile +// does not know, which with -coverpkg=./... means it was not built in). +func fileBindingFor(prof covProfile, relFile string) string { + for _, b := range profileBlocksFor(prof, relFile) { + if b.count > 0 { + return schema.BindingFileCovered + } + } + return schema.BindingFileNotReached +} + // profileBlocksFor finds the profile entry whose import-qualified path ends // with the repo-relative file, on a path-component boundary. func profileBlocksFor(prof covProfile, relFile string) []covBlock { diff --git a/internal/probe/coverage_test.go b/internal/probe/coverage_test.go index 6dcdf2b..65ef975 100644 --- a/internal/probe/coverage_test.go +++ b/internal/probe/coverage_test.go @@ -62,6 +62,10 @@ func Unrelated() int { return 1 } // INV-901 lives on a const, outside any function: not checkable. const RefOnConst = "INV-901" +`, + "other.go": `package covmod + +func Other() int { return 2 } `, "gate_test.go": `package covmod @@ -78,6 +82,12 @@ func TestINV900_NameOnlyNeverCallsGate(t *testing.T) { t.Fatal("unrelated broke") } } + +func TestOnlyOther(t *testing.T) { + if Other() != 2 { + t.Fatal("other broke") + } +} `, } for rel, content := range files { @@ -126,3 +136,57 @@ func TestCoverageProvenBinding(t *testing.T) { t.Errorf("const-site claim binding = %q, want none (annotation not in any function)", b) } } + +// TestFileBindingFor: the file-level evaluator for model-proposed edges. +// Executed blocks anywhere in the file confirm the edge; a file whose blocks +// all read zero — or one the profile does not know — refutes it. +func TestFileBindingFor(t *testing.T) { + prof := parseCoverProfile(realProfileSnippet) + if got := fileBindingFor(prof, "cmd/tool/cmd_config.go"); got != schema.BindingFileCovered { + t.Errorf("executed file = %q, want %q", got, schema.BindingFileCovered) + } + if got := fileBindingFor(prof, "pkg/other/other.go"); got != schema.BindingFileNotReached { + t.Errorf("zero-count file = %q, want %q", got, schema.BindingFileNotReached) + } + if got := fileBindingFor(prof, "pkg/unknown/nope.go"); got != schema.BindingFileNotReached { + t.Errorf("unknown file = %q, want %q", got, schema.BindingFileNotReached) + } +} + +// TestLLMEdgeFileBinding: end-to-end through the dispatcher. An LLM-proposed +// claim has no reference sites, yet its probe run IS instrumented (the +// pre-pass marks SourceLLM claims) and the edge is evaluated at file +// granularity against the claim's own file: the test that executes gate.go +// confirms the edge; the test that only touches other.go refutes it. The +// VERDICTS stay untouched — both probes pass; only the edge differs. +func TestLLMEdgeFileBinding(t *testing.T) { + dir := writeCovModule(t) + pReaches := schema.GoTestProbeID("gate_test.go", "TestINV900_GateRejectsNil") + pElsewhere := schema.GoTestProbeID("gate_test.go", "TestOnlyOther") + + claims := []schema.Claim{ + {ID: "LLM:gate.go:aaaa", Shape: schema.ShapeAssertion, Text: "gate rejects nil", + Source: schema.Source{Kind: schema.SourceLLM, File: "gate.go", Ref: "llm"}, + ProbeIDs: []string{pReaches}}, + {ID: "LLM:gate.go:bbbb", Shape: schema.ShapeAssertion, Text: "a claim its named test never touches", + Source: schema.Source{Kind: schema.SourceLLM, File: "gate.go", Ref: "llm"}, + ProbeIDs: []string{pElsewhere}}, + } + evidence := NewDispatcher(2, GoTestRunner{}).Dispatch(context.Background(), dir, claims) + + if len(evidence) != 2 || len(evidence[0]) != 1 || len(evidence[1]) != 1 { + t.Fatalf("evidence shape = %v", evidence) + } + confirmed, refutedEdge := evidence[0][0], evidence[1][0] + if !confirmed.Ran || !confirmed.Passed || !refutedEdge.Ran || !refutedEdge.Passed { + t.Fatalf("verdicts degraded by instrumentation: %+v / %+v", confirmed, refutedEdge) + } + if confirmed.Binding != schema.BindingFileCovered { + t.Errorf("edge into executed file = %q, want %q (detail %q)", + confirmed.Binding, schema.BindingFileCovered, confirmed.Detail) + } + if refutedEdge.Binding != schema.BindingFileNotReached { + t.Errorf("edge into untouched file = %q, want %q", + refutedEdge.Binding, schema.BindingFileNotReached) + } +} diff --git a/internal/probe/probe.go b/internal/probe/probe.go index 73a454e..6dbe898 100644 --- a/internal/probe/probe.go +++ b/internal/probe/probe.go @@ -52,11 +52,13 @@ func NewDispatcher(concurrency int, runners ...Runner) *Dispatcher { // with Ran=false — recorded, not silently dropped. The remainder is computed // from what did not verify, so an unrunnable probe must leave a trace. func (d *Dispatcher) Dispatch(ctx context.Context, repoDir string, claims []schema.Claim) [][]schema.Evidence { - // Pre-pass: mark go-test probes whose claims carry code reference sites — - // those runs are instrumented for coverage so the attribution pass below - // can evaluate each edge's binding (see coverage.go). + // Pre-pass: mark go-test probes whose edges the attribution pass below + // must evaluate against a coverage profile — claims carrying code + // reference sites (function-level binding, see coverage.go) and + // LLM-proposed claims (file-level binding: a model-proposed edge COUNTS + // only when execution demonstrably reaches the claim's file). for _, c := range claims { - if !hasGoRefSite(c) { + if !hasGoRefSite(c) && c.Source.Kind != schema.SourceLLM { continue } for _, pid := range c.ProbeIDs { @@ -112,10 +114,17 @@ func (d *Dispatcher) Dispatch(ctx context.Context, repoDir string, claims []sche ev := *results[pid] ev.ClaimID = c.ID // Binding is a property of the EDGE: the shared execution's - // profile is evaluated against THIS claim's reference sites. + // profile is evaluated against THIS claim's own targets — + // reference sites for annotated claims, the claim's file for + // model-proposed edges. No profile means no binding statement, + // which for an LLM edge fails closed at weighing. if ev.Ran { if p, ok := covProfiles.Load(pid); ok { - ev.Binding = bindingFor(repoDir, c.RefSites, p.(covProfile)) + if c.Source.Kind == schema.SourceLLM { + ev.Binding = fileBindingFor(p.(covProfile), c.Source.File) + } else { + ev.Binding = bindingFor(repoDir, c.RefSites, p.(covProfile)) + } } } out[i][j] = ev diff --git a/internal/receipt/markdown.go b/internal/receipt/markdown.go index cdc8158..f18a7ca 100644 --- a/internal/receipt/markdown.go +++ b/internal/receipt/markdown.go @@ -58,7 +58,7 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) { fmt.Fprintln(w, "|---|---|---|") for _, res := range r.Remainder { fmt.Fprintf(w, "| `%s` | %s | `%s:%d` |\n", - mdCell(res.Claim.ID), mdCell(res.Claim.Text+anchorNote(res.Claim)+llmNote(res.Claim)), + mdCell(res.Claim.ID), mdCell(res.Claim.Text+anchorNote(res.Claim)+llmNote(res.Claim)+llmEdgeNote(res)), res.Claim.Source.File, res.Claim.Source.Line) } } @@ -72,7 +72,7 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) { if res.Status == schema.StatusVerified { fmt.Fprintf(w, "| %s | `%s` | %s |\n", res.EffectiveTier, mdCell(res.Claim.ID), - mdCell(res.Claim.Text+anchorNote(res.Claim)+bindingNote(res))) + mdCell(res.Claim.Text+anchorNote(res.Claim)+llmNote(res.Claim)+bindingNote(res))) } } fmt.Fprintln(w, "\n") diff --git a/internal/receipt/receipt.go b/internal/receipt/receipt.go index 56c76d7..729e5ae 100644 --- a/internal/receipt/receipt.go +++ b/internal/receipt/receipt.go @@ -35,7 +35,7 @@ func Assemble(change gitdiff.Change, claims []schema.Claim, evidence [][]schema. for j := range evs { evs[j].Detail = sanitizePaths(evs[j].Detail, change.Repo) } - status, tier := weigh(evs) + status, tier := weigh(c, evs) res := schema.ClaimResult{ Claim: c, @@ -119,9 +119,11 @@ func bindingNote(res schema.ClaimResult) string { nameOnly := false for _, e := range res.Evidence { switch e.Binding { - case "covered": + case schema.BindingCovered: return " [binding: coverage-proven]" - case "name-only": + case schema.BindingFileCovered: + return " [binding: file-coverage-proven]" + case schema.BindingNameOnly: nameOnly = true } } @@ -131,6 +133,30 @@ func bindingNote(res schema.ClaimResult) string { return "" } +// 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 +// profile existed to confirm it. Rendered on remainder rows — the claim's +// probe DID run, and silently rendering the row as "nothing checked" would +// hide that a pass was discarded. +func llmEdgeNote(res schema.ClaimResult) string { + if res.Claim.Source.Kind != schema.SourceLLM { + return "" + } + for _, e := range res.Evidence { + if !e.Verified() { + continue + } + switch e.Binding { + case schema.BindingFileNotReached: + return " [llm edge rejected: the probe passed but never executed " + res.Claim.Source.File + "]" + case "": + return " [llm edge unconfirmed: no coverage profile, so the pass raised nothing]" + } + } + return "" +} + // llmNote marks an LLM-proposed claim wherever it renders: a reader must // never mistake a model's proposal for something the change wrote down. func llmNote(c schema.Claim) string { @@ -280,12 +306,20 @@ func scrubHost(s, host string) string { // raises nothing); effective tier is the highest a passing probe // conferred. // - unverified: nothing ran that could raise the claim. Remainder. -func weigh(evs []schema.Evidence) (schema.Status, schema.Tier) { +// +// 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. +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(): + case e.Verified() && (c.Source.Kind != schema.SourceLLM || e.Binding == schema.BindingFileCovered): anyVerified = true if e.Tier > best { best = e.Tier @@ -346,8 +380,8 @@ func WriteText(w io.Writer, r schema.Receipt) { fmt.Fprintln(w, "VERIFIED") for _, res := range r.Results { if res.Status == schema.StatusVerified { - fmt.Fprintf(w, " [%s] %s — %s%s%s\n", res.EffectiveTier, res.Claim.ID, res.Claim.Text, - anchorNote(res.Claim), bindingNote(res)) + fmt.Fprintf(w, " [%s] %s — %s%s%s%s\n", res.EffectiveTier, res.Claim.ID, res.Claim.Text, + anchorNote(res.Claim), llmNote(res.Claim), bindingNote(res)) } } fmt.Fprintln(w) @@ -369,8 +403,8 @@ func WriteText(w io.Writer, r schema.Receipt) { fmt.Fprintln(w, " (empty — every harvested claim reached a probe)") } for _, res := range r.Remainder { - fmt.Fprintf(w, " %s — %s [%s:%d]%s%s\n", res.Claim.ID, res.Claim.Text, - res.Claim.Source.File, res.Claim.Source.Line, anchorNote(res.Claim), llmNote(res.Claim)) + fmt.Fprintf(w, " %s — %s [%s:%d]%s%s%s\n", res.Claim.ID, res.Claim.Text, + res.Claim.Source.File, res.Claim.Source.Line, anchorNote(res.Claim), llmNote(res.Claim), llmEdgeNote(res)) } writeCoverage(w, r.Coverage) diff --git a/internal/receipt/receipt_test.go b/internal/receipt/receipt_test.go index b7c54a9..661ec69 100644 --- a/internal/receipt/receipt_test.go +++ b/internal/receipt/receipt_test.go @@ -421,3 +421,74 @@ func TestDetailSanitizationIsCategorical(t *testing.T) { t.Errorf("short-hostname guard failed: %q", got) } } + +// llmClaim is a bound LLM proposal for the edge-gate tests. +func llmClaim() schema.Claim { + return schema.Claim{ + ID: "LLM:pkg/gate.go:0a1b2c3d", Shape: schema.ShapeAssertion, + Text: "the gate rejects nil", + Source: schema.Source{Kind: schema.SourceLLM, File: "pkg/gate.go", Line: 0, Ref: "llm"}, + ProbeIDs: []string{"go-test:pkg/gate_test.go:TestGateRejectsNil"}, + } +} + +func llmEvidence(passed bool, binding string) [][]schema.Evidence { + return [][]schema.Evidence{{{ + ClaimID: "LLM:pkg/gate.go:0a1b2c3d", ProbeID: "go-test:pkg/gate_test.go:TestGateRejectsNil", + Tier: schema.T1Assertion, Ran: true, Passed: passed, Binding: binding, + }}} +} + +// TestLLMPassCountsOnlyWithConfirmedEdge: the fail-closed gate on +// model-proposed edges. A pass verifies ONLY with binding "file-covered"; +// a pass whose edge was refuted by coverage, or never confirmed at all, +// raises nothing and the remainder row says which. Refutation stays +// unconditional — a failing probe blocks regardless of the edge. +func TestLLMPassCountsOnlyWithConfirmedEdge(t *testing.T) { + cases := []struct { + name string + passed bool + binding string + wantStatus schema.Status + wantNote string + }{ + {"confirmed edge verifies", true, schema.BindingFileCovered, schema.StatusVerified, ""}, + {"refuted edge stays remainder", true, schema.BindingFileNotReached, schema.StatusUnverified, "llm edge rejected"}, + {"unconfirmed edge stays remainder", true, "", schema.StatusUnverified, "llm edge unconfirmed"}, + {"failing probe refutes regardless", false, "", schema.StatusRefuted, ""}, + } + for _, tc := range cases { + t.Run(tc.name, func(t *testing.T) { + r := Assemble(gitdiff.Change{BaseRef: "main", HeadRef: "wip"}, + []schema.Claim{llmClaim()}, llmEvidence(tc.passed, tc.binding), schema.Coverage{}) + if got := r.Results[0].Status; got != tc.wantStatus { + t.Fatalf("status = %q, want %q", got, tc.wantStatus) + } + var text strings.Builder + WriteText(&text, r) + if tc.wantNote != "" && !strings.Contains(text.String(), tc.wantNote) { + t.Errorf("text receipt lacks %q:\n%s", tc.wantNote, text.String()) + } + }) + } +} + +// TestLLMVerifiedRowKeepsProvenance: a verified LLM claim must still be +// recognizable as model-proposed, in BOTH renderers — verification must not +// launder the provenance away — and the confirmed edge is stated beside it. +func TestLLMVerifiedRowKeepsProvenance(t *testing.T) { + r := Assemble(gitdiff.Change{BaseRef: "main", HeadRef: "wip"}, + []schema.Claim{llmClaim()}, llmEvidence(true, schema.BindingFileCovered), schema.Coverage{}) + + var text, md strings.Builder + WriteText(&text, r) + WriteMarkdown(&md, r) + for name, out := range map[string]string{"text": text.String(), "markdown": md.String()} { + if !strings.Contains(out, "[llm-proposed]") { + t.Errorf("%s verified row lost llm provenance:\n%s", name, out) + } + if !strings.Contains(out, "[binding: file-coverage-proven]") { + t.Errorf("%s verified row lacks the edge statement:\n%s", name, out) + } + } +} diff --git a/schema/schema.go b/schema/schema.go index 362f6a4..20f1620 100644 --- a/schema/schema.go +++ b/schema/schema.go @@ -181,17 +181,34 @@ type Evidence struct { Detail string `json:"detail,omitempty"` Duration string `json:"duration,omitempty"` // Binding states how strongly this probe is tied to THIS claim — the - // second rung of proof-carrying binding, orthogonal to the tier. - // "covered": the probe's execution demonstrably reached the enclosing - // function of a code site naming the claim's id — proof the test - // exercises the annotated region (still not proof it asserts the right - // property). "name-only": the binding was checked and NO annotated region - // was reached — the tie between this probe and this claim is the name - // alone. Empty: no coverage check applied (no code sites, or the probe - // kind has no prover yet). + // second rung of proof-carrying binding, orthogonal to the tier. See the + // Binding* constants for the vocabulary. Empty: no coverage check applied + // (no code sites, or the probe kind has no prover yet). Binding string `json:"binding,omitempty"` } +// Binding values — how a probe→claim edge was checked. The first two apply to +// claims whose id is annotated in shipped code (RefSites); the file-level pair +// applies to LLM-proposed edges, where the claim carries a file but no line. +const ( + // BindingCovered: the probe's execution demonstrably reached the + // enclosing function of a code site naming the claim's id — proof the + // test exercises the annotated region (still not proof it asserts the + // right property). + BindingCovered = "covered" + // BindingNameOnly: the binding was checked and NO annotated region was + // reached — the tie between this probe and this claim is the name alone. + BindingNameOnly = "name-only" + // BindingFileCovered: the probe's execution demonstrably reached the file + // the claim is about. The file-level analogue of BindingCovered, used for + // model-proposed edges: it is what makes such an edge count at all. + BindingFileCovered = "file-covered" + // BindingFileNotReached: the probe ran instrumented and its execution + // 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" +) + // Verified reports whether this evidence raises its claim: the probe ran, // passed, AND confers a tier above T0. A pass at T0 confers nothing — T0 IS // the unverified tier, so counting such a pass as verification would mint @@ -342,4 +359,4 @@ type Receipt struct { } // SchemaVersion is the current version of the receipt schema (the payload). -const SchemaVersion = "0.0.7" +const SchemaVersion = "0.0.8"