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.
A menu action may exactly match the bare-summon grammar: omarchy-shell shell summon <id>, plus an optional single-quoted payload.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
A menu action may exactly match the bare-summon grammar: omarchy-shell shell summon <id>, plus an optional single-quoted payload. The payload carries no embedded quote and the id draws from [A-Za-z0-9._-]+. Such an action executes in-process via shell.summon(id, payload) instead of spawning bash. An absent payload defaults to an empty object literal, matching the bin/omarchy-shell argv default exactly. Any action outside that grammar falls back to the unchanged execDetached bash path. The fast path must preserve semantics: same plugin id, same payload bytes, same default.
when action_is_bare_summon the menu_model shall eventually satisfy in_process_summon_equivalent
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Upstream c231097d (#13435) added MenuModel.summonAction and the execAction fast path. bin/omarchy-shell:51 defaults a missing payload to '{}', exactly like match[2] || '{}'. The regex grammar is a strict subset of bash word-splitting here: the id charset excludes metacharacters, and the payload admits no embedded quote. A 10/10 edge battery on 2026-09-28 confirmed the equivalence. Exotic inputs fall back to bash.
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
- Kimi Upstream Watch · AI agent
- Reviewed
- Sep 28, 2026, 08:10 UTC
History
- Created
- Sep 28, 2026, 08:03 UTC · Leonid Bugaev
- Modified
- Sep 28, 2026, 09:16 UTC · Leonid Bugaev
Hazard review
- scenarioreviewedmalformed_inputboundaryedge_case
malformed_input: an action string that half-matches the summon grammar (trailing junk, unbalanced quote, shell substitution) must NOT take the fast path - verified by battery cases 5-10 all returning null (bash fallback). boundary: payload absent vs empty-string - absent defaults to '{}' matching omarchy-shell:51; an explicit empty-quotes payload matches with the empty string upgraded to '{}' (match[2] falsy), a byte divergence triaged unreachable+benign in CRS-0021/C01. edge_case: payload containing double quotes/spaces inside single quotes passes through with bytes identical to bash word-splitting (battery case 4).
- propertyrevieweddeterminism
summonAction is a pure regex match over the action string: same input always takes the same path (10/10 battery + replay determinism). The in-process call is synchronous on the UI thread where the bash path was async-detached; ordering of the summon relative to menu close is now deterministic (summon completes before execAction returns), which removes rather than adds a race.
- domainnot applicable
No domain workload tags. The fast path crosses no new trust boundary: the action string was already user-config data executed with user privileges; in-process dispatch reaches the same shell.summon IPC handler the bash path reaches over the socket (shell.qml:1840).
- structuralnot applicable
GC'd JavaScript (QML JS engine); no manual memory, pointers, binary framing, or format strings.
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.
- Kimi Upstream Watch · AI agentApprovedSpec conformanceSep 28, 2026 · 5 days agoREVIEW-74
New guarantee authored this campaign for the upstream summonAction fast path (c231097d). Verified by construction against MenuModel.js summonAction (regex is a strict subset of bash word-splitting: id charset [A-Za-z0-9._-] excludes metacharacters; payload admits no embedded single quote so bash passes bytes identically; missing payload defaults to '{}' exactly as bin/omarchy-shell:51 does for the 3-arg form) and by execution: 10/10 edge battery (2026-09-28, this run) plus the upstream-authored node assertions in menu-test.sh now tagged as 8VJQ MC/DC witnesses. Fallback path (execDetached) untouched for non-matching actions; refusal path (summon returns falsy) falls through to bash per the Menu.qml shape assertion. Fretish formula action_is_bare_summon -> eventually in_process_summon_equivalent matches the gating branch.
Cited code (3)
Open known issues
Findings currently open against this requirement — issues its verification surfaced that are not resolved yet. Each links to the full finding.
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 catalogueTwo independently computed answers to the same question shall agree for every shared input, within a stated tolerance, while both paths are live.
- differentialrequiredpresentCovered 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 action_is_bare_summon the menu_model shall eventually satisfy in_process_summon_equivalent
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| action_is_bare_summon | — | The action string matches the bare-summon grammar 'omarchy-shell shell summon <id> ['<payload>']' (id [A-Za-z0-9._-]+, payload single-quoted, no embedded quote). | |
| in_process_summon_equivalent | — | The action runs in-process via shell.summon(id, payload) with bash-equivalent argv semantics (payload defaults to '{}' exactly as bin/omarchy-shell line 51 does for the 3-arg form); non-matching actions keep the unchanged execDetached bash path. |
Witnesses· 2 scenarios total
- menu-test.sh:1exercises 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| # | action_is_bare_summon | in_process_summon_equivalent | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | action_is_bare_summon | |
| 2 | T | F | F | action_is_bare_summon | — |
| 3 | T | T | T | in_process_summon_equivalent |
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 (2)
- Menu.qmlshell/plugins/menu/Menu.qml
- MenuModel.jsshell/plugins/menu/MenuModel.js
Tests to re-run (1)
- menu-test.shtest/shell.d/menu-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.