proof(interp): denotational correspondence harness for eval_data_expr (PROOF-2 / gap-001)#55
Merged
Merged
Conversation
… (PROOF-2 / gap-001) Ties the Lean denotational model `evalDataExpr` (JtvCore.lean) to 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 `mod denotational_correspondence`: - `denot` re-encodes the four Lean rules in i128. - `interpreter_matches_denotational_model_on_int_fragment` exhaustively checks every height-≤2 integer-fragment expression (7 leaves → 4039 exprs) across 3 states (~12k cases): interpreter == denot on all. - `overflow_is_the_correspondence_boundary` pins that `Value::Int` is i64 with checked_add/checked_neg → it errors at the i64 edge, never wraps (Lean ℤ is unbounded, so correspondence holds exactly within i64 range). - `shared_golden_corpus_matches_lean` mirrors 7 concrete (expr, σ, value) points that are ALSO pinned by `rfl` in JtvCore.lean (cross-side anchor). JtvCore.lean gains 5 golden `example`s (State.empty[x ↦ v] updates, all rfl). Honest bound: integer fragment only; 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 + full workspace green), fmt + clippy -D clean, full lake build exit 0, 0 sorry/admit/axiom, 0 True-typed theorems. Docs: PROOF-CAPABILITY-MATRIX (interpreter_correctness row + new correspondence section + outstanding bullet), gap-001 marked partial in STATE.a2ml. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742
hyperpolymath
marked this pull request as ready for review
June 21, 2026 06:52
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Establishes a denotational correspondence between the Lean model and the running Rust interpreter — the first real wiring for PROOF-2 /
gap-001(proofs validate models, not the implementation).Bridges Lean
evalDataExpr(jtv_proofs/JtvCore.lean) ↔ Rusteval_data_expr(crates/jtv-core/src/interpreter.rs) over the integer fragment the model covers:lit | var | add | negoverσ : String → Int.Harness (
mod denotational_correspondencein interpreter.rs)denot— re-encodes the four Lean rules exactly, ini128.interpreter_matches_denotational_model_on_int_fragment— exhaustively enumerates every height-≤2 integer-fragment expression (7 leaves → 4039 exprs) across 3 states (~12k cases) and assertsinterpreter == denoton all of them. Turns "the interpreter matches the model" from a claim into a checked property.overflow_is_the_correspondence_boundary— pins thatValue::Intis i64 withchecked_add/checked_neg, so it errors at the i64 edge, never wraps; since Lean ℤ is unbounded, correspondence holds exactly within i64 range.shared_golden_corpus_matches_lean— 7 concrete(expr, σ, value)points mirrored on both sides: pinned byrflinJtvCore.lean(5 newexamples usingState.empty[x ↦ v]) and by assertion in Rust.Honest bound
Integer fragment only (strings / float / rational / complex / calls / lists / tuples are outside the model); within i64 range; exhaustive-up-to-depth, not a Lean-mechanised refinement of the Rust evaluator (that is the deeper PROOF-2 rung). Documented in-code and in the matrix.
Verification (local)
cargo test --workspacegreen (lib 142 → 145, +3 new)cargo fmt --all --checkclean;cargo clippy --workspace --all-targetsclean (-D warnings)lake buildexit 0;0 sorry/admit/axiom;0 True-typed theoremsDocs
PROOF-CAPABILITY-MATRIX.adoc—interpreter_correctnessrow updated (nowJtvCore + interpreter.rs, still honestlypartial), new "Interpreter ↔ denotational-model correspondence" section, outstanding-work bullet.gap-001marked partial inSTATE.a2ml.🤖 Generated with Claude Code
Generated by Claude Code