Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,18 @@ claims that are *already written* into the change:
without adopting its title. Measured on a real 101-file change: 53 of 72
spec-id claims resolved, 17 honestly ambiguous, and the 2 orphans were both
real findings — an antipattern id cited in a PR title but never added to
the catalog, and an invariant no document defines.
the catalog, and an invariant no document defines. A repo that defines **no
spec-id corpus at all** is not practicing the convention: a probe-less
reference there has no possible referent, so it is a **mention**, not a
claim — suppressed rather than minted into the remainder, with the count
disclosed in the receipt's coverage. The gate sits at the premise level
deliberately: measured across two real corpora (2,880 and 642 sightings),
the dominant real-assertion shape is a mid-comment parenthetical id —
textually identical to an explanatory example — so no stricter annotation
grammar could separate the two without destroying most of the real harvest.
Measured on this repo's own sweep: the remainder's 7 example-id rows (0 of
7 were real invariants) became a single disclosed suppression line, while
both corpus-bearing dogfood repos produced byte-identical receipts.
- **Go probe bindings are coverage-proven where the code is annotated.** The
second rung. When a claim's id is also written into shipped code (its
*reference sites*, preserved through claim merges), the go-test probe run
Expand Down
4 changes: 3 additions & 1 deletion cmd/correctful/main.go
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,9 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL
if err != nil {
return fmt.Errorf("listing definition corpus: %w", err)
}
harvest.AnchorClaims(claims, harvest.BuildDefIndex(root, docs), change.Files)
var mentions int
claims, mentions = harvest.AnchorClaims(claims, harvest.BuildDefIndex(root, docs), change.Files)
coverage.SuppressedMentions = mentions

evidence := probe.NewDispatcher(concurrency, probe.Default()...).
Dispatch(ctx, root, claims)
Expand Down
37 changes: 34 additions & 3 deletions internal/harvest/anchor.go
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,27 @@ func BuildDefIndex(repoDir string, files []string) DefIndex {
}

// AnchorClaims resolves every spec-id claim against the definition index, in
// place. With an empty index (no corpus) it annotates nothing.
// place, and returns the claims it kept plus a count of suppressed mentions.
//
// PREMISE GATE. With an EMPTY index — a repo that defines no spec-id corpus
// anywhere — a probe-less spec-id reference cannot be a claim: with no
// definition to refer to, the sighting is a MENTION of an identifier, not an
// assertion about a defined invariant. Those claims are dropped and counted
// (the count is disclosed in the receipt's coverage — suppressing remainder
// rows silently would be the exact dishonesty the remainder exists to
// prevent). Everything else — probed spec-id claims, MUST clauses, test-name
// claims — passes through untouched.
//
// The gate is at the PREMISE level deliberately, not the token level.
// Measured across two real corpora (2,880 and 642 sightings): the dominant
// real-assertion convention is a mid-comment parenthetical id — exactly the
// shape of an explanatory example — so no annotation grammar can separate the
// two textually without destroying most of the real harvest. What separates
// them is the referent: real corpora define their ids in spec documents, and
// a repo with zero definitions is not practicing the convention at all. In a
// repo WITH a corpus, unresolvable ids stay as orphans — an orphan against an
// existing vocabulary is an anomaly worth surfacing, and both measured
// corpora yielded true orphans that were real findings.
//
// Two measured refinements beyond exact-id lookup:
//
Expand All @@ -121,9 +141,19 @@ func BuildDefIndex(repoDir string, files []string) DefIndex {
// title) lies inside the changed files, that definition is the claim's —
// a mechanical join, not a guess. A whole-tree sweep changes every file
// and therefore scopes nothing, which is the correct degeneration.
func AnchorClaims(claims []schema.Claim, idx DefIndex, changed []string) {
func AnchorClaims(claims []schema.Claim, idx DefIndex, changed []string) ([]schema.Claim, int) {
if len(idx) == 0 {
return
kept := claims[:0]
suppressed := 0
for _, c := range claims {
if c.Source.Kind == schema.SourceSpecID &&
specIDFromSegment(c.ID) == c.ID && len(c.ProbeIDs) == 0 {
suppressed++
continue
}
kept = append(kept, c)
}
return kept, suppressed
}
inChange := make(map[string]bool, len(changed))
for _, f := range changed {
Expand Down Expand Up @@ -168,6 +198,7 @@ func AnchorClaims(claims []schema.Claim, idx DefIndex, changed []string) {
c.Text = c.ID + ": " + title
}
}
return claims, 0
}

// parentID strips a sub-variant letter: INV-013d -> INV-013. Empty when the
Expand Down
40 changes: 29 additions & 11 deletions internal/harvest/anchor_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ func TestAnchorClaims(t *testing.T) {
{ID: "INV-777", Shape: schema.ShapeInvariant, Text: "INV-777 (referenced; no bound probe from harvest)"},
{ID: "MUST:docs/wire-rfc.md:1", Shape: schema.ShapeMustClause, Text: "The relay MUST forward frames in order."},
}
AnchorClaims(claims, idx, nil)
claims, _ = AnchorClaims(claims, idx, nil)

resolved := claims[0]
if resolved.Anchor == nil || resolved.Anchor.Status != schema.AnchorResolved {
Expand Down Expand Up @@ -148,14 +148,32 @@ func TestAnchorClaims(t *testing.T) {
}
}

// TestAnchorClaimsNoCorpus: a repo with no definition corpus gets no anchor
// annotations at all — a repo that never states invariants in documents
// should not have every claim flagged for it.
// TestAnchorClaimsNoCorpus: a repo with no definition corpus at all is not
// practicing the spec-id convention, so a probe-less spec-id reference there
// is a MENTION with no possible referent — suppressed and counted, never
// minted as a remainder row. Probed spec-id claims (a test binds the id) and
// non-spec claims pass through, and nothing gets an anchor annotation.
func TestAnchorClaimsNoCorpus(t *testing.T) {
claims := []schema.Claim{{ID: "INV-001", Shape: schema.ShapeInvariant, Text: "t"}}
AnchorClaims(claims, DefIndex{}, nil)
if claims[0].Anchor != nil {
t.Errorf("anchor = %+v, want nil when the corpus is empty", claims[0].Anchor)
claims := []schema.Claim{
{ID: "INV-001", Shape: schema.ShapeInvariant, Text: "t",
Source: schema.Source{Kind: schema.SourceSpecID, File: "a.go", Line: 3}},
{ID: "INV-002", Shape: schema.ShapeInvariant, Text: "tested",
Source: schema.Source{Kind: schema.SourceSpecID, File: "a.go", Line: 9},
ProbeIDs: []string{"go-test:x:TestINV002"}},
{ID: "MUST:doc.md:1", Shape: schema.ShapeMustClause, Text: "The tool MUST run.",
Source: schema.Source{Kind: schema.SourceRFCMust, File: "doc.md", Line: 1}},
}
kept, suppressed := AnchorClaims(claims, DefIndex{}, nil)
if suppressed != 1 {
t.Fatalf("suppressed = %d, want 1 (the probe-less reference)", suppressed)
}
if len(kept) != 2 || kept[0].ID != "INV-002" || kept[1].ID != "MUST:doc.md:1" {
t.Fatalf("kept = %+v, want the probed spec-id claim and the MUST clause", kept)
}
for _, c := range kept {
if c.Anchor != nil {
t.Errorf("anchor = %+v, want nil when the corpus is empty", c.Anchor)
}
}
}

Expand Down Expand Up @@ -187,7 +205,7 @@ func TestAnchorSubVariantFallsBackToParent(t *testing.T) {
{ID: "INV-020a", Shape: schema.ShapeInvariant, Text: "orig-20a"},
{ID: "INV-099z", Shape: schema.ShapeInvariant, Text: "orig-99z"},
}
AnchorClaims(claims, idx, nil)
claims, _ = AnchorClaims(claims, idx, nil)

if a := claims[0].Anchor; a == nil || a.Status != schema.AnchorAmbiguous || len(a.Sites) != 2 {
t.Errorf("INV-013d anchor = %+v, want ambiguous via parent's two colliding sites", claims[0].Anchor)
Expand Down Expand Up @@ -233,15 +251,15 @@ func TestAnchorChangeScopedDisambiguation(t *testing.T) {
}

unscoped := fresh()
AnchorClaims(unscoped, idx, nil)
unscoped, _ = AnchorClaims(unscoped, idx, nil)
for _, c := range unscoped {
if c.Anchor == nil || c.Anchor.Status != schema.AnchorAmbiguous {
t.Errorf("%s without change scope = %+v, want ambiguous", c.ID, c.Anchor)
}
}

scoped := fresh()
AnchorClaims(scoped, idx, []string{"specs/loader.md", "gate/loader_test.go"})
scoped, _ = AnchorClaims(scoped, idx, []string{"specs/loader.md", "gate/loader_test.go"})
own := scoped[0]
if own.Anchor == nil || own.Anchor.Status != schema.AnchorResolved ||
own.Text != "INV-004: Config check is routed through the loader" ||
Expand Down
3 changes: 3 additions & 0 deletions internal/receipt/markdown.go
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,9 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) {
if hist := unreadHistogram(cov); hist != "" {
fmt.Fprintf(w, "<sub>unread (no harvester for): %s</sub>\n", hist)
}
if cov.SuppressedMentions > 0 {
fmt.Fprintf(w, "<sub>%s</sub>\n", mentionNote(cov.SuppressedMentions))
}
fmt.Fprintf(w, "\n<sub>schema %s · exit gate: refuted claims block; the remainder informs, never fails</sub>\n", r.SchemaVersion)
}

Expand Down
9 changes: 9 additions & 0 deletions internal/receipt/receipt.go
Original file line number Diff line number Diff line change
Expand Up @@ -304,6 +304,15 @@ func writeCoverage(w io.Writer, cov schema.Coverage) {
if hist := unreadHistogram(cov); hist != "" {
fmt.Fprintf(w, " unread (no harvester for): %s\n", hist)
}
if cov.SuppressedMentions > 0 {
fmt.Fprintf(w, " %s\n", mentionNote(cov.SuppressedMentions))
}
}

// mentionNote states the premise-gate disclosure identically in every
// renderer — one phrasing, no drift between the receipt's formats.
func mentionNote(n int) string {
return fmt.Sprintf("%d spec-id mention(s) not minted as claims — the repo defines no spec-id corpus, so a reference has no possible referent", n)
}

// detailOf picks the evidence detail a reader needs: for a refuted claim, the
Expand Down
20 changes: 20 additions & 0 deletions internal/receipt/receipt_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,26 @@ func TestT0PassConfersNoVerification(t *testing.T) {
}
}

// TestSuppressedMentionsAreDisclosed: when the premise gate drops spec-id
// mentions (no definition corpus), BOTH renderers state the suppression —
// removing remainder rows silently would be the exact dishonesty the
// remainder exists to prevent.
func TestSuppressedMentionsAreDisclosed(t *testing.T) {
r := Assemble(gitdiff.Change{}, nil, nil, schema.Coverage{SuppressedMentions: 7})

var md strings.Builder
WriteMarkdown(&md, r)
if !strings.Contains(md.String(), "7 spec-id mention(s) not minted") {
t.Errorf("markdown receipt omits the suppression disclosure:\n%s", md.String())
}

var txt strings.Builder
WriteText(&txt, r)
if !strings.Contains(txt.String(), "7 spec-id mention(s) not minted") {
t.Errorf("text receipt omits the suppression disclosure:\n%s", txt.String())
}
}

// TestRemainderSectionAlwaysRenders: the text receipt states the remainder even
// when it is empty, so its absence is a declared result, not an omission.
func TestRemainderSectionAlwaysRenders(t *testing.T) {
Expand Down
10 changes: 9 additions & 1 deletion schema/schema.go
Original file line number Diff line number Diff line change
Expand Up @@ -287,6 +287,14 @@ type Coverage struct {
Claimed int `json:"claimed"` // files sourcing ≥1 claim
Scanned int `json:"scanned"` // read by ≥1 harvester, 0 claims
Unread int `json:"unread"` // no harvester read the file
// SuppressedMentions counts spec-id sightings that were NOT minted as
// claims because the repo defines no spec-id corpus at all: with no
// definition anywhere, a reference has no possible referent — it is a
// MENTION of an identifier, not a claim about a defined invariant. The
// suppression is disclosed here because dropping entries from the
// remainder silently would be exactly the dishonesty the remainder
// exists to prevent.
SuppressedMentions int `json:"suppressed_mentions,omitempty"`
}

// Receipt is the per-change output: what was claimed, what was verified, and —
Expand All @@ -304,4 +312,4 @@ type Receipt struct {
}

// SchemaVersion is the current version of the receipt schema (the payload).
const SchemaVersion = "0.0.4"
const SchemaVersion = "0.0.5"
Loading