"
+ ) in top
+ # Only the conditional proof carries the row; the open statement assumes nothing.
+ assert page.count('
') == 1
+
+ css = (tmp_path / "out/stylesheets/blueprint.css").read_text(encoding="utf-8")
+ assert ".bp-ref-conditional::before, .bp-swatch-conditional { background: #E9DFFC; border-color: #6B3FCF; }" in css
+ assert "[data-md-color-scheme=slate] .bp-ref-conditional::before" in css
+ assert ".bp-conditional .bp-mark { color: #6B3FCF; }" in css
+
+
+def test_the_strict_policy_shows_the_same_proof_as_proved_with_no_assumptions(tmp_path: Path) -> None:
+ project = _conditional_project(tmp_path, "forbidden")
+
+ render_site(project / "blueprint", tmp_path / "out", lean_root=project)
+ page = (tmp_path / "out/roadmap/README.md").read_text(encoding="utf-8")
+
+ assert '
Assumes' not in page
diff --git a/tests/test_runtime.py b/tests/test_runtime.py
index 247419ea..f67c09ae 100644
--- a/tests/test_runtime.py
+++ b/tests/test_runtime.py
@@ -284,3 +284,61 @@ def test_adapter_rejects_inconsistent_hand_built_graph_without_host_paths(tmp_pa
"chapter/section/base: dependency union does not match typed dependencies",
)
assert str(tmp_path) not in str(error.value)
+
+
+def _policy_project(tmp_path: Path, policy: str | None) -> Path:
+ """`_project` plus an open theorem, a reduction proved from it, and a statement waiting on a gap."""
+ project = _project(tmp_path)
+ if policy is not None:
+ _article(project, "README.md", title="Roadmap", open_statements=policy)
+ theorem = {"declaration": "theorem", "statement": "formalized"}
+ _article(project, "chapter/section/open.md", title="Open", lean="Project.open_thm", **theorem)
+ _article(
+ project,
+ "chapter/section/reduction.md",
+ title="Reduction",
+ lean="Project.reduction",
+ proof="formalized",
+ proof_dependencies=("open.md",),
+ **theorem,
+ )
+ _article(project, "chapter/section/gap.md", title="Gap", declaration="theorem")
+ _article(project, "chapter/section/waiting.md", title="Waiting", proof_dependencies=("gap.md",), **theorem)
+ return project
+
+
+def _status_payloads(project: Path) -> tuple[bool, dict[str, dict[str, object]]]:
+ payload = json.loads(load_runtime_graph(project).to_json())
+ return payload["open_statements"], {
+ node["id"].removeprefix("chapter/section/"): node["status"] for node in payload["nodes"]
+ }
+
+
+def test_strict_runtime_readiness_comes_from_the_derived_status(tmp_path: Path) -> None:
+ """Runtime readiness once ignored proof prerequisites that `work list` enforced."""
+ open_statements, statuses = _status_payloads(_policy_project(tmp_path, None))
+
+ assert open_statements is False
+ reduction = statuses["reduction"]
+ assert (reduction["state"], reduction["can_state"], reduction["can_prove"]) == ("proved", False, False)
+ assert (reduction["assumes"], reduction["waiting_on"]) == ([], [])
+ waiting = statuses["waiting"]
+ assert (waiting["state"], waiting["can_state"], waiting["can_prove"]) == ("stated", False, False)
+ assert waiting["waiting_on"] == ["chapter/section/gap"]
+ assert all(status["assumes"] == [] for status in statuses.values())
+
+
+def test_open_runtime_records_the_policy_and_what_each_proof_assumes(tmp_path: Path) -> None:
+ open_statements, statuses = _status_payloads(_policy_project(tmp_path, "allowed"))
+
+ assert open_statements is True
+ reduction = statuses["reduction"]
+ assert (reduction["state"], reduction["can_state"], reduction["can_prove"]) == ("conditional", True, True)
+ assert reduction["assumes"] == ["chapter/section/open"]
+ assert reduction["waiting_on"] == []
+ assert not reduction["fully_proved"]
+ waiting = statuses["waiting"]
+ assert (waiting["state"], waiting["can_state"], waiting["can_prove"]) == ("stated", True, False)
+ assert (waiting["assumes"], waiting["waiting_on"]) == ([], ["chapter/section/gap"])
+ assert statuses["open"]["state"] == "can_prove"
+ assert statuses["open"]["assumes"] == []
diff --git a/tests/test_status.py b/tests/test_status.py
index 0fad04b4..68ee4195 100644
--- a/tests/test_status.py
+++ b/tests/test_status.py
@@ -4,8 +4,8 @@
import pytest
-from autoform_cli.graph import load_graph
-from autoform_cli.status import derive, summarize
+from autoform_cli.graph import Graph, Node, load_graph
+from autoform_cli.status import NodeStatus, derive, summarize
def _node(blueprint: Path, relative: str, body: str = "", **metadata: str) -> None:
@@ -172,3 +172,163 @@ def test_assumptions_and_propositions_keep_the_proof_obligation(
_node(blueprint, "d.md", declaration=declaration, statement="formalized")
assert not derive(load_graph(blueprint))["d"].proved
+
+
+def _mixed_statuses(blueprint: Path, policy: str) -> dict[str, NodeStatus]:
+ """One graph with every kind of node the two policies treat differently.
+
+ ``hidden``, ``open``, ``inner`` and ``side`` are open statements: stated
+ theorems with no Lean proof. ``reduction`` and ``top`` are proved on top of
+ them, ``up`` is in Mathlib, and ``gap`` and ``bridge`` are not stated.
+ """
+ _node(blueprint, "README.md", open_statements=policy)
+ _node(blueprint, "kind.md", declaration="def", statement="formalized")
+ theorem = {"declaration": "theorem"}
+ stated = {**theorem, "statement": "formalized"}
+ proved = {**stated, "proof": "formalized"}
+ _node(blueprint, "lemma.md", "## Depends on\n\n- [Kind](kind.md)\n", **proved)
+ _node(blueprint, "hidden.md", **stated)
+ _node(blueprint, "up.md", "## Depends on\n\n- [Hidden](hidden.md)\n", **theorem, mathlib="true")
+ _node(blueprint, "open.md", "## Depends on\n\n- [Kind](kind.md)\n", **stated)
+ _node(
+ blueprint,
+ "reduction.md",
+ "## Depends on\n\n- [Lemma](lemma.md)\n\n## Proof depends on\n\n- [Open](open.md)\n",
+ **proved,
+ )
+ _node(blueprint, "gap.md", **theorem)
+ _node(blueprint, "inner.md", **stated)
+ _node(blueprint, "side.md", **stated)
+ _node(
+ blueprint,
+ "outer.md",
+ "## Depends on\n\n- [Inner](inner.md)\n\n## Proof depends on\n\n- [Side](side.md)\n",
+ **stated,
+ )
+ _node(blueprint, "bridge.md", "## Depends on\n\n- [Open](open.md)\n", **theorem)
+ _node(
+ blueprint,
+ "top.md",
+ "## Depends on\n\n- [Up](up.md)\n\n## Proof depends on\n\n- [Outer](outer.md)\n- [Bridge](bridge.md)\n",
+ **proved,
+ )
+ _node(
+ blueprint,
+ "waits.md",
+ "## Depends on\n\n- [Gap](gap.md)\n\n## Proof depends on\n\n- [Gap](gap.md)\n- [Bridge](bridge.md)\n",
+ **theorem,
+ )
+ _node(
+ blueprint,
+ "pending.md",
+ "## Proof depends on\n\n- [Gap](gap.md)\n- [Reduction](reduction.md)\n",
+ **stated,
+ )
+ return derive(load_graph(blueprint))
+
+
+def _readiness(
+ statuses: dict[str, NodeStatus],
+) -> dict[str, tuple[str, bool, bool, tuple[str, ...], tuple[str, ...]]]:
+ return {
+ node_id: (status.key, status.can_state, status.can_prove, status.waiting_on, status.assumes)
+ for node_id, status in statuses.items()
+ }
+
+
+def test_the_strict_policy_waits_for_proof_prerequisites_to_be_proved(tmp_path: Path) -> None:
+ statuses = _mixed_statuses(tmp_path / "blueprint", "forbidden")
+
+ assert _readiness(statuses) == {
+ "roadmap": ("can_state", True, False, (), ()),
+ "kind": ("fully_proved", True, True, (), ()),
+ "lemma": ("fully_proved", True, True, (), ()),
+ "hidden": ("can_prove", True, True, (), ()),
+ "up": ("mathlib", True, True, (), ()),
+ "open": ("can_prove", True, True, (), ()),
+ # Proved, so nothing is waited on, but under this policy its unproved
+ # proof prerequisite would have kept the statement from landing.
+ "reduction": ("proved", False, False, (), ()),
+ "gap": ("can_state", True, False, (), ()),
+ "inner": ("can_prove", True, True, (), ()),
+ "side": ("can_prove", True, True, (), ()),
+ "outer": ("stated", False, False, ("side",), ()),
+ "bridge": ("can_state", True, False, (), ()),
+ "top": ("proved", False, False, (), ()),
+ # Unstated statement prerequisites first, then unproved proof ones, once each.
+ "waits": ("planned", False, False, ("gap", "bridge"), ()),
+ "pending": ("stated", False, False, ("gap",), ()),
+ }
+
+
+def test_the_open_policy_waits_only_for_prerequisites_to_be_stated(tmp_path: Path) -> None:
+ statuses = _mixed_statuses(tmp_path / "blueprint", "allowed")
+
+ assert _readiness(statuses) == {
+ "roadmap": ("can_state", True, False, (), ()),
+ "kind": ("fully_proved", True, True, (), ()),
+ "lemma": ("fully_proved", True, True, (), ()),
+ "hidden": ("can_prove", True, True, (), ()),
+ "up": ("mathlib", True, True, (), ()),
+ "open": ("can_prove", True, True, (), ()),
+ "reduction": ("conditional", True, True, (), ("open",)),
+ "gap": ("can_state", True, False, (), ()),
+ "inner": ("can_prove", True, True, (), ()),
+ "side": ("can_prove", True, True, (), ()),
+ "outer": ("can_prove", True, True, (), ("inner", "side")),
+ "bridge": ("can_state", True, False, (), ("open",)),
+ # can_prove reads the prerequisites, not the assertion: bridge is not stated.
+ "top": ("conditional", True, False, (), ("inner", "outer")),
+ # An unstated node waits only on its statement prerequisites.
+ "waits": ("planned", False, False, ("gap",), ()),
+ "pending": ("stated", True, False, ("gap",), ("open",)),
+ }
+
+
+@pytest.mark.parametrize("policy", ["forbidden", "allowed"])
+def test_a_fully_proved_node_assumes_nothing(tmp_path: Path, policy: str) -> None:
+ statuses = _mixed_statuses(tmp_path / "blueprint", policy)
+
+ fully_proved = {node_id for node_id, status in statuses.items() if status.fully_proved}
+ assert fully_proved == {"kind", "lemma"}
+ assert all(status.assumes == () for status in statuses.values() if status.fully_proved)
+
+
+def test_assumptions_reach_what_the_lean_proof_can_reach(tmp_path: Path) -> None:
+ """``top`` rests on ``up``, ``outer`` and ``bridge``, and each stops the walk differently.
+
+ Mathlib ``up`` is upstream, so ``hidden`` behind it is not reached. ``bridge``
+ is not stated, so it has no Lean declaration to lead to ``open``. ``outer``
+ is open: its own sorry and its statement prerequisite ``inner`` are reached,
+ but ``side``, which only its missing proof would use, is not.
+ """
+ statuses = _mixed_statuses(tmp_path / "blueprint", "allowed")
+
+ assert statuses["top"].assumes == ("inner", "outer")
+ # The walk stops at bridge for its dependents, but bridge's own proof would
+ # still rest on open. A Mathlib node rests on nothing.
+ assert statuses["bridge"].assumes == ("open",)
+ assert statuses["up"].assumes == ()
+
+
+@pytest.mark.parametrize("open_statements", [False, True])
+def test_a_missing_dependency_counts_as_neither_stated_nor_proved(
+ tmp_path: Path, open_statements: bool
+) -> None:
+ node = Node(
+ id="result",
+ title="Result",
+ path=tmp_path / "result.md",
+ dependencies=("ghost", "phantom"),
+ statement_dependencies=("ghost",),
+ proof_dependencies=("phantom",),
+ declaration="theorem",
+ statement_formalized=True,
+ )
+ graph = Graph(blueprint_dir=tmp_path, nodes={"result": node}, open_statements=open_statements)
+
+ status = derive(graph)["result"]
+
+ assert (status.key, status.can_state, status.can_prove) == ("stated", False, False)
+ assert status.waiting_on == ("ghost", "phantom")
+ assert status.assumes == ()
diff --git a/tests/test_visualization.py b/tests/test_visualization.py
index a85dda67..85d6af3c 100644
--- a/tests/test_visualization.py
+++ b/tests/test_visualization.py
@@ -132,6 +132,27 @@ def test_green_stops_at_an_unproved_prerequisite(tmp_path: Path) -> None:
assert statuses["top"].key == "proved"
+def test_a_conditional_proof_has_its_own_colour_and_legend_entry(tmp_path: Path) -> None:
+ """A proof resting on a sorry must not share the fully proved green."""
+ blueprint = tmp_path / "blueprint"
+ _write_node(blueprint / "roadmap" / "README.md", "Roadmap", open_statements="allowed")
+ _write_node(blueprint / "roadmap" / "open.md", "Open", declaration="theorem", statement="formalized")
+ _write_node(
+ blueprint / "roadmap" / "top.md",
+ "Top",
+ [("Open", "open.md")],
+ declaration="theorem",
+ statement="formalized",
+ proof="formalized",
+ )
+
+ document = export_graph(blueprint).read_text(encoding="utf-8")
+
+ assert '("Top"):::conditional' in document
+ assert f"classDef conditional fill:{_state('conditional').fill}" in document
+ assert '
' in document
+ assert "Proof compiles, but rests on an open statement whose Lean proof is still sorry." in document
+
def test_cli_writes_only_the_graph_by_default(
tmp_path: Path, capsys: pytest.CaptureFixture[str]
) -> None:
diff --git a/tests/test_work.py b/tests/test_work.py
index efc094c1..a13c7310 100644
--- a/tests/test_work.py
+++ b/tests/test_work.py
@@ -325,19 +325,22 @@ def test_work_cli_emits_stable_json(tmp_path: Path, capsys) -> None:
assert cli.main(["work", "list", str(project), "--lean-root", str(project), "--json"]) == 0
frontier = json.loads(capsys.readouterr().out)
- assert set(frontier) == {"items", "schema", "source_revision"}
+ assert set(frontier) == {"items", "open_statements", "schema", "source_revision"}
assert frontier["schema"] == WORK_SCHEMA
+ assert frontier["open_statements"] is False
assert frontier["source_revision"] == source_revision
assert [item["phase"] for item in frontier["items"]] == ["proof", "statement"]
assert frontier["items"][0] == {
"article_id": "af_000000000000000000000003",
"article_path": "blueprint/roadmap/chapter/prove.md",
"article_revision": prove_revision,
+ "assumes": [],
"blockers": [],
"claim_target": "af_000000000000000000000003",
"dependencies": ["chapter/base"],
"lean_targets": [{"declaration": "Project.prove", "source_file": "Project.lean"}],
"node_id": "chapter/prove",
+ "open_statements": False,
"phase": "proof",
"ready": True,
"source_targets": [],
@@ -481,3 +484,335 @@ def test_node_ids_cannot_impersonate_article_ids(tmp_path: Path, capsys) -> None
assert cli.main(["work", "context", "af_000000000000000000000002", str(project)]) == 2
assert "node id has the form of an article_id" in capsys.readouterr().err
+
+
+def _policy_project(tmp_path: Path, policy: str | None) -> Path:
+ """`_project` plus an open theorem, a reduction proved from it, and articles resting on them.
+
+ *policy* is the `open_statements` value in `roadmap/README.md`; ``None``
+ writes no roadmap page, so the project keeps the default strict policy.
+ """
+ project = _project(tmp_path)
+ if policy is not None:
+ (project / "blueprint/roadmap/README.md").write_text(
+ f"---\nopen_statements: {policy}\n---\n\n# Roadmap\n", encoding="utf-8"
+ )
+ stated = ["declaration: theorem", "statement: formalized"]
+ _article(
+ project,
+ "open.md",
+ title="Open",
+ metadata=["article_id: af_00000000000000000000000b", *stated, "lean: Project.open_thm Project.open_aux"],
+ depends="base.md",
+ )
+ _article(
+ project,
+ "reduction.md",
+ title="Reduction",
+ metadata=["article_id: af_00000000000000000000000c", *stated, "proof: formalized", "lean: Project.reduction"],
+ proof_depends="open.md",
+ )
+ _article(
+ project,
+ "uses.md",
+ title="Uses",
+ metadata=["article_id: af_00000000000000000000000d", *stated, "lean: Project.uses"],
+ depends="open.md",
+ )
+ _article(
+ project,
+ "corollary.md",
+ title="Corollary",
+ metadata=["article_id: af_00000000000000000000000e", "declaration: theorem"],
+ depends="reduction.md",
+ )
+ # Neither belongs in the assumption contract: one is upstream, the other names no declaration.
+ _article(
+ project,
+ "upstream.md",
+ title="Upstream",
+ metadata=["declaration: theorem", "mathlib: true", "lean: Project.upstream"],
+ )
+ _article(project, "unnamed.md", title="Unnamed", metadata=["declaration: def", "statement: formalized"])
+ return project
+
+
+def _blocked_articles(project: Path) -> None:
+ """Add articles whose prerequisites block them differently under the two policies."""
+ _article(
+ project,
+ "waits.md",
+ title="Waits",
+ metadata=["article_id: af_000000000000000000000010", "declaration: theorem"],
+ depends="state.md",
+ proof_depends="prove.md",
+ )
+ _edit(project, "waits.md", "- [dependency](prove.md)", "- [dependency](prove.md)\n- [dependency](state.md)")
+ _article(
+ project,
+ "stuck.md",
+ title="Stuck",
+ metadata=[
+ "article_id: af_000000000000000000000011",
+ "declaration: theorem",
+ "statement: formalized",
+ "lean: Project.stuck",
+ ],
+ depends="blocked.md",
+ proof_depends="prove.md",
+ )
+ _edit(project, "stuck.md", "- [dependency](prove.md)", "- [dependency](prove.md)\n- [dependency](state.md)")
+ _article(
+ project,
+ "main.md",
+ title="Main",
+ metadata=[
+ "article_id: af_000000000000000000000012",
+ "declaration: theorem",
+ "statement: formalized",
+ "lean: Project.main",
+ ],
+ proof_depends="prove.md",
+ )
+
+
+def _blockers(project: Path) -> dict[str, tuple[str | None, tuple[str, ...]]]:
+ selectors = ("chapter/waits", "chapter/stuck", "chapter/main")
+ items = {selector: work_context(project, selector)[1] for selector in selectors}
+ return {selector: (item.phase, item.blockers) for selector, item in items.items()}
+
+
+def test_strict_blockers_list_unstated_statement_prerequisites_then_unproved_proof_ones(
+ tmp_path: Path,
+) -> None:
+ project = _project(tmp_path)
+ _blocked_articles(project)
+
+ assert _blockers(project) == {
+ "chapter/waits": (None, ("chapter/state", "chapter/prove")),
+ "chapter/stuck": (None, ("chapter/blocked", "chapter/prove", "chapter/state")),
+ "chapter/main": (None, ("chapter/prove",)),
+ }
+
+
+def test_open_blockers_wait_only_for_prerequisites_to_be_stated(tmp_path: Path) -> None:
+ project = _project(tmp_path)
+ (project / "blueprint/roadmap/README.md").write_text(
+ "---\nopen_statements: allowed\n---\n\n# Roadmap\n", encoding="utf-8"
+ )
+ _blocked_articles(project)
+
+ assert _blockers(project) == {
+ # Unstated, so only its statement prerequisites can hold it back.
+ "chapter/waits": (None, ("chapter/state",)),
+ # Stated: prove is stated too, so only the unstated prerequisites remain.
+ "chapter/stuck": (None, ("chapter/blocked", "chapter/state")),
+ "chapter/main": ("proof", ()),
+ }
+ _, main = work_context(project, "chapter/main")
+ assert main.assumes == ("chapter/prove",)
+ assert "chapter/main" in {item.node_id for item in list_ready_work(project).items}
+
+
+def test_strict_work_text_is_unchanged(tmp_path: Path, capsys) -> None:
+ project = _policy_project(tmp_path, None)
+ revision = load_runtime_graph(project).source_revision
+ uses = hashlib.sha256((project / "blueprint/roadmap/chapter/uses.md").read_bytes()).hexdigest()
+
+ assert cli.main(["work", "list", str(project)]) == 0
+ assert capsys.readouterr().out == (
+ "statement: chapter/corollary [af_00000000000000000000000e] - Corollary\n"
+ "proof: chapter/open [af_00000000000000000000000b] - Open\n"
+ "proof: chapter/prove [af_000000000000000000000003] - Prove me\n"
+ "statement: chapter/state [af_000000000000000000000002] - State me\n"
+ "proof: chapter/uses [af_00000000000000000000000d] - Uses\n"
+ )
+
+ assert cli.main(["work", "context", "chapter/uses", str(project)]) == 0
+ assert capsys.readouterr().out == (
+ "Uses (chapter/uses)\n"
+ "State: can_prove\n"
+ "Phase: proof\n"
+ "Claim target: af_00000000000000000000000d\n"
+ "Article: blueprint/roadmap/chapter/uses.md\n"
+ f"Article revision: {uses}\n"
+ f"Graph source revision: {revision}\n"
+ "Dependencies: chapter/open\n"
+ "Lean: Project.uses\n"
+ )
+
+
+def test_open_work_text_names_the_policy_and_what_each_item_assumes(tmp_path: Path, capsys) -> None:
+ project = _policy_project(tmp_path, "allowed")
+ revision = load_runtime_graph(project).source_revision
+ uses = hashlib.sha256((project / "blueprint/roadmap/chapter/uses.md").read_bytes()).hexdigest()
+
+ assert cli.main(["work", "list", str(project)]) == 0
+ assert capsys.readouterr().out == (
+ "Open statements: allowed (a statement may land with a sorry proof)\n"
+ "statement: chapter/corollary [af_00000000000000000000000e] - Corollary\n"
+ " assumes: chapter/open\n"
+ "proof: chapter/open [af_00000000000000000000000b] - Open\n"
+ "proof: chapter/prove [af_000000000000000000000003] - Prove me\n"
+ "statement: chapter/state [af_000000000000000000000002] - State me\n"
+ "proof: chapter/uses [af_00000000000000000000000d] - Uses\n"
+ " assumes: chapter/open\n"
+ )
+
+ assert cli.main(["work", "context", "chapter/uses", str(project)]) == 0
+ assert capsys.readouterr().out == (
+ "Uses (chapter/uses)\n"
+ "State: can_prove\n"
+ "Phase: proof\n"
+ "Open statements: allowed\n"
+ "Assumes: chapter/open\n"
+ "Claim target: af_00000000000000000000000d\n"
+ "Article: blueprint/roadmap/chapter/uses.md\n"
+ f"Article revision: {uses}\n"
+ f"Graph source revision: {revision}\n"
+ "Dependencies: chapter/open\n"
+ "Lean: Project.uses\n"
+ )
+
+ assert cli.main(["work", "context", "chapter/prove", str(project)]) == 0
+ context = capsys.readouterr().out.splitlines()
+ assert "Open statements: allowed" in context
+ assert not any(line.startswith("Assumes:") for line in context)
+
+ assert cli.main(["work", "list", str(project), "--json"]) == 0
+ frontier = json.loads(capsys.readouterr().out)
+ assert frontier["open_statements"] is True
+ assert {item["node_id"]: item["assumes"] for item in frontier["items"]} == {
+ "chapter/corollary": ["chapter/open"],
+ "chapter/open": [],
+ "chapter/prove": [],
+ "chapter/state": [],
+ "chapter/uses": ["chapter/open"],
+ }
+ assert all(item["open_statements"] is True for item in frontier["items"])
+
+
+def _contract_article(
+ node_id: str,
+ article_id: str,
+ state: str,
+ declarations: list[str],
+ *,
+ open_: bool = False,
+ assumes: tuple[str, ...] = (),
+ allowed: tuple[str, ...] = (),
+) -> dict[str, object]:
+ return {
+ "allowed_open_declarations": list(allowed),
+ "article_id": article_id,
+ "assumes": list(assumes),
+ "declarations": declarations,
+ "id": node_id,
+ "open": open_,
+ "state": state,
+ }
+
+
+def test_work_assumptions_under_the_strict_policy_lists_articles_with_nothing_open(
+ tmp_path: Path, capsys
+) -> None:
+ project = _policy_project(tmp_path, "forbidden")
+
+ assert cli.main(["work", "assumptions", str(project), "--json"]) == 0
+ output = capsys.readouterr().out
+ contract = json.loads(output)
+ assert output == json.dumps(contract, sort_keys=True, separators=(",", ":")) + "\n"
+ assert contract == {
+ "schema": work_module.ASSUMPTIONS_SCHEMA,
+ "open_statements": False,
+ "source_revision": load_runtime_graph(project).source_revision,
+ "articles": [
+ _contract_article("chapter/base", "af_000000000000000000000001", "fully_proved", ["Project.base"]),
+ _contract_article(
+ "chapter/open", "af_00000000000000000000000b", "can_prove", ["Project.open_thm", "Project.open_aux"]
+ ),
+ _contract_article("chapter/prove", "af_000000000000000000000003", "can_prove", ["Project.prove"]),
+ _contract_article("chapter/reduction", "af_00000000000000000000000c", "proved", ["Project.reduction"]),
+ _contract_article("chapter/uses", "af_00000000000000000000000d", "can_prove", ["Project.uses"]),
+ ],
+ }
+
+ assert cli.main(["work", "assumptions", str(project)]) == 0
+ assert capsys.readouterr().out == "Open statements: forbidden\n"
+
+
+def test_work_assumptions_under_the_open_policy_bounds_each_article(
+ tmp_path: Path, capsys, monkeypatch: pytest.MonkeyPatch
+) -> None:
+ project = _policy_project(tmp_path, "allowed")
+ open_declarations = ("Project.open_aux", "Project.open_thm")
+
+ assert cli.main(["work", "assumptions", str(project), "--json"]) == 0
+ contract = json.loads(capsys.readouterr().out)
+ assert contract == {
+ "schema": "autoform-assumptions/v1",
+ "open_statements": True,
+ "source_revision": load_runtime_graph(project).source_revision,
+ "articles": [
+ _contract_article("chapter/base", "af_000000000000000000000001", "fully_proved", ["Project.base"]),
+ # Declarations keep their authored order; the allowance is sorted.
+ _contract_article(
+ "chapter/open",
+ "af_00000000000000000000000b",
+ "can_prove",
+ ["Project.open_thm", "Project.open_aux"],
+ open_=True,
+ allowed=open_declarations,
+ ),
+ _contract_article(
+ "chapter/prove",
+ "af_000000000000000000000003",
+ "can_prove",
+ ["Project.prove"],
+ open_=True,
+ allowed=("Project.prove",),
+ ),
+ _contract_article(
+ "chapter/reduction",
+ "af_00000000000000000000000c",
+ "conditional",
+ ["Project.reduction"],
+ assumes=("chapter/open",),
+ allowed=open_declarations,
+ ),
+ _contract_article(
+ "chapter/uses",
+ "af_00000000000000000000000d",
+ "can_prove",
+ ["Project.uses"],
+ open_=True,
+ assumes=("chapter/open",),
+ allowed=(*open_declarations, "Project.uses"),
+ ),
+ ],
+ }
+
+ monkeypatch.chdir(project)
+ assert cli.main(["work", "assumptions", "--json"]) == 0
+ assert json.loads(capsys.readouterr().out) == contract
+
+ assert cli.main(["work", "assumptions", str(project / "blueprint")]) == 0
+ assert capsys.readouterr().out == (
+ "Open statements: allowed\n"
+ "open: chapter/open (Project.open_thm, Project.open_aux)\n"
+ "open: chapter/prove (Project.prove)\n"
+ "conditional: chapter/reduction assumes chapter/open\n"
+ "open: chapter/uses (Project.uses)\n"
+ "conditional: chapter/uses assumes chapter/open\n"
+ )
+
+
+def test_work_assumptions_reports_errors_on_stderr_with_exit_2(tmp_path: Path, capsys) -> None:
+ assert cli.main(["work", "assumptions", str(tmp_path / "missing")]) == 2
+ assert capsys.readouterr().err == "error: project or blueprint directory does not exist\n"
+
+ project = _policy_project(tmp_path, "maybe")
+ assert cli.main(["work", "assumptions", str(project), "--json"]) == 2
+ captured = capsys.readouterr()
+ assert captured.out == ""
+ assert captured.err == "error: roadmap:2: 'open_statements' accepts allowed or forbidden\n"
From ce0c1235ef3e6a7f5155f0c47f5bdde3a2ab4300 Mon Sep 17 00:00:00 2001
From: Jack McCarthy <37917934+Deicyde@users.noreply.github.com>
Date: Mon, 5 Oct 2026 05:31:52 -0400
Subject: [PATCH 02/38] Pin readiness wording, Assumes row order and the empty
open frontier
Nothing pinned the reworded legend meanings for can_prove and can_state
or the policy-neutral Next up explanations, so add a legend test and a
landing-page test for both phases. The conditional article test now
checks that the Assumes row sits after the Lean row and before
Discussion, as spec A3 places it. Under the open policy, `work list`
names the policy even when nothing is ready; a test covers that branch.
Also restore the two blank lines after the conditional legend test.
---
tests/test_render.py | 25 +++++++++++++++++++++++++
tests/test_visualization.py | 15 +++++++++++++++
tests/test_work.py | 14 ++++++++++++++
3 files changed, 54 insertions(+)
diff --git a/tests/test_render.py b/tests/test_render.py
index ae5cfea8..cee93485 100644
--- a/tests/test_render.py
+++ b/tests/test_render.py
@@ -1315,6 +1315,9 @@ def test_a_conditional_proof_names_the_open_statements_it_assumes(tmp_path: Path
) in top
# Only the conditional proof carries the row; the open statement assumes nothing.
assert page.count('Assumes') == 1
+ # The row follows the implementation row and precedes Discussion.
+ meta = top[top.index('