From bc3ec784098c2c57fd494a822a7f635c8f695d93 Mon Sep 17 00:00:00 2001 From: hyperpolymath Date: Sun, 21 Jun 2026 17:40:04 +0000 Subject: [PATCH] =?UTF-8?q?feat(formal):=20real-lift=20R1=20=E2=80=94=20fi?= =?UTF-8?q?rst=20real=20=E2=9F=A6compile=20p=E2=9F=A7=20=3D=20=E2=9F=A6p?= =?UTF-8?q?=E2=9F=A7=20(RealCompile.v)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Climbs the REAL-LIFT ladder (formal/REAL-LIFT.adoc) from R0 to R1: the first mechanized codegen-preservation theorem on the REAL objects — the actual lib/wasm.ml instruction IR and the real (resolved) lib/ast.ml expression core — retiring the toy K1/K1Let on real objects. RealWasm.v (grown): adds locals (LocalGet/LocalSet) and the comparison ops I32Eq/I32LtS, threading a mutable locals store through wexec. wexec is refactored through a per-instruction step1 so the sequencing lemmas wexec_app/wexec_seq (which the preservation proof composes with) are one line each. wexec_sound is retained for the pure (no_local) fragment. RealCompile.v (new, R1): - source rexpr: the resolved int/bool/let/binary core of lib/ast.ml (de Bruijn LEVELS — name resolution is P-7; bool = 0/1, int = Z); - eval: the reference dynamic semantics (mirrors lib/interp.ml); - compile: lowers let to LocalSet into a pre-sized locals array (slot = binding depth; siblings reuse slots), mirroring lib/codegen.ml; - compile_correct: eval env e = Some v -> wexec (compile |env| e) locals st = Some (locals', v :: st), carrying an env<->locals agreement invariant with fresh-slot allocation and low-slot preservation through the induction; - compile_program_correct: runs a closed program from the zero-initialised array. All axiom-free (Print Assumptions: Closed under the global context). formal/ now 17 files, 29 closure reports. Wired into _CoqProject / justfile / .hypatia-ignore / README.adoc; REAL-LIFT.adoc (R1 landed, R2 next) + PROOF-NEEDS.adoc (K-1 row, section 6 Wave 3) updated. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- .hypatia-ignore | 2 + docs/PROOF-NEEDS.adoc | 32 ++++--- formal/README.adoc | 43 ++++++--- formal/REAL-LIFT.adoc | 40 +++++--- formal/RealCompile.v | 206 ++++++++++++++++++++++++++++++++++++++++++ formal/RealWasm.v | 191 +++++++++++++++++++++++++-------------- formal/_CoqProject | 1 + formal/justfile | 2 +- 8 files changed, 409 insertions(+), 108 deletions(-) create mode 100644 formal/RealCompile.v diff --git a/.hypatia-ignore b/.hypatia-ignore index f9ac6336..31bf50c1 100644 --- a/.hypatia-ignore +++ b/.hypatia-ignore @@ -82,3 +82,5 @@ cicd_rules/banned_language_file:formal/RealWasm.v # not a glob, so a new .v needs its own lines). cicd_rules/vlang_detected:formal/Rows.v cicd_rules/banned_language_file:formal/Rows.v +cicd_rules/vlang_detected:formal/RealCompile.v +cicd_rules/banned_language_file:formal/RealCompile.v diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index efa03811..a1e7e693 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -70,7 +70,7 @@ than the prose corpus suggests: `TypeSafety.v` is example lemmas about list length, not AffineScript. Not core-metatheory. * **`formal/`** — the directory #513 names as the mechanized-proof target now - **exists** (Coq/Rocq 8.18), axiom-free throughout — **16 files, 27 `Print + **exists** (Coq/Rocq 8.18), axiom-free throughout — **17 files, 29 `Print Assumptions` closure reports**, all "Closed under the global context". Codegen keystone: `K1_CodegenPreservation.v` (K-1 minimal) + `K1Let_CodegenPreservation.v` (K-1 grown with variables/`let`/environment). @@ -83,7 +83,9 @@ than the prose corpus suggests: Affine/QTT layer: `QttSemiring.v` (`{0,1,ω}`) + `AffineUsage.v` (`λx.x` affine, `λx. x x` not) + `QttTyping.v` (quantitative typing, `usage x t = Γ x` sound) + `QttDynamic.v` (the dynamic half: - β-reduction preserves the usage profile). See <>, <>. + β-reduction preserves the usage profile). Real lift (`REAL-LIFT.adoc`): + `RealWasm.v` (real `lib/wasm.ml` IR — i32 core + locals) + `RealCompile.v` + (R1: the first real `⟦compile p⟧ = ⟦p⟧`). See <>, <>. * **Research tracks** (not core soundness): `docs/academic/tropical-session-types/` (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`, `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue, @@ -223,11 +225,14 @@ The work in flight changes which obligations are *load-bearing* and which are fragment compiled to a stack machine — `K1Let_CodegenPreservation.v` grows it with de Bruijn variables, `let`, and an environment. The **real lift** onto the real AffineScript AST + real typed-WASM semantics is scoped in - `formal/REAL-LIFT.adoc` (fragment ladder R0→R-eff); its first stone is - **landed** — `formal/RealWasm.v` (R0) re-targets the *actual* `lib/wasm.ml` - `instr`/`value_type` with a stack-arity soundness theorem (checked code never - traps). R1 (real `RealAst`/`RealAstSem`/`RealCompile` for the int/bool/let - fragment) is the first real `⟦compile p⟧ = ⟦p⟧`. + `formal/REAL-LIFT.adoc` (fragment ladder R0→R-eff); **R0 + R1 landed**. + `formal/RealWasm.v` (R0) re-targets the *actual* `lib/wasm.ml` + `instr`/`value_type` (i32 core + locals) with a stack-arity soundness theorem; + `formal/RealCompile.v` (R1) gives the **first real `⟦compile p⟧ = ⟦p⟧`** — + resolved int/bool/`let`/binary source, reference `eval`, `compile` to real + wasm, `compile_correct` (env↔locals agreement) + `compile_program_correct`, + retiring `K1`/`K1Let` on real objects. R2 (structured control, fuel-indexed) is + next, and is the rung that settles #601 concretely. * **K-2 — Effect-soundness is *blocked*, not merely unproven.** P-6 cannot be honestly *stated against the current backend* because #555 drops handler arms on three of the codegen targets. The obligation must be split: (a) prove @@ -399,11 +404,14 @@ F-1 (full transformer preservation) is non-trivial rather than a formality. the **real typed-WASM operational semantics**, then re-prove K-1/F-1/F-2 against them (this is what makes K-1/F-1 `XL`, and what actually resolves #601). Planned as a strict-superset *fragment ladder* in `formal/REAL-LIFT.adoc` - (R0→R1→R2→R-mem→R-float→R-str→R-call→R-wrap→R-eff); **R0 landed** - (`formal/RealWasm.v` — real `lib/wasm.ml` IR, i32 core, arity soundness). Then - the still-`prose`/`absent` obligations: P-5 (inference), P-6 (effects — blocked - on #555/K-2, = rung R-eff), P-7 (resolution), P-8 (parser), P-10 (coherence); - faces F-6/F-7; full-language borrowing (P-3) pending #553. + (R0→R1→R2→R-mem→R-float→R-str→R-call→R-wrap→R-eff); **R0 + R1 landed** + (`formal/RealWasm.v` — real `lib/wasm.ml` IR, i32 core + locals; + `formal/RealCompile.v` — the first real `⟦compile p⟧ = ⟦p⟧`, retiring K1/K1Let + on real objects). **R2** (structured control, fuel-indexed) is next and settles + #601 concretely. Then the still-`prose`/`absent` obligations: P-5 (inference), + P-6 (effects — blocked on #555/K-2, = rung R-eff), P-7 (resolution), P-8 + (parser), P-10 (coherence); faces F-6/F-7; full-language borrowing (P-3) + pending #553. | Wave 2; #555; #553 |=== diff --git a/formal/README.adoc b/formal/README.adoc index 40bbffec..2c1473b6 100644 --- a/formal/README.adoc +++ b/formal/README.adoc @@ -96,8 +96,14 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires. | **mechanized**, axiom-free | `RealWasm.v` -| **Real lift R0** (`REAL-LIFT.adoc`) — the real `lib/wasm.ml` IR (i32 core): - `wexec` + arity checker + soundness (`wexec_sound`: checked code never traps) +| **Real lift R0+R1** (`REAL-LIFT.adoc`) — the real `lib/wasm.ml` IR: i32 core + + locals (`LocalGet`/`LocalSet`) + comparisons; `wexec`, `wexec_sound` +| **mechanized**, axiom-free + +| `RealCompile.v` +| **Real lift R1** — the first *real* `⟦compile p⟧ = ⟦p⟧`: resolved int/bool/`let` + source, reference `eval`, `compile` to real wasm, `compile_correct` (retires + K1/K1Let on real objects) | **mechanized**, axiom-free |=== @@ -220,17 +226,28 @@ the same canonical AST emit identical code). The observational version for the trailing-statement/tail split is mechanized separately in `invariant-path/proofs/SameCube.agda` (F-2). -== The real lift (R0) - -`RealWasm.v` is the first foundation stone of the *real lift* — replacing the -toy stack machine with the actual `lib/wasm.ml` IR. R0 covers the pure i32 -numeric core (real `instr` / `value_type` names), a stack-machine `wexec`, an -arity checker `wcheck`, and the soundness theorem `wexec_sound`: arity-checked -code never gets stuck — the target-side invariant the real K-1 preservation -proof rests on. The full plan — the fragment ladder R0 → R1 → R2 → R-mem → -R-float → R-str → R-call → R-wrap → R-eff, the Coq module structure, and the -strategy for each hard part (loops/termination, linear memory, floats, the -elaboration nodes, effects) — is `formal/REAL-LIFT.adoc`. +== The real lift (R0 → R1) + +The *real lift* replaces the toy stack machine with the actual `lib/wasm.ml` IR +and the toy source with the real (resolved) AST, climbing a strict-superset +fragment ladder. Two rungs are down: + +* **R0** (`RealWasm.v`) — the pure i32 numeric core (real `instr` / `value_type` + names), a stack-machine `wexec`, an arity checker `wcheck`, and `wexec_sound`: + arity-checked, local-free code never gets stuck. +* **R1** (`RealWasm.v` grown with **locals** + comparisons; `RealCompile.v`) — + the **first real `⟦compile p⟧ = ⟦p⟧`**. The source is the resolved + (de Bruijn-level) int/bool/`let`/binary core of `lib/ast.ml`; `eval` is the + reference semantics; `compile` lowers `let` to `LocalSet` into a pre-sized + locals array. `compile_correct` carries an env↔locals *agreement* invariant + with fresh-slot allocation and low-slot preservation through the induction; + `compile_program_correct` runs a closed program from the zero-initialised + array. This **retires `K1`/`K1Let` on real objects**. + +The full plan — the rest of the ladder (R2 → R-mem → R-float → R-str → R-call → +R-wrap → R-eff), the Coq module structure, and the strategy for each hard part +(loops/termination via fuel, linear memory, floats, the elaboration nodes, +effects) — is `formal/REAL-LIFT.adoc`. == Scope (honest) diff --git a/formal/REAL-LIFT.adoc b/formal/REAL-LIFT.adoc index 22af1efd..5c44bd56 100644 --- a/formal/REAL-LIFT.adoc +++ b/formal/REAL-LIFT.adoc @@ -126,16 +126,19 @@ arity-checked code never gets stuck). That is the first real foundation stone. | `RealAst.v` | The real source `expr`/`stmt`/`program` inductives (faithful to `lib/ast.ml`), - per-fragment. -| planned (S0) + per-fragment. (R1's `rexpr` core lives inline in `RealCompile.v`; split out as + the fragment grows.) +| R1 inline | `RealAstSem.v` | The reference dynamic semantics (mirrors `lib/interp.ml`), per-fragment. -| planned (S0) + (R1's `eval` lives inline in `RealCompile.v`.) +| R1 inline | `RealCompile.v` -| The real `compile` (port of `lib/codegen.ml`), per-fragment. -| planned (K-1/R1) +| The real `compile` (port of `lib/codegen.ml`) + (for R1) the source `rexpr` + core, reference `eval`, and the preservation theorem `compile_correct`. +| **R1 landed** | `RealPreservation.v` | `⟦compile p⟧ = ⟦p⟧` — the real K-1, per-fragment; then re-chains @@ -157,11 +160,14 @@ next. The rung names are stable references the `PROOF-NEEDS.adoc` rows will cite `wexec` + arity soundness. (`RealWasm.v`) | The toy stack machine's *target* — real names now. -| **R1** -| Source side S0+S1: `ExprLit`/`ExprVar`/`ExprLet`/`ExprBinary` (int/bool) → - `RealAst.v` + `RealAstSem.v`; `compile` for them (`RealCompile.v`); locals - (`LocalGet/Set/Tee`) + i64 in `RealWasm.v`. First real `⟦compile p⟧=⟦p⟧`. -| Subsumes **K1** and **K1Let** on real objects. +| **R1** ✅ +| Source `ExprLit`/`ExprVar`/`ExprLet`/`ExprBinary` (int/bool), resolved to + de Bruijn levels — `rexpr` + reference `eval` + `compile` + the preservation + theorem `compile_correct` (`RealCompile.v`); **locals** (`LocalGet`/`LocalSet`) + + comparison ops added to `RealWasm.v`. First real `⟦compile p⟧=⟦p⟧`, run from + the zero-initialised locals array (`compile_program_correct`). (`LocalTee`/i64 + fold in with R2/R-wrap.) +| **Subsumes K1 and K1Let on real objects.** | **R2** | Structured control: `Block/Loop/If/Br/BrIf/Return`; `ExprIf`/`ExprMatch`/ @@ -269,9 +275,15 @@ already has the front-end scaffolding (`F1_TransformerPreservation.v`, == 8. Status * **R0 landed** — `RealWasm.v`: real `instr`/`value_type` names, `wexec`, - `wcheck`, `wexec_sound` (arity-checked code never traps), axiom-free. -* Next: **R1** — stand up `RealAst.v` + `RealAstSem.v` + `RealCompile.v` for the - int/bool/let/binary fragment and prove the first real `⟦compile p⟧ = ⟦p⟧`, - adding locals + i64 to `RealWasm.v`. + `wcheck`, `wexec_sound` (arity-checked, local-free code never traps), axiom-free. +* **R1 landed** — `RealWasm.v` grown with **locals** (`LocalGet`/`LocalSet`) + + comparison ops; `RealCompile.v` gives the resolved int/bool/`let`/binary source + `rexpr`, the reference `eval`, the `compile` to real wasm, and the **first real + `⟦compile p⟧ = ⟦p⟧`** — `compile_correct` (env↔locals agreement, fresh-slot + allocation, low-slot preservation) + `compile_program_correct`. Axiom-free. + Retires `K1`/`K1Let` on real objects. +* Next: **R2** — structured control (`Block`/`Loop`/`If`/`Br`/`Return`, + `ExprIf`/`ExprMatch`/`while`) on a fuel-indexed `wexec`; this is the rung that + settles #601 concretely. Tracked against `docs/PROOF-NEEDS.adoc` §6 Wave 3 and #513. diff --git a/formal/RealCompile.v b/formal/RealCompile.v new file mode 100644 index 00000000..e97ad61b --- /dev/null +++ b/formal/RealCompile.v @@ -0,0 +1,206 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *) + +(* + RealCompile.v + ═════════════ + REAL-LIFT rung R1 (see formal/REAL-LIFT.adoc): the first **real** + ⟦compile p⟧ = ⟦p⟧, on the real RealWasm.v target IR. + + Source: the resolved (de Bruijn LEVEL) core of lib/ast.ml — integer/bool + literals (ExprLit), variables (ExprVar), let (ExprLet), and binary operators + (ExprBinary: + - * & | == <). de Bruijn levels are how lib/codegen.ml sees the + AST after lib/resolve.ml — name resolution itself is obligation P-7. Bool ≔ + 0/1, Int ≔ Z, so the single observable is Z. + + `eval` (mirrors lib/interp.ml) is the reference dynamic semantics. `compile` + (mirrors lib/codegen.ml) lowers `let` to `LocalSet d` into a pre-sized locals + array (slot = binding depth d; siblings reuse slots). The theorem + `compile_correct`: + + eval env e = Some v → agree env locals → d = |env| → enough slots → + wexec (compile d e) locals st = Some (locals', v :: st) + ∧ |locals'| = |locals| ∧ (low slots < d unchanged) + + and the closed-program corollary `compile_program_correct` runs it from the + zero-initialised locals array. This RETIRES the toy K1 / K1Let on REAL objects + — the target is RealWasm's actual lib/wasm.ml instruction names with mutable + locals, not an ad-hoc machine. Axiom-free, no Admitted. + + `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. +*) + +Require Import List. +Require Import ZArith. +Require Import PeanoNat. +Require Import Lia. +Require Import ASFormal.RealWasm. +Import ListNotations. + +(* ── source: the resolved R1 core of lib/ast.ml ───────────────────────────── *) +Inductive lit := LInt (z : Z) | LBool (b : bool). +Inductive bop := BAdd | BSub | BMul | BAnd | BOr | BEq | BLt. +Inductive rexpr := +| RLit (l : lit) +| RVar (i : nat) (* de Bruijn LEVEL: outermost binder = 0 *) +| RLet (e1 e2 : rexpr) (* let _ = e1 in e2 *) +| RBin (b : bop) (e1 e2 : rexpr). + +Definition lit_val (l : lit) : Z := + match l with LInt z => z | LBool b => if b then 1 else 0 end. + +Definition bop_val (b : bop) (a c : Z) : Z := + match b with + | BAdd => Z.add a c | BSub => Z.sub a c | BMul => Z.mul a c + | BAnd => Z.land a c | BOr => Z.lor a c + | BEq => if Z.eqb a c then 1 else 0 + | BLt => if Z.ltb a c then 1 else 0 + end. + +(* ── reference semantics (mirrors lib/interp.ml): env = level-indexed list ── *) +Fixpoint eval (env : list Z) (e : rexpr) : option Z := + match e with + | RLit l => Some (lit_val l) + | RVar i => nth_error env i + | RLet e1 e2 => + match eval env e1 with + | Some v1 => eval (env ++ [v1]) e2 + | None => None + end + | RBin b e1 e2 => + match eval env e1, eval env e2 with + | Some a, Some c => Some (bop_val b a c) + | _, _ => None + end + end. + +(* ── compiler (mirrors lib/codegen.ml): d = binding depth = next free slot ── *) +Definition bop_instr (b : bop) : instr := + match b with + | BAdd => I32Add | BSub => I32Sub | BMul => I32Mul + | BAnd => I32And | BOr => I32Or + | BEq => I32Eq | BLt => I32LtS + end. + +Fixpoint compile (d : nat) (e : rexpr) : list instr := + match e with + | RLit l => [I32Const (lit_val l)] + | RVar i => [LocalGet i] + | RLet e1 e2 => compile d e1 ++ [LocalSet d] ++ compile (S d) e2 + | RBin b e1 e2 => compile d e1 ++ compile d e2 ++ [bop_instr b] + end. + +(* max extra local slots e needs above its starting depth. *) +Fixpoint depth (e : rexpr) : nat := + match e with + | RLit _ | RVar _ => 0 + | RLet e1 e2 => Nat.max (depth e1) (S (depth e2)) + | RBin _ e1 e2 => Nat.max (depth e1) (depth e2) + end. + +(* the binop instruction realises bop_val on the (reversed) operand stack. *) +Lemma step1_bop : forall b lo v1 v2 t, + step1 (bop_instr b) lo (v2 :: v1 :: t) = Some (lo, bop_val b v1 v2 :: t). +Proof. destruct b; reflexivity. Qed. + +(* ── agreement: locals' first |env| slots hold env ────────────────────────── *) +Definition agree (env locals : list Z) : Prop := + forall i, i < length env -> nth_error locals i = nth_error env i. + +(* ── the preservation theorem ─────────────────────────────────────────────── *) +Lemma compile_correct : forall e env d locals st v, + eval env e = Some v -> + length env = d -> + agree env locals -> + d + depth e <= length locals -> + exists locals', + wexec (compile d e) locals st = Some (locals', v :: st) /\ + length locals' = length locals /\ + (forall i, i < d -> nth_error locals' i = nth_error locals i). +Proof. + induction e as [ l | i | e1 IH1 e2 IH2 | b e1 IH1 e2 IH2 ]; + intros env d locals st v Heval Hlen Hagree Hbound; cbn [depth] in Hbound. + - (* RLit *) + cbn in Heval. injection Heval as Hv; subst v. + exists locals. cbn [compile wexec step1]. + split; [reflexivity | split; [reflexivity | intros; reflexivity]]. + - (* RVar i *) + cbn in Heval. + assert (Hi : i < length env) by (apply nth_error_Some; rewrite Heval; discriminate). + exists locals. cbn [compile wexec step1]. + rewrite (Hagree i Hi), Heval. cbn. + split; [reflexivity | split; [reflexivity | intros; reflexivity]]. + - (* RLet e1 e2 *) + cbn in Heval. + destruct (eval env e1) as [v1|] eqn:Hev1; cbn in Heval; [| discriminate]. + destruct (IH1 env d locals st v1 Hev1 Hlen Hagree ltac:(lia)) + as [locals1 [Hw1 [Hlen1 Hlow1]]]. + assert (Hd : d < length locals1) by lia. + assert (Hag2 : agree (env ++ [v1]) (set_nth d v1 locals1)). + { intros j Hj. rewrite app_length in Hj; cbn in Hj. + destruct (Nat.eq_dec j d) as [->|Hjd]. + - rewrite set_nth_eq by lia. + rewrite nth_error_app2 by lia. rewrite Hlen, Nat.sub_diag. reflexivity. + - rewrite set_nth_neq by lia. rewrite Hlow1 by lia. + rewrite (Hagree j) by lia. rewrite nth_error_app1 by lia. reflexivity. } + destruct (IH2 (env ++ [v1]) (S d) (set_nth d v1 locals1) st v Heval + ltac:(rewrite app_length; cbn; lia) Hag2 + ltac:(rewrite set_nth_length; lia)) + as [locals2 [Hw2 [Hlen2 Hlow2]]]. + exists locals2. split; [| split]. + + apply wexec_seq with (lo1:=locals1) (st1:=v1::st); [exact Hw1|]. + apply wexec_seq with (lo1:=set_nth d v1 locals1) (st1:=st); [| exact Hw2]. + cbn [wexec step1]. + assert (Hltb : Nat.ltb d (length locals1) = true) by (apply Nat.ltb_lt; lia). + rewrite Hltb. reflexivity. + + rewrite Hlen2, set_nth_length. exact Hlen1. + + intros j Hj. rewrite Hlow2 by lia. rewrite set_nth_neq by lia. apply Hlow1; lia. + - (* RBin b e1 e2 *) + cbn in Heval. + destruct (eval env e1) as [v1|] eqn:Hev1; cbn in Heval; [| discriminate]. + destruct (eval env e2) as [v2|] eqn:Hev2; cbn in Heval; [| discriminate]. + injection Heval as Hv; subst v. + destruct (IH1 env d locals st v1 Hev1 Hlen Hagree ltac:(lia)) + as [locals1 [Hw1 [Hlen1 Hlow1]]]. + assert (Hag1 : agree env locals1). + { intros j Hj. rewrite Hlow1 by lia. apply Hagree; lia. } + destruct (IH2 env d locals1 (v1 :: st) v2 Hev2 Hlen Hag1 + ltac:(rewrite Hlen1; lia)) + as [locals2 [Hw2 [Hlen2 Hlow2]]]. + exists locals2. split; [| split]. + + apply wexec_seq with (lo1:=locals1) (st1:=v1::st); [exact Hw1|]. + apply wexec_seq with (lo1:=locals2) (st1:=v2::v1::st); [exact Hw2|]. + cbn [wexec]. rewrite step1_bop. reflexivity. + + rewrite Hlen2. exact Hlen1. + + intros j Hj. rewrite Hlow2 by lia. apply Hlow1; lia. +Qed. + +(* ── closed-program corollary ─────────────────────────────────────────────── *) +Corollary compile_program_correct : forall e v, + eval [] e = Some v -> + exists locals', + wexec (compile 0 e) (repeat 0%Z (depth e)) [] = Some (locals', [v]). +Proof. + intros e v Heval. + destruct (compile_correct e [] 0 (repeat 0%Z (depth e)) [] v Heval) + as [locals' [Hw _]]. + - reflexivity. + - intros i Hi; cbn in Hi; lia. + - rewrite repeat_length; lia. + - exists locals'; exact Hw. +Qed. + +(* concrete: let x = 2+3 in x*4 ⇒ 20, end-to-end. *) +Example r1_eval_demo : + eval [] (RLet (RBin BAdd (RLit (LInt 2)) (RLit (LInt 3))) + (RBin BMul (RVar 0) (RLit (LInt 4)))) = Some 20%Z. +Proof. reflexivity. Qed. + +Example r1_exec_demo : + wexec (compile 0 (RLet (RBin BAdd (RLit (LInt 2)) (RLit (LInt 3))) + (RBin BMul (RVar 0) (RLit (LInt 4))))) [0%Z] [] + = Some ([5%Z], [20%Z]). +Proof. reflexivity. Qed. + +Print Assumptions compile_correct. +Print Assumptions compile_program_correct. diff --git a/formal/RealWasm.v b/formal/RealWasm.v index 92c6c5e4..6f256b36 100644 --- a/formal/RealWasm.v +++ b/formal/RealWasm.v @@ -4,29 +4,20 @@ (* RealWasm.v ══════════ - The REAL-LIFT foundation stone (see formal/REAL-LIFT.adoc). - - The toy K-1 (K1_CodegenPreservation.v) compiles to an ad-hoc stack machine - invented for the proof. The real lift re-targets the *actual* compiler IR — - lib/wasm.ml's `instr` / `value_type` / `wasm_module`. This file begins that by - encoding the **R0 fragment**: the pure i32 numeric stack core, with the real - constructor names from lib/wasm.ml, a stack-machine evaluator `wexec`, a - stack-arity checker `wcheck`, and a soundness theorem — *arity-checked code - never gets stuck* (`wexec_sound`). This is the target-side invariant the real - K-1 preservation proof will rest on (a well-typed wasm body cannot trap on the - covered fragment). - - Scope of R0 (deliberately the smallest real slice; the ladder in - REAL-LIFT.adoc adds the rest): - * i32 only; i32 is modelled as `Z` — **wrap-around (mod 2^32) is deferred** - (milestone R-wrap). The constructor names and stack discipline are exact. - * No locals / memory / control / i64 / f64 yet (R1/R2/R-float milestones). - - `value_type` is given in full (faithful to lib/wasm.ml) even though R0's - evaluator only inhabits I32 — so later milestones extend, not rewrite, it. - - Axiom-free, no Admitted. `.v` is Coq, not V-lang — see formal/README.adoc and - .hypatia-ignore. + The REAL-LIFT target IR (see formal/REAL-LIFT.adoc). Grows across rungs. + + R0 — pure i32 numeric stack core (real lib/wasm.ml instr/value_type names), + stack-machine wexec, arity checker wcheck, soundness wexec_sound. + R1 — adds **locals** (LocalGet/LocalSet) and the comparison ops I32Eq/I32LtS, + threading a mutable locals store through wexec. wexec is refactored + through a per-instruction `step1`, so the append lemma `wexec_app` + (the sequencing lemma RealCompile.v's preservation proof composes with) + is one line. wexec_sound is retained for the **pure** (`no_local`) + fragment: arity-checked local-free code never traps and never touches + the locals. + + i32 ≔ Z (wrap deferred to rung R-wrap). Axiom-free, no Admitted. + `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. *) Require Import List. @@ -38,44 +29,107 @@ Import ListNotations. (* lib/wasm.ml `value_type` — full, faithful. *) Inductive value_type := I32 | I64 | F32 | F64. -(* R0 slice of lib/wasm.ml `instr`: the pure i32 numeric stack core. - Real names; i32 ≔ Z (wrap deferred). *) +(* R0 i32 core + R1 (comparisons + locals), real lib/wasm.ml names. *) Inductive instr := | I32Const (z : Z) | I32Add | I32Sub | I32Mul | I32And | I32Or | I32Xor +| I32Eq | I32LtS (* R1: comparisons *) | I32Eqz -| Drop. +| Drop +| LocalGet (i : nat) (* R1: locals *) +| LocalSet (i : nat). + +Definition stack := list Z. +Definition locals := list Z. + +(* set the i-th local (out of range ⇒ unchanged; callers stay in range). *) +Fixpoint set_nth (i : nat) (v : Z) (l : locals) : locals := + match i, l with + | O, _ :: r => v :: r + | S i', x :: r => x :: set_nth i' v r + | _, [] => [] + end. + +Lemma set_nth_length : forall i v l, length (set_nth i v l) = length l. +Proof. induction i; intros v l; destruct l; simpl; auto. Qed. + +Lemma set_nth_eq : forall i v l, i < length l -> nth_error (set_nth i v l) i = Some v. +Proof. + induction i; intros v l Hlt; destruct l; simpl in *; try lia. + - reflexivity. + - apply IHi; lia. +Qed. -Definition stack := list Z. +Lemma set_nth_neq : forall i j v l, i <> j -> nth_error (set_nth j v l) i = nth_error l i. +Proof. + induction i; intros j v l Hne; destruct j; destruct l; simpl; try reflexivity. + - contradiction. + - apply IHi; lia. +Qed. + +(* one-instruction step over (locals, stack). None = trap (underflow / oob). *) +Definition step1 (i : instr) (lo : locals) (st : stack) : option (locals * stack) := + match i with + | I32Const z => Some (lo, z :: st) + | I32Add => match st with a :: b :: t => Some (lo, Z.add b a :: t) | _ => None end + | I32Sub => match st with a :: b :: t => Some (lo, Z.sub b a :: t) | _ => None end + | I32Mul => match st with a :: b :: t => Some (lo, Z.mul b a :: t) | _ => None end + | I32And => match st with a :: b :: t => Some (lo, Z.land b a :: t) | _ => None end + | I32Or => match st with a :: b :: t => Some (lo, Z.lor b a :: t) | _ => None end + | I32Xor => match st with a :: b :: t => Some (lo, Z.lxor b a :: t) | _ => None end + | I32Eq => match st with a :: b :: t => Some (lo, (if Z.eqb b a then 1 else 0)%Z :: t) | _ => None end + | I32LtS => match st with a :: b :: t => Some (lo, (if Z.ltb b a then 1 else 0)%Z :: t) | _ => None end + | I32Eqz => match st with a :: t => Some (lo, (if Z.eqb a 0 then 1 else 0)%Z :: t) | _ => None end + | Drop => match st with _ :: t => Some (lo, t) | _ => None end + | LocalGet k => match nth_error lo k with Some v => Some (lo, v :: st) | None => None end + | LocalSet k => match st with + | v :: t => if Nat.ltb k (length lo) then Some (set_nth k v lo, t) else None + | [] => None + end + end. -(* Big-step stack-machine evaluator. None = stuck (stack underflow). *) -Fixpoint wexec (is : list instr) (st : stack) : option stack := +Fixpoint wexec (is : list instr) (lo : locals) (st : stack) : option (locals * stack) := match is with - | [] => Some st - | I32Const z :: r => wexec r (z :: st) - | I32Add :: r => match st with a :: b :: t => wexec r (Z.add b a :: t) | _ => None end - | I32Sub :: r => match st with a :: b :: t => wexec r (Z.sub b a :: t) | _ => None end - | I32Mul :: r => match st with a :: b :: t => wexec r (Z.mul b a :: t) | _ => None end - | I32And :: r => match st with a :: b :: t => wexec r (Z.land b a :: t) | _ => None end - | I32Or :: r => match st with a :: b :: t => wexec r (Z.lor b a :: t) | _ => None end - | I32Xor :: r => match st with a :: b :: t => wexec r (Z.lxor b a :: t) | _ => None end - | I32Eqz :: r => match st with a :: t => wexec r ((if Z.eqb a 0 then 1%Z else 0%Z) :: t) | _ => None end - | Drop :: r => match st with _ :: t => wexec r t | _ => None end + | [] => Some (lo, st) + | i :: r => match step1 i lo st with + | Some (lo', st') => wexec r lo' st' + | None => None + end end. -(* Stack-arity discipline (a degenerate wasm validation: track the i32 count). *) +(* sequencing — the lemma the preservation proof composes with. *) +Lemma wexec_app : forall is1 is2 lo st, + wexec (is1 ++ is2) lo st = + match wexec is1 lo st with Some (lo', st') => wexec is2 lo' st' | None => None end. +Proof. + induction is1 as [| i r IH]; intros is2 lo st; simpl. + - reflexivity. + - destruct (step1 i lo st) as [[lo' st']|]; [apply IH | reflexivity]. +Qed. + +(* the run-then-run composition, in the shape the preservation proof applies. *) +Lemma wexec_seq : forall is1 is2 lo st lo1 st1 lo2 st2, + wexec is1 lo st = Some (lo1, st1) -> + wexec is2 lo1 st1 = Some (lo2, st2) -> + wexec (is1 ++ is2) lo st = Some (lo2, st2). +Proof. intros. rewrite wexec_app, H. exact H0. Qed. + +(* ── arity discipline (degenerate validation: i32 stack height) ──────────── *) Definition consumes (i : instr) : nat := match i with | I32Const _ => 0 - | I32Add | I32Sub | I32Mul | I32And | I32Or | I32Xor => 2 + | LocalGet _ => 0 + | I32Add | I32Sub | I32Mul | I32And | I32Or | I32Xor | I32Eq | I32LtS => 2 | I32Eqz => 1 | Drop => 1 + | LocalSet _ => 1 end. Definition produces (i : instr) : nat := match i with | Drop => 0 + | LocalSet _ => 0 | _ => 1 end. @@ -88,40 +142,41 @@ Fixpoint wcheck (is : list instr) (n : nat) : option nat := else None end. -(* ── soundness: arity-checked code never gets stuck ─────────────────────── - If the body checks from height n to height m, then on any stack of height n - it runs to Some stack of height m. The target invariant the real K-1 needs. *) -Theorem wexec_sound : forall is n m st, - wcheck is n = Some m -> length st = n -> - exists st', wexec is st = Some st' /\ length st' = m. +(* the pure (local-free) fragment. *) +Fixpoint no_local (is : list instr) : Prop := + match is with + | [] => True + | LocalGet _ :: _ => False + | LocalSet _ :: _ => False + | _ :: r => no_local r + end. + +(* ── soundness: arity-checked, local-free code never traps ───────────────── + (and never touches the locals). The target invariant for the pure core; the + locals-using case is covered operationally + by RealCompile.v's preservation. *) +Theorem wexec_sound : forall is n m lo st, + wcheck is n = Some m -> length st = n -> no_local is -> + exists st', wexec is lo st = Some (lo, st') /\ length st' = m. Proof. - induction is as [| i r IH]; intros n m st Hchk Hlen; cbn in Hchk. + induction is as [| i r IH]; intros n m lo st Hchk Hlen Hnl; cbn in Hchk. - injection Hchk as <-. exists st. split; [reflexivity | exact Hlen]. - destruct (Nat.leb (consumes i) n) eqn:Hle; [| discriminate]. apply Nat.leb_le in Hle. - destruct i; cbn in Hchk, Hle |- *. - + (* I32Const *) eapply IH; [exact Hchk |]. cbn. lia. - + (* I32Add *) destruct st as [| a [| b t]]; cbn in Hlen; try (exfalso; lia). - eapply IH; [exact Hchk |]. cbn in Hlen |- *; lia. - + (* I32Sub *) destruct st as [| a [| b t]]; cbn in Hlen; try (exfalso; lia). - eapply IH; [exact Hchk |]. cbn in Hlen |- *; lia. - + (* I32Mul *) destruct st as [| a [| b t]]; cbn in Hlen; try (exfalso; lia). - eapply IH; [exact Hchk |]. cbn in Hlen |- *; lia. - + (* I32And *) destruct st as [| a [| b t]]; cbn in Hlen; try (exfalso; lia). - eapply IH; [exact Hchk |]. cbn in Hlen |- *; lia. - + (* I32Or *) destruct st as [| a [| b t]]; cbn in Hlen; try (exfalso; lia). - eapply IH; [exact Hchk |]. cbn in Hlen |- *; lia. - + (* I32Xor *) destruct st as [| a [| b t]]; cbn in Hlen; try (exfalso; lia). - eapply IH; [exact Hchk |]. cbn in Hlen |- *; lia. - + (* I32Eqz *) destruct st as [| a t]; cbn in Hlen; try (exfalso; lia). - eapply IH; [exact Hchk |]. cbn in Hlen |- *; lia. - + (* Drop *) destruct st as [| a t]; cbn in Hlen; try (exfalso; lia). - eapply IH; [exact Hchk |]. cbn in Hlen |- *; lia. + destruct i; cbn in Hchk, Hle, Hnl |- *; + try contradiction; + try (eapply IH; [exact Hchk | cbn; lia | exact Hnl]). + all: destruct st as [| a [| b t]]; cbn in Hlen |- *; + try (exfalso; lia); + (eapply IH; [exact Hchk | cbn in Hlen |- *; lia | exact Hnl]). Qed. -(* A concrete sanity check: (2 + 3) * 4 evaluates to [20], and it arity-checks. *) +(* concrete sanity checks. *) Example wexec_demo : - wexec [I32Const 2; I32Const 3; I32Add; I32Const 4; I32Mul] [] = Some [20%Z]. + wexec [I32Const 2; I32Const 3; I32Add; I32Const 4; I32Mul] [] [] = Some ([], [20%Z]). +Proof. reflexivity. Qed. + +Example wexec_local_demo : + wexec [I32Const 7; LocalSet 0; LocalGet 0] [0%Z] [] = Some ([7%Z], [7%Z]). Proof. reflexivity. Qed. Example wcheck_demo : diff --git a/formal/_CoqProject b/formal/_CoqProject index a9457476..6b332769 100644 --- a/formal/_CoqProject +++ b/formal/_CoqProject @@ -15,3 +15,4 @@ QttTyping.v QttDynamic.v F5_RenderFaithful.v RealWasm.v +RealCompile.v diff --git a/formal/justfile b/formal/justfile index 11c09e0e..4d78562b 100644 --- a/formal/justfile +++ b/formal/justfile @@ -13,7 +13,7 @@ check: F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \ P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc \ QttSemiring AffineUsage QttTyping QttDynamic \ - F5_RenderFaithful RealWasm; do + F5_RenderFaithful RealWasm RealCompile; do echo "== coqc $f.v ==" o="$(coqc -Q . ASFormal "$f.v")" printf '%s\n' "$o"