Merge math-first evidence gate fixups

.github/workflows/math-check.yml

@@ -77,6 +77,10 @@ jobs:
         run: |
           python3 scripts/math-first/test_validate_deepseek_receipts.py
 
+      - name: Self-tests for require_math_evidence (incl. regression)
+        run: |
+          python3 scripts/math-first/test_require_math_evidence.py
+
       - name: Validate claims registry
         run: |
           python3 scripts/math-first/validate_claims_registry.py

.pre-commit-config.yaml

@@ -78,11 +78,17 @@ repos:
           (Lean Semantics kernels, ArithmeticSpec docs, stack solidification
           receipts), require that at least one file under
           shared-data/artifacts/deepseek_review/ or
-          0-Core-Formalism/lean/Semantics/ is also part of the commit. This
+          0-Core-Formalism/lean/Semantics/ -- or claims.yaml -- is also part
-          enforces the math-first contract at commit time; the same check
+          of the same commit. This enforces the math-first contract at
-          runs in CI for PR-scope coverage.
+          commit time; the same check runs in CI for PR-scope coverage.
-        entry: scripts/math-first/require_math_evidence.py
+        entry: scripts/math-first/require_math_evidence.py --staged
         language: python
-        files: '^(0-Core-Formalism/lean/Semantics/|6-Documentation/docs/distilled/|shared-data/data/stack_solidification/).*$'
+        # always_run + pass_filenames: false because pre-commit's per-hook
-        pass_filenames: true
+        # ``files`` filter would otherwise strip evidence files (receipts,
+        # claims.yaml) from the staged file list before the script ever
+        # sees them. The script reads the full staged set itself via
+        # ``git diff --cached --name-only`` and exits 0 early if no
+        # math-track files are present, so this is cheap.
+        always_run: true
+        pass_filenames: false
         require_serial: true

docs/math-first-tooling.md

@@ -97,12 +97,18 @@ python3 scripts/math-first/validate_deepseek_receipts.py \
   shared-data/artifacts/deepseek_review/<topic>_<model>_<ts>.receipt.json
 ```
 
-The validator has its own self-tests:
+The receipt validator and the evidence gate both have self-tests:
 
 ```bash
 python3 scripts/math-first/test_validate_deepseek_receipts.py
+python3 scripts/math-first/test_require_math_evidence.py
 ```
 
+The `require_math_evidence` self-test includes a regression for the
+pre-commit `files`-filter bug: it builds a throwaway repo, stages a
+math-track file plus a receipt, then invokes the script with `--staged`
+to confirm both files are visible end-to-end.
+
 ## Mathematical Claim Registry
 
 [`claims.yaml`](../claims.yaml) is the single source of truth for the rigor
@@ -140,12 +146,16 @@ or `sources` exists on disk.
 * `claims-registry-schema` — runs the registry validator whenever
   `claims.yaml` is staged.
 * `receipt-required-for-math-content` — invokes
-  `scripts/math-first/require_math_evidence.py`. If a commit touches a
+  `scripts/math-first/require_math_evidence.py --staged`. If a commit
-  math-track surface (`0-Core-Formalism/lean/Semantics/`,
+  touches a math-track surface (`0-Core-Formalism/lean/Semantics/`,
   `6-Documentation/docs/distilled/`,
   `shared-data/data/stack_solidification/`), the same commit must also touch
   a math-evidence surface (a DeepSeek receipt, a Lean kernel, or
-  `claims.yaml`).
+  `claims.yaml`). The hook is configured with `always_run: true` and
+  `pass_filenames: false` so the script reads the entire staged set via
+  `git diff --cached --name-only`; pre-commit's per-hook `files` filter
+  would otherwise strip evidence files from the argv before the script
+  could see them.
 
 ### Install
 
@@ -174,7 +184,11 @@ math-first surface. It has three jobs:
 3. **`pre-commit`** — runs every pre-commit hook against the PR's range of
    changed files (`pre-commit run --from-ref <base> --to-ref HEAD`), so the
    guardrails are honoured even when a contributor has not installed the
-   hooks locally.
+   hooks locally. Note: `receipt-required-for-math-content` is a no-op in
+   this CI job because pre-commit's `--from-ref / --to-ref` mode does not
+   stage anything in the index, so the script's `--staged` lookup returns
+   an empty file list and exits 0. PR-scope enforcement of the same rule
+   lives in the dedicated `require-evidence` job above.
 
 The pre-existing `wolfram-verification.yml` workflow continues to police
 mathematical formulas inside Lean source for missing Wolfram Alpha
@@ -244,6 +258,7 @@ uv run --python 3.11 \
   bash -c '
     python3 scripts/math-first/validate_deepseek_receipts.py \
       && python3 scripts/math-first/test_validate_deepseek_receipts.py \
+      && python3 scripts/math-first/test_require_math_evidence.py \
       && python3 scripts/math-first/validate_claims_registry.py \
       && for r in shared-data/artifacts/deepseek_review/*.receipt.json; do \
            python3 5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py --verify-only "$r"; \

scripts/math-first/require_math_evidence.py

@@ -21,10 +21,12 @@ Math-evidence surfaces (accepted as evidence):
 
 Usage:
     scripts/math-first/require_math_evidence.py [FILES ...]
+    scripts/math-first/require_math_evidence.py --staged
     scripts/math-first/require_math_evidence.py --from-git-diff BASE_REF
 
-If neither files nor ``--from-git-diff`` is supplied the script exits 0 with
+If no input mode is supplied the script exits 0 with a noop. Pre-commit
-a noop. Pre-commit invokes it with the staged file list, CI invokes it with
+invokes it with ``--staged`` so the script sees the entire staged set
+regardless of pre-commit's own ``files`` filter; CI invokes it with
 ``--from-git-diff origin/<base>``.
 
 Exit code:
@@ -38,7 +40,34 @@ import subprocess
 import sys
 from pathlib import Path
 
-REPO_ROOT = Path(__file__).resolve().parents[2]
+
+def _git_toplevel(cwd: Path | None = None) -> Path:
+    """Return the absolute path of the git working tree containing ``cwd``.
+
+    Defaults to the current working directory. The script never assumes the
+    git repo lives at a hardcoded path because that would be wrong when the
+    script is run from a different working tree -- notably, the temp repo
+    set up by ``test_require_math_evidence.py``. Pre-commit and CI both
+    happen to invoke the script from inside the repo root, so letting the
+    git subprocess inherit cwd is correct in every real-world case.
+    """
+    cmd = ["git", "rev-parse", "--show-toplevel"]
+    try:
+        result = subprocess.run(
+            cmd,
+            capture_output=True,
+            text=True,
+            check=True,
+            cwd=str(cwd) if cwd is not None else None,
+        )
+    except subprocess.CalledProcessError as exc:
+        print(
+            f"error: `{' '.join(cmd)}` failed: {exc.stderr.strip()}",
+            file=sys.stderr,
+        )
+        raise SystemExit(2)
+    return Path(result.stdout.strip())
+
 
 MATH_TRACK_PREFIXES: tuple[str, ...] = (
     "0-Core-Formalism/lean/Semantics/",
@@ -80,9 +109,37 @@ def _is_evidence(path: str) -> bool:
 
 
 def _files_from_git_diff(base_ref: str) -> list[str]:
+    cwd = _git_toplevel()
     cmd = ["git", "diff", "--name-only", f"{base_ref}...HEAD"]
     try:
-        result = subprocess.run(cmd, capture_output=True, text=True, check=True, cwd=REPO_ROOT)
+        result = subprocess.run(
+            cmd, capture_output=True, text=True, check=True, cwd=str(cwd)
+        )
+    except subprocess.CalledProcessError as exc:
+        print(f"error: `{' '.join(cmd)}` failed: {exc.stderr.strip()}", file=sys.stderr)
+        raise SystemExit(2)
+    return [line.strip() for line in result.stdout.splitlines() if line.strip()]
+
+
+def _files_from_staged() -> list[str]:
+    """Return the staged file list via ``git diff --cached --name-only``.
+
+    Used by the pre-commit hook so the script sees every staged file --
+    math-track *and* evidence -- regardless of pre-commit's per-hook
+    ``files`` filter. This is important because pre-commit otherwise strips
+    receipts and ``claims.yaml`` from the argv before the script ever sees
+    them, which would cause the evidence check to falsely fail.
+
+    The subprocess cwd is the actual git toplevel containing the *current*
+    working directory, not a hardcoded path -- so the script works
+    correctly inside the regression test's temp repo too.
+    """
+    cwd = _git_toplevel()
+    cmd = ["git", "diff", "--cached", "--name-only"]
+    try:
+        result = subprocess.run(
+            cmd, capture_output=True, text=True, check=True, cwd=str(cwd)
+        )
     except subprocess.CalledProcessError as exc:
         print(f"error: `{' '.join(cmd)}` failed: {exc.stderr.strip()}", file=sys.stderr)
         raise SystemExit(2)
@@ -101,10 +158,21 @@ def main(argv: list[str] | None = None) -> int:
         metavar="BASE_REF",
         help="Compute the file list from `git diff --name-only BASE_REF...HEAD`.",
     )
+    parser.add_argument(
+        "--staged",
+        action="store_true",
+        help="Compute the file list from `git diff --cached --name-only` "
+        "(use this from pre-commit so the entire staged set is visible).",
+    )
     args = parser.parse_args(argv)
 
+    if sum(bool(x) for x in (args.from_git_diff, args.staged, args.files)) > 1:
+        parser.error("--from-git-diff, --staged, and explicit FILES are mutually exclusive")
+
     if args.from_git_diff:
         files = _files_from_git_diff(args.from_git_diff)
+    elif args.staged:
+        files = _files_from_staged()
     else:
         files = list(args.files)
 

scripts/math-first/test_require_math_evidence.py

@@ -0,0 +1,235 @@
+#!/usr/bin/env python3
+"""Self-check suite for ``require_math_evidence.py``.
+
+Covers the classification logic plus the pre-commit-vs-CI regression that
+motivated the follow-up fix: pre-commit applies its per-hook ``files``
+filter before the script runs, so the script must read the full staged
+set itself (via ``--staged``) rather than rely on the argv list.
+
+Exit code:
+    0  all cases passed.
+    1  at least one case failed.
+"""
+from __future__ import annotations
+
+import os
+import subprocess
+import sys
+import tempfile
+from pathlib import Path
+
+SCRIPT = Path(__file__).with_name("require_math_evidence.py")
+
+
+def _run(args: list[str], cwd: Path | None = None, env: dict[str, str] | None = None) -> tuple[int, str, str]:
+    cmd = [sys.executable, str(SCRIPT), *args]
+    result = subprocess.run(
+        cmd,
+        capture_output=True,
+        text=True,
+        cwd=str(cwd) if cwd else None,
+        env=env,
+    )
+    return result.returncode, result.stdout, result.stderr
+
+
+def _git(*args: str, cwd: Path) -> subprocess.CompletedProcess[str]:
+    return subprocess.run(
+        ["git", *args],
+        capture_output=True,
+        text=True,
+        check=True,
+        cwd=str(cwd),
+        env={
+            **os.environ,
+            "GIT_AUTHOR_NAME": "test",
+            "GIT_AUTHOR_EMAIL": "test@example.invalid",
+            "GIT_COMMITTER_NAME": "test",
+            "GIT_COMMITTER_EMAIL": "test@example.invalid",
+        },
+    )
+
+
+CASES: list[tuple[str, list[str], int]] = [
+    # (label, argv, expected exit code)
+    ("noop_empty", [], 0),
+    ("only_evidence_receipt", ["shared-data/artifacts/deepseek_review/x.receipt.json"], 0),
+    ("only_evidence_claims", ["claims.yaml"], 0),
+    ("only_unrelated", ["README.md", "src/foo.py"], 0),
+    ("lean_self_evidence", ["0-Core-Formalism/lean/Semantics/Kernel.lean"], 0),
+    ("doc_without_evidence", ["6-Documentation/docs/distilled/Spec.md"], 1),
+    (
+        "doc_with_receipt",
+        [
+            "6-Documentation/docs/distilled/Spec.md",
+            "shared-data/artifacts/deepseek_review/some.receipt.json",
+        ],
+        0,
+    ),
+    (
+        "doc_with_claims",
+        ["6-Documentation/docs/distilled/Spec.md", "claims.yaml"],
+        0,
+    ),
+    (
+        "stack_solidification_without_evidence",
+        ["shared-data/data/stack_solidification/foo.json"],
+        1,
+    ),
+    (
+        "stack_solidification_with_lean",
+        [
+            "shared-data/data/stack_solidification/foo.json",
+            "0-Core-Formalism/lean/Semantics/Bar.lean",
+        ],
+        0,
+    ),
+]
+
+
+def _run_argv_cases() -> int:
+    failures = 0
+    for label, argv, expected in CASES:
+        code, stdout, stderr = _run(argv)
+        if code != expected:
+            failures += 1
+            print(f"FAIL {label}: expected exit {expected}, got {code}")
+            if stdout.strip():
+                print(f"  stdout: {stdout.strip()}")
+            if stderr.strip():
+                print(f"  stderr: {stderr.strip()}")
+        else:
+            print(f"OK   {label} (exit {code})")
+    return failures
+
+
+def _run_mutex_check() -> int:
+    """`--staged` and `--from-git-diff` and explicit FILES are mutually exclusive."""
+    failures = 0
+    for argv in (
+        ["--staged", "--from-git-diff", "main"],
+        ["--staged", "claims.yaml"],
+        ["--from-git-diff", "main", "claims.yaml"],
+    ):
+        code, _stdout, stderr = _run(argv)
+        if code != 2:
+            failures += 1
+            print(f"FAIL mutex {argv}: expected exit 2, got {code}")
+            if stderr.strip():
+                print(f"  stderr: {stderr.strip()}")
+        else:
+            print(f"OK   mutex {argv} (exit {code})")
+    return failures
+
+
+def _run_staged_regression() -> int:
+    """Regression for the pre-commit ``files``-filter bug.
+
+    Builds a throwaway git repo so this test is self-contained -- the
+    test does not depend on the state of the real repo's index. The
+    script is run with ``cwd=tmp_path`` (NOT via ``runpy``) so that
+    ``git rev-parse --show-toplevel`` inside the script resolves to the
+    temp repo, and ``git diff --cached`` queries the temp repo's index.
+
+    Three sub-cases:
+        (a) math-track-only staged                -> expect exit 1
+            (proves the script actually evaluates classification logic;
+            without (a) the next sub-case could pass vacuously by
+            short-circuiting on an empty diff)
+        (b) math-track + receipt staged           -> expect exit 0
+            (the original pre-commit ``files``-filter bug)
+        (c) math-track + claims.yaml staged       -> expect exit 0
+            (verifies the registry-update path)
+    """
+    failures = 0
+    with tempfile.TemporaryDirectory() as tmp:
+        tmp_path = Path(tmp).resolve()
+        _git("init", "-q", cwd=tmp_path)
+
+        math_track = tmp_path / "6-Documentation" / "docs" / "distilled" / "Spec.md"
+        math_track.parent.mkdir(parents=True, exist_ok=True)
+        math_track.write_text("# math claim\n")
+
+        receipt = (
+            tmp_path / "shared-data" / "artifacts" / "deepseek_review" / "x.receipt.json"
+        )
+        receipt.parent.mkdir(parents=True, exist_ok=True)
+        receipt.write_text("{}\n")
+
+        claims = tmp_path / "claims.yaml"
+        claims.write_text("claims: []\n")
+
+        def _stage_only(*relpaths: str) -> None:
+            # Reset the index to a clean state, then stage exactly the
+            # supplied paths. ``git reset`` is safe here -- the temp repo
+            # has no commits, so there is no "HEAD" to reset against. We
+            # instead remove everything currently in the index.
+            _git("rm", "--cached", "-rf", "--ignore-unmatch", ".", cwd=tmp_path)
+            for relpath in relpaths:
+                _git("add", "--", relpath, cwd=tmp_path)
+
+        def _invoke() -> subprocess.CompletedProcess[str]:
+            return subprocess.run(
+                [sys.executable, str(SCRIPT), "--staged"],
+                capture_output=True,
+                text=True,
+                cwd=str(tmp_path),
+            )
+
+        def _assert(label: str, expected_exit: int, *staged: str) -> int:
+            _stage_only(*staged)
+            indexed = _git("diff", "--cached", "--name-only", cwd=tmp_path).stdout.splitlines()
+            indexed = [line for line in indexed if line.strip()]
+            if sorted(indexed) != sorted(staged):
+                print(f"FAIL {label}: index does not match expected staging")
+                print(f"  expected: {sorted(staged)}")
+                print(f"  actual:   {sorted(indexed)}")
+                return 1
+            result = _invoke()
+            if result.returncode != expected_exit:
+                print(
+                    f"FAIL {label}: expected exit {expected_exit}, "
+                    f"got {result.returncode}"
+                )
+                if result.stdout.strip():
+                    print(f"  stdout: {result.stdout.strip()}")
+                if result.stderr.strip():
+                    print(f"  stderr: {result.stderr.strip()}")
+                return 1
+            print(f"OK   {label} (exit {expected_exit})")
+            return 0
+
+        failures += _assert(
+            "staged_regression_negative (math-only -> FAIL)",
+            1,
+            "6-Documentation/docs/distilled/Spec.md",
+        )
+        failures += _assert(
+            "staged_regression_positive_receipt (math + receipt -> OK)",
+            0,
+            "6-Documentation/docs/distilled/Spec.md",
+            "shared-data/artifacts/deepseek_review/x.receipt.json",
+        )
+        failures += _assert(
+            "staged_regression_positive_claims (math + claims.yaml -> OK)",
+            0,
+            "6-Documentation/docs/distilled/Spec.md",
+            "claims.yaml",
+        )
+    return failures
+
+
+def main() -> int:
+    failures = 0
+    failures += _run_argv_cases()
+    failures += _run_mutex_check()
+    failures += _run_staged_regression()
+    if failures:
+        print(f"\n{failures} case(s) FAILED")
+        return 1
+    print("\nAll require_math_evidence self-checks passed.")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())

scripts/math-first/validate_claims_registry.py

@@ -26,7 +26,6 @@ from __future__ import annotations
 
 import argparse
 import json
-import re
 import sys
 from pathlib import Path
 from typing import Any
@@ -35,11 +34,21 @@ REPO_ROOT = Path(__file__).resolve().parents[2]
 SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "claims-registry.schema.json"
 DEFAULT_REGISTRY = REPO_ROOT / "claims.yaml"
 
-# Anything matching one of these prefixes is treated as an external citation
+# Anything matching one of these prefixes (case-insensitively) is treated
-# rather than a repo-relative path, and is therefore not required to resolve
+# as an external citation rather than a repo-relative path, and is therefore
-# to a file on disk.
+# not required to resolve to a file on disk. The list is intentionally
-_EXTERNAL_PREFIXES = ("http://", "https://", "arXiv:", "arxiv:", "doi:", "DOI:")
+# closed: matching every ``scheme:`` blob would silently skip path checks
-_EXTERNAL_RE = re.compile(r"^[A-Za-z]+:")
+# for anything that happens to contain a colon (e.g. ``Module:Theorem``),
+# which would hide registry rot.
+_EXTERNAL_PREFIXES: tuple[str, ...] = (
+    "http://",
+    "https://",
+    "arxiv:",
+    "doi:",
+    "isbn:",
+    "mailto:",
+    "urn:",
+)
 
 
 def _load_schema(schema_path: Path) -> dict[str, Any]:
@@ -90,9 +99,8 @@ def _load_registry(registry_path: Path) -> dict[str, Any]:
 
 
 def _is_external(reference: str) -> bool:
-    if reference.startswith(_EXTERNAL_PREFIXES):
+    lowered = reference.lower()
-        return True
+    return any(lowered.startswith(prefix) for prefix in _EXTERNAL_PREFIXES)
-    return bool(_EXTERNAL_RE.match(reference))
 
 
 def _check_path(reference: str) -> tuple[bool, str]:
@@ -126,9 +134,13 @@ def main(argv: list[str] | None = None) -> int:
     schema = _load_schema(args.schema)
     registry = _load_registry(args.path)
 
-    from jsonschema import Draft202012Validator
+    from jsonschema import Draft202012Validator, FormatChecker
 
-    validator = Draft202012Validator(schema)
+    # FormatChecker keeps date-time / uri / etc. behaviour consistent with
+    # validate_deepseek_receipts.py. Even though the current claims schema
+    # does not declare any ``format`` keywords, threading the checker in
+    # avoids a footgun for the next contributor who adds one.
+    validator = Draft202012Validator(schema, format_checker=FormatChecker())
     errors = sorted(validator.iter_errors(registry), key=lambda e: list(e.absolute_path))
     if errors:
         print(f"FAIL {args.path}")

shared-data/schemas/claims-registry.schema.json

@@ -64,7 +64,10 @@
       },
       "allOf": [
         {
-          "if": { "properties": { "status": { "const": "verified-by-ai" } } },
+          "if": {
+            "required": ["status"],
+            "properties": { "status": { "const": "verified-by-ai" } }
+          },
           "then": {
             "required": ["review_receipts"],
             "properties": {
@@ -73,7 +76,10 @@
           }
         },
         {
-          "if": { "properties": { "status": { "const": "formally-proven" } } },
+          "if": {
+            "required": ["status"],
+            "properties": { "status": { "const": "formally-proven" } }
+          },
           "then": { "required": ["lean"] }
         }
       ]