You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Give the device one owner of the answer to "what heavy work may run now, and what is the rider
looking at" — CoreMode — and delete the four surviving copies of that answer.
This issue does not move any host onto App::run_pass, does not touch HostCommand/HostEvent,
and does not delete the board's arena bookkeeping. Those are S6 and (for the arena) never — see
"What is deliberately not deleted".
Read this first: the S5 row is stale in three places
S5 — Mode machine (after FS5); delete freeze/arena/search-arm modules. Gate: union of ring-module
tests green; on-glass soak
It was written against develop at e7f1b11c. Three of its four clauses no longer describe the
code. All line numbers and facts below are origin/develop at 3943301e (the #1486 merge).
1. "delete … search-arm …" understates it: link_gate.rs is almost entirely dead, not just its
search arm. The epic §1.2 lists TransferGate as the owner of "one transfer across two wires".
That is no longer true. TransferGate::claim, release, holder, in_flight, busy and the whole GateOwner enum have zero production callers anywhere in the repository. FS5/FS7.5 moved
one-transfer-at-a-time into the flat engine, which answers busy carrying the live RequestId
(firmware/obc-link/src/flat/engine.rs:1462), and scoped the #1039 per-wire teardown rule to Engine::on_link_up / on_link_lost (firmware/obc-fw-nrf54l/src/flat_store.rs:1179–1195). The
only surviving call sites of the entire module are begin_search / end_search in firmware/obc-fw-nrf54l/src/ride.rs:371, 378, 388, 1830. search_live() has no production
caller either — the board computes that fact a third way, from its own nav_run.is_some()
(ride.rs:1063). link/mod.rs:13 still documents an Armed type that no longer exists.
Consequence: begin_search() can no longer fail for a streaming transfer, because in_flight() is
never true. The nav ⊥ usb rule survives only because ArenaGate refuses claim_nav while the USB
arm is out — and the rider is then told "the scratch arena is busy" by a path whose sibling error
string still says "a cable transfer holds the store". S5 deletes link_gate.rs outright, and
the rule it was carrying moves to CoreMode where it can be stated once.
2. "delete … arena …" contradicts the #1433 amendment and would move tested rules into an
untested crate. The amendment (which post-dates the row) says: "The board arena remains a physical
resource. The board executor maps an admitted effect to an arena claim."ArenaGate answers a
question CoreMode has no business answering: who holds the block right now, at per-frame
granularity, and whose bytes are in it (ArenaInit::Skippable, the ~131 KB-per-frame memset
skip). A render span is a claim inside one pass; it is not a product mode. arena_gate.rs also lives
in obc-app precisely because the board crate has no test harness in CI, and its nine tests pin
the memset-skip cliff and the NotHeld loudness.
What S5 does take from arena_gate.rs is the proof-token inputs. Today MapQuiesced::prove(freeze_active, base_draws_map) and TransferReady::prove(transfer_screen_up, search_live) let any caller assemble a proof out of its
own copies of the facts — and ride.rs:1066 does exactly that. After S5 the only mint is CoreMode.
3. "Mode machine" as a fresh state machine is the wrong shape; this is a collapse, not a
build. S2 already gave the planning lifecycle to NavigatorMachine. What is left over is
genuinely small: two per-family "the executor holds the nav arm" levels, one transfer level, and one
level→edge bit for the banner. The value of S5 is not a new machine — it is that after it there is
exactly one place that says a search is live, where today there are four:
Copy
Where
Written by
RerouteFreeze::{route_live, detour_live}
firmware/obc-app/src/reroute_freeze.rs:78–86
NavigatorMachine (since S2)
TransferGate::searching
firmware/obc-app/src/link_gate.rs:77
ride.rs:371/378/388/1830
ArenaGate::owner == Nav
firmware/obc-app/src/arena_gate.rs
firmware/obc-fw-nrf54l/src/arena.rs
nav_run: Option<NavRun>
firmware/obc-fw-nrf54l/src/ride.rs:759
the ride loop
The epic's own §2.1 sentence — "The fact 'a route search is live' exists as three independent
flags" — undercounted by one.
The capability contract: Capabilities::calculate and DeviceFacts
(firmware/obc-app/src/device_core/shared.rs:190–360). DC2 already reads CoreMode admission as
a fact — DeviceFacts::heavy_operations is documented as "CoreMode's verdict on heavy work"
and stage 12 is named Admission (device_core/pass.rs:676–700). S5 is what makes that
documentation true.
The three exclusion rules and why each is a product rule: firmware/obc-app/src/arena_gate.rs:12–20.
The read surface (this is what must not change behaviour)
App method
app.rs
Production readers
reroute_freeze_active()
1196
ride.rs:2216 (skip the map redraw), app.rs:778 (pause the matcher), app.rs:3229 (banner), app.rs:3240, app.rs:3247
nav_arena_precondition()
1213
ride.rs:374
map_transfer_card_up()
2160
ride.rs:1042/1054/1066
take_dirty()'s freeze edge
3271
ride.rs:2225 (overlay-only frame)
plan_in_flight()
1205
none. Tests only.
TransferReady has a second mint with no App in scope: main.rs:803, the card-recovery USB boot
path (spawn_map_recovery_usb) — no ride loop, no renderer, no planner exists there. It needs a
named constructor, not a re-derivation.
What already exists and must be used, not rebuilt
NavigatorMachine::live_family() (navigator.rs:352) — not the same fact as plan_live(). live is "an operation is current"; plan_live() is "the executor holds the nav arm". They
diverge across the whole cancel window on purpose (admit_intent's doc, navigator.rs:283–290):
a cancellation the executor has not been handed yet has not stopped anything. CoreMode must be
fed by the second fact, never the first.
ExternalFacts::note_transfer / TransferState (device_core/shared.rs:428–436, 584–586) — the
fact vocabulary already exists; nothing in production feeds it yet.
Stage 12 stage_admission (device_core/pass.rs:686–700) — already computes heavy_operations: matches!(self.pass.transfer, TransferState::Idle). It does not account for a
live search, so NavigatorCapabilities::plan_detour stays advertised mid-search today.
App::set_map_transfer (ride.rs:1053) — the board already reports the map transfer's level
every pass. No new board feeder call is needed.
Locked design
One component, CoreMode, in firmware/obc-app/src/device_core/core_mode.rs. It holds four
bits and nothing else:
pubstructCoreMode{route_search:bool,// the executor holds the nav arm for a route plandetour_search:bool,// …for a detour plantransferring:bool,// a bulk transfer holds the store (latest level)engaged_shown:bool,// the freeze's level→edge converter}
Two search levels, not a family tag. The arm is one block, so it stays out until every family
that took it is done, and a tag would have to pick a winner (Scratch arena: three-way RAM share (render scratch / nav / USB staging) + 25 KB render-cap growth #1146; reroute_freeze.rs:82–86 and
the the_freeze_outlives_the_first_of_two_live_runs test). Two live runs is reachable through the
legacy drain's cancel window, so the union is not speculative.
The visible mode carries no payload:
pubenumModeState{Free,Searching,Transferring}
The epic sketched Searching { family } and Transferring { wire }. Both payloads are
deleted from the design, per the speculative-capability rule:
the banner is one family-independent string (Msg::MapRecalculating, app.rs:3230) — no
consumer of the family exists;
Searching outranks Transferring when both levels are set, and the ranking decides only what
the rider is told — it never decides admission, which reads the levels.
CoreMode is a level, never latched, and never a second copy.route_search / detour_search are written only from NavigatorMachine's existing three transitions — next_plan_effect (engage), note_answer (release), note_cancel_delivered (release) — which is
exactly where RerouteFreeze is written today. transferring is written only from App::set_map_transfer. Nothing else may write any of them.
The freeze becomes a derived view.frozen = mode.searching() && base_draws_map(). Every App reader keeps its signature and its behaviour: reroute_freeze_active(), reroute_banner_rows(), overlay_active(), and the take_dirty()
edge. RerouteFreeze as a type is gone.
CoreMode is the only mint for the arena proofs.MapQuiesced::prove(bool, bool) and TransferReady::prove(bool, bool) lose their public two-argument constructors:
App::nav_arena_precondition() mints MapQuiesced from mode.searching() || !base_draws_map();
a new App::usb_stage_precondition() mints TransferReady from map_transfer_card_up() && !mode.searching(), and ride.rs:1063–1066 stops computing search_live from nav_run;
TransferReady::recovery_boot() is the one named escape for main.rs:803, documented as "no
ride loop, no renderer and no planner exist on this boot path".
ArenaGate, ArenaOwner, ArenaInit and the board's arena.rs are untouched.
Stage 12 reads the mode.stage_admission sets heavy_operations: self.mode.admits_heavy() instead of re-deriving it from pass.transfer.
This is the one deliberate behaviour change in the pass: plan_route, plan_detour and dfu.install now also withdraw while a search is live, which is what DC2 already documents. pass.transfer stops being a second store of the transfer level; ExternalFacts::transfer() is
consumed at stage 2 straight into CoreMode.
The banner's drawing half moves to screen/vocab/chrome.rs, beside the other overlay chrome. PlanFamily moves to navigator.rs, its actual owner.
No new task, no atomics, no allocator, no event bus.CoreMode is plain data inside App, &mut for the same reason ArenaGate is: the ride loop is the sole switcher.
What is deliberately not deleted
arena_gate.rs's ownership machine and ArenaInit (reason 2 above). The row's word "arena" is
answered by re-sourcing the proofs, not by deleting the module.
Anything in HostCommand / HostEvent / compat.rs / migration.rs (S6).
The three overlay edge converters are not merged here — that is S4 S4 — Replace manual dirty mirrors with declared render keys #1447, after S6. S5 removes
one of the three (RerouteFreeze::engaged_shown becomes CoreMode::engaged_shown, same bit, one
owner); InputPlane::overlay_was_active and UiRuntime::overlay_edge stay.
Target files
firmware/obc-app/src/device_core/core_mode.rs # NEW — the component and its tests
firmware/obc-app/src/device_core/mod.rs # + the module and its re-exports
firmware/obc-app/src/device_core/pass.rs # stage 2 feeds the transfer level; stage 12 reads the mode
firmware/obc-app/src/navigator.rs # + PlanFamily; the three transitions write CoreMode
firmware/obc-app/src/app.rs # the freeze readers derive; the two proof mints
firmware/obc-app/src/arena_gate.rs # − the two public `prove` constructors; + `recovery_boot`
firmware/obc-app/src/screen/vocab/chrome.rs # + the Recalculating banner drawing
firmware/obc-app/src/lib.rs # − the link_gate module and its re-exports
firmware/obc-app/src/reroute_freeze.rs # DELETED
firmware/obc-app/src/link_gate.rs # DELETED
firmware/obc-fw-nrf54l/src/ride.rs # − begin_search/end_search/nav_run-as-search-fact
firmware/obc-fw-nrf54l/src/link/mod.rs # − TRANSFER_ACTIVE and the stale `Armed` doc line
firmware/obc-fw-nrf54l/src/main.rs # the recovery mint
firmware/obc-app/tests/detour_flow.rs # the integration pins follow the seam
tools/check_screen_vocabulary.py # + the banner landmark
Implementation steps
Add CoreMode with its four levels, ModeState, admits_heavy(), searching(), take_engaged_edge(base_draws_map). Port reroute_freeze.rs's five tests onto it first, with
their comments, before anything is deleted (the epic's rule).
Move PlanFamily into navigator.rs. Make NavigatorMachine's three transitions write CoreMode instead of RerouteFreeze. Keep live_family() and plan_live() distinct — do not
collapse them; add a test that pins the divergence across the cancel window.
Move the banner drawing into screen/vocab/chrome.rs, add its landmark to tools/check_screen_vocabulary.py, and delete reroute_freeze.rs. App::render_overlay, reroute_banner_rows and overlay_active keep their signatures.
Feed transferring from App::set_map_transfer and from ExternalFacts::transfer() at stage 2.
Delete PassState::transfer.
Re-point stage 12's heavy_operations at CoreMode::admits_heavy(). Re-read the conformance
traces that assert on plan_detour / dfu.install — this arm changes what they see.
Replace the two prove constructors with App::nav_arena_precondition() / App::usb_stage_precondition() and TransferReady::recovery_boot(). Update ride.rs:1063–1066
and main.rs:803.
Delete link_gate.rs, its lib.rs module + re-exports, link::TRANSFER_ACTIVE, the four begin_search/end_search call sites, and fix link/mod.rs:13's stale Armed line. nav_run
stays as the board's planner run handle — it must stop being read as "a search is live".
Delete App::plan_in_flight (no production caller) or, if a test genuinely needs it, move it
behind #[cfg(test)]. State which, and why, in the PR.
Re-measure every resource value against the table below and itemize any increase.
Deletions
Must land in the same PR that replaces them:
firmware/obc-app/src/reroute_freeze.rs — the whole file (297 lines).
firmware/obc-app/src/link_gate.rs — the whole file (268 lines), including GateOwner, claim, release, holder, in_flight, busy, begin_search, end_search, search_live and the seven
tests, of which the four transfer-owner tests are testing code nothing calls.
firmware/obc-app/src/lib.rs's pub mod link_gate; and pub use link_gate::{GateOwner, TransferGate};
(lib.rs:49, 93).
firmware/obc-fw-nrf54l/src/link/mod.rs's TRANSFER_ACTIVE static and its doc block.
The four TRANSFER_ACTIVE.begin_search() / .end_search() call sites in ride.rs.
ride.rs's let search_live = nav_run.is_some(); pair (1063–1065).
MapQuiesced::prove and TransferReady::prove as public constructors.
PassState::transfer (device_core/pass.rs:229).
App::plan_in_flight (app.rs:1205).
LOC honesty.#1397 §3.1 budgets Area A at −230 production lines. That estimate assumed the
mode machine would absorb arena_gate.rs's ownership half, which this slice does not do, and did not know link_gate.rs's transfer half was dead. Expect roughly −250 to −400 production
lines net: two files (565 lines, ~230 of them tests) leave, ~150 arrive as core_mode.rs plus ~60
of relocated banner drawing. A PR that lands net-positive here is probably leaving a second copy of
a level behind. Update the epic's Area A row rather than bending the slice to it.
Required tests
Port before deleting. Focused, not exhaustive — the union of the two dying modules' suites, minus
the four transfer-owner tests whose subject is gone.
CoreMode (ported from reroute_freeze.rs)
The freeze follows the search and the base screen: nothing frozen at rest, nothing frozen on a
chrome base, engaged over a map base.
Releasing twice is harmless and a new search re-engages.
The repaint edge follows the engaged level, not the search's start edge — the regression where a
host keyed on the start edge paints nothing for the whole search.
CoreMode (new, and each one is a copy this slice removes)
admits_heavy() is false while a search is live — the axis stage 12 did not have.
admits_heavy() is false while a transfer streams, and true again when it ends.
ModeState reports Searching when both levels are set, and the ranking never changes what admits_heavy() answers.
A MapQuiesced cannot be minted over a map base with no search live; a TransferReady cannot be
minted while a search is live. (The arena_gate.rs precondition tests, re-pointed at the new mint.)
firmware/obc-app/tests/overlay_plane.rs and tests/dirty.rs unchanged and green.
firmware/obc-app/tests/detour_flow.rs's freeze/precondition assertions (lines 287–307, 385,
423–448) keep their meaning through the new seam.
Conformance (obc-host-core)
All DC1 scenarios × 5 runners green with the same disposition table. A new differing cell is a
blocking failure — except where step 5 above legitimately changes a capability arm, in which case
the trace is re-read and the change is stated in the PR, not absorbed.
Every LegacyOwned row still names a later owner. No row is retired by this slice.
On-glass soak
The exit criterion the row names. The board is available; the bootloader prerequisite (#617) and the
flash-twice quirk apply.
Why it cannot be skipped: on a shipping build a refused arena claim degrades silently — the
frame skips its map redraw and tries again. The whole failure mode this slice must not introduce is
a map that never redraws again, and no host test can see it.
Build and rig
cd firmware/obc-fw-nrf54l
cargo run --release --features debug-uart # default profile: has_nav + the USB device plane
debug-uart swaps the sensors for the VCOM feed so a ride can be driven headlessly. HWFC must be
OFF in the Board Configurator or host→device injection is silently ignored. Drive with pyserial at
115200 on /dev/cu.usbmodem*133 (rtscts=False); stty+printf does not work. Script lives in the
session scratchpad under a unique prefix (s5_soak.py) per the parallel-agent scratchpad rule.
Liveness probe first, every run. The J-Link CDC wedges silently: write() succeeds, RTT keeps
flowing, nothing lands, and a blind script then "passes" every step. Snapshot the RTT log size, send
six taps, sleep 2 s, re-check. Zero growth = wedged; only a physical DK power-cycle clears it.
A — the freeze window over a map base (render ⊥ nav), ≥50 cycles, ~30 min — automatable
The window this whole mechanism exists for is Back out of the planning spinner while the planner is
still running, which is the only way a map base lands under a live search.
Stream F <lat> <lon> fixes at ~1 Hz in small steps (teleport rejection).
BackHold → Ride menu → K t 1 to Detour → press → rejoin chooser → press (posts the plan and
pushes the spinner) → immediatelyK b d/K b u to pop the spinner while the planner runs.
Observe, per cycle, in RTT: nav plan: start, then the banner's single overlay repaint, then —
on the pass the answer lands — exactly one full map repaint (the pending_map_redraw
catch-up).
Repeat ≥50 times, interleaving: a cancel while planning, a plan started from the menus (chrome
base — must freeze nothing and raise no banner), and a plan whose answer is NoPath.
Pass: every cycle shows the start → banner → answer → full-repaint sequence; zero arena: lines
reporting Busy/NotHeld for Render or Nav; zero plan answers reporting a failure tier that is not
a genuine NoPath; no cycle ends with the map quiet for more than one wake after the answer.
B — nav ⊥ usb and render ⊥ usb, ~20 min — semi-automatable (needs a hand on the cable)
Cable in J3, an active route loaded, ride running.
Start a map upload. The transfer card comes up; render ⊥ usb holds by construction.
During the upload: BackHold → Detour → press.
Then end the upload and repeat the plan.
Pass: the plan during the upload is refused before the planner arms, and the refusal message
names the transfer — not "the scratch arena is busy", and not a NoPath. After the upload ends,
the same input plans normally. arena: USB write-combining arm granted / reclaimed appear exactly
once each per upload.
C — the stuck-freeze soak, 60 min — automatable
A continuous ride with a plan cycle every ~60 s and a periodic Z <mpp> zoom nudge. The script
asserts that after every freeze release a map render line appears within two wakes, and that deep_ride_high_water never crosses deep_ride_margin_min.
Pass: 60 uninterrupted minutes, zero missed catch-ups, no WDT reset, no boot fault.
Genuinely human, and flagged as such
Confirming the banner is legible and correctly placed over a real frozen map on the reflective
panel. RTT proves the rows were pushed; only an eye proves it reads as "recalculating" rather than
"wedged". (The pixel geometry itself is proven off-device by obc-sim --png --freeze and V0's
manifest — the on-glass part is the panel, not the pixels.)
Confirming the map catches up whole when the freeze lifts (no torn or half frame).
Plugging and unplugging the cable for scenario B.
The physical DK power-cycle if the VCOM CDC wedges.
Record the result in the PR the way #1146 P2's baseline note did — that note still carries "the on-glass soak is pending" for this exact mechanism. This slice is what closes it.
Resource limits
Baseline is firmware/tools/resource_baseline.json at 3943301e (re-pinned by PR #1486). Report
every value; itemize any increase.
Item
Baseline
Rule
size_of::<App>() (compile_time_allocations.app)
50,928 B
Must not grow. Three bools leave RerouteFreeze; four arrive in CoreMode; expect flat or −8.
Board resident (measured_resident)
320,616 B
Must not grow. link::TRANSFER_ACTIVE (2 B) leaves.
resident_ram_max
320,688 B
Ceiling.
uninit_max
132,096 B
Unchanged — no arm is touched.
arena_total / render / nav / usb
131,072 / 131,072 / 97,344 / 131,072 B
Unchanged, to the byte. An arm change is out of scope for this slice.
full_frame_sized_writable_count
2
Unchanged (FB + ARENA).
poll_frame_measured
9,792 B
Limit 12,288 B.
task_frame_measured
1,100 B
Limit 8,192 B.
residual_stack_measured
38,808 B
Floor 38,808 B.
boot_chain_measured_pinned_host
13,768 B
Ceiling 24,576 B; headroom floor 4,096 B.
deep_ride_high_water
37,016 B
Margin floor 8,704 B.
measured_flash
1,524,676 B
A record, not a gate (see the file's _flash_note_1096). Re-pin from this PR's embedded run and state the delta.
No allocator, no new task, no atomics in CoreMode, no combined Effect/Outcome/Intent enum,
no event bus (#1433 §14, §16).
Verification
obc test -p obc-app
obc test -p obc-host-core
obc test fixtures -p obc-host-core
cargo clippy -p obc-app -p obc-host-core --all-targets -- -D warnings
obc check fmt device board
obc suites check # tools/check_screen_vocabulary.py gains a landmark
python3 docs/build_docs.py --check-links # only if the arena/freeze rules are described in docs/content
Plus the board build and the soak above:
cd firmware/obc-fw-nrf54l && cargo run --release --features debug-uart
Definition of done
CoreMode exists, holds the four levels, and is the only writer and the only reader
source for "a search is live" and "a transfer is live".
The board no longer derives "a search is live" from nav_run, and TRANSFER_ACTIVE is gone.
MapQuiesced and TransferReady can only be minted from CoreMode, plus the one named
recovery-boot escape.
Stage 12 reads CoreMode::admits_heavy(); heavy capabilities withdraw for a live search as
well as a live transfer, and the conformance disposition table is unchanged except where that
arm is stated to change it.
V0's 270-frame manifest is byte-identical; obc-sim --png --freeze still draws the banner.
Every resource value re-measured and reported; nothing in the arena moved.
Open questions for the implementer to settle in review
Does CoreMode need an Installing level?shared.rs:212 claims admission is withdrawn "while a transfer streams or an install is armed", but the code checks only the transfer,
and an armed install reboots immediately. Deliberately not locked above: adding a level for a
window that ends in a reboot looks like provisioning for an operation that never happens. If the
answer is no, fix the sentence in shared.rs in this PR.
How wide is the transfer level? Today the only thing that reports a streaming transfer is the map transfer card. A route, trip or weather upload streams without one. That is a gap in the fact, not in CoreMode — the flat engine knows the truth and S6 wires ExternalFacts::note_transfer from it. Confirm this is left as a stated gap rather than papered
over with a fourth derivation.
nav_run's remaining role. It stays as the board's planner-run handle. Is there a cheap way
to make "read nav_run as a search fact" impossible again later — a newtype, or does the CoreMode-only mint already close it?
Parent epic: #1397
Program tracker: #1448
Program position: App core, S5 (mode machine)
Start gates:
and is the single writer of
RerouteFreeze.flat store). Met, and it is load-bearing here for a reason the row could not have known: FS5 is
what made
TransferGate's transfer half dead code. See the re-scope below.Goal
Give the device one owner of the answer to "what heavy work may run now, and what is the rider
looking at" —
CoreMode— and delete the four surviving copies of that answer.This issue does not move any host onto
App::run_pass, does not touchHostCommand/HostEvent,and does not delete the board's arena bookkeeping. Those are S6 and (for the arena) never — see
"What is deliberately not deleted".
Read this first: the S5 row is stale in three places
The row in #1397 reads:
It was written against
developate7f1b11c. Three of its four clauses no longer describe thecode. All line numbers and facts below are
origin/developat3943301e(the #1486 merge).1. "delete … search-arm …" understates it:
link_gate.rsis almost entirely dead, not just itssearch arm. The epic §1.2 lists
TransferGateas the owner of "one transfer across two wires".That is no longer true.
TransferGate::claim,release,holder,in_flight,busyand the wholeGateOwnerenum have zero production callers anywhere in the repository. FS5/FS7.5 movedone-transfer-at-a-time into the flat engine, which answers
busycarrying the liveRequestId(
firmware/obc-link/src/flat/engine.rs:1462), and scoped the #1039 per-wire teardown rule toEngine::on_link_up/on_link_lost(firmware/obc-fw-nrf54l/src/flat_store.rs:1179–1195). Theonly surviving call sites of the entire module are
begin_search/end_searchinfirmware/obc-fw-nrf54l/src/ride.rs:371, 378, 388, 1830.search_live()has no productioncaller either — the board computes that fact a third way, from its own
nav_run.is_some()(
ride.rs:1063).link/mod.rs:13still documents anArmedtype that no longer exists.Consequence:
begin_search()can no longer fail for a streaming transfer, becausein_flight()isnever true. The
nav ⊥ usbrule survives only becauseArenaGaterefusesclaim_navwhile the USBarm is out — and the rider is then told
"the scratch arena is busy"by a path whose sibling errorstring still says
"a cable transfer holds the store". S5 deleteslink_gate.rsoutright, andthe rule it was carrying moves to
CoreModewhere it can be stated once.2. "delete … arena …" contradicts the #1433 amendment and would move tested rules into an
untested crate. The amendment (which post-dates the row) says: "The board arena remains a physical
resource. The board executor maps an admitted effect to an arena claim."
ArenaGateanswers aquestion
CoreModehas no business answering: who holds the block right now, at per-framegranularity, and whose bytes are in it (
ArenaInit::Skippable, the ~131 KB-per-framememsetskip). A render span is a claim inside one pass; it is not a product mode.
arena_gate.rsalso livesin
obc-appprecisely because the board crate has notestharness in CI, and its nine tests pinthe memset-skip cliff and the
NotHeldloudness.What S5 does take from
arena_gate.rsis the proof-token inputs. TodayMapQuiesced::prove(freeze_active, base_draws_map)andTransferReady::prove(transfer_screen_up, search_live)let any caller assemble a proof out of itsown copies of the facts — and
ride.rs:1066does exactly that. After S5 the only mint isCoreMode.3. "Mode machine" as a fresh state machine is the wrong shape; this is a collapse, not a
build. S2 already gave the planning lifecycle to
NavigatorMachine. What is left over isgenuinely small: two per-family "the executor holds the nav arm" levels, one transfer level, and one
level→edge bit for the banner. The value of S5 is not a new machine — it is that after it there is
exactly one place that says a search is live, where today there are four:
RerouteFreeze::{route_live, detour_live}firmware/obc-app/src/reroute_freeze.rs:78–86NavigatorMachine(since S2)TransferGate::searchingfirmware/obc-app/src/link_gate.rs:77ride.rs:371/378/388/1830ArenaGate::owner == Navfirmware/obc-app/src/arena_gate.rsfirmware/obc-fw-nrf54l/src/arena.rsnav_run: Option<NavRun>firmware/obc-fw-nrf54l/src/ride.rs:759The epic's own §2.1 sentence — "The fact 'a route search is live' exists as three independent
flags" — undercounted by one.
Source of truth
CoreModein the component table), §10 (platformexecutors), and the amendment's
"CoreMode boundary" paragraph in #1397.
Capabilities::calculateandDeviceFacts(
firmware/obc-app/src/device_core/shared.rs:190–360). DC2 already readsCoreModeadmission asa fact —
DeviceFacts::heavy_operationsis documented as "CoreMode's verdict on heavy work"and stage 12 is named
Admission(device_core/pass.rs:676–700). S5 is what makes thatdocumentation true.
firmware/obc-app/src/arena_gate.rs:12–20.firmware/obc-app/src/reroute_freeze.rs:60–72(Scratch arena: three-way RAM share (render scratch / nav / USB staging) + 25 KB render-cap growth #1146) andnavigator.rs:479–491.RerouteFreeze::take_engaged_edgeandApp::take_dirty(
app.rs:3262–3273).Current code
What holds the state today
RerouteFreeze(3 bools + 6 methods)firmware/obc-app/src/reroute_freeze.rsNavigatorMachine; banner drawing in the same filePlanFamilyBANNER_*,banner_rows,draw_banner)TransferGate+GateOwnerfirmware/obc-app/src/link_gate.rsArenaGate,ArenaOwner,ArenaInitfirmware/obc-app/src/arena_gate.rsMapQuiesced,TransferReadyCoreModenav_runfirmware/obc-fw-nrf54l/src/ride.rs:759The read surface (this is what must not change behaviour)
Appmethodapp.rsreroute_freeze_active()ride.rs:2216(skip the map redraw),app.rs:778(pause the matcher),app.rs:3229(banner),app.rs:3240,app.rs:3247nav_arena_precondition()ride.rs:374map_transfer_card_up()ride.rs:1042/1054/1066take_dirty()'s freeze edgeride.rs:2225(overlay-only frame)plan_in_flight()TransferReadyhas a second mint with noAppin scope:main.rs:803, the card-recovery USB bootpath (
spawn_map_recovery_usb) — no ride loop, no renderer, no planner exists there. It needs anamed constructor, not a re-derivation.
What already exists and must be used, not rebuilt
NavigatorMachine::live_family()(navigator.rs:352) — not the same fact asplan_live().liveis "an operation is current";plan_live()is "the executor holds the nav arm". Theydiverge across the whole cancel window on purpose (
admit_intent's doc,navigator.rs:283–290):a cancellation the executor has not been handed yet has not stopped anything.
CoreModemust befed by the second fact, never the first.
ExternalFacts::note_transfer/TransferState(device_core/shared.rs:428–436, 584–586) — thefact vocabulary already exists; nothing in production feeds it yet.
stage_admission(device_core/pass.rs:686–700) — already computesheavy_operations: matches!(self.pass.transfer, TransferState::Idle). It does not account for alive search, so
NavigatorCapabilities::plan_detourstays advertised mid-search today.screen/vocab/chrome.rs— the shared chrome home V1 V1 — Move shared screen vocabulary out of screen/mod.rs #1442 created.App::set_map_transfer(ride.rs:1053) — the board already reports the map transfer's levelevery pass. No new board feeder call is needed.
Locked design
One component,
CoreMode, infirmware/obc-app/src/device_core/core_mode.rs. It holds fourbits and nothing else:
Two search levels, not a family tag. The arm is one block, so it stays out until every family
that took it is done, and a tag would have to pick a winner (Scratch arena: three-way RAM share (render scratch / nav / USB staging) + 25 KB render-cap growth #1146;
reroute_freeze.rs:82–86andthe
the_freeze_outlives_the_first_of_two_live_runstest). Two live runs is reachable through thelegacy drain's cancel window, so the union is not speculative.
The visible mode carries no payload:
The epic sketched
Searching { family }andTransferring { wire }. Both payloads aredeleted from the design, per the speculative-capability rule:
Msg::MapRecalculating,app.rs:3230) — noconsumer of the family exists;
Engine::on_link_up/on_link_lost), so putting it back on a mode would re-provision a rulethat already has an owner.
SearchingoutranksTransferringwhen both levels are set, and the ranking decides only whatthe rider is told — it never decides admission, which reads the levels.
CoreModeis a level, never latched, and never a second copy.route_search/detour_searchare written only fromNavigatorMachine's existing three transitions —next_plan_effect(engage),note_answer(release),note_cancel_delivered(release) — which isexactly where
RerouteFreezeis written today.transferringis written only fromApp::set_map_transfer. Nothing else may write any of them.The freeze becomes a derived view.
frozen = mode.searching() && base_draws_map(). EveryAppreader keeps its signature and its behaviour:reroute_freeze_active(),reroute_banner_rows(),overlay_active(), and thetake_dirty()edge.
RerouteFreezeas a type is gone.CoreModeis the only mint for the arena proofs.MapQuiesced::prove(bool, bool)andTransferReady::prove(bool, bool)lose their public two-argument constructors:App::nav_arena_precondition()mintsMapQuiescedfrommode.searching() || !base_draws_map();App::usb_stage_precondition()mintsTransferReadyfrommap_transfer_card_up() && !mode.searching(), andride.rs:1063–1066stops computingsearch_livefromnav_run;TransferReady::recovery_boot()is the one named escape formain.rs:803, documented as "noride loop, no renderer and no planner exist on this boot path".
ArenaGate,ArenaOwner,ArenaInitand the board'sarena.rsare untouched.Stage 12 reads the mode.
stage_admissionsetsheavy_operations: self.mode.admits_heavy()instead of re-deriving it frompass.transfer.This is the one deliberate behaviour change in the pass:
plan_route,plan_detouranddfu.installnow also withdraw while a search is live, which is what DC2 already documents.pass.transferstops being a second store of the transfer level;ExternalFacts::transfer()isconsumed at stage 2 straight into
CoreMode.The banner's drawing half moves to
screen/vocab/chrome.rs, beside the other overlay chrome.PlanFamilymoves tonavigator.rs, its actual owner.No new task, no atomics, no allocator, no event bus.
CoreModeis plain data insideApp,&mutfor the same reasonArenaGateis: the ride loop is the sole switcher.What is deliberately not deleted
arena_gate.rs's ownership machine andArenaInit(reason 2 above). The row's word "arena" isanswered by re-sourcing the proofs, not by deleting the module.
App::take_hold_canceland the hold seam (EPIC — Device core: one product kernel, typed effects, thin platform executors #1433 §6).HostCommand/HostEvent/compat.rs/migration.rs(S6).one of the three (
RerouteFreeze::engaged_shownbecomesCoreMode::engaged_shown, same bit, oneowner);
InputPlane::overlay_was_activeandUiRuntime::overlay_edgestay.Target files
Implementation steps
CoreModewith its four levels,ModeState,admits_heavy(),searching(),take_engaged_edge(base_draws_map). Portreroute_freeze.rs's five tests onto it first, withtheir comments, before anything is deleted (the epic's rule).
PlanFamilyintonavigator.rs. MakeNavigatorMachine's three transitions writeCoreModeinstead ofRerouteFreeze. Keeplive_family()andplan_live()distinct — do notcollapse them; add a test that pins the divergence across the cancel window.
screen/vocab/chrome.rs, add its landmark totools/check_screen_vocabulary.py, and deletereroute_freeze.rs.App::render_overlay,reroute_banner_rowsandoverlay_activekeep their signatures.transferringfromApp::set_map_transferand fromExternalFacts::transfer()at stage 2.Delete
PassState::transfer.heavy_operationsatCoreMode::admits_heavy(). Re-read the conformancetraces that assert on
plan_detour/dfu.install— this arm changes what they see.proveconstructors withApp::nav_arena_precondition()/App::usb_stage_precondition()andTransferReady::recovery_boot(). Updateride.rs:1063–1066and
main.rs:803.link_gate.rs, itslib.rsmodule + re-exports,link::TRANSFER_ACTIVE, the fourbegin_search/end_searchcall sites, and fixlink/mod.rs:13's staleArmedline.nav_runstays as the board's planner run handle — it must stop being read as "a search is live".
App::plan_in_flight(no production caller) or, if a test genuinely needs it, move itbehind
#[cfg(test)]. State which, and why, in the PR.Deletions
Must land in the same PR that replaces them:
firmware/obc-app/src/reroute_freeze.rs— the whole file (297 lines).firmware/obc-app/src/link_gate.rs— the whole file (268 lines), includingGateOwner,claim,release,holder,in_flight,busy,begin_search,end_search,search_liveand the seventests, of which the four transfer-owner tests are testing code nothing calls.
firmware/obc-app/src/lib.rs'spub mod link_gate;andpub use link_gate::{GateOwner, TransferGate};(
lib.rs:49, 93).firmware/obc-fw-nrf54l/src/link/mod.rs'sTRANSFER_ACTIVEstatic and its doc block.TRANSFER_ACTIVE.begin_search()/.end_search()call sites inride.rs.ride.rs'slet search_live = nav_run.is_some();pair (1063–1065).MapQuiesced::proveandTransferReady::proveas public constructors.PassState::transfer(device_core/pass.rs:229).App::plan_in_flight(app.rs:1205).LOC honesty. #1397 §3.1 budgets Area A at −230 production lines. That estimate assumed the
mode machine would absorb
arena_gate.rs's ownership half, which this slice does not do, and didnot know
link_gate.rs's transfer half was dead. Expect roughly −250 to −400 productionlines net: two files (565 lines, ~230 of them tests) leave, ~150 arrive as
core_mode.rsplus ~60of relocated banner drawing. A PR that lands net-positive here is probably leaving a second copy of
a level behind. Update the epic's Area A row rather than bending the slice to it.
Required tests
Port before deleting. Focused, not exhaustive — the union of the two dying modules' suites, minus
the four transfer-owner tests whose subject is gone.
CoreMode(ported fromreroute_freeze.rs)chrome base, engaged over a map base.
host keyed on the start edge paints nothing for the whole search.
CoreMode(new, and each one is a copy this slice removes)admits_heavy()is false while a search is live — the axis stage 12 did not have.admits_heavy()is false while a transfer streams, and true again when it ends.ModeStatereportsSearchingwhen both levels are set, and the ranking never changes whatadmits_heavy()answers.MapQuiescedcannot be minted over a map base with no search live; aTransferReadycannot beminted while a search is live. (The
arena_gate.rsprecondition tests, re-pointed at the new mint.)Navigator
live_family()and the mode's search level diverge across the cancel window: the cancel isadmitted,
liveclears, the mode staysSearchinguntilnote_cancel_delivered. This is thearena race Scratch arena: three-way RAM share (render scratch / nav / USB staging) + 25 KB render-cap growth #1146 exists to prevent and nothing pins it today.
Capabilities / pass
plan_route,plan_detouranddfu.installare withdrawn while a search is live.Rendering
obc-sim --png --freezestill renders the banner in its band; V0 V0 — Build the screen-vocabulary verification net #1441's 270-frame manifest isbyte-identical. The banner moving modules must move no pixel.
firmware/obc-app/tests/overlay_plane.rsandtests/dirty.rsunchanged and green.firmware/obc-app/tests/detour_flow.rs's freeze/precondition assertions (lines 287–307, 385,423–448) keep their meaning through the new seam.
Conformance (
obc-host-core)blocking failure — except where step 5 above legitimately changes a capability arm, in which case
the trace is re-read and the change is stated in the PR, not absorbed.
the_conformance_replay_wake_profile_and_pass_costre-pinned.LegacyOwnedrow still names a later owner. No row is retired by this slice.On-glass soak
The exit criterion the row names. The board is available; the bootloader prerequisite (#617) and the
flash-twice quirk apply.
Why it cannot be skipped: on a shipping build a refused arena claim degrades silently — the
frame skips its map redraw and tries again. The whole failure mode this slice must not introduce is
a map that never redraws again, and no host test can see it.
Build and rig
debug-uartswaps the sensors for the VCOM feed so a ride can be driven headlessly. HWFC must beOFF in the Board Configurator or host→device injection is silently ignored. Drive with pyserial at
115200 on
/dev/cu.usbmodem*133(rtscts=False);stty+printfdoes not work. Script lives in thesession scratchpad under a unique prefix (
s5_soak.py) per the parallel-agent scratchpad rule.Liveness probe first, every run. The J-Link CDC wedges silently:
write()succeeds, RTT keepsflowing, nothing lands, and a blind script then "passes" every step. Snapshot the RTT log size, send
six taps, sleep 2 s, re-check. Zero growth = wedged; only a physical DK power-cycle clears it.
A — the freeze window over a map base (
render ⊥ nav), ≥50 cycles, ~30 min — automatableThe window this whole mechanism exists for is Back out of the planning spinner while the planner is
still running, which is the only way a map base lands under a live search.
F <lat> <lon>fixes at ~1 Hz in small steps (teleport rejection).K t 1to Detour → press → rejoin chooser → press (posts the plan andpushes the spinner) → immediately
K b d/K b uto pop the spinner while the planner runs.nav plan: start, then the banner's single overlay repaint, then —on the pass the answer lands — exactly one full map repaint (the
pending_map_redrawcatch-up).
base — must freeze nothing and raise no banner), and a plan whose answer is
NoPath.Pass: every cycle shows the start → banner → answer → full-repaint sequence; zero
arena:linesreporting
Busy/NotHeldfor Render or Nav; zero plan answers reporting a failure tier that is nota genuine
NoPath; no cycle ends with the map quiet for more than one wake after the answer.B —
nav ⊥ usbandrender ⊥ usb, ~20 min — semi-automatable (needs a hand on the cable)render ⊥ usbholds by construction.Pass: the plan during the upload is refused before the planner arms, and the refusal message
names the transfer — not
"the scratch arena is busy", and not aNoPath. After the upload ends,the same input plans normally.
arena: USB write-combining arm granted/reclaimedappear exactlyonce each per upload.
C — the stuck-freeze soak, 60 min — automatable
A continuous ride with a plan cycle every ~60 s and a periodic
Z <mpp>zoom nudge. The scriptasserts that after every freeze release a map render line appears within two wakes, and that
deep_ride_high_waternever crossesdeep_ride_margin_min.Pass: 60 uninterrupted minutes, zero missed catch-ups, no WDT reset, no boot fault.
Genuinely human, and flagged as such
panel. RTT proves the rows were pushed; only an eye proves it reads as "recalculating" rather than
"wedged". (The pixel geometry itself is proven off-device by
obc-sim --png --freezeand V0'smanifest — the on-glass part is the panel, not the pixels.)
Record the result in the PR the way #1146 P2's baseline note did — that note still carries
"the on-glass soak is pending" for this exact mechanism. This slice is what closes it.
Resource limits
Baseline is
firmware/tools/resource_baseline.jsonat3943301e(re-pinned by PR #1486). Reportevery value; itemize any increase.
size_of::<App>()(compile_time_allocations.app)RerouteFreeze; four arrive inCoreMode; expect flat or −8.measured_resident)link::TRANSFER_ACTIVE(2 B) leaves.resident_ram_maxuninit_maxarena_total/render/nav/usbfull_frame_sized_writable_countFB+ARENA).poll_frame_measuredtask_frame_measuredresidual_stack_measuredboot_chain_measured_pinned_hostdeep_ride_high_watermeasured_flash_flash_note_1096). Re-pin from this PR'sembeddedrun and state the delta.No allocator, no new task, no atomics in
CoreMode, no combinedEffect/Outcome/Intentenum,no event bus (#1433 §14, §16).
Verification
Plus the board build and the soak above:
Definition of done
CoreModeexists, holds the four levels, and is the only writer and the only readersource for "a search is live" and "a transfer is live".
reroute_freeze.rsandlink_gate.rsare deleted; their surviving rules are tested onCoreMode, and every named regression (Scratch arena: three-way RAM share (render scratch / nav / USB staging) + 25 KB render-cap growth #1146 per-family release, the two-live-runs union, theengaged-level edge) has a ported test that was green before the deletion landed.
nav_run, andTRANSFER_ACTIVEis gone.MapQuiescedandTransferReadycan only be minted fromCoreMode, plus the one namedrecovery-boot escape.
CoreMode::admits_heavy(); heavy capabilities withdraw for a live search aswell as a live transfer, and the conformance disposition table is unchanged except where that
arm is stated to change it.
obc-sim --png --freezestill draws the banner."the on-glass soak is pending" note in
resource_baseline.jsonis updated to say it happened.Open questions for the implementer to settle in review
CoreModeneed anInstallinglevel?shared.rs:212claims admission is withdrawn"while a transfer streams or an install is armed", but the code checks only the transfer,
and an armed install reboots immediately. Deliberately not locked above: adding a level for a
window that ends in a reboot looks like provisioning for an operation that never happens. If the
answer is no, fix the sentence in
shared.rsin this PR.map transfer card. A route, trip or weather upload streams without one. That is a gap in the
fact, not in
CoreMode— the flat engine knows the truth and S6 wiresExternalFacts::note_transferfrom it. Confirm this is left as a stated gap rather than paperedover with a fourth derivation.
nav_run's remaining role. It stays as the board's planner-run handle. Is there a cheap wayto make "read
nav_runas a search fact" impossible again later — a newtype, or does theCoreMode-only mint already close it?