JS-SAM: cross-platform sandbox, Opus 4.8, and real Phase-3 spin traces

[jdubray]

Summary

Follow-up to the JS-SAM backend: makes it runnable on a Windows host, refreshes
the default Claude model, fixes two display/reporting defects, and — the main
addition — stands up the Phase 3 (transition validation) trace-capture
harness for spin, enabling the first complete four-phase JS-SAM run.

With these changes, spin / JS-SAM / Claude Opus 4.8 scores across all four
phases:

Phase	Result
1 compilation_check	PASS (0 errors)
2 runtime_check	PASS (326,592 states, depthMax 6)
3 transition_validation	PASS — 87.5% (7/8) against real kernel traces
4 invariant_verification	PASS (3/3)

The one Phase-3 failure is diagnostic: the generated model reproduces blocking
lock() acquisitions but its try_lock acquire never actually takes the lock —
caught only by replaying against transitions captured from the real Asterinas
spinlock.

Changes

• js_sam: cross-platform Docker sandbox. _run_helper was POSIX-only
  (os.getuid, host-path mounts). Now uses fixed container mount points
  (/opt/js-sam, /work), forward-slash -v sources, a specPath rewrite, and
  a hasattr(os, "getuid")-guarded --user. Linux/macOS behavior unchanged;
  runs on Windows/Docker Desktop.
• Model refresh. claude → claude-opus-4-8 (Sonnet 4 retired 2026-06-15);
  new _should_omit_sampling_params() drops temperature/top_p/top_k for
  models that 400 on them (Opus 4.7+, Fable 5, Mythos 5) — LiteLLM drop_params
  doesn't yet cover them.
• UTF-8 console output. Result summaries printed ✓/✗ and crashed on a
  Windows cp1252 console after a successful eval; std streams are reconfigured to
  UTF-8.
• states_explored for non-TLA+ backends. Was hardcoded 0 even though the
  JS-SAM helper reports stepsExplored; now threaded through
  ModelCheckOutcome, and the invariant evaluator's top-level field (previously
  0 for all backends) is populated.
• Spin Phase-3 trace harness (scripts/harness/spin/*,
  data/patches/spin_2thread_ktest.patch, data/sys_traces/spin/*). Clones
  Asterinas v0.16.0 (the patch doesn't apply to main), applies the reference
  instrumentation + a new 2-actor test_spin_2thread ktest (try_lock
  avoids single-CPU deadlock; the reference tests are single-actor), builds and
  runs it under QEMU-TCG on an ext4 docker volume, and folds the kernel serial
  JSON into JS-SAM (pre,post) windows keyed on the objective
  {lockHeld, lockHolder} state.

Notes

• docs/js_sam_first_experiment.md is a full write-up (method, capture
  pipeline, results, limitations, reproduction).
• The captured NDJSON is checked in for convenience; the harness regenerates it
  (scripts/harness/spin/run.sh). The large Asterinas clone stays gitignored.
• Requires the node:20-slim and asterinas/asterinas:0.16.0-20250822 images.

🤖 Generated with Claude Code

[Qian-Cheng-nju]

Reviewed the diff end-to-end — no correctness bugs. I confirmed the parse_traces.py regex and action names (TryAcquireBlocking/AcquireSuccess/AcquireFail/StopSpinning/Release) match what the reference spin_trace.rs instrumentation actually emits, folded the 10 ktest events by hand and got the same 8 windows as the checked-in spin_2thread.ndjson, and verified the states_explored threading is consistent across ModelCheckOutcome / runtime_check / the invariant evaluator. Two minor harness-robustness nits inline; both are non-blocking.

[Qian-Cheng-nju]

Small robustness nit on this idempotency guard. The script runs under set -euo pipefail, so if the reference patch applies (creating spin_trace.rs) but the second git apply below fails, the checkout is left half-patched. On the next run this guard sees spin_trace.rs already exists and skips the whole clone+patch block — so test_spin_2thread never gets added, and build_and_test.sh then runs cargo osdk test test_spin_2thread against a test that isn't there. Recovering needs a manual rm -rf "$SRC".

Consider keying the guard on a sentinel written only after both patches succeed, or doing rm -rf "$SRC" on any failure, so a partial apply self-heals on re-run.

[Qian-Cheng-nju]

rc=$? here can't actually report a failing test. With set -e at the top, a non-zero exit from the cargo osdk test call above aborts the script before this echo runs; when the echo is reached, $? is the exit status of the preceding successful command (0). So this line always prints rc=0.

Not harmful in practice — run.sh still catches the non-zero container exit via its || { …; exit 1; } — but the DONE line is misleading. To make it reflect the real result, capture it explicitly, e.g. run the test with set +e around it and rc=$?; echo "===== DONE rc=$rc =====".