RFD 0083 — Defeat-plane compilation: the Governatori transform as elaboration-time strict rules

• State: committed
• Opened: 2026-07-21
• Decides: the defeasibility semantics of RFD 0028 — honest heads, the defeat-directive plane, Governatori-with-explicit-superiority as strategy #1 — are realized by compiling the mechanized transform at elaboration time into ordinary strict WFS rules emitted into the .oxbin, replacing the interpretive runtime resolver (oxc-runtime/src/defeasible.rs). RFD 0028’s decisions D1–D11 are unchanged; this RFD only changes where and how strategy #1’s compilation scheme (D5 hook 3, D6) runs — from a runtime survivor-traversal to a lowering-time program transform. Settles the semantics question left open by #1791 (recursive #[default] dependencies): the recursive fixpoint is defined, not refused. The regression floor is partly in place: #1789 (for #1788) has merged; the #1790 reinstatement fix and the interim fail-open hardening (#1796, cone-sensitive reentrancy) remain open. Folds in #1792 structurally. Green-lit after the ground-truth oracle (#1793, merged) exposed the bug family’s shared architectural signature; the recursive-fixpoint Lean entry gate is delivered in #1797 (CompiledFixpoint.lean, D6, merged).

In plain language — what changes and why

Nothing about the language changes. #[default] rules, #[defeats] edges, and every program that uses them keep their exact meaning; no program is rewritten, refused, or reinterpreted. What changes is how the engine carries that meaning out.

Today, defeat is executed by a dedicated interpreter inside the runtime: when a query touches a defeasible head, a resolver walks the defeat graph head by head, computing which clauses survive, caching intermediate results, and guarding itself against revisiting a head it is already working on. That machinery re-implements, by hand, work the rule evaluator already knows how to do — and the recurring wrong-law bugs all came from exactly the hand-made parts: results that depended on the order heads were resolved, a cache that could be poisoned by a partial answer, and a self-protection fallback that served pre-defeat rows when startled.

After this change, defeat is compiled instead of interpreted: at build time, each #[default] clause and #[defeats] edge is translated into a few ordinary strict rules (a rule for the clause’s support, a rule deriving a blocked marker from surviving attackers, and a public rule saying “the head holds where supported and not blocked”). The ordinary evaluator then runs those rules like any others. Fixpoint iteration, ordering, reinstatement chains, and depth-independence stop being properties we implement and test for — they are what the evaluator does by construction, for every rule.

Why we trust the translation: it is not designed here — it is the construction the mechanized semantics already specifies and proves correct, and the executable oracle (the reference evaluator plus generated-program differential) accepts the compiled path only if it agrees with that semantics across every generated program. Why now: the interpreter’s bug family kept reaching users as silently wrong derived law; and the incremental-circuits work compiles rules, so an interpreted defeat plane would need permanent special-casing there, while a compiled one is supported for free.

Question

RFD 0028 D6 promoted a promise from implementation note to definition: the meaning of a #[default]/#[defeats] program is the meaning of its compiled core program. The shipped implementation did not honor that. It kept an interpretive runtime resolver — a per-head survivor traversal that resolves the defeat graph on every derive query, computing the warranted extent by folding per-clause contributions against blocking sets built from surviving attackers, in topological order, guarded by a reentrancy check.

That resolver has produced a family of correctness defects that share one signature. The question: is the resolver fixable in place, or does the architecture itself have to change — and if it changes, to what, and what does the substrate have to prove first?

Context — the bug family and its shared signature

The resolver (Store::defeasible_survivors, oxc-runtime/src/defeasible.rs, Store::defeasible_survivors) approximates a well-founded / team-defeat fixpoint with three mechanisms that together are the fault line:

1. a per-head memo (DefeasibleSurvivorsMemo) keyed by relation short name, mutated as heads resolve;
2. a reentrancy guard (visiting: BTreeSet<String>, let reentrant = !visiting.insert(...), the visiting-stack guard in defeasible.rs); and
3. a fail-open fallback — on re-entry the resolver serves catalogs.support.clone(), the raw pre-defeat extent (the re-entry arm of defeasible_survivors), and writes that under-computed result into the shared memo.

Every defect is a facet of these three:

Three of the four (#1788, #1791, #1792) are the same primitive: the fail-open reentrancy fallback writing raw pre-defeat data into a shared, order-sensitive, short-name-keyed memo. #1790 is that bookkeeping failing in the suppression direction. The mechanized transform (spec/lean/Argon/Reasoning/Defeasibility/Transform.lean) already specifies the sound target — a topological team-defeat fold over blocking derived from surviving attackers, F2 reinstatement, strict-unattackability — and proves the defeat algebra; the runtime diverges from it by approximation. The indictment is architectural: an interpretive resolver’s correctness depends on resolution order, exact seed scope, key namespacing, and elaboration-time graph guarantees that do not all hold, and no local patch removes that dependence — #1789 removed one spurious trigger, but the fail-open branch remains reachable on accepted programs (#1791).

The ground-truth oracle (PR #1793, merged) made this measurable: a brute-force reference evaluator of RFD 0028 D2 (the executable mirror of Transform.lean), a seeded program generator, a #1788 leak ladder, and an env-gated soak (generated_differential_soak), wired as a differential against the production .oxbin/Store path (oxc-runtime/tests/defeat_plane_oracle.rs). It is the instrument that turned each defect into a repeatable divergence and revealed they are one shape.

The strategic alignment is independent and points the same way. The DBSP circuit program (RFD 0018, lines 60/136) delivers defeasibility as Maher’s three-stratum compilation — the defeat plane becomes ordinary stratified Datalog with proof tags as derived-predicate labellings, which sits inside DBSP’s proven, standard incremental fragment (positive recursion + stratified NAF). An interpretive resolver is not a set of stratified derived predicates; it cannot be lifted by the circuit’s lift(Q) and would force out-of-band special-casing the circuit cannot incrementalize (the only piece needing a new kernel — recursive-WFS-on-DBSP — is explicitly deferred and is the richer, ambiguity-propagating defeasibility, not the compiled plane). Compiled defeat is circuit-ready by construction; interpretive defeat is a permanent exception.

Decision

Compile the defeat plane at elaboration time. The strategy transform (RFD 0028 D5 hook 3) runs in oxc-instantiate at lowering, beside the existing defeat validation/stamping pass (lower/defeat.rs::resolve_workspace_defeat_plane), and emits the Governatori compilation as ordinary strict rules into the .oxbin. Everything downstream of lowering — the reasoner, the runtime, the projection cache, the DBSP circuit — sees an ordinary WFS program. The interpretive resolver in oxc-runtime/src/defeasible.rs is deleted. There is no defeat-specific evaluation path.

The architectural contrast in one figure — a hand-rolled fixpoint recomputed per query versus a program transform run once at lowering:

  INTERPRETER  (deleted)                      TRANSFORM  (this RFD)
  ──────────────────────                      ─────────────────────
  every derive query, per head:               elaboration, once per source:
    Store::defeasible_survivors                  resolve_workspace_defeat_plane emits, per head:
      topological walk over heads                  $defeat::support::<clause>   (support)
      per-head memo  (short-name key) ◀─┐          $defeat::block::<head>[::<label>]
      reentrancy guard ──── fail-open ──┘            H :- support, not block     (public)
        catalogs.support.clone()                → .oxbin: ordinary strict WFS rules
        (raw pre-defeat extent)                  ─────────────────────────────────────
    ── fixpoint computed BY HAND ──             runtime: one Engine::evaluate
      order-, scope-, key-dependent               the WFS fixpoint, computed NATIVELY
      (the bug family)                            (NAF memo, cone slicing, projection
                                                   cache all apply — for free)

The memo, the guard, and the fail-open fallback — the whole left column — have no counterpart on the right. They were an interpreter’s way of computing a fixpoint the evaluator computes natively.

D1 — What the elaborated program looks like

For each defeasible head H (a head with a #[default] clause, or a #[defeats] target), the transform emits, per Transform.lean’s construction:

• Support atoms — the per-clause contribution over the converged catalog. Each source clause of H lowers to a strict rule whose head is an internal support relation carrying the clause identity; recursion in the clause body reads the converged public head (the F1 fix, defeasible_clause_contribution made static — the head is never cleared).
• Blocking atoms — for each #[defeats] edge into H, a strict rule deriving an internal blocking relation from the attacker’s surviving support projected through the edge’s resolved argument binding. Because the attacker’s surviving support is itself an emitted relation (recursively transformed), a defeated defeater contributes no blocking tuple — F2 (blockFromSurvivors, defeated_defeater_does_not_block) becomes a structural NAF join, not a runtime intersection.
• The team-defeat fold — the public head H is emitted as strict rules projecting each clause’s support NAF-guarded against the applicable blocking relation (head-level blocking for every default clause; clause-level blocking naming the clause’s #[label]). A strict (non-#[default]) clause projects unguarded — strict-unattackability (strict_clause_unattackable) is the absence of a NAF guard, not a runtime flag. An unbeaten teammate keeps the conclusion because its unguarded (or unblocked) projection still fires (team defeat, team_defeat_unbeaten_survives).
• Reinstatement via F2 — falls out: the blocking relation reads surviving attacker support, which is itself a fold over its blocking, so a pardoned attacker’s blocking tuple is simply never derived.

The blocking guards introduce NAF; the target/attacker resolution order the interpreter walked by hand is now the reasoner’s ordinary WFS evaluation of a stratified-NAF (or, on a target↔attacker negative cycle, genuinely well-founded) program. The topological traversal, the memo, the guard, and the fallback have no counterpart — they were an interpreter’s way of computing a fixpoint the evaluator computes natively.

Naming discipline. Internal relations are minted under a $-prefixed family, qualified by the source head’s catalog path — e.g. $defeat::support::<qpath>::<label>, $defeat::block::<qpath>, $defeat::block::<qpath>::<label> — never short names. Qualified keying is the structural fix for #1792: the short-name collision class cannot recur because there are no short-name keys. Internal heads are non-public (excluded from query surfaces, SDK generation, and extraction signatures); an old generic reader that walks all rules sees ordinary RuleDecl bodies with unfamiliar $-names and executes them harmlessly (they are range-restricted strict rules like any other).

Worked example — one compiled program, rule for rule

A minimal defeat-bearing program: one #[default] (a general rule), one #[defeats] (a stricter exception), one downstream reader. Surface (illustrative):

#[default] #[label(general)]
eligible(P) :- resident(P).       // the default: residents are eligible, defeasibly

#[defeats(general)]
excluded(P) :- felon(P).          // the defeater: felons are excluded, defeating `general`

canVote(P) :- eligible(P).        // the reader: a downstream consumer of the defeasible head

The transform emits (canonical $-qualified names abbreviated; Transform.lean / CompiledFixpoint.lean give the authoritative construction):

$defeat::support::eligible::general(P) :- resident(P).      (1) support
$defeat::support::excluded::c0(P)      :- felon(P).         (2) support (attacker)
excluded(P) :- $defeat::support::excluded::c0(P).           (3) public head (strict clause)
$defeat::block::eligible::general(P)   :- excluded(P).      (4) block
eligible(P) :- $defeat::support::eligible::general(P),      (5) public head (default clause)
               not $defeat::block::eligible::general(P).
canVote(P) :- eligible(P).                                  (6) reader (unchanged)

One sentence per rule: (1) the default clause’s per-clause contribution over the converged catalog — a plain strict rule, no guard. (2) the attacker’s contribution, likewise. (3) the attacker’s public head; excluded is a strict (non-#[default]) clause, so it projects unguarded — strict-unattackability is the absence of a NAF guard, not a runtime flag. (4) the blocking relation for the general clause reads the attacker’s surviving support, which is exactly its public head excluded (F2 as a structural NAF join: a defeated defeater would have no excluded tuple, so no block tuple). (5) the public head eligible projects its support NAF-guarded against the blocking relation — the team-defeat fold; a felon resident derives $defeat::block::eligible::general and so eligible does not fire, while a non-felon resident is unblocked and keeps the conclusion. (6) the reader is untouched — it reads the ordinary public head eligible like any relation. The topological walk, the memo, the guard, and the fallback have no rule here.

The recursive-default flip (#1791), where the resolver mis-served. A default that reads itself transitively:

#[default] reaches(X, Y) :- edge(X, Y).                     // base
#[default] reaches(X, Z) :- edge(X, Y), reaches(Y, Z).      // recursive step

There is no #[defeats] edge, so no blocking relation is emitted; the compiled program is:

$defeat::support::reaches::c0(X,Y) :- edge(X,Y).
$defeat::support::reaches::c1(X,Z) :- edge(X,Y), reaches(Y,Z).   // recursion reads the
                                                                  // CONVERGED public head (F1)
reaches(X,Y) :- $defeat::support::reaches::c0(X,Y).
reaches(X,Z) :- $defeat::support::reaches::c1(X,Z).

With no live defeater the public head is the ordinary least fixpoint — the full transitive closure (D2 case 2, WFS-native Datalog recursion). The interpreter mis-served here: its reentrancy guard fired on the self-recursive head and returned the raw pre-defeat one-hop extent (catalogs.support.clone()), so multi-hop reaches tuples were lost. The compiled path has no guard to fire and derives the complete closure — the rewrite’s headline correctness fix.

D2 — Recursive defaults (the Lean prerequisite; settles #1791)

Three cases must be distinguished; the interpreter conflated the first two into its fail-open branch:

1. Defeat-graph cycle (attacker/target identities form a cycle): refuse, OE0718, unchanged. This is where the well-behaved compilation stories diverge (RFD 0028 D4); v1 picks none.
2. Positive rule-dependency cycle among #[default] heads, with no defeat edge among them (a default head recursive through itself or mutually with peers, e.g. transitive closure marked #[default]): admit. This is ordinary Datalog recursion; WFS defines it. The interpreter refused it only by accident (the reentrancy guard), an interpreter limitation with no cause once compilation removes the recursive host-language calls.
3. A #[default] head that is both recursive and a defeat target (its blocking guard reads an attacker that recursively depends on it): admit. The emitted blocking guard is a NAF atom; recursion through NAF is precisely WFS’s domain. Under the compiled program the head’s extent is the WFS model — true where warranted, possibly undefined on a genuine target↔attacker negative cycle. RFD 0028 D6 already defines defeasible meaning as the compiled program’s meaning, so an undefined tuple is a defined outcome, not a resolver failure. No OE1317-style stratification gate is added for defeat — OE1317 exists because recursion through aggregation lacks a fixpoint; recursion through NAF has WFS. One existing gate is adjacent and must be respected, not contradicted: OE1365 (NegatedWfsRelation, oxc-reasoning compile/stratify.rs) refuses a cross-stratum not R where R is a WFS SCC that can carry undefined atoms — the honest interim until three-valued undefined propagates into derive heads (#134/#165). This does not gate case 3: a head both recursive and a defeat target sits in one WFS SCC with its own blocking guard (same-SCC NAF is evaluated by the well-founded evaluator directly, never OE1365-refused). The emission must keep that property — the compiled H :- support, not $defeat::block::… and the negated blocking relation stay in a single WFS SCC whenever a target↔attacker negative cycle exists, so no cross-stratum not over an undefined-carrying blocking relation is produced. Establishing this (or refusing the residual split shape) is a D6 obligation, called out there.

The fail-open fallback (#1791) dies structurally: a compiled program has no reentrancy guard and no raw-support branch to fall into. The declaration-plane gap closes not by widening OE0718 to the rule-dependency graph but by making the rule-dependency graph a legal WFS input.

This is the rewrite’s entry gate. Transform.lean today is honest that it proves the defeat algebra over a clause’s contribution as a converged input and narrows the fixpoint↔attribution correspondence for genuinely recursive heads to the WFS catch-up (#134), backed by differential-oracle corpus tests (defeasible_recursion_v0, defeasible_defeated_defeater_v0). Compiling the transform makes that correspondence load-bearing: the emitted program’s WFS model is the shipped semantics, so the theorems must state it. The Lean prerequisite is scoped in D6 and delivered in PR #1797 (CompiledFixpoint.lean, merged) plus the #134 Part A stratified-defeat bridge; the only surviving reduction is the positive-recursive-stratum lemma reported in D6.

D3 — Wire discipline, artifact, and versioning

The transform runs at elaboration, so a naive artifact would carry both the executable defeat metadata (the GovernatoriSuperiority strategy id and resolved DefeatEdge sets stamped by resolve_workspace_defeat_plane) and the emitted compiled rules — inviting a runtime that still had an interpreter to re-resolve the plane over the public heads and double-apply defeat. The wire discipline forecloses that:

• Executable rules carry only the compiled strict program. For every derive rule of a defeat-bearing module, the emitted .oxbin sets is_default = false, defeats = [], defeat_strategy = None. The original clauses are not executable rules; the public head and $-internal helpers are ordinary strict rules. An old runtime therefore evaluates the compiled program and cannot re-interpret — there is nothing left to trigger an interpreter.
• A separate, additive, inert provenance carrier (DefeatCompilationProvenance, module-level) retains what the executable rules shed: representation = compiled, the strategy id, source rule identities, #[label]s, #[default] markers, resolved edges + bindings, and the deterministic map from source clauses to emitted rules and proof-tag classes. Reflection, ox derive --explain, provenance, extraction audit, and the D8 proof-tag surface read this carrier; evaluation never does. This is what preserves RFD 0028 D8 (proof tags computed from defeasibility metadata) and the audit surface after the executable metadata is stripped.

Consequences for versioning:

• The artifact grows, linearly in clauses plus defeat edges (added RuleDecl bodies, symbols, $-relations) plus the provenance carrier. This is a normal artifact-content change: the artifact hash moves for any compiled program, exactly as any lowering change moves it.
• No Core-IR version bump. No RuleIR / AtomIR / Term shape changes — only more ordinary rules. Adding rules is not an IR-shape change.
• .oxbin format minor bump for the additive DefeatCompilationProvenance section carrier (backward-safe: an old runtime ignores an additive section and evaluates the compiled rules).
• DERIVATION_SEMANTIC_EPOCH (oxc-runtime/src/lib.rs, the constant gating persisted projection-cache validity per RFD 0072 D5) is not bumped for the compile flip, and no new committed field is added. The switch is elaboration-time (D4): flipping it changes which artifact elaboration emits for a given source — a legacy-metadata artifact or a compiled-strict-program artifact — not which path a runtime takes over a fixed artifact. The two artifacts have distinct hashes. The artifact hash is the discriminator: it is already an input to oxc_oxbin::projection_cache::derivation_commitment, so a cache built against one artifact can never be served against the other — the caches separate with no derivation_commitment change. For any fixed artifact both representations of the runtime produce the same projection: a compiled artifact evaluates its strict rules identically on any runtime (a pre-rewrite runtime no-ops the absent defeat plane and runs the compiled rules — see D4); a legacy artifact drives the resolver on any runtime that still has one. Nothing changes a derived result for a fixed artifact, so there is no same-artifact dual-path hazard to guard — the D3-stripping-vs-same-artifact contradiction that a runtime switch would create does not arise. Hence no epoch bump and no derivation_commitment slot for the switch value. (The compiler/AGENTS.md contract — “any semantic change under materialize/prepare/evaluate MUST bump DERIVATION_SEMANTIC_EPOCH” — is satisfied vacuously: the semantic change rides the artifact hash, which the contract already covers, not the epoch.)

D4 — Migration and the elaboration switch

The switch is an elaboration-time flag, not a runtime evaluation mode. Env var, house OX_/OXC_ family: OXC_DEFEAT_ELABORATE (1 = elaboration compiles the defeat plane into strict rules per D1; 0 = elaboration emits the legacy executable defeat metadata for the retained runtime resolver). Flipping it selects which artifact elaboration produces for a given source, not which path a runtime takes over a fixed artifact — so the two settings yield two different artifacts whose hashes already separate every downstream cache (D3): no derivation_commitment change and no epoch bump accompany the flip. It is still a kill switch in the compiler/AGENTS.md sense — an emission switch that gates a semantic change is a kill switch too — and it obeys the same taxonomy (house-flag naming, staged default, incident-rollback reach); it simply discriminates via the artifact hash rather than a runtime branch.

• Phase 1: default 0 — elaboration emits legacy metadata; the compiled artifact is opt-in, exercised by the oracle in CI. The interpretive resolver is retained and drives legacy artifacts.

• Phase 2: default 1 — elaboration compiles by default; legacy emission reachable for incident rollback only. The resolver is retained through the soak (it still evaluates any legacy artifact and the rollback path).

• Phase 3: legacy emission removed and defeasible.rs deleted together. The resolver exists precisely to evaluate legacy artifacts, so it is deleted only when legacy emission is — one step, not two.

• Migration story.

  • (a) Old artifacts (legacy metadata, emitted before the flip) continue through the retained resolver during the soak window, unchanged and unaffected by the flip; recompiling their source under =1 produces the compiled artifact. The resolver is not deleted until legacy emission is (Phase 3), so no old artifact is ever left without an evaluator.
  • (b) The soak compares the two artifacts’ models — compiled vs legacy for the same source — which is exactly the oracle differential + EmitVectors (D5): one source, two elaboration outputs, model equality.
  • (c) Mixed deployments are forward- and backward-safe. A pre-rewrite runtime given a compiled artifact finds no defeat metadata (has_defeat_plane() false → strict path, projection_consume.rs:268) and evaluates the compiled strict rules correctly, with no resolver involvement (forward-compat verified in review). A post-rewrite runtime given a legacy artifact drives the retained resolver, unchanged.

• Rollout order. #1789 (#1788) lands first, on the interpreter — merged; its dependency-cone seeding fix and conformance ladder (the #1788 leak ladder) are the first course of the regression floor. The #1790 reinstatement fix and the interim fail-open hardening (#1796, cone-sensitive reentrancy) are still open on the interpreter; their conformance chains complete the floor. The compiled path must be oracle-clean on every case those fixes made pass, and must additionally fix the #1791 recursive-default case they leave open (the oracle’s known-failure entry for #1791 flips to agreement, which the harness’s stale-entry guard forces to be edited out).

• Acceptance gate. The compiled path is accepted when it is oracle-clean against the merged oracle (PR #1793): (a) zero new divergences over the deterministic CI seed set (the 64 pinned seeds run in-CI); (b) every pinned known-failure the rewrite fixes now agrees, forcing its removal from the expected-divergence list; (c) the env-gated soak (generated_differential_soak, OXC_DEFEAT_PLANE_SOAK=<count>; single-seed replay via OXC_DEFEAT_PLANE_SEED=<n>; run under binary(defeat_plane_oracle)) stays clean at the standing count. The accepted Phase-2 gate is the standing 1000-seed differential soak run clean against the flip candidate, alongside the deterministic per-CI 64-seed set (a). (An earlier revision named a one-off owner-scheduled acceptance-scale run of ~10⁶ seeds before the flip; that extra-large run was retired — the standing 1000-seed differential is the accepted gate, the 64-seed set runs per-CI.) Acceptance is soak-clean plus the emission vectors (D5).

D5 — The Lean golden transformed-program vectors (canonical-form check)

The oracle (D4) checks the compiled path against an independent reference evaluator. This RFD additionally commits to checking the production transform against the mechanized transform, rule-for-rule, via the existing EmitVectors infrastructure (spec/lean/EmitVectors.lean, lake exe emit-vectors <layer> → compiler/tests/lean-vectors/, replayed by a Rust conformance harness alongside conformance_replay.rs). Concretely, a new defeasible vector layer:

• Lean emits, per vector: the normalized defeasible input (clauses, rule identities, labels, default flags, resolved targets + bindings); the expected compiled strict program in canonical form (deterministic public-projection and $-helper names, heads, positive atoms, NAF atoms, canonical rule order); and the Lean-computed WFS result (true extents, undefined extents, proof-tag attribution). The compiled program is produced by Transform.lean’s construction, not hand-written.
• Rust asserts: (1) feed the normalized input through the production transform; (2) canonically serialize the emitted strict rules; (3) assert equality with Lean’s compiled-program payload — rule-for-rule, no missing or extra rules (this is the “byte-level transformed-program check”: canonical-form equality of the emitted rule set, not raw .oxbin bytes, which EmitVectors does not carry); (4) evaluate the produced program through Engine::evaluate; (5) assert true/undefined/proof-tag results equal Lean’s model. Steps 3 and 5 separately detect transform drift and evaluator drift.

Honest scope: EmitVectors emits computed semantic models, and its EvalProgram Term/AtomIR are oracle twins outside the Argon.lean mech-audited closure (spec/lean/AGENTS.md). The defeasible layer inherits that oracle-vs-canonical split; the canonical serialization it diffs against is the transform’s normalized output form, defined by this layer, not the canonical CoreIR shape.

D6 — Lean prerequisite (scoped here; delivered in PR #1797, merged)

Transform.lean must be lifted from defeat algebra over a converged contribution to the recursive fixpoint the compiled program computes (D2). This is the rewrite’s entry gate. It is scoped by this RFD and delivered (merged) in PR #1797 (spec/lean/Argon/Reasoning/Defeasibility/CompiledFixpoint.lean, ~635 lines added; no sorry, no axiom; the full Argon library builds). The transform emits an ordinary Datalog.Program whose wfTrue is the shipped semantics, reusing wfModel / wfTrue / wfModel_union_old — no second evaluator. PR #1797 (merged) introduced the obligations below and their theorems:

• Replace Clause.support : Set Tuple (an opaque converged input) with rule bodies interpreted against a global WFS approximation/model — reuse Reasoning/WellFounded.wfModel and the compiled-rule adequacy of Reasoning/Compiled (CRule.fire_eq_TP); do not define a second evaluator.
• Define qualified rule/head identity and the whole-program defeat DAG (the latter already decidable, DefeatGraph / decidableSelfLoop).
• Define the executable transform to a Datalog.Program: support relations, attacker-survival / blocking relations, per-clause NAF-guarded survival, and public-head projection.
• Prove: (i) emitted $-names are fresh (no collision with source vocabulary — the Extension.wfModel_union_old conservativity shape); (ii) the transform preserves safety/range-restriction (Compiled.Safe.head_determined, the OE1303 witness); (iii) a recursive clause’s support equals the transformed program’s WFS support projection (the F1 correspondence, proved for the block-free and stratified-defeat fragments in #134 Part A); (iv) induction over the acyclic defeat DAG yields F2/reinstatement (lift the existing pardoned_target_survives from opaque blocking to derived blocking under the fixpoint); (v) the public-head WFS projection equals declarative warrant (warranted), the D10.1 theorem now over the recursive construction; (vi) the result is independent of rule/head enumeration order (the property the interpreter’s memo violated — #1788); (vii) the emitted stratification keeps every negated blocking relation and the head that negates it in one WFS SCC (proved as negated_block_same_scc in CompiledFixpoint.lean) on a target↔attacker negative cycle, so the OE1365 cross-stratum-not-over-undefined gate (D2) never fires on a compiled defeat program — or, if a residual split shape is reachable, it is refused rather than silently under-defined.
• Retire the RuleStrength mirror with the surface triple (RFD 0028 D10.6) if not already gone.

Delivered status (PR #1797, merged), obligation-by-obligation. Obligations (i) rule bodies over a global WFS model with no second evaluator (emitted, wfTrue_mem_iff, wfPossible_mem_iff), (ii) fresh $-names / non-collision (internal_atoms_fresh, emitted_internal_HeadsIn; helpers_conservative is an abstract conservativity property over internal-avoiding base programs, never instantiable at emitted itself, whose public rules read internal atoms), (iv) preserved range-restriction (pubRules_range_restricted, blockRules_range_restricted), F2/reinstatement over derived blocking inside the fixpoint (block_extent_iff, derived_block_pardoned, derived_pardoned_target_survives), enumeration-order independence — the property the interpreter’s memo violated, #1788 (emitted is a Set; suppFromList_perm_invariant), and (vii) the emitted NAF staying within one WFS SCC so OE1365 never fires (negated_block_same_scc) are proved. The decision-table worked examples are discharged against Transform.warranted (the franchise ladder verdicts).

The stratified-defeat bridge — delivered (#134 Part A). Obligations (iii) recursive-support correspondence and (v)/(vi) public-head WFS projection = declarative warrant are proved for the block-free / positive fragment (pub_projection_blockfree) and for the stratified-defeat fragment — a head that is a live defeat target but whose defeat graph is acyclic (no target↔attacker mutual-defeat cycle). There the two-valued warrant genuinely exists and is bridged: the blocking layer is positive over the attacker’s public head, so given decided attackers it collapses to two-valued (block_two_valued, blockL_two_valued); the public head is the two-valued team-defeat fold over that fixpoint-derived blocking (pub_extent_iff); two-valuedness propagates from the attacker stratum to the target stratum (stratified_head_step); and for the acyclic non-recursive fragment the whole well-founded model is provably two-valued with no undefined atom (stratified_two_valued, stratified_wfModel_two_valued), witnessed end-to-end on a live-defeat program (voteLadder_two_valued, voteLadder_ben_definitely_false: ben’s franchise is definitely false, not undefined). This discharges the no-cycle half of (vii) for the acyclic non-recursive sub-fragment as a theorem-plus-inspection (stratified_wfModel_two_valued) rather than prose alone; the general no-cycle case with positive recursion inside a stratum remains the reduction named below.

What the mutual-defeat cycle is — a decision, not a remainder. For a head that is simultaneously recursive and a defeat target with a genuine target↔attacker negative cycle (D2 case 3 — a rule-dependency cycle through the attacker’s derivation, not the defeat-graph identity cycle OE0718 refuses), there is no two-valued declarative warrant to bridge to: the cyclic heads are undefined in the well-founded model, and — per RFD 0028 D6, meaning is the compiled program’s meaning — that three-valued reading is the canonical semantics. This is exactly the region where the deleted interpretive resolver was order-dependent (the topological memo / reentrancy guard / fail-open fallback produced an answer that depended on enumeration order); removing that defect family is a goal of this RFD, and emitted being a Set under wfTrue has no order to depend on (suppFromList_perm_invariant). So the cyclic case is not a debt tracked against #134 — it is a recorded outcome, load-bearing via (vii) (negated_block_same_scc) and now witnessed: on the worked two-head cycle program (acyclic defeat graph, negative rule-dependency cycle through each attacker’s support) both public heads compute to undefined in the mechanized well-founded model (cyc_a_undefined, cyc_b_undefined in CompiledFixpoint.lean) — the Can the reference chapter promises, produced by the fixpoint, not asserted in prose. Because that undefined outcome is surprising to an author who expected a definite verdict, elaboration now warns on the shape: OW0740 (mutual-defeat-cycle-undefined) detects the target↔attacker negative cycle over the resolved defeat edges + lowered rule bodies (representation-independent — it does not depend on the D4 elaboration switch) and names the mutually-defeating public heads. It is a WARNING, not a refusal — the outcome is canonical, not an error.

The genuinely-reduced residual. One narrow case remains reduced rather than re-proved: a head recursive through positive support within a stratum that is also an acyclic defeat target (positive recursion entangled with a satisfiable blocking guard). stratified_head_step is its stratification induction step; assembling it across a positive recursive cycle needs the standard “a positive/negation-free program’s well-founded model is its two-valued least model” fact, which the substrate does not yet carry. This is the only surviving #134 catch-up for the defeat plane; it does not block the Phase-1 opt-in path (oracle + soak cover it empirically) and it is named in CompiledFixpoint.lean’s honest-scope note rather than hidden in a sorry.

D7 — What dies, what remains

Deleted from oxc-runtime/src/defeasible.rs (the interpretive resolver surface):

• defeasible_survivors — the topological survivor traversal (the memo, the visiting reentrancy guard, the fail-open catalogs.support.clone() fallback);
• warranted_support_catalog, warranted_contribution_catalog, raw_classical_support_catalog, defeasible_clause_contribution — the catalogs re-seeded per head, and the per-clause attribution over them;
• DefeasibleSurvivorsMemo and the short-name keying throughout;
• strength_stratified_snapshot and the RFD-0026-era fused strict ∪ (defeasible \ defeater) fast path — superseded (the RuleStrength triple is retired surface).

The fail-open fallback (#1791) and the reentrancy guard have no counterpart in a compiled program: there is no runtime recursion to guard.

Remains in the runtime: nothing defeat-specific in the evaluation path. The public head extent comes from the compiled strict rules via the one Engine::evaluate path (compiler contract: one evaluation path). The reflection/audit projection is thin and read-only: ox derive --explain, provenance, and the D8 proof-tag surface read DefeatCompilationProvenance (D3), not a resolver. The #[default]/#[defeats]/#[label] reading, validation, resolution, and cycle refusal (OE0716–OE0721) stay in oxc-instantiate (defeasibility.rs, lower/defeat.rs) — that is the elaboration-side surface the transform is built beside, unchanged in what it validates; resolve_workspace_defeat_plane gains the emission step and the metadata-stripping/provenance-writing discipline (D3).

Other live consumers of the deleted catalogs — the reroute, named explicitly. Beyond the resolver internals above, three call sites read the deleted catalogs today. Under the one- Engine::evaluate model each reads the compiled public head via ordinary derived provenance instead; the DefeatCompilationProvenance carrier (D3) supplies any per-clause / proof-tag attribution these paths surfaced from the old catalogs:

• Check evaluation — oxc-runtime checks.rs, warranted_support_catalog (warranted_support_catalog). A check over a defeasible head reads the compiled public-head extent directly; the warranted support catalog is exactly what the compiled projection computes, so the read becomes the ordinary derived extent, no catalog.
• Projection-cache defeat-eligibility gate — projection_consume.rs:268, branching on has_defeat_plane(). A compiled artifact reports no defeat plane, so the branch takes the ordinary strict path and compiled defeat becomes projection-cache-eligible: an ordinary strict program is cacheable where the interpreted plane was gated out of the cache. This is an unstated positive consequence — promoted to D8.
• Scenario / snapshot path — derive_read.rs:1214/1223 (incl. strength_stratified_snapshot). Scenario snapshots read the compiled public-head extent through ordinary provenance; the RuleStrength-stratified snapshot is retired with the surface triple (listed in “what dies”).

D8 — Performance

The transformed program adds internal rules and atoms per defeasible head (support, blocking, projection), linear in clauses + edges. Cost model:

• More rules, but ordinary semi-naive incrementality applies — the emitted rules are normal IDB rules; the reasoner evaluates them with the same machinery as any program. The interpreter paid a per-query graph traversal with per-head catalog rebuilds (materialize_predicates_at cloned repeatedly); the compiled program pays one fixpoint over a larger rule set, amortized by the maintained model.
• The already-merged NAF memo / cone slicing optimizations apply to the internal blocking atoms for free — they are ordinary NAF atoms, indistinguishable to the optimizer from any other. The interpreter’s hand-rolled survivor traversal could benefit from none of them.
• Projection-cache eligibility, gained. A compiled defeat-bearing artifact reports no defeat plane (has_defeat_plane() false, projection_consume.rs:268), so it takes the ordinary strict path and becomes projection-cache-eligible — the interpreted plane was gated out of the persisted cache; the compiled program is cached like any strict program (D7).
• DBSP-ready (RFD 0018): the compiled plane is the Maher three-stratum form that lifts into the circuit; incremental maintenance of defeasible heads comes from the circuit compiler with no defeat-specific operator.

Benchmark plan: the oracle’s generated programs at scale (the soak corpus at high seed counts, as a throughput probe alongside its correctness role); and defeasibility enters plan_bench — a defeat-bearing program family added to the standing benchmark set, measured dispatch and batched, compiled vs the (retained, Phase-1/2) interpreter as the baseline arbiter at small N.

D9 — Cross-module defeat and future work

RFD 0082 (cross-module defeat) requires defeat-edge resolution across the workspace-combined artifact rather than per file (RFD 0028 D3’s v1 file-local narrowing, #362). The compiled transform honors this by construction: it runs at lowering over resolved edges, and lifting resolution to the combined artifact changes only which edges reach the transform, not the transform. Qualified $-naming (D1) means #1792’s short-name collision folds in for free — cross-module same-named heads produce distinct qualified internal relations.

Rationale

• The fixpoint belongs to the evaluator. The interpreter re-implemented a well-founded fixpoint by hand — topological order, memo, reentrancy guard — and every defect is a way that hand-rolled fixpoint diverges from the real one under order, scope, or keying. Compiling to strict rules hands the fixpoint back to the machinery that is proven to compute it (Reasoning/WellFounded, AFT, the differential oracle). Three of four defects vanish structurally, not by patch.
• RFD 0028 D6, honored. “The meaning of a #[default]/#[defeats] program is the meaning of its compiled core program” stops being aspirational: the compiled program is the only program. D5 hook 3 (the transform slot) is used as designed.
• Circuit alignment is free, not engineered. Compiled defeat is already inside DBSP’s proven fragment (RFD 0018); the interpreter would have been a permanent exception in the circuit.
• The oracle makes acceptance objective. PR #1793 is a differential the rewrite either passes or does not; the Lean golden vectors add a mechanized transform-drift check on top.

Alternatives considered

• Patch the resolver in place. Rejected. #1789 patched one trigger; the fail-open branch is still reachable (#1791), and the memo/order/keying dependence is intrinsic to interpreting a fixpoint. Each patch narrows the divergence without removing its cause.
• Refuse recursive #[default] dependencies (the D2 track-(a) alternative). Rejected as the semantics track: it refuses legitimate WFS-native Datalog (self- and mutual positive recursion), conflates rule-dependency edges with defeat edges, and preserves an interpreter limitation after compilation removes its cause. Retained only as a possible temporary migration gate with a diagnostic distinct from OE0718 — not the shipped semantics.
• Keep executable defeat metadata + a runtime discriminator (instead of stripping it, D3). Rejected: an old runtime ignores the discriminator and re-interprets the retained markers — double application. Stripping to a self-contained strict program is the only backward-safe form.
• Behavioral-only golden vectors (input + expected warranted model, no compiled-program check). Rejected: it detects evaluator drift but not transform drift; the RFD wants both (D5 steps 3 and 5).
• A core_ir version bump for the internal heads. Rejected: no IR shape changes; a minor bump does not protect against the double-application hazard anyway (the format gate accepts future minors) — the strip-and-provenance discipline (D3) is what protects.

Consequences

• The Lean prerequisite (D6) is delivered in PR #1797 (merged; CompiledFixpoint.lean) plus the #134 Part A stratified-defeat bridge: recursive-support / warrant (iii)/(v)/(vi) proved for the block-free and stratified-defeat (acyclic) fragments, with provable two-valuedness (no undefined) on the acyclic non-recursive fragment. On a genuine target↔attacker mutual-defeat cycle the heads are undefined and that is the semantics (RFD 0028 D6) — not a bridge to build. The only surviving reduction is the positive-recursive-stratum two-valued lemma.
• #1789 has merged (regression floor, first course); the #1790 reinstatement fix and the interim fail-open hardening (#1796) are still open and complete the floor. #1791’s semantics are settled here (admit, define). #1792 folds in via qualified naming.
• A .oxbin format minor bump is owed (the additive DefeatCompilationProvenance carrier); no DERIVATION_SEMANTIC_EPOCH bump and no Core-IR bump. The switch is elaboration-time, so the artifact hash — not the epoch — separates compiled from legacy caches (D3/D4).
• oxc-runtime/src/defeasible.rs is deleted at Phase 3; the runtime carries no defeat-specific evaluation, only a read-only provenance projection for explain/audit.
• Defeasibility becomes DBSP-incrementalizable with no special case (RFD 0018).

Open questions

• The exact DefeatCompilationProvenance shape and whether it is a new .oxbin section or an extension of an existing metadata section — a lowering/format detail settled at implementation.
• Whether the temporary refusal gate (the rejected D2 track-(a)) is worth landing for Phase 1 as a belt-and-suspenders guard while the recursive theorems (D6) are in progress, or whether the oracle + soak are sufficient assurance for the recursive cases from the start.
• Proof-tag attribution for undefined tuples on a target↔attacker negative cycle (D2 case 3): the Governatori four-tag scheme (+Δ/−Δ/+∂/−∂) maps cleanly onto true/false extents; the tag for a WFS-undefined defeasible tuple is a D8 mapping question deferred to the provenance layer.

Relationship to existing records

• RFD 0028 — the semantics this RFD realizes, unchanged (D1–D11). This RFD changes only where strategy #1’s compilation runs (D5 hook 3 → elaboration).
• RFD 0018 (incremental rule circuits) — compiled defeat is inside the proven incremental fragment; the alignment motivating this RFD (Context, D8, D9).
• RFD 0072 — the projection-cache validity contract (artifact hash + derivation commitment) that makes the cache-discriminator reasoning load-bearing: the elaboration-time switch separates caches by artifact hash with no epoch bump (D3/D4).
• RFD 0082 (cross-module defeat) — honored by construction; the transform runs over resolved edges regardless of resolution scope (D9).
• #1788 / PR #1789 (merged), #1790, #1791, #1792 — the bug family; the shape classes (Context) and the structural fixes (D2, D7, D9).
• PR #1796 — interim fail-open hardening (cone-sensitive reentrancy) of the soon-to-be-deleted resolver guard; references #1791, does not close it (the compiled path deletes the guard).
• PR #1793 (merged) — the acceptance oracle (D4) and the Phase-2 golden-vector path (D5).
• PR #1797 — the Lean entry gate (CompiledFixpoint.lean, D6, merged): the recursive-fixpoint transform correctness, all obligations proved bar the positive-recursive-stratum reduction.
• #134 — the WFS mechanization catch-up; D6’s theorems (iii)/(v)/(vi) plus the #134 Part A stratified-defeat bridge remove its narrowing for the defeat plane on the block-free and stratified-defeat (acyclic) fragments. The mutual-defeat-cycle case is undefined-by-decision, not an open bridge; the only surviving catch-up is the positive-recursive-stratum two-valued lemma.