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 0039 — Composable mutations: nested invocation and derived reads

  • State: accepted — implemented (nested invocation Operation::Invoke #566; derived-extent reads Operation::ForEach #571; closed-nesting soundness mechanized on the never-merged scratch/nested-mutation-soundness branch)
  • Opened: 2026-06-19
  • Decides: how a mutate body (1) invokes another mutation — including a trait mutate member — and (2) reads the deductive plane (a derive/query result) to drive effects, so that the “rules that apply rules” pattern is expressible inside the language rather than only via host-side orchestration. Builds on RFD 0015 (the atomic buffer→prevalidate→commit body), RFD 0025 (the check delta-guard), RFD 0026 (trait members + receiver dispatch), and the pipeline slot RFD 0035 D1 reserved for mutations.

This RFD is Lean-first where it touches soundness: the atomicity of nested composition and the confluence of snapshot reads are the executed meaning, held in spec/lean/Argon/Runtime/ (extending MutationSemantics.lean’s runMutation_error_noop) and gated by the differential oracle. The surface grammar, the operation IR, and the call-graph analysis are engine architecture settled here. It commits a plan, folded into the implementing PRs per the discussion-first practice.

Question

A modeler writes a generic workflow rule as a trait and an impl:

pub trait Rule {
    derive Applicable(Self)
    mutate Apply(self)
}
impl Rule for LateFeeRule {
    derive Applicable(rule: Self) :- /* … conditions over rule.* … */
    mutate Apply(self) { /* create a RightDutyPair; enqueue a WorkflowRequest; update self.applied = true */ }
}

The deductive half works — Applicable(rule) derives, and a query returns the applicable rule ids. The modeler then wants to apply them, in Argon:

pub mutate ApplyApplicableRules() {
    for rule in Applicable {        // read the derived set
        Rule::Apply(rule);          // invoke each rule's mutation
    }
}

Today neither line works. There is no operation for invoking a mutation — a call in statement position is silently dropped (oxc-instantiate/src/mutate_lower.rs, the _ => {} arm of lower_stmt_expr) — and there is no path from a mutate body into the reasoner, so a for cannot range over a derived predicate. What are the correct semantics for a mutation that calls a mutation, and for a mutation that reads a derived set to drive its effects?

Context

The two-plane substrate

Argon already firewalls a deductive plane (derive/query: monotone, fixpoint, no effects) from an effect plane (mutate: insert/update/delete, executed as one atomic all-or-nothing transaction over a discardable overlay — RFD 0015, proven by runMutation_error_noop in Runtime/MutationSemantics.lean). The check delta-guard (RFD 0025) already invokes the reasoner over the committed ⊎ buffered overlay at one defined point, so a controlled deductive read at a transaction boundary is not a new capability — only a newly surfaced one.

Trait-member dispatch already works

RFD 0026’s receiver dispatch is live at runtime: resolve_mutation_invocable recognizes a trait-member callable, member_receiver_individual extracts the self receiver from the args map, and select_member_impl picks the unique covering impl by the receiver’s actual classification (refusing on zero or on <:-incomparable multiple covers). What is missing is (a) self lowering in expression position (a separate bug, #550) and (b) an operation that drives this dispatch from inside a body.

Prior art (the design is not invented here)

Six independent traditions converge on one model:

  • Transaction Logic (Bonner & Kifer, TCS 133, 1994): a transaction is evaluated over a path of states; serial conjunction ⊗ is “do φ then ψ”; a sub-transaction call splices its body inline into the caller’s path, so the whole transitive call tree is one path that commits-or-aborts wholesale by construction. Tests (reads) interleave with updates and see prior writes.
  • Nested transactions / closed nesting (Moss 1981; Gray & Reuter savepoints): a subtransaction’s effects merge into the parent on subcommit and become durable only at top-level commit; a child abort is a partial rollback the parent may catch. Closed nesting is exactly the model that preserves top-level all-or-nothing.
  • Dedalus / Bloom + CALM (Alvaro, Hellerstein et al.): deductions are instantaneous within a step over a frozen snapshot; state change is deferred to a step boundary. CALM explains why: applying a non-monotone write (delete/aggregate) mid-fixpoint makes derivations order-dependent and destroys confluence.
  • LogicBlox / Rel (Aref et al., SIGMOD 2015; RelationalAI 2025): EDB/IDB firewall; updates are a delta plane recomputed over an immutable snapshot at named stages (@start/@final); one composite transactional fixpoint; integrity checked at the boundary, abort wholesale.
  • Active-rule termination & confluence (Aiken, Widom, Hellerstein, SIGMOD 1992): set-oriented (statement-level) firing over the net-effect delta; termination guaranteed by an acyclic triggering graph (sufficient, conservative); confluence requires commutativity over the transitive-trigger closure.
  • Golog / IndiGolog and Flix: a body as an ordered sequence of tests and primitive actions with read-your-writes; a static type-and-effect wall with effect polymorphism (a caller’s effect subsumes its callee’s, by inference).

Decision

D1 — A mutate body is reads-over-a-snapshot serially composed with deferred writes

The guiding principle, and the one-line semantics:

A mutate body is a serial composition of state-preserving reads (against the deductive-fixpoint snapshot) and deferred writes; a sub-mutation call is closed-nested — its writes merge into the parent’s single transactional buffer and become durable only at the top-level commit, so the whole transitive call tree is one atomic all-or-nothing unit.

D2 — Nested invocation: Operation::Invoke, closed-nested

Add an Operation::Invoke { callable, args } to the core IR. At runtime it does not call execute_mutation (which commits and runs its own check cycle). It resolves the callable (reusing resolve_mutation_invocable + select_member_impl) and runs the callee’s operations into the caller’s BodyExec — the same pending effect buffer and collections overlay — under a child binding scope for the callee’s parameters. That is closed nesting realized directly on the RFD 0015 overlay: effects merge up, the check delta-guard runs once at the outer commit, and atomicity composes for free.

  • Termination: the mutation call graph must be statically acyclic in v1 (no recursive mutation cycles). This is the decidable, safe choice and matches the decidability-tier philosophy. Mutual recursion / fixpoint-to-quiescence is a separately-gated future feature.
  • Failure: a sub-mutation’s failed require aborts the whole top-level transaction. Argon has no try/recover surface; catchable savepoint-style partial rollback is a deliberate deferral (it needs a recovery construct first).
  • Effect discipline: adopt the call-purity ladder fn ⊆ query ⊆ derive ⊆ mutation; a caller may invoke only equal-or-lower-impurity callees, and mutation → mutation composes into one atomic transaction. The effect is inferred (Flix-style polymorphism), not annotated.

D3 — Derived reads: snapshot at a fixpoint boundary, set-oriented, fire-once

A for x in <derived-extent> iterates a snapshot of the derived predicate taken at the deductive fixpoint of the body-entry state — never a partially-applied relation (CALM). This needs a read-goal term that invokes the reasoner from the mutation runtime, which is the mutation slot RFD 0035 D1 reserved.

  • Default = snapshot-once: compute the applicable set at entry, fire each Apply exactly once. Trivially terminating; confluent when the rule mutations have disjoint footprints. This is the set-oriented / statement-level reading.
  • Iterate-to-quiescence (recompute the set after each firing) is a strictly-more-expressive, strictly-more-dangerous later feature, gated on a static acyclicity check of the triggering graph (the stratification analysis in another hat) plus a loud runtime iteration bound. Not in v1.

D4 — Keep the two planes’ read semantics distinct

The apparent tension between Transaction-Logic read-your-writes and CALM snapshot-reads dissolves once the planes are separated:

  • Reading a derived predicate → a stable snapshot at a fixpoint boundary (D3).
  • Reading the body’s own direct writes (a scalar/collection it set) → read-your-writes (already partial via buffered_collection, RFD 0015 RC2).

Rationale

The decision is the intersection of all six traditions, and — crucially — it requires no new execution substrate. Operation::Invoke-into-the-parent-BodyExec is simultaneously Transaction Logic’s serial-conjunction splice, Moss’s closed-nested merge-up, and Bloom’s defer-to-boundary; the snapshot read is LogicBlox’s staged @final and Dedalus’s frozen-snapshot fixpoint; the fire-once default is Aiken–Widom–Hellerstein’s set-oriented semantics with a guaranteed-terminating triggering graph. Each maps onto machinery Argon already has (the overlay, the reasoner-over-overlay in check discharge, the stratification/tier analysis), which is why the soundness obligation is an extension of an existing theorem rather than a new framework.

Alternatives

  • Open nesting (a sub-mutation’s effects escape early, atomicity restored via compensating inverses). Rejected: it breaks top-level all-or-nothing and owes hand-written inverses; closed nesting is strictly safer and is what the overlay already supports.
  • Iterate-to-quiescence as the default. Rejected as default: it is what some workflow modelers expect, but it is exactly where non-termination and order-dependence live. It is offered only behind the static guard above.
  • Nested calls each commit independently (no closed nesting). Rejected: it shatters atomicity — a failure in a later sub-call could not undo an earlier committed one — contradicting the §7.5 “any error emits nothing” guarantee.
  • Host-side-only orchestration (the status quo: query, then loop and dispatch from the SDK). Retained as always-valid, but insufficient — and even it was blocked by the self bug (#550). “Rules that apply rules” is a first-class modeling pattern, not glue.

Consequences

  • A new Operation::Invoke IR variant and a read-goal term; the lowering replaces the silent _ => {} drop. The runtime threads Invoke into the current BodyExec rather than a fresh one.
  • The Lean gains a closed-nesting atomicity lemma (composition preserves runMutation_error_noop) and a snapshot-read confluence statement; the differential oracle gates the executor.
  • The reference manual §7.5 grows the invocation and derived-read forms; §7.7 (emit/sinks) is orthogonal.
  • Supersedes the nested-call scope creep folded into #74. Tracking issue: #551.

Soundness plan (Lean-first, scratch-mechanized before the executor)

Per the discipline that novel soundness frameworks are mechanized in scratch Lean before implementation and held by the differential oracle, here is the obligation, scoped against the existing model in Argon/Runtime/MutationSemantics.lean.

What the existing model already gives us (verified)

  • A mutate body is evalMutate : MutateDecl → Env → ReadView → Except Abort (List Effect × Value). It threads a MutState := { fresh, effects : List Effect } through evalStmts; the read-view rv is a read-only argument — it never changes during a body. Effects accumulate in MutState.effects; commit folds applyEffect over them only on the .ok branch; runMutation no-ops on .error (runMutation_error_noop, require_fail_atomic).
  • Consequence for D3 (snapshot read), already structural: because rv is read-only through evalStmts/evalExpr, any derived read inside a body observes the body-entry committed state by construction. The v1 snapshot semantics needs no new invariant — it is the only thing the model can express. (The overlay-staged re-derivation variant — the iterate-to-quiescence door — is what would require new machinery.)

What to add

  1. A statement constructor Stmt.invoke (callee : MutateDecl) (args : List Expr) (the Lean image of Operation::Invoke).
  2. An evalStmt (.invoke callee argExprs) case that evaluates the argument expressions against the current (env, rv, st), binds the callee’s parameters, and runs the callee’s require guards + body statements into the same MutState — appending the callee’s effects to st.effects and threading st.fresh. Aborts propagate through Except unchanged.

Theorems to prove

  • T1 — Closed-nesting atomicity (the headline). For any body containing invoke statements, runMutation is all-or-nothing: if evalMutate = .error err then runMutation = rv. Strategy: this is runMutation_error_noop unchanged — it depends only on evalMutate returning effects solely on .ok, which the shared-buffer/Except-propagation invoke case preserves. The proof lifts for free; that is the entire point of running the callee into the parent buffer rather than committing it.
  • T2 — Effect-buffer monotonicity. On .ok, an invoke extends st.effects by exactly the callee’s emitted effects (a list append), in callee-emission order spliced at the call site — the Lean form of Transaction Logic’s serial-conjunction splice / Moss’s merge-up. Grounds “the transitive call tree is one effect list committed once.”
  • T3 — Fire-once confluence (D3). For a snapshot set S iterated by for x in S { Apply(x) }, if the per-element effect sets have disjoint footprints (no two write the same (id, field) / (id, concept) / relation tuple), then commit is independent of the iteration order of S. Strategy: a commutativity lemma on applyEffect for footprint-disjoint effects, lifted over foldl.

Mechanization result (scratch branch scratch/nested-mutation-soundness)

A faithful self-contained miniature of MutationSemantics.lean proved all three (zero sorry/axiom; only propext/Classical.choice/Quot.sound), with one consequential refinement on T3:

  • T1 and T2 lift cleanly, no extra hypotheses. runMutation_error_noop survives the shared-buffer Stmt.invoke verbatim — confirming the formal payoff of run-into-parent over commit-nested.
  • T3 holds only up to observational equivalence, not structural equality — and this is mechanized as a counterexample theorem, not a caveat. The literal goal commit (commit rv A) B = commit (commit rv B) A is false even for footprint-disjoint effects, because applyEffect prepends to the classification/relation lists ((id,c) :: …, as the production applyEffect does too), so two disjoint asserts land in opposite list order. Confluence is true against an Obs interface — equal classification/relation membership, equal property lookups, equal nextFresh — i.e. up to what reads can observe. T3 is proved up to Obs, lifted over List.Perm.

Consequence for the executor. Order-independence of the apply-all loop is a read-interface property, not a representation property. The Invoke executor needs no commit-order canonicalization provided reads go through the membership/lookup interface, and the differential oracle must compare observable reads, not raw buffer/store layout.

The one new obligation: termination

Adding invoke breaks the structural termination_by (sizeOf s, 0) measure — a call runs the callee’s body, which is not a sub-term of the call statement. This is precisely why D2 mandates a statically acyclic mutation call graph: it is what makes the composed evaluator terminating and the recursion well-founded. Two encodings, in increasing fidelity:

  • (a) Fuel/gas — a depth parameter that decreases per invoke; models the runtime depth bound. Cheapest; lets T1–T3 be proved immediately, parametrically over fuel.
  • (b) Well-founded recursion on the acyclic call-graph rank — measure = (topological rank of the callee in the dependency DAG, then sizeOf within a body). This is the faithful image of D2’s static check and the honest termination story; it is the harder mechanization.

Recommended cut: prove T1–T3 under (a) fuel first (they are about atomicity/confluence, orthogonal to why evaluation terminates), and discharge termination separately under (b) as the acyclicity decision’s own lemma. Keep all of this on a scratch branch (never merged); the differential oracle gates the Rust executor against the executed meaning, exactly as for the reasoner.

Open questions

  • Lean first: mechanize closed-nesting atomicity and snapshot-read confluence in scratch Lean before the executor lands (the F2.4 bar). What is the minimal lemma shape that composes with the existing overlay proof? Resolved (scratch branch scratch/nested-mutation-soundness): T1/T2 lift unchanged; T3 confluence holds up to observational equivalence (see Mechanization result above). The minimal shape is runMutation_error_noop verbatim for atomicity + an Obs-quotiented commutativity for confluence.
  • Dispatch over buffered classification: should select_member_impl at an Invoke site read the receiver’s buffered (read-your-writes) classification or the committed one? Committed is the v1 answer; buffered is a coherent enhancement once scalar RYW lands.
  • Derived-read staging: is the snapshot taken at body-entry committed state, or re-derived over the committed ⊎ buffered overlay at the point of the for (as check discharge does)? D3 fixes v1 at body-entry; the overlay-staged variant is the iterate-to-quiescence door.
  • Quiescence guard: the exact triggering-graph construction over mutation effects and its relationship to the existing stratification pass.