Skip to content

Prove CZ stages infeasible when they can't fit (slot capacity / reachability) #1084

Open

Description

@weinbe58

Problem

When a CZ stage cannot be placed at all, NoHome reports it as a plain UNSOLVABLE with no proof. NoReturnStrategyBase then raises PlacementError ("could not route atoms to valid partner sites"), which nothing catches, so the compile fails. The message doesn't say whether:

  • the request is impossible, e.g. more CZ pairs than there are usable entangling slots; or
  • the heuristic gave up on a stage that another strategy might place.

Nothing splits a CZ layer that doesn't fit into rounds that do.

Near term: prove genuinely impossible stages

At the CZ pulse, every pair must occupy its own entangling slot (a site of an entangling word pair) with both halves free. External atoms (blocked) are immovable, so a slot with a blocked half can never be used. Two necessary conditions follow, and either one failing is a sound proof that the stage has no plan:

  1. Capacity: the number of CZ pairs must not exceed the number of slots with neither half blocked. The count includes pairs already in an entangling zone. With overlapping entangling pairs the count is an upper bound on capacity, so the check can only say "impossible" when that's true.
  2. Reachability: each pair needs at least one such slot whose halves its two qubits can reach, one each, ignoring every other atom.

When either fails:

  • return UNSOLVABLE with Proof.NO_PLAN (SolveResult::proven_unsolvable);
  • have PlacementError say why, e.g. "provably impossible: 5 CZ pairs but only 4 entangling slots are free".

The check is cheap: a slot count and distance lookups, done once per stage before any candidate is built.

Notes:

  • Relative to blocked, like Push and Rotate's proofs. With block_spectators, it means "impossible with the spectators left in place".
  • What it can't prove: stages that fail only because the stage's own atoms occupy the free slots. Those stay unproven UNSOLVABLE.

Related: a clash in the rule's candidate is an error, not unsolvable

Under MoverSelection.RULE, a rule candidate whose mover lands on another stage atom is sent to the router unchecked. The router rejects it as a malformed target (DuplicateTargetLocation), so the placement errors instead of reporting the stage unplaceable. RANKED and ROUTE_ALL drop such a candidate instead (#1083).

Later: split CZ layers that don't fit

Instead of failing, a stage that genuinely doesn't fit could be split into rounds that each fit. That's a scheduling-level design change, separate from the above.

Context: review of #1083 (Epic 4 phases 2–3), crates/bloqade-lanes-search/src/placement/nohome.rs.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions