|
| 1 | +(* SPDX-License-Identifier: MPL-2.0 *) |
| 2 | +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *) |
| 3 | + |
| 4 | +(* |
| 5 | + K1Let_CodegenPreservation.v |
| 6 | + ═══════════════════════════ |
| 7 | + K-1, GROWN. Extends the minimal K1_CodegenPreservation fragment with the |
| 8 | + first real binder: de Bruijn **variables** and **`let`**, evaluated under an |
| 9 | + environment. The target machine gains a **locals** register alongside the |
| 10 | + operand stack; compilation balances `IBind`/`IUnbind` so locals scope |
| 11 | + correctly. The codegen-preservation theorem is re-proven for this richer |
| 12 | + fragment — still complete and axiom-free (no `Admitted`). |
| 13 | +
|
| 14 | + This is a step of the K-1 obligation toward the real AST (binders → |
| 15 | + environments). `if`/control-flow is the next increment (it needs structured |
| 16 | + target control + a termination measure, deliberately out of this step). |
| 17 | +
|
| 18 | + `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. |
| 19 | + Check: coqc -Q . ASFormal K1Let_CodegenPreservation.v |
| 20 | +*) |
| 21 | + |
| 22 | +Require Import List. |
| 23 | +Import ListNotations. |
| 24 | + |
| 25 | +(* ════════════════════════ Source (env-based, with let) ═══════════════════ *) |
| 26 | + |
| 27 | +Inductive sval : Type := VNat (n : nat) | VBool (b : bool). |
| 28 | + |
| 29 | +Inductive sexp : Type := |
| 30 | +| SNat (n : nat) |
| 31 | +| SBool (b : bool) |
| 32 | +| SVar (i : nat) (* de Bruijn index into the environment *) |
| 33 | +| SAdd (a b : sexp) |
| 34 | +| SAnd (a b : sexp) |
| 35 | +| SLet (e1 e2 : sexp). (* let x = e1 in e2 ; x is index 0 in e2 *) |
| 36 | + |
| 37 | +Definition senv := list sval. |
| 38 | + |
| 39 | +Fixpoint seval (env : senv) (e : sexp) : option sval := |
| 40 | + match e with |
| 41 | + | SNat n => Some (VNat n) |
| 42 | + | SBool b => Some (VBool b) |
| 43 | + | SVar i => nth_error env i |
| 44 | + | SAdd a b => |
| 45 | + match seval env a, seval env b with |
| 46 | + | Some (VNat x), Some (VNat y) => Some (VNat (x + y)) |
| 47 | + | _, _ => None |
| 48 | + end |
| 49 | + | SAnd a b => |
| 50 | + match seval env a, seval env b with |
| 51 | + | Some (VBool x), Some (VBool y) => Some (VBool (andb x y)) |
| 52 | + | _, _ => None |
| 53 | + end |
| 54 | + | SLet e1 e2 => |
| 55 | + match seval env e1 with |
| 56 | + | Some v => seval (v :: env) e2 |
| 57 | + | None => None |
| 58 | + end |
| 59 | + end. |
| 60 | + |
| 61 | +(* ═══════════════ Target: stack machine + a locals register ════════════════ *) |
| 62 | + |
| 63 | +Inductive wval : Type := WNat (n : nat) | WBool (b : bool). |
| 64 | + |
| 65 | +Definition obs (v : sval) : wval := |
| 66 | + match v with VNat n => WNat n | VBool b => WBool b end. |
| 67 | + |
| 68 | +Inductive instr : Type := |
| 69 | +| IPushN (n : nat) |
| 70 | +| IPushB (b : bool) |
| 71 | +| IGet (i : nat) (* push locals[i] onto the stack *) |
| 72 | +| IAdd |
| 73 | +| IAnd |
| 74 | +| IBind (* pop stack top, push it onto locals (new index 0) *) |
| 75 | +| IUnbind. (* drop locals[0]; operand stack unchanged *) |
| 76 | + |
| 77 | +Definition code := list instr. |
| 78 | +Definition locals := list wval. |
| 79 | +Definition stack := list wval. |
| 80 | + |
| 81 | +Definition wstep (i : instr) (l : locals) (s : stack) : option (locals * stack) := |
| 82 | + match i, l, s with |
| 83 | + | IPushN n, l, s => Some (l, WNat n :: s) |
| 84 | + | IPushB b, l, s => Some (l, WBool b :: s) |
| 85 | + | IGet k, l, s => |
| 86 | + match nth_error l k with |
| 87 | + | Some w => Some (l, w :: s) |
| 88 | + | None => None |
| 89 | + end |
| 90 | + | IAdd, l, WNat b :: WNat a :: s' => Some (l, WNat (a + b) :: s') |
| 91 | + | IAnd, l, WBool b :: WBool a :: s' => Some (l, WBool (andb a b) :: s') |
| 92 | + | IBind, l, w :: s' => Some (w :: l, s') |
| 93 | + | IUnbind, _ :: l', s => Some (l', s) |
| 94 | + | _, _, _ => None |
| 95 | + end. |
| 96 | + |
| 97 | +Fixpoint wexec (c : code) (l : locals) (s : stack) : option (locals * stack) := |
| 98 | + match c with |
| 99 | + | [] => Some (l, s) |
| 100 | + | i :: rest => |
| 101 | + match wstep i l s with |
| 102 | + | Some (l', s') => wexec rest l' s' |
| 103 | + | None => None |
| 104 | + end |
| 105 | + end. |
| 106 | + |
| 107 | +Fixpoint compile (e : sexp) : code := |
| 108 | + match e with |
| 109 | + | SNat n => [IPushN n] |
| 110 | + | SBool b => [IPushB b] |
| 111 | + | SVar i => [IGet i] |
| 112 | + | SAdd a b => compile a ++ compile b ++ [IAdd] |
| 113 | + | SAnd a b => compile a ++ compile b ++ [IAnd] |
| 114 | + | SLet e1 e2 => compile e1 ++ [IBind] ++ compile e2 ++ [IUnbind] |
| 115 | + end. |
| 116 | + |
| 117 | +(* ═════════════════════════ preservation (no Admitted) ════════════════════ *) |
| 118 | + |
| 119 | +(* Execution distributes over code concatenation — the workhorse that lets the |
| 120 | + `let` case step its `IBind`/`IUnbind` cleanly without continuation juggling. *) |
| 121 | +Lemma wexec_app : forall c1 c2 l s, |
| 122 | + wexec (c1 ++ c2) l s = |
| 123 | + match wexec c1 l s with |
| 124 | + | Some (l', s') => wexec c2 l' s' |
| 125 | + | None => None |
| 126 | + end. |
| 127 | +Proof. |
| 128 | + induction c1 as [| i c1 IH]; intros c2 l s; simpl. |
| 129 | + - reflexivity. |
| 130 | + - destruct (wstep i l s) as [[l' s'] |]; [apply IH | reflexivity]. |
| 131 | +Qed. |
| 132 | + |
| 133 | +(* Codegen preservation, generalized over the operand stack `s` and carrying |
| 134 | + the environment/locals correspondence `l = map obs env`. `IUnbind` restores |
| 135 | + locals, so the machine returns to the same `l` it started with. *) |
| 136 | +Lemma compile_correct : forall e env v l s, |
| 137 | + seval env e = Some v -> |
| 138 | + l = map obs env -> |
| 139 | + wexec (compile e) l s = Some (l, obs v :: s). |
| 140 | +Proof. |
| 141 | + induction e as [n | b | i | a IHa b IHb | a IHa b IHb | e1 IH1 e2 IH2]; |
| 142 | + intros env v l s Hev Hl; simpl in Hev; subst l. |
| 143 | + - (* SNat *) inversion Hev; subst; reflexivity. |
| 144 | + - (* SBool *) inversion Hev; subst; reflexivity. |
| 145 | + - (* SVar *) |
| 146 | + apply (map_nth_error obs) in Hev; simpl; rewrite Hev; reflexivity. |
| 147 | + - (* SAdd *) |
| 148 | + destruct (seval env a) as [[x | xb] |] eqn:Ha; try discriminate; |
| 149 | + destruct (seval env b) as [[y | yb] |] eqn:Hb; try discriminate; |
| 150 | + inversion Hev; subst; clear Hev; simpl compile; |
| 151 | + rewrite wexec_app, (IHa env (VNat x) (map obs env) s Ha eq_refl); simpl; |
| 152 | + rewrite wexec_app, (IHb env (VNat y) (map obs env) (WNat x :: s) Hb eq_refl); simpl; |
| 153 | + reflexivity. |
| 154 | + - (* SAnd *) |
| 155 | + destruct (seval env a) as [[xn | x] |] eqn:Ha; try discriminate; |
| 156 | + destruct (seval env b) as [[yn | y] |] eqn:Hb; try discriminate; |
| 157 | + inversion Hev; subst; clear Hev; simpl compile; |
| 158 | + rewrite wexec_app, (IHa env (VBool x) (map obs env) s Ha eq_refl); simpl; |
| 159 | + rewrite wexec_app, (IHb env (VBool y) (map obs env) (WBool x :: s) Hb eq_refl); simpl; |
| 160 | + reflexivity. |
| 161 | + - (* SLet *) |
| 162 | + destruct (seval env e1) as [v1 |] eqn:H1; try discriminate; simpl in Hev; |
| 163 | + simpl compile; |
| 164 | + rewrite wexec_app, (IH1 env v1 (map obs env) s H1 eq_refl); simpl; |
| 165 | + rewrite wexec_app, (IH2 (v1 :: env) v (obs v1 :: map obs env) s Hev eq_refl); simpl; |
| 166 | + reflexivity. |
| 167 | +Qed. |
| 168 | + |
| 169 | +(* For a closed program (empty env) the locals balance back to empty and the |
| 170 | + result is the single wasm value on the operand stack. *) |
| 171 | +Theorem k1let_preservation_holds : forall e v, |
| 172 | + seval [] e = Some v -> |
| 173 | + wexec (compile e) [] [] = Some ([], [obs v]). |
| 174 | +Proof. |
| 175 | + intros e v H. |
| 176 | + exact (compile_correct e [] v [] [] H eq_refl). |
| 177 | +Qed. |
| 178 | + |
| 179 | +Print Assumptions k1let_preservation_holds. |
0 commit comments