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 takes any text as input.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
The JSONC stripper takes any text as input. Outside string literals, each character that JS \s matches is whitespace. This includes ASCII whitespace with the vertical tab and the form feed, and a byte order mark U+FEFF at the start or anywhere else. It also includes the Unicode spaces U+00A0, U+1680, U+2000 to U+200A, U+2028, U+2029, U+202F, U+205F and U+3000. The stripper keeps each line feed and emits each other such character as one ASCII space. Inside string literals it copies every character unchanged.
when space_outside_string the menu_model shall always satisfy space_passed_as_ascii
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
This requirement states the input domain of stripJsonc and parseMenuJsonc. JSON.parse accepts only four ASCII whitespace characters. A user file can still carry a byte order mark or a Unicode space from an editor or a paste. Upstream reads such a character as whitespace only before a whole-line comment, because the comment regex ^\s*// is Unicode-aware. The first PR #13968 commit (ff77cd02) lost that, so a file with a byte order mark and a leading comment had no rows. The follow-up commit efa5170b adds the \s branch to the scanner.
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
- Oct 1, 2026, 17:41 UTC · Claude Pr 13968 · AI agent
- Modified
- Oct 1, 2026, 18:41 UTC · Claude Pr 13968 · AI agent
Hazard review
- scenarioreviewedmalformed_inputboundaryedge_casetotalityinput_domain
totality: the description names every character class outside strings (each JS \s character, the comma, the comment opener, the quote, anything else via 66FW, C8W1 and E4J2) and inside strings (copied unchanged), so no input has unspecified handling. malformed_input: the input domain is any text, and each of the 19 non-ASCII characters that JS \s matches is whitespace outside strings. Witnessed rows cover a byte order mark, U+00A0, U+2028 and U+3000 before a leading comment, before an indented comment line and before the opening brace. boundary: a byte order mark as the first character and a line feed right before a comment. edge_case: Unicode spaces inside a string stay unchanged, and a carriage return becomes a space while its line feed stays. Catalog 1.11.0 re-review: input_domain applied, this requirement states the byte-level domain of the stripper: every JS whitespace character outside strings, a byte-order mark anywhere, LF / CRLF line endings, any character inside strings; U+FFFD and NUL are not whitespace and still reject the file through JSON.parse. 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 \s test is a pure character class check in a single pass, so the same text always strips the same way. A seeded differential test in test/node/menumodel-replay.test.mjs inserts all 19 non-ASCII \s characters and compares the result 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. It decodes no bytes, because the QML file reader supplies a JS string.
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-261001-ENZ2
Read stripJsonc on the PR #13968 tree including efa5170b. Outside a string, every character that is not a quote, a // opener or a comma reaches the branch /\s/.test(ch), which emits a line feed as is and any other match as one ASCII space; the in-string branch copies every character before any other test, so a Unicode space inside a string stays unchanged. JS \s is the Unicode White_Space set plus U+FEFF: the four ASCII characters JSON.parse accepts, the remaining ASCII controls \v and \f, and 19 non-ASCII characters (the test asserts the count). A leading byte order mark therefore becomes a space, so no separate BOM rule is needed. A comma look-ahead uses the same \s test, so a Unicode space between a trailing comma and its closer does not keep the comma. The violation rows need the \s branch removed (outside a string a matched character skips the rule) or a broken string branch (inside a string a character is rewritten), so both are dispositioned defensive. Witnessed rows: byte order mark, U+00A0, U+2028, U+3000, U+2003, vertical tab, form feed, tab and carriage return outside strings; U+00A0, U+FEFF and U+2029 inside a string; a seeded differential with the vertical tab, the form feed and all 19 non-ASCII characters against a token-level reference model (3000 inputs, 0 mismatches). The vertical tab and form feed are ASCII but JSON.parse rejects them too; upstream accepted them only before a // comment and ff77cd02 lost that (amended pending fix b2dae8db adds them to the PR tests).
Cited code (4)
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
2 obligations · 2 discharged
Browse the catalogueBehavior when inputs are syntactically or structurally invalid.
FMEA mode (a): a byte order mark or Unicode space outside a string reaches JSON.parse, which rejects the file, so every row of the user extension goes away with no error. This is the ff77cd02 regression for a file saved with a byte order mark and a leading comment. FMEA mode (b): the stripper also changes a Unicode space inside a string, so a label or action changes while the parse still succeeds. FMEA mode (c): the stripper replaces a line feed with a space, so a later // comment swallows the next line.
- differentialrequiredpresentCovered by 2 tests
- negativerequiredpresentCovered by 4 tests
- nominalrequiredpresentCovered by 4 tests
Every reachable input combination is covered by a requirement.
FMEA mode: a character class outside the stated domain has no specified result, so a later refactor changes it silently. The ff77cd02 commit did exactly that for a byte order mark before a comment, and no requirement or test noticed. This requirement names every JS \s character, and the differential test inserts all 19 non-ASCII ones.
- differentialrequiredpresentCovered 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
when space_outside_string the menu_model shall always satisfy space_passed_as_ascii
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| space_outside_string | — | A character outside every string literal matches JS \s: ASCII whitespace, the byte order mark U+FEFF, or a Unicode space such as U+00A0, U+2028 or U+3000. | |
| space_passed_as_ascii | — | The stripper applies its whitespace rule to the character: a line feed stays a line feed, and any other character becomes one ASCII space. |
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| # | space_outside_string | space_passed_as_ascii | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | space_outside_string | |
| 2 | T | F | F | space_outside_string | — |
| 3 | T | T | T | space_passed_as_ascii |
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.