Proof Portal
Omarchy
ProbeLabs74 findings · 89 requirementsA 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 emoji picker's search lists an emoji exactly when three things hold.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
The emoji picker's search lists an emoji exactly when three things hold. The entry has an emoji. Its keywords contain the search text. The list still has room for it. The search trims the search text and ignores case. An empty search text matches every emoji. Text that is not a JSON array gives an empty list. The list has room while fewer than the limit of matching emojis come before the entry in the picker's order. The limit is 1000 unless the caller gives a number. A limit of 0 or less lists nothing. This requirement does not state the order of the list.
the emoji_picker shall always satisfy (emoji_listed <=> (emoji_present & query_in_keywords & emoji_within_limit))
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
shell/plugins/emojis/EmojiSearch.js holds the search that the emoji picker (Emojis.qml) runs on every keystroke. parseEmojis reads emojis.json. filterEmojis builds the list with normalizedQuery and keywordText. The picker selects the first entry of the list, and Enter hands it to bin/omarchy-menu-emoji-insert, a menu action script (SYS-REQ-260922-6642). This requirement states which emojis the list holds, as the upstream code behaves. It does not state the order. Upstream keeps the order of emojis.json, so a match inside an unrelated word can come first.
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
- Claude Quattro Proof · AI agent
- Reviewed
- Oct 4, 2026, 07:53 UTC
History
- Created
- Oct 4, 2026, 07:48 UTC · Claude Quattro Proof · AI agent
- Modified
- Oct 4, 2026, 07:53 UTC · Claude Quattro Proof · AI agent
Hazard review
- scenarioreviewedboundaryedge_caseempty_input
Worst case: an emoji the search should list is missing, or one it should not list shows, and Enter inserts the wrong one. boundary: a list that reaches the limit stops there; a limit of 0 or less lists nothing; a missing or non-numeric limit counts as 1000 (witnessed). edge_case: an entry with no emoji or a missing entry is skipped even when its keywords match; capitals and spaces around the search text (witnessed). empty_input: an empty search text lists every emoji up to the limit (witnessed). input_domain is not applicable: the search text is plain typed text that filterEmojis only trims, lowercases and looks for. concurrency_scale is not applicable: the picker runs filterEmojis synchronously on each key over one fixed list.
- propertyrevieweddeterminismtotality
determinism: the same search text, emojis and limit give the same list, since filterEmojis reads nothing else. totality: every search text and limit give a list, maybe empty, and text that is not a JSON array gives an empty list.
- structuralnot applicable
Array walks and substring checks on strings that are already decoded; no memory, numeric or encoding transform beyond lowercasing.
- domainnot applicable
Which emojis the picker window lists only. No trust boundary, privilege, network, crypto or process surface; the insert helper is outside this requirement.
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.
- Claude Quattro Proof · AI agentApprovedSpec conformanceOct 4, 2026 · 1 hour agoREVIEW-261004-TD57
Read shell/plugins/emojis/EmojiSearch.js at upstream 393a43d4. filterEmojis walks the emojis once. A limit that is missing, null or not a number becomes 1000, a negative one becomes 0, and a limit of 0 returns an empty list at once. In the loop it skips an entry that is missing or has no emoji (its e field) before anything else. It then pushes the entry when the search text is empty or the lowercased keywords contain it; normalizedQuery trims and lowercases the search text and keywordText lowercases the k field. After each push it stops once the list holds the limit. So emoji_listed holds exactly when emoji_present, query_in_keywords and emoji_within_limit hold, where the room is counted in the order the loop sees the emojis. The four violation rows need the skip, the match test or the stop removed; they are dispositioned defensive. parseEmojis returns the parsed value only when it is an array and an empty list otherwise. The requirement leaves the order out: upstream lists matches in the order of emojis.json. Witnesses in test/shell.d/menu-emoji-picker-test.sh: matching emojis listed for a word, a padded capitalised and an empty search text and with the default limit; non-matching, emoji-less and over-limit entries not listed; parseEmojis on an array, an object and bad text.
Cited code (10)
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 need a synced audit
The evidence matrix behind each obligation comes from the audit index, which is produced by running an audit — not read from git. 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
the emoji_picker shall always satisfy (emoji_listed <=> (emoji_present & query_in_keywords & emoji_within_limit))
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| emoji_present | — | The entry is an object with a non-empty emoji (its e field). | |
| query_in_keywords | — | The entry's keywords (its k field), lowercased, contain the search text after trimming and lowercasing. An empty search text matches every entry. | |
| emoji_within_limit | — | Fewer than the limit of matching emojis come before the entry in the picker's order. The limit is 1000 when the caller gives none or a value that is not a number; a limit of 0 or less leaves no room. | |
| emoji_listed | — | The emoji is in the list the emoji picker's search returns. |
Witnesses· 2 scenarios total
- menu-emoji-picker-test.sh:1exercises 2 condition scenarios
MC/DC truth table· 6 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| # | emoji_listed | emoji_present | emoji_within_limit | query_in_keywords | Result | Proves | Covering test |
|---|---|---|---|---|---|---|---|
| 1 | F | F | F | F | T | emoji_listed | |
| 2 | T | F | F | F | F | emoji_listed | Exempted · defensive — filterEmojis skips a missing entry or one with no emoji before it tests the keywords or pushes, so such an entry reaches out.push only if that continue is removed (reviewed: REVIEW-261004-TD57) |
| 3 | T | F | T | T | F | emoji_present | Exempted · defensive — the emoji check runs before the keyword test, so matching keywords cannot list an entry with no emoji (reviewed: REVIEW-261004-TD57) |
| 4 | T | T | F | T | F | emoji_within_limit | Exempted · defensive — a limit of 0 returns an empty list before the loop, and the loop breaks as soon as the list holds the limit, so a match past the limit is pushed only if that break is removed (reviewed: REVIEW-261004-TD57) |
| 5 | T | T | T | F | F | query_in_keywords | Exempted · defensive — out.push sits inside the test that the search text is empty or the keywords contain it, so a non-matching entry is listed only if that test is removed (reviewed: REVIEW-261004-TD57) |
| 6 | T | T | T | T | T | emoji_present |
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
Files to re-check (1)
- EmojiSearch.jsshell/plugins/emojis/EmojiSearch.js
Tests to re-run (1)
- menu-emoji-picker-test.shtest/shell.d/menu-emoji-picker-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.