[atiernan]

Note added when this PR was opened (2026-11-13). Stacked on the 5.18 PR; one docs commit. 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/ipc-surfaces-cfd15e (item 5.18). Base this PR on that branch,
and merge it after.

What

Item 5.24 of docs/phases/phase-5.md: a design note, not code, as 5.0(i)'s I1
recommends. It is one new section at the end of the file, "Appendix: nested
browsing contexts (item 5.24)". The file has no contents list, so nothing else was
added. The Status table, the 5.0 decisions and every item's text are untouched. No
code changes and no theorem is claimed.

The note is written against the kernel as 5.18 left it (spec.rs, statements.rs,
the README on claude/ipc-surfaces-cfd15e) and against the GPU process's sandbox
from 5.21a.

Decided in the note

1. Which iframes become frames. A cross-origin iframe is its own renderer. A
   same-origin one stays inside the parent's renderer, and the kernel never sees
   it until it navigates cross-origin.
2. The frame tree is the renderers. Renderer gains parent, slot, rect
   and depth; State gains focus. renderers_wf becomes a tree invariant:
   one top-level renderer per tab, no cycles, a unique (parent, slot), and the
   limits.
3. Messages. ChildFrame (tag 20: slot, url, x, y, width, height) and
   ChildGone (tag 21: slot). Neither collides with today's tags (1–11, 14, 15,
   18, 19, 101–114). No kernel-to-renderer message is added, and the parent is
   told nothing about its child.
4. A GPU process per frame, entering 5.21a's sandbox. The child's viewport is
   its rect's size; its position is never sent to it.
5. Composition. New outputs PaintFrame (no URL or title), Place and
   Unplace. The host keeps one clipped surface per frame (a CALayer with
   masksToBounds, an X11 child window, or a DirectComposition visual). The child
   is drawn above its parent.
6. Input by hit rectangle. Input goes to the deepest frame under the point,
   translated into its coordinates. A click moves keyboard focus.
7. A child's own navigation stays in its slot. Its target=_top is dropped.
8. Cross-site frames are cookie-averse and get no storage. This keeps the
   cookie noninterference theorem with no third-party declassification.
9. Kills are contained to subtrees. A dead child leaves a placeholder, and the
   parent learns nothing.
10. Limits: depth 4 and 16 frames per tab.

Theorems, stated to become ensures

• Restated per frame:
  • theorem_paint_fits_viewport: a child's frame fits its rect;
  • theorem_paint_only_own_tab;
  • theorem_viewport_only_to_own_tab;
  • theorem_input_only_to_hit_frame, which replaces the own-tab input theorem.
• New:
  • theorem_frame_only_in_its_rect;
  • theorem_parent_gets_nothing_from_child;
  • theorem_kill_contained.
• Unchanged in substance: theorem_address_bar_integrity, since Paint
  stays the top-level frame's.
• Noninterference changes in three places:
  • outputs are addressed by frame, with Place attributed to the parent;
  • two declassifications: a parent's frame events become FrameDecl or
    FrameRemoved, and the user's input delivered to a frame becomes InputTo;
  • the relation between runs gains equal frame records and focus.

Cost

Compared with 5.18 on that branch:

• 5.18 changed 27 kernel source files (+2,981 lines), added +485 lines in
  clazel-ipc and +294 in tests, 20 certified mutations and five new theorems.
• Frames are estimated larger: 4,000 to 5,000 kernel lines and about 30
  mutations, because the changed invariant reaches every lemma that assumes one
  renderer per tab.
• That is besides host composition on three window systems, in-process
  same-origin documents in the renderer, and a GPU process per frame.

Open questions for the maintainer

These are listed separately in the appendix:

1. A GPU process per frame, or one per site.
2. No cookies for cross-site frames, or partitioned cookies.
3. Stacking a parent's content over a child.
4. The limits (chosen, not measured).
5. A clickjacking hold-off, with frame-ancestors.
6. Whether a parent gets a load event.
7. target=_top with user activation.

Checks

cargo xtask check: STATIC CHECKS PASSED. No code changed. CI has not run.
cargo xtask verify was not run, as instructed.

🤖 Generated with Claude Code