diff --git a/docs/contracts/README.md b/docs/contracts/README.md index c293635a..e9823028 100644 --- a/docs/contracts/README.md +++ b/docs/contracts/README.md @@ -379,7 +379,7 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1 | C-342 | bytes.copy_from with a negative length or offset copies nothing on both targets | 0.62.0 | active | fixture | 1 | | C-343 | A tail `!` over a declared-Result plain callee yields the payload in a lifted effect fn | 0.63.0 | active | fixture | 1 | | C-344 | guard-else-err inside a call-argument block after a Result bind runs on every leg | 0.63.0 | active | fixture | 1 | -| C-345 | An effect call passed as a Result/Option parameter keeps its Result at every parameter index | 0.63.0 | active | fixture | 1 | +| C-345 | A Result passed as a call argument keeps its Result at every parameter index, generic parameters included | 0.63.0 | active | fixture | 2 | | C-346 | A heap-payload ?? lowers on the incumbent leg as a call argument and as a match subject | 0.63.0 | active | fixture | 1 | | C-347 | Operator round trips over a known literal print that literal on both targets | 0.63.0 | active | fixture | 1 | | C-348 | Byte-indexed string slices validate UTF-8 boundaries | 0.63.0 | active | fixture | 1 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index f2415c7d..07ce4830 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. -134 normative sections; 823 distinct executable fixtures. +134 normative sections; 824 distinct executable fixtures. | Section | Contracts | Fixtures (how CI runs each) | |---------|-----------|------------------------------| @@ -30,7 +30,7 @@ | ALS-C2 | C-014 | `spec/wasm_cross/set_insertion_order.almd` (byte-compare)
`spec/wasm_cross/set_index_order.almd` (byte-compare)
`spec/wasm_cross/map_set_index_threshold.almd` (byte-compare) | | ALS-C3 | C-015, C-124, C-185 | `spec/wasm_cross/compound_eq.almd` (byte-compare)
`spec/wasm_cross/deep_eq_heap.almd` (byte-compare)
`spec/wasm_cross/map_set_eq.almd` (byte-compare)
`spec/wasm_cross/variant_record_literal_equality.almd` (byte-compare)
`spec/wasm_cross/unique_non_flat_element.almd` (byte-compare)
`spec/wasm_cross/list_of_tuples_equality.almd` (byte-compare)
`spec/wasm_cross/map_rich_variant_key.almd` (byte-compare)
`spec/wasm_cross/value_deep_eq.almd` (byte-compare)
`spec/wasm_cross/fan_any_early_winner.almd` (byte-compare) | | ALS-C4 | C-034, C-354 | `spec/wasm_cross/list_insert_clamp.almd` (byte-compare)
`spec/wasm_cross/list_remove_at_oob.almd` (byte-compare)
`spec/wasm_cross/list_swap_oob.almd` (byte-compare)
`spec/wasm_cross/list_slice_oob.almd` (byte-compare)
`spec/wasm_cross/list_sort_short.almd` (byte-compare)
`spec/wasm_cross/list_with_capacity.almd` (byte-compare)
`spec/wasm_cross/negative_offset_and_width_totality.almd` (byte-compare)
`spec/wasm_cross/repeat_size_ceiling.almd` (byte-compare)
`spec/wasm_cross/matrix_slice_rows_domain.almd` (byte-compare)
`spec/wasm_fail/matrix_conv1d_stride_aborts.almd` (both-target test) | -| ALS-C5 | C-033, C-125, C-131, C-150, C-213, C-337, C-340, C-342, C-343, C-344, C-345, C-346 | `spec/wasm_cross/alias_cow.almd` (byte-compare)
`spec/lang/alias_cow_test.almd` (both-target test)
`spec/wasm_cross/module_var_alias_cow.almd` (byte-compare)
`spec/wasm_cross/witness_straightline.almd` (byte-compare)
`spec/wasm_cross/map_set_in_place.almd` (byte-compare)
`spec/wasm_cross/list_push_on_record_field.almd` (byte-compare)
`spec/wasm_cross/bytes_set_value_semantics.almd` (byte-compare)
`spec/wasm_cross/loop_buffer_churn.almd` (byte-compare)
`spec/wasm_cross/loop_push_trailing_increment.almd` (byte-compare)
`spec/wasm_cross/ctor_var_copy_semantics.almd` (byte-compare)
`spec/wasm_cross/bytes_writer_family.almd` (byte-compare)
`spec/wasm_cross/bytes_temp_receiver.almd` (byte-compare)
`spec/wasm_cross/endian_auto_import.almd` (byte-compare)
`spec/wasm_cross/bytes_copy_within_offset_domain.almd` (byte-compare)
`spec/wasm_cross/bytes_search_edit_family.almd` (byte-compare)
`spec/wasm_cross/unwrap_or_strict_default.almd` (byte-compare)
`spec/wasm_cross/get_or_strict_default.almd` (byte-compare)
`spec/wasm_cross/bytes_copy_from_negative_len.almd` (byte-compare)
`spec/wasm_cross/tail_bang_over_declared_result_callee.almd` (byte-compare)
`spec/wasm_cross/guard_err_in_call_arg_block.almd` (byte-compare)
`spec/wasm_cross/result_param_not_first.almd` (byte-compare)
`spec/wasm_cross/unwrap_or_heap_arg_and_subject.almd` (byte-compare) | +| ALS-C5 | C-033, C-125, C-131, C-150, C-213, C-337, C-340, C-342, C-343, C-344, C-345, C-346 | `spec/wasm_cross/alias_cow.almd` (byte-compare)
`spec/lang/alias_cow_test.almd` (both-target test)
`spec/wasm_cross/module_var_alias_cow.almd` (byte-compare)
`spec/wasm_cross/witness_straightline.almd` (byte-compare)
`spec/wasm_cross/map_set_in_place.almd` (byte-compare)
`spec/wasm_cross/list_push_on_record_field.almd` (byte-compare)
`spec/wasm_cross/bytes_set_value_semantics.almd` (byte-compare)
`spec/wasm_cross/loop_buffer_churn.almd` (byte-compare)
`spec/wasm_cross/loop_push_trailing_increment.almd` (byte-compare)
`spec/wasm_cross/ctor_var_copy_semantics.almd` (byte-compare)
`spec/wasm_cross/bytes_writer_family.almd` (byte-compare)
`spec/wasm_cross/bytes_temp_receiver.almd` (byte-compare)
`spec/wasm_cross/endian_auto_import.almd` (byte-compare)
`spec/wasm_cross/bytes_copy_within_offset_domain.almd` (byte-compare)
`spec/wasm_cross/bytes_search_edit_family.almd` (byte-compare)
`spec/wasm_cross/unwrap_or_strict_default.almd` (byte-compare)
`spec/wasm_cross/get_or_strict_default.almd` (byte-compare)
`spec/wasm_cross/bytes_copy_from_negative_len.almd` (byte-compare)
`spec/wasm_cross/tail_bang_over_declared_result_callee.almd` (byte-compare)
`spec/wasm_cross/guard_err_in_call_arg_block.almd` (byte-compare)
`spec/wasm_cross/result_param_not_first.almd` (byte-compare)
`spec/wasm_cross/result_generic_param_arg.almd` (byte-compare)
`spec/wasm_cross/unwrap_or_heap_arg_and_subject.almd` (byte-compare) | | ALS-C6 | C-039 | `spec/wasm_cross/map_set_typechange.almd` (byte-compare)
`spec/wasm_cross/map_set_ops.almd` (byte-compare) | | ALS-C7 | C-036, C-224, C-226 | `spec/wasm_cross/records_variants.almd` (byte-compare)
`spec/wasm_cross/match_result.almd` (byte-compare)
`spec/wasm_cross/closures_and_variants.almd` (byte-compare)
`spec/wasm_cross/playground_default.almd` (byte-compare)
`spec/wasm_cross/match_container_literal.almd` (byte-compare)
`spec/wasm_cross/match_payload_string_literal.almd` (byte-compare)
`spec/wasm_cross/record_default_field_omitted.almd` (byte-compare)
`spec/wasm_cross/if_let_guard_let.almd` (byte-compare)
`spec/wasm_cross/mut_param_call_chain.almd` (byte-compare)
`spec/wasm_cross/mut_param_writeback_growth.almd` (byte-compare)
`spec/wasm_cross/list_push_on_record_field.almd` (byte-compare) | | ALS-C8 | C-038 | `spec/wasm_cross/sized_int_record_fields.almd` (byte-compare)
`spec/wasm_cross/sized_numeric_literals.almd` (byte-compare) | diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index 1768d331..c2b430e9 100644 --- a/docs/contracts/contracts.toml +++ b/docs/contracts/contracts.toml @@ -4227,12 +4227,13 @@ evidence = [ [[contract]] id = "C-345" spec = "ALS-C5" -title = "An effect call passed as a Result/Option parameter keeps its Result at every parameter index" -statement = "When an effect fn call is the argument for a parameter declared `Result[..]` or `T?`, the callee receives the CARRIER (Ok/Err, some/none) on every leg, whatever the parameter's index: `show(\"a\", f(1))` with `show(tag: String, r: Result[Int, String])` prints `a=ok 1`, and `f(-1)` in the same position prints the Err. The auto-`?` desugar exempted only ARGUMENT 0 of a callee whose FIRST param is Result/Option (#558), so a Result param at index ≥ 1 had its effect-call argument unwrapped to the payload — native emitted `show(tag, f(1)?)` (rustc E0308, a build failure), the incumbent wasm leg failed validation (`expected i32, found i64`) and the structural leg walled `ty-mismatch` — an accepted program no leg could build (#1970). The exemption is a per-parameter flag derived from the signature table now, consulted at every argument index; the `result.*`/`option.*` intrinsic fallback still covers argument 0." +title = "A Result passed as a call argument keeps its Result at every parameter index, generic parameters included" +statement = "When a call's Result is the argument for a parameter that accepts a Result — one declared `Result[..]` or `T?`, or a type variable instantiated at Result (`id(int.parse(\"7\"))` with `fn id[T](x: T) -> T`, a `list.fold` seeded with a Result-returning call) — the callee receives the CARRIER (Ok/Err, some/none) on every leg, whatever the parameter's index: `show(\"a\", f(1))` with `show(tag: String, r: Result[Int, String])` prints `a=ok 1`, and `f(-1)` in the same position prints the Err. The auto-`?` desugar exempted only ARGUMENT 0 of a callee whose FIRST param is Result/Option (#558), so a Result param at index ≥ 1 had its effect-call argument unwrapped to the payload — native emitted `show(tag, f(1)?)` (rustc E0308, a build failure), the incumbent wasm leg failed validation (`expected i32, found i64`) and the structural leg walled `ty-mismatch` — an accepted program no leg could build (#1970). The per-parameter flag that replaced it still read only DECLARED Result/Option parameters, so inside an effect fn a type-variable parameter instantiated at Result had its argument unwrapped the same way (`id(int.parse(\"7\")?)`: rustc E0308, an E082 ty-mismatch wall on wasm) though the checker accepted the program (#3646). No call argument takes the auto-`?` now: the checker constrains every argument against its parameter (a Result where `Int` is expected is E005; propagation is the explicit `!`), so an argument still Result-typed is one its parameter accepts." since = "0.63.0" status = "active" evidence = [ { path = "spec/wasm_cross/result_param_not_first.almd", class = "fixture" }, + { path = "spec/wasm_cross/result_generic_param_arg.almd", class = "fixture" }, ] [[contract]] id = "C-346" diff --git a/spec/wasm_cross/result_generic_param_arg.almd b/spec/wasm_cross/result_generic_param_arg.almd new file mode 100644 index 00000000..c157e3b4 --- /dev/null +++ b/spec/wasm_cross/result_generic_param_arg.almd @@ -0,0 +1,39 @@ +// @contract: C-345 +// A Result-returning call passed where a TYPE-VARIABLE parameter is +// instantiated at Result keeps its Result, as a declared Result parameter's +// argument does (result_param_not_first). The auto-`?` desugar kept an +// argument's Result only where the callee DECLARED the parameter Result / +// Option, so in an effect fn `id(int.parse("7"))`, a fold seeded with a +// Result call, or `map.get_or(m, k, int.parse(s))` lowered with a `?` on +// the argument — rustc E0308 natively, an E082 ty-mismatch wall on wasm — +// though `almide check` accepted the program. Found by the counted stdlib +// inspection (#3646). +fn id[T](x: T) -> T = x + +fn mk(n: Int) -> Result[Int, String] = if n > 0 then ok(n) else err("neg ${n}") + +effect fn step(n: Int) -> Int = if n < 0 then err("neg ${n}")! +else n + +fn show(tag: String, r: Result[Int, String]) -> String = match r { + ok(v) => "${tag}=ok ${v}", + err(e) => "${tag}=err ${e}", +} + +effect fn main() -> Unit = { + let a: Result[Int, String] = id(int.parse("7")) + println(show("id", a)) + let b: Result[Int, String] = id(mk(-1)) + println(show("id-err", b)) + let c: Result[Int, String] = list.fold([1, 2], mk(5), (acc, x) => acc) + println(show("fold", c)) + let m: Map[String, Result[Int, String]] = map.new() + let d: Result[Int, String] = map.get_or(m, "k", int.parse("x")) + println(show("map.get_or", d)) + let e: Result[Int, String] = list.get_or([mk(1)], 3, mk(9)) + println(show("get_or", e)) + let f: Result[Int, String] = id(step(-2)) + println(show("id-effect", f)) + let g: Result[Int, String] = list.fold([1], step(4), (acc, x) => acc) + println(show("fold-effect", g)) +}