RFD 0006 — Field mutability via mut

• State: discussion
• Opened: 2026-05-28
• Decides: surface syntax for opting a field into post-construction updatability; the implicit default for non-annotated fields; the interaction with #[intrinsic], from-clauses, refinement, and metatype rigidity; how update-stmt becomes the only legal write path; the lowering to append-only event pairs; the elaborator checks and diagnostic codes.

Question

Argon’s spec today has no field-level mutability discipline. Every non-derived field is implicitly mutable via the update-stmt grammar (§7.5:306). This contradicts the rest of the architecture — the substrate is value-semantic with no borrows (§7:26), .oxbin is content-addressed and immutable (§19), the event log is append-only (§20.1), and the Lean State.lean + Fixpoint.lean prove information-monotonicity. Should Argon admit a field-level mutability marker (mut), what’s the default, and how does it interact with the existing modifiers?

Context

Today’s effective semantics

• field-decl ::= attribute* Ident ':' TypeExpr ('=' expr)? ('from' relation-ref)? (§5.1:18). No mutability slot.
• update-stmt ::= 'update' (Ident | pattern) 'set' '{' field-assign (',' …)* '}' ('where' expr)? ';' (§7.5:306). Any field may appear in field-assign.
• Worked example (§7.5:334): update c: Company set { name = new } — name is implicitly updatable.
• #[intrinsic] is an attribute (not a keyword) declaring that a field must be set at kind level by every iof-instance (§5.1:135, §10.2:57). It governs construction-time required-ness, not post-construction mutability. A field can be both #[intrinsic] and (today) implicitly updatable.

What’s opt-out from mutability today

• Refinement-determined classification (§7.5:357) — the substrate derives membership; explicit insert iof rejected with OE0211 IofInsertOnRefinedType.
• Rigid metatype classification (§7.5:356) — kind / subkind / category individuals can’t be re-classified; insert iof / delete iof rejected with OE0210 IofInsertOnRigidType.
• from-derived fields (§5.1:18) — value comes from a relation projection; not directly assignable.
• Architectural — .oxbin, Module, Engine (§19); axiom_events only grows via append (§20).

The genuine gap

There is no language for “field that is set at construction (or by #[intrinsic] binding, or from-derived) and may not be subsequently updated.” Modelers write pub kind Person { name: String, dob: Date, current_address: Text } with no way to say “name and dob are set-once; only current_address changes.” Today’s update-stmt admits writes to any of them.

The Argon vault’s open-questions doc (Efforts/On/Argon/scratch/open-questions response.md #18) names this verbatim: “Mutability annotations. No grep hit for mut/const/#[mut] on properties. Likely absent. Tied to #19 (change patterns). Genuine gap.”

mut is available

Per appendix-a:6-18, mut is not in the reserved keyword list. The mutation-related reserved words are mutate, insert, delete, update, upsert, detach, forget. Adding mut is a non-conflicting lexer change.

Decision

Surface

mut is a field-declaration modifier. Without it, fields are set at construction (or via #[intrinsic] kind-level binding, or by from-clause derivation) and immutable thereafter. With it, a field admits writes via update-stmt inside mutate bodies.

pub kind Person {
    name: String,                   // set at construction; not updatable
    dob: Date,                      // set at construction; not updatable
    #[intrinsic] ssn: Text,         // must be set at kind binding; not updatable
    mut current_address: Text,      // updatable post-construction
    mut current_employer: Company?, // updatable, optional
    #[intrinsic] mut current_role: EmploymentRole,  // both: required at construction, updatable later
}

pub mutate move(p: Person, addr: Text) {
    update p set { current_address = addr };       // OK
    // update p set { name = "Bob" };              // OE0820: name is not `mut`
}

Updated grammar

field-decl ::= attribute* 'mut'? Ident ':' TypeExpr ('=' expr)? ('from' relation-ref)?

Order: attribute* mut? Ident. Attributes precede mut; mut precedes the identifier. This places mut adjacent to the field name where its scope is most visible.

Defaults

• A non-mut field is immutable post-construction.
• A mut field is mutable post-construction.
• A from-derived field is always derived (not directly assignable); mut on a from-derived field is rejected with OE0822 MutOnDerivedField.
• A field with #[intrinsic] is required at construction; orthogonal to mut.

Lowering

Field mutations lower to append-only event pairs on the underlying axiom. A mutate body with update p set { current_address = "new" } emits:

1. A retract event (Polarity::Retract) on the prior property_assertion row whose body is { entity_id = p, property_id = NameRef(current_address), value = "old" }. The retract event’s asserts_axiom points to the prior assert’s EventId.
2. A new assert event (Polarity::Assert) on the new property_assertion row whose body is { entity_id = p, property_id = NameRef(current_address), value = "new" }.

Both share the same content-addressed AxiomKey for the proposition “p has current_address X” — the proposition’s identity is the property assertion’s logical content; the value is what changes. Per RFD 0001, AxiomKey is BLAKE3-128(canonical_body), so old and new have distinct AxiomKeys but the same (entity_id, property_id) pair identifies them as alternative assertions of the same property.

Elaborator checks

• OE0820 UpdateImmutableField — update e set { f = expr } where f is not mut. Caller is the update-stmt elaborator.
• OE0821 MutOnRefinementDerivedField — reserved; not yet emitted (refinements are concept-level today, not field-level; this exists in case refinement gains field-level derivation later).
• OE0822 MutOnDerivedField — mut f: T from rel.range. The from-clause already determines the value; mut is contradictory.
• OE0823 MutOnRelationTupleField — reserved for Form B/C relation tuple bodies whose intrinsic fields may want their own mutability discipline; nail down when relation-tuple updates land.

Interaction with the four orthogonal axes

The four existing constraint axes plus mut form a clean matrix:

Same commit ships update-stmt

The update-stmt grammar (§7.5:306) is reserved but unimplemented in the parser/lowerer/runtime today. mut is a no-op without update. The implementation of this RFD ships:

1. Parser: update statement parsing (§7.5:306 + 307).
2. Lowerer: update lowers to a new Operation::Update core_ir variant which expands to retract+assert event pairs at runtime.
3. Elaborator: rejects update p set { non_mut_field = ... } with OE0820.
4. Runtime: execute_mutation’s operation interpreter handles Operation::Update.

Local let mut is OUT OF SCOPE for this RFD

The §7.5:293 'let' Ident (':' TypeExpr)? '=' expr ';' grammar has no rebind form. A let mut x = ...; x = ... local-rebind story is meaningful but deferred to a follow-up RFD when the mutate-body language grows expression-level computation needs. The current RFD only addresses field mutability on declarations.

Rationale

Why immutable by default

Three reasons:

1. Aligns the surface with the substrate. Argon is content-addressed, append-only, value-semantic. Implicit field mutability is the one surface-level dissonance with the rest of the architecture. Making mutability opt-in restores coherence.

2. Forces modelers to identify stable attributes. Real ontologies have a sharp distinction between identity-bearing attributes (birth date, SSN, kind classification) and contingent attributes (current address, status, balance). Today’s syntax doesn’t make this visible. mut-by-default would have been a research-friendly default but explicit-opt-in matches the Mercury / Rust / Haskell tradition: types tell you what’s mutable.

3. Pairs with the rest of Argon’s modeling discipline. #[intrinsic] says “must be set”; from says “is derived”; <: says “is subsumed by”; refinement says “is constrained by.” Adding mut says “may change post-construction” — slots into the same pattern. No mut ⇒ no post-construction change.

Why keyword over attribute (mut vs #[mut])

Three considerations:

• Visual prominence. Mutability affects how the field participates in mutations; it’s a first-class semantic property, not metadata. Keyword form (pub mut current_address: Text) signals this; attribute form (#[mut] current_address: Text) reads as decoration.

• Consistency with rest of the surface. pub, from, where, :, = are all keyword-shaped in field declarations. #[intrinsic] is an attribute because it’s a kind-level constraint (governs the binding site), not a value-level property. mut is value-level. Keyword fits.

• Frequency of use. Field declarations are common; mut will appear often. Keyword form is shorter (3 chars + space vs 8 chars + space).

Why ship update-stmt with mut

The update keyword is reserved but the parser doesn’t recognize it; the lowerer doesn’t emit Operation::Update. Without it, mut is a marker that nothing reads. Two reasons to ship together:

• Coherent surface. Modelers learn mut and update together as a unit. Documentation lands as one chapter, not two halves separated by a release.
• End-to-end testable. A pub_fact_keystone analog with pub mutate move(p: Person, a: Text) { update p set { current_address = a }; } followed by a query_derive proves the full path.

Why orthogonal mut × #[intrinsic]

The two govern different lifecycle points:

• #[intrinsic] — “must be specified by every iof-instance at kind binding”
• mut — “may be re-assigned post-construction by update-stmt”

A real ontology pattern: #[intrinsic] mut employment_role: Role — every employee has a role from day one, and the role can change as they’re promoted. Forcing them to choose between “intrinsic” and “mutable” is a false dichotomy.

Why no let mut in this RFD

The mutate-body statement language (§7.5:293-313) is currently minimal: let, match, insert/update/delete/upsert/detach/emit, for, if, expr;. Local rebinding is interesting but isolated — it doesn’t interact with the field-mutability story. Treating it separately lets the field-mutability discussion stay focused.

Alternatives considered

Alt 1: mut as documentation only (β from the design discussion)

Keep current “any field is implicitly updatable” semantics. Use mut as a documentation marker driving tooling (audit, indexes, change-notification).

Rejected: doesn’t close the gap the vault names. Adds noise without changing semantics. The whole virtue of mut is forcing modelers to identify which attributes change.

Alt 2: mut for non-field axes only (γ)

Skip field-level mutability; use mut for pub mut concept (concept-level opt-in to state change) or pub mut rel (relation-level opt-in to tuple update).

Rejected: pub mut concept is redundant with metatype-driven rigidity (role is already anti-rigid). pub mut rel is interesting (insert/delete vs update) but is a smaller question than field mutability and can be addressed via a future RFD once relation-tuple intrinsic-field semantics solidify.

Alt 3: Attribute form #[mut]

Use #[mut] instead of mut. Composes with the existing attribute machinery; parallel to #[intrinsic].

Rejected as primary surface. Considered seriously; the keyword form wins on visual prominence + consistency with pub / from (other field-decl keywords). Attribute form might be admitted as an alias if grep-friendly attribute scanning becomes valuable, but the canonical surface is the keyword.

Alt 4: Tri-state: mut / default / const

Add both mut (mutable) and const (set-at-construction-then-frozen) with default being “construction-time once, kind-level once, no other constraint.” (const is already reserved per appendix-a:8.)

Rejected: the three-state design is more expressive but adds modeler load. The current architectural decision is “default to immutable; opt-in to mutability via mut.” const stays reserved for compile-time-known-value semantics if/when that landing strip becomes necessary.

Alt 5: Per-field via update rule mode

Instead of marking the field, mark the mutate body: declare which fields the body may touch via a frame clause. Closer to TLA+ / Reiter SSA semantics.

Rejected: heavier syntax. Real-world ontology workflows have many small mutations touching one field each; per-mutate-body declaration would multiply boilerplate. Field-level marker is more direct.

Consequences

Wire format

property_assertion events already carry an EventId and the body. Adding mut doesn’t change the wire format — the runtime emits retract+assert event pairs as it would for any other mutation. The field-decl’s mut marker is part of the concept/struct/etc. declaration’s wire body and rides along.

core_ir

Operation enum (today: InsertIof, DeleteIof, InsertTuple, DeleteTuple, Forget) gains:

#![allow(unused)]
fn main() {
Operation::Update {
    entity: Term,
    assigns: Vec<FieldAssign>,
    where_clause: Option<Term>,
},
}

Plus the FieldAssign shape: { field_name: String, op: AssignOp, expr: Term } where AssignOp is Set | AddSet | SubSet (for =, +=, -=).

Parser

• New mut keyword recognized at the lexer level (added to grammar.toml’s keyword list).
• field-decl parser admits optional mut token between attributes and the ident.
• update-stmt parser implements §7.5:306 including where clause.

Elaborator

• lower_concept_decl / lower_struct_decl walk field declarations; carry mut flag through to wire body (ConceptDeclBody.fields[i].mut_flag or similar — TBD when the field body wire shape solidifies).
• lower_mutate_body recognizes update-stmt, produces Operation::Update.
• Elaborator checks (OE0820, OE0822) emitted during update-stmt lowering.

Runtime

execute_mutation’s operation interpreter gains a Operation::Update arm:

1. For each FieldAssign, evaluate the expr against the current state.
2. Look up the prior property assertion event for (entity, field_name).
3. Emit a retract event for the prior + assert event for the new.

Diagnostics

Three new codes in grammar.toml, propagating to oxc-diagnostics::generated.rs + appendix-c-diagnostic-codes.md:

• OE0820 UpdateImmutableField — update e set { f = expr } where f lacks mut.
• OE0821 MutOnRefinementDerivedField — reserved; not yet emitted.
• OE0822 MutOnDerivedField — mut f: T from rel.range is contradictory.

Spec migration

The spec’s worked examples need updating. Specifically:

• §7.5:334 update c: Company set { name = new } — either annotate name as mut or rename the example to use a field that’s plausibly mut.
• §21 walking example: review for any field updates and add mut annotations.

Lean

Argon/Syntax/Decl.lean (field-decl) gains a mut: Bool field. Argon/Storage/AxiomBody.lean doesn’t change (property assertions are already individual axiom events; the retract+assert lineage is already in Polarity + asserts_axiom). Argon/TypeSystem/FlowTyping.lean may need refinement of the immutability assumption to “non-mut fields stay immutable across mutation”; the proof obligation is small (per-field discipline rather than blanket immutability).

CI drift gate

field-decl’s Lean inductive carries mut: Bool; the matching Rust struct in oxc-protocol::storage::FieldDecl (or wherever fields are wire-typed) must include it. CI drift check covers this.

Open questions

• Should mut admit += / -= only on numeric types? §7.5:307 field-assign allows =, +=, -=. For text fields current_address += "..." is ambiguous (string concatenation? error?). Lean toward: += / -= admitted only when the field’s type implements the arithmetic ops (Nat, Int, Real, Money, Duration). Resolve when the trait system covers numeric op overloading.

• mut on collection fields: pub mut friends: List<Person> — does mut admit both update p set { friends = [...] } (replace) and insert p.friends(other) (push)? Probably both, but the semantics need pinning down when collection-field mutation lands.

• mut on relation tuple bodies (Form B/C): a relation declared with intrinsic property body (§5.2 Form C) carries its own fields. Do those fields admit mut? Almost certainly yes, with the same defaults — but the syntactic surface (pub rel hasJob(p: Person, c: Company) [1] [1..*] { mut salary: Money }) needs validation. Reserved as OE0823.

• Interaction with #[brave] / stable models (§7.8): mut writes happen at runtime; brave-derived facts at build time. The two don’t collide today but if a #[brave] rule references a mut field’s prior value, the rule’s stratification needs to account for the temporal axis. Defer to when brave rules see real use.

• Update via partial assignment: update p set { current_address = ..., current_employer = ... } — atomic both-or-neither, or sequential? Today’s transactional semantics of mutate bodies suggests atomic; the elaborator emits the retract+assert event pairs in a single mutation transaction. Confirm when the runtime’s transaction semantics formalize.

• Identity-preserving field mutation: when a mut field changes, the entity’s IndividualId stays the same (RFD 0001). The AxiomKey for the property changes (content-addressed). Confirm the MutationReceipt shape adequately captures the lineage for downstream consumers (provenance witnesses, audit logs).

• Should pub fact (RFD 0004) be able to set a mut field at construction? pub fact Person(alice) { current_address: "..." } — yes, presumably, since this is construction-time assignment, not post-construction update. The fact-decl grammar in RFD 0004 doesn’t yet have a body form for setting fields; add when needed.