feat(formal): real-lift R2 — structured conditionals (fuel-indexed wexec)#664
Merged
Conversation
…xec)
Third rung of the real lift (formal/REAL-LIFT.adoc). Adds structured
control to the real target IR and source core, and proves the
compiler-correctness simulation still holds across a conditional.
Target IR (RealWasm.v):
- new instr `IfElse (thn els : list instr)` = lib/wasm.ml's `If` minus
the block_type validation annotation.
- because `instr` now nests `list instr`, a *structural* `wexec` is
rejected by Coq's guard checker ("cannot guess decreasing argument";
the recursive call descends into a branch sub-list, not the tail).
So `wexec` becomes **fuel-indexed** (decreasing on a `nat`), exactly as
REAL-LIFT.adoc anticipated for R2. Fuel keeps definitional computation,
so `cbn`/`reflexivity`/the demos still evaluate.
- fuel breaks the old one-line `wexec_seq` (per-cons decrement means
`wexec (is1++is2) != wexec is2 . wexec is1`). Recovered with:
* wexec_le_S / wexec_mono — more fuel never loses a Some result;
* wexec_app_some — additive sequencing: f1 on is1 then f2 on is2
gives f1+f2 on is1++is2 (the fuel-world replacement for wexec_seq);
* wexec_S_cons / wexec_ifelse — one-step unfold lemmas (by
reflexivity) used via rewrite to stop cbn over-reducing the
IfElse branch run.
Source core (RealCompile.v):
- new `RIf (c thn els : rexpr)`; eval branches on Z.eqb vc 0; compile
emits `compile c ++ [IfElse (compile thn) (compile els)]`.
- compile_correct restated **existential-in-fuel**:
exists fuel locals', wexec fuel (compile d e) locals st
= Some (locals', v :: st) /\ ...
(env<->locals agreement + low-slot preservation unchanged). The RIf
case opens with `change (compile d (RIf ...)) with (... ++ [IfElse ...])`
to expose the `++` while keeping the inner compiles named, then
discharges via wexec_app_some + wexec_le_S.
- wexec_sound retired in this fuel refactor — it was a convenience
soundness restatement, not load-bearing for compile_correct.
Whole formal/ track re-audited: zero axioms, no Admitted
(`Print Assumptions` closed under the global context for every closure).
Next sub-rung R2-loops (Loop/Br + while/for, reusing the fuel device;
settles the value-returning-tail question behind #601).
Refs REAL-LIFT.adoc, docs/PROOF-NEEDS.adoc (K-1 row).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…ile simulation (settles #601) (#665) Fourth rung of the real lift (`formal/REAL-LIFT.adoc`): **structured control with backward jumps**, and a source `while` whose lowering is proved correct — settling the **#601** value-returning-tail question concretely. Axiom-free throughout. > Branch note: pushed to `claude/lucid-cray-4a22dp-r2loops` rather than `claude/lucid-cray-4a22dp` — the latter is still present at the merged #664 tip and is now protected against direct pushes (force/ff/delete all blocked), so a fresh branch was the only push path. Diff is against current `main` (post-#664), so it shows **only** the R2-loops changes. ## What landed **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 `RealCompile.compile_correct` still compile unchanged. **R2-loops (new file `RealLoop.v`)** - The R2 executor `wexec : … → option (locals×stack)` can't 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 *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, so `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`). - A *mutual* `instr`/`list instr` `branchfree` predicate is **rejected by Coq's guard checker** (list recursion only decreases on the spine), so instead of a `wexec→cexec` bridge over a flag, 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 would instead keep its value on the stack. ## Verification `coqc` 8.18, whole `formal/` track re-audited against current `main`: - **19 files compile**, **33 `Print Assumptions` reports**, every one *"Closed under the global context"* — **zero axioms, no `Admitted`**. ## 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-ignore` wire `RealLoop.v` in. ## Next Rung **R-mem** (linear memory: load/store, tuples/arrays/records). `for`/`break`/`continue` and a general source-divergence model reuse this `cexec`. Refs `REAL-LIFT.adoc`, `docs/PROOF-NEEDS.adoc` (K-1 row), #601. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- _Generated by [Claude Code](https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr)_ Co-authored-by: Claude <noreply@anthropic.com>
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.
Third rung of the real lift (
formal/REAL-LIFT.adoc). Adds structured control to the real target IR + source core, and shows the compiler-correctness simulation still holds across a conditional. Axiom-free throughout.What landed
Target IR (
formal/RealWasm.v)IfElse (thn els : list instr)—lib/wasm.ml'sIfminus theblock_typevalidation annotation.instrnow nestslist instr, a structuralwexecis rejected by Coq's guard checker ("cannot guess decreasing argument" — the recursive call descends into a branch sub-list, not the tail). Sowexecbecomes fuel-indexed (decreasing on anat), exactly asREAL-LIFT.adocanticipated for R2. Fuel keeps definitional computation, socbn/reflexivity/ the demos still evaluate.wexec_seq(per-cons decrement ⇒wexec (is1++is2) ≠ wexec is2 ∘ wexec is1). Recovered with:wexec_le_S/wexec_mono— more fuel never loses aSomeresult;wexec_app_some— additive sequencing: runis1withf1, thenis2withf2, getis1++is2withf1+f2(the fuel-world replacement forwexec_seq);wexec_S_cons/wexec_ifelse— one-step unfold lemmas (byreflexivity) used viarewritesocbndoesn't over-reduce theIfElsebranch run.Source core (
formal/RealCompile.v)RIf (c thn els : rexpr);evalbranches onZ.eqb vc 0;compileemitscompile c ++ [IfElse (compile thn) (compile els)].compile_correctrestated existential-in-fuel:exists fuel locals', wexec fuel (compile d e) locals st = Some (locals', v :: st) /\ …(env↔locals agreement + low-slot preservation unchanged). The
RIfcase opens withchange (compile d (RIf …)) with (… ++ [IfElse …])to expose the++while keeping inner compiles named, then discharges viawexec_app_some+wexec_le_S.wexec_soundretired in this fuel refactor — it was a convenience soundness restatement, not load-bearing forcompile_correct.Verification
coqc8.18, wholeformal/track re-audited after rebasing onto currentmain(incl. #648's now-wiredRows.v):Print Assumptionsreports, every one "Closed under the global context" — zero axioms, noAdmitted.Docs
formal/REAL-LIFT.adoc(R2 row + nested-control section),formal/README.adoc(RealWasm/RealCompile rows + "The real lift (R0 → R2)"),docs/PROOF-NEEDS.adoc(K-1 row) updated. Conflict-resolved cleanly against #648 (Rows.v / P-11) and #658 (licence normalisation).Next
Sub-rung R2-loops (
Loop/Br+ while/for, reusing the fuel device; settles the value-returning-tail question behind #601), then R-mem / R-float / R-str / … performal/REAL-LIFT.adoc.Refs
REAL-LIFT.adoc,docs/PROOF-NEEDS.adoc(K-1 row).🤖 Generated with Claude Code
https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr
Generated by Claude Code