diff --git a/tests/fixtures/atlas_formal_build_3b39/README.md.txt b/tests/fixtures/atlas_formal_build_3b39/README.md.txt new file mode 100644 index 000000000..a3dd293c8 --- /dev/null +++ b/tests/fixtures/atlas_formal_build_3b39/README.md.txt @@ -0,0 +1,144 @@ +# Formal package: SIDE24 arithmetic skeleton (Lean 4, core only) + +Scientific effect: **NONE**. This directory is the second package in the +repository's formal-verification lane. The lane's contract is the +[formal-verification guide](../docs/FORMAL_VERIFICATION.md); new work is claimed in +the relevant current pull request or work discussion under the +[current workflow](../governance/OP-WORKFLOW-20260930.md). +Closed [work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) is the +historical formal-ladder work item; the first package is the +[Math- pilot](https://github.com/d6g8k5htny-coder/Math-/tree/cc2989c1280f4f227d0c6aa30c8841d6ba01e46e/formal) +(13 GP-FOR-192 scalar companions, Lean 4 + Mathlib). This package follows the same +manifest, status, gate and alignment contract and adds nothing to the +scientific-status vocabulary. + +What it covers: the exact integer and rational identities and inequalities that +sections 1–4 of the [SIDE24 coefficient note](sources/side24_v1/PROOF.md) +(`Math-@9d7b6802…`, SHA-256 `c06dacc…`) rely on — 31 theorems, stated in core +Lean as cross-multiplied integer facts and proved by `decide`. What it does not +cover is listed target by target in [SCOPE.md](SCOPE.md): not the coefficient +bound `0.07340691930603427103 < c_{2,24} < 0.07340691930603427104`, not the +definition of the coefficient, not any Gaussian, Kac–Rice, cone-integral, +Stirling or interval-arithmetic step, not `coefficient.py`. Relative to the +guide's historical work-offer table this is the **first step only** of the "Numerical +formalizer" offer; the exact coefficient definition and the proof-producing +enclosure pipeline are not supplied. + +## Layout + +| Path | Role | +|---|---| +| `lean-toolchain`, `lakefile.toml`, `lake-manifest.json` | Pinned toolchain `leanprover/lean4:v4.34.1`; Lake package `UniversalLaw` with **no** dependencies (`dependency_revisions` is empty and the gate checks the lock agrees) | +| `UniversalLaw.lean` | Root module; imports exactly the three registered modules | +| `UniversalLaw/Side24/Ledger.lean` | 17 targets: pairing count, image constant, `60E < 10^-108`, Taylor partial sum of `exp(288/125)`, odd-block minors, section-4 exponent bounds, density-comparison order of magnitude | +| `UniversalLaw/Side24/ConeMoments.lean` | 10 targets: conditional variances, transverse covariance thirds, `D_1 = 4/3`, `D_2 = 29/6 − √6` algebra, cube-root simplification, Hessian block eigenvalues | +| `UniversalLaw/Side24/Endpoints.lean` | 4 targets: the published 20-digit endpoints as integers — adjacency, ordering, magnitude. **Not an enclosure of the coefficient.** | +| `sources/side24_v1/` | Byte copies of the two pinned Layer 0 sources (`PROOF.md`, `ENCLOSURE.json`) | +| `manifest.json` | Evidence sidecar: package identity, toolchain, allowed axioms, SHA-256 of every bound file, pinned sources, 31 targets with verbatim informal anchors and `does_not_claim`, executable negative controls | +| `SCOPE.md` | Exact coverage and "not established" per target; the review contract | +| `ALIGNMENT.md` | Generated from the manifest (`--write-alignment`); never hand-edited | +| `GLOSSARY.md` | Descriptive mapping of project terms to standard objects and Lean availability | +| `REVIEW_LANE.md`, `reviews/` | Independent statement-alignment review procedure, JSON record template, validator | + +## Status vocabulary (same as the Math- lane) + +- `formalization_status` in `manifest.json` is **`proved`**: proof text is + supplied and bound by hash. The manifest cannot say `kernel-checked`; the gate + refuses a manifest that self-awards execution. +- **`kernel-checked`** appears only in the receipt written by a trusted + `--run-lean` execution (`formal/.lake/formal-evidence/receipt.json`), which + records the checked Git commit, Lean version, manifest digest, per-target + transitive axioms (all `[]` here), log hashes, and negative-control outcomes. + A receipt supplied by a caller is untrusted until matched to the actual + workflow run and commit. +- `alignment_status` is **`PENDING_INDEPENDENT_REVIEW`**. The author is + Anthropic / Claude via a Cursor cloud agent (2026-09-27); an alignment record + from the same provider, family or agent is refused by the validator. The + manifest cannot say `ACCEPTED`. +- In the ladder of [#95](https://github.com/d6g8k5htny-coder/main/issues/95) + (L0 prose … L5 proof-assistant-checked, `verification_level` separate from + scientific status) a target with a trusted `kernel-checked` receipt is L5 + evidence for exactly that target. +- None of these labels is a Layer 0 ACCEPT/AMEND verdict or moves one. + +## Run it + +Toolchain (once, ~200 MB, no Mathlib cache needed): + +```sh +curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none +export PATH="$HOME/.elan/bin:$PATH" +``` + +From the repository root: + +```sh +python3 tools/formal_gate_check.py # source-only: hashes, inventory, anchors, no Lean run +python3 tools/formal_gate_check.py --run-lean # fresh build, leanchecker, axiom audit, controls, receipt +python3 -B -S -m unittest tests.test_formal_gate -v +``` + +The source-only gate prints `SOURCE_IDENTITY_PASS (not a Lean build or +scientific acceptance): `. `--run-lean` removes `.lake/build`, +runs `lake build`, `leanchecker` on every module, a transitive `#print axioms` +audit restricted to `propext` / `Classical.choice` / `Quot.sound`, an +elaborated-type capture, and the executable negative controls: seven +tightened-or-wrong statements written into a scratch copy of the Lean text +(each must be rejected by Lean), plus `sorry`, an indirectly imported custom +axiom, and `native_decide` (each must be rejected by the axiom gate). It then +re-runs the source check to confirm the manifest digest did not move, and only +then writes the receipt. Locally the whole run takes about five seconds. + +Maintenance (these write): `--refresh-hashes` after editing any bound file, +then `--write-alignment` after editing targets, then the gate again. + +The gate fails closed on: hash mismatch; an unregistered `.lean` file or any +unbound file inside `formal/`; a bound file that does not exist; a control or +scope file missing from the bound set; toolchain or dependency-lock drift; +`sorry`, `native_decide` or an `axiom` declaration outside comments; a root +module that imports anything but the registered modules; a target inventory +that differs from the theorem names actually declared (in module order); a +pinned source whose local bytes changed or whose repository is not one of the +project's public repositories; an anchor that is not a verbatim substring; a +missing `does_not_claim`; a stale `ALIGNMENT.md`; a manifest with duplicate JSON +keys. + +## Why core Lean and not Mathlib here + +Everything the arithmetic skeleton needs is `Nat`/`Int` and `decide`, which the +kernel evaluates with GMP-backed literals in well under a second. That keeps +this package's CI cost at seconds with no multi-gigabyte cache. The Math- pilot +already carries the Mathlib dependency (revision +`d13f23b723b8a846827a245b89c10fc7d3f11612`, same Lean `v4.34.1`); any statement +here that needs `ℝ`, `Real.Gamma`, `Real.exp`, `Real.pi`, Gaussian measures or +matrices — the coefficient definition `c_{d,ref}`, the enclosure itself, the +P15 constant `ρ*` — belongs in that Mathlib lane, not in a second dependency +tree. See the rollout record for the coordination items. + +## Coordination + +Find current tasks in [main #275](https://github.com/d6g8k5htny-coder/main/issues/275) and coordinate with +other contributors on [main #307](https://github.com/d6g8k5htny-coder/main/issues/307). +The pickup itself belongs in the relevant current pull request or work discussion. + +- [docs/FORMAL_VERIFICATION.md](../docs/FORMAL_VERIFICATION.md) — lane contract + and the historical work-offer table, not current assignments. +- [docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md](../docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md) + — what this package adds, how it converged onto the Math- contract, what is + asked of other repositories and agents, and this session's capability limits. + This dated record preserves the original rollout; its pickup routing is + superseded by the current workflow linked below. +- [Work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) — historical + formal-ladder work item. Record actual pickup of alignment review or of the remaining + "Numerical formalizer" steps in the relevant current pull request or work + discussion under the [current workflow](../governance/OP-WORKFLOW-20260930.md). + +## What this package does not do + +It does not change `STATUS.md`, `PROOF_INDEX.md`, `LANDING_CLAIMS` or any +ACCEPT/AMEND outcome. It does not turn a hash match, a green build or a +kernel-checked lemma into acceptance of the theorem built on it. It does not +verify `coefficient.py`. It does not make AI-authored Lean text independent; +the author label stays until a distinct reviewer's record validates. It is not +a second scientific-status database and adds no status vocabulary beyond the +lane's. diff --git a/tests/fixtures/atlas_formal_build_3b39/REVIEW_LANE.md.txt b/tests/fixtures/atlas_formal_build_3b39/REVIEW_LANE.md.txt new file mode 100644 index 000000000..a4796b066 --- /dev/null +++ b/tests/fixtures/atlas_formal_build_3b39/REVIEW_LANE.md.txt @@ -0,0 +1,94 @@ +# Independent statement-alignment review (this package) + +The Lean kernel checks that a proof establishes its statement. It cannot check +that the statement is the one the informal text makes. That is an independent +review task with its own lane, distinct from Layer 0 analytic review and from +the author-side act of writing the Lean text. The contract is the lane's +([formal-verification guide](../docs/FORMAL_VERIFICATION.md), "Gate and trust +boundary") and is restated for this package in +[SCOPE.md § Review contract](SCOPE.md#review-contract). + +## Who may review + +Anyone whose provider, family **and** agent all differ from the author's +(`Anthropic` / `Claude` / Cursor cloud agent, 2026-09-27). The validator refuses +a record where any of the three coincides, case-insensitively. Same-provider +reviewers earn zero organizational-independence credit whatever they write; +this is the repository's existing rule and it applies to Lean text as to prose. + +## What the reviewer does + +Read the exact current head first; a changed source, scope, toolchain or +manifest stales any earlier record. Then, for each of the 31 targets in +`manifest.json`: + +1. Locate the `informal_anchor` in the pinned local source copy under + `sources/side24_v1/` and read its context. +2. Read the Lean **statement** (not the proof) and its docstring. Decide + whether it is the informal statement at the scope stated in `SCOPE.md`: + same constants, same quantifiers, same direction of inequality, same + scaling. Most targets are cross-multiplied integer forms of rational + identities; check the cross-multiplication. +3. Read `does_not_claim` and the "Not established" column of `SCOPE.md`. + Confirm the Lean statement does not silently claim more than the anchor and + that what it omits is named. +4. Record a per-target verdict: `ALIGNED`, `ALIGNED AT NARROWER SCOPE` (say + what is narrower) or `MISALIGNED` (say exactly how). Do not grade the proof + (the kernel did) and do not grade the Layer 0 mathematics (different lane). + +The reviewer need not run Lean, but should quote the gate output at the +reviewed commit (`SOURCE_IDENTITY_PASS … ` and, if available, +the workflow run that produced the receipt). + +## What the reviewer records + +Two files under `reviews/`, named `_.md` and `.json`: + +- **Markdown**: reviewer identity and provider; **source exposure** (whether the + Lean proof text or docstrings were read before forming a view of each + statement — reading the proof first is the weakest form and must be stated); + the reviewed commit, manifest digest and scope digest; one row per target + with the verdict. +- **JSON**: copy [`reviews/TEMPLATE_alignment_review.json`](reviews/TEMPLATE_alignment_review.json) + and fill it in. `disposition` is `ACCEPTED` only if **every** target is + `ALIGNED` or `ALIGNED AT NARROWER SCOPE` with the narrowing recorded; + otherwise leave the record unaccepted — the validator refuses it, which is + the intended outcome. `manifest_sha256` is the SHA-256 of + `formal/manifest.json` at the reviewed commit; `scope_sha256` is the hash of + `formal/SCOPE.md` recorded in the manifest's `files`. `targets` is exactly + the 31 manifest target names. `evidence` points to the committed Markdown + record by repository, 40-character commit, path and SHA-256. + +Validate: `python3 tools/formal_gate_check.py --alignment formal/reviews/.json`. +The validator checks structure, digests, coverage and lineage independence. It +does not authenticate that the review happened; a controller has to retrieve +the referenced evidence at the referenced commit. + +A `MISALIGNED` verdict is corrected at the source: fix the Lean statement (new +hash, new `--run-lean` receipt) or fix the anchor, then re-review. + +## What this lane cannot do + +- Promote a Layer 0 status. `STATUS.md` and `PROOF_INDEX.md` move only through + their own source-bound review. +- Make an author-side proof independent by relabelling; independence is + recorded from the reviewer's actual identity and lineage. +- Substitute for formalising the analytic content. An aligned arithmetic lemma + remains an arithmetic lemma. +- Flip `alignment_status` in `manifest.json`. That field stays + `PENDING_INDEPENDENT_REVIEW`; the accepted record is the evidence, and a + controller consumes it. + +## Current state + +All 31 targets: authored by Anthropic / Claude via a Cursor cloud agent on +2026-09-27; `proved` at source; `kernel-checked` only in the receipt of a +trusted run; alignment `PENDING_INDEPENDENT_REVIEW`. No record other than the +template exists. Record actual pickup in the relevant current pull request or work +discussion under the [current workflow](../governance/OP-WORKFLOW-20260930.md) so two +reviewers do not duplicate the work. Find current tasks in +[main #275](https://github.com/d6g8k5htny-coder/main/issues/275) and coordinate with other contributors on +[main #307](https://github.com/d6g8k5htny-coder/main/issues/307). +Closed +[work item #95](https://github.com/d6g8k5htny-coder/main/issues/95) remains the +historical formal-ladder work item. diff --git a/tests/fixtures/atlas_formal_build_3b39/formal_gate_check.py.txt b/tests/fixtures/atlas_formal_build_3b39/formal_gate_check.py.txt new file mode 100644 index 000000000..b057225d3 --- /dev/null +++ b/tests/fixtures/atlas_formal_build_3b39/formal_gate_check.py.txt @@ -0,0 +1,391 @@ +#!/usr/bin/env python3 +"""Source-bound Lean evidence gate for the main-side formal package (stdlib only). + +Follows the contract of the Math- formal lane (docs/FORMAL_VERIFICATION.md, +work item #95): a manifest is an evidence sidecar, not a scientific register. + +Default (source-only, no Lean run): the manifest is well formed and cannot +self-award execution or review; every bound file matches its SHA-256; every +Lean module is registered; no `sorry`, `native_decide` or `axiom` appears +outside comments; the root module imports exactly the registered modules; the +target inventory equals the theorem declarations found in those modules; every +pinned informal source has a local byte copy with the recorded size and hash; +every target's informal anchor is a verbatim substring of its source. + +`--run-lean`: additionally performs a fresh build of the pinned package, runs a +transitive `#print axioms` audit restricted to propext / Classical.choice / +Quot.sound, captures elaborated types, executes real negative controls +(tightened inequalities, a wrong constant, `sorry`, an indirect custom axiom, +`native_decide`) and writes logs plus a receipt under `.lake/formal-evidence/`. +Only that receipt carries `kernel-checked`; the committed manifest says +`proved`. A receipt from arbitrary input is untrusted until matched to the +actual workflow run and checked Git commit. + +`--axioms-output FILE`: audit a captured `#print axioms` output without running +Lean (for tests and split CI steps). + +`--alignment REVIEW.json`: validate an independently authored alignment record +against the current manifest and scope digests. This checks structure, +identity, coverage and lineage independence; it does not authenticate that the +review happened and never promotes scientific status. + +Nothing here edits STATUS.md, PROOF_INDEX.md or any review verdict. +""" +from __future__ import annotations + +import argparse +import hashlib +import json +import os +from pathlib import Path, PurePosixPath +import re +import shutil +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[1] +MANIFEST = "formal/manifest.json" +ALLOWED = frozenset({"propext", "Classical.choice", "Quot.sound"}) +NAME = r"[A-Za-z_][A-Za-z0-9_.']*" +AXIOM_LINE = re.compile(r"'(" + NAME + r")' (?:depends on axioms: \[([^\]]*)\]|does not depend on any axioms)") +HEX40 = re.compile(r"[0-9a-f]{40}") +HEX64 = re.compile(r"[0-9a-f]{64}") +PUBLIC_REPOS = {"d6g8k5htny-coder/main", "d6g8k5htny-coder/Math-", "d6g8k5htny-coder/query-", + "d6g8k5htny-coder/meta-framework", "d6g8k5htny-coder/Universal-Law-Workspace"} +THEOREM = re.compile(r"^(?:theorem|lemma)\s+(" + NAME + r")", re.M) +NAMESPACE = re.compile(r"^namespace\s+(\S+)", re.M) +TOOLCHAIN = "leanprover/lean4:v4.34.1" +BUILD_DIR = ".lake" + + +def sha(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_json(text: str): + def unique(pairs): + obj = {} + for key, value in pairs: + require(key not in obj, "duplicate JSON key: " + key) + obj[key] = value + return obj + return json.loads(text, object_pairs_hook=unique) + + +def safe_path(root: Path, relative) -> Path: + require(isinstance(relative, str) and relative and "\\" not in relative, f"invalid path: {relative!r}") + pure = PurePosixPath(relative) + require(not pure.is_absolute() and ".." not in pure.parts and str(pure) == relative, f"unsafe path: {relative}") + path = root + for part in pure.parts: + path = path / part + require(not path.is_symlink(), f"symlink refused: {relative}") + require(path.is_file() and path.resolve().is_relative_to(root.resolve()), f"missing or escaping file: {relative}") + return path + + +def strip_lean_comments(text: str) -> str: + """Remove `--` line comments and nested `/- -/` block comments. Comment text + cannot smuggle a proof term; the kernel audit of `sorryAx` is authoritative.""" + out, i, depth, n = [], 0, 0, len(text) + while i < n: + two = text[i:i + 2] + if depth: + if two == "/-": + depth, i = depth + 1, i + 2 + elif two == "-/": + depth, i = depth - 1, i + 2 + else: + out.append("\n" if text[i] == "\n" else " ") + i += 1 + elif two == "/-": + depth, i = 1, i + 2 + elif two == "--": + end = text.find("\n", i) + i = n if end < 0 else end + else: + out.append(text[i]) + i += 1 + return "".join(out) + + +def audit_axioms(text: str, targets: list) -> dict: + require(isinstance(targets, list) and targets and len(set(targets)) == len(targets), "empty or duplicate target list") + records = {} + for match in AXIOM_LINE.finditer(text): + name, raw = match.groups() + require(name in targets and name not in records, "unexpected or duplicate axiom target: " + name) + axioms = [] if raw is None or not raw.strip() else [a.strip() for a in raw.split(",")] + require(all(re.fullmatch(NAME, a) for a in axioms), "malformed axiom name") + require(set(axioms) <= ALLOWED, "forbidden transitive axiom: " + repr(sorted(set(axioms) - ALLOWED))) + records[name] = sorted(set(axioms)) + require(not AXIOM_LINE.sub("", text).strip(), "unrecognized audit output") + require(set(records) == set(targets), "missing target axiom report") + return records + + +def source_check(root: Path, manifest_rel: str = MANIFEST) -> tuple[dict, str, Path]: + root = root.resolve() + raw = safe_path(root, manifest_rel).read_bytes() + m = load_json(raw.decode("utf-8")) + require(m.get("schema_version") == 1 and m.get("scientific_effect") == "NONE", "invalid evidence schema") + require(m.get("scientific_status_authority") is False, "manifest must declare scientific_status_authority false") + require(m.get("formalization_status") == "proved" and m.get("alignment_status") == "PENDING_INDEPENDENT_REVIEW", + "source metadata cannot self-award execution or review") + for key in ("package", "package_root", "root_module", "lean_toolchain"): + require(isinstance(m.get(key), str) and m[key].strip(), key + " must be a nonempty string") + require(m["lean_toolchain"] == TOOLCHAIN, "unsupported Lean toolchain in manifest") + pkg_rel = m["package_root"] + pkg = root / pkg_rel + require(pkg.is_dir() and not pkg.is_symlink(), "package root missing") + files = m.get("files") + require(isinstance(files, dict) and files, "empty file manifest") + for name, digest in files.items(): + require(isinstance(digest, str) and HEX64.fullmatch(digest), "invalid source hash: " + name) + require(sha(safe_path(root, name).read_bytes()) == digest, "source hash mismatch: " + name) + required = {f"{pkg_rel}/lean-toolchain", f"{pkg_rel}/lakefile.toml", f"{pkg_rel}/lake-manifest.json", + f"{pkg_rel}/{m['root_module']}.lean", f"{pkg_rel}/SCOPE.md", f"{pkg_rel}/GLOSSARY.md", + f"{pkg_rel}/README.md", "tools/formal_gate_check.py", "tests/test_formal_gate.py"} + require(required <= set(files), "unbound control or scope file: " + repr(sorted(required - set(files)))) + require((pkg / "lean-toolchain").read_text(encoding="utf-8").strip() == TOOLCHAIN, "wrong Lean toolchain file") + lock = load_json((pkg / "lake-manifest.json").read_text(encoding="utf-8")) + packages = lock.get("packages", []) + require(isinstance(packages, list), "invalid lake manifest") + actual = {p["name"]: p["rev"] for p in packages} + require(len(actual) == len(packages), "duplicate dependency") + require(actual == m.get("dependency_revisions"), "dependency lock mismatch") + require(all(HEX40.fullmatch(v) for v in actual.values()), "unpinned dependency") + modules = m.get("source_modules") + require(isinstance(modules, list) and modules and len(set(modules)) == len(modules), "invalid source module list") + expected_root = "".join("import " + path[:-5].replace("/", ".") + "\n" for path in modules) + root_text = strip_lean_comments((pkg / (m["root_module"] + ".lean")).read_text(encoding="utf-8")) + require("".join(line + "\n" for line in root_text.splitlines() if line.strip()) == expected_root, + "root must only import registered modules") + names = [] + for path in modules: + require(f"{pkg_rel}/{path}" in files and path.endswith(".lean"), "unbound source module: " + path) + text = strip_lean_comments((pkg / path).read_text(encoding="utf-8")) + require(not re.search(r"\bsorry\b", text), "sorry in " + path) + require(not re.search(r"\bnative_decide\b", text), "native_decide in " + path) + require(not re.search(r"^\s*axiom\b", text, re.M), "custom axiom declaration in " + path) + namespaces = NAMESPACE.findall(text) + require(len(namespaces) == 1, "each module must open exactly one namespace: " + path) + names.extend(namespaces[0] + "." + n for n in THEOREM.findall(text)) + targets = m.get("targets") + require(isinstance(targets, list) and targets, "empty target list") + target_names = [] + sources = {s["id"]: s for s in m.get("sources", [])} if isinstance(m.get("sources"), list) else None + require(isinstance(sources, dict) and sources, "sources must be a nonempty list") + source_text = {} + for s in m["sources"]: + require(set(s) == {"id", "repository", "commit", "path", "bytes", "sha256", "local_copy"}, "source rows have a fixed schema") + require(s["repository"] in PUBLIC_REPOS, "nonpublic source repository refused: " + str(s["repository"])) + require(isinstance(s["commit"], str) and HEX40.fullmatch(s["commit"]), "invalid commit for " + s["id"]) + require(isinstance(s["sha256"], str) and HEX64.fullmatch(s["sha256"]), "invalid sha256 for " + s["id"]) + require(type(s["bytes"]) is int and s["bytes"] > 0, "invalid byte count for " + s["id"]) + payload = safe_path(root, s["local_copy"]).read_bytes() + require(len(payload) == s["bytes"] and sha(payload) == s["sha256"], "local copy differs from pinned bytes: " + s["id"]) + require(s["local_copy"] in files, "pinned source copy not bound in files: " + s["local_copy"]) + source_text[s["id"]] = payload.decode("utf-8") + for t in targets: + require(isinstance(t, dict) and set(t) == {"name", "module", "title", "source", "informal_anchor", "does_not_claim"}, + "target rows have a fixed schema") + require(isinstance(t["name"], str) and re.fullmatch(NAME, t["name"]), "invalid target name") + require(t["module"] in modules, "target module not registered: " + t["name"]) + for key in ("title", "does_not_claim"): + require(isinstance(t[key], str) and t[key].strip(), f"{t['name']}: {key} must be nonempty") + require(t["source"] in source_text, f"{t['name']}: unknown source") + require(isinstance(t["informal_anchor"], str) and t["informal_anchor"].strip(), f"{t['name']}: empty informal anchor") + require(t["informal_anchor"] in source_text[t["source"]], f"{t['name']}: informal anchor is not a verbatim substring of its source") + target_names.append(t["name"]) + require(target_names == names, "target inventory differs from source declarations") + lean_files = {p.relative_to(pkg).as_posix() for p in pkg.rglob("*.lean") if BUILD_DIR not in p.relative_to(pkg).parts} + require(lean_files == set(modules) | {m["root_module"] + ".lean"}, "unregistered Lean module: " + repr(sorted(lean_files - set(modules) - {m['root_module'] + '.lean'}))) + for p in pkg.rglob("*"): + rel = p.relative_to(root).as_posix() + if p.is_file() and BUILD_DIR not in p.relative_to(pkg).parts and rel not in files: + require(rel in set(m.get("unbound_files", [])), "file in package not bound or declared unbound: " + rel) + return m, sha(raw), pkg + + +def lake_binary() -> str | None: + found = shutil.which("lake") + if found: + return found + candidate = Path.home() / ".elan/bin/lake" + return str(candidate) if candidate.is_file() else None + + +def run(command, label, out: Path, cwd: Path, env, expect_success=True): + result = subprocess.run(command, cwd=cwd, text=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, timeout=900, env=env) + (out / (label + ".log")).write_text(result.stdout, encoding="utf-8") + print(label + ": exit " + str(result.returncode), flush=True) + require((result.returncode == 0) == expect_success, "unexpected process outcome: " + label + "\n" + result.stdout[-6000:]) + return result.stdout + + +def negative_controls(m: dict, pkg: Path) -> dict: + """Real mutation controls: each must be rejected by Lean or by the axiom gate.""" + root_import = "import " + m["root_module"] + "\n" + cases = {} + for label, spec in m.get("negative_controls", {}).items(): + module_text = (pkg / spec["module"]).read_text(encoding="utf-8") + require(spec["replace"] in module_text, "negative control text not found: " + label) + cases[label] = (module_text.replace(spec["replace"], spec["with"]), False, None) + cases["sorry"] = (root_import + "theorem injected : False := by sorry\n#print axioms injected\n", True, "injected") + cases["custom_imported"] = (root_import + "axiom hiddenPremise : False\ntheorem middle : False := hiddenPremise\n" + "theorem injected : False := middle\n#print axioms injected\n", True, "injected") + cases["native"] = (root_import + "theorem injected : (2 : Nat) + 2 = 4 := by native_decide\n#print axioms injected\n", True, "injected") + return cases + + +def execute(m: dict, digest: str, pkg: Path, root: Path) -> dict: + lake = lake_binary() + require(lake is not None, "lake not found on PATH or in ~/.elan/bin") + env = dict(os.environ, PATH=f"{Path(lake).parent}{os.pathsep}{os.environ.get('PATH', '')}") + out = pkg / BUILD_DIR / "formal-evidence" + out.mkdir(parents=True, exist_ok=True) + require(not (pkg / BUILD_DIR).is_symlink() and not (pkg / BUILD_DIR / "build").is_symlink(), "symlink build directory") + if (pkg / BUILD_DIR / "build").exists(): + shutil.rmtree(pkg / BUILD_DIR / "build") + targets = [t["name"] for t in m["targets"]] + run([lake, "build"], "build", out, pkg, env) + run([lake, "env", "leanchecker", m["root_module"]], "leanchecker", out, pkg, env) + audit = out / "Audit.lean" + audit.write_text("import " + m["root_module"] + "\n" + "\n".join("#print axioms " + n for n in targets) + "\n", encoding="utf-8") + axioms = audit_axioms(run([lake, "env", "lean", str(audit)], "axioms", out, pkg, env), targets) + types = out / "Types.lean" + types.write_text("import " + m["root_module"] + "\nset_option pp.explicit true\n" + "\n".join("#check " + n for n in targets) + "\n", encoding="utf-8") + run([lake, "env", "lean", str(types)], "elaborated-types", out, pkg, env) + outcomes = {} + for label, (source, succeeds, target) in negative_controls(m, pkg).items(): + path = out / (label + ".lean") + path.write_text(source, encoding="utf-8") + log = run([lake, "env", "lean", str(path)], label, out, pkg, env, succeeds) + if target: + matches = list(AXIOM_LINE.finditer(log)) + require(matches, "negative control missing axiom report: " + label) + try: + audit_axioms("\n".join(x.group() for x in matches), [target]) + except ValueError: + outcomes[label] = "REJECTED_BY_AXIOM_GATE" + else: + raise ValueError("negative control escaped: " + label) + else: + require("is false" in log or "unsolved goals" in log or "failed" in log, "negative control did not fail on its proof goal: " + label) + outcomes[label] = "REJECTED_BY_LEAN" + _, after, _ = source_check(root) + require(after == digest, "manifest changed during execution") + version = run([lake, "env", "lean", "--version"], "version", out, pkg, env).strip() + require("version 4.34.1" in version, "unexpected running Lean version") + head = subprocess.run(["git", "rev-parse", "HEAD"], cwd=root, text=True, capture_output=True).stdout.strip() + require(HEX40.fullmatch(head or ""), "missing exact checked commit") + receipt = dict(schema_version=1, scientific_effect="NONE", scientific_status_authority=False, + package=m["package"], formalization_status="kernel-checked", + alignment_status="PENDING_INDEPENDENT_REVIEW", manifest_sha256=digest, checked_commit=head, + repository=os.environ.get("GITHUB_REPOSITORY"), workflow_run_id=os.environ.get("GITHUB_RUN_ID"), + lean_version=version, dependency_revisions=m["dependency_revisions"], axioms=axioms, + negative_controls=outcomes) + receipt["logs"] = {p.name: sha(p.read_bytes()) for p in sorted(out.glob("*.log"))} + (out / "receipt.json").write_text(json.dumps(receipt, indent=2, sort_keys=True) + "\n", encoding="utf-8") + return receipt + + +def check_alignment(review: dict, manifest_digest: str, targets: list, scope_digest: str): + require(isinstance(review, dict), "review must be object") + require(review.get("disposition") == "ACCEPTED", "alignment not accepted") + require(review.get("manifest_sha256") == manifest_digest, "stale alignment manifest") + require(review.get("scope_sha256") == scope_digest, "stale alignment scope") + covered = review.get("targets", []) + require(isinstance(covered, list) and len(covered) == len(set(covered)) and set(covered) == set(targets), "partial or ambiguous review") + a, r = review.get("author", {}), review.get("reviewer", {}) + for key in ("provider", "family", "agent"): + require(isinstance(a.get(key), str) and a[key].strip() and isinstance(r.get(key), str) and r[key].strip(), "missing review lineage") + require(a[key].strip().casefold() != r[key].strip().casefold(), "lineage not independent: " + key) + e = review.get("evidence", {}) + require(isinstance(e.get("repository"), str) and re.fullmatch(r"[^/\s]+/[^/\s]+", e["repository"]), "missing evidence repo") + require(isinstance(e.get("commit"), str) and HEX40.fullmatch(e["commit"]), "mutable review ref") + require(isinstance(e.get("sha256"), str) and HEX64.fullmatch(e["sha256"]), "missing review hash") + require(isinstance(e.get("path"), str) and e["path"] and not PurePosixPath(e["path"]).is_absolute() + and ".." not in PurePosixPath(e["path"]).parts, "missing or unsafe review path") + + +def render_alignment(m: dict) -> str: + lines = ["# Informal–formal alignment table", "", + f"Generated from `{MANIFEST}` by `tools/formal_gate_check.py --write-alignment`; do not hand-edit.", + "Each row pairs one Lean target with the verbatim informal text it is attached to. The kernel checks the", + "declaration; the independent alignment review (see REVIEW_LANE.md) checks that the declaration says what", + "the anchor says. Source-level formalization status of every row is `proved`; only a trusted run receipt", + "reports `kernel-checked`. Nothing here is a Layer 0 review outcome.", "", + "| Lean target | Title | Informal anchor | Source | Does not claim |", "|---|---|---|---|---|"] + for t in m["targets"]: + anchor = "`" + " ".join(t["informal_anchor"].split()).replace("`", "'").replace("|", "\\|") + "`" + cells = [f"`{t['name']}`", t["title"].replace("|", "\\|"), anchor, t["source"], t["does_not_claim"].replace("|", "\\|")] + lines.append("| " + " | ".join(cells) + " |") + lines.append("") + return "\n".join(lines) + + +def refresh_hashes(root: Path, manifest_rel: str = MANIFEST) -> int: + path = safe_path(root, manifest_rel) + m = load_json(path.read_text(encoding="utf-8")) + changed = 0 + for name in list(m["files"]): + digest = sha(safe_path(root, name).read_bytes()) + if m["files"][name] != digest: + m["files"][name] = digest + changed += 1 + path.write_text(json.dumps(m, indent=2, ensure_ascii=False) + "\n", encoding="utf-8") + return changed + + +def main(argv=None) -> int: + p = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + p.add_argument("--root", type=Path, default=ROOT) + p.add_argument("--manifest", default=MANIFEST) + p.add_argument("--run-lean", action="store_true", help="fresh build, leanchecker, axiom audit, negative controls, receipt") + p.add_argument("--axioms-output", type=Path, help="audit a captured #print axioms output without running Lean") + p.add_argument("--alignment", type=Path, help="validate an independently authored alignment record; never promotes science") + p.add_argument("--alignment-table", default="formal/ALIGNMENT.md", help="generated table to compare against the manifest") + p.add_argument("--write-alignment", action="store_true", help="regenerate the alignment table and exit") + p.add_argument("--refresh-hashes", action="store_true", help="rewrite manifest file hashes from disk and exit") + args = p.parse_args(argv) + root = args.root.resolve() + try: + if args.refresh_hashes: + print(f"updated {refresh_hashes(root, args.manifest)} file hashes in {args.manifest}") + return 0 + m, digest, pkg = source_check(root, args.manifest) + if args.write_alignment: + (root / args.alignment_table).write_text(render_alignment(m), encoding="utf-8") + print("wrote " + args.alignment_table) + return 0 + require(safe_path(root, args.alignment_table).read_text(encoding="utf-8") == render_alignment(m), + "alignment table differs from the manifest rendering; regenerate with --write-alignment") + if args.alignment: + check_alignment(load_json(args.alignment.read_text(encoding="utf-8")), digest, + [t["name"] for t in m["targets"]], m["files"][f"{m['package_root']}/SCOPE.md"]) + print("ALIGNMENT_RECORD_STRUCTURE_PASS (identity, coverage and lineage only; the review itself must be retrieved and authenticated)") + if args.axioms_output: + axioms = audit_axioms(args.axioms_output.read_text(encoding="utf-8"), [t["name"] for t in m["targets"]]) + print(json.dumps({"axiom_audit": axioms, "manifest_sha256": digest}, indent=2, sort_keys=True)) + if args.run_lean: + print(json.dumps(execute(m, digest, pkg, root), indent=2, sort_keys=True)) + elif not args.axioms_output: + print("SOURCE_IDENTITY_PASS (not a Lean build or scientific acceptance): " + digest) + print(json.dumps({"package": m["package"], "targets": len(m["targets"]), "sources": len(m["sources"]), + "formalization_status": m["formalization_status"], "alignment_status": m["alignment_status"]}, + sort_keys=True)) + except (ValueError, KeyError, TypeError, OSError, UnicodeDecodeError, subprocess.SubprocessError) as e: + print("FORMAL_GATE_FAIL: " + str(e), file=sys.stderr) + return 1 + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tests/fixtures/atlas_formal_build_3b39/manifest.json b/tests/fixtures/atlas_formal_build_3b39/manifest.json new file mode 100644 index 000000000..0d694d705 --- /dev/null +++ b/tests/fixtures/atlas_formal_build_3b39/manifest.json @@ -0,0 +1,365 @@ +{ + "schema_version": 1, + "scientific_effect": "NONE", + "scientific_status_authority": false, + "package": "side24-arithmetic-skeleton", + "package_root": "formal", + "root_module": "UniversalLaw", + "formalization_status": "proved", + "alignment_status": "PENDING_INDEPENDENT_REVIEW", + "meaning": "Evidence sidecar for the main-side Lean package, following the Math- formal lane contract (docs/FORMAL_VERIFICATION.md; historical formal-ladder work item #95, retained in coordination.work_item as provenance rather than current pickup routing). `proved` here means proof text supplied and bound by hash; `kernel-checked` is reported only by the receipt of a trusted --run-lean execution at an exact commit. Alignment is a separate pending/accepted/stale dimension. Nothing in this file is a scientific register entry or changes any ACCEPT/AMEND disposition.", + "coordination": { + "guide": "docs/FORMAL_VERIFICATION.md", + "work_item": "https://github.com/d6g8k5htny-coder/main/issues/95", + "math_pilot": "https://github.com/d6g8k5htny-coder/Math-/tree/cc2989c1280f4f227d0c6aa30c8841d6ba01e46e/formal", + "rollout_record": "docs/FORMAL_VERIFICATION_ROLLOUT_20260927.md", + "work_offer_addressed": "Numerical formalizer, first step only: the exact arithmetic skeleton of the SIDE24 note. The coefficient definition and the proof-producing enclosure pipeline are NOT supplied." + }, + "author": { + "provider": "Anthropic", + "family": "Claude", + "agent": "Cursor cloud agent, 2026-09-27" + }, + "lean_toolchain": "leanprover/lean4:v4.34.1", + "dependency_revisions": {}, + "allowed_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ], + "files": { + "formal/lean-toolchain": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", + "formal/lakefile.toml": "58f0fa6864cc03e9bcbef2d8c0404e9f3385a30a6124000454319367906cbe4a", + "formal/lake-manifest.json": "562d38ad95598486b2b592e6d072d5d3212735bfeb1cb6d8eb8ec04492522ba2", + "formal/UniversalLaw.lean": "cb94ad3490a00bc35b420a53a42ff65b6fc66a46b8a26ef1b87035d7bb15587e", + "formal/UniversalLaw/Side24/Ledger.lean": "ae4a14f3db8cf26668e55e2d2f80e0dcecb0703826b40396d91fb6e0d266d3f7", + "formal/UniversalLaw/Side24/ConeMoments.lean": "2bcd4a83683188856bce010c3dcdec6904e45a6d73b50b9f3891e632ff58985c", + "formal/UniversalLaw/Side24/Endpoints.lean": "095102245297707316cfd7e244d5509f9b102fe5aa638b7acdbbcf9d3c9d52bd", + "formal/sources/side24_v1/PROOF.md": "c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769", + "formal/sources/side24_v1/ENCLOSURE.json": "72b6cd92d31394cdaf5da8919a5d548e902228af1f095cc184158a71d8287811", + "formal/SCOPE.md": "fd06700628b1fbc81c5cfe3786aaa455032375bcb879914f068a66b726802a17", + "formal/GLOSSARY.md": "342d4efb374fea31c39e51f8f6bcdbc50d7fb5fea1fd393eda21afff92c62fb8", + "formal/README.md": "54436dfd808547d9da9ce0a2ad64b0e5935bb755844fef99b298281c49044aaa", + "formal/REVIEW_LANE.md": "887f56209471fc0194d601a4f8a0c82eb75852e1c97da0400c16d447669e6340", + "formal/reviews/TEMPLATE_alignment_review.json": "e722e928ca43c16981e063d8eb1c91e9bf8c683241d9dcf156400a419e72feb3", + "formal/reviews/README.md": "333ca71e7c676cee89e5d01cd61999c21bb0584e41d6bdacb18afa410109f95d", + "tools/formal_gate_check.py": "21c355e02ac6e01337d10465a3105b34b93f832586ee60aa2430f662a90cd8b7", + "tests/test_formal_gate.py": "4286136d8b24eca9b26d1e7b12933bed5b0961809b362a60c3af7bf46e6ed4b6" + }, + "unbound_files": [ + "formal/manifest.json", + "formal/ALIGNMENT.md" + ], + "sources": [ + { + "id": "side24-proof", + "repository": "d6g8k5htny-coder/Math-", + "commit": "9d7b6802424fb4715b31999066aafca8ee2f3cca", + "path": "coefficients/side24_v1/PROOF.md", + "bytes": 10272, + "sha256": "c06daccc4ba4b9168522b9888b76a7d599934fc3b91bd753ee5d492262917769", + "local_copy": "formal/sources/side24_v1/PROOF.md" + }, + { + "id": "side24-enclosure", + "repository": "d6g8k5htny-coder/Math-", + "commit": "9d7b6802424fb4715b31999066aafca8ee2f3cca", + "path": "coefficients/side24_v1/ENCLOSURE.json", + "bytes": 1090, + "sha256": "72b6cd92d31394cdaf5da8919a5d548e902228af1f095cc184158a71d8287811", + "local_copy": "formal/sources/side24_v1/ENCLOSURE.json" + } + ], + "source_modules": [ + "UniversalLaw/Side24/Ledger.lean", + "UniversalLaw/Side24/ConeMoments.lean", + "UniversalLaw/Side24/Endpoints.lean" + ], + "targets": [ + { + "name": "UniversalLaw.Side24.pairing_sum_six", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Product-rule pairing count at q=6 equals 76", + "source": "side24-proof", + "informal_anchor": "The coefficient sum for q=6 is\n1+15+45+15=76", + "does_not_claim": "the derivative bound 76|x|^6 e^(-|x|^2/2) itself" + }, + { + "name": "UniversalLaw.Side24.pairing_sum_le_six", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Pairing counts for q<=6 are at most 76", + "source": "side24-proof", + "informal_anchor": "it bounds the smaller orders as well", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem" + }, + { + "name": "UniversalLaw.Side24.pairing_terms_six", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Individual pairing terms 1, 15, 45, 15", + "source": "side24-proof", + "informal_anchor": "1+15+45+15=76", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem" + }, + { + "name": "UniversalLaw.Side24.sixth_moment_double_factorial", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Double factorial 5!! = 15", + "source": "side24-proof", + "informal_anchor": "At zero, every such\ncontraction has absolute value at most15.", + "does_not_claim": "that Gaussian derivative contractions at zero are bounded by 15" + }, + { + "name": "UniversalLaw.Side24.lattice_shell_constant", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Shell constants 27·27 = 729 and 729·2 = 1458", + "source": "side24-proof", + "informal_anchor": "<=729 sum_{j>=1} j^9 e^(-288j^2)\n <=1458 e^(-288).", + "does_not_claim": "the lattice-point count or the geometric tail sum" + }, + { + "name": "UniversalLaw.Side24.geometric_ratio_constants", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Ratio constants 2^9 = 512 and 288·3 = 864", + "source": "side24-proof", + "informal_anchor": "successive terms have ratio at most512e^(-864)<1/2", + "does_not_claim": "that the ratio is below 1/2" + }, + { + "name": "UniversalLaw.Side24.period_exponent", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Period-24 exponent 24^2/2 = 288", + "source": "side24-proof", + "informal_anchor": "sum_{n!=0} |n|^6 e^(-288|n|^2)", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem" + }, + { + "name": "UniversalLaw.Side24.image_constant_value", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Image constant 1458·(76·24^6+15) = 21175738586478", + "source": "side24-proof", + "informal_anchor": "E := 1458*(76*24^6+15)*10^(-125)\n = 21175738586478 *10^(-125).", + "does_not_claim": "the inequality |D^q K_24(0)-D^q K_infty(0)| < E" + }, + { + "name": "UniversalLaw.Side24.exp_taylor_partial_sum_gt_ten", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Degree-20 Taylor partial sum of exp(288/125) exceeds 10", + "source": "side24-proof", + "informal_anchor": "The code proves e^(288/125)>10 using the positive rational Taylor sum through20", + "does_not_claim": "that the partial sum is below exp(288/125) (positivity of the omitted terms is analysis)" + }, + { + "name": "UniversalLaw.Side24.covariance_relative_bound", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "60E < 10^(-108) as the integer inequality 60·21175738586478 < 10^17", + "source": "side24-proof", + "informal_anchor": "epsilon=10^(-108), since60E= I/3" + }, + { + "name": "UniversalLaw.Side24.odd_block_eigenvalues", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Odd block trace 16 and determinant 6 = 8^2 - 58", + "source": "side24-proof", + "informal_anchor": "[[1,-3],[-3,15]], whose eigenvalues are8 +/- sqrt(58)", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem" + }, + { + "name": "UniversalLaw.Side24.odd_block_shifted_minors", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Shifted odd block minors 2/3 and 7/9 (scaled by 3: 2 and 7)", + "source": "side24-proof", + "informal_anchor": "subtract I/3 and use first principal minor2/3 and determinant7/9", + "does_not_claim": "Sylvester's criterion" + }, + { + "name": "UniversalLaw.Side24.smaller_eigenvalue_exceeds_third", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "8 - sqrt(58) > 1/3 via 23^2 > 58·9", + "source": "side24-proof", + "informal_anchor": "Its smaller eigenvalue exceeds\n1/3", + "does_not_claim": "monotonicity of the square root" + }, + { + "name": "UniversalLaw.Side24.exponent_bounds", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Exponent inequalities a+2b<14 and 2a+b<13 for d=2,3 (in sixths)", + "source": "side24-proof", + "informal_anchor": "For d=2,3, a+2b<14 and2a+b<13.", + "does_not_claim": "the log/exp estimates that follow" + }, + { + "name": "UniversalLaw.Side24.exponent_values", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "Exact a, b values for d=2,3", + "source": "side24-proof", + "informal_anchor": "a=m+2/3+n/2, b=d+n/2.", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem" + }, + { + "name": "UniversalLaw.Side24.ratio_constant_ordering", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "13 <= 32 and 28 <= 32", + "source": "side24-proof", + "informal_anchor": "ratio between1-13epsilon and\n1+28epsilon, hence safely between1-32epsilon and1+32epsilon", + "does_not_claim": "the elementary log/exp bounds" + }, + { + "name": "UniversalLaw.Side24.density_comparison_below_reported", + "module": "UniversalLaw/Side24/Ledger.lean", + "title": "32·10^(-108) < 10^(-106)", + "source": "side24-proof", + "informal_anchor": "|c_d,24/c_d,ref -1| < 10^(-106), d=2,3.", + "does_not_claim": "the multiplicative density comparison" + }, + { + "name": "UniversalLaw.Side24.conditional_third_derivative_variance", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "Conditional variance tau^2 = 15 - 9 = 6", + "source": "side24-proof", + "informal_anchor": "Var(t)=15, Cov(t,G)=(-3,0,...,0)", + "does_not_claim": "the Gaussian conditioning formula or the covariance derivatives" + }, + { + "name": "UniversalLaw.Side24.transverse_covariance_entries_thirds", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "Transverse covariance entries 8/3, 1, 2/3 from the delta formula", + "source": "side24-proof", + "informal_anchor": "Cov(A_ij,A_kl | V=0)\n = (2/3)delta_ij delta_kl + delta_ik delta_jl + delta_il delta_jk.", + "does_not_claim": "the delta formula itself" + }, + { + "name": "UniversalLaw.Side24.cone_moment_m1_thirds", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "D_1 = 4/3 is half of 8/3", + "source": "side24-proof", + "informal_anchor": "D_1=E[A^2 1{A<0}]=4/3.", + "does_not_claim": "centred Gaussian symmetry" + }, + { + "name": "UniversalLaw.Side24.trace_and_traceless_variances", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "Var(s) = 5/3, Var(x) = Var(y) = 1, Cov(s,x) = 0 from the 2x2 covariance entries", + "source": "side24-proof", + "informal_anchor": "Var(s)=5/3 and Var(x)=Var(y)=1.", + "does_not_claim": "independence beyond zero covariance, which is Gaussian" + }, + { + "name": "UniversalLaw.Side24.fourth_moment_of_trace", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "E s^4 = 3·(5/3)^2 = 25/3", + "source": "side24-proof", + "informal_anchor": "E s^2=5/3, E s^4=25/3", + "does_not_claim": "the Gaussian fourth-moment identity" + }, + { + "name": "UniversalLaw.Side24.exponential_moment_of_trace", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "1 + 5/3 = 8/3 behind E exp(-s^2/2) = sqrt(3/8)", + "source": "side24-proof", + "informal_anchor": "E exp(-s^2/2)=sqrt(3/8)", + "does_not_claim": "the Gaussian exponential-moment identity" + }, + { + "name": "UniversalLaw.Side24.cone_moment_m2_algebra", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "D_2 algebra: rational part 29/6 and 4·sqrt(3/8) = sqrt(6)", + "source": "side24-proof", + "informal_anchor": "D_2 = (1/2)[25/3-20/3+8-8sqrt(3/8)]\n = 29/6-sqrt(6).", + "does_not_claim": "the integral identity or the Rayleigh cone integration" + }, + { + "name": "UniversalLaw.Side24.cube_root_simplification", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "6^2·2 = 3·24 behind 6^(2/3)/24^(1/3) = (3/2)^(1/3)", + "source": "side24-proof", + "informal_anchor": "simplifying 6^(2/3)/24^(1/3)=(3/2)^(1/3)", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem" + }, + { + "name": "UniversalLaw.Side24.pin_determinant_and_joint_dimension", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "det diag(3,1,..,1) = 3 and joint dimensions 6, 10", + "source": "side24-proof", + "informal_anchor": "Its dimension is at most10.", + "does_not_claim": "the analytic statement the arithmetic is attached to; the coefficient bound; the parent theorem" + }, + { + "name": "UniversalLaw.Side24.hessian_block_eigenvalues", + "module": "UniversalLaw/Side24/ConeMoments.lean", + "title": "Hessian block eigenvalues 4, 5, 2 exceed 1/3", + "source": "side24-proof", + "informal_anchor": "The reference Hessian block has eigenvalues d+2 on trace and2 on traceless matrices", + "does_not_claim": "the spectral decomposition" + }, + { + "name": "UniversalLaw.Side24.d2_endpoints_adjacent", + "module": "UniversalLaw/Side24/Endpoints.lean", + "title": "Published d=2 endpoints are adjacent 20-digit decimals", + "source": "side24-enclosure", + "informal_anchor": "\"2\": {\n \"lower\": \"0.07340691930603427103\",\n \"upper\": \"0.07340691930603427104\"", + "does_not_claim": "that c_2,24 lies between them" + }, + { + "name": "UniversalLaw.Side24.d3_endpoints_adjacent", + "module": "UniversalLaw/Side24/Endpoints.lean", + "title": "Published d=3 endpoints are adjacent 20-digit decimals", + "source": "side24-enclosure", + "informal_anchor": "\"3\": {\n \"lower\": \"0.04177593184059834334\",\n \"upper\": \"0.04177593184059834335\"", + "does_not_claim": "that c_3,24 lies between them" + }, + { + "name": "UniversalLaw.Side24.d3_below_d2", + "module": "UniversalLaw/Side24/Endpoints.lean", + "title": "Published d=3 interval lies below the d=2 interval", + "source": "side24-enclosure", + "informal_anchor": "\"scientific_acceptance\": false", + "does_not_claim": "anything about the true coefficients" + }, + { + "name": "UniversalLaw.Side24.endpoints_in_unit_tenth", + "module": "UniversalLaw/Side24/Endpoints.lean", + "title": "Published endpoints lie in (0, 1/10)", + "source": "side24-enclosure", + "informal_anchor": "\"relative_periodization_bound\": \"1e-106\"", + "does_not_claim": "anything about the true coefficients" + } + ], + "negative_controls": { + "false_exponent_bound_d3": { + "module": "UniversalLaw/Side24/Ledger.lean", + "replace": "sixB d < 78", + "with": "sixB d < 77" + }, + "false_covariance_bound": { + "module": "UniversalLaw/Side24/Ledger.lean", + "replace": "60 * imageConstant < 10 ^ 17", + "with": "60 * imageConstant < 10 ^ 15" + }, + "false_exp_partial_sum": { + "module": "UniversalLaw/Side24/Ledger.lean", + "replace": "10 * (125 ^ 20 * fact 20) < expTaylorNumerator", + "with": "11 * (125 ^ 20 * fact 20) < expTaylorNumerator" + }, + "wrong_image_constant": { + "module": "UniversalLaw/Side24/Ledger.lean", + "replace": "= 21175738586478", + "with": "= 21175738586479" + }, + "false_eigenvalue_third": { + "module": "UniversalLaw/Side24/Ledger.lean", + "replace": "58 * 9 < 23 ^ 2", + "with": "58 * 9 < 22 ^ 2" + }, + "false_trace_variance": { + "module": "UniversalLaw/Side24/ConeMoments.lean", + "replace": "20 * 3 = 5 * 12", + "with": "20 * 3 = 6 * 12" + }, + "false_endpoint_adjacency": { + "module": "UniversalLaw/Side24/Endpoints.lean", + "replace": "d2Upper = d2Lower + 1", + "with": "d2Upper = d2Lower + 2" + } + } +} diff --git a/tests/fixtures/atlas_formal_build_3b39/test_formal_gate.py.txt b/tests/fixtures/atlas_formal_build_3b39/test_formal_gate.py.txt new file mode 100644 index 000000000..0b36e5139 --- /dev/null +++ b/tests/fixtures/atlas_formal_build_3b39/test_formal_gate.py.txt @@ -0,0 +1,366 @@ +"""Positive and negative controls for the main-side formal gate. + +Synthetic controls build a disposable mini package so each mutation is +isolated. Repository controls run the real manifest in source-only mode, and — +when a Lean toolchain is on PATH or in ~/.elan — execute the real package +(build, leanchecker, axiom audit, negative controls, receipt). +""" +import contextlib +import hashlib +import importlib.util +import io +import json +from pathlib import Path +import tempfile +import unittest + +ROOT = Path(__file__).resolve().parents[1] +spec = importlib.util.spec_from_file_location("gate", ROOT / "tools/formal_gate_check.py") +gate = importlib.util.module_from_spec(spec) +spec.loader.exec_module(gate) + +TOOLCHAIN = "leanprover/lean4:v4.34.1" +LEAN = """namespace Demo + +/-- Source: "two and two make four". A docstring mentioning sorry is harmless. -/ +theorem two_add : 2 + 2 = 4 := by decide + +theorem tight : 77 < 78 := by decide + +end Demo +""" +SOURCE = "Section 1. In the source, two and two make four; also 77 < 78 here.\n" +AUDIT = "'Demo.two_add' does not depend on any axioms\n'Demo.tight' does not depend on any axioms\n" + + +def sha(data: bytes) -> str: + return hashlib.sha256(data).hexdigest() + + +class SyntheticControls(unittest.TestCase): + def setUp(self): + self.tmp = tempfile.TemporaryDirectory() + self.addCleanup(self.tmp.cleanup) + self.root = Path(self.tmp.name) + for d in ("pkg/Demo", "pkg/sources", "pkg/reviews", "tools", "tests"): + (self.root / d).mkdir(parents=True) + self.write("pkg/lean-toolchain", TOOLCHAIN + "\n") + self.write("pkg/lakefile.toml", 'name = "Demo"\n[[lean_lib]]\nname = "Demo"\n') + self.write("pkg/lake-manifest.json", '{"packages": []}\n') + self.write("pkg/Demo.lean", "import Demo.Basic\n\n/-! root docstring -/\n") + self.write("pkg/Demo/Basic.lean", LEAN) + self.write("pkg/sources/SOURCE.md", SOURCE) + for name in ("SCOPE.md", "GLOSSARY.md", "README.md"): + self.write("pkg/" + name, name + "\n") + self.write("tools/formal_gate_check.py", "# bound control copy\n") + self.write("tests/test_formal_gate.py", "# bound control copy\n") + self.bound = ["pkg/lean-toolchain", "pkg/lakefile.toml", "pkg/lake-manifest.json", "pkg/Demo.lean", + "pkg/Demo/Basic.lean", "pkg/sources/SOURCE.md", "pkg/SCOPE.md", "pkg/GLOSSARY.md", + "pkg/README.md", "tools/formal_gate_check.py", "tests/test_formal_gate.py"] + self.manifest = { + "schema_version": 1, "scientific_effect": "NONE", "scientific_status_authority": False, + "package": "demo", "package_root": "pkg", "root_module": "Demo", + "formalization_status": "proved", "alignment_status": "PENDING_INDEPENDENT_REVIEW", + "lean_toolchain": TOOLCHAIN, "dependency_revisions": {}, + "allowed_axioms": ["propext", "Classical.choice", "Quot.sound"], + "files": {}, "unbound_files": ["pkg/manifest.json", "pkg/ALIGNMENT.md"], + "sources": [{"id": "src", "repository": "d6g8k5htny-coder/Math-", "commit": "a" * 40, "path": "SOURCE.md", + "bytes": len(SOURCE.encode()), "sha256": sha(SOURCE.encode()), "local_copy": "pkg/sources/SOURCE.md"}], + "source_modules": ["Demo/Basic.lean"], + "targets": [ + {"name": "Demo.two_add", "module": "Demo/Basic.lean", "title": "two add", "source": "src", + "informal_anchor": "two and two make four", "does_not_claim": "anything else"}, + {"name": "Demo.tight", "module": "Demo/Basic.lean", "title": "tight", "source": "src", + "informal_anchor": "77 < 78", "does_not_claim": "anything else"}, + ], + "negative_controls": {"tight": {"module": "Demo/Basic.lean", "replace": "77 < 78", "with": "77 < 77"}}, + } + self.refresh() + self.audit = self.root / "audit.txt" + self.audit.write_text(AUDIT) + + def write(self, relative, text): + (self.root / relative).write_text(text) + + def refresh(self): + self.manifest["files"] = {p: sha((self.root / p).read_bytes()) for p in self.bound} + self.save() + + def save(self): + (self.root / "pkg/manifest.json").write_text(json.dumps(self.manifest)) + (self.root / "pkg/ALIGNMENT.md").write_text(gate.render_alignment(self.manifest)) + + def check(self): + return gate.source_check(self.root, "pkg/manifest.json") + + def assertInvalid(self, fragment): + with self.assertRaisesRegex((ValueError, KeyError, TypeError), fragment): + self.check() + + # positive controls + + def test_valid_source_check_and_no_writes(self): + before = {str(p): p.read_bytes() for p in self.root.rglob("*") if p.is_file()} + m, digest, pkg = self.check() + self.assertEqual(digest, sha((self.root / "pkg/manifest.json").read_bytes())) + self.assertEqual([t["name"] for t in m["targets"]], ["Demo.two_add", "Demo.tight"]) + self.assertEqual(before, {str(p): p.read_bytes() for p in self.root.rglob("*") if p.is_file()}) + + def test_cli_source_only_reports_not_a_build(self): + buf = io.StringIO() + with contextlib.redirect_stdout(buf): + code = gate.main(["--root", str(self.root), "--manifest", "pkg/manifest.json", + "--alignment-table", "pkg/ALIGNMENT.md"]) + self.assertEqual(code, 0) + self.assertIn("SOURCE_IDENTITY_PASS (not a Lean build", buf.getvalue()) + + def test_audit_from_file_passes(self): + gate.audit_axioms(self.audit.read_text(), ["Demo.two_add", "Demo.tight"]) + + # manifest cannot self-award + + def test_manifest_cannot_claim_kernel_checked(self): + self.manifest["formalization_status"] = "kernel-checked" + self.save() + self.assertInvalid("cannot self-award") + + def test_manifest_cannot_claim_alignment(self): + self.manifest["alignment_status"] = "ACCEPTED" + self.save() + self.assertInvalid("cannot self-award") + + def test_status_authority_must_be_false(self): + self.manifest["scientific_status_authority"] = True + self.save() + self.assertInvalid("scientific_status_authority") + + def test_duplicate_json_key(self): + (self.root / "pkg/manifest.json").write_text('{"schema_version":1,"schema_version":1}') + self.assertInvalid("duplicate JSON key") + + # file identity + + def test_hash_mismatch(self): + self.write("pkg/Demo/Basic.lean", LEAN.replace("77 < 78", "77 < 79")) + self.assertInvalid("source hash mismatch") + + def test_unregistered_lean_module(self): + self.write("pkg/Demo/Extra.lean", "theorem extra : True := trivial\n") + self.manifest["files"]["pkg/Demo/Extra.lean"] = sha(b"theorem extra : True := trivial\n") + self.save() + self.assertInvalid("unregistered Lean module") + + def test_unbound_package_file(self): + self.write("pkg/notes.txt", "x\n") + self.assertInvalid("not bound or declared unbound") + + def test_control_files_must_be_bound(self): + del self.manifest["files"]["tools/formal_gate_check.py"] + self.save() + self.assertInvalid("unbound control or scope file") + + def test_scope_must_be_bound(self): + del self.manifest["files"]["pkg/SCOPE.md"] + self.save() + self.assertInvalid("unbound control or scope file") + + def test_toolchain_mismatch(self): + self.write("pkg/lean-toolchain", "leanprover/lean4:v4.0.0\n") + self.refresh() + self.assertInvalid("wrong Lean toolchain") + + def test_dependency_lock_mismatch(self): + self.write("pkg/lake-manifest.json", '{"packages": [{"name": "mathlib", "rev": "' + "b" * 40 + '"}]}\n') + self.refresh() + self.assertInvalid("dependency lock mismatch") + + def test_root_must_import_exactly_registered_modules(self): + self.write("pkg/Demo.lean", "import Demo.Basic\nimport Demo.Extra\n") + self.refresh() + self.assertInvalid("root must only import") + + # Lean text scan + + def test_sorry_in_code(self): + self.write("pkg/Demo/Basic.lean", LEAN.replace("by decide\n\ntheorem tight", "by sorry\n\ntheorem tight")) + self.refresh() + self.assertInvalid("sorry in") + + def test_sorry_only_in_comments_ignored(self): + self.write("pkg/Demo/Basic.lean", LEAN + "-- sorry native_decide axiom in a line comment\n/- nested /- sorry -/ still comment -/\n") + self.refresh() + self.check() + + def test_native_decide_refused(self): + self.write("pkg/Demo/Basic.lean", LEAN.replace(":= by decide\n\ntheorem tight", ":= by native_decide\n\ntheorem tight")) + self.refresh() + self.assertInvalid("native_decide in") + + def test_custom_axiom_refused(self): + self.write("pkg/Demo/Basic.lean", LEAN.replace("end Demo", "axiom parent : 1 = 1\n\nend Demo")) + self.refresh() + self.assertInvalid("custom axiom declaration") + + # target inventory and anchors + + def test_unregistered_theorem_refused(self): + self.write("pkg/Demo/Basic.lean", LEAN.replace("end Demo", "theorem extra : 1 = 1 := rfl\n\nend Demo")) + self.refresh() + self.assertInvalid("target inventory differs") + + def test_target_order_must_match_source(self): + self.manifest["targets"].reverse() + self.save() + self.assertInvalid("target inventory differs") + + def test_missing_theorem_refused(self): + self.manifest["targets"].append({"name": "Demo.three_add", "module": "Demo/Basic.lean", "title": "t", "source": "src", + "informal_anchor": "two and two", "does_not_claim": "x"}) + self.save() + self.assertInvalid("target inventory differs") + + def test_anchor_not_verbatim(self): + self.manifest["targets"][0]["informal_anchor"] = "two and two make five" + self.save() + self.assertInvalid("not a verbatim substring") + + def test_source_bytes_changed(self): + self.write("pkg/sources/SOURCE.md", SOURCE + "x") + self.manifest["files"]["pkg/sources/SOURCE.md"] = sha((SOURCE + "x").encode()) + self.save() + self.assertInvalid("local copy differs from pinned bytes") + + def test_nonpublic_source_repository_refused(self): + self.manifest["sources"][0]["repository"] = "someone/private" + self.save() + self.assertInvalid("nonpublic source repository") + + def test_does_not_claim_required(self): + self.manifest["targets"][0]["does_not_claim"] = " " + self.save() + self.assertInvalid("does_not_claim must be nonempty") + + # axiom audit + + def test_audit_missing_target(self): + with self.assertRaisesRegex(ValueError, "missing target axiom report"): + gate.audit_axioms("'Demo.two_add' does not depend on any axioms\n", ["Demo.two_add", "Demo.tight"]) + + def test_audit_sorry_axiom(self): + with self.assertRaisesRegex(ValueError, "forbidden transitive axiom"): + gate.audit_axioms(AUDIT.replace("'Demo.tight' does not depend on any axioms", + "'Demo.tight' depends on axioms: [sorryAx]"), ["Demo.two_add", "Demo.tight"]) + + def test_audit_native_axiom(self): + with self.assertRaisesRegex(ValueError, "Lean.ofReduceBool"): + gate.audit_axioms(AUDIT.replace("'Demo.tight' does not depend on any axioms", + "'Demo.tight' depends on axioms: [Lean.ofReduceBool]"), ["Demo.two_add", "Demo.tight"]) + + def test_audit_allowed_axioms_pass(self): + records = gate.audit_axioms(AUDIT.replace("'Demo.tight' does not depend on any axioms", + "'Demo.tight' depends on axioms: [propext, Classical.choice, Quot.sound]"), + ["Demo.two_add", "Demo.tight"]) + self.assertEqual(records["Demo.tight"], ["Classical.choice", "Quot.sound", "propext"]) + + def test_audit_unrecognized_output_fails(self): + with self.assertRaisesRegex(ValueError, "unrecognized audit output"): + gate.audit_axioms(AUDIT + "Basic.lean:4:0: error: something\n", ["Demo.two_add", "Demo.tight"]) + + def test_audit_unexpected_target_fails(self): + with self.assertRaisesRegex(ValueError, "unexpected or duplicate"): + gate.audit_axioms(AUDIT + "'Demo.extra' does not depend on any axioms\n", ["Demo.two_add", "Demo.tight"]) + + # alignment record + + def review(self, **overrides): + m, digest, _ = self.check() + record = {"disposition": "ACCEPTED", "manifest_sha256": digest, "scope_sha256": m["files"]["pkg/SCOPE.md"], + "targets": ["Demo.two_add", "Demo.tight"], + "author": {"provider": "Anthropic", "family": "Claude", "agent": "cursor"}, + "reviewer": {"provider": "OpenAI", "family": "GPT", "agent": "codex"}, + "evidence": {"repository": "d6g8k5htny-coder/main", "commit": "c" * 40, + "path": "formal/reviews/x.md", "sha256": "d" * 64}} + record.update(overrides) + return record, digest, m + + def test_alignment_valid(self): + record, digest, m = self.review() + gate.check_alignment(record, digest, ["Demo.two_add", "Demo.tight"], m["files"]["pkg/SCOPE.md"]) + + def test_alignment_same_provider_refused(self): + record, digest, m = self.review(reviewer={"provider": "anthropic", "family": "Other", "agent": "x"}) + with self.assertRaisesRegex(ValueError, "lineage not independent: provider"): + gate.check_alignment(record, digest, ["Demo.two_add", "Demo.tight"], m["files"]["pkg/SCOPE.md"]) + + def test_alignment_stale_manifest_refused(self): + record, digest, m = self.review(manifest_sha256="0" * 64) + with self.assertRaisesRegex(ValueError, "stale alignment manifest"): + gate.check_alignment(record, digest, ["Demo.two_add", "Demo.tight"], m["files"]["pkg/SCOPE.md"]) + + def test_alignment_partial_coverage_refused(self): + record, digest, m = self.review(targets=["Demo.two_add"]) + with self.assertRaisesRegex(ValueError, "partial or ambiguous"): + gate.check_alignment(record, digest, ["Demo.two_add", "Demo.tight"], m["files"]["pkg/SCOPE.md"]) + + def test_alignment_not_accepted_refused(self): + record, digest, m = self.review(disposition="ACCEPTED_AT_NARROWER_SCOPE") + with self.assertRaisesRegex(ValueError, "alignment not accepted"): + gate.check_alignment(record, digest, ["Demo.two_add", "Demo.tight"], m["files"]["pkg/SCOPE.md"]) + + def test_alignment_mutable_ref_refused(self): + record, digest, m = self.review(evidence={"repository": "d6g8k5htny-coder/main", "commit": "main", + "path": "formal/reviews/x.md", "sha256": "d" * 64}) + with self.assertRaisesRegex(ValueError, "mutable review ref"): + gate.check_alignment(record, digest, ["Demo.two_add", "Demo.tight"], m["files"]["pkg/SCOPE.md"]) + + # alignment table drift + + def test_alignment_table_drift_fails_cli(self): + (self.root / "pkg/ALIGNMENT.md").write_text("stale\n") + with contextlib.redirect_stdout(io.StringIO()): + code = gate.main(["--root", str(self.root), "--manifest", "pkg/manifest.json", "--alignment-table", "pkg/ALIGNMENT.md"]) + self.assertEqual(code, 1) + + +class RepositoryControls(unittest.TestCase): + def test_real_manifest_source_check(self): + m, digest, pkg = gate.source_check(ROOT) + self.assertEqual(m["formalization_status"], "proved") + self.assertEqual(m["alignment_status"], "PENDING_INDEPENDENT_REVIEW") + self.assertIs(m["scientific_status_authority"], False) + self.assertEqual(len(m["targets"]), 31) + self.assertEqual(m["dependency_revisions"], {}) + self.assertEqual((ROOT / "formal/ALIGNMENT.md").read_text(), gate.render_alignment(m)) + + def test_real_manifest_cli_source_only(self): + buf = io.StringIO() + with contextlib.redirect_stdout(buf): + self.assertEqual(gate.main(["--root", str(ROOT)]), 0) + self.assertIn("SOURCE_IDENTITY_PASS (not a Lean build or scientific acceptance)", buf.getvalue()) + + def test_real_template_record_is_refused(self): + m, digest, _ = gate.source_check(ROOT) + template = json.loads((ROOT / "formal/reviews/TEMPLATE_alignment_review.json").read_text()) + with self.assertRaises(ValueError): + gate.check_alignment(template, digest, [t["name"] for t in m["targets"]], m["files"]["formal/SCOPE.md"]) + + @unittest.skipUnless(gate.lake_binary(), "Lean toolchain not installed") + def test_real_package_executes_with_receipt(self): + m, digest, pkg = gate.source_check(ROOT) + with contextlib.redirect_stdout(io.StringIO()): + receipt = gate.execute(m, digest, pkg, ROOT) + self.assertEqual(receipt["formalization_status"], "kernel-checked") + self.assertEqual(receipt["alignment_status"], "PENDING_INDEPENDENT_REVIEW") + self.assertEqual(set(receipt["axioms"]), {t["name"] for t in m["targets"]}) + self.assertTrue(all(v == [] for v in receipt["axioms"].values())) + controls = receipt["negative_controls"] + self.assertEqual(controls["sorry"], "REJECTED_BY_AXIOM_GATE") + self.assertEqual(controls["custom_imported"], "REJECTED_BY_AXIOM_GATE") + self.assertEqual(controls["native"], "REJECTED_BY_AXIOM_GATE") + for label in m["negative_controls"]: + self.assertEqual(controls[label], "REJECTED_BY_LEAN", label) + self.assertTrue((pkg / ".lake/formal-evidence/receipt.json").is_file()) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/test_atlas_formal_evidence_build.py b/tests/test_atlas_formal_evidence_build.py index 5a2b1ab8c..0c07e26a7 100644 --- a/tests/test_atlas_formal_evidence_build.py +++ b/tests/test_atlas_formal_evidence_build.py @@ -1,23 +1,69 @@ """Source-identity assembly, never mathematical acceptance.""" from pathlib import Path -import copy +import hashlib import json +import tempfile import unittest from tools.atlas_formal_evidence_build import build_connection ROOT = Path(__file__).resolve().parents[1] CLAIM = 'math.side24-coefficient' +FIXTURE = ROOT/'tests/fixtures/atlas_formal_build_3b39' +HISTORICAL_MANIFEST = '8dfcfe4e9296bca47eede517f37b546ea420ec6b51944b7c16164a906b40e090' +HISTORICAL_FILES = { + 'formal/README.md': ('README.md.txt', + '54436dfd808547d9da9ce0a2ad64b0e5935bb755844fef99b298281c49044aaa'), + 'formal/REVIEW_LANE.md': ('REVIEW_LANE.md.txt', + '887f56209471fc0194d601a4f8a0c82eb75852e1c97da0400c16d447669e6340'), + 'tools/formal_gate_check.py': ('formal_gate_check.py.txt', + '21c355e02ac6e01337d10465a3105b34b93f832586ee60aa2430f662a90cd8b7'), + 'tests/test_formal_gate.py': ('test_formal_gate.py.txt', + '4286136d8b24eca9b26d1e7b12933bed5b0961809b362a60c3af7bf46e6ed4b6'), +} + + +def digest(raw): + return hashlib.sha256(raw).hexdigest() class FormalConnectionAssembly(unittest.TestCase): def setUp(self): - self.snapshot = json.loads((ROOT/'docs/site/current.json').read_bytes()) + self.temp = tempfile.TemporaryDirectory() + self.root = Path(self.temp.name) + manifest_raw = (FIXTURE/'manifest.json').read_bytes() + self.assertEqual(digest(manifest_raw), HISTORICAL_MANIFEST) + manifest = json.loads(manifest_raw) + for relative, expected in manifest['files'].items(): + fixture = HISTORICAL_FILES.get(relative) + raw = (FIXTURE/fixture[0]).read_bytes() if fixture else (ROOT/relative).read_bytes() + self.assertEqual(digest(raw), expected, relative) + destination = self.root/relative + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes(raw) + (self.root/'formal/manifest.json').write_bytes(manifest_raw) + for relative in ( + 'docs/site/dependency-source/GRAPH.json', + 'docs/site/evidence/side24-main-3b39/review.json', + 'docs/site/evidence/side24-main-3b39/review.md', + ): + raw = (ROOT/relative).read_bytes() + destination = self.root/relative + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes(raw) + self.snapshot = json.loads((ROOT/'tests/fixtures/atlas_formal_projection.json').read_bytes()) self.proof = (ROOT/'formal/sources/side24_v1/PROOF.md').read_bytes() self.artifact = (ROOT/'docs/site/evidence/side24-main-3b39/verified-execution.zip').read_bytes() + def tearDown(self): + self.temp.cleanup() + def build(self): - return build_connection(ROOT, self.snapshot, self.proof, self.artifact) + return build_connection(self.root, self.snapshot, self.proof, self.artifact) + + def test_live_manifest_drift_is_refused_before_historical_evidence_is_rebound(self): + with self.assertRaisesRegex(ValueError, 'formal manifest changed'): + build_connection(ROOT, self.snapshot, self.proof, self.artifact) def test_exact_proof_source_connects_to_original_checked_closed_declaration(self): result = self.build() @@ -42,24 +88,29 @@ def test_actual_adverse_review_is_retained_without_turning_one_aligned_row_into_ def test_changed_proof_bytes_are_refused(self): self.proof += b'\n' - with self.assertRaisesRegex(ValueError, 'proof'): self.build() + with self.assertRaisesRegex(ValueError, 'proof'): + self.build() def test_changed_graph_scope_is_refused_even_with_same_fingerprint(self): self.snapshot['graph']['data']['nodes'][CLAIM]['scope'] = 'Full theorem' - with self.assertRaisesRegex(ValueError, 'graph record'): self.build() + with self.assertRaisesRegex(ValueError, 'graph record'): + self.build() def test_same_name_or_fingerprint_with_wrong_blob_is_refused(self): source = next(s for s in self.snapshot['sources'] if s['path'] == 'coefficients/side24_v1/PROOF.md') source['blob'] = '0'*40 - with self.assertRaisesRegex(ValueError, 'proof inventory'): self.build() + with self.assertRaisesRegex(ValueError, 'proof inventory'): + self.build() def test_modified_execution_archive_is_not_trusted(self): self.artifact += b'\n' - with self.assertRaisesRegex(ValueError, 'artifact identity'): self.build() + with self.assertRaisesRegex(ValueError, 'artifact identity'): + self.build() def test_missing_named_claim_cannot_use_an_equally_named_source(self): del self.snapshot['graph']['data']['nodes'][CLAIM] - with self.assertRaisesRegex(ValueError, 'graph record'): self.build() + with self.assertRaisesRegex(ValueError, 'graph record'): + self.build() if __name__ == '__main__':