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.
When the JSONC stripper meets a // comment opener outside every string literal, it drops the comment wherever the opener sits on the line.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
When the JSONC stripper meets a // comment opener outside every string literal, it drops the comment wherever the opener sits on the line. The drop stops before the line break, so the tokens on each side stay apart. An opener inside a string literal is data, and the stripper copies it unchanged.
the menu_model shall always satisfy comment_tail_dropped <=> !comment_in_string
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Upstream MenuModel.js stripJsonc removes only whole-line comments. An inline comment tail stays in the text, JSON.parse rejects the whole file, and the menu goes empty (#13493). PR omacom/omarchy#13968 strips comments in its string-aware scanner and keeps the line break.
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 Pr 13968 · AI agent
- Reviewed
- Oct 1, 2026, 17:45 UTC
History
- Created
- Sep 27, 2026, 23:52 UTC · Kimi Zero Warnings · AI agent
- Modified
- Oct 1, 2026, 17:44 UTC · Claude Pr 13968 · AI agent
Hazard review
- scenarioreviewedmalformed_inputboundaryedge_caseinput_domain
malformed_input: an inline comment tail is legal JSONC that the stripper must remove without a change to string bytes. boundary: a comment at end of input with no line break drops to the end, and a comment between two tokens keeps its line break, so 1//c, a line break and 2 is still rejected. edge_case: // inside a string ("A // B") stays as data, JSON syntax inside a comment tail has no effect, and a whole-line comment with an unbalanced quote does not open a string. Catalog 1.11.0 re-review: input_domain applied, a // comment ends at a line feed, so LF and CRLF files keep the tokens on each side apart and any JS whitespace before the opener is read as a space; in a CR-only file a comment runs to the end of the file (KI-MENU-JSONC-CR-LINE-ENDINGS, open, not changed by this PR). 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.
- propertyrevieweddeterminism
The scanner is one left-to-right pass with no environment, order or time inputs, so the same text always strips the same way. The seeded differential test in test/node/menumodel-replay.test.mjs includes inline comments.
- domainnot applicable
No domain workload tags (HTTP, crypto or IPC frameworks) apply. The component parses a local user-authored config file into a menu model.
- structuralnot applicable
The code is garbage-collected JavaScript in the QML JS engine. It has no manual memory, pointer arithmetic, binary framing or format strings, so the C-family structural catalog does not apply.
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 Pr 13968 · AI agentApprovedSpec conformanceOct 1, 2026 · 2 days agoREVIEW-73
Re-reviewed on the PR #13968 scanner (pr/13968 mirror). The equivalence comment_tail_dropped <=> !comment_in_string matches stripJsonc: outside a string, a / followed by / enters the comment branch, which advances to the character before the next line feed (or to end of input) and emits nothing, so the line feed stays and the tokens on each side are not joined; inside a string the characters are copied before the comment test runs. Witness rows cover an inline tail at end of input, whole-line and inline comments in one pass, and // inside a string (a label and a URL in an action); the negative row shows 1//c, a line break and 2 is still rejected. The violation row needs the comment branch removed, so it is dispositioned defensive. Report #13493 now exits 0 on this tree.
Cited code (3)
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 catalogueBehavior when inputs are syntactically or structurally invalid.
FMEA mode (a): an inline comment tail stays in the text and JSON.parse rejects the whole menu file. Every row of that file goes away until the user edits the file. FMEA mode (b): a scanner that drops the line break with the comment joins the tokens on each side, so 1//c and then 2 on the next line becomes 12 and changes a value. FMEA mode (c): a comment opener inside a string is taken as a comment and cuts a label or action. The PR #13968 scanner forbids all three modes.
- negativerequiredpresentCovered by 2 tests
- nominalrequiredpresentCovered by 2 tests
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 menu_model shall always satisfy comment_tail_dropped <=> !comment_in_string
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| comment_in_string | — | The comment opener sits inside a string literal. | |
| comment_tail_dropped | — | The bytes from the comment opener up to the line break are dropped; the line break stays. |
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| # | comment_in_string | comment_tail_dropped | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | F | comment_in_string | — |
| 2 | F | T | T | comment_tail_dropped | |
| 3 | T | F | T | comment_in_string |
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
Files to re-check (1)
- MenuModel.jsshell/plugins/menu/MenuModel.js
Tests to re-run (2)
- menumodel-replay.test.mjstest/node/menumodel-replay.test.mjs
- 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.