diff --git a/docs/contracts/README.md b/docs/contracts/README.md index fe1e0b99..79f72288 100644 --- a/docs/contracts/README.md +++ b/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 | 5 | +| C-132 | mut parameters of reallocating containers persist to the caller at every call position | 0.28.6 | active | fixture | 6 | | 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 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index 7833a0e3..60fa3d91 100644 --- a/docs/contracts/conformance.md +++ b/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. -132 normative sections; 812 distinct executable fixtures. +132 normative sections; 813 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)
`spec/wasm_cross/heap_result_if_bind_chain.almd` (byte-compare)
`spec/wasm_cross/heap_result_if_match_arm_frame.almd` (byte-compare)
`spec/wasm_cross/heap_result_if_record_arm.almd` (byte-compare)
`spec/wasm_cross/heap_result_if_str_int.almd` (byte-compare)
`spec/wasm_cross/heap_result_tuple_return.almd` (byte-compare)
`spec/wasm_cross/heap_result_err_interp.almd` (byte-compare)
`spec/wasm_cross/nested_match_heap_arm.almd` (byte-compare)
`spec/wasm_cross/result_heap_err_match.almd` (byte-compare)
`spec/wasm_cross/result_heap_ok_match.almd` (byte-compare)
`spec/wasm_cross/str_result_heap_bind.almd` (byte-compare)
`spec/wasm_cross/result_match_rewrap_modcall.almd` (byte-compare)
`spec/wasm_cross/variant_pair_result_return.almd` (byte-compare)
`spec/wasm_cross/record_pair_result_return.almd` (byte-compare)
`spec/wasm_cross/result_option_call_payload_return.almd` (byte-compare)
`spec/wasm_cross/closure_rich_list_capture.almd` (byte-compare)
`spec/wasm_cross/pipe_lambda_block_value.almd` (byte-compare)
`spec/wasm_cross/pipe_chain_scalar_bind.almd` (byte-compare)
`spec/wasm_cross/heap_result_if_bind.almd` (byte-compare)
`spec/wasm_cross/map_fold_heap_acc_skv.almd` (byte-compare)
`spec/wasm_cross/map_interp_string_value.almd` (byte-compare)
`spec/wasm_cross/heap_result_if_option_aggregate.almd` (byte-compare)
`spec/wasm_cross/list_enumerate_rich.almd` (byte-compare)
`spec/wasm_cross/list_float_equality_family.almd` (byte-compare)
`spec/wasm_cross/adr0005_operator_equivalence.almd` (byte-compare) | | ALS-M11 | C-108, C-369 | `spec/wasm_cross/unwrap_in_callarg.almd` (byte-compare)
`spec/wasm_cross/unwrap_in_if_arm.almd` (byte-compare)
`spec/wasm_cross/unwrap_in_recursion.almd` (byte-compare)
`spec/wasm_cross/unwrap_or_operand.almd` (byte-compare)
`spec/wasm_cross/let_unwrap_propagation.almd` (byte-compare)
`spec/wasm_cross/destructure_let_unwrap.almd` (byte-compare)
`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)
`spec/wasm_cross/list_comprehensive.almd` (byte-compare)
`spec/wasm_cross/list_sort_short.almd` (byte-compare)
`spec/wasm_cross/string_is_alphanumeric.almd` (byte-compare)
`spec/wasm_cross/string_to_upper.almd` (byte-compare)
`spec/wasm_cross/split_empty_sep.almd` (byte-compare)
`spec/wasm_cross/replace_empty_pat.almd` (byte-compare)
`spec/wasm_cross/list_minmax_str.almd` (byte-compare)
`spec/wasm_cross/list_modify_heap.almd` (byte-compare)
`spec/wasm_cross/list_set_value.almd` (byte-compare)
`spec/wasm_cross/list_update_heap.almd` (byte-compare)
`spec/wasm_cross/list_sort_str.almd` (byte-compare)
`spec/wasm_cross/whilep_str.almd` (byte-compare)
`spec/wasm_cross/chunk_str.almd` (byte-compare)
`spec/wasm_cross/fold_heap_acc.almd` (byte-compare)
`spec/wasm_cross/reduce_str.almd` (byte-compare)
`spec/wasm_cross/closure_accumulator.almd` (byte-compare)
`spec/wasm_cross/value_object_leak_loop.almd` (byte-compare)
`spec/wasm_cross/pop_heap_element.almd` (byte-compare)
`spec/wasm_cross/enumerate_unnameable_element.almd` (byte-compare)
`spec/wasm_cross/list_of_maps_loop_build.almd` (byte-compare)
`spec/wasm_cross/nested_three_level_literal.almd` (byte-compare)
`spec/wasm_cross/nested_three_level_loop_build.almd` (byte-compare)
`spec/wasm_cross/list_unique_by_str_key.almd` (byte-compare)
`spec/wasm_cross/scan_heap_acc.almd` (byte-compare)
`spec/wasm_cross/list_zip_with_typed.almd` (byte-compare)
`spec/wasm_cross/list_heapelem_rc.almd` (byte-compare)
`spec/wasm_cross/list_flatten_borrow.almd` (byte-compare)
`spec/wasm_cross/native_wall_shapes.almd` (byte-compare)
`spec/wasm_cross/unwrap_or_heap_payload.almd` (byte-compare)
`spec/wasm_cross/unwrap_or_tuple_payload_extract.almd` (byte-compare)
`spec/lang/unwrap_or_tuple_payload_bind_test.almd` (both-target test)
`spec/wasm_cross/unwrap_or_tail_result.almd` (byte-compare)
`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)
`spec/wasm_cross/bytes_push_inplace.almd` (byte-compare)
`spec/wasm_cross/mut_heap_param.almd` (byte-compare)
`spec/wasm_cross/bytes_param_writeback.almd` (byte-compare)
`spec/wasm_cross/mut_param_effect_never_err.almd` (byte-compare)
`spec/wasm_cross/effect_mut_generic_port.almd` (byte-compare)
`spec/wasm_cross/mut_param_effect_can_err.almd` (byte-compare)
`spec/wasm_cross/place_mutation.almd` (byte-compare)
`spec/wasm_cross/mut_param_branch_forward.almd` (byte-compare)
`spec/wasm_cross/sql_highlight_tokens.almd` (byte-compare)
`spec/wasm_cross/bytes_push_growth.almd` (byte-compare)
`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)
`spec/wasm_cross/bytes_push_inplace.almd` (byte-compare)
`spec/wasm_cross/mut_heap_param.almd` (byte-compare)
`spec/wasm_cross/bytes_param_writeback.almd` (byte-compare)
`spec/wasm_cross/mut_param_effect_never_err.almd` (byte-compare)
`spec/wasm_cross/effect_mut_generic_port.almd` (byte-compare)
`spec/wasm_cross/mut_param_effect_can_err.almd` (byte-compare)
`spec/wasm_cross/mut_param_err_write_visible.almd` (byte-compare)
`spec/wasm_cross/place_mutation.almd` (byte-compare)
`spec/wasm_cross/mut_param_branch_forward.almd` (byte-compare)
`spec/wasm_cross/sql_highlight_tokens.almd` (byte-compare)
`spec/wasm_cross/bytes_push_growth.almd` (byte-compare)
`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)
`tests/diagnostics/e024-unsigned-negative-literal/broken.almd` (checker)
`spec/wasm_cross/uint64_upper_half.almd` (byte-compare)
`spec/wasm_cross/sized_int_overflow_wrap.almd` (byte-compare) | | ALS-M15 | C-221 | `spec/wasm_cross/effect_slot_carrier.almd` (byte-compare)
`spec/wasm_cross/effect_fn_value.almd` (byte-compare)
`spec/lang/fallible_user_hof_test.almd` (both-target test) | | ALS-R1 | C-035 | `spec/wasm_cross/int_div_by_zero.almd` (byte-compare)
`spec/wasm_cross/match_result.almd` (byte-compare)
`spec/wasm_cross/option_result.almd` (byte-compare)
`spec/wasm_cross/early_return_control_flow.almd` (byte-compare)
`spec/wasm_cross/effect_main_guard_err.almd` (byte-compare)
`spec/wasm_cross/effect_main_guard_ok.almd` (byte-compare) | diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index 9336e207..28a37085 100644 --- a/docs/contracts/contracts.toml +++ b/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` 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 only (`Result[(T, Buf), String]`), the err arm carries no buffer, and at a `!` site the err propagates BEFORE any write-back, so the caller's slot keeps its pre-call binding (the ratified err-path order, the one the was-Unit form always realized); 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`. Boundary: the err-path buffer is READABLE only through a `??`/`match` consumer of the call, which is refused on every mut-param callee (never-err included) — native's `&mut` shows pre-err writes there, so that consumer stays walled until the ruling is carried to native; a declared-Result effect fn whose err type is not `String` stays excluded (`mut-param`). 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` 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` 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` 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." since = "0.28.6" status = "active" evidence = [ @@ -1687,6 +1687,7 @@ evidence = [ { path = "spec/wasm_cross/mut_param_effect_never_err.almd", class = "fixture" }, { 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" }, ] [[contract]] id = "C-133" @@ -2768,7 +2769,7 @@ evidence = [ id = "C-226" spec = "ALS-C7" title = "A mut parameter crossing a call boundary mutates the caller's data on both targets" -statement = "Passing a `mut` parameter to another function mutates the caller's data byte-identically native <-> wasm, in every #1207 shape: a Unit effect fn forwarding its own mut param to another effect fn (`g(mut a) = { h(a)! }`), tail recursion threading a mut Bytes buffer through an `if` arm (the Barnsley-fern chaos-game shape), a loop-heavy call chain (10k writebacks — an ownership imbalance would trap or leak only under repetition), and a growth writeback where the callee REALLOCATES (list.push through a guarded chain) so the caller must observe the successor handle. Mechanism, two halves: (1) the C-132 move-mode rewriter rotates the effect wrapper onto the bound call (`Unwrap{Block{let buf = call; wb}}` -> `Block{let buf = Unwrap{call}; wb}`), so the tree carries only proven shapes — the C-222 bind-position unwrap and a statement Block — instead of a wrapper-over-Block no lowering accepts; (2) the unit-arm assign machinery admits the write-back into the fn's OWN borrowed mut-param slot (drop-old skipped: the callee consumed the old buffer, which flowed in as the mut arg and returned as the same handle or its realloc successor), recognized structurally by VarId — the assigned temp must be call-bound with the assign target among that call's Var arguments. Before this contract every mut-param call chain fell off the wasm leg (walls naming the condition instead of the arm — the #1207 report). Excluded and honestly walled, as before: a VALUE-returning effect fn with a mut param (tuple-inside-Result plumbing, the documented C-132 exclusion). The #1770 addendum: a caller that keeps writing its own mut param AFTER a helper write-back, with the buffer reallocating during those later writes, must return the intact successor — the write-back's Assign made the param an epilogue owner ON TOP of the param pass's release, and the double dec freed the returned buffer (its freelist link zeroed the first payload word: native [1,16,...], wasm [0,0,0,0,...]). The epilogue now releases each local exactly once (the param pass skips rc_owned members), pinned by mut_param_writeback_growth and the zlib deflate helpers restored to their natural forwarding shape. EXTENDED (#2411, 0.63.0): the mutation may target a LIST FIELD of the mut record parameter — `list.push(h.kids, kid)` and `list.clear(h.xs)` where `h: mut Holder` — and the caller's record carries the grown list afterwards, byte-identical to native. Before this clause the structural leg's `push` arm accepted only a plain var receiver and refused a field with `list-push-nonvar`, while the incumbent brick refused the enclosing loop for its own reason, so the builder idiom — a `mut` record parameter accumulating into its list fields inside a `for` loop, the shape #2316 was found in — had NO wasm route at all: it built on native only, and the source gave no sign. It now routes through the copy-on-write field write the leg already owns (`lower_field_assign`, the C-033 doctrine) as `h.f = h.f + [v]` / `h.f = []`: the record block is copied, the replaced slot's credit is released, the fresh list takes its own credit, the var is rebound — no second receiver mode in the push arm, so every credit rides a path a fixture already pins. The cost model is the leg's own for any field write (a fresh record per write; the list concat is O(n) per push) and a 1000-push loop is a row of the fixture so a leak would show in the allocation ledger rather than in stdout. Element shapes covered: Int (scalar, no credit), Float (crosses the push helper as a bit pattern), String and a record (heap, the concat takes the credit); an alias taken before the push keeps the old list (C-033). DECLARED OMISSION: a nested receiver path (`h.i.xs`, `xs[i].f`) is still refused with the same `list-push-nonvar` — the field write takes one var and one field — and `tests/list_push_on_record_field_test.rs` pins that it stays a wall rather than silently widening. It predates the release: reproduced on the published v0.62.0 asset." +statement = "Passing a `mut` parameter to another function mutates the caller's data byte-identically native <-> wasm, in every #1207 shape: a Unit effect fn forwarding its own mut param to another effect fn (`g(mut a) = { h(a)! }`), tail recursion threading a mut Bytes buffer through an `if` arm (the Barnsley-fern chaos-game shape), a loop-heavy call chain (10k writebacks — an ownership imbalance would trap or leak only under repetition), and a growth writeback where the callee REALLOCATES (list.push through a guarded chain) so the caller must observe the successor handle. Mechanism, two halves: (1) the C-132 move-mode rewriter rotates the effect wrapper onto the bound call (`Unwrap{Block{let buf = call; wb}}` -> `Block{let buf = Unwrap{call}; wb}`), so the tree carries only proven shapes — the C-222 bind-position unwrap and a statement Block — instead of a wrapper-over-Block no lowering accepts; (2) the unit-arm assign machinery admits the write-back into the fn's OWN borrowed mut-param slot (drop-old skipped: the callee consumed the old buffer, which flowed in as the mut arg and returned as the same handle or its realloc successor), recognized structurally by VarId — the assigned temp must be call-bound with the assign target among that call's Var arguments. Before this contract every mut-param call chain fell off the wasm leg (walls naming the condition instead of the arm — the #1207 report). A VALUE-returning effect fn with a mut param, walled when this contract landed, is carried by C-132: the buffer rides the Result's ok arm (#1576) and its err arm (#2917), so a write made before an err reaches the caller as on native. The #1770 addendum: a caller that keeps writing its own mut param AFTER a helper write-back, with the buffer reallocating during those later writes, must return the intact successor — the write-back's Assign made the param an epilogue owner ON TOP of the param pass's release, and the double dec freed the returned buffer (its freelist link zeroed the first payload word: native [1,16,...], wasm [0,0,0,0,...]). The epilogue now releases each local exactly once (the param pass skips rc_owned members), pinned by mut_param_writeback_growth and the zlib deflate helpers restored to their natural forwarding shape. EXTENDED (#2411, 0.63.0): the mutation may target a LIST FIELD of the mut record parameter — `list.push(h.kids, kid)` and `list.clear(h.xs)` where `h: mut Holder` — and the caller's record carries the grown list afterwards, byte-identical to native. Before this clause the structural leg's `push` arm accepted only a plain var receiver and refused a field with `list-push-nonvar`, while the incumbent brick refused the enclosing loop for its own reason, so the builder idiom — a `mut` record parameter accumulating into its list fields inside a `for` loop, the shape #2316 was found in — had NO wasm route at all: it built on native only, and the source gave no sign. It now routes through the copy-on-write field write the leg already owns (`lower_field_assign`, the C-033 doctrine) as `h.f = h.f + [v]` / `h.f = []`: the record block is copied, the replaced slot's credit is released, the fresh list takes its own credit, the var is rebound — no second receiver mode in the push arm, so every credit rides a path a fixture already pins. The cost model is the leg's own for any field write (a fresh record per write; the list concat is O(n) per push) and a 1000-push loop is a row of the fixture so a leak would show in the allocation ledger rather than in stdout. Element shapes covered: Int (scalar, no credit), Float (crosses the push helper as a bit pattern), String and a record (heap, the concat takes the credit); an alias taken before the push keeps the old list (C-033). DECLARED OMISSION: a nested receiver path (`h.i.xs`, `xs[i].f`) is still refused with the same `list-push-nonvar` — the field write takes one var and one field — and `tests/list_push_on_record_field_test.rs` pins that it stays a wall rather than silently widening. It predates the release: reproduced on the published v0.62.0 asset." since = "0.56.2" status = "active" evidence = [ diff --git a/spec/wasm_cross/mut_param_effect_can_err.almd b/spec/wasm_cross/mut_param_effect_can_err.almd index 84fe571c..a692fdd9 100644 --- a/spec/wasm_cross/mut_param_effect_can_err.almd +++ b/spec/wasm_cross/mut_param_effect_can_err.almd @@ -1,8 +1,8 @@ // @contract: C-132 // #1576: a CAN-ERR effect fn with a `mut` param takes the C-132 move-mode -// tuple rewrite — `(T, Buf)` rides the ok payload only; the err arm carries no -// buffer and propagates BEFORE any write-back (the ratified err-path order, -// the same one the was-Unit form realizes). Previously this class was the +// tuple rewrite — `(T, Buf)` rides the ok payload (since #2917 the err arm +// carries the buffer too: see mut_param_err_write_visible.almd). Previously +// this class was the // last honest wall under the DDD package tree (`mut-param:can-err-effect`). // Matrix — one row per payload kind the carrier admits, crossed with the // buffer kinds and the argument places: @@ -15,9 +15,8 @@ // `mut self` (the #1622 can-err half, the DDD port spelling) // err : the last call errs before mutating; `!` propagates to main — // stderr `Error: bad`, exit 1, byte-identical on both targets. -// Not pinned here (walled on every mut-param callee, never-err included): -// a `??`/`match` consumer of the call, the only way the caller could READ -// its buffer after an err — see the C-132 statement for the boundary. +// A `??`/`match` consumer of the call, the only way the caller can READ its +// buffer after an err, is pinned in mut_param_err_write_visible.almd. type Box = { n: Int } type Pair = { a: Int, b: Int } diff --git a/spec/wasm_cross/mut_param_err_write_visible.almd b/spec/wasm_cross/mut_param_err_write_visible.almd new file mode 100644 index 00000000..31cebd08 --- /dev/null +++ b/spec/wasm_cross/mut_param_err_write_visible.almd @@ -0,0 +1,92 @@ +// @contract: C-132 +// #1871 ruling (B), #2917: a CAN-ERR effect fn that writes its `mut` param and +// THEN errs leaves the write visible to the caller, on every leg — native's +// `&mut` semantics. Every raising exit of the callee (an explicit `err(..)` +// tail, a guard exit, a propagated `x!`) carries the buffer it holds at that +// point, and the call site writes it back on BOTH arms: an unpropagated call +// (`??`, `match`, a bound Result, `let _ =`) writes back and then yields the +// Result; a `!` call writes back and then propagates, so a caller one level up +// that catches the err still sees the write. +type Log = { lines: List[String], n: Int } + +// explicit err tail after a write +effect fn push_then_err(mut xs: List[Int], v: Int) -> Int = { + list.push(xs, v) + if v > 5 then err("too big") else ok(v * 2) +} + +// guard exit after a write +effect fn push_then_guard(mut xs: List[Int], v: Int) -> Int = { + list.push(xs, v) + guard v % 2 == 0 else err("odd") + v +} + +effect fn check(v: Int) -> Int = { + guard v >= 0 else err("negative") + v +} + +// a propagated `x!` after a write (String buffer) +effect fn append_then_check(mut s: String, v: Int) -> Int = { + s = s + "<${v}>" + let w = check(v)! + w + 1 +} + +// record buffer, err after two writes +effect fn log_then_fail(mut log: Log, msg: String) -> Unit = { + log.lines = log.lines + [msg] + log.n = log.n + 1 + guard msg != "boom" else err("boom seen") + () +} + +fn show(r: Result[Int, String]) -> String = match r { + ok(v) => "ok ${v}", + err(e) => "err ${e}", +} + +// the `!` form: writes back, then propagates to ITS caller +effect fn forward(mut xs: List[Int], v: Int) -> Int = { + list.push(xs, 0) + let r = push_then_err(xs, v)! + r + 1 +} + +effect fn main() -> Unit = { + var xs: List[Int] = [] + // `??` + let a = push_then_err(xs, 9) ?? -1 + println("?? err: a=${a} xs=${xs}") + let b = push_then_err(xs, 2) ?? -1 + println("?? ok: b=${b} xs=${xs}") + // match + let m = match push_then_guard(xs, 3) { + ok(v) => "ok ${v}", + err(e) => "err ${e}", + } + println("match err: ${m} xs=${xs}") + let m2 = match push_then_guard(xs, 4) { + ok(v) => "ok ${v}", + err(e) => "err ${e}", + } + println("match ok: ${m2} xs=${xs}") + // bound Result, propagated `x!` inside the callee + var s = "s" + let r: Result[Int, String] = append_then_check(s, -3) + println("bound err: ${show(r)} s=${s}") + let r2: Result[Int, String] = append_then_check(s, 7) + println("bound ok: ${show(r2)} s=${s}") + // record buffer, `let _ =` + var log: Log = { lines: [], n: 0 } + let _ = log_then_fail(log, "hi") + let _ = log_then_fail(log, "boom") + println("log: n=${log.n} lines=${log.lines}") + // the `!` form, caught one level up + var ys: List[Int] = [1] + let f = forward(ys, 8) ?? -7 + println("forward err: f=${f} ys=${ys}") + let g = forward(ys, 3) ?? -7 + println("forward ok: g=${g} ys=${ys}") +}