refactor(echo): Safe-only reverse-block policy + rustfmt

Per design decision: reverse blocks accept only EchoSafe; EchoNeutral and
EchoBreaking are both rejected (stricter than spec §9, which permits Neutral
via residue reversal — deferred until that runtime mechanism exists).

- echo.rs: admissible_in_reverse ⇔ Safe; tests + docs updated; rustfmt-clean.
- typechecker.rs: EchoViolation message reflects Safe-only policy.
- JtvEcho.lean: Echo.admissible is Safe-only; admissible_iff ↔ e = safe.
  join_admissible / blockEcho_admissible still hold (join is safe ⇔ both safe).
- spec §9, ALIGNMENT, PROOF matrix: record the Safe-only policy + the four
  Echo design decisions (effect-only; Safe-only; infer+@echo; bridge deferred).

https://claude.ai/code/session_01EJLZKDtcF1RGdKx6TcUTQG

Author: claude

ALIGNMENT-AFFINESCRIPT.adoc

@@ -115,13 +115,28 @@ truthing discipline, because a mechanized proof cannot lie.
 * [ ] Wire `JtvEcho` into the `proof-regression.yml` gate (already covered by
   the `lakefile.lean` default target).
 
+==== Design decisions (2026-06-02)
+
+. *Echo is effect-only* — a static dimension alongside `Purity`, not a value
+  type (spec §12). A first-class `Echo<T>` value type is reserved for a later
+  phase.
+. *Safe-only reversal* — reverse blocks accept only `EchoSafe`; `Neutral` and
+  `Breaking` are rejected (see §9 implementation note).
+. *Echo source = infer + `@echo(...)` override* — inferred from operation shape,
+  with an optional annotation mirroring `@pure`/`@total`. Lossy numeric widening
+  (e.g. `Float→Int`) is to carry `Neutral` echo.
+. *Agda↔Lean proof bridge deferred* — `JtvEcho.lean` re-mechanizes the model
+  independently for now; `echo-types` remains the Agda source of truth.
+
 === Phase 2 — Echo Types in the checker (commenced here)
 
 * [x] Implement the Echo effect lattice in `crates/jtv-core/src/echo.rs`
   (`Safe ⊑ Neutral ⊑ Breaking`, join, admissibility) — the executable image of
   `JtvEcho.lean`.
-* [x] Enforce spec §9 in the type checker: a `reverse` block is rejected when
-  its aggregate echo is `Breaking` (`JtvError::EchoViolation`).
+* [x] Enforce reversibility in the type checker (Safe-only policy): a `reverse`
+  block is rejected unless every statement is `EchoSafe` — `Neutral` and
+  `Breaking` both raise `JtvError::EchoViolation`. (Spec §9 permits `Neutral` via
+  residue reversal; deferred until that runtime mechanism exists.)
 * [ ] Propagate echo through Data inference as a second effect dimension
   (alongside `Purity`); surface `@echo(...)` annotations.
 * [ ] Bridge value-level fibres (`echo-types`) to the effect classes for

crates/jtv-core/src/echo.rs

@@ -52,10 +52,17 @@ impl Echo {
     }
 
     /// Whether this echo may appear inside a reverse block.
-    /// Spec v2 §9: reverse blocks forbid `Breaking` (information-destroying)
-    /// statements. Corresponds to `Echo.admissible` in `JtvEcho.lean`.
+    ///
+    /// 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.
+    ///
+    /// Corresponds to `Echo.admissible` in `JtvEcho.lean`.
     pub fn admissible_in_reverse(self) -> bool {
-        self != Echo::Breaking
+        self == Echo::Safe
     }
 }
 
@@ -159,42 +166,34 @@ 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.
         assert!(Safe.admissible_in_reverse());
-        assert!(Neutral.admissible_in_reverse());
+        assert!(!Neutral.admissible_in_reverse());
         assert!(!Breaking.admissible_in_reverse());
     }
 
     #[test]
     fn add_assign_independent_is_safe() {
         // x += y  (y independent of x)  ->  Safe
-        let stmt = ReversibleStmt::AddAssign(
-            "x".to_string(),
-            DataExpr::Identifier("y".to_string()),
-        );
+        let stmt =
+            ReversibleStmt::AddAssign("x".to_string(), DataExpr::Identifier("y".to_string()));
         assert_eq!(classify_reversible_stmt(&stmt), Echo::Safe);
     }
 
     #[test]
     fn self_reference_is_breaking() {
         // x += x  destroys the original x  ->  Breaking
-        let stmt = ReversibleStmt::AddAssign(
-            "x".to_string(),
-            DataExpr::Identifier("x".to_string()),
-        );
+        let stmt =
+            ReversibleStmt::AddAssign("x".to_string(), DataExpr::Identifier("x".to_string()));
         assert_eq!(classify_reversible_stmt(&stmt), Echo::Breaking);
     }
 
     #[test]
     fn block_breaking_iff_any_breaking() {
         // [Safe, Safe] -> Safe ; one Breaking poisons the block.
-        let safe = ReversibleStmt::AddAssign(
-            "x".to_string(),
-            DataExpr::Number(Number::Int(5)),
-        );
-        let breaking = ReversibleStmt::AddAssign(
-            "y".to_string(),
-            DataExpr::Identifier("y".to_string()),
-        );
+        let safe = ReversibleStmt::AddAssign("x".to_string(), DataExpr::Number(Number::Int(5)));
+        let breaking =
+            ReversibleStmt::AddAssign("y".to_string(), DataExpr::Identifier("y".to_string()));
         assert_eq!(classify_stmts(&[safe.clone()]), Echo::Safe);
         assert_eq!(classify_stmts(&[safe.clone(), breaking]), Echo::Breaking);
     }

crates/jtv-core/src/typechecker.rs

@@ -409,11 +409,12 @@ impl TypeChecker {
         let aggregate = echo::classify_stmts(body);
         if !aggregate.admissible_in_reverse() {
             return Err(JtvError::EchoViolation(format!(
-                "reverse block has echo {aggregate}: it destroys information \
-                 and cannot be inverted. Reverse blocks may only contain \
-                 {} or {} statements (no total erasure).",
+                "reverse block has echo {aggregate}: it is not fully reversible. \
+                 Reverse blocks may only contain {} statements (bijective +/-); \
+                 lossy ({} / {}) operations are not invertible here.",
                 Echo::Safe,
-                Echo::Neutral
+                Echo::Neutral,
+                Echo::Breaking
             )));
         }
         Ok(())

jtv_proofs/JtvEcho.lean

@@ -18,9 +18,11 @@
   Lattice order:  `safe ⊑ neutral ⊑ breaking`  (join moves rightward, losing
   guarantees — mirroring the effect lattice `Total ⊑ Pure ⊑ Impure`).
 
-  The headline result for the type checker is `blockEcho_admissible`: a reverse
-  block is admissible iff *no* constituent statement is `breaking`. This is the
-  formal contract enforced by `crates/jtv-core/src/echo.rs`.
+  The headline result for the type checker is `blockEcho_admissible`: under the
+  **Safe-only** reversal policy, a reverse block is admissible iff *every*
+  constituent statement is `safe` (fully reversible). `neutral` (lossy but
+  residue-retaining) and `breaking` are both rejected. This is the formal
+  contract enforced by `crates/jtv-core/src/echo.rs`.
 
   Proofs are deliberately Mathlib-free (Lean core only) and discharge every
   goal by finite case analysis, matching the style of the other JtV proofs.
@@ -103,13 +105,16 @@ theorem le_breaking (a : Echo) : a ≤ Echo.breaking := by
 -- SECTION 2: REVERSE-BLOCK ADMISSIBILITY (the type-checker contract)
 -- ============================================================================
 
-/-- Boolean admissibility: an Echo may appear in a reverse block iff it does
-    not totally erase information (spec v2 §9 forbids `EchoBreaking`). -/
+/-- Boolean admissibility: an Echo may appear in a reverse block iff it is
+    `safe`. This is the **Safe-only** policy: a reverse block must be fully
+    reversible, so lossy `neutral` operations (whose Bennett-style residue
+    reversal is not yet implemented) are rejected alongside `breaking`. Spec v2
+    §9 permits `neutral` in principle; the checker is conservatively stricter. -/
 def Echo.admissible : Echo → Bool
-  | .breaking => false
-  | _         => true
+  | .safe => true
+  | _     => false
 
-theorem admissible_iff (e : Echo) : e.admissible = true ↔ e ≠ Echo.breaking := by
+theorem admissible_iff (e : Echo) : e.admissible = true ↔ e = Echo.safe := by
   cases e <;> simp [Echo.admissible]
 
 /-- **Key compositional law.** The echo of a composite operation `a ⊔ b` is
@@ -142,8 +147,8 @@ def allAdmissible : List Echo → Bool
   | e :: es => e.admissible && allAdmissible es
 
 /-- **Reverse-block soundness.** A block's aggregate echo is admissible iff
-    every statement in it is admissible — i.e. a reverse block is well-typed
-    exactly when it contains no `breaking` (information-destroying) statement.
+    every statement in it is admissible — i.e. (under the Safe-only policy) a
+    reverse block is well-typed exactly when every statement is `safe`.
 
     This is the property `echo::classify_stmts` / the reverse-block gate in
     `crates/jtv-core/src/echo.rs` must implement. -/

spec/jtv_v2_type_system_corrected.adoc

@@ -127,6 +127,12 @@ Allowed only if:
 - no EchoBreaking statements
 - no loops in V2
 
+Implementation note (2026-06-02): the checker enforces a *stricter, Safe-only*
+policy — every statement must be `EchoSafe`. `EchoNeutral` is permitted by this
+spec in principle (reversal via a retained residue, Bennett-style), but that
+runtime mechanism is unimplemented, so the checker conservatively rejects it.
+See `crates/jtv-core/src/echo.rs` and `jtv_proofs/JtvEcho.lean`.
+
 == 10. Soundness Theorem
 
 Theorem (Safe Fragment Termination):

verification/PROOF-CAPABILITY-MATRIX.adoc

@@ -70,7 +70,7 @@ induction. Corrected as part of the Phase-1 doc-truthing pass.
 | `string_not_executable` | JtvSecurity | `verified` | User strings are never code (injection impossibility).
 | `strong_normalization` | JtvExtended | `verified` | Data fragment strongly normalizing.
 | `confluence` | JtvExtended | `verified` | Data reduction confluent.
-| `blockEcho_admissible` | JtvEcho | `verified` | Reverse block admissible ⇔ no `Breaking` statement (the checker contract).
+| `blockEcho_admissible` | JtvEcho | `verified` | Reverse block admissible ⇔ every statement `Safe` (Safe-only policy; the checker contract).
 | `injective_fibre_subsingleton` | JtvEcho | `verified` | `EchoSafe` ⇔ injective ⇔ recoverable.
 | `residue_lossy` | JtvEcho | `verified` | Structured loss is genuine and one-way.
 | `parser_correctness` | — | `absent` | Parser produces a valid AST. (PROOF-1, High.)