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 menu can issue an answer while the write for an earlier answer still runs.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
The menu can issue an answer while the write for an earlier answer still runs. Several summons that arrive together cause this, because each summon cancels the request before it. The menu then starts a new write process for that answer at once, beside the running one. The menu never makes an answer wait for an earlier write, and it never drops an answer. Every caller thus gets its done file.
when finish_requested & prior_answer_write_running the dmenu_protocol shall eventually satisfy answer_write_started_concurrently
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
@omarchybot pushed head b7bd59c4 of upstream PR omacom/omarchy#9056. That head replaces the shared resultProc Process in finishRequest with Quickshell.execDetached, one fresh process per answer. On the earlier head 0b4fe292 a burst of summons stranded callers. Each cancel set resultProc.command and running = true while the previous write still ran. Quickshell ignores that, so the answer never reached its done file. In a live burst of 20 concurrent omarchy-menu-select calls, 7-12 callers stayed stuck on 0b4fe292, 19 on quattro and 0 on b7bd59c4. This closes the busy-resultProc leg (SX26/C14) of KI-MENU-REQUEST-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
- Claude Quattro Proof · AI agent
- Reviewed
- Oct 1, 2026, 21:05 UTC
History
- Created
- Oct 1, 2026, 20:46 UTC · Claude Quattro Proof · AI agent
- Modified
- Oct 1, 2026, 20:46 UTC · Claude Quattro Proof · AI agent
Hazard review
- scenarioreviewedconcurrentconcurrency_scale
This is the mitigation for the concurrent-answer hazard. Several summons that arrive together each answer the request before them while the first answer write still runs. Worst case without it: a caller polls its done file forever because its answer was set on a busy shared Process and ignored. With one detached process per answer the writes run side by side; each targets its own caller-unique done file (omarchy-menu-select and omarchy-menu-input use mktemp paths), so concurrent writes cannot cross. Residual: a write process that fails to start (fork failure) is not observed or retried; the peer-death trigger (the shell dies after a summon) is outside this requirement and stays tracked on KI-MENU-REQUEST-LIFECYCLE. Catalog 1.11.0 re-review: concurrency_scale applied. It is this requirement: answers issued while earlier writes run each start their own write (witnessed with three back-to-back pickers; a live burst of 20 left 0 callers stuck). input_domain not applicable: Util.shellQuote quotes the answer strings unchanged, and nothing is parsed here.
- propertyreviewedatomicity
finishRequest captures both file paths and clears requestActive/selectionFile/doneFile before it starts the write, so a later summon can never redirect an in-flight answer; the selection write orders printf to the selection file before the done-file truncation inside one bash command.
- domainnot applicable
No domain workload tags; the menu dmenu protocol is a local QML plugin plus bash scripts with no network, crypto, or privilege surface.
- structuralnot applicable
QML/JS (GC'd) plus bash writing shell-quoted paths; no manual memory, pointers, or binary framing.
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 1, 2026 · yesterdayREVIEW-261001-W7QD
Read finishRequest on the PR #9056 tree at head b7bd59c4. After the no-active-request early return it captures activeSelectionFile and activeDoneFile, clears requestActive/selectionFile/doneFile, and hands the answer to Quickshell.execDetached in both branches (done-only for a cancel, printf to the selection file then the done file for a selection). execDetached starts a fresh detached process on every call and reads no state of an earlier one, so an answer issued while an earlier write still runs starts its own write at once: finish_requested & prior_answer_write_running gives answer_write_started_concurrently. The violation row (an answer while a write runs, and no write of its own) needs a shared Process back in place of execDetached, which is exactly the 0b4fe292 code where a start on a running Process was ignored; it is dispositioned defensive. Witnesses in test/shell.d/menu-test.sh run the real open/finishRequest/openDmenu/openExistingMenu/openRoute bodies under node vm with writes held in flight; the back-to-back witness fails on the 0b4fe292 Menu.qml (one write of three) and passes on b7bd59c4 (three writes, the second and third concurrent). Out of the structural model: whether Quickshell really starts every execDetached process (no fork failure) is a runtime property; the live 20-summon burst left 0 callers stuck on b7bd59c4.
Cited code (2)
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).
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 finish_requested & prior_answer_write_running the dmenu_protocol shall eventually satisfy answer_write_started_concurrently
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| finish_requested | — | The QML side finishes an active request with a selection or null. | |
| prior_answer_write_running | — | The write process for an earlier answer (a cancel or a selection) has not exited yet when the menu issues the next answer. | |
| answer_write_started_concurrently | — | The menu starts a write process of its own for the new answer while the earlier answer write is still running, instead of waiting for it or dropping the new answer. |
Witnesses· 3 scenarios total
- bashReferenceSummonexercises 3 condition scenarios
MC/DC truth table· 4 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| # | answer_write_started_concurrently | finish_requested | prior_answer_write_running | Result | Proves | Covering test |
|---|---|---|---|---|---|---|
| 1 | F | F | T | T | finish_requested | |
| 2 | F | T | F | T | prior_answer_write_running | |
| 3 | F | T | T | F | answer_write_started_concurrently | — |
| 4 | T | T | T | T | answer_write_started_concurrently |
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
Nothing downstream depends on this yet
No downstream impact — "The menu can issue an answer while the write for an earlier…" has no downstream edges.
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.