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.
The merged item tree is addressable by id.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
The merged item tree is addressable by id. An id present in the tree yields its item, and any other id yields null. Menu state then falls back to the root menu instead of a dangling entry.
when item_requested the menu_model shall eventually satisfy item_by_id_resolved
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Menu.qml item lines 233-235; the by-id accessor over the merged tree used by guard evaluation, navigation fallbacks, and route/state lookups.
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:03 UTC · Leonid Bugaev
Hazard review
- scenarioreviewedmalformed_inputedge_case
Worst case: prototype-member id (constructor/toString) resolves to an inherited truthy function, skipping the || null fallback and the root-menu fallback the req promises - slugify keeps pure a-z ids and desktop-derived app rows share the items map, so the mechanism is reachable, graded low (menu-surface error, no data or privilege). malformed_input: any other absent id answers null and the caller falls back to root, the exact contract. edge_case: an id present with a falsy value would also fall through the || chain, but every merged entry is an object (truthy), so only inherited members can take the wrong arm. Catalog 1.11.0 re-review: input_domain not applicable, it reads no external text input. concurrency_scale not applicable, a pure function of its arguments, recomputed on each load or keystroke: no state across calls, no process, timer or lock.
- propertyrevieweddeterminism
determinism: item() is a pure map read - the same tree and id answer identically on every call; no ordering or collection dependence. totality: the function is defined for every string id by construction (fall-through to null), so the answer space is total; the one non-total corner (inherited-member ids) is graded under scenario.malformed_input. idempotency/commutativity do not pertain to a lookup.
- structuralreviewednil_safety
nil_safety IS this requirement: the || null fallback distinguishes absent from present and the callers documented fallback-to-root consumes the null answer; MenuModel parents walk with depth/path guards capped at 32, so a malformed parent chain cannot loop the model. No memory, pointer, or encoding surface in the QML/JS lookup itself; the prototype-chain read is graded as malformed_input (scenario), not a structural class - the catalog carries no JS-prototype-membership class and forking one for a single low-graded site would be catalog noise, not a gap.
- domainnot applicable
no cross-process call, no timeout surface, no concurrency (QML single-threaded event loop), no trust boundary crossed: ids come from the repo-shipped default JSONC, the user own config, or slugified desktop-file ids on the same machine - the lookup map is written with own properties (merge assigns nextItems[id]) so only never-written prototype names can resolve inherited, and no privileged sink consumes item(). external_call/concurrency/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-E3G7
Read item() in Menu.qml. The accessor returns root.items[id] or null, so a present id yields its item and any other id yields null; the lookup always answers and never returns a dangling entry. item_requested models the caller by-id lookup, item_by_id_resolved the coherent answer. Formula conforms to the code.
Cited code (1)
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 when inputs are syntactically or structurally invalid.
an id that names an Object.prototype member (constructor, toString, valueOf - all pure a-z, so slugify preserves them and a desktop app literally named Constructor gets slug id constructor) escapes the || null fallback: root.items[id] resolves up the prototype chain to a truthy function instead of null, so the callers null check passes and a function object flows where an entry is expected - the root-menu fallback this req promises is skipped and the row/bind path throws on the missing entry fields
- negativerequiredpresentCovered by 1 test
- 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 item_requested the menu_model shall eventually satisfy item_by_id_resolved
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| # | item_by_id_resolved | item_requested | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | item_requested | |
| 2 | F | T | F | item_by_id_resolved | — |
| 3 | T | T | T | item_by_id_resolved |
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.