feat(L10): rung-3b runtime — per-variable delta residue replay

CHANGELOG.md

@@ -12,6 +12,7 @@ All notable changes to this project will be documented in this file.
 - **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 rung 3b (runtime half) — echo-residue cells + runtime replay.** `reverse <name>` now has an operational meaning: restore the agent to the checkpoint captured by the matching `reversible as <name>`. New explicit `residue <name>` agent-member declaration (the chosen *explicit state cell* design) declares a residue cell; `AgentInstance` carries a `residues: HashMap<String, ResidueCell>` where `ResidueCell = Holding(state-snapshot) | Spent` (the evaluator shadow of the Idris `ResidueCell`). Evaluator semantics: `reversible as <name>` snapshots the agent state map *before* its body runs (`Holding`), so a later — possibly cross-handler — `reverse <name>` restores that snapshot and marks the cell `Spent`; a second `reverse <name>` finds `Spent`/absent and is a no-op (the runtime witness of `takeForReverse : … → Maybe` = `Nothing`). The cell lives on the instance, so it persists across handler firings, closing the cross-handler once-only that the static half (#50) could only check by presence. Built on the §11b.7 mutable-state substrate; *checkpoint* semantics (restore the whole state map, not a per-variable delta) is the honest scope. Additive `residue_decl` grammar (`grammar.pest` + `spec/grammar.ebnf`, new `residue` keyword) + `AgentDecl.residues` field; declared residues also feed the rung-3b static presence-set. Evaluator tests prove an actual cross-handler rollback (debit then `reverse undo` restores the balance) and the spent-is-no-op discipline. New `examples/transactional_rollback.007`. Spec: TYPE-SYSTEM-SPEC §11b.8.
+- **Layer 10 rung 3b runtime — residue replay is a per-variable delta, not a whole-state checkpoint.** Refines the runtime residue cell so `reverse <name>` restores *only* the state fields its `reversible as <name>` body mutated, leaving everything else — including unrelated `set`s made by *intervening* handlers — intact. `reversible as` now captures a **before-image delta** (the prior values of exactly the `set` fields, found by a static `collect_set_fields` scan that descends through nested control), and `reverse` writes just those back, rather than cloning/restoring the whole `AgentInstance.state` map. This fixes a real clobber: under the previous whole-checkpoint cut, a `reverse` would silently revert an unrelated field that a later handler had changed. Over-approximating the field set is harmless (a field `set` only on an untaken branch is captured at its current value, so write-back is a no-op). New evaluator test `residue_reverse_is_per_field_delta_not_whole_checkpoint` (debit arms `undo` on `balance`; a separate handler changes `note`; `reverse undo` restores `balance` but preserves `note`) — 914 `oo7-core` lib tests passing, fmt + clippy clean. Spec/example/design-note updated from "checkpoint" to "per-variable delta" wording in lockstep. Spec: TYPE-SYSTEM-SPEC §11b.8.
 - **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/eval.rs

@@ -23,7 +23,7 @@ use crate::ast::*;
 use crate::trace::{DecisionTrace, TraceRecord};
 use chrono::Utc;
 use serde_json::Value as JsonValue;
-use std::collections::{HashMap, VecDeque};
+use std::collections::{HashMap, HashSet, VecDeque};
 
 /// Safety limit for loops without break — prevents infinite loops
 /// in the reference evaluator. Production runtimes would use fuel/budgets.
@@ -553,13 +553,73 @@ impl BranchStrategy for ConsensusStrategy {
 /// handler firings (the cross-handler rung-3b path).
 #[derive(Debug, Clone)]
 pub enum ResidueCell {
-    /// A live reversal checkpoint: the agent state captured immediately before
-    /// the `reversible as <name>` body ran. `reverse <name>` restores it.
+    /// A live reversal *delta*: the before-image of exactly the state fields the
+    /// `reversible as <name>` body mutates, captured immediately before it ran.
+    /// `reverse <name>` writes each captured field back, leaving every other
+    /// field — including unrelated `set`s from intervening handlers — untouched.
     Holding(HashMap<String, RtValue>),
     /// The residue has already been replayed (consumed exactly once).
     Spent,
 }
 
+/// Collect the names of agent `state` fields that a control body assigns via
+/// `set <field> = …`, descending through every nested control construct. This
+/// is the static support of a `reversible as` body's before-image delta: the
+/// evaluator snapshots exactly these fields before the body runs. Over-approx
+/// is harmless — a field that is `set` only on an untaken branch is captured at
+/// its current value, so restoring it is a no-op. (Mirrors the recursion shape
+/// of the type checker's `collect_reversible_as_bindings`.)
+fn collect_set_fields(body: &[ControlStmt]) -> HashSet<String> {
+    fn go(stmt: &ControlStmt, out: &mut HashSet<String>) {
+        match stmt {
+            ControlStmt::SetState { field, .. } => {
+                out.insert(field.clone());
+            }
+            ControlStmt::Reversible(b)
+            | ControlStmt::Irreversible(b)
+            | ControlStmt::Reverse(b)
+            | ControlStmt::ReversibleAs { body: b, .. }
+            | ControlStmt::Loop { body: b, .. }
+            | ControlStmt::EnterDiscourse { body: b, .. } => {
+                for s in b {
+                    go(s, out);
+                }
+            }
+            ControlStmt::If {
+                then_body,
+                else_body,
+                ..
+            } => {
+                for s in then_body.iter().chain(else_body) {
+                    go(s, out);
+                }
+            }
+            ControlStmt::Branch { arms, .. } => {
+                for arm in arms {
+                    for s in &arm.body {
+                        go(s, out);
+                    }
+                }
+            }
+            ControlStmt::Match { arms, .. } => {
+                for (_pat, body) in arms {
+                    if let ControlExprOrBlock::Block(stmts, _) = body {
+                        for s in stmts {
+                            go(s, out);
+                        }
+                    }
+                }
+            }
+            _ => {}
+        }
+    }
+    let mut out = HashSet::new();
+    for s in body {
+        go(s, &mut out);
+    }
+    out
+}
+
 /// A live agent instance in the runtime. Each spawned agent gets one.
 ///
 /// Agents are cooperative (single-threaded): message delivery is
@@ -1958,18 +2018,26 @@ impl Evaluator {
                 r
             }
             ControlStmt::ReversibleAs { binding, body } => {
-                // L10 rung-3b runtime: snapshot the agent's state *before* the
-                // body runs, store it as a `Holding` residue cell keyed by
-                // `binding`, then run the body. A later `reverse <binding>`
-                // restores this checkpoint. The cell lives on the agent
-                // instance, so the snapshot survives into other handlers.
+                // L10 rung-3b runtime: capture a *before-image delta* of the
+                // fields this body mutates, store it as a `Holding` residue cell
+                // keyed by `binding`, then run the body. A later `reverse
+                // <binding>` restores exactly those fields. Snapshotting only the
+                // touched fields (not the whole state map) means a `reverse`
+                // leaves state that the body never wrote untouched — including
+                // unrelated `set`s made by intervening handlers. The cell lives
+                // on the agent instance, so the delta survives into other
+                // handlers.
+                let touched = collect_set_fields(body);
                 if let Some(agent_id) = self.current_agent_id.clone()
                     && let Some(agent) = self.agents.get_mut(&agent_id)
                 {
-                    let snapshot = agent.state.clone();
+                    let before_image: HashMap<String, RtValue> = touched
+                        .iter()
+                        .filter_map(|f| agent.state.get(f).map(|v| (f.clone(), v.clone())))
+                        .collect();
                     agent
                         .residues
-                        .insert(binding.clone(), ResidueCell::Holding(snapshot));
+                        .insert(binding.clone(), ResidueCell::Holding(before_image));
                 }
                 env.push_scope();
                 let r = self.eval_stmts(body, env);
@@ -1978,15 +2046,19 @@ impl Evaluator {
             }
             ControlStmt::ReverseNamed { target } => {
                 // L10 rung-3b runtime: replay the named residue. If its cell is
-                // `Holding`, restore the snapshotted agent state and mark the
-                // cell `Spent` (consumed once). If `Spent` or absent, this is a
-                // no-op — the runtime witness of `takeForReverse` = `Nothing`.
+                // `Holding`, restore each field in the before-image delta to its
+                // captured value and mark the cell `Spent` (consumed once). If
+                // `Spent` or absent, this is a no-op — the runtime witness of
+                // `takeForReverse` = `Nothing`. Only the recorded fields are
+                // written back; all other state is left as-is.
                 if let Some(agent_id) = self.current_agent_id.clone()
                     && let Some(agent) = self.agents.get_mut(&agent_id)
-                    && let Some(ResidueCell::Holding(snapshot)) = agent.residues.get(target)
+                    && let Some(ResidueCell::Holding(before_image)) = agent.residues.get(target)
                 {
-                    let snapshot = snapshot.clone();
-                    agent.state = snapshot;
+                    let before_image = before_image.clone();
+                    for (field, value) in before_image {
+                        agent.state.insert(field, value);
+                    }
                     agent.residues.insert(target.clone(), ResidueCell::Spent);
                 }
                 RtValue::Unit

crates/oo7-core/src/eval_tests.rs

@@ -1324,6 +1324,108 @@ mod tests {
         );
     }
 
+    #[test]
+    fn residue_reverse_is_per_field_delta_not_whole_checkpoint() {
+        // The residue captures a *before-image delta* of only the fields its
+        // body mutates, so `reverse` leaves unrelated state alone. Here `debit`
+        // arms `undo` touching only `balance`; a separate `annotate` handler
+        // then changes the unrelated field `note`; `reverse undo` restores
+        // `balance` but MUST preserve `note`. A whole-state checkpoint would
+        // have clobbered `note` back to its pre-debit value — this test pins
+        // the delta semantics that fixes that.
+        let mut evaluator = Evaluator::new();
+        let agent_decl = AgentDecl {
+            name: "Ledger".to_string(),
+            capabilities: vec![],
+            budget: None,
+            implements: vec![],
+            locale: None,
+            data_blocks: vec![],
+            handlers: vec![
+                // debit: arm `undo`, touching ONLY `balance`.
+                Handler {
+                    event: "debit".to_string(),
+                    params: vec![("amount".to_string(), "Int".to_string())],
+                    body: vec![ControlStmt::ReversibleAs {
+                        binding: "undo".to_string(),
+                        body: vec![ControlStmt::SetState {
+                            field: "balance".to_string(),
+                            value: ControlExpr::BinOp(
+                                Box::new(ControlExpr::Var("balance".to_string())),
+                                BinOp::Sub,
+                                Box::new(ControlExpr::Var("amount".to_string())),
+                            ),
+                        }],
+                    }],
+                },
+                // annotate: change the UNRELATED field `note`, no residue.
+                Handler {
+                    event: "annotate".to_string(),
+                    params: vec![("ignored".to_string(), "Int".to_string())],
+                    body: vec![ControlStmt::SetState {
+                        field: "note".to_string(),
+                        value: ControlExpr::DataLit(DataExpr::Int(7)),
+                    }],
+                },
+                // rollback: replay the `undo` delta.
+                Handler {
+                    event: "rollback".to_string(),
+                    params: vec![("ignored".to_string(), "Int".to_string())],
+                    body: vec![ControlStmt::ReverseNamed {
+                        target: "undo".to_string(),
+                    }],
+                },
+            ],
+            states: vec![
+                ("balance".to_string(), DataExpr::Int(100)),
+                ("note".to_string(), DataExpr::Int(0)),
+            ],
+            residues: vec!["undo".to_string()],
+        };
+        evaluator.register_agent_decl(agent_decl);
+
+        let mut env = Env::new();
+        evaluator.eval_stmt(
+            &ControlStmt::Spawn {
+                attested: false,
+                linear: false,
+                binding: "h".to_string(),
+                agent_name: "Ledger".to_string(),
+                caps: vec![],
+                args: vec![],
+            },
+            &mut env,
+        );
+        let agent_id = match env.get("h") {
+            Some(RtValue::Handle(id)) => id.clone(),
+            _ => panic!("Expected handle"),
+        };
+        let field = |e: &Evaluator, k: &str| e.agents.get(&agent_id).unwrap().state.get(k).cloned();
+
+        // Debit 30: balance 100 -> 70; delta {balance:100} held. note untouched.
+        evaluator.run_agent_handler(&agent_id, "debit", &RtValue::Int(30));
+        assert_eq!(field(&evaluator, "balance"), Some(RtValue::Int(70)));
+        assert_eq!(field(&evaluator, "note"), Some(RtValue::Int(0)));
+
+        // Annotate AFTER the checkpoint: note 0 -> 7 (unrelated to `undo`).
+        evaluator.run_agent_handler(&agent_id, "annotate", &RtValue::Int(0));
+        assert_eq!(field(&evaluator, "note"), Some(RtValue::Int(7)));
+
+        // Reverse: balance restored to 100, but note STAYS 7 (delta, not
+        // whole-checkpoint — the unrelated intervening write survives).
+        evaluator.run_agent_handler(&agent_id, "rollback", &RtValue::Int(0));
+        assert_eq!(
+            field(&evaluator, "balance"),
+            Some(RtValue::Int(100)),
+            "reverse must restore the field the body mutated"
+        );
+        assert_eq!(
+            field(&evaluator, "note"),
+            Some(RtValue::Int(7)),
+            "reverse must NOT clobber a field the body never touched"
+        );
+    }
+
     // ================================================================
     // SECTION 20: AGENT ERGONOMICS — query_trace
     // ================================================================