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.

Behavioral change review

Keep an uninstall confirmation from answering the next menu summon

by buger10 changed files32 requirements by whole-file tracemerge:04bab1c4 (merge of head 09bfcda4)
Behaviour changes need a reviewer's approval

Approve each of the 4 backward-compatibility changes: a reviewer or above approves it, or the author fixes it.

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: Keep an uninstall confirmation from answering the next menu summon

ChangeKeep an uninstall confirmation from answering the next menu summon#14052
1 modified1 added30 affected requirements are not intended to change — each must keep holdingCompare exact intent
30 requirements reached only through a trace to a whole changed file · all re-confirmed (trace review re-stamped, no text change)
  • When no row is selectable, the menu shows no cursor at all rather than parking one on a row Enter cannot run.re-confirmedSW-REQ-260922-3JG5
  • Unparseable input (after stripping), non-object JSON, and non-object entries yield an empty or skipped item set; no exception escapes the parser.re-confirmedSW-REQ-260922-3T3F
  • finishRequest with no active request or no done file just closes the menu. It creates or truncates no files.re-confirmedSW-REQ-260922-3VTN
  • The menu discards a guard batch that exits nonzero or by signal, keeping the last complete result set in effect.re-confirmedSW-REQ-260922-4079
  • 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.re-confirmedSW-REQ-260922-46HY
  • open(payload) dispatches on mode: select/input open the dmenu flow, anything else opens the resolved route. close() cancels.re-confirmedSW-REQ-260922-50RE
  • A route matching no id and no alias resolves to the literal input. A misspelling still attempts to open that id without a rewrite.re-confirmedSW-REQ-260922-74BZ
  • 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.re-confirmedSW-REQ-260922-7NPE
  • When the rows do not fit, the list height ends mid-row: the clipped peek row tells the eye there is more below the fold.re-confirmedSW-REQ-260922-B757
  • finishRequest with a null selection (Escape/cancel) creates only the done file, so the caller observes the cancel as an empty selection.re-confirmedSW-REQ-260922-C8HX
  • Absent an exact id, a route equal to a declared alias resolves to the id of the item declaring the alias.re-confirmedSW-REQ-260922-CYB9
  • Drilling in pushes the previous menu on the navigation stack. Backspace/Left pops it, or falls back to the parent menu when the stack is empty.re-confirmedSW-REQ-260922-DE93
  • 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.re-confirmedSW-REQ-260922-DQ9P
  • The parser strips full-line // comments and trailing commas before JSON parsing, so the authored JSONC parses to its declared entries.re-confirmedSW-REQ-260922-E4J2
  • swapProviderRows drops exactly the rows carrying the re-run provider's providerMenu and appends the new batch, leaving static children and other providers'…re-confirmedSW-REQ-260922-EFNR
  • finishRequest with a selection writes the value to the selection file and creates the done file, shell-quoted, and only then closes.re-confirmedSW-REQ-260922-FGZQ
  • Applied guard results drive the view. A row hides when its when: is false.re-confirmedSW-REQ-260922-JRW1
  • When a route resolves to an action item with a non-empty action, the action runs directly and no menu opens.re-confirmedSW-REQ-260922-N3RM
  • A dmenu option may lead with a glyph TAB and trail a subtext TAB. The picker shows the glyph but never returns it.re-confirmedSW-REQ-260922-NM45
  • 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).re-confirmedSW-REQ-260922-PRNV
  • Scores tier exact label, whole-word app name, label prefix, label substring, name text, then description.re-confirmedSW-REQ-260922-SJ7P
  • Search lists current-menu matches before deeper (drilldown) matches, with a divider section exactly when both groups are non-empty.re-confirmedSW-REQ-260922-TKDP
  • When a route resolves to a link item, the menu opens at the link's target.re-confirmedSW-REQ-260922-XW52
  • Cursor movement lands on the next selectable row in the direction of travel, wrapping at the list ends. Movement steps over disabled rows.re-confirmedSW-REQ-260922-Z48F
  • mergeAppRows and swapProviderRows return fresh maps that drop orphan ids and the replaced batch.re-confirmedSW-REQ-260922-Z680
  • A menu action may exactly match the bare-summon grammar: omarchy-shell shell summon <id>, plus an optional single-quoted payload.re-confirmedSW-REQ-260928-8VJQ
  • The merged item tree is addressable by id. An id present in the tree yields its item, and any other id yields null.re-confirmedSW-REQ-260929-B8N9
  • After the first filter keystroke or submenu move, the card top edge and the maximum rows height freeze at their current values.re-confirmedSW-REQ-260929-DXFJ
  • Row selection follows the pointer only after it genuinely moves past the gate threshold. It never lands on a non-selectable row.re-confirmedSW-REQ-260929-T378
  • Activating a row runs its action, follows its link, or drills into its submenu. The cursor never rests on a disabled row.re-confirmedSYS-REQ-260922-P708
Pull request description · as submitted at evaluation (Oct 3, 2026, 07:04 UTC)

Fixes #14052.

Note

A summon now cancels a pending "Do you want to uninstall …?" question, the way its Cancel button does. Before, the question stayed on top of the new prompt with Uninstall preselected, so the Enter meant for the prompt uninstalled the app and cancelled the prompt.

quattro 821ae58This PR
Delete on an app, then a prompt (omarchy-menu-select) is summonedthe question stays on top of the promptthe prompt replaces the question
Enter on that promptprompt cancelled (exit 1), app uninstalledapple, exit 0; app still installed
Same with omarchy-menu-input or omarchy menu summon <route>app uninstallednothing uninstalled
Delete, then Enter / Escape / Cancel on the question itselfuninstall / cancel / cancelunchanged

What changes

open(payloadJson) is where every summon enters the menu, on its way to openDmenu() or openRoute() → openExistingMenu(). It now calls cancelDelete() when a question is pending:

// A summon replaces the rows an uninstall confirmation was raised for,
// so the confirmation must not stay up to answer the new request.
if (root.deleteConfirmOpen) root.cancelDelete()

Until now the question was dropped on its own only in onOpenedChanged when the menu closed. A summon keeps opened true, so the question survived and kept taking every key.

Why cancelDelete() and why in open()
  • cancelDelete() is exactly what the Cancel button and Escape do. It also re-arms the pointer gate and refocuses the key catcher. The open paths do both anyway, so that repeat is harmless, and using it keeps "dismiss the question" in one place.
  • open() is the only caller of openDmenu() and openRoute(), so one line covers select, input and route summons. On the action-alias branch of openRoute() the menu closes anyway, and onOpenedChanged already cleared the question there.
  • Other paths that rebuild rows while the menu is open (JSONC reloads, onAppsChanged, providers) are not new requests, and deleteTarget holds the app id, so they can't retarget the uninstall. They are unchanged.

A 71-second narrated capture of the real shell under Quickshell, with keys from a virtual keyboard: upstream quattro 821ae58 uninstalls the app and cancels the prompt, and this branch's head 09bfcda answers the prompt and keeps the app:

https://github.com/user-attachments/assets/de6daf44-a8a2-4025-b04c-bd02a952e6fa

How to check it

  • new test/shell.d/menu-uninstall-confirm-test.sh: 10 ok; on quattro it fails at its first assertion
  • every assertion that shows the bug fails on quattro by itself, not only the first one
  • all menu tests still pass (menu-test.sh 127, menu-guards 18, menu-plugin 12, menu-images 6, keybindings-menu 16, launcher-remove 5)
  • the full ./test/shell run fails the same 17 files before and after (my Linux box isn't an Omarchy install); the new file passes
  • in the real shell (summons over IPC, keys from wtype): the issue's scenario on quattro deletes the launcher; on this branch the prompt returns apple (kiwi for an input prompt) and the launcher stays. Escape, Cancel, Enter on the question itself, and closing the menu behave as before
Commands
bash test/shell.d/menu-uninstall-confirm-test.sh

# the same test against quattro's Menu.qml (expect: not ok - a select prompt summoned over an uninstall confirmation dismisses it)
git checkout 821ae58 -- shell/plugins/menu/Menu.qml && bash test/shell.d/menu-uninstall-confirm-test.sh; git checkout HEAD -- shell/plugins/menu/Menu.qml

for f in test/shell.d/menu*-test.sh test/shell.d/keybindings-menu-test.sh test/shell.d/launcher-remove-test.sh; do
  bash "$f" >/dev/null 2>&1 && echo "ok   $f" || echo "FAIL $f"
done

For the live check, follow the issue's steps (a throwaway launcher and a queued omarchy-menu-select).

About the test

The test runs the real open, openRoute, openExistingMenu, openDmenu, requestDeleteSelected, cancelDelete, confirmDelete, cancel and finishRequest bodies from Menu.qml. It also runs the real Keys.onPressed handler and ConfirmDialog.handleKey under node:vm, with the rows, the result writer and the app library stubbed. A regex on Menu.qml could only check that the line exists. This shows the behaviour: a summon dismisses the question, and the next Enter answers the prompt and removes nothing.

  • The cases are a select prompt, an input prompt and a route summon over a pending question. One more checks that Enter on the question itself still uninstalls.
  • A last assertion fails if the code writes a property the harness doesn't stub, so the harness can't silently drift from Menu.qml.
  • It is its own file so it doesn't collide with the many open PRs that append to menu-test.sh.

What it could affect

Only the moment a summon arrives while the uninstall question is up. With no question pending, open() does what it did before. I test-merged this branch with each of the 91 open PRs that touch Menu.qml. It adds a conflict to none of them. Each merges exactly as it does with quattro, including the PRs that change open(): #13043, #13246, #12698, #8396, #8537 and #9056.

Independent verification: the evidence for this PR comes from a full proof audit of 09bfcda merged onto the current quattro (evaluated merge f7291a5): test report 56 passed · 0 failed · 0 skipped, plus 7 tests observed by the behaviour comparison run: 7 passed.

2 requirements · approved → proposed clause

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

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

    Delete with the cursor on an app row opens an uninstall confirmation naming the app. Confirming removes the app through the shared app library and closes the menu. Cancelling closes the dialog and returns focus without removing anything. Non-app rows ignore the key.

    when delete_key_on_app the menu_actions shall eventually satisfy uninstall_confirmed_flow

    v2 · proposed in this change

    Delete with the cursor on an app row opens an uninstall confirmation naming the app. Confirming removes the app through the shared app library and closes the menu. Cancelling closes the dialog and returns focus without removing anything. Non-app rows ignore the key.

    when delete_key_on_app the menu_actions shall eventually satisfy uninstall_confirmed_flow

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

  • SW-REQ-261002-VJR1new in this change
    menuadded
    v1 · previously approved

    New requirement — no prior clause.

    v2 · proposed in this change

    A summon can arrive while the uninstall confirmation shows. The menu then closes the confirmation and removes nothing, as its Cancel button does. The summoned prompt or route then takes the next key. So the confirmation cannot answer a request that replaced its rows.

    when summon_over_pending_uninstall the menu_actions shall immediately satisfy pending_uninstall_dismissed

    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-6642

Behaviour changes4 unapproved compatibility changes

4 changes between base and head need a reviewer's approval (or a fix) · behaviour comparison: 219 inputs over 5 partitions.

4 behaviour changes — all intended — each was checked against the requirements.

  • 4

    A summon can arrive while the uninstall confirmation shows. The menu then closes the confirmation and removes nothing, as its Cancel button does.

    “Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1).” Read the full note

    Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case.

    intended per buger's note · SW-REQ-261002-VJR1new in this change · see the 4 findings

Every finding, with base → head and the evidence · 4 findings from 4 sources

Existing test changed

checked0 findings

An existing test's expectation changed, or an existing test was removed, skipped or weakened. Run: 1 existing test file(s) changed.

MC/DC evidence changed

checked0 findings

The base run's and the head run's MC/DC evidence differ for a decision present in both. Run: 85 decision(s) at the base, 86 at the head.

Removed behaviour

checked1 finding

A removed or replaced expression had behaviour no test preserves.

  • unapprovedflagged for maintainerspocs/menu-qml-static.sh
    cf-4d41f5e4cae16ee6

    Removed behaviour: regex anchors ^ / $: input boundaries vs line boundaries depends on the multiline flag

    Base
    sed -n '/function openExistingMenu/,/^  }/p' "$F" | grep -qF 'deleteConfirmOpen'; st=$?
    Head
    intended change (SW-REQ-261002-VJR1)
    Evidence
    proof change behavior-diff --base 39746e651fad5ac9ccd23e581c07c43ad1596b51 --head 04bab1c4ecf40fa9f419eeb2642e3cf3fbadc7d0
    Recorded argument
    SW-REQ-261002-VJR1new in this change — an argument for the approver, never an approval

    Auditor's note by buger (external auditor) on 2026-10-03: Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

    Earlier notes (8)

    Auditor's note by buger (external auditor) on 2026-10-05 (on an earlier evaluation): Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-04 (on an earlier evaluation): Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-04 (on an earlier evaluation): Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-02 (on an earlier evaluation): Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-02 (on an earlier evaluation): Intended: a check in the proof-of-concept script that showed the confirmation surviving a summon is removed, because this PR fixes that bug (SW-REQ-261002-VJR1). The script is not part of the product, and the PR's own test now covers the case. — a note for the maintainers, not an approval.

Observed behaviour differs

checked3 findings

Base and head produced different output on the same recorded input. Run: 219 input(s) over 5 partition(s).

  • unapprovedflagged for maintainerslifecycle
    cf-58419914dab2f835

    Output differs on lifecycle input "# Verifies: SW-REQ-261002-VJR1\n# Delete raises the uninstall"…

    Base
    # omarchy-bdiff v1 lifecycle\n
events MDIK\n
caller 1 input: <cancel>\n
final opened=false mode=input requestActive=false doneFileOwner=-\n
actions -\n
apps -\n
confirm open=false target=-\n
removed firefox\n
stray-writes -\n
    Head
    # omarchy-bdiff v1 lifecycle\n
events MDIK\n
caller 1 input: ""\n
final opened=false mode=input requestActive=false doneFileOwner=-\n
actions -\n
apps -\n
confirm open=false target=-\n
removed -\n
stray-writes -\n
    Evidence
    proof change behavior-diff --base 39746e651fad5ac9ccd23e581c07c43ad1596b51 --head 04bab1c4ecf40fa9f419eeb2642e3cf3fbadc7d0
    Input
    # Verifies: SW-REQ-261002-VJR1\n # Delete raises the uninstall confirmation, then an input prompt is summoned and Enter is pressed.\n M D I K\n
    Digest
    sha256:ae8371708551…
    Recorded argument
    classified intended · SW-REQ-261002-VJR1new in this change — an argument for the approver, never an approval

    Auditor's note by buger (external auditor) on 2026-10-03: Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Earlier notes (8)

    Auditor's note by buger (external auditor) on 2026-10-05 (on an earlier evaluation): Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-04 (on an earlier evaluation): Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-04 (on an earlier evaluation): Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-02 (on an earlier evaluation): Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-02 (on an earlier evaluation): Intended: an input prompt summoned over the uninstall confirmation now closes it, so the next Enter answers the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

  • unapprovedflagged for maintainerslifecycle
    cf-64edcd0cc0114af1

    Output differs on lifecycle input "# Verifies: SW-REQ-261002-VJR1\n# Delete raises the uninstall"…

    Base
    # omarchy-bdiff v1 lifecycle\n
events MDMK\n
callers -\n
final opened=false mode=menu requestActive=false doneFileOwner=-\n
actions -\n
apps -\n
confirm open=false target=-\n
removed firefox\n
stray-writes -\n
    Head
    # omarchy-bdiff v1 lifecycle\n
events MDMK\n
callers -\n
final opened=false mode=menu requestActive=false doneFileOwner=-\n
actions -\n
apps firefox\n
confirm open=false target=-\n
removed -\n
stray-writes -\n
    Evidence
    proof change behavior-diff --base 39746e651fad5ac9ccd23e581c07c43ad1596b51 --head 04bab1c4ecf40fa9f419eeb2642e3cf3fbadc7d0
    Input
    # Verifies: SW-REQ-261002-VJR1\n # Delete raises the uninstall confirmation, then a route is summoned and Enter is pressed.\n M D M K\n
    Digest
    sha256:ee09e12e7f5f…
    Recorded argument
    classified intended · SW-REQ-261002-VJR1new in this change — an argument for the approver, never an approval

    Auditor's note by buger (external auditor) on 2026-10-03: Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

    Earlier notes (8)

    Auditor's note by buger (external auditor) on 2026-10-05 (on an earlier evaluation): Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-04 (on an earlier evaluation): Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-04 (on an earlier evaluation): Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-02 (on an earlier evaluation): Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-02 (on an earlier evaluation): Intended: a menu route summoned over the uninstall confirmation now closes it, so the next Enter acts on the new menu instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; Enter, Escape and Cancel on the dialog itself behave as before. — a note for the maintainers, not an approval.

  • unapprovedflagged for maintainerslifecycle
    cf-c57a38ab9ab3f83e

    Output differs on lifecycle input "# Verifies: SW-REQ-261002-VJR1\n# Delete raises the uninstall"…

    Base
    # omarchy-bdiff v1 lifecycle\n
events MDSK\n
caller 1 select: <cancel>\n
final opened=false mode=select requestActive=false doneFileOwner=-\n
actions -\n
apps -\n
confirm open=false target=-\n
removed firefox\n
stray-writes -\n
    Head
    # omarchy-bdiff v1 lifecycle\n
events MDSK\n
caller 1 select: "alpha"\n
final opened=false mode=select requestActive=false doneFileOwner=-\n
actions -\n
apps -\n
confirm open=false target=-\n
removed -\n
stray-writes -\n
    Evidence
    proof change behavior-diff --base 39746e651fad5ac9ccd23e581c07c43ad1596b51 --head 04bab1c4ecf40fa9f419eeb2642e3cf3fbadc7d0
    Input
    # Verifies: SW-REQ-261002-VJR1\n # Delete raises the uninstall confirmation, then a select prompt is summoned and Enter is pressed.\n M D S K\n
    Digest
    sha256:5aa49b042edf…
    Recorded argument
    classified intended · SW-REQ-261002-VJR1new in this change — an argument for the approver, never an approval

    Auditor's note by buger (external auditor) on 2026-10-03: Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Earlier notes (8)

    Auditor's note by buger (external auditor) on 2026-10-05 (on an earlier evaluation): Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-04 (on an earlier evaluation): Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-04 (on an earlier evaluation): Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-03 (on an earlier evaluation): Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-02 (on an earlier evaluation): Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

    Auditor's note by buger (external auditor) on 2026-10-02 (on an earlier evaluation): Intended: a select prompt summoned over the uninstall confirmation now closes it, so the next Enter picks from the prompt instead of uninstalling the app (SW-REQ-261002-VJR1). This fixes #14052; nothing is removed, as with the dialog's Cancel button. — a note for the maintainers, not an approval.

Partitions: corpus (corpus, 17), data (data, 176), lifecycle (corpus, 20), scale (scale, 3), timing (timing, 3) · harness h="${OMARCHY_BDIFF_HARNESS:-test/bdiff/harness.mjs}"; [ -f "$h" ] || { echo "behaviour-diff harness missing at this revision: $h" >&2; exit 127; }; exec node "$h" {rev} {input}

30 requirements are in reach (30 whose traced file changed); none is intended to change — each must keep holding.

What could it affect?

32 unique requirements in 1 area. Every changed file in the verification scope maps to a requirement. 1 changed file is outside the verification scope (e.g. reproducers) — listed for transparency.

32 requirementsGrouped into 1 area
Behavioural areaWhy affected RequirementsEvidence gaps
1 changed file is outside the verification scope (e.g. reproducers) — listed for transparency.
1 area contains 32 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 32 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?

48 obligation checks across 32 requirements — every one is passing or accounted for; none is open. The breakdown below says how each is settled.

  • 48 obligation checks
  • 31 observed passing in this run
  • 14 covered by more specific requirements
  • 3 covered by an open known issue (accepted as debt, not fixed)
  • 32 requirements
  • 20 with every own check passing
  • 9 settled through more specific requirements or an open known issue accepted as debt
  • 3 verified by their own tests (no obligation checklist)
Test report: 56 passed · 0 failed · 0 skipped · 6/6 tagged tests joined7 tests observed by the behaviour comparison run: 7 passed · 0 failed merge:04bab1c4

No requirement needs attention on this evaluation.

✓ Supported× Mismatch≠ Conflicting◷ Stale○ Not observed / no linked test↳ Child spec◇ Accepted debt— Not specifiedObserved per obligation class
Evidence limits · 13 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
  • 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
  • Coverage not measured for: test/bdiff/corpus/lifecycle/seq-delete-confirm-cancel-button.events, test/bdiff/corpus/lifecycle/seq-delete-confirm-enter.events, test/bdiff/corpus/lifecycle/seq-delete-confirm-escape.events (+3 more)
  • Whether 20 relevant tests actually run the changed code
  • Side effects of the changed functions (what they now call or write) — not reported in this package
  • 2 possible problems raised by the AI review that no test settles yet:
    • Question: on a real Quickshell, does the next key after a summon over the confirmation reach the new prompt?
    • Question: is dismissing the confirmation also right when the summon re-opens the menu the user is already in?
    Read the AI review
  • 8 AI review remarks no recorded fact can confirm or refute (opinion, not evidence) Read the AI review
  • 13 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
Code reach

0 of 0 changed decision lines reached by tests Code reach says which changed lines ran under some test; it does not say the behaviour was checked.

Not measured: test/bdiff/corpus/lifecycle/seq-delete-confirm-cancel-button.events, test/bdiff/corpus/lifecycle/seq-delete-confirm-enter.events, test/bdiff/corpus/lifecycle/seq-delete-confirm-escape.events, test/bdiff/corpus/lifecycle/seq-delete-confirm-then-input-enter.events, test/bdiff/corpus/lifecycle/seq-delete-confirm-then-menu-enter.events, test/bdiff/corpus/lifecycle/seq-delete-confirm-then-select-enter.events

Removed behaviour · 1 behaviour of replaced expressions
Replaced expressionBehaviour it hadAccounted for by
pocs/menu-qml-static.sh
sed -n '/function openExistingMenu/,/^ }/p' "$F" | grep -qF 'deleteConfirmOpen'; st=$?		regex anchors ^ / $: input boundaries vs line boundaries depends on the multiline flagintended changeSW-REQ-261002-VJR1new in this change

What remains unresolved?

4 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 findingApprove the backward-compatibility change, or fix itRemoved behaviour at pocs/menu-qml-static.sh: Removed behaviour: regex anchors ^ / $: input boundaries vs line boundaries depends on the multiline flag (base "sed -n '/function openExistingMenu/,/^ }/p' \"$F\" | grep -qF"… → head "intended change (SW-REQ-261002-VJR1)"); not approved as a compatibility change.
Prevents a ready verdict · Medium severityIntroduced by this changeReviewerInspect
Unresolved findingApprove the backward-compatibility change, or fix itObserved behaviour differs at lifecycle: Output differs on lifecycle input "# Verifies: SW-REQ-261002-VJR1\n# Delete raises the uninstall"… (base "# omarchy-bdiff v1 lifecycle\nevents MDIK\ncaller 1 input: <ca"… → head "# omarchy-bdiff v1 lifecycle\nevents MDIK\ncaller 1 input: \"\"\n"…); not approved as a compatibility change.
Prevents a ready verdict · Medium severityIntroduced by this changeReviewerInspect
Unresolved findingApprove the backward-compatibility change, or fix itObserved behaviour differs at lifecycle: Output differs on lifecycle input "# Verifies: SW-REQ-261002-VJR1\n# Delete raises the uninstall"… (base "# omarchy-bdiff v1 lifecycle\nevents MDMK\ncallers -\nfinal ope"… → head "# omarchy-bdiff v1 lifecycle\nevents MDMK\ncallers -\nfinal ope"…); not approved as a compatibility change.
Prevents a ready verdict · Medium severityIntroduced by this changeReviewerInspect
Unresolved findingApprove the backward-compatibility change, or fix itObserved behaviour differs at lifecycle: Output differs on lifecycle input "# Verifies: SW-REQ-261002-VJR1\n# Delete raises the uninstall"… (base "# omarchy-bdiff v1 lifecycle\nevents MDSK\ncaller 1 select: <c"… → head "# omarchy-bdiff v1 lifecycle\nevents MDSK\ncaller 1 select: \"a"…); not approved as a compatibility change.
Prevents a ready verdict · Medium severityIntroduced by this changeReviewerInspect

Who decides?

Approve each of the 4 backward-compatibility changes: a reviewer or above approves it, or the author fixes it.

Behaviour changes need a reviewer's approval

proof.yaml @39746e65 · Reviewer · merge:04bab1c4

Next decision: human judgement — backward-compatibility changes are unapproved · readiness: not ready yet

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
Reviewer · approved policy
Accepted identity
GitHub login, portal user
Approved policy
proof.yaml @39746e651fad5ac9ccd23e581c07c43ad1596b51
Policy digest
sha256:6849bf0c5173df9a4c032c277bbbe7e2c44d26de26fa1c342a64e75ef30cb5fe
Policy in this change
Unchanged
Enforcement
Portal or forge
Evaluated revision
04bab1c4ecf40fa9f419eeb2642e3cf3fbadc7d0 (merge of head 09bfcda4 into base 39746e65)
Proof · review by exceptionEvery fact above comes from the evaluated evidence package.Legacy full view
Behaviour changes need a reviewer's approvalBound to merge:04bab1c4
Decision