diff --git a/telperion/docs/CROSS_CAMPAIGN_EDGES_2026-09-19.md b/telperion/docs/CROSS_CAMPAIGN_EDGES_2026-09-19.md new file mode 100644 index 000000000..f5628d391 --- /dev/null +++ b/telperion/docs/CROSS_CAMPAIGN_EDGES_2026-09-19.md @@ -0,0 +1,97 @@ +# Cross-campaign dependency edges in the missions registry (2026-09-19) + +*`conjecture1_proved = False`. This is registry plumbing, not mathematics.* + +## The problem + +`load_campaign` rejected any `depends_on` target outside its own campaign. The +corpus is emphatically cross-campaign: mirrormere's Route-D nodes consume rh's +`E6Bridge*` results on the `rvm_bridge` island. With no way to say so, authors +reached for the nearest same-campaign proxy while the node title named the real +source, and the 2026-09-18 registry audit found **five nodes whose dependency +edges the corpus does not support**. The audit also found that all 44 live proof +links are `via = direct`: the `reduction` mechanism, the one that actually +consumes dependency edges, had never been used once. + +So the registry has been recording a chain of reductions toward a conjecture +while in fact holding a collection of independent direct proofs. The edges were +decorative. This change makes them mean something, which is also what makes it +dangerous, hence the emphasis below. + +## The mechanism + +A `depends_on` entry is now one of: + +| form | meaning | +|---|---| +| `RH_corridor_bound` | a node in the same campaign (unchanged, still the default) | +| `rh:RH_corridor_bound` | the node `RH_corridor_bound` in the campaign whose **directory** is `rh` | + +The campaign part is the directory name, not `manifest.name`: the directory is +what `--campaign` takes and what a reference must resolve against (`rh`, not +`RH.conjecture`). + +Three layers, deliberately separated: + +1. **`load_campaign(root)`** validates internal references exactly as before. An + external reference is checked for *syntax* and *file existence* only + (`/..//nodes/.toml`). It does not load the other + campaign, so there is no recursion and no load-order coupling. +2. **`load_universe(missions_root)`** loads every campaign, resolves every + external reference for real, and asserts **global** acyclicity. A cycle like + `rh:A -> mm:B -> rh:A` is invisible to any per-campaign check by + construction; this is the layer that sees it. +3. **`compute_universe_closures(universe)`** runs one global closure fixpoint + keyed by `(campaign, slug)`. + +`verify_campaign` auto-loads the sibling universe when it can, and falls back to +`None` when it cannot, which leaves every external edge dirty. + +## The anti-cascade rule + +A cross-campaign edge is a new path for an unverified premise to reach a +`proved` node. The 2026-09-18 audit *demonstrated*, on a throwaway campaign, +that the gate could mark a node proved from a stub. So the rule here is stated +as a single invariant and tested from the negative side: + +> An edge counts toward a clean closure only when its target genuinely +> resolves, has status `proved`, **and** is itself closure-clean under the +> global fixpoint. Every other case is dirty. There is no code path that turns +> an unresolved, unproved, or dirty edge clean. + +Two specific traps, both of which bit during implementation and are now tests: + +- **No universe, external edge.** Returns dirty. A caller who forgets to pass + the universe gets a conservative answer, never an optimistic one. +- **Never trust the target's stored flag.** The first implementation fell back + to the external node's stored `closure_clean` when no global pass was + available. That is exactly how transitive dirt launders across a boundary: a + reduction node's stored flag can read `True` while its own chain is dirty. + `test_transitive_dirt_propagates_across_campaigns` caught it. The fallback is + gone; the global fixpoint is computed instead. + +Note that a **direct** proof is unaffected by its dependency edges, by design: +it stands on its artifact and the gate that checked it. Edges constrain +`reduction` proofs. That asymmetry is why the registry could accumulate +unsupported edges without any node becoming falsely clean. + +## What this does not do + +- It does not fix the five unsupported edges. Only one of them + (`MM_weil_form_certified_height`, which needs `rh:RH_rvm_unconditional`) is a + genuine cross-campaign case, and it lives on an unmerged branch. The other + four are dependency-correctness questions the mechanism cannot settle: a node + whose title refutes its own edges needs an author's judgement, not a syntax. +- It does not make anything proved, and no node's status changes here. +- It does not retro-fit `via = reduction` anywhere. The reduction relation is + now usable across campaigns; whether a given proof is a reduction remains a + claim its author must make and the gate must check. + +## Tests + +`tests/test_missions_cross_campaign.py`, 19 tests, most of them negative: +malformed references, missing target, missing campaign, internal validation +unchanged, global cycle detection, and six closure cases covering unproved, +proved-but-dirty, no-universe, transitive dirt, and the direct-proof asymmetry. +The full mission subset stays green at 331 passed, and all four real campaigns +load as a universe and verify OK. diff --git a/telperion/src/telperion/missions/registry.py b/telperion/src/telperion/missions/registry.py index 92d9f8496..8390491e7 100644 --- a/telperion/src/telperion/missions/registry.py +++ b/telperion/src/telperion/missions/registry.py @@ -45,6 +45,59 @@ class Campaign: manifest: MissionManifest nodes: Dict[str, Node] # keyed by slug + @property + def cname(self) -> str: + """The campaign's on-disk directory name -- its identity in a dep ref. + + Deliberately the directory name, not ``manifest.name``: the directory is + what the CLI's ``--campaign`` takes and what a cross-campaign reference + must resolve against (``rh``, not ``RH.conjecture``). + """ + return self.root.name + + +# --------------------------------------------------------------------------- +# Cross-campaign dependency references +# +# A depends_on entry is either a bare slug (same campaign, unchanged) or a +# qualified reference ":", e.g. "rh:RH_rvm_unconditional". +# The qualified form exists because real dependencies cross campaigns: the +# mirrormere D3 node genuinely needs the rh cumulative-RvM theorem. Before this +# existed, authors substituted a same-campaign proxy while the node title named +# the real source, which put five unsupported edges in the registry. +# --------------------------------------------------------------------------- + +DEP_SEP = ":" + + +def parse_dep(dep: str, home: str) -> tuple: + """Split a depends_on entry into ``(campaign_dir, slug)``. + + ``home`` is the referring campaign's directory name, used for bare slugs. + Raises SchemaError on a malformed reference. + """ + if DEP_SEP not in dep: + if not dep: + raise SchemaError("empty depends_on entry") + return (home, dep) + camp, _, slug = dep.partition(DEP_SEP) + if not camp or not slug or DEP_SEP in slug: + raise SchemaError( + f"malformed cross-campaign reference {dep!r}; " + f"expected '{DEP_SEP}'" + ) + return (camp, slug) + + +def is_external(dep: str, home: str) -> bool: + """True iff *dep* names a node in a campaign other than *home*.""" + return parse_dep(dep, home)[0] != home + + +def dep_ref(campaign: str, slug: str) -> str: + """Render a qualified reference.""" + return f"{campaign}{DEP_SEP}{slug}" + # --------------------------------------------------------------------------- # Load @@ -75,13 +128,26 @@ def load_campaign(root: Path) -> Campaign: ) nodes[sl] = node - # Validate depends_on references + # Validate depends_on references. Internal refs must be present in this + # campaign; external refs are checked by file existence only -- resolving + # them fully would recurse across campaigns, so full cross-campaign + # validation (including global acyclicity) lives in load_universe. + home = root.name for sl, node in nodes.items(): for dep in node.depends_on: - if dep not in nodes: - raise SchemaError( - f"Node {sl!r} depends_on {dep!r} which is not in the campaign." - ) + camp, target = parse_dep(dep, home) + if camp == home: + if target not in nodes: + raise SchemaError( + f"Node {sl!r} depends_on {dep!r} which is not in the campaign." + ) + else: + ext = root.parent / camp / "nodes" / f"{target}.toml" + if not ext.is_file(): + raise SchemaError( + f"Node {sl!r} depends_on external {dep!r}, but no such node " + f"file exists at {ext}." + ) campaign = Campaign(root=root, manifest=manifest, nodes=nodes) assert_acyclic(campaign) @@ -92,6 +158,17 @@ def load_campaign(root: Path) -> Campaign: # DAG invariants # --------------------------------------------------------------------------- +def _internal_deps(campaign: Campaign, slug: str) -> List[str]: + """This node's same-campaign dependency slugs (external refs dropped).""" + home = campaign.cname + out = [] + for dep in campaign.nodes[slug].depends_on: + camp, target = parse_dep(dep, home) + if camp == home: + out.append(target) + return out + + def assert_acyclic(campaign: Campaign) -> None: """Raise SchemaError naming a cycle if the dependency graph is cyclic.""" # Iterative DFS with three-colour marking: 0=unvisited, 1=in-stack, 2=done @@ -102,7 +179,7 @@ def assert_acyclic(campaign: Campaign) -> None: if color[start] != WHITE: continue # DFS stack holds (slug, iterator-over-its-deps) - stack: List[tuple] = [(start, iter(campaign.nodes[start].depends_on))] + stack: List[tuple] = [(start, iter(_internal_deps(campaign, start)))] color[start] = GREY while stack: @@ -131,6 +208,102 @@ def assert_acyclic(campaign: Campaign) -> None: # Open-leaves query # --------------------------------------------------------------------------- + +# --------------------------------------------------------------------------- +# Universe: every campaign under one missions root, with cross-campaign edges +# --------------------------------------------------------------------------- + +@dataclass +class Universe: + root: Path + campaigns: Dict[str, Campaign] # keyed by directory name + + def resolve(self, home: str, dep: str) -> Optional[Node]: + """The Node a depends_on entry names, or None if it does not resolve. + + None is the conservative answer everywhere it is used: an edge that does + not resolve must never be treated as satisfied. + """ + camp, target = parse_dep(dep, home) + c = self.campaigns.get(camp) + if c is None: + return None + return c.nodes.get(target) + + +def load_universe(missions_root: Path) -> Universe: + """Load every campaign under *missions_root* and validate all edges. + + A campaign directory is one containing ``mission.toml``. Raises SchemaError + if any cross-campaign reference does not resolve, or if the GLOBAL graph + (internal and external edges together) contains a cycle. + """ + missions_root = Path(missions_root) + campaigns: Dict[str, Campaign] = {} + for d in sorted(missions_root.iterdir()): + if d.is_dir() and (d / "mission.toml").is_file(): + campaigns[d.name] = load_campaign(d) + uni = Universe(root=missions_root, campaigns=campaigns) + + for cname, camp in campaigns.items(): + for sl, node in camp.nodes.items(): + for dep in node.depends_on: + if not is_external(dep, cname): + continue + if uni.resolve(cname, dep) is None: + raise SchemaError( + f"Node {cname}:{sl} depends_on {dep!r}, which does not " + f"resolve to a node in this missions root." + ) + assert_acyclic_universe(uni) + return uni + + +def assert_acyclic_universe(uni: Universe) -> None: + """Raise SchemaError naming a cycle in the GLOBAL dependency graph. + + Internal cycles are already rejected per campaign; this catches the ones a + per-campaign check structurally cannot see, e.g. rh:A -> mm:B -> rh:A. + """ + WHITE, GREY, BLACK = 0, 1, 2 + color: Dict[tuple, int] = {} + for cname, camp in uni.campaigns.items(): + for sl in camp.nodes: + color[(cname, sl)] = WHITE + + def deps_of(key: tuple) -> List[tuple]: + cname, sl = key + node = uni.campaigns[cname].nodes[sl] + out = [] + for dep in node.depends_on: + camp, target = parse_dep(dep, cname) + if (camp, target) in color: + out.append((camp, target)) + return out + + for start in list(color): + if color[start] != WHITE: + continue + stack: List[tuple] = [(start, iter(deps_of(start)))] + color[start] = GREY + path: List[tuple] = [start] + while stack: + key, it = stack[-1] + try: + nxt = next(it) + except StopIteration: + color[key] = BLACK + stack.pop() + path.pop() + continue + if color.get(nxt) == GREY: + cyc = " -> ".join(f"{c}{DEP_SEP}{s}" for c, s in path + [nxt]) + raise SchemaError(f"cross-campaign dependency cycle: {cyc}") + if color.get(nxt) == WHITE: + color[nxt] = GREY + path.append(nxt) + stack.append((nxt, iter(deps_of(nxt)))) + def open_leaves( campaign: Campaign, claims: Optional[Dict[str, Claim]] = None, diff --git a/telperion/src/telperion/missions/verify.py b/telperion/src/telperion/missions/verify.py index dc967cb66..15b859762 100644 --- a/telperion/src/telperion/missions/verify.py +++ b/telperion/src/telperion/missions/verify.py @@ -208,7 +208,85 @@ def refutation_matches(artifact_text: str, node: Node, root: Path) -> bool: # _compute_closures (pure) and recompute_closures (pure + write-back) # --------------------------------------------------------------------------- -def _compute_closures(campaign: Campaign) -> Dict[str, bool]: + + +def compute_universe_closures(universe) -> Dict[tuple, bool]: + """Global closure fixpoint across every campaign, keyed by (campaign, slug). + + Same rules as the single-campaign pass, but dependency edges may cross + campaigns. The result is cached on the universe as ``.closures`` so a + single load serves every consumer. Anything that does not resolve stays + dirty; there is no path here that turns an unresolved edge clean. + """ + from .registry import parse_dep + + closure: Dict[tuple, bool] = {} + for cname, camp in universe.campaigns.items(): + for sl, node in camp.nodes.items(): + if node.proof is not None: + closure[(cname, sl)] = node.proof.closure_clean + + changed = True + while changed: + changed = False + for cname, camp in universe.campaigns.items(): + for sl, node in camp.nodes.items(): + if node.proof is None or node.proof.via != "reduction": + continue + ok = True + for dep in node.depends_on: + dcamp, dtarget = parse_dep(dep, cname) + tgt = universe.campaigns.get(dcamp) + tnode = tgt.nodes.get(dtarget) if tgt is not None else None + if (tnode is None or tnode.status != "proved" + or not closure.get((dcamp, dtarget), False)): + ok = False + break + if ok != closure.get((cname, sl), False): + closure[(cname, sl)] = ok + changed = True + + try: + universe.closures = closure + except Exception: + pass + return closure + + +def _dep_is_clean(campaign, dep: str, closure: Dict[str, bool], universe=None) -> bool: + """Is this dependency edge satisfied for closure purposes? + + THE ANTI-CASCADE RULE. An edge counts only when its target genuinely + resolves, is `proved`, and is itself closure-clean. An EXTERNAL edge with + no universe supplied, or one whose target does not resolve, is FALSE -- + never True. A cross-campaign reference must not be able to launder an + unverified premise into a clean closure, which is exactly the failure mode + the 2026-09-18 registry audit demonstrated on a throwaway campaign. + """ + from .registry import parse_dep + + home = campaign.root.name + camp, target = parse_dep(dep, home) + if camp == home: + node = campaign.nodes.get(target) + return node is not None and node.status == "proved" and closure.get(target, False) + if universe is None: + return False + ext = universe.resolve(home, dep) + if ext is None or ext.status != "proved": + return False + # NEVER fall back to the target's STORED closure_clean flag: a reduction + # node's stored flag can say True while its own dependency chain is dirty, + # which is precisely how transitive dirt would get laundered across a + # campaign boundary. Compute the global fixpoint instead (cached on the + # universe), and treat anything unavailable as dirty. + ext_closure = getattr(universe, "closures", None) + if ext_closure is None: + ext_closure = compute_universe_closures(universe) + return bool(ext_closure.get((camp, target), False)) + + +def _compute_closures(campaign: Campaign, universe=None) -> Dict[str, bool]: """Pure fixpoint: compute closure_clean for every node with a proof link. Rules: @@ -245,9 +323,7 @@ def _compute_closures(campaign: Campaign) -> Dict[str, bool]: if node.proof is None or node.proof.via != "reduction": continue all_clean = all( - dep in campaign.nodes - and campaign.nodes[dep].status == "proved" - and closure.get(dep, False) + _dep_is_clean(campaign, dep, closure, universe) for dep in node.depends_on ) if all_clean != closure.get(sl, False): @@ -373,10 +449,25 @@ def grant_status(campaign: Campaign, slug: str) -> Node: # verify_campaign -- READ-ONLY audit battery # --------------------------------------------------------------------------- + +def _autoload_universe(root: Path): + """Best-effort: load the sibling campaigns so external edges can resolve. + + Returns None if the siblings cannot be loaded for any reason, which leaves + every external edge dirty -- the safe direction. + """ + try: + from .registry import load_universe + return load_universe(Path(root).parent) + except Exception: + return None + + def verify_campaign( root: Path, deep_lean: bool = False, runner: Optional[Callable] = None, + universe=None, ) -> VerifyReport: """Full invariant battery (read-only). Returns VerifyReport(errors, warnings, ok). @@ -410,7 +501,12 @@ def verify_campaign( manifest = campaign.manifest # Compute fresh closure flags WITHOUT writing to disk (read-only audit) - fresh_closures = _compute_closures(campaign) + # Cross-campaign edges resolve only when a universe is supplied. Without + # one, an external edge is treated as dirty, so the battery can warn but + # never certify an external dependency as satisfied. + if universe is None: + universe = _autoload_universe(root) + fresh_closures = _compute_closures(campaign, universe) # 2. Status coherence for proved/refuted nodes for sl, node in campaign.nodes.items(): diff --git a/telperion/tests/test_missions_cross_campaign.py b/telperion/tests/test_missions_cross_campaign.py new file mode 100644 index 000000000..92b4d56ac --- /dev/null +++ b/telperion/tests/test_missions_cross_campaign.py @@ -0,0 +1,217 @@ +"""Cross-campaign dependency edges in the missions registry. + +A depends_on entry is either a bare slug (same campaign) or a qualified +reference ":". The qualified form exists because real +dependencies cross campaigns; before it existed, five nodes carried a +same-campaign proxy edge while the node title named the real source. + +The tests that matter here are the NEGATIVE ones. A cross-campaign edge is a +new way for an unverified premise to reach a `proved` node, so most of this +file is about the anti-cascade rule: an edge that does not genuinely resolve to +a proved, closure-clean node must never count as satisfied. + +conjecture1_proved = False. +""" +from __future__ import annotations + +import pytest + +from telperion.missions.registry import ( + Campaign, dep_ref, is_external, load_campaign, load_universe, parse_dep, +) +from telperion.missions.schema import SchemaError +from telperion.missions.verify import _compute_closures + + +# --------------------------------------------------------------------------- # +# fixture: a two-campaign missions root built from scratch +# --------------------------------------------------------------------------- # + +MISSION = '''description = "test campaign" +environment_mathlib_rev = "de5ce8a9" +environment_toolchain = "leanprover/lean4:v4.34.0-rc1" +goal_node = "{goal}" +name = "{name}" +title = "{title}" +''' + + +def _node(tmp, camp, slug, *, status="open", deps=(), proof=None): + body = [ + f'name = "{slug.replace("_", ".", 1)}"', + f'title = "node {slug}"', + 'kind = "lemma"', + f'status = "{status}"', + f'statement_module = "Statements.{slug}"', + "depends_on = [" + ", ".join(f'"{d}"' for d in deps) + "]", + 'created = "2026-09-19"', + 'updated = "2026-09-19"', + ] + if proof is not None: + artifact, via, clean = proof + body += [ + "", + "[proof]", + f'artifact = "{artifact}"', + 'artifact_kind = "lean_module"', + f'via = "{via}"', + f"closure_clean = {str(clean).lower()}", + ] + d = tmp / camp / "nodes" + d.mkdir(parents=True, exist_ok=True) + (d / f"{slug}.toml").write_text("\n".join(body) + "\n") + + +@pytest.fixture +def root(tmp_path): + """Two campaigns: 'up' (the source of truth) and 'down' (depends on it).""" + for camp, name, goal in (("up", "UP.goal", "UP_goal"), ("down", "DOWN.goal", "DOWN_goal")): + (tmp_path / camp).mkdir(parents=True, exist_ok=True) + (tmp_path / camp / "mission.toml").write_text( + MISSION.format(name=name, title=camp, goal=goal)) + _node(tmp_path, "up", "UP_goal") + _node(tmp_path, "down", "DOWN_goal") + return tmp_path + + +# --------------------------------------------------------------------------- # +# reference syntax +# --------------------------------------------------------------------------- # + +def test_parse_dep_bare_slug_is_home_campaign(): + assert parse_dep("RH_corridor_bound", "rh") == ("rh", "RH_corridor_bound") + assert not is_external("RH_corridor_bound", "rh") + + +def test_parse_dep_qualified_reference(): + assert parse_dep("rh:RH_rvm_unconditional", "mirrormere") == ("rh", "RH_rvm_unconditional") + assert is_external("rh:RH_rvm_unconditional", "mirrormere") + # a qualified ref naming the home campaign is internal, not external + assert not is_external("rh:RH_x", "rh") + assert dep_ref("rh", "RH_x") == "rh:RH_x" + + +@pytest.mark.parametrize("bad", ["", ":", "rh:", ":slug", "a:b:c"]) +def test_parse_dep_rejects_malformed(bad): + with pytest.raises(SchemaError): + parse_dep(bad, "rh") + + +# --------------------------------------------------------------------------- # +# loading and validation +# --------------------------------------------------------------------------- # + +def test_external_edge_loads_when_target_exists(root): + _node(root, "up", "UP_thm", status="open") + _node(root, "down", "DOWN_uses", deps=("up:UP_thm",)) + camp = load_campaign(root / "down") + assert camp.nodes["DOWN_uses"].depends_on == ("up:UP_thm",) + assert camp.cname == "down" + + +def test_external_edge_to_missing_node_is_rejected(root): + _node(root, "down", "DOWN_uses", deps=("up:UP_absent",)) + with pytest.raises(SchemaError, match="external"): + load_campaign(root / "down") + + +def test_external_edge_to_missing_campaign_is_rejected(root): + _node(root, "down", "DOWN_uses", deps=("nosuch:UP_thm",)) + with pytest.raises(SchemaError): + load_campaign(root / "down") + + +def test_internal_edge_still_validated(root): + _node(root, "down", "DOWN_uses", deps=("DOWN_absent",)) + with pytest.raises(SchemaError, match="not in the campaign"): + load_campaign(root / "down") + + +def test_universe_loads_every_campaign(root): + _node(root, "up", "UP_thm") + _node(root, "down", "DOWN_uses", deps=("up:UP_thm",)) + uni = load_universe(root) + assert set(uni.campaigns) == {"up", "down"} + assert uni.resolve("down", "up:UP_thm").status == "open" + assert uni.resolve("down", "up:UP_absent") is None + + +def test_universe_rejects_cross_campaign_cycle(root): + # up:UP_a -> down:DOWN_b -> up:UP_a is invisible to any per-campaign check + _node(root, "up", "UP_a", deps=("down:DOWN_b",)) + _node(root, "down", "DOWN_b", deps=("up:UP_a",)) + load_campaign(root / "up") # each campaign alone is acyclic + load_campaign(root / "down") + with pytest.raises(SchemaError, match="cycle"): + load_universe(root) + + +# --------------------------------------------------------------------------- # +# THE ANTI-CASCADE RULE +# --------------------------------------------------------------------------- # + +def _down_closure(root, universe=None): + camp = load_campaign(root / "down") + return _compute_closures(camp, universe) + + +def test_reduction_over_external_dep_is_clean_only_when_target_is_proved(root): + _node(root, "up", "UP_thm", status="proved", + proof=("../../examples/x/Up.lean", "direct", True)) + _node(root, "down", "DOWN_uses", status="proved", deps=("up:UP_thm",), + proof=("../../examples/x/Down.lean", "reduction", True)) + uni = load_universe(root) + assert _down_closure(root, uni)["DOWN_uses"] is True + + +def test_external_dep_that_is_not_proved_makes_closure_dirty(root): + _node(root, "up", "UP_thm", status="open") # NOT proved + _node(root, "down", "DOWN_uses", status="proved", deps=("up:UP_thm",), + proof=("../../examples/x/Down.lean", "reduction", True)) + uni = load_universe(root) + # stored flag says True; the fixpoint must overrule it + assert _down_closure(root, uni)["DOWN_uses"] is False + + +def test_external_dep_proved_but_dirty_does_not_launder(root): + """A proved-but-not-closure-clean target must not make the consumer clean.""" + _node(root, "up", "UP_thm", status="proved", + proof=("../../examples/x/Up.lean", "direct", False)) # dirty on purpose + _node(root, "down", "DOWN_uses", status="proved", deps=("up:UP_thm",), + proof=("../../examples/x/Down.lean", "reduction", True)) + uni = load_universe(root) + assert _down_closure(root, uni)["DOWN_uses"] is False + + +def test_external_dep_without_a_universe_is_never_clean(root): + """Single-campaign closure cannot see across campaigns, so it must say False. + + This is the conservative direction: a caller who forgets to pass the + universe gets a dirty closure, never a clean one. + """ + _node(root, "up", "UP_thm", status="proved", + proof=("../../examples/x/Up.lean", "direct", True)) + _node(root, "down", "DOWN_uses", status="proved", deps=("up:UP_thm",), + proof=("../../examples/x/Down.lean", "reduction", True)) + assert _down_closure(root, universe=None)["DOWN_uses"] is False + + +def test_transitive_dirt_propagates_across_campaigns(root): + """up:UP_mid is a reduction over an unproved node, so down must be dirty too.""" + _node(root, "up", "UP_base", status="open") + _node(root, "up", "UP_mid", status="proved", deps=("UP_base",), + proof=("../../examples/x/Mid.lean", "reduction", True)) + _node(root, "down", "DOWN_uses", status="proved", deps=("up:UP_mid",), + proof=("../../examples/x/Down.lean", "reduction", True)) + uni = load_universe(root) + assert _compute_closures(load_campaign(root / "up"), uni)["UP_mid"] is False + assert _down_closure(root, uni)["DOWN_uses"] is False + + +def test_direct_proof_is_unaffected_by_an_external_dep(root): + """A direct proof stands on its artifact; deps are documentary for it.""" + _node(root, "up", "UP_thm", status="open") + _node(root, "down", "DOWN_direct", status="proved", deps=("up:UP_thm",), + proof=("../../examples/x/Down.lean", "direct", True)) + uni = load_universe(root) + assert _down_closure(root, uni)["DOWN_direct"] is True