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.
All when/checked/disabled expressions evaluate in one batched bash run whose per-item results drive row visibility, checkmarks, and dimming.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
All when/checked/disabled expressions evaluate in one batched bash run whose per-item results drive row visibility, checkmarks, and dimming.
when guards_evaluated the guard_pipeline shall eventually satisfy system_state_reflected
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
The menu opens on the last evaluation's answers; per-row forks made the shipped menu spend over a second contradicting the state it describes.
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 Zero Warnings · AI agent
- Reviewed
- Sep 27, 2026, 21:25 UTC
History
- Created
- Sep 22, 2026, 13:33 UTC · Kimi Dogfood · AI agent
- Modified
- Oct 1, 2026, 21:29 UTC · Claude Quattro · AI agent
Hazard review
- scenarioreviewederror_handlingedge_caseconcurrency_scale
Worst case graded in the deferral above: a blocking guard expression freezes the answer set for the session (tracked debt). error_handling: a batch killed by signal (exitStatus set) or a non-zero exit keeps the previous complete answer set - a half-read batch never adopts; a reader exiting non-zero cannot kill the batch (|| : guard); unparsable output lines are skipped by the id:tag:value shape guard. edge_case: a run arriving while one is in flight is coalesced via guardsPending and re-run once the flight lands, so concurrent evaluation requests cannot interleave collected output. nominal: one batched run drives visibility, checkmarks, and dimming from per-item answers, exactly the contract. Catalog 1.11.0 re-review: input_domain not applicable, guard expressions reach it already parsed by SW-REQ-260922-E4J2; batch output parsing is stated on SW-REQ-260922-4079. concurrency_scale applied, evaluations are requested repeatedly while a batch runs and are coalesced; the batch without a deadline is the deferred external_call_timeout_bounded obligation.
- propertyrevieweddeterminism
determinism: the same guard expressions over the same system state answer the same batch, and the batched pipeline (one bash run for all when/checked/disabled) means no per-row forking can reorder answers within an evaluation - the perf defect the req was authored against. Freshness across evaluations is bounded by the deferral above, not by non-determinism.
- structuralnot applicable
expressions are config-authored (user is the trust root for their own menu config, same disposition as the keybindings script review) and are interpolated into bash -lc after reader-slot substitution; no memory/pointer/encoding surface in the QML parser, which is a shape-guarded line splitter dispositioned under scenario.error_handling.
- domainreviewed
external_call_timeout_bounded evaluated and DEFERRED (see obligation_deferrals): the bash -lc guard child has no deadline and a blocking expression freezes guard freshness for the session, tracked as KI-MENU-GUARD-BATCH-NO-DEADLINE with a green tripwire - a child-process site, deliberately NOT attached to the KI-MENU-SELECT-POLL-DEADLOCK poll-loop KI. No other domain class fires: no network, no identity crossing, single consumer of the answers.
Change history
Every recorded revision of this requirement's source file — newest first, each with its commit message and the diff for that change.
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.
2 obligations · 1 deferred · 1 discharged
Browse the catalogueEvidence tagged via <REQ> is witnessed by a requirement that satisfies this one — normal for stakeholder / aggregate requirements, which are proven through the requirements that refine them.
Behavior when operations fail or dependencies are unavailable.
- negativerequiredpresentCovered by 1 test
- nominalrequiredpresentCovered by 1 test
Every cross-process call shall declare connect, read, and total deadlines; no external call is defaulted to "no timeout."
the whole guard batch runs as one bash -lc child with no deadline: a user guard expression that blocks (waiting on a lock, a slow probe, stdin - guardLine wraps the expression but does not redirect stdin) wedges guardProc.running forever, guardsPending then defers every later evaluation, and the menu shows the last complete answer set indefinitely - rows checked/visible per state that no longer holds. Mitigation by design: a when: only hides on explicit false, so a dead batch fails visible, and a killed batch (exitStatus set) keeps the last complete set rather than adopting a half-read one. This is a child-process-without-deadline site, NOT the reproduced done_file poll-loop mechanism of KI-MENU-SELECT-POLL-DEADLOCK. The fix shape is a Process-side deadline (kill + re-arm) with an explicit staleness policy on guard answers. Reproduced and tracked on KI-MENU-GUARD-BATCH-NO-DEADLINE with a green tripwire over the real Menu.qml guard code.
- nominalrequireddeferredWitnessing deferred — accepted while the tracking known issue stays open.
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 guards_evaluated the guard_pipeline shall eventually satisfy system_state_reflected
Witnesses· 3 scenarios total
- preludeexercises 3 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| # | guards_evaluated | system_state_reflected | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | guards_evaluated | |
| 2 | T | F | F | guards_evaluated | |
| 3 | T | T | T | system_state_reflected |
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
Requirements (7)
- The rewrite touches only the plain $(reader) form, mapping…menu · SW
- The menu discards a guard batch that exits nonzero or by…menu · SW
- Applied guard results drive the viewmenu · SW
- The generated guard script holds exactly one if-line per…menu · SW
- The prelude's omarchy-pkg-present/missing shadows agree…menu · SW
- A value command shared by several guards (emenu · SW
- When no item declares a guard, the guard script is empty…menu · SW
Files to re-check (2)
- MenuModel.jsshell/plugins/menu/MenuModel.js
- Menu.qmlshell/plugins/menu/Menu.qml
Tests to re-run (4)
- menu-guards-test.shtest/shell.d/menu-guards-test.sh
- menu-compositor-test.shtest/shell.d/menu-compositor-test.sh
- menumodel-replay.test.mjstest/node/menumodel-replay.test.mjs
- menu-test.shtest/shell.d/menu-test.sh
What this rests on
Parent requirements (1)
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.