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 sees a comment opener, it drops the comment only when the opener sits outside each string literal.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
When the JSONC stripper sees a comment opener, it drops the comment only when the opener sits outside each string literal. The comment runs to the end of the line. An opener inside a string literal is data and stays 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.
MenuModel.js stripJsonc stripped only line-anchored comments. An inline comment tail survived stripping, JSON.parse rejected the whole file, and the menu went empty. PoC review/upstream-repro-jsonc-inline-comment.js. Deferred claim CRS-0017/C01 = CRS-0019/C02 = CRS-0020/C01.
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, 23:58 UTC
History
- Created
- Sep 27, 2026, 23:52 UTC · Kimi Zero Warnings · AI agent
- Modified
- Sep 28, 2026, 00:04 UTC · Kimi Zero Warnings · AI agent
Hazard review
- scenarioreviewedmalformed_inputboundaryedge_case
malformed_input: an inline comment tail is legal JSONC the stripper must remove WITHOUT touching string-literal bytes; pre-fix it survived and JSON.parse rejected the whole file (empty menu). boundary: a comment opener at EOF with no newline drops to EOF (witnessed); an empty comment // does the same. edge_case: // inside a string literal ("A // B") is data and stays verbatim (witnessed); JSON syntax inside a comment tail is ignored (witnessed negative).
- propertyrevieweddeterminism
The scanner is a single left-to-right pass with no environment, ordering, or timing inputs. Identical bytes always strip identically. Differential fuzz against the pre-fix baseline is Phase 3 of this campaign.
- domainnot applicable
No domain workload tags (HTTP/crypto/IPC frameworks); the component parses a local user-authored config file into a menu model.
- structuralnot applicable
Implementation is GC'd JavaScript (QML JS engine). No manual memory, pointer arithmetic, binary framing, or format strings exist here. The structural catalog targets C-family hazards that cannot exist here.
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-73
FRETish equivalence (comment_tail_dropped <=> !comment_in_string) matches the code: stripJsonc's single pass drops bytes from a // opener to end-of-line only when outside a string literal (MenuModel.js:27-28), and copies string contents verbatim. Witness rows cover F->T twice (inline tail at EOF without newline; full-line plus inline comments in one pass), T->F (label "A // B" preserved verbatim), a negative (JSON syntax inside a comment tail ignored), and a no-action row (comment-free input unchanged). RED observed pre-fix (inline tail emptied the menu: expected 1 actual 0 in both harnesses), GREEN after folding comment stripping into the scanner.
Cited code (2)
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
1 obligation
Browse the catalogueFMEA mode (a): an inline comment tail survives stripping and JSON.parse rejects the whole menu file. Every menu row vanishes; the user loses the entire menu until the file is fixed. FMEA mode (b): a full-line comment containing a quote opens a fake string in a naive scanner. Then real content would be eaten as comment. The string-aware scanner on this branch forbids both modes. The grading records the pre-fix worst case this requirement now forbids.
Discharging tests pending a synced audit.
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 to the end of the line are dropped |
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
Nothing downstream depends on this yet
No downstream impact — "When the JSONC stripper sees a comment opener, it drops the…" has no downstream edges.
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.