From 36a069f2369233582bd71603d70760006c4b09ab Mon Sep 17 00:00:00 2001 From: O6lvl4 Date: Wed, 30 Sep 2026 20:45:58 +0900 Subject: [PATCH 1/3] Evaluate every fan.map element in the reference evaluator and surface the lowest-index Err Co-Authored-By: Claude Opus 5.5 (1M context) --- ref/src/stdlib_ext2.rs | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/ref/src/stdlib_ext2.rs b/ref/src/stdlib_ext2.rs index b9b59ec3..a1da8e4f 100644 --- a/ref/src/stdlib_ext2.rs +++ b/ref/src/stdlib_ext2.rs @@ -1086,11 +1086,18 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec) -> Result return mismatch(name, "a function", other), }; let mut vals: Vec = Vec::new(); + // C-005 / ADR-0024 D1: fan.map evaluates EVERY element, and the + // lowest-index Err is the one that surfaces + let mut first_err: Option> = None; for x in xs.iter() { let r = it.call_value(&c, vec![x.clone()])?; match (name, r) { ("fan.map", Value::Ok(v)) => vals.push((*v).clone()), - ("fan.map", Value::Err(e)) => return Ok(Ok(Value::Err(e))), // first err, index order + ("fan.map", Value::Err(e)) => { + if first_err.is_none() { + first_err = Some(e); + } + } ("fan.map", v) => vals.push(v), ("fan.any", Value::Ok(v)) => return Ok(Ok(Value::Ok(v))), // first success wins ("fan.any", Value::Err(_)) => {} @@ -1101,9 +1108,10 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec) -> Result unreachable!(), } } - Ok(match name { - "fan.map" => ok(Value::List(Rc::new(vals))), - "fan.any" => err_str("fan.any: all candidates failed"), + Ok(match (name, first_err) { + ("fan.map", Some(e)) => Value::Err(e), + ("fan.map", None) => ok(Value::List(Rc::new(vals))), + ("fan.any", _) => err_str("fan.any: all candidates failed"), _ => Value::List(Rc::new(vals)), }) } From fc71f5e8053cf6b24a571756dc7921026bbe28d6 Mon Sep 17 00:00:00 2001 From: O6lvl4 Date: Wed, 30 Sep 2026 20:45:58 +0900 Subject: [PATCH 2/3] Restate C-004, C-005 and C-200 as ADR-0024's sequential run-every-element observation and pin them with two fixtures Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/contracts/README.md | 4 +-- docs/contracts/conformance.md | 4 +-- docs/contracts/contracts.toml | 8 +++-- docs/specs/als/runtime.md | 12 ++++++- proofs/als-validation.toml | 6 ++-- .../fan_map_err_runs_every_element.almd | 16 +++++++++ .../fan_trap_waits_for_elements_below.almd | 35 +++++++++++++++++++ 7 files changed, 74 insertions(+), 11 deletions(-) create mode 100644 spec/wasm_cross/fan_map_err_runs_every_element.almd create mode 100644 spec/wasm_cross/fan_trap_waits_for_elements_below.almd diff --git a/docs/contracts/README.md b/docs/contracts/README.md index 6bc85e8b..8b502569 100644 --- a/docs/contracts/README.md +++ b/docs/contracts/README.md @@ -39,7 +39,7 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1 | C-002 | Signed MIN / -1 overflow aborts, at the TRUE per-width MIN | 0.24.0 | active | fixture | 3 | | C-003 | Non-aborting integer div/mod stay byte-identical | 0.24.0 | active | fixture | 1 | | C-004 | fan.any / fan.map / fan.settle are deterministic by list order | 0.24.0 | active | fixture | 6 | -| C-005 | fan error propagation surfaces as the unified main-error abort | 0.24.0 | active | fixture | 4 | +| C-005 | fan error propagation surfaces as the unified main-error abort | 0.24.0 | active | fixture | 5 | | C-006 | [fan.timeout does not exist — wall-clock deadlines live at the host boundary](C-006-fan-timeout-removed.md) | 0.29.0 | active | fixture | 0 | | C-007 | Abortable top-level lets evaluate eagerly at startup | 0.24.0 | active | fixture | 2 | | C-008 | [Compound interpolation renders the Almide-literal repr (containers)](C-008-009-010-repr.md) | 0.24.0 | active | fixture | 3 | @@ -234,7 +234,7 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1 | C-197 | Linear-memory exhaustion is a resource limit with a defined abort | 0.41.0 | active | fixture | 5 | | C-198 | A head count below 1 is a defined abort, identically on both targets | 0.42.0 | active | fixture | 1 | | C-199 | A fan block joins every sibling and reports the first Err in list order | 0.42.0 | active | fixture | 1 | -| C-200 | A trap in a fan sibling exits through the unified main-error abort, convergently | 0.42.0 | active | fixture | 1 | +| C-200 | A trap in a fan sibling exits through the unified main-error abort, convergently | 0.42.0 | active | fixture | 2 | | C-201 | An Option combinator's tuple result is materializable as an owned element for every element-type combination | 0.44.0 | active | fixture | 1 | | C-202 | Time constructors guard their domain: negative aborts, overflow saturates | 0.47.0 | active | fixture | 3 | | C-203 | The time-type operator algebra is unit-exact and saturating on both targets | 0.47.0 | active | fixture | 1 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index 030ecfda..11071bb9 100644 --- a/docs/contracts/conformance.md +++ b/docs/contracts/conformance.md @@ -101,7 +101,7 @@ | 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) | | ALS-R2 | C-008, C-009, C-010, C-011, C-222 | `spec/wasm_cross/compound_repr_interp.almd` (byte-compare)
`spec/wasm_cross/repr_parity_pin.almd` (byte-compare)
`spec/wasm_cross/fuzz_found_nested_interp_capture.almd` (byte-compare)
`spec/wasm_cross/compound_repr_records_interp.almd` (byte-compare)
`spec/wasm_cross/compound_repr_recursive_interp.almd` (byte-compare)
`spec/integration/modules/cross_module_repr_test.almd` (both-target test)
`spec/integration/modules/cross_module_repr_derive_test.almd` (both-target test)
`tests/module_type_repr_test.rs` (cargo gate)
`spec/wasm_cross/recursive_generic_repr_interp.almd` (byte-compare)
`spec/wasm_cross/float_concrete.almd` (byte-compare)
`spec/wasm_cross/num_edge_to_string.almd` (byte-compare)
`spec/wasm_cross/int_float_ops.almd` (byte-compare)
`spec/wasm_cross/float_interp_forms.almd` (byte-compare)
`spec/wasm_cross/nested_unwrap_propagation.almd` (byte-compare) | -| ALS-R3 | C-004, C-005, C-006, C-199, C-321, C-349 | `spec/wasm_cross/fan_deterministic.almd` (byte-compare)
`spec/wasm_cross/fan_map_inline_lambda.almd` (byte-compare)
`spec/wasm_cross/fan_pure_thunks.almd` (byte-compare)
`spec/wasm_cross/fan_var_thunk_list.almd` (byte-compare)
`spec/wasm_cross/fan_effect_mapper.almd` (byte-compare)
`spec/wasm_cross/fan_effect_mapper_capability.almd` (byte-compare)
`spec/embedded_cross/fan_mapper_effect_callback_forms.almd` (both-target test)
`spec/wasm_cross/fan_map_err.almd` (byte-compare)
`spec/wasm_cross/fan_map_inline_err.almd` (byte-compare)
`spec/wasm_cross/fan_any_allfail.almd` (byte-compare)
`spec/wasm_cross/option_none_unwrap_term.almd` (byte-compare)
`tests/diagnostics/e027-fan-timeout-removed/broken.almd` (checker)
`tests/diagnostic_harness_test.rs` (cargo gate)
`spec/wasm_cross/fan_block_err_list_order.almd` (byte-compare)
`spec/wasm_cross/fan_prefetch_fs.almd` (byte-compare)
`tests/component_p3_test.rs` (cargo gate)
`spec/wasm_cross/fan_arm_unwrap_or.almd` (byte-compare) | +| ALS-R3 | C-004, C-005, C-006, C-199, C-321, C-349 | `spec/wasm_cross/fan_deterministic.almd` (byte-compare)
`spec/wasm_cross/fan_map_inline_lambda.almd` (byte-compare)
`spec/wasm_cross/fan_pure_thunks.almd` (byte-compare)
`spec/wasm_cross/fan_var_thunk_list.almd` (byte-compare)
`spec/wasm_cross/fan_effect_mapper.almd` (byte-compare)
`spec/wasm_cross/fan_effect_mapper_capability.almd` (byte-compare)
`spec/embedded_cross/fan_mapper_effect_callback_forms.almd` (both-target test)
`spec/wasm_cross/fan_map_err.almd` (byte-compare)
`spec/wasm_cross/fan_map_inline_err.almd` (byte-compare)
`spec/wasm_cross/fan_map_err_runs_every_element.almd` (byte-compare)
`spec/wasm_cross/fan_any_allfail.almd` (byte-compare)
`spec/wasm_cross/option_none_unwrap_term.almd` (byte-compare)
`tests/diagnostics/e027-fan-timeout-removed/broken.almd` (checker)
`tests/diagnostic_harness_test.rs` (cargo gate)
`spec/wasm_cross/fan_block_err_list_order.almd` (byte-compare)
`spec/wasm_cross/fan_prefetch_fs.almd` (byte-compare)
`tests/component_p3_test.rs` (cargo gate)
`spec/wasm_cross/fan_arm_unwrap_or.almd` (byte-compare) | | ALS-R4 | C-012 | `spec/wasm_cross/const_fold_nonfinite_float.almd` (byte-compare) | | ALS-R5 | C-096, C-112, C-118, C-133, C-189, C-214, C-215, C-290, C-327, C-330, C-328, C-329, C-331, C-366, C-367, C-370 | `spec/wasm_cross/process_args.almd` (byte-compare)
`spec/wasm_cross/random_int_entropy.almd` (byte-compare)
`spec/wasm_cross/env_args.almd` (byte-compare)
`spec/wasm_cross/env_get.almd` (byte-compare)
`spec/wasm_cross/env_platform_reporting.almd` (byte-compare)
`spec/stdlib/process_timeout_test.almd` (both-target test)
`spec/stdlib/fs_if_exists_test.almd` (both-target test)
`spec/wasm_cross/fs_read_directory_errno.almd` (byte-compare)
`spec/wasm_cross/fs_read_text_utf8.almd` (byte-compare)
`spec/wasm_cross/env_sleep_pause.almd` (byte-compare)
`spec/wasm_cross/availability_pure_batch.almd` (byte-compare)
`tests/component_p3_test.rs` (cargo gate)
`spec/embedded_cross/http_client_errs.almd` (both-target test)
`spec/embedded_cross/http_framed_errs.almd` (both-target test)
`spec/embedded_cross/http_error_classes.almd` (both-target test)
`spec/wasm_cross/env_set_overlay.almd` (byte-compare)
`spec/wasm_cross/zlib_selfhost.almd` (byte-compare)
`spec/stdlib/http_call_test.almd` (both-target test)
`spec/embedded_cross/http_call_handle_errs.almd` (both-target test)
`spec/serve_cross/http_serve_replay.almd` (both-target test)
`spec/serve_cross/http_serve_shutdown.almd` (both-target test)
`spec/embedded_cross/http_header_refusal.almd` (both-target test) | | ALS-R6 | C-042, C-137, C-220, C-225, C-227, C-228, C-229, C-230, C-270, C-272, C-273, C-278, C-282, C-283, C-284 | `spec/wasm_cross/fs_preopen_resolve.almd` (byte-compare)
`spec/wasm_cross/fs_relative_path.almd` (byte-compare)
`spec/stdlib/fs_stat_test.almd` (both-target test)
`spec/stdlib/fs_streaming_test.almd` (both-target test)
`spec/stdlib/fs_fold_lines_range_test.almd` (both-target test)
`spec/stdlib/fs_fold_lines_chunked_test.almd` (both-target test)
`spec/wasm_cross/line_endings_bare_cr.almd` (byte-compare)
`spec/wasm_cross/fs_read_lines.almd` (byte-compare)
`spec/wasm_cross/fs_metadata_family.almd` (byte-compare)
`spec/wasm_cross/fs_composition_family.almd` (byte-compare)
`spec/wasm_cross/matrix_select_rows.almd` (byte-compare)
`spec/wasm_cross/fs_glob_segments.almd` (byte-compare)
`spec/wasm_cross/matrix_select_rows_oob.almd` (byte-compare)
`spec/wasm_cross/matrix_q_dims_guard.almd` (byte-compare)
`spec/wasm_cross/matrix_select_rows_q1_partial_block.almd` (byte-compare)
`spec/wasm_cross/bytes_negative_offset_family.almd` (byte-compare)
`spec/wasm_cross/matrix_domain_edges.almd` (byte-compare)
`spec/wasm_cross/matrix_q1_full_loader_cols_beyond_buffer.almd` (byte-compare)
`spec/wasm_cross/flight_pid_control.almd` (byte-compare)
`spec/wasm_cross/matrix_q_fp16_scale_domain.almd` (byte-compare)
`spec/wasm_cross/fs_list_dir_multipass.almd` (byte-compare)
`spec/wasm_cross/fs_write_errno.almd` (byte-compare)
`spec/wasm_fail/rope_geometry_exceeds_aborts.almd` (both-target test)
`spec/wasm_cross/rope_geometry_family.almd` (byte-compare)
`spec/wasm_cross/rope_at_family.almd` (byte-compare)
`spec/wasm_fail/matrix_index_oob_aborts.almd` (both-target test)
`spec/wasm_cross/matrix_index_domain_family.almd` (byte-compare)
`spec/wasm_cross/callee_shadowing_family.almd` (byte-compare)
`spec/wasm_cross/fallible_hof_effect_callback_family.almd` (byte-compare) | @@ -125,7 +125,7 @@ | ALS-T3 | C-087, C-298, C-299 | `spec/wasm_cross/json_number_unicode.almd` (byte-compare)
`spec/wasm_cross/json_string_span.almd` (byte-compare)
`spec/wasm_cross/json_parse_lenient_edges.almd` (byte-compare)
`spec/wasm_cross/json_many_keys.almd` (byte-compare)
`spec/wasm_cross/codec_decode_error_surface.almd` (byte-compare)
`spec/wasm_cross/codec_deep_nesting.almd` (byte-compare)
`spec/wasm_cross/codec_doc_array.almd` (byte-compare)
`spec/wasm_cross/codec_empty_and_bool.almd` (byte-compare)
`spec/wasm_cross/codec_extra_keys.almd` (byte-compare)
`spec/wasm_cross/codec_int_float_boundaries.almd` (byte-compare)
`spec/wasm_cross/codec_list_list_field.almd` (byte-compare)
`spec/wasm_cross/codec_list_default_field.almd` (byte-compare)
`spec/wasm_cross/codec_nested_records.almd` (byte-compare)
`spec/wasm_cross/codec_option_numeric.almd` (byte-compare)
`spec/wasm_cross/codec_string_escapes.almd` (byte-compare)
`spec/wasm_cross/codec_variant_roundtrip.almd` (byte-compare)
`spec/wasm_cross/codec_whitespace_tolerance.almd` (byte-compare)
`spec/wasm_cross/codec_list_default.almd` (byte-compare)
`spec/wasm_cross/codec_triple_list.almd` (byte-compare)
`spec/wasm_cross/hash_digests.almd` (byte-compare)
`spec/stdlib/hash_test.almd` (both-target test) | | ALS-T4 | C-129, C-171 | `spec/wasm_cross/list_chunk_windows.almd` (byte-compare)
`spec/wasm_cross/list_chunk_zero.almd` (byte-compare)
`spec/wasm_cross/list_windows_zero.almd` (byte-compare)
`spec/wasm_cross/list_window_zero.almd` (byte-compare)
`spec/wasm_cross/bytes_f16_offset_overflow.almd` (byte-compare) | | ALS-T5 | C-020, C-162 | `spec/wasm_cross/string_case_unicode.almd` (byte-compare)
`spec/wasm_cross/io_write_ordering.almd` (byte-compare) | -| ALS-T6 | C-001, C-002, C-047, C-067, C-154, C-155, C-161, C-169, C-184, C-196, C-197, C-198, C-200, C-219, C-353 | `spec/wasm_cross/int_div_by_zero.almd` (byte-compare)
`spec/wasm_cross/int_mod_by_zero.almd` (byte-compare)
`spec/wasm_cross/int_div_by_zero_literal.almd` (byte-compare)
`spec/wasm_cross/int_div_overflow.almd` (byte-compare)
`spec/wasm_cross/int_mod_overflow.almd` (byte-compare)
`spec/wasm_cross/int8_div_overflow.almd` (byte-compare)
`spec/wasm_cross/int_pow_negative_exponent.almd` (byte-compare)
`spec/wasm_cross/int_pow_overflow_wraps.almd` (byte-compare)
`spec/wasm_cross/int_rotate_nonpositive_width.almd` (byte-compare)
`spec/wasm_cross/index_bounds.almd` (byte-compare)
`spec/wasm_cross/index_bounds_write_heap.almd` (byte-compare)
`spec/wasm_cross/index_bounds_i64.almd` (byte-compare)
`spec/wasm_cross/index_bounds_write_only_var.almd` (byte-compare)
`spec/wasm_cross/int_clamp_inverted.almd` (byte-compare)
`spec/wasm_cross/float_clamp_invalid.almd` (byte-compare)
`spec/wasm_cross/to_fixed_domain_abort.almd` (byte-compare)
`spec/wasm_cross/to_fixed_domain_abort_hi.almd` (byte-compare)
`spec/wasm_cross/to_fixed_wide_precision.almd` (byte-compare)
`spec/wasm_cross/matrix_dims_guard.almd` (byte-compare)
`spec/wasm_cross/matrix_dims_guard_overflow.almd` (byte-compare)
`spec/wasm_cross/matrix_zero_cols_rows.almd` (byte-compare)
`spec/wasm_cross/matrix_dims_guard_rows.almd` (byte-compare)
`spec/wasm_cross/matrix_q_dims_guard.almd` (byte-compare)
`spec/wasm_cross/count_domain_nonbytes.almd` (byte-compare)
`spec/wasm_cross/matrix_dims_guard_product.almd` (byte-compare)
`spec/wasm_cross/matrix_from_bytes_count_domain.almd` (byte-compare)
`spec/wasm_cross/string_repeat_empty.almd` (byte-compare)
`spec/wasm_cross/list_repeat_size_ceiling.almd` (byte-compare)
`spec/wasm_cross/int_pow_operator_negative_base.almd` (byte-compare)
`spec/wasm_cross/recursion_depth_within_limits.almd` (byte-compare)
`spec/wasm_cross/allocation_within_limits.almd` (byte-compare)
`spec/wasm_cross/bytes_new_exhaustion.almd` (byte-compare)
`spec/wasm_cross/bytes_alloc_ceiling_domain.almd` (byte-compare)
`spec/wasm_cross/bytes_pad_ceiling_oom.almd` (byte-compare)
`spec/wasm_cross/prim_alloc_count_domain.almd` (byte-compare)
`tests/alloc_bump_wrap_test.rs` (cargo gate)
`spec/wasm_cross/matrix_head_count_domain.almd` (byte-compare)
`spec/wasm_cross/fan_sibling_trap.almd` (byte-compare)
`tests/incumbent_exit_tail_test.rs` (cargo gate)
`spec/wasm_cross/guard_else_exit_code.almd` (byte-compare)
`spec/wasm_cross/matrix_shape_precondition_family.almd` (byte-compare)
`spec/wasm_cross/matrix_shape_precondition_activations.almd` (byte-compare)
`spec/wasm_fail/matrix_shape_mismatch_aborts.almd` (both-target test)
`spec/wasm_fail/matrix_ragged_from_lists_aborts.almd` (both-target test)
`spec/wasm_fail/matrix_linear_row_bias_aborts.almd` (both-target test)
`spec/wasm_fail/matrix_concat_cols_rows_aborts.almd` (both-target test) | +| ALS-T6 | C-001, C-002, C-047, C-067, C-154, C-155, C-161, C-169, C-184, C-196, C-197, C-198, C-200, C-219, C-353 | `spec/wasm_cross/int_div_by_zero.almd` (byte-compare)
`spec/wasm_cross/int_mod_by_zero.almd` (byte-compare)
`spec/wasm_cross/int_div_by_zero_literal.almd` (byte-compare)
`spec/wasm_cross/int_div_overflow.almd` (byte-compare)
`spec/wasm_cross/int_mod_overflow.almd` (byte-compare)
`spec/wasm_cross/int8_div_overflow.almd` (byte-compare)
`spec/wasm_cross/int_pow_negative_exponent.almd` (byte-compare)
`spec/wasm_cross/int_pow_overflow_wraps.almd` (byte-compare)
`spec/wasm_cross/int_rotate_nonpositive_width.almd` (byte-compare)
`spec/wasm_cross/index_bounds.almd` (byte-compare)
`spec/wasm_cross/index_bounds_write_heap.almd` (byte-compare)
`spec/wasm_cross/index_bounds_i64.almd` (byte-compare)
`spec/wasm_cross/index_bounds_write_only_var.almd` (byte-compare)
`spec/wasm_cross/int_clamp_inverted.almd` (byte-compare)
`spec/wasm_cross/float_clamp_invalid.almd` (byte-compare)
`spec/wasm_cross/to_fixed_domain_abort.almd` (byte-compare)
`spec/wasm_cross/to_fixed_domain_abort_hi.almd` (byte-compare)
`spec/wasm_cross/to_fixed_wide_precision.almd` (byte-compare)
`spec/wasm_cross/matrix_dims_guard.almd` (byte-compare)
`spec/wasm_cross/matrix_dims_guard_overflow.almd` (byte-compare)
`spec/wasm_cross/matrix_zero_cols_rows.almd` (byte-compare)
`spec/wasm_cross/matrix_dims_guard_rows.almd` (byte-compare)
`spec/wasm_cross/matrix_q_dims_guard.almd` (byte-compare)
`spec/wasm_cross/count_domain_nonbytes.almd` (byte-compare)
`spec/wasm_cross/matrix_dims_guard_product.almd` (byte-compare)
`spec/wasm_cross/matrix_from_bytes_count_domain.almd` (byte-compare)
`spec/wasm_cross/string_repeat_empty.almd` (byte-compare)
`spec/wasm_cross/list_repeat_size_ceiling.almd` (byte-compare)
`spec/wasm_cross/int_pow_operator_negative_base.almd` (byte-compare)
`spec/wasm_cross/recursion_depth_within_limits.almd` (byte-compare)
`spec/wasm_cross/allocation_within_limits.almd` (byte-compare)
`spec/wasm_cross/bytes_new_exhaustion.almd` (byte-compare)
`spec/wasm_cross/bytes_alloc_ceiling_domain.almd` (byte-compare)
`spec/wasm_cross/bytes_pad_ceiling_oom.almd` (byte-compare)
`spec/wasm_cross/prim_alloc_count_domain.almd` (byte-compare)
`tests/alloc_bump_wrap_test.rs` (cargo gate)
`spec/wasm_cross/matrix_head_count_domain.almd` (byte-compare)
`spec/wasm_cross/fan_sibling_trap.almd` (byte-compare)
`spec/wasm_cross/fan_trap_waits_for_elements_below.almd` (byte-compare)
`tests/incumbent_exit_tail_test.rs` (cargo gate)
`spec/wasm_cross/guard_else_exit_code.almd` (byte-compare)
`spec/wasm_cross/matrix_shape_precondition_family.almd` (byte-compare)
`spec/wasm_cross/matrix_shape_precondition_activations.almd` (byte-compare)
`spec/wasm_fail/matrix_shape_mismatch_aborts.almd` (both-target test)
`spec/wasm_fail/matrix_ragged_from_lists_aborts.almd` (both-target test)
`spec/wasm_fail/matrix_linear_row_bias_aborts.almd` (both-target test)
`spec/wasm_fail/matrix_concat_cols_rows_aborts.almd` (both-target test) | | ALS-T7 | C-007, C-077, C-111 | `spec/wasm_cross/top_let_div_eager.almd` (byte-compare)
`spec/wasm_cross/top_let_div_used.almd` (byte-compare)
`spec/wasm_cross/r5_mod_global_init_order.almd` (byte-compare)
`spec/wasm_cross/module_global_const.almd` (byte-compare) | | ALS-T8 | C-028, C-029 | `spec/wasm_cross/int_from_hex.almd` (byte-compare)
`spec/wasm_cross/int_parse_overflow.almd` (byte-compare) | | ALS-T9 | C-025 | `spec/wasm_cross/float_to_fixed.almd` (byte-compare) | diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index 657a8348..99032b35 100644 --- a/docs/contracts/contracts.toml +++ b/docs/contracts/contracts.toml @@ -108,7 +108,7 @@ evidence = [ id = "C-004" spec = "ALS-R3" title = "fan.any / fan.map / fan.settle are deterministic by list order" -statement = "`fan.any` tries thunks in list order and returns the first Ok. `fan.map` runs element fns sequentially in list order; `fan.settle` returns results in list order. All are byte-identical native == wasm. (any skips failures to find an Ok.) `fan.race` was REMOVED in 0.42.0: under the deterministic model it was exactly `thunks[0]()` — `desugar_fan.rs` replaced the call with thunk[0]'s body and never evaluated the rest — so its name promised a wall-clock race the language does not have. It is an E027 check-time tombstone, the same treatment `fan.timeout` got in 0.29.0. EXCEPTION: side-effect INTERLEAVING inside `fan { }` block arms and `fan.settle` thunks is wall-clock on native (both run on real threads) and sequential on wasm — they pin their RESULT (tuple / list) order only. The block was an undercount here until #915's audit: it spawns per-arm scoped threads on native, the same interleaving class as settle. The three MAPPER heads (`fan.map/any/settle(xs, f)`) accept an EFFECT callback in both spellings — an inline lambda calling an effect fn, and a bare effect-fn value — and the result is byte-identical on both legs (#1350; the slot's `is_effect: false` was a declaration bug, never a permission, since unification is effect-agnostic by #1055). A callback reaching a stdlib capability with no wasm implementation (`http.get`) walls on the wasm leg, but that is the capability's own gap — it walls identically with no `fan` in the program — not a mapper-purity rule. The converse holds too (#1406): a CAPABILITY-BEARING callback whose capability HAS a wasm implementation (fs) runs byte-identically on both legs, in both spellings — an inline lambda reaching fs directly, and a lambda calling an effect HELPER that wraps fs (the passthrough shape `effect fn helper(p) = fs.read_text(p)`, which seeds no ResultErr and carries no `!`/`?` of its own) — consumed via `??` and via `!` alike. Two compiler facts carry this cell: the can-err ABI seeds a fn whose TAIL position returns a foreign Result (`returns_foreign_result`, so the passthrough keeps the uniform Result-carrier funcref ABI), and the mapper's result-family tracking is TYPE-split at the classify sites (`is_fan_any_map` + `is_heap_ok_result` — the pre-routing name `fan.any_map` covers all nine 3×3 pairings, so the String-output pairings' heap-Ok cap-as-tag family cannot be told apart by name). EXTENDED (#1406, 0.61.2): on the STRUCTURAL leg (the 0.60 default, which `almide run --target wasm` takes for fs programs) every spelling the ruling admits agrees with native on all three mapper heads — the canonical `!` tail (`(p) => fs.read_text(p)!`, `(p) => helper(p)!`), a COMPOUND body with a statement before the `!`, and a bare effect-fn VALUE — consumed via `!`, `??`, and a match over settle's list. Two shapes diverged before: `fan.settle`'s canonical `!` (the frontend strips the marker only for `list.*` callees, and settle desugars to `list.map` AFTER that pass, so the emitter saw `ok(unwrap(f(p)))`) and a compound body on ANY head — the structural leg inlined the callback into the ENCLOSING frame, so its `!` propagated out of `main` (`Error: No such file or directory (os error 2)` at the time; since #2090 the same line reads `Error: fs.read_text(\"p\"): No such file or directory (os error 2)` — the call and its operand prefixed, the errno tail verbatim — on every leg, exit 1) where native captured the err into the element's Result. A callback body that still propagates after the canonical-wrapper strip is now lowered once as a closure value and called per element through the funcref table (the #1806 route the fs walkers take), so its `!` rides the closure's own Result channel; the fn-value `list.map` route gained the closure convention's RC-3 +1 on the borrowed element it hands the callee. The fixture lives in spec/embedded_cross (an fs program routes to the incumbent on the BUILD path), the fs-backed effect column is one row per head in spec/lang/fan_mapper_matrix_test.almd (fan.race is the reasoned omission: its mapper meters a PURE body, E006), and the http-bodied twin stays refused on stock artifacts by the CAPABILITY — proofs/wall-corpus/fan_mapper_http_callback.almd pins the E081 text naming `http.get`, never the mapper — while the embedded lane serves it identically to native (C-328)." +statement = "`fan.any` tries thunks in list order and returns the first Ok. `fan.map` and `fan.settle` behave as a sequential evaluation of EVERY element in list order, whatever the substrate (ADR-0024 D1): the observation (stdout, stderr, exit code, returned value) is that of evaluating element 0, then element 1, and so on to the last, and no choice of substrate (sequential, threads, async subtasks) may change it; `fan.map` returns the results in list order, `fan.settle` every element's Result in list order. All are byte-identical native == wasm. (any skips failures to find an Ok.) `fan.race` was REMOVED in 0.42.0: under the deterministic model it was exactly `thunks[0]()` — `desugar_fan.rs` replaced the call with thunk[0]'s body and never evaluated the rest — so its name promised a wall-clock race the language does not have. It is an E027 check-time tombstone, the same treatment `fan.timeout` got in 0.29.0. EXCEPTION: side-effect INTERLEAVING inside `fan { }` block arms and `fan.settle` thunks is wall-clock on native (both run on real threads) and sequential on wasm — they pin their RESULT (tuple / list) order only. The block was an undercount here until #915's audit: it spawns per-arm scoped threads on native, the same interleaving class as settle. The three MAPPER heads (`fan.map/any/settle(xs, f)`) accept an EFFECT callback in both spellings — an inline lambda calling an effect fn, and a bare effect-fn value — and the result is byte-identical on both legs (#1350; the slot's `is_effect: false` was a declaration bug, never a permission, since unification is effect-agnostic by #1055). A callback reaching a stdlib capability with no wasm implementation (`http.get`) walls on the wasm leg, but that is the capability's own gap — it walls identically with no `fan` in the program — not a mapper-purity rule. The converse holds too (#1406): a CAPABILITY-BEARING callback whose capability HAS a wasm implementation (fs) runs byte-identically on both legs, in both spellings — an inline lambda reaching fs directly, and a lambda calling an effect HELPER that wraps fs (the passthrough shape `effect fn helper(p) = fs.read_text(p)`, which seeds no ResultErr and carries no `!`/`?` of its own) — consumed via `??` and via `!` alike. Two compiler facts carry this cell: the can-err ABI seeds a fn whose TAIL position returns a foreign Result (`returns_foreign_result`, so the passthrough keeps the uniform Result-carrier funcref ABI), and the mapper's result-family tracking is TYPE-split at the classify sites (`is_fan_any_map` + `is_heap_ok_result` — the pre-routing name `fan.any_map` covers all nine 3×3 pairings, so the String-output pairings' heap-Ok cap-as-tag family cannot be told apart by name). EXTENDED (#1406, 0.61.2): on the STRUCTURAL leg (the 0.60 default, which `almide run --target wasm` takes for fs programs) every spelling the ruling admits agrees with native on all three mapper heads — the canonical `!` tail (`(p) => fs.read_text(p)!`, `(p) => helper(p)!`), a COMPOUND body with a statement before the `!`, and a bare effect-fn VALUE — consumed via `!`, `??`, and a match over settle's list. Two shapes diverged before: `fan.settle`'s canonical `!` (the frontend strips the marker only for `list.*` callees, and settle desugars to `list.map` AFTER that pass, so the emitter saw `ok(unwrap(f(p)))`) and a compound body on ANY head — the structural leg inlined the callback into the ENCLOSING frame, so its `!` propagated out of `main` (`Error: No such file or directory (os error 2)` at the time; since #2090 the same line reads `Error: fs.read_text(\"p\"): No such file or directory (os error 2)` — the call and its operand prefixed, the errno tail verbatim — on every leg, exit 1) where native captured the err into the element's Result. A callback body that still propagates after the canonical-wrapper strip is now lowered once as a closure value and called per element through the funcref table (the #1806 route the fs walkers take), so its `!` rides the closure's own Result channel; the fn-value `list.map` route gained the closure convention's RC-3 +1 on the borrowed element it hands the callee. The fixture lives in spec/embedded_cross (an fs program routes to the incumbent on the BUILD path), the fs-backed effect column is one row per head in spec/lang/fan_mapper_matrix_test.almd (fan.race is the reasoned omission: its mapper meters a PURE body, E006), and the http-bodied twin stays refused on stock artifacts by the CAPABILITY — proofs/wall-corpus/fan_mapper_http_callback.almd pins the E081 text naming `http.get`, never the mapper — while the embedded lane serves it identically to native (C-328)." since = "0.24.0" status = "active" evidence = [ @@ -124,12 +124,13 @@ evidence = [ id = "C-005" spec = "ALS-R3" title = "fan error propagation surfaces as the unified main-error abort" -statement = "The first element fn returning Err in `fan.map` (named or inline lambda) and the all-fail case of `fan.any` (defined `Err(\"fan.any: all candidates failed\")`) all propagate as `Error: ` + exit 1 on BOTH targets via the effect-main termination — NOT a native panic (101) nor a wasm trap (134)." +statement = "`fan.map` (named or inline lambda) evaluates EVERY element in list order, including the elements after one that returns Err (ADR-0024 D1): their output appears in list order before the abort, and when several elements return Err the LOWEST-INDEX Err is the one that surfaces, the same rule `fan { }` block arms follow (C-199). That Err and the all-fail case of `fan.any` (defined `Err(\"fan.any: all candidates failed\")`) propagate as `Error: ` + exit 1 on BOTH targets via the effect-main termination — NOT a native panic (101) nor a wasm trap (134). To stop at the first failure, the writer spells a `for` loop with `!`." since = "0.24.0" status = "active" evidence = [ { path = "spec/wasm_cross/fan_map_err.almd", class = "fixture" }, { path = "spec/wasm_cross/fan_map_inline_err.almd", class = "fixture" }, + { path = "spec/wasm_cross/fan_map_err_runs_every_element.almd", class = "fixture" }, { path = "spec/wasm_cross/fan_any_allfail.almd", class = "fixture" }, { path = "spec/wasm_cross/option_none_unwrap_term.almd", class = "fixture" }, ] @@ -2450,11 +2451,12 @@ evidence = [ id = "C-200" spec = "ALS-T6" title = "A trap in a fan sibling exits through the unified main-error abort, convergently" -statement = "A runtime trap inside a `fan` sibling (division by zero, integer overflow, index out of bounds) terminates the program through the SAME unified `Error: ` + exit 1 the effect-main path uses — never a native panic (101) nor a wasm trap (134) — and the two targets agree, including on what reached stdout first. In-flight siblings are NOT waited for: measured with a 1.5s-sleeping second sibling, both targets abort in ~0s with an empty stdout. This closes #1026's third complaint (the block's documented outcomes — a tuple, or the first Err in list order per C-199 — were not the only exits, and the trap exit was uncontracted). It does NOT require the per-arm output buffering the Unit's design note proposed: that was written on the assumption that the trap case diverged, and the measurement says it converges. Buffering remains the answer to a DIFFERENT question — C-004's EXCEPTION clause, where two siblings both PRINT and native interleaves by wall clock while wasm is sequential." +statement = "A runtime trap inside a `fan` element (division by zero, integer overflow, index out of bounds, `panic`, a failed `assert`) terminates the program through the SAME unified `Error: ` + exit 1 the effect-main path uses — never a native panic (101) nor a wasm trap (134) — and the observation is that of the sequential evaluation (ADR-0024 D6): a trap in element k means elements 0..k-1 ran to completion and their output appears in list order, then element k's output up to the trap, and nothing of any element after k. A concurrent substrate meets this by no longer starting elements, WAITING for every element below k, letting the lowest-index trap win, and flushing the timelines below it in order, then the trapping element's partial timeline, before the abort; an element above k is not waited for and its output is discarded. RESIDUAL (stated, not hidden): an element above the winning trap that a concurrent substrate had already started may have sent requests to the outside world that the sequential evaluation never sends — the observation matches, the effect on the world does not; a trap is a bug-class exit, and closing it would require never starting element k+1 before element k finishes, which is sequential execution. This replaces the 0.42.0 rule that in-flight siblings are NOT waited for (#1026: measured then with a 1.5s-sleeping second sibling, both targets aborted in ~0s with an empty stdout — still the observation when the trapping element is the FIRST, as in fan_sibling_trap.almd). Per-element output buffering (ADR-0011 D1) is what lets a concurrent substrate meet it, and is the same mechanism C-004's EXCEPTION clause waits on." since = "0.42.0" status = "active" evidence = [ { path = "spec/wasm_cross/fan_sibling_trap.almd", class = "fixture" }, + { path = "spec/wasm_cross/fan_trap_waits_for_elements_below.almd", class = "fixture" }, ] # ── OPTION TUPLE-PAYLOAD MATRIX ─ diff --git a/docs/specs/als/runtime.md b/docs/specs/als/runtime.md index b2ffa748..488fcf4c 100644 --- a/docs/specs/als/runtime.md +++ b/docs/specs/als/runtime.md @@ -1,6 +1,6 @@ # ALS — 実行時規範（Runtime） -> Last updated: 2026-09-28 +> Last updated: 2026-09-30 プログラム実行の観測規範（エラー終了・文字列補間の表示形・並行コンビネータ）。 参照方法は [strings.md](strings.md) 冒頭と同じ。 @@ -39,6 +39,16 @@ auto-wrap、map の mapper はしない)。`fan.settle { a; b }` の返りは 完了したものではなく、引数リストの先頭から評価した最初の該当)。エラーは ALS-R1 の統一 abort 形で表面化する。 +`fan.map` と `fan.settle` の観測(stdout・stderr・終了コード・返り値)は、 +**全要素をリスト順に一つずつ評価した逐次評価**の観測と同一でなければならない。 +実行基盤(逐次・スレッド・非同期 subtask)の選択はこの観測を変えてはならない +(C-004)。`fan.map` はある要素が Err を返した後も**残りの全要素を評価し**、 +Err が複数あれば**最小 index の Err** を結果とする — ブロック形 `fan { }` +と同じ規則(C-005、C-199、`spec/wasm_cross/fan_map_err_runs_every_element.almd`)。 +要素 k の trap は、要素 0..k-1 が完了して出力がリスト順に現れ、要素 k の +trap までの出力の後に abort する観測となり、k より後の要素の出力は現れない +(C-200、`spec/wasm_cross/fan_trap_waits_for_elements_below.almd`)。 + `fan.race` と `fan.timeout` は 0.42.0 / 0.29.0 でいったん削除された後、 **決定的意味論を得て 0.47.0 で復活した**: race は (spend, index) 辞書式 最小の勝者則(ALS-DT3、C-205 — mapper 形 `fan.race(budget?, xs, f)` を含む)、 diff --git a/proofs/als-validation.toml b/proofs/als-validation.toml index e6c985ee..8aea6c7a 100644 --- a/proofs/als-validation.toml +++ b/proofs/als-validation.toml @@ -677,9 +677,9 @@ verdict = "accurate" [[section]] id = "ALS-R3" -hash = "sha256:d6f1d3484576" -reviewed = "2026-08-27" -by = "O6lvl4 (via the Claude session; four-agent adversarial review 2026-08-27 — prose cross-checked against contract statements, named fixtures and 100+ live probes on almide 0.59.1; 36 sections amended to measurement before stamping)" +hash = "sha256:45ff6fa8a0bb" +reviewed = "2026-09-30" +by = "O6lvl4 (via the Claude session; the ADR-0024 paragraph — sequential run-every-element observation for fan.map / fan.settle, lowest-index Err, trap in element k observed as the sequential evaluation — checked against the amended C-004, C-005 and C-200 statements, C-199, ADR-0024 D1/D6 in almide/almide, and the reference evaluator on spec/wasm_cross/fan_map_err_runs_every_element.almd and fan_trap_waits_for_elements_below.almd)" independent = "no" verdict = "accurate" diff --git a/spec/wasm_cross/fan_map_err_runs_every_element.almd b/spec/wasm_cross/fan_map_err_runs_every_element.almd new file mode 100644 index 00000000..2a352b43 --- /dev/null +++ b/spec/wasm_cross/fan_map_err_runs_every_element.almd @@ -0,0 +1,16 @@ +// @contract: C-005 +// fan.map evaluates EVERY element in list order, including the elements after one +// that returns Err (ADR-0024 D1), and the LOWEST-INDEX Err is the one that surfaces. +// Elements 2 and 4 fail; elements 3 and 5 still run, so all five lines reach stdout +// in list order, and the abort names element 2 — not element 4, and not whichever +// failed first in wall-clock time. The block form `fan { }` already had this rule +// (C-199); a short-circuit after element 2 would print only two lines. +effect fn step(x: Int) -> Result[Int, String] = { + println("element ${x}") + if x == 2 or x == 4 then err("element ${x} failed") else ok(x * 100) +} + +effect fn main() -> Unit = { + let mapped = fan.map([1, 2, 3, 4, 5], (x) => step(x))! + println("unreachable: ${list.len(mapped)}") +} diff --git a/spec/wasm_cross/fan_trap_waits_for_elements_below.almd b/spec/wasm_cross/fan_trap_waits_for_elements_below.almd new file mode 100644 index 00000000..21fc0286 --- /dev/null +++ b/spec/wasm_cross/fan_trap_waits_for_elements_below.almd @@ -0,0 +1,35 @@ +// @contract: C-200 +// A trap in fan element k is observed as the sequential evaluation would observe it +// (ADR-0024 D6): elements 0..k-1 ran to completion and their output reaches stdout +// in list order, then the abort; nothing of any element after k appears. Here the +// trapping element is the SECOND, so the first element's line must be on stdout +// before `Error: division by zero`, and the third element's line must not be. A +// concurrent substrate meets this by waiting for every element below the trap and +// discarding the output of the elements above it; fan_sibling_trap.almd pins the +// case where the trapping element is the first. +// +// The trap is a division by zero routed through `int.parse` so constant folding +// cannot see the zero at compile time. +effect fn before() -> Result[Int, String] = { + println("element 0") + ok(1) +} + +effect fn crash() -> Result[Int, String] = { + let zero = int.parse("0") ?? 1 + ok(100 / zero) +} + +effect fn after() -> Result[Int, String] = { + println("element 2") + ok(3) +} + +effect fn main() -> Unit = { + let (a, b, c) = fan { + before() + crash() + after() + } + println("unreachable ${a} ${b} ${c}") +} From 4d55e195a7a11284c45f7e3d360c72d7c748981b Mon Sep 17 00:00:00 2001 From: O6lvl4 Date: Wed, 30 Sep 2026 23:34:09 +0900 Subject: [PATCH 3/3] Regenerate the conformance index after rebasing onto the C-132 amendment Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/contracts/conformance.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index 11071bb9..95d93e2b 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; 817 distinct executable fixtures. +134 normative sections; 819 distinct executable fixtures. | Section | Contracts | Fixtures (how CI runs each) | |---------|-----------|------------------------------|