From 0db52f07ebb671e2ffef951da9d9d50654cb0410 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 17:57:12 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat(echo):=20v2=20(c)=20Neutral=20reversal?= =?UTF-8?q?=20bridge=20=E2=80=94=20Lean=20rung?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Formalises the Bennett-style residue/token reversal (ADR-0007 D5/D6 Neutral tier), generalising reversibility beyond the Safe/group case. JtvTheorems (operational): - RevOp.execBackwardWithToken: restore the overwritten var from a retained token. - rev_forward_backward_with_token: forward then token-restore recovers the FULL state at every variable, UNCONDITIONALLY (no x ∉ e.freeVars needed) — the self-referential case that defeats rev_forward_backward. - rev_backward_naive_fails_self_ref: proves the naive inverse fails for x += x (0 ≠ 1), so the token is necessary. JtvEcho (effect contract for reversible{}->tok): - Echo.admissibleWithResidue: admits safe + neutral, rejects breaking. - admissibleWithResidue_iff, admissible_implies_admissibleWithResidue, neutral_residue_only, join_admissibleWithResidue. - blockEcho_admissibleWithResidue (block soundness) + breaking_blocks_residual_reversal. lake build green; 0 sorry/admit/axiom; 0 warnings. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- jtv_proofs/JtvEcho.lean | 76 +++++++++++++++++++++++++++++++++++++ jtv_proofs/JtvTheorems.lean | 47 +++++++++++++++++++++++ 2 files changed, 123 insertions(+) diff --git a/jtv_proofs/JtvEcho.lean b/jtv_proofs/JtvEcho.lean index 655f98f..6958e4d 100644 --- a/jtv_proofs/JtvEcho.lean +++ b/jtv_proofs/JtvEcho.lean @@ -28,6 +28,12 @@ residue-retaining) and `breaking` are both rejected. This is the formal contract enforced by `crates/jtv-core/src/echo.rs`. + The companion result `blockEcho_admissibleWithResidue` (Section 2b) formalises + the v2 `reversible { } -> tok` policy: `neutral` is *also* admissible there, + because its loss lineage is retained as a token (Bennett-style); only + `breaking` is rejected. The operational justification is + `rev_forward_backward_with_token` in `JtvTheorems`. + Proofs are deliberately Mathlib-free (Lean core only) and discharge every goal by finite case analysis, matching the style of the other JtV proofs. -/ @@ -135,6 +141,43 @@ theorem admissible_downward_closed (a b : Echo) : cases a <;> cases b <;> intro hle hb <;> simp_all [LE.le, Echo.le, Echo.join, Echo.admissible] +-- ============================================================================ +-- SECTION 2b: RESIDUE-RETAINING ADMISSIBILITY (the reversible{}->tok contract) +-- ============================================================================ + +/-- Boolean admissibility under the **residue-retaining** (Bennett) policy: an + Echo may appear in a `reversible { } -> tok` block iff it is not `breaking`. + Unlike `admissible` (Safe-only), this admits `neutral`: a lossy op is + reversible when its loss lineage (the retained token / residue) is kept. The + operational justification is `rev_forward_backward_with_token` in + `JtvTheorems`. `breaking` (total erasure) is still rejected — no token can + recover destroyed lineage. (ADR-0007 D5/D6; spec v2 §9.) -/ +def Echo.admissibleWithResidue : Echo → Bool + | .breaking => false + | _ => true + +theorem admissibleWithResidue_iff (e : Echo) : + e.admissibleWithResidue = true ↔ e ≠ Echo.breaking := by + cases e <;> simp [Echo.admissibleWithResidue] + +/-- The Safe-only policy is strictly stronger: anything admissible under + `reverse { }` is admissible under `reversible { } -> tok`. -/ +theorem admissible_implies_admissibleWithResidue (e : Echo) : + e.admissible = true → e.admissibleWithResidue = true := by + cases e <;> simp [Echo.admissible, Echo.admissibleWithResidue] + +/-- `neutral` is exactly the capability the token form adds: rejected by + Safe-only, accepted with a retained residue. -/ +theorem neutral_residue_only : + Echo.neutral.admissible = false ∧ Echo.neutral.admissibleWithResidue = true := + ⟨rfl, rfl⟩ + +/-- Compositional law for the residue policy (mirrors `join_admissible`). -/ +theorem join_admissibleWithResidue (a b : Echo) : + (a ⊔ b).admissibleWithResidue + = (a.admissibleWithResidue && b.admissibleWithResidue) := by + cases a <;> cases b <;> rfl + -- ============================================================================ -- SECTION 3: REVERSE BLOCKS AS LISTS OF ECHOES -- ============================================================================ @@ -174,6 +217,39 @@ theorem breaking_blocks_reversal (pre post : List Echo) : show (e.admissible && allAdmissible (pre ++ Echo.breaking :: post)) = false rw [ih]; exact Bool.and_false _ +-- ---------------------------------------------------------------------------- +-- Residue-policy block soundness (companion to the Safe-only results above, +-- placed here because it consumes `blockEcho` from this section). +-- ---------------------------------------------------------------------------- + +/-- Block-level "all admissible with residue" (residue/Bennett policy). -/ +def allAdmissibleWithResidue : List Echo → Bool + | [] => true + | e :: es => e.admissibleWithResidue && allAdmissibleWithResidue es + +/-- **Residue-block soundness.** A `reversible { } -> tok` block is well-typed + iff every statement is non-`breaking` — the contract `echo.rs` enforces for + the token-carrying reversal form. -/ +theorem blockEcho_admissibleWithResidue (es : List Echo) : + (blockEcho es).admissibleWithResidue = allAdmissibleWithResidue es := by + induction es with + | nil => rfl + | cons e es ih => + show (e ⊔ blockEcho es).admissibleWithResidue + = (e.admissibleWithResidue && allAdmissibleWithResidue es) + rw [join_admissibleWithResidue, ih] + +/-- Even with residue retention, a single `breaking` op blocks reversal. -/ +theorem breaking_blocks_residual_reversal (pre post : List Echo) : + (blockEcho (pre ++ Echo.breaking :: post)).admissibleWithResidue = false := by + rw [blockEcho_admissibleWithResidue] + induction pre with + | nil => rfl + | cons e pre ih => + show (e.admissibleWithResidue + && allAdmissibleWithResidue (pre ++ Echo.breaking :: post)) = false + rw [ih]; exact Bool.and_false _ + -- ============================================================================ -- SECTION 4: FIBRES — THE echo-types CORRESPONDENCE -- ============================================================================ diff --git a/jtv_proofs/JtvTheorems.lean b/jtv_proofs/JtvTheorems.lean index 4124f5d..80b46da 100644 --- a/jtv_proofs/JtvTheorems.lean +++ b/jtv_proofs/JtvTheorems.lean @@ -375,6 +375,53 @@ theorem rev_forward_backward (op : RevOp) (σ : State) (x : String) (e : DataExp exact hfree simp [h] +/-- Execute a reversible operation backward using a *retained token* — the value + of the overwritten variable saved *before* the forward step. This is the + Bennett-style residue reversal: rather than recomputing the inverse from `e` + (which fails when `x` is self-referential, `x ∈ e.freeVars`), restore the + variable directly from the saved token. -/ +def RevOp.execBackwardWithToken (op : RevOp) (σ : State) (tok : Int) : State := + match op with + | addAssign x _ => σ[x ↦ tok] + | subAssign x _ => σ[x ↦ tok] + +/-- + **Theorem (Neutral reversibility — recoverable given its token).** For an + `x += e` operation, restoring `x` from the token `σ x` (its value saved before + the forward step) recovers the original state at *every* variable — + **unconditionally**, even when `x ∈ e.freeVars` (the self-referential case + that defeats `rev_forward_backward`). This is the formal contract of the v2 + `reversible { } -> tok` form: a `neutral` (lossy) op stays reversible when its + loss lineage (the token) is retained — ADR-0007 D5/D6, the `neutral` tier + (cancellative-monoid reverse-given-residue). The effect-level companion is + `Jtv.Echo.blockEcho_admissibleWithResidue`. +-/ +theorem rev_forward_backward_with_token + (op : RevOp) (σ : State) (x : String) (e : DataExpr) + (hop : op = RevOp.addAssign x e) (y : String) : + RevOp.execBackwardWithToken op (RevOp.execForward op σ) (σ x) y = σ y := by + subst hop + simp only [RevOp.execForward, RevOp.execBackwardWithToken, State.update] + by_cases h : y = x + · subst h; simp + · simp [h] + +/-- + **Why the token is necessary.** In the self-referential case `x += x` + (`e = var x`, so `x ∈ e.freeVars`), the naive `execBackward` does *not* recover + the original value: concretely at `σ x = 1` it yields `0 ≠ 1`. This is exactly + the `neutral` (lossy) case that the Safe-only `execBackward` / + `rev_forward_backward` cannot handle and that the token form above repairs. +-/ +theorem rev_backward_naive_fails_self_ref : + ∃ (σ : State) (x : String) (e : DataExpr), + x ∈ e.freeVars ∧ + RevOp.execBackward (RevOp.addAssign x e) + (RevOp.execForward (RevOp.addAssign x e) σ) x ≠ σ x := by + refine ⟨(fun _ => 1), "x", DataExpr.var "x", ?_, ?_⟩ + · simp [DataExpr.freeVars] + · simp [RevOp.execForward, RevOp.execBackward, State.update, evalDataExpr] + -- ============================================================================ -- SECTION 10: ADDITIONAL PROPERTIES -- ============================================================================ From 6a789239137d748e52df85ecb08a9aab71285aeb Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 18:25:50 +0000 Subject: [PATCH 2/3] =?UTF-8?q?feat(echo):=20v2=20(c)=20Neutral=20reversal?= =?UTF-8?q?=20bridge=20=E2=80=94=20Rust=20typechecker=20+=20runtime?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Makes the Echo type system gate the language's reversal forms per ADR-0007 D5/D6, admitting the Neutral (token-recoverable) tier. echo.rs: reclassify self-reference (x += x) Breaking -> Neutral (token-recoverable, Bennett-style, not total erasure; in the addition-only group every overwrite can be tokenised, so Breaking is reserved for future non-group / tropical systems per D6). Add Echo::admissible_with_residue (admits Safe + Neutral, rejects Breaking). typechecker.rs: split the Echo gate. reversible{}->tok (token bound) uses the residue policy check_echo_admissible_with_residue admitting Neutral; reverse{} and tokenless reversible{} stay Safe-only. The token unlocks the Neutral tier. reversible.rs: RecordedOp::Snapshot residue op — a self-referential step records the overwritten value and inverts by RESTORING it (Bennett), not the wrong naive minus-value. Runtime counterpart of execBackwardWithToken. Tests green: 99 lib + integration; clippy -D warnings clean. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- crates/jtv-core/src/echo.rs | 65 +++++++++++++----- crates/jtv-core/src/reversible.rs | 83 +++++++++++++++++++--- crates/jtv-core/src/typechecker.rs | 107 ++++++++++++++++++++++------- 3 files changed, 204 insertions(+), 51 deletions(-) diff --git a/crates/jtv-core/src/echo.rs b/crates/jtv-core/src/echo.rs index fa36fd3..51ee479 100644 --- a/crates/jtv-core/src/echo.rs +++ b/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); } } diff --git a/crates/jtv-core/src/reversible.rs b/crates/jtv-core/src/reversible.rs index 883f970..868f825 100644 --- a/crates/jtv-core/src/reversible.rs +++ b/crates/jtv-core/src/reversible.rs @@ -19,6 +19,12 @@ pub enum RecordedOp { then_ops: Vec, else_ops: Vec, }, + /// 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))); + } } diff --git a/crates/jtv-core/src/typechecker.rs b/crates/jtv-core/src/typechecker.rs index 30ccdc5..e314d60 100644 --- a/crates/jtv-core/src/typechecker.rs +++ b/crates/jtv-core/src/typechecker.rs @@ -383,13 +383,22 @@ impl TypeChecker { } ControlStmt::ReversibleBlock(rb) => { // The forward pass records a reversal log that a later - // `reverse tok` inverts, so the body must satisfy the SAME Echo - // admissibility rule as a `reverse` block — otherwise the - // recorded log cannot be soundly inverted. Checked structurally - // and FIRST (like `ReverseBlock`); previously this arm skipped - // the Echo gate entirely, leaving the `reversible` form - // un-checked. - self.check_echo_admissible(&rb.body)?; + // `reverse tok` inverts. Echo admissibility is checked + // structurally and FIRST (like `ReverseBlock`). The policy + // depends on whether a residue token is retained: + // * `reversible { } -> tok` (token bound): the residue policy + // — `EchoNeutral` (structured loss) IS admissible because a + // later `reverse tok` recovers it from the saved residue + // (Bennett); only `EchoBreaking` is rejected. This is the + // v2 "(c)" Neutral bridge. + // * `reversible { }` (no token): no residue is available to + // invert from, so it falls back to the Safe-only policy, + // exactly like a plain `reverse` block. + if rb.token_binding.is_some() { + self.check_echo_admissible_with_residue(&rb.body)?; + } else { + self.check_echo_admissible(&rb.body)?; + } for stmt in &rb.body { self.check_reversible_stmt(stmt)?; } @@ -415,14 +424,15 @@ impl TypeChecker { } } - /// Enforce the Echo admissibility rule for a `reverse` / `reversible` - /// block (spec v2 §9) under the **Safe-only** reversal policy: the block is - /// well-typed iff its aggregate echo is `EchoSafe` — i.e. every statement - /// is bijective (`+`/`-` with no self-reference). `EchoNeutral` (structured, - /// residue-retaining loss) and `EchoBreaking` (total erasure) are both - /// rejected, since neither is invertible by the implemented runtime. This - /// is the type-checker realisation of `blockEcho_admissible` in - /// `jtv_proofs/JtvEcho.lean`. + /// Enforce the Echo admissibility rule for a plain `reverse { }` block (and + /// a tokenless `reversible { }`) (spec v2 §9) under the **Safe-only** + /// reversal policy: the block is well-typed iff its aggregate echo is + /// `EchoSafe` — i.e. every statement is bijective (`+`/`-` with no + /// self-reference). `EchoNeutral` (structured, residue-retaining loss) and + /// `EchoBreaking` (total erasure) are both rejected, since neither is + /// invertible without a retained token. This is the type-checker + /// realisation of `blockEcho_admissible` in `jtv_proofs/JtvEcho.lean`; the + /// residue (token) policy is `check_echo_admissible_with_residue`. fn check_echo_admissible(&self, body: &[ReversibleStmt]) -> Result<()> { let aggregate = echo::classify_stmts(body); if !aggregate.admissible_in_reverse() { @@ -438,6 +448,30 @@ impl TypeChecker { Ok(()) } + /// Enforce the Echo admissibility rule for a `reversible { } -> tok` block + /// (spec v2 §9) under the **residue-retaining** (Bennett) policy: the block + /// is well-typed iff its aggregate echo is not `EchoBreaking` — i.e. every + /// statement is either bijective (`EchoSafe`) or structured-loss + /// (`EchoNeutral`) whose residue the bound token retains for a later + /// `reverse tok`. Only `EchoBreaking` (total erasure) is rejected. This is + /// the type-checker realisation of `blockEcho_admissibleWithResidue` in + /// `jtv_proofs/JtvEcho.lean` (the v2 "(c)" Neutral bridge). + fn check_echo_admissible_with_residue(&self, body: &[ReversibleStmt]) -> Result<()> { + let aggregate = echo::classify_stmts(body); + if !aggregate.admissible_with_residue() { + return Err(JtvError::EchoViolation(format!( + "reversible block has echo {aggregate}: it destroys information. \ + A `reversible {{ }} -> tok` block may contain {} and {} statements \ + (the token retains the residue to invert them), but not {} \ + (total erasure), which no token can recover.", + Echo::Safe, + Echo::Neutral, + Echo::Breaking + ))); + } + Ok(()) + } + fn check_reversible_stmt(&mut self, stmt: &ReversibleStmt) -> Result<()> { match stmt { ReversibleStmt::AddAssign(target, expr) | ReversibleStmt::SubAssign(target, expr) => { @@ -645,9 +679,11 @@ mod tests { } #[test] - fn test_reverse_block_rejects_breaking_echo() { - // A reverse block whose statement destroys information (self-reference, - // EchoBreaking) must be rejected by the type checker (spec v2 §9). + fn test_reverse_block_rejects_self_reference() { + // A plain `reverse { }` block is Safe-only: a self-referential statement + // (EchoNeutral, `x += x`) is rejected because, without a token, its + // residue is not available to invert from. With a token the + // `reversible { } -> tok` form admits it — see the residue tests below. use crate::ast::*; let mut checker = TypeChecker::new(); let block = ReverseBlock { @@ -677,13 +713,15 @@ mod tests { } #[test] - fn test_reversible_block_rejects_breaking_echo() { - // A `reversible { … } -> tok` block records a reversal log; if any - // statement is information-destroying (EchoBreaking) the log cannot be - // inverted, so the type checker must reject it under the SAME Echo gate - // as a plain `reverse` block (spec v2 §9). + fn test_reversible_block_with_token_admits_self_reference() { + // A `reversible { x += x } -> tok` block retains a residue (token) for + // the self-referential (EchoNeutral) statement, so a later `reverse tok` + // inverts it (Bennett). Under the residue policy it is ADMITTED — only + // EchoBreaking (total erasure) is rejected. The v2 "(c)" Neutral bridge; + // contrast `test_reverse_block_rejects_self_reference` (no token). use crate::ast::*; let mut checker = TypeChecker::new(); + checker.env.set_var("x".to_string(), Type::Int); let block = ReversibleBlockStmt { body: vec![ReversibleStmt::AddAssign( "x".to_string(), @@ -692,8 +730,7 @@ mod tests { token_binding: Some("tok".to_string()), }; let stmt = ControlStmt::ReversibleBlock(block); - let result = checker.check_control_stmt(&stmt); - assert!(matches!(result, Err(JtvError::EchoViolation(_)))); + assert!(checker.check_control_stmt(&stmt).is_ok()); } #[test] @@ -712,6 +749,26 @@ mod tests { assert!(checker.check_control_stmt(&stmt).is_ok()); } + #[test] + fn test_reversible_block_without_token_rejects_self_reference() { + // Without a bound token there is no retained residue to invert from, so + // a tokenless `reversible { x += x }` falls back to the Safe-only policy + // and the self-referential (EchoNeutral) statement is rejected — the + // token is exactly what unlocks the Neutral tier. + use crate::ast::*; + let mut checker = TypeChecker::new(); + let block = ReversibleBlockStmt { + body: vec![ReversibleStmt::AddAssign( + "x".to_string(), + DataExpr::Identifier("x".to_string()), + )], + token_binding: None, + }; + let stmt = ControlStmt::ReversibleBlock(block); + let result = checker.check_control_stmt(&stmt); + assert!(matches!(result, Err(JtvError::EchoViolation(_)))); + } + #[test] fn test_coercion() { let code = r#" From d39811828fa2931ba4619c1c5ab9a98781d1ba92 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 18:25:50 +0000 Subject: [PATCH 3/3] docs: record v2 (c) Neutral bridge landed (ADR-0007 + STATE) https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .machine_readable/6a2/STATE.a2ml | 7 +++--- ...nly-mandate-and-reversibility-tiering.adoc | 22 +++++++++++++------ 2 files changed, 19 insertions(+), 10 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 05f280b..ec1165f 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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] diff --git a/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc b/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc index 6626f23..d997663 100644 --- a/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc +++ b/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc @@ -177,13 +177,21 @@ basis for the v2 `(c)` Neutral bridge and the number-system → tier map. semantics layer must (a) give each system a value model, (b) classify each by its additive algebra → Echo tier per D6, and (c) keep addition-only (D1) — `×`/`÷` generated, not primitive. -. *v2 "(c)" bridge.* Implements the Neutral tier of D5: `reverse { }` - stays Safe-only; `reversible { } -> tok` admits Neutral via the - retained log/token (Bennett). Lean: extend `JtvEcho` with - `admissibleWithResidue` + a "Neutral recoverable given its token" - theorem mirroring `rev_forward_backward`. Runtime: `reversible.rs` - must record/invert residue for Neutral, or the gate stays - conservative with the scope documented. +. *v2 "(c)" bridge (LANDED 2026-06-15).* Implements the Neutral tier of + D5: `reverse { }` stays Safe-only; `reversible { } -> tok` admits + Neutral via the retained log/token (Bennett). Lean: `JtvEcho` + `admissibleWithResidue` + `blockEcho_admissibleWithResidue`, and + `JtvTheorems` `execBackwardWithToken` / + `rev_forward_backward_with_token` (full-state recovery, unconditional — + even self-referential `x += x`) + `rev_backward_naive_fails_self_ref` + (proves the token is *necessary*). Runtime/typechecker: `echo.rs` + reclassifies self-reference `Breaking → Neutral` (token-recoverable, not + erasure; `Breaking` is now reserved for future non-group / idempotent + systems per D6); `typechecker.rs` gates `reversible { } -> tok` on + `check_echo_admissible_with_residue` (the token unlocks Neutral; + tokenless `reversible { }` and `reverse { }` stay Safe-only); + `reversible.rs` `RecordedOp::Snapshot` records and restores the residue. + `lake build` + `cargo test` + clippy `-D warnings` all green. . *Revisit `DataExpr.neg`* per the D2 note. . *Identity preserved.* D1–D3 confirm v2/Echo do **not** erode JtV: injection-impossibility rests on `no_control_to_data_flow` + disjoint