feat(epi): surface @epi(...) epistemic-grade annotation (ADR-0009 D2)

Mirrors the @echo surface for the epistemic axis, completing the ADR-0009
D1+D2 function-declaration effect surface (Echo + Epistemic, first-class).

- Syntax: `@epi(Opaque|Partial|Transparent)` before `fn`, order-independent
  with `@pure`/`@echo` (grammar `epi_marker`; parser marker loop extended).
- AST: `FunctionDecl.epi_annotation: Option<Epistemic>`. The `Epistemic` enum
  moves epistemic.rs -> ast.rs with a `pub use crate::ast::Epistemic` re-export
  (same ast <-> epistemic cycle-break as Echo); every `epistemic::Epistemic`
  site is unchanged.
- Check: `check_echo_annotations` -> `check_effect_annotations`, now verifying
  BOTH axes `inferred <= annotated` (echo and epi) against the composed
  `resolved_effects` (FunctionEffect carries .echo + .epi).
- Round-trip: pretty.rs + formatter.rs emit `@epi` after `@echo`.

5 new tests (parse @epi + echo&epi together; epi upper-bound accept/reject;
round-trip); 138 lib tests, cargo fmt + clippy clean.

Remaining on this axis: carry the (echo, epi) row in `TypeAnnotation::Function`
(function-valued params).

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 — 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]

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<Echo>,
+    /// Optional `@epi(...)` epistemic-grade ceiling (ADR-0009 D2), checked the
+    /// same way as `echo_annotation`.
+    pub epi_annotation: Option<Epistemic>,
     pub body: Vec<ControlStmt>,
 }
 

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,
         }
     }

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,
         }
     }

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);

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)? }
 

crates/jtv-core/src/parser.rs

@@ -77,11 +77,12 @@ fn parse_function(pair: pest::iterators::Pair<Rule>) -> Result<TopLevel> {
 
     let mut purity = Purity::Impure;
     let mut echo_annotation: Option<Echo> = None;
+    let mut epi_annotation: Option<Epistemic> = 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<Rule>) -> Result<TopLevel> {
             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<Rule>) -> Result<TopLevel> {
         return_type,
         purity,
         echo_annotation,
+        epi_annotation,
         body,
     }))
 }
@@ -149,6 +154,15 @@ fn parse_echo_grade(marker: pest::iterators::Pair<Rule>) -> Option<Echo> {
     })
 }
 
+/// Extract the Epistemic grade from an `@epi(...)` marker pair (ADR-0009 D2).
+fn parse_epi_grade(marker: pest::iterators::Pair<Rule>) -> Option<Epistemic> {
+    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<Rule>) -> Result<Param> {
     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();