[atiernan]

Note added when this PR was opened (2026-11-13). Stacked on the 5.19 PR. The host does not act on the policy yet. It was built overnight with no CI run; the test and proof results below are the building session's own local runs. The proof jobs need a full-verification approval.

Stacked on claude/style-fetches (items 5.18 and 5.19, tip 261a1215). Base this PR on that branch, and merge it after.

CI has not run. cargo xtask verify was not run in any form. Everything below is from local runs.

What

The part of Phase 5 item 5.17c that waited for the kernel. GpuReady { software } and GpuRefused now mean something; there is a new host event, GpuExited; and the item's four rules are in the kernel's spec, proven, with the numbers stated once: gpu_window (300 s), gpu_exits (3), gpu_sites (3).

• Events:
  • GpuExited { id } (the host's).
  • GpuSoftware (the host's --gpu=software).
  • GpuSiteExit { lock }. The host never sends it: it is the declassified part of another domain's exit.
• Outputs:
  • GpuStopped { tab, url } (rule 4's notice).
  • GpuAllSoftware (to the host, once).
• Policy: Policy::GpuSoftware.
• State: GpuState, holding a record per renderer, the every-tab bit, and the two most recent sites.
• No IPC message added.

Commits:

1. Spec and theorem statements, alone (rule 3).
2. Exec kernel and proofs.
3. Tests, and exec lint fixes.
4. Mutations and README.

Decisions (all in src/spec.rs's header and the kernel README)

1. GpuExited { id }, not the item's { tab }. Keyed by id, an exit of a replaced GPU process names no live renderer and is ignored.
2. One record per renderer, tagged with id and lock as 5.18's titles are.
   • Records are not removed when their renderer goes: ids are never reused, so a stale record is never read.
   • Cost: one small record per renderer that ever sent a GPU message or exit. Listed.
3. Per origin, not per site. Rule 2 holds "until it navigates to another site". Here it holds until the tab's renderer is replaced, which a navigation to another origin of the same site also does.
4. Time is the kernel's now, in seconds, from the host's Tick.
5. The mode. The first spawns stay 5.18's Spawn { id, Gpu }, so no 5.18 output changes.
   • Policy::Gpu means the run's mode.
   • The kernel tells the host GpuAllSoftware once, after which the host starts every Gpu process in software.
   • Restarts name their mode.
6. Rule 1: the restart is a new GPU process plus the tab's viewport again, which makes the renderer resend its list. The renderer cannot take a new descriptor, so the host keeps the GPU end of the list channel. That host part is not built.
7. Rules 2 and 4 count a record's last two exits in its current mode. A change of mode clears them.
8. Rule 3 counts hardware exits while drawing, by site (the renderer's Domain). The kernel keeps the two most recent distinct sites.
9. A refusal is the machine's.
   • An exit before GpuReady in hardware puts every tab in software, and is not counted by site.
   • GpuRefused itself changes nothing; the exit that follows is the refusal.
   • An exit before GpuReady in software is rule 4.
10. No fallback (macOS) is the host's to handle. A host without a software driver starts nothing for software and draws the notice itself.
11. GpuReady { software: true } from a hardware start marks the record as software.
12. A frame paints only after the current process's GpuReady.
13. Rule 4's "reloading tries once more" is not built. A stopped tab starts again only when its renderer is replaced or the tab is reopened. A restart on a same-origin commit would add outputs to the commit path that every navigation theorem covers. Listed.

Noninterference

theorem_cookie_noninterference keeps its form. What changed:

• A GpuExited belongs to its renderer's domain, as that renderer's frames do.
• Rule 3's shared count is the channel between sites, and it is stated, not hidden. Another domain's exit is declassified to exactly what it does to the shared state:
  • GpuSoftware, for an exit before GpuReady in hardware (a refusal);
  • GpuSiteExit { lock }, for a hardware exit while drawing: the site's lock goes into the shared count, and at most one bit, every tab to software, comes out;
  • nothing else of the exit reaches an observer. lemma_gpu_declassify proves this.
• The relation between the two runs gains the shared bit, the shared sites, and the observer's records.

Evidence

Verus, local, macOS arm64, one run at a time under .git/kani.lock, each capped at 30 min and 8 GB:

• clazel-kernel: 855 verified, 0 errors, wall 56 s, peak 3.1 GB. Before this item it was 780.

Theorems, all proven and all listed in Cargo.toml:

• theorem_gpu_exit_contained: a GPU exit changes only the crash policy's state, and no record but its own renderer's. Every output is for that renderer or its tab, or is the host's GpuAllSoftware.
• theorem_gpu_restart_bounded, with 300 s and two exits written out: a restart in the same mode happens only if the record does not hold two exits with the older within 300 s, and the record is then updated exactly. A mode change records no exits.
• theorem_site_cannot_demote_others, with theorem_gpu_sites_wf_kept: every tab goes to software only through one of these:
  • GpuSoftware;
  • a refusal before GpuReady;
  • a hardware exit while two other, distinct sites have exits within 300 s.
• theorem_paint_after_restart: 5.18's paint theorems restated over restarts.
• theorem_channel_only_own_tab, restated to allow the restart.
• Every earlier theorem is re-proven, noninterference included. What that took:
  • the frame lemmas and the rel builders gained the crash policy's state;
  • three rlimits were raised;
  • gpu_exited was split into the lookup and gpu_exit_of, with the same meaning.
• No escape hatch was used, and no tier was changed.

Mutations, each run alone under the lock with cargo xtask mutate:

• 12 new, all killed with a certificate that Verus checks:
  • gpu-window-shorter, gpu-window-longer (299 s, 301 s);
  • gpu-exits-four;
  • gpu-rule2-never, gpu-rule4-never;
  • gpu-sites-four, gpu-sites-two;
  • gpu-site-counts-own;
  • gpu-refusal-hardware;
  • gpu-paint-before-ready;
  • gpu-ready-not-running;
  • gpu-restart-other-id.
• 3 existing 5.18 mutations re-run and killed, because their witness state changed: paint-tab-is-renderer-id, resize-to-next-gpu, replace-without-gpu.
• The other 59 existing kernel mutations were not re-run. Their find strings still each match exactly once, and no expect was changed.

Tests and checks:

• cargo test -p clazel-kernel -j 4: 59 passed, 0 failed. This includes the new tests/gpu_policy.rs with 14 rows: rules 1 to 4, the refusal in hardware and in software, the 299 s and 300 s edges, one site with many tabs, sites 300 s apart, GpuSoftware told once, a software-only GpuReady, no paint after an exit until GpuReady, an unknown id, and the declassified count.
• behaviour.rs updated: a frame now paints only after GpuReady.
• cargo clippy --workspace --all-targets --locked -- -D warnings: clean.
• cargo fmt --all -- --check: clean.
• cargo xtask check: STATIC CHECKS PASSED.

Which copy of the policy is the specification

The kernel's src/spec.rs is the specification. clazel-gpu's src/policy.rs lives on claude/gpu-fallback-cfed1c, which this branch does not contain (there is no clazel-gpu here). The two models differ:

• per tab there, per renderer here;
• milliseconds there, seconds here;
• a fallback config there, which is the host's here;
• a reload event there, none here.

So agreement cannot be shown without rewriting one of them.

Recommended at the join: remove policy.rs and its Kani harnesses from clazel-gpu, keeping only the start answer and the blocklist there. This branch does not do the join.

The kernel README says this. clazel-gpu's README is not on this branch. The paragraph to add to it at the join:

The crash policy's specification is the kernel's (clazel-kernel/src/spec.rs, item 5.17c, proven there). src/policy.rs was a first version for the kernel to take over; it is removed here, and this crate keeps the start answer (GpuReady/GpuRefused) and the blocklist.

Not done, not verified

• The host does not act on any of this yet. It runs in text mode and starts no GPU process (5.18's decision 2). So GpuExited, Policy::GpuSoftware, GpuAllSoftware and GpuStopped are unused until the window (5.20 to 5.23). Keeping the list channel's GPU end for restarts is also unbuilt.
• Rule 4's "reloading tries once more" (decision 13).
• Records are not removed (decision 2).
• The 59 older mutations were not re-run.
• The real-process test (a GPU process killed mid-frame) needs the GPU process binary and the host.
• CI has not run, and its proof jobs need a full-verification reviewer's approval.

🤖 Generated with Claude Code