diff --git a/README.md b/README.md
index ca7cfd0..6cda4ad 100644
--- a/README.md
+++ b/README.md
@@ -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
diff --git a/cmd/correctful/main.go b/cmd/correctful/main.go
index c14902e..5b9f6f5 100644
--- a/cmd/correctful/main.go
+++ b/cmd/correctful/main.go
@@ -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)
diff --git a/internal/harvest/anchor.go b/internal/harvest/anchor.go
index 7606c22..3702f12 100644
--- a/internal/harvest/anchor.go
+++ b/internal/harvest/anchor.go
@@ -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:
//
@@ -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 {
@@ -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
diff --git a/internal/harvest/anchor_test.go b/internal/harvest/anchor_test.go
index 53ff8d0..90a48dc 100644
--- a/internal/harvest/anchor_test.go
+++ b/internal/harvest/anchor_test.go
@@ -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 {
@@ -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)
+ }
}
}
@@ -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)
@@ -233,7 +251,7 @@ 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)
@@ -241,7 +259,7 @@ func TestAnchorChangeScopedDisambiguation(t *testing.T) {
}
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" ||
diff --git a/internal/receipt/markdown.go b/internal/receipt/markdown.go
index e78145e..02f4d0e 100644
--- a/internal/receipt/markdown.go
+++ b/internal/receipt/markdown.go
@@ -81,6 +81,9 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) {
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))
+ }
fmt.Fprintf(w, "\nschema %s · exit gate: refuted claims block; the remainder informs, never fails\n", r.SchemaVersion)
}
diff --git a/internal/receipt/receipt.go b/internal/receipt/receipt.go
index fdf4f40..0f5ba4c 100644
--- a/internal/receipt/receipt.go
+++ b/internal/receipt/receipt.go
@@ -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
diff --git a/internal/receipt/receipt_test.go b/internal/receipt/receipt_test.go
index 0772992..e94a5db 100644
--- a/internal/receipt/receipt_test.go
+++ b/internal/receipt/receipt_test.go
@@ -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) {
diff --git a/schema/schema.go b/schema/schema.go
index 08698e5..f5cd8d4 100644
--- a/schema/schema.go
+++ b/schema/schema.go
@@ -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 —
@@ -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"