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.
After the first filter keystroke or submenu move, the card top edge and the maximum rows height freeze at their current values.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
After the first filter keystroke or submenu move, the card top edge and the maximum rows height freeze at their current values. The card then grows and shrinks downward instead of re-centering on every resize. Closing the menu clears the freeze, so the next open centers again.
when menu_interacted the menu_presentation shall eventually satisfy card_top_frozen
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Menu.qml panel.freezeCardTop lines 1147-1152 and onShownChanged line 1163; presentation stability of the presented menu session, reset by the close lifecycle.
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_casenominal
Worst case graded above: freeze captured over an empty filtered set pins cardTop/maxRowsHeight at empty-card values until close; accepted low (cosmetic, self-clears on close). nominal: first filter keystroke or submenu move captures the on-screen top and rows height, after which resize grows the card downward - the witnessed happy path. boundary: the sentinel pair cardTop=-1/maxRowsHeight=-1 is distinguished from the valid frozen value 0 (top at the very screen edge) by the >= 0 test, so a legitimately-zero top survives; closing clears both sentinels. malformed_input does not fire: no external input reaches the freeze path.
- propertyreviewedidempotency
idempotency: freezeCardTop guards on cardTop < 0, so repeated interactions re-capture nothing - the freeze-once-per-open semantics IS the contract, and the idempotency obligation is met by the same guard rather than duplicated in the checklist. determinism: the captured top is a pure function of geometry at first interaction.
- structuralnot applicable
pure QML presentation state: two int properties and a comparison, no memory/pointer/encoding surface; the sentinel arithmetic is dispositioned under scenario.boundary.
- domainnot applicable
no cross-process call, no timeout surface, no concurrency (single-threaded QML event loop, shown-change and interaction handlers cannot interleave mid-freeze), no trust boundary - the freeze state never leaves the menu surface. External-call and identity classes do not fire.
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-CKBG
Read panel.freezeCardTop and onShownChanged. setFilter and setActiveMenu call freezeCardTop while the card is shown, pinning cardTop to the centered top and maxRowsHeight to the current rows height; onShownChanged resets both to -1 when the surface unmaps on close. menu_interacted models the first interaction, card_top_frozen the pinned pair cleared by close. 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 · 1 discharged
Browse the catalogueBehavior for unusual but valid input combinations.
the freeze capture lands while the active filter has zero visible rows: maxRowsHeight pins at 0 and cardTop pins at the centered position, so the card grows downward from a top computed for an empty card until the menu closes - a cosmetic wedge the freeze-once semantics makes sticky for the whole open
- nominalrequiredpresentCovered by 1 test
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 menu_interacted the menu_presentation shall eventually satisfy card_top_frozen
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| # | card_top_frozen | menu_interacted | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | menu_interacted | |
| 2 | F | T | F | card_top_frozen | Exempted · defensive — setFilter and setActiveMenu call panel.freezeCardTop() on every interaction path while the card is shown; an interaction leaving cardTop unset needs those calls removed (reviewed: REVIEW-MC1) |
| 3 | T | T | T | card_top_frozen |
Compiled formalization (CoCoSpec)· parse: valid
((H( not menu_interacted)) or ( not (SI( (menu_interacted and (ZtoPre( not menu_interacted))), ( not card_top_frozen) ))))
SCOPE: in the interval defined by the entire execution.
TRIGGER: first point in the interval if menu_interacted is true and any point in the interval where menu_interacted becomes true (from false).
REQUIRED BEHAVIOR: for every trigger, card_top_frozen must hold at some time point between (and including) the trigger and the end of the interval.
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
Files to re-check (1)
- Menu.qmlshell/plugins/menu/Menu.qml
Tests to re-run (1)
- menu-pointer-lifecycle-test.shtest/shell.d/menu-pointer-lifecycle-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.