diff --git a/autoform_cli/README.md b/autoform_cli/README.md index c316452a..bd527384 100644 --- a/autoform_cli/README.md +++ b/autoform_cli/README.md @@ -84,7 +84,8 @@ An article asserts only facts a human or agent verified: | Key | Meaning | | --- | --- | | `statement: formalized` | The Lean statement exists and compiles. | -| `statement: retracted` | A revision retracted the statement while `lean:` still names the old declaration, which stays in the build until Formalize restates the article and records `statement: formalized` in its place. Requires `lean:`; invalid with `proof: formalized` or `mathlib: true`. CI's `autoform check` at an older `AUTOFORM_REF` rejects the marker, so move the pin first; until then, retract by removing `statement` and `proof` and keeping `lean:`. | +| `statement: retracted` | A revision retracted the statement while `lean:` still names the old declaration, which stays in the build until Formalize restates the article and records `statement: formalized` in its place. Requires `lean:`; invalid with `proof: formalized` or `mathlib: true`. CI's `autoform check` at an older `AUTOFORM_REF` rejects the marker, so move the pin first; until then, retract by removing `statement`, `statement_hash`, and `proof` and keeping `lean:`. | +| `statement_hash: sha256:...` | The statement Agent Review passed: `sha256:` and 64 lowercase hex digits, as `autoform skeleton` prints it. Requires `statement: formalized`; invalid with `statement: retracted` or `mathlib: true`. CI fails when the statement drifts from it, as `autoform skeleton --check-statements` reports. | | `proof: formalized` | The Lean proof compiles. Under the open policy it may rest on open statements, and the article is then conditional; only the derived `fully_proved` means complete and `sorry`-free. | | `mathlib: true` | The result is upstreamed into Mathlib. | | `not_ready: true` | Needs more blueprint work before it can be attempted. | @@ -340,6 +341,7 @@ Extract what a reader must trust for each formalized statement: autoform skeleton blueprint --lean-root . autoform skeleton blueprint --lean-root . --node chapter/main-result autoform skeleton blueprint --lean-root . --output skeleton.json --packets review-packets --passages review-passages +autoform skeleton blueprint --lean-root . --check-statements ``` A theorem means what its statement means. The skeleton of a `lean:` @@ -383,7 +385,7 @@ environment rather than by the source text: its kernel face is an opaque constant, so the body a reader would see is not what Lean checks. The command exits nonzero when a `lean:` name is absent from the sources or from the built environment, or reaches a refused declaration; that name is unresolved for its article only, other articles still extract, and it writes nothing into the vault; -`--output` records the `autoform-skeleton/v4` report, which contains no +`--output` records the `autoform-skeleton/v5` report, which contains no timestamp or absolute path, for a later render or review to consume. The report identifies the exact blueprint, its complete target set, and whether the extraction covered all targets or an explicit `--node` selection. It @@ -428,6 +430,42 @@ the article's hash and review hash as null rather than hashing the rest. It compares reports across builds; it is not a stable statement identifier, reviewer authentication, or an approval key. +Each article also gets a **statement hash**, printed as `statement_hash` in +`--json` and as a `== ID · statement_hash sha256:...` line in the text report. +It is the SHA-256 of canonical JSON over the schema `autoform-statement/v1`, +the article's statement text (the published statement: the body between the +title and the first heading, dependency sections dropped, with line endings +and trailing whitespace normalized), and the sorted, de-duplicated name, kind, +and elaborated meaning of every `lean:` declaration and every project +declaration its statement rests on. A theorem's meaning is its type, so a proof +leaves the hash alone; axioms, external assumptions, boundary modules, the +Lean version, and the cited passage are left out. A toolchain bump rotates it +only when it changes the elaborated terms. It is null when any of the article's +names is unresolved. The report records the statement text it hashes. + +Formalize records the hash as `statement_hash` beside `statement: formalized` +once the statement passes Agent Review. `--check-statements` then compares +every recorded hash with the current one and exits 1 with one line per drifted +article: + +```text +error: ID: statement_hash OLD is recorded but the statement now hashes to NEW; re-review the statement and record the new hash +``` + +An article that records a hash but has no `lean:`, or one of whose names is +unresolved, also fails. Articles without the key are not checked; when none +records one, the command prints `no article records statement_hash; nothing +to check` and exits 0 without running Lean, and otherwise a clean run prints +`N recorded statement hash(es) match`. It honours `--timeout` and does not +combine with `--node`, `--json`, `--output`, `--packets`, or `--passages`. The +generated `autoform-verify.yml` runs it after the kernel-trust audit, so a type +edit that still compiles, or an edit to the article's statement text, fails CI +instead of keeping the article proved. Like the drift hash, it is a drift +check, not reviewer authentication or an approval key. A project whose +`AUTOFORM_REF` predates the key stops at `autoform check` with `unsupported +frontmatter key 'statement_hash'`; move the pin and replace the workflow with +the version `autoform init` writes before recording hashes. + Reports and packet manifests also carry an evidence hash over the exact packet shown to a reviewer. It identifies those bytes but does not authenticate who reviewed them. An article review hash additionally binds the joint packet to the @@ -916,10 +954,10 @@ Markdown (step 6); Formalize carries out the Lean side (steps 1 to 5). names X beside X', so the audit keeps accepting that `sorry` as an open statement, and R records `proof` only after step 4 deletes X. Statement-impacted articles replace `statement: formalized` with - `statement: retracted`, lose `proof`, and keep `lean:`, so they return to - the frontier as revisions; under the open policy a statement-impacted - theorem stays an open statement meanwhile (see [open - statements](#open-statements)). When X's proof is sorry-free, + `statement: retracted`, lose `statement_hash` and `proof`, and keep + `lean:`, so they return to the frontier as revisions; under the open + policy a statement-impacted theorem stays an open statement meanwhile + (see [open statements](#open-statements)). When X's proof is sorry-free, proof-impacted articles keep everything, since their proofs still use the valid old X; migrating them to X' is later work. While it is still `sorry`, proof-impacted theorems lose `proof: formalized` but keep @@ -941,14 +979,15 @@ Markdown (step 6); Formalize carries out the Lean side (steps 1 to 5). `contained` says, and its `claim_targets` are incomplete: add every stated article whose Lean imports the changed module and treat it as statement-impacted. A statement-impacted article keeps `statement` only - after an Agent Review of its source faithfulness under X's new meaning; - otherwise it records `statement: retracted`, loses `proof`, and keeps + after an Agent Review of its source faithfulness under X's new meaning, + and then records its new `statement_hash`; otherwise it records + `statement: retracted`, loses `statement_hash` and `proof`, and keeps `lean:`. A repaired dependent proof keeps `proof: formalized` only after an Agent Review of the repair; otherwise it loses `proof`. A theorem's proof that cannot be repaired becomes exactly `sorry` under the open policy; otherwise delete the declaration and remove its article's - `lean:`, `statement`, and `proof`, which works only when nothing else - uses it. When neither applies, the + `lean:`, `statement`, `statement_hash`, and `proof`, which works only + when nothing else uses it. When neither applies, the revision is blocked: release the claims and report it. Record what happened under `## Execution notes` of each touched article. 3. Claim the route's claim set with one `autoform claim acquire`. When it is @@ -976,12 +1015,13 @@ Markdown (step 6); Formalize carries out the Lean side (steps 1 to 5). design, while CI, which runs neither, passes. 6. When Roadmap revises an article, its statement text or only its Lean, it records the decision and retracts the article: it replaces `statement: - formalized` with `statement: retracted`, removes `proof: formalized`, and - keeps `lean:`, which `work impact` needs, so the article returns to the - frontier as a revision; an article without `lean:` just loses `statement` - and `proof`. It retracts only that article and the dependents whose - Markdown text the revision rewrites; the Lean-side impact decides every - other dependent. Roadmap edits only Markdown: it releases its claims and + formalized` with `statement: retracted`, removes `statement_hash` and + `proof: formalized`, and keeps `lean:`, which `work impact` needs, so the + article returns to the frontier as a revision; an article without `lean:` + just loses `statement`, `statement_hash`, and `proof`. It retracts only + that article and the dependents whose Markdown text the revision rewrites; + the Lean-side impact decides every other dependent. Roadmap edits only + Markdown: it releases its claims and leaves the Lean revision to Formalize. ## Local runtime doctor diff --git a/autoform_cli/__main__.py b/autoform_cli/__main__.py index 60aa4816..1a895d9d 100644 --- a/autoform_cli/__main__.py +++ b/autoform_cli/__main__.py @@ -29,6 +29,7 @@ from .skeleton import ( DEFAULT_PROBE_TIMEOUT, SkeletonError, + check_statement_hashes, extract_skeletons, format_report, run_probe, @@ -237,6 +238,11 @@ def main(argv: Sequence[str] | None = None) -> int: help=f"seconds the Lean probe may run (default {DEFAULT_PROBE_TIMEOUT:g}); " "the Lake freshness check before it has its own budget", ) + skeleton.add_argument( + "--check-statements", + action="store_true", + help="fail when an article's recorded statement_hash no longer matches its statement", + ) render = subparsers.add_parser("render", help="build the publishable blueprint") render.add_argument("blueprint_dir") @@ -740,6 +746,27 @@ def _positive_seconds(value: str) -> float: def _skeleton(args: argparse.Namespace) -> int: + runner = None if args.timeout is None else lambda probe, root: run_probe(probe, root, timeout=args.timeout) + if args.check_statements: + if args.nodes or args.json or args.output is not None or args.packets is not None or args.passages is not None: + print( + "error: --check-statements does not combine with --node, --json, --output, --packets, or --passages", + file=sys.stderr, + ) + return 2 + try: + recorded, failures = check_statement_hashes(args.blueprint_dir, lean_root=args.lean_root, runner=runner) + except SkeletonError as exc: + for issue in exc.issues: + print(f"error: {issue}", file=sys.stderr) + return 2 + for failure in failures: + print(f"error: {failure}", file=sys.stderr) + if not recorded: + print("no article records statement_hash; nothing to check") + elif not failures: + print(f"{recorded} recorded statement hash(es) match") + return 1 if failures else 0 if args.passages is not None and args.packets is None: print("error: --passages requires --packets", file=sys.stderr) return 2 @@ -754,9 +781,7 @@ def _skeleton(args: argparse.Namespace) -> int: report = extract_skeletons( args.blueprint_dir, lean_root=args.lean_root, - runner=None - if args.timeout is None - else lambda probe, root: run_probe(probe, root, timeout=args.timeout), + runner=runner, node_ids=tuple(args.nodes) if args.nodes else None, ) if args.packets is not None and not report.clean: diff --git a/autoform_cli/graph.py b/autoform_cli/graph.py index aa08c31c..a4d96eeb 100644 --- a/autoform_cli/graph.py +++ b/autoform_cli/graph.py @@ -22,12 +22,14 @@ _HTML_COMMENT = re.compile(r"|$)", re.DOTALL) _INLINE_CODE = re.compile(r"(`+).*?\1") ARTICLE_ID_PATTERN = re.compile(r"af_[0-9a-f]{24}\Z") +STATEMENT_HASH_PATTERN = re.compile(r"sha256:[0-9a-f]{64}\Z") _FRONTMATTER_KEYS = frozenset( { "article_id", "declaration", "lean", "statement", + "statement_hash", "proof", "mathlib", "mathlib_declaration", @@ -83,6 +85,9 @@ class Node: #: ``lean:`` still names the old declaration, which stays in the build #: until Formalize restates the article. statement_retracted: bool = False + #: ``statement_hash``: the statement hash ``autoform skeleton`` printed + #: when the statement passed review; ``--check-statements`` compares it. + statement_hash: str | None = None proof_formalized: bool = False mathlib: bool = False mathlib_declaration: str | None = None @@ -233,6 +238,7 @@ def resolve(targets: tuple[str, ...], node: _ParsedNode = parsed_node) -> list[s lean=metadata.get("lean"), statement_formalized=metadata.get("statement") == _FORMALIZED, statement_retracted=metadata.get("statement") == _RETRACTED, + statement_hash=metadata.get("statement_hash"), proof_formalized=metadata.get("proof") == _FORMALIZED, mathlib=metadata.get("mathlib") in _TRUE, mathlib_declaration=metadata.get("mathlib_declaration"), @@ -488,6 +494,11 @@ def _parse_frontmatter(node_id: str, lines: list[str]) -> tuple[dict[str, str], issues.append(f"{node_id}: proof: formalized needs statement: formalized, not retracted") if metadata.get("mathlib") in _TRUE: issues.append(f"{node_id}: a mathlib: true article cannot record statement: retracted") + if "statement_hash" in metadata: + if metadata.get("statement") != _FORMALIZED: + issues.append(f"{node_id}: statement_hash needs statement: formalized; without it, omit statement_hash") + if metadata.get("mathlib") in _TRUE: + issues.append(f"{node_id}: a mathlib: true article cannot record statement_hash") return metadata, end + 1, issues @@ -499,6 +510,10 @@ def _normalize_value(node_id: str, line_number: int, key: str, value: str) -> tu if not ARTICLE_ID_PATTERN.fullmatch(value): return value, f"{location}: malformed article_id {value!r}" return value, None + if key == "statement_hash": + if not STATEMENT_HASH_PATTERN.fullmatch(value): + return value, f"{location}: malformed statement_hash {value!r}; expected sha256: and 64 lowercase hex digits" + return value, None if key == "statement": if folded not in {_FORMALIZED, _RETRACTED}: return value, ( diff --git a/autoform_cli/skeleton.py b/autoform_cli/skeleton.py index fddf6c80..f88b6972 100644 --- a/autoform_cli/skeleton.py +++ b/autoform_cli/skeleton.py @@ -46,8 +46,9 @@ index_project, ) -SKELETON_SCHEMA = "autoform-skeleton/v4" +SKELETON_SCHEMA = "autoform-skeleton/v5" SEMANTIC_SCHEMA = "autoform-lean-expr/v4" +STATEMENT_HASH_SCHEMA = "autoform-statement/v1" #: Every line the probe wants read back starts with this marker, so Lean's own #: informational output can never be mistaken for a result. @@ -304,6 +305,8 @@ class NodeSkeleton: #: article then has no hash, since one over the rest would miss changes #: to the missing declaration. complete: bool = True + #: The article's own statement text, as :func:`article_statement` cuts it. + statement_text: str = "" def blind_text(self) -> str: """The article's declarations as one blind packet, for a faithfulness judge. @@ -354,6 +357,33 @@ def review_hash(self) -> str | None: } return _sha256_id(json.dumps(material, sort_keys=True, ensure_ascii=False).encode()) + @property + def statement_hash(self) -> str | None: + """Fingerprint what a reviewed statement certifies, for ``statement_hash:``. + + It binds the article's statement text and the elaborated meaning of + its declarations and every project declaration they trust, and nothing + else: proofs, axioms, library assumptions, boundary modules, the Lean + version, the cited passage, and source spelling stay out, so removing a + ``sorry``, bumping the toolchain, or editing a citation leaves it alone. + """ + + if not self.complete: + return None + declarations = sorted( + { + (item.name, item.kind, item.semantic) + for declaration in self.declarations + for item in (declaration, *declaration.trusted) + } + ) + material = { + "declarations": [list(item) for item in declarations], + "schema": STATEMENT_HASH_SCHEMA, + "statement": self.statement_text, + } + return _sha256_id(json.dumps(material, sort_keys=True, ensure_ascii=False).encode()) + def as_dict(self) -> dict[str, object]: return { "article_path": self.article_path, @@ -364,6 +394,8 @@ def as_dict(self) -> dict[str, object]: "passage": self.passage, "passage_locator": self.passage_locator, "review_hash": self.review_hash, + "statement_hash": self.statement_hash, + "statement_text": self.statement_text, } @@ -610,6 +642,9 @@ def _node_from_dict( locator = _report_value(item.get("passage_locator"), f"passage locator for {node_id}", optional=True) if (passage is None) != (locator is None): raise SkeletonError([f"mismatched passage fields for {node_id} in skeleton report"]) + statement_text = item.get("statement_text") + if type(statement_text) is not str: + raise SkeletonError([f"invalid statement text for {node_id} in skeleton report"]) return NodeSkeleton( node_id=node_id, article_path=article_path, @@ -617,6 +652,7 @@ def _node_from_dict( passage=passage, passage_locator=locator, complete={declaration.name for declaration in declarations} == set(targets.get(node_id, ())), + statement_text=statement_text, ) @@ -2109,6 +2145,7 @@ def extract_graph_skeletons( selected = [(node, names) for node, names in selected if node.id in wanted] selection = "filtered" passages: dict[str, tuple[str | None, str | None]] = {} + statements = {node.id: article_statement(node) for node, _ in selected} # An article whose cited passage cannot be found cannot be judged for # faithfulness, so its declarations are unresolved rather than shown alone. broken_passages: dict[str, str] = {} @@ -2203,6 +2240,7 @@ def extract_graph_skeletons( passage=passage, passage_locator=locator, complete={item.name for item in declarations} == set(names), + statement_text=statements[node.id], ) ) return SkeletonReport( @@ -2232,6 +2270,73 @@ def _statement(value: object) -> str | None: return _TRAILING_VALUE.sub("", value).rstrip() +def article_statement(node: Node) -> str: + """Return the article's own statement text, the part ``statement_hash`` binds. + + It is what the published site sets inside the statement box: the prose + after the H1 and before the first section heading, without the dependency + sections. Only line endings and trailing whitespace are normalized. + """ + + from .render import _split_body + + try: + content = node.path.read_bytes() + except OSError as exc: + raise SkeletonError([f"{node.id}: cannot read the article: {exc}"]) from exc + if node.source_sha256 is not None and hashlib.sha256(content).hexdigest() != node.source_sha256: + raise SkeletonError( + [f"{node.id}: the article changed while skeletons were being extracted; retry after the project is idle"] + ) + statement, _ = _split_body(content.decode("utf-8")) + return "\n".join(line.rstrip() for line in statement.splitlines()) + + +def check_statement_hashes( + blueprint_dir: str | Path, + *, + lean_root: str | Path, + runner: ProbeRunner | None = None, +) -> tuple[int, tuple[str, ...]]: + """Compare every recorded ``statement_hash`` with the current one. + + Returns how many articles record one and one failure line per article + whose hash no longer holds or cannot be computed. When no article records + one, Lean never runs. + """ + + try: + graph = load_graph(blueprint_dir) + except GraphValidationError as exc: + raise SkeletonError(exc.issues) from exc + recorded = {node.id: node for node in graph.nodes.values() if node.statement_hash is not None} + failures: dict[str, str] = {} + for node_id, node in recorded.items(): + if not node.lean: + failures[node_id] = f"{node_id}: statement_hash is recorded but the article names no lean: declaration" + probed = tuple(sorted(node_id for node_id in recorded if node_id not in failures)) + if probed: + report = extract_skeletons(graph.blueprint_dir, lean_root=lean_root, runner=runner, node_ids=probed) + if report.blueprint_hash != _blueprint_hash(graph): + raise SkeletonError( + ["the blueprint changed while statement hashes were being checked; retry after the project is idle"] + ) + reasons = {issue.node_id: f"{issue.declaration}: {issue.reason}" for issue in report.unresolved} + for node_id in probed: + expected = recorded[node_id].statement_hash + skeleton = report.node(node_id) + current = None if skeleton is None else skeleton.statement_hash + if current is None: + why = reasons.get(node_id, "a declaration is unresolved") + failures[node_id] = f"{node_id}: statement_hash cannot be checked: {why}" + elif current != expected: + failures[node_id] = ( + f"{node_id}: statement_hash {expected} is recorded but the statement now hashes to {current}; " + "re-review the statement and record the new hash" + ) + return len(recorded), tuple(failures[node_id] for node_id in sorted(failures)) + + def source_passage(node: Node, blueprint: Path, *, issues: list[str] | None = None) -> tuple[str | None, str | None]: """Return the passage an article cites through a line locator, and the locator. @@ -2478,6 +2583,9 @@ def format_report(report: SkeletonReport, *, lean_root: Path | None = None) -> s out.append("") if not node.declarations: out += [f"== {node.node_id} · no skeleton", ""] + else: + statement = node.statement_hash or "none: a declaration is unresolved" + out += [f"== {node.node_id} · statement_hash {statement}", ""] for issue in report.unresolved: out.append(f"error: {issue.message}") return "\n".join(out).rstrip("\n") + "\n" @@ -2951,6 +3059,7 @@ def _where(item: TrustedDeclaration) -> str: "PROBE_MARKER", "SEMANTIC_SCHEMA", "SKELETON_SCHEMA", + "STATEMENT_HASH_SCHEMA", "DeclarationSkeleton", "LeanLibrary", "NodeSkeleton", @@ -2959,6 +3068,8 @@ def _where(item: TrustedDeclaration) -> str: "SkeletonError", "SkeletonReport", "TrustedDeclaration", + "article_statement", + "check_statement_hashes", "extract_graph_skeletons", "extract_skeletons", "format_report", diff --git a/autoform_cli/templates/github/workflows/autoform-verify.yml b/autoform_cli/templates/github/workflows/autoform-verify.yml index 427171b0..108590f1 100644 --- a/autoform_cli/templates/github/workflows/autoform-verify.yml +++ b/autoform_cli/templates/github/workflows/autoform-verify.yml @@ -111,3 +111,12 @@ jobs: "$AUTOFORM_ROOT_PACKAGE" "$archive" "$probe" fi lake env lean "$probe" + + - name: Check recorded statement hashes + run: | + set -euo pipefail + # An article's statement_hash binds the statement Agent Review approved + # (its text and the elaborated Lean meaning). A drifted statement fails + # here until it is re-reviewed and the new hash recorded. + uvx --from "git+${AUTOFORM_SOURCE}@${AUTOFORM_REF}" \ + autoform skeleton blueprint --lean-root . --check-statements diff --git a/skills/agent-review/SKILL.md b/skills/agent-review/SKILL.md index fd182306..6e3a901e 100644 --- a/skills/agent-review/SKILL.md +++ b/skills/agent-review/SKILL.md @@ -47,6 +47,8 @@ the evidence hash for the exact packet that was read. For a source-faithfulness verdict, record the article review hash that binds the joint packet to the cited passage, its locator, and the skeleton hash. These hashes are provenance evidence, not reviewer authentication or an approval key. +When a statement passes, report the article's `statement_hash` from the same +skeleton output; Formalize records it next to `statement: formalized`. A read-back verdict also copies its raw read-back hashes as specified by its rubric. Candidate code runs during extraction and can forge process output, so treat diff --git a/skills/formalize/SKILL.md b/skills/formalize/SKILL.md index c2d2181b..85345b4f 100644 --- a/skills/formalize/SKILL.md +++ b/skills/formalize/SKILL.md @@ -65,7 +65,8 @@ Lean uses: start from `autoform work impact` and make only the edits the [revision contract](../../autoform_cli/README.md#revision-contract) requires, under the claims it requires. A work item flagged `revision`, whose article records `statement: retracted`, is such a revision; restating it replaces -`statement: retracted` with `statement: formalized`. Never add a new use of a +`statement: retracted` with `statement: formalized` and records the restated +statement's `statement_hash`. Never add a new use of a deprecated declaration. Search the pinned Mathlib checkout before adding helpers, and use the shared Lean LSP and REPL with `` as the project path. Finish with the focused Lake target. Declare the result in a module the @@ -111,7 +112,13 @@ score instead. On acceptance, update only the claimed article with the exact compiled declaration and truthful assertions: `statement: formalized`, plus `proof: -formalized` once the proof is complete. On a useful failed route, record only +formalized` once the proof is complete. Record `statement: formalized` together +with the `statement_hash` that `autoform skeleton /blueprint +--lean-root --node ` prints for the candidate Agent Review passed. +The hash binds the article's statement text and the elaborated meaning of its +declarations, so a later edit to either fails CI's `--check-statements` until +the statement is reviewed again and the new hash recorded. A proof does not +change it: the proof phase leaves a recorded hash as it is. On a useful failed route, record only distilled reusable evidence under `## Execution notes`—the remaining goal, checked lemmas, and next route—never a transcript or retry counter. A missing prerequisite, an incorrect decomposition, a change another article needs, or a diff --git a/skills/roadmap/SKILL.md b/skills/roadmap/SKILL.md index b89cfd72..f20911c1 100644 --- a/skills/roadmap/SKILL.md +++ b/skills/roadmap/SKILL.md @@ -76,12 +76,13 @@ from. A refused acquire means another agent owns the article: leave it and report it. Claims write refs to the board's remote, which is outward-facing, so make sure the request covers them. When a revision changes a statement whose article has `lean:`, retract it: replace `statement: formalized` with -`statement: retracted`, remove `proof: formalized`, and keep `lean:`, which -Formalize needs to run `autoform work impact`; an article without `lean:` just -loses `statement` and `proof`. When the project's CI pins an `AUTOFORM_REF` -older than the marker, its `autoform check` rejects `statement: retracted`: -remove `statement` and `proof` and keep `lean:` until the pin moves, and report -the old pin. Under the open policy a retracted theorem stays +`statement: retracted`, remove `statement_hash` and `proof: formalized`, and +keep `lean:`, which Formalize needs to run `autoform work impact`; an article +without `lean:` just loses `statement`, `statement_hash`, and `proof`. When the +project's CI pins an `AUTOFORM_REF` older than the marker, its `autoform check` +rejects `statement: retracted`: remove `statement`, `statement_hash`, and +`proof` and keep `lean:` until the pin moves, and report the old pin. Under the +open policy a retracted theorem stays an open statement, so whatever rests on it stays conditionally proved. Retract only that article and the dependents whose Markdown text the revision rewrites, claiming them all in one acquire; the Lean-side impact decides every other diff --git a/skills/setup/assets/cabannes-thesis-project/.github/workflows/autoform-verify.yml b/skills/setup/assets/cabannes-thesis-project/.github/workflows/autoform-verify.yml index 1144ff2c..f0216d53 100644 --- a/skills/setup/assets/cabannes-thesis-project/.github/workflows/autoform-verify.yml +++ b/skills/setup/assets/cabannes-thesis-project/.github/workflows/autoform-verify.yml @@ -111,3 +111,12 @@ jobs: "$AUTOFORM_ROOT_PACKAGE" "$archive" "$probe" fi lake env lean "$probe" + + - name: Check recorded statement hashes + run: | + set -euo pipefail + # An article's statement_hash binds the statement Agent Review approved + # (its text and the elaborated Lean meaning). A drifted statement fails + # here until it is re-reviewed and the new hash recorded. + uvx --from "git+${AUTOFORM_SOURCE}@${AUTOFORM_REF}" \ + autoform skeleton blueprint --lean-root . --check-statements diff --git a/tests/test_graph.py b/tests/test_graph.py index 7a7da9fe..ad9aa2ea 100644 --- a/tests/test_graph.py +++ b/tests/test_graph.py @@ -329,6 +329,70 @@ def test_rejects_a_retracted_statement_that_cannot_keep_its_declaration( assert raised.value.issues == (message,) +_STATEMENT_HASH = "sha256:" + "0123456789abcdef" * 4 + + +def test_records_a_statement_hash(tmp_path: Path) -> None: + blueprint = tmp_path / "blueprint" + _node( + blueprint, + "result.md", + "# Result\n", + declaration="theorem", + statement="formalized", + statement_hash=_STATEMENT_HASH, + lean="Ns.result", + ) + _node(blueprint, "other.md", "# Other\n", declaration="theorem", statement="formalized", lean="Ns.other") + + nodes = load_graph(blueprint).nodes + + assert nodes["result"].statement_hash == _STATEMENT_HASH + assert nodes["other"].statement_hash is None + + +@pytest.mark.parametrize( + ("metadata", "message"), + [ + ( + {"statement": "formalized", "statement_hash": _STATEMENT_HASH.upper()}, + "result:4: malformed statement_hash", + ), + ( + {"statement": "formalized", "statement_hash": _STATEMENT_HASH[:-1]}, + "result:4: malformed statement_hash", + ), + ( + {"statement": "formalized", "statement_hash": _STATEMENT_HASH.removeprefix("sha256:")}, + "result:4: malformed statement_hash", + ), + ( + {"statement_hash": _STATEMENT_HASH}, + "result: statement_hash needs statement: formalized; without it, omit statement_hash", + ), + ( + {"statement": "retracted", "statement_hash": _STATEMENT_HASH}, + "result: statement_hash needs statement: formalized; without it, omit statement_hash", + ), + ( + {"statement": "formalized", "statement_hash": _STATEMENT_HASH, "mathlib": "true"}, + "result: a mathlib: true article cannot record statement_hash", + ), + ], +) +def test_rejects_a_statement_hash_without_a_statement_to_bind( + tmp_path: Path, metadata: dict[str, str], message: str +) -> None: + blueprint = tmp_path / "blueprint" + _node(blueprint, "result.md", "# Result\n", lean="Ns.result", **metadata) + + with pytest.raises(GraphValidationError) as raised: + load_graph(blueprint) + + assert len(raised.value.issues) == 1 + assert raised.value.issues[0].startswith(message) + + def test_records_origin_and_source_links_without_treating_them_as_edges(tmp_path: Path) -> None: blueprint = tmp_path / "blueprint" source = blueprint / "sources" / "paper.md" diff --git a/tests/test_skeleton.py b/tests/test_skeleton.py index 5917cb0a..ab55ec2a 100644 --- a/tests/test_skeleton.py +++ b/tests/test_skeleton.py @@ -17,6 +17,7 @@ import psutil from autoform_cli.__main__ import main +from autoform_cli.graph import load_graph from autoform_cli.lean import PACKET_SCHEMA, PASSAGE_SCHEMA, index_project from autoform_cli.skeleton import ( DeclarationSkeleton, @@ -46,6 +47,8 @@ _project_control_snapshot, _without_comments, _probe_record_issue, + article_statement, + check_statement_hashes, extract_skeletons, format_report, lean_libraries, @@ -1488,7 +1491,7 @@ def test_report_round_trips_through_json_deterministically(tmp_path: Path) -> No path.write_text(first, encoding="utf-8") assert load_skeleton_report(path) == report - for schema in ("autoform-skeleton/v1", "autoform-skeleton/v2", "autoform-skeleton/v3"): + for schema in ("autoform-skeleton/v1", "autoform-skeleton/v2", "autoform-skeleton/v3", "autoform-skeleton/v4"): legacy = report.as_dict() legacy["schema"] = schema _assert_load_rejects(path, legacy) @@ -1627,6 +1630,82 @@ def test_text_report_quotes_the_sources_a_reader_must_trust(tmp_path: Path) -> N assert " -- Skel.NonAmbiguous {Y : Type} (S : Y → Prop) : Prop\n" in text # The quoted source travels inside the report, so no Lean tree is needed to print it. assert " def Eligible (S : Y → Prop) (y : Y) : Prop := S y\n" in format_report(report) + assert f"== basics/determined · statement_hash {report.nodes[0].statement_hash}\n" in text + + +def test_statement_hash_binds_the_statement_text_and_meaning_only(tmp_path: Path) -> None: + node = _fake_report(tmp_path).nodes[0] + (declaration,) = node.declarations + base = node.statement_hash + assert base is not None and re.fullmatch(r"sha256:[0-9a-f]{64}", base) + assert node.statement_text == "A statement." + + def with_root(**changes: object) -> NodeSkeleton: + return replace(node, declarations=(replace(declaration, **changes),)) + + # What a proof, the toolchain, or a citation can change leaves it alone, + # although the drift hash moves for some of them. + assert with_root(lean_version="4.99.0").hash != node.hash + for unchanged in ( + with_root(lean_version="4.99.0"), + with_root(axioms=(), axiom_semantics=()), + with_root(assumed=(), assumed_semantics=(), boundary_modules=()), + with_root(end_line=99, statement="theorem respelled : True", statement_comments=()), + replace(node, passage="Theorem 1.", passage_locator="sources/book.txt#L1-L1"), + ): + assert unchanged.statement_hash == base + + # The article's statement text, a root's meaning, or a trusted item's meaning rotates it. + other_type = _semantic({"type": {"sort": {"succ": {"zero": None}}}}) + first, *rest = declaration.trusted + for changed in ( + replace(node, statement_text="A stronger statement."), + with_root(semantic=other_type), + with_root(trusted=(replace(first, semantic=other_type), *rest)), + with_root(trusted=(replace(first, kind="opaque"), *rest)), + ): + assert changed.statement_hash not in {None, base} + + # Shared trusted items count once, whatever order the declarations come in. + second = replace(declaration, name="Skel.other") + assert replace(node, declarations=(declaration, second)).statement_hash == ( + replace(node, declarations=(second, declaration)).statement_hash + ) + assert replace(node, complete=False).statement_hash is None + + +def test_article_statement_is_the_published_statement_with_normalized_line_ends(tmp_path: Path) -> None: + blueprint = _blueprint(tmp_path, lean={"determined": "Skel.observation_determined"}) + article = blueprint / "roadmap" / "basics" / "determined.md" + article.write_bytes( + b"---\r\nlean: Skel.observation_determined\r\n---\r\n\r\n# determined\r\n\r\n" + b"Every \r\nobservation is determined.\t\r\n\r\n## Depends on\r\n\r\nNone.\r\n\r\n" + b"## Sources\r\n\r\n- Chapter 1\r\n" + ) + statement = article_statement(load_graph(blueprint).nodes["basics/determined"]) + assert statement == "Every\nobservation is determined." + + article.write_text( + "---\nlean: Skel.observation_determined\n---\n\n# determined\n\n" + "Every\nobservation is determined.\n\n## Sources\n\n- Chapter 2, a different citation\n", + encoding="utf-8", + ) + assert article_statement(load_graph(blueprint).nodes["basics/determined"]) == statement + + +def test_report_records_the_statement_text_its_hash_binds(tmp_path: Path) -> None: + report = _fake_report(tmp_path) + path = tmp_path / "skeleton.json" + node = report.as_dict()["nodes"][0] + assert (node["statement_text"], node["statement_hash"]) == ("A statement.", report.nodes[0].statement_hash) + + payload = report.as_dict() + payload["nodes"][0]["statement_text"] = "A different statement." + _assert_load_rejects(path, payload, "not a canonical") + + payload = report.as_dict() + payload["nodes"][0]["statement_text"] = None + _assert_load_rejects(path, payload, "invalid statement text") def _cli(tmp_path: Path, monkeypatch, *arguments: object) -> int: @@ -1680,6 +1759,111 @@ def fake_run_probe(probe: str, root: Path, *, timeout: float) -> str: assert "expected a positive number of seconds" in capsys.readouterr().err +def _record_statement_hash(blueprint: Path, stem: str, statement_hash: str) -> Path: + """Record ``statement: formalized`` and ``statement_hash`` on one ``_blueprint`` article.""" + + article = blueprint / "roadmap" / "basics" / f"{stem}.md" + text = article.read_text(encoding="utf-8") + article.write_text( + text.replace("---\n\n#", f"statement: formalized\nstatement_hash: {statement_hash}\n---\n\n#", 1), + encoding="utf-8", + ) + return article + + +def _current_statement_hash(blueprint: Path, project: Path, node_id: str, capsys) -> str | None: + main(["skeleton", str(blueprint), "--lean-root", str(project), "--node", node_id, "--json"]) + (node,) = json.loads(capsys.readouterr().out)["nodes"] + return node["statement_hash"] + + +def test_cli_check_statements_skips_lean_when_no_article_records_a_hash( + tmp_path: Path, capsys, monkeypatch +) -> None: + project = _project(tmp_path) + blueprint = _blueprint(tmp_path, lean={"determined": "Skel.observation_determined"}) + + def no_probe(probe: str, root: Path) -> str: + raise AssertionError("the probe must not run") + + monkeypatch.setattr("autoform_cli.skeleton.run_probe", no_probe) + command = ["skeleton", str(blueprint), "--lean-root", str(project), "--check-statements"] + + assert main(command) == 0 + assert capsys.readouterr().out == "no article records statement_hash; nothing to check\n" + assert main([*command, "--json"]) == 2 + assert "--check-statements does not combine with" in capsys.readouterr().err + + +def test_cli_check_statements_fails_on_a_changed_statement(tmp_path: Path, capsys, monkeypatch) -> None: + project = _project(tmp_path) + blueprint = _blueprint(tmp_path, lean={"determined": "Skel.observation_determined"}) + monkeypatch.setattr("autoform_cli.skeleton.run_probe", lambda probe, root: _fake_probe_output()) + command = ["skeleton", str(blueprint), "--lean-root", str(project), "--check-statements"] + recorded = _current_statement_hash(blueprint, project, "basics/determined", capsys) + assert recorded is not None + article = _record_statement_hash(blueprint, "determined", recorded) + + assert main(command) == 0 + assert capsys.readouterr().out == "1 recorded statement hash(es) match\n" + assert main(["skeleton", str(blueprint), "--lean-root", str(project)]) == 0 + assert f"== basics/determined · statement_hash {recorded}\n" in capsys.readouterr().out + + article.write_text( + article.read_text(encoding="utf-8").replace("A statement.", "A stronger statement."), encoding="utf-8" + ) + current = _current_statement_hash(blueprint, project, "basics/determined", capsys) + assert current not in {None, recorded} + + assert main(command) == 1 + captured = capsys.readouterr() + assert captured.out == "" + assert captured.err.splitlines() == [ + f"error: basics/determined: statement_hash {recorded} is recorded but the statement now hashes to " + f"{current}; re-review the statement and record the new hash" + ] + + +def test_cli_check_statements_fails_when_a_recorded_hash_cannot_be_computed( + tmp_path: Path, capsys, monkeypatch +) -> None: + project = _project(tmp_path) + blueprint = _blueprint( + tmp_path, + lean={"determined": "Skel.observation_determined", "phantom": "Skel.doesNotExist", "plain": "Skel.plain"}, + ) + monkeypatch.setattr("autoform_cli.skeleton.run_probe", lambda probe, root: _fake_probe_output()) + _record_statement_hash(blueprint, "phantom", "sha256:" + "0" * 64) + unnamed = _record_statement_hash(blueprint, "plain", "sha256:" + "1" * 64) + unnamed.write_text(unnamed.read_text(encoding="utf-8").replace("lean: Skel.plain\n", ""), encoding="utf-8") + + assert main(["skeleton", str(blueprint), "--lean-root", str(project), "--check-statements"]) == 1 + + assert capsys.readouterr().err.splitlines() == [ + "error: basics/phantom: statement_hash cannot be checked: " + "Skel.doesNotExist: declaration not found in the Lean sources", + "error: basics/plain: statement_hash is recorded but the article names no lean: declaration", + ] + + +def test_cli_check_statements_sets_the_probe_timeout(tmp_path: Path, capsys, monkeypatch) -> None: + project = _project(tmp_path) + blueprint = _blueprint(tmp_path, lean={"determined": "Skel.observation_determined"}) + _record_statement_hash(blueprint, "determined", "sha256:" + "0" * 64) + timeouts: list[float] = [] + + def fake_run_probe(probe: str, root: Path, *, timeout: float) -> str: + timeouts.append(timeout) + return _fake_probe_output() + + monkeypatch.setattr("autoform_cli.__main__.run_probe", fake_run_probe) + command = ["skeleton", str(blueprint), "--lean-root", str(project), "--check-statements"] + + assert main([*command, "--timeout", "1800"]) == 1 + assert timeouts == [1800.0] + assert "re-review the statement and record the new hash" in capsys.readouterr().err + + def test_cli_reports_extraction_failures_on_stderr(tmp_path: Path, capsys) -> None: blueprint = _blueprint(tmp_path, lean={"determined": "Skel.observation_determined"}) @@ -2054,6 +2238,47 @@ def test_the_probe_reads_a_built_project(tmp_path: Path) -> None: extract_skeletons(blueprint, lean_root=project) +@pytest.mark.skipif(not _lean_toolchain_available(), reason="needs lake and the fixture's Lean toolchain") +def test_statement_hash_survives_a_proof_and_catches_a_type_edit(tmp_path: Path) -> None: + project = _project(tmp_path) + _build(project, "Skel.Main") + blueprint = _blueprint(tmp_path, lean={"determined": "Skel.observation_determined"}) + + def extract() -> NodeSkeleton: + report = extract_skeletons(blueprint, lean_root=project) + assert report.clean + return report.nodes[0] + + before = extract() + recorded = before.statement_hash + assert recorded is not None and extract().statement_hash == recorded + _record_statement_hash(blueprint, "determined", recorded) + assert check_statement_hashes(blueprint, lean_root=project) == (1, ()) + + # Proving the theorem drops `sorryAx`: the drift hash moves, the statement hash does not. + main_lean = project / "Skel" / "Main.lean" + _replace_source(main_lean, " sorry\n", " obtain ⟨y, hy⟩ := o.nonempty\n exact ⟨y, hy, fun z hz => h z y hz hy⟩\n") + _build(project, "Skel.Main") + proved = extract() + assert proved.declarations[0].axioms == () and proved.hash != before.hash + assert proved.statement_hash == recorded + assert check_statement_hashes(blueprint, lean_root=project) == (1, ()) + + # A type edit that still compiles is caught. + _replace_source(main_lean, "∀ z, o.admits z → z = y := by", "∀ z, o.admits z → y = z := by") + _replace_source(main_lean, "h z y hz hy⟩", "h y z hy hz⟩") + _build(project, "Skel.Main") + edited = extract().statement_hash + assert edited not in {None, recorded} + assert check_statement_hashes(blueprint, lean_root=project) == ( + 1, + ( + f"basics/determined: statement_hash {recorded} is recorded but the statement now hashes to " + f"{edited}; re-review the statement and record the new hash", + ), + ) + + @pytest.mark.skipif(not _lean_toolchain_available(), reason="needs lake and the fixture's Lean toolchain") def test_probe_records_bypass_the_command_capture_and_other_output(tmp_path: Path) -> None: # Lean holds a command's `IO.println` output until the command ends, then