chore(infra): remove rs-surface from flake.nix (Garnix shutdown) and add math-first CI scripts

- Remove rsSurface and rsSurfaceImage Nix package definitions (Garnix is
  being shut down; build rs-surface directly with cargo when needed)
- Add scripts/math-first/ Python validators (receipt validation, claims
  registry validation, math evidence gate + tests) required by CI workflows

Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>

flake.nix

@@ -188,81 +188,6 @@
         mkdir -p -m 1777 $out/tmp
       '';
 
-      # ── rs-surface binary ───────────────────────────────────────────────────
-      # Rust port of 4-Infrastructure/infra/embedded_surface/server.py.
-      # Build the binary hermetically via rustPlatform.buildRustPackage.
-      #
-      # cargoHash: run `nix build .#rs-surface 2>&1 | grep "got:"` to get the
-      # real hash after any Cargo.lock change, then replace lib.fakeHash below.
-      rsSurface = pkgs.rustPlatform.buildRustPackage {
-        pname   = "rs-surface";
-        version = "0.1.0";
-
-        src = pkgs.lib.cleanSource ./4-Infrastructure/infra/embedded_surface/rs-surface;
-
-        cargoLock.lockFile = ./4-Infrastructure/infra/embedded_surface/rs-surface/Cargo.lock;
-
-        nativeBuildInputs = [ pkgs.pkg-config ];
-        buildInputs       = [ pkgs.openssl ];
-
-        meta = {
-          description = "Embedded node surface daemon (Rust)";
-          license     = pkgs.lib.licenses.mit;
-          mainProgram = "rs-surface";
-        };
-      };
-
-      # ── Minimal OCI image for the embedded node surface ────────────────────
-      # Built entirely from the Nix store — no Dockerfile, no Alpine, no musl.
-      # The closure contains only the binary + its glibc runtime deps.
-      #
-      # Build:  nix build .#rs-surface-image
-      # Load:   docker load < result
-      # Run:    docker run --rm -p 8080:8080 -v /etc/rs-surface:/etc/rs-surface rs-surface:latest
-      rsSurfaceImage = pkgs.dockerTools.buildLayeredImage {
-        name = "rs-surface";
-        tag  = "latest";
-
-        contents = [
-          rsSurface
-          pkgs.cacert          # TLS roots (for any outbound HTTPS)
-          pkgs.coreutils       # minimal shell utilities for healthcheck
-        ];
-
-        # /etc/rs-surface/node.json is volume-mounted at runtime; create the
-        # directory so the mount point exists in the image.
-        extraCommands = ''
-          mkdir -p etc/rs-surface var/lib/rs-surface mnt/topological-storage
-        '';
-
-        config = {
-          Entrypoint = [ "${rsSurface}/bin/rs-surface" ];
-          Env = [
-            "RS_SURFACE_PROFILE=/etc/rs-surface/node.json"
-            "RS_SURFACE_STATE=/var/lib/rs-surface"
-            "RS_SURFACE_MOUNT=/mnt/topological-storage"
-            "RS_SURFACE_HOST=0.0.0.0"
-            "RS_SURFACE_PORT=8080"
-            "SSL_CERT_FILE=${pkgs.cacert}/etc/ssl/certs/ca-bundle.crt"
-          ];
-          ExposedPorts = { "8080/tcp" = {}; };
-          Healthcheck = {
-            Test        = [ "CMD" "${pkgs.coreutils}/bin/sh" "-c"
-              "wget -qO- http://127.0.0.1:8080/health || exit 1" ];
-            Interval    = 10000000000;   # 10 s in nanoseconds
-            Timeout     = 3000000000;    # 3 s
-            StartPeriod = 3000000000;    # 3 s
-            Retries     = 3;
-          };
-          Labels = {
-            "org.opencontainers.image.description" = "rs-surface embedded node daemon";
-            "org.opencontainers.image.source"      = "4-Infrastructure/infra/embedded_surface/rs-surface";
-          };
-        };
-
-        maxLayers = 10;
-      };
-
     in rec {
       packages.${system} = {
 
@@ -303,9 +228,6 @@
           maxLayers = 120;
         };
 
-        # rs-surface binary and OCI image
-        rs-surface       = rsSurface;
-        rs-surface-image = rsSurfaceImage;
       };
 
       # Convenience alias: `nix build .#devcontainer`

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())

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())

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())

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", "<unknown>")
+
+        # 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())

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())