diff --git a/specs/sessions/pmodel/.gitignore b/specs/sessions/pmodel/.gitignore
new file mode 100644
index 00000000..8e5ee8ff
--- /dev/null
+++ b/specs/sessions/pmodel/.gitignore
@@ -0,0 +1,3 @@
+# P compiler / checker outputs
+PGenerated/
+PCheckerOutput/
diff --git a/specs/sessions/pmodel/Dockerfile b/specs/sessions/pmodel/Dockerfile
new file mode 100644
index 00000000..4f492c66
--- /dev/null
+++ b/specs/sessions/pmodel/Dockerfile
@@ -0,0 +1,79 @@
+# syntax=docker/dockerfile:1
+
+# ---------------------------------------------------------------------------
+# Official P toolchain image.
+#
+# Bundles everything needed to compile and check P programs:
+# - .NET SDK 8.0 (the P compiler / PChecker are implemented in C#)
+# - JDK 17 + Maven (the PEx / PSym checker backends run on the JVM; the P
+# Java sources target Java 17 -- see Src/PEx/pom.xml)
+# - graphviz (used to render coverage / state-machine diagrams)
+# - the `p` CLI (built from this repository and installed as a global
+# dotnet tool)
+#
+# Build: docker build -t p .
+# Run: docker run --rm -it -v "$PWD":/workspace p
+# ---------------------------------------------------------------------------
+
+# --- Stage 1: build the P tool from the repository source ------------------
+FROM mcr.microsoft.com/dotnet/sdk:8.0 AS build
+
+# The P compiler build runs the ANTLR4 code generator, which shells out to
+# `java`, so a JDK is required even just to `dotnet pack` the tool.
+RUN apt-get update \
+ && apt-get install -y --no-install-recommends openjdk-17-jdk-headless \
+ && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /src
+COPY . .
+
+# Pack the `p` command-line tool into a local NuGet package. This mirrors the
+# `dotnet pack` step used by the release workflow; the resulting .nupkg lands
+# under Bld/Drops/Release/Binaries/ (see Directory.Build.props).
+RUN dotnet pack Src/PCompiler/PCommandLine/PCommandLine.csproj -c Release \
+ && mkdir -p /nupkg \
+ && cp Bld/Drops/Release/Binaries/[Pp].*.nupkg /nupkg/
+
+# --- Stage 2: the toolchain image ------------------------------------------
+FROM mcr.microsoft.com/dotnet/sdk:8.0
+
+LABEL org.opencontainers.image.title="P" \
+ org.opencontainers.image.description="Toolchain image for the P formal modeling language (P compiler, PChecker, PEx). Includes .NET 8, JDK 17, Maven and graphviz." \
+ org.opencontainers.image.source="https://github.com/p-org/P" \
+ org.opencontainers.image.documentation="https://p-org.github.io/P/" \
+ org.opencontainers.image.licenses="MIT"
+
+# Install the JVM toolchain (PEx/PSym backends) and graphviz. openjdk-17 is
+# available for both amd64 and arm64 in the Debian repositories used by the
+# .NET SDK base image, so this image builds natively on both architectures.
+RUN apt-get update \
+ && apt-get install -y --no-install-recommends \
+ openjdk-17-jdk-headless \
+ maven \
+ graphviz \
+ && rm -rf /var/lib/apt/lists/*
+
+# The JDK install path is arch-specific in the Debian layout
+# (java-17-openjdk-amd64 vs -arm64), so point a stable symlink at whichever
+# one this build produced and set JAVA_HOME to that fixed location. This keeps
+# JAVA_HOME identical and correct on both amd64 and arm64.
+RUN JAVA_BIN="$(readlink -f "$(command -v java)")" \
+ && JAVA_DIR="$(dirname "$(dirname "$JAVA_BIN")")" \
+ && ln -s "$JAVA_DIR" /usr/lib/jvm/default-jdk
+ENV JAVA_HOME=/usr/lib/jvm/default-jdk
+
+# Install the `p` tool built in stage 1 from the local package source.
+COPY --from=build /nupkg /tmp/nupkg
+RUN dotnet tool install --global --add-source /tmp/nupkg P \
+ && rm -rf /tmp/nupkg
+ENV PATH="${PATH}:/root/.dotnet/tools"
+
+# Also expose the tools directory to login shells (which re-source
+# /etc/profile and would otherwise drop the ENV above).
+RUN echo 'export PATH="$PATH:/root/.dotnet/tools"' > /etc/profile.d/dotnet-tools.sh
+
+# Sanity check: fail the build if the CLI is not runnable.
+RUN p --help > /dev/null
+
+WORKDIR /workspace
+CMD ["bash"]
diff --git a/specs/sessions/pmodel/OpenJDSessions.pproj b/specs/sessions/pmodel/OpenJDSessions.pproj
new file mode 100644
index 00000000..0dc71488
--- /dev/null
+++ b/specs/sessions/pmodel/OpenJDSessions.pproj
@@ -0,0 +1,10 @@
+
+
+ OpenJDSessions
+
+ PSrc
+ PSpec
+ PTst
+
+ PGenerated
+
diff --git a/specs/sessions/pmodel/PSpec/ActionLivenessSpec.p b/specs/sessions/pmodel/PSpec/ActionLivenessSpec.p
new file mode 100644
index 00000000..e9bfa38a
--- /dev/null
+++ b/specs/sessions/pmodel/PSpec/ActionLivenessSpec.p
@@ -0,0 +1,23 @@
+/*****************************************************************************
+ * ActionLivenessSpec.p — every started action eventually terminates
+ * (specs/sessions/session.md: no recovery path; subprocess always exits via
+ * normal exit, timeout→SIGKILL, or cancel→grace→SIGKILL).
+ *
+ * Liveness: whenever an action is Running (Busy), the system must eventually
+ * reach a state where no action is Running (Idle).
+ *****************************************************************************/
+
+spec ActionLivenessSpec observes eMonActionStart, eMonActionEnd {
+ start state Idle {
+ on eMonActionStart goto Busy;
+ // A spurious end without a start is caught by SessionStateSpec.
+ ignore eMonActionEnd;
+ }
+
+ hot state Busy {
+ on eMonActionEnd goto Idle;
+ // Nested starts can't happen (SessionStateSpec enforces ≤1); ignore
+ // defensively so this spec stays focused on the liveness question.
+ ignore eMonActionStart;
+ }
+}
diff --git a/specs/sessions/pmodel/PSpec/CancelDeliverySpec.p b/specs/sessions/pmodel/PSpec/CancelDeliverySpec.p
new file mode 100644
index 00000000..6f30558d
--- /dev/null
+++ b/specs/sessions/pmodel/PSpec/CancelDeliverySpec.p
@@ -0,0 +1,48 @@
+/*****************************************************************************
+ * CancelDeliverySpec.p — a cancel that is issued must actually take effect.
+ *
+ * Invariant: if a cancel is issued for the currently-running action (via ANY
+ * delivery channel — cancel_action, a malformed directive, OR an external
+ * SessionConfig.cancel_token cascade), then that action MUST NOT complete
+ * Successfully. It must end Canceled, Failed (e.g. mark_action_failed), or
+ * Timeout. In other words, an acknowledged cancel is never silently dropped.
+ *
+ * This is exactly the guarantee the same-user path provides (its subprocess
+ * loop awaits the CancellationToken directly, so a cancel over either the
+ * watch channel or the token is observed). It is the guarantee the CROSS-USER
+ * path currently BREAKS: run_via_helper only observes cancels that arrive over
+ * the watch/pipe channel, so a token-only external cancel (viaWatch = false)
+ * is not seen and the action can run to a Success/Failed exit as if no cancel
+ * happened. Model-checking tcWorkerAgentCrossUser against this spec fails on
+ * the current (buggy) routing and passes once the cross-user path also honours
+ * a token-delivered cancel.
+ *****************************************************************************/
+
+spec CancelDeliverySpec observes eMonActionStart, eMonCancelIssued, eMonActionEnd {
+ var canceled: bool; // a cancel was issued for the in-flight action
+
+ start state Idle {
+ on eMonActionStart goto Active;
+ ignore eMonCancelIssued, eMonActionEnd;
+ }
+
+ state Active {
+ entry { canceled = false; }
+
+ on eMonCancelIssued do (m: (actionId: tActionId, viaWatch: bool)) {
+ canceled = true;
+ }
+
+ on eMonActionEnd do (m: (actionId: tActionId, st: tActionState)) {
+ if (canceled) {
+ assert m.st != ACT_SUCCESS,
+ format ("Action {0} was canceled but completed Successfully — the cancel was dropped (cross-user token-only cancel not observed by run_via_helper?).", m.actionId);
+ }
+ goto Idle;
+ }
+
+ // Only one action runs at a time (SessionStateSpec enforces ≤1), so a
+ // second start here would be a bug in the harness; ignore defensively.
+ ignore eMonActionStart;
+ }
+}
diff --git a/specs/sessions/pmodel/PSpec/EnvStackSpec.p b/specs/sessions/pmodel/PSpec/EnvStackSpec.p
new file mode 100644
index 00000000..f98aec6d
--- /dev/null
+++ b/specs/sessions/pmodel/PSpec/EnvStackSpec.p
@@ -0,0 +1,47 @@
+/*****************************************************************************
+ * EnvStackSpec.p — environment LIFO + no-duplicate invariants
+ * (specs/sessions/session.md § Environment Management, § Why LIFO enforcement).
+ *
+ * Asserts:
+ * - environments are popped in strict LIFO order (last pushed = first popped)
+ * - no duplicate environment id is ever on the stack simultaneously
+ * - cleanup() with a non-empty stack is flagged (onExit scripts skipped)
+ *****************************************************************************/
+
+spec EnvStackSpec observes eMonEnter, eMonExit, eMonCleanup {
+ var stack: seq[tEnvId];
+
+ start state Watching {
+ entry { stack = default(seq[tEnvId]); }
+
+ on eMonEnter do (id: tEnvId) {
+ assert !contains(id), format ("Duplicate environment {0} pushed onto stack", id);
+ stack += (sizeof(stack), id);
+ }
+
+ on eMonExit do (id: tEnvId) {
+ assert sizeof(stack) > 0, "Exit with empty environment stack";
+ assert stack[sizeof(stack) - 1] == id,
+ format ("Non-LIFO exit: popped {0} but top is {1}", id, stack[sizeof(stack) - 1]);
+ stack -= (sizeof(stack) - 1);
+ }
+
+ on eMonCleanup do (depth: int) {
+ assert depth == sizeof(stack), "monitor/session stack depth diverged";
+ // Documented hazard, not a correctness bug in the model, but a
+ // well-formed driver should have exited everything first.
+ assert depth == 0,
+ format ("cleanup() called with {0} environment(s) still entered", depth);
+ }
+ }
+
+ fun contains(id: tEnvId): bool {
+ var i: int;
+ i = 0;
+ while (i < sizeof(stack)) {
+ if (stack[i] == id) { return true; }
+ i = i + 1;
+ }
+ return false;
+ }
+}
diff --git a/specs/sessions/pmodel/PSpec/MonitorEvents.p b/specs/sessions/pmodel/PSpec/MonitorEvents.p
new file mode 100644
index 00000000..8c7b6493
--- /dev/null
+++ b/specs/sessions/pmodel/PSpec/MonitorEvents.p
@@ -0,0 +1,16 @@
+/*****************************************************************************
+ * MonitorEvents.p — events announced by Session for the spec monitors.
+ * These carry no behavior; they let the monitors observe the abstract state.
+ *****************************************************************************/
+
+event eMonStateChanged : (fromState: tSessionState, toState: tSessionState);
+event eMonActionStart : (actionId: tActionId, kind: tActionKind);
+event eMonActionEnd : (actionId: tActionId, st: tActionState);
+event eMonEnter : tEnvId; // env pushed
+event eMonExit : tEnvId; // env popped
+event eMonCleanup : int; // stack depth at cleanup()
+event eMonHelperBadToken; // helper rejected a bad/missing token
+// A cancel was issued for the current action. viaWatch = travelled the watch/
+// pipe channel (cancel_action / malformed directive); false = token-only
+// (external SessionConfig.cancel_token cascade).
+event eMonCancelIssued : (actionId: tActionId, viaWatch: bool);
diff --git a/specs/sessions/pmodel/PSpec/SessionStateSpec.p b/specs/sessions/pmodel/PSpec/SessionStateSpec.p
new file mode 100644
index 00000000..d89063dc
--- /dev/null
+++ b/specs/sessions/pmodel/PSpec/SessionStateSpec.p
@@ -0,0 +1,66 @@
+/*****************************************************************************
+ * SessionStateSpec.p — the SessionState transition + brittle-session invariants
+ * (specs/sessions/session.md § Transitions, § Brittle Sessions).
+ *
+ * Asserts:
+ * - only documented transitions occur
+ * - Ended is terminal (no transition out)
+ * - at most one action Running at a time
+ * - after any Failed/Canceled/Timeout the session is ending-only: it may only
+ * reach Ready via S_READY_ENDING, never plain S_READY again
+ *****************************************************************************/
+
+spec SessionStateSpec observes eMonStateChanged, eMonActionStart, eMonActionEnd {
+ var actionsRunning: int; // must never exceed 1
+ var brittle: bool; // a terminal-failure action has occurred
+
+ start state Watching {
+ entry { actionsRunning = 0; brittle = false; }
+
+ on eMonStateChanged do (t: (fromState: tSessionState, toState: tSessionState)) {
+ assert validTransition(t.fromState, t.toState),
+ format ("Illegal SessionState transition {0} -> {1}", t.fromState, t.toState);
+
+ // Ended is terminal.
+ assert t.fromState != S_ENDED,
+ "SessionState left the terminal Ended state";
+
+ // Once brittle, the session must not return to plain Ready. The
+ // only allowed non-ending resting state after a failure is
+ // S_READY_ENDING (reached via ReadyEnding) or S_ENDED.
+ if (brittle) {
+ assert t.toState != S_READY,
+ "Brittle session transitioned back to Ready (should be ReadyEnding)";
+ }
+ }
+
+ on eMonActionStart do (m: (actionId: tActionId, kind: tActionKind)) {
+ actionsRunning = actionsRunning + 1;
+ assert actionsRunning <= 1,
+ format ("More than one action running concurrently ({0})", actionsRunning);
+ }
+
+ on eMonActionEnd do (m: (actionId: tActionId, st: tActionState)) {
+ actionsRunning = actionsRunning - 1;
+ assert actionsRunning >= 0, "action ended without a matching start";
+ if (m.st == ACT_FAILED || m.st == ACT_CANCELED || m.st == ACT_TIMEOUT) {
+ brittle = true;
+ }
+ }
+ }
+}
+
+/* The transition relation from specs/sessions/session.md § Transitions. */
+fun validTransition(fromS: tSessionState, toS: tSessionState): bool {
+ if (fromS == toS) { return true; } // announce fires even for no-op re-sets
+ // Ready → Running | Ended
+ if (fromS == S_READY) { return toS == S_RUNNING || toS == S_ENDED; }
+ // Running → Ready | ReadyEnding | Canceling
+ if (fromS == S_RUNNING) { return toS == S_READY || toS == S_READY_ENDING || toS == S_CANCELING; }
+ // Canceling → Ready | ReadyEnding
+ if (fromS == S_CANCELING) { return toS == S_READY || toS == S_READY_ENDING; }
+ // ReadyEnding → Running | Ended
+ if (fromS == S_READY_ENDING) { return toS == S_RUNNING || toS == S_ENDED; }
+ // Ended → (none)
+ return false;
+}
diff --git a/specs/sessions/pmodel/PSrc/CrossUserHelper.p b/specs/sessions/pmodel/PSrc/CrossUserHelper.p
new file mode 100644
index 00000000..16facc8a
--- /dev/null
+++ b/specs/sessions/pmodel/PSrc/CrossUserHelper.p
@@ -0,0 +1,102 @@
+/*****************************************************************************
+ * CrossUserHelper.p — persistent cross-user helper
+ * (specs/sessions/embedded-cross-user-helper.md).
+ *
+ * Models the security-relevant behavior only:
+ * - one command at a time (implicitly sequential protocol)
+ * - every command carries a token; verified for equality
+ * - bad/missing token ⇒ {"error":"invalid token"} AND the current run is
+ * left untouched (a bad-token cancel is NOT an unauthenticated cancel)
+ * - helper stays alive on bad token (log-and-ignore, not exit → no DoS)
+ *
+ * Token entropy, constant-time compare, JSON framing, poll(2), Job Objects,
+ * DACLs, and the reader-thread/channel are out of scope.
+ *****************************************************************************/
+
+machine CrossUserHelper {
+ var owner: machine; // the Session that spawned us
+ var token: tToken; // expected auth token (from --auth-token)
+ var runActionId: tActionId; // action currently running (-1 = idle)
+ var emitsLeft: int;
+
+ start state Init {
+ entry (cfg: (session: machine, token: tToken)) {
+ owner = cfg.session;
+ token = cfg.token;
+ runActionId = -1;
+ goto Idle;
+ }
+ }
+
+ state Idle {
+ ignore eTick; // a leftover tick from a prior run is harmless when idle
+
+ on eHelperRun do (r: tHelperRun) {
+ if (r.token != token) {
+ // invalid token: no child spawn, helper stays alive.
+ send r.session, eHelperInvalidToken;
+ announce eMonHelperBadToken;
+ return;
+ }
+ runActionId = r.actionId;
+ emitsLeft = choose(4);
+ send owner, eHelperPid, runActionId;
+ goto Running;
+ }
+
+ // A cancel/shutdown while idle: verify token, otherwise ignore.
+ on eHelperCancel do (c: tHelperCancel) {
+ if (c.token != token) { send owner, eHelperInvalidToken; announce eMonHelperBadToken; }
+ }
+ on eHelperShutdown do (s: (session: machine, token: tToken)) {
+ if (s.token == token) { raise halt; }
+ else { send s.session, eHelperInvalidToken; announce eMonHelperBadToken; }
+ }
+ }
+
+ state Running {
+ entry { send this, eTick; }
+
+ on eTick do {
+ if (emitsLeft > 0) {
+ emitsLeft = emitsLeft - 1;
+ send owner, eHelperOut, runActionId; // {"out": line}
+ send this, eTick; // yield so a cancel can interleave
+ } else {
+ // Child exits normally (Success/Failed decided by exit code).
+ if ($) { done(ACT_SUCCESS, 0); } else { done(ACT_FAILED, 1); }
+ }
+ }
+
+ on eHelperCancel do (c: tHelperCancel) {
+ if (c.token != token) {
+ // SECURITY INVARIANT: bad-token cancel must NOT stop the run.
+ send owner, eHelperInvalidToken;
+ announce eMonHelperBadToken;
+ return;
+ }
+ if (c.actionId != runActionId) { return; }
+ if (c.method == CM_TERMINATE) { done(ACT_CANCELED, -9); }
+ else {
+ // NotifyThenTerminate: exit during grace or get killed.
+ if ($) { done(ACT_CANCELED, 0); } else { done(ACT_CANCELED, -9); }
+ }
+ }
+
+ // Shutdown mid-run: valid token tears down the helper.
+ on eHelperShutdown do (s: (session: machine, token: tToken)) {
+ if (s.token == token) { raise halt; }
+ else { send s.session, eHelperInvalidToken; announce eMonHelperBadToken; }
+ }
+ }
+
+ fun done(finalSt: tActionState, code: tExitCode) {
+ // The helper reports {"exited": code}; the session maps this to a
+ // SubprocessResult and finalizes the action. We reuse eProcessExited
+ // so the Session state machine is agnostic to same-user vs cross-user.
+ send owner, eHelperExited, (actionId = runActionId, code = code);
+ send owner, eProcessExited, (actionId = runActionId, st = finalSt, code = code);
+ runActionId = -1;
+ goto Idle;
+ }
+}
diff --git a/specs/sessions/pmodel/PSrc/Events.p b/specs/sessions/pmodel/PSrc/Events.p
new file mode 100644
index 00000000..a2b1e5cc
--- /dev/null
+++ b/specs/sessions/pmodel/PSrc/Events.p
@@ -0,0 +1,145 @@
+/*****************************************************************************
+ * Events.p — Event and type declarations for the openjd-sessions model.
+ *
+ * Every event here abstracts a concrete interaction described in
+ * specs/sessions/*.md. Payloads carry only what the invariants need — no
+ * bytes, no real paths, no crypto. See README.md § "Out of scope".
+ *****************************************************************************/
+
+/* ---- Abstract identifiers -------------------------------------------------
+ * We model identifiers as ints. Environments and actions get fresh ids from
+ * the driver; tokens are abstract equality-only values.
+ */
+type tEnvId = int; // environment identifier on the LIFO stack
+type tActionId = int; // one per action instance (fresh each action)
+type tToken = int; // helper auth token — compared only for equality
+type tExitCode = int;
+
+/* ---- Action kinds ---------------------------------------------------------
+ * The four ways an action enters the Session: onEnter, onExit, onRun (task),
+ * and the ad-hoc run_subprocess path.
+ */
+enum tActionKind {
+ ENTER_ENV,
+ EXIT_ENV,
+ RUN_TASK,
+ RUN_SUBPROCESS
+}
+
+/* ---- ActionState (src/action_status.rs) -----------------------------------
+ * Terminal states: Success, Failed, Canceled, Timeout. Running is the only
+ * non-terminal state.
+ */
+enum tActionState {
+ ACT_RUNNING,
+ ACT_SUCCESS,
+ ACT_FAILED,
+ ACT_CANCELED,
+ ACT_TIMEOUT
+}
+
+/* ---- SessionState (src/session.rs) ---------------------------------------- */
+enum tSessionState {
+ S_READY,
+ S_RUNNING,
+ S_CANCELING,
+ S_READY_ENDING,
+ S_ENDED
+}
+
+/* ---- CancelMethod (runner/mod.rs) ----------------------------------------- */
+enum tCancelMethod {
+ CM_TERMINATE, // immediate kill
+ CM_NOTIFY_THEN_TERMINATE // SIGTERM, grace, then SIGKILL
+}
+
+/* ===========================================================================
+ * Client → Session : lifecycle commands (the public Session API).
+ * ===========================================================================
+ */
+
+// enter_environment(env, .., identifier, ..)
+type tEnterReq = (client: machine, envId: tEnvId);
+event eEnterEnv : tEnterReq;
+
+// exit_environment(identifier, .., keep_session_running, ..)
+type tExitReq = (client: machine, envId: tEnvId, keepRunning: bool);
+event eExitEnv : tExitReq;
+
+// run_task(script, ..) — task action. Payload: the client machine.
+// (P has no single-field named tuples, so single-value payloads are bare.)
+event eRunTask : machine;
+
+// run_subprocess(command, ..) — ad-hoc subprocess. Payload: client machine.
+event eRunSubprocess : machine;
+
+// cancel_action(time_limit, mark_action_failed). Payload: mark_action_failed.
+event eCancelAction : bool;
+
+// SessionConfig.cancel_token fired externally (permanent, cascades).
+event eSessionCancelToken;
+
+// cleanup(). Payload: client machine.
+event eCleanup : machine;
+
+/* Replies back to the client so a driver can sequence its next command. */
+event eActionDone : tActionState; // action completed (payload: final state)
+event eCmdRejected : tSessionState; // command refused (payload: rejecting state)
+event eCleanupDone;
+
+/* The Subprocess machine receives its action parameters via its constructor
+ * (see Subprocess.p `start state Init` entry), so there is no separate
+ * "start action" event on the same-user path. */
+
+/* ===========================================================================
+ * Subprocess / ActionFilter → Session : the ActionMessage enum
+ * (specs/sessions/action-messages.md).
+ *
+ * These are the openjd_* directives parsed from stdout, delivered in real
+ * time over the (unbounded) mpsc channel and applied with &mut self.
+ * ===========================================================================
+ */
+event eProgress : (actionId: tActionId, value: int); // openjd_progress
+event eStatus : tActionId; // openjd_status
+event eFail : tActionId; // openjd_fail
+event eSetEnv : (actionId: tActionId, envId: tEnvId, name: int); // openjd_env
+event eUnsetEnv : (actionId: tActionId, envId: tEnvId, name: int); // openjd_unset_env
+event eRedactedEnv : (actionId: tActionId, envId: tEnvId, name: int); // openjd_redacted_env
+event eCancelMarkFailed: tActionId; // malformed directive
+
+/* Subprocess lifecycle → Session. eProcessExited is the action_future
+ * completing; drive_action drains remaining messages before finalizing. */
+event eProcessExited : (actionId: tActionId, st: tActionState, code: tExitCode);
+
+/* Self-scheduled continuation "tick": lets a streaming machine yield between
+ * emitted lines so external events (a cancel) can interleave. Without this, a
+ * goto-loop would run to completion and no cancel could ever land mid-stream. */
+event eTick;
+
+/* ===========================================================================
+ * Session → Subprocess : cancellation / signals.
+ * ===========================================================================
+ */
+event eCancelRequest : (actionId: tActionId, method: tCancelMethod); // over watch channel
+event eGraceExpired : tActionId; // notify grace elapsed → SIGKILL
+event eExitGrace : tActionId; // 5s post-EOF grace → SIGKILL
+
+/* ===========================================================================
+ * Session ↔ CrossUserHelper : newline-delimited JSON wire protocol
+ * (specs/sessions/embedded-cross-user-helper.md). Every command carries a
+ * token; responses do not.
+ * ===========================================================================
+ */
+type tHelperRun = (session: machine, actionId: tActionId, token: tToken);
+type tHelperCancel = (actionId: tActionId, method: tCancelMethod, token: tToken);
+
+event eHelperRun : tHelperRun; // {"token","command","args","env","cwd"}
+event eHelperCancel : tHelperCancel; // {"token","cancel":...}
+event eHelperShutdown: (session: machine, token: tToken); // {"token","shutdown":true}
+
+// Responses (helper → session)
+event eHelperPid : tActionId;
+event eHelperOut : tActionId;
+event eHelperExited : (actionId: tActionId, code: tExitCode);
+event eHelperError : tActionId; // {"error": "..."}
+event eHelperInvalidToken; // {"error":"invalid token"} — run untouched
diff --git a/specs/sessions/pmodel/PSrc/Session.p b/specs/sessions/pmodel/PSrc/Session.p
new file mode 100644
index 00000000..44e8aa87
--- /dev/null
+++ b/specs/sessions/pmodel/PSrc/Session.p
@@ -0,0 +1,411 @@
+/*****************************************************************************
+ * Session.p — the SessionState machine (specs/sessions/session.md).
+ *
+ * Drives one action at a time, manages a LIFO environment stack and the
+ * cumulative env-var change set, and enforces the brittle-session contract.
+ * Announces monitor events so the specs in PSpec/ can check invariants.
+ *****************************************************************************/
+
+/* Config passed in by the driver at creation. */
+type tSessionConfig = (
+ crossUser: bool, // route actions through the cross-user helper
+ hasCancelToken: bool // whether SessionConfig.cancel_token is wired
+);
+
+/* Fault-injection knob for the cross-user token-cancel channel.
+ * true = the cross-user path observes a cancel delivered over EITHER the
+ * watch/pipe channel or the token. All test cases check green.
+ * false = the cross-user path observes a cancel ONLY over the watch/pipe
+ * channel, so a token-only external cancel is not seen and
+ * tcExternalCancelCrossUser fails CancelDeliverySpec.
+ * Exists so CancelDeliverySpec can be shown to have teeth (flip → red on the
+ * cross-user token-only path, green elsewhere). Keep true. */
+fun CROSS_USER_HONORS_TOKEN_CANCEL(): bool { return true; }
+
+/* Per-environment record: the set/unset env-var names contributed by that env
+ * (from `variables` + openjd_env/openjd_unset_env directives). Popping the env
+ * must remove exactly this contribution from the cumulative set. */
+type tEnvRecord = (envId: tEnvId, sets: set[int], unsets: set[int]);
+
+machine Session {
+ var sstate: tSessionState; // 'state' is a reserved word in P
+ var endingOnly: bool; // ReadyEnding "brittle" flag
+
+ // Environment LIFO stack (index 0 = bottom, last = top).
+ var stack: seq[tEnvRecord];
+
+ // Current action bookkeeping.
+ var nextActionId: tActionId;
+ var curActionId: tActionId;
+ var curKind: tActionKind;
+ var curState: tActionState;
+ var curClient: machine;
+ var curEnvId: tEnvId; // env being entered/exited (for env-var changes)
+ var curCancelMethod: tCancelMethod; // the action's configured cancel method
+ var cancelRequested: bool; // cancel_action or cancel-token seen for cur action
+ var markFailed: bool; // cancel_action(mark_action_failed = true)
+ // Whether the WORKER's cancel-detection channel actually observed a cancel
+ // for the current action. Same-user: true whenever any cancel is delivered
+ // (the subprocess awaits the sticky token). Cross-user: true only when the
+ // cancel reached the helper over the watch/pipe channel. This is what the
+ // code's terminal-state computation keys off (subprocess.rs is_cancelled /
+ // cross_user_helper.rs has_changed), so finalizeAction overlays Canceled
+ // from it rather than trusting the subprocess's natural exit.
+ var workerObservedCancel: bool;
+
+ // Permanent session-level cancel (SessionConfig.cancel_token). Once set it
+ // cascades to the current AND all future actions.
+ var sessionCanceled: bool;
+
+ // Cross-user helper wiring.
+ var crossUser: bool;
+ var helper: machine;
+ var token: tToken; // the helper's auth token (abstract)
+
+ var worker: machine; // the Subprocess machine driving cur action
+
+ start state Init {
+ entry (cfg: tSessionConfig) {
+ crossUser = cfg.crossUser;
+ nextActionId = 1;
+ sessionCanceled = false;
+ endingOnly = false;
+ if (crossUser) {
+ token = 42; // abstract, fixed for this session
+ helper = new CrossUserHelper((session = this, token = token));
+ }
+ setState(S_READY);
+ goto Ready;
+ }
+ }
+
+ /* ---- Ready / ReadyEnding -------------------------------------------------
+ * Ready and ReadyEnding share a state here; `endingOnly` distinguishes them.
+ * In ending-only mode, only exit_environment and cleanup are accepted.
+ */
+ state Ready {
+ on eEnterEnv do (req: tEnterReq) {
+ if (endingOnly) { reject(req.client); return; }
+ // Duplicate identifier rejection (spec: session.md).
+ if (envOnStack(req.envId)) { reject(req.client); return; }
+ curClient = req.client;
+ curEnvId = req.envId;
+ // Push the (empty) env record now; onEnter env-var changes fill it in.
+ stack += (sizeof(stack), (envId = req.envId, sets = default(set[int]),
+ unsets = default(set[int])));
+ announce eMonEnter, req.envId;
+ beginAction(ENTER_ENV, chooseCancelMethod());
+ }
+
+ on eExitEnv do (req: tExitReq) {
+ // Allowed in both Ready and ReadyEnding.
+ // LIFO enforcement: identifier must match top of stack.
+ if (sizeof(stack) == 0 || topEnv() != req.envId) { reject(req.client); return; }
+ if (!req.keepRunning) { endingOnly = true; }
+ curClient = req.client;
+ curEnvId = req.envId;
+ // The environment is removed from tracking BEFORE the onExit script
+ // runs: "a failed exit is still an exit," and later exits must
+ // proceed in LIFO order regardless of the onExit result.
+ popTop();
+ beginAction(EXIT_ENV, chooseCancelMethod());
+ }
+
+ on eRunTask do (client: machine) {
+ if (endingOnly) { reject(client); return; }
+ curClient = client;
+ curEnvId = -1;
+ beginAction(RUN_TASK, chooseCancelMethod());
+ }
+
+ on eRunSubprocess do (client: machine) {
+ if (endingOnly) { reject(client); return; }
+ curClient = client;
+ curEnvId = -1;
+ beginAction(RUN_SUBPROCESS, CM_TERMINATE); // ad-hoc always Terminate
+ }
+
+ on eCleanup do (client: machine) {
+ doCleanup(client);
+ }
+
+ // The permanent session cancel token can fire while idle; remember it.
+ on eSessionCancelToken do { sessionCanceled = true; }
+
+ // A stray cancel while idle is a no-op (SessionCancelHandle returns false).
+ on eCancelAction do (markFailedReq: bool) { /* no action running */ }
+ }
+
+ /* ---- Running -------------------------------------------------------------
+ * Exactly one action in flight. Process ActionMessages, handle cancel, and
+ * finalize on eProcessExited.
+ */
+ state Running {
+ // Real code awaits inside the action; a well-behaved driver issues no
+ // new lifecycle command until eActionDone. Defer any that race in.
+ defer eEnterEnv, eExitEnv, eRunTask, eRunSubprocess, eCleanup;
+ // Helper transport responses are logging/relay only; state changes come
+ // via eProcessExited (sent alongside eHelperExited).
+ ignore eHelperPid, eHelperOut, eHelperExited, eHelperInvalidToken;
+
+ on eProgress do (m: (actionId: tActionId, value: int)) {
+ if (m.actionId == curActionId) { /* update action_status.progress */ }
+ }
+ on eStatus do (aid: tActionId) { }
+ on eFail do (aid: tActionId) {
+ // openjd_fail records a fail_message ONLY; it does NOT cancel. The
+ // process runs to EOF and the result becomes Failed (unless a
+ // timeout/cancel supersedes). No state change here.
+ }
+ // openjd_env changes are folded into the cumulative set ONLY while
+ // entering an environment. Verified against session.rs: run_task /
+ // run_subprocess pass a fresh identifier that is NOT a key in
+ // created_env_vars, so apply_message's get_mut(identifier) returns None
+ // and the change is silently discarded; on exit the env is already
+ // removed from environments_entered, so its onExit changes are dropped
+ // from the fold too. Only ENTER_ENV attributes changes (to the env being
+ // entered, which is the current top of stack).
+ on eSetEnv do (m: (actionId: tActionId, envId: tEnvId, name: int)) {
+ if (curKind == ENTER_ENV) { applySet(m.name); }
+ }
+ on eUnsetEnv do (m: (actionId: tActionId, envId: tEnvId, name: int)) {
+ if (curKind == ENTER_ENV) { applyUnset(m.name); }
+ }
+ on eRedactedEnv do (m: (actionId: tActionId, envId: tEnvId, name: int)) {
+ if (curKind == ENTER_ENV) { applySet(m.name); } // SetEnv + redaction
+ }
+ on eCancelMarkFailed do (aid: tActionId) {
+ if (aid == curActionId) {
+ markFailed = true; cancelRequested = true;
+ // A malformed directive routes through cancel_action(None, true)
+ // (session.rs), which delivers the action's CONFIGURED cancel
+ // method — NOT an unconditional Terminate.
+ requestCancel(curCancelMethod);
+ goto Canceling;
+ }
+ }
+
+ on eCancelAction do (markFailedReq: bool) {
+ cancelRequested = true;
+ if (markFailedReq) { markFailed = true; }
+ requestCancel(chooseCancelMethod());
+ setState(S_CANCELING);
+ goto Canceling;
+ }
+
+ on eSessionCancelToken do {
+ sessionCanceled = true;
+ cancelRequested = true;
+ // External token cancel: token-only delivery (viaWatch = false).
+ deliverCancel(CM_TERMINATE, false);
+ setState(S_CANCELING);
+ goto Canceling;
+ }
+
+ on eProcessExited do (m: (actionId: tActionId, st: tActionState, code: tExitCode)) {
+ if (m.actionId == curActionId) { finalizeAction(m.st); }
+ }
+ }
+
+ /* ---- Canceling -----------------------------------------------------------
+ * Cancel requested; waiting for the subprocess to exit. Late ActionMessages
+ * are still drained (drive_action drains after exit).
+ */
+ state Canceling {
+ defer eEnterEnv, eExitEnv, eRunTask, eRunSubprocess, eCleanup;
+ ignore eProgress, eStatus, eSetEnv, eUnsetEnv, eRedactedEnv, eFail;
+ ignore eHelperPid, eHelperOut, eHelperExited, eHelperInvalidToken;
+
+ on eCancelAction do (markFailedReq: bool) { if (markFailedReq) { markFailed = true; } }
+ on eSessionCancelToken do { sessionCanceled = true; }
+ on eCancelMarkFailed do (aid: tActionId) { if (aid == curActionId) { markFailed = true; } }
+
+ on eProcessExited do (m: (actionId: tActionId, st: tActionState, code: tExitCode)) {
+ // finalizeAction applies the cancel overlay from session state
+ // (workerObservedCancel / markFailed), so both the Running and
+ // Canceling paths funnel through the same classification logic.
+ if (m.actionId == curActionId) { finalizeAction(m.st); }
+ }
+ }
+
+ /* ---- Ended (terminal) ---------------------------------------------------- */
+ state Ended {
+ ignore eProgress, eStatus, eFail, eSetEnv, eUnsetEnv, eRedactedEnv,
+ eCancelMarkFailed, eProcessExited, eCancelAction, eSessionCancelToken,
+ eHelperPid, eHelperOut, eHelperExited, eHelperInvalidToken;
+ on eEnterEnv do (req: tEnterReq) { reject(req.client); }
+ on eExitEnv do (req: tExitReq) { reject(req.client); }
+ on eRunTask do (client: machine) { reject(client); }
+ on eRunSubprocess do (client: machine) { reject(client); }
+ on eCleanup do (client: machine) { send client, eCleanupDone; }
+ }
+
+ /* ===================== helper functions ===================== */
+
+ fun beginAction(kind: tActionKind, cm: tCancelMethod) {
+ curActionId = nextActionId;
+ nextActionId = nextActionId + 1;
+ curKind = kind;
+ curCancelMethod = cm;
+ curState = ACT_RUNNING;
+ markFailed = false;
+ workerObservedCancel = false;
+ // Every action installs FRESH cancel state (session.md): a prior
+ // cancel_action never poisons a later action...
+ cancelRequested = false;
+ // ...but SessionConfig.cancel_token is permanent and cascades.
+ if (sessionCanceled) { cancelRequested = true; }
+
+ setState(S_RUNNING);
+ announce eMonActionStart, (actionId = curActionId, kind = kind);
+
+ if (crossUser) {
+ worker = helper; // helper owns the child; it will spawn/relay
+ send helper, eHelperRun, (session = this, actionId = curActionId, token = token);
+ } else {
+ worker = new Subprocess((
+ session = this, actionId = curActionId, kind = kind,
+ cancelMethod = cm, envId = curEnvId));
+ }
+ // SessionConfig.cancel_token is permanent: if it already fired, every
+ // future action's cancel token is born cancelled, so cascade now. This
+ // is a token-only cascade (viaWatch = false), like eSessionCancelToken.
+ if (sessionCanceled) {
+ deliverCancel(CM_TERMINATE, false);
+ setState(S_CANCELING);
+ goto Canceling;
+ }
+ goto Running;
+ }
+
+ // Cancellation is delivered over TWO channels:
+ // - the watch channel (cancel_request_rx), which the session mirrors onto
+ // the cross-user helper stdin via cancel_writer; AND
+ // - the per-action CancellationToken.
+ // cancel_action fires BOTH; a bare external SessionConfig.cancel_token cancel
+ // fires ONLY the token. The same-user subprocess awaits the token directly,
+ // so it observes a cancel from EITHER channel. The cross-user helper is
+ // driven by the pipe, so it observes the watch/pipe channel; whether it also
+ // honours the token is the CROSS_USER_HONORS_TOKEN_CANCEL knob.
+ //
+ // `viaWatch` = the cancel travelled the watch channel (true for cancel_action
+ // and malformed-directive cancels; false for a bare external token cancel).
+ fun requestCancel(cm: tCancelMethod) { deliverCancel(cm, true); }
+
+ fun deliverCancel(cm: tCancelMethod, viaWatch: bool) {
+ announce eMonCancelIssued, (actionId = curActionId, viaWatch = viaWatch);
+ if (crossUser) {
+ // The cross-user helper observes a cancel over the watch/pipe channel
+ // (viaWatch); it additionally honours a token-only cancel iff the
+ // knob is set. With the knob off, a token-only cancel is not observed
+ // and CancelDeliverySpec fails on tcExternalCancelCrossUser — the
+ // fault injection that shows the spec has teeth.
+ if (viaWatch || CROSS_USER_HONORS_TOKEN_CANCEL()) {
+ workerObservedCancel = true;
+ send helper, eHelperCancel, (actionId = curActionId, method = cm, token = token);
+ }
+ } else {
+ // Same-user subprocess awaits the sticky token directly, so a cancel
+ // over EITHER channel is observed — zero-latency, never lost to EOF.
+ workerObservedCancel = true;
+ send worker, eCancelRequest, (actionId = curActionId, method = cm);
+ }
+ }
+
+ fun finalizeAction(reportedState: tActionState) {
+ var finalState: tActionState;
+ finalState = reportedState;
+
+ // Apply the cancel overlay from session-level state, mirroring the
+ // code's terminal-state computation. If the worker's detection channel
+ // observed a cancel, the outcome is Canceled — regardless of the
+ // process's natural exit (subprocess.rs: the sticky is_cancelled()
+ // check sits ABOVE the success() check). Timeout still wins over Cancel
+ // (checked first in the code), so a reported Timeout is preserved. The
+ // sole rewrite on top is Canceled → Failed when mark_action_failed was
+ // requested (session.rs).
+ if (workerObservedCancel && finalState != ACT_TIMEOUT) {
+ if (markFailed) { finalState = ACT_FAILED; }
+ else { finalState = ACT_CANCELED; }
+ }
+
+ curState = finalState;
+ announce eMonActionEnd, (actionId = curActionId, st = finalState);
+
+ // Brittle-session rule: any failure/cancel/timeout ⇒ ending-only.
+ if (finalState == ACT_FAILED || finalState == ACT_CANCELED || finalState == ACT_TIMEOUT) {
+ endingOnly = true;
+ }
+
+ // A FAILED or CANCELED onEnter leaves the environment ON the stack — it
+ // is pushed before the action runs and only removed by a later exit, so
+ // the agent can still run its onExit during brittle-session teardown.
+ //
+ // EXIT_ENV already popped the environment at exit-start (see eExitEnv),
+ // so nothing to pop here regardless of the onExit result.
+
+ if (endingOnly) { setState(S_READY_ENDING); }
+ else { setState(S_READY); }
+
+ send curClient, eActionDone, finalState;
+ goto Ready;
+ }
+
+ fun doCleanup(client: machine) {
+ if (crossUser) { send helper, eHelperShutdown, (session = this, token = token); }
+ // cleanup() while environments remain leaves onExit un-run (documented
+ // hazard). The monitor flags a non-empty stack at cleanup.
+ announce eMonCleanup, sizeof(stack);
+ setState(S_ENDED);
+ send client, eCleanupDone;
+ goto Ended;
+ }
+
+ /* ---- env-var change set (attach to the env being entered) ---- */
+ fun applySet(name: int) {
+ var rec: tEnvRecord;
+ if (sizeof(stack) == 0) { return; }
+ rec = stack[sizeof(stack) - 1];
+ rec.unsets -= (name); // unset-wins is per-env; a later set overrides
+ rec.sets += (name);
+ stack[sizeof(stack) - 1] = rec;
+ }
+ fun applyUnset(name: int) {
+ var rec: tEnvRecord;
+ if (sizeof(stack) == 0) { return; }
+ rec = stack[sizeof(stack) - 1];
+ rec.sets -= (name);
+ rec.unsets += (name);
+ stack[sizeof(stack) - 1] = rec;
+ }
+
+ fun popTop() {
+ if (sizeof(stack) > 0) {
+ announce eMonExit, topEnv();
+ stack -= (sizeof(stack) - 1);
+ }
+ }
+
+ fun topEnv(): tEnvId { return stack[sizeof(stack) - 1].envId; }
+
+ fun envOnStack(id: tEnvId): bool {
+ var i: int;
+ i = 0;
+ while (i < sizeof(stack)) {
+ if (stack[i].envId == id) { return true; }
+ i = i + 1;
+ }
+ return false;
+ }
+
+ fun reject(client: machine) { send client, eCmdRejected, sstate; }
+
+ fun chooseCancelMethod(): tCancelMethod {
+ if ($) { return CM_TERMINATE; } else { return CM_NOTIFY_THEN_TERMINATE; }
+ }
+
+ fun setState(s: tSessionState) {
+ announce eMonStateChanged, (fromState = sstate, toState = s);
+ sstate = s;
+ }
+}
diff --git a/specs/sessions/pmodel/PSrc/Subprocess.p b/specs/sessions/pmodel/PSrc/Subprocess.p
new file mode 100644
index 00000000..cd771a36
--- /dev/null
+++ b/specs/sessions/pmodel/PSrc/Subprocess.p
@@ -0,0 +1,108 @@
+/*****************************************************************************
+ * Subprocess.p — abstract async subprocess (specs/sessions/subprocess.md).
+ *
+ * Models the same-user path: spawn a child, stream a nondeterministic number
+ * of openjd_* directives, then exit — OR respond to a cancel request with
+ * notify-then-terminate / immediate terminate, always eventually exiting.
+ *
+ * Byte-level I/O, UTF-8 decoding, 64KB truncation, setsid/killpg/dup2 are all
+ * out of scope; a "line" is an opaque directive choice.
+ *****************************************************************************/
+
+machine Subprocess {
+ var session: machine;
+ var actionId: tActionId;
+ var kind: tActionKind;
+ var cancelMethod: tCancelMethod;
+ var envId: tEnvId;
+ var emitsLeft: int; // how many more directives this run will emit
+ //
+ // NOTE ON CANCEL CLASSIFICATION. The subprocess here reports only its
+ // NATURAL termination (Success / Failed / Timeout). It does NOT itself
+ // decide "Canceled". In the code, the Canceled verdict is computed from
+ // shared state checked after the read loop — the sticky
+ // `cancel_token.is_cancelled()` (same-user, subprocess.rs) or the watch
+ // channel `has_changed()` (cross-user, cross_user_helper.rs). That is
+ // session-controlled state, not a raceable in-band message, so the Session
+ // applies the cancel overlay in finalizeAction (see Session.p). Modeling it
+ // there — rather than racing an eCancelRequest against EOF — is what makes
+ // the same-user path correctly deterministic (a cancel is never "lost to
+ // EOF") while still letting the cross-user token-drop bug surface.
+
+ start state Init {
+ entry (cfg: (session: machine, actionId: tActionId, kind: tActionKind,
+ cancelMethod: tCancelMethod, envId: tEnvId)) {
+ session = cfg.session;
+ actionId = cfg.actionId;
+ kind = cfg.kind;
+ cancelMethod = cfg.cancelMethod;
+ envId = cfg.envId;
+ // Emit between 0 and 3 directives before finishing.
+ emitsLeft = choose(4);
+ goto Streaming;
+ }
+ }
+
+ /* ---- Streaming: emit directives, then terminate NATURALLY. ---------------
+ * We yield via a self-scheduled eTick between lines so the checker can
+ * schedule an incoming eCancelRequest between any two emitted directives.
+ * A received cancel just stops the stream promptly (liveness) and lets the
+ * process finish; it does NOT decide the terminal state — the Session
+ * applies the Canceled overlay in finalizeAction based on session-level
+ * cancel state (sticky token / watch channel), mirroring the code.
+ */
+ state Streaming {
+ entry { send this, eTick; }
+
+ on eTick do {
+ if (emitsLeft > 0) {
+ emitsLeft = emitsLeft - 1;
+ emitOneDirective();
+ send this, eTick; // yield, then continue streaming
+ } else {
+ finishNaturally();
+ }
+ }
+
+ // A cancel received in-band (same-user path) stops the stream promptly.
+ // The Session decides the terminal classification.
+ on eCancelRequest do (m: (actionId: tActionId, method: tCancelMethod)) {
+ if (m.actionId == actionId) { finishNaturally(); }
+ }
+ }
+
+ fun finishNaturally() {
+ // The process's OWN exit outcome, independent of cancel: Success,
+ // Failed (nonzero exit), or Timeout (killed by the timeout path).
+ if ($) { finish(ACT_SUCCESS, 0); }
+ else if ($) { finish(ACT_FAILED, 1); }
+ else { finish(ACT_TIMEOUT, -9); }
+ }
+
+ fun emitOneDirective() {
+ // Pick one openjd_* directive. envId is the environment being entered
+ // (or -1 for tasks / ad-hoc subprocess).
+ var pick: int;
+ pick = choose(6);
+ if (pick == 0) { send session, eProgress, (actionId = actionId, value = choose(101)); }
+ else if (pick == 1) { send session, eStatus, actionId; }
+ else if (pick == 2) { send session, eSetEnv, (actionId = actionId, envId = envId, name = choose(3)); }
+ else if (pick == 3) { send session, eUnsetEnv, (actionId = actionId, envId = envId, name = choose(3)); }
+ else if (pick == 4) { send session, eRedactedEnv, (actionId = actionId, envId = envId, name = choose(3)); }
+ else { /* a malformed directive → CancelMarkFailed */
+ send session, eCancelMarkFailed, actionId; }
+ }
+
+ /* ---- Done: exited and finalized. A cancel arriving AFTER finalization is
+ * a genuine no-op (the process is already gone and the result reported);
+ * this differs from a cancel arriving before EOF, which the sticky flag
+ * turns into a Canceled result above. ----------------------------------- */
+ state Done {
+ ignore eCancelRequest, eGraceExpired, eExitGrace, eTick;
+ }
+
+ fun finish(finalSt: tActionState, code: tExitCode) {
+ send session, eProcessExited, (actionId = actionId, st = finalSt, code = code);
+ goto Done;
+ }
+}
diff --git a/specs/sessions/pmodel/PTst/Drivers.p b/specs/sessions/pmodel/PTst/Drivers.p
new file mode 100644
index 00000000..0518f28d
--- /dev/null
+++ b/specs/sessions/pmodel/PTst/Drivers.p
@@ -0,0 +1,192 @@
+/*****************************************************************************
+ * Drivers.p — client machines that exercise the Session like the worker agent.
+ *
+ * Each driver issues lifecycle commands, waits for the reply (eActionDone /
+ * eCmdRejected / eCleanupDone) before issuing the next — mirroring the real
+ * "one action at a time" usage — and finally cleans up.
+ *****************************************************************************/
+
+/* A driver that walks a typical worker-agent pattern:
+ * enter job env → enter step env → run tasks → exit envs (LIFO) → cleanup.
+ * With nondeterminism it may also cancel, hit failures, and try illegal
+ * commands (which must be rejected, not crash).
+ */
+machine WorkerAgentDriver {
+ var session: machine;
+ var crossUser: bool;
+ var tasksLeft: int;
+ var tasksPlanned: bool;
+
+ start state Init {
+ entry (cu: bool) {
+ crossUser = cu;
+ session = new Session((crossUser = crossUser, hasCancelToken = false));
+ goto EnterJobEnv;
+ }
+ }
+
+ state EnterJobEnv {
+ entry { send session, eEnterEnv, (client = this, envId = 1); }
+ on eActionDone goto EnterStepEnv;
+ on eCmdRejected goto CleanupNow; // env failed to enter → tear down
+ }
+
+ state EnterStepEnv {
+ // The driver can't see Session internals; if the step-env enter is
+ // rejected (e.g. the session went brittle), it handles eCmdRejected and
+ // proceeds to teardown. No need to predict ending-only here.
+ entry { send session, eEnterEnv, (client = this, envId = 2); }
+ on eActionDone goto RunTasks;
+ on eCmdRejected goto ExitStepEnv;
+ }
+
+ state RunTasks {
+ entry {
+ // Plan a bounded number of tasks ONCE, so the state space is finite.
+ if (!tasksPlanned) { tasksLeft = choose(3); tasksPlanned = true; }
+ if (tasksLeft > 0) {
+ tasksLeft = tasksLeft - 1;
+ send session, eRunTask, this;
+ } else {
+ goto ExitStepEnv;
+ }
+ }
+ on eActionDone goto RunTasks;
+ on eCmdRejected goto ExitStepEnv;
+ }
+
+ state ExitStepEnv {
+ entry {
+ // Exit env 2 if it's the top; otherwise skip to job-env exit.
+ send session, eExitEnv, (client = this, envId = 2, keepRunning = false);
+ }
+ on eActionDone goto ExitJobEnv;
+ on eCmdRejected goto ExitJobEnv; // env 2 wasn't on top; try job env
+ }
+
+ state ExitJobEnv {
+ entry { send session, eExitEnv, (client = this, envId = 1, keepRunning = false); }
+ on eActionDone goto CleanupNow;
+ on eCmdRejected goto CleanupNow;
+ }
+
+ state CleanupNow {
+ entry { send session, eCleanup, this; }
+ on eCleanupDone goto Done;
+ }
+
+ state Done { }
+}
+
+/* A driver that cancels the very first action, then must only be allowed to
+ * exit environments and clean up (brittle-session contract). */
+machine CancelDriver {
+ var session: machine;
+ start state Init {
+ entry (cu: bool) {
+ session = new Session((crossUser = cu, hasCancelToken = false));
+ send session, eEnterEnv, (client = this, envId = 1);
+ goto AwaitEnter;
+ }
+ }
+ state AwaitEnter {
+ // Fire a cancel as soon as we can; the Session is in Running. The
+ // cancel may lose the race to a clean EOF, in which case onEnter
+ // finishes Success and the session is NOT brittle — that's legal, so
+ // the assertion below is guarded on the reported terminal state.
+ entry { send session, eCancelAction, false; }
+ on eActionDone do (st: tActionState) {
+ if (st == ACT_SUCCESS) { goto ExitEnv; } // cancel lost the race
+ else { goto TryIllegalThenCleanup; } // brittle now
+ }
+ on eCmdRejected goto Cleanup;
+ }
+ state TryIllegalThenCleanup {
+ // The onEnter did NOT succeed, so the session is brittle: run_task must
+ // be rejected.
+ entry { send session, eRunTask, this; }
+ on eCmdRejected goto ExitEnv; // expected
+ on eActionDone do (st: tActionState) {
+ assert false, "run_task accepted after a failed/canceled action (brittle-session violated)";
+ }
+ }
+ state ExitEnv {
+ entry { send session, eExitEnv, (client = this, envId = 1, keepRunning = false); }
+ on eActionDone goto Cleanup;
+ on eCmdRejected goto Cleanup;
+ }
+ state Cleanup {
+ entry { send session, eCleanup, this; }
+ on eCleanupDone goto Done;
+ }
+ state Done { }
+}
+
+/* A driver that cancels via the EXTERNAL SessionConfig.cancel_token (a bare
+ * token cancel — NOT cancel_action), mirroring a caller cancelling a whole
+ * session from outside its async context. A token-only cancel must still take
+ * effect on both the same-user and cross-user paths; CancelDeliverySpec asserts
+ * this. (With CROSS_USER_HONORS_TOKEN_CANCEL flipped off, the cross-user run is
+ * where that assertion bites — see Session.p.) Runs both crossUser values via
+ * the test setup. */
+machine ExternalCancelDriver {
+ var session: machine;
+ start state Init {
+ entry (cu: bool) {
+ session = new Session((crossUser = cu, hasCancelToken = true));
+ send session, eEnterEnv, (client = this, envId = 1);
+ goto AwaitEnter;
+ }
+ }
+ state AwaitEnter {
+ // Fire the EXTERNAL token cancel while the onEnter action is Running.
+ entry { send session, eSessionCancelToken; }
+ on eActionDone do (st: tActionState) { goto ExitEnv; }
+ on eCmdRejected goto Cleanup;
+ }
+ state ExitEnv {
+ entry { send session, eExitEnv, (client = this, envId = 1, keepRunning = false); }
+ on eActionDone goto Cleanup;
+ on eCmdRejected goto Cleanup;
+ }
+ state Cleanup {
+ entry { send session, eCleanup, this; }
+ on eCleanupDone goto Done;
+ }
+ state Done { }
+}
+
+/* A driver focused on the cross-user helper token security invariant:
+ * a bad-token cancel must NOT stop a running action. We can't inject a bad
+ * token through the Session (it always sends the right one), so this driver
+ * talks to a helper directly. */
+machine HelperTokenDriver {
+ var helper: machine;
+ var good: tToken;
+
+ start state Init {
+ entry {
+ good = 7;
+ helper = new CrossUserHelper((session = this, token = good));
+ send helper, eHelperRun, (session = this, actionId = 100, token = good);
+ goto Running;
+ }
+ }
+ state Running {
+ // Immediately try a cancel with the WRONG token.
+ entry { send helper, eHelperCancel, (actionId = 100, method = CM_TERMINATE, token = good + 1); }
+ on eHelperInvalidToken do { /* expected: run continues */ }
+ ignore eHelperPid, eHelperOut, eHelperExited;
+ on eProcessExited do (m: (actionId: tActionId, st: tActionState, code: tExitCode)) {
+ // The action must have ended on its own terms (Success/Failed),
+ // NOT Canceled — the bad-token cancel had no effect.
+ assert m.st != ACT_CANCELED,
+ "bad-token cancel canceled a running action (helper security violated)";
+ send helper, eHelperShutdown, (session = this, token = good);
+ goto Done;
+ }
+ }
+ state Done {
+ ignore eHelperPid, eHelperOut, eHelperExited, eHelperInvalidToken, eProcessExited;
+ }
+}
diff --git a/specs/sessions/pmodel/PTst/TestScripts.p b/specs/sessions/pmodel/PTst/TestScripts.p
new file mode 100644
index 00000000..46e01427
--- /dev/null
+++ b/specs/sessions/pmodel/PTst/TestScripts.p
@@ -0,0 +1,74 @@
+/*****************************************************************************
+ * TestScripts.p — test cases wiring drivers + spec monitors together.
+ *
+ * Run a single case: p check -tc tcWorkerAgentSameUser
+ * Run all: p check
+ *
+ * Each module literal lists every machine that can be instantiated during the
+ * run (listing an unused machine is harmless). Specs are attached with
+ * `assert in `.
+ *****************************************************************************/
+
+/* ---- same-user worker-agent lifecycle ---- */
+test tcWorkerAgentSameUser
+ [main = SetupWorkerAgentSameUser]:
+ assert SessionStateSpec, EnvStackSpec, ActionLivenessSpec, CancelDeliverySpec in
+ { SetupWorkerAgentSameUser, WorkerAgentDriver, Session, Subprocess, CrossUserHelper };
+
+machine SetupWorkerAgentSameUser {
+ start state Init { entry { new WorkerAgentDriver(false); } }
+}
+
+/* ---- cross-user worker-agent lifecycle (routes through the helper) ---- */
+test tcWorkerAgentCrossUser
+ [main = SetupWorkerAgentCrossUser]:
+ assert SessionStateSpec, EnvStackSpec, ActionLivenessSpec, CancelDeliverySpec in
+ { SetupWorkerAgentCrossUser, WorkerAgentDriver, Session, Subprocess, CrossUserHelper };
+
+machine SetupWorkerAgentCrossUser {
+ start state Init { entry { new WorkerAgentDriver(true); } }
+}
+
+/* ---- cancel_action → brittle-session contract ---- */
+test tcCancelBrittle
+ [main = SetupCancel]:
+ assert SessionStateSpec, EnvStackSpec, ActionLivenessSpec, CancelDeliverySpec in
+ { SetupCancel, CancelDriver, Session, Subprocess, CrossUserHelper };
+
+machine SetupCancel {
+ start state Init { entry { new CancelDriver(false); } }
+}
+
+/* ---- external token cancel, SAME-user (delivered via the token; the
+ * same-user subprocess awaits the token, so the cancel takes effect) ---- */
+test tcExternalCancelSameUser
+ [main = SetupExternalCancelSameUser]:
+ assert SessionStateSpec, EnvStackSpec, ActionLivenessSpec, CancelDeliverySpec in
+ { SetupExternalCancelSameUser, ExternalCancelDriver, Session, Subprocess, CrossUserHelper };
+
+machine SetupExternalCancelSameUser {
+ start state Init { entry { new ExternalCancelDriver(false); } }
+}
+
+/* ---- external token cancel, CROSS-user. A token-only cancel must still take
+ * effect on the cross-user path (CancelDeliverySpec). This is the case that
+ * turns red when CROSS_USER_HONORS_TOKEN_CANCEL is flipped off — the fault
+ * injection that shows the spec is specific to this path. ---- */
+test tcExternalCancelCrossUser
+ [main = SetupExternalCancelCrossUser]:
+ assert SessionStateSpec, EnvStackSpec, ActionLivenessSpec, CancelDeliverySpec in
+ { SetupExternalCancelCrossUser, ExternalCancelDriver, Session, Subprocess, CrossUserHelper };
+
+machine SetupExternalCancelCrossUser {
+ start state Init { entry { new ExternalCancelDriver(true); } }
+}
+
+/* ---- cross-user helper token security ---- */
+test tcHelperTokenSecurity
+ [main = SetupHelperToken]:
+ assert ActionLivenessSpec in
+ { SetupHelperToken, HelperTokenDriver, CrossUserHelper };
+
+machine SetupHelperToken {
+ start state Init { entry { new HelperTokenDriver(); } }
+}
diff --git a/specs/sessions/pmodel/README.md b/specs/sessions/pmodel/README.md
new file mode 100644
index 00000000..2970604c
--- /dev/null
+++ b/specs/sessions/pmodel/README.md
@@ -0,0 +1,251 @@
+# P model of `openjd-sessions`
+
+A [P](https://p-org.github.io/P/) formal model of the `openjd-sessions` runtime
+(`crates/openjd-sessions`). Sessions are a small set of concurrent state
+machines exchanging events — a Session driving one action at a time, an abstract
+Subprocess, and (optionally) a persistent cross-user Helper — so they map
+naturally onto P `machine`s, `event`s, and `spec` monitors.
+
+The model is an **abstraction**, not a port: it captures the control-flow and
+ordering contracts documented in [`specs/sessions/`](../) and asserts the
+invariants against every interleaving the P checker explores. It deliberately
+drops bytes, real paths, crypto, and wall-clock time (see
+[Out of scope](#out-of-scope-for-the-model)).
+
+Cross-references to the Rust source (`session.rs:NNNN`) mark decisions that were
+verified against the implementation rather than the prose spec — a few of these
+diverged from the informal specs and the model follows the code.
+
+## Layout
+
+```
+pmodel/
+├── OpenJDSessions.pproj # P project file (PSrc + PSpec + PTst)
+├── Dockerfile # P toolchain image (from p-org/P PR #983)
+├── PSrc/ # the model
+│ ├── Events.p # events + shared types (SessionState, ActionState, …)
+│ ├── Session.p # the SessionState machine (the core)
+│ ├── Subprocess.p # abstract async subprocess (same-user path)
+│ └── CrossUserHelper.p # persistent cross-user helper + token protocol
+├── PSpec/ # invariant monitors
+│ ├── MonitorEvents.p # events the Session announces to the monitors
+│ ├── SessionStateSpec.p # legal transitions, ≤1 action, brittle-session
+│ ├── EnvStackSpec.p # LIFO exits, no duplicate env, clean teardown
+│ ├── ActionLivenessSpec.p # every started action eventually terminates
+│ └── CancelDeliverySpec.p # an issued cancel is never silently dropped
+└── PTst/ # drivers + test cases
+ ├── Drivers.p # WorkerAgent / Cancel / ExternalCancel / HelperToken
+ └── TestScripts.p # test declarations (tc*)
+```
+
+## Status
+
+**Compiles and model-checks clean** with P CLI 3.1.0. All six test cases report
+0 bugs (2000+ schedules each) at the default settings. Two independent
+fault-injection knobs confirm the monitors are live, not vacuous:
+
+- Removing the exit-time stack pop makes `EnvStackSpec` fail.
+- `CROSS_USER_HONORS_TOKEN_CANCEL()` in `PSrc/Session.p` defaults to `true` (the
+ cross-user path observes a cancel over either delivery channel). Flipping it to
+ `false` makes the cross-user path ignore a token-only cancel;
+ `tcExternalCancelCrossUser` then fails `CancelDeliverySpec` while
+ `tcExternalCancelSameUser` and `tcWorkerAgentCrossUser` stay green — showing
+ `CancelDeliverySpec` has teeth and is specific to the cross-user token-cancel
+ path. See [Two-channel cancel delivery](#two-channel-cancel-delivery).
+
+## Building & running the checker
+
+There is no P toolchain checked into this repo. Use the toolchain image built
+from [p-org/P PR #983](https://github.com/p-org/P/pull/983) (bundles the .NET
+SDK, JDK 17, Maven, graphviz, and the `p` CLI).
+
+**Build the toolchain image** — the `Dockerfile` here is a verbatim copy of the
+one added in that PR; it builds `p` from a **P checkout**, so build it with a
+clone of `p-org/P` as the context, not from this directory. Any container
+runtime works (Docker Desktop, colima, Rancher, …):
+
+```bash
+git clone https://github.com/p-org/P.git /tmp/P
+# use the PR's Dockerfile (or check out the PR branch, which already contains it)
+docker build -t p -f specs/sessions/pmodel/Dockerfile /tmp/P
+```
+
+**Compile and model-check** the model by mounting this directory as the
+workspace:
+
+```bash
+cd specs/sessions/pmodel
+docker run --rm -it -v "$PWD":/workspace p \
+ bash -lc 'p compile && p check -tc tcWorkerAgentSameUser'
+```
+
+Useful invocations (inside the container, or with a native `p` on `PATH`):
+
+| Command | What it does |
+|---------|--------------|
+| `p compile` | Compile `OpenJDSessions.pproj` |
+| `p check` | Run all test cases |
+| `p check -tc tcWorkerAgentSameUser` | Same-user lifecycle |
+| `p check -tc tcWorkerAgentCrossUser` | Cross-user lifecycle (routes through the helper) |
+| `p check -tc tcCancelBrittle` | cancel_action → brittle-session contract |
+| `p check -tc tcExternalCancelCrossUser` | External token cancel on a cross-user session (turns red under the fault-injection knob) |
+| `p check -tc tcHelperTokenSecurity` | Bad-token cancel must not stop a run |
+| `p check -tc tcWorkerAgentSameUser -i 10000` | 10k schedules (more coverage) |
+
+## Test cases
+
+| Test case | Drivers | Specs asserted |
+|-----------|---------|----------------|
+| `tcWorkerAgentSameUser` | `WorkerAgentDriver(crossUser=false)` | State, EnvStack, Liveness, CancelDelivery |
+| `tcWorkerAgentCrossUser` | `WorkerAgentDriver(crossUser=true)` | State, EnvStack, Liveness, CancelDelivery |
+| `tcCancelBrittle` | `CancelDriver` (via `cancel_action`) | State, EnvStack, Liveness, CancelDelivery |
+| `tcExternalCancelSameUser` | `ExternalCancelDriver(crossUser=false)` | State, EnvStack, Liveness, CancelDelivery |
+| `tcExternalCancelCrossUser` | `ExternalCancelDriver(crossUser=true)` | State, EnvStack, Liveness, CancelDelivery |
+| `tcHelperTokenSecurity` | `HelperTokenDriver` | Liveness (+ inline security asserts) |
+
+---
+
+## What the model covers
+
+### Machines (P `machine`s)
+
+- **Session** — the driver. Holds `SessionState` {Ready, Running, Canceling,
+ ReadyEnding, Ended}, a LIFO env stack, the cumulative env-var change set, and
+ the `ending_only` brittle flag.
+- **Subprocess** — one per action on the same-user path. Emits a
+ nondeterministic sequence of `openjd_*` directives, then reaches a terminal
+ `ActionState` via normal exit, timeout→SIGKILL, or cancel→grace→SIGKILL.
+- **CrossUserHelper** — persistent process on the cross-user path; sequential
+ command loop; token check; abstracts the poll-multiplex of cancel-stdin vs
+ child-stdout.
+- **Drivers** (`PTst`) — stand in for the worker agent / CLI: issue
+ enter/exit/run/cancel/cleanup and the external `cancel_token`.
+
+Environments are modeled as **data** (stack entries carrying their env-var
+contribution), not machines; their `onEnter`/`onExit` scripts reuse the action
+path.
+
+### Events (P `event`s)
+
+- **Lifecycle commands** (Driver→Session): `eEnterEnv`, `eExitEnv(keepRunning)`,
+ `eRunTask`, `eRunSubprocess`, `eCancelAction(markFailed)`,
+ `eSessionCancelToken`, `eCleanup`.
+- **Action messages** (Subprocess/Filter→Session, the `ActionMessage` enum):
+ `eProgress`, `eStatus`, `eFail`, `eSetEnv`, `eUnsetEnv`, `eRedactedEnv`,
+ `eCancelMarkFailed`.
+- **Subprocess lifecycle / signals**: `eProcessExited(state, code)`,
+ `eCancelRequest(method)`, `eGraceExpired`, `eExitGrace`.
+- **Helper wire protocol** (Session↔Helper): `eHelperRun{token}`,
+ `eHelperCancel{method, token}`, `eHelperShutdown{token}`; responses
+ `eHelperPid`, `eHelperOut`, `eHelperExited`, `eHelperError`,
+ `eHelperInvalidToken`.
+
+### Invariants asserted (P `spec` monitors)
+
+**State machine** (`SessionStateSpec`):
+- Only the documented `SessionState` transitions occur.
+- Exactly one action `Running` at a time.
+- After any action Failed/Canceled/Timeout the session is brittle: it never
+ returns to plain `Ready` — only `ReadyEnding` or `Ended`.
+- `Ended` is terminal.
+
+**Environment stack** (`EnvStackSpec`):
+- Exits are strictly LIFO; `exit(id)` matches the top of stack.
+- No duplicate env identifier is ever on the stack.
+- `cleanup()` with a non-empty stack is flagged (onExit scripts skipped).
+- The env-var change set is the exact fold of per-env changes in entry order
+ (last-writer-wins within an env); popping an env removes exactly its
+ contribution. Only `onEnter`-time changes are attributed; task / onExit /
+ ad-hoc `openjd_env` changes are discarded.
+
+**Cancellation** (in `Session` + drivers):
+- `cancel_action` valid only from `Running` → `Canceling`.
+- Every action installs **fresh** cancel state, so a cancel never poisons a
+ later action — *except* `SessionConfig.cancel_token`, whose cancel is
+ permanent and cascades to all current and future actions.
+- Cancel classification is a session-level overlay applied in `finalizeAction`
+ from whether the worker's detection channel observed the cancel (sticky
+ same-user token / cross-user watch channel), not a raceable in-band message.
+ `Timeout` still wins; the only rewrite on top is Canceled→Failed under
+ `mark_action_failed`.
+- A cancel with a wrong/missing token never terminates the running child
+ (`HelperTokenDriver`).
+
+**Cancel delivery** (`CancelDeliverySpec`):
+- An issued cancel (any channel) is never silently dropped: a canceled action
+ must not complete `Success`. This is the invariant the cross-user
+ token-cancel bug violates — see below.
+
+**Liveness** (`ActionLivenessSpec`):
+- Every started action eventually terminates (exit, timeout, or
+ cancel→grace→kill).
+
+**Helper protocol** (`CrossUserHelper`):
+- Strictly sequential: after a run command, only that action's output then one
+ exit/error before the next command.
+- Token verified on every command; bad token ⇒ `eHelperInvalidToken` and the
+ helper stays alive (no crash / no DoS) and the current run is untouched.
+
+### Two-channel cancel delivery
+
+Cancellation is delivered over **two channels**: the watch channel
+(`cancel_request_rx`, mirrored to the cross-user helper over `cancel_writer`) and
+the per-action `CancellationToken`. `cancel_action` fires **both**; a bare
+external `SessionConfig.cancel_token.cancel()` — the parent token a caller holds
+to cancel a whole session from outside its async context — fires **only the
+token**. Both paths must ultimately produce a `Canceled` outcome, whichever
+channel carried the cancel.
+
+`CancelDeliverySpec` asserts exactly this: any issued cancel eventually takes
+effect (a canceled action never completes `Success`). The
+`CROSS_USER_HONORS_TOKEN_CANCEL()` knob in `PSrc/Session.p` lets the cross-user
+path be made deliberately blind to the token-only channel — a fault injection
+that flips `tcExternalCancelCrossUser` red while same-user cases stay green,
+demonstrating the spec is specific to this channel/path combination. It defaults
+to honoring both channels.
+
+Rationale for individual modeling choices that might surprise a reader (e.g.
+cancel classification is a session-level overlay rather than a raceable message;
+only `onEnter`-time `openjd_env` changes are attributed) is documented inline at
+the relevant point in the `.p` sources.
+
+### P language notes (why some names look odd)
+
+A few names deviate from the Rust source to satisfy the P grammar; they carry
+the same meaning:
+
+- `state` is a P keyword, so the Session's state variable is `sstate` and the
+ `SessionState` payload fields are `fromState`/`toState` (not `from`/`to`,
+ which are also reserved).
+- P has **no single-field named tuples**, so single-value event payloads are
+ bare types (`event eRunTask : machine;`, `event eActionDone : tActionState;`)
+ rather than `(client: machine)` etc.
+- `ActionState` payload fields are named `st` (again, `state` is reserved).
+- Streaming machines yield via a self-sent `eTick` between emitted lines; a
+ plain `goto`-loop runs to completion in P and would prevent an incoming cancel
+ from ever interleaving mid-stream.
+
+## Out of scope for the model
+
+- **OS/filesystem semantics** — TempDir, sticky-bit checks, `remove_dir_all`,
+ `sudo rm -rf`, DACL/permission bits, chown/chmod. File ownership appears only
+ as an abstract token for the helper security invariant.
+- **Byte-level I/O** — UTF-8 lossy decoding, 64KB line truncation, BufReader
+ buffer-before-poll. A "line" is an opaque directive choice.
+- **Cryptography** — token entropy/CSPRNG/constant-time compare. The token is an
+ abstract equality-only value; only its behavioral consequences are asserted.
+- **Format-string / expression evaluation** — symbol table, path mapping, let
+ bindings, EXPR extension (these live in `openjd-expr`/`openjd-model`).
+- **Redaction / logging** — `********` substitution, `echo_openjd_directives`,
+ log content (purely observational).
+- **Platform mechanics** — Win32 console/`CTRL_BREAK`, Job Objects,
+ `CreateProcessAsUser`, `setsid`/`killpg`/`dup2`, `CreateEnvironmentBlock`
+ retry race. Abstracted to notify-signal / terminate-signal / kill-tree.
+- **Real time** — timeouts and grace periods are nondeterministic *events*, not
+ wall-clock; the 5s/30s/120s/300s constants are policy, not correctness.
+- **Callback performance / blocking**, `debug_collect_stdout` accumulation, and
+ the `Drop` best-effort safety net (the model asserts only that state reaches
+ `Ended`).
+- **PyO3 bindings** — `SessionCancelHandle`, `clone_cancel_writer`,
+ `override_action_state`. The cancel-from-another-thread concurrency is modeled
+ (via `eSessionCancelToken` / helper `cancel_writer`); the FFI is not.