diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index e2e578f..3a61416 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.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]
diff --git a/crates/jtv-core/src/ast.rs b/crates/jtv-core/src/ast.rs
index 6435464..004c626 100644
--- a/crates/jtv-core/src/ast.rs
+++ b/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,
pub return_type: Option,
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,
pub body: Vec,
}
diff --git a/crates/jtv-core/src/echo.rs b/crates/jtv-core/src/echo.rs
index c888e7a..d2cb87f 100644
--- a/crates/jtv-core/src/echo.rs
+++ b/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.
diff --git a/crates/jtv-core/src/effect.rs b/crates/jtv-core/src/effect.rs
index b474af3..b9faaf7 100644
--- a/crates/jtv-core/src/effect.rs
+++ b/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,
}
}
diff --git a/crates/jtv-core/src/epistemic.rs b/crates/jtv-core/src/epistemic.rs
index fea4915..833b5e9 100644
--- a/crates/jtv-core/src/epistemic.rs
+++ b/crates/jtv-core/src/epistemic.rs
@@ -133,6 +133,7 @@ mod tests {
.collect(),
return_type: None,
purity: Purity::Pure,
+ echo_annotation: None,
body,
}
}
diff --git a/crates/jtv-core/src/formatter.rs b/crates/jtv-core/src/formatter.rs
index 0bacdbf..8b2fb66 100644
--- a/crates/jtv-core/src/formatter.rs
+++ b/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);
diff --git a/crates/jtv-core/src/grammar.pest b/crates/jtv-core/src/grammar.pest
index bc2e38f..a9b4165 100644
--- a/crates/jtv-core/src/grammar.pest
+++ b/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)? }
diff --git a/crates/jtv-core/src/parser.rs b/crates/jtv-core/src/parser.rs
index 3350e33..44dfdb2 100644
--- a/crates/jtv-core/src/parser.rs
+++ b/crates/jtv-core/src/parser.rs
@@ -76,19 +76,28 @@ fn parse_function(pair: pest::iterators::Pair) -> Result {
let mut inner = pair.into_inner();
let mut purity = Purity::Impure;
+ let mut echo_annotation: Option = None;
let mut first = inner
.next()
.ok_or_else(|| JtvError::ParseError("Expected function declaration".to_string()))?;
- // Check for purity marker
- if first.as_rule() == Rule::purity_marker {
- purity = match first.as_str() {
- "@pure" => Purity::Pure,
- "@total" => Purity::Total,
- _ => Purity::Impure,
- };
+ // Consume any leading markers — `@pure`/`@total` and `@echo(...)` — in any order.
+ loop {
+ match first.as_rule() {
+ Rule::purity_marker => {
+ purity = match first.as_str() {
+ "@pure" => Purity::Pure,
+ "@total" => Purity::Total,
+ _ => Purity::Impure,
+ };
+ }
+ Rule::echo_marker => {
+ echo_annotation = parse_echo_grade(first.clone());
+ }
+ _ => break,
+ }
first = inner.next().ok_or_else(|| {
- JtvError::ParseError("Expected function name after purity marker".to_string())
+ JtvError::ParseError("Expected function name after marker".to_string())
})?;
}
@@ -126,10 +135,20 @@ fn parse_function(pair: pest::iterators::Pair) -> Result {
params,
return_type,
purity,
+ echo_annotation,
body,
}))
}
+/// Extract the Echo grade from an `@echo(...)` marker pair (ADR-0009 D1).
+fn parse_echo_grade(marker: pest::iterators::Pair) -> Option {
+ marker.into_inner().next().map(|g| match g.as_str() {
+ "Neutral" => Echo::Neutral,
+ "Breaking" => Echo::Breaking,
+ _ => Echo::Safe,
+ })
+}
+
fn parse_param(pair: pest::iterators::Pair) -> Result {
let mut inner = pair.into_inner();
let name = inner
@@ -964,6 +983,32 @@ mod tests {
assert!(result.is_ok());
}
+ #[test]
+ fn test_parse_echo_annotation() {
+ let program = parse_program("@echo(Neutral) fn f(): Int { return 0 }").unwrap();
+ match &program.statements[0] {
+ TopLevel::Function(func) => assert_eq!(func.echo_annotation, Some(Echo::Neutral)),
+ _ => panic!("expected a function"),
+ }
+ }
+
+ #[test]
+ fn test_parse_echo_with_purity_either_order() {
+ for code in [
+ "@pure @echo(Breaking) fn f(): Int { return 0 }",
+ "@echo(Breaking) @pure fn f(): Int { return 0 }",
+ ] {
+ let program = parse_program(code).unwrap();
+ match &program.statements[0] {
+ TopLevel::Function(func) => {
+ assert_eq!(func.purity, Purity::Pure);
+ assert_eq!(func.echo_annotation, Some(Echo::Breaking));
+ }
+ _ => panic!("expected a function"),
+ }
+ }
+ }
+
#[test]
fn test_parse_symbolic_literal() {
let code = "x = #pi + #e";
diff --git a/crates/jtv-core/src/pretty.rs b/crates/jtv-core/src/pretty.rs
index 84da58f..eb58f0f 100644
--- a/crates/jtv-core/src/pretty.rs
+++ b/crates/jtv-core/src/pretty.rs
@@ -193,6 +193,18 @@ impl PrettyPrinter {
Purity::Impure => {}
}
+ // Echo grade annotation
+ if let Some(echo) = func.echo_annotation {
+ out.push_str(&format!(
+ "@echo({}) ",
+ match echo {
+ Echo::Safe => "Safe",
+ Echo::Neutral => "Neutral",
+ Echo::Breaking => "Breaking",
+ }
+ ));
+ }
+
// Signature
out.push_str("fn ");
out.push_str(&func.name);
@@ -564,6 +576,13 @@ mod tests {
round_trip("fn add(a: Int, b: Int): Int { return a + b }");
}
+ #[test]
+ fn test_round_trip_echo_annotation() {
+ // The @echo(...) grade must survive parse -> print -> parse.
+ round_trip("@echo(Neutral) fn double(x: Int): Int { return x + x }");
+ round_trip("@pure @echo(Breaking) fn id(x: Int): Int { return x }");
+ }
+
#[test]
fn test_round_trip_pure_function() {
round_trip("@pure fn double(x: Int): Int { return x + x }");
@@ -688,6 +707,7 @@ mod tests {
params: vec![],
return_type: Some(TypeAnnotation::Basic(BasicType::Int)),
purity: Purity::Impure,
+ echo_annotation: None,
body: vec![ControlStmt::Return(Some(DataExpr::Number(Number::Int(0))))],
};
let rendered = printer.print_function(&func, 0);
diff --git a/crates/jtv-core/src/typechecker.rs b/crates/jtv-core/src/typechecker.rs
index 3f90be2..42a454e 100644
--- a/crates/jtv-core/src/typechecker.rs
+++ b/crates/jtv-core/src/typechecker.rs
@@ -3,6 +3,7 @@
use crate::ast::*;
use crate::echo::{self, Echo};
+use crate::effect;
use crate::error::{JtvError, Result};
use std::collections::HashMap;
@@ -197,6 +198,9 @@ impl TypeChecker {
self.check_top_level(stmt)?;
}
+ // Third pass: Echo annotation check (ADR-0009 D1, upper-bound policy).
+ self.check_echo_annotations(program)?;
+
if self.errors.is_empty() {
Ok(())
} else {
@@ -204,6 +208,42 @@ impl TypeChecker {
}
}
+ /// Verify each `@echo(...)` annotation is an upper bound on the function's
+ /// inferred (composed) echo grade — `inferred ⊑ annotated` (ADR-0009 D1).
+ /// A function may declare *more* loss than it incurs, never less. The
+ /// inferred grade is the carrier-aware, call-graph-composed `resolved_effects`,
+ /// so a caller can be checked against a callee's declared ceiling (modular).
+ fn check_echo_annotations(&self, program: &Program) -> Result<()> {
+ fn grade_name(e: Echo) -> &'static str {
+ match e {
+ Echo::Safe => "Safe",
+ Echo::Neutral => "Neutral",
+ Echo::Breaking => "Breaking",
+ }
+ }
+ let effects = effect::resolved_effects(program);
+ for stmt in &program.statements {
+ if let TopLevel::Function(func) = stmt {
+ if let Some(annotated) = func.echo_annotation {
+ let inferred = effects
+ .get(&func.name)
+ .map(|e| e.echo)
+ .unwrap_or(Echo::Safe);
+ if !inferred.leq(annotated) {
+ return Err(JtvError::EchoViolation(format!(
+ "function `{}` declares `@echo({})` but its inferred echo is `{}` — \
+ a function may declare more loss than it incurs, never less",
+ func.name,
+ grade_name(annotated),
+ grade_name(inferred),
+ )));
+ }
+ }
+ }
+ }
+ Ok(())
+ }
+
fn register_function(&mut self, func: &FunctionDecl) -> Result<()> {
let params: Vec = func
.params
@@ -819,6 +859,61 @@ mod tests {
.is_ok());
}
+ // Build a function whose inferred echo is Neutral: a self-referential
+ // `reversible { x += x } -> tok` over a prior local `x`.
+ fn neutral_function(annotation: Option) -> Program {
+ use crate::ast::*;
+ Program {
+ statements: vec![TopLevel::Function(FunctionDecl {
+ name: "f".to_string(),
+ params: vec![],
+ return_type: None,
+ purity: Purity::Impure,
+ echo_annotation: annotation,
+ body: vec![
+ ControlStmt::Assignment(Assignment {
+ target: "x".to_string(),
+ value: Expr::Data(DataExpr::Number(Number::Int(0))),
+ }),
+ ControlStmt::ReversibleBlock(ReversibleBlockStmt {
+ body: vec![ReversibleStmt::AddAssign(
+ "x".to_string(),
+ DataExpr::Identifier("x".to_string()),
+ )],
+ token_binding: Some("tok".to_string()),
+ }),
+ ],
+ })],
+ }
+ }
+
+ #[test]
+ fn echo_annotation_upper_bound_accepts_over_declaration() {
+ // inferred Neutral ⊑ annotated Neutral (exact) and ⊑ Breaking (looser) → ok.
+ for ann in [Echo::Neutral, Echo::Breaking] {
+ let program = neutral_function(Some(ann));
+ assert!(TypeChecker::new().check_program(&program).is_ok());
+ }
+ }
+
+ #[test]
+ fn echo_annotation_upper_bound_rejects_under_declaration() {
+ // @echo(Safe) on a Neutral function: Neutral ⋢ Safe → rejected.
+ let program = neutral_function(Some(Echo::Safe));
+ assert!(matches!(
+ TypeChecker::new().check_program(&program),
+ Err(JtvError::EchoViolation(_))
+ ));
+ }
+
+ #[test]
+ fn echo_annotation_absent_is_unconstrained() {
+ // No annotation → no ceiling check; the Neutral function type-checks.
+ assert!(TypeChecker::new()
+ .check_program(&neutral_function(None))
+ .is_ok());
+ }
+
#[test]
fn test_reversible_block_with_token_admits_self_reference() {
// A `reversible { x += x } -> tok` block retains a residue (token) for