feat(trace): tape format versioning — version-stamped tapes, refuse-on-mismatch (#411)

CHANGELOG.md

@@ -13,6 +13,23 @@ All notable changes to EigenScript are documented here.
   `chr of n` == `str_from_bytes of [n]` across the shared range.
 
 ### Added
+- **Trace-tape format versioning** (#411): every tape now opens with a
+  `V <format> <runtime>` header (both the hosted `EIGS_TRACE` file and the
+  embed sink), and replay refuses a tape whose format or runtime version
+  doesn't match the running binary — missing/malformed/mismatched headers
+  exit with status 3 (hosted) or reject the tape at `eigs_set_replay_tape`
+  (embed, returns 0). Version-and-reject, no migration, no override flag;
+  the decision and the residual dev-build honesty gap are recorded in
+  docs/TRACE.md. Pre-#411 (headerless) tapes are no longer replayable.
+  Hardened by adversarial review: an unopenable `EIGS_REPLAY` path is now
+  fatal too (was warn-and-run-live — the same silent divergence); the
+  embed install validates *every* session header of a concatenated
+  journal up front and swaps atomically (a refused/OOM install leaves the
+  previously active tape and strict mode untouched, and can never abort
+  the host mid-eval); torn mid-stream `V` lines refuse instead of
+  slipping through the record filter; and `--version`/`--help` are
+  handled before `trace_init` so a stale exported `EIGS_REPLAY` can't
+  take down pure queries.
 - **W016 — bare-predicate aliasing fence** (#396, completing it): a bare
   trajectory predicate outside a loop condition (`if stable:`,
   `ok is converged`, `return diverging`) reads the last-observed binding —

docs/TRACE.md

@@ -23,10 +23,11 @@ predicted-not-taken load + branch.
 
 ## Tape Format
 
-The tape is plain text, one record per line, three record kinds:
+The tape is plain text, one record per line, four record kinds:
 
 | Record | Meaning |
 |--------|---------|
+| `V <format> <runtime>` | Version header — always the first record (e.g. `V 1 0.26.0`). Stamped once per tape-open; a journal appended across sessions carries one per session. See [Format Versioning](#format-versioning-411). |
 | `L <line>` | Source-line event (from `OP_LINE`). Adjacent duplicate lines with no `A`/`N` between them are deduped — the compiler emits per-statement LINEs and bare repeats are noise. |
 | `A <name>=<value>` | Assignment delta: a top-level binding changed. |
 | `N <fn>=<value>` | Nondeterministic builtin return — the replay-determinism substrate. |
@@ -145,11 +146,60 @@ that actually failed, not a fresh one that might not.
 Under `--json`, each result carries a `"tape"` field for CI to archive as an
 artifact; the human form prints the replay line.
 
-**Same-binary caveat.** A tape is a reproducer for the interpreter build that
-recorded it. Until tape-format versioning lands (#411), do not replay a tape
-against a different EigenScript version — archive the tape *and* the version
-that produced it. `EIGS_REPLAY_STRICT=1` turns any record/replay mismatch into a
-loud abort rather than a silent divergence.
+**Same-version enforcement.** A tape is a reproducer for the EigenScript
+version that recorded it, and since #411 the runtime enforces that
+mechanically: replaying an archived tape after a version bump refuses loudly
+instead of silently diverging (see [Format Versioning](#format-versioning-411)).
+Archiving jobs need only keep the tape — it names its own version on line 1.
+`EIGS_REPLAY_STRICT=1` additionally turns any record/replay *name* mismatch
+into a loud abort.
+
+## Format Versioning (#411)
+
+The tape is a persisted artifact — CI archives failure tapes, bundles may
+carry one, embedders journal them — so it names its own provenance. **The
+decision: version-stamped tapes, refuse-on-mismatch. There is no
+compatibility promise, ever** — a tape is valid for exactly the format
+*and* runtime version that recorded it, matching the no-backcompat policy
+everywhere else in the runtime (version-and-reject, never migrate).
+
+- Every tape's first record is `V <format> <runtime>`. The format integer
+  (`TRACE_FORMAT_VERSION` in `src/trace.h`) bumps on **any** change to the
+  tape encoding; the runtime string is the recording binary's version.
+- On replay, a missing header, a malformed (torn) header, a different
+  format version, a different runtime version, an empty tape, or an
+  unopenable `EIGS_REPLAY` path each refuse loudly — hosted replay exits
+  with status 3 (the replay-divergence status), and `eigs_set_replay_tape`
+  returns 0 without installing the tape. Replay never falls back to a
+  live run: the user asked for a replay, and a plausible-looking live run
+  is exactly the silent divergence the header exists to prevent.
+- Mid-stream `V` records are legal (a journal appended across sessions
+  carries one per session) but each must match, or replay aborts. The
+  embed seam validates **every** session header at install time, so a
+  mixed-version journal is refused up front (return 0, the previously
+  installed tape left untouched) rather than aborting the host mid-run;
+  the mid-stream abort therefore only fires for `EIGS_REPLAY` files.
+
+```
+$ EIGS_REPLAY=old-v0.26.0.tape eigenscript sim.eigs
+trace: tape recorded on EigenScript 0.26.0, this binary is 0.27.0 —
+refusing to replay; a tape is valid only for the version that recorded
+it (docs/TRACE.md)
+$ echo $?
+3
+```
+
+There is no override flag. The tape is plain text: if you are certain a
+tape is valid for this binary (say, two dev builds of the same tree),
+editing line 1 is the override — a deliberate, visible act. The residual
+honesty gap runs the other way: version *equality* is necessary, not
+sufficient. Two different dev builds can share the string `dev` (or an
+unreleased version), and the header cannot tell them apart — release
+boundaries are enforced; dev builds are on their honor.
+
+Regression coverage: the `version refuse` cases in `tests/test_replay.sh`
+plant each mismatch class (format, runtime, missing header, empty file)
+and require the exit-3 refusal.
 
 ## Temporal Interrogatives and `state_at`
 

src/eigs_embed.h

@@ -146,17 +146,29 @@ void           eigs_value_buffer_set(EigsValue *v, int i, double x); /* OOB: no-
 /* ---- Trace tape (record + replay) ----------------------------------
  * The runtime's replay tape (hosted: EIGS_TRACE / EIGS_REPLAY files),
  * reachable without a filesystem. Install a sink and every tape record
- * (L/A/N lines) streams to it as bytes — the sink receives complete
+ * (V/L/A/N lines) streams to it as bytes — the sink receives complete
  * newline-terminated lines (an oversized record arrives in ordered
- * chunks). Installing a sink ENABLES recording; passing NULL stops it.
- * The sink fires from inside evaluation — do not re-enter the runtime
- * from it; buffer the bytes and act between evals.
+ * chunks). Installing a sink ENABLES recording — the first bytes are the
+ * version header (`V <format> <runtime>`, #411); a journal appended
+ * across several installs carries one header per session. Passing NULL
+ * stops recording. The sink fires from inside evaluation — do not
+ * re-enter the runtime from it; buffer the bytes and act between evals.
  *
  * eigs_set_replay_tape hands the whole tape back as the replay source
- * (bytes are copied; returns 0 on OOM; NULL clears). While replay is
- * active, nondet builtins return the tape's recorded N values in order
- * instead of consulting their live sources. `strict` makes a tape/
- * program name mismatch fatal instead of logged-and-tolerated.
+ * (bytes are copied; NULL clears). Returns 0 on OOM or when the tape is
+ * REFUSED: a tape whose version headers are missing, torn, or don't
+ * match this runtime (format and version both) is never installed —
+ * version-and-reject, no migration (#411, docs/TRACE.md; reason goes to
+ * stderr). EVERY session header in a concatenated journal is validated
+ * at install time, so refusal always happens here, not mid-eval. The
+ * call is atomic: on any 0 return the previously installed tape (and
+ * its strict mode) survives untouched. An empty journal is refused —
+ * a fresh store has nothing to replay; install nothing instead. Store
+ * tape bytes verbatim: strip a header and replay refuses the journal.
+ * While replay is active, nondet builtins return the tape's recorded N
+ * values in order instead of consulting their live sources. `strict`
+ * makes a tape/program name mismatch fatal instead of
+ * logged-and-tolerated.
  *
  * Host builtins participate through the take/record pair — the same
  * contract the runtime's own nondet builtins use:

src/embed_smoke.c

@@ -246,6 +246,35 @@ int main(void) {
     CHECK(r != NULL && eigs_value_as_num(r) == 104.0, "clear: live again");
     if (r) eigs_value_release(r);
 
+    /* --- #411 refusal contract: install-time, atomic, return 0. ------ */
+    /* Headerless tape: refused, nothing installed, live source intact. */
+    static const char noh[] = "N host_sensor=999\n";
+    CHECK(eigs_set_replay_tape(noh, sizeof noh - 1, 0) == 0,
+          "headerless tape refused (return 0)");
+    r = eigs_eval_string("host_sensor of []");
+    CHECK(r != NULL && eigs_value_as_num(r) == 105.0,
+          "refused install: live source untouched");
+    if (r) eigs_value_release(r);
+
+    /* Mixed-version concatenated journal: a later session's mismatched
+     * header refuses the WHOLE install up front — never a mid-eval abort. */
+    static char mixed[sizeof g_tape + 64];
+    size_t ml = g_tape_len;
+    memcpy(mixed, g_tape, ml);
+    ml += (size_t)snprintf(mixed + ml, sizeof mixed - ml,
+                           "V 1 0.0.0-elsewhere\nN host_sensor=888\n");
+    CHECK(eigs_set_replay_tape(mixed, ml, 0) == 0,
+          "mixed-version journal refused at install");
+
+    /* Atomic swap: a refused install leaves the ACTIVE tape serving. */
+    CHECK(eigs_set_replay_tape(g_tape, g_tape_len, 0) == 1, "good tape re-set");
+    CHECK(eigs_set_replay_tape(noh, sizeof noh - 1, 0) == 0, "swap refused");
+    r = eigs_eval_string("host_sensor of []");
+    CHECK(r != NULL && eigs_value_as_num(r) == 100.0,
+          "refused swap: previous tape still serves");
+    if (r) eigs_value_release(r);
+    CHECK(eigs_set_replay_tape(NULL, 0, 0) == 1, "replay cleared (411 block)");
+
     /* --- Source provider: import resolves from the embedder. --------- */
     eigs_set_source_provider(smoke_provider, NULL);
     r = eigs_eval_string("import smokemod\nsmokemod[\"answer\"]");

src/main.c

@@ -187,10 +187,9 @@ int main(int argc, char **argv) {
         argc -= 2;
     }
 
-    trace_init();
-    atexit(trace_shutdown);
-
-    /* --version doesn't touch the runtime; handle it before any state. */
+    /* --version doesn't touch the runtime; handle it before any state —
+     * including trace_init: a stale EIGS_REPLAY in the environment is a
+     * fatal header check (#411) and must not take down pure queries. */
     if (argc >= 2 && (strcmp(argv[1], "--version") == 0 || strcmp(argv[1], "-v") == 0)) {
         printf("%s\n", EIGENSCRIPT_VERSION);
         return 0;
@@ -222,6 +221,9 @@ int main(int argc, char **argv) {
         return 0;
     }
 
+    trace_init();
+    atexit(trace_shutdown);
+
     /* --fmt is a pure source transformer; no VM, no arena, no state. */
     if (argc >= 2 && strcmp(argv[1], "--fmt") == 0) {
         if (argc < 3) {