Proof Portal

Project overview

Omarchy

ProbeLabsviewing a historical run

A 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.

Viewing historical run 77b0188Oct 3, 2026, 06:18 PMpr/14155Back to current
All requirements
RequirementSW-REQ-261003-B7ZASoftwareReview

The Apps menu orders its rows by the collation of the locale and ignores case.

This requirement changed after its last recorded review, so approval is stale. Automated checks pass.
PriorityshallTypeguaranteeCategoryfunctionalComponentmenuAssuranceCFindingsnone open

Specification

The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.

Description

The Apps menu orders its rows by the collation of the locale and ignores case. A name that starts with an accented Latin letter, such as Écrans or Übersetzer, sorts under its base letter. Names in other scripts sort where the collation of the locale puts them. In the Apps menu, two equal names keep their id order. Under ru_RU, el_GR or zh_CN the script of that language comes first, before the Latin names. Under en_US or fr_FR other scripts come after the Latin names. Qt takes the collation from LC_ALL, then LC_COLLATE, then LANG; LANGUAGE does not change it. Under C or C.UTF-8 it keeps UTF-16 code-unit order, the same as before the fix. This requirement states only the order of the rows. SW-REQ-261003-C9GM states which apps the list holds. AppSearch.sortedEntries, which gives the same list to plugins, uses the same comparison. Ties keep a fixed order by desktop id, the same as the Apps menu.

FRETish formula
when apps_rows_rebuilt the menu_view shall immediately satisfy apps_rows_in_letter_order
View full formal model

Rationale & tags

Why this requirement exists, and how it is categorised.

Upstream omacom/omarchy quattro a85e29ab has this defect. rebuildDisplay sorts the Apps rows with its own comparator, because DesktopEntries can reorder its values when an application starts. The comparator compares the lowercased names with < and >, that is by UTF-16 code unit. So every name that starts with a letter above U+007A goes after z. App names come from the Name of each desktop entry for the user's language. On a French desktop, Écrans and Éditeur de texte show after Zed. A check in the real shell with LANG=fr_FR.UTF-8 showed this order on a85e29ab. The fix compares the names with localeCompare, as the search sort in the same function already does. The fix keeps the tie-break on the id. With the fix, the real shell shows the two names under E. AppSearch.sortedEntries, which gives the same list to plugins, now uses localeCompare too. After review, a second upstream commit (c4a14aa9) breaks its ties on the desktop id, as the Apps menu does. So two names that collate equal come out in id order, whatever order they arrive in. A composed and a decomposed É are such a pair. The node witnesses (test/shell.d/menu-apps-order-test.sh, the behaviour-diff harness and test/shell.d/menu-apps-order-bdiff-test.sh) run the comparator under the ICU collation of Node. They pin the comparator, not the collation of Qt. The PR test runs node under LC_ALL=C.UTF-8, where node uses the root collation. So its result does not depend on the locale of the test machine. Checks in the real shell cover Qt. Under fr_FR.UTF-8 the accented names move under their base letter. Under ru_RU, el_GR and zh_CN the script of the language now comes first; on a85e29ab it came after Z. Under en_US and fr_FR other scripts still follow the Latin names. Under C.UTF-8 the order stays as on a85e29ab. Checks with the QML engine of Qt 6.11 show which setting selects the collation. With LANG=fr_FR.UTF-8 and LC_COLLATE=C.UTF-8, É stays after Z. With LANG=en_US.UTF-8 and LC_COLLATE=fr_FR.UTF-8, É sorts under E. LANGUAGE does not change the order. Under en_US, names that start with a symbol, such as _Under, (beta) X or ~Tilde, now sort before digits and letters. This requirement accepts these changes as the order of the locale.

Verification & provenance

How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).

Assurance levelC
Formalizationvalid
Realizabilityrealizable
Vacuitychecked_ok
Strategyfretish

Review

Status
in_review
Reviewer
Claude Pr New D · AI agent
Reviewed
Oct 3, 2026, 07:51 UTC

History

Created
Oct 3, 2026, 07:49 UTC · Claude Pr New D · AI agent
Modified
Oct 3, 2026, 16:10 UTC · Claude Pr New D · AI agent

Hazard review

Reviewed Oct 3, 2026, 07:51 UTCby agent:claude-pr-new-Dcatalog v1.11.0
  • scenarioreviewededge_caseempty_input

    Worst case: an app whose name starts with an accented or non-Latin letter shows after Z, so a user who scans the list by letter does not find it where it belongs. edge_case: precomposed accents (É, Ü), a decomposed accent (E plus a combining mark), non-Latin scripts, mixed case and two equal names; each case sorts by localeCompare and an equal pair keeps id order (witnessed). empty_input: an entry with no name gives the empty string, which sorts first as before. boundary not applicable: the comparator has no range or limit. input_domain not applicable: the names reach the comparator as decoded strings from DesktopEntries; it parses nothing. concurrency_scale not applicable: one synchronous sort on the GUI thread per rebuild.

  • propertyrevieweddeterminismtotality

    determinism: the same names and ids give the same order on every rebuild, whatever order DesktopEntries returns them in, because a tie on the name falls back to the id. totality: the comparator returns a defined result for every pair of rows, including equal names, empty names and names in any script.

  • structuralnot applicable

    One string comparison inside an array sort; no memory, numeric or encoding transform. The names are already decoded strings when they reach the comparator.

  • domainnot applicable

    Display order of rows inside the shell window only; no trust boundary, privilege, network, crypto or process surface.

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.

  1. Claude Pr New D · AI agentApprovedSpec conformanceOct 3, 2026 · 16 hours agoREVIEW-261003-39RH

    Re-review for the second upstream commit c4a14aa9 of PR #14155. AppSearch.sortedEntries now orders by localeCompare of the lowercased key and then by the desktop id, the same tie-break as the Apps comparator in rebuildDisplay (localeCompare of the lowercased labels, then the item id). So two names that collate equal come out in id order whatever order they arrive in; this supersedes the input-order wording of REVIEW-261003-JH9B and REVIEW-261003-721N. The PR test now runs node under LC_ALL=C.UTF-8, so its expectations use the root collation on any test machine, and it asserts id order for a composed and a decomposed É in both arrival orders. seq-apps-plugin-tie shows the menu and the plugin list agree on that order. B7ZA states that ties keep a fixed order by desktop id, the same as the Apps menu. The formula and the defensive violation row (REVIEW-261003-JTMM) are unchanged.

    Cited code (4)
  2. Claude Pr New D · AI agentApprovedSpec conformanceOct 3, 2026 · 20 hours agoREVIEW-261003-721N

    Final re-review on quattro-proof 49cd12b0, where shell/services/AppSearch.js is in the verification scope. sortedEntries carries an Implements line for SW-REQ-261003-B7ZA next to SW-REQ-261003-C9GM. With no query it orders by localeCompare of the lowercased key, and when that returns 0 by the old < and > on the key and then the name. So two different names that collate equal keep one order, and identical names keep their input order, as before. The Apps comparator in rebuildDisplay orders by localeCompare of the lowercased labels and then the id. Under C or C.UTF-8 Qt keeps UTF-16 code-unit order, the same as before the fix; LC_ALL, then LC_COLLATE, then LANG select the collation. Witnesses: the PR test runs the real sortedEntries (accented names, collate-equal names in both input orders) and the Apps comparator; seq-apps-plugin-list shows the menu and the plugin list agree. C9GM (which apps the library lists) is unaffected: only the order changes.

    Cited code (5)
  3. Claude Pr New D · AI agentApprovedSpec conformanceOct 3, 2026 · 20 hours agoREVIEW-261003-GDCZ

    Re-review of the round-3 text corrections. Under C or C.UTF-8 Qt keeps UTF-16 code-unit order, the same as before the fix; this corrects the term code-point order in REVIEW-261003-AP6S and REVIEW-261003-CY43. B7ZA now states which setting selects the collation: Qt takes it from LC_ALL, then LC_COLLATE, then LANG, and LANGUAGE does not change it. Checks with the QML engine of Qt 6.11 show it: LANG=fr_FR.UTF-8 with LC_COLLATE=C.UTF-8 keeps É after Z, and LANG=en_US.UTF-8 with LC_COLLATE=fr_FR.UTF-8 puts É under E. The comparator, the formula and the defensive violation row (REVIEW-261003-JTMM) are unchanged. The witness test now also asserts the encoding, ascii and first-row inputs (15 cases).

    Cited code (3)
  4. Claude Pr New D · AI agentApprovedSpec conformanceOct 3, 2026 · 20 hours agoREVIEW-261003-JH9B

    Re-review for the c5ed4375 form of AppSearch.sortedEntries, which supersedes the sortedEntries wording of REVIEW-261003-CY43. With no query, sortedEntries orders by localeCompare of the lowercased key; when that returns 0 it falls back to the old < and > on the key and then on the name. So two different names that collate equal, such as a composed and a decomposed É, get one order whatever the input order (the PR test checks both input orders). Two identical names compare 0 at every step and keep their input order, as on a85e29ab; there is no id tie-break in sortedEntries. B7ZA now says exactly that. The Apps comparator in rebuildDisplay is unchanged from CY43: localeCompare of the lowercased labels, then the id.

    Cited code (4)
  5. Claude Pr New D · AI agentApprovedSpec conformanceOct 3, 2026 · 22 hours agoREVIEW-261003-CY43

    Round-3 re-review on the upstream change cb981de6. The Apps comparator in rebuildDisplay orders the lowercased names with localeCompare and falls back to the id only on a tie. AppSearch.sortedEntries, which the plugin API hands out, now orders by the lowercased key and then the name with localeCompare, so a plugin sees the menu order. The restated claim matches the collation: accented Latin names sort under their base letter; with the language's own collation (ru_RU, el_GR, zh_CN) that script comes first, before the Latin names, where a85e29ab put it after Z; under en_US or fr_FR other scripts follow the Latin names; under C or C.UTF-8 Qt keeps code-point order. The real shell shows each of these orders. The node witnesses pin the comparator: seq-apps-locale-ru/el/zh collate as that locale through @locale, seq-apps-nonlatin as en-US, and the PR test's fourth case runs the real sortedEntries. The formula and the defensive violation row (REVIEW-261003-JTMM) are unchanged.

    Cited code (5)
  6. Claude Pr New D · AI agentApprovedSpec conformanceOct 3, 2026 · 23 hours agoREVIEW-261003-AP6S

    Re-review after the restatement on quattro-proof 87c3ca68. The comparator in rebuildDisplay orders the lowercased names with localeCompare and falls back to the id only on a tie, so the rows follow the collation of the locale, not a promise that every name sorts under a Latin letter. Accented Latin names sort under their base letter (seq-apps-french, seq-apps-german, seq-apps-decomposed). Greek, Cyrillic, Arabic and Han names sort after the Latin names, at base and at head (seq-apps-nonlatin). Symbol-led names now sort before digits and letters (seq-apps-symbols), the same order the real shell shows under en_US.UTF-8. Qt supplies the collation in the shell; under C or C.UTF-8 it keeps code-point order, so the change is a no-op there (real shell). The node witnesses pin the comparator, not Qt's collation. The formula and the defensive violation row (REVIEW-261003-JTMM) are unchanged.

    Cited code (4)
  7. Claude Pr New D · AI agentApprovedSpec conformanceOct 3, 2026 · yesterdayREVIEW-261003-JTMM

    Read shell/plugins/menu/Menu.qml on the pr-new-D tree (upstream a85e29ab plus the fix). rebuildDisplay, with no search query and the Apps menu active, collects the visible child rows and sorts them with an inline comparator. The comparator lowercases both labels and orders them by localeCompare; only when localeCompare returns 0 does it fall back to the item id, compared with < and >. So apps_rows_rebuilt leads to apps_rows_in_letter_order in the same call, before the rows go to displayModel. rebuildDisplay is the only place that fills displayModel for a non-dmenu menu, and every path that shows the Apps menu (openExistingMenu, setActiveMenu, provider refresh) calls it. With a search query the search sort applies instead, which already used localeCompare. The violation row (a rebuilt Apps list that is not in that order) needs the comparator to go back to the code-unit < and > of a85e29ab; it is dispositioned defensive. The PR's test test/shell.d/menu-apps-order-test.sh extracts this comparator from Menu.qml and runs it on French and German names and on a case tie; it fails on a85e29ab.

    Cited code (5)

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).

FRETish formula

when apps_rows_rebuilt the menu_view shall immediately satisfy apps_rows_in_letter_order

Variables

NameTypeDirectionDescription
apps_rows_rebuilt—The Apps menu rows are rebuilt for display with no search query, from the desktop entry names in the user's language.
apps_rows_in_letter_order—The Apps rows are in localeCompare order of their lowercased names under the collation of the locale. A name that starts with an accented Latin letter sorts under its base letter. Names in other scripts sort where the collation puts them: first for the script of the locale, otherwise after the Latin names. Equal names keep their id order.

Witnesses· 3 scenarios total

  • menu-apps-order-bdiff-test.sh:1
    exercises 2 condition scenarios
  • menu-apps-order-test.sh:1
    exercises 1 condition scenario

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.

Covereda test exercises this rowExempteda reviewed mcdc:ignoreNo-actionfalse-result row satisfied by designUncoveredneeds a covering test
#apps_rows_in_letter_orderapps_rows_rebuiltResultProvesCovering test
1FFTapps_rows_rebuilt
2FTFapps_rows_in_letter_order—
3TTTapps_rows_in_letter_order

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).

If you change this

Requirements
0
Files
2
Tests
19
At-risk contracts
0

Files to re-check (2)

  • Menu.qmlshell/plugins/menu/Menu.qml
  • AppSearch.jsshell/services/AppSearch.js

Tests to re-run (19)

  • seq-apps-ascii.eventstest/bdiff/corpus/lifecycle/seq-apps-ascii.events
  • seq-apps-case-tie.eventstest/bdiff/corpus/lifecycle/seq-apps-case-tie.events
  • seq-apps-decomposed.eventstest/bdiff/corpus/lifecycle/seq-apps-decomposed.events
  • seq-apps-encoding.eventstest/bdiff/corpus/lifecycle/seq-apps-encoding.events
  • seq-apps-first-row.eventstest/bdiff/corpus/lifecycle/seq-apps-first-row.events
  • seq-apps-french-reordered.eventstest/bdiff/corpus/lifecycle/seq-apps-french-reordered.events
  • seq-apps-french.eventstest/bdiff/corpus/lifecycle/seq-apps-french.events
  • seq-apps-german.eventstest/bdiff/corpus/lifecycle/seq-apps-german.events
  • seq-apps-locale-el.eventstest/bdiff/corpus/lifecycle/seq-apps-locale-el.events
  • seq-apps-locale-ru.eventstest/bdiff/corpus/lifecycle/seq-apps-locale-ru.events
  • seq-apps-locale-zh.eventstest/bdiff/corpus/lifecycle/seq-apps-locale-zh.events
  • seq-apps-nonlatin.eventstest/bdiff/corpus/lifecycle/seq-apps-nonlatin.events
  • seq-apps-plugin-list.eventstest/bdiff/corpus/lifecycle/seq-apps-plugin-list.events
  • seq-apps-plugin-tie.eventstest/bdiff/corpus/lifecycle/seq-apps-plugin-tie.events
  • seq-apps-root-control.eventstest/bdiff/corpus/lifecycle/seq-apps-root-control.events
  • seq-apps-symbols.eventstest/bdiff/corpus/lifecycle/seq-apps-symbols.events
  • harness.mjstest/bdiff/harness.mjs
  • menu-apps-order-bdiff-test.shtest/shell.d/menu-apps-order-bdiff-test.sh
  • menu-apps-order-test.shtest/shell.d/menu-apps-order-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.

Sign in to discuss this with the proof team.Sign in