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.

PR #14054
Requirement · as recorded in PR #14054's evidenceSW-REQ-261002-VJR1Added by this changeNot in the baseline yet

A summon can arrive while the uninstall confirmation shows.

component menu · guarantee · assurance level C

Back to the change reviewEvidence package
This change adds this requirement — it isn't in the project's baseline yet, so it has no project requirement page. Shown exactly as the evidence package for PR #14054 records it (evaluated commit ca9c8878); it joins the project's requirements once the change is merged and the project is audited again.

What it says

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.

Formal sentence (FRETish)when summon_over_pending_uninstall the menu_actions shall immediately satisfy pending_uninstall_dismissed

Where it sits

Parent
SYS-REQ-260922-6642
Satisfies
SYS-REQ-260922-6642
Component
menu
Traces at the evaluated commit
1 implemented by · 1 satisfies · 8 verified by
Fields this change sets
status, priority, category, req_type, fretish, description, formalization_strategy, parent, component, rationale, variables, traces.satisfies, verification.assurance_level, verification.formalization_status

Evidence in this change

Changed as intended — Observed passing · 8 tests: 8 passed · 0 failed

Obligations

Kind of evidenceFromObservedTests
Error handlinginherited from SYS-REQ-260922-6642No test linked yet0 · 0✓ 0✗ 0∅

Tests that verify it 1

  • test/shell.d/menu-uninstall-confirm-test.shpassed
7 tests observed by the behaviour comparison run: 7 passed · 0 failed
  • test/bdiff/corpus/lifecycle/seq-delete-confirm-cancel-button.eventspassed
  • test/bdiff/corpus/lifecycle/seq-delete-confirm-enter.eventspassed
  • test/bdiff/corpus/lifecycle/seq-delete-confirm-escape.eventspassed
  • test/bdiff/corpus/lifecycle/seq-delete-confirm-then-input-enter.eventspassed
  • test/bdiff/corpus/lifecycle/seq-delete-confirm-then-menu-enter.eventspassed
  • test/bdiff/corpus/lifecycle/seq-delete-confirm-then-select-enter.eventspassed
  • test/bdiff/harness.mjspassed

Code it is traced to

Implemented by
  • shell/plugins/menu/Menu.qml:open
Changed files (9)
  • shell/plugins/menu/Menu.qml
  • 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
  • test/bdiff/harness.mjs
  • test/shell.d/menu-uninstall-confirm-test.sh

Behaviour changes attributed to it

3 observed output differences · 4 compatibility findings (4 unapproved) — review them on the change

  • Same as the select case for an input prompt: base removed the app and cancelled the caller; head answered the prompt with the typed text (empty here) and removed nothing. · intended
  • Route summon over a raised confirmation, then Enter. Base: the stale confirmation removed the app. Head: the confirmation was cancelled; Enter activated the first row of the new menu (the app row launches, as in the harness menu) and nothing was removed. · intended
  • Delete raised the uninstall confirmation, then a select prompt was summoned and Enter pressed. Base: the stale confirmation answered (Uninstall preselected): the app was removed and the prompt caller got a cancel. Head: the summon cancelled the confirmation; Enter picked the first row (alpha) and nothing was removed. This is the fix. · intended

What to check in review

  • Confirm the new requirement is needed, sits in the right part of the spec, and is labeled with the right kind of rule and concern.
  • Check that parent decomposition and planned implementation/test/doc evidence are intentional before merge.
  • Make sure lifecycle state is merge-ready and not left as unfinished authoring work.

Every fact on this page comes from the evidence package sha256:8921e417abbb…