Proof Portal

Sign in
Project overview

Omarchy

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

Behavioral change review

Fix menu JSONC parsing: commas in strings, array roots, inline comments

by buger4 changed files6 requirements by changed function · 24 by whole-file tracemerge:0e2dd894 (merge of head ff77cd02)
Changes required

Investigate the 21 blocking findings not shown to pre-date this change: fix, or establish they are not caused by it. 2 other blocking findings pre-date it (held at the base too).

Review decision
Review by exceptionSupported detail stays available, not in your way.
Legacy full view
Quick reviewFull detail

What am I accepting?

Declared by the change request: Fix menu JSONC parsing: commas in strings, array roots, inline comments

ChangeFix menu JSONC parsing: commas in strings, array roots, inline comments#13250, #13492, #13493
19 modified4 added7 affected requirements are not intended to change — each must keep holdingCompare exact intent
7 requirements reached only through a trace to a whole changed file
  • When a route resolves to an action item with a non-empty action, the action runs directly and no menu opens.SW-REQ-260922-N3RM
  • Search lists current-menu matches before deeper (drilldown) matches, with a divider section exactly when both groups are non-empty.SW-REQ-260922-TKDP
  • When a route resolves to a link item, the menu opens at the link's target.SW-REQ-260922-XW52
  • Dynamic rows (apps, provider enumerations) replace their source's previous batch atomically: orphans dropped, duplicates listed once, static rows untouched.SYS-REQ-260922-0M8A
  • A route string (exact id, declared alias, or normalized spelling) opens the item it denotes; unknown strings fall through as literal ids.SYS-REQ-260922-R8DQ
  • A filter query narrows to visible, selectable rows whose name or description matches every term, ranked by match quality.SYS-REQ-260922-V7W6
  • The menu Lock row invokes the lock component's CLI entry point omarchy-system-lock with no arguments. The callee engages the session lock and exits 0.SYS-REQ-260927-WC89
Pull request description · as submitted at evaluation (Oct 1, 2026, 20:12 UTC)

Fixes #13250, fixes #13492, fixes #13493.

This replaces #13255, #13511 and #13512, which fixed these bugs one at a time and conflicted in menu-test.sh. It is one commit on quattro 8b4eae6.

Note

Three menu-JSONC parsing bugs, fixed in one string-aware pass. The shipped menu parses unchanged (the same 344 rows), and the result is compared against #13681 on 200,000 generated documents.

What this changes

IssueWhat goes wrong on quattroAfter this PR
#13250a comma inside a string (, ] or , } in a label or action) is silently eatenthe string is kept intact
#13492an array root turns into entries "0", "1", …an array root contributes no entries
#13493one inline // comment makes the whole file fail to parseinline comments are handled, the file parses

stripJsonc becomes one string-aware pass, and parseMenuJsonc returns no rows for an array root. docs/menu.md states these rules.

How the new pass works

String contents are copied as is; outside a string, // drops the rest of its line (keeping the newline), and a comma is dropped only when the next thing that isn't whitespace or a // comment is } or ]. parseMenuJsonc returns no rows for an array root, as it already does for null, numbers and strings.

Reproduce each bug (one-liners, from the repo root)

#13250 — commas inside strings are eaten. The trailing-comma regex doesn't know about strings, so a , ] or , } inside a label or action gets "repaired" and the parse still succeeds:

node -e 'const m=require("./shell/plugins/menu/MenuModel.js"); console.log(m.parseMenuJsonc(`{"b": {"label": "x, ]y", "action": "mv f{.bak,}"}}`).map(r => [r.label, r.action]))'

quattro: [ [ 'x ]y', 'mv f{.bak}' ] ]. This PR: [ [ 'x, ]y', 'mv f{.bak,}' ] ].

#13492 — an array root turns into entries `"0"`, `"1"`, …. typeof [] === "object", so an array passes the root check and for..in walks its indices:

node -e 'const m=require("./shell/plugins/menu/MenuModel.js"); console.log(m.parseMenuJsonc(`[{"label": "x"}, {"label": "y"}]`).map(r => r.id))'

quattro: [ '0', '1' ]. This PR: [].

#13493 — one inline comment empties the menu. Only whole-line // comments are stripped, so an inline tail reaches JSON.parse, which throws:

node -e 'const m=require("./shell/plugins/menu/MenuModel.js"); console.log(m.parseMenuJsonc(`{"a": {"label": "A"}} // note`).length)'

quattro: 0. This PR: 1.

A 16-second capture of the shipped parser on quattro 8b4eae6 and then on this branch, reading a menu whose last entry ends with a trailing comma and an inline // favorites comment, and the shipped sample config with its examples enabled: quattro returns 0 rows, this branch returns all 3:

https://github.com/user-attachments/assets/709e8dcf-9c19-4523-947b-23a91e13f9ea

What it could affect

Only stripJsonc and parseMenuJsonc in shell/plugins/menu/MenuModel.js; the shipped menu parses to the same 344 rows, with identical row data. /* */ block comments stay unsupported.

Important

A trailing comma, then a // comment line, then } must keep parsing: the sample extension looks like that once its example rows are uncommented. #13512 and #13681 both break it; here the comma check also skips comments.

Reproduce the trailing-comma-then-comment shape

The sample extension is config/omarchy/extensions/omarchy-menu.jsonc. Folding comments into the scanner breaks this shape unless the comma check also skips comments — which is why that clause is there.

node -e 'const m=require("./shell/plugins/menu/MenuModel.js"); console.log(m.parseMenuJsonc(`{\n  "a": {"label": "A"},\n  // "b": {"label": "B"},\n}`).length)'

quattro: 1. #13512 (f75205f) and #13681 (6acbace): 0. This PR: 1.

How to check it

  • test/shell.d/menu-test.sh gets 16 new assertions (127 → 143 ok)
  • every branch and condition in the rewritten parser is exercised in both directions
  • the shipped menu is unchanged: 344 rows, identical row data
  • every menu test still passes, and so do the related PRs' own menu-test.sh files
  • 200,000 generated documents parse the same as #13681, except for the comma fix
The 16 new assertions — 9 that fail on quattro, 7 that pin behaviour it already gets right
  • 9 fail on `quattro`: comma inside a label and inside an action; array root, plain and commented; inline tail; mixed whole-line and inline comments; JSON syntax inside a comment; trailing comma then an inline comment before } and before ].
  • 7 pin behaviour `quattro` already gets right: escaped backslash before a trailing comma; object root; an items array skipped while its sibling entry still parses; // inside a string; trailing comma, whole-line comment, }; {"n": 1//c + newline + 2} still rejected; the sample extension with its example rows uncommented.

Together with the generated-input comparison below, these exercise every branch and condition in the rewritten parser in both directions.

Run every menu test, and the related PRs' own tests, against this branch

Every shell test that reads the menu parser or menu files passes on this branch, as on quattro (Linux, Node 26):

for f in $(grep -rlE 'MenuModel|parseMenuJsonc|stripJsonc|omarchy-menu\.jsonc|menu/Menu\.qml' test/shell.d); do bash "$f" >/dev/null 2>&1 && echo "ok   $f" || echo "FAIL $f"; done

The menu-test.sh files from #13255, #13511, #13512, #13681, #13305 and #6525 also pass when run against this branch's code.

Compare with #13681 on 200,000 generated documents (compare.js)

Save the script below as compare.js and run:

git fetch https://github.com/omacom/omarchy pull/13681/head && git show FETCH_HEAD:shell/plugins/menu/MenuModel.js > /tmp/MenuModel-13681.js && node compare.js /tmp/MenuModel-13681.js

It prints 200000 documents: 4187 parse differently; with the comment-skip clause off: 0. So on this input the comma check is the only difference in stripping.

// node compare.js <other MenuModel.js>   (from the repo root of this branch)
// Generates JSONC documents and compares what this branch's stripJsonc and the
// other file's stripJsonc parse them to. Also reruns the comparison with this
// branch's "skip // comments after a comma" clause turned off.
const fs = require('fs'), vm = require('vm')
const load = src => { const c = {}; vm.runInNewContext(src + '\nthis.s = stripJsonc', c); return c.s }
const mine = fs.readFileSync('shell/plugins/menu/MenuModel.js', 'utf8')
const noSkip = mine.replace(/\} else if \(input\[next\] === "\/" && input\[next \+ 1\] === "\/"\) \{/, '} else if (false) {')
if (noSkip === mine) throw new Error('comment-skip clause not found')
const a = load(mine), b = load(fs.readFileSync(process.argv[2], 'utf8')), c = load(noSkip)
let seed = 7
const rnd = n => (seed = (seed * 1103515245 + 12345) & 0x7fffffff) % n, pick = xs => xs[rnd(xs.length)]
const ws = () => pick(['', ' ', '\n', '  ', '\r\n', '\t', ' \f', ' '])
const com = () => pick(['', '', '// c\n', '// "q" , ] }\n', ' // x', '//\n', ' // t\n'])
const str = () => '"' + pick(['x', 'x, ]y', 'a // b', 'q\\\\', 'e\\"', '{.bak,}', 'u']) + '"'
const val = d => [str, () => pick(['1', 'true', 'null']), () => arr(d + 1), () => obj(d + 1)][rnd(d > 2 ? 2 : 4)]()
const list = (o, c, item) => { let n = rnd(3), s = o + ws() + com(); for (let i = 0; i < n; i++) { s += item() + ws() + com(); if (i < n - 1 || rnd(2)) s += ',' + ws() + com() } return s + ws() + c }
const arr = d => list('[', ']', () => val(d))
const obj = d => list('{', '}', () => pick(['"a"', '"label"', '"action"', '"aliases"']) + ws() + ':' + ws() + val(d))
const parse = (f, s) => { try { return JSON.stringify(JSON.parse(f(s))) } catch (e) { return 'ERR' } }
const N = 200000
let differ = 0, differNoSkip = 0
for (let k = 0; k < N; k++) {
  const s = com() + (rnd(5) ? obj(0) : arr(0)) + ws() + com()
  const pb = parse(b, s)
  if (parse(a, s) !== pb) differ++
  if (parse(c, s) !== pb) differNoSkip++
}
console.log(`${N} documents: ${differ} parse differently; with the comment-skip clause off: ${differNoSkip}`)

Open points

#13681 by @AnPod fixes the same three issues the same way, except for the comma check above. #13305 and #6525 touch the same lines, so whichever lands first makes the others conflict.

Related PRs
PRWhat it coversNote
#13681 by @AnPodthe same three issues, same approachapart from the comma check above, it behaves the same; it also rejects array roots
#13305 by @Cid-oe#13250 on its owntouches the same lines
#6525 by @itscallsshinline commentstouches the same lines

What I'm asking

A review of this as the single fix for #13250, #13492 and #13493.

Note

If you'd rather merge #13681, carrying over the comma lookahead and its tests would be enough, and I'll close this one.

Independent verification: the menu parser's requirements, tests and coverage are on https://portal.reqproof.com/projects/omarchy.

23 requirements · approved → proposed clause

A proposed clause is not approved because a related test passes.

  • SW-REQ-260922-2JZT
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    The rewrite touches only the plain $(reader) form, mapping it to the captured slot. command -v reader, VAR=x reader, and every other form runs the real command.

    when plain_substitution_form the guard_pipeline shall eventually satisfy only_plain_form_substituted

    v2 · proposed in this change

    The rewrite touches only the plain $(reader) form, mapping it to the captured slot. command -v reader, VAR=x reader, and every other form runs the real command.

    when plain_substitution_form the guard_pipeline shall eventually satisfy only_plain_form_substituted

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-47T8

  • SW-REQ-260922-3T3F
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    Unparseable input (after stripping), non-object JSON, and non-object entries yield an empty or skipped item set; no exception escapes the parser.

    when json_invalid the menu_model shall eventually satisfy empty_item_set & !parse_error_raised

    v2 · proposed in this change

    Unparseable input (after stripping), non-object JSON, and non-object entries yield an empty or skipped item set; no exception escapes the parser.

    when json_invalid the menu_model shall eventually satisfy empty_item_set & !parse_error_raised

    Metadata only — clause unchanged. Changed fields: rationale · parent SYS-REQ-260922-PPDW

  • SW-REQ-260922-46HY
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    An entry with action is an action, with target a link, otherwise a menu. An undeclared parent derives from the dotted id (or root). Root's parent is empty.

    when entry_shape_declared the menu_model shall eventually satisfy kind_and_parent_inferred

    v2 · proposed in this change

    An entry with action is an action, with target a link, otherwise a menu. An undeclared parent derives from the dotted id (or root). Root's parent is empty.

    when entry_shape_declared the menu_model shall eventually satisfy kind_and_parent_inferred

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-PPDW

  • SW-REQ-260922-74BZ
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    A route matching no id and no alias resolves to the literal input. A misspelling still attempts to open that id without a rewrite.

    when route_input & !exact_id_match & !alias_match the menu_router shall eventually satisfy route_is_literal_input

    v2 · proposed in this change

    A route matching no id and no alias resolves to the literal input. A misspelling still attempts to open that id without a rewrite.

    when route_input & !exact_id_match & !alias_match the menu_router shall eventually satisfy route_is_literal_input

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-R8DQ

  • SW-REQ-260922-7NPE
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    A user entry overrides the default per key while keeping the row's original order slot. The model injects a root item with label Go when no source declares one.

    when user_entry_overrides the menu_model shall eventually satisfy per_key_override_applied & root_injected

    v2 · proposed in this change

    A user entry overrides the default per key while keeping the row's original order slot. The model injects a root item with label Go when no source declares one.

    when user_entry_overrides the menu_model shall eventually satisfy per_key_override_applied & root_injected

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-PPDW

  • SW-REQ-260922-CYB9
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    Absent an exact id, a route equal to a declared alias resolves to the id of the item declaring the alias. Alias comparison lowercases and maps underscores to dashes.

    when route_input & !exact_id_match & alias_match the menu_router shall eventually satisfy route_is_alias_target

    v2 · proposed in this change

    Absent an exact id, a route equal to a declared alias resolves to the id of the item declaring the alias. Alias comparison lowercases and maps underscores to dashes.

    when route_input & !exact_id_match & alias_match the menu_router shall eventually satisfy route_is_alias_target

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-R8DQ

  • SW-REQ-260922-DQ9P
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    A row matches only when every query term appears in its name text (label, leaf id, aliases) or as a whole word in its description. Invisible and disabled rows never match.

    when query_terms_given the menu_search shall eventually satisfy all_terms_matched & row_hidden_from_results

    v2 · proposed in this change

    A row matches only when every query term appears in its name text (label, leaf id, aliases) or as a whole word in its description. Invisible and disabled rows never match.

    when query_terms_given the menu_search shall eventually satisfy all_terms_matched & row_hidden_from_results

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-V7W6

  • SW-REQ-260922-E4J2
    menumodified
    v1 · previously approved

    The parser strips full-line // comments and trailing commas before JSON parsing, so the authored JSONC parses to its declared entries.

    when jsonc_has_comments_or_commas the menu_model shall eventually satisfy items_parsed

    v2 · proposed in this change

    The parser strips // comments and trailing commas outside string literals before JSON parsing, so the authored JSONC parses to its declared entries.

    when jsonc_has_comments_or_commas the menu_model shall eventually satisfy items_parsed

    Changed fields: description, rationale · parent SYS-REQ-260922-PPDW

  • SW-REQ-260922-EFNR
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    swapProviderRows drops exactly the rows carrying the re-run provider's providerMenu and appends the new batch, leaving static children and other providers' rows untouched.

    when provider_reran the menu_model shall eventually satisfy previous_batch_replaced

    v2 · proposed in this change

    swapProviderRows drops exactly the rows carrying the re-run provider's providerMenu and appends the new batch, leaving static children and other providers' rows untouched.

    when provider_reran the menu_model shall eventually satisfy previous_batch_replaced

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-0M8A

  • SW-REQ-260922-JRW1
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    Applied guard results drive the view. A row hides when its when: is false. A static submenu or link hides when no descendant is visible, while provider-backed menus stay visible. A checked:true or disabled:true row earns the check-mark label. A disabled row dims and skips the cursor.

    when guard_results_applied the menu_view shall eventually satisfy rows_hidden_or_marked_per_results

    v2 · proposed in this change

    Applied guard results drive the view. A row hides when its when: is false. A static submenu or link hides when no descendant is visible, while provider-backed menus stay visible. A checked:true or disabled:true row earns the check-mark label. A disabled row dims and skips the cursor.

    when guard_results_applied the menu_view shall eventually satisfy rows_hidden_or_marked_per_results

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-47T8

  • SW-REQ-260922-MQ37
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    The generated guard script holds exactly one if-line per declared when, checked, or disabled, each echoing <id>:<w|c|d>:<0|1>; items with no guard get none.

    when guards_declared the guard_pipeline shall eventually satisfy one_line_per_guard

    v2 · proposed in this change

    The generated guard script holds exactly one if-line per declared when, checked, or disabled, each echoing <id>:<w|c|d>:<0|1>; items with no guard get none.

    when guards_declared the guard_pipeline shall eventually satisfy one_line_per_guard

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-47T8

  • SW-REQ-260922-PRNV
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    An exact id match wins over every alias. App rows are never routable, so an installed app's keywords cannot shadow a menu route (htop ships Keywords=system).

    when route_input & exact_id_match the menu_router shall eventually satisfy route_is_exact_id

    v2 · proposed in this change

    An exact id match wins over every alias. App rows are never routable, so an installed app's keywords cannot shadow a menu route (htop ships Keywords=system).

    when route_input & exact_id_match the menu_router shall eventually satisfy route_is_exact_id

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-R8DQ

  • SW-REQ-260922-RGCV
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    The prelude's omarchy-pkg-present/missing shadows agree with pacman -Q everywhere. This covers provides resolution, version constraints deferred to pacman, and the no-argument case (present true of nothing, missing not).

    when pkg_presence_asked the guard_pipeline shall eventually satisfy shadow_matches_pacman

    v2 · proposed in this change

    The prelude's omarchy-pkg-present/missing shadows agree with pacman -Q everywhere. This covers provides resolution, version constraints deferred to pacman, and the no-argument case (present true of nothing, missing not).

    when pkg_presence_asked the guard_pipeline shall eventually satisfy shadow_matches_pacman

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-47T8

  • SW-REQ-260922-SJ7P
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    Scores tier exact label, whole-word app name, label prefix, label substring, name text, then description. Menus and links promote by 2, apps demote by 5 within a tier. Final order breaks ties by depth then declaration order.

    when match_quality_varies the menu_search shall eventually satisfy better_match_ranks_first

    v2 · proposed in this change

    Scores tier exact label, whole-word app name, label prefix, label substring, name text, then description. Menus and links promote by 2, apps demote by 5 within a tier. Final order breaks ties by depth then declaration order.

    when match_quality_varies the menu_search shall eventually satisfy better_match_ranks_first

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-V7W6

  • SW-REQ-260922-W17G
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    A value command shared by several guards (e.g. omarchy-default-browser across seven rows) runs once per batch, captured eagerly before any guard line.

    when reader_value_reused the guard_pipeline shall eventually satisfy reader_read_once

    v2 · proposed in this change

    A value command shared by several guards (e.g. omarchy-default-browser across seven rows) runs once per batch, captured eagerly before any guard line.

    when reader_value_reused the guard_pipeline shall eventually satisfy reader_read_once

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-47T8

  • SW-REQ-260922-Y58B
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    When no item declares a guard, the guard script is empty and no guard process runs.

    when no_guards_declared the guard_pipeline shall eventually satisfy empty_guard_script

    v2 · proposed in this change

    When no item declares a guard, the guard script is empty and no guard process runs.

    when no_guards_declared the guard_pipeline shall eventually satisfy empty_guard_script

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-47T8

  • SW-REQ-260922-Z680
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    mergeAppRows and swapProviderRows return fresh maps that drop orphan ids and the replaced batch. They list a duplicated incoming id once and never write into their input maps.

    when orphan_id_present | provider_reran the menu_model shall eventually satisfy orphans_dropped & id_listed_once & inputs_not_mutated

    v2 · proposed in this change

    mergeAppRows and swapProviderRows return fresh maps that drop orphan ids and the replaced batch. They list a duplicated incoming id once and never write into their input maps.

    when orphan_id_present | provider_reran the menu_model shall eventually satisfy orphans_dropped & id_listed_once & inputs_not_mutated

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-0M8A

  • SW-REQ-260927-66FWnew in this change
    menuadded
    v1 · previously approved

    New requirement — no prior clause.

    v2 · proposed in this change

    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)

    Changed fields: status, priority, category, req_type, fretish, description, formalization_strategy, parent, component, rationale, variables, traces.satisfies, verification.assurance_level, verification.formalization_status · parent SYS-REQ-260922-PPDW

  • SW-REQ-260928-8VJQ
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    A menu action may exactly match the bare-summon grammar: omarchy-shell shell summon <id>, plus an optional single-quoted payload. The payload carries no embedded quote and the id draws from [A-Za-z0-9._-]+. Such an action executes in-process via shell.summon(id, payload) instead of spawning bash. An absent payload defaults to an empty object literal, matching the bin/omarchy-shell argv default exactly. Any action outside that grammar falls back to the unchanged execDetached bash path. The fast path must preserve semantics: same plugin id, same payload bytes, same default.

    when action_is_bare_summon the menu_model shall eventually satisfy in_process_summon_equivalent

    v2 · proposed in this change

    A menu action may exactly match the bare-summon grammar: omarchy-shell shell summon <id>, plus an optional single-quoted payload. The payload carries no embedded quote and the id draws from [A-Za-z0-9._-]+. Such an action executes in-process via shell.summon(id, payload) instead of spawning bash. An absent payload defaults to an empty object literal, matching the bin/omarchy-shell argv default exactly. Any action outside that grammar falls back to the unchanged execDetached bash path. The fast path must preserve semantics: same plugin id, same payload bytes, same default.

    when action_is_bare_summon the menu_model shall eventually satisfy in_process_summon_equivalent

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent SYS-REQ-260922-R8DQ

  • SW-REQ-260928-BMFEnew in this change
    menuadded
    v1 · previously approved

    New requirement — no prior clause.

    v2 · proposed in this change

    A top-level JSON array is not an object map of menu entries. The parser returns an empty item set for it, as it does for every other non-object root. No phantom rows with numeric ids appear.

    when array_root_present the menu_model shall always satisfy array_root_rejected

    Changed fields: status, priority, category, req_type, fretish, description, formalization_strategy, parent, component, rationale, variables, traces.satisfies, verification.assurance_level, verification.formalization_status · parent SYS-REQ-260922-PPDW

  • SW-REQ-260928-C8W1new in this change
    menuadded
    v1 · previously approved

    New requirement — no prior clause.

    v2 · proposed in this change

    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

    Changed fields: status, priority, category, req_type, fretish, description, formalization_strategy, parent, component, rationale, variables, traces.satisfies, verification.assurance_level, verification.formalization_status · parent SYS-REQ-260922-PPDW

  • SW-REQ-261001-BNZGnew in this change
    menuadded
    v1 · previously approved

    New requirement — no prior clause.

    v2 · proposed in this change

    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

    Changed fields: status, priority, category, req_type, fretish, description, formalization_strategy, parent, component, rationale, variables, traces.satisfies, verification.assurance_level, verification.formalization_status · parent SYS-REQ-260922-PPDW

  • SYS-REQ-260922-PPDW
    menumetadata only — clause unchangedmodified
    v1 · previously approved

    The default JSONC and the user extension merge into one ordered item tree: per-key user overrides, stable order, inferred kinds and parents, injected root.

    when menu_sources_loaded the menu_model shall eventually satisfy item_tree_merged

    v2 · proposed in this change

    The default JSONC and the user extension merge into one ordered item tree: per-key user overrides, stable order, inferred kinds and parents, injected root.

    when menu_sources_loaded the menu_model shall eventually satisfy item_tree_merged

    Metadata only — clause unchanged (only review stamps / timestamps / lifecycle bookkeeping changed). · parent STK-REQ-260922-XTNR

Behaviour changesCompatibility not checked

This evaluation recorded no backward-compatibility check — compatibility is unknown, not confirmed.

What could it affect?

30 unique requirements in 1 area. 2 changed files are unmapped; the boundary is open.

30 requirementsGrouped into 1 area
Behavioural areaWhy affected RequirementsEvidence gaps
2 changed files are outside the mapped boundary. 30 is the identified scope, not a guaranteed maximum. Inspect gaps
1 area contains 30 requirements; areas are disjoint groups, not samples.View this scope’s evidence
Scope and interface boundaries · no interface contract crossed

Engine scope reading: One focused change All 30 touched requirement(s) are related in the intent graph (satisfies/parent, sibling or shared component).

1 spec cluster (engine grouping, not areas)

Interface contracts crossed

None recorded.

Why should I believe it works?

No test outcome can be joined: test results weren't collected for this evaluation.

  • 59 obligation checks
  • 23 with no linked test yet
  • 36 covered by more specific requirements
  • 30 requirements
  • 20 with a check still open
  • 7 settled through more specific requirements or an open known issue accepted as debt
  • 3 with no observed test outcome
Test report: not configured17/17 changed decision lines reached merge:0e2dd894
Configure/emit test results — no outcome can be joined

Per-test results could not be read (test results weren't collected for this evaluation), so none of the 59 obligation cells in scope has an observed outcome.

Required work

No test outcome joined yet — 30 of 30 not observed (a missing observation, not a failing test).

Requirements this change reaches: the row-level observed result, then the obligation kinds the spec requires with the observed outcome of each kind's tagged tests.
Requirement / behaviourError handling (obligation kind — observed)BoundaryExternal call timeout boundedNominalMalformed input+3 kindsNext step
SW-REQ-260922-3T3FUnparseable input (after stripping), non-object JSON, and non-object entries yield an empty or skipped item set; no exception escapes the parser.Menu
Not observedNot observed————Add evidence
SW-REQ-260922-E4J2The parser strips // comments and trailing commas outside string literals before JSON parsing, so the authored JSONC parses to its declared entries.Menu
Child spec (inherited from SYS-REQ-260922-PPDW)Child spec (inherited from SYS-REQ-260922-PPDW)—————
SW-REQ-260927-66FWnew in this changeThe 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.Menu
Child spec (inherited from SYS-REQ-260922-PPDW)Child spec (inherited from SYS-REQ-260922-PPDW)——Not observed—Add evidence
SW-REQ-260928-BMFEnew in this changeA top-level JSON array is not an object map of menu entries. The parser returns an empty item set for it, as it does for every other non-object root. No phantom rows with numeric ids appear.Menu
Child spec (inherited from SYS-REQ-260922-PPDW)Child spec (inherited from SYS-REQ-260922-PPDW)——Not observed—Add evidence
SW-REQ-260928-C8W1new in this changeWhen 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.Menu
Child spec (inherited from SYS-REQ-260922-PPDW)Child spec (inherited from SYS-REQ-260922-PPDW)——Not observed—Add evidence
SW-REQ-261001-BNZGnew in this changeThe 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.Menu
Child spec (inherited from SYS-REQ-260922-PPDW)Child spec (inherited from SYS-REQ-260922-PPDW)——Not observedAdd evidence
SW-REQ-260922-2JZTThe rewrite touches only the plain $(reader) form, mapping it to the captured slot. command -v reader, VAR=x reader, and every other form runs the real command.Menu
Child spec (inherited from SYS-REQ-260922-47T8)—No linked test (inherited from SYS-REQ-260922-47T8)———Add evidence
SW-REQ-260922-46HYAn entry with action is an action, with target a link, otherwise a menu. An undeclared parent derives from the dotted id (or root). Root's parent is empty.Menu
Child spec (inherited from SYS-REQ-260922-PPDW)Child spec (inherited from SYS-REQ-260922-PPDW)—————
SW-REQ-260922-74BZA route matching no id and no alias resolves to the literal input. A misspelling still attempts to open that id without a rewrite.Menu
—Not observed————Add evidence
SW-REQ-260922-7NPEA user entry overrides the default per key while keeping the row's original order slot. The model injects a root item with label Go when no source declares one.Menu
Child spec (inherited from SYS-REQ-260922-PPDW)Child spec (inherited from SYS-REQ-260922-PPDW)—————
SW-REQ-260922-CYB9Absent an exact id, a route equal to a declared alias resolves to the id of the item declaring the alias. Alias comparison lowercases and maps underscores to dashes.Menu
—Child spec (inherited from SYS-REQ-260922-R8DQ)—————
SW-REQ-260922-DQ9PA row matches only when every query term appears in its name text (label, leaf id, aliases) or as a whole word in its description. Invisible and disabled rows never match.Menu
———————
✓ Supported× Mismatch≠ Conflicting◷ Stale○ Not observed / no linked test↳ Child spec— Not specifiedObserved per obligation class
Evidence limits · 15 skipped checks · code reach is not behavioural evidence
Skipped checks — did not run, so they prove nothing either way
  • build_matrix_complete no build_targets declared
  • description_grammar_enumeration_complete Turned off in the project's check policy
  • documentation_coverage Turned off in the project's check policy
  • documented_claim_verified no documented_behaviors declared
  • dual_path_guards_equivalent no dual-path rules declared
  • known_issue_closure_platform_bound no known issue declares platforms
  • lemma_binding_freshness no separate-file lemma bindings recorded yet
  • no_authored_change_surface_reviewed Turned off in the project's check policy
  • security_surface_covered Turned off in the project's check policy
  • signal_fixtures_valid Turned off in the project's check policy
  • slow_tests_clean Test results weren't collected for this evaluation
  • solver_latency_clean solver latency check skipped: detected 2 concurrent proof processes; rerun in isolation for honest measurement
  • spec_lint_mediation_contract_contradicted Turned off in the project's check policy
  • spec_lint_na_denies_property_enforced_unevenly Turned off in the project's check policy
  • spec_lint_na_denies_property_the_code_manages Turned off in the project's check policy
Not checked
  • 4 relevant tests — no per-test result recorded
  • Whether 4 relevant tests actually run the changed code
  • 2 changed files traced to no requirement
  • Side effects of the changed functions (what they now call or write) — not reported in this package
  • 3 possible problems raised by the AI review that no test settles yet:
    • Question: if upstream merges ff77cd02 WITHOUT b2dae8db, does a menu file with a BOM or a Unicode space before a // comment stop loading?
    • Question: does the scanner behave the same under Qt's QV4 engine as under node?
    • Question: do user extensions that were silently ignored before now load and override shipped entries?
    Read the AI review
  • 8 AI review remarks no recorded fact can confirm or refute (opinion, not evidence) Read the AI review
  • 15 audit checks skipped or not run
  • Who produced this evidence — the producer isn't signed, so authorship isn't attested (the content itself is checked by its digest)
Approximations and uncertainty the engine declared
  • Function level mapping comes from trace targets `path:symbol` / line ranges (authored + derived) and function local annotations; a whole file trace is file level (weak) and says nothing about which function a requirement needs.
  • Intent relations: requirement level = satisfies/parent or siblings under a parent with <= 20 children; component level = shared component (incl. traces.components); contract level = an interface requirement naming both components. A missing spec edge can make a real dependency look uncodified, and a broad contract can make an uncodified dependency look related — every candidate is a question for a reviewer, not a verdict on the code or the spec.
  • Removed code traces: targets naming a removed/renamed/moved function or a deleted file, and requirement ids cited on removed diff lines that the evaluated file no longer cites. remainingTraces counts the requirement's other code targets at the evaluated revision without re checking that each still resolves.
  • Renamed/moved detection is best effort: a removed and an added function with the same name in different files are "moved"; a different name with >= 80% identical normalized body lines (>= 3 lines) is "renamed"; anything else is removed + added.
  • Scope clusters are seeded only by directly touched requirements (spec changes and code changed); behavior affected requirements are what the change reaches and are judged by the uncodified connection rule instead.
  • Uncodified connections need call level impact (review.effects — C/C++ only today): this package has none, so NO uncodified connection could be detected. Absence of such candidates proves nothing here.
  • Units are function granular only where a parser extracts function boundaries (tree sitter languages, plus C/C++ function like macros); other changed files are one file granular unit, and hunks outside any function are attributed to the file only when no function of that file changed.
  • When a changed function is traced only at FILE level, every requirement of its file is a from side seed: a relation through any of them counts as codified, so a coarse trace can MASK an uncodified connection (and inflate scope clusters — see coarse trace).
  • effects unavailable
  • unmapped code
Code reach

17 of 17 changed decision lines reached by tests · 34 of 34 decisions fully exercised Code reach says which changed lines ran under some test; it does not say the behaviour was checked.

What remains unresolved?

24 items need work before this change can be ready.

What must change before readiness — the same gaps as the evidence table, by next action.
What needs to happenWhy it mattersWho can actInspect
Unresolved findingAdd malformed input evidence for SW-REQ-260927-66FWThe 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
Blocks readiness · High severityIntroduced by this changeChange authorInspect
Unresolved findingAdd malformed input evidence for SW-REQ-260928-BMFEA top-level JSON array is not an object map of menu entries. The parser returns an empty item set for it, as it does for every other non-object root. No phantom rows with numeric ids appear
Blocks readiness · High severityIntroduced by this changeChange authorInspect
Unresolved findingAdd malformed input evidence for SW-REQ-260928-C8W1When 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
Blocks readiness · High severityIntroduced by this changeChange authorInspect
Unresolved findingAdd malformed input and totality evidence for SW-REQ-261001-BNZGThe 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
Blocks readiness · High severityIntroduced by this changeChange authorInspect
Unresolved findingResolve the failing checkRequired check known_issue_sibling_disposition failed at the evaluated revision (it passed at the baseline: introduced).
Blocks readiness · Medium severityIntroduced by this changeChange authorInspect
Unresolved findingAdd external call timeout bounded evidence for SW-REQ-260922-2JZTThe rewrite touches only the plain $(reader) form, mapping it to the captured slot. command -v reader, VAR=x reader, and every other form runs the real command
Blocks readiness · High severityNot proven pre-existingChange authorInspect
Unresolved findingAdd boundary and error handling evidence for SW-REQ-260922-3T3FUnparseable input (after stripping), non-object JSON, and non-object entries yield an empty or skipped item set; no exception escapes the parser
Blocks readiness · High severityNot proven pre-existingChange authorInspect
Unresolved findingAdd boundary evidence for SW-REQ-260922-74BZA route matching no id and no alias resolves to the literal input. A misspelling still attempts to open that id without a rewrite
Blocks readiness · High severityNot proven pre-existingChange authorInspect
2 residual blockers pre-existing (also at base) and still block under proof.yaml @4f1a8197.
Inspect

Who decides?

Investigate the 21 blocking findings not shown to pre-date this change: fix, or establish they are not caused by it. 2 other blocking findings pre-date it (held at the base too).

Changes required

proof.yaml @4f1a8197 · Change author · merge:0e2dd894

Next decision: investigation — blocking findings are open · readiness: blocked

Policy & authority

Decisions are recorded by people with authority over the change; this page is read-only.

Required authority, approved policy and evaluated revision
Required authority
Change author · approved policy
Accepted identity
GitHub login, portal user
Approved policy
proof.yaml @4f1a8197f7b5f7eec2795c645a5a4853a194bbda
Policy digest
sha256:b8d5c5cead7a2eeb36b843204040b025993208bf7f5ae100ca80b8d0ae22fef7
Policy in this change
Unchanged
Enforcement
Portal or forge
Evaluated revision
0e2dd894093affa4a4cdea2cd7aab175ca3bb702 (merge of head ff77cd02 into base 4f1a8197)
Proof · review by exceptionEvery fact above comes from the evaluated evidence package.Legacy full view
Changes requiredBound to merge:0e2dd894
Decision