Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions docs/contracts/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -254,12 +254,12 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1
| C-217 | let _ = f() discards the Result — the err does not propagate | 0.55.0 | active | fixture | 1 |
| C-218 | a heap-payload ?? returned as the fn tail yields the same value on both targets | 0.56.0 | active | fixture | 2 |
| C-219 | a Never-typed call in a branch arm runs on both targets and sets the exit code | 0.56.0 | active | fixture | 1 |
| C-220 | fs streaming line walkers fold/each with read_lines line semantics | 0.56.1 | active | fixture | 0 |
| C-220 | fs streaming line walkers fold/each with read_lines line semantics | 0.56.1 | active | fixture | 1 |
| C-221 | An effect fn-typed slot admits pure and fallible lambdas with one carrier semantics | 0.56.1 | active | fixture | 2 |
| C-222 | An expression-nested scalar unwrap propagates the err identically on both legs | 0.56.1 | active | fixture | 1 |
| C-223 | Matrix transcendentals compute through the vendored musl-libm, not the platform one | 0.56.1 | active | fixture | 3 |
| C-224 | if let / guard let bind and release heap payloads identically on both targets | 0.56.1 | active | fixture | 1 |
| C-225 | fs.read_lines materializes a file's lines identically on both targets | 0.56.2 | active | fixture | 1 |
| C-225 | fs.read_lines materializes a file's lines identically on both targets | 0.56.2 | active | fixture | 2 |
| C-226 | A mut parameter crossing a call boundary mutates the caller's data on both targets | 0.56.2 | active | fixture | 3 |
| C-227 | The fs metadata and composition family answers identically on both targets | 0.56.2 | active | fixture | 1 |
| C-228 | The fs composition family and the matrix row selectors answer identically on both targets | 0.56.2 | active | fixture | 3 |
Expand Down
4 changes: 2 additions & 2 deletions docs/contracts/conformance.md
Original file line number Diff line number Diff line change
Expand Up @@ -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; 809 distinct executable fixtures.
132 normative sections; 810 distinct executable fixtures.

| Section | Contracts | Fixtures (how CI runs each) |
|---------|-----------|------------------------------|
Expand Down Expand Up @@ -104,7 +104,7 @@
| ALS-R3 | C-004, C-005, C-006, C-199, C-321, C-349 | `spec/wasm_cross/fan_deterministic.almd` (byte-compare)<br>`spec/wasm_cross/fan_map_inline_lambda.almd` (byte-compare)<br>`spec/wasm_cross/fan_pure_thunks.almd` (byte-compare)<br>`spec/wasm_cross/fan_var_thunk_list.almd` (byte-compare)<br>`spec/wasm_cross/fan_effect_mapper.almd` (byte-compare)<br>`spec/wasm_cross/fan_effect_mapper_capability.almd` (byte-compare)<br>`spec/embedded_cross/fan_mapper_effect_callback_forms.almd` (both-target test)<br>`spec/wasm_cross/fan_map_err.almd` (byte-compare)<br>`spec/wasm_cross/fan_map_inline_err.almd` (byte-compare)<br>`spec/wasm_cross/fan_any_allfail.almd` (byte-compare)<br>`spec/wasm_cross/option_none_unwrap_term.almd` (byte-compare)<br>`tests/diagnostics/e027-fan-timeout-removed/broken.almd` (checker)<br>`tests/diagnostic_harness_test.rs` (cargo gate)<br>`spec/wasm_cross/fan_block_err_list_order.almd` (byte-compare)<br>`spec/wasm_cross/fan_prefetch_fs.almd` (byte-compare)<br>`tests/component_p3_test.rs` (cargo gate)<br>`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 | `spec/wasm_cross/process_args.almd` (byte-compare)<br>`spec/wasm_cross/random_int_entropy.almd` (byte-compare)<br>`spec/wasm_cross/env_args.almd` (byte-compare)<br>`spec/wasm_cross/env_get.almd` (byte-compare)<br>`spec/wasm_cross/env_platform_reporting.almd` (byte-compare)<br>`spec/stdlib/process_timeout_test.almd` (both-target test)<br>`spec/stdlib/fs_if_exists_test.almd` (both-target test)<br>`spec/wasm_cross/fs_read_directory_errno.almd` (byte-compare)<br>`spec/wasm_cross/fs_read_text_utf8.almd` (byte-compare)<br>`spec/wasm_cross/env_sleep_pause.almd` (byte-compare)<br>`spec/wasm_cross/availability_pure_batch.almd` (byte-compare)<br>`tests/component_p3_test.rs` (cargo gate)<br>`spec/embedded_cross/http_client_errs.almd` (both-target test)<br>`spec/embedded_cross/http_framed_errs.almd` (both-target test)<br>`spec/wasm_cross/env_set_overlay.almd` (byte-compare)<br>`spec/wasm_cross/zlib_selfhost.almd` (byte-compare)<br>`spec/stdlib/http_call_test.almd` (both-target test)<br>`spec/embedded_cross/http_call_handle_errs.almd` (both-target test)<br>`spec/serve_cross/http_serve_replay.almd` (both-target test)<br>`spec/serve_cross/http_serve_shutdown.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)<br>`spec/wasm_cross/fs_relative_path.almd` (byte-compare)<br>`spec/stdlib/fs_stat_test.almd` (both-target test)<br>`spec/stdlib/fs_streaming_test.almd` (both-target test)<br>`spec/stdlib/fs_fold_lines_range_test.almd` (both-target test)<br>`spec/stdlib/fs_fold_lines_chunked_test.almd` (both-target test)<br>`spec/wasm_cross/fs_read_lines.almd` (byte-compare)<br>`spec/wasm_cross/fs_metadata_family.almd` (byte-compare)<br>`spec/wasm_cross/fs_composition_family.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows.almd` (byte-compare)<br>`spec/wasm_cross/fs_glob_segments.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows_oob.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q_dims_guard.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows_q1_partial_block.almd` (byte-compare)<br>`spec/wasm_cross/bytes_negative_offset_family.almd` (byte-compare)<br>`spec/wasm_cross/matrix_domain_edges.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q1_full_loader_cols_beyond_buffer.almd` (byte-compare)<br>`spec/wasm_cross/flight_pid_control.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q_fp16_scale_domain.almd` (byte-compare)<br>`spec/wasm_cross/fs_list_dir_multipass.almd` (byte-compare)<br>`spec/wasm_cross/fs_write_errno.almd` (byte-compare)<br>`spec/wasm_fail/rope_geometry_exceeds_aborts.almd` (both-target test)<br>`spec/wasm_cross/rope_geometry_family.almd` (byte-compare)<br>`spec/wasm_cross/rope_at_family.almd` (byte-compare)<br>`spec/wasm_fail/matrix_index_oob_aborts.almd` (both-target test)<br>`spec/wasm_cross/matrix_index_domain_family.almd` (byte-compare)<br>`spec/wasm_cross/callee_shadowing_family.almd` (byte-compare)<br>`spec/wasm_cross/fallible_hof_effect_callback_family.almd` (byte-compare) |
| 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)<br>`spec/wasm_cross/fs_relative_path.almd` (byte-compare)<br>`spec/stdlib/fs_stat_test.almd` (both-target test)<br>`spec/stdlib/fs_streaming_test.almd` (both-target test)<br>`spec/stdlib/fs_fold_lines_range_test.almd` (both-target test)<br>`spec/stdlib/fs_fold_lines_chunked_test.almd` (both-target test)<br>`spec/wasm_cross/line_endings_bare_cr.almd` (byte-compare)<br>`spec/wasm_cross/fs_read_lines.almd` (byte-compare)<br>`spec/wasm_cross/fs_metadata_family.almd` (byte-compare)<br>`spec/wasm_cross/fs_composition_family.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows.almd` (byte-compare)<br>`spec/wasm_cross/fs_glob_segments.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows_oob.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q_dims_guard.almd` (byte-compare)<br>`spec/wasm_cross/matrix_select_rows_q1_partial_block.almd` (byte-compare)<br>`spec/wasm_cross/bytes_negative_offset_family.almd` (byte-compare)<br>`spec/wasm_cross/matrix_domain_edges.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q1_full_loader_cols_beyond_buffer.almd` (byte-compare)<br>`spec/wasm_cross/flight_pid_control.almd` (byte-compare)<br>`spec/wasm_cross/matrix_q_fp16_scale_domain.almd` (byte-compare)<br>`spec/wasm_cross/fs_list_dir_multipass.almd` (byte-compare)<br>`spec/wasm_cross/fs_write_errno.almd` (byte-compare)<br>`spec/wasm_fail/rope_geometry_exceeds_aborts.almd` (both-target test)<br>`spec/wasm_cross/rope_geometry_family.almd` (byte-compare)<br>`spec/wasm_cross/rope_at_family.almd` (byte-compare)<br>`spec/wasm_fail/matrix_index_oob_aborts.almd` (both-target test)<br>`spec/wasm_cross/matrix_index_domain_family.almd` (byte-compare)<br>`spec/wasm_cross/callee_shadowing_family.almd` (byte-compare)<br>`spec/wasm_cross/fallible_hof_effect_callback_family.almd` (byte-compare) |
| ALS-R7 | C-274, C-335 | `spec/embedded_cross/fs_fallible_callback_compound.almd` (both-target test)<br>`spec/wasm_cross/fs_fallible_stream_callback.almd` (byte-compare)<br>`spec/stdlib/fs_streaming_test.almd` (both-target test)<br>`tests/fs_streaming_family_gate_test.rs` (cargo gate)<br>`spec/wasm_cross/path_extension_hidden.almd` (byte-compare) |
| ALS-R8 | C-275, C-368 | `spec/wasm_cross/http_response_headers.almd` (byte-compare)<br>`spec/stdlib/http_router_test.almd` (both-target test) |
| ALS-R9 | C-350, C-351 | `tests/incumbent_exit_tail_test.rs` (cargo gate)<br>`spec/wasm_cross/exit_code_out_of_range.almd` (byte-compare)<br>`spec/wasm_cross/exit_code_upper_bound.almd` (byte-compare)<br>`spec/wasm_cross/exit_code_passthrough.almd` (byte-compare)<br>`spec/embedded_cross/exit_status_passthrough.almd` (both-target test)<br>`tests/diagnostics/e084-exit-code-domain/broken.almd` (checker)<br>`tests/diagnostics/e084-exit-code-signed/broken.almd` (checker)<br>`tests/diagnostics/e084-exit-code-pipe/broken.almd` (checker)<br>`tests/exit_literal_check_test.rs` (cargo gate) |
Expand Down
6 changes: 4 additions & 2 deletions docs/contracts/contracts.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2700,13 +2700,14 @@ evidence = [
id = "C-220"
spec = "ALS-R6"
title = "fs streaming line walkers fold/each with read_lines line semantics"
statement = "The streaming family {`fs.fold_lines`, `fs.for_each_line`} walks a file line-by-line through a buffered reader without materializing a `List[String]` — peak memory is O(longest line), not O(file) (measured: 2.2 GB eager vs 1 MB streaming on a 632 MB input, research/benchmark/perf/README.md). Line semantics byte-match `fs.read_lines`: split on \\n, one trailing \\r stripped per line, no phantom empty line after a trailing newline, a final newline-less line still yielded, and a missing file is the same err(message) the eager reader produces. An empty file folds to `init` with zero callback invocations. One deliberate divergence, inherent to streaming: a mid-file read error surfaces AFTER the callbacks for earlier lines have run — the eager reader fails before yielding anything. The family is exactly {fold_lines, for_each_line, fold_lines_range, fold_lines_chunked} (tests/fs_streaming_family_gate_test.rs). The range cell is the chunk worker's walker — a line is owned by the chunk containing the byte BEFORE its first byte (line 0 by the chunk containing byte 0), so folding a partition of [0, file_size) visits every line exactly once. The chunked cell runs one range worker per chunk on scoped threads INSIDE the runtime (the fan machinery's purity gate keeps effectful bodies sequential, so file parallelism is the fs module's own intrinsic) and returns partials in CHUNK ORDER — merging stays with the caller, so the observable result is deterministic whatever the thread schedule, and the emitted program's Send+Sync bounds make a state-capturing callback a compile error rather than a race. Transforming pipelines belong on fold_lines, the eager List belongs to read_lines, and chunk workers accumulate (for_each has no range/chunked cell). The ADR-0006 fallible callback forms are NO LONGER a tracked omission: the two sequential, callback-driven cells {fold_lines, for_each_line} carry them (C-274, #1144) and the two partitioned cells {fold_lines_range, fold_lines_chunked} decline them for a stated reason — a partitioned walk has no defined first err — with tests/fs_streaming_family_gate_test.rs pinning BOTH columns, so the family's ADR-0006 shape is now machine-enforced rather than narrated. The PLAIN surface's wasm reach is still partial — the callback crosses the runtime boundary, and generic HOF closures are the wasm defunctionalization frontier (#1134) — so only the accumulator shapes with self-host twins in stdlib/fs_fold_lines.almd (`fold_lines` with a `Map[String, Int]` acc, `fold_lines_chunked` with a `Map[String, Int]` / `Int` / `List[String]` acc, `fold_lines_range` with a `List[String]` acc) run on wasm, byte-identical to native; every other cell — a String acc, non-String-element list accs — routes to an unregistered `_x` name and walls honestly at render, never a wrong-typed link; `for_each_line` has no twin at all and walls on both its plain and fallible forms. The wasm render walls honestly, and the pinned fixtures bind the wasm leg on arrival, C-215-style."
statement = "The streaming family {`fs.fold_lines`, `fs.for_each_line`} walks a file line-by-line through a buffered reader without materializing a `List[String]` — peak memory is O(longest line), not O(file) (measured: 2.2 GB eager vs 1 MB streaming on a 632 MB input, research/benchmark/perf/README.md). Line semantics byte-match `fs.read_lines`: split on \\n, the \\r of a \\r\\n terminator stripped with it and a bare \\r kept as line content (a \\r ending the file stays on the last line), no phantom empty line after a trailing newline, a final newline-less line still yielded, and a missing file is the same err(message) the eager reader produces. An empty file folds to `init` with zero callback invocations. One deliberate divergence, inherent to streaming: a mid-file read error surfaces AFTER the callbacks for earlier lines have run — the eager reader fails before yielding anything. The family is exactly {fold_lines, for_each_line, fold_lines_range, fold_lines_chunked} (tests/fs_streaming_family_gate_test.rs). The range cell is the chunk worker's walker — a line is owned by the chunk containing the byte BEFORE its first byte (line 0 by the chunk containing byte 0), so folding a partition of [0, file_size) visits every line exactly once. The chunked cell runs one range worker per chunk on scoped threads INSIDE the runtime (the fan machinery's purity gate keeps effectful bodies sequential, so file parallelism is the fs module's own intrinsic) and returns partials in CHUNK ORDER — merging stays with the caller, so the observable result is deterministic whatever the thread schedule, and the emitted program's Send+Sync bounds make a state-capturing callback a compile error rather than a race. Transforming pipelines belong on fold_lines, the eager List belongs to read_lines, and chunk workers accumulate (for_each has no range/chunked cell). The ADR-0006 fallible callback forms are NO LONGER a tracked omission: the two sequential, callback-driven cells {fold_lines, for_each_line} carry them (C-274, #1144) and the two partitioned cells {fold_lines_range, fold_lines_chunked} decline them for a stated reason — a partitioned walk has no defined first err — with tests/fs_streaming_family_gate_test.rs pinning BOTH columns, so the family's ADR-0006 shape is now machine-enforced rather than narrated. The PLAIN surface's wasm reach is still partial — the callback crosses the runtime boundary, and generic HOF closures are the wasm defunctionalization frontier (#1134) — so only the accumulator shapes with self-host twins in stdlib/fs_fold_lines.almd (`fold_lines` with a `Map[String, Int]` acc, `fold_lines_chunked` with a `Map[String, Int]` / `Int` / `List[String]` acc, `fold_lines_range` with a `List[String]` acc) run on wasm, byte-identical to native; every other cell — a String acc, non-String-element list accs — routes to an unregistered `_x` name and walls honestly at render, never a wrong-typed link; `for_each_line` has no twin at all and walls on both its plain and fallible forms. The wasm render walls honestly, and the pinned fixtures bind the wasm leg on arrival, C-215-style."
since = "0.56.1"
status = "active"
evidence = [
{ path = "spec/stdlib/fs_streaming_test.almd", class = "fixture" },
{ path = "spec/stdlib/fs_fold_lines_range_test.almd", class = "fixture" },
{ path = "spec/stdlib/fs_fold_lines_chunked_test.almd", class = "fixture" },
{ path = "spec/wasm_cross/line_endings_bare_cr.almd", class = "fixture" },
]
[[contract]]
id = "C-221"
Expand Down Expand Up @@ -2756,11 +2757,12 @@ evidence = [
id = "C-225"
spec = "ALS-R6"
title = "fs.read_lines materializes a file's lines identically on both targets"
statement = "`fs.read_lines(path)` returns the file's lines with `str::lines()` semantics byte-identically native <-> wasm: split on \\n, one trailing \\r stripped per line (CRLF), no phantom empty line after a trailing newline, a final newline-less line still yielded, the empty file `Ok([])`, and a missing file the err channel on both legs. The wasm self-host (stdlib/fs_read_lines.almd) is the native oracle's exact composition — `read_to_string(path).map(|s| s.lines()...)` becomes prim.read_text_file + string.lines — so the line-splitting semantics are shared with C-220's streaming family by construction, and the result rides fs.list_dir's proven `Result[List[String], String]` cap-as-tag rails (tag @16, recursive DropResultListStr). Before this contract fs.read_lines had NO wasm body at all: every program touching it fell off the wasm leg (a COMPILER_FRONTIER row in proofs/wasm-reachability-baseline.txt, burned down with this contract). `fs.read_lines_if_exists` stays native-only debt on that ledger — its `Result[List[String]?, String]` shape has no tracking rails yet, and the reachability ratchet keeps it honest."
statement = "`fs.read_lines(path)` returns the file's lines with `str::lines()` semantics byte-identically native <-> wasm: split on \\n, the \\r of a \\r\\n terminator stripped with it and a bare \\r kept as line content (a \\r ending the input stays on the last line), no phantom empty line after a trailing newline, a final newline-less line still yielded, the empty file `Ok([])`, and a missing file the err channel on both legs. The wasm self-host (stdlib/fs_read_lines.almd) is the native oracle's exact composition — `read_to_string(path).map(|s| s.lines()...)` becomes prim.read_text_file + string.lines — so the line-splitting semantics are shared with C-220's streaming family by construction, and the result rides fs.list_dir's proven `Result[List[String], String]` cap-as-tag rails (tag @16, recursive DropResultListStr). Before this contract fs.read_lines had NO wasm body at all: every program touching it fell off the wasm leg (a COMPILER_FRONTIER row in proofs/wasm-reachability-baseline.txt, burned down with this contract). `fs.read_lines_if_exists` stays native-only debt on that ledger — its `Result[List[String]?, String]` shape has no tracking rails yet, and the reachability ratchet keeps it honest."
since = "0.56.2"
status = "active"
evidence = [
{ path = "spec/wasm_cross/fs_read_lines.almd", class = "fixture" },
{ path = "spec/wasm_cross/line_endings_bare_cr.almd", class = "fixture" },
]
[[contract]]
id = "C-226"
Expand Down
5 changes: 2 additions & 3 deletions ref/src/stdlib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1428,10 +1428,9 @@ pub fn call(it: &mut Interp, name: &str, args: Vec<Value>) -> Result<Value, Flow
cur.push(c);
}
}
// The final UNTERMINATED line keeps a trailing '\r': only a "\r\n"
// pair is a line ending, a bare '\r' is content (`str::lines`).
if !cur.is_empty() {
if cur.ends_with('\r') {
cur.pop();
}
out.push(Value::str(&cur));
}
Ok(Value::List(Rc::new(out)))
Expand Down
5 changes: 2 additions & 3 deletions ref/src/stdlib_ext.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1357,10 +1357,9 @@ pub fn split_lines(s: &str) -> Vec<String> {
cur.push(c);
}
}
// The final UNTERMINATED line keeps a trailing '\r': the '\r' goes only with
// the '\n' it precedes (native pops a '\n', and only then a '\r').
if !cur.is_empty() {
if cur.ends_with('\r') {
cur.pop();
}
out.push(cur);
}
out
Expand Down
Loading
Loading