Skip to content

nav: prove klickweg connectivity via the sanctioned Core brick (ruff #61 · lance-graph #669/#670/#673)#89

Merged
AdaWorldAPI merged 1 commit into
mainfrom
claude/nav-connectivity-core-brick
Jul 8, 2026
Merged

nav: prove klickweg connectivity via the sanctioned Core brick (ruff #61 · lance-graph #669/#670/#673)#89
AdaWorldAPI merged 1 commit into
mainfrom
claude/nav-connectivity-core-brick

Conversation

@AdaWorldAPI

Copy link
Copy Markdown
Owner

What & why

ruff #61 landed the harvest half of the navigation-topology arm — ruff_spo_triplet::Predicate::NavigatesTo (the agnostic "screen→screen" SPO fact, count 64→65) + the WinForms navigates_to harvester. Its Core consumer halfcontract::class_view::{screens_reachable_from, nav_is_fully_connected} (lance-graph #670, strengthened to reached == screens by codex P2 in #673) — is now the sanctioned brick for the exact connectivity check op-nexgen had hand-rolled as a live scripts/nav-crawl.sh BFS.

This migrates op-nexgen's klickweg connectivity onto that brick — the same off-brick → sanctioned-brick move already done for WideFieldMask::from_universe_present (#669).

The Lego-kit wiring

  • SCREEN_UNIVERSE is the single source of screen order; a screen's position is its index there, shared by both the mask universe and the ComputeEdge positions, so the two can never drift.
  • served_screens_mask() mints the screens universe via the sanctioned WideFieldMask::from_universe_present (carries the 256-field SoC guard), never an ad-hoc from_positions.
  • NAV_EDGES reuses the Core ComputeEdge shape (the jump half of the topology kit) — one more brick, not a parallel edge type.
  • klickweg_is_connected() = nav_is_fully_connected(NAV_ROOT, NAV_EDGES, served):
    • asserted at boot (WARN, non-fatal — a disconnected nav graph is a level-editor bug, not a reason to refuse to serve);
    • proven at test time (klickweg_is_fully_connected_via_core_brick) — the compile-time counterpart to the live crawl.
  • nav_edges_match_static_table cross-checks the static NAV_EDGES manifest against the live nav_edges derivation so it can't silently drift; screen_universe_matches_routes proves every declared screen is actually routed.

Compile-safety of ruff #61

The additive Predicate::NavigatesTo variant is compile-safe for op-nexgen — the crate consumes ModelGraph / Triple / expand / Field / Model / Function, never an exhaustive match on Predicate. Verified.

Tests

  • op-server nav:: 7/7 green (2 new connectivity/drift tests + 1 route-coverage test, 4 pre-existing).
  • Zero new warnings vs main — the 5 pre-existing nav.rs dead-code/doc warnings are unchanged (confirmed by clippy on pristine main).

🤖 Generated with Claude Code


Generated by Claude Code

…-graph #670/#673)

The board's navigation connectivity ("does every pipe lead somewhere,
is the level fully connected" — the Mario-World-editor validator) was
only verified by the live `scripts/nav-crawl.sh` BFS. ruff #61 landed the
harvest half of the navigation-topology arm (`ruff_spo_triplet::
Predicate::NavigatesTo` + the WinForms `navigates_to` harvester), and its
Core consumer half — `contract::class_view::{screens_reachable_from,
nav_is_fully_connected}` (lance-graph #670, strengthened to reached ==
screens by codex P2 in #673) — is now the sanctioned brick for exactly
this check.

This migrates op-nexgen's klickweg connectivity onto that brick, the same
off-brick → sanctioned-brick move already done for `WideFieldMask::
from_universe_present` (#669):

- `SCREEN_UNIVERSE` is the single source of screen order; a screen's
  position is its index there, shared by both the mask universe and the
  `ComputeEdge` positions so the two cannot drift.
- `served_screens_mask()` mints the `screens` universe via the sanctioned
  `WideFieldMask::from_universe_present` (carries the 256-field SoC guard),
  never an ad-hoc `from_positions`.
- `NAV_EDGES` reuses the Core `ComputeEdge` shape (jump half of the
  topology Lego kit) — one more brick, not a parallel edge type.
- `klickweg_is_connected()` = `nav_is_fully_connected(NAV_ROOT, NAV_EDGES,
  served)`; asserted at boot (WARN, non-fatal — a disconnected nav graph
  is a level-editor bug, not a reason to refuse to serve) and proven at
  test time (`klickweg_is_fully_connected_via_core_brick`), the
  compile-time counterpart to the live crawl.
- `nav_edges_match_static_table` cross-checks the static `NAV_EDGES`
  manifest against the live `nav_edges` derivation so it can never
  silently drift; `screen_universe_matches_routes` proves every declared
  screen is actually routed.

ruff #61's additive `Predicate::NavigatesTo` variant (64→65) is
compile-safe for op-nexgen — the crate consumes `ModelGraph/Triple/
expand/Field/Model/Function`, never an exhaustive `match` on `Predicate`.

Tests: op-server nav:: 7/7 green. No new warnings vs main (the 5
pre-existing nav.rs dead-code/doc warnings are unchanged).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01U9t3fRwXmPC6tCpMtnfTrM
@AdaWorldAPI AdaWorldAPI merged commit 8e52475 into main Jul 8, 2026
@cursor

cursor Bot commented Jul 8, 2026

Copy link
Copy Markdown

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_50f12fa2-a6f1-4ea4-8c6f-fcd95f2a0788)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants