hyperpolymath · hyperpolymath · Jun 21, 2026 · Jun 21, 2026
@@ -46,7 +46,7 @@ milestones = [
 
 [blockers-and-issues]
 issues = [
-  { id = "gap-001", description = "Verification chain incomplete: proofs validate models but not wired to Rust interpreter", severity = "medium", status = "known" },
+  { id = "gap-001", description = "Verification chain incomplete: proofs validate models but not wired to Rust interpreter. PARTIAL 2026-06-21: denotational correspondence harness ties Lean evalDataExpr ↔ Rust eval_data_expr over the integer fragment (interpreter.rs mod denotational_correspondence: exhaustive height-≤2 agreement ~12k cases + i64 overflow boundary + cross-side golden corpus mirrored as rfl examples in JtvCore.lean). Remaining: Lean-mechanised refinement of the evaluator + extended surface", severity = "medium", status = "known", follow-up = "mechanised refinement; extend past the integer fragment" },
   { id = "gap-002", description = "typing_coercion in JtvTypes.lean weaker than docstring — proves existence not coercion to target type", severity = "low", status = "known", follow-up = "ADR needed" },
   { id = "gap-003", description = "Coprocessor implementation gated on PataCL Phase 1", severity = "medium", status = "external-dependency" },
   { id = "gap-004", description = "Reversibility round-trip not guaranteed end-to-end at integration level", severity = "medium", status = "known" },
@@ -92,7 +92,8 @@ sessions = [
   { 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) [LANDED 2026-06-18, prefix-marker syntax]; 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." },
   { date = "2026-06-18", subject = "Function-TYPE grade carrying (ADR-0009 D1/D3) — completes the ADR-0009 effect surface. A function type Fn(...) -> T may now carry the (echo,epi) row with PREFIX markers (user choice): @echo(Neutral) @epi(Partial) Fn(Int) -> Int. ast.rs: new EffectGrade { echo: Option<Echo>, epi: Option<Epistemic> } (Default); TypeAnnotation::Function gains a trailing EffectGrade; typechecker Type::Function likewise. grammar.pest function_type now (echo_marker|epi_marker)* ~ 'Fn' ...; parser splits the leading markers from the param/return type_annotations. annotation_to_type carries the grade into Type::Function; Display + pretty.rs + formatter.rs emit the prefix markers (round-trip). coercible_to gains a function-type case: COVARIANT in the grade (grade_leq — a function that loses/reveals LESS is usable where MORE is allowed; None target = unconstrained; None source can't satisfy a Some ceiling; params/return invariant for now). 4 tests (parse graded + ungraded; round-trip; covariance accept/reject/unconstrained); 142 lib tests, fmt/clippy green. HONEST SCOPE: representational/forward-infrastructure — JtV has no first-class function VALUES (no lambdas/indirect calls) yet, so the value-against-type coercion is correct but LATENT until function values land. ADR-0009 D1+D2+D3 declaration+type effect surface now COMPLETE." },
-  { date = "2026-06-21", subject = "type_preservation lifted past τ=int to the integer-represented family {int,hex,binary} (gap-005 partial). LOCAL LEAN TOOLCHAIN UNBLOCKED: elan 4.2.2 was present but had no toolchain, and `release.lean-lang.org` is off the egress allowlist (its 'Host not in allowlist' page is the stray 'H' that broke elan's release-metadata parse). Bypassed by fetching the v4.12.0 linux tarball straight from GitHub releases (github.com + the asset host ARE allowlisted) and unpacking it into ~/.elan/toolchains/leanprover--lean4---v4.12.0 — elan then recognises the pinned toolchain; full `lake build` exit 0 (suite is mathlib-free, zero packages, no network). PROOF (JtvTypes.lean SECTION 6): inductive TypedValue gains hex + binary constructors (all three number systems share the Int runtime carrier — hex/binary ARE int-represented); new predicate JtvType.isIntRepr {int,hex,binary}↦True else False; type_preservation generalised from `τ=int → …` to `(hτ : τ.isIntRepr) → TypedValue (evalDataExpr e σ) τ`, proved `cases τ <;> first | exact TypedValue.{int,hex,binary} | simp only [JtvType.isIntRepr] at hτ`; type_preservation_int corollary recovers the original τ=int statement (via subst + trivial). `#print axioms` ⇒ BOTH new theorems depend on NO axioms. INVARIANTS held: full lake build exit 0; 0 sorry/admit/axiom (word-boundary grep); 0 True-typed theorems. DOCS synced: PROOF-CAPABILITY-MATRIX (scope-of-model rewrite + new key-theorems row + 'checked 2026-06-04; re-verified 2026-06-21' note), ADR-0007 consequence #1, ADR-0010 §gap-005 + §Open. float/rational/complex/symbolic REMAIN stated-unproven (distinct carriers, each needs its own value model). NOTE for next session: the local toolchain at ~/.elan is ephemeral (container reclaimed on inactivity) — re-run the GitHub-releases bypass to restore `lake build`; CI (proof-regression.yml) is the durable verifier." }
+  { date = "2026-06-21", subject = "type_preservation lifted past τ=int to the integer-represented family {int,hex,binary} (gap-005 partial). LOCAL LEAN TOOLCHAIN UNBLOCKED: elan 4.2.2 was present but had no toolchain, and `release.lean-lang.org` is off the egress allowlist (its 'Host not in allowlist' page is the stray 'H' that broke elan's release-metadata parse). Bypassed by fetching the v4.12.0 linux tarball straight from GitHub releases (github.com + the asset host ARE allowlisted) and unpacking it into ~/.elan/toolchains/leanprover--lean4---v4.12.0 — elan then recognises the pinned toolchain; full `lake build` exit 0 (suite is mathlib-free, zero packages, no network). PROOF (JtvTypes.lean SECTION 6): inductive TypedValue gains hex + binary constructors (all three number systems share the Int runtime carrier — hex/binary ARE int-represented); new predicate JtvType.isIntRepr {int,hex,binary}↦True else False; type_preservation generalised from `τ=int → …` to `(hτ : τ.isIntRepr) → TypedValue (evalDataExpr e σ) τ`, proved `cases τ <;> first | exact TypedValue.{int,hex,binary} | simp only [JtvType.isIntRepr] at hτ`; type_preservation_int corollary recovers the original τ=int statement (via subst + trivial). `#print axioms` ⇒ BOTH new theorems depend on NO axioms. INVARIANTS held: full lake build exit 0; 0 sorry/admit/axiom (word-boundary grep); 0 True-typed theorems. DOCS synced: PROOF-CAPABILITY-MATRIX (scope-of-model rewrite + new key-theorems row + 'checked 2026-06-04; re-verified 2026-06-21' note), ADR-0007 consequence #1, ADR-0010 §gap-005 + §Open. float/rational/complex/symbolic REMAIN stated-unproven (distinct carriers, each needs its own value model). NOTE for next session: the local toolchain at ~/.elan is ephemeral (container reclaimed on inactivity) — re-run the GitHub-releases bypass to restore `lake build`; CI (proof-regression.yml) is the durable verifier." },
+  { date = "2026-06-21", subject = "interpreter_correctness (PROOF-2 / gap-001) rung — denotational correspondence harness. Ties the Lean denotational model evalDataExpr ↔ the Rust interpreter eval_data_expr over the integer fragment the model covers (lit|var|add|neg over σ:String→Int). crates/jtv-core/src/interpreter.rs gains `mod denotational_correspondence`: (1) `denot` re-encodes the four Lean rules in i128; (2) `interpreter_matches_denotational_model_on_int_fragment` EXHAUSTIVELY enumerates every height-≤2 integer-fragment expression (5 lits × 2 vars = 7 leaves → 4039 exprs) across 3 states ≈ 12k cases, asserting interpreter == denot on all; (3) `overflow_is_the_correspondence_boundary` pins that Value::Int is i64 with checked_add/checked_neg → ERRORS at the i64 edge, never wraps (so correspondence boundary is exactly i64 range, Lean ℤ being unbounded); (4) `shared_golden_corpus_matches_lean` mirrors 7 concrete (expr,σ,value) points that are ALSO pinned by `rfl` in JtvCore.lean (cross-side anchor; the 5 new Lean `example`s use State.empty[x↦v] updates, all close by rfl). HONEST BOUND: integer fragment only (strings/float/rational/complex/calls/lists/tuples out of model); within i64 range; exhaustive-up-to-depth, NOT a Lean-mechanised refinement of the Rust evaluator (the deeper PROOF-2 rung). VERIFIED locally: cargo test (145 lib incl. 3 new + full workspace green), cargo fmt --check + clippy -D warnings clean, full lake build exit 0, 0 sorry/admit/axiom, 0 True-typed theorems. DOCS: PROOF-CAPABILITY-MATRIX (interpreter_correctness row JtvCore+interpreter.rs/partial + new 'Interpreter ↔ denotational-model correspondence' section + outstanding-work bullet), gap-001 partial. NEXT on PROOF-2: mechanised refinement (model the Rust evaluator in Lean) and/or extend the harness past the integer fragment." }
 ]
 
 [design-artefact-locations]

@@ -806,3 +806,197 @@ fn double(x: Int): Int {
         assert_eq!(sum, Value::Int(15)); // 1+2+3+4+5
     }
 }
+
+// ===========================================================================
+// Denotational correspondence (PROOF-2 / gap-001)
+//
+// Bridges this interpreter's `eval_data_expr` to the Lean denotational model
+// `evalDataExpr` in jtv_proofs/JtvCore.lean, over the integer fragment the
+// model covers:  DataExpr = lit | var | add | neg  evaluated against a state
+// σ : String → Int.
+//
+// `denot` re-encodes the four Lean rules exactly (in i128, giving Lean's
+// unbounded ℤ headroom). We then EXHAUSTIVELY enumerate every integer-fragment
+// expression up to height 2 over a small literal/variable set, across several
+// states, and assert the interpreter agrees with `denot` on all of them.
+//
+// Honest bound:
+//   (1) integer fragment only — String/Float/Rational/Complex/Hex/Binary/
+//       Symbolic literals and FunctionCall/List/Tuple are outside the model;
+//   (2) within i64 range — `Value::Int` is i64 (`checked_add`/`checked_neg`),
+//       Lean's ℤ is unbounded, so they agree exactly where no i64 overflow
+//       occurs; the enumeration stays in range by construction, and
+//       `overflow_is_the_correspondence_boundary` pins the edge;
+//   (3) this is exhaustive-up-to-depth correspondence, NOT a Lean-mechanised
+//       refinement of the Rust evaluator (that is the deeper PROOF-2 rung).
+// ===========================================================================
+#[cfg(test)]
+mod denotational_correspondence {
+    use super::*;
+    use crate::ast::{DataExpr, Number};
+    use std::collections::HashMap;
+
+    /// The Lean `evalDataExpr` rules, re-encoded in i128.
+    /// `None` for any node outside the modelled integer fragment.
+    fn denot(e: &DataExpr, sigma: &HashMap<String, i128>) -> Option<i128> {
+        match e {
+            DataExpr::Number(Number::Int(n)) => Some(*n as i128),
+            DataExpr::Identifier(x) => Some(*sigma.get(x).unwrap_or(&0)),
+            DataExpr::Add(l, r) => Some(denot(l, sigma)? + denot(r, sigma)?),
+            DataExpr::Negate(inner) => Some(-denot(inner, sigma)?),
+            _ => None,
+        }
+    }
+
+    /// Every integer-fragment expression of height ≤ `height`.
+    fn enumerate(height: usize, lits: &[i64], vars: &[&str]) -> Vec<DataExpr> {
+        let mut out: Vec<DataExpr> = Vec::new();
+        for &n in lits {
+            out.push(DataExpr::Number(Number::Int(n)));
+        }
+        for &v in vars {
+            out.push(DataExpr::Identifier(v.to_string()));
+        }
+        if height > 0 {
+            let sub = enumerate(height - 1, lits, vars);
+            for e in &sub {
+                out.push(DataExpr::Negate(Box::new(e.clone())));
+            }
+            for a in &sub {
+                for b in &sub {
+                    out.push(DataExpr::Add(Box::new(a.clone()), Box::new(b.clone())));
+                }
+            }
+        }
+        out
+    }
+
+    /// A fresh interpreter with the given state σ seeded as integer variables.
+    fn seed(state: &HashMap<String, i64>) -> Interpreter {
+        let mut interp = Interpreter::new();
+        for (k, v) in state {
+            interp.set_variable(k.clone(), Value::Int(*v));
+        }
+        interp
+    }
+
+    #[test]
+    fn interpreter_matches_denotational_model_on_int_fragment() {
+        let lits = [-2i64, -1, 0, 1, 2];
+        let vars = ["x", "y"];
+        let states: Vec<HashMap<String, i64>> = vec![
+            HashMap::from([("x".to_string(), 0i64), ("y".to_string(), 0i64)]),
+            HashMap::from([("x".to_string(), 3i64), ("y".to_string(), -1i64)]),
+            HashMap::from([("x".to_string(), -2i64), ("y".to_string(), 2i64)]),
+        ];
+        let exprs = enumerate(2, &lits, &vars);
+
+        let mut checked = 0u64;
+        for state in &states {
+            let mut interp = seed(state);
+            let sigma: HashMap<String, i128> =
+                state.iter().map(|(k, v)| (k.clone(), *v as i128)).collect();
+            for e in &exprs {
+                let expected = denot(e, &sigma)
+                    .expect("every enumerated expression is in the integer fragment");
+                // The corpus is constructed to stay within i64 range.
+                assert!(
+                    expected >= i64::MIN as i128 && expected <= i64::MAX as i128,
+                    "corpus left i64 range ({expected}); shrink literals or height"
+                );
+                match interp.eval_data_expr(e) {
+                    Ok(Value::Int(n)) => assert_eq!(
+                        n as i128, expected,
+                        "interpreter vs denotation disagree on {e:?} under {state:?}"
+                    ),
+                    other => panic!(
+                        "expected Ok(Int({expected})) for {e:?} under {state:?}, got {other:?}"
+                    ),
+                }
+                checked += 1;
+            }
+        }
+        // height-2 over 7 leaves = 4039 expressions × 3 states.
+        assert!(
+            checked >= 12_000,
+            "expected a substantial corpus, checked only {checked}"
+        );
+    }
+
+    #[test]
+    fn overflow_is_the_correspondence_boundary() {
+        // i64::MAX + 1 is 2^63 in ℤ — out of i64 range. The interpreter must
+        // SIGNAL overflow (checked_add), never wrap, so the correspondence
+        // boundary is exactly i64 range.
+        let e = DataExpr::Add(
+            Box::new(DataExpr::Number(Number::Int(i64::MAX))),
+            Box::new(DataExpr::Number(Number::Int(1))),
+        );
+        let mut interp = Interpreter::new();
+        let sigma = HashMap::new();
+        let denotational = denot(&e, &sigma).unwrap();
+        assert!(
+            denotational > i64::MAX as i128,
+            "this case is meant to exceed i64"
+        );
+        assert!(
+            interp.eval_data_expr(&e).is_err(),
+            "interpreter must error where ℤ leaves i64 range, not wrap"
+        );
+
+        // neg(i64::MIN) is 2^63 in ℤ — also out of range → must error too.
+        let e2 = DataExpr::Negate(Box::new(DataExpr::Number(Number::Int(i64::MIN))));
+        assert!(
+            interp.eval_data_expr(&e2).is_err(),
+            "neg(i64::MIN) must error (checked_neg), not wrap"
+        );
+    }
+
+    #[test]
+    fn shared_golden_corpus_matches_lean() {
+        // EXACTLY mirrors the golden `example`s in jtv_proofs/JtvCore.lean —
+        // each (expr, σ, value) is pinned by `rfl` on the Lean side.
+        let lit = |n: i64| DataExpr::Number(Number::Int(n));
+        let var = |s: &str| DataExpr::Identifier(s.to_string());
+        let add = |a: DataExpr, b: DataExpr| DataExpr::Add(Box::new(a), Box::new(b));
+        let neg = |a: DataExpr| DataExpr::Negate(Box::new(a));
+
+        let cases: Vec<(DataExpr, HashMap<String, i64>, i64)> = vec![
+            (add(lit(2), lit(3)), HashMap::new(), 5),
+            (neg(lit(5)), HashMap::new(), -5),
+            (neg(add(lit(1), lit(2))), HashMap::new(), -3),
+            (add(neg(lit(2)), lit(5)), HashMap::new(), 3),
+            (
+                add(var("x"), lit(1)),
+                HashMap::from([("x".to_string(), 4i64)]),
+                5,
+            ),
+            (
+                add(var("x"), neg(var("x"))),
+                HashMap::from([("x".to_string(), 7i64)]),
+                0,
+            ),
+            (
+                add(add(var("x"), var("y")), lit(1)),
+                HashMap::from([("x".to_string(), 3i64), ("y".to_string(), 4i64)]),
+                8,
+            ),
+        ];
+
+        for (e, state, expected) in &cases {
+            let sigma: HashMap<String, i128> =
+                state.iter().map(|(k, v)| (k.clone(), *v as i128)).collect();
+            assert_eq!(
+                denot(e, &sigma),
+                Some(*expected as i128),
+                "denotational reference mismatch on {e:?}"
+            );
+            let mut interp = seed(state);
+            assert_eq!(
+                interp.eval_data_expr(e).unwrap(),
+                Value::Int(*expected),
+                "interpreter mismatch on {e:?}"
+            );
+        }
+    }
+}