Pin Brain formula evidence and verify SHA-256

static/3d/brain.html

@@ -12,8 +12,8 @@
      server performs fixed-allowlist, read-only, timeout + byte-bounded public reads:
        · Models / Datasets / Spaces / Collections — Hugging Face Hub API (SZLHOLDINGS)
        · Repositories — GitHub REST API (org szl-holdings)
-       · Proved formulas — the ProvedFormulas.lean source file, fetched server-side from
-         szl-holdings/a11oy and its `theorem` declarations counted in that observation.
+       · Proved formulas — a commit-pinned ProvedFormulas.lean artifact, fetched
+         server-side, SHA-256 verified, then counted for `theorem` declarations.
        · Fleet vitals — live /healthz probes of the organ Spaces (a11oy · killinchu ·
          anatomy · amaru · sentra), each answer is that organ's own, right now.
        · Open frontier — live Hub counts of the open-weights orgs the a11oy backbone
@@ -196,13 +196,14 @@ function countText(lobe) {
 const LOBES = [
   {
     key: "formulas", name: "Frontal — proved formulas", color: COL.formulas,
-    dir: [0, 0.55, 0.95], url: "https://github.com/" + GH_ORG + "/a11oy/blob/main/proofs/lutar-lean/Lutar/Puriq/Formulas/ProvedFormulas.lean",
+    dir: [0, 0.55, 0.95], url: "https://github.com/" + GH_ORG + "/a11oy/blob/22b084d4a74abb4d5911ca9dc303c35d222bd284/proofs/lutar-lean/Lutar/Puriq/Formulas/ProvedFormulas.lean",
     fetchStat: async () => {
       const s = requireLive(await EVIDENCE, "formulas");
       const n = s.theorem_count;
       return { text: n + " theorems", honesty: "MEASURED",
-        caption: "Frontal lobe · " + n + " `theorem` declarations counted server-side from the live " +
-          "ProvedFormulas.lean source on main · MEASURED via same-origin bounded evidence route · click to read the proofs" };
+        caption: "Frontal lobe · " + n + " `theorem` declarations counted server-side from a commit-pinned " +
+          "ProvedFormulas.lean artifact · SHA-256 " + s.content_sha256.slice(0, 12) + "… VERIFIED · " +
+          "MEASURED via same-origin bounded evidence route · click to read the pinned proofs" };
     },
   },
   {

szl3d_holographic.py

@@ -26,6 +26,7 @@ Mirrors the existing in-image static-serve pattern (serve.py /static/shared/{fna
 from __future__ import annotations
 
 import asyncio
+import hashlib
 import json
 import os
 from concurrent.futures import ThreadPoolExecutor, as_completed
@@ -251,8 +252,14 @@ def no_cdn_violations(base: Path):
 _BRAIN_PAGE_CAP = 100
 _BRAIN_TIMEOUT_S = 4.0
 _BRAIN_MAX_BYTES = 5 * 1024 * 1024
+_BRAIN_FORMULA_COMMIT = "22b084d4a74abb4d5911ca9dc303c35d222bd284"
+_BRAIN_FORMULA_PATH = "proofs/lutar-lean/Lutar/Puriq/Formulas/ProvedFormulas.lean"
+_BRAIN_FORMULA_SHA256 = "847d2e332017a5bfe3e7823092acf0245840f6b20f3d6f1544f723fd1607612e"
 _BRAIN_SOURCES: Dict[str, str] = {
-    "formulas": "https://raw.githubusercontent.com/szl-holdings/a11oy/main/proofs/lutar-lean/Lutar/Puriq/Formulas/ProvedFormulas.lean",
+    "formulas": (
+        "https://raw.githubusercontent.com/szl-holdings/a11oy/"
+        f"{_BRAIN_FORMULA_COMMIT}/{_BRAIN_FORMULA_PATH}"
+    ),
     "models": "https://huggingface.co/api/models?author=SZLHOLDINGS&limit=100&full=false",
     "datasets": "https://huggingface.co/api/datasets?author=SZLHOLDINGS&limit=100&full=false",
     "spaces": "https://huggingface.co/api/spaces?author=SZLHOLDINGS&limit=100&full=false",
@@ -301,6 +308,8 @@ def _brain_health(url: str) -> Dict[str, Any]:
 
 
 def _brain_error(exc: BaseException) -> str:
+    if isinstance(exc, ValueError) and str(exc) == "source_integrity_mismatch":
+        return "source_integrity_mismatch"
     if isinstance(exc, HTTPError):
         return f"upstream_http_{exc.code}"
     if isinstance(exc, (TimeoutError, OSError)):
@@ -338,6 +347,7 @@ def brain_evidence(
     fetch_json: Callable[[str], Any] = _brain_json,
     fetch_text: Callable[[str], str] = _brain_text,
     fetch_health: Callable[[str], Dict[str, Any]] = _brain_health,
+    expected_formula_sha256: str = _BRAIN_FORMULA_SHA256,
 ) -> Dict[str, Any]:
     """Build one honest Brain observation from fixed public sources.
 
@@ -371,10 +381,21 @@ def brain_evidence(
         if "formulas" in errors:
             raise errors["formulas"]
         source = raw["formulas"]
+        content_sha256 = hashlib.sha256(source.encode("utf-8")).hexdigest()
+        if content_sha256 != expected_formula_sha256:
+            raise ValueError("source_integrity_mismatch")
         theorem_count = len(_re.findall(r"(^|\n)\s*theorem\s", source))
         lobes["formulas"] = {
             "state": "LIVE", "data_label": "MEASURED",
-            "source_url": _BRAIN_SOURCES["formulas"], "theorem_count": theorem_count,
+            "source_url": _BRAIN_SOURCES["formulas"],
+            "source_repository": "szl-holdings/a11oy",
+            "source_path": _BRAIN_FORMULA_PATH,
+            "source_commit": _BRAIN_FORMULA_COMMIT,
+            "mutable_reference": False,
+            "theorem_count": theorem_count,
+            "content_sha256": content_sha256,
+            "expected_content_sha256": expected_formula_sha256,
+            "integrity_state": "VERIFIED",
         }
     except BaseException as exc:
         lobes["formulas"] = _unavailable(_BRAIN_SOURCES["formulas"], exc)
@@ -456,6 +477,8 @@ def brain_evidence(
             "read_only": True, "same_origin_browser_read": True,
             "fixed_allowlist": True, "timeout_seconds_per_source": _BRAIN_TIMEOUT_S,
             "response_byte_cap": _BRAIN_MAX_BYTES, "page_cap": _BRAIN_PAGE_CAP,
+            "formula_source_commit_pinned": True,
+            "formula_content_sha256_verified": True,
             "cache_or_last_good_fallback": False,
             "note": "Every request is a fresh bounded observation. Missing sources remain UNAVAILABLE.",
         },

test/test_holographic_zero_cdn.py

@@ -1,6 +1,7 @@
 """Zero-CDN and honest same-origin evidence contract regressions."""
 from __future__ import annotations
 
+import hashlib
 import unittest
 from pathlib import Path
 from unittest.mock import patch
@@ -39,14 +40,18 @@ class HolographicZeroCdnTests(unittest.TestCase):
         self.assertNotIn("fetch('https://", brain)
 
     def test_complete_observation_is_live_and_measured(self):
+        formula_source = "theorem one : True := by trivial\n  theorem two : True := by trivial\n"
         payload = holographic.brain_evidence(
             fetch_json=self._json,
-            fetch_text=lambda _url: "theorem one : True := by trivial\n  theorem two : True := by trivial\n",
+            fetch_text=lambda _url: formula_source,
             fetch_health=self._health,
+            expected_formula_sha256=hashlib.sha256(formula_source.encode("utf-8")).hexdigest(),
         )
         self.assertEqual(payload["state"], "LIVE")
         self.assertEqual(payload["live_lobes"], payload["lobe_count"])
         self.assertEqual(payload["lobes"]["formulas"]["theorem_count"], 2)
+        self.assertEqual(payload["lobes"]["formulas"]["integrity_state"], "VERIFIED")
+        self.assertFalse(payload["lobes"]["formulas"]["mutable_reference"])
         self.assertEqual(payload["lobes"]["models"]["downloads_sum"], 10)
         self.assertEqual(payload["lobes"]["fleet"]["up_count"], 5)
         self.assertFalse(payload["limits"]["cache_or_last_good_fallback"])
@@ -58,10 +63,12 @@ class HolographicZeroCdnTests(unittest.TestCase):
                 raise TimeoutError("test timeout")
             return self._json(url)
 
+        formula_source = "theorem one : True := by trivial\n"
         payload = holographic.brain_evidence(
             fetch_json=partial_json,
-            fetch_text=lambda _url: "theorem one : True := by trivial\n",
+            fetch_text=lambda _url: formula_source,
             fetch_health=self._health,
+            expected_formula_sha256=hashlib.sha256(formula_source.encode("utf-8")).hexdigest(),
         )
         frontier = payload["lobes"]["frontier"]
         self.assertEqual(payload["state"], "DEGRADED")
@@ -70,6 +77,25 @@ class HolographicZeroCdnTests(unittest.TestCase):
         failed = next(row for row in frontier["sources"] if row["org"] == "zai-org")
         self.assertEqual(failed["reason"], "upstream_unreachable_or_timeout")
 
+    def test_formula_source_is_commit_pinned_and_hash_allowlisted(self):
+        url = holographic._BRAIN_SOURCES["formulas"]
+        self.assertIn(holographic._BRAIN_FORMULA_COMMIT, url)
+        self.assertNotIn("/main/", url)
+        self.assertEqual(len(holographic._BRAIN_FORMULA_COMMIT), 40)
+        self.assertEqual(len(holographic._BRAIN_FORMULA_SHA256), 64)
+
+    def test_formula_hash_mismatch_is_unavailable_not_measured(self):
+        payload = holographic.brain_evidence(
+            fetch_json=self._json,
+            fetch_text=lambda _url: "theorem tampered : True := by trivial\n",
+            fetch_health=self._health,
+        )
+        formula = payload["lobes"]["formulas"]
+        self.assertEqual(payload["state"], "DEGRADED")
+        self.assertEqual(formula["state"], "UNAVAILABLE")
+        self.assertEqual(formula["reason"], "source_integrity_mismatch")
+        self.assertNotIn("theorem_count", formula)
+
     def test_route_is_get_only_no_store_and_same_contract(self):
         app = FastAPI()
         expected = {