|
| 1 | +(* SPDX-License-Identifier: MPL-2.0 *) |
| 2 | +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *) |
| 3 | + |
| 4 | +(* |
| 5 | + RealCompile.v |
| 6 | + ═════════════ |
| 7 | + REAL-LIFT rung R1 (see formal/REAL-LIFT.adoc): the first **real** |
| 8 | + ⟦compile p⟧ = ⟦p⟧, on the real RealWasm.v target IR. |
| 9 | +
|
| 10 | + Source: the resolved (de Bruijn LEVEL) core of lib/ast.ml — integer/bool |
| 11 | + literals (ExprLit), variables (ExprVar), let (ExprLet), and binary operators |
| 12 | + (ExprBinary: + - * & | == <). de Bruijn levels are how lib/codegen.ml sees the |
| 13 | + AST after lib/resolve.ml — name resolution itself is obligation P-7. Bool ≔ |
| 14 | + 0/1, Int ≔ Z, so the single observable is Z. |
| 15 | +
|
| 16 | + `eval` (mirrors lib/interp.ml) is the reference dynamic semantics. `compile` |
| 17 | + (mirrors lib/codegen.ml) lowers `let` to `LocalSet d` into a pre-sized locals |
| 18 | + array (slot = binding depth d; siblings reuse slots). The theorem |
| 19 | + `compile_correct`: |
| 20 | +
|
| 21 | + eval env e = Some v → agree env locals → d = |env| → enough slots → |
| 22 | + wexec (compile d e) locals st = Some (locals', v :: st) |
| 23 | + ∧ |locals'| = |locals| ∧ (low slots < d unchanged) |
| 24 | +
|
| 25 | + and the closed-program corollary `compile_program_correct` runs it from the |
| 26 | + zero-initialised locals array. This RETIRES the toy K1 / K1Let on REAL objects |
| 27 | + — the target is RealWasm's actual lib/wasm.ml instruction names with mutable |
| 28 | + locals, not an ad-hoc machine. Axiom-free, no Admitted. |
| 29 | +
|
| 30 | + `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. |
| 31 | +*) |
| 32 | + |
| 33 | +Require Import List. |
| 34 | +Require Import ZArith. |
| 35 | +Require Import PeanoNat. |
| 36 | +Require Import Lia. |
| 37 | +Require Import ASFormal.RealWasm. |
| 38 | +Import ListNotations. |
| 39 | + |
| 40 | +(* ── source: the resolved R1 core of lib/ast.ml ───────────────────────────── *) |
| 41 | +Inductive lit := LInt (z : Z) | LBool (b : bool). |
| 42 | +Inductive bop := BAdd | BSub | BMul | BAnd | BOr | BEq | BLt. |
| 43 | +Inductive rexpr := |
| 44 | +| RLit (l : lit) |
| 45 | +| RVar (i : nat) (* de Bruijn LEVEL: outermost binder = 0 *) |
| 46 | +| RLet (e1 e2 : rexpr) (* let _ = e1 in e2 *) |
| 47 | +| RBin (b : bop) (e1 e2 : rexpr). |
| 48 | + |
| 49 | +Definition lit_val (l : lit) : Z := |
| 50 | + match l with LInt z => z | LBool b => if b then 1 else 0 end. |
| 51 | + |
| 52 | +Definition bop_val (b : bop) (a c : Z) : Z := |
| 53 | + match b with |
| 54 | + | BAdd => Z.add a c | BSub => Z.sub a c | BMul => Z.mul a c |
| 55 | + | BAnd => Z.land a c | BOr => Z.lor a c |
| 56 | + | BEq => if Z.eqb a c then 1 else 0 |
| 57 | + | BLt => if Z.ltb a c then 1 else 0 |
| 58 | + end. |
| 59 | + |
| 60 | +(* ── reference semantics (mirrors lib/interp.ml): env = level-indexed list ── *) |
| 61 | +Fixpoint eval (env : list Z) (e : rexpr) : option Z := |
| 62 | + match e with |
| 63 | + | RLit l => Some (lit_val l) |
| 64 | + | RVar i => nth_error env i |
| 65 | + | RLet e1 e2 => |
| 66 | + match eval env e1 with |
| 67 | + | Some v1 => eval (env ++ [v1]) e2 |
| 68 | + | None => None |
| 69 | + end |
| 70 | + | RBin b e1 e2 => |
| 71 | + match eval env e1, eval env e2 with |
| 72 | + | Some a, Some c => Some (bop_val b a c) |
| 73 | + | _, _ => None |
| 74 | + end |
| 75 | + end. |
| 76 | + |
| 77 | +(* ── compiler (mirrors lib/codegen.ml): d = binding depth = next free slot ── *) |
| 78 | +Definition bop_instr (b : bop) : instr := |
| 79 | + match b with |
| 80 | + | BAdd => I32Add | BSub => I32Sub | BMul => I32Mul |
| 81 | + | BAnd => I32And | BOr => I32Or |
| 82 | + | BEq => I32Eq | BLt => I32LtS |
| 83 | + end. |
| 84 | + |
| 85 | +Fixpoint compile (d : nat) (e : rexpr) : list instr := |
| 86 | + match e with |
| 87 | + | RLit l => [I32Const (lit_val l)] |
| 88 | + | RVar i => [LocalGet i] |
| 89 | + | RLet e1 e2 => compile d e1 ++ [LocalSet d] ++ compile (S d) e2 |
| 90 | + | RBin b e1 e2 => compile d e1 ++ compile d e2 ++ [bop_instr b] |
| 91 | + end. |
| 92 | + |
| 93 | +(* max extra local slots e needs above its starting depth. *) |
| 94 | +Fixpoint depth (e : rexpr) : nat := |
| 95 | + match e with |
| 96 | + | RLit _ | RVar _ => 0 |
| 97 | + | RLet e1 e2 => Nat.max (depth e1) (S (depth e2)) |
| 98 | + | RBin _ e1 e2 => Nat.max (depth e1) (depth e2) |
| 99 | + end. |
| 100 | + |
| 101 | +(* the binop instruction realises bop_val on the (reversed) operand stack. *) |
| 102 | +Lemma step1_bop : forall b lo v1 v2 t, |
| 103 | + step1 (bop_instr b) lo (v2 :: v1 :: t) = Some (lo, bop_val b v1 v2 :: t). |
| 104 | +Proof. destruct b; reflexivity. Qed. |
| 105 | + |
| 106 | +(* ── agreement: locals' first |env| slots hold env ────────────────────────── *) |
| 107 | +Definition agree (env locals : list Z) : Prop := |
| 108 | + forall i, i < length env -> nth_error locals i = nth_error env i. |
| 109 | + |
| 110 | +(* ── the preservation theorem ─────────────────────────────────────────────── *) |
| 111 | +Lemma compile_correct : forall e env d locals st v, |
| 112 | + eval env e = Some v -> |
| 113 | + length env = d -> |
| 114 | + agree env locals -> |
| 115 | + d + depth e <= length locals -> |
| 116 | + exists locals', |
| 117 | + wexec (compile d e) locals st = Some (locals', v :: st) /\ |
| 118 | + length locals' = length locals /\ |
| 119 | + (forall i, i < d -> nth_error locals' i = nth_error locals i). |
| 120 | +Proof. |
| 121 | + induction e as [ l | i | e1 IH1 e2 IH2 | b e1 IH1 e2 IH2 ]; |
| 122 | + intros env d locals st v Heval Hlen Hagree Hbound; cbn [depth] in Hbound. |
| 123 | + - (* RLit *) |
| 124 | + cbn in Heval. injection Heval as Hv; subst v. |
| 125 | + exists locals. cbn [compile wexec step1]. |
| 126 | + split; [reflexivity | split; [reflexivity | intros; reflexivity]]. |
| 127 | + - (* RVar i *) |
| 128 | + cbn in Heval. |
| 129 | + assert (Hi : i < length env) by (apply nth_error_Some; rewrite Heval; discriminate). |
| 130 | + exists locals. cbn [compile wexec step1]. |
| 131 | + rewrite (Hagree i Hi), Heval. cbn. |
| 132 | + split; [reflexivity | split; [reflexivity | intros; reflexivity]]. |
| 133 | + - (* RLet e1 e2 *) |
| 134 | + cbn in Heval. |
| 135 | + destruct (eval env e1) as [v1|] eqn:Hev1; cbn in Heval; [| discriminate]. |
| 136 | + destruct (IH1 env d locals st v1 Hev1 Hlen Hagree ltac:(lia)) |
| 137 | + as [locals1 [Hw1 [Hlen1 Hlow1]]]. |
| 138 | + assert (Hd : d < length locals1) by lia. |
| 139 | + assert (Hag2 : agree (env ++ [v1]) (set_nth d v1 locals1)). |
| 140 | + { intros j Hj. rewrite app_length in Hj; cbn in Hj. |
| 141 | + destruct (Nat.eq_dec j d) as [->|Hjd]. |
| 142 | + - rewrite set_nth_eq by lia. |
| 143 | + rewrite nth_error_app2 by lia. rewrite Hlen, Nat.sub_diag. reflexivity. |
| 144 | + - rewrite set_nth_neq by lia. rewrite Hlow1 by lia. |
| 145 | + rewrite (Hagree j) by lia. rewrite nth_error_app1 by lia. reflexivity. } |
| 146 | + destruct (IH2 (env ++ [v1]) (S d) (set_nth d v1 locals1) st v Heval |
| 147 | + ltac:(rewrite app_length; cbn; lia) Hag2 |
| 148 | + ltac:(rewrite set_nth_length; lia)) |
| 149 | + as [locals2 [Hw2 [Hlen2 Hlow2]]]. |
| 150 | + exists locals2. split; [| split]. |
| 151 | + + apply wexec_seq with (lo1:=locals1) (st1:=v1::st); [exact Hw1|]. |
| 152 | + apply wexec_seq with (lo1:=set_nth d v1 locals1) (st1:=st); [| exact Hw2]. |
| 153 | + cbn [wexec step1]. |
| 154 | + assert (Hltb : Nat.ltb d (length locals1) = true) by (apply Nat.ltb_lt; lia). |
| 155 | + rewrite Hltb. reflexivity. |
| 156 | + + rewrite Hlen2, set_nth_length. exact Hlen1. |
| 157 | + + intros j Hj. rewrite Hlow2 by lia. rewrite set_nth_neq by lia. apply Hlow1; lia. |
| 158 | + - (* RBin b e1 e2 *) |
| 159 | + cbn in Heval. |
| 160 | + destruct (eval env e1) as [v1|] eqn:Hev1; cbn in Heval; [| discriminate]. |
| 161 | + destruct (eval env e2) as [v2|] eqn:Hev2; cbn in Heval; [| discriminate]. |
| 162 | + injection Heval as Hv; subst v. |
| 163 | + destruct (IH1 env d locals st v1 Hev1 Hlen Hagree ltac:(lia)) |
| 164 | + as [locals1 [Hw1 [Hlen1 Hlow1]]]. |
| 165 | + assert (Hag1 : agree env locals1). |
| 166 | + { intros j Hj. rewrite Hlow1 by lia. apply Hagree; lia. } |
| 167 | + destruct (IH2 env d locals1 (v1 :: st) v2 Hev2 Hlen Hag1 |
| 168 | + ltac:(rewrite Hlen1; lia)) |
| 169 | + as [locals2 [Hw2 [Hlen2 Hlow2]]]. |
| 170 | + exists locals2. split; [| split]. |
| 171 | + + apply wexec_seq with (lo1:=locals1) (st1:=v1::st); [exact Hw1|]. |
| 172 | + apply wexec_seq with (lo1:=locals2) (st1:=v2::v1::st); [exact Hw2|]. |
| 173 | + cbn [wexec]. rewrite step1_bop. reflexivity. |
| 174 | + + rewrite Hlen2. exact Hlen1. |
| 175 | + + intros j Hj. rewrite Hlow2 by lia. apply Hlow1; lia. |
| 176 | +Qed. |
| 177 | + |
| 178 | +(* ── closed-program corollary ─────────────────────────────────────────────── *) |
| 179 | +Corollary compile_program_correct : forall e v, |
| 180 | + eval [] e = Some v -> |
| 181 | + exists locals', |
| 182 | + wexec (compile 0 e) (repeat 0%Z (depth e)) [] = Some (locals', [v]). |
| 183 | +Proof. |
| 184 | + intros e v Heval. |
| 185 | + destruct (compile_correct e [] 0 (repeat 0%Z (depth e)) [] v Heval) |
| 186 | + as [locals' [Hw _]]. |
| 187 | + - reflexivity. |
| 188 | + - intros i Hi; cbn in Hi; lia. |
| 189 | + - rewrite repeat_length; lia. |
| 190 | + - exists locals'; exact Hw. |
| 191 | +Qed. |
| 192 | + |
| 193 | +(* concrete: let x = 2+3 in x*4 ⇒ 20, end-to-end. *) |
| 194 | +Example r1_eval_demo : |
| 195 | + eval [] (RLet (RBin BAdd (RLit (LInt 2)) (RLit (LInt 3))) |
| 196 | + (RBin BMul (RVar 0) (RLit (LInt 4)))) = Some 20%Z. |
| 197 | +Proof. reflexivity. Qed. |
| 198 | + |
| 199 | +Example r1_exec_demo : |
| 200 | + wexec (compile 0 (RLet (RBin BAdd (RLit (LInt 2)) (RLit (LInt 3))) |
| 201 | + (RBin BMul (RVar 0) (RLit (LInt 4))))) [0%Z] [] |
| 202 | + = Some ([5%Z], [20%Z]). |
| 203 | +Proof. reflexivity. Qed. |
| 204 | + |
| 205 | +Print Assumptions compile_correct. |
| 206 | +Print Assumptions compile_program_correct. |
0 commit comments