From 4920cfa4305f3e2e771075c98eedeca788b2004d Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 12:54:01 +0000 Subject: [PATCH] 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`. 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 Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .machine_readable/6a2/STATE.a2ml | 7 ++- crates/jtv-core/src/ast.rs | 17 ++++++ crates/jtv-core/src/echo.rs | 14 ++--- crates/jtv-core/src/effect.rs | 11 ++-- crates/jtv-core/src/epistemic.rs | 1 + crates/jtv-core/src/formatter.rs | 12 ++++ crates/jtv-core/src/grammar.pest | 6 +- crates/jtv-core/src/parser.rs | 61 ++++++++++++++++--- crates/jtv-core/src/pretty.rs | 20 +++++++ crates/jtv-core/src/typechecker.rs | 95 ++++++++++++++++++++++++++++++ 10 files changed, 218 insertions(+), 26 deletions(-) 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