From 246a2e2ed2fc41b1c87aa7faafb165e6ca13dca8 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 02:11:04 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat(JtvEcho):=20mechanise=20Echo=C3=97Epis?= =?UTF-8?q?temic=20function-effect=20lattice=20(ADR-0009)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds SECTION 5 to the Lean development: the formal counterpart of the Rust `epistemic.rs` + `effect.rs` slices that completed ADR-0009 D1-D3. * `Epistemic` inductive (hidden/bounded/full = Opaque/Partial/Transparent; the lowercase keywords are reserved in Lean, hence the rename) with `Epistemic.join` (full absorbing, hidden unit) and the lattice laws epi_join_comm / epi_join_assoc / epi_join_idem. * `FunctionEffect` structure — a point in the product lattice `Echo × Epistemic` — with componentwise `FunctionEffect.join` and the laws feffect_join_comm / feffect_join_assoc / feffect_join_idem proved from the Echo (SECTION 1) and Epistemic component laws. The three product laws are exactly what makes call-graph composition (`resolved_effects` in effect.rs) well-defined: the join fold is order- and repetition-independent, so `g ∘ f` carries `effect f ⊔ effect g` however the calls are arranged. `lake build` green; zero sorry/admit/axiom. Completes the (b) workstream (Echo + Epistemic first-class) on the proof side. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- jtv_proofs/JtvEcho.lean | 71 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/jtv_proofs/JtvEcho.lean b/jtv_proofs/JtvEcho.lean index 6958e4d..4015e73 100644 --- a/jtv_proofs/JtvEcho.lean +++ b/jtv_proofs/JtvEcho.lean @@ -312,4 +312,75 @@ theorem neg_injective : Injective (fun n : Int => -n) := by have h' : -a = -b := h omega +-- ============================================================================ +-- SECTION 5: FUNCTION EFFECTS — Echo × Epistemic (ADR-0009 D1+D3) +-- ============================================================================ + +/- + ADR-0009 lifts Echo to a first-class *function effect* and adds a parallel + *Epistemic* effect (what a function reveals about its inputs). The effect a + function carries is a point in the product lattice `Echo × Epistemic`, and + composition across calls is the (idempotent, commutative) join. This section + mechanises the Epistemic lattice and the product, mirroring the Echo lattice + of SECTION 1, and pins the lattice laws that make composition well-defined. + + Constructor names map to the Rust `epistemic.rs` / ADR-0009 D2 grades: + `hidden = Opaque`, `bounded = Partial`, `full = Transparent` + (lowercase `opaque` / `partial` are Lean keywords, hence the rename). +-/ + +/-- The epistemic grade (ADR-0009 D2): how much a function reveals about inputs. + `hidden ⊑ bounded ⊑ full` (= Opaque ⊑ Partial ⊑ Transparent). -/ +inductive Epistemic where + | hidden + | bounded + | full + deriving Repr, DecidableEq + +/-- Join (worst-case revelation): `full` absorbing, `hidden` the unit. -/ +def Epistemic.join : Epistemic → Epistemic → Epistemic + | .full, _ => .full + | _, .full => .full + | .bounded, _ => .bounded + | _, .bounded => .bounded + | .hidden, .hidden => .hidden + +theorem epi_join_comm (a b : Epistemic) : a.join b = b.join a := by + cases a <;> cases b <;> rfl + +theorem epi_join_assoc (a b c : Epistemic) : + (a.join b).join c = a.join (b.join c) := by + cases a <;> cases b <;> cases c <;> rfl + +theorem epi_join_idem (a : Epistemic) : a.join a = a := by + cases a <;> rfl + +/-- The function effect row (ADR-0009 D3): a point in `Echo × Epistemic`, + composed componentwise. -/ +structure FunctionEffect where + echo : Echo + epi : Epistemic + deriving Repr, DecidableEq + +/-- Componentwise join of two function effects. -/ +def FunctionEffect.join (x y : FunctionEffect) : FunctionEffect := + { echo := x.echo ⊔ y.echo, epi := x.epi.join y.epi } + +/-- **Composition is a commutative, idempotent join** (ADR-0009): the effect of + a composite is the join of its parts', and these three laws make that fold + independent of the order and repetition of calls — so `g ∘ f` carries + `effect f ⊔ effect g` however the calls are arranged. -/ +theorem feffect_join_comm (a b : FunctionEffect) : a.join b = b.join a := by + cases a; cases b + simp [FunctionEffect.join, join_comm, epi_join_comm] + +theorem feffect_join_assoc (a b c : FunctionEffect) : + (a.join b).join c = a.join (b.join c) := by + cases a; cases b; cases c + simp [FunctionEffect.join, join_assoc, epi_join_assoc] + +theorem feffect_join_idem (a : FunctionEffect) : a.join a = a := by + cases a + simp [FunctionEffect.join, join_idem, epi_join_idem] + end Jtv.Echo From 191acf24a96168b886df273f0cb6c2c7023bbfd2 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 02:18:06 +0000 Subject: [PATCH 2/3] feat(JtvEcho): stratify number systems by additive algebra (spec D6 groundwork) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds SECTION 6: the reversibility tier of `+` over a number system is not a per-system stipulation but is *forced* by the carrier's additive algebra. * `NumAlgebra` (abelianGroup / approxGroup / nonGroup) — one constructor per Echo tier; the algebra tower maps 1:1 onto the SECTION 1 Echo lattice, so three levels suffice (a finer Monoid ⊂ CancellativeMonoid ⊂ Group tower would collapse onto the same 3-valued codomain). * `NumSystem` (the seven addable JtvType carriers) + `NumSystem.algebra` + `NumAlgebra.echo` + `NumSystem.echo` — the stratification map. Headline theorems pin the two design facts: * `hex_binary_collapse` — hex/binary are *encodings of ℤ*, not new algebras, so they carry int's tier exactly (encoding ≠ algebra). * `exact_groups_safe` — int/rational/complex/symbolic are exact abelian groups, hence `safe`. * `float_not_safe` / `float_neutral` — IEEE-754 addition is non-associative, so its reversal is lossy; the stratification lifts float to `neutral`. This is the single place "addition-only ⇒ reversible" is qualified by the carrier (and does not threaten the abstract lattice laws — those grade, not compute). * `no_current_system_breaks` — `breaking` is presently empty, reserved for a future non-invertible (nonGroup) system. * `reversal_tier_by_algebra` — ties the tier back to the SECTION 1/2b reversal policies: `safe` ⇔ exact abelian group; non-`breaking` ⇔ not a nonGroup. This answers the design question "are number systems additive on proofs, or a rework, or stratified?" — they are *stratified*: the existing Int results become the ℤ (abelianGroup) instance, and each further carrier is classified by its additive algebra rather than reproving the spine. `lake build` green; zero sorry/admit/axiom. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- jtv_proofs/JtvEcho.lean | 110 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) diff --git a/jtv_proofs/JtvEcho.lean b/jtv_proofs/JtvEcho.lean index 4015e73..e3e7616 100644 --- a/jtv_proofs/JtvEcho.lean +++ b/jtv_proofs/JtvEcho.lean @@ -383,4 +383,114 @@ theorem feffect_join_idem (a : FunctionEffect) : a.join a = a := by cases a simp [FunctionEffect.join, join_idem, epi_join_idem] +-- ============================================================================ +-- SECTION 6: NUMBER-SYSTEM STRATIFICATION BY ADDITIVE ALGEBRA +-- ============================================================================ + +/- + The reversibility tier of `+` — and hence of `reverse { x += v }` — over a + given number system is NOT a per-system stipulation. It is *forced* by the + additive algebra of the carrier. This section stratifies JtV's numeric + systems by where they sit in the additive-algebra tower and reads off the + Echo tier mechanically. + + Additive-algebra tower (only the levels reversal can distinguish): + + abelianGroup associative + commutative + EXACT inverses + → reverse-add is total and exact → safe + approxGroup commutative with identity, but NON-associative + and inverses only approximate (rounding) + → reverse-add recoverable but lossy → neutral + nonGroup `+` not invertible at all (e.g. tropical + min-plus): no reverse exists → breaking + + This tower maps 1:1 onto the Echo lattice of SECTION 1 (safe/neutral/breaking) + — which is why three levels suffice: a finer carrier tower + (Monoid ⊂ CancellativeMonoid ⊂ Group) would collapse onto the same 3-valued + Echo codomain. + + Headline collapse: `hex` and `binary` are NOT distinct algebras — they are + *encodings of ℤ* (cf. the `JtvType` constructor comments "represented as + int"), so they share `int`'s `abelianGroup` instance. The seven surface + systems thus reduce to TWO inhabited algebra classes here; `nonGroup` is + reserved for future non-invertible systems (spec D6). + + Mirrors `crates/jtv-core/src/number.rs` (the runtime carriers) and the + numeric constructors of `Jtv.JtvType`. +-/ + +/-- The additive-algebra class of a carrier, at the granularity reversal cares + about. One constructor per Echo tier. -/ +inductive NumAlgebra where + | abelianGroup -- exact inverses; reverse-add total & exact + | approxGroup -- non-associative / rounding; reverse-add lossy + | nonGroup -- `+` not invertible; no reverse + deriving Repr, DecidableEq + +/-- JtV's addable number systems (the numeric constructors of `JtvType`). -/ +inductive NumSystem where + | int | rational | complex | symbolic | hex | binary | float + deriving Repr, DecidableEq + +/-- Where each system sits in the additive-algebra tower. `hex`/`binary` map to + the SAME class as `int` because they are encodings of ℤ, not new algebras. -/ +def NumSystem.algebra : NumSystem → NumAlgebra + | .int => .abelianGroup + | .rational => .abelianGroup + | .complex => .abelianGroup + | .symbolic => .abelianGroup + | .hex => .abelianGroup -- ℤ in hex clothing + | .binary => .abelianGroup -- ℤ in binary clothing + | .float => .approxGroup -- IEEE-754: non-associative, rounding + +/-- The Echo tier *forced* by an additive algebra. This is the stratification + law: the reversal tier is a function of the algebra, never a free choice. -/ +def NumAlgebra.echo : NumAlgebra → Echo + | .abelianGroup => .safe + | .approxGroup => .neutral + | .nonGroup => .breaking + +/-- A number system's reversal tier = the Echo of its additive algebra. -/ +def NumSystem.echo (s : NumSystem) : Echo := s.algebra.echo + +-- The stratification is total and the map is a genuine function of the algebra, +-- so every result below is closed by definitional reduction / finite decision. + +/-- **The hex/binary collapse**: the integer *encodings* carry int's tier + exactly — encoding is not algebra. -/ +theorem hex_binary_collapse : + NumSystem.echo .hex = NumSystem.echo .int + ∧ NumSystem.echo .binary = NumSystem.echo .int := ⟨rfl, rfl⟩ + +/-- The exact abelian groups are all `safe` (`+` is fully reversible). -/ +theorem exact_groups_safe : + NumSystem.echo .int = .safe + ∧ NumSystem.echo .rational = .safe + ∧ NumSystem.echo .complex = .safe + ∧ NumSystem.echo .symbolic = .safe := ⟨rfl, rfl, rfl, rfl⟩ + +/-- **Float is not `safe`.** IEEE-754 addition is non-associative, so its + reversal is lossy; the stratification lifts it to `neutral`. This is the one + place the surface "addition-only ⇒ reversible" slogan is *qualified* by the + carrier — and exactly why float's Echo grade sits above `safe`. -/ +theorem float_not_safe : NumSystem.echo .float ≠ .safe := by decide + +theorem float_neutral : NumSystem.echo .float = .neutral := rfl + +/-- **No current system is `breaking`.** Every inhabited carrier is at least an + approximate group, so the `breaking` tier is presently empty — it is held in + reserve for a future non-invertible (`nonGroup`) system. -/ +theorem no_current_system_breaks (s : NumSystem) : NumSystem.echo s ≠ .breaking := by + cases s <;> decide + +/-- **Stratification meets the reversal policies.** Reading the algebra off the + carrier decides admissibility under both policies of SECTION 1/2b: + `safe` (Safe-only reversal) holds iff the carrier is an exact abelian group; + non-`breaking` (the `reversible { } -> tok` token policy, which also admits + `neutral`) holds iff the carrier is not a `nonGroup`. -/ +theorem reversal_tier_by_algebra (s : NumSystem) : + (NumSystem.echo s = .safe ↔ s.algebra = .abelianGroup) + ∧ (NumSystem.echo s ≠ .breaking ↔ s.algebra ≠ .nonGroup) := by + cases s <;> decide + end Jtv.Echo From 254561b40048ae5333f0d5c91e62a97b08e2123f Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 06:04:29 +0000 Subject: [PATCH 3/3] feat(echo): carrier-aware Echo classification (float += -> Neutral) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Makes Echo classification consult the carrier's number system, not just the statement shape — the first compiler-side step of "Echo as a real typesystem feature". Operational counterpart of JtvEcho.lean SECTION 6. echo.rs: * NumAlgebra / additive_algebra / carrier_echo — the Rust mirror of the Lean stratification (AbelianGroup -> Safe, ApproxGroup -> Neutral, NonGroup -> Breaking; hex/binary share int's class as Z-encodings; Bool/String have no additive algebra). * CarrierEnv (var -> BasicType) threaded through env-aware classifiers (classify_*_in_env, function_echo_in_env). A reversible `+=` now joins its statement shape (self-ref -> Neutral) with its carrier echo, so `x += v` over a float grades Neutral even without self-reference. * Shape-only wrappers (classify_stmts, function_echo, ...) preserved: an empty env defaults every carrier to Int (Safe), so existing behaviour and the other callers are unchanged. effect.rs: * own_effect now seeds a CarrierEnv from the function's parameter type annotations, so `fn f(x: float) { reverse { x += y } }` resolves to echo Neutral end-to-end through resolved_effects. Default-carrier soundness: a variable absent from the env is treated as Int (Safe), not "unknown-lossy" — JtV numeric literals default to int (inferType (lit _) = int in Lean), so the only lossy carrier (float) is exactly the one that must be annotated/inferred to exist. Fuller inferred-local-type envs are a later slice. No unwrap/unwrap_or (avoids Hypatia dangerous-default). cargo fmt + clippy clean; 122 lib tests pass incl. 4 new carrier-aware cases. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- crates/jtv-core/src/echo.rs | 231 ++++++++++++++++++++++++++-------- crates/jtv-core/src/effect.rs | 63 +++++++++- 2 files changed, 243 insertions(+), 51 deletions(-) diff --git a/crates/jtv-core/src/echo.rs b/crates/jtv-core/src/echo.rs index 7ae445e..c888e7a 100644 --- a/crates/jtv-core/src/echo.rs +++ b/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 { + 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; + +/// 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); + } } diff --git a/crates/jtv-core/src/effect.rs b/crates/jtv-core/src/effect.rs index 5c81ebd..b474af3 100644 --- a/crates/jtv-core/src/effect.rs +++ b/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, ¶m_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); + } }