feat(echo): function-effect lattice, number-system stratification, and carrier-aware classification

crates/jtv-core/src/echo.rs

@@ -29,6 +29,7 @@
 // typing — it lives alongside `Purity`, not inside `Type`.
 
 use crate::ast::*;
+use std::collections::HashMap;
 
 /// The three loss classes of the Echo taxonomy.
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
@@ -98,6 +99,68 @@ impl std::fmt::Display for Echo {
     }
 }
 
+// ============================================================================
+// CARRIER STRATIFICATION (mirror of `JtvEcho.lean` SECTION 6)
+// ============================================================================
+
+/// The additive-algebra class of a carrier — the Rust mirror of `NumAlgebra`
+/// in `jtv_proofs/JtvEcho.lean` (SECTION 6). The reversal tier of `+` over a
+/// number system is *forced* by this class, not stipulated per system.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum NumAlgebra {
+    /// Exact inverses (ℤ, ℚ, ℂ, symbolic, and the ℤ-encodings hex/binary):
+    /// reverse-add is total and exact.
+    AbelianGroup,
+    /// Non-associative / rounding (IEEE-754 float): reverse-add is lossy.
+    ApproxGroup,
+    /// `+` not invertible (reserved for a future tropical / min-plus system):
+    /// no reverse exists.
+    NonGroup,
+}
+
+/// Where a carrier sits in the additive-algebra tower. `Hex`/`Binary` share
+/// `Int`'s class because they are *encodings of ℤ*, not new algebras
+/// (`hex_binary_collapse` in Lean). Non-numeric carriers (`Bool`/`String`)
+/// have no additive algebra — they cannot be `+=` targets in well-typed code.
+pub fn additive_algebra(ty: &BasicType) -> Option<NumAlgebra> {
+    use BasicType::*;
+    match ty {
+        Int | Hex | Binary | Rational | Complex | Symbolic => Some(NumAlgebra::AbelianGroup),
+        Float => Some(NumAlgebra::ApproxGroup),
+        Bool | String => None,
+    }
+}
+
+/// The Echo tier *forced* by a carrier's additive algebra — the operational
+/// counterpart of `NumSystem.echo` ∘ `NumAlgebra.echo` in Lean SECTION 6:
+/// `AbelianGroup → Safe`, `ApproxGroup → Neutral`, `NonGroup → Breaking`. A
+/// non-numeric carrier induces no additive-reversal obligation, hence `Safe`.
+pub fn carrier_echo(ty: &BasicType) -> Echo {
+    match additive_algebra(ty) {
+        Some(NumAlgebra::AbelianGroup) | None => Echo::Safe,
+        Some(NumAlgebra::ApproxGroup) => Echo::Neutral,
+        Some(NumAlgebra::NonGroup) => Echo::Breaking,
+    }
+}
+
+/// A carrier environment: the declared number system of in-scope variables,
+/// built from type annotations (function params today; inferred local types in
+/// a later slice). Threaded into Echo classification so that `+=` over a lossy
+/// carrier (e.g. float) is graded by the carrier, not just the statement shape.
+pub type CarrierEnv = HashMap<String, BasicType>;
+
+/// The carrier echo of a variable. A variable absent from the env is treated as
+/// JtV's default numeric carrier `Int` (an exact abelian group → `Safe`): JtV
+/// numeric literals default to `int` (cf. `inferType (lit _) = int` in Lean), so
+/// an unannotated numeric *is* `int`. The default is therefore sound — only an
+/// explicitly-`float` carrier (recorded in the env) lifts a `+=` to `Neutral`.
+fn carrier_echo_of(env: &CarrierEnv, var: &str) -> Echo {
+    match env.get(var) {
+        Some(ty) => carrier_echo(ty),
+        None => Echo::Safe,
+    }
+}
+
 /// Does `expr` reference variable `var`? Self-reference in a reversible
 /// assignment destroys the original value (e.g. `x += x` cannot be inverted),
 /// which is exactly a `Breaking` echo.
@@ -114,101 +177,116 @@ fn data_expr_uses(expr: &DataExpr, var: &str) -> bool {
     }
 }
 
-/// Classify the echo of a single reversible statement.
-pub fn classify_reversible_stmt(stmt: &ReversibleStmt) -> Echo {
+/// Classify the echo of a single reversible statement under a carrier env.
+///
+/// Two independent sources of loss are joined:
+///   1. statement *shape* — self-reference (`x += x`) destroys the original
+///      value, recoverable only from a retained residue/token (`Neutral`);
+///   2. the *carrier* — over a non-group / approximate number system (e.g.
+///      `float`) reverse-add is itself lossy, so the carrier lifts the grade
+///      regardless of shape (`carrier_echo`, mirroring Lean SECTION 6).
+pub fn classify_reversible_stmt_in_env(stmt: &ReversibleStmt, env: &CarrierEnv) -> Echo {
     match stmt {
-        // `x += e` / `x -= e` is reversible (Safe) unless the target appears
-        // 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) {
-                // 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`.
+            // Shape: self-reference is `Neutral` (token-recoverable, Bennett),
+            // never `Breaking` — in the addition-only group every overwrite can
+            // be tokenised. Formal basis: `rev_forward_backward_with_token` /
+            // `rev_backward_naive_fails_self_ref` in `JtvTheorems`.
+            let shape = if data_expr_uses(expr, target) {
                 Echo::Neutral
             } else {
                 Echo::Safe
-            }
+            };
+            // Carrier: a lossy number system (float) grades the reverse-add up.
+            shape.join(carrier_echo_of(env, target))
         }
         // A reversible `if` is as lossy as its lossiest branch. The Data guard
         // is pure (Safe); branches are classified conservatively.
         ReversibleStmt::If(if_stmt) => {
-            let then_echo = classify_control_stmts(&if_stmt.then_branch);
-            let else_echo = if_stmt
-                .else_branch
-                .as_ref()
-                .map(|b| classify_control_stmts(b))
-                .unwrap_or(Echo::Safe);
+            let then_echo = classify_control_stmts_in_env(&if_stmt.then_branch, env);
+            let else_echo = match &if_stmt.else_branch {
+                Some(b) => classify_control_stmts_in_env(b, env),
+                None => Echo::Safe,
+            };
             then_echo.join(else_echo)
         }
     }
 }
 
-/// Aggregate echo of a list of reversible statements: the join of their
-/// echoes (starting from `Safe`). Matches `blockEcho` in `JtvEcho.lean`.
-pub fn classify_stmts(stmts: &[ReversibleStmt]) -> Echo {
+/// Aggregate echo of reversible statements under a carrier env: the join of
+/// their echoes (from `Safe`). Matches `blockEcho` in `JtvEcho.lean`.
+pub fn classify_stmts_in_env(stmts: &[ReversibleStmt], env: &CarrierEnv) -> Echo {
     stmts
         .iter()
-        .map(classify_reversible_stmt)
+        .map(|s| classify_reversible_stmt_in_env(s, env))
         .fold(Echo::Safe, Echo::join)
 }
 
-/// Classify control statements appearing inside a reversible `if` branch.
-/// Plain assignments are reversible (Safe); nested reverse blocks recurse;
-/// anything else is treated conservatively as `Neutral` (structured loss we
-/// cannot yet prove reversible).
-fn classify_control_stmts(stmts: &[ControlStmt]) -> Echo {
+/// Classify control statements inside a reversible `if` branch under a carrier
+/// env. Plain assignments are reversible (Safe); nested reverse blocks recurse
+/// (carrying the env on so their `+=` carriers are seen); anything else is
+/// treated conservatively as `Neutral`.
+fn classify_control_stmts_in_env(stmts: &[ControlStmt], env: &CarrierEnv) -> Echo {
     stmts
         .iter()
         .map(|s| match s {
             ControlStmt::Assignment(_) => Echo::Safe,
-            ControlStmt::ReverseBlock(b) => classify_stmts(&b.body),
+            ControlStmt::ReverseBlock(b) => classify_stmts_in_env(&b.body, env),
             _ => Echo::Neutral,
         })
         .fold(Echo::Safe, Echo::join)
 }
 
+/// Shape-only classification of a single reversible statement (no carrier
+/// context): every carrier is treated as JtV's default `Int` (Safe). Equivalent
+/// to `classify_reversible_stmt_in_env` with an empty env; retained for
+/// classifying isolated snippets without a type environment.
+pub fn classify_reversible_stmt(stmt: &ReversibleStmt) -> Echo {
+    classify_reversible_stmt_in_env(stmt, &CarrierEnv::new())
+}
+
+/// Shape-only aggregate echo of reversible statements (empty carrier env).
+pub fn classify_stmts(stmts: &[ReversibleStmt]) -> Echo {
+    classify_stmts_in_env(stmts, &CarrierEnv::new())
+}
+
 // ============================================================================
 // SECTION 4: ECHO AS A FUNCTION EFFECT (ADR-0009 D1, slice 1)
 // ============================================================================
 
 /// The Echo grade a *function body* induces (ADR-0009 D1) — the inference half
-/// of Echo-as-a-first-class-function-effect. It is the join of the echoes of the
-/// body's statements: addition-only data assignments are `Safe` (no loss);
-/// `reverse` / `reversible` blocks contribute their block echo
-/// (`classify_stmts`); control flow joins its sub-bodies. Lifts the block-level
-/// `classify_stmts` to a whole function body.
+/// of Echo-as-a-first-class-function-effect — under a carrier env. It is the
+/// join of the echoes of the body's statements: addition-only data assignments
+/// are `Safe` (no loss); `reverse` / `reversible` blocks contribute their block
+/// echo (`classify_stmts_in_env`, so float-carrier `+=` grades `Neutral`);
+/// control flow joins its sub-bodies.
 ///
-/// Slice 1 computes a function's *own* body grade; resolving the grade of
-/// `FunctionCall`s (joining the callee's grade into the caller's) is a later
-/// slice that needs a function-echo environment.
-pub fn function_echo(body: &[ControlStmt]) -> Echo {
+/// Computes a function's *own* body grade; resolving the grade of
+/// `FunctionCall`s (joining the callee's into the caller's) is `resolved_effects`
+/// in `effect.rs`.
+pub fn function_echo_in_env(body: &[ControlStmt], env: &CarrierEnv) -> Echo {
     body.iter()
-        .map(control_stmt_echo)
+        .map(|s| control_stmt_echo_in_env(s, env))
         .fold(Echo::Safe, Echo::join)
 }
 
-fn control_stmt_echo(s: &ControlStmt) -> Echo {
+fn control_stmt_echo_in_env(s: &ControlStmt, env: &CarrierEnv) -> Echo {
     match s {
         // Addition-only data assignment: no loss.
         ControlStmt::Assignment(_) => Echo::Safe,
         ControlStmt::If(i) => {
-            let then_echo = function_echo(&i.then_branch);
+            let then_echo = function_echo_in_env(&i.then_branch, env);
             match &i.else_branch {
-                Some(b) => then_echo.join(function_echo(b)),
+                Some(b) => then_echo.join(function_echo_in_env(b, env)),
                 None => then_echo,
             }
         }
-        ControlStmt::While(w) => function_echo(&w.body),
-        ControlStmt::For(f) => function_echo(&f.body),
-        // Reverse / reversible blocks carry their own block echo.
-        ControlStmt::ReverseBlock(b) => classify_stmts(&b.body),
-        ControlStmt::ReversibleBlock(b) => classify_stmts(&b.body),
-        ControlStmt::Block(ss) => function_echo(ss),
+        ControlStmt::While(w) => function_echo_in_env(&w.body, env),
+        ControlStmt::For(f) => function_echo_in_env(&f.body, env),
+        // Reverse / reversible blocks carry their own block echo (carrier-aware).
+        ControlStmt::ReverseBlock(b) => classify_stmts_in_env(&b.body, env),
+        ControlStmt::ReversibleBlock(b) => classify_stmts_in_env(&b.body, env),
+        ControlStmt::Block(ss) => function_echo_in_env(ss, env),
         // Reading, printing, and token consumption induce no data loss here.
         ControlStmt::Return(_)
         | ControlStmt::Print(_)
@@ -217,6 +295,12 @@ fn control_stmt_echo(s: &ControlStmt) -> Echo {
     }
 }
 
+/// Shape-only function-body echo (no carrier context): every carrier defaults to
+/// JtV's `Int` (Safe). Equivalent to `function_echo_in_env` with an empty env.
+pub fn function_echo(body: &[ControlStmt]) -> Echo {
+    function_echo_in_env(body, &CarrierEnv::new())
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -333,4 +417,53 @@ mod tests {
         assert_eq!(classify_stmts(std::slice::from_ref(&safe)), Echo::Safe);
         assert_eq!(classify_stmts(&[safe.clone(), neutral]), Echo::Neutral);
     }
+
+    #[test]
+    fn carrier_echo_mirrors_section6() {
+        use BasicType::*;
+        // Exact abelian groups (incl. the ℤ-encodings hex/binary) are Safe.
+        for t in [Int, Hex, Binary, Rational, Complex, Symbolic] {
+            assert_eq!(carrier_echo(&t), Echo::Safe);
+        }
+        // Float is the one approx-group carrier -> Neutral.
+        assert_eq!(carrier_echo(&Float), Echo::Neutral);
+        // hex/binary collapse onto int's tier exactly (encoding != algebra).
+        assert_eq!(carrier_echo(&Hex), carrier_echo(&Int));
+        assert_eq!(carrier_echo(&Binary), carrier_echo(&Int));
+        // Non-numeric carriers have no additive algebra.
+        assert_eq!(additive_algebra(&Bool), None);
+        assert_eq!(additive_algebra(&BasicType::String), None);
+    }
+
+    #[test]
+    fn float_add_assign_is_neutral_via_carrier() {
+        // x += y  (y independent of x): Safe over int, Neutral over float.
+        let stmt =
+            ReversibleStmt::AddAssign("x".to_string(), DataExpr::Identifier("y".to_string()));
+        // No carrier context -> default int -> Safe (backward compatible).
+        assert_eq!(classify_reversible_stmt(&stmt), Echo::Safe);
+        let float_env = CarrierEnv::from([("x".to_string(), BasicType::Float)]);
+        assert_eq!(
+            classify_reversible_stmt_in_env(&stmt, &float_env),
+            Echo::Neutral
+        );
+        let int_env = CarrierEnv::from([("x".to_string(), BasicType::Int)]);
+        assert_eq!(classify_reversible_stmt_in_env(&stmt, &int_env), Echo::Safe);
+    }
+
+    #[test]
+    fn float_carrier_lifts_block_and_function() {
+        // reverse { x += y } over a float x  ->  Neutral (carrier), though the
+        // statement shape alone (no self-ref) would be Safe.
+        let body = vec![ControlStmt::ReverseBlock(ReverseBlock {
+            body: vec![ReversibleStmt::AddAssign(
+                "x".to_string(),
+                DataExpr::Identifier("y".to_string()),
+            )],
+        })];
+        let float_env = CarrierEnv::from([("x".to_string(), BasicType::Float)]);
+        assert_eq!(function_echo_in_env(&body, &float_env), Echo::Neutral);
+        // Without carrier context, default int -> Safe.
+        assert_eq!(function_echo(&body), Echo::Safe);
+    }
 }

crates/jtv-core/src/effect.rs

@@ -12,7 +12,7 @@
 // is a later slice.
 
 use crate::ast::*;
-use crate::echo::{function_echo, Echo};
+use crate::echo::{function_echo_in_env, CarrierEnv, Echo};
 use crate::epistemic::{function_epistemic, Epistemic};
 use std::collections::HashMap;
 
@@ -41,13 +41,31 @@ impl FunctionEffect {
 }
 
 /// A function's OWN effect, from its body alone (not yet its callees').
+///
+/// The Echo half is *carrier-aware*: parameters with a numeric type annotation
+/// seed a `CarrierEnv`, so a `reverse { x += v }` over a `float` parameter grades
+/// `Neutral` (lossy reverse-add) rather than `Safe`. See `echo::carrier_echo` and
+/// `JtvEcho.lean` SECTION 6.
 pub fn own_effect(func: &FunctionDecl) -> FunctionEffect {
     FunctionEffect {
-        echo: function_echo(&func.body),
+        echo: function_echo_in_env(&func.body, &param_carrier_env(func)),
         epi: function_epistemic(func),
     }
 }
 
+/// Seed a carrier environment from a function's parameter type annotations.
+/// Locals without annotations default to JtV's `Int` carrier (`Safe`); a fuller
+/// inferred-type env is a later slice.
+fn param_carrier_env(func: &FunctionDecl) -> CarrierEnv {
+    func.params
+        .iter()
+        .filter_map(|p| match &p.type_annotation {
+            Some(TypeAnnotation::Basic(bt)) => Some((p.name.clone(), bt.clone())),
+            _ => None,
+        })
+        .collect()
+}
+
 /// Resolve every function's full effect, joining in the effects of the functions
 /// it calls (transitively). ADR-0009 D1+D3: composition is join across the call
 /// graph. The effect lattice is finite and join is monotone, so the fixpoint
@@ -346,4 +364,45 @@ mod tests {
         let env = resolved_effects(&prog);
         assert_eq!(env["f"], FunctionEffect::SAFE);
     }
+
+    #[test]
+    fn float_param_reverse_block_resolves_neutral() {
+        // fn f(x: float) { reverse { x += y } }
+        // Carrier-aware own effect: the float carrier makes the reverse-add
+        // Neutral, even though `x += y` has no self-reference.
+        let mut f = func(
+            "f",
+            vec!["x"],
+            vec![ControlStmt::ReverseBlock(ReverseBlock {
+                body: vec![ReversibleStmt::AddAssign(
+                    "x".to_string(),
+                    DataExpr::Identifier("y".to_string()),
+                )],
+            })],
+        );
+        f.params[0].type_annotation = Some(TypeAnnotation::Basic(BasicType::Float));
+        let prog = Program {
+            statements: vec![TopLevel::Function(f)],
+        };
+        let env = resolved_effects(&prog);
+        assert_eq!(env["f"].echo, Echo::Neutral);
+
+        // The same body with an int parameter stays Safe.
+        let mut g = func(
+            "g",
+            vec!["x"],
+            vec![ControlStmt::ReverseBlock(ReverseBlock {
+                body: vec![ReversibleStmt::AddAssign(
+                    "x".to_string(),
+                    DataExpr::Identifier("y".to_string()),
+                )],
+            })],
+        );
+        g.params[0].type_annotation = Some(TypeAnnotation::Basic(BasicType::Int));
+        let prog2 = Program {
+            statements: vec![TopLevel::Function(g)],
+        };
+        let env2 = resolved_effects(&prog2);
+        assert_eq!(env2["g"].echo, Echo::Safe);
+    }
 }