ArchSpec::validate() performs no AOD geometry checks — reuse check_lane_group_geometry over fully-occupied bus lane groups

[weinbe58]

Problem

ArchSpec::validate() (validate.rs:60) — the gate that every from_components and from_json_validated call passes through — performs no AOD geometry validation whatsoever. It is purely structural: minimum counts, non-negative grid spacings, uniform grid dimensions and word site counts, index ranges for site/word/zone bus refs and entangling pairs, bus relation well-formedness (unique sources, unique destinations, acyclic), zone-crossing for zone buses, mode validity, and zone bounding-box non-overlap. For paths it checks only finite coordinates, a valid zone_id, and waypoints.len() >= 2.

Nothing checks that a bus is physically realizable by an AOD: no Cartesian-product (complete-grid) check on bus endpoints, no uniform-displacement (single-shift) check, no check on the set of words participating in a site bus, and no check that a stored path bears any relation to the lane it is keyed by.

Today the only enforcement of AOD rectangle geometry is _validate_aod_rectangle in the Python ZoneBuilder (arch/build/imperative.py), plus a warnings.warn for the single-shift invariant in _compute_paths. A spec loaded from JSON never sees either — and that is how the production architecture is loaded (_physical_spec.json → from_json_validated). So the shipped Gemini physical spec's own buses have never been machine-checked for AOD feasibility; the "always go through the builder" guidance is the sole mechanism, and it is advisory.

Reproducer

A zone with two words whose intra-word site pitch differs — word 0's sites at x = 0/10 µm, word 1's at x = 100/130 µm — and a site bus [0] -> [1]:

• ZoneBuilder.add_site_bus accepts it (its rectangle check runs in word-template index space, (s % nx, s // nx), which is identical for every word).
• _compute_paths accepts it silently — its single-shift check reads self._site_nm(0, ...), i.e. word 0's coordinates only, so it never sees word 1's differing displacement.
• The generated path for word 1 runs (100.0, 0.0) -> (110.0, 0.0), while that lane's own destination site is at (130.0, 0.0). The path terminates on empty space.
• ArchSpec.from_components() and from_json_validated() both accept the resulting spec with zero errors and zero warnings.

The spec carries the contradiction internally: lane_endpoints() returns the correct destination, get_path() returns a path that does not go there, and nothing compares them.

The same class of hole exists one level up for word buses, whose displacement check is per-pair but reads only site 0 (self._site_nm(dw, 0)), so it assumes uniform intra-word geometry across words. Two words with 1 µm and 2 µm internal pitch produce a site-1 path ending at 51 µm when its destination is at 52 µm — again silent, again accepted by validate().

The check we already have, in the wrong place

check_lane_group_geometry (query.rs:859) is exactly the complete-grid / Cartesian-product test we want. It just never runs at spec-validation time — it is invoked from check_lanes on a runtime LaneAddr group about to execute as one AOD shot.

It also only covers the source side. Per lane_endpoints (query.rs:428), "site_id and word_id always encode the forward-direction source", and check_lane_group_geometry resolves position from those fields directly — so it validates the src rectangle and says nothing about destinations or displacement uniformity.

Proposal

In ArchSpec::validate(), synthesize the fully occupied lane group for every bus in every zone — the maximal set of lanes the bus can carry — and run the geometry check over it.

Group construction, per zone z:

• word bus b: { LaneAddr(WordBus, w, s, b, Forward, z) | w in bus.src, s in z.sites_with_word_buses }
• site bus b: { LaneAddr(SiteBus, w, s, b, Forward, z) | w in z.words_with_site_buses, s in bus.src }

Then assert, for each group:

1. Source positions form a complete grid — check_lane_group_geometry verbatim.
2. Destination positions form a complete grid — same test applied to lane_endpoints(lane).1. Needs either a variant taking LocationAddrs or a small refactor of check_lane_group_geometry into a helper over (f64, f64) positions.
3. Uniform src→dst displacement across the whole group (the AOD single-shift invariant). Not covered by check_lane_group_geometry at all; this is the check that catches the reproducer above. Promoting it from a Python warnings.warn to a spec-level error also makes it apply per-word/per-site rather than against word 0 alone.
4. Path/lane endpoint consistency — for each entry in paths, first waypoint == lane_endpoints(lane).0 position and last waypoint == .1 position. Cheapest of the four, catches the most, and is a pure consistency check between two fields the spec already carries.

(3) and (4) are independently valuable and could land first; (1) and (2) are the direct reuse the title refers to.

Blast radius

I audited both bundled specs against all four checks — everything passes, so this is additive with no expected churn on the Python side:

Check	gemini.physical	gemini.logical
bus src & dst endpoints each form a Cartesian product	pass (3 site + 19 word buses)	pass (19 word buses)
uniform src→dst displacement across all participating words and sites	pass	pass
site-bus participating word set is rectangular	pass (odd words = cols 1,3 × rows 0–4)	pass
path first/last waypoint matches lane src/dst	pass, 1120/1120	pass, 110/110

The real implementation cost is the hand-constructed specs in Rust tests — validate.rs's own ~30 test fixtures, arch/query.rs, atom_state.rs, bloqade-lanes-search/src/test_utils.rs, the CLI integration and C-API fixtures. Those are minimal specs built for structural coverage and were never required to be AOD-feasible; each will need auditing or adjusting. That is the bulk of the work, not the checks themselves.

Open questions

• Empty words_with_site_buses with non-empty site_buses. build() emits [] both when a zone has no site buses and when no word opted in, so the fully-occupied site-bus group can come out empty. Decide whether that is a skip or an error (it is arguably already a malformed spec — site buses that no word can use).
• Zone buses. Left out of the proposal above; whether an inter-zone bus should satisfy the same complete-grid constraint depends on how the AOD hands off across zones, and I did not want to assume.
• Error taxonomy. Whether these become a new ArchSpecError variant or reuse LaneGroupError::AODConstraintViolation wrapped into one.

Context

Found while reviewing #1006 (ArchBuilder.from_spec / ZoneBuilder.from_zone, implementing the spec in QuEraComputing/bloqade-internal#445). That PR makes the validating builder reachable for JSON-loaded specs, which is real progress — but it leaves AOD enforcement in the layer that can be bypassed rather than the layer that cannot. Deliberately kept out of #1006's scope.

[weinbe58]

Correction, and a fifth check

First, a correction to something I got wrong when scoping this. I described the path search as using two competing obstacle models — node candidacy requiring clearance from grid lines per axis, edge validity only blocking a crossing of a grid point — and called the first "strictly stronger." That reading was wrong. They are the static and swept forms of one constraint:

• _enumerate_safe_positions._valid(p) accepts a reference position only when every atom in the bus clears every grid line on that axis. Node validity is then x in safe_xs OR y in safe_ys — an or, because clearance on either axis alone is enough to guarantee no AOD trap coincides with an SLM site.
• The edge check adds blockers only for offsets whose y + off_y is a grid row (or x + off_x a grid column), i.e. exactly the atoms that would sweep through a site.

Same invariant, checked statically at waypoints with a margin and continuously along segments.

The model, confirmed

Per @weinbe58: the path must not intersect the grid values, and a bus's start and end must be SLM sites, because buses are transport routes between SLM sites.

That pins the semantics down and gives check 4 above its actual rationale — the endpoint check isn't merely an internal-consistency nicety, it is the definition of what a bus is. It also adds a fifth:

5. A stored path's interior must not intersect the grid. For each bus's fully-occupied lane group (constructed exactly as in the proposal above), at every interior waypoint no atom in the bus may sit on a grid point, and no segment may carry an atom across one.

The important property: this is clearance-free. x_clearance / y_clearance are search parameters and are deliberately not persisted (see the reasoning in QuEraComputing/bloqade-internal#445 §5 — an invariant every path had to satisfy would have been serialized). But "does not actually intersect" is the zero-margin form of the same constraint and needs no clearance value, so unlike the margin it is expressible at the spec layer. Validation enforces the invariant; the clearance stays a knob for the generator.

Both bundled specs already satisfy it

Audited every bus in both, using the fully-occupied lane groups:

	buses	lanes missing	endpoints not on their lane's SLM site	interior waypoint on a grid point	segment sweeping a grid point
gemini.physical	22	0	0	0	0
gemini.logical	19	0	0	0	0

So check 5 lands clean alongside the other four, and the blast-radius note above is unchanged: the cost is auditing the hand-built Rust fixtures, not the shipped data.

[weinbe58]

Correction to check 3: uniform displacement is too strict

Check 3 above says "uniform src→dst displacement across the whole group (the AOD single-shift invariant)". That is wrong as a hardware rule, and adopting it at the spec layer would reject buses the machine can perform.

Per @weinbe58: the requirement is only that the displacements be AOD-compatible. An AOD is a crossed pair of deflectors — traps sit at the Cartesian product of its x-tones and y-tones, and each tone is swept independently. So a transport is realizable exactly when it is separable and order-preserving:

• every atom's x-displacement depends only on which column it occupies, and its y-displacement only on its row — an atom may not leave its own tone;
• tone counts match end to end — a transport cannot add or drop a tone midway;
• tones keep their relative order, since two frequencies cannot pass through each other.

Uniform translation is a special case of this. Compressing or expanding a rectangle gives every column a different displacement and is still one AOD operation.

Why this matters concretely

I had implemented the uniform version in the Python builder first, and it rejected three buses that are perfectly legal:

bus	uniform rule	AOD rule
word pitch 1 µm → 2 µm (x-expansion)	rejected	accepted
site pitch 10 µm → 30 µm	rejected	accepted
rows y=[0,10] → y=[0,20] (y-expansion)	rejected	accepted
reversal [0,1,2,3] → [7,6,5,4]	rejected	rejected — tones cross
column swap [0,1] → [5,4]	rejected	rejected — atom leaves its tone
shear (one row swaps, the other does not)	rejected	rejected
two columns collapsing onto one	rejected	rejected — drops a tone

So check 3 should read: the bus's atom set must map separably and order-preservingly from source tones to destination tones.

Algorithm

Now implemented in Python as ZoneBuilder._check_aod_compatible, called from add_word_bus and add_site_bus. It takes one (src_position, dst_position) pair per atom the bus carries — for a word bus that is every site of every src word, for a site bus every participating word — and:

src_x, src_y = sorted unique source x / y
dst_x, dst_y = sorted unique destination x / y
require len(src_x) == len(dst_x) and len(src_y) == len(dst_y)
for (sx, sy) -> (dx, dy):
    require (dx, dy) == (dst_x[rank of sx in src_x], dst_y[rank of sy in src_y])

The rank lookup is what enforces order preservation; the equality is what enforces separability. Building the pair list from every atom rather than sampling site 0 / word 0 is what closes the gap noted in the original post.

Note the validator and the path search are allowed to disagree

ZoneBuilder._compute_paths searches one reference path and applies its deltas to every lane, so it handles rigid translations only. A compression bus is therefore accepted by the hardware rule and then declined by the search — it warns and emits no paths, leaving the bus legal but unrouted, which §6 of QuEraComputing/bloqade-internal#445 already describes as a valid state. @weinbe58 confirmed giving up there is fine.

That asymmetry is deliberate and only runs one way: the validator answers can the hardware do this, the search answers can I find a route. Worth stating in the Rust implementation so nobody later "fixes" the validator to match the search.

Blast radius unchanged

The audit table in the original post still holds. Separability is strictly weaker than uniformity, so the bundled specs — which passed the uniform check on every bus — pass this one too.