|
| 1 | +(* SPDX-License-Identifier: PMPL-1.0-or-later *) |
| 2 | +(* SPDX-FileCopyrightText: 2024-2026 hyperpolymath *) |
| 3 | + |
| 4 | +(** typed-wasm ownership verifier — Stage 7. |
| 5 | +
|
| 6 | + Statically verifies typed-wasm Level 7 (aliasing safety) and Level 10 |
| 7 | + (linearity) constraints on AffineScript's Wasm IR. |
| 8 | +
|
| 9 | + The verifier runs after codegen on the in-memory [Wasm.wasm_module] |
| 10 | + together with the ownership annotations collected during codegen. |
| 11 | + It is a second line of defence: the QTT quantity checker (Stage 1) already |
| 12 | + enforces these rules at the AffineScript source level; this module |
| 13 | + re-checks them on the emitted Wasm IR to catch any codegen bugs. |
| 14 | +
|
| 15 | + Level 10 — Linearity: a parameter annotated [Linear] (TyOwn) must be |
| 16 | + loaded exactly once in the function body. Loading zero times means the |
| 17 | + owned value is dropped; loading more than once means it may be duplicated. |
| 18 | +
|
| 19 | + Level 7 — Aliasing safety: a parameter annotated [ExclBorrow] (TyMut) |
| 20 | + must be loaded at most once. Multiple loads create aliased references to |
| 21 | + the same mutable memory, violating exclusive-borrow invariants. |
| 22 | +
|
| 23 | + [SharedBorrow] (TyRef) and [Unrestricted] params are not checked by this |
| 24 | + pass (no constraints violated by multiple reads of a shared reference). |
| 25 | +
|
| 26 | + Branch semantics: for [If] instructions, we take the {b max} of the |
| 27 | + use-counts across the two branches (since only one branch executes at |
| 28 | + runtime). This is conservative: a linear param used exactly once in |
| 29 | + each branch of an if/else is counted as 1 (correct), not 2. Stage 8 |
| 30 | + will refine this with a per-path analysis if needed. |
| 31 | +
|
| 32 | + @see typed-wasm LEVEL-STATUS.md — Level 7 and Level 10 sections. |
| 33 | +*) |
| 34 | + |
| 35 | +open Codegen |
| 36 | + |
| 37 | +(* ============================================================================ |
| 38 | + Error types |
| 39 | + ============================================================================ *) |
| 40 | + |
| 41 | +(** An ownership violation found in a Wasm function body. *) |
| 42 | +type ownership_error = |
| 43 | + | LinearNotUsed of { func_idx : int; param_idx : int } |
| 44 | + (** Level 10: Linear parameter was never loaded — dropped without consumption. |
| 45 | + The owned resource leaks. *) |
| 46 | + | LinearUsedMultiple of { func_idx : int; param_idx : int; count : int } |
| 47 | + (** Level 10: Linear parameter was loaded [count] times — potential duplication. |
| 48 | + Only one consumer is permitted. *) |
| 49 | + | ExclBorrowAliased of { func_idx : int; param_idx : int; count : int } |
| 50 | + (** Level 7: ExclBorrow parameter was loaded [count] times — aliasing violation. |
| 51 | + An exclusive borrow must not have multiple simultaneous references. *) |
| 52 | + |
| 53 | +(* ============================================================================ |
| 54 | + Use-count analysis |
| 55 | + ============================================================================ *) |
| 56 | + |
| 57 | +(** Count how many times [local_idx] is loaded inside [instrs]. |
| 58 | +
|
| 59 | + For [If] nodes the branch counts are combined with [max] rather than |
| 60 | + summed, reflecting that only one branch executes. All other nodes are |
| 61 | + summed. Nested [Block] and [Loop] bodies are descended into. *) |
| 62 | +let rec count_uses (local_idx : int) (instrs : Wasm.instr list) : int = |
| 63 | + List.fold_left (fun acc instr -> acc + uses_in_instr local_idx instr) 0 instrs |
| 64 | + |
| 65 | +and uses_in_instr (local_idx : int) (instr : Wasm.instr) : int = |
| 66 | + match instr with |
| 67 | + | Wasm.LocalGet n -> if n = local_idx then 1 else 0 |
| 68 | + | Wasm.Block (_, body) | Wasm.Loop (_, body) -> |
| 69 | + count_uses local_idx body |
| 70 | + | Wasm.If (_, then_, else_) -> |
| 71 | + (* Only one branch executes: take max so that |
| 72 | + If { then: LocalGet 0 } { else: LocalGet 0 } counts as 1, not 2. *) |
| 73 | + max (count_uses local_idx then_) (count_uses local_idx else_) |
| 74 | + | _ -> 0 |
| 75 | + |
| 76 | +(* ============================================================================ |
| 77 | + Per-function verification |
| 78 | + ============================================================================ *) |
| 79 | + |
| 80 | +(** Verify ownership constraints for one function. |
| 81 | +
|
| 82 | + [func] is the Wasm function body. |
| 83 | + [param_kinds] are the ownership annotations for each parameter (in order). |
| 84 | + [func_idx] is the global function index (for error reporting). |
| 85 | + Returns all violations found (empty list = clean). *) |
| 86 | +let verify_function |
| 87 | + (func : Wasm.func) |
| 88 | + (param_kinds : ownership_kind list) |
| 89 | + (func_idx : int) |
| 90 | + : ownership_error list = |
| 91 | + List.concat_map (fun (param_idx, kind) -> |
| 92 | + let uses = count_uses param_idx func.Wasm.f_body in |
| 93 | + match kind with |
| 94 | + | Linear -> |
| 95 | + (* Exactly once: zero = dropped, >1 = may be duplicated. *) |
| 96 | + if uses = 0 then |
| 97 | + [LinearNotUsed { func_idx; param_idx }] |
| 98 | + else if uses > 1 then |
| 99 | + [LinearUsedMultiple { func_idx; param_idx; count = uses }] |
| 100 | + else |
| 101 | + [] |
| 102 | + | ExclBorrow -> |
| 103 | + (* At most once: >1 creates simultaneous aliases. *) |
| 104 | + if uses > 1 then |
| 105 | + [ExclBorrowAliased { func_idx; param_idx; count = uses }] |
| 106 | + else |
| 107 | + [] |
| 108 | + | Unrestricted | SharedBorrow -> |
| 109 | + (* No constraints on these ownership kinds. *) |
| 110 | + [] |
| 111 | + ) (List.mapi (fun i k -> (i, k)) param_kinds) |
| 112 | + |
| 113 | +(* ============================================================================ |
| 114 | + Module-level verification |
| 115 | + ============================================================================ *) |
| 116 | + |
| 117 | +(** Verify ownership constraints across an entire Wasm module. |
| 118 | +
|
| 119 | + [wasm_mod] is the compiled module. |
| 120 | + [annots] is the list of [(func_idx, param_kinds, ret_kind)] annotations |
| 121 | + collected by codegen and stored in the [affinescript.ownership] custom |
| 122 | + section (but here provided in structured form directly from [Codegen]). |
| 123 | +
|
| 124 | + Imported functions have no body and are skipped. |
| 125 | + Returns all violations found. *) |
| 126 | +let verify_module |
| 127 | + (wasm_mod : Wasm.wasm_module) |
| 128 | + (annots : (int * ownership_kind list * ownership_kind) list) |
| 129 | + : ownership_error list = |
| 130 | + let import_count = List.length wasm_mod.Wasm.imports in |
| 131 | + List.concat_map (fun (func_idx, param_kinds, _ret_kind) -> |
| 132 | + let local_idx = func_idx - import_count in |
| 133 | + if local_idx < 0 || local_idx >= List.length wasm_mod.Wasm.funcs then |
| 134 | + [] (* Imported function: no IR to inspect *) |
| 135 | + else |
| 136 | + let func = List.nth wasm_mod.Wasm.funcs local_idx in |
| 137 | + verify_function func param_kinds func_idx |
| 138 | + ) annots |
| 139 | + |
| 140 | +(* ============================================================================ |
| 141 | + Pipeline integration — parse ownership section from the module |
| 142 | + ============================================================================ *) |
| 143 | + |
| 144 | +(** Parse the [affinescript.ownership] custom section payload into structured |
| 145 | + [(func_idx, param_kinds, ret_kind)] annotations. |
| 146 | +
|
| 147 | + Binary encoding (from [Codegen.build_ownership_section]): |
| 148 | + u32le count |
| 149 | + for each entry: |
| 150 | + u32le func_idx |
| 151 | + u8 n_params |
| 152 | + u8[n] param_kinds (0=Unrestricted, 1=Linear, 2=SharedBorrow, 3=ExclBorrow) |
| 153 | + u8 ret_kind *) |
| 154 | +let parse_ownership_section_payload |
| 155 | + (payload : bytes) |
| 156 | + : (int * ownership_kind list * ownership_kind) list = |
| 157 | + let kind_of_byte = function |
| 158 | + | 1 -> Linear |
| 159 | + | 2 -> SharedBorrow |
| 160 | + | 3 -> ExclBorrow |
| 161 | + | _ -> Unrestricted |
| 162 | + in |
| 163 | + let pos = ref 0 in |
| 164 | + let len = Bytes.length payload in |
| 165 | + let read_u32_le () = |
| 166 | + if !pos + 4 > len then 0 |
| 167 | + else begin |
| 168 | + let b0 = Char.code (Bytes.get payload !pos) in |
| 169 | + let b1 = Char.code (Bytes.get payload (!pos + 1)) in |
| 170 | + let b2 = Char.code (Bytes.get payload (!pos + 2)) in |
| 171 | + let b3 = Char.code (Bytes.get payload (!pos + 3)) in |
| 172 | + pos := !pos + 4; |
| 173 | + b0 lor (b1 lsl 8) lor (b2 lsl 16) lor (b3 lsl 24) |
| 174 | + end |
| 175 | + in |
| 176 | + let read_u8 () = |
| 177 | + if !pos >= len then 0 |
| 178 | + else begin |
| 179 | + let b = Char.code (Bytes.get payload !pos) in |
| 180 | + pos := !pos + 1; |
| 181 | + b |
| 182 | + end |
| 183 | + in |
| 184 | + let count = read_u32_le () in |
| 185 | + List.init count (fun _ -> |
| 186 | + let func_idx = read_u32_le () in |
| 187 | + let n_params = read_u8 () in |
| 188 | + let param_kinds = List.init n_params (fun _ -> kind_of_byte (read_u8 ())) in |
| 189 | + let ret_kind = kind_of_byte (read_u8 ()) in |
| 190 | + (func_idx, param_kinds, ret_kind) |
| 191 | + ) |
| 192 | + |
| 193 | +(** Verify a Wasm module using the embedded [affinescript.ownership] custom |
| 194 | + section. This is the primary entry point for the pipeline and the CLI. |
| 195 | +
|
| 196 | + Returns [Ok ()] if no violations are found, [Error errs] otherwise. *) |
| 197 | +let verify_from_module |
| 198 | + (wasm_mod : Wasm.wasm_module) |
| 199 | + : (unit, ownership_error list) Result.t = |
| 200 | + match List.assoc_opt "affinescript.ownership" wasm_mod.Wasm.custom_sections with |
| 201 | + | None -> |
| 202 | + (* No ownership section: nothing to verify. This is not an error — |
| 203 | + modules compiled without ownership qualifiers have no constraints. *) |
| 204 | + Ok () |
| 205 | + | Some payload -> |
| 206 | + let annots = parse_ownership_section_payload payload in |
| 207 | + let errors = verify_module wasm_mod annots in |
| 208 | + if errors = [] then Ok () else Error errors |
| 209 | + |
| 210 | +(* ============================================================================ |
| 211 | + Pretty-printing |
| 212 | + ============================================================================ *) |
| 213 | + |
| 214 | +(** Format a single ownership error for human-readable output. *) |
| 215 | +let pp_error (fmt : Format.formatter) (err : ownership_error) : unit = |
| 216 | + match err with |
| 217 | + | LinearNotUsed { func_idx; param_idx } -> |
| 218 | + Format.fprintf fmt |
| 219 | + "Level 10 violation: function %d, param %d — Linear (own) param dropped \ |
| 220 | + (must be consumed exactly once)" |
| 221 | + func_idx param_idx |
| 222 | + | LinearUsedMultiple { func_idx; param_idx; count } -> |
| 223 | + Format.fprintf fmt |
| 224 | + "Level 10 violation: function %d, param %d — Linear (own) param loaded \ |
| 225 | + %d times (exactly 1 required; possible duplication)" |
| 226 | + func_idx param_idx count |
| 227 | + | ExclBorrowAliased { func_idx; param_idx; count } -> |
| 228 | + Format.fprintf fmt |
| 229 | + "Level 7 violation: function %d, param %d — ExclBorrow (mut) param \ |
| 230 | + aliased (%d simultaneous references; at most 1 permitted)" |
| 231 | + func_idx param_idx count |
| 232 | + |
| 233 | +(** Format a full verification report. Prints "OK" if no errors. *) |
| 234 | +let pp_report (fmt : Format.formatter) (errs : ownership_error list) : unit = |
| 235 | + match errs with |
| 236 | + | [] -> |
| 237 | + Format.fprintf fmt "typed-wasm ownership verification: OK@." |
| 238 | + | _ -> |
| 239 | + Format.fprintf fmt "typed-wasm ownership verification: %d violation(s)@." |
| 240 | + (List.length errs); |
| 241 | + List.iter (fun e -> |
| 242 | + Format.fprintf fmt " %a@." pp_error e |
| 243 | + ) errs |
0 commit comments