diff --git a/docs/contracts/README.md b/docs/contracts/README.md index 1532d209..68460074 100644 --- a/docs/contracts/README.md +++ b/docs/contracts/README.md @@ -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 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index 97ce1639..a7776f70 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; 809 distinct executable fixtures. +132 normative sections; 810 distinct executable fixtures. | Section | Contracts | Fixtures (how CI runs each) | |---------|-----------|------------------------------| @@ -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)
`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-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)
`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/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) | -| 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/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) | +| 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) | | ALS-R7 | C-274, C-335 | `spec/embedded_cross/fs_fallible_callback_compound.almd` (both-target test)
`spec/wasm_cross/fs_fallible_stream_callback.almd` (byte-compare)
`spec/stdlib/fs_streaming_test.almd` (both-target test)
`tests/fs_streaming_family_gate_test.rs` (cargo gate)
`spec/wasm_cross/path_extension_hidden.almd` (byte-compare) | | ALS-R8 | C-275, C-368 | `spec/wasm_cross/http_response_headers.almd` (byte-compare)
`spec/stdlib/http_router_test.almd` (both-target test) | | ALS-R9 | C-350, C-351 | `tests/incumbent_exit_tail_test.rs` (cargo gate)
`spec/wasm_cross/exit_code_out_of_range.almd` (byte-compare)
`spec/wasm_cross/exit_code_upper_bound.almd` (byte-compare)
`spec/wasm_cross/exit_code_passthrough.almd` (byte-compare)
`spec/embedded_cross/exit_status_passthrough.almd` (both-target test)
`tests/diagnostics/e084-exit-code-domain/broken.almd` (checker)
`tests/diagnostics/e084-exit-code-signed/broken.almd` (checker)
`tests/diagnostics/e084-exit-code-pipe/broken.almd` (checker)
`tests/exit_literal_check_test.rs` (cargo gate) | diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index e7831d04..4ef424eb 100644 --- a/docs/contracts/contracts.toml +++ b/docs/contracts/contracts.toml @@ -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" @@ -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" diff --git a/ref/src/stdlib.rs b/ref/src/stdlib.rs index 91dd72b2..1798d34f 100644 --- a/ref/src/stdlib.rs +++ b/ref/src/stdlib.rs @@ -1428,10 +1428,9 @@ pub fn call(it: &mut Interp, name: &str, args: Vec) -> Result Vec { 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 diff --git a/spec/wasm_cross/line_endings_bare_cr.almd b/spec/wasm_cross/line_endings_bare_cr.almd new file mode 100644 index 00000000..15e95cb6 --- /dev/null +++ b/spec/wasm_cross/line_endings_bare_cr.almd @@ -0,0 +1,52 @@ +// @contract: C-225, C-220 +// #2813: a line ending is "\n" or "\r\n" — a BARE '\r' is line CONTENT, the +// `str::lines` rule every line surface shares: `string.lines`, `fs.read_lines` +// (its composition) and the streaming walkers `fs.fold_lines` / `for_each_line` +// (native pops a '\n', and only then a '\r'). The incumbent wasm leg's self-host +// walkers stripped a '\r' from the FINAL line even when no '\n' followed it +// ("abc\r" read as "abc"); the structural leg and native kept it. +// +// The inputs are chosen off the degenerate line: the CR ends the input, ends it +// twice, ends the last of two lines, sits mid-line, precedes a CRLF, and stands +// alone — each line is printed with its CRs spelled out, so a stripped or a +// kept '\r' is a visible byte, not a length that happens to match. +// +// SELF-CONTAINED: creates its own temp dir (never printed), removes it at the end. +import fs + +fn spell(l: String) -> String = "'" + string.replace(l, "\r", "") + "'" + +fn show(ls: List[String]) -> String = ls |> list.map((l) => spell(l)) |> list.join(" ") + +effect fn step(acc: Int, l: String) -> Result[Int, String] = ok(acc * 100 + string.len(l) + 1) + +effect fn visit(l: String) -> Result[Unit, String] = { + println(" each ${spell(l)}") + ok(()) +} + +effect fn probe(dir: String, name: String, s: String) -> Unit = { + let p = dir + "/probe.txt" + fs.write(p, s)! + println(name) + println(" lines ${show(string.lines(s))}") + println(" read ${show(fs.read_lines(p)!)}") + println(" fold ${fs.fold_lines(p, "", (acc, l) => acc + spell(l))!}") + println(" fold_i ${int.to_string(fs.fold_lines(p, 0, (acc, l) => acc * 100 + string.len(l) + 1)!)}") + println(" fold_! ${int.to_string(fs.fold_lines(p, 0, (acc, l) => step(acc, l)!)!)}") + fs.for_each_line(p, (l) => visit(l)!)! +} + +effect fn main() -> Unit = { + let dir = fs.create_temp_dir("xt_bare_cr")! + probe(dir, "cr-end", "abc\r")! + probe(dir, "cr-cr-end", "abc\r\r")! + probe(dir, "cr-ends-last-line", "a\nbc\r")! + probe(dir, "crlf-end", "abc\r\n")! + probe(dir, "lf-end", "abc\n")! + probe(dir, "empty", "")! + probe(dir, "lone-cr", "\r")! + probe(dir, "crlf-then-cr", "\r\n\r")! + probe(dir, "cr-mid-and-doubled", "a\rb\r\r\n\rc\r")! + fs.remove_all(dir)! +}