feat(missions): cross-campaign dependency edges, with an anti-cascade rule - #575
Merged
Merged
Conversation
… rule load_campaign rejected any depends_on target outside its own campaign, so authors substituted same-campaign proxies while node titles named the real source. The 2026-09-18 audit found five nodes whose edges the corpus does not support, and that all 44 proof links are via=direct -- the reduction relation, the one that consumes edges, had never been used. A depends_on entry is now a bare slug (same campaign, unchanged) or a qualified '<campaign-dir>:<NodeSlug>'. Three layers: load_campaign validates external refs by file existence only (no recursion); load_universe resolves them and asserts GLOBAL acyclicity, which catches rh:A -> mm:B -> rh:A that no per-campaign check can see; compute_universe_closures runs one global fixpoint. verify_campaign auto-loads the sibling universe and falls back to None, which leaves external edges dirty. THE ANTI-CASCADE RULE: an edge counts only when its target resolves, is proved, and is itself closure-clean under the global fixpoint. Everything else is dirty. The first implementation fell back to the target's STORED closure_clean flag when no global pass was available; test_transitive_dirt_propagates_across_campaigns caught that laundering transitive dirt across a boundary, and the fallback is gone. 19 new tests, most negative. Mission subset 331 passed; all four campaigns load as a universe and verify OK. No node status changes. conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Remedies the structural finding from the 2026-09-18 registry audit (#574): there was no cross-campaign edge mechanism at all, so authors substituted same-campaign proxies while node titles named the real source. Five nodes ended up with edges the corpus does not support. The same audit found all 44 proof links are
via = direct, so thereductionrelation — the one that actually consumes dependency edges — had never been used once. The registry was recording a chain of reductions while holding a collection of independent direct proofs.The mechanism
A
depends_onentry is now either a bare slug (same campaign, unchanged and still the default) or a qualified<campaign-dir>:<NodeSlug>, e.g.rh:RH_rvm_unconditional. The campaign part is the directory name, because that is what--campaigntakes and what a reference must resolve against.Three deliberately separate layers:
load_campaignvalidates internal refs exactly as before; an external ref is checked for syntax and file existence only, so there is no recursion or load-order coupling.load_universeresolves every external ref for real and asserts global acyclicity — a cycle likerh:A -> mm:B -> rh:Ais invisible to any per-campaign check by construction.compute_universe_closuresruns one global closure fixpoint keyed by(campaign, slug).verify_campaignauto-loads the sibling universe and falls back toNone, which leaves external edges dirty.The anti-cascade rule, which is the point
A cross-campaign edge is a new path for an unverified premise to reach a
provednode, and the audit demonstrated that the gate could already be fooled by a stub. So:Two traps hit during implementation, both now tests. A missing universe yields dirty, never clean. And the first implementation fell back to the external target's stored
closure_cleanflag —test_transitive_dirt_propagates_across_campaignscaught that laundering transitive dirt across a campaign boundary, because a reduction node's stored flag can read true while its own chain is dirty. That fallback is gone.Scope, stated honestly
This does not fix the five unsupported edges. Only one of them is a genuine cross-campaign case and it lives on an unmerged branch; the other four are dependency-correctness questions that need an author's judgement, not a syntax. No node status changes here, and nothing becomes proved.
Verification
19 new tests, most of them negative. Mission subset: 331 passed. All four real campaigns load as a universe and
mission verifyreports OK for each.conjecture1_proved = False.🤖 Generated with Claude Code