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 JSONC stripper looks ahead from each comma outside every string literal.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
The JSONC stripper looks ahead from each comma outside every string literal. The look-ahead skips whitespace and each // comment up to its line break. The stripper drops the comma only when the next other character is a closing brace or bracket. A comma inside a string literal is data, and the stripper copies it unchanged.
the menu_model shall always satisfy trailing_comma_dropped <=> (!comma_in_string & next_char_closes_json)
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
PR omacom/omarchy#13968 replaces the two regex passes in MenuModel.js stripJsonc with one string-aware scanner. The upstream comma regex also matched inside strings, so a label such as "x, ]y" changed while the parse still succeeded (#13250). The look-ahead skips comments as well as whitespace. Thus a trailing comma, then a commented-out entry, then the closer still parses, as in the shipped extension template with its examples uncommented. A look-ahead that stops at the first non-whitespace character keeps that comma and empties the menu, which is the #13512 and #13681 regression.
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, 15:24 UTC · Leonid Bugaev
- Modified
- Oct 1, 2026, 18:04 UTC · Claude Pr 13968 · AI agent
Hazard review
- scenarioreviewedmalformed_inputboundaryedge_caseinput_domain
malformed_input: JSONC trailing commas are legal JSONC but not JSON, and the stripper must remove them without a change to string bytes. Witnessed rows cover a comma and closer inside a label and inside an action, plus a real trailing comma before } and before ]. boundary: a comma at end of input with no closer stays, and a comma followed only by a comment and then the closer is dropped. edge_case: an escaped backslash before the closing quote ends the string, and a trailing comma, then a whole-line or inline comment, then } or ] is dropped (the #13512 shape). Catalog 1.11.0 re-review: input_domain applied, the comma rule holds over the domain stated on SW-REQ-260922-E4J2 and SW-REQ-261001-BNZG: the look-ahead skips LF, CRLF and every other JS whitespace character, so a trailing comma followed by U+00A0, VT or CRLF and a closer is dropped, and a comma inside a string is data whatever characters surround it. 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. A seeded differential test in test/node/menumodel-replay.test.mjs compares it with an independent reference model.
- 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-21
Re-reviewed on the PR #13968 scanner (pr/13968 mirror; supersedes the 2026-09-27 review of the fork scanner). The equivalence trailing_comma_dropped <=> !comma_in_string & next_char_closes_json matches stripJsonc: the in-string branch copies every character before any comma test, so an in-string comma is never dropped; outside a string a comma starts a look-ahead that skips each \s character and each // comment up to (not past) its line break, and the comma is appended unless the look-ahead stops on } or ]. next_char_closes_json is therefore defined over the next character that is neither whitespace nor part of a // comment; a trailing comma, a commented-out entry and the closer drop the comma (the #13512 and #13681 regression shape stays green). End of input during the look-ahead keeps the comma. The three violation rows need the append, the closer test or the string branch broken, so they are dispositioned defensive.
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): the stripper changes a label such as "x, ]y" to "x ]y" while the parse still succeeds, so the user sees a wrong row name. FMEA mode (b): an action such as mv f{.bak,} loses its in-string comma, and the changed command runs with the user's privileges on row activation. FMEA mode (c): a look-ahead that does not skip // comments keeps a real trailing comma before a commented-out entry, JSON.parse rejects the file, and the whole file contributes no rows. JSON.parse accepts the text in modes (a) and (b), so no error shows. 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 trailing_comma_dropped <=> (!comma_in_string & next_char_closes_json)
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| comma_in_string | — | The comma sits inside a JSON string literal. | |
| next_char_closes_json | — | The next character after the comma that is neither whitespace nor part of a // comment is } or ]. | |
| trailing_comma_dropped | — | The comma is dropped from the stripped JSON before parsing. |
Witnesses· 2 scenarios total
- menu-test.sh:1exercises 2 condition scenarios
MC/DC truth table· 5 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| # | comma_in_string | next_char_closes_json | trailing_comma_dropped | Result | Proves | Covering test |
|---|---|---|---|---|---|---|
| 1 | F | F | F | T | next_char_closes_json | |
| 2 | F | F | T | F | trailing_comma_dropped | — |
| 3 | F | T | F | F | next_char_closes_json | — |
| 4 | F | T | T | T | comma_in_string | |
| 5 | T | T | T | F | comma_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.