v2 (c) Neutral reversal bridge: Echo types gate reversibility with a retained residue (Lean + Rust)

.machine_readable/6a2/STATE.a2ml

@@ -7,7 +7,7 @@ project = "julia-the-viper"
 version = "0.0.1"
 last-updated = "2026-06-15"
 status = "active"
-session = "2026-06-15 — bookkeeping/tidying consolidation: lake build green (8 libs, 0 sorry/admit/axiom, 0 vacuity, 0 lint warnings); 4 stray branches resolved (2 stale-merged flagged for UI deletion — git push --delete returned 403 — + codeql weekly->monthly cron folded + estate-standardization salvaged: CODEOWNERS + 17 wiki SPDX headers); ADR-0007 gains the graded-comonad/tropical-grade characterization note; PMPL-1.0 vs MPL-2.0 header discrepancy flagged for governance decision (gap-006); number-system-semantics + v2 (c) bridge remain queued"
+session = "2026-06-15 — bookkeeping/tidying consolidation: lake build green (8 libs, 0 sorry/admit/axiom, 0 vacuity, 0 lint warnings); 4 stray branches resolved (2 stale-merged flagged for UI deletion — git push --delete returned 403 — + codeql weekly->monthly cron folded + estate-standardization salvaged: CODEOWNERS + 17 wiki SPDX headers); ADR-0007 gains the graded-comonad/tropical-grade characterization note; PMPL-1.0 vs MPL-2.0 header discrepancy flagged for governance decision (gap-006); v2 (c) Neutral reversal bridge LANDED (Lean + Rust, green); number-system-semantics (gap-005) remains the next rung"
 
 [project-context]
 name = "Julia The Viper"
@@ -58,7 +58,7 @@ issues = [
 actions = [
   "Governance hardening (branch claude/jtv-governance-hardening): pin governance-reusable@main → SHA (consistent with sibling standards reusables); add secret-scanner.yml wrapper (standards reusable exists at 524523c); add 'actions' language to codeql.yml; harden proof-regression download-then-run; NOTE the reusable-call-job missing-timeout Hypatia findings are false-positives (timeout-minutes is invalid on reusable-call jobs)",
   "Number-system semantics (ADR-0007 D6): value model for the 7 systems + per-system additive-algebra → Echo-tier classification; keep addition-only (×/÷ generated, not primitive); lift type_preservation beyond τ=int",
-  "v2 (c) token/residue neutral-reversal bridge (ADR-0007 D5 Neutral tier): JtvEcho admissibleWithResidue + Neutral-recoverable-given-token theorem; typechecker reversible{}->tok admits Neutral; runtime residue in reversible.rs (or documented conservative scope)",
+  "v2 (c) token/residue neutral-reversal bridge — LANDED 2026-06-15 (ADR-0007 D5 Neutral tier): JtvEcho admissibleWithResidue + blockEcho_admissibleWithResidue; JtvTheorems execBackwardWithToken + rev_forward_backward_with_token + rev_backward_naive_fails_self_ref; echo.rs self-ref Breaking->Neutral; typechecker.rs check_echo_admissible_with_residue (token unlocks Neutral); reversible.rs RecordedOp::Snapshot residue. NEXT: (b) Echo as a first-class function effect",
   "Echo as first-class function effect ('(b)') — after (c) stabilises",
   "Verification bridge: correlation tests between Lean semantics and Rust interpreter",
   "PataCL Phase 1 → unblocks JtV coproc implementation Phase 2"
@@ -83,7 +83,8 @@ sessions = [
   { date = "2026-06-13", subject = "PR #27 merged: de-vacuated 8 True-typed believeme theorems (string_not_executable, confluence, no_vulnerable_constructs, no_reverse_joinpoints, dataExpr_no_control, data_evaluation_secure, control_data_noninterference, rev_composition) into real compiled statements; NO-VACUITY + Int-only-scope recorded in capability matrix" },
   { date = "2026-06-13", subject = "ADR-0007: addition-only mandate (absolute; ×/÷ generated, not primitive); subtraction = reverse addition (not 2s-complement/not primitive); Harvard-in-von-Neumann AOLD insertability; shortest-path-to-equality + Echo lineage + cross-system routing; additive-algebra → reversibility-tier (group→Safe / cancellative→Neutral / idempotent→Breaking; Echo's own join is idempotent)" },
   { date = "2026-06-15", subject = "Bookkeeping/tidying consolidation: confirmed lake build green (8 libs); cleared all Lean unused-variable lint warnings (_-prefix); resolved 4 stray remote branches (flagged 2 stale-merged changelog/tech-debt for UI deletion — content already on main, git 403 blocked programmatic delete; folded codeql weekly->monthly cron; salvaged CODEOWNERS + 17 wiki SPDX headers from estate-standardization-20260607, dropped its superseded pre-repair Lean drafts + old contractiles); ADR-0007 graded-comonad/tropical-grade characterization note; flagged PMPL-1.0 vs MPL-2.0 discrepancy (gap-006)" },
-  { date = "2026-06-15", subject = "Security-hygiene clean (post-#33): triaged the Hypatia 67-finding report — informational (--exit-zero, gate passed), none originating from #33. Added CodeQL actions language; DELETED the frozen playground/experiments/_attic archive (17 files incl. stray npm package.json + a Julia demo), clearing both criticals + several highs at the source, with all dangling refs cleaned (deno.json excludes, bot_directives/hypatia.a2ml, .hypatia-ignore, playground README/Justfile); documented rsr_check.rs unsafe_block as a verified false-positive (Hypatia matched the RSR checker's own detection string). Deferred to a deliberate governance-hardening pass: secret-scanner.yml creation, scorecard job-perms, curl|sh install hardening." }
+  { date = "2026-06-15", subject = "Security-hygiene clean (post-#33): triaged the Hypatia 67-finding report — informational (--exit-zero, gate passed), none originating from #33. Added CodeQL actions language; DELETED the frozen playground/experiments/_attic archive (17 files incl. stray npm package.json + a Julia demo), clearing both criticals + several highs at the source, with all dangling refs cleaned (deno.json excludes, bot_directives/hypatia.a2ml, .hypatia-ignore, playground README/Justfile); documented rsr_check.rs unsafe_block as a verified false-positive (Hypatia matched the RSR checker's own detection string). Deferred to a deliberate governance-hardening pass: secret-scanner.yml creation, scorecard job-perms, curl|sh install hardening." },
+  { date = "2026-06-15", subject = "v2 (c) Neutral reversal bridge LANDED (Lean + Rust). Lean: JtvTheorems execBackwardWithToken + rev_forward_backward_with_token (full-state Bennett recovery, unconditional even for self-referential x += x) + rev_backward_naive_fails_self_ref (token necessary); JtvEcho admissibleWithResidue + blockEcho_admissibleWithResidue + admissible_implies_admissibleWithResidue + neutral_residue_only. Rust: echo.rs reclassifies self-reference Breaking->Neutral (token-recoverable, not erasure; Breaking reserved for future non-group/tropical systems per D6); typechecker.rs splits the Echo gate — reversible{}->tok uses check_echo_admissible_with_residue (admits Neutral; tokenless + reverse{} stay Safe-only); reversible.rs RecordedOp::Snapshot records/restores the residue. lake build + cargo test (99 lib + integration) + clippy -D warnings all green." }
 ]
 
 [design-artefact-locations]

crates/jtv-core/src/echo.rs

@@ -58,19 +58,34 @@ impl Echo {
         self.join(other) == other
     }
 
-    /// Whether this echo may appear inside a reverse block.
+    /// Whether this echo may appear inside a plain `reverse { }` block.
     ///
-    /// Policy: **Safe-only.** A reverse block must be fully reversible, so only
-    /// `EchoSafe` (bijective `+`/`-`) statements are admissible. `EchoNeutral`
-    /// is rejected too: although spec v2 §9 permits it *in principle*
-    /// (reversal via a retained residue, Bennett-style), that runtime mechanism
-    /// is not implemented, so the checker conservatively requires `Safe`.
-    /// `EchoBreaking` is of course always rejected.
+    /// Policy: **Safe-only.** A `reverse { }` block inverts immediately with no
+    /// retained residue, so only `EchoSafe` (bijective `+`/`-`) statements are
+    /// admissible. `EchoNeutral` is rejected here because, without a token, its
+    /// loss lineage is not available to invert from; `EchoBreaking` is of
+    /// course always rejected.
     ///
     /// Corresponds to `Echo.admissible` in `JtvEcho.lean`.
     pub fn admissible_in_reverse(self) -> bool {
         self == Echo::Safe
     }
+
+    /// Whether this echo may appear inside a `reversible { } -> tok` block —
+    /// the **residue-retaining** (Bennett) policy.
+    ///
+    /// A `reversible { } -> tok` form records a reversal log and binds a token,
+    /// so a later `reverse tok` can invert `EchoNeutral` (structured-loss)
+    /// statements by restoring their retained residue — not just `EchoSafe`
+    /// ones. `EchoBreaking` (total erasure) is still rejected: no token can
+    /// recover destroyed lineage.
+    ///
+    /// Corresponds to `Echo.admissibleWithResidue` in `JtvEcho.lean`; the
+    /// operational justification is `rev_forward_backward_with_token` in
+    /// `JtvTheorems`.
+    pub fn admissible_with_residue(self) -> bool {
+        self != Echo::Breaking
+    }
 }
 
 impl std::fmt::Display for Echo {
@@ -106,7 +121,15 @@ pub fn classify_reversible_stmt(stmt: &ReversibleStmt) -> Echo {
         // in `e`, in which case the original value is destroyed (Breaking).
         ReversibleStmt::AddAssign(target, expr) | ReversibleStmt::SubAssign(target, expr) => {
             if data_expr_uses(expr, target) {
-                Echo::Breaking
+                // Self-reference (e.g. `x += x`): the naive `-` inverse fails,
+                // but the original value is recoverable from a retained residue
+                // (token) — this is the `Neutral` (Bennett) tier, NOT total
+                // erasure. In the addition-only group every overwrite can be
+                // tokenised, so `Breaking` never arises here; it is reserved for
+                // future non-group / idempotent number systems (ADR-0007 D6).
+                // Formal basis: `rev_forward_backward_with_token` /
+                // `rev_backward_naive_fails_self_ref` in `JtvTheorems`.
+                Echo::Neutral
             } else {
                 Echo::Safe
             }
@@ -173,10 +196,15 @@ mod tests {
         assert!(Neutral.leq(Breaking));
         assert!(Safe.leq(Breaking));
         assert!(!Breaking.leq(Safe));
-        // Safe-only reversal policy: only Safe is admissible in a reverse block.
+        // Safe-only reversal policy (`reverse { }`): only Safe is admissible.
         assert!(Safe.admissible_in_reverse());
         assert!(!Neutral.admissible_in_reverse());
         assert!(!Breaking.admissible_in_reverse());
+        // Residue policy (`reversible { } -> tok`): Safe + Neutral admissible,
+        // Breaking rejected. Matches `Echo.admissibleWithResidue` in Lean.
+        assert!(Safe.admissible_with_residue());
+        assert!(Neutral.admissible_with_residue());
+        assert!(!Breaking.admissible_with_residue());
     }
 
     #[test]
@@ -188,20 +216,25 @@ mod tests {
     }
 
     #[test]
-    fn self_reference_is_breaking() {
-        // x += x  destroys the original x  ->  Breaking
+    fn self_reference_is_neutral() {
+        // x += x  is lossy but token-recoverable (Bennett)  ->  Neutral, not
+        // Breaking. Rejected by `reverse { }` (Safe-only) yet admitted by
+        // `reversible { } -> tok` (residue policy).
         let stmt =
             ReversibleStmt::AddAssign("x".to_string(), DataExpr::Identifier("x".to_string()));
-        assert_eq!(classify_reversible_stmt(&stmt), Echo::Breaking);
+        assert_eq!(classify_reversible_stmt(&stmt), Echo::Neutral);
+        assert!(!classify_reversible_stmt(&stmt).admissible_in_reverse());
+        assert!(classify_reversible_stmt(&stmt).admissible_with_residue());
     }
 
     #[test]
-    fn block_breaking_iff_any_breaking() {
-        // [Safe, Safe] -> Safe ; one Breaking poisons the block.
+    fn block_neutral_when_any_self_reference() {
+        // [Safe] -> Safe ; a self-referential (Neutral) statement lifts the
+        // whole block to Neutral (still token-recoverable, never Breaking).
         let safe = ReversibleStmt::AddAssign("x".to_string(), DataExpr::Number(Number::Int(5)));
-        let breaking =
+        let neutral =
             ReversibleStmt::AddAssign("y".to_string(), DataExpr::Identifier("y".to_string()));
         assert_eq!(classify_stmts(std::slice::from_ref(&safe)), Echo::Safe);
-        assert_eq!(classify_stmts(&[safe.clone(), breaking]), Echo::Breaking);
+        assert_eq!(classify_stmts(&[safe.clone(), neutral]), Echo::Neutral);
     }
 }

crates/jtv-core/src/reversible.rs

@@ -19,6 +19,12 @@ pub enum RecordedOp {
         then_ops: Vec<RecordedOp>,
         else_ops: Vec<RecordedOp>,
     },
+    /// Residue/token (Bennett) record: the value of `target` that a
+    /// self-referential (Neutral) step overwrote, saved *before* the step. The
+    /// naive `-value` inverse is wrong for self-reference, so this is reversed
+    /// by restoring `old_value`. Runtime counterpart of `execBackwardWithToken`
+    /// in `jtv_proofs/JtvTheorems.lean` (the v2 "(c)" Neutral bridge).
+    Snapshot { target: String, old_value: Value },
 }
 
 impl RecordedOp {
@@ -42,6 +48,13 @@ impl RecordedOp {
                 then_ops: then_ops.iter().rev().map(|op| op.inverse()).collect(),
                 else_ops: else_ops.iter().rev().map(|op| op.inverse()).collect(),
             },
+            // A snapshot's inverse is the snapshot itself: applying it restores
+            // the saved residue (`old_value`), which is exactly the undo of the
+            // step that overwrote `target`.
+            RecordedOp::Snapshot { target, old_value } => RecordedOp::Snapshot {
+                target: target.clone(),
+                old_value: old_value.clone(),
+            },
         }
     }
 }
@@ -218,11 +231,22 @@ impl ReversibleInterpreter {
                 let current = self.get_variable(target)?;
                 let new_value = current.add(&value)?;
 
-                // Record the operation
-                self.trace.record(RecordedOp::AddAssign {
-                    target: target.clone(),
-                    value: value.clone(),
-                });
+                // Record the operation. Self-reference (`x += x`) is the Neutral
+                // tier: the naive `-value` inverse is wrong, so snapshot the
+                // overwritten value (the residue/token) and invert by restoring
+                // it (Bennett). Independent targets are Safe: record the added
+                // value and invert by subtraction.
+                if expr_contains_var(expr, target) {
+                    self.trace.record(RecordedOp::Snapshot {
+                        target: target.clone(),
+                        old_value: current,
+                    });
+                } else {
+                    self.trace.record(RecordedOp::AddAssign {
+                        target: target.clone(),
+                        value: value.clone(),
+                    });
+                }
 
                 self.variables.insert(target.clone(), new_value);
                 Ok(())
@@ -233,11 +257,19 @@ impl ReversibleInterpreter {
                 let neg_value = value.negate()?;
                 let new_value = current.add(&neg_value)?;
 
-                // Record the operation
-                self.trace.record(RecordedOp::SubAssign {
-                    target: target.clone(),
-                    value: value.clone(),
-                });
+                // See AddAssign: self-reference snapshots the residue (Neutral);
+                // independent targets record the value and invert by addition.
+                if expr_contains_var(expr, target) {
+                    self.trace.record(RecordedOp::Snapshot {
+                        target: target.clone(),
+                        old_value: current,
+                    });
+                } else {
+                    self.trace.record(RecordedOp::SubAssign {
+                        target: target.clone(),
+                        value: value.clone(),
+                    });
+                }
 
                 self.variables.insert(target.clone(), new_value);
                 Ok(())
@@ -329,6 +361,12 @@ impl ReversibleInterpreter {
                 }
                 Ok(())
             }
+            // Restore the saved residue — the Bennett undo of a self-referential
+            // (Neutral) overwrite.
+            RecordedOp::Snapshot { target, old_value } => {
+                self.variables.insert(target.clone(), old_value.clone());
+                Ok(())
+            }
         }
     }
 
@@ -594,4 +632,29 @@ mod tests {
         // State should be identical to original
         assert_eq!(interp.get_state(), &original_state);
     }
+
+    #[test]
+    fn test_neutral_self_reference_recovered_via_residue() {
+        // The v2 "(c)" Neutral bridge at runtime: `x += x` is lossy under the
+        // naive `-` inverse, but the recorded residue (a snapshot of the old x)
+        // restores it exactly — forward then reverse = identity.
+        let mut interp = ReversibleInterpreter::new();
+        interp.set("x".to_string(), Value::Int(5));
+
+        let block = ReverseBlock {
+            body: vec![ReversibleStmt::AddAssign(
+                "x".to_string(),
+                DataExpr::Identifier("x".to_string()),
+            )],
+        };
+
+        // Forward `x += x`  ->  x = 10, snapshotting old x = 5.
+        interp.execute_forward(&block).unwrap();
+        assert_eq!(interp.get("x"), Some(&Value::Int(10)));
+
+        // Reverse via the recorded residue restores the original x = 5
+        // (the naive `x -= x` inverse would wrongly yield 0).
+        interp.execute_reverse().unwrap();
+        assert_eq!(interp.get("x"), Some(&Value::Int(5)));
+    }
 }