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.
Drilling into a submenu records the parent menu, the selected index, and the selected row id.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Drilling into a submenu records the parent menu, the selected index, and the selected row id. Back returns to the parent menu and puts the cursor on the remembered row when that row is still listed and selectable. Otherwise the cursor starts from the saved index and settles off disabled rows. A forward drill-in starts on the first row.
when back_navigated & remembered_row_present the menu_navigation shall eventually satisfy remembered_row_selected
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Upstream PR omacom/omarchy#13012 (head 7a7fb10c) changes Menu.qml setActiveMenu to push {menu, index, itemId} records and restore them on goBack (id first, saved index as fallback). Known limit, recorded as KI-MENU-BACK-FILTERED-INDEX: the saved index of a drill-in from a filtered search points into the filtered list.
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
- V2 Third Party Review · AI agent
- Reviewed
- Oct 1, 2026, 08:20 UTC
History
- Created
- Oct 1, 2026, 08:00 UTC · V2 Third Party Review · AI agent
- Modified
- Oct 1, 2026, 08:12 UTC · V2 Third Party Review · AI agent
Hazard review
- scenarioreviewedboundaryedge_case
boundary: the remembered row disabled or gone on return - the id loop skips non-selectable rows and the saved index is settled off disabled rows by rebuildDisplay, witnessed in test/shell.d/menu-pointer-lifecycle-test.sh (the PR #13012 witness block). edge_case: a drill-in from a filtered search saves an index into the filtered list while Back clears the filter, so the fallback index can land on an unrelated parent row (pocs/pr13012-back-from-search.js reproduces it; the baseline started at row 0) - tracked as KI-MENU-BACK-FILTERED-INDEX. Provider-backed parents that load rows asynchronously follow the id only once at restore; later rebuilds keep the index. All consequences are cursor placement only, no action runs. Catalog 1.11.0 re-review: input_domain not applicable, the requirement reads no bytes; it acts on in-shell navigation state (the nav stack and row ids). concurrency_scale not applicable, each key press runs to completion on the single QML event loop, and a deep Back chain pops one record per press.
- propertyreviewedtotality
Every Back yields a defined cursor - the remembered row, the settled saved index, or row 0 for a forward drill-in; the navigation record shape change stays inside Menu.qml (navStack readers are setActiveMenu/goBack and the resets in openExistingMenu/openDmenu).
- domainnot applicable
Pure in-shell navigation state; no IPC, file, network, crypto, or privilege surface.
- structuralnot applicable
Array concat/slice of small records plus integer indices; no manual memory, pointers, or binary framing.
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.
- V2 Third Party Review · AI agentApprovedSpec conformanceOct 1, 2026 · 2 days agoREVIEW-261001-BFW5
Read setActiveMenu and goBack on the PR #13012 tree. A history push records {menu, index: selectedIndex, itemId of displayModel row at selectedIndex}. goBack pops the record and calls setActiveMenu(previous.menu, false, false, previous): selectedIndex starts at the saved index, rebuildDisplay settles it off disabled rows, then a scan selects the first row whose itemId matches the record and rowSelectable(i) holds. back_navigated & remembered_row_present -> remembered_row_selected is exactly that scan; the violation row (present and selectable but not selected) needs the scan removed, so it is dispositioned defensive. The not-present arm falls back to the settled saved index. Limit recorded separately (KI-MENU-BACK-FILTERED-INDEX): the saved index of a drill-in made from a filtered search indexes the filtered list, while Back rebuilds the unfiltered parent list, so the fallback can land on an unrelated row.
Cited code (3)
Open known issues
Findings currently open against this requirement — issues its verification surfaced that are not resolved yet. Each links to the full finding.
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 back_navigated & remembered_row_present the menu_navigation shall eventually satisfy remembered_row_selected
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| back_navigated | — | Back (Backspace/Left on an empty filter) pops a navigation record that carries the parent menu's saved selection (index and row id). | |
| remembered_row_present | — | The row id saved in the popped navigation record is listed, and selectable, in the rebuilt parent menu. | |
| remembered_row_selected | — | The cursor rests on the remembered row in the parent menu. |
Witnesses· 3 scenarios total
- navHarnessexercises 3 condition scenarios
MC/DC truth table· 4 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| # | back_navigated | remembered_row_present | remembered_row_selected | Result | Proves | Covering test |
|---|---|---|---|---|---|---|
| 1 | F | T | F | T | back_navigated | |
| 2 | T | F | F | T | remembered_row_present | |
| 3 | T | T | F | F | back_navigated | — |
| 4 | T | T | T | T | remembered_row_selected |
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.
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
Nothing downstream depends on this yet
No downstream impact — "Drilling into a submenu records the parent menu, the…" has no downstream edges.
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.