|
| 1 | +(* SPDX-License-Identifier: MPL-2.0 *) |
| 2 | +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *) |
| 3 | + |
| 4 | +(* |
| 5 | + K1_CodegenPreservation.v |
| 6 | + ════════════════════════ |
| 7 | + Wave-0 seed of obligation **K-1** from docs/PROOF-NEEDS.adoc: |
| 8 | + "codegen → typed-WASM semantic-preservation" — the keystone every face |
| 9 | + (via F-1) and every aLib conformer ultimately composes through. |
| 10 | +
|
| 11 | + This file is a Coq/Rocq PROOF SCRIPT. It is NOT V-lang and NOT Verilog — |
| 12 | + the `.v` extension is shared between Coq, Verilog and V-lang. The estate |
| 13 | + language policy bans *V-lang* (→ Zig) and carves Coq proof scripts out of |
| 14 | + the `cicd_rules/vlang_detected` rule via `path_allow_prefixes`; this repo |
| 15 | + makes that explicit for `formal/` in `.hypatia-ignore`. |
| 16 | +
|
| 17 | + SCOPE (honest). This discharges K-1 for a deliberately minimal fragment: |
| 18 | + a two-type (nat, bool) expression language with `add` and `and`, compiled |
| 19 | + to a little stack machine that stands in for typed-WASM. The full |
| 20 | + obligation — the real AffineScript AST and the real typed-WASM operational |
| 21 | + semantics — is future work that *expands* this core, exactly the way |
| 22 | + solo-core's Duet/Ensemble tracks expand the Solo fragment. What is proven |
| 23 | + here is the genuine article for the fragment: a complete, machine-checked |
| 24 | + compiler-correctness theorem with NO `Admitted`, NO `Axiom`, NO `postulate` |
| 25 | + (estate rule: load-bearing proofs must be constructive and complete). |
| 26 | +
|
| 27 | + Check it: coqc formal/K1_CodegenPreservation.v (or: just -f formal/justfile check) |
| 28 | +*) |
| 29 | + |
| 30 | +Require Import List. |
| 31 | +Import ListNotations. |
| 32 | + |
| 33 | +(* ══════════════════ Source: a minimal AffineScript fragment ══════════════ *) |
| 34 | + |
| 35 | +Inductive sval : Type := |
| 36 | +| VNat (n : nat) |
| 37 | +| VBool (b : bool). |
| 38 | + |
| 39 | +Inductive sexp : Type := |
| 40 | +| SNat (n : nat) |
| 41 | +| SBool (b : bool) |
| 42 | +| SAdd (e1 e2 : sexp) |
| 43 | +| SAnd (e1 e2 : sexp). |
| 44 | + |
| 45 | +(* Big-step source evaluator. Partial: `add` on bools (or `and` on nats) is |
| 46 | + stuck (None), so `seval e = Some v` is a real, non-trivial hypothesis. *) |
| 47 | +Fixpoint seval (e : sexp) : option sval := |
| 48 | + match e with |
| 49 | + | SNat n => Some (VNat n) |
| 50 | + | SBool b => Some (VBool b) |
| 51 | + | SAdd e1 e2 => |
| 52 | + match seval e1, seval e2 with |
| 53 | + | Some (VNat a), Some (VNat b) => Some (VNat (a + b)) |
| 54 | + | _, _ => None |
| 55 | + end |
| 56 | + | SAnd e1 e2 => |
| 57 | + match seval e1, seval e2 with |
| 58 | + | Some (VBool a), Some (VBool b) => Some (VBool (andb a b)) |
| 59 | + | _, _ => None |
| 60 | + end |
| 61 | + end. |
| 62 | + |
| 63 | +(* ══════════════ Target: a minimal typed-WASM-style stack machine ═════════ *) |
| 64 | + |
| 65 | +Inductive wval : Type := |
| 66 | +| WNat (n : nat) |
| 67 | +| WBool (b : bool). |
| 68 | + |
| 69 | +Inductive instr : Type := |
| 70 | +| IPushN (n : nat) |
| 71 | +| IPushB (b : bool) |
| 72 | +| IAdd |
| 73 | +| IAnd. |
| 74 | + |
| 75 | +Definition code := list instr. |
| 76 | +Definition stack := list wval. |
| 77 | + |
| 78 | +(* One instruction over the stack. None = trap (ill-typed operand stack), |
| 79 | + the analogue of a typed-WASM validation failure. *) |
| 80 | +Definition wstep (i : instr) (s : stack) : option stack := |
| 81 | + match i, s with |
| 82 | + | IPushN n, s => Some (WNat n :: s) |
| 83 | + | IPushB b, s => Some (WBool b :: s) |
| 84 | + | IAdd, WNat b :: WNat a :: s' => Some (WNat (a + b) :: s') |
| 85 | + | IAnd, WBool b :: WBool a :: s' => Some (WBool (andb a b) :: s') |
| 86 | + | _, _ => None |
| 87 | + end. |
| 88 | + |
| 89 | +Fixpoint wexec (c : code) (s : stack) : option stack := |
| 90 | + match c with |
| 91 | + | [] => Some s |
| 92 | + | i :: rest => |
| 93 | + match wstep i s with |
| 94 | + | Some s' => wexec rest s' |
| 95 | + | None => None |
| 96 | + end |
| 97 | + end. |
| 98 | + |
| 99 | +(* ══════════════════════ Compiler: source → stack code ════════════════════ *) |
| 100 | + |
| 101 | +Fixpoint compile (e : sexp) : code := |
| 102 | + match e with |
| 103 | + | SNat n => [IPushN n] |
| 104 | + | SBool b => [IPushB b] |
| 105 | + | SAdd e1 e2 => compile e1 ++ compile e2 ++ [IAdd] |
| 106 | + | SAnd e1 e2 => compile e1 ++ compile e2 ++ [IAnd] |
| 107 | + end. |
| 108 | + |
| 109 | +(* Value correspondence: a source value and the wasm value it denotes. *) |
| 110 | +Definition obs (v : sval) : wval := |
| 111 | + match v with |
| 112 | + | VNat n => WNat n |
| 113 | + | VBool b => WBool b |
| 114 | + end. |
| 115 | + |
| 116 | +(* ════════════════ The K-1 obligation, for this fragment ══════════════════ *) |
| 117 | + |
| 118 | +(* Codegen preserves meaning: if the source evaluates to v, then running the |
| 119 | + compiled code on the empty operand stack yields exactly [obs v]. *) |
| 120 | +Definition K1_preservation : Prop := |
| 121 | + forall (e : sexp) (v : sval), |
| 122 | + seval e = Some v -> |
| 123 | + wexec (compile e) [] = Some [obs v]. |
| 124 | + |
| 125 | +(* ───────────────────────── discharge (no Admitted) ──────────────────────── *) |
| 126 | + |
| 127 | +(* Correctness in continuation-passing form: running `compile e` followed by |
| 128 | + any continuation `k`, from any stack `s`, is the same as running `k` with |
| 129 | + the source value `v` pushed. Threading `k` is exactly the induction |
| 130 | + strength needed (and avoids reasoning about a residual `match`). *) |
| 131 | +Lemma compile_correct : forall e v s k, |
| 132 | + seval e = Some v -> |
| 133 | + wexec (compile e ++ k) s = wexec k (obs v :: s). |
| 134 | +Proof. |
| 135 | + induction e as [n | b | e1 IH1 e2 IH2 | e1 IH1 e2 IH2]; |
| 136 | + intros v s k Hev; simpl in Hev. |
| 137 | + - (* SNat *) inversion Hev; subst; reflexivity. |
| 138 | + - (* SBool *) inversion Hev; subst; reflexivity. |
| 139 | + - (* SAdd *) |
| 140 | + destruct (seval e1) as [[a | ab] |]; try discriminate; |
| 141 | + destruct (seval e2) as [[b | bb] |]; try discriminate; |
| 142 | + inversion Hev; subst; clear Hev; simpl; rewrite <- !app_assoc; |
| 143 | + rewrite (IH1 _ s _ eq_refl), (IH2 _ _ _ eq_refl); reflexivity. |
| 144 | + - (* SAnd *) |
| 145 | + destruct (seval e1) as [[na | a] |]; try discriminate; |
| 146 | + destruct (seval e2) as [[nb | b] |]; try discriminate; |
| 147 | + inversion Hev; subst; clear Hev; simpl; rewrite <- !app_assoc; |
| 148 | + rewrite (IH1 _ s _ eq_refl), (IH2 _ _ _ eq_refl); reflexivity. |
| 149 | +Qed. |
| 150 | + |
| 151 | +Theorem k1_preservation_holds : K1_preservation. |
| 152 | +Proof. |
| 153 | + unfold K1_preservation; intros e v Hev. |
| 154 | + pose proof (compile_correct e v [] [] Hev) as H. |
| 155 | + rewrite app_nil_r in H; simpl in H; exact H. |
| 156 | +Qed. |
| 157 | + |
| 158 | +(* `Print Assumptions` must report "Closed under the global context" — i.e. |
| 159 | + the theorem rests on no axioms. CI greps for exactly that string. *) |
| 160 | +Print Assumptions k1_preservation_holds. |
0 commit comments