JS-SAM follow-ups: broader traces, 4-model comparison, shared agent translator

config/models.yaml

@@ -35,6 +35,35 @@ models:
     # prior run's cap and stay within non-streaming timeout limits.
     max_tokens: 64000
 
+  # Sibling Claude tiers for cross-model comparison (same ANTHROPIC_API_KEY).
+  # Sonnet 4.6 rejects temperature AND top_p together, so set only temperature;
+  # both tiers still accept sampling params (unlike Opus 4.7+), so they are kept.
+  sonnet:
+    provider: "anthropic"
+    model_name: "claude-sonnet-4-6"
+    api_key_env: "ANTHROPIC_API_KEY"
+    temperature: 0.1
+    max_tokens: 64000
+
+  haiku:
+    provider: "anthropic"
+    model_name: "claude-haiku-4-5"
+    api_key_env: "ANTHROPIC_API_KEY"
+    temperature: 0.1
+    max_tokens: 64000
+
+  # Claude Fable 5 — Anthropic's most capable model. Sampling params
+  # (temperature/top_p/top_k) are removed (dropped by the adapter's
+  # _should_omit_sampling_params) and thinking is always on (no thinking config
+  # is sent). 128K max output; kept at 64000 for non-streaming. Fable reasons
+  # heavily per request, so allow a long timeout.
+  fable:
+    provider: "anthropic"
+    model_name: "claude-fable-5"
+    api_key_env: "ANTHROPIC_API_KEY"
+    max_tokens: 64000
+    timeout: 1800
+
   deepseek_tencent:
     provider: "deepseek"
     url: "https://api.lkeap.cloud.tencent.com/v1"

data/patches/spin_2thread_ktest.patch

@@ -1,6 +1,6 @@
 --- a/ostd/src/sync/spin_trace_tests.rs
 +++ b/ostd/src/sync/spin_trace_tests.rs
-@@ -98,7 +98,35 @@
+@@ -98,7 +98,73 @@
          crate::early_println!("Expected trace count: 18 events");
          crate::early_println!("- 6 tests × 3 events each (TryAcquire + Success + Release) = 18 total");
      }
@@ -33,11 +33,49 @@
 +
 +        crate::early_println!("=== 2-Thread SpinLock Trace Complete ===");
 +    }
++
++    /// Longer 2-actor sequence for broader Phase-3 coverage: alternating
++    /// holders, try_lock successes, and repeated failed contention. Still
++    /// single-CPU-safe (contention only ever via non-blocking try_lock).
++    #[ktest]
++    fn test_spin_seq() {
++        crate::early_println!("=== Spin Sequence Trace Start ===");
++        let lock = Arc::new(SpinTrace::<u32, PreemptDisabled>::new(0));
++
++        // Round 1: 0 holds (blocking), 1 fails, 0 releases.
++        let g = lock.lock_with_thread_id(0);
++        assert!(lock.try_lock_with_thread_id(1).is_none());
++        drop(g);
++        // Round 2: 1 holds (blocking), 0 fails, 1 releases.
++        let g = lock.lock_with_thread_id(1);
++        assert!(lock.try_lock_with_thread_id(0).is_none());
++        drop(g);
++        // Round 3: 0 acquires via try from free, releases.
++        let g = lock.try_lock_with_thread_id(0).expect("free");
++        drop(g);
++        // Round 4: 1 acquires via try from free, releases.
++        let g = lock.try_lock_with_thread_id(1).expect("free");
++        drop(g);
++        // Round 5: uncontended back-to-back blocking acquires by each actor.
++        let g = lock.lock_with_thread_id(0);
++        drop(g);
++        let g = lock.lock_with_thread_id(1);
++        drop(g);
++        // Round 6: 0 holds, 1 fails twice, 0 releases, 1 acquires, releases.
++        let g = lock.lock_with_thread_id(0);
++        assert!(lock.try_lock_with_thread_id(1).is_none());
++        assert!(lock.try_lock_with_thread_id(1).is_none());
++        drop(g);
++        let g = lock.lock_with_thread_id(1);
++        drop(g);
++
++        crate::early_println!("=== Spin Sequence Trace Complete ===");
++    }
 +
      #[ktest]
      fn test_tla_trace_simple() {
          crate::early_println!("=== TLA+ SpinLock Randomized Trace Test Start ===");
-@@ -212,4 +240,4 @@
+@@ -212,4 +278,4 @@
              _ => unreachable!(),
          }
      }

data/sys_traces/spin/spin_seq.ndjson

@@ -0,0 +1,20 @@
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "try"}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "ReleaseLock", "data": {"thread": 0}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "try"}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "ReleaseLock", "data": {"thread": 1}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "try"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "ReleaseLock", "data": {"thread": 0}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "try"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "ReleaseLock", "data": {"thread": 1}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "ReleaseLock", "data": {"thread": 0}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "ReleaseLock", "data": {"thread": 1}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 0, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "try"}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "try"}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": true, "lockHolder": 0}}
+{"action": "ReleaseLock", "data": {"thread": 0}, "pre_state": {"lockHeld": true, "lockHolder": 0}, "post_state": {"lockHeld": false, "lockHolder": null}}
+{"action": "AcquireLock", "data": {"thread": 1, "callType": "lock"}, "pre_state": {"lockHeld": false, "lockHolder": null}, "post_state": {"lockHeld": true, "lockHolder": 1}}
+{"action": "ReleaseLock", "data": {"thread": 1}, "pre_state": {"lockHeld": true, "lockHolder": 1}, "post_state": {"lockHeld": false, "lockHolder": null}}

docs/js_sam_model_comparison.md

@@ -0,0 +1,61 @@
+# JS-SAM Multi-Model Comparison — `spin`
+
+**Task:** `spin` (Asterinas spinlock) · **Backend:** JS-SAM · **Method:** `direct_call`
+**Date:** 2026-07-01 · Trace corpus: 28 windows (2 scenarios, real kernel capture)
+
+Four Claude models generated a JS-SAM `spin` specification and were scored across
+all four phases against the **same** 28-window transition-validation corpus.
+
+| Model | P1 syntax | P2 runtime (states) | P3 transition | P4 invariants |
+|---|---|---|---|---|
+| Claude Opus 4.8   | PASS | PASS (326,592) | **89.3% (25/28)** — Acquire 88%, Release 100% | 3/3 |
+| Claude Fable 5    | PASS | PASS (326,592) | **50.0% (14/28)** — Acquire 82%, **Release 0%** | 3/3 |
+| Claude Sonnet 4.6 | PASS | PASS (326,592) | **50.0% (14/28)** | 3/3 |
+| Claude Haiku 4.5  | PASS | PASS (326,592) | **21.4% (6/28)**  | 3/3 |
+
+## Finding
+
+**Transition validation is the discriminating phase.** Every model passes syntax
+(Phase 1), bounded model checking (Phase 2), and invariant verification (Phase 4)
+— those phases do not separate the models on this task. Only Phase 3, which
+replays real Asterinas spinlock transitions against each generated model, spreads
+them out:
+
+> Opus 4.8 (89.3%) ≫ Fable 5 = Sonnet 4.6 (50.0%) ≫ Haiku 4.5 (21.4%)
+
+This confirms that, for JS-SAM on `spin`, the signal lives in whether the
+generated model reproduces the **real system's behavior** — not in whether it
+parses, explores cleanly, or satisfies invariants (which even the weakest model
+achieves).
+
+### General capability does not predict spec-modeling accuracy
+
+The most striking result is **Claude Fable 5** — Anthropic's most capable model —
+scoring only 50.0%, *below* Opus 4.8 and tied with the mid-tier Sonnet. The
+cause is specific and systematic, not noise: Fable's model handles acquisition
+reasonably (82.4%) but **no-ops every `ReleaseLock`** (0 of 11). After a release,
+its model leaves the lock held (`lockHeld` stays `true`, the holder is not
+cleared), so every release transition diverges from the real system:
+
+```
+ReleaseLock  expected {lockHeld: false, lockHolder: null}
+             got      {lockHeld: true,  lockHolder: 0}
+```
+
+Its release *logic* reads correctly in isolation (guard on holder, then clear
+state), but in practice the release never takes effect on replay — a categorical
+modeling defect in one action. That a top-capability model can produce a spec
+with a whole-action bug, while passing Phases 1/2/4, is exactly the kind of
+signal transition validation exists to surface: **benchmark capability rankings
+do not automatically transfer to formal-modeling accuracy.**
+
+## Notes
+
+- All runs use `direct_call` and the same 28-window corpus
+  (`data/sys_traces/spin/*.ndjson`, captured via `scripts/harness/spin/run.sh`).
+- The recurring Opus failures are the `try_lock`-from-free transitions described
+  in `docs/js_sam_first_experiment.md` §6 (3 of 28 windows).
+- Model entries: `claude` (Opus 4.8), `fable` (Fable 5), `sonnet` (Sonnet 4.6),
+  `haiku` (Haiku 4.5) in `config/models.yaml`, all via `ANTHROPIC_API_KEY`.
+  Fable 5 sends no sampling params or thinking config (both removed on that
+  model); the adapter's `_should_omit_sampling_params` covers it.

scripts/harness/spin/build_and_test.sh

@@ -10,6 +10,8 @@
 #   {"seq":N,"thread":T,"lock":0,"state":"locked|unlocked","action":A,"actor":T}
 # which scripts/harness/spin/parse_traces.py folds into NDJSON windows.
 set -e
+# $1 = ktest name to run (default: test_spin_2thread)
+KTEST="${1:-test_spin_2thread}"
 export PATH=/nix/store/4zpvbvn0cvmmn9k05b1qgr5xh7i6r9ka-nix-2.31.1/bin:$PATH
 echo 'connect-timeout = 60000' >> /etc/nix/nix.conf
 
@@ -26,8 +28,8 @@ echo "===== installing cargo-osdk ====="
 OSDK_LOCAL_DEV=1 cargo install cargo-osdk --path osdk --locked
 echo "===== make initramfs ====="
 make initramfs
-echo "===== cargo osdk test (test_spin_2thread) ====="
+echo "===== cargo osdk test ($KTEST) ====="
 cd ostd
 timeout 1200 cargo osdk test --features tla-trace --target-arch x86_64 \
-  --qemu-args='-accel tcg' test_spin_2thread 2>&1
+  --qemu-args='-accel tcg' "$KTEST" 2>&1
 echo "===== DONE rc=$? ====="

scripts/harness/spin/run.sh

@@ -45,20 +45,30 @@ if [ ! -e "$SRC/ostd/src/sync/spin_trace.rs" ]; then
   tr -d '\r' < "$ADD_PATCH" | git -C "$SRC" apply --whitespace=nowarn
 fi
 
-# 3. Build + run under QEMU, capturing serial output. Source is read-only; the
-# build happens on the ext4 volume `spin-work`; cargo cache on `spin-cargo`.
-echo "[run.sh] building + running test_spin_2thread under QEMU (see $LOG)" >&2
-docker run --rm --privileged \
-  -v "$SRC:/src:ro" \
-  -v "$SCRIPT_DIR:/harness:ro" \
-  -v "spin-work:/build" \
-  -v "spin-cargo:/root/.cargo" \
-  "$IMAGE" bash /harness/build_and_test.sh > "$LOG" 2>&1 || {
-    echo "[run.sh] docker run failed; tail of $LOG:" >&2
-    tail -40 "$LOG" >&2
-    exit 1
-  }
-
-# 4. Parse serial JSON -> NDJSON windows.
-python3 "$SCRIPT_DIR/parse_traces.py" "$LOG" "$TRACES_OUT"
-echo "[run.sh] traces written to $TRACES_OUT" >&2
+# 3-4. For each scenario: build + run the ktest under QEMU (source read-only,
+# build on the ext4 `spin-work` volume, cargo cache on `spin-cargo`), capture
+# serial output, and parse it into an NDJSON trace file. trace_loader.py loads
+# every *.ndjson under data/sys_traces/spin, so more scenarios = broader Phase-3
+# coverage. Format: "<ktest name>:<output file>".
+SCENARIOS=(
+  "test_spin_2thread:spin_2thread.ndjson"
+  "test_spin_seq:spin_seq.ndjson"
+)
+TRACES_DIR="$(dirname "$TRACES_OUT")"
+mkdir -p "$TRACES_DIR"
+for entry in "${SCENARIOS[@]}"; do
+  ktest="${entry%%:*}"; outfile="${entry##*:}"
+  echo "[run.sh] building + running $ktest under QEMU (see $LOG)" >&2
+  docker run --rm --privileged \
+    -v "$SRC:/src:ro" \
+    -v "$SCRIPT_DIR:/harness:ro" \
+    -v "spin-work:/build" \
+    -v "spin-cargo:/root/.cargo" \
+    "$IMAGE" bash /harness/build_and_test.sh "$ktest" > "$LOG" 2>&1 || {
+      echo "[run.sh] docker run failed for $ktest; tail of $LOG:" >&2
+      tail -40 "$LOG" >&2
+      exit 1
+    }
+  python3 "$SCRIPT_DIR/parse_traces.py" "$LOG" "$TRACES_DIR/$outfile"
+done
+echo "[run.sh] traces written to $TRACES_DIR" >&2

tests/test_evaluation/test_agent_translation.py

@@ -0,0 +1,90 @@
+"""Unit tests for the shared, language-neutral agent-translation core.
+
+The real path shells out to the claude-code / codex CLI; these tests mock that
+subprocess boundary so routing, workspace setup, and output handling are
+verified without a live agent.
+"""
+
+import json
+from pathlib import Path
+
+from tla_eval.evaluation.semantics.agent_translation import (
+    run_agent_translation,
+    select_agent_cli,
+)
+
+
+def test_select_agent_cli_routing():
+    for claude in ("sonnet", "opus", "haiku", "claude-opus-4-8", "", "default"):
+        assert select_agent_cli(claude) == "claude"
+    for codex in ("codex", "gpt-5", "o4-mini"):
+        assert select_agent_cli(codex) == "codex"
+
+
+def test_run_agent_translation_success(monkeypatch):
+    async def fake_exec(workspace_path, model_name, agent_cli, timeout):
+        ws = Path(workspace_path)
+        # Instructions + caller-supplied files landed in the workspace.
+        assert (ws / "CLAUDE.md").read_text() == "do it"
+        assert (ws / "specification.tla").read_text() == "MODULE X"
+        out = ws / "output" / "invariants.json"
+        out.parent.mkdir(parents=True, exist_ok=True)
+        out.write_text('{"invariants": []}', encoding="utf-8")
+        return {"success": True}
+
+    monkeypatch.setattr(
+        "tla_eval.evaluation.semantics.agent_translation._execute_agent_cli", fake_exec
+    )
+    ok, content, err = run_agent_translation(
+        instructions="do it",
+        extra_files={"specification.tla": "MODULE X"},
+        model_name="sonnet",
+        timeout=5,
+    )
+    assert ok and err is None
+    assert json.loads(content) == {"invariants": []}
+
+
+def test_run_agent_translation_missing_output(monkeypatch):
+    async def fake_exec(workspace_path, model_name, agent_cli, timeout):
+        return {"success": True}  # reports success but writes nothing
+
+    monkeypatch.setattr(
+        "tla_eval.evaluation.semantics.agent_translation._execute_agent_cli", fake_exec
+    )
+    ok, content, err = run_agent_translation(
+        instructions="x", extra_files={}, model_name="sonnet", timeout=5
+    )
+    assert not ok and content is None and "did not produce" in err
+
+
+def test_run_agent_translation_cli_failure(monkeypatch):
+    async def fake_exec(workspace_path, model_name, agent_cli, timeout):
+        return {"success": False, "error": "CLI not found"}
+
+    monkeypatch.setattr(
+        "tla_eval.evaluation.semantics.agent_translation._execute_agent_cli", fake_exec
+    )
+    ok, content, err = run_agent_translation(
+        instructions="x", extra_files={}, model_name="sonnet", timeout=5
+    )
+    assert not ok and content is None and err == "CLI not found"
+
+
+def test_run_agent_translation_uses_codex_md(monkeypatch):
+    async def fake_exec(workspace_path, model_name, agent_cli, timeout):
+        ws = Path(workspace_path)
+        assert agent_cli == "codex"
+        assert (ws / "CODEX.md").exists() and not (ws / "CLAUDE.md").exists()
+        out = ws / "output" / "invariants.json"
+        out.parent.mkdir(parents=True, exist_ok=True)
+        out.write_text("{}", encoding="utf-8")
+        return {"success": True}
+
+    monkeypatch.setattr(
+        "tla_eval.evaluation.semantics.agent_translation._execute_agent_cli", fake_exec
+    )
+    ok, _content, err = run_agent_translation(
+        instructions="x", extra_files={}, model_name="codex", timeout=5
+    )
+    assert ok and err is None

tests/test_languages/test_js_sam.py

@@ -246,3 +246,33 @@ def test_unknown_translator_unsupported(self):
         )
         assert translated == {}
         assert error
+
+    def test_agent_translator_routes_to_shared_core(self):
+        # claude-code / codex route through the shared agent_translation core
+        # instead of the direct API call. Mock the core (no CLI required).
+        from unittest import mock
+
+        backend = JsSamBackend()
+        captured = {}
+
+        def fake_run(**kwargs):
+            captured.update(kwargs)
+            return (
+                True,
+                '{"invariants":[{"name":"MutualExclusion","predicate":"(s)=>true"}]}',
+                None,
+            )
+
+        with mock.patch(
+            "tla_eval.evaluation.semantics.agent_translation.run_agent_translation",
+            side_effect=fake_run,
+        ):
+            translated, error = backend.translate_invariants(
+                self._templates(), "module.exports = {}", "spin",
+                translator="claude-code",
+            )
+        assert error is None
+        assert translated == {"MutualExclusion": "(s)=>true"}
+        # It fed the generated spec to the agent and picked the claude CLI code.
+        assert "specification.js" in captured["extra_files"]
+        assert captured["model_name"] == "sonnet"