wasm-gc: set vectors in place and keep older versions valid

.github/workflows/ci.yml

@@ -338,6 +338,7 @@ jobs:
             wasm_gc_games_differential_mir \
             wasm_gc_handler_carrier \
             wasm_gc_map_versions_spec \
+            wasm_gc_vector_versions_spec \
             wasm_gc_optimize_trunc_sat \
             wasm_gc_packed_sequence \
             wasm_gc_perslot_int_unboxing_differential \

CHANGELOG.md

@@ -64,6 +64,7 @@ The generated loop is now written from the program's source alone, and the manif
 - **Generated Rust moves the rest of a nested record into its update.** `Setting.update(setting, window = Window.update(setting.window, created = Map.set(setting.window.created, k, v)), height = setting.height + 1)` used to clone `setting.window` and `setting.window.created`, so every `Map.set` copied the Map. When nothing reads that part of `setting` again, the Map now moves into `Map.set` and the other fields of `setting.window` move into the new `Window`.
 - **`check` no longer asks a verify block of a function taking a `Tcp.Socket` or a `Wait.Item`.** Every constructor of either carries a capability resource, so no verify case can write one, but the exemption only looked into the types of the function's own module. It now looks into a capability's own records and sums by the same rule.
 - **Generated Rust builds when a record is updated after one of its fields was read.** `progress = flight.progress` followed by `Flight.update(flight, progress = f(progress))` inside a pair of functions that tail-call each other generated Rust that moved the field out and then moved the whole record, which rustc rejects (E0382). A loop that read a field in a `let` and later returned the whole record failed the same way. Such a field read now moves only when nothing reads that part of the record again and is copied otherwise, and the field read into `f` moves in both spellings (`f(progress)` and `f(flight.progress)`), so a Map `f` updates is not copied.
+- **wasm-gc: `Vector.set` no longer copies the vector.** `set` copied the whole array unless the compiler could prove nothing else held the vector, which it cannot for a vector held in a record field. A record holding a 100,000-cell Vector took 0.21 s for 2000 sets and 1.8 s for 20,000 under `aver run --wasm-gc`. A Vector is now a version over an array, like a Map: `set` writes the cell in place and returns a new version, and the vector it was given stays valid because the old cell is kept with it. The same runs now take 0.04 s. Reading an older version again costs one step for each set made since. `bench/scenarios/vector_ops` runs in 0.37 ms instead of 18 ms on wasmtime and 0.29 ms instead of 13 ms on V8. `==` on two Vectors now compiles on wasm-gc; before, the module failed validation. A program with no Vector value compiles to the same bytes as before. A function that touches a Vector is no longer offered for certification, because the certificate wall models a Vector as a plain array; `tools/certkit/fixtures/cell_at.av` loses its certificate.
 - **wasm-gc: `Map.set` no longer copies the map, and `Map.remove` no longer changes the map it was given.** `set` copied every bucket unless the compiler could prove the map had no other holder, which it cannot for a map held in a record field such as an answer module's state. A 100 000-entry state map served 2000 `Map.set` requests in 11 s under `aver run --wasm-gc` and 1.9 s on Node 26. `remove` wrote into the map it was given, so a caller that still held that map saw the key gone. Both now write into the map's arrays in place and return a new version. The version they were given stays valid, because a record of what the write replaced is kept with it. The same run now takes 0.4 s under `aver run --wasm-gc` and 0.3 s on Node. Reading an older version again costs one step for each write made since.
 - **A program with the generated loop can key its own waits by a type of its own.** The loop keys its wait by `Int`, and a hand-written `Wait.poll` keyed by a sum beside it used to be refused by the Rust door ("this program keys one wait set by 'Int' and another by 'Watch'") and to fail wasm-gc validation. In a program that answers a capability of its own, each such wait, in the entry or in a dependency, now goes through helpers generated for its key type that carry it through an `Int`-keyed wait. It answers the same keys in the same order. Its recording holds the `Int`-keyed wait. The wasm-gc wait ABI is unchanged, and `--target wasip2` runs such waits too. A program that answers no capability still keys all its waits one way.
 - **`check` no longer asks a verify block of a function no verify case can call.** A parameter of a capability resource type (`Tcp.Connection`, `Work.Job`, a job kind's handle), or of a tuple, record or sum of the module that always carries one, has no value a case can write, so such a pure branching helper failed `error[missing-verify]` with no way to satisfy it. It is now exempt, the way effectful functions are. A parameter with an empty value (`List`, `Option`, a sum with a resource-free variant) still needs its verify block.

docs/certification.md

@@ -105,7 +105,7 @@ L3 is derived by the wall (`GrammarTotal.checkTermGroup`), never read from a man
 
 Every certified export reports one class, `source-plan-v1`, with facets the wall derives from the plan: `recursive`, `mutual`, `calls`, `records`, `variants`, `strings`, `floats`.
 
-The plan grammar is the admitted subset of optimized MIR. It covers Int, Bool, Float and String literals; locals and named `let`; calls to other planned functions, including self and mutual recursion and tail calls; Int `+ - *` and the six comparisons; Bool `and`, `or`, `not`, `==` and `!=`; Float comparisons other than `!=`; String `+`, `==`, `!=` and interpolation of String parts; `if`; records with two or more fields (create in declared order, and project); user variants, `Option` and `Result` (construct and match); matches on Int, Bool and String literals and flat tuple destructuring; `Option.withDefault` and `Result.withDefault`; `Option.withDefault(Vector.get(v, i), <literal>)`; `Int.div` and `Int.mod` by a nonzero literal, or fused under `Result.withDefault` with an Int default; the empty list and `List.prepend`.
+The plan grammar is the admitted subset of optimized MIR. It covers Int, Bool, Float and String literals; locals and named `let`; calls to other planned functions, including self and mutual recursion and tail calls; Int `+ - *` and the six comparisons; Bool `and`, `or`, `not`, `==` and `!=`; Float comparisons other than `!=`; String `+`, `==`, `!=` and interpolation of String parts; `if`; records with two or more fields (create in declared order, and project); user variants, `Option` and `Result` (construct and match); matches on Int, Bool and String literals and flat tuple destructuring; `Option.withDefault` and `Result.withDefault`; `Int.div` and `Int.mod` by a nonzero literal, or fused under `Result.withDefault` with an Int default; the empty list and `List.prepend`. A function that touches a `Vector` is declined: on wasm-gc a `Vector` value is a version struct over a shared array, and the wall models it as the plain array of its elements.
 
 A function is declined, with the MIR node or type named in the reason, when it has effects, uses raw i64 slots, negates an Int (the negation helper has no wall template yet), uses an Int literal outside the i64 range, does Float arithmetic, calls through a function value, matches on a list, or uses any other node outside the subset. A function is also declined when the producer's check finds that its plan does not lower to exactly its code entry.
 

docs/wasm-gc-custom-capabilities.md

@@ -66,7 +66,7 @@ embedded runner lifts these values directly into transport-neutral
 | `Result`, `Option`, tuple, record | typed GC struct reference |
 | sum type | nominal root reference carrying a typed variant struct |
 | `List` | nullable typed cons reference |
-| `Vector` | typed mutable GC array reference |
+| `Vector` | typed GC struct reference to one version over a mutable array; read and fill it through the `Vector` helpers below |
 | `Map` | Aver's typed deterministic map reference |
 | proof-packed `List<Int>` refinement | typed GC array reference; record factories/projectors bridge its declared carrier |
 

src/codegen/cert/plan_from_mir.rs

@@ -278,16 +278,16 @@ impl TypeTableBuilder {
                 }
                 Ok(PlanTy::Result(Box::new(t), Box::new(e)))
             }
-            ("Vector", 1) => {
-                let t = arg(self, 0)?;
-                let idx = layout
-                    .vector(&canon)
-                    .ok_or_else(|| format!("type `{canon}` is not registered"))?;
-                if !self.table.vecs.iter().any(|v| v.0 == t) {
-                    self.table.vecs.push((t.clone(), idx));
-                }
-                Ok(PlanTy::Vec(Box::new(t)))
-            }
+            // A `Vector<T>` value is a version struct over its array on
+            // wasm-gc (`codegen::wasm_gc::vectors`), and reading it may
+            // reroot the versions sharing that array. The wall models a
+            // Vector as the plain array of its elements, so a function that
+            // touches one is declined rather than certified against the
+            // wrong representation.
+            ("Vector", 1) => Err(format!(
+                "type `{canon}`: a Vector is a versioned struct on wasm-gc, and the wall \
+                 models it as a plain array"
+            )),
             ("List", 1) => {
                 let t = arg(self, 0)?;
                 let idx = layout

src/codegen/wasm_gc/README.md

@@ -81,7 +81,7 @@ Aver is statically typed; the type checker has already proven what each value is
 | `List<T>`            | `(ref null $List_T)` where `$List_T = (struct (field T) (field (ref null $List_T)))` |
 | `Tuple<T1,T2,…>`     | `(ref null $Tuple_T1_T2_…)`                                            |
 | `Map<K,V>`           | `(ref null $Map_K_V)` — flat hashtable struct                          |
-| `Vector<T>`          | `(ref null (array T))` (or `$Vector_T` wrapping array + len)          |
+| `Vector<T>`          | `(ref null $Vector_T)`: a version over `(array (mut T))` (see `vectors.rs`) |
 | `Record name`        | `(ref null $Record_name)` — named struct                               |
 | `Constructor name`   | `(ref null $Constr_name)` — named struct subtype of the variant root  |
 

src/codegen/wasm_gc/body/emit.rs

@@ -168,13 +168,13 @@ pub(super) fn sum_or_record_eq_fn(ty: &crate::types::Type, ctx: &EmitCtx<'_>) ->
                 .collect();
             ctx.fn_map.list_ops.get(&canonical).and_then(|ops| ops.eq)
         }
-        crate::types::Type::Vector(_) => {
-            let canonical: String = ty
-                .display()
+        // The vector helpers are registered per `List<T>` pair.
+        crate::types::Type::Vector(inner) => {
+            let canonical: String = format!("List<{}>", inner.display())
                 .chars()
                 .filter(|c| !c.is_whitespace())
                 .collect();
-            ctx.fn_map.vfl_ops.get(&canonical).and_then(|ops| ops.eq)
+            ctx.fn_map.vfl_ops_lookup(&canonical).and_then(|ops| ops.eq)
         }
         // Map<K,V> structural eq — `__eq_Map<K,V>` slot lives in
         // MapHelperRegistry but we mirror the fn idx into