feat(formal): real-lift R2-loops — backward jumps (Loop/Br/BrIf) + while simulation (settles #601)#665
Merged
Conversation
…(settles #601) Fourth rung of the real lift (formal/REAL-LIFT.adoc): structured control with **backward jumps**, and the source `while` whose lowering is proved correct — settling the #601 value-returning-tail question concretely. Axiom-free. Target IR (RealWasm.v): - adds the faithful lib/wasm.ml structured-control instructions `Block`, `Loop`, `Br k`, `BrIf k` to `instr` (+ dead `step1` arms). Zero blast radius: the proven `wexec` and `compile_correct` still compile unchanged. R2-loops (new file RealLoop.v): - the R2 executor `wexec : … → option (locals×stack)` cannot express "this code branched to label k", so it cannot run `Br`. R2-loops introduces a **branch-aware** executor `cexec` returning an `outcome` (`ONormal`/`OBranch k`/`OTrap`). It reuses the very same fuel device R2 used for forward control: a `Loop` consumed by `Br 0` re-enters by recursing with decremented fuel, so `cexec` stays a structural `Fixpoint` (definitional — `cbn`/`reflexivity`/demos still compute; a real countdown `while` evaluates by `reflexivity`). - `cexec_le_S`/`cexec_mono` (more fuel never changes a `Some`) + `cexec_app_normal` (additive sequencing when the prefix ends `Normal`). - mutual `instr`/`list instr` recursion is rejected by Coq's guard checker (list recursion only decreases on the spine), so instead of a `branchfree` predicate the R2 expression compiler is re-proved directly into `cexec`: `cexec_compile` (the `cexec` analogue of `compile_correct`). - source statements `SSkip`/`SSeq`/`SSet`/`SWhile` with a fuel-indexed reference `run_stmt` (+ `run_stmt_mono`, `run_stmt_length`) and a lowering `compile_stmt` taking `while` to `Block[Loop[<cond>;I32Eqz;BrIf 1;<body>; Br 0]]`. - `cexec_loop` — the loop-simulation lemma (induction on the while's fuel: cond-false unwinds with `OBranch 1`, caught by the Block; cond-true runs the body and re-enters via `OBranch 0`). - `compile_stmt_correct` — a terminating statement's lowering runs to the same locals, leaving the value stack **empty** (`cexec … = Some (ONormal lo' [])`). A `while` is a statement (unit tail); this is #601 settled concretely — the expression tail instead keeps its value on the stack. Whole formal/ track re-audited: **19 files, 33 `Print Assumptions` closure reports, all "Closed under the global context" — zero axioms, no Admitted.** Next rung **R-mem** (linear memory: load/store, tuples/arrays/records). (`for`/`break`/`continue` + a general source-divergence model reuse this cexec.) Refs REAL-LIFT.adoc, docs/PROOF-NEEDS.adoc (K-1 row), #601. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
|
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.
Fourth rung of the real lift (
formal/REAL-LIFT.adoc): structured control with backward jumps, and a sourcewhilewhose lowering is proved correct — settling the #601 value-returning-tail question concretely. Axiom-free throughout.What landed
Target IR (
RealWasm.v)lib/wasm.mlstructured-control instructionsBlock,Loop,Br k,BrIf ktoinstr(+ deadstep1arms). Zero blast radius — the provenwexecandRealCompile.compile_correctstill compile unchanged.R2-loops (new file
RealLoop.v)wexec : … → option (locals×stack)can't express "this code branched to label k", so it cannot runBr. R2-loops introduces a branch-aware executorcexecreturning anoutcome(ONormal/OBranch k/OTrap). It reuses the same fuel device R2 used for forward control: aLoopconsumed byBr 0re-enters by recursing with decremented fuel, socexecstays a structuralFixpoint— definitional, socbn/reflexivity/demos still compute (a real countdownwhileevaluates byreflexivity).cexec_le_S/cexec_mono(more fuel never changes aSome) +cexec_app_normal(additive sequencing when the prefix endsNormal).instr/list instrbranchfreepredicate is rejected by Coq's guard checker (list recursion only decreases on the spine), so instead of awexec→cexecbridge over a flag, the R2 expression compiler is re-proved directly intocexec:cexec_compile(thecexecanalogue ofcompile_correct).SSkip/SSeq/SSet/SWhilewith a fuel-indexed referencerun_stmt(+run_stmt_mono,run_stmt_length), and a loweringcompile_stmttakingwhiletoBlock[Loop[<cond>; I32Eqz; BrIf 1; <body>; Br 0]].cexec_loop— the loop-simulation lemma (induction on the while's fuel: cond-false unwinds withOBranch 1, caught by theBlock; cond-true runs the body and re-enters viaOBranch 0).compile_stmt_correct— a terminating statement's lowering runs to the same locals, leaving the value stack empty (cexec … = Some (ONormal lo' [])). Awhileis a statement (unit tail); this is Face transformers disagree on trailing-statement lowering —greetcompiles to 2 wasm classes #601 settled concretely — the expression tail would instead keep its value on the stack.Verification
coqc8.18, wholeformal/track re-audited against currentmain:Print Assumptionsreports, every one "Closed under the global context" — zero axioms, noAdmitted.Docs
formal/REAL-LIFT.adoc(R2 row + §5 hard-parts + §8 status),formal/README.adoc(RealLoop row + "real lift R0 → R2-loops"),docs/PROOF-NEEDS.adoc(counts 18→19 / 31→33, K-1 row)._CoqProject/justfile/.hypatia-ignorewireRealLoop.vin.Next
Rung R-mem (linear memory: load/store, tuples/arrays/records).
for/break/continueand a general source-divergence model reuse thiscexec.Refs
REAL-LIFT.adoc,docs/PROOF-NEEDS.adoc(K-1 row), #601.🤖 Generated with Claude Code
https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
Generated by Claude Code