Module register_alloc_viz 

Studio easter egg — certified linear-scan register allocation, visualised.

Pure data → SVG (no Z3, no JS): a basic block’s variable live ranges are laid on an instruction timeline as bars, coloured by the physical register they’re assigned. When the block is over-pressure, the bars that provably must spill are flagged red and the certified Hall/clique witness is reported. The allocation comes straight from the certified register_alloc engine, so the picture is a faithful view of a re-checkable result — the same engine that crushes Z3 on the colouring encoding, here rendered for a one-glance “watch the allocator decide” demo.

Structs

RegSpec

A parsed register-allocation spec: named variable live ranges + the physical register budget.

Functions

allocation_report

A textual allocation report for the Studio output panel: the physical register assigned to each variable, or — when the block is over-pressure — the spill verdict naming its mutually-interfering clique. This is the “compiler back-end output” view that pairs with the render timeline; the per-variable registers come from the same linear_scan_assignment the animation replays, and the feasibility/clique verdict from the certified allocate result, so the two views agree.

interference_edges

The interference graph’s edges: every pair of variables (i, j) (i < j) whose live ranges overlap, so they cannot share a register. Register allocation is exactly colouring this graph; for straight-line code it is an interval graph (perfect), so its chromatic number equals the largest clique equals the register pressure.

is_register_alloc_spec

Whether spec is a register-allocation spec (a registers: budget plus at least one live range). This is the single source of truth the Studio uses to route Hardware-mode input to the allocator easter egg, so the wiring (panel visibility, output panel, viz panel) can never drift from what the parser actually accepts.

is_valid_linear_scan

Re-check a linear-scan assignment: every assigned register is within budget, and no two variables that are live at the same time are given the same register — the soundness property any register allocation must satisfy. (Spilled variables, None, impose no constraint: they live in memory.)

linear_scan_assignment

A deterministic linear-scan assignment: variable index i → the physical register it is given, or None if linear-scan must spill it (no register was free when it became live). This is the data the animated view replays — each variable becomes one bar that lights up in its register’s lane while it is live. Re-checkable via is_valid_linear_scan. It spills nothing exactly when the block fits the budget (peak pressure ≤ registers), so it agrees with the certified allocate decision while also showing which value gets evicted when it does not.

parse_register_spec

Parse a spec of the form (one name: start-end per line, plus a registers: N budget):

pressure_profile

Register pressure sampled at each instruction in tmin..tmax: profile[i] is how many variables are live at instruction tmin + i. Its maximum is the register pressure (the fewest registers the block could ever need), which is what the budget line is drawn against — wherever the profile rises above the budget, spilling is unavoidable.

render

Render the certified allocation of spec as (svg, verdict). The SVG is an animated linear-scan: a live-range timeline above an animated register file, with a sweep line crossing both so you can watch each value claim and release its register (and, when over capacity, drop to a spill lane). The verdict is the plain-language, certified summary.