From f5faa95b919e182dc425d36b97940570dc648655 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 18:46:20 +0000 Subject: [PATCH] =?UTF-8?q?feat(L10):=20rung-3b=20runtime=20=E2=80=94=20pe?= =?UTF-8?q?r-variable=20delta=20residue=20replay?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Refine `reverse ` to restore only the state fields its `reversible as ` body mutated (a before-image delta), not the whole agent state map. Fixes a real clobber: under the whole-checkpoint cut a reverse would silently revert an unrelated field that an intervening handler had changed. - eval: `collect_set_fields` statically scans the body (descending nested control) for `set` targets; `ReversibleAs` captures the before-image of just those fields as `Holding(delta)`; `ReverseNamed` writes them back rather than replacing the whole `AgentInstance.state`. Over-approximation is harmless (a field set only on an untaken branch is captured at its current value, so write-back is a no-op). - test: residue_reverse_is_per_field_delta_not_whole_checkpoint — a reverse restores `balance` but preserves a `note` an intervening handler changed. - spec §11b.8 / example / design-note: "checkpoint" -> "per-variable delta" in lockstep. 914 oo7-core lib tests pass; fmt + clippy clean; example + e2e green. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- CHANGELOG.md | 1 + crates/oo7-core/src/eval.rs | 104 +++++++++++++++++++++++----- crates/oo7-core/src/eval_tests.rs | 102 +++++++++++++++++++++++++++ docs/echo-residue-integration.adoc | 8 ++- examples/transactional_rollback.007 | 19 ++--- spec/TYPE-SYSTEM-SPEC.adoc | 36 ++++++---- 6 files changed, 227 insertions(+), 43 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b947021..5bb5117 100644 --- a/CHANGELOG.md +++ b/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 ` in one handler is now reversible by `reverse ` 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 ` 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 = `.** 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 = ` 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 ` now has an operational meaning: restore the agent to the checkpoint captured by the matching `reversible as `. New explicit `residue ` agent-member declaration (the chosen *explicit state cell* design) declares a residue cell; `AgentInstance` carries a `residues: HashMap` where `ResidueCell = Holding(state-snapshot) | Spent` (the evaluator shadow of the Idris `ResidueCell`). Evaluator semantics: `reversible as ` snapshots the agent state map *before* its body runs (`Holding`), so a later — possibly cross-handler — `reverse ` restores that snapshot and marks the cell `Spent`; a second `reverse ` 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 ` restores *only* the state fields its `reversible as ` 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 ` 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. diff --git a/crates/oo7-core/src/eval.rs b/crates/oo7-core/src/eval.rs index 55fb9e8..699f995 100644 --- a/crates/oo7-core/src/eval.rs +++ b/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 ` body ran. `reverse ` restores it. + /// A live reversal *delta*: the before-image of exactly the state fields the + /// `reversible as ` body mutates, captured immediately before it ran. + /// `reverse ` writes each captured field back, leaving every other + /// field — including unrelated `set`s from intervening handlers — untouched. Holding(HashMap), /// The residue has already been replayed (consumed exactly once). Spent, } +/// Collect the names of agent `state` fields that a control body assigns via +/// `set = …`, 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 { + fn go(stmt: &ControlStmt, out: &mut HashSet) { + 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 ` - // 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 + // ` 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 = 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 diff --git a/crates/oo7-core/src/eval_tests.rs b/crates/oo7-core/src/eval_tests.rs index adf2bef..8877cfd 100644 --- a/crates/oo7-core/src/eval_tests.rs +++ b/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 // ================================================================ diff --git a/docs/echo-residue-integration.adoc b/docs/echo-residue-integration.adoc index e4d78cd..df235f1 100644 --- a/docs/echo-residue-integration.adoc +++ b/docs/echo-residue-integration.adoc @@ -244,9 +244,11 @@ restorable by a `reverse ` in another — closing the cross-handler once-only that the static half (§11b.6) could only check by presence. See TYPE-SYSTEM-SPEC §11b.8 and `examples/transactional_rollback.007`. -The *checkpoint* semantics (restore the whole state map, not a per-variable -delta) is the honest scope of this first runtime cut; the proof-side bridge -lemma against echo-types remains the natural next step. +The replay uses a *per-variable delta*: `reversible as ` captures the +before-image of only the fields its body mutates (a static scan of the body), +and `reverse ` writes just those back — so unrelated state, including +intervening `set`s by other handlers, survives the reversal. The proof-side +bridge lemma against echo-types remains the natural next step. == Cross-repo bridge (echo-types) diff --git a/examples/transactional_rollback.007 b/examples/transactional_rollback.007 index 5a4f78a..2a8f80e 100644 --- a/examples/transactional_rollback.007 +++ b/examples/transactional_rollback.007 @@ -8,19 +8,20 @@ -- channel is made explicit with a `residue ` agent member. -- -- Runtime semantics (evaluator): --- * `reversible as undo { ... }` SNAPSHOTS the agent's state map *before* the --- body runs (storing it as a `Holding` cell keyed `undo`), then runs the --- body — which here mutates `balance` via `set`; --- * `reverse undo` RESTORES that snapshot and marks the cell `Spent`; a --- second `reverse undo` finds `Spent` and is a no-op (replay at most once, --- the runtime witness of the Idris `takeForReverse : ... -> Maybe`). +-- * `reversible as undo { ... }` captures a BEFORE-IMAGE DELTA of just the +-- fields its body mutates (`balance`) *before* the body runs (storing it as +-- a `Holding` cell keyed `undo`), then runs the body; +-- * `reverse undo` WRITES BACK those captured fields and marks the cell +-- `Spent`; a second `reverse undo` finds `Spent` and is a no-op (replay at +-- most once, the runtime witness of the Idris `takeForReverse : ... -> Maybe`). -- --- The cell lives on the agent instance, so a snapshot taken in `debit` is +-- The cell lives on the agent instance, so a delta captured in `debit` is -- restorable by `reverse undo` in the *separate* `rollback` handler — the -- cross-handler reversal the rung-3b static half could only check by presence. -- --- Checkpoint semantics: `reverse` restores the whole state map to the --- snapshot, not a per-variable delta. See TYPE-SYSTEM-SPEC §11b.8. +-- Per-variable delta semantics: `reverse` restores only the fields the body +-- touched, leaving unrelated state (and intervening `set`s by other handlers) +-- intact. See TYPE-SYSTEM-SPEC §11b.8. agent Transactional { -- Mutable agent state (§11b.7) is the substrate the residue cell snapshots. diff --git a/spec/TYPE-SYSTEM-SPEC.adoc b/spec/TYPE-SYSTEM-SPEC.adoc index 122159b..019c8cd 100644 --- a/spec/TYPE-SYSTEM-SPEC.adoc +++ b/spec/TYPE-SYSTEM-SPEC.adoc @@ -853,21 +853,27 @@ agent Transactional { Operational semantics (evaluator): -* `reversible as { body }` **snapshots** the agent's state map - immediately *before* `body` runs, storing it in a cell keyed by `` as - `Holding(snapshot)`, then runs `body` (which may `set` state). The cell lives - on the agent instance, so the snapshot survives into later handler firings. -* `reverse ` consumes the cell: if it is `Holding(snapshot)`, the agent's - state is **restored** to `snapshot` and the cell becomes `Spent`. If it is - `Spent` or absent, `reverse ` is a no-op — the runtime witness of - `takeForReverse` returning `Nothing` (replay at most once). - -This is a *checkpoint* semantics: `reverse` restores the whole agent state map -to the snapshot, not a per-variable delta. The cell (`ResidueCell::Holding` / -`Spent`) is the evaluator shadow of the Idris `ResidueCell` GADT in -`EchoResidueLinear.idr`. The explicit `residue ` declaration also feeds -the rung-3b static presence-set (§11b.6), so a `reverse ` against a -declared cell type-checks even with no literal `reversible as ` in view. +* `reversible as { body }` captures a **before-image delta** — the prior + values of exactly the state fields `body` assigns via `set` (found by a static + scan of `body`, descending through nested control) — immediately *before* + `body` runs, storing it in a cell keyed by `` as `Holding(delta)`, then + runs `body`. The cell lives on the agent instance, so the delta survives into + later handler firings. +* `reverse ` consumes the cell: if it is `Holding(delta)`, each field in + the delta is **written back** to its captured value and the cell becomes + `Spent`. If it is `Spent` or absent, `reverse ` is a no-op — the runtime + witness of `takeForReverse` returning `Nothing` (replay at most once). + +This is a *per-variable delta* semantics: `reverse` restores only the fields the +body mutated, so state the body never touched — including unrelated `set`s made +by *intervening* handlers between the `reversible as` and the `reverse` — is left +intact. (Over-approximating the field set is harmless: a field assigned only on +an untaken branch is captured at its current value, so writing it back is a +no-op.) The cell (`ResidueCell::Holding` / `Spent`) is the evaluator shadow of +the Idris `ResidueCell` GADT in `EchoResidueLinear.idr`. The explicit `residue +` declaration also feeds the rung-3b static presence-set (§11b.6), so a +`reverse ` against a declared cell type-checks even with no literal +`reversible as ` in view. == 12. The Layers in Concert