|
| 1 | +(* SPDX-License-Identifier: MPL-2.0 *) |
| 2 | +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *) |
| 3 | + |
| 4 | +(* |
| 5 | + RealMem.v |
| 6 | + ═════════ |
| 7 | + REAL-LIFT rung **R-mem** (see formal/REAL-LIFT.adoc): linear memory. |
| 8 | + Adds the load/store execution for `lib/wasm.ml`'s `I32Load`/`I32Store` (the |
| 9 | + instructions were added to `instr` in RealWasm.v) and a source heap layer — |
| 10 | + `tuple`/`record`-style cells laid out at consecutive addresses — with the |
| 11 | + build-then-project round-trip proved. |
| 12 | +
|
| 13 | + Memory is **word-addressed** (`mem := list Z`, address = cell index): the |
| 14 | + deterministic layout the codegen's elaboration nodes assume, where tuples / |
| 15 | + records / arrays are runs of i32 cells. (Byte-granular `[len][utf8]` layout |
| 16 | + and IEEE lanes are the later R-str / R-float rungs; bit-exact wrap is R-wrap.) |
| 17 | +
|
| 18 | + Memory ops are *straight-line* (no control), so unlike R2's `wexec` / the |
| 19 | + R2-loops `cexec`, the memory executor `mexec` is a **structural** `Fixpoint` |
| 20 | + on the instruction list — no fuel needed. The heap round-trip is then exactly |
| 21 | + `set_nth`'s get-after-set, reused from RealWasm. |
| 22 | +
|
| 23 | + Axiom-free, no Admitted. |
| 24 | + `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. |
| 25 | +*) |
| 26 | + |
| 27 | +Require Import List. |
| 28 | +Require Import ZArith. |
| 29 | +Require Import PeanoNat. |
| 30 | +Require Import Lia. |
| 31 | +Require Import ASFormal.RealWasm. |
| 32 | +Require Import ASFormal.RealCompile. |
| 33 | +Import ListNotations. |
| 34 | + |
| 35 | +(* ── word-addressed linear memory ─────────────────────────────────────────── *) |
| 36 | +Definition mem := list Z. |
| 37 | +Definition mem_get (m : mem) (a : nat) : option Z := nth_error m a. |
| 38 | +Definition mem_set (a : nat) (v : Z) (m : mem) : mem := set_nth a v m. |
| 39 | + |
| 40 | +Lemma mem_set_length : forall a v m, length (mem_set a v m) = length m. |
| 41 | +Proof. intros; apply set_nth_length. Qed. |
| 42 | + |
| 43 | +Lemma mem_get_set_eq : forall a v m, a < length m -> mem_get (mem_set a v m) a = Some v. |
| 44 | +Proof. intros; apply set_nth_eq; assumption. Qed. |
| 45 | + |
| 46 | +Lemma mem_get_set_neq : forall a a' v m, |
| 47 | + a <> a' -> mem_get (mem_set a' v m) a = mem_get m a. |
| 48 | +Proof. intros; apply set_nth_neq; assumption. Qed. |
| 49 | + |
| 50 | +(* bump allocator: base = current size; reserve n zeroed cells. *) |
| 51 | +Definition alloc (n : nat) (m : mem) : nat * mem := (length m, m ++ repeat 0%Z n). |
| 52 | + |
| 53 | +Lemma alloc_base : forall n m, fst (alloc n m) = length m. |
| 54 | +Proof. reflexivity. Qed. |
| 55 | + |
| 56 | +Lemma alloc_length : forall n m, length (snd (alloc n m)) = length m + n. |
| 57 | +Proof. intros; cbn. rewrite app_length, repeat_length; reflexivity. Qed. |
| 58 | + |
| 59 | +(* ── memory-aware executor (structural on the instruction list) ─────────────── |
| 60 | + I32Load off : pop addr a, push mem[⌊a⌋+off]. |
| 61 | + I32Store off : pop value v then addr a, set mem[⌊a⌋+off] := v. |
| 62 | + everything else: the memory-free `step1` (memory unchanged). Control |
| 63 | + instructions (Block/Loop/Br/BrIf/IfElse) trap via step1 = None — combining |
| 64 | + memory with control is the next sub-rung. *) |
| 65 | +Fixpoint mexec (is : list instr) (m : mem) (lo : locals) (st : stack) |
| 66 | + : option (mem * locals * stack) := |
| 67 | + match is with |
| 68 | + | [] => Some (m, lo, st) |
| 69 | + | a :: r => |
| 70 | + match a with |
| 71 | + | I32Load off => |
| 72 | + match st with |
| 73 | + | addr :: t => |
| 74 | + match mem_get m (Z.to_nat addr + off) with |
| 75 | + | Some v => mexec r m lo (v :: t) |
| 76 | + | None => None |
| 77 | + end |
| 78 | + | [] => None |
| 79 | + end |
| 80 | + | I32Store off => |
| 81 | + match st with |
| 82 | + | v :: addr :: t => mexec r (mem_set (Z.to_nat addr + off) v m) lo t |
| 83 | + | _ => None |
| 84 | + end |
| 85 | + | _ => |
| 86 | + match step1 a lo st with |
| 87 | + | Some (lo', st') => mexec r m lo' st' |
| 88 | + | None => None |
| 89 | + end |
| 90 | + end |
| 91 | + end. |
| 92 | + |
| 93 | +(* sequencing: straight-line, so a plain structural split (no fuel/monotonicity). *) |
| 94 | +Lemma mexec_app : forall is1 m lo st m1 lo1 st1, |
| 95 | + mexec is1 m lo st = Some (m1, lo1, st1) -> |
| 96 | + forall is2, |
| 97 | + mexec (is1 ++ is2) m lo st = mexec is2 m1 lo1 st1. |
| 98 | +Proof. |
| 99 | + induction is1 as [| a r IH]; intros m lo st m1 lo1 st1 H is2. |
| 100 | + - cbn in H. injection H as -> -> ->. reflexivity. |
| 101 | + - cbn [app]. destruct a; |
| 102 | + try (cbn [mexec] in H |- *; destruct (step1 _ lo st) as [[lo' st']|]; |
| 103 | + [ apply IH; exact H | discriminate H ]). |
| 104 | + + (* I32Load *) |
| 105 | + cbn [mexec] in H |- *. destruct st as [| addr t]; [discriminate H|]. |
| 106 | + destruct (mem_get m (Z.to_nat addr + off)) as [v|]; [| discriminate H]. |
| 107 | + apply IH; exact H. |
| 108 | + + (* I32Store *) |
| 109 | + cbn [mexec] in H |- *. destruct st as [| v [| addr t]]; try discriminate H. |
| 110 | + apply IH; exact H. |
| 111 | +Qed. |
| 112 | + |
| 113 | +(* ── concrete sanity: store then load the same cell round-trips ─────────────── *) |
| 114 | +Example mexec_store_load_demo : |
| 115 | + (* mem = [0;0;0]; store 42 at addr 1, then load addr 1 ⇒ 42 *) |
| 116 | + mexec [I32Const 1; I32Const 42; I32Store 0; I32Const 1; I32Load 0] |
| 117 | + [0;0;0]%Z [] [] |
| 118 | + = Some (mem_set 1 42 [0;0;0]%Z, [], [42%Z]). |
| 119 | +Proof. reflexivity. Qed. |
| 120 | + |
| 121 | +(* the executor-level store→load round-trip: storing v at a fresh in-range cell |
| 122 | + then loading it back yields v (this is `set_nth`'s get-after-set, lifted |
| 123 | + through `mexec`). *) |
| 124 | +Lemma mexec_store_then_load : forall m a v, |
| 125 | + a < length m -> |
| 126 | + mexec [I32Const (Z.of_nat a); I32Const v; I32Store 0; |
| 127 | + I32Const (Z.of_nat a); I32Load 0] m [] [] |
| 128 | + = Some (mem_set a v m, [], [v]). |
| 129 | +Proof. |
| 130 | + intros m a v Ha. |
| 131 | + cbn [mexec step1]. |
| 132 | + rewrite Nat.add_0_r, Nat2Z.id. |
| 133 | + rewrite mem_get_set_eq by exact Ha. |
| 134 | + reflexivity. |
| 135 | +Qed. |
| 136 | + |
| 137 | +(* ── heap tuples: build a 2-cell tuple at `base`, then project both fields ──── |
| 138 | + This is the codegen's deterministic cell layout (field i at base+i) proved as |
| 139 | + a get-after-set round-trip — the precondition for arrays / records / strings. |
| 140 | + (`base` is the address the bump allocator hands out; a runtime `memory.grow` |
| 141 | + that produces it, and field expressions with control, are the next sub-rung.) *) |
| 142 | +Theorem mexec_pair_build_proj : forall m base v0 v1, |
| 143 | + base + 1 < length m -> |
| 144 | + exists m', |
| 145 | + (* build: store v0 at base+0, v1 at base+1 *) |
| 146 | + mexec [I32Const (Z.of_nat base); I32Const v0; I32Store 0; |
| 147 | + I32Const (Z.of_nat base); I32Const v1; I32Store 1] m [] [] |
| 148 | + = Some (m', [], []) |
| 149 | + (* project field 0 ⇒ v0 *) |
| 150 | + /\ mexec [I32Const (Z.of_nat base); I32Load 0] m' [] [] = Some (m', [], [v0]) |
| 151 | + (* project field 1 ⇒ v1 *) |
| 152 | + /\ mexec [I32Const (Z.of_nat base); I32Load 1] m' [] [] = Some (m', [], [v1]). |
| 153 | +Proof. |
| 154 | + intros m base v0 v1 Hb. |
| 155 | + exists (mem_set (base + 1) v1 (mem_set base v0 m)). split; [| split]. |
| 156 | + - cbn [mexec step1]. rewrite !Nat2Z.id, Nat.add_0_r. reflexivity. |
| 157 | + - cbn [mexec step1]. rewrite Nat2Z.id, Nat.add_0_r. |
| 158 | + rewrite mem_get_set_neq by lia. |
| 159 | + rewrite mem_get_set_eq by lia. reflexivity. |
| 160 | + - cbn [mexec step1]. rewrite Nat2Z.id. |
| 161 | + rewrite mem_get_set_eq by (rewrite mem_set_length; lia). reflexivity. |
| 162 | +Qed. |
| 163 | + |
| 164 | +Print Assumptions mexec_store_then_load. |
| 165 | +Print Assumptions mexec_pair_build_proj. |
0 commit comments