Disclose scope exclusions on the receipt; pin the harvested input

.github/workflows/correctful.yml

@@ -40,7 +40,12 @@ jobs:
           cat receipt.md
           cat receipt.md >> "$GITHUB_STEP_SUMMARY"
 
+      # The comment is a delivery channel, not the contract: the Gate step
+      # carries the verdict, and the receipt is also in the job summary and
+      # log. A GitHub API outage here must not fail a clean receipt (measured:
+      # a GraphQL 503 failed the job before the Gate step ever ran).
       - name: Post or update PR comment
+        continue-on-error: true
         env:
           GH_TOKEN: ${{ github.token }}
           PR: ${{ github.event.pull_request.number }}

README.md

@@ -202,6 +202,19 @@ claims that are *already written* into the change:
   exercised the library beneath the annotated cmd-level enforcement sites).
   Instrumentation never degrades a verdict: an instrumented run that cannot
   execute falls back to a plain run and simply carries no binding statement.
+- **The scope boundary states its own blind spots, and the input is pinned.**
+  The change resolver deliberately excludes two classes of untracked file —
+  never-tracked top-level trees (an installed tool's cache; measured, one
+  such tree drowned a 184-file change under 2,000+ files) and hidden paths.
+  Those files never reach the harvest, so the coverage section cannot account
+  for them; the receipt therefore discloses the exclusions at the scope
+  boundary itself (`excluded`: reason, count, and the trees affected — a
+  brand-new top-level directory of real work stays invisible until its first
+  `git add`, and the receipt now *says so* on every affected run). Beside the
+  commit SHAs, `input_digest` pins a SHA-256 over the exact harvested content
+  (sorted path + per-file content hash, deletions marked absent), so a
+  mid-branch receipt over staged, unstaged, or untracked work — which no
+  commit SHA identifies — is reproducible and comparable too.
 - **Same-id claims merge; accept/reject pairs earn T2.** Every test named for
   one invariant becomes a probe of the same claim — all run, any can refute.
   When one of those tests is accept-polarity and another is reject-polarity

cmd/correctful/main.go

@@ -90,6 +90,9 @@ func run(base, repo, format string, concurrency int, timeout time.Duration, useL
 	if root == "" {
 		root = repo
 	}
+	// Pin the harvested input: commit SHAs identify only committed state, and
+	// a mid-branch receipt harvests the working tree.
+	change.InputDigest = gitdiff.InputDigest(root, change.Files)
 
 	// Harvest claims, then dispatch probes against them.
 	harvesters := harvest.Default()

internal/gitdiff/gitdiff.go

@@ -4,9 +4,14 @@ package gitdiff
 
 import (
 	"context"
+	"crypto/sha256"
+	"encoding/hex"
 	"fmt"
+	"io"
 	"os"
 	"os/exec"
+	"path/filepath"
+	"sort"
 	"strings"
 )
 
@@ -20,6 +25,26 @@ type Change struct {
 	BaseSHA string
 	HeadSHA string
 	Files   []string
+	// Excluded discloses what Resolve deliberately left OUT of Files. Those
+	// files never reach the harvest, so the coverage section cannot mention
+	// them — this is the one place the exclusion can be stated, and "blind
+	// spots are always stated" applies to the scope boundary itself.
+	Excluded []Exclusion
+	// InputDigest pins the exact content harvested (see the InputDigest
+	// function). HeadSHA identifies a clean tree; a mid-branch receipt over
+	// staged, unstaged, or untracked work needs this to be reproducible.
+	InputDigest string
+}
+
+// Exclusion is one scope rule's deliberate effect on the change: how many
+// files the resolver left out, why, and (for the territory rule) which
+// top-level trees they lived in. Counts, not paths — the measured case was
+// thousands of cache files, and reproducing the list would drown the receipt
+// in exactly the noise the rule exists to exclude.
+type Exclusion struct {
+	Reason string   // stable identifier: "untracked-territory" | "untracked-hidden"
+	Count  int      // files excluded by this rule
+	Dirs   []string // top-level trees affected (territory rule only), sorted
 }
 
 // Resolve returns the files changed between baseRef and the working tree head in
@@ -67,26 +92,54 @@ func Resolve(ctx context.Context, dir, baseRef string) (Change, error) {
 		trackedTop[top] = true
 	}
 	untracked, _ := run(ctx, dir, "ls-files", "--others", "--exclude-standard")
+	// Hidden is checked FIRST so a hidden file inside a never-tracked tree is
+	// attributed to the harvest-wide hidden-path principle, not the narrower
+	// territory rule. Tracked hidden files (a CI workflow) are unaffected —
+	// the exclusions apply to the untracked union only.
+	hidden := 0
+	territoryDirs := map[string]bool{}
+	territory := 0
 	for _, f := range nonEmptyLines(untracked) {
+		if hiddenPath(f) {
+			hidden++
+			continue
+		}
 		top, _, inDir := strings.Cut(f, "/")
 		if inDir && !trackedTop[top] {
-			continue // an entirely untracked top-level tree; the root itself is always tracked territory
+			// An entirely untracked top-level tree; the root itself is
+			// always tracked territory.
+			territoryDirs[top] = true
+			territory++
+			continue
 		}
-		if hiddenPath(f) || contains(files, f) {
+		if contains(files, f) {
 			continue
 		}
 		files = append(files, f)
 	}
+	var excluded []Exclusion
+	if territory > 0 {
+		dirs := make([]string, 0, len(territoryDirs))
+		for d := range territoryDirs {
+			dirs = append(dirs, d)
+		}
+		sort.Strings(dirs)
+		excluded = append(excluded, Exclusion{Reason: "untracked-territory", Count: territory, Dirs: dirs})
+	}
+	if hidden > 0 {
+		excluded = append(excluded, Exclusion{Reason: "untracked-hidden", Count: hidden})
+	}
 
 	baseSHA, _ := run(ctx, dir, "merge-base", baseRef, "HEAD")
 	headSHA, _ := run(ctx, dir, "rev-parse", "HEAD")
 	return Change{
-		Repo:    strings.TrimSpace(repo),
-		BaseRef: baseRef,
-		HeadRef: strings.TrimSpace(head),
-		BaseSHA: strings.TrimSpace(baseSHA),
-		HeadSHA: strings.TrimSpace(headSHA),
-		Files:   files,
+		Repo:     strings.TrimSpace(repo),
+		BaseRef:  baseRef,
+		HeadRef:  strings.TrimSpace(head),
+		BaseSHA:  strings.TrimSpace(baseSHA),
+		HeadSHA:  strings.TrimSpace(headSHA),
+		Files:    files,
+		Excluded: excluded,
 	}, nil
 }
 
@@ -177,6 +230,53 @@ func TrackedByPattern(ctx context.Context, dir string, patterns ...string) ([]st
 	return nonEmptyLines(out), nil
 }
 
+// InputDigest computes a SHA-256 pin over the exact content the harvest will
+// read, so a receipt over a DIRTY tree — staged, unstaged, or untracked work
+// that no commit SHA identifies — is still reproducible: same file set, same
+// bytes, same digest.
+//
+// The formula, so anyone can recompute it: for each file of the resolved set
+// in ascending path order, feed the outer SHA-256 the path, a NUL, then the
+// 32 raw bytes of the file content's own SHA-256 (the string "absent" instead
+// when the path is not a readable regular file — a deletion is part of the
+// change's identity too), then a newline. Per-file inner hashing makes file
+// boundaries unambiguous regardless of content bytes.
+func InputDigest(dir string, files []string) string {
+	sorted := append([]string(nil), files...)
+	sort.Strings(sorted)
+	outer := sha256.New()
+	for _, f := range sorted {
+		io.WriteString(outer, f)
+		outer.Write([]byte{0})
+		if sum, ok := fileSHA256(filepath.Join(dir, f)); ok {
+			outer.Write(sum)
+		} else {
+			io.WriteString(outer, "absent")
+		}
+		outer.Write([]byte{'\n'})
+	}
+	return hex.EncodeToString(outer.Sum(nil))
+}
+
+// fileSHA256 streams a regular file into a SHA-256, reporting !ok for
+// anything unreadable or non-regular (deleted files, directories, symlink
+// targets outside the tree).
+func fileSHA256(abs string) ([]byte, bool) {
+	fh, err := os.Open(abs)
+	if err != nil {
+		return nil, false
+	}
+	defer fh.Close()
+	if fi, err := fh.Stat(); err != nil || !fi.Mode().IsRegular() {
+		return nil, false
+	}
+	h := sha256.New()
+	if _, err := io.Copy(h, fh); err != nil {
+		return nil, false
+	}
+	return h.Sum(nil), true
+}
+
 func run(ctx context.Context, dir string, args ...string) (string, error) {
 	cmd := exec.CommandContext(ctx, "git", args...)
 	cmd.Dir = dir

internal/gitdiff/gitdiff_test.go

@@ -202,4 +202,54 @@ func TestResolveIncludesUntrackedButNotHiddenState(t *testing.T) {
 	if change.BaseSHA == "" || change.HeadSHA == "" {
 		t.Errorf("SHA pins missing: %+v", change)
 	}
+	// The exclusions above must be DISCLOSED, not silent: the skipped files
+	// never reach the harvest, so the scope boundary is the only place the
+	// blind spot can be stated.
+	if len(change.Excluded) != 2 {
+		t.Fatalf("excluded = %+v, want the territory and hidden rules disclosed", change.Excluded)
+	}
+	terr, hid := change.Excluded[0], change.Excluded[1]
+	if terr.Reason != "untracked-territory" || terr.Count != 1 || len(terr.Dirs) != 1 || terr.Dirs[0] != "toolcache" {
+		t.Errorf("territory exclusion = %+v, want 1 file under toolcache", terr)
+	}
+	if hid.Reason != "untracked-hidden" || hid.Count != 1 {
+		t.Errorf("hidden exclusion = %+v, want 1 hidden untracked file", hid)
+	}
+}
+
+// TestInputDigestPinsWorkingTreeContent: the digest is a function of the
+// resolved set's CONTENT alone — stable across recomputation and input
+// order, changed by an edit, and defined (via an absence marker) for a file
+// the change deletes.
+func TestInputDigestPinsWorkingTreeContent(t *testing.T) {
+	dir := t.TempDir()
+	if err := os.WriteFile(filepath.Join(dir, "a.go"), []byte("package a\n"), 0o644); err != nil {
+		t.Fatal(err)
+	}
+	if err := os.WriteFile(filepath.Join(dir, "b.go"), []byte("package b\n"), 0o644); err != nil {
+		t.Fatal(err)
+	}
+
+	d1 := InputDigest(dir, []string{"a.go", "b.go", "gone.go"})
+	d2 := InputDigest(dir, []string{"gone.go", "b.go", "a.go"}) // order must not matter
+	if d1 != d2 {
+		t.Errorf("digest depends on input order: %s vs %s", d1, d2)
+	}
+	if len(d1) != 64 {
+		t.Errorf("digest = %q, want 64 hex chars", d1)
+	}
+
+	if err := os.WriteFile(filepath.Join(dir, "b.go"), []byte("package b // edited\n"), 0o644); err != nil {
+		t.Fatal(err)
+	}
+	if d3 := InputDigest(dir, []string{"a.go", "b.go", "gone.go"}); d3 == d1 {
+		t.Errorf("digest unchanged by a content edit — it pins nothing")
+	}
+
+	// A deleted file is part of the change's identity: present-then-deleted
+	// and never-present must both be representable, and a set WITHOUT the
+	// deleted path digests differently from one with it.
+	if with, without := InputDigest(dir, []string{"a.go", "gone.go"}), InputDigest(dir, []string{"a.go"}); with == without {
+		t.Errorf("deleted file invisible to the digest")
+	}
 }

internal/receipt/markdown.go

@@ -30,8 +30,12 @@ func WriteMarkdown(w io.Writer, r schema.Receipt) {
 		fmt.Fprintf(w, "Anchoring: %d of %d spec-id claims resolved to definitions · %d ambiguous · %d orphan\n\n",
 			a.Resolved, a.SpecIDClaims, a.Ambiguous, a.Orphan)
 	}
-	fmt.Fprintf(w, "Change: `%s...%s`%s — %d files\n\n", r.Change.BaseRef, r.Change.HeadRef,
+	fmt.Fprintf(w, "Change: `%s...%s`%s — %d files\n", r.Change.BaseRef, r.Change.HeadRef,
 		mdCell(shaNote(r.Change)), len(r.Change.Files))
+	if note := exclusionNote(r.Change.Excluded); note != "" {
+		fmt.Fprintf(w, "<sub>%s</sub>\n", note)
+	}
+	fmt.Fprintln(w)
 
 	if s.Refuted > 0 {
 		fmt.Fprintln(w, "### ❌ Refuted — a probe ran and the claim did not hold")

internal/receipt/receipt.go

@@ -61,12 +61,14 @@ func Assemble(change gitdiff.Change, claims []schema.Claim, evidence [][]schema.
 			// The receipt carries the repository NAME, never its location: a
 			// receipt is shareable, and external-tool details are scrubbed of
 			// local paths for the same reason (see sanitizePaths).
-			Repo:    filepath.Base(change.Repo),
-			BaseRef: change.BaseRef,
-			HeadRef: change.HeadRef,
-			BaseSHA: change.BaseSHA,
-			HeadSHA: change.HeadSHA,
-			Files:   change.Files,
+			Repo:        filepath.Base(change.Repo),
+			BaseRef:     change.BaseRef,
+			HeadRef:     change.HeadRef,
+			BaseSHA:     change.BaseSHA,
+			HeadSHA:     change.HeadSHA,
+			Files:       change.Files,
+			Excluded:    exclusions(change.Excluded),
+			InputDigest: change.InputDigest,
 		},
 		Results:   results,
 		Remainder: remainder,
@@ -153,21 +155,60 @@ func anchorNote(c schema.Claim) string {
 	return ""
 }
 
-// shaNote renders the immutable pins beside the symbolic refs, abbreviated.
+// 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
 	}
+	var parts []string
 	switch {
 	case c.BaseSHA != "" && c.HeadSHA != "":
-		return fmt.Sprintf(" (%s..%s)", short(c.BaseSHA), short(c.HeadSHA))
+		parts = append(parts, short(c.BaseSHA)+".."+short(c.HeadSHA))
 	case c.HeadSHA != "":
-		return fmt.Sprintf(" (@%s)", short(c.HeadSHA))
+		parts = append(parts, "@"+short(c.HeadSHA))
 	}
-	return ""
+	if c.InputDigest != "" {
+		parts = append(parts, "input:"+short(c.InputDigest))
+	}
+	if len(parts) == 0 {
+		return ""
+	}
+	return " (" + strings.Join(parts, " · ") + ")"
+}
+
+// exclusions maps the resolver's scope-exclusion records into the schema.
+func exclusions(in []gitdiff.Exclusion) []schema.Exclusion {
+	var out []schema.Exclusion
+	for _, e := range in {
+		out = append(out, schema.Exclusion{Reason: e.Reason, Count: e.Count, Dirs: e.Dirs})
+	}
+	return out
+}
+
+// exclusionNote states the scope boundary's own blind spot in one line —
+// shared by every renderer so the disclosure cannot drift between formats.
+func exclusionNote(excl []schema.Exclusion) string {
+	if len(excl) == 0 {
+		return ""
+	}
+	var parts []string
+	for _, e := range excl {
+		switch e.Reason {
+		case "untracked-territory":
+			parts = append(parts, fmt.Sprintf("%d untracked file(s) in never-tracked top-level trees (%s) — invisible until first `git add`",
+				e.Count, strings.Join(e.Dirs, ", ")))
+		case "untracked-hidden":
+			parts = append(parts, fmt.Sprintf("%d hidden untracked file(s)", e.Count))
+		default:
+			parts = append(parts, fmt.Sprintf("%d file(s): %s", e.Count, e.Reason))
+		}
+	}
+	return "scope excluded " + strings.Join(parts, " · ")
 }
 
 // sanitizePaths scrubs local filesystem locations from probe detail text: the
@@ -239,7 +280,11 @@ func WriteText(w io.Writer, r schema.Receipt) {
 	if r.Change.Repo != "" {
 		fmt.Fprintf(w, "  [%s]", r.Change.Repo)
 	}
-	fmt.Fprintf(w, "\nfiles: %d changed\n\n", len(r.Change.Files))
+	fmt.Fprintf(w, "\nfiles: %d changed\n", len(r.Change.Files))
+	if note := exclusionNote(r.Change.Excluded); note != "" {
+		fmt.Fprintf(w, "  %s\n", note)
+	}
+	fmt.Fprintln(w)
 
 	fmt.Fprintf(w, "claims: %d   verified: %d   refuted: %d   unverified: %d\n",
 		s.TotalClaims, s.Verified, s.Refuted, s.Unverified)