Proof Portal
Omarchy
ProbeLabsviewing a historical runA proof layer — requirements, tests and verified fixes — for two of Omarchy's subsystems: the application menu (launcher scripts, QML model, JSONC config, search and selection) and the lock screen (lock scripts, QML, PAM authentication). Scope is deliberately limited to those components of omacom/omarchy; the rest of the distribution is not covered.
A summon can reach the menu while the shell starts, before both menu files have answered.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
A summon can reach the menu while the shell starts, before both menu files have answered. The default file answers when it loads. The optional user file answers when it loads or when it fails to load. If the route does not resolve against the files loaded so far, the menu falls back to root and keeps the route pending. A route that resolves at once opens at once, as at any other time. When both files have answered, the menu tries the pending route one time. It opens the route if the route resolves and the menu is still open in menu mode. Then the menu drops the route, also when it did not open. The menu drops the route earlier if the user types into the menu or opens another menu. A summon that arrives after both files have answered does not wait. If its route does not resolve, the menu shows root and does not open the route later.
when route_fell_back_before_load & pending_route_resolves & menu_untouched_on_root the menu_router shall eventually satisfy pending_route_opened
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Upstream omacom/omarchy quattro 821ae589 has this defect. The shell queues a summon that arrives before the menu plugin loads. It hands the summon to open() as soon as the plugin loads (shell.qml registerPanelLoader, deliverIfLoaded). Neither FileView has read its JSONC file at that point, and the user extension usually answers first. So openRoute cannot resolve the route, and openExistingMenu falls back to root. Nothing opens the route when the files land. Super+Escape right after login or a shell restart shows the main menu, and an action alias never runs. openRoute already writes the route to pendingInitialMenu, which nothing read since the bash menu went away (edfd68d4, 4cd6593b). The fix keeps the route pending only when the menu fell back to root. rebuildItemsFromSources opens it through openRoute once it resolves, so aliases, links and action aliases behave as for any summon. The first version of the fix (43d787d4) opened the route as soon as it resolved. That could happen against the default file alone. So an early summon of about ran the default command when the user file overrides it. The route also stayed pending after the user opened another menu and went back to root. So a later load or a live edit could still open it. Review of #14055 found both. The follow-up (48405669) waits for both files, tries the route once, and drops it when the user types or opens another menu. setFilter and setActiveMenu clear it, and onLoadFailed records that the user file answered.
Verification & provenance
How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).
Review
- Status
- in_review
- Reviewer
- Claude Pr B · AI agent
- Reviewed
- Oct 2, 2026, 12:45 UTC
History
- Created
- Oct 2, 2026, 12:25 UTC · Claude Code · AI agent
- Modified
- Oct 2, 2026, 15:14 UTC · Claude Pr B · AI agent
Hazard review
- scenarioreviewededge_case
Worst case: a summon made during startup opens the main menu, runs the default command that the user file overrides, or a pending route later pulls the user out of a menu they chose. edge_case: each load order is a case - the default file first, the user file first, a missing user file, and a menu or action override that only the user file defines (witnessed). The route waits until both files answered and gets one try. A route that resolves at once, a missing id (also when a later edit adds it), a summon after both files answered, a summon with no route, a select prompt that replaced the summon, a summon closed before the files load, and a user who typed, opened another menu, or opened one and went back to root do not replay (witnessed). An action alias runs once. boundary not applicable: the decision is a set of booleans, with no range or limit. input_domain not applicable: the route string goes through the same resolveRoute as any summon. concurrency_scale not applicable: both FileView handlers and the summon run one after the other on the GUI thread; only their order varies, which the edge cases cover.
- propertyreviewedtotality
Every summoned route ends in one defined state: opened at once, opened by its one try after both menu files answered while the menu is still open in menu mode and untouched, or left on root and dropped. No path opens a route the user did not summon, opens it twice, or opens it after the user typed or opened another menu.
- structuralnot applicable
One string property and one guarded call; no memory, encoding or numeric surface.
- domainnot applicable
Menu navigation state only. Action aliases run through the same runAction path as any summon, under their own requirements.
Change history
Every recorded revision of this requirement's source file — newest first, each with its commit message and the diff for that change.
Review history
Human and AI-agent approvals of this requirement — the 'why was this approved' lineage, each with the reviewer's justification and the code it cites.
- Claude Pr B · AI agentApprovedSpec conformanceOct 2, 2026 · 2 days agoREVIEW-261002-NS9R
Read shell/plugins/menu/Menu.qml on the pr-B tree (upstream 821ae589 plus the fix). openRoute writes the route to pendingInitialMenu and calls openExistingMenu, which clears it when the requested item is the one shown. So the route stays pending only when the menu fell back to root (route_fell_back_before_load). At the end of rebuildItemsFromSources, which both FileView handlers call, the menu calls openRoute(pending) when a route is pending, the menu is open in menu mode on root with an empty filter (menu_untouched_on_root), and the route resolves to an item (pending_route_resolves). openRoute resolves aliases, follows links and runs action aliases, so pending_route_opened means the same as for any summon. The violation row (a resolved pending route left unopened on an untouched root) needs that call removed, which is the 821ae589 behaviour; it is dispositioned defensive. Witnesses in test/shell.d/menu-startup-route-test.sh run the real open, openRoute, openExistingMenu, openDmenu, cancel and rebuildItemsFromSources bodies and the FileView handlers under node vm, with both load orders; the replay rows fail on 821ae589. A route that resolves at once, a missing id, and a user who opened another menu or typed do not replay.
Cited code (3)
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
The tests that discharge each obligation aren't available for a historical run
The evidence matrix behind each obligation comes from the live audit index, which can't be rebuilt for a past commit. Nothing here means unknown — not that the requirement has no obligations.
Formula evidence
The formal formula behind this requirement, the variables it is written over, and the tests that exercise it (each term is explained inline).
Formula evidence
The formal formula behind this requirement, the variables it is written over, and the tests that exercise it (each term is explained inline).
FRETish formula
when route_fell_back_before_load & pending_route_resolves & menu_untouched_on_root the menu_router shall eventually satisfy pending_route_opened
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| route_fell_back_before_load | — | A summon arrived before both menu files had answered and named a route that the files loaded so far do not define, so the menu fell back to root. A summon after both files answered never sets this. | |
| pending_route_resolves | — | When both menu files have answered (the default file loaded, the user file loaded or failed), the merged items define the item that the pending route names. | |
| menu_untouched_on_root | — | Since the summon, the menu stayed open in menu mode, and the user neither typed into it nor opened another menu. | |
| pending_route_opened | — | The menu opens the pending route one time, as a summon would, which opens the item, follows a link or runs an action alias. |
Witnesses· 4 scenarios total
- loadexercises 4 condition scenarios
MC/DC truth table· 5 rows
Each row assigns the formula's conditions (T/F) and shows the Result— the formula's value for that input row, not a test pass/fail. A row proves a condition when flipping only that condition flips the outcome. The test that covers each row is linked.
mcdc:ignoreNo-actionfalse-result row satisfied by designUncoveredneeds a covering test| # | menu_untouched_on_root | pending_route_opened | pending_route_resolves | route_fell_back_before_load | Result | Proves | Covering test |
|---|---|---|---|---|---|---|---|
| 1 | F | F | T | T | T | menu_untouched_on_root | |
| 2 | T | F | F | T | T | pending_route_resolves | |
| 3 | T | F | T | F | T | route_fell_back_before_load | |
| 4 | T | F | T | T | F | menu_untouched_on_root | — |
| 5 | T | T | T | T | T | pending_route_opened |
Its place
How this requirement connects — what proves it, what it affects, and what it rests on. Authored links only here; automatically derived links come from the audit index.
Loading graph…
Trace evidence
The concrete artifacts linked to this requirement — implementing code, verifying tests, documents, and the findings raised against it.
0 open · 1 resolved
No open findings
Everything flagged against this requirement has been resolved.
Impact
Blast radius — authored trace links only (automatically derived links come from the audit index and aren't shown here).
Impact
Blast radius — authored trace links only (automatically derived links come from the audit index and aren't shown here).
If you change this
Files to re-check (1)
- Menu.qmlshell/plugins/menu/Menu.qml
Tests to re-run (14)
- seq-route-after-load.eventstest/bdiff/corpus/lifecycle/seq-route-after-load.events
- seq-startup-action-alias.eventstest/bdiff/corpus/lifecycle/seq-startup-action-alias.events
- seq-startup-default-only.eventstest/bdiff/corpus/lifecycle/seq-startup-default-only.events
- seq-startup-default-then-missing-user.eventstest/bdiff/corpus/lifecycle/seq-startup-default-then-missing-user.events
- seq-startup-missing-user-then-default.eventstest/bdiff/corpus/lifecycle/seq-startup-missing-user-then-default.events
- seq-startup-navigate-before-user.eventstest/bdiff/corpus/lifecycle/seq-startup-navigate-before-user.events
- seq-startup-root-summon.eventstest/bdiff/corpus/lifecycle/seq-startup-root-summon.events
- seq-startup-route-closed.eventstest/bdiff/corpus/lifecycle/seq-startup-route-closed.events
- seq-startup-route-reload.eventstest/bdiff/corpus/lifecycle/seq-startup-route-reload.events
- seq-startup-route-summon.eventstest/bdiff/corpus/lifecycle/seq-startup-route-summon.events
- seq-startup-route-then-select.eventstest/bdiff/corpus/lifecycle/seq-startup-route-then-select.events
- seq-startup-type-before-user.eventstest/bdiff/corpus/lifecycle/seq-startup-type-before-user.events
- harness.mjstest/bdiff/harness.mjs
- menu-startup-route-test.shtest/shell.d/menu-startup-route-test.sh
What this rests on
Discussions
Discuss this with the proof team. Nothing changes in your audit automatically — you open a request and a staff member records any outcome inside the thread.