diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 3a61416..91089ad 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 — 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)" +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) (the @epi(...) surface LANDED 2026-06-18); 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. 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", + "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) (the @epi(...) surface LANDED 2026-06-18)", "Verification bridge: correlation tests between Lean semantics and Rust interpreter", "PataCL Phase 1 → unblocks JtV coproc implementation Phase 2" ] @@ -89,7 +89,8 @@ sessions = [ { 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 = "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." } + { 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." }, + { date = "2026-06-18", subject = "@epi(...) epistemic-grade surface (ADR-0009 D2) — mirror of the @echo surface. @epi(Opaque|Partial|Transparent) annotation on functions: grammar.pest epi_marker; parser.rs marker loop also consumes epi_marker → FunctionDecl.epi_annotation (order-independent with @pure/@echo). Epistemic enum moved epistemic.rs→ast.rs (gains Serialize) with `pub use crate::ast::Epistemic` re-export, same cycle-break as Echo. typechecker.rs check_echo_annotations renamed check_effect_annotations: now checks BOTH axes (inferred.echo ⊑ @echo, inferred.epi ⊑ @epi) against resolved_effects (FunctionEffect carries .echo + .epi). pretty.rs + formatter.rs emit @epi after @echo. 5 new tests (parser @epi + echo&epi-together, typechecker epi accept/reject, round-trip); 138 lib tests, fmt/clippy green. Completes the ADR-0009 D1+D2 function-DECLARATION effect surface. REMAINING on this axis: carry the (echo,epi) row in TypeAnnotation::Function (function-VALUED params) — has a function-type grade-syntax + variance design choice to settle." } ] [design-artefact-locations] diff --git a/crates/jtv-core/src/ast.rs b/crates/jtv-core/src/ast.rs index 004c626..499089e 100644 --- a/crates/jtv-core/src/ast.rs +++ b/crates/jtv-core/src/ast.rs @@ -214,6 +214,19 @@ pub enum Echo { Breaking, } +/// The epistemic grade (ADR-0009 D2): how much a function reveals about its +/// inputs; lattice order `Opaque ⊑ Partial ⊑ Transparent`. Defined here for the +/// same cycle reason as `Echo`; `epistemic.rs` re-exports it and owns its ops. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub enum Epistemic { + /// Reveals nothing about the inputs. + Opaque, + /// Reveals a bounded function of the inputs. + Partial, + /// Reveals the inputs fully (the output determines the input). + Transparent, +} + #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] pub struct FunctionDecl { pub name: String, @@ -223,6 +236,9 @@ pub struct FunctionDecl { /// Optional `@echo(...)` grade ceiling (ADR-0009 D1). The checker verifies /// the inferred (composed) echo does not exceed it: `inferred ⊑ annotated`. pub echo_annotation: Option, + /// Optional `@epi(...)` epistemic-grade ceiling (ADR-0009 D2), checked the + /// same way as `echo_annotation`. + pub epi_annotation: Option, pub body: Vec, } diff --git a/crates/jtv-core/src/effect.rs b/crates/jtv-core/src/effect.rs index b9faaf7..560fe14 100644 --- a/crates/jtv-core/src/effect.rs +++ b/crates/jtv-core/src/effect.rs @@ -269,6 +269,7 @@ mod tests { return_type: None, purity: Purity::Pure, echo_annotation: None, + epi_annotation: None, body, } } diff --git a/crates/jtv-core/src/epistemic.rs b/crates/jtv-core/src/epistemic.rs index 833b5e9..303f628 100644 --- a/crates/jtv-core/src/epistemic.rs +++ b/crates/jtv-core/src/epistemic.rs @@ -15,16 +15,10 @@ use crate::ast::*; use std::collections::HashSet; -/// The epistemic grade (ADR-0009 D2): how much a function reveals about inputs. -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum Epistemic { - /// Reveals nothing about the inputs. - Opaque, - /// Reveals a bounded function of the inputs. - Partial, - /// Reveals the inputs fully (the output determines the input). - Transparent, -} +/// The epistemic grade (ADR-0009 D2). The enum lives in `ast` (so the AST can +/// carry an `@epi(...)` annotation without a module cycle); re-exported here, +/// where its lattice operations are defined. +pub use crate::ast::Epistemic; impl Epistemic { fn rank(self) -> u8 { @@ -134,6 +128,7 @@ mod tests { return_type: None, purity: Purity::Pure, echo_annotation: None, + epi_annotation: None, body, } } diff --git a/crates/jtv-core/src/formatter.rs b/crates/jtv-core/src/formatter.rs index 8b2fb66..01ef51d 100644 --- a/crates/jtv-core/src/formatter.rs +++ b/crates/jtv-core/src/formatter.rs @@ -132,6 +132,18 @@ impl Formatter { )); } + // Epistemic grade annotation + if let Some(epi) = func.epi_annotation { + self.output.push_str(&format!( + "@epi({}) ", + match epi { + Epistemic::Opaque => "Opaque", + Epistemic::Partial => "Partial", + Epistemic::Transparent => "Transparent", + } + )); + } + // 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 a9b4165..66cf0c1 100644 --- a/crates/jtv-core/src/grammar.pest +++ b/crates/jtv-core/src/grammar.pest @@ -122,7 +122,7 @@ encoding_clause = { "encoding" ~ string } // ===== FUNCTIONS ===== function_decl = { - (purity_marker | echo_marker)* ~ "fn" ~ identifier ~ "(" ~ param_list? ~ ")" ~ (":" ~ return_type)? ~ block + (purity_marker | echo_marker | epi_marker)* ~ "fn" ~ identifier ~ "(" ~ param_list? ~ ")" ~ (":" ~ return_type)? ~ block } purity_marker = { "@pure" | "@total" } @@ -131,6 +131,10 @@ purity_marker = { "@pure" | "@total" } echo_marker = { "@echo" ~ "(" ~ echo_grade ~ ")" } echo_grade = { "Safe" | "Neutral" | "Breaking" } +// ADR-0009 D2: an optional Epistemic grade ceiling on the function arrow. +epi_marker = { "@epi" ~ "(" ~ epi_grade ~ ")" } +epi_grade = { "Opaque" | "Partial" | "Transparent" } + 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 44dfdb2..f9c5e5d 100644 --- a/crates/jtv-core/src/parser.rs +++ b/crates/jtv-core/src/parser.rs @@ -77,11 +77,12 @@ fn parse_function(pair: pest::iterators::Pair) -> Result { let mut purity = Purity::Impure; let mut echo_annotation: Option = None; + let mut epi_annotation: Option = None; let mut first = inner .next() .ok_or_else(|| JtvError::ParseError("Expected function declaration".to_string()))?; - // Consume any leading markers — `@pure`/`@total` and `@echo(...)` — in any order. + // Consume any leading markers — `@pure`/`@total`, `@echo(...)`, `@epi(...)` — in any order. loop { match first.as_rule() { Rule::purity_marker => { @@ -94,6 +95,9 @@ fn parse_function(pair: pest::iterators::Pair) -> Result { Rule::echo_marker => { echo_annotation = parse_echo_grade(first.clone()); } + Rule::epi_marker => { + epi_annotation = parse_epi_grade(first.clone()); + } _ => break, } first = inner.next().ok_or_else(|| { @@ -136,6 +140,7 @@ fn parse_function(pair: pest::iterators::Pair) -> Result { return_type, purity, echo_annotation, + epi_annotation, body, })) } @@ -149,6 +154,15 @@ fn parse_echo_grade(marker: pest::iterators::Pair) -> Option { }) } +/// Extract the Epistemic grade from an `@epi(...)` marker pair (ADR-0009 D2). +fn parse_epi_grade(marker: pest::iterators::Pair) -> Option { + marker.into_inner().next().map(|g| match g.as_str() { + "Partial" => Epistemic::Partial, + "Transparent" => Epistemic::Transparent, + _ => Epistemic::Opaque, + }) +} + fn parse_param(pair: pest::iterators::Pair) -> Result { let mut inner = pair.into_inner(); let name = inner @@ -983,6 +997,28 @@ mod tests { assert!(result.is_ok()); } + #[test] + fn test_parse_epi_annotation() { + let program = parse_program("@epi(Partial) fn f(): Int { return 0 }").unwrap(); + match &program.statements[0] { + TopLevel::Function(func) => assert_eq!(func.epi_annotation, Some(Epistemic::Partial)), + _ => panic!("expected a function"), + } + } + + #[test] + fn test_parse_echo_and_epi_together() { + let program = + parse_program("@echo(Neutral) @epi(Transparent) fn f(): Int { return 0 }").unwrap(); + match &program.statements[0] { + TopLevel::Function(func) => { + assert_eq!(func.echo_annotation, Some(Echo::Neutral)); + assert_eq!(func.epi_annotation, Some(Epistemic::Transparent)); + } + _ => panic!("expected a function"), + } + } + #[test] fn test_parse_echo_annotation() { let program = parse_program("@echo(Neutral) fn f(): Int { return 0 }").unwrap(); diff --git a/crates/jtv-core/src/pretty.rs b/crates/jtv-core/src/pretty.rs index eb58f0f..b2de486 100644 --- a/crates/jtv-core/src/pretty.rs +++ b/crates/jtv-core/src/pretty.rs @@ -205,6 +205,18 @@ impl PrettyPrinter { )); } + // Epistemic grade annotation + if let Some(epi) = func.epi_annotation { + out.push_str(&format!( + "@epi({}) ", + match epi { + Epistemic::Opaque => "Opaque", + Epistemic::Partial => "Partial", + Epistemic::Transparent => "Transparent", + } + )); + } + // Signature out.push_str("fn "); out.push_str(&func.name); @@ -583,6 +595,12 @@ mod tests { round_trip("@pure @echo(Breaking) fn id(x: Int): Int { return x }"); } + #[test] + fn test_round_trip_epi_annotation() { + round_trip("@epi(Transparent) fn f(x: Int): Int { return x }"); + round_trip("@echo(Neutral) @epi(Partial) fn g(x: Int): Int { return x + 1 }"); + } + #[test] fn test_round_trip_pure_function() { round_trip("@pure fn double(x: Int): Int { return x + x }"); @@ -708,6 +726,7 @@ mod tests { return_type: Some(TypeAnnotation::Basic(BasicType::Int)), purity: Purity::Impure, echo_annotation: None, + epi_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 42a454e..a0f12cc 100644 --- a/crates/jtv-core/src/typechecker.rs +++ b/crates/jtv-core/src/typechecker.rs @@ -198,8 +198,8 @@ impl TypeChecker { self.check_top_level(stmt)?; } - // Third pass: Echo annotation check (ADR-0009 D1, upper-bound policy). - self.check_echo_annotations(program)?; + // Third pass: Echo + Epistemic annotation check (ADR-0009 D1/D2, upper-bound). + self.check_effect_annotations(program)?; if self.errors.is_empty() { Ok(()) @@ -208,34 +208,53 @@ 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 { + /// Verify each `@echo(...)` / `@epi(...)` annotation is an upper bound on the + /// function's inferred (composed) grade — `inferred ⊑ annotated` (ADR-0009 + /// D1/D2). A function may declare *more* loss / revelation 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_effect_annotations(&self, program: &Program) -> Result<()> { + fn echo_name(e: Echo) -> &'static str { match e { Echo::Safe => "Safe", Echo::Neutral => "Neutral", Echo::Breaking => "Breaking", } } + fn epi_name(e: Epistemic) -> &'static str { + match e { + Epistemic::Opaque => "Opaque", + Epistemic::Partial => "Partial", + Epistemic::Transparent => "Transparent", + } + } let effects = effect::resolved_effects(program); for stmt in &program.statements { if let TopLevel::Function(func) = stmt { + let inferred = effects + .get(&func.name) + .copied() + .unwrap_or(effect::FunctionEffect::SAFE); 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) { + if !inferred.echo.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), + echo_name(annotated), + echo_name(inferred.echo), + ))); + } + } + if let Some(annotated) = func.epi_annotation { + if !inferred.epi.leq(annotated) { + return Err(JtvError::EchoViolation(format!( + "function `{}` declares `@epi({})` but its inferred epistemic grade is \ + `{}` — a function may declare more revelation than it incurs, never less", + func.name, + epi_name(annotated), + epi_name(inferred.epi), ))); } } @@ -870,6 +889,7 @@ mod tests { return_type: None, purity: Purity::Impure, echo_annotation: annotation, + epi_annotation: None, body: vec![ ControlStmt::Assignment(Assignment { target: "x".to_string(), @@ -914,6 +934,35 @@ mod tests { .is_ok()); } + #[test] + fn epi_annotation_upper_bound_accepts_over_declaration() { + // An Opaque function (output independent of inputs) passes under any ceiling. + for ann in ["Opaque", "Partial", "Transparent"] { + let src = format!("@epi({ann}) fn f(x: Int): Int {{ return 0 }}"); + let program = parse_program(&src).unwrap(); + assert!( + TypeChecker::new().check_program(&program).is_ok(), + "@epi({ann}) over an Opaque function should pass" + ); + } + } + + #[test] + fn epi_annotation_upper_bound_rejects_under_declaration() { + // Returning a parameter is Transparent; @epi(Opaque|Partial) under-declares. + for ann in ["Opaque", "Partial"] { + let src = format!("@epi({ann}) fn f(x: Int): Int {{ return x }}"); + let program = parse_program(&src).unwrap(); + assert!( + matches!( + TypeChecker::new().check_program(&program), + Err(JtvError::EchoViolation(_)) + ), + "@epi({ann}) over a Transparent function should reject" + ); + } + } + #[test] fn test_reversible_block_with_token_admits_self_reference() { // A `reversible { x += x } -> tok` block retains a residue (token) for