feat(echo): surface @echo(...) function-grade annotation + upper-bound check (ADR-0009 D1)

Surfaces the Echo grade in the function arrow per ADR-0009 D1 -- the
"Echo as a first-class function effect" surface slice (the proof + effect-
composition halves already landed).

Design (Bundle A): parameterised syntax + upper-bound policy.

- Syntax: `@echo(Safe|Neutral|Breaking)` before `fn`, order-independent with
  `@pure`/`@total` (grammar `echo_marker`; parser consumes leading markers in a
  loop). One directive carrying the grade -- scales to a later `@epi(...)`.
- AST: `FunctionDecl.echo_annotation: Option<Echo>`. The `Echo` enum moves from
  `echo.rs` to `ast.rs` (so the AST can hold it without the `ast` <-> `echo`
  cycle) and is re-exported `pub use crate::ast::Echo` from `echo.rs`, so every
  `echo::Echo` site is unchanged.
- Check (upper bound): `typechecker::check_echo_annotations` verifies
  `inferred <= annotated` against the carrier-aware, call-graph-composed
  `effect::resolved_effects`. A function may declare MORE loss than it incurs,
  never less; callers can be checked against a callee's declared ceiling
  (modular). The reverse-block gate still uses the ACTUAL inferred grade, so the
  annotation cannot loosen reversal soundness.
- Round-trip: `pretty.rs` + `formatter.rs` emit `@echo(...)` after purity.

6 tests (parse + either-order, upper-bound accept/reject/absent, round-trip);
133 lib tests, cargo fmt + clippy clean.

Remaining (noted in effect.rs + STATE): the grade in `TypeAnnotation::Function`
(function-valued params) and the parallel `@epi(...)` surface.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -7,7 +7,7 @@ project = "jtv"
 version = "0.0.1"
 last-updated = "2026-06-18"
 status = "active"
-session = "2026-06-18 — Echo arc completed + number systems stratified. (b) Echo+Epistemic first-class DONE (proof side, ADR-0009): JtvEcho.lean SECTION 5 = Epistemic lattice + Echo×Epistemic product FunctionEffect lattice + comm/assoc/idem composition laws (matching the already-merged echo.rs/epistemic.rs/effect.rs). Number systems STRATIFIED (ADR-0007 D6 realized as ADR-0010): JtvEcho.lean SECTION 6 3-level NumAlgebra tower 1:1 with the Echo lattice (hex/binary=ℤ-encodings collapse to int's tier; float=approxGroup→Neutral); echo.rs carrier-aware classification (CarrierEnv; reversible += graded shape⊔carrier; default-carrier=Int sound) + effect.rs param-seeded env; number.rs runtime-value bridge Value::reversal_echo. PR #44 + #45 (bridge+ADR-0010) merged; float-LOCALS soundness gate also LANDED (typechecker.rs check_echo_admissible{,_with_residue} seed CarrierEnv from the inferred env self.env → reverse{} over a float local correctly rejected, float routes to reversible{}->tok). lake + cargo green (127 lib tests, 0 sorry/unwrap). NEXT rung: value-level semantics beyond τ=int (gap-005)"
+session = "2026-06-18 — Surface Echo grades (ADR-0009 D1) + repo rename julia-the-viper→jtv. SURFACE ECHO: @echo(Safe|Neutral|Breaking) annotation on functions (grammar echo_marker + parser loop, order-independent with @pure); FunctionDecl.echo_annotation — the Echo enum moved ast.rs with an echo.rs `pub use` re-export to break the ast↔echo cycle; upper-bound check typechecker.rs check_echo_annotations (inferred ⊑ annotated, against the carrier-aware call-graph-composed effect.rs resolved_effects); pretty.rs + formatter.rs emit @echo (round-trip). 133 lib tests, fmt/clippy green. RENAME: full julia-the-viper→jtv slug + Julia the Viper→JtV prose across the repo (PR #47 merged) + nextgen-languages catalogue (#87 merged, rebuilt after main dropped all submodules); etymology kept as a README/CLAUDE footnote; the GitHub Settings repo-rename is the user's remaining manual step. NEXT rung: grade in TypeAnnotation::Function (function-valued params) + @epi(...) surface; value-level semantics beyond τ=int (gap-005)"
 
 [project-context]
 name = "JtV"
@@ -59,7 +59,7 @@ 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 stratification (ADR-0007 D6 / ADR-0010) — LANDED 2026-06-18: per-system additive-algebra → Echo-tier classification at proof level (JtvEcho.lean SECTION 6), type level (echo.rs carrier_echo + CarrierEnv carrier-aware += grading, effect.rs param-seeded env), value level (number.rs Value::reversal_echo), and the carrier-aware TYPECHECKER GATE (typechecker.rs check_echo_admissible{,_with_residue} seed CarrierEnv from the inferred env self.env → reverse{} over a float LOCAL correctly rejected; float routes to reversible{}->tok). STILL OPEN: lift type_preservation semantics beyond τ=int (gap-005); carrier-awareness inside reversible-if branches (rare corner); keep addition-only (×/÷ generated)",
   "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)') — LANDED 2026-06-18 (ADR-0009): echo.rs function_echo + epistemic.rs function_epistemic + effect.rs FunctionEffect row + resolved_effects call-graph fixpoint; JtvEcho.lean SECTION 5 mechanises the Echo×Epistemic product lattice + comm/assoc/idem composition laws",
+  "Echo as first-class function effect ('(b)') — LANDED 2026-06-18 (ADR-0009): echo.rs function_echo + epistemic.rs function_epistemic + effect.rs FunctionEffect row + resolved_effects call-graph fixpoint; JtvEcho.lean SECTION 5 mechanises the Echo×Epistemic product lattice + comm/assoc/idem composition laws. SURFACE side LANDED 2026-06-18: @echo(Safe|Neutral|Breaking) annotation on FunctionDecl (grammar echo_marker + parser, order-independent with @pure; Echo enum moved to ast.rs + echo.rs re-export to break the cycle) + upper-bound check typechecker.rs check_echo_annotations (inferred ⊑ annotated, via resolved_effects) + pretty/formatter @echo round-trip. REMAINING: grade in TypeAnnotation::Function (function-valued params) + @epi(...) surface",
   "Verification bridge: correlation tests between Lean semantics and Rust interpreter",
   "PataCL Phase 1 → unblocks JtV coproc implementation Phase 2"
 ]
@@ -88,7 +88,8 @@ sessions = [
   { date = "2026-06-17", subject = "License + hardening + ADR-0008. License (gap-006 RESOLVED, PR #36 merged): full per-file SPDX = MPL-2.0 (code) + CC-BY-SA-4.0 (docs); 190 MPL + 77 CC-BY-SA headers; PALIMPSEST.adoc retired; LICENSING.md rewritten; stray MIT/GPL/PMPL/or-later normalised. (PR #34 security clean + #35 v2-c bridge also merged earlier.) Workflow hardening (PR #37 merged): curl|sh installers (proof-regression elan, setup.sh just) -> download-then-run; rsr_check.rs unsafe_block self-trip cleared. Deferred (need hyperpolymath/standards reusable, out of session MCP scope): secret-scanner.yml, scorecard.yml job-perms. ADR-0008 (this commit): neg -> reverse-only; purist/adulterated dialect via feature-gated sugar + discouragement lint + purity certificate (resolves ADR-0007 D2); implementation is follow-on." },
   { date = "2026-06-18", subject = "neg-dialect impl slice 1 + ADR-0009. PR #39 merged: jtv-core dialect.rs purity certificate (ADR-0008 D4) -- read-only AST scan stamping a program purist-jtv vs adulterated-jtv by counting expression-level neg sugar; reverse-block subtraction stays purist; 5 tests; cleared a self-introduced Hypatia unwrap_dangerous_default critical via Option::iter().sum(). ADR-0009 (this commit): Echo + Epistemic as first-class GRADED FUNCTION EFFECTS -- Echo grade {Safe<=Neutral<=Breaking} carried in the arrow, composing by the existing join; Epistemic = knowledge/observability axis {Opaque<=Partial<=Transparent} as a parallel graded effect (dual to Echo: loss vs revelation); product-lattice effect row; orthogonal to Purity + the dialect certificate. Implementation slice-wise (Echo-effect first). Still parked: (b) impl, number-system semantics, license wave-2, standards-blocked hardening (secret-scanner/scorecard)." },
   { date = "2026-06-18", subject = "Echo arc completed + number-system stratification (PR #44 merged via rebase → main: SECTION 5+6 + carrier-aware echo; then bridge+ADR-0010 PR). (b) Echo+Epistemic first-class DONE on the proof side: JtvEcho.lean SECTION 5 = Epistemic lattice (hidden/bounded/full) + Echo×Epistemic product FunctionEffect lattice + comm/assoc/idem composition laws (mirrors the already-merged echo.rs/epistemic.rs/effect.rs). Number systems STRATIFIED (ADR-0007 D6 realized as ADR-0010): JtvEcho.lean SECTION 6 = 3-level NumAlgebra tower (abelianGroup/approxGroup/nonGroup) 1:1 with the Echo lattice; theorems hex_binary_collapse (hex/binary are ℤ-encodings, share int's tier) / exact_groups_safe / float_not_safe (IEEE-754 non-associative → approxGroup → Neutral) / no_current_system_breaks / reversal_tier_by_algebra. echo.rs made carrier-aware: NumAlgebra/additive_algebra/carrier_echo + CarrierEnv threaded through classify_*_in_env/function_echo_in_env; a reversible += is graded shape⊔carrier (float += → Neutral); shape-only wrappers preserve prior behaviour (empty env ⇒ Int=Safe); default-carrier=Int is sound (literals default to int). effect.rs own_effect seeds the env from param annotations. number.rs runtime-value bridge Value::number_system + Value::reversal_echo (delegates to carrier_echo — single source of truth). ADR-0010 reconciles with ADR-0007 D6 (float is approxGroup not D6-cancellative; D6's cancellative/idempotent Neutral/Breaking routes anticipated-but-uninhabited). lake + cargo fmt/clippy/test green (124 lib tests), 0 sorry/admit/axiom, no unwrap/unwrap_or. OPEN: float-LOCALS soundness slice (locals carry no annotation → thread typechecker inferred types into CarrierEnv, else a reverse{} over a float local is wrongly Safe-admitted); value-level type_preservation beyond τ=int (gap-005)." },
-  { date = "2026-06-18", subject = "Float-locals soundness slice (typechecker carrier-aware gate). Echo admissibility is checked at the reverse-block site inside check_control_stmt, where self.env already holds the INFERRED types of params + prior local assignments — so typechecker.rs check_echo_admissible{,_with_residue} now build a CarrierEnv from self.env (Type→BasicType for the 7 numeric Types; non-numeric/Any omitted → default Int=Safe) and call echo::classify_stmts_in_env. Effect: a reverse{} over a float LOCAL (typed only by inference, e.g. x = 2.5) is correctly REJECTED under Safe-only (was wrongly Safe-admitted); reversible{}->tok still admits it (token retains the rounding residue). Contained change (no reordering, no new inference pass). 4 typechecker tests (float carrier rejected; inferred-float-local rejected end-to-end; int contrast ok; float reversible-tok admitted). ADR-0010 §Status/§Consequences/§Open updated (slice landed; remaining minor corner = carrier-awareness inside reversible-if branches). cargo fmt/clippy/test green (127 lib tests; cleared a clippy approx_constant deny on a 3.14 literal → 2.5). Whole-suite check: no existing test/example relied on a float reverse{} being accepted, so the stricter rule broke nothing." }
+  { date = "2026-06-18", subject = "Float-locals soundness slice (typechecker carrier-aware gate). Echo admissibility is checked at the reverse-block site inside check_control_stmt, where self.env already holds the INFERRED types of params + prior local assignments — so typechecker.rs check_echo_admissible{,_with_residue} now build a CarrierEnv from self.env (Type→BasicType for the 7 numeric Types; non-numeric/Any omitted → default Int=Safe) and call echo::classify_stmts_in_env. Effect: a reverse{} over a float LOCAL (typed only by inference, e.g. x = 2.5) is correctly REJECTED under Safe-only (was wrongly Safe-admitted); reversible{}->tok still admits it (token retains the rounding residue). Contained change (no reordering, no new inference pass). 4 typechecker tests (float carrier rejected; inferred-float-local rejected end-to-end; int contrast ok; float reversible-tok admitted). ADR-0010 §Status/§Consequences/§Open updated (slice landed; remaining minor corner = carrier-awareness inside reversible-if branches). cargo fmt/clippy/test green (127 lib tests; cleared a clippy approx_constant deny on a 3.14 literal → 2.5). Whole-suite check: no existing test/example relied on a float reverse{} being accepted, so the stricter rule broke nothing." },
+  { date = "2026-06-18", subject = "Surface Echo grades (ADR-0009 D1) — Bundle A (parameterised syntax + upper-bound policy). @echo(Safe|Neutral|Breaking) annotation on functions: grammar.pest echo_marker = '@echo' '(' echo_grade ')' and function_decl markers now (purity_marker|echo_marker)*; parser.rs consumes leading markers in a loop (order-independent with @pure) → FunctionDecl.echo_annotation. The Echo enum moved echo.rs→ast.rs (gains Serialize) with a `pub use crate::ast::Echo` re-export in echo.rs to break the ast↔echo cycle so FunctionDecl can hold it; all `echo::Echo` sites unchanged. UPPER-BOUND check typechecker.rs check_echo_annotations (3rd pass of check_program): inferred ⊑ annotated against the carrier-aware call-graph-composed effect.rs resolved_effects — a function may declare MORE loss than it incurs, never less (modular: caller checks against callee's declared ceiling). The reverse-gate still uses the ACTUAL inferred grade, so an annotation can't loosen reversal soundness. pretty.rs + formatter.rs emit @echo after purity (round-trip fidelity, pinned by a pretty round_trip test). 6 new tests (2 parser incl. either-order, 3 typechecker accept/reject/absent, 1 round-trip); 133 lib tests, fmt/clippy green. effect.rs header note refreshed. REMAINING: grade in TypeAnnotation::Function (function-valued params); parallel @epi(...) surface." }
 ]
 
 [design-artefact-locations]

crates/jtv-core/src/ast.rs

@@ -200,12 +200,29 @@ pub enum LogicalOp {
 
 // ===== FUNCTIONS =====
 
+/// The three loss classes of the Echo effect taxonomy (spec v2 §8–9); lattice
+/// order `Safe ⊑ Neutral ⊑ Breaking`. Defined here, rather than in `echo.rs`, so
+/// the AST can carry an `@echo(...)` annotation without a module cycle
+/// (`echo.rs` imports `ast`). `echo.rs` re-exports it and owns its lattice ops.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+pub enum Echo {
+    /// No loss — injective / reversible.
+    Safe,
+    /// Structured loss — non-total erasure, residue retained.
+    Neutral,
+    /// Total erasure — irreversible.
+    Breaking,
+}
+
 #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
 pub struct FunctionDecl {
     pub name: String,
     pub params: Vec<Param>,
     pub return_type: Option<TypeAnnotation>,
     pub purity: Purity,
+    /// Optional `@echo(...)` grade ceiling (ADR-0009 D1). The checker verifies
+    /// the inferred (composed) echo does not exceed it: `inferred ⊑ annotated`.
+    pub echo_annotation: Option<Echo>,
     pub body: Vec<ControlStmt>,
 }
 

crates/jtv-core/src/echo.rs

@@ -31,16 +31,10 @@
 use crate::ast::*;
 use std::collections::HashMap;
 
-/// The three loss classes of the Echo taxonomy.
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
-pub enum Echo {
-    /// No loss — injective / reversible.
-    Safe,
-    /// Structured loss — non-total erasure, residue retained.
-    Neutral,
-    /// Total erasure — irreversible.
-    Breaking,
-}
+/// The three loss classes of the Echo taxonomy. The enum lives in `ast` (so the
+/// AST can carry an `@echo(...)` annotation without a module cycle); it is
+/// re-exported here, where its lattice operations are defined.
+pub use crate::ast::Echo;
 
 impl Echo {
     /// Least upper bound. `Breaking` is absorbing; `Safe` is the unit.

crates/jtv-core/src/effect.rs

@@ -6,10 +6,12 @@
 // Epistemic via `function_epistemic`); `resolved_effects` joins in the effects
 // of the functions it calls, transitively, to a fixpoint over the call graph.
 //
-// This is the *composition* half of Echo+Epistemic-as-function-effects. It works
-// over the existing AST via an effect environment — it does not yet store the
-// grade in the type AST (`TypeAnnotation::Function`); that surface-level wiring
-// is a later slice.
+// This is the *composition* half of Echo+Epistemic-as-function-effects. The
+// surface `@echo(...)` annotation on a `FunctionDecl` and its upper-bound check
+// (`inferred ⊑ annotated`, ADR-0009 D1) landed via the typechecker's
+// `check_echo_annotations`, which consumes `resolved_effects` here. Carrying the
+// grade in the *type* AST (`TypeAnnotation::Function`, for function-valued
+// params) and the parallel `@epi(...)` surface remain later slices.
 
 use crate::ast::*;
 use crate::echo::{function_echo_in_env, CarrierEnv, Echo};
@@ -266,6 +268,7 @@ mod tests {
                 .collect(),
             return_type: None,
             purity: Purity::Pure,
+            echo_annotation: None,
             body,
         }
     }

crates/jtv-core/src/epistemic.rs

@@ -133,6 +133,7 @@ mod tests {
                 .collect(),
             return_type: None,
             purity: Purity::Pure,
+            echo_annotation: None,
             body,
         }
     }

crates/jtv-core/src/formatter.rs

@@ -120,6 +120,18 @@ impl Formatter {
             Purity::Impure => {}
         }
 
+        // Echo grade annotation
+        if let Some(echo) = func.echo_annotation {
+            self.output.push_str(&format!(
+                "@echo({}) ",
+                match echo {
+                    Echo::Safe => "Safe",
+                    Echo::Neutral => "Neutral",
+                    Echo::Breaking => "Breaking",
+                }
+            ));
+        }
+
         // Function signature
         self.output.push_str("fn ");
         self.output.push_str(&func.name);

crates/jtv-core/src/grammar.pest

@@ -122,11 +122,15 @@ encoding_clause = { "encoding" ~ string }
 
 // ===== FUNCTIONS =====
 function_decl = {
-    purity_marker? ~ "fn" ~ identifier ~ "(" ~ param_list? ~ ")" ~ (":" ~ return_type)? ~ block
+    (purity_marker | echo_marker)* ~ "fn" ~ identifier ~ "(" ~ param_list? ~ ")" ~ (":" ~ return_type)? ~ block
 }
 
 purity_marker = { "@pure" | "@total" }
 
+// ADR-0009 D1: an optional Echo grade ceiling on the function arrow.
+echo_marker = { "@echo" ~ "(" ~ echo_grade ~ ")" }
+echo_grade = { "Safe" | "Neutral" | "Breaking" }
+
 param_list = { param ~ ("," ~ param)* }
 param = { identifier ~ (":" ~ type_annotation)? }