From 0613305be649868756e794d23f8e1b9fb1be60c7 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Mon, 15 Jun 2026 01:24:48 +0000 Subject: [PATCH] feat(infra): add math-first CI scripts and fix wolfram-verification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Create the five missing scripts referenced by .pre-commit-config.yaml and .github/workflows/math-check.yml: - validate_deepseek_receipts.py — validates *.receipt.json against schema - validate_claims_registry.py — validates claims.yaml against schema + path checks - require_math_evidence.py — enforces evidence alongside math-track edits - test_validate_deepseek_receipts.py — 4 self-tests for receipt validator - test_require_math_evidence.py — 3 self-tests for evidence checker Fix wolfram-verification workflow: - Change permissions from issues:write to pull-requests:write (fixes 403) - Add TODO(wolfram-verify) annotations to E8Sidon.lean false positives ("normalized" in docstrings matching the normalize pattern) Co-Authored-By: Allaun Silverfox --- .github/workflows/wolfram-verification.yml | 2 +- .../lean/Semantics/Semantics/E8Sidon.lean | 4 +- scripts/math-first/require_math_evidence.py | 122 +++++++++++++++++ .../math-first/test_require_math_evidence.py | 115 ++++++++++++++++ .../test_validate_deepseek_receipts.py | 126 ++++++++++++++++++ .../math-first/validate_claims_registry.py | 100 ++++++++++++++ .../math-first/validate_deepseek_receipts.py | 69 ++++++++++ 7 files changed, 535 insertions(+), 3 deletions(-) create mode 100644 scripts/math-first/require_math_evidence.py create mode 100644 scripts/math-first/test_require_math_evidence.py create mode 100644 scripts/math-first/test_validate_deepseek_receipts.py create mode 100644 scripts/math-first/validate_claims_registry.py create mode 100644 scripts/math-first/validate_deepseek_receipts.py diff --git a/.github/workflows/wolfram-verification.yml b/.github/workflows/wolfram-verification.yml index 13fb55d3..5b428a7a 100644 --- a/.github/workflows/wolfram-verification.yml +++ b/.github/workflows/wolfram-verification.yml @@ -14,7 +14,7 @@ on: permissions: contents: read - issues: write + pull-requests: write jobs: wolfram-verification: diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean index 9dc041b4..620a4f97 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean @@ -124,7 +124,7 @@ lemma E8_normalization : -(2 * (8 : ℚ) / bernoulli 8) = 480 := by /-! ### Proof strategy (valence formula approach) -Let E₄, E₈ be the normalized Eisenstein series of weights 4, 8 for SL(2,ℤ). +Let E₄, E₈ be the normalized Eisenstein series of weights 4, 8 for SL(2,ℤ). -- TODO(wolfram-verify): standard Eisenstein normalization from Serre Ch.VII Their q-expansions are: E₄(τ) = 1 + 240 Σ_{n≥1} σ₃(n) qⁿ @@ -259,7 +259,7 @@ def r8 (n : ℕ) : ℕ := if n = 0 then 1 else 480 * sigma7 n /-- r₈ matches the E₈ theta series: Θ_{E₈} = E₄ (a classical result). - The theta series of E₈ equals the normalized Eisenstein series of weight 4, + The theta series of E₈ equals the normalized Eisenstein series of weight 4, -- TODO(wolfram-verify): classical Θ_{E₈} = E₄ identity so r₈(n) for n ≥ 1 equals 240 · σ₃(n). Wait — this uses E₄, not E₈. The identity Θ_{E₈} = E₄ is itself a diff --git a/scripts/math-first/require_math_evidence.py b/scripts/math-first/require_math_evidence.py new file mode 100644 index 00000000..d8f6644b --- /dev/null +++ b/scripts/math-first/require_math_evidence.py @@ -0,0 +1,122 @@ +#!/usr/bin/env python3 +"""Require math evidence (receipt or Lean change) alongside math-track edits. + +This script enforces the math-first contract: if a commit or PR touches files +in a math-track surface, at least one evidence file must also be present. + +Usage: + # CI mode: compare against a base ref + python3 scripts/math-first/require_math_evidence.py --from-git-diff origin/main + + # Pre-commit mode: check staged files + python3 scripts/math-first/require_math_evidence.py --staged + +Exits 0 if: + - No math-track files are present in the changeset, OR + - At least one evidence file is also in the changeset + +Exits 1 if math-track files are present but no evidence file accompanies them. +""" + +from __future__ import annotations + +import argparse +import subprocess +import sys +from pathlib import Path + +# Math-track surface prefixes: files under these paths require evidence +MATH_TRACK_PREFIXES = ( + "0-Core-Formalism/lean/Semantics/", + "6-Documentation/docs/distilled/", + "shared-data/data/stack_solidification/", +) + +# Evidence patterns: if any changed file matches, the requirement is satisfied +EVIDENCE_PREFIXES = ( + "shared-data/artifacts/deepseek_review/", + "0-Core-Formalism/lean/Semantics/", +) +EVIDENCE_FILES = ( + "claims.yaml", +) + + +def get_changed_files_git_diff(base_ref: str) -> list[str]: + """Get changed files by diffing against a base ref.""" + result = subprocess.run( + ["git", "diff", "--name-only", base_ref + "...HEAD"], + capture_output=True, text=True, check=False, + ) + if result.returncode != 0: + # Fall back to two-dot diff + result = subprocess.run( + ["git", "diff", "--name-only", base_ref], + capture_output=True, text=True, check=True, + ) + return [f for f in result.stdout.strip().split("\n") if f] + + +def get_changed_files_staged() -> list[str]: + """Get staged files for pre-commit hook.""" + result = subprocess.run( + ["git", "diff", "--cached", "--name-only"], + capture_output=True, text=True, check=True, + ) + return [f for f in result.stdout.strip().split("\n") if f] + + +def is_math_track(path: str) -> bool: + return any(path.startswith(p) for p in MATH_TRACK_PREFIXES) + + +def is_evidence(path: str) -> bool: + if any(path.startswith(p) for p in EVIDENCE_PREFIXES): + return True + if path in EVIDENCE_FILES: + return True + return False + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + group = parser.add_mutually_exclusive_group(required=True) + group.add_argument("--from-git-diff", metavar="BASE_REF", + help="Compare HEAD against BASE_REF") + group.add_argument("--staged", action="store_true", + help="Check staged files (pre-commit mode)") + args = parser.parse_args() + + if args.staged: + changed = get_changed_files_staged() + else: + changed = get_changed_files_git_diff(args.from_git_diff) + + if not changed: + print("No changed files") + return 0 + + math_files = [f for f in changed if is_math_track(f)] + if not math_files: + print("No math-track files in changeset — skipping evidence check") + return 0 + + evidence_files = [f for f in changed if is_evidence(f)] + if evidence_files: + print(f"OK: {len(math_files)} math-track file(s) with " + f"{len(evidence_files)} evidence file(s)") + return 0 + + # Math-track files present but no evidence + print("FAIL: math-track files changed but no evidence accompanies them:") + for f in math_files: + print(f" - {f}") + print("\nPlease include at least one of:") + print(" - A DeepSeek review receipt under shared-data/artifacts/deepseek_review/") + print(" - A Lean source file under 0-Core-Formalism/lean/Semantics/") + print(" - An update to claims.yaml") + return 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/math-first/test_require_math_evidence.py b/scripts/math-first/test_require_math_evidence.py new file mode 100644 index 00000000..a2a612a8 --- /dev/null +++ b/scripts/math-first/test_require_math_evidence.py @@ -0,0 +1,115 @@ +#!/usr/bin/env python3 +"""Self-tests for require_math_evidence.py. + +Tests the classification logic (is_math_track, is_evidence) without needing +a live git repo. Exits 0 on success, 1 on failure. +""" + +from __future__ import annotations + +import importlib.util +import sys +from pathlib import Path + +SCRIPT_DIR = Path(__file__).resolve().parent + + +def _load_module(): + """Import require_math_evidence as a module (it has dashes in the dir name).""" + spec = importlib.util.spec_from_file_location( + "require_math_evidence", + SCRIPT_DIR / "require_math_evidence.py", + ) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def test_math_track_classification() -> bool: + """Verify is_math_track correctly identifies math-track paths.""" + mod = _load_module() + + positives = [ + "0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean", + "6-Documentation/docs/distilled/ArithmeticSpec.md", + "shared-data/data/stack_solidification/receipt.md", + ] + negatives = [ + "4-Infrastructure/shim/some_script.py", + "scripts/math-first/validate_deepseek_receipts.py", + "README.md", + "flake.nix", + ] + + ok = True + for p in positives: + if not mod.is_math_track(p): + print(f"FAIL: {p} should be math-track but is not") + ok = False + for p in negatives: + if mod.is_math_track(p): + print(f"FAIL: {p} should NOT be math-track but is") + ok = False + + if ok: + print("PASS: math-track classification") + return ok + + +def test_evidence_classification() -> bool: + """Verify is_evidence correctly identifies evidence paths.""" + mod = _load_module() + + positives = [ + "shared-data/artifacts/deepseek_review/foo.receipt.json", + "0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean", + "claims.yaml", + ] + negatives = [ + "4-Infrastructure/shim/some_script.py", + "README.md", + ] + + ok = True + for p in positives: + if not mod.is_evidence(p): + print(f"FAIL: {p} should be evidence but is not") + ok = False + for p in negatives: + if mod.is_evidence(p): + print(f"FAIL: {p} should NOT be evidence but is") + ok = False + + if ok: + print("PASS: evidence classification") + return ok + + +def test_lean_file_is_self_evidence() -> bool: + """A Lean file IS its own evidence (under the evidence prefix).""" + mod = _load_module() + lean = "0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean" + if not mod.is_math_track(lean): + print("FAIL: Lean file not detected as math-track") + return False + if not mod.is_evidence(lean): + print("FAIL: Lean file not detected as evidence") + return False + print("PASS: Lean file is both math-track and evidence (self-evidencing)") + return True + + +def main() -> int: + tests = [ + test_math_track_classification, + test_evidence_classification, + test_lean_file_is_self_evidence, + ] + passed = sum(1 for t in tests if t()) + total = len(tests) + print(f"\n{passed}/{total} tests passed") + return 0 if passed == total else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/math-first/test_validate_deepseek_receipts.py b/scripts/math-first/test_validate_deepseek_receipts.py new file mode 100644 index 00000000..3e0f0384 --- /dev/null +++ b/scripts/math-first/test_validate_deepseek_receipts.py @@ -0,0 +1,126 @@ +#!/usr/bin/env python3 +"""Self-tests for validate_deepseek_receipts.py. + +Runs minimal smoke tests to verify the validator works against the live +schema and any existing receipts. Exits 0 on success, 1 on failure. +""" + +from __future__ import annotations + +import json +import sys +import tempfile +from pathlib import Path + +# Ensure we can import the validator's logic +SCRIPT_DIR = Path(__file__).resolve().parent +REPO_ROOT = SCRIPT_DIR.parents[1] +SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "deepseek-review-receipt.schema.json" + +try: + from jsonschema import Draft202012Validator, ValidationError +except ImportError: + print("SKIP: jsonschema not installed") + sys.exit(0) + + +def test_schema_compiles() -> bool: + """The schema itself must be valid JSON Schema.""" + if not SCHEMA_PATH.exists(): + print("SKIP: schema file not found") + return True + schema = json.loads(SCHEMA_PATH.read_text()) + Draft202012Validator.check_schema(schema) + print("PASS: schema compiles") + return True + + +def test_valid_receipt_accepted() -> bool: + """A minimal valid primary receipt must pass validation.""" + if not SCHEMA_PATH.exists(): + print("SKIP: schema file not found") + return True + schema = json.loads(SCHEMA_PATH.read_text()) + validator = Draft202012Validator(schema) + + valid_receipt = { + "schema": "ollama_deepseek_review_receipt_v1", + "created_at": "2026-01-01T00:00:00+00:00", + "model": "deepseek-v3.2", + "endpoint": "https://ollama.com/v1/chat/completions", + "prompt_sha256": "sha256:" + "a" * 64, + "answer_sha256": "sha256:" + "b" * 64, + "usage": {"prompt_tokens": 100, "completion_tokens": 200, "total_tokens": 300}, + "context_files": ["some/file.lean"], + "answer_path": "shared-data/artifacts/deepseek_review/test.md", + } + + errors = list(validator.iter_errors(valid_receipt)) + if errors: + print("FAIL: valid receipt rejected:") + for err in errors: + print(f" {err.message}") + return False + print("PASS: valid receipt accepted") + return True + + +def test_invalid_receipt_rejected() -> bool: + """A receipt missing required fields must be rejected.""" + if not SCHEMA_PATH.exists(): + print("SKIP: schema file not found") + return True + schema = json.loads(SCHEMA_PATH.read_text()) + validator = Draft202012Validator(schema) + + invalid_receipt = {"schema": "ollama_deepseek_review_receipt_v1"} + errors = list(validator.iter_errors(invalid_receipt)) + if not errors: + print("FAIL: invalid receipt was accepted") + return False + print("PASS: invalid receipt rejected") + return True + + +def test_bad_sha256_rejected() -> bool: + """A receipt with malformed SHA-256 must be rejected.""" + if not SCHEMA_PATH.exists(): + print("SKIP: schema file not found") + return True + schema = json.loads(SCHEMA_PATH.read_text()) + validator = Draft202012Validator(schema) + + receipt = { + "schema": "ollama_deepseek_review_receipt_v1", + "created_at": "2026-01-01T00:00:00+00:00", + "model": "deepseek-v3.2", + "endpoint": "https://ollama.com/v1/chat/completions", + "prompt_sha256": "not-a-hash", + "answer_sha256": "sha256:" + "b" * 64, + "usage": {"prompt_tokens": 100, "completion_tokens": 200, "total_tokens": 300}, + "context_files": ["some/file.lean"], + "answer_path": "shared-data/artifacts/deepseek_review/test.md", + } + errors = list(validator.iter_errors(receipt)) + if not errors: + print("FAIL: bad SHA-256 was accepted") + return False + print("PASS: bad SHA-256 rejected") + return True + + +def main() -> int: + tests = [ + test_schema_compiles, + test_valid_receipt_accepted, + test_invalid_receipt_rejected, + test_bad_sha256_rejected, + ] + passed = sum(1 for t in tests if t()) + total = len(tests) + print(f"\n{passed}/{total} tests passed") + return 0 if passed == total else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/math-first/validate_claims_registry.py b/scripts/math-first/validate_claims_registry.py new file mode 100644 index 00000000..9355c683 --- /dev/null +++ b/scripts/math-first/validate_claims_registry.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +"""Validate claims.yaml against its JSON Schema and check referenced paths. + +Usage (CI or local): + python3 scripts/math-first/validate_claims_registry.py + +Validates: + 1. claims.yaml parses as valid YAML + 2. Contents match shared-data/schemas/claims-registry.schema.json + 3. Every repo-relative path referenced in claims.yaml actually exists on disk + +Exits 0 on success, 1 on any failure. +""" + +from __future__ import annotations + +import json +import sys +from pathlib import Path + +try: + import yaml +except ImportError: + print("SKIP: PyYAML not installed (pip install PyYAML)") + sys.exit(0) + +try: + from jsonschema import Draft202012Validator +except ImportError: + print("SKIP: jsonschema not installed (pip install 'jsonschema>=4.21')") + sys.exit(0) + +REPO_ROOT = Path(__file__).resolve().parents[2] +CLAIMS_PATH = REPO_ROOT / "claims.yaml" +SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "claims-registry.schema.json" + + +def main() -> int: + if not CLAIMS_PATH.exists(): + print("SKIP: claims.yaml not found") + return 0 + + if not SCHEMA_PATH.exists(): + print(f"SKIP: schema not found at {SCHEMA_PATH}") + return 0 + + # Parse YAML + try: + data = yaml.safe_load(CLAIMS_PATH.read_text()) + except yaml.YAMLError as exc: + print(f"FAIL: claims.yaml is not valid YAML — {exc}") + return 1 + + # Validate against schema + schema = json.loads(SCHEMA_PATH.read_text()) + validator = Draft202012Validator(schema) + errors = list(validator.iter_errors(data)) + if errors: + print("FAIL: claims.yaml schema validation errors:") + for err in errors: + print(f" {err.json_path}: {err.message}") + return 1 + + print("OK claims.yaml matches schema") + + # Check referenced paths exist + missing = 0 + claims = data.get("claims", []) + for claim in claims: + cid = claim.get("id", "") + + # Check lean path + lean_path = claim.get("lean") + if lean_path and not (REPO_ROOT / lean_path).exists(): + print(f"WARN {cid}: lean path does not exist — {lean_path}") + # Warn only; the file might be in a different branch + + # Check review receipt paths + for rpath in claim.get("review_receipts", []): + if not (REPO_ROOT / rpath).exists(): + print(f"FAIL {cid}: receipt not found — {rpath}") + missing += 1 + + # Check source paths (skip external citations) + for spath in claim.get("sources", []): + if spath.startswith("http://") or spath.startswith("https://"): + continue + if not (REPO_ROOT / spath).exists(): + print(f"WARN {cid}: source not found — {spath}") + + if missing: + print(f"\n{missing} referenced receipt(s) not found on disk", file=sys.stderr) + return 1 + + print(f"\n{len(claims)} claim(s) validated OK") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/math-first/validate_deepseek_receipts.py b/scripts/math-first/validate_deepseek_receipts.py new file mode 100644 index 00000000..24011c6c --- /dev/null +++ b/scripts/math-first/validate_deepseek_receipts.py @@ -0,0 +1,69 @@ +#!/usr/bin/env python3 +"""Validate every tracked DeepSeek review receipt against its JSON Schema. + +Usage (CI or local): + python3 scripts/math-first/validate_deepseek_receipts.py + +Exits 0 if every receipt under shared-data/artifacts/deepseek_review/ +matches shared-data/schemas/deepseek-review-receipt.schema.json, or if +no receipts exist yet. Exits 1 on any validation failure. +""" + +from __future__ import annotations + +import json +import sys +from pathlib import Path + +try: + from jsonschema import Draft202012Validator +except ImportError: + print("SKIP: jsonschema not installed (pip install 'jsonschema>=4.21')") + sys.exit(0) + +REPO_ROOT = Path(__file__).resolve().parents[2] +SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "deepseek-review-receipt.schema.json" +RECEIPTS_DIR = REPO_ROOT / "shared-data" / "artifacts" / "deepseek_review" + + +def main() -> int: + if not SCHEMA_PATH.exists(): + print(f"SKIP: schema not found at {SCHEMA_PATH}") + return 0 + + schema = json.loads(SCHEMA_PATH.read_text()) + validator = Draft202012Validator(schema) + + receipts = sorted(RECEIPTS_DIR.glob("*.receipt.json")) if RECEIPTS_DIR.exists() else [] + if not receipts: + print("No receipts to validate") + return 0 + + failures = 0 + for path in receipts: + try: + data = json.loads(path.read_text()) + except json.JSONDecodeError as exc: + print(f"FAIL {path.relative_to(REPO_ROOT)}: invalid JSON — {exc}") + failures += 1 + continue + + errors = list(validator.iter_errors(data)) + if errors: + print(f"FAIL {path.relative_to(REPO_ROOT)}:") + for err in errors: + print(f" {err.json_path}: {err.message}") + failures += 1 + else: + print(f"OK {path.relative_to(REPO_ROOT)}") + + if failures: + print(f"\n{failures} receipt(s) failed validation", file=sys.stderr) + return 1 + + print(f"\n{len(receipts)} receipt(s) validated OK") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())