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

[jasisz]

Follow-up to #1443, which fixed the VM and generated Rust. The same shape, a record holding a 100,000-cell Vector with each step doing match Vector.set(s.cells, i, x), copied the whole array on wasm-gc as well.

Cause

On wasm-gc, Vector.set wrote the array in place only when mir_arg_uniquely_owned held: a last-use local whose slot is not aliased, or a fresh collection. Otherwise it allocated a new array and array.copyd every cell. A vector read from a record field is covered by neither, so every step copied. This is the same thing #1433 found for Map.set, and wasm-gc has no reference counts to decide it at run time.

Fix: versions over one array, as #1433 did for Map

The details are in the new src/codegen/wasm_gc/vectors.rs.

• A Vector<T> value is now a version struct (arr, diff, held) over the existing (array (mut T)), and there is a diff struct (next, idx, value) for each Vector<T>. The registry allocates both for every Vector<T> in vector_order. vector_type_idx still names the array, which the internal Vector<String> of the string concat helper keeps using as it did. aver_to_wasm("Vector<T>") now names the version.
• set(v, i, x, owned) makes v current, builds a new version w over the same array, records the old cell in a diff on v pointing at w, and writes the cell. Out-of-range handling stays at the call sites, unchanged.
• current(v) -> array makes v the version that owns the array's contents. It walks the diff chain to the current version and swaps the recorded cells back, reversing the chain, the same algorithm as the map reroot. It returns at once when v is already current. Every read of the elements goes through it: get, the fused get-or, List.fromVector, eq, hash, and the capability ABI get/set helpers the Rust and JavaScript hosts use. len reads array.len directly, because every version has the same length.
• held is set on a version once another version's diff points at it. When the compiler proves the receiver unique and it is current and not held, the cell is written with nothing recorded, so a builder loop allocates nothing.
• eq of two versions that share an array copies one side first.
• Vector.new, __vector_new, Vector.fromList and the host new helper wrap their fresh array in a version with no diff.
• Side fix: == on two vectors looked the vector helpers up by the Vector<T> spelling, but they are registered under their List<T> pair. Before this change the module failed validation (expected i64, found (ref null $type)); now it compiles.

Cost: each non-owned set allocates two small structs. Reading an older version again costs one swap per set made since. A read of a current version pays one call to current and a null test.

Measurements

These are release builds, aver run --wasm-gc on wasmtime, best of 3, for tests/fixtures/vector_field_set/main.av (the same fixture as #1443, added here too so the branch stands alone):

sets	before	after
2000	0.205 s	0.038 s
20000	1.774 s	0.043 s

What remains is startup and building the 100,000-cell vector.

aver bench bench/scenarios/vector_ops.toml (the only vector_* scenario), p50:

target	before	after
wasm-gc (wasmtime)	17.88 ms	0.366 ms
wasm-gc-v8 (Node 26)	12.82 ms	0.288 ms

vector_ops fills a 5000-cell vector through a parameter that was not proven unique, so before this change every set copied the array.

A read-only probe with 200,000 fused Vector.get calls on a vector no set touches measured 9.37 ms before and 9.24 ms after, so the current call on reads costs nothing measurable.

Certification

The wall models Vector<T> as the plain array of its elements (Grammar.lean: vec t is "a wasm array of the element representation"), with Vector.get admitted fused. That is no longer the value representation, and a read may reroot. So plan_from_mir declines any function whose plan mentions a Vector type, with the reason type Vector: a Vector is a versioned struct on wasm-gc, and the wall models it as a plain array. The wall and aver-cert are unchanged. A package that claimed a vector plan anyway would be checked against the old array lowering, which no longer matches the emitted bytes.

• tools/cert_ratchet.py reports one drop: tools/certkit/fixtures/cell_at.av: cellAt. The baseline is updated with --update --allow-drop. Every other program keeps all its certified functions, bridges and law-claims (197 certified functions).
• cert_verify_accepts_fused_vector_read_and_declines_three_tampers becomes cert_declines_a_function_that_reads_a_vector, which asserts the decline and its reason.
• Only a program with a Vector value gets versions. That means a type naming one in a signature, a binding annotation, a record or variant field, or a capability boundary type, or a call to a Vector builtin or List.fromVector. The registry still keeps a Vector<T> array for every List<T> helper pair and for the string concatenation helper. In a program without a Vector value those arrays stay plain, and the from_list / to_list / eq / hash helpers are emitted exactly as on main, so the module is byte-identical. The concatenation helper's Vector<String> argument is always the bare array, in both cases.
  • Checked against main for every program under examples/, tools/certkit/fixtures, bench/scenarios and tests/fixtures that compiles on both: 525 of 558 are byte-identical. The 33 that differ all have a Vector value. Some get it through a dependency (checkers/render), through the generated wait helpers of run_wait_own_key (Vector.fromList(keys)), or through a capability type (capability_manifest).
  • The wasip2 component snapshot (greet / shout) keeps main's bytes: 2496-byte core module, same sha256.
  • a_program_without_a_vector_value_is_unchanged_by_versions pins the size and sha256 of a list, interpolation and + program to main's.
• btc-listener at 5698c8e (main.av compiled with --certify) has the same results on main and on this branch: 632 certified exports, 119 law-claims, 494 bridges, 138 declined bridges. Every function that touches a Vector there was already declined on main for another reason, such as Call Builtin(Vector.fromList). Its module grows 768,493 → 799,495 bytes (+4.0%), because a program with a Vector value versions every Vector<T>, including the ones its List<T> helpers register.
• docs/certification.md drops the fused vector read from the admitted grammar and says why.

Tests

• New tests/wasm_gc_vector_versions_spec.rs, added to the wasm-gc CI lane. Each program runs on the VM and on wasm-gc against a hand-checked answer:
  • a chain of versions read back in any order;
  • two branches from one base;
  • == between versions that share an array;
  • a builder loop whose base is kept;
  • a record field the caller keeps;
  • an older version described against a dead newer one;
  • Vector<String> and a set past the end;
  • the fixture.
• It also has a WAT check: the versioned set helper neither copies nor allocates an array.
• wasm_gc_container_read_ownership: fresh_local_set_stays_in_place_while_container_read_copies asserted that the container-read variant clones. Neither variant clones now, so the test is renamed neither_a_fresh_nor_a_container_read_set_copies. The provenance × operation matrix in that file still checks the values on the VM, wasm-gc and the self-host.
• Differential fuzz, run locally: 1500 random programs (and 150 more after the byte fix) of 40 to 120 operations each, VM against wasm-gc. The programs mix set through match, the fused withDefault spelling, an owned fill loop, a set through a record field, and reads, lengths, == and full dumps of arbitrary earlier versions. Every program gave identical output.
• Fault injection on the new guards:
  • With eq's shared-array copy removed, equality_between_versions_that_share_an_array fails.
  • With the held check removed from the owned write, every test still passes. I could not build a program where the ownership analysis grants a unique receiver to a version that another version is described against: a set result bound by a match, a withDefault of a set with a fresh default, and an argument to a function whose parameter would graduate all stayed non-owned. The check is kept because the write is unsound without it the moment the analysis grants such a receiver.
• Passing locally:
  • cargo test -p aver-lang --lib --features wasm,wasip2;
  • every suite of the wasm-gc and wasip2 CI lanes except cert_verify_spec and cert_certify_spec, which ran separately (next item);
  • with Lean: cert_certify_spec (40 tests, run again after the byte fix), cert_decode_spec and cert_one_build_spec, plus the decline test in cert_verify_spec;
  • cargo test -p aver-cert, except phase_timeout::check_fails_closed_when_a_lean_step_exceeds_the_time_limit, which looks for leftover build dirs under /tmp while this machine's temp dir is elsewhere (this PR does not touch aver-cert);
  • cargo fmt and the three CI clippy commands.
• cross_int_euclidean_divmod_vm_vs_wasm_gc overflows the compiler's stack in the local debug build. It does so with a debug build of main too, and it passes in CI.
• I did not run the full Lean-backed cert_verify_spec locally. The Certification lanes on this PR cover it.

What the wall has to learn (follow-up, not in this PR)

Merge this PR only after the wall supports the new representation. Until then the producer declines any function whose plan mentions a Vector.

Types. These are per Vector<T>, in the one rec group, only in a program with a Vector value.

• $arr_T = (array (mut T)). This is main's type, and it is still vecStruct t for the concatenation helper's Vector<String>.
• $vec_T = (struct (field (mut (ref null $arr_T))) (field (mut (ref null $diff_T))) (field (mut i32))), with fields arr, diff and held. This is the value type of a Vector<T>.
• $diff_T = (struct (field (mut (ref null $vec_T))) (field (mut i32)) (field (mut T))), with fields next, idx and value.

For Vector<Int> in a bignum module these are, for example, $arr = 3, $vec = 11 and $diff = 12, and T is (ref null $aint).

Helper bytes for Vector<Int>. Sizes are body sizes including the size prefix; "main" is the same helper on main.

helper	main	this PR	kind
current(v) -> $arr (new; the reroot)	—	219	two loops; writes struct.set / array.set
set(v, i, x, owned) -> $vec (new)	—	82	straight-line; calls current; allocates two structs; struct.set and array.set
from_list	107	114	loop; wraps the result in a fresh version
to_list	59	68	loop; calls current first
eq	79	148	loop; calls current on both; copies one side when they share an array
hash	68	77	loop; calls current first
ABI new / len / get / set (for Vector<Unit>)	8 / 7 / 11 / 12	15 / 11 / 13 / 14	new wraps; len adds a struct.get; get/set call current

Inline code at the call sites also changes:

• Vector.len adds one struct.get $vec 0 before array.len.
• The fused Option.withDefault(Vector.get(v, i), lit) (the wall's vecGetOrB) reads array.len through struct.get, and calls current before array.get.
• The boxed get and set call current and set.
• Vector.new, __vector_new and Vector.fromList end in ref.null $diff; i32.const 0; struct.new $vec.

What can be pinned byte for byte. Every helper is a fixed template per T, parameterized only by the three type indices, the element value type and the current function index. So each can be pinned the way the wall pins __aint_to_index.

• set and the four ABI helpers are straight-line.
• current, eq, hash, from_list and to_list contain loops. The wall's WInstr has no loop / br / struct.set / array.set / array.new_default / array.copy / ref.eq, so it cannot execute these today. It also models WVal as trees (structv / arr values), with no store or identity, so it cannot express two versions sharing one mutable array. Either the machine learns a store with references and those instructions, or current and set enter as host-style contracts with the properties below, each proved once against its pinned template.

Properties that keep the plan's vec t model (every version reads its own contents) true. They are stated over a store H. contents_H(v) is H.arr(v) when H.diff(v) is null, and otherwise contents_H(H.diff(v).next) with cell idx replaced by value.

1. Representation. SRepr (.vec t vs) v iff v is a $vec_T reference and contents_H(v) = ws with SReprL vs ws. The length bound stays.
2. current(v)
   • Returns a with a = H'.arr(v), H'.diff(v) = null and H'.array(a) = contents_H(v).
   • It is a frame for meaning: for every $vec_T reference u, contents_H'(u) = contents_H(u). Only the representation of the chain changes.
   • It terminates, because the chain is finite and acyclic, which every helper preserves.
3. set(v, i, x, 0), for i < |contents_H(v)|:
   • Returns a fresh w with contents_H'(w) = contents_H(v)[i := x].
   • Every other version keeps its contents (contents_H'(u) = contents_H(u) for all u ≠ w), including v itself.
   • Afterwards H'.held(w) = 1.
4. set(v, i, x, 1) writes in place and returns v. This is sound only when held(v) = 0 and nothing reads v again. The first half holds when held(u) = 1 for every u that some diff's next points at: set sets held on the version it describes against, and current sets it on each version it restores. That invariant must be proved. The second half is the compiler's static mir_arg_uniquely_owned claim, which the wall cannot check. So a certified plan should either be lowered with owned = 0 everywhere, or cite the last-use fact as a checked premise.
5. Reads (len, the fused get, to_list, hash, the ABI get) observe exactly contents_H(v). len reads the array directly, which is sound because every version of a lineage shares one array and set never resizes it.
6. eq(a, b) equals elementwise equality of contents_H(a) and contents_H(b). When both share an array, it compares a copy of contents_H(a) taken before current(b) reroots.