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.
Row selection follows the pointer only after it genuinely moves past the gate threshold.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Row selection follows the pointer only after it genuinely moves past the gate threshold. It never lands on a non-selectable row. Keyboard navigation, filtering, menu transitions, the delete dialog, and opening the menu disarm the gate. Synthetic hover churn under a stationary pointer therefore cannot move the selection.
when pointer_moves_over_rows the menu_pointer shall eventually satisfy gated_row_selection
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Menu.qml disarmPointer line 978 and selectFromPointer lines 982-987 via PointerMoveGate; pointer-driven selection is a distinct trigger from keyboard traversal (Z48F) and must not fight it.
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
- Leonid Bugaev
- Reviewed
- Sep 29, 2026, 14:34 UTC
History
- Created
- Sep 29, 2026, 13:51 UTC · Leonid Bugaev
- Modified
- Sep 30, 2026, 08:04 UTC · Leonid Bugaev
Hazard review
- scenarioreviewededge_casemalformed_input
Worst case graded above: synthetic hover churn is the exact threat the movement gate exists to defeat, and the residual is jitter accumulating across a burst - graded low, guarded by the moved() threshold plus the rowSelectable second guard. edge_case: every interaction that should reset intent (keyboard nav, filtering, menu transitions, the delete dialog, opening the menu) calls disarmPointer, so gate state cannot survive a context switch. malformed_input: a non-selectable row answer short-circuits the write before cursorActive/selectedIndex change - selection can never park on a disabled row. nominal is witnessed by the executing assertions in menu-pointer-lifecycle-test.sh.
- propertyrevieweddeterminism
determinism: the same pointer trajectory over the same rows answers the same selection - gate state is a pure function of movement history since the last disarm, and QML event-loop serialization means no interleaving can reorder moved()/rowSelectable() against the writes they guard. concurrency does not pertain (single-threaded); totality of the disarm enumeration is the accepted residual graded above.
- structuralnot applicable
the gate is scalar pointer arithmetic (deltas against a threshold) with an explicit reset - no memory, encoding, or sentinel surface beyond what scenario/property already carry; no nil object reaches the guard (rows pass resolved entries).
- domainnot applicable
no cross-process call, no timeout, no IPC, no trust boundary: the gate guards QML-internal pointer events inside one compositor surface. The dmenu/picker poll surfaces that DO carry timeout debt live in the dmenu protocol reqs (deferred under KI-MENU-SELECT-POLL-DEADLOCK), not here.
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.
- Leonid BugaevApprovedSpec conformanceSep 29, 2026 · 4 days agoREVIEW-260929-DTC8
Read disarmPointer and selectFromPointer. selectFromPointer returns unless pointerGate.moved reports genuine movement past the threshold, and returns again when rowSelectable reports the row disabled; only then does it raise cursorActive and move selectedIndex. disarmPointer resets the gate and runs from keyboard select, setFilter, setActiveMenu, cancelDelete, cancel, and openExistingMenu. pointer_moves_over_rows models gate-passed movement; gated_row_selection is the gate-honored landing. Formula conforms to the code.
Cited code (2)
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
1 obligation
Browse the cataloguesynthetic hover churn under a stationary pointer (a redraw loop or a stray device emitting move events with sub-threshold deltas) repeatedly re-enters selectFromPointer; the gate exists precisely so this cannot walk the selection, but a gate threshold crossed by accumulated sub-threshold jitter across one event burst would land the cursor on a row the user never aimed at - the disarm enumeration (keyboard nav, filtering, menu transition, delete dialog, open) must keep covering every interaction that should reset intent
Discharging tests pending a synced audit.
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 pointer_moves_over_rows the menu_pointer shall eventually satisfy gated_row_selection
Witnesses· 2 scenarios total
- extractQmlFunctionexercises 2 condition scenarios
MC/DC truth table· 3 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| # | gated_row_selection | pointer_moves_over_rows | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | pointer_moves_over_rows | |
| 2 | F | T | F | gated_row_selection | — |
| 3 | T | T | T | gated_row_selection |
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.
No findings affect this requirement
Nothing was flagged against this requirement in the pinned run.
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 — "Row selection follows the pointer only after it genuinely…" 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.