diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 089a39e..ae62e25 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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, epi: Option } (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] diff --git a/crates/jtv-core/src/interpreter.rs b/crates/jtv-core/src/interpreter.rs index 448995d..9fad750 100644 --- a/crates/jtv-core/src/interpreter.rs +++ b/crates/jtv-core/src/interpreter.rs @@ -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) -> Option { + 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 { + let mut out: Vec = 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) -> 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> = 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 = + 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, 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 = + 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:?}" + ); + } + } +} diff --git a/jtv_proofs/JtvCore.lean b/jtv_proofs/JtvCore.lean index 387561f..1390827 100644 --- a/jtv_proofs/JtvCore.lean +++ b/jtv_proofs/JtvCore.lean @@ -165,3 +165,13 @@ example : evalExpr (Expr.add (Term.lit 2) (Term.lit 3)) State.empty = 5 := rfl example : evalDataExpr (DataExpr.add (DataExpr.lit 2) (DataExpr.lit 3)) State.empty = 5 := rfl example : evalDataExpr (DataExpr.neg (DataExpr.lit 5)) State.empty = -5 := rfl + +-- Shared "golden corpus": these exact (expr, σ, value) points are mirrored in +-- crates/jtv-core/src/interpreter.rs (mod denotational_correspondence), pinning +-- the interpreter ↔ model correspondence at concrete inputs in BOTH the Lean +-- denotational model and the Rust interpreter (PROOF-2 / gap-001). +example : evalDataExpr (DataExpr.neg (DataExpr.add (DataExpr.lit 1) (DataExpr.lit 2))) State.empty = -3 := rfl +example : evalDataExpr (DataExpr.add (DataExpr.neg (DataExpr.lit 2)) (DataExpr.lit 5)) State.empty = 3 := rfl +example : evalDataExpr (DataExpr.add (DataExpr.var "x") (DataExpr.lit 1)) (State.empty["x" ↦ 4]) = 5 := rfl +example : evalDataExpr (DataExpr.add (DataExpr.var "x") (DataExpr.neg (DataExpr.var "x"))) (State.empty["x" ↦ 7]) = 0 := rfl +example : evalDataExpr (DataExpr.add (DataExpr.add (DataExpr.var "x") (DataExpr.var "y")) (DataExpr.lit 1)) (State.empty["x" ↦ 3]["y" ↦ 4]) = 8 := rfl diff --git a/verification/PROOF-CAPABILITY-MATRIX.adoc b/verification/PROOF-CAPABILITY-MATRIX.adoc index 86873fa..7b86624 100644 --- a/verification/PROOF-CAPABILITY-MATRIX.adoc +++ b/verification/PROOF-CAPABILITY-MATRIX.adoc @@ -118,7 +118,7 @@ orthogonal to v2 — Echo is representation-agnostic.) | `injective_fibre_subsingleton` | JtvEcho | `verified` | `EchoSafe` ⇔ injective ⇔ recoverable. | `residue_lossy` | JtvEcho | `verified` | Structured loss is genuine and one-way. | `parser_correctness` | — | `absent` | Parser produces a valid AST. (PROOF-1, High.) -| `interpreter_correctness` | — | `partial` | Interpreter matches denotational semantics. (PROOF-2.) +| `interpreter_correctness` | JtvCore + interpreter.rs | `partial` | Rust `eval_data_expr` ↔ Lean `evalDataExpr` denotational correspondence over the integer fragment: exhaustive agreement on all height-≤2 expressions × 3 states (~12k cases), the i64 overflow boundary pinned, and a cross-side golden corpus (same points by `rfl` in `JtvCore.lean` and by assertion in `mod denotational_correspondence`). Open: full mechanised refinement + the extended surface. (PROOF-2.) | `wasm_compilation_correctness` | — | `absent` | WASM output matches semantics. (PROOF-3, Medium.) |=== @@ -147,9 +147,35 @@ Echo violation regardless of the variables' type bindings. the `echo-types` Agda library is the conceptual source/reference. The Agda↔Lean bridge is deferred to Phase 4 — grammar v2 is not blocked on a cross-prover bridge. +== Interpreter ↔ denotational-model correspondence (gap-001) + +The Lean `evalDataExpr` (the denotational model) and the Rust `eval_data_expr` +(the running interpreter) are tied together by a correspondence harness in +`crates/jtv-core/src/interpreter.rs` (`mod denotational_correspondence`): + +[cols="1,3"] +|=== +| `jtv_proofs/JtvCore.lean` | `crates/jtv-core/src/interpreter.rs` + +| `evalDataExpr` (lit / var / add / neg over `σ : String → Int`) | `denot` (the same four rules, re-encoded in `i128`) +| golden `example … := rfl` corpus | `shared_golden_corpus_matches_lean` (same points, by assertion) +| (ℤ is unbounded) | `overflow_is_the_correspondence_boundary` (i64 edge: `checked_add`/`checked_neg` error, never wrap) +|=== + +`interpreter_matches_denotational_model_on_int_fragment` exhaustively checks +*every* integer-fragment expression of height ≤ 2 across three states (~12k +cases) — turning "the interpreter matches the model" from a claim into a +checked property. Honest bound: integer fragment only, within i64 range, +exhaustive-up-to-depth (not a Lean-mechanised refinement of the evaluator). + == Outstanding proof work (sequenced in ALIGNMENT-AFFINESCRIPT.adoc) * PROOF-1 `parser_correctness` (High) — `absent`. -* PROOF-2 `interpreter_correctness` (High) — `partial`. +* PROOF-2 `interpreter_correctness` (High) — `partial`. Denotational + correspondence harness landed (integer fragment, exhaustive to height 2 + + overflow boundary + cross-side golden corpus). Remaining: lift to a + Lean-mechanised refinement of the Rust evaluator, and extend past the + integer fragment (strings / the carrier-distinct number systems / calls / + lists / tuples). * PROOF-3 `wasm_compilation_correctness` (Medium) — `absent`. * Echo: bridge value-level fibre classification to function-call echo (Phase 2).