feat(L10): mutable agent state — set <field> = <expr>

The runtime substrate for L10 rung-3b: agent handlers received a *copy* of
agent state with no write-back, so state was effectively immutable and there
was no assignment statement at all. The new `set <field> = <expr>` control
statement assigns to a declared `state` field and persists into the live
`AgentInstance.state`, so a later handler firing observes the new value.

- AST: additive `ControlStmt::SetState { field, value }` (existing untouched).
- Grammar: `grammar.pest` `set_stmt` rule + `set` keyword; `spec/grammar.ebnf`
  mirror — both grammar guards exit 0, `set_stmt` is in the shared rule set.
- Eval: write through to `AgentInstance.state` + `Env::update` so in-handler
  reads see the new value.
- Typecheck: the target must be a declared agent `state` (new
  `agent_state_fields`, mirroring rung-3b's `agent_residue_names` save/restore)
  and the value's type must unify with the field's declared type — new
  `TypeErrorKind::AssignToNonState` → `agent_api` `SET_NON_STATE`.
- Threaded the additive variant through codegen cranelift/elixir/native,
  dual_ast, formatter, metainterpreter, CFG, and the oracle checker.

Tests: 1 parser + 3 typechecker (declared-ok / non-state-error / type-mismatch)
+ 2 evaluator (within-agent `set count = 7` persistence; `set count = count + 1`
accumulating across three `receive` firings, observed as 3 by a separate
`report` handler) — 910 oo7-core lib tests pass, fmt + clippy clean. New
`examples/mutable_agent_state.007` (parse + typecheck + run; full e2e
PASS=55 FAIL=0). Spec: TYPE-SYSTEM-SPEC §11b.7; CHANGELOG; echo-residue-
integration.adoc substrate note.

Note: the pre-existing `oo7-typechecker-oracle` `production_and_oracle_agree`
differential test fails on clean `main` too (verified via git stash, 3/3 runs;
proptest is nondeterministic and can't find its persistence file) — it is a
production-vs-oracle divergence on a trivial total fn, not a regression here.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Roadmap (1)-(4) ALL DONE. Next substantive work = the L10 rung-3b RUNTIME half, which is blocked behind a prerequisite the user chose: BUILD MUTABLE AGENT STATE FIRST. Today an agent handler gets a COPY of state (run_agent_handler in eval.rs: env.set(name, val.clone())) with NO write-back, and there is no state-assignment statement — so a runtime residue cell has nowhere to persist across handlers. Step A: add a state-assignment statement (additive ControlStmt variant, e.g. `set <field> = <expr>` / `<field> := <expr>`) + evaluator write-back into AgentInstance.state; spec+grammar(pest<->ebnf)+tests in lockstep. Step B: explicit `residue <name>` agent-member cell (user's chosen design, refining the static half's implicit agent_residue_names presence-set) + runtime snapshot-on-`reversible as` / restore-on-`reverse` with Holding/Spent (Idris takeForReverse:Maybe is the model). This closes the once-only discipline the static half could only check by presence."
-last_action: "Roadmap item (4) CONSOLIDATE — swept AFFIRMATION.adoc, the status doc, and the next-Claude handover prompt to the verified merged state at 214a08f (branch claude/consolidate-l10-rung3b-proofsuite). #50 (rung-3b static) merged to main via admin-merge; all four recent feature branches (#49/#50/#51 + earlier) deleted on origin, no open PRs, no dangling branches. Renamed docs/status/must-intend-wish-2026-06-19.adoc -> -2026-06-20.adoc and updated both xrefs (AFFIRMATION + handover). Row sweeps: gap-fill intend -> done (imports+locales+choreographies+functions+types+agents); L10 rung-3b -> static done / runtime is the named follow-on (needs mutable state first); proof-suite labels reconciled to 35/37-verified, last 2 (M2 mathcomp + E1 Coquelicot) CI-canonical. CHANGELOG [Unreleased] already current — not touched. Prior this session: rung-3b static (#50, merged), #51 proof-suite refresh (merged), #49 fn/type/agent dup (merged), #48 docs, #47 awk fix, Rocq9 local, #46/#45."
-updated: 2026-06-20T00:18:53Z
+next_action: "L10 rung-3b RUNTIME — Step A (mutable agent state) DONE this session (branch claude/mutable-agent-state, PR pending). Remaining = Step B: the explicit `residue <name>` cell + runtime replay, layered on the new mutable-state substrate. Plan: (1) add a `residue <name>` agent-member (additive AgentMember/grammar/parser, declared cell — the user's chosen EXPLICIT STATE CELL design, refining rung-3b static's implicit agent_residue_names presence-set); (2) at runtime, snapshot the residue on `reversible as <name>` into the cell (Holding), and on `reverse <name>` restore/replay it and mark it Spent — modelling the Idris ResidueCell `takeForReverse : Maybe` (Spent => no-op/Nothing). This closes the cross-handler once-only discipline the static half could only check by presence. The mutable-state write-back path (eval.rs SetState -> AgentInstance.state) is the substrate to reuse for the cell's persistence."
+last_action: "L10 rung-3b runtime Step A — MUTABLE AGENT STATE (branch claude/mutable-agent-state off main fda2604). Added `set <field> = <expr>`: additive ControlStmt::SetState{field,value}; grammar.pest set_stmt + `set` keyword + spec/grammar.ebnf mirror (both grammar guards green, set_stmt shared); parser build_set_stmt; eval writes through to AgentInstance.state (was a non-writeable copy) + Env::update for in-handler reads; typechecker validates target is a declared `state` (new agent_state_fields set mirroring agent_residue_names) and value type matches (new TypeErrorKind::AssignToNonState -> agent_api SET_NON_STATE w/ declare_state/use_let remediations); threaded codegen cranelift/elixir/native + dual_ast + formatter + metainterpreter + CFG + oracle check.rs. Tests: 1 parser + 3 typechecker (declared-ok / non-state-error / type-mismatch) + 2 evaluator (within-agent persistence; cross-handler accumulation observed by a separate handler) — 910 oo7-core lib tests pass, fmt+clippy clean. New example examples/mutable_agent_state.007 (parse+typecheck+run pass; full e2e PASS=55 FAIL=0). Docs: TYPE-SYSTEM-SPEC §11b.7, CHANGELOG, echo-residue-integration.adoc substrate note. NOTE: oo7-typechecker-oracle differential `production_and_oracle_agree` fails — verified PRE-EXISTING (fails identically on clean main, 3/3 runs; proptest nondeterministic, can't find persistence file), NOT a regression. Prior: consolidate (#52 merged fda2604), rung-3b static (#50), #51/#49/#48/#47/#46/#45."
+updated: 2026-06-20T01:30:00Z
 
 @blockers:
 - id: proof-debt

.machine_readable/session-log.txt

@@ -48,3 +48,5 @@
 [2026-06-19 23:49:09] Roadmap item 2 — L10 RUNG 3b STATIC HALF (branch claude/l10-rung3b-static off pre-#49 main). Design (chosen autonomously per user "just drive"): IMPLICIT per-agent scope, static-half-first. check_agent_decl now collects agent_residue_names (all handlers reversible-as bindings, recursive collector mirroring collect_linear_lets) BEFORE the handler loop; the per-handler named_residues isolation stays (intra-body 3a linear discipline). take_named_residue changed Result<(),String> -> 3-way enum ResidueTake{Took,AlreadySpent,NotPresent}; ReverseNamed arm: Took=ok(3a consume), AlreadySpent=in-body double-reverse error, NotPresent=ok IFF agent_residue_names.contains(target) [cross-handler presence, rung 3b] else reverse-without-residue. Key correctness: AlreadySpent (in-body double) NOT masked by agent-presence; cross-FUNCTION still rejected (functions dont populate the set); cross-handler once-only deferred to RUNTIME (firing order unknown, takeForReverse:Maybe). Verified via CLI: r1 cross-handler OK, r2 undeclared->error, r3 in-body-double->error. 3 typechecker tests + examples/cross_handler_reversibility.007 (parse+check+RUN all pass). 900 oo7-core lib pass; fmt+clippy clean. Docs lockstep: spec TYPE-SYSTEM-SPEC new 11b.6, docs/echo-residue-integration.adoc (rung-3b static landed / runtime-half still open), CHANGELOG. REMAINING: 3b runtime half (evaluator replay); roadmap (3) full suite green [write M5 agda], (4) consolidate. Pushing -> draft PR.
 
 [2026-06-20 00:18:53] Roadmap item 4 — CONSOLIDATE (branch claude/consolidate-l10-rung3b-proofsuite off main 214a08f). #50 (L10 rung-3b static half) merged to main via admin-merge (sha 214a08f); webhook confirmed merged + auto-unsubscribed. State verified: no open PRs, all recent feature branches (#46/#48/#49/#50/#51 + earlier) deleted on origin, no dangling work. Swept the three governance docs to the verified merged state: (1) AFFIRMATION.adoc re-affirmed at 214a08f / 2026-06-20 — L10 now "done (static)" incl. rung-3b cross-handler-by-presence, the "I do NOT affirm" list reduced to the single runtime follow-on (mutable state) + the 2 CI-only proofs; (2) docs/status/must-intend-wish-2026-06-19.adoc renamed -> -2026-06-20.adoc (both xrefs updated), gap-fill intend -> done (imports+locales+choreographies+functions+types+agents), rung-3b row -> static done/runtime follow-on, proof-suite reconciled to 35/37-verified; (3) docs/handover/NEXT-CLAUDE-PROMPT.md regenerated at 214a08f — open-work list now leads with "build mutable agent state" (the user-chosen prerequisite) then the explicit `residue <name>` cell runtime half, fixed last-3->last-2 proof count, added the static->explicit-cell "evolution not reopen" note. CHANGELOG [Unreleased] already current (rung-3b static, fn/type/agent dup, just gate, proof gating all present) — not touched. STATE.a2ml next_action set to the mutable-state build (Step A: state-assignment ControlStmt + eval write-back into AgentInstance.state; Step B: explicit residue cell + snapshot/restore Holding/Spent). Docs-only consolidation; no code/proof changes, so no build delta to verify.
+
+[2026-06-20 01:30:00] L10 rung-3b RUNTIME, Step A — MUTABLE AGENT STATE (branch claude/mutable-agent-state off main fda2604). Implements the user-chosen "build mutable state first" prerequisite for the rung-3b runtime. Added the `set <field> = <expr>` control statement: additive ControlStmt::SetState{field,value}; grammar.pest set_stmt rule + `set` keyword + spec/grammar.ebnf mirror (both grammar guards exit 0, set_stmt in the shared rule set); parser build_set_stmt; eval.rs writes the value through to the live AgentInstance.state map (handlers previously got a non-writeable copy) AND Env::update so in-handler reads see it; typechecker validates the target is a declared agent `state` via a new agent_state_fields set (mirrors rung-3b's agent_residue_names save/restore in check_agent_decl) and unifies the value type against the field's declared type — new TypeErrorKind::AssignToNonState surfaced to agents as SET_NON_STATE (declare_state/use_let remediations). Threaded the additive variant through all compiler-enumerated match sites: codegen cranelift (agent-runtime no-op group) / elixir (rebind shadow) / native (zig assignment) + dual_ast (Let-node lowering) + formatter (`set f = e`) + metainterpreter (meta_record) + semantic CFG (Assignment node) + oracle check.rs (parity::skip "set-state"). Tests: parser set_state_parses; typechecker l10_set_declared_state_ok / l10_set_non_state_is_error / l10_set_state_type_mismatch_is_error; evaluator set_state_mutates_agent_state (set count=7 persists into agent.state) + set_state_persists_across_handlers (set count=count+1 fired 3x, observed as 3 by a SEPARATE report handler) — 910 oo7-core lib tests pass (was 901-ish), fmt clean, clippy clean. New example examples/mutable_agent_state.007 (parse+typecheck+run all pass; full e2e suite PASS=55 FAIL=0 SKIP=17). Docs in lockstep: TYPE-SYSTEM-SPEC §11b.7 (mutable agent state), CHANGELOG [Unreleased] entry, docs/echo-residue-integration.adoc "substrate landed" note pointing at Step B. PRE-EXISTING FAILURE NOTED: oo7-typechecker-oracle differential test `production_and_oracle_agree` fails — verified via git stash that it fails identically on clean main (3/3 runs); proptest is nondeterministic (FileFailurePersistence can't find lib.rs/main.rs) and the divergence is production=Reject/oracle=Accept on a trivial total fn, unrelated to this change. Step B (explicit `residue <name>` cell + runtime snapshot/restore Holding/Spent replay) is the remaining rung-3b runtime work, layered on this substrate.

CHANGELOG.md

@@ -10,6 +10,7 @@ All notable changes to this project will be documented in this file.
 - **Layer 10 phase 2 — the residue is a linear undo-capability.** The checker's residue stack now carries `Linear<Echo<T>>` (was a bare `Echo<T>`), making the consumed-once discipline explicit in the type. Discipline: *affine capability, linear consumption* — a given reversal log is consumed at most once (a double `reverse` of one residue is rejected) yet a `reversible` block need not be paired with a `reverse` (an un-reversed residue is **not** an error; reversibility is a capability, usually unused). Mechanised in `proofs/idris2/EchoResidueLinear.idr` (`reverseLinear` consumes `(1 e : Echo f y)`; `ResidueCell` Holding/Spent = the residue as agent state; `holdingReverses`/`spentDoesNotReverse`; `%default total`, zero `believe_me`, `idris2 --check` clean). 3 new typechecker tests (883 `oo7-core` lib tests passing). Remaining rung: cross-handler *named* residues (residue-binding grammar syntax, Harvard-guarded — kept separate). Spec/docs updated in lockstep.
 - **Layer 10 phase 3 (rung 3a) — named residues within a body.** New surface syntax `reversible as <name> { … }` binds the echo residue to a name; `reverse <name>` replays it (anonymous `reversible {…}`/`reverse {…}` unchanged). The named residue is tracked per body as a `Holding(Linear<Echo<T>>)` cell that `reverse` transitions to `Spent` — the static mirror of `ResidueCell` (Holding/Spent) in `EchoResidueLinear.idr`. Same affine/linear discipline: double `reverse <name>` is rejected (cell already `Spent`); a never-replayed binding is **not** an error; named residues are scoped per body (no cross-body leak). Additive AST variants `ReversibleAs`/`ReverseNamed` (existing variants untouched); grammar (`grammar.pest` + `spec/grammar.ebnf`), parser, typechecker (`named_residues` map + per-function/handler isolation), and the eval/codegen/formatter/dual-ast/metainterpreter/CFG/oracle pipeline all threaded. 2 parser + 5 typechecker tests (890 `oo7-core` lib tests passing; fmt clean, clippy `-D warnings` exit 0). Remaining rung 3b: cross-handler residues through agent state (irreducibly partly runtime — `takeForReverse : Maybe`). Spec: TYPE-SYSTEM-SPEC §11b.5; docs `docs/echo-residue-integration.adoc`.
 - **Layer 10 rung 3b (static half) — cross-handler named residues.** A `reversible as <name>` in one handler is now reversible by `reverse <name>` in *another* handler of the same agent — the residue is carried through agent state. The per-handler isolation that previously severed this is lifted to a per-agent `agent_residue_names` set collected up front; a cross-handler `reverse <name>` type-checks by **presence** (some handler declares it). The discipline is honestly split: within one handler the rung-3a *linear* discipline still holds (in-body double-`reverse` rejected), but cross-handler *once-only* is a **runtime** property — handler firing order is not statically known (`takeForReverse : Maybe`), so it is deferred to the runtime half. `take_named_residue` now returns a 3-way `ResidueTake` (`Took`/`AlreadySpent`/`NotPresent`) so the in-body double-reverse (`AlreadySpent`) is not masked by agent-level presence. Cross-*function* carry stays rejected (functions don't share state). 3 new typechecker tests + new `examples/cross_handler_reversibility.007` (parse + typecheck + run all pass). The runtime replay (evaluator executing the reversal log) is the remaining follow-on.
+- **Mutable agent state — `set <field> = <expr>`.** The runtime substrate the rung-3b residue cell needs: agent handlers previously received a *copy* of agent state with no write-back, so state was effectively immutable and there was no assignment statement at all. The new `set <field> = <expr>` control statement assigns to a declared `state` field and **persists** the value into the live `AgentInstance.state`, so a later handler firing observes it (proven by two evaluator tests: within-agent `set count = 7` persistence, and `set count = count + 1` accumulating across three `receive` firings observed by a *separate* `report` handler). Static discipline: the target must be a declared `state` of the enclosing agent — assigning a `let`/param/undeclared name is the new `SET_NON_STATE` error (`TypeErrorKind::AssignToNonState`, surfaced to agents with `declare_state`/`use_let` remediations) — and the value's type must match the field's declared type (else an L1 `TypeMismatch`). Additive AST variant `SetState { field, value }` (existing variants untouched); grammar (`grammar.pest` + `spec/grammar.ebnf` `set_stmt`, new `set` keyword), parser, eval (write into `AgentInstance.state` + `Env::update` for in-handler reads), typechecker (`agent_state_fields` set, mirroring rung-3b's `agent_residue_names`), and the codegen ×3 / dual-ast / formatter / metainterpreter / CFG / oracle pipeline all threaded. 1 parser + 3 typechecker + 2 evaluator tests (910 `oo7-core` lib tests passing; fmt + clippy clean) + new `examples/mutable_agent_state.007` (parse + typecheck + run all pass). Spec: TYPE-SYSTEM-SPEC §11b.7.
 - **Layer 10 proofs gated in the canonical proof suite.** The L10 echo-types proofs are now first-class suite entries (`audits/canonical-proof-suite/MANIFEST.a2ml`), gated nightly like the M/S/E classics: new `language` domain `L1` (`proofs/idris2/EchoResidue.idr`, headline `reverseAfterIrreversibleIllTyped`) and `L2` (`proofs/idris2/EchoResidueLinear.idr`, headline `reverseLinear`) — 37 entries total. Each gets the runner's banned-construct scan + `idris2 --check` + symbol-defined check; both verified locally (exit 0, zero banned constructs). The two files' "zero believe_me/assert_total/sorry" disclaimer comments were reworded so the substring banned-scan doesn't false-positive on the very tokens they disclaim. New end-to-end example `examples/named_reversibility.007` exercises `reversible as`/`reverse <name>` through the full pipeline (parse + typecheck + run all pass).
 - **`just gate` — one-command, billing-independent local green-check.** Runs every locally-faithful CI stage in sequence (rustfmt, clippy, `cargo test`, grammar-check, verify-harvard, e2e, `idris2 --check` of all 12 Idris proofs), continues past failures, and prints a per-stage PASS/FAIL/SKIP summary with a non-zero exit on any FAIL. Stages needing an absent toolchain (idris2) or an external GitHub action (A2ML/K9 validators, security scans) self-skip with a notice rather than failing, so it runs anywhere; the rocq canonical-proof-suite (needs Rocq 9) and external manifest/security scans stay CI/nightly-only. Verified GREEN on `main`. Distinct from `just ci` (build/test/lint/verify simulation) and `just check` (fast fmt/lint/test pre-commit).
 - **Import binding-collision detection.** The type checker now validates `import` declarations: every binding an import introduces — an `as` alias, each selective `from … import` item, or a bare `import a.b.c`'s last segment (`c`) — must be unique across the program. A collision (e.g. `import a as x` + `import b as x`, or `from m import abs, abs`) is now a `DuplicateImport` error instead of being silently accepted (imports were previously skipped by the gather pass entirely). Surfaced to agents via `agent_api` code `IMPORT_DUPLICATE_BINDING` (+`rename_import`/`remove_duplicate` remediations). Complements the existing `import_resolver` (which only detects *circular* imports). 4 new typechecker tests (894 `oo7-core` lib tests passing); `examples/imports.007` and the other import-bearing examples are unaffected.

crates/oo7-core/src/agent_api.rs

@@ -693,6 +693,31 @@ fn type_error_to_agent_error(te: &typechecker::TypeError) -> AgentError {
                 patch: None,
             }],
         },
+        TypeErrorKind::AssignToNonState { field } => AgentError {
+            code: "SET_NON_STATE".to_string(),
+            level: 1,
+            message: te.message.clone(),
+            location: None,
+            context: serde_json::json!({ "field": field }),
+            remediations: vec![
+                Remediation {
+                    strategy: "declare_state".to_string(),
+                    description: format!(
+                        "Declare `state {field}: T = ...` on the agent before assigning it"
+                    ),
+                    confidence: 0.7,
+                    patch: None,
+                },
+                Remediation {
+                    strategy: "use_let".to_string(),
+                    description: format!(
+                        "If `{field}` is a local, bind it with `let {field} = ...` instead of `set`"
+                    ),
+                    confidence: 0.5,
+                    patch: None,
+                },
+            ],
+        },
     }
 }
 

crates/oo7-core/src/ast.rs

@@ -359,6 +359,12 @@ pub enum ControlStmt {
     /// earlier `reversible as undo { ... }`. Consumes the residue: a second
     /// `reverse undo` is the L10 reverse-without-residue error.
     ReverseNamed { target: String },
+    /// `set <field> = <expr>` — assigns to a declared agent `state` field,
+    /// making agent state mutable. The assignment persists into the agent
+    /// instance's state map, so a later handler observes the new value
+    /// (the runtime substrate the L10 rung-3b residue cell builds on).
+    /// `field` must name a `state` declared on the enclosing agent.
+    SetState { field: String, value: ControlExpr },
     /// `enter discourse name { ... }` — execute within a discourse's interpretation rules.
     /// Branch strategy and evidence weights change within the block.
     EnterDiscourse {