Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD 0082 — Cross-module defeat: import-scoped #[defeats] resolution, component-level strategy identity, and the combined-artifact defeat pass

  • State: discussion
  • Opened: 2026-07-19
  • Decides: how a #[defeats(target(args))] directive in one module resolves against a head, label, or trait member declared in another module of the same package — extending the defeat-directive plane of RFD 0028 from file-local resolution to import-scoped resolution. Settles the deferred build-pipeline work RFD 0028 D3’s v1-scope amendment named and tracked as issue #362: the defeat pass lifts out of per-file elaboration into a combined-artifact pass over the module graph; #[defeats] targets resolve over the importing module’s visible names (public and imported); the single strategy per connected defeat graph invariant (RFD 0028 D7) is checked at workspace assembly instead of guaranteed by construction, stamped on the connected component; cross-package defeat edges are refused in this version (in-package only — the package, not the workspace, is the trust boundary); and the diagnostic surface gains distinct codes for the failure modes the wider resolution scope introduces. This RFD is a successor amendment to RFD 0028; it continues that RFD’s D-numbering (D12–D19) and changes nothing about the surface (D1–D2), the strategy-as-compilation architecture (D5–D6), or the semantics of the attack itself (D3–D4). The feature is additive: every program that compiles today keeps compiling unchanged.

Prior state (RFD 0028, accepted): the defeat plane ships file-local. A module is a single .ar file with its own rule catalog; #[defeats] resolves only against that file’s catalog, and a target naming a head, label, or trait member outside the file refuses as unresolvable. That restriction was recorded as a deliberate v1 scope cut, not a semantic wall: “workspace-scoped resolution requires lifting the defeat pass out of per-file elaboration into a combined-artifact pass — a build-pipeline change deferred so it does not ride alongside the two correctness fixes [that] PR lands” (RFD 0028 D3 v1-scope amendment). D7 records what the file-local rule buys: “selection is per module, which structurally guarantees that a connected defeat graph is single-strategy — edges resolve within the module that declared them.” That guarantee is exactly what this RFD must reconstruct once edges are allowed to cross the file boundary.

Question

Statutory-law modeling is the driving workload, and it wants a file layout the file-local defeat plane cannot express. A maintainable tax-code corpus is one file per statute section — the file tree mirrors the code’s own structure, each section reads like the statute it encodes, and a section edit re-elaborates only that section. Exceptions are the essence of statutory drafting: a general provision states a rule, and a later, more specific provision — a different section, a different file — overrides it (“except as otherwise provided …”). The modeling ideal is that the overriding section names what it overrides, with the override semantics living on the overriding rule, where a reader of that section finds it:

// section_1016.ar — the exception carries the attack, in its own file
#[defeats(section_1012::cost_basis.section_1012_a(taxpayer, property))]
pub derive adjusted_basis(taxpayer, property) :- /* … */ ;

(The full two-file version of this example, with both modules spelled out and the pass’s steps narrated, is worked in Consequences below.)

Today this refuses: cost_basis is declared in section_1012.ar, and #[defeats] resolves only against the catalog of the file that declares the attack. The only way to make the defeat plane span two sections is to collapse both sections into one file — which destroys the one-file-per- section layout, kills separate compilation of a section, and does not compose across packages at all.

There is a proven alternative that works cross-file today, without the defeat plane: give each provision a provisional conclusion tagged with the scope where it holds, publish an explicit “yields to a more specific region” relation, and adjudicate precedence centrally by negation-as-failure over that relation and a scope-nesting order. No rule ever names another rule; the override is data plus one central adjudication module. This pattern scales — it has been demonstrated at the scale of a full statute subtitle. But it relocates the override semantics away from the overriding rule: to learn that section 1016 displaces section 1012’s basis, a reader must read the central adjudication module and the scope lattice, not section 1016. That relocation is precisely the compositionality defect the defeat-directive plane exists to fix (RFD 0028 defect 4: “an exception … can’t live in another module under its own honest name”). The central-adjudication pattern is a sound and useful tool, and nothing here removes it; but it is not the surface the rewrite is reaching for.

Two questions. (1) How does a #[defeats] target resolve to a head, label, or trait member declared in another module, so that the overriding rule can name what it overrides, across files, and stay goto-def-able? (2) Once defeat edges cross the file boundary, a connected defeat graph can span modules that selected different reasoning strategies (RFD 0028 D6/D7) — where does the single-strategy invariant get re-established, and what refuses when it cannot hold?

Context

The addressing substrate already exists. Post-qualified-catalog naming, every rule head, labeled clause, and trait member has a fully-qualified catalog key (module::head, Trait::member @ Type), and the resolver already parses all three target spellings — head(args), head.label(args), Trait::member(args) @ Type — and the trait-qualified grain already resolves by segment-exact qualified key. What is file-local is not the spelling but the catalog the spelling is resolved against: the resolver builds its head/label/qualified views from a single file’s rule identities and refuses any target that misses in that one file’s views.

The soundness of the attack does not depend on the file boundary. The Governatori compilation (RFD 0028 D6) is stated per labeled rule and resolved edge; the mechanization ranges over abstract rule identities and an abstract superiority relation and never mentions which file an edge’s endpoints came from. The transform-correctness core, team defeat, ambiguity blocking, strict- unattackability, and the defeated-defeater (reinstatement) property are proved over a program’s clauses and its derived blocking sets — objects that are indifferent to whether two clauses share a file. The defeat-complete extraction theorem preserves warrant given that a rule’s support and the support of all its defeaters are preserved, again over abstract rule identities. The merged, cross-module defeat graph is a bigger instance of the same structure, not a new one.

The genuine hard parts are exactly the two the deferral named: (a) target resolution and defeat- graph cycle detection are cross-declaration and today run inside per-file elaboration, so cross- module edges force a pass that sees more than one file; and (b) the strategy id is recorded per module, and a connected defeat graph that spans modules has no single module to own it.

D12 — Target resolution over the importing module’s visible names

A #[defeats(target(args))] directive resolves its target against the import-scoped catalog of the module that declares the attack: the union of that module’s own rule catalog and the catalog entries reachable through its use edges. The three target spellings are unchanged — head(args), head.label(args), Trait::member(args) @ Type — and all three now resolve across the import closure by the same rules they use file-locally today. Scope follows ordinary name resolution exactly: a use of the RULE (or a glob/alias/re-export reaching it) puts its bare short name in scope; a use of the MODULE binds the module name only, so its members are addressable by the qualified-path spelling (module::head(args)), not by bare name. Resolution stays checked at elaboration and stays goto-def-able: an unresolvable target refuses loudly (D17), and an editor can jump from the #[defeats] directive to the targeted declaration in the other file.

Disambiguation by qualified path. When a short head name is visible from more than one imported module, the bare head(args) spelling is ambiguous and refuses (D17). The author disambiguates by writing the qualified path — other_module::head(args) — resolving the head against exactly the named module. The trait-qualified spelling Trait::member(args) @ Type is already segment-exact and needs no change. Qualified-path targeting is the general disambiguation mechanism and is available for every grain, not only the trait member grain.

Visibility: you can defeat only what you can see. A #[defeats] target must resolve to a declaration the attacking module can actually name — a pub declaration in a module it imports. A private (non-pub) rule is not a legal defeat target from any module that could not otherwise name it, exactly as it is not a legal use target. This is decided: defeat visibility equals ordinary name visibility — including the one carve-out ordinary visibility already grants: a declaring module’s descendants see its private names, so a descendant may attack an ancestor’s private #[default] rule. No new visibility notion is introduced in either direction.

Rationale. There is no action-at-a-distance on private rules. A rule a module keeps private is an implementation detail; letting a distant module attack it would make that private rule’s conclusions silently depend on code its author cannot see and did not consent to expose. Tying defeat visibility to ordinary visibility means the set of things that can attack a rule is exactly the set of modules that can name it — a bound the author already controls with pub. It also keeps one visibility rule in the language rather than a second, defeat-only visibility notion, which was the alternative and is rejected: a separate “defeatable but not otherwise public” grade is a new axis of surface complexity with no demonstrated need, and can be added later without breaking anything if a need appears (recorded open, D19).

D13 — The combined-artifact defeat pass

Defeat-plane resolution and validation lift out of per-file elaboration into a combined-artifact pass that runs at workspace assembly, after every module in the workspace has lowered to its per-module rule identities and before the workspace’s rules go to stratification. This is the build-pipeline change RFD 0028 deferred. Concretely: each module’s elaboration still produces its per-module rule-identity table (head qualified paths, labels, is_default, the raw parsed #[defeats] targets, argument bindings) exactly as today; the combined pass consumes the tables of a module and its import closure, builds the import-scoped catalog (D12), resolves every target, runs the discipline gates over the merged graph (strict-unattackability, per-tuple argument binding, duplicate-label, acyclicity), stamps the resolved edge set onto each attacker’s wire record, and stamps the component strategy id (D14).

Where it runs. In oxc-instantiate, at workspace assembly, driven by the workspace pipeline — not a separate link executable. The elaborator already owns the rule-identity grain the pass needs and already owns the wire records the pass stamps; the pass is a workspace-level phase over per-module elaboration outputs, not a new tool. It runs before the loud evaluability gate so a cross-module target that fails to resolve refuses with the same finality as a file-local one, and no .oxbin is written for a workspace whose defeat plane does not resolve.

Fate of the per-file refusal. Target resolution moves wholesale into the combined pass; there is no file-local resolution step left to keep. The reasoning: a file cannot decide in isolation whether a target that misses its own catalog is a genuine misspelling or a legitimate reference to another file — the two are indistinguishable without the import closure, so a per-file “file-local misspelling” refusal would produce false positives on every valid cross-module edge. The unresolvable-target diagnostic (RFD 0028’s OE0716) therefore becomes the combined pass’s code: it fires when a target misses the import-scoped catalog, and its message distinguishes the misspelling case (no such name anywhere visible) from the not-imported case (the name exists in a module this one does not use) — see D17. The three purely-local gates that need nothing beyond the declaring module — the malformed-target refusal, the per-tuple argument-binding refusal, and the duplicate-label-per-head refusal (labels are per-head identities within one module) — still fire per-file at read time, for editor latency, and are re-checked in the combined pass; only resolution against a catalog wider than the module is combined-pass-only.

Incremental recompute. The combined pass’s validity is scoped to the connected defeat component, not the whole workspace. An edit to a module invalidates the resolved defeat plane of exactly the components its rules participate in: changing a #[default] marker, a #[label], a #[defeats] target, or the pub/visibility of a potential target, or adding or removing a rule that a cross-module target resolves to, re-runs the pass over the affected component(s). A module that participates in no cross-module edge has a single-module component and recomputes exactly as the file-local pass does today — the common case pays nothing new. This keeps separate compilation of a section: editing one section re-runs the defeat pass only over the components that section’s rules touch, which for a statute corpus is the section plus the specific provisions that attack it or that it attacks, not the whole title. (The worst case — an edit that merges or splits a large component — recomputes the whole merged component; whether finer sub-component invalidation is worth its complexity is open, D19.)

D14 — Strategy identity lives on the connected defeat component

The strategy id (RFD 0028 D6 — which compilation scheme gives the program its meaning) moves from per-module to per connected defeat component. A connected component of the merged defeat graph is the unit that gets compiled together by one strategy’s transform, so it is the natural owner of the id. The combined pass computes the components, and for each component records its strategy id on the wire record of every module that participates in the component — so each artifact stays honest about which compilation gave its defeat-bearing rules their meaning, and no single module is privileged as “the” owner of a shared component.

What refuses. A module selects a strategy (in this version, implicitly, the sole strategy — Governatori with explicit superiority; RFD 0028 D6). When a new edge connects two modules that selected incompatible strategies, the component spans conflicting strategies and the combined pass refuses with a distinct strategy-conflict code (D17), naming the two modules and their strategies. This is the D7 invariant — single strategy per connected defeat graph — now checked at workspace assembly rather than guaranteed by the file boundary. In this version, with one strategy in the language, the conflict is unreachable in practice; the check exists from day one so that when a second strategy arrives as a use-imported vocabulary (RFD 0028 D7), the invariant is already enforced at the right grain and the refusal is already specified.

D15 — Cross-package edges are refused; in-package only

A #[defeats] edge may cross module (file) boundaries within one package. It may not cross a package boundary — in a workspace holding several packages, the binding constraint is the package, which is strictly tighter than the workspace: a #[defeats] target that resolves into a different package refuses in this version (D17), even though the addressing substrate could name it.

Rationale. A package is a trust and versioning boundary. Cross-package defeat would mean a dependency update could silently change your conclusions — a new version of a package you import could add a #[defeats] edge that overrides one of your defaults, or change which of its clauses your edge resolves to, altering what your program derives with no change to your source. For a legal or contractual corpus that is an unacceptable failure mode: the meaning of your rules must not move underneath you because a dependency published a point release. Within one workspace the author owns every package and every version simultaneously, so there is no unversioned third-party surface and no silent drift; the same author can see and reason about every edge in the component. Cross-package composition through honest heads (ordinary use of a public predicate, strategy- independent) is unaffected and works exactly as it does today — it is only the defeat edge across the package boundary that is refused. Whether cross-package defeat can ever be made safe (a package declaring which of its clauses it exposes as defeatable, versioned as part of its public interface) is left open (D19); refusing it now forecloses nothing and keeps the dangerous case out of a version whose semantics we can fully defend.

D16 — Consent to be overridden: #[default] is the token, within the package

A module you import must not be silently overridden without a marker its author placed. In the defeat plane that marker already exists: #[default] (RFD 0028 D1) marks a clause as overridable, and RFD 0028 D4 already refuses any #[defeats] target that resolves to a clause not marked #[default] (strict conclusions are unattackable). That refusal carries the whole consent story across the module boundary unchanged: a cross-module #[defeats] edge is legal only against a #[default] clause, so a rule can be overridden from another file only if its own author wrote #[default] on it. #[default] is the opt-in. A rule with no #[default] marker is strict and cannot be attacked, from its own file or any other.

Combined with D15, the consent rule is: a cross-module #[defeats] target must name a #[default] clause in a module of the same package. The #[default] marker supplies per-clause consent to be overridden; the same-package restriction supplies the versioning guarantee that the consent cannot be exercised by code the author does not control and cannot see change. This is the defensible position: overridability is never implicit (you must write #[default]), and it is never reachable from outside the trust boundary (you must be in the same package). Requiring an additional cross-module-specific consent annotation beyond #[default] was considered and rejected as redundant within a package: #[default] already means “this clause may be displaced by a more specific rule,” and inside one package, authored together, that is the entire meaning the author needs to grant. The heavier annotation belongs to the cross-package case, which is refused here and left open (D19).

D17 — Diagnostics: the failure modes wider resolution introduces

All codes are stated by role; exact numbers are assigned at implementation against the live catalog, per RFD 0028 D11’s discipline (no raw-string emissions; feature-named codes). The defeat plane owns OE0716–OE0721; the intervening numbers are occupied by other subsystems, so the new codes open a fresh slot (OE0736–OE0739) rather than extending that block contiguously.

  • Unresolvable cross-module target (the existing unresolvable-target code, widened). A target misses the import-scoped catalog. The message distinguishes two sub-cases so the fix is obvious: no such name is visible anywhere (a misspelling), versus a matching public name exists in a module this one does not use (add the import, or write the qualified path). Resolution-checked at elaboration; goto-def-able.
  • Ambiguous cross-module target (new). A bare short head name resolves to a public head in more than one imported module. The message names each candidate’s module and instructs the author to disambiguate with the qualified path module::head(args) (D12).
  • Defeat target not visible (new, or folded into the unresolvable code as a third sub-case). A target resolves to a declaration that exists but is not pub in its module, so the attacker cannot name it (D12). The message states that defeat visibility equals name visibility and that the target must be made pub by its own author.
  • Cross-package defeat refused (new). A target resolves into a different package (D15). The message states the in-workspace-only rule and its reason (a dependency update must not silently change your conclusions), and points at honest-head composition as the cross-package tool.
  • Defeat component spans conflicting strategies (new). A component’s modules selected incompatible strategies (D14). The message names the two modules and their strategies. Inert in this version (one strategy), specified for the multi-strategy future.

Every one of these is resolution-checked at elaboration in the combined pass; none is deferred to runtime. (Assigned at implementation: OE0736 ambiguous target, OE0737 target not visible, OE0738 cross-package refused, OE0739 component strategy conflict; OE0716 widened as described.) The existing defeat-plane codes — strict-conclusion-unattackable, defeat-graph-cycle, duplicate-label-per-head, unbound-directive-argument — are unchanged in meaning and wider in scope (the graph and the catalog they range over are now the merged, cross-module ones).

D18 — Semantics: the graph gets bigger, the theorems do not change

The well-founded/grounded semantics of a #[default]/#[defeats] program is unchanged by cross-module resolution. The meaning of the program is still the meaning of its Governatori compilation onto the core stratified/WFS semantics (RFD 0028 D6); cross-module resolution only changes which resolved edges populate the defeat graph the transform consumes. The mechanization already ranges over abstract rule identities and an abstract superiority relation and never refers to a file boundary, so the theorems carry to the merged graph without change in substance:

  • Transform correctness / team defeat / ambiguity blocking / strict-unattackability. Stated over a program’s clauses and its derived blocking sets. A clause’s blocking set is the image of its attackers’ surviving tuples under the resolved edge relation, indifferent to which module an attacker lives in. Merging the graph adds edges to the relation; the per-tuple warrant specification and its equality with the compiled extent are unchanged.
  • Reinstatement across modules (the defeated-defeater property). A defeated defeater stops blocking its target because the blocked set is the image of the attacker’s surviving tuples; if the attacker was itself defeated — by a rule in any module, since the surviving set is computed over the merged graph — the target reinstates. Monotonicity of blocking in the attacker’s surviving set is the load-bearing lemma and is stated over sets of tuples, not modules. Cross-module reinstatement is therefore already covered.
  • Extraction across modules. The defeat-complete extraction theorem preserves a rule’s warrant given its support and all its defeaters’ support are preserved; the defeat-closure it requires is direct-defeat only, over abstract rule identities. When defeaters live in other modules, the closure crosses the module boundary — the theorem’s assumption (“all its defeaters”) is unchanged, only the set it quantifies over now spans files. Extraction operating pre-transform over labeled rules and edges (RFD 0028 D5) is the relevant grain and needs no restatement of substance.

What the mechanization needs, restated for the merged graph:

  1. Cycle detection over the merged graph. Acyclicity (the defeat-graph-cycle refusal) must be decided over the whole connected component, not one file. Two independently-authored, individually- acyclic modules can form a cycle when a new edge connects them — the defeat graph can have a cycle even when the module import graph does not (edges may point up, down, or across the import DAG). Acyclicity is checked on the defeat graph directly, over the whole component; it remains decidable on a finite graph and its computational witness is the combined pass’s cycle finder. This is a restatement of the existing decidable-acyclicity obligation over a wider, still-finite graph.
  2. The topological order the reinstatement fixpoint relies on now ranges over the merged, acyclic component. The defeat-algebra theorems (proved) are unchanged; the topological induction that iterates them (narrowed to the well-founded-semantics catch-up) iterates over the component instead of the file. No new proof obligation beyond re-instantiating the existing one at the component grain.
  3. The extraction signature includes cross-module edges. The theorem statement is unchanged; its edge carrier is the merged edge set.

No new semantic obligation is created; the obligations are the existing RFD 0028 D10 obligations re-instantiated over the merged graph. The differential-oracle corpus (RFD 0028 D10.2) gains cross-module fixtures — a two-file transitive-defeat case and a two-file reinstatement case — so the wider graph is exercised end-to-end against the compiled semantics.

D19 — Open questions this RFD does not close

  • Cross-package defeat. Refused here (D15). Whether it can be made safe — a package declaring a defeatable interface (which of its #[default] clauses it exposes to cross-package attack), versioned as part of its public surface so a dependency bump cannot silently move conclusions — is open. This is the “a regulation package defeats a clause it does not own” aspiration; it is powerful and dangerous, and it needs a versioning story before it can land.
  • Strategy-id ownership across packages. D14 stamps the id on the component within a workspace. When a defeat component could span packages (only if cross-package defeat lands), whose declared strategy vocabulary owns the id, and how a strategy mismatch across a package boundary is surfaced as a dependency-resolution error rather than a build error, is open — coupled to the cross-package question above.
  • A separate defeat-visibility grade. D12 decides defeat visibility equals name visibility. A distinct “defeatable but otherwise private” grade — a rule an author exposes only as a defeat target, not for ordinary use — is a plausible future refinement with no demonstrated need yet; recorded, not adopted. It can be added without breaking D12.
  • Incremental recompute granularity under adversarial editing. D13 scopes invalidation to the connected component. The worst case — an edit that merges or splits a large component (adding the first edge between two big sub-graphs, or removing the only edge joining them) — recomputes the whole merged component. Whether a finer sub-component invalidation is worth its complexity is an implementation-staging question, open.
  • Implementation staging. The pass-lift (D13), the resolution widening (D12), the component- strategy stamping (D14), and the new diagnostics (D17) are separable slices; the order in which they land, and whether the strategy-conflict machinery (inert with one strategy) waits for the second strategy, is open and is a sequencing decision, not a design one.

Rationale (summary)

  • Import-scoped resolution puts the override on the overriding rule, in its own file, goto-def-able — the compositionality the defeat plane exists to deliver, now across files. It reuses the existing three spellings and the existing qualified-catalog substrate; nothing about the surface changes.
  • Lifting the pass to workspace assembly is the minimal pipeline change that makes cross-declaration resolution and cycle detection see more than one file, and scoping its validity to the connected component preserves separate compilation of a section.
  • Putting the strategy id on the component and checking the invariant at assembly reconstructs exactly the guarantee the file boundary gave for free (D7), at the grain that will still hold when a second strategy arrives.
  • Refusing cross-package defeat keeps the version whose semantics we can fully defend: overridability is explicit (#[default]) and unreachable from outside the trust boundary, so no dependency update can silently change a program’s conclusions.

Alternatives considered

  • Keep the defeat plane file-local; model cross-section override with provisional facts + central negation-as-failure adjudication. This works cross-file today and scales, and it stays available — nothing here removes it. It is rejected as the answer to this RFD’s question because it relocates the override semantics away from the overriding rule into a central adjudication module and a scope lattice, which is the compositionality defect the defeat plane exists to fix. It is the right tool when engine-level proof tags and strategy diagnostics are not needed; it is not the surface the statutory-corpus modeling effort is reaching for.
  • Collapse a defeat cluster into one file. The only way the file-local plane spans sections today. Rejected at statute scale: it destroys the one-file-per-section layout, kills separate compilation, and does not compose across packages at all. It remains fine for a small, tightly- coupled cluster that genuinely fits one file.
  • A separate defeat-only visibility grade. Rejected for this version (D12): a second visibility axis with no demonstrated need; addable later without breaking D12.
  • Allow cross-package defeat now. Rejected (D15): it lets a dependency update silently change a program’s conclusions, unacceptable for a legal/contractual corpus, and it needs a versioned defeatable-interface story that does not yet exist.
  • A per-file “file-local misspelling” refusal kept alongside the combined pass. Rejected (D13): a file cannot distinguish a misspelling from a valid cross-module reference without the import closure, so a per-file resolution refusal would false-positive on every valid cross-module edge.

Consequences

  • Nothing breaks. The feature is additive. Every program that compiles today has a defeat plane whose edges all resolve file-locally; under the combined pass each such module is a single-module connected component that resolves and validates exactly as before, and pays no new incremental- recompute cost.
  • The tax-corpus authoring pattern it enables: one file per statute section, each section reading like the statute, exceptions carrying their own attacks across files under honest heads.
  • The build pipeline gains a workspace-assembly phase in oxc-instantiate; the wire record gains a component strategy id (stamped on every participating module); the diagnostic catalog gains the D17 codes.
  • The mechanization’s RFD 0028 D10 obligations are re-instantiated over the merged graph; the differential-oracle corpus gains cross-module fixtures. No new semantic obligation is created.

What changes for the author

Before this RFD, a #[defeats] target had to name a rule in the same file; the only way to make an exception overridable across provisions was to collapse the provisions into one file. Now:

  • What you can write. All three target spellings — head(args), head.label(args), Trait::member(args) @ Type — may name a rule in another file, provided your module can see it: import the RULE (a use leaf, glob, or alias) and the bare spelling resolves exactly as a local one does; import only its MODULE and the qualified-path spelling module::head(args) names it — the same reading every other name position has. The qualified path also disambiguates when a bare short name is visible from more than one imported module.
  • What the target must be. A pub #[default] clause in a module of the same package — the same consent rule as before (#[default] is the opt-in), now carrying across files.
  • New refusals you can hit, and their fixes. A target that exists but is not imported refuses with the not-imported sub-case of the unresolvable-target code (fix: add the use, or write the qualified path). A bare name visible from two imported modules refuses as ambiguous (fix: qualified path). A non-pub target refuses (fix: its author makes it pub). A target in another package refuses (no fix by design — compose through public predicates instead). A cycle formed by edges across files refuses exactly as a local cycle does.
  • What does not change. Every file-local program keeps its exact meaning and messages; runtime evaluation is untouched; no new syntax exists — these are the existing directives with a wider resolution scope.

Worked example — a general basis rule overridden across files

Two files, two modules, one package. section_1012.ar states the general rule that a property’s basis is its cost. section_1016.ar states the exception: certain adjustments displace that general basis. The exception names what it overrides, in its own file.

// section_1012.ar — the general rule: basis is cost. Overridable by a more specific provision.
pub derive is_property(taxpayer, property) :- /* … acquisition facts … */ ;

#[default]
#[label(section_1012_a)]
pub derive cost_basis(taxpayer, property) :-
    is_property(taxpayer, property),
    acquisition_cost(taxpayer, property, _);

// section_1016.ar — the exception: an adjustment to basis displaces the general cost basis.
use pkg::usc26::subchapter_o::section_1012;   // binds the module name; its members
                                              // are addressable as `section_1012::…`

// The overriding rule names exactly the clause it overrides, in the file where the override lives.
#[defeats(section_1012::cost_basis.section_1012_a(taxpayer, property))]
pub derive adjusted_basis(taxpayer, property) :-
    is_property(taxpayer, property),
    basis_adjustment(taxpayer, property, _);

Reading the two files: section 1012 states that cost is the default basis and marks it #[default], granting consent to be overridden by a more specific provision (D16). Section 1016 states the adjustment rule and, on that rule, declares that it defeats section 1012(a)’s cost basis for the same (taxpayer, property) tuple (per-tuple blocking, RFD 0028 D3). The combined pass resolves section_1012::cost_basis.section_1012_a against section 1016’s import-scoped catalog (it imports the section-1012 module, so the qualified spelling names it — D12), confirms the target is #[default] (D16) and in the same package (D15), places the two rules in one connected defeat component, stamps the strategy id on both modules (D14), and checks the merged graph is acyclic (D18). Where an adjustment applies, cost_basis is blocked for that tuple and adjusted_basis supplies the basis; where no adjustment applies, the default cost basis survives. Editing section 1016 re-runs the defeat pass over this two-module component only, not the whole title (D13).

Relationship to RFD 0028

This RFD is a successor amendment to RFD 0028 (Defeasibility redesign). It continues that RFD’s D-numbering (D12–D19) and discharges the deferred build-pipeline work its D3 v1-scope amendment named, tracked as issue #362. It changes nothing about RFD 0028’s decided surface (honest heads, the directive plane, the three target spellings — D1–D3), the attack discipline (D4), the strategy-as-compilation architecture and its four hooks (D5), the Governatori strategy (D6), or the proof-tag channel (D8). It amends RFD 0028 D3 (target resolution becomes import-scoped, workspace-assembly-time, not file-local), RFD 0028 D7 (the single-strategy-per-connected-graph invariant is checked at workspace assembly and owned by the connected component, not guaranteed by the file boundary), and RFD 0028 D11 (the diagnostic inventory gains the D17 codes). The Lean obligations are RFD 0028 D10 re-instantiated over the merged defeat graph, with no new obligation in substance.

Open questions

Collected from D19: cross-package defeat and its versioned defeatable-interface story; strategy-id ownership across packages; a separate defeat-visibility grade; incremental-recompute granularity when an edit merges or splits a large component; and implementation staging of the separable slices (pass-lift, resolution widening, component-strategy stamping, diagnostics) including whether the inert strategy-conflict machinery waits for a second strategy to exist.