Found while adding is_dir (#576) with the tape-first treatment: the older filesystem predicates in src/builtins.c are neither trace-recorded nor replay-blocked:
file_exists — fopen probe, plain returnls — readdir listingmkdir — returns a stat-based success bit (and mutates the fs)getcwd, exe_path — process-environment reads
They sit in neither of docs/TRACE.md's two lists (wrapped N-record sources vs. loudly-non-replayable). Under EIGS_REPLAY they run live: a program that branches on file_exists of p replays against the current filesystem, not the recorded one — the same closed-world hole #471 closed for args, and the same class the (closed) #148 covered for proc_*. A tape recorded on one machine silently diverges on another.
Newly added fs reads are traced (is_dir #576, read_line #558 — both carry N records and replay deterministically), so the inconsistency is now visible side by side in the File I/O table of docs/BUILTINS.md.
Proposed: wrap the pure reads (file_exists, ls, getcwd, exe_path) with TRACE_NONDET_RET/TAKE+RECORD; decide mkdir (a write whose return is fs-dependent) either the same way or as a loudly-non-replayable builtin per the #148 convention. One replay test per builtin (record, mutate the fs, replay must serve the recorded answer — same shape as the #576 test in tests/test_replay.sh).
Found while adding
is_dir(#576) with the tape-first treatment: the older filesystem predicates in src/builtins.c are neither trace-recorded nor replay-blocked:file_exists— fopen probe, plain returnls— readdir listingmkdir— returns a stat-based success bit (and mutates the fs)getcwd,exe_path— process-environment readsThey sit in neither of docs/TRACE.md's two lists (wrapped N-record sources vs. loudly-non-replayable). Under
EIGS_REPLAYthey run live: a program that branches onfile_exists of preplays against the current filesystem, not the recorded one — the same closed-world hole #471 closed forargs, and the same class the (closed) #148 covered forproc_*. A tape recorded on one machine silently diverges on another.Newly added fs reads are traced (
is_dir#576,read_line#558 — both carry N records and replay deterministically), so the inconsistency is now visible side by side in the File I/O table of docs/BUILTINS.md.Proposed: wrap the pure reads (
file_exists,ls,getcwd,exe_path) withTRACE_NONDET_RET/TAKE+RECORD; decidemkdir(a write whose return is fs-dependent) either the same way or as a loudly-non-replayable builtin per the #148 convention. One replay test per builtin (record, mutate the fs, replay must serve the recorded answer — same shape as the #576 test in tests/test_replay.sh).