RFD 0076 — Mutability of relation ends

• State: discussion
• Note: landing as a staged design record; enforcement arrives in the check, write, and durable slices — canonical spec text describing this rule is not provisional.
• Opened: 2026-07-12
• Decides: whether relation ends adopt the field-mutability rule — immutable unless declared mut — and what the write path, tuple lifecycle, and reflection plane must enforce for an immutable end.
• Affects: relation declaration syntax; the write-path gate; the reflection plane; the ArgUFO vocabulary package (arg_ufo/relations.ar, arg_ufo/metarels.ar — external to this repository)

Summary

Argon fields are immutable post-construction unless their declaration places mut before the field name. This RFD applies the same rule to relation ends:

rel-param ::= 'mut'? Ident ':' TypeExpr

Every relation end is immutable unless it is declared mut. The modifier is written immediately before the end name, not after its type:

pub rel bindsSpouse(mut marriage: Marriage, spouse: Person) [0..1] [2];

Here marriage is mutable and spouse is immutable. There is no immutable keyword, [immutable] suffix, or relation-wide immutable modifier; the absence of mut is the immutable spelling.

The analogy with properties stops at the declaration posture. Relation ends are not assignable fields: Argon never updates the individuals in an asserted tuple. A change retracts the old relation assertion and inserts a new one. Under this proposal, if an end is immutable, the old assertion cannot be retracted while its dependent individual remains; retracting that dependent would automatically retract the relation assertion.

Problem

UFO makes strong modal claims about certain relation bindings, and ArgUFO can currently only document them:

• Existential dependence. Relators, modes, and qualities existentially depend on the individuals they bind. The binding is rigid: an aspect inheres in exactly one bearer for its whole existence. A specific headache that inheres in Alice cannot be rebound to Bob; a marriage mediates the same spouses for as long as it exists. The [1] bracket on InheresIn’s bearer caps the count (OE1341), not its stability: delete the edge to Alice and insert one to Bob and the cap is never exceeded. The immutable-end gate must refuse retraction of the Alice tuple while the aspect still exists. The legal way to end the binding is to retract the dependent aspect, which cascades the relation retraction.

• Essential parts. A person cannot continue as the same individual after replacing their brain. A direct retraction of hasBrain(person, brain) would leave that replacement path open. With an immutable brain end, the person must be retracted first; the parthood assertion then disappears by cascade.

• Immutable perdurants. metarels.ar repeatedly notes that events are immutable and exist only once they have occurred. The event-part relations (participational, structural, temporal) and the event-linking relations (creation, termination) should therefore keep their asserted endpoint bindings stable.

The write path currently accepts direct tuple retractions and replacements that violate those constraints.

Motivation

Relation-end mutability should follow the field-mutability rule rather than introduce a second modifier system:

The immutable default is also the safer ontology-authoring default. Stable bindings need no annotation, while a contingent binding is visible at its declaration site. It gives the write path a declaration-level stability bit that cardinality alone cannot provide. Relations retain their tuple semantics: mut controls whether assertion history may vary at an end; it does not make that end an assignable location.

Scope / non-goals

• Covers asserted, subsumed, and rule-derived extent changes for declared relations: logical tuple retraction, replacement by a distinct assertion, and constrained cascade retraction when a dependent context ends. It does not cover pure derive/query heads, tuple ordering, or uniqueness.
• Does not introduce immutable, const, [immutable], or a relation-wide mutability modifier. Absence of mut is sufficient.
• Does not introduce relation-end update or stable relation-binding identity.
• Specifies the required individual-retraction cascade. The source spelling for requesting a RetractIndividuals set is decided: retract x; for a single individual and retract {x, y}; for a set, lowering to the kernel RetractIndividuals effect. The source forms are documented in the mutate chapter (spec/reference/src/declarations/rules/mutate.md).
• Initially enforces lifetime semantics only for identity-bearing dependent contexts. An unsupported primordial or reference-valued context is rejected unless the corresponding end is mut.
• Keeps transaction-time correction distinct from ordinary relation deletion. Its surface and authorization are specified here (the amendment section: amend, capability-gated); its enforcement is a later implementation slice.
• Enforces the lifetime-bound relation needed by essential parthood; other ontology-specific consequences of termination remain separate constraints.
• Does not decide relation-body field mutability or its update surface.

Proposed solution

Four coordinated pieces: syntax, tuple-lifecycle semantics, enforcement, and reflection.

1. Syntax — mut before the relation-end name

Extend the existing relation parameter grammar with an optional mut before the identifier:

rel-param ::= 'mut'? Ident ':' TypeExpr

Examples:

// A material relation. People may work for different organizations throughout
// their lives; organizations may have different employees over time.
pub rel worksFor(
    mut employee: Person,
    mut employer: Organization
) [0..*] [0..1];

// A mediation relation. A particular marriage cannot involve different
// spouses, while a person may participate in different marriages throughout
// their life.
pub rel bindsSpouse(
    mut marriage: Marriage,
    spouse: Person
) [0..1] [2];

// An essential-parthood relation. A person cannot have a different brain.
pub rel hasBrain(
    mut person: Person,
    brain: Brain
) [0..1] [1];

hasBrain illustrates the immutable binding of a person to a particular brain. Under this proposal, hasBrain(person, brain) cannot be retracted directly while person exists; retracting person would automatically retract the relation assertion.

The ordering matches field declarations: if relation-end attributes are added later, their order is attribute* mut? Ident. This RFD does not introduce relation-end attributes.

Mutability is declared on concrete relation ends. This RFD does not add mut to metarel signatures or define metarel-level inheritance. A vocabulary that requires a position to remain immutable can reject a concrete relation’s mut opt-out through the reflection check below.

Ordinary relation subsumption does constrain mutability. A child relation may tighten a parent mut end by omitting mut, but it may not weaken an immutable parent end. Effective mutability at position i is therefore conjunctive over the relation and every transitive superrelation at that position. Declaring mut where any applicable parent is immutable is rejected with a RelationEndMutabilityWeakening diagnostic.

Relation-body field declarations are syntactically unchanged. Their mutation semantics remain the separate relation-tuple-field question reserved by Argon RFD 0006; endpoint mut does not decide it.

2. Tuple lifecycle — retract, then insert

A relation assertion is an immutable proposition. Its endpoint values are never updated in place, and this RFD adds no relation-target update form. A logical relation change uses the existing tuple operations:

pub mutate changeEmployer(
    employee: Person,
    currentEmployer: Organization,
    newEmployer: Organization
) {
    delete worksFor(employee, currentEmployer);
    insert worksFor(employee, newEmployer);
}

Surface delete R(args) retracts every live assertion matching that exact tuple proposition; insert R(args) appends a separate assertion. The two operations may be atomic members of one mutation, but they do not preserve or update a relation-instance identity.

Mutability is interpreted positionally, using the same fixed-complement rule as cardinality. For endpoint i, hold every other endpoint fixed. Those other arguments form the dependent context for the value at i:

A dependent context is live while all of its endpoint individuals exist. For each endpoint and live context, consider the set of asserted values at that endpoint:

• if endpoint i is mut, that set may grow or shrink while the dependent context survives, provided the transition satisfies every other end’s lifetime gate;
• if endpoint i is unmarked, its complete value set is established atomically by the first transaction that asserts that endpoint fiber. Every value for the fiber must be present in that initialization transaction; after commit, the set cannot grow, shrink, or substitute members while the dependent context survives;
• the initialization set remains governed by the declared cardinality. The two immutable spouse tuples required by bindsSpouse(...)[2] must therefore be asserted together when that marriage binding is initialized.

For a binary relation, the dependent context is the individual at the opposite end. Therefore:

• both ends of worksFor are mut, so the old tuple may be retracted directly before the new tuple is inserted;
• spouse in bindsSpouse is immutable, so Marriage is the dependent individual. Retract the marriage first; its bindsSpouse tuples are then retracted automatically. The mut marriage end permits a surviving person to participate in another marriage later;
• brain in hasBrain is immutable, so Person is the dependent individual. Retract the person first; hasBrain(person, brain) then retracts by cascade.

For an n-ary relation, the fixed complement contains more than one individual; mut alone does not designate one distinguished owner among them. The complement is treated as the dependent context collectively, and that context ceases when any one of its individual members is retracted. A vocabulary that requires one distinguished dependent must declare that role separately.

This lifecycle rule initially applies only when every member of the dependent context is an identity-bearing individual. Primordial values and references have no individual lifetime to retract. Until a separate rule exists, a declaration that leaves an end immutable when its dependent context contains such a value is rejected with an ImmutableRelationEndNonIndividualContext diagnostic; the modeler must mark that end mut.

3. Enforcement — retraction and replacement gates

The write path enforces the declaration in three places:

1. Explicit tuple retraction. First locate the exact live tuple named by delete R(args). If no tuple matches, deletion remains an idempotent no-op. If a tuple matches and any endpoint is unmarked, reject direct deletion with a newly allocated ImmutableRelationEndRetraction diagnostic. Because deleting one tuple removes one value from every endpoint fiber, direct tuple retraction is admitted only when every end is mut.
2. Tuple assertion. insert R(args) continues through the existing existence, endpoint-type, and cardinality gates. For an uninitialized immutable fiber, all values inserted for that fiber in the transaction form its initial frozen set. For an initialized immutable fiber, inserting an already-active tuple remains idempotent, but a new value is rejected with an ImmutableRelationEndInsertion diagnostic.
3. Individual retraction. Before applying effects, collect the transaction’s complete set of logical individual retractions and validate it atomically. For every incident tuple and every unmarked endpoint, at least one individual in that endpoint’s dependent context must belong to the set. Otherwise the transaction is refused: retracting brain cannot leave its dependent person alive, and retracting spouse cannot leave its dependent marriage alive. When the condition holds, incident relation facts retract by cascade.
4. Subsumed and derived extent deltas. After relation-subsumption closure and dependency maintenance compute the transaction’s net extent delta, apply the same initialization and retraction gates to every affected declared relation. This includes parent-relation rows contributed by a child and facts derived by rules whose head extends a declared relation. A premise retraction that would make such an immutable derived binding disappear while its dependent context survives refuses the whole transaction; declared relation heads do not bypass mutability merely because no source delete names them directly. The gate has no plane exemption: a standpoint’s composed view — its own facts and rules together with the DEFAULT layer that restricts into every view — is an extent of the declared relation, so a premise write that varies an immutable derived binding in any standpoint’s view refuses exactly as one that varies the base view, whichever plane owns the rule and whichever owns the premise. The freeze witness reads each plane’s own retained assert-polarity history (the DEFAULT layer for the base view, DEFAULT plus the standpoint’s layer for a scoped view): a scoped fiber initialized by a scoped assertion is frozen by that assertion, not deferred with the derived-only residue. (The cardinality gate set the plane precedent — a scoped tuple counts toward a declared cap; gate 1’s base-plane delete match under “Compatibility and migration” is a plane-locality rule for locating the named assertion, not a mutability exemption.) Pure pub derive or query heads with no relation declaration have no end-mutability metadata and remain outside this RFD.

The third rule is conjunctive across all immutable ends. For binary R(a, b) with both ends immutable, retracting only a is insufficient because b is still the dependent context for the immutable a end; both participants must be in the same logical retraction set. For n-ary relations, retracting any one member makes that particular dependent context non-live, but every other immutable-end context must still pass independently.

This closes the delete-then-insert loophole. A direct delete is refused for any tuple with an immutable end. The only legal removal is a cascade whose dependent-context closure passes, after which the removed individual cannot be used as an endpoint of a replacement assertion. (One bounded residue of this no-reuse guarantee — a fiber initialized only through the derived plane, re-derived after identity resurrection — is deliberately deferred and pinned; see “The erasure channel is gated, and one bounded residue is deferred” below.)

Individual retraction and cascade are implementation prerequisites

Argon currently has no ordinary logical individual-retraction statement. delete iof(x, T) only declassifies x from T, while forget x physically erases history; neither is the lifecycle operation required here. This RFD introduces a kernel RetractIndividuals effect over a finite set of identities; a singular lifecycle request lowers to a singleton set. After the dependency-closure gate above succeeds, it atomically appends retractions for every live identity-bearing base event owned by or incident to each selected individual: positive and refuted classifications, individual-property assertions and individual-valued property references, and positive and refuted relation tuples. Normal dependency maintenance then revises derived facts. History is retained; after the operation, no live event introduces or references a retracted individual.

The source spelling of RetractIndividuals is retract x; (single) and retract {x, y}; (set), lowering to the kernel effect; its gates are part of this proposal. Relation-end mutability cannot ship until that operation and its constrained cascade are implemented; neither delete iof nor forget may stand in for it.

No stable relation-binding identifier is required. The old and new tuples remain distinct propositions identified by their relation and arguments.

The erasure channel is gated, and one bounded residue is deferred

forget remains the privileged physical-erasure channel (build-time capability, separate authorization), not a lifecycle operation — but at transaction time the binding an erasure would remove is still live, so the erasure operation runs the same dependent-context coverage as RetractIndividuals over its target’s incident tuples: erasing a value-side individual while the dependent context survives is refused exactly as the cascade would be. forget therefore cannot stand in for a refused cascade. Erasing the dependent itself remains legal and takes its incident bindings with it, mirroring the cascade direction this section prescribes.

The freeze witnesses read retained assert-polarity history, and a committed erasure retains none: after forget x, no assert-polarity event on any plane or polarity introduces or references x (relation arguments walked into nested collection values), and the target’s pre-existing closing retractions are erased with their asserts. Physical erasure is that gate-and-read-visible guarantee, and its safeguard is the authorization boundary, not the lifecycle gates. Two replay artifacts are retained by design and are pinned executably in the runtime write-gate suite: each erased LIVE event leaves one freshly-minted extent-closing retraction event (a body clone whose closed assert no longer exists — the receipt the durable-replay journal needs, so a reopened store drops the re-added assert instead of resurrecting it), and the durable journal itself retains the erased events’ history closed rather than expunged (replay re-adds, then drops). Neither artifact is served by a read or consulted by a freeze witness.

Everything the substrate holds is bitemporal except what forget has touched, and this is the erasure contract on two layers. At the query surface forget destroys its target’s bitemporality: the axiom events and their bitemporal history are expunged from the served store, so an as_of reconstruction over the erased identity returns nothing. This is the point of the channel, not a shortfall — right-to-erasure obligations require that historical reconstructions cease to answer, which a bitemporal retraction cannot satisfy: RetractIndividuals records an ordinary closing event in the bitemporal log, so after retract x an as_of query still reconstructs x’s pre-cessation belief state in full. The two verbs share the same coverage gate and differ exactly here — logical cessation preserves the reconstructable trail, physical erasure removes it. At the storage substrate the durable-replay journal retains the erased bytes closed alongside the tombstone as an append-only-durability necessity, not as queryable history: no query or freeze-witness path reaches them, and replay consults the tombstone to re-erase so recovery is deterministic. A regime demanding physical destruction of even those closed bytes is a storage-lifecycle / compaction concern outside language semantics.

One bounded residue follows and is deliberately deferred to the follow-on lifecycle-surface / richer- forget proposal rather than approximated unsoundly: a fiber initialized only through the derived plane keeps no asserted witness in its own relation’s subsumption closure once its premises are cascade-retracted, so re-classifying the retracted identity and re-asserting a premise re-derives the immutable binding around a different value without refusal. An exact gate needs historical rule re-evaluation (or an identity-retirement rule for logically-retracted individuals, itself a lifecycle-surface decision). The residue is pinned by an executable ledger test in the runtime write-gate suite (oxc-runtime’s relation-mutability laundering tests) so the boundary cannot silently move in either direction. The runtime pin splices the kernel operation directly; a corpus twin using the retract x; / retract {x, y}; source spelling follows as the lifecycle surface matures.

Relatedly, the resurrection gate’s relation-tuple-endpoint arm (an individual retracted this transaction that a surviving tuple still names at an endpoint) has no end-to-end corpus twin: the endpoint-existence floor (OE0232) refuses a tuple over a non-existent endpoint before the net-view gate could ever observe one, so the shape is unreachable except by invoking the gate directly. The arm is therefore pinned by a direct-invocation runtime test as a net-view backstop rather than a source-level scenario, alongside the laundering residue above.

Transaction-time correction is a separate channel

Ordinary delete R(args) always follows the lifecycle gates above; it carries no correction exemption. A mis-recorded immutable assertion may be superseded only through a distinct, privileged transaction-time correction channel. Immutable-fiber initialization and retraction gates read the corrected transaction-time view, so an assertion superseded through that channel does not freeze an erroneous value; ordinary source deletion cannot masquerade as correction. That channel is the amendment operation specified in section 5 below.

4. Reflection — expose the effective is_mut bit

Expose a total, catalog-sorted atom for each declared relation end:

armMutability(relation: TypeRef, index: Nat, is_mut: Bool)

Every end contributes one row. An unmarked end contributes false; a mut end contributes true only when every transitive superrelation also permits mutation at that position. This shares the reflection-plane extension proposed in RFD 0075 (metarel cardinality reflection — the sibling relation-end reflection record, in review concurrently), since both are per-end declaration facts. The bit authorizes value variation through tuple retract/assert history; it does not advertise an endpoint-update operation.

With the immutable default, ArgUFO audits forbidden opt-outs rather than requiring explicit immutable annotations:

#[static]
pub check MutableCharacterizationBearer(relation: TypeRef) :-
    meta(relation) == characterization,
    armMutability(relation, 1, true)
    => Diagnostic {
        severity: Severity::Error,
        code: "ArgUFO::E_MutableCharacterizationBearer",
        message: "The bearer end of a characterization must not be declared mut.",
    };

The storage and wire representation should likewise carry a per-end is_mut boolean, parallel to the existing field mutability flag.

5. Amendment — correcting the record at belief time

Immutability protects two different things that the write path had conflated: the world cannot rebind an immutable end, and the record of what was asserted cannot be silently rewritten. The lifecycle gates above enforce the first. But a binding may be mis-recorded — asserted in error, false when it was made — and the modeler must be able to correct the record without pretending the world changed.

The two exits are distinct:

• World-exit is a cascade. The binding was true and has ended because a participant ceased; RetractIndividuals retracts the dependent context and the incident tuples fall away. History retains the binding (it was true once), so the freeze witness keeps the fiber initialized and the vacated value can never be reused.
• Record-exit is an amendment. The binding was never true; the assertion was false ab initio. Withdrawing it releases the freeze contribution it should never have made, so the corrected value is admitted where the frozen fiber would otherwise refuse it. Bitemporal history retains what-was-believed-when — the correction is auditable, not an erasure.

Concretely, with bornTo(mut child, mother) (the mother end immutable) and a child B first recorded as born to A, later known to be born to C:

pub mutate correct_birth_mother(child: Person, wrong: Person, right: Person) {
    // The record was wrong from the start: B was never born to A.
    amend bornTo(child, wrong) => bornTo(child, right);
}

Today this is impossible: delete bornTo(B, A) refuses (OE1402, immutable end), insert bornTo(B, C) refuses (OE1403, the mother fiber froze at {A}), and the only escape — RetractIndividuals{B} and full re-entry — cascades away every binding B participates in. Amendment is the missing narrow tool.

Syntax — one verb, two forms

Amendment adds a single reserved keyword, amend, with a primitive form and an ergonomic composite:

amend-stmt ::= 'amend' predicate-call ';'                          // withdrawal (truth unknown)
            |  'amend' predicate-call '=>' predicate-call ';'      // atomic withdraw + correct

• amend R(args); — the primitive. Withdraw the assertion as false ab initio when the true value is not (yet) known. It withdraws positive evidence: the proposition returns to unknown, not refuted.
• amend R(args) => R(args'); — the composite. Withdraw and assert the corrected proposition as one atomic operation validated against a single transaction-time view. The => makes the atomic old-becomes-new intent syntactically evident. It is exactly the primitive followed by a corrected insert, fused so the two cannot separate.

amend is deliberately a distinct verb from delete: delete is the valid-time ender (the binding stops being true now), amend is the belief-time corrector (the binding was never true). Conflating them — the whole hazard this section closes — must not be possible at the surface.

Alternatives considered

The primitive-plus-composite split was first drafted as two keywords (rescind + amend). It was reduced to one: withdrawal and replacement differ only by an optional replacement clause, share one authority, one history treatment, and one atomic validation, and there is no distinct substrate operation behind rescind — the old and new tuples are already distinct propositions, so the composite is a fusion of the primitive and a corrected assert, not a second concept. Reserving a second common domain word (rescind) for no semantic gain was not justified against the language’s posture of returning vocabulary to modelers wherever a keyword is not required. #[correction] delete was rejected outright: it spells correction as a flavour of delete, defeating the un-confusability that motivates the whole channel.

Semantics

Belief-time, corrected-view projection. An amended tuple is marked false ab initio and retained bitemporally — the audit history is never rewritten. The freeze and dependent-context gates read a corrected transaction-time view: the retained assert-polarity history minus the tuples this transaction amends. Amendment is thus the exact inverse of the cascade — where RetractIndividuals grows the freeze witness (a logical retraction retains history, so a vacated value can never be reused), amendment subtracts the amended assertion from the witness the gates read, so the corrected value is admitted. An amendment is a first-class withdrawal event keyed by the superseded assertion’s event identity and plane, not a rewrite of the retained log; the corrected view is a projection over event history, so a tuple still supported by another source, assertion event, or closure route is never silently subtracted. The subtraction is event-keyed, not value-keyed-for-all-time: a withdrawal releases only the assertion events it named (those recorded before it), so a later re-assertion of the same tuple is a fresh initialization that re-freezes the fiber. Concretely amend R(a); insert R(a); re-establishes the freeze, so a subsequent insert R(a') refuses exactly as with no amendment; only amend R(a); insert R(a'); directly (no intervening re-assertion) admits the replacement. A value-keyed marker that subtracted the re-assertion too would launder a rebind — two live values at an immutable end through a stale marker.

Initializer vs non-initializer. Amending the sole initializer of an immutable fiber leaves it uninitialized in the corrected view; the corrected assertion then initializes it afresh. Amending one of several tuples in a fiber whose declared minimum exceeds one (e.g. one of the two spouse tuples a bindsSpouse(...)[2] requires) leaves the fiber initialized — the surviving tuples still witness it — and re-checks the minimum against the surviving corrected set. A withdrawal that would leave an established immutable fiber non-empty but below its declared minimum refuses with OE1407 (AmendmentBelowMinimum). This is deliberately distinct from OE1398: that code refuses a first-transaction under-filled initialization; OE1407 refuses an under-filling correction of an already-established fiber — a different cause and a different point in the fiber’s life.

Atomicity. The composite validates the withdrawal and the corrected assertion against a single pre-state and commits all-or-nothing: if the corrected assertion is inadmissible, the whole amend … => … commits nothing.

One net-view coverage check. The amended tuple is excluded from the corrected view only for the gates, and coverage is validated once over the whole transaction’s net corrected view — withdrawals subtracted, corrected assertions and any lifecycle effects overlaid — never as a per-effect exemption. A composite followed by a cascade (amend R(a,b) => R(a,c); then a retraction touching a) therefore cannot launder anything: the corrected R(a,c) is live in the net view the coverage gate reads, and every unrelated incident binding remains visible to it.

All-mut relations. Amending a tuple of an all-mut relation is admitted, not linted. The freeze-release is vacuous there (nothing is frozen), but the bitemporal marking still differs meaningfully from delete: amend records “never believed”, delete records “true until now”. Choosing between them is a modeling decision, so the surface admits both.

Rule-derived tuples cannot be amended. You amend premises, not conclusions. amend R(args) naming a tuple that is live but has no directly-asserted (or refuted) event — a purely rule-derived conclusion — refuses with OE1406 (AmendmentTargetNotAsserted) rather than succeeding as a silent no-op; the modeler must amend the premises and let dependency maintenance recompute the consequence. A tuple with neither an event nor a live row is the idempotent no-op, exactly as an unmatched delete is. Where an asserted tuple is also independently derivable, amendment withdraws the asserted contribution and the tuple remains live by derivation until its premises are corrected — correcting the record is not the same as deleting the consequence.

Refutations. Amending a standing refutation (not_fact) is the symmetric case — withdrawing a mistaken refutation. The mutate surface has no refutation-mutation form today, and the retract-time status of a refutation is an open question in the negative-facts design (a withdrawn refutation leans toward unknown). Amendment of refutations is therefore deferred to that surface; this section specifies amendment over positive relation assertions.

New diagnostics. OE1405 (AmendWithoutCapability), OE1406 (AmendmentTargetNotAsserted), OE1407 (AmendmentBelowMinimum), OE1409 (AmendCorrectionRelationMismatch — a composite corrects a fact of one relation, so its withdrawal and correction must name the same relation), allocated by the amendment slice; reserved here as design-record forward references.

Abuse guard — amendment is capability-gated

Left free, amendment is a rebind-laundering channel: any code path could “correct” an immutable binding to a different value and call it a fix. The guard has the same posture as physical erasure (forget) — a capability the module grants explicitly, so ordinary code cannot quietly correct facts — while being a strictly weaker act (amendment retains a full bitemporal audit trail; erasure destroys history):

• Source gate. A mutate body containing amend refuses to build (OE1405 AmendWithoutCapability) unless the enclosing mutate declaration grants #[allow_amend], exactly as forget requires #[allow_forget]. The capability is greppable and visible at the declaration site.
• Serving-layer authorization. Correction authority is operational, so the serving layer authorizes an amendment against the invoking principal, and the authorization is target-scoped (a deployment may permit correcting birth records while forbidding correction of identity or security relations). This is a stronger posture than a blanket build-time bit precisely because amendment changes which transaction-time assertion is authoritative.
• Audit trail. Every amendment produces immutable bitemporal provenance — the false-ab-initio withdrawal event is retained, not erased — so the capability is auditable by construction.

A further per-relation restriction (forbidding amendment of named relations) needs no new mechanism: it is expressible as a static check over the schema, the same audit plane ArgUFO already uses to forbid mut opt-outs.

Independent design review: positions and resolutions

The syntax and semantics above were pressure-tested in a structured adversarial design review against the reference manual and the mechanized semantics. The positions that survived verification were adopted; those grounded in a misreading were rebutted. The substantive exchange:

Worked examples

Syntax note: the mut end modifier is carried by this design record; parser and check support land with the check-plane slice, so these examples are illustrative here and gate-verified once that slice is in.

The declaration — what changed

use std::core::{type, rel};
pub type Person;
pub type Organization;
pub type Marriage;

// Both ends vary over time → both opt in. This relation behaves exactly
// as every relation did before this design.
pub rel worksFor(mut employee: Person, mut employer: Organization) [0..*] [0..1];

// A marriage cannot swap spouses (`spouse` keeps the immutable default),
// but a surviving person may marry again later (`marriage` is mut from the
// person's side of the story).
pub rel bindsSpouse(mut marriage: Marriage, spouse: Person) [0..1] [2];

Before this design every relation end was implicitly rewritable: nothing distinguished “this employment can change employer” from “this marriage cannot change spouses” — both edits were silently legal. Now the declaration states which it is, and the default is the safe one: immutable unless said otherwise. mut sits before the end name, exactly where concept fields already put it — no new modifier system.

An all-mut relation is the pre-design semantics

mutate changeJobs(p: Person, from: Organization, to: Organization) {
    delete worksFor(p, from);   // admitted — every end of worksFor is mut
    insert worksFor(p, to);     // admitted
}

An all-mut relation is the pre-design behaviour, proven not just promised: the mechanization’s runMutationChecked_unconstrained_eq says the gated runner is the old interpreter when everything is mut (see “The mechanization, in plain language”). Existing programs keep compiling and keep their meaning.

Modeling posture (two postures, not two kinds of fact). “Isn’t changing jobs really a different employment contract?” — yes, if the domain models the contract. bindsSpouse reifies the relator (the marriage is an entity whose relata are constitutive — immutable ends, lifecycle via retract-and-cascade); worksFor(mut, mut) deliberately does not reify — it tracks only the current association, a coarser view whose tuples are rebindable snapshots (history stays queryable bitemporally). A domain that cares about the employment itself declares EmploymentContract and gives its relation immutable ends, making “changing jobs” a retraction of one contract and the creation of another — the same shape as the marriage. What this design adds is that the schema now states which posture each relation takes; before, everything silently behaved like the coarse view.

Why not worksFor(employee, mut employer) — “the employer is a property of the person”? Because mut is read per fiber, not per individual: an immutable employee end would freeze each employer’s employee set at its first asserting transaction (the company could never hire again), and since a matched delete removes a value from every fiber it touches, direct retraction requires every end mut — so the person could never leave either (OE1402). The one-sided “property of the person” intuition is carried elsewhere in the declaration: the [0..1] bracket on the employer end says each person has at most one employer at a time, and a domain that truly treats employer as a subject-owned attribute should model it as a mut field on Person — whose one-sided update semantics is exactly what this feature’s mut posture is copied from. Single-end mut is for genuinely one-sided lifetimes like the marriage: “for a fixed marriage, the spouse set freezes” is true; “for a fixed person, the marriage set freezes” would forbid remarriage.

The freeze (OE1403)

// Transaction 1 — initializes marriage m1's spouse fiber. The exact [2]
// bracket means both tuples must arrive together (see OE1398 below).
insert bindsSpouse(m1, alice);
insert bindsSpouse(m1, bob);

// Later transaction:
insert bindsSpouse(m1, carol);   // refused OE1403 — m1's spouse set froze at initialization
insert bindsSpouse(m1, alice);   // admitted — re-asserting an active tuple is idempotent
insert bindsSpouse(m2, carol);   // admitted — a fresh marriage initializes its own fiber

For an immutable end, the first transaction that asserts a fiber (here: the spouses of m1) freezes its complete value set. Growing it later refuses; repeating it is harmless; a different dependent context (m2) is a new fiber with its own initialization. The gate reads the closed extent — initializing through a subrelation or a standpoint-scoped view freezes the same fiber, so there is no back route.

Direct retraction (OE1402)

mutate divorceWrong(m: Marriage, p: Person) {
    delete bindsSpouse(m, p);    // refused OE1402 — bindsSpouse has an immutable end
}

Deleting a tuple would shorten an immutable binding’s life while the marriage it depends on still exists — the “not shorter” half of the lifetime equation. A delete that matches nothing stays a no-op: the gate refuses real shortenings, not re-runs.

The legal exit — the cascade

// Source spelling `retract m1;` lowers to the kernel effect
// RetractIndividuals { m1 }:
retract m1;
// ⇒ retracts m1 AND cascades: bindsSpouse(m1, alice), bindsSpouse(m1, bob)
//   are retracted with it, atomically, in the same transaction. alice and
//   bob survive; their frozen bindings do not outlive m1.

An immutable binding dies exactly when the thing it is about dies — the “not longer” half of the equation. The cascade is ordinary logical retraction (history stays queryable; nothing is erased), and the mechanization proves the sweep is complete: after it, no surviving assertion or refutation names m1.

When the cascade refuses (OE1404)

// Suppose employsCelebrant(mut ceremony: Ceremony, celebrant: Person)
// and c1 is a ceremony with celebrant dave.
RetractIndividuals { dave }
// refused OE1404 — dave sits at the IMMUTABLE end. Retracting him would strand
//   c1's frozen celebrant binding: c1 (the dependent context) survives, so the
//   binding may not die. Retract { dave, c1 } together, or none.

The cascade only releases a frozen binding when its dependent context is in the retraction set. If the context survives, refusing is the only safe answer — and the gate fails closed on anything it cannot decide, including a retraction target buried inside a collection value (pinned by collection_embedded_target_refuses_retraction).

Declaration-time refusals — before any data exists

pub type Amount;                       // a value-sorted type
pub rel hasBudget(project: Project, amount: Amount) [0..1] [1];
//                                 ^^^^^^ refused OE0267 — an immutable end whose
// dependent context is value-sorted can NEVER be released: a value has no
// lifetime to retract, so the fact would be permanently unretractable.
// Fix: declare `mut amount`.

pub rel supervises(mut boss: Person, report: Person) [0..*] [0..1];
pub rel mentors <: supervises (boss: Person, mut report: Person) [0..*] [0..1];
//                                           ^^^ refused OE0268 — a child may TIGHTEN
// a parent's mut end by omitting mut, but may not loosen an immutable one.

insert bindsSpouse(m3, alice);   // refused OE1398 (alone in a transaction) — the
// exact [2] bracket + freeze-at-initialization means an under-filled
// initialization could never grow to completion. Assert both spouses together.

The declaration plane refuses the traps before they can exist: an immutable end must have a context whose retraction could someday release it (OE0267, the unretractable-fact trap); subsumption can only make ends stricter (OE0268); and a frozen minimum must be met at the moment of freezing (OE1398). Status of each in this staged record: OE0267 is allocated and enforced by the check-plane slice; OE0268’s weakening rule is stated normatively (section 1) but its enforcement lands with the check-plane slice; OE1398’s below-minimum-initialization refusal is described in prose only in this record — it is not yet allocated to the catalog nor enforced, and lands with the write slice.

Mechanization of the two declaration-plane gates (OE0267, OE0268) was deferred and tracked, not carved out — the standing allowance for code to run ahead of the Lean covers evaluation / runtime semantics, not a declaration-plane gate over the subsumption lattice, which is substrate the Lean is canonical for. That obligation is now discharged in spec/lean/Argon/Substrate/RelationEndMutability.lean, which mechanizes the effective-mutability fold and both gates:

• The conjunctive fold effMutAt (effective mut = the relation AND every transitive superrelation declare mut at the position — the runtime EndMutability vector’s per-position value), with effMutAt_le_declared (effective is a lower bound on the declared bit), effMutAt_antitone (adding a parent can only tighten, never loosen), and immutable_parent_forces_immutable (any immutable transitive parent forces the end immutable).
• OE0268 as oe0268Accepts, with accepted_declared_is_effective: in any accepted schema a child’s declared mut equals its effective mut at every position — a weakening declaration is refused, never folded into an effective loosening.
• OE0267 as oe0267Accepts, with oe0267_context_individual_bearing (an accepted immutable end has a nonempty, identity-bearing dependent context) and oe0267_unary_immutable_refused (the vacuous unary end is refused — the declaration-time catch of the runtime coverage rule’s vacuous-false arm, tupleContextCovered).

Issue #1786 tracked this obligation and is closed by it.

Choosing mut end by end — gallery and decision procedure

pub type Kid; pub type Toy; pub type Person; pub type Passport;

// Transferable ownership: a pure association, like worksFor. Giving a toy
// away = delete + insert, and delete needs every end mut.
pub rel ownedBy(mut toy: Toy, mut owner: Kid) [0..*] [0..1];

// Provenance: "this toy was made FOR this kid." The recipient is
// constitutive — remaking it for someone else is a different fact. The kid's
// side still grows (they receive more toys over time).
pub rel madeFor(mut toy: Toy, recipient: Kid) [0..*] [0..1];

// Birth: a child's birth-mother never changes (immutable), but a mother's
// set of children grows with each birth (mut).
pub rel bornTo(mut child: Person, mother: Person) [0..*] [1];

// Issuance: a passport is issued to exactly one person, forever; a person
// accumulates passports over a lifetime.
pub rel issuedTo(mut passport: Passport, holder: Person) [0..*] [1];

How to read these. mut is per fiber — fix the other end, ask whether that value set may change after its first assertion:

• bornTo: fix a child → their birth-mother set is one value, frozen forever (immutable). Fix a mother → her children set grows with each birth (mut). Same shape for madeFor and issuedTo — one end is constitutive of the tuple, the other end accumulates history.
• ownedBy: fix a toy → its owner changes when gifted (mut); fix a kid → their toy collection changes (mut). Rebinding requires delete, which needs every end mut — so any transferable association is all-mut by necessity.

What the gates then do for each. insert bornTo(tim, anna) after Tim already has a recorded mother → OE1403 (a second birth-mother is not new information, it contradicts frozen information). delete issuedTo(p42, alice) → OE1402 (an issuance cannot be unhappened while both survive). RetractIndividuals { p42 } (the passport is destroyed/expired out of the domain) → cascade releases the frozen binding; Alice survives. RetractIndividuals { alice } alone → OE1404 — her passports sit at the mut end, fine, but her children’s bornTo bindings hold frozen ends; retract the dependent contexts together or not at all.

Decision procedure, three questions per relation:

1. Will a tuple ever be deleted while both individuals still exist? → every end mut (it is an association; ownedBy, worksFor).
2. Otherwise: which ends are fixed the moment the tuple exists, and which side keeps accumulating? Constitutive end stays immutable, accumulating end gets mut (bornTo, madeFor, issuedTo, bindsSpouse).
3. Is the only honest exit the disappearance of a participant? → that is the cascade doing its job, and the declaration needs no mut on that end.

The mechanization, in plain language

The mechanization (spec/lean/Argon/Runtime/MutationSemantics.lean) states the feature as a gated runner layered on the existing mutation interpreter, then proves the properties a reviewer would otherwise take on faith.

Backward compatibility — the keystone.

• runMutationChecked_unconstrained_eq — with no immutability constraint declared (the theorem is stated over the empty per-end mutability decode — the pre-design reading, which admits exactly what an explicit all-mut vector admits), the gated runner is definitionally the old ungated interpreter. This is the proof that the feature is opt-in and introduces no second semantics.
• relationGatesAdmit_unconstrained — the same fact at the gate level: an all-mut program admits every effect.

The two write gates (refusals are theorems, not test cases).

• retract_matched_immutable_refuses — a delete R(args) matching a live tuple at a relation with any effectively-immutable end refuses (the “not shorter” half).
• retract_unmatched_is_noop — the idempotent arm: a delete matching nothing is a no-op even at an immutable relation.
• assert_frozen_fiber_refuses — an insert carrying a new value for an already-initialized endpoint fiber refuses. Freeze means frozen.
• runMutationChecked_refused_noop — atomicity by construction: a refused mutation commits nothing; there is no partially-applied state to reason about.

The cascade half (the sign-off question), with its safety envelope.

• applyRetractIndividuals_uncovered_refuses — the coverage gate fails closed: if any effectively-immutable end of any incident tuple is not explained by the retraction set, the whole operation refuses.
• retractIndividuals_classifications_clean / retractIndividuals_relations_clean — after a covered retraction, no surviving classification and no surviving tuple names a retracted individual.
• retractIndividuals_refuted_classifications_clean / retractIndividuals_refuted_relations_clean — the same cleanliness for negative beliefs: a standing refutation about a retracted individual does not survive either.
• refuted_only_binding_gates_value_side — a binding that exists only as a refutation still gates its value side exactly as an asserted one would.
• collection_embedded_target_refuses_retraction — a retraction target embedded inside a collection value refuses the whole retraction (Abort), never silently releases.
• retractIndividuals_preserves_fiberInitialized — the cascade cannot un-initialize a fiber: retraction is ordinary logical retraction, never erasure, so it cannot launder an illegal rebind of a frozen end.

The amendment suite (amend, section 5) is mechanized in the same file: it releases exactly the amended assertion’s freeze contribution (a corrected insert is admitted where OE1403 refused), preserves the audit history, preserves other fibers, re-checks the minimum on a non-initializer amendment, refuses a purely-derived target, keeps the composite atomic, and leaves all-mut programs unchanged.

The deliberate asymmetry, stated rather than implied. Coverage reads an argument as “about” a retracted individual only at top level (Value.ceases), while incidence detection looks arbitrarily deep (Value.referencesAny). The consequence is fail-closed by design: a retraction target buried inside a collection value makes the evidence incomplete and the whole retraction refuse.

Staged ahead of use. The companion file spec/lean/Argon/Reasoning/Datalog/RelationApplication.lean carries two obligations for relation-value application: structural_containment (a declared child <: parent specialization edge entails extension containment in a structurally-closed program) and dispatch_selected_iff (reading the compiled finite-dispatch helper at an admitted selector is exactly applying the selected relation — the helper adds no semantic premise). Nothing in this record or the check/write-plane slices consumes them; they are obligations for the relation-value-application enforcement plane to discharge when it lands, and the module doc says so.

System shape and slice ownership

One feature, three planes, each owning exactly the rule its layer can decide. (No diagram-embedding markup is used in this spec tree; the shape is given as an ASCII figure.)

source: rel R(mut a: A, b: B)
        │
        ▼
┌──────────────────────────────────────────────────────────────┐
│ DECLARATION PLANE  — check-plane slice                         │
│   oxc-check::end_mutability                                    │
│   OE0267: an immutable end must have a dependent-context sort  │
└──────────────────────────────────────────────────────────────┘
        │ legal declarations only
        ▼
┌──────────────────────────────────────────────────────────────┐
│ WRITE PLANE  — write-gate slice                                │
│   oxc-runtime::end_mutability                                  │
│   decision table: insert on initialized immutable fiber        │
│     → OE1403 · matched delete → OE1402                         │
│   ┌────────────────────────────────────────────────────────┐  │
│   │ CASCADE SUB-UNIT (sign-off-pending)                     │  │
│   │   RetractIndividuals coverage → cascade, or OE1404       │  │
│   │   fail-closed                                           │  │
│   └────────────────────────────────────────────────────────┘  │
└──────────────────────────────────────────────────────────────┘
        ▲
        │ enforcing modules cite chapter + Lean def
        │ (chapter→module back-pointers land with the check/write
        │  slices, which own the enforcing code)
        │
┌──────────────────────────────────────────────────────────────┐
│ DESIGN RECORD  — this slice                                    │
│   spec/reference relations.md: ends immutable unless mut       │
│   spec/reference mutate.md:    write-plane refusals            │
│                                OE1402 / OE1403 / OE1404        │
│   spec/lean MutationSemantics: freeze / coverage / cascade,    │
│     mechanized, fail-closed on undecidable coverage           │
│   relations.md ↔ MutationSemantics: same rule, stated twice —  │
│     the mutation-semantics shapes are Lean-internal and        │
│     untagged, so their parity is the mechanization itself,     │
│     not a drift check                                          │
└──────────────────────────────────────────────────────────────┘

The book and Lean (this record) state the lifetime equation — an immutable binding lives exactly as long as its dependent context; the check plane refuses at declaration time what could never satisfy it (an immutable end whose sort admits no dependent context would make facts permanently unretractable); the write gate enforces it at runtime (no shortening while the context lives; the cascade — the one open sign-off — is the “no outliving” half). Nothing else moves: no parser change beyond one token position, no evaluator change, and the feature is opt-in per end, so every existing declaration keeps its meaning.

Maintainability rationale

Each rule lives in one module at the layer whose book chapter states it, and the links are machine-checked where a gate exists and stated honestly where one does not: the enforcing modules cite their chapters and Lean definitions (the chapter→module back-pointers land with the check/write slices, which own the enforcing code), the diagnostic codes in prose are gated against the catalog, and the drift gate covers tagged-inductive Lean↔Rust mirrors — the mutation-semantics shapes in this slice are Lean-internal and deliberately untagged, so their parity claim is the mechanization itself, not a drift check. Changing a rule is therefore a one-module edit plus its cited record — there is no second copy to forget. The one genuinely contested piece, the cascade, is isolated behind a module boundary whose header carries an honest removal inventory, so either exit-path outcome (cascade, or explicit per-binding retraction) is a bounded, enumerated change rather than an excavation.

Compatibility and migration

The grammar change is source-compatible: existing relation declarations still parse. The semantic default is intentionally stricter, however. Every existing unmarked end becomes lifetime-bound, so a model that currently varies a relation end while its dependent context survives must add mut before exactly that end.

Migration should audit delete R(args) and delete-plus-insert replacement patterns. Keep replacement as retract/insert and annotate only the ends allowed to vary. If an end is immutable, replace direct tuple deletion with retraction of its dependent context and rely on the automatic relation cascade. A plain tuple delete is not legal merely because it is terminal: it must satisfy every immutable-end lifetime gate. Most initial relation assertions and models that never retract tuples need no source change, with three declaration-level exceptions the stricter default itself introduces: a relation whose immutable end has a primordial, value-typed, or reference-sort dependent context is rejected (ImmutableRelationEndNonIndividualContext) even if it is only ever read — the modeler must mark the opposite end mut; a static fact set (or single-transaction initialization) that establishes an immutable fiber below its declared minimum cardinality is rejected rather than frozen permanently under-filled; and armMutability becomes a reserved reflection-atom name (ReservedIntrinsicName) — a previously valid declaration of that name must be renamed, because a same-module declaration would mask the total per-end reflection rows for every dynamic reader and let the very module under a forbidden-opt-out audit shadow the audit atom into an empty extent. This behavior change belongs in a breaking language release; there is no legacy mutable-by-default mode in the proposed design — no edition switch, build flag, or attribute restores the mutable default for source a post-RFD compiler builds.

Migration must also audit relation hierarchies. A child mut end beneath an immutable parent is a mutability-weakening error, and premise mutations that retract immutable derived facts must be converted to dependent-context retractions or rejected.

One further behavior change rides this proposal’s enforcement work, and migration should note it: gate 1’s “exact live tuple named by delete R(args)” is a BASE-plane lookup, aligning tuple deletion with the standpoint sheaf semantics (a fact asserted inside standpoint s { … } is s’s own local belief; the base write path edits the base plane). A DEFAULT-scope delete therefore no longer reaches into a standpoint to retract that plane’s seeded belief — previously it removed matching rows from every plane — and this holds for fully-mut relations too. A model that relied on a base delete clearing scoped beliefs must retract them within their standpoint. This is a plane-locality alignment, not a mutability gate: the per-end is_mut decode of pre-RFD artifacts (below) is unaffected.

At upgrade, each unmarked end’s currently live value set becomes its frozen initialization set. Historical data showing a removal or substitution while the same dependent context survived is a migration diagnostic rather than a value to normalize silently. The non-normalization half is enforced in the write path (a historically-removed value is never silently re-admitted); the REPORTING half — an offline audit listing such historical anomalies — is deliberately deferred to the breaking-release migration tooling (an ox doctor/ox migrate surface that does not exist yet) and is a follow-up gate for shipping that release, not a runtime behavior this proposal depends on.

Relation declarations gain a per-end is_mut flag, riding a MAJOR bump of the artifact core-IR version, so a published artifact adopts the stricter default only through a rebuild. The bump is major, not minor, because the additions are not safe for an older reader to ignore: under the version-robustness rule (a consumer accepts any artifact whose major does not exceed its own) a minor bump would let a pre-RFD runtime load a post-RFD artifact, skip the unknown per-end flags, and execute ordinary tuple mutations with every immutability gate silently absent — under-enforcing semantics the artifact’s source was audited against. With the major bump a pre-RFD runtime refuses the artifact loudly instead. In the other direction nothing is lost: a pre-bump artifact still loads on the post-RFD runtime (its lower major is accepted) and keeps its recorded pre-RFD semantics — every end reads as mut, exactly what its declaring compiler enforced (never all-immutable, which would impose gates its source was never audited against). That is faithful decode of an old artifact, not a mode of the new design: a post-RFD build cannot produce a mutable-by-default artifact, and the version stamp keeps pre-RFD artifacts distinguishable for any stricter deployment policy. The mutation IR/wire surface also gains RetractIndividuals. Relation-tuple events and their stored history remain unchanged: each is still identified by its relation and arguments, and logical individual retraction expands to ordinary retraction events. Existing history can seed the incidence index; no binding-id backfill or relation-tuple event migration is required.

References

• RFD 0006, Field mutability via mut — the modifier placement and immutable default followed by this proposal; relation mutation remains retract/assert rather than field update.
• The relation declaration chapter of the reference manual (spec/reference/src/declarations/constructs/relations.md) — the existing rel-param grammar this proposal extends.
• RFD 0075, Metarel cardinality reflection — the sibling reflection-plane extension (the relation-end notion and its per-end facet atoms), in review concurrently with this record.
• The ArgUFO vocabulary package (external to this repository): arg_ufo/metatypes.ar (the rigidity axis, the type-plane analogue of relation mutability), arg_ufo/relations.ar (InheresIn, Mediates, ExternallyDependsOn, HasComponent, HasMember, and their cardinality brackets), arg_ufo/metarels.ar (the existential-dependence and event-mereology metarels whose binding-stability axioms are prose today), and arg_ufo/metarel_constraints.ar (the existing relation-arm audits and the intended home of mutability checks).
• OE0234 — the fixed-metatype reclassification refusal, an analogous modal write gate.
• OE1341 — the cardinality gate that relation-end mutability complements.