Proof Portal
Omarchy
ProbeLabs73 findings · 87 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 rewrite touches only the plain $(reader) form, mapping it to the captured slot.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
The rewrite touches only the plain $(reader) form, mapping it to the captured slot. command -v reader, VAR=x reader, and every other form runs the real command.
when plain_substitution_form the guard_pipeline shall eventually satisfy only_plain_form_substituted
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
MenuModel.js substituteGuardReaders lines 462-467 and the comment at 437-442.
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:34 UTC · Kimi Dogfood · AI agent
- Modified
- Sep 27, 2026, 21:25 UTC · Kimi Zero Warnings · AI agent
Hazard review
- scenarioreviewedboundaryedge_case
Worst case: a guard expression embedding the plain form inside a larger word, e.g. x$(omarchy-default-browser)y, is substring-matched and rewritten to a broken token, so the guard script emits a malformed command that fails silently under >/dev/null 2>&1 and the row answers 0 - a row can misreport visible state. boundary: the plain-form/non-plain split is an exact-string match; forms touching it on either side are the tested partition (untouched test leaves command -v, env-prefixed, and piped forms intact). edge_case: containment occurrences and repeated occurrences of the same reader inside one expression are the unusual-but-valid inputs; global split/join handles repetition and the containment risk is graded, not ignored. Catalog 1.11.0 re-review: input_domain not applicable, it rewrites guard expressions authored in the menu config, which reach it already parsed by SW-REQ-260922-E4J2. concurrency_scale not applicable, a pure function of its arguments, recomputed on each load or keystroke: no state across calls, no process, timer or lock.
- propertyreviewedtotality
split/join over a JS string is defined for every expression value, so substitution is total: any guard expression yields a defined rewritten string; no input partition crashes or hangs the transform. malformed_input needs no separate class here - the transform never parses the expression, it only rewrites an exact literal, so unparsable shell is out of scope for this requirement and lands in the guard-execution requirements downstream.
- structuralnot applicable
Pure in-process JS string splitting and joining; no manual memory, pointers, format-string sinks, numeric casts, or encoding round-trips - the substitution is byte-level on an already-parsed string.
- domainnot applicable
In-process string transform over menu config text; no network, IPC, crypto, SQL, browser, or filesystem surface, and no domain tag on the requirement fires an applies_when.
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 Zero Warnings · AI agentApprovedSpec conformanceSep 27, 2026 · 5 days agoREVIEW-31
Read substituteGuardReaders and menu-guards-test.sh. The rewrite is a global split/join on the exact plain $(reader) form per GUARD_READERS entry; command -v reader, VAR=x reader and piped forms never match the pattern and run the real command (the 'untouched' test at line 72 proves all three non-plain forms survive verbatim). The FRETish condition plain_substitution_form models exactly the pattern-match branch; there is no other gating. Formula conforms to the code.
Cited code (1)
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
when plain_substitution_form the guard_pipeline shall eventually satisfy only_plain_form_substituted
Witnesses· 2 scenarios total
- preludeexercises 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| # | only_plain_form_substituted | plain_substitution_form | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | plain_substitution_form | |
| 2 | F | T | F | only_plain_form_substituted | Exempted · defensive — the substitution is a global replace of the exact plain form; an occurrence left behind needs a broken replace mcdc:witness-out-of-process (reviewed: REVIEW-M5) |
| 3 | T | T | T | only_plain_form_substituted |
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)
- MenuModel.jsshell/plugins/menu/MenuModel.js
Tests to re-run (1)
- menu-guards-test.shtest/shell.d/menu-guards-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.