Console: a reloaded console keeps its HALT after the remote lifetime (#985)

keel/web/api.py

@@ -313,7 +313,8 @@ def read_pulse(cfg: ServeConfig, _query: Query, _state: Any, now_ts: int) -> dic
     this endpoint's to interpret. A read that failed and a window that held nothing are different
     facts, so a non-ok window keeps its own status and detail rather than flattening to "empty".
 
-    `halt_token` is `security.halt_token(cfg.token)`, on this endpoint only, for the HALT button:
+    `halt_token` is `security.halt_token(cfg.token)`, on this endpoint only, for the HALT button
+    (and in this endpoint's failure and expired-session refusal, `pulse_halt`, #958 #985):
     see `payload.setup_payload` for why a derived write token may ride a GET body, and
     `server._gated_action` for why the halt needs nothing else. Never `gates_token`, which no
     endpoint serves (#968): it releases a halt, and the page that stops keel must not hold the
@@ -347,7 +348,14 @@ def read_pulse(cfg: ServeConfig, _query: Query, _state: Any, now_ts: int) -> dic
 
 
 def pulse_halt(cfg: ServeConfig) -> dict[str, str]:
-    """The HALT control's inputs when the Pulse report could not be built (#958).
+    """The HALT control's inputs when the Pulse report could not be built (#958), and for the
+    expired-session refusal of that read (#985).
+
+    Two callers, one shape. The Pulse route calls it when `gather_pulse` fails; and
+    `server.KeelHandler._expired_pulse_halt` calls it on the remote-lifetime refusal, for a request
+    carrying this session's cookie only, before admission completes. There the kill-switch reading
+    below is the only ledger read, read-only -- the same read as on #958's path -- so an expired
+    session reaches no report, no other table and no write.
 
     `halt_token` is minted from the session, so it cannot fail. The kill-switch reading is the one
     ledger read here, through its own repo open and `pulse.halt_resume_command` -- never through
@@ -926,7 +934,9 @@ class ApiRoute:
     sortable: tuple[str, ...] = field(default=())
     #: Whether a failed read still answers with the HALT control's inputs (#958). `/api/pulse`
     #: only: it is the view that halts, and `pulse_halt` reads what the button needs apart from
-    #: the report, so a report that raises does not take the stop with it.
+    #: the report, so a report that raises does not take the stop with it. The same flag picks
+    #: the one route whose remote-lifetime refusal carries them to the session's own cookie
+    #: (`server.KeelHandler._expired_pulse_halt`, #985).
     halt_on_failure: bool = False
 
 
@@ -1332,15 +1342,23 @@ def _bound_venue(cfg: ServeConfig) -> str:
         return guards.DEFAULT_VENUE
 
 
-def refusal_document(status: int, title: str, detail: str) -> dict[str, Any]:
+def refusal_document(
+    status: int, title: str, detail: str, *, halt: dict[str, str] | None = None
+) -> dict[str, Any]:
     """A refusal raised BEFORE routing -- a failed host check, a missing session cookie.
 
     Lives here rather than in the handler so that every `/api/*` body, admitted or not, is built by
     one function against one contract. It carries no `engine`, and that is the reason the success
     and failure documents are told apart by HTTP status rather than by a field: these refusals
     happen before admission, and filling in `engine` would mean an unauthenticated request reading
-    the deployment state off disk."""
-    return payload.error_envelope(int(time.time()), status=status, title=title, detail=detail)
+    the deployment state off disk.
+
+    `halt` is `None` but for one refusal: the expired remote session's, on `/api/pulse`, for a
+    request carrying this session's cookie (`server.KeelHandler._expired_pulse_halt`, #985) --
+    `pulse_halt`'s `{halt_token, resume_command}`, the shape #958's failed Pulse carries."""
+    return payload.error_envelope(
+        int(time.time()), status=status, title=title, detail=detail, halt=halt
+    )
 
 
 def action_document(result: Any) -> dict[str, Any]:

keel/web/gates.py

@@ -201,9 +201,10 @@ class UngatedAction:
 #: other request stops authenticating after `security.REMOTE_SESSION_MAX_AGE_SECONDS`; a halt
 #: carrying the session cookie and the halt token does not (`server._is_a_tokened_halt`). That
 #: serves a console still showing a Pulse from before the lifetime ended, whose memory holds the
-#: token, or any client that holds it. A RELOADED console cannot obtain the token: only
-#: `/api/pulse` serves it, and that keeps the lifetime. Its HALT is #985's to restore; meanwhile
-#: the refusal names `keel kill`. A leaked halt token can at worst halt, which `keel resume` at
+#: token, or any client that holds it. A RELOADED console gets the token from `/api/pulse`'s
+#: expiry refusal, which carries `{halt_token, resume_command}` to a request bearing this
+#: session's cookie and to nothing else (`server._expired_pulse_halt`, #985); that refusal still
+#: names `keel kill`. A leaked halt token can at worst halt, which `keel resume` at
 #: a terminal undoes, and it opens no release (#968).
 HALT = UngatedAction(operation=engage_kill_switch, done=KILL_ENGAGED_LINE)
 

keel/web/payload.py

@@ -2564,10 +2564,14 @@ def error_envelope(
     would mean an unauthenticated request reading the deployment database -- the same argument
     that keeps `engine` out of this document.
 
-    `halt` (#958) is `null` on every failure but one: Pulse's own, after admission, where it is
-    `halt_fallback`'s `{halt_token, resume_command}`. The HALT button lives on Pulse, and a stop
-    that vanished whenever the report beside it failed to build would make stopping slower than
-    starting. Present and `null` everywhere else for `attestations`' reason -- a constant key set.
+    `halt` (#958) is `null` on every failure but two, both Pulse's, where it is `halt_fallback`'s
+    `{halt_token, resume_command}`: the report failing after admission (#958), and the remote
+    session's lifetime refusal to a request carrying this session's cookie (#985,
+    `server.KeelHandler._expired_pulse_halt`), which a halt carrying the token outlives (#983).
+    The HALT button lives on Pulse, and a stop that vanished whenever the report beside it failed
+    to build, or whenever the console was reloaded after the lifetime, would make stopping slower
+    than starting. Present and `null` everywhere else for `attestations`' reason -- a constant
+    key set.
     """
     return {
         "as_of": iso(now_ts),
@@ -2579,7 +2583,9 @@ def error_envelope(
 
 
 def halt_fallback(*, halt_token: str, resume_command: str) -> dict[str, str]:
-    """What the HALT control needs when the Pulse report could not be built (#958): the halt
+    """What the HALT control needs when the Pulse report could not be built (#958), or when the
+    remote session's lifetime has expired and `/api/pulse` is refused for this session's cookie
+    (#985, `server.KeelHandler._expired_pulse_halt`): the halt
     token and the resume command, the same two values `pulse_payload` carries as `halt_token`
     and `halt.resume_command`, and nothing else. Bare strings, under the same names, so the
     client hands them to the same two readers (`actions.rememberHaltToken`, `render.haltControl`)

keel/web/security.py

@@ -52,7 +52,8 @@
    `HttpOnly` and must never be written into the page.
 
    One derivation per surface, never one shared: `csrf_token` for a setup step (served on
-   `/api/setup`), `halt_token` for the halt (served on `/api/pulse`), and `gates_token` for a
+   `/api/setup`), `halt_token` for the halt (served on `/api/pulse` -- in its document, or in its
+   expired-session refusal to the session's own cookie, #985), and `gates_token` for a
    Tier 1 release -- which is served by NO endpoint (#968), so a browser session can stop keel
    and cannot restart it. Each route checks its own token in its own header.
 
@@ -126,8 +127,11 @@
 #: a stop is the one failure mode the console must not have, and what a leaked token gains from
 #: the exemption is the power to halt -- undone by `keel resume` at a terminal, never a release.
 #: It serves a console still showing a Pulse from before the lifetime ended, or any client holding
-#: the token; a reloaded console cannot get the token (`/api/pulse` keeps the lifetime), so its
-#: HALT waits on #985 and the refusal names `keel kill` meanwhile.
+#: the token. A reloaded console gets the token from the expiry refusal itself: on `/api/pulse`,
+#: and for a request carrying this session's cookie only, that refusal carries the HALT control's
+#: `{halt_token, resume_command}` (`server.KeelHandler._expired_pulse_halt`, #985). It re-opens
+#: no read and no other endpoint serves the token. The refusal still names `keel kill`, for a
+#: browser with no cached shell, which is refused the page that would draw the button.
 REMOTE_SESSION_MAX_AGE_SECONDS = 12 * 60 * 60
 
 #: ⛔ THE BRUTE-FORCE ARITHMETIC, WRITTEN DOWN SO NOBODY ADDS A RATE LIMITER FOR THE WRONG

keel/web/server.py

@@ -522,7 +522,9 @@ def _send_json(self, code: int, document: dict[str, Any]) -> None:
         if self.command != "HEAD":
             self.wfile.write(payload)
 
-    def _refuse(self, code: int, heading: str, detail: str) -> None:
+    def _refuse(
+        self, code: int, heading: str, detail: str, *, halt: dict[str, str] | None = None
+    ) -> None:
         """A refusal, in the media type the caller asked for by the path it used.
 
         **Path-scoped, not method-scoped, and not content-negotiated.** A refusal handed to a
@@ -541,12 +543,15 @@ def _refuse(self, code: int, heading: str, detail: str) -> None:
         `Accept`-based negotiation was the alternative and it is worse here: a client that forgets
         the header would get the wrong media type from a JSON endpoint, and the one thing this
         server can be certain about is which path was requested.
+
+        `halt` is `None` on every refusal but one: the expired session's on `/api/pulse`, for
+        this session's cookie (`_expired_pulse_halt`, #985). It rides the JSON document only.
         """
         # **Before anything is written.** See `_drain_request_body`: a refusal that leaves a
         # request body unread poisons the next request on the same connection.
         self._drain_request_body()
         if urlsplit(self.path).path.startswith(API_PREFIX):
-            self._send_json(code, api.refusal_document(code, heading, detail))
+            self._send_json(code, api.refusal_document(code, heading, detail, halt=halt))
             return
         self._send(code, f"{heading}\n\n{detail}\n")
 
@@ -686,8 +691,13 @@ def _admitted(self, *, outlives_the_lifetime: bool = False) -> bool:
             )
             return False
         # #648: an ENFORCED lifetime, checked before the token so an expired session cannot be
-        # distinguished from a wrong one by which refusal comes back. Only a remote-configured
-        # server has one -- see `ServeConfig.session_expired_at`.
+        # distinguished from a wrong one by which refusal comes back -- with one exception since
+        # #985: on a GET or HEAD of `/api/pulse` a request bearing THIS session's cookie gets a
+        # refusal that carries `halt`, and a wrong or missing cookie gets `halt: null`. That is
+        # acceptable because only the holder of the real 256-bit session token can see the
+        # difference, and it tells them nothing they could not already use (`_is_a_tokened_halt`
+        # admits that halt anyway). Every other request still cannot tell the two apart. Only a
+        # remote-configured server has a lifetime -- see `ServeConfig.session_expired_at`.
         #
         # #983, the owner's decision: the halt is exempt. A console left running past the lifetime
         # refused its own stop, and refusing a stop is the one failure mode this surface must not
@@ -696,9 +706,10 @@ def _admitted(self, *, outlives_the_lifetime: bool = False) -> bool:
         # cookie below is still checked, and so is the halt token, by `_gated_action`.
         #
         # It serves a console still showing a Pulse from before the lifetime ended (the token is
-        # in its memory), or any client that holds the token. A RELOADED console cannot get it:
-        # only `/api/pulse` serves the token and that keeps the lifetime. Its HALT is #985's to
-        # restore; until then the refusal below names `keel kill`.
+        # in its memory), or any client that holds the token. A RELOADED console gets the token
+        # back from this refusal itself, on `/api/pulse` and for this session's cookie only
+        # (#985, `_expired_pulse_halt`). The refusal still names `keel kill`: a browser with no
+        # cached shell is refused the page that would draw the button.
         expires = self.cfg.session_expired_at
         if expires is not None and not outlives_the_lifetime and time.time() >= expires:
             self._refuse(
@@ -709,6 +720,7 @@ def _admitted(self, *, outlives_the_lifetime: bool = False) -> bool:
                 "screenshot or terminal scrollback should not still work tomorrow. Restart "
                 "`keel serve` and open the address it prints. To stop trading now, run "
                 "`keel kill` at the terminal.",
+                halt=self._expired_pulse_halt(),
             )
             return False
         cookies = parse_cookie_header(self.headers.get("Cookie"))
@@ -736,6 +748,39 @@ def _admitted(self, *, outlives_the_lifetime: bool = False) -> bool:
             return False
         return True
 
+    def _expired_pulse_halt(self) -> dict[str, str] | None:
+        """The HALT control's inputs for the expired-session refusal, or `None` (#985).
+
+        **Owner-approved design.** Since #983 a halt carrying the halt token outlives the remote
+        session lifetime, but the token reaches a browser only on `/api/pulse`, which keeps the
+        lifetime -- so a console reloaded after it had no button. The expiry refusal on that one
+        read now carries #958's `{halt_token, resume_command}` (`api.pulse_halt`), the same shape
+        a failed Pulse carries, so the client draws the same control.
+
+        Three conditions, all of them: a GET (or HEAD) -- the read, never a write to the same
+        path; a path whose route is the one that halts (`ApiRoute.halt_on_failure`, `/api/pulse`
+        alone); and THIS session's cookie. Without the cookie the refusal is the #648 one with
+        nothing extra: the halt token is derived from the session token, and a request that has
+        not shown the session is not handed a credential. With it, nothing is handed that the
+        cookie's holder could not already use -- `_is_a_tokened_halt` admits exactly that halt.
+        This is the one place an expired session's refusal differs from a wrong token's (see the
+        #648 note in `_admitted`); only the holder of the real session token can see it.
+
+        Nothing else about the expired session changes: the refusal is still a 403 with
+        `data: null`, no release and no setup write is admitted, no other read answers, and no
+        other endpoint serves the halt token. Never `gates_token` (#968), here as on every path.
+        The one ledger read is `pulse_halt`'s kill-switch reading, read-only, as on #958's path.
+        """
+        if self.command not in ("GET", "HEAD"):
+            return None
+        route = api.API_ROUTES.get(urlsplit(self.path).path)
+        if route is None or not route.halt_on_failure:
+            return None
+        cookies = parse_cookie_header(self.headers.get("Cookie"))
+        if not tokens_match(cookies.get(SESSION_COOKIE), self.cfg.token):
+            return None
+        return api.pulse_halt(self.cfg)
+
     def _sec_fetch_site_ok(self) -> bool:
         """Checked on EVERY `POST`, `/setup/*` included -- unlike `_api_client_header_ok` below,
         a plain HTML `<form method=post>` DOES carry `Sec-Fetch-Site`: it is Fetch Metadata, set

keel/web/static/js/actions.js

@@ -63,7 +63,8 @@ import { runAction, runHalt } from "./api.js";
 let token = "";
 
 /**
- * This session's halt token, from `/api/pulse`'s `data.halt_token`.
+ * This session's halt token, from `/api/pulse`'s `data.halt_token` -- or its failure's or
+ * expired-session refusal's `halt.halt_token` (#958, #985), handed in the same shape.
  *
  * `""` until a pulse document has been read, for `token`'s reason: the only thing that can halt
  * is a form this client drew from that document. An empty gate reaches the server and is refused

keel/web/static/js/api.js

@@ -84,9 +84,11 @@
  *                                        `undefined`, which every consumer treats as
  *                                        "nothing to show" rather than as a mistake. That
  *                                        is exactly how the banner shipped dead.
- * @property {any}          halt    `{halt_token, resume_command}` on a failed `/api/pulse`, else
- *                                  `null` (#958): the HALT control's inputs, delivered apart from
- *                                  the report so a report that failed to build keeps the stop.
+ * @property {any}          halt    `{halt_token, resume_command}` on a failed `/api/pulse`
+ *                                  (#958), or on its remote-lifetime 403 to this session's
+ *                                  cookie (#985), else `null`: the HALT control's inputs,
+ *                                  delivered apart from the report so a report that failed to
+ *                                  build, or a console reloaded after the lifetime, keeps the stop.
  *                                  Read off a FAILURE document only -- a built Pulse carries the
  *                                  same values in its `data`.
  */

keel/web/static/js/main.js

@@ -639,16 +639,22 @@ async function paint(route, rebuild, force) {
     // refused this browser. The two 403s (`_admitted`'s host check and its session check) share
     // this branch on purpose. They have the same remedy from the operator's side: the address
     // keel printed is what admits this browser, and pasting it is the action either one needs.
-      if (primary.error && primary.error.status === REFUSED_STATUS) {
-        rebuildInto(refusedView(primary, reconnect), Boolean(force));
-      } else if (route.name === "pulse" && primary.halt) {
-        // #958: Pulse's report failed to build, and the failure still carries the HALT control's
-        // inputs. The stop is offered anyway -- stopping is never slower than starting
+    //
+    // The HALT arm comes FIRST, ahead of the 403 (#985). Two Pulse answers carry `halt`: #958's
+    // failed report, and the expired remote session's 403, which the server sends with `halt`
+    // only to this session's cookie (`server._expired_pulse_halt`) -- since #983 it accepts the
+    // halt past the lifetime, and a reloaded console has no other way to get the token. Every
+    // other 403 carries `halt: null` and reaches the reconnect field as before. The branch is on
+    // the PRESENCE of `halt`, never on the refusal's title.
+      if (route.name === "pulse" && primary.halt) {
+        // The stop is offered anyway -- stopping is never slower than starting
         // (`keel/web/gates.py`) -- through the same token holder `mount` uses and the same
-        // control `pulseView` draws. Not the stopped view: keel is running, and that view
-        // offers no stop.
+        // control `pulseView` draws, with the failure's or the refusal's own words under it.
+        // Not the stopped view: keel is running, and that view offers no stop.
         rememberHaltToken(primary.halt);
         rebuildInto(pulseFailedView(primary), Boolean(force));
+      } else if (primary.error && primary.error.status === REFUSED_STATUS) {
+        rebuildInto(refusedView(primary, reconnect), Boolean(force));
       } else {
         rebuildInto(stoppedView(primary, pathFor(SETUP_ROUTE)), Boolean(force));
       }