Restate C-004, C-005 and C-200 as ADR-0024's sequential run-every-element observation

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 |

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: <msg>` + 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: <msg>` + 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: <msg>` + 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: <msg>` + 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 ─

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)` を含む)、

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"