[atiernan]

⚠️ Rule change for review: CLAUDE.md rule 1

This branch makes xtask/src/sys.rs accept a new form in clazel-sys, and CLAUDE.md
rule 1's wording should change to match it. CLAUDE.md is not edited in this branch:
the session that wrote it does not edit CLAUDE.md on another session's instruction, so
the change is proposed here for the maintainer to apply at merge. The patch is
gpu-drawing-5.17b-claude-md-rule1.patch in the side-session notes folder.

Old:

Inside it, every unsafe is one block holding one call to a foreign function from
the fixed list in xtask/src/sys.rs, with a // SAFETY: comment …

Proposed:

Inside it, every unsafe is one block holding one call to a foreign function from
the fixed list in xtask/src/sys.rs, or one cast of a listed dispatcher to a typed
function pointer, in a const (a call through such a const counts as a foreign
call), with a // SAFETY: comment …

Why: the plan reaches Metal through several #[link_name = "objc_msgSend"]
declarations, one per message signature. rustc 1.98.1 rejects that under CI's
-D warnings:

warning: `msg_void_usize` redeclares `objc_msgSend` with a different signature
 --> src/main.rs:6:5
  |
4 |     #[link_name = "objc_msgSend"]
  |     ----------------------------- `objc_msgSend` previously declared here
5 |     fn msg_id(r: *mut c_void, s: *mut c_void) -> *mut c_void;
6 |     #[link_name = "objc_msgSend"]
  |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this signature doesn't match the previous declaration
  |
  = note: expected `unsafe extern "C-unwind" fn(*mut c_void, *mut c_void) -> *mut c_void`
             found `unsafe extern "C-unwind" fn(*mut c_void, *mut c_void, usize)`
  = note: `#[warn(clashing_extern_declarations)]` on by default

Three options were put to the maintainer, who delegated the decision to the
coordinating session. That session chose typed casts (option 1), under conditions this
branch implements. Rejected: allowing the lint in clazel-sys's manifest (it weakens a
lint, against rule 2), and assembly trampolines (a new kind of code to audit).

The clazel-sys audit is outstanding

clazel-sys gains src/macos/metal.rs. Its author, this session, must not write the
audit row: a different session must audit it. Until then cargo xtask check fails
on the audit, and that is its only failing check:

==> clazel-sys audit
    docs/SYS-AUDITS.md: stale audit of crates/clazel-sys: the latest row covers 07a363f6776cde9274c74c5431c81553f7b29ec5e4798ede81a5f756f62b8351, the source is now 71577331d291369dc61268fd595c553dba47e8b7384a311bfe3fb0673f5d89a0. Every change needs a new audit by a session other than the author's
    source SHA-256 71577331d291369dc61268fd595c553dba47e8b7384a311bfe3fb0673f5d89a0
    covers 7 files: crates/clazel-sys/Cargo.toml, crates/clazel-sys/src/lib.rs, crates/clazel-sys/src/linux.rs, crates/clazel-sys/src/macos.rs, crates/clazel-sys/src/macos/metal.rs, crates/clazel-sys/src/windows.rs, crates/clazel-sys/src/windows/window.rs
    FAIL  clazel-sys audit
RESULT: FAILED

unsafe blocks: 62 (237 lines) before, 137 (336 lines) after, of which 21 are
dispatcher casts (cargo xtask check prints both counts, and README.md states them).

Foreign functions added (METAL in xtask/src/sys.rs, file
crates/clazel-sys/src/macos/metal.rs): objc_msgSend (a dispatcher, never called
directly), objc_getClass, sel_registerName, MTLCreateSystemDefaultDevice,
IOSurfaceCreate, CFRelease, plus an empty block that links Foundation. The 21
dispatcher casts (METAL_CASTS), one per message signature: MSG_ID, MSG_VOID,
MSG_USIZE, MSG_ID_ID, MSG_ID_USIZE, MSG_VOID_ID, MSG_VOID_USIZE,
MSG_VOID_BOOL, MSG_ID_ID_ID_OUT, MSG_ID_ID_OUT, MSG_ID_PTR_USIZE_USIZE,
MSG_ID_USIZE_USIZE, MSG_ID_ID_ID_USIZE, MSG_ID_IDS_IDS_USIZE,
MSG_VOID_ID_USIZE_ID_USIZE_USIZE, MSG_VOID_ID_USIZE_USIZE,
MSG_VOID_PTR_USIZE_USIZE, MSG_VOID_SCISSOR, MSG_VOID_CLEAR,
MSG_VOID_USIZE_USIZE_USIZE_USIZE_USIZE, MSG_VOID_OUT_USIZE_REGION_USIZE. Each lists
above it every selector that uses it.

For the auditor (docs/SYS-AUDITS.md is not edited here): beyond the usual checks,
each dispatcher cast needs its function type compared with every method its comment
lists, exactly: receiver id and SEL first, then each parameter's width and
signedness (NSUInteger is usize; unsigned long is 64 bits; BOOL is bool on
Apple silicon, the only target the module builds for), pointer parameters, structures
passed by value (MTLScissorRect, MTLClearColor, MTLRegion, whose #[repr(C)]
declarations need checking against <Metal/MTLTypes.h> and the encoder headers), and
the return type (void against id against NSUInteger). A mismatch is undefined
behaviour no machine check here catches. Also worth a reviewer's eye:

• The casts are extern "C". An Objective-C exception thrown through one would unwind
  where that ABI forbids it. Metal raises exceptions for API misuse, which the wrappers'
  checks are meant to rule out. Whether the casts should be "C-unwind" (the checker
  accepts only "C" today) is left to review.
• The IOSurface property keys are passed as their string values ("IOSurfaceWidth"
  and so on), because the kIOSurface… constants are data symbols the checker does
  not allow. The values are those of the header. A real-device test checks that a
  texture on a surface gets the surface's size.
• Every object is held at +1: autoreleased results are retained, and
  with_autorelease_pool drains around each frame.
• Citations follow the existing docs <Uppercase…> form, written
  docs Framework/Class/member (for example docs Metal/MTLDevice/newCommandQueue).
  No new citation form was added to the checker.

The checker change (xtask/src/sys.rs, its own commit 4d4c7d8, before any Metal code)

It accepts this form and nothing wider:

• The dispatcher. A dispatcher (only objc_msgSend) is declared once, as
  fn objc_msgSend();, and is named nowhere else.
• The cast. Its one use is a const on its file's list, written exactly
  const NAME: unsafe extern "C" fn(..) -> .. = unsafe { std::mem::transmute(objc_msgSend as unsafe extern "C" fn()) };,
  with a // SAFETY: comment directly above.
• Calls through it. Such a const is named only in calls inside unsafe blocks,
  one call per block, each with its own // SAFETY: comment.

Each rejected form has a planted test:

• any other transmute or transmute_copy, of data or in an unlisted const;
• a turbofish, another path, another source, a source type with parameters, or a
  second call in the block;
• a target that is not unsafe extern "C" fn ("C-unwind", a safe extern "C" fn,
  Option<..>, usize);
• a cast with no // SAFETY: comment;
• the dispatcher called directly, coerced to a pointer, or declared with parameters or
  a return type;
• a call through a local function pointer;
• a cast's name rebound or passed around;
• two calls in one block.

Found on the way and closed in the same commit: unsafe extern "C" fn f() {}, an
unsafe fn, used to be read as an extern block and passed. It is now rejected. Function
pointer types are no longer counted as unsafe blocks (xtask/src/scan.rs), and the
check prints the dispatcher casts separately. Not extended to Vulkan's
vkGetDeviceProcAddr: that needs a second dispatcher kind, a looked-up pointer rather
than a symbol, to be decided when that backend is built.

What this branch does (item 5.17b, first part)

New crate crates/clazel-gpu, tier 0, placed with the renderer in PLACES.

• The shared batching (src/batch.rs). Gpu::draw takes the list's bytes, decodes
  and validates them with clazel-displaylist, and relies only on
  theorem_validated_bounds. It turns the list into a frame of atlas replacements,
  uploads, and draws of one quad format under scissor rectangles.
• A linear glyph atlas (src/atlas.rs): a bump allocator over word-aligned slots,
  compacted when full, up to 128 MiB.
• Backends below a small trait (src/backend.rs), plus a fake backend with no
  foreign calls (src/soft.rs).
• A software reference (src/reference.rs) that paints a list straight from its
  items, independent of the batching.
• Five scenes covering every list item. Each is tested through the fake backend
  against the reference, exactly.
• Shaders, fixed at build time. shaders/quad.metal in MSL, and quad.vert and
  quad.frag in GLSL, compiled to the committed .spv files by naga 30.0.1 in xtask
  (tooling, never shipped). cargo xtask check has a new row, "compiled GPU shaders
  (SPIR-V)", that confirms they match, and cargo xtask tables rewrites them. naga's
  packages are on the allowlist: 19 tooling rows; foldhash is proof and libm
  moved to shipped, each explained in its row (neither is compiled into the browser).
• The Metal backend (src/metal.rs, macOS on Apple silicon). It draws into a
  texture on an IOSurface the backend creates, behind Target, which 5.18 can supply.
  Uploads are blit copies ordered with the render passes; each frame is one command
  buffer, waited for.

Metal results

tests/metal.rs draws every scene and compares each list's pixels with the software
reference (allowed: one level per channel) and with stored pixels (tests/pixels/,
exact). On this machine (Apple M1 Pro, macOS 26.7.2) every channel of every scene
equals the reference: 0 channels differ across 7 lists, 19,968 channels in all. A
mutant shader that gives masks full coverage fails both comparisons. Each test prints
what it ran on, as clazel-gpu: Metal device "<name>" (…). The name comes from the OS
(system_profiler, hw.model, kern.hv_vmm_present); the clazel-sys wrappers can't
read the device's own name without new foreign calls, so none were added. On this
machine it prints clazel-gpu: Metal device "Apple M1 Pro" (Metal support: Metal 4; hw.model MacBookPro18,3; kern.hv_vmm_present 0; …).

A missing device is a skip only on a developer's machine. When CI is set, no
usable Metal device is a test failure, saying so. CI's macos-15 runner (Apple
silicon, virtualised) is expected to offer a paravirtual Metal device, and this PR's
first CI run settles whether it does. So far the Metal tests have run only on this
machine. A paravirtual device may behave differently (IOSurface-backed textures, the
blit path, rounding), so a failure there is possible and would be real information.

Kani

Each harness ran alone, in its own process group, with a 20-minute and 8 GB cap polled
every 5 s.

Harness	Covers	Result	Wall time	Peak memory
place_any	every input	passed	12 s	0.67 GB
grown_capacity_any	every capacity the atlas holds	passed	3 s	< 0.01 GB
rect_at_any	every input	passed	2 s	< 0.01 GB
intersect_any	every input	passed	1 s	< 0.01 GB
blend_any	every input	passed	2 s	< 0.01 GB
visible_any	every input (the draw step's cut)	passed	2 s	< 0.01 GB
clip_then_draw_any	one draw, any viewport, clip and quad	passed	5 s	< 0.01 GB

Removed at a cap, each listed as not covered in the README:

• texel_index_any: the 20-minute cap, twice, at 0.17 GB.
• atlas_upload_any: 8 GB in 83 s.
• The first form of clip_then_draw_any: 8 GB in 21 s. It was split into
  visible_any and the one-draw form above.

No cbmc, goto-* or kani-driver process was left after any run.

Miri

One test per process, 10-minute cap; times on Miri's clock:

Test	Time
scene "atlas"	55.9 s
scene "masks"	39.2 s
scene "clips"	30.7 s
scene "fill"	27.5 s
scene "frames"	18.3 s
bad_lists_are_refused_before_drawing	14.5 s
blending_is_the_exact_value_rounded	12.6 s
the rest	under 1 s each
clazel-sys sizes_are_checked_before_any_call	0.001 s

Two tests were first over CI's 300 s and were fixed before this table:

• The scenes as one test took 523 s, most of it building the ramp coverage byte by
  byte. The ramp is now one 256-byte period repeated, the same bytes.
• The blend test took 290 s. Its inputs are now thinned under cfg(miri), with the
  reason stated in the test.

The tests that call the GPU are ignored under Miri, as stated in each of them.

Decisions (recorded in crates/clazel-gpu/README.md)

• Blending. Source-over in 8-bit sRGB, premultiplied, with no gamma correction. The
  reference rounds the exact value once, halves up, and clamps.
• Colours. A list's colours have no rule, so a channel may exceed its alpha; the
  result clamps at 255.
• Clips. Clips are scissors. Quads are cut to the viewport, not to the clip, and
  nothing is drawn under an empty clip.
• Pipeline. One pipeline, one quad per item. The shaders bound their own reads, and
  naga adds bounds checks to the SPIR-V.
• Atlas. The atlas is linear, with word-aligned slots (Metal's buffer copies on
  macOS need multiples of 4), up to 128 MiB, so a compaction always fits.
• Frames. Each frame starts transparent black. The viewport is up to 8192 a side.
  One frame at a time.
• Metal specifics. The MSL is compiled when the backend starts: the machine has no
  offline Metal toolchain. Apple silicon only.
• Status image. clazel-gpu is placed with the renderer; the detail image has no
  GPU-process panel yet (5.27).

What is left of 5.17b

• The Vulkan backend (Linux, lavapipe). It needs libvulkan-only linking,
  hand-written #[repr(C)] structures, a second dispatcher kind for
  vkGetDeviceProcAddr, no WSI, and the committed SPIR-V.
• The Direct3D 12 backend (Windows, WARP). It needs COM vtable calls taught to the
  checker, DXBC shaders with a check like the SPIR-V one, and
  CreateSwapChainForCompositionSurfaceHandle.
• Neither can run on this machine. Intel Macs are not supported.
• The shared buffers and the process boundary are items 5.18 and 5.21a.

Verification state

• Run locally:
  • cargo test for clazel-gpu, clazel-sys and xtask: all pass.
  • clippy -D warnings on those three crates, and cargo fmt --all --check: clean.
  • cargo xtask check: only the clazel-sys audit fails, as above.
• cargo xtask verify --changed was not run, by instruction.
• CI's full verification has not run. Its proof jobs need a reviewer of the
  full-verification environment to approve the run.

🤖 Generated with Claude Code