Proof Portal

Sign in
Project overview

Omarchy

ProbeLabs65 findings · 95 requirements

A 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.

Inbox
ReportR-28GitHub issuePublicFixed

Menu JSONC: an inline `//` comment tail silently empties every entry in that menu file

Reported by buger · filed Sep 28, 2026 · open at source · 5 revisions

Open at source
Decided: Duplicate — decided by agents · verified 4 days ago.

At a glance

1 · What is claimed?
  • ConfirmedViolates SW-REQ-260922-E4J2: an inline // comment tail makes parseMenuJsonc return no rows, so the whole menu file contributes nothing
  • ConfirmedReproducible: parseMenuJsonc('{"a": {"label": "A"}} // note') returns []
  • ConfirmedAffects the menu component
  • LinkedMatches known issue KI-MENU-JSONC-INLINE-COMMENT
2 · What does it affect?
AreaIn the audited areamenu· Decided by agents · verified
3 · Is it reproducible?
An engine-executed run exited 1 and showed the defect signal. See reproducer
4 · What remains unclear?
Nothing recorded as open.
5 · What happens next?
Decided by agents and verified by a second, independent agent — see the decision.

Original report

Revision12345 (current)
Menu JSONC: an inline `//` comment tail silently empties the entire menurevision 1 · captured 2026-09-28 21:23 UTC via poll

A single inline comment tail on a content line — {"a": {...}} // note — makes the entire menu come back empty. Full-line comments are handled; a comment at the end of a line silently kills every row.

Reproduced on current master (ce925cb1), using the repo's own parser, stock file fetched straight from this repo (narrated, 67s):

https://github.com/user-attachments/assets/c1078418-35ac-43b1-a11b-e09897ffa5ee

Repro (run from the repo root, node ≥ 18):

// repro.js
const m = require("./shell/plugins/menu/MenuModel.js");

console.log(m.parseMenuJsonc('{"a": {"label": "A"}} // note'));
// expected: one row "A"   actual: [] — the whole menu is gone

console.log(m.parseMenuJsonc('{"a": {"label": "A"}}').map(r => r.label));        // ["A"]  no comment: fine
console.log(m.parseMenuJsonc('// note\n{"a": {"label": "A"}}').map(r => r.label)); // ["A"]  full-line comment: fine
console.log(m.parseMenuJsonc('{"a": {"label": "A // B"}}').map(r => r.label));     // ["A // B"]  // in a string: data

What happens. The comment stripper in stripJsonc is line-anchored:

.replace(/^\s*\/\/[^\n]*(\n|$)/gm, "")

so an inline tail after content never matches and survives stripping. JSON.parse then throws on the leftover // note, and the catch in parseMenuJsonc silently returns an empty item set. One trailing comment → zero menu rows, no error surfaced.

Blast radius. JSONC's whole point is allowing comments; a user who documents an entry inline ("reboot": { … } // firmware-safe reboot) loses their entire menu and gets no hint why. The failure is silent and total rather than local to the commented line.

Fix. Strip inline comment tails too, but string-aware: // inside a string literal ("A // B") is data and must stay verbatim — the same requirement the trailing-comma scanner in #13255 already honors. We have a fix ready that extends that scanner to comments (with regression tests covering the contrasts above, node replay + shell suite), and will raise it as a PR shortly. Whichever of this and #13255 lands second is a small rebase over stripJsonc.

Found while auditing the menu component with [Proof](https://reqproof.com) — formal verification with full MC/DC coverage of the menu's bash and QML code paths.

View raw text
A single **inline** comment tail on a content line — `{"a": {...}} // note` — makes the entire menu come back empty. Full-line comments are handled; a comment at the end of a line silently kills every row.

Reproduced on current master (`ce925cb1`), using the repo's own parser, stock file fetched straight from this repo (narrated, 67s):

https://github.com/user-attachments/assets/c1078418-35ac-43b1-a11b-e09897ffa5ee

**Repro** (run from the repo root, node ≥ 18):

```js
// repro.js
const m = require("./shell/plugins/menu/MenuModel.js");

console.log(m.parseMenuJsonc('{"a": {"label": "A"}} // note'));
// expected: one row "A"   actual: [] — the whole menu is gone

console.log(m.parseMenuJsonc('{"a": {"label": "A"}}').map(r => r.label));        // ["A"]  no comment: fine
console.log(m.parseMenuJsonc('// note\n{"a": {"label": "A"}}').map(r => r.label)); // ["A"]  full-line comment: fine
console.log(m.parseMenuJsonc('{"a": {"label": "A // B"}}').map(r => r.label));     // ["A // B"]  // in a string: data
```

**What happens.** The comment stripper in `stripJsonc` is line-anchored:

```js
.replace(/^\s*\/\/[^\n]*(\n|$)/gm, "")
```

so an inline tail after content never matches and survives stripping. `JSON.parse` then throws on the leftover `// note`, and the `catch` in `parseMenuJsonc` silently returns an **empty item set**. One trailing comment → zero menu rows, no error surfaced.

**Blast radius.** JSONC's whole point is allowing comments; a user who documents an entry inline (`"reboot": { … } // firmware-safe reboot`) loses their *entire* menu and gets no hint why. The failure is silent and total rather than local to the commented line.

**Fix.** Strip inline comment tails too, but string-aware: `//` inside a string literal (`"A // B"`) is data and must stay verbatim — the same requirement the trailing-comma scanner in #13255 already honors. We have a fix ready that extends that scanner to comments (with regression tests covering the contrasts above, node replay + shell suite), and will raise it as a PR shortly. Whichever of this and #13255 lands second is a small rebase over `stripJsonc`.

*Found while auditing the menu component with [Proof](https://reqproof.com) — formal verification with full MC/DC coverage of the menu's bash and QML code paths.*
  • c1078418-35ac-43b1-a11b-e09897ffa5ee

Validation

AI validator claude-code (claude-opus-5.5) · evaluated revision 5 at product commit 1e43373287af · sealed 2026-10-04T21:45:44Z

Validator's summary (commentary, not evidence)

Re-validation of omacom/omarchy#13493 (latest revision, edited 2026-10-02) on quattro-proof 1e433732 (upstream quattro 035ce29f product code plus the proof layer). The menu parser is unchanged since the previous validation (311d29c7..1e433732 merges upstream 035ce29f, whose only menu changes are two data rows in the stock omarchy-menu.jsonc (Install/Remove > Service > Microsoft), the image-picker helper bin/omarchy-menu-images and one display property on the bar's menu button; Menu.qml, MenuModel.js, ConfirmDialog.qml and omarchy-menu-select are byte-identical, and the rest is lock-screen and other non-menu upstream changes plus proof-layer records) and the result holds. stripJsonc removes only whole-line // comments, so an inline tail after a value survives, JSON.parse throws, and parseMenuJsonc returns no rows for the whole file. The reproducer (parser level) gets [] for an inline tail after the root object and on an entry line; full-line comments, '//' inside a string, and a trailing comma followed by a comment line and the closer all keep their rows (controls). Real entry path, checked separately in the running shell: a user extension file whose first entry ends with '// my entry' contributes no rows on this baseline (both its entries vanish), and both rows appear with #13968 merged; the comma-then-comment-line shape keeps its row on both. The baseline tracks the defect as KI-MENU-JSONC-INLINE-COMMENT (open). The latest revision's table reproduces for the open PRs: #13681 fails the control (0 rows), #13968 passes both shapes; #13512 is closed and was not re-run. Documented limitation or defect? Both. docs/menu.md documents it, and #13493 argues it should change because the failure is silent. The reproducer was re-run on 1e433732 with identical output; the live-shell runs are reused from 20d4e6ae (author-recorded): Menu.qml, MenuModel.js and omarchy-menu-select are unchanged since then apart from comment-only trace lines, and the two stock-menu rows added since (Install/Remove > Service > Microsoft) are outside what these runs exercise.

  • ConfirmedViolates a requirementThe parser strips full-line // comments and trailing commas… SW-REQ-260922-E4J2

    Violates SW-REQ-260922-E4J2: an inline // comment tail makes parseMenuJsonc return no rows, so the whole menu file contributes nothing

    Engine: engine-executed run exited 1 and showed the defect signal

    What “confirmed” means here: the requirement exists and the engine reproduced the defect. That the reproducer exercises THIS requirement is the validator's argument (see rationale).

    Evidence: requirement SW-REQ-260922-E4J2 · file test/reports/report-cmulr8j7w0hy01gw4menggvbx.sh

    Validator's rationale (commentary): SW-REQ-260922-E4J2 FRETish: 'when jsonc_has_comments_or_commas the menu_model shall eventually satisfy items_parsed' (the item set parses to the declared entries). The reproducer's inline-comment inputs parse to [] instead of their declared rows. The description's narrower wording ('full-line // comments') matches docs/menu.md, which documents the limitation; the report argues it should change because the failure is silent.

  • ConfirmedReproducible

    Reproducible: parseMenuJsonc('{"a": {"label": "A"}} // note') returns []

    Engine: engine-executed run exited 1 and showed the defect signal

    Evidence: file test/reports/report-cmulr8j7w0hy01gw4menggvbx.sh

  • ConfirmedAffects a componentmenu

    Affects the menu component

    Engine: confirmed violation of SW-REQ-260922-E4J2 owned by menu

    Evidence: requirement SW-REQ-260922-E4J2 · file test/reports/report-cmulr8j7w0hy01gw4menggvbx.sh

  • LinkedDuplicate ofstripJsonc removes only whole-line // comments; an inline comment tail empties the whole file (omacom/omarchy#13493) KI-MENU-JSONC-INLINE-COMMENT

    Matches known issue KI-MENU-JSONC-INLINE-COMMENT

    Engine: the known issue exists; whether the report duplicates it is settled by a human disposition; it affects the mapped requirement(s) SW-REQ-260922-E4J2

    Evidence: known_issue KI-MENU-JSONC-INLINE-COMMENT · requirement SW-REQ-260922-E4J2

    Validator's rationale (commentary): The baseline KI records exactly this defect (an inline comment tail empties the file) and links #13493.

Known issues examined for duplicates
Engine reference checks at 1e43373287af (9/9 ok)
  • okcommit1e43373287afbd6dca4674ad463d5b5db7812358
  • okbase commit1e43373287afbd6dca4674ad463d5b5db7812358
  • okbase ancestry1e43373287afbd6dca4674ad463d5b5db7812358
  • okproduct code untouchedthis report's reproducer branch
  • okbranchthis report's reproducer branch
  • okfiletest/reports/report-cmulr8j7w0hy01gw4menggvbx.sh
  • okrequirementSW-REQ-260922-E4J2
  • okcomponentmenu
  • okknown issueKI-MENU-JSONC-INLINE-COMMENT

The engine's own check, at validation time, that the commits, the reproducer branch (touching only reproducer files), the reproducer files and every mapped requirement / component / known issue really exist.

10 earlier checks — superseded by the newest one above

Each new check of the report replaces the previous one; only the newest result above counts. Earlier results are kept for the record.

  • Reproduced— checked report revision 5 on Oct 4, 2026; earlier check, superseded
  • Reproduced— checked report revision 5 on Oct 3, 2026; earlier check, superseded
  • Reproduced— checked report revision 5 on Oct 3, 2026; earlier check, superseded
  • Reproduced— checked report revision 5 on Oct 2, 2026; earlier check, superseded
  • Reproduced— checked report revision 5 on Oct 2, 2026; earlier check, superseded
  • Reproduced— checked report revision 5 on Oct 2, 2026; earlier check, superseded
  • Reproduced— checked report revision 3 on Oct 2, 2026; earlier check, superseded
  • Reproduced— checked report revision 1 on Oct 1, 2026; earlier check, superseded
  • Refuted— checked report revision 1 on Oct 1, 2026; earlier check, superseded
  • Reproduced— checked report revision 1 on Sep 29, 2026; earlier check, superseded

Validator-authored hypothesis. Each claim's verification is engine-computed: confirmed only from an engine-executed reproducer run recorded in this record, refuted when recorded evidence contradicts it. Prose is commentary. The disposition of the report is a human decision.

Reproducer

engine-runexit 1 · expected exit 0 · defect exit 1 · 29 ms · 2026-10-04T21:45:44Z→ showed the defect
test/reports/report-cmulr8j7w0hy01gw4menggvbx.shon this report's reproducer branch @ 1e43373287
sh test/reports/report-cmulr8j7w0hy01gw4menggvbx.sh

Setup failure: exit 2 means the reproducer could not set up (e.g. the product did not build) — such a run decides nothing.

Defect signal: output contains DEFECT:

Matched lines (engine, over the full output)
DEFECT: inline comment tail after the root object -- input "{\"a\": {\"label\": \"A\"}} // note" -> rows [] (expected ["a=\"A\""])
DEFECT: inline comment tail on an entry line -- input "{\n  \"a\": {\"label\": \"A\"}, // first\n  \"b\": {\"label\": \"B\"}\n}" -> rows [] (expected ["a=\"A\"","b=\"B\""])
Observed output · 701 bytes
DEFECT: inline comment tail after the root object -- input "{\"a\": {\"label\": \"A\"}} // note" -> rows [] (expected ["a=\"A\""])
DEFECT: inline comment tail on an entry line -- input "{\n  \"a\": {\"label\": \"A\"}, // first\n  \"b\": {\"label\": \"B\"}\n}" -> rows [] (expected ["a=\"A\"","b=\"B\""])
ok: control: full-line comment -- input "// note\n{\"a\": {\"label\": \"A\"}}" -> rows ["a=\"A\""]
ok: control: // inside a string is data -- input "{\"a\": {\"label\": \"A // B\"}}" -> rows ["a=\"A // B\""]
ok: control: trailing comma, whole-line comment, closer keeps the row -- input "{\n  \"a\": {\"label\": \"A\"},\n  // note\n}" -> rows ["a=\"A\""]
RESULT: 2 case(s) violate the requirement

Needs: linux · node >= 18 on PATH (the script exits 2 with SETUP: otherwise); nothing to build: MenuModel.js is plain JavaScript loaded straight from the worktree · ran on linux/amd64

Author's comparative runs — commentary, not engine evidence
  • author-recordedon this baseline with upstream PR omacom/omarchy#13968 head b2dae8db merged · exit 0
    sh test/reports/report-cmulr8j7w0hy01gw4menggvbx.sh
    RESULT: all cases parse to the declared entries
  • author-recordedon upstream PR omacom/omarchy#13681 head 6acbace1 (its MenuModel.js over this baseline) · exit 1
    sh test/reports/report-cmulr8j7w0hy01gw4menggvbx.sh
    DEFECT: control: trailing comma, whole-line comment, closer keeps the row ... RESULT: 1 case(s) violate the requirement
  • author-recordedon live shell: Quickshell 0.3.1 on a headless sway compositor, the tree's own shell and stock menu, the user extension file ~/.config/omarchy/extensions/omarchy-menu.jsonc read by the shell's FileView; rows read back through a read-only IPC probe injected into a private copy; this baseline [run on 20d4e6ae, same menu code] · exit 1
    user extension: {"probe-mine": {...}, // my entry\n "probe-two": {...}}
    root menu shows only the 10 stock rows: Mine and Two are gone
  • author-recordedon live shell: Quickshell 0.3.1 on a headless sway compositor, the tree's own shell and stock menu, the user extension file ~/.config/omarchy/extensions/omarchy-menu.jsonc read by the shell's FileView; rows read back through a read-only IPC probe injected into a private copy; this baseline with upstream PR omacom/omarchy#13968 head b2dae8db merged [run on 20d4e6ae, same menu code] · exit 0
    same user extension file
    root menu rows Mine and Two present
  • author-recordedon live shell: Quickshell 0.3.1 on a headless sway compositor, the tree's own shell and stock menu, the user extension file ~/.config/omarchy/extensions/omarchy-menu.jsonc read by the shell's FileView; rows read back through a read-only IPC probe injected into a private copy; this baseline and with #13968 [run on 20d4e6ae, same menu code] · exit 0
    control: trailing comma, then a // comment line, then the closer
    row Mine present on both

Linked

Decision

Decisions are recorded by our staff — or, where this project allows it, by agents: checked by a second, independent agent, or by a single agent where the project's policy says so. Any decision reached so far is shown below.