State in C-132 that a mut-param callee sees the pre-call value of the global its argument is rooted at

docs/contracts/README.md

@@ -166,7 +166,7 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1
 | C-129 | list.chunk / list.windows non-positive sizes: negative keeps the promoted norm, zero aborts in the T6 form | 0.28.4 | active | fixture | 4 |
 | C-130 | option/map combinators hand back OWNED heap results (no bare pass-through handles) | 0.28.5 | active | fixture | 2 |
 | C-131 | Loop-rebuilt buffers are O(n): COW guards only LIVE aliases, and LICM never hoists heap allocations | 0.28.6 | active | fixture | 2 |
-| C-132 | mut parameters of reallocating containers persist to the caller at every call position | 0.28.6 | active | fixture | 6 |
+| C-132 | mut parameters of reallocating containers persist to the caller at every call position | 0.28.6 | active | fixture | 8 |
 | C-133 | env.get observes the host environment identically on native and wasm | 0.29.0 | active | fixture | 1 |
 | C-134 | Vendored-libm atan / tanh are byte-identical cross-target | 0.30.0 | active | fuzz(3000) | 1 |
 | C-135 | Declared-Unit effect fn ABI agrees between def and every call site | 0.30.0 | active | fixture | 1 |

docs/contracts/conformance.md

@@ -11,7 +11,7 @@
 > (spec-coverage + evidence-class >= fixture for every active contract), so this
 > page cannot legitimately contain an empty Fixtures cell.
 
-134 normative sections; 815 distinct executable fixtures.
+134 normative sections; 817 distinct executable fixtures.
 
 | Section | Contracts | Fixtures (how CI runs each) |
 |---------|-----------|------------------------------|
@@ -96,7 +96,7 @@
 | ALS-M10 | C-106, C-115, C-163, C-165, C-166, C-287, C-288, C-289, C-291 | `spec/wasm_cross/heap_result_if_append.almd` (byte-compare)<br>`spec/wasm_cross/heap_result_if_bind_chain.almd` (byte-compare)<br>`spec/wasm_cross/heap_result_if_match_arm_frame.almd` (byte-compare)<br>`spec/wasm_cross/heap_result_if_record_arm.almd` (byte-compare)<br>`spec/wasm_cross/heap_result_if_str_int.almd` (byte-compare)<br>`spec/wasm_cross/heap_result_tuple_return.almd` (byte-compare)<br>`spec/wasm_cross/heap_result_err_interp.almd` (byte-compare)<br>`spec/wasm_cross/nested_match_heap_arm.almd` (byte-compare)<br>`spec/wasm_cross/result_heap_err_match.almd` (byte-compare)<br>`spec/wasm_cross/result_heap_ok_match.almd` (byte-compare)<br>`spec/wasm_cross/str_result_heap_bind.almd` (byte-compare)<br>`spec/wasm_cross/result_match_rewrap_modcall.almd` (byte-compare)<br>`spec/wasm_cross/variant_pair_result_return.almd` (byte-compare)<br>`spec/wasm_cross/record_pair_result_return.almd` (byte-compare)<br>`spec/wasm_cross/result_option_call_payload_return.almd` (byte-compare)<br>`spec/wasm_cross/closure_rich_list_capture.almd` (byte-compare)<br>`spec/wasm_cross/pipe_lambda_block_value.almd` (byte-compare)<br>`spec/wasm_cross/pipe_chain_scalar_bind.almd` (byte-compare)<br>`spec/wasm_cross/heap_result_if_bind.almd` (byte-compare)<br>`spec/wasm_cross/map_fold_heap_acc_skv.almd` (byte-compare)<br>`spec/wasm_cross/map_interp_string_value.almd` (byte-compare)<br>`spec/wasm_cross/heap_result_if_option_aggregate.almd` (byte-compare)<br>`spec/wasm_cross/list_enumerate_rich.almd` (byte-compare)<br>`spec/wasm_cross/list_float_equality_family.almd` (byte-compare)<br>`spec/wasm_cross/adr0005_operator_equivalence.almd` (byte-compare) |
 | ALS-M11 | C-108, C-369 | `spec/wasm_cross/unwrap_in_callarg.almd` (byte-compare)<br>`spec/wasm_cross/unwrap_in_if_arm.almd` (byte-compare)<br>`spec/wasm_cross/unwrap_in_recursion.almd` (byte-compare)<br>`spec/wasm_cross/unwrap_or_operand.almd` (byte-compare)<br>`spec/wasm_cross/let_unwrap_propagation.almd` (byte-compare)<br>`spec/wasm_cross/destructure_let_unwrap.almd` (byte-compare)<br>`spec/wasm_cross/lambda_failure_channel.almd` (byte-compare) |
 | ALS-M12 | C-045, C-100, C-101, C-147, C-148, C-141, C-164, C-168, C-172, C-218 | `spec/wasm_cross/list_string_param_join_len.almd` (byte-compare)<br>`spec/wasm_cross/list_comprehensive.almd` (byte-compare)<br>`spec/wasm_cross/list_sort_short.almd` (byte-compare)<br>`spec/wasm_cross/string_is_alphanumeric.almd` (byte-compare)<br>`spec/wasm_cross/string_to_upper.almd` (byte-compare)<br>`spec/wasm_cross/split_empty_sep.almd` (byte-compare)<br>`spec/wasm_cross/replace_empty_pat.almd` (byte-compare)<br>`spec/wasm_cross/list_minmax_str.almd` (byte-compare)<br>`spec/wasm_cross/list_modify_heap.almd` (byte-compare)<br>`spec/wasm_cross/list_set_value.almd` (byte-compare)<br>`spec/wasm_cross/list_update_heap.almd` (byte-compare)<br>`spec/wasm_cross/list_sort_str.almd` (byte-compare)<br>`spec/wasm_cross/whilep_str.almd` (byte-compare)<br>`spec/wasm_cross/chunk_str.almd` (byte-compare)<br>`spec/wasm_cross/fold_heap_acc.almd` (byte-compare)<br>`spec/wasm_cross/reduce_str.almd` (byte-compare)<br>`spec/wasm_cross/closure_accumulator.almd` (byte-compare)<br>`spec/wasm_cross/value_object_leak_loop.almd` (byte-compare)<br>`spec/wasm_cross/pop_heap_element.almd` (byte-compare)<br>`spec/wasm_cross/enumerate_unnameable_element.almd` (byte-compare)<br>`spec/wasm_cross/list_of_maps_loop_build.almd` (byte-compare)<br>`spec/wasm_cross/nested_three_level_literal.almd` (byte-compare)<br>`spec/wasm_cross/nested_three_level_loop_build.almd` (byte-compare)<br>`spec/wasm_cross/list_unique_by_str_key.almd` (byte-compare)<br>`spec/wasm_cross/scan_heap_acc.almd` (byte-compare)<br>`spec/wasm_cross/list_zip_with_typed.almd` (byte-compare)<br>`spec/wasm_cross/list_heapelem_rc.almd` (byte-compare)<br>`spec/wasm_cross/list_flatten_borrow.almd` (byte-compare)<br>`spec/wasm_cross/native_wall_shapes.almd` (byte-compare)<br>`spec/wasm_cross/unwrap_or_heap_payload.almd` (byte-compare)<br>`spec/wasm_cross/unwrap_or_tuple_payload_extract.almd` (byte-compare)<br>`spec/lang/unwrap_or_tuple_payload_bind_test.almd` (both-target test)<br>`spec/wasm_cross/unwrap_or_tail_result.almd` (byte-compare)<br>`spec/wasm_cross/pipe_unwrap_or_family.almd` (byte-compare) |
-| ALS-M13 | C-061, C-110, C-132, C-136, C-324, C-325, C-326 | `spec/wasm_cross/mut_map_param.almd` (byte-compare)<br>`spec/wasm_cross/bytes_push_inplace.almd` (byte-compare)<br>`spec/wasm_cross/mut_heap_param.almd` (byte-compare)<br>`spec/wasm_cross/bytes_param_writeback.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_effect_never_err.almd` (byte-compare)<br>`spec/wasm_cross/effect_mut_generic_port.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_effect_can_err.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_err_write_visible.almd` (byte-compare)<br>`spec/wasm_cross/place_mutation.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_branch_forward.almd` (byte-compare)<br>`spec/wasm_cross/sql_highlight_tokens.almd` (byte-compare)<br>`spec/wasm_cross/bytes_push_growth.almd` (byte-compare)<br>`spec/wasm_cross/gzip_inflate_members.almd` (byte-compare) |
+| ALS-M13 | C-061, C-110, C-132, C-136, C-324, C-325, C-326 | `spec/wasm_cross/mut_map_param.almd` (byte-compare)<br>`spec/wasm_cross/bytes_push_inplace.almd` (byte-compare)<br>`spec/wasm_cross/mut_heap_param.almd` (byte-compare)<br>`spec/wasm_cross/bytes_param_writeback.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_effect_never_err.almd` (byte-compare)<br>`spec/wasm_cross/effect_mut_generic_port.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_effect_can_err.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_err_write_visible.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_global_callee_sees_precall.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_global_no_reach_in_place.almd` (byte-compare)<br>`spec/wasm_cross/place_mutation.almd` (byte-compare)<br>`spec/wasm_cross/mut_param_branch_forward.almd` (byte-compare)<br>`spec/wasm_cross/sql_highlight_tokens.almd` (byte-compare)<br>`spec/wasm_cross/bytes_push_growth.almd` (byte-compare)<br>`spec/wasm_cross/gzip_inflate_members.almd` (byte-compare) |
 | ALS-M14 | C-173, C-179, C-180 | `spec/wasm_cross/unsigned_literal_domain.almd` (byte-compare)<br>`tests/diagnostics/e024-unsigned-negative-literal/broken.almd` (checker)<br>`spec/wasm_cross/uint64_upper_half.almd` (byte-compare)<br>`spec/wasm_cross/sized_int_overflow_wrap.almd` (byte-compare) |
 | ALS-M15 | C-221 | `spec/wasm_cross/effect_slot_carrier.almd` (byte-compare)<br>`spec/wasm_cross/effect_fn_value.almd` (byte-compare)<br>`spec/lang/fallible_user_hof_test.almd` (both-target test) |
 | ALS-R1 | C-035 | `spec/wasm_cross/int_div_by_zero.almd` (byte-compare)<br>`spec/wasm_cross/match_result.almd` (byte-compare)<br>`spec/wasm_cross/option_result.almd` (byte-compare)<br>`spec/wasm_cross/early_return_control_flow.almd` (byte-compare)<br>`spec/wasm_cross/effect_main_guard_err.almd` (byte-compare)<br>`spec/wasm_cross/effect_main_guard_ok.almd` (byte-compare) |

docs/contracts/contracts.toml

@@ -1678,7 +1678,7 @@ evidence  = [
 id        = "C-132"
 spec      = "ALS-M13"
 title     = "mut parameters of reallocating containers persist to the caller at every call position"
-statement = "A `mut` parameter of a REALLOCATING container (List, String, Bytes) mutated in place inside the callee persists to the caller on wasm exactly as native, at EVERY call position — statement, Bind/Assign RHS, nested expression, loop bodies — and for both bare-var and record-FIELD arguments (`push9(b.items, 7)` writes the buffer back into the field). Value-returning callees return an (orig, buffer) tuple destructured at the call site; Unit callees return the buffer. Previously only Unit callees in statement position were lowered: `let i = push9(v, 7)` pushed into a discarded copy (wasm len=1 vs native len=3, silent len=0 from empty; a real MLP printed loss 0.0), the #705 class.The SAME persistence holds through a PLAIN (non-`mut`) `Bytes` parameter, reached by a different route: the byte-writer family (`set_*`/`append_*`/`write_*`, plus `fill`/`copy_from`/`copy_within`) is `@intrinsic`s whose mutation lives in the native `&mut Vec<u8>` signature, so the `.almd` declaration carries no `mut` marker while the effect is identical — a callee writing into a `Bytes` param mutates the CALLER's buffer on both targets, and a temporary argument (legal here, since E032 only forbids one for a declared `mut` param) simply has no observable slot. Both backends always agreed; the INTERPRETER did not until 2026-08-15 — its #1022 copy-out fired only on `param.is_mut`, so the write died at the frame boundary and the third judge voted the unmodified buffer, which the first scheduled both-arch fuzz night surfaced as a false `both targets disagree with reference interpreter` (run 31861833115, seed 509789329843 index 150, #1436). The interp now copies a `Bytes` param out by TYPE as well as by declaration. EXTENDED (#1576, 0.61.2): a CAN-ERR effect fn with a `mut` param takes the same tuple rewrite — `(T, Buf)` rides the OK payload; every payload kind the carrier admits pins byte-identical — Int, String, record, List, Option, a declared-Result `T!` (stripped to its raw payload first: `(Result, Buf)` had double-layered the carrier, structural `ok(22)` vs native `22`, and an INVALID module on the incumbent), and a scalar tuple — crossed with record/List/String buffers, bare-var and record-FIELD argument places, nested `!` forwarding, and a generic bound over an `effect fn` protocol method with `mut self` (the DDD port spelling; `spec/gauntlet/pkg/mut_port` now runs). Two caller-side holes closed with it: a RESOLVED cross-module call (`CallTarget::Module`, the mono instance's `place_order.place_order(repo, ..)`) and a `Type.method` spelled from another module than the method's (the bound's `MemoryOrderRepo.save` from `place_order`) were never rewritten, so the callee's returned buffer was dropped — native `rev=$37.50`, wasm `rev=$0.00`. A declared-Result effect fn whose err type is not `String` stays excluded (`mut-param`). AMENDED (#1871 ruling (B), #2917): a write the callee makes to its `mut` param BEFORE it errs is VISIBLE to the caller, on wasm exactly as native's `&mut`. The buffer rides the err arm too: every raising exit of the callee — an explicit `err(..)` tail, a guard exit, every `x!`/`x?` propagation inside it — carries the buffer it holds at that point, and the call site writes it back on BOTH arms. An unpropagated call (a bound Result, `??`, `match`, `let _ =`) writes back, then yields ok/err at its declared Result type; a `!` call writes back, then propagates, so a caller one level up that catches the err reads the write. This withdraws the #1576 order (the err propagated before any write-back and the caller's slot kept its pre-call binding), which went unobserved only while every consumer that could read the err-path buffer was walled. `mut_param_err_write_visible.almd` pins explicit-err, guard and propagated-`!` exits after a write, read through `??`, `match`, a bound Result, `let _ =` and a `!` forwarded one level up, over List, String and record buffers. SUPERSEDED (#2466, dialect epoch 5): the plain-`Bytes`-parameter route is closed. The byte-writer family now declares its receiver `mut` (the native `&mut Vec<u8>` first parameter made explicit on the surface, gated by scripts/check-mut-receivers.sh), so a callee that writes its caller's buffer declares `mut b: Bytes` and takes this contract's declared-`mut` route, and a plain parameter or a temporary argument to a writer is E032 — the checker, not a target, now decides that the caller's buffer changes. `bytes_param_writeback.almd` carries its helpers as `mut` parameters, and `bytes_clear_mut_param.almd` pins `bytes.clear` through a `mut` parameter in both write-back shapes."
+statement = "A `mut` parameter of a REALLOCATING container (List, String, Bytes) mutated in place inside the callee persists to the caller on wasm exactly as native, at EVERY call position — statement, Bind/Assign RHS, nested expression, loop bodies — and for both bare-var and record-FIELD arguments (`push9(b.items, 7)` writes the buffer back into the field). Value-returning callees return an (orig, buffer) tuple destructured at the call site; Unit callees return the buffer. Previously only Unit callees in statement position were lowered: `let i = push9(v, 7)` pushed into a discarded copy (wasm len=1 vs native len=3, silent len=0 from empty; a real MLP printed loss 0.0), the #705 class.The SAME persistence holds through a PLAIN (non-`mut`) `Bytes` parameter, reached by a different route: the byte-writer family (`set_*`/`append_*`/`write_*`, plus `fill`/`copy_from`/`copy_within`) is `@intrinsic`s whose mutation lives in the native `&mut Vec<u8>` signature, so the `.almd` declaration carries no `mut` marker while the effect is identical — a callee writing into a `Bytes` param mutates the CALLER's buffer on both targets, and a temporary argument (legal here, since E032 only forbids one for a declared `mut` param) simply has no observable slot. Both backends always agreed; the INTERPRETER did not until 2026-08-15 — its #1022 copy-out fired only on `param.is_mut`, so the write died at the frame boundary and the third judge voted the unmodified buffer, which the first scheduled both-arch fuzz night surfaced as a false `both targets disagree with reference interpreter` (run 31861833115, seed 509789329843 index 150, #1436). The interp now copies a `Bytes` param out by TYPE as well as by declaration. EXTENDED (#1576, 0.61.2): a CAN-ERR effect fn with a `mut` param takes the same tuple rewrite — `(T, Buf)` rides the OK payload; every payload kind the carrier admits pins byte-identical — Int, String, record, List, Option, a declared-Result `T!` (stripped to its raw payload first: `(Result, Buf)` had double-layered the carrier, structural `ok(22)` vs native `22`, and an INVALID module on the incumbent), and a scalar tuple — crossed with record/List/String buffers, bare-var and record-FIELD argument places, nested `!` forwarding, and a generic bound over an `effect fn` protocol method with `mut self` (the DDD port spelling; `spec/gauntlet/pkg/mut_port` now runs). Two caller-side holes closed with it: a RESOLVED cross-module call (`CallTarget::Module`, the mono instance's `place_order.place_order(repo, ..)`) and a `Type.method` spelled from another module than the method's (the bound's `MemoryOrderRepo.save` from `place_order`) were never rewritten, so the callee's returned buffer was dropped — native `rev=$37.50`, wasm `rev=$0.00`. A declared-Result effect fn whose err type is not `String` stays excluded (`mut-param`). AMENDED (#1871 ruling (B), #2917): a write the callee makes to its `mut` param BEFORE it errs is VISIBLE to the caller, on wasm exactly as native's `&mut`. The buffer rides the err arm too: every raising exit of the callee — an explicit `err(..)` tail, a guard exit, every `x!`/`x?` propagation inside it — carries the buffer it holds at that point, and the call site writes it back on BOTH arms. An unpropagated call (a bound Result, `??`, `match`, `let _ =`) writes back, then yields ok/err at its declared Result type; a `!` call writes back, then propagates, so a caller one level up that catches the err reads the write. This withdraws the #1576 order (the err propagated before any write-back and the caller's slot kept its pre-call binding), which went unobserved only while every consumer that could read the err-path buffer was walled. `mut_param_err_write_visible.almd` pins explicit-err, guard and propagated-`!` exits after a write, read through `??`, `match`, a bound Result, `let _ =` and a `!` forwarded one level up, over List, String and record buffers. SUPERSEDED (#2466, dialect epoch 5): the plain-`Bytes`-parameter route is closed. The byte-writer family now declares its receiver `mut` (the native `&mut Vec<u8>` first parameter made explicit on the surface, gated by scripts/check-mut-receivers.sh), so a callee that writes its caller's buffer declares `mut b: Bytes` and takes this contract's declared-`mut` route, and a plain parameter or a temporary argument to a writer is E032 — the checker, not a target, now decides that the caller's buffer changes. `bytes_param_writeback.almd` carries its helpers as `mut` parameters, and `bytes_clear_mut_param.almd` pins `bytes.clear` through a `mut` parameter in both write-back shapes. AMENDED (#3103 ruling (A)): a `mut` argument is COPIED IN and written back. A callee that reads the module-level `var` its argument is rooted at — bare or through a field path, directly, through another fn, or through a closure it calls — sees the global's PRE-call value until the call returns, on every leg; the write-back then stores the callee's buffer into the place, overwriting a write the callee made to that same place (a write to another part of the global is kept). The structural wasm leg had handed the callee the global's own block, so a read of the global inside the call printed the callee's in-progress push where native and the interpreter printed the pre-call value. The wasm leg pays the copy only when the callee can REACH that global (a compile-time over-approximation over the call graph: a call through a closure or fn value reaches every global); a callee that cannot keeps the in-place, zero-copy call. `mut_param_global_callee_sees_precall.almd` pins a bare global, a field, a nested field, a reach through another fn and one through a closure; `mut_param_global_no_reach_in_place.almd` pins a callee that cannot reach the global."
 since     = "0.28.6"
 status    = "active"
 evidence  = [
@@ -1688,6 +1688,8 @@ evidence  = [
   { path = "spec/wasm_cross/effect_mut_generic_port.almd", class = "fixture" },
   { path = "spec/wasm_cross/mut_param_effect_can_err.almd", class = "fixture" },
   { path = "spec/wasm_cross/mut_param_err_write_visible.almd", class = "fixture" },
+  { path = "spec/wasm_cross/mut_param_global_callee_sees_precall.almd", class = "fixture" },
+  { path = "spec/wasm_cross/mut_param_global_no_reach_in_place.almd", class = "fixture" },
 ]
 [[contract]]
 id        = "C-133"