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.

PR #13968
Requirement · as recorded in PR #13968's evidenceSW-REQ-260928-BMFEAdded by this changeNot in the baseline yet

A top-level JSON array is not an object map of menu entries.

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 #13968 records it (evaluated commit e491b524); it joins the project's requirements once the change is merged and the project is audited again.

What it says

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.

Formal sentence (FRETish)when array_root_present the menu_model shall always satisfy array_root_rejected

Where it sits

Parent
SYS-REQ-260922-PPDW
Satisfies
SYS-REQ-260922-PPDW
Component
menu
Traces at the evaluated commit
1 implemented by · 1 satisfies · 2 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 · 2 tests: 2 passed · 0 failed

Obligations

Kind of evidenceFromObservedTests
Boundaryinherited from SYS-REQ-260922-PPDWObserved passing1 · 1✓ 0✗ 0∅
Error handlinginherited from SYS-REQ-260922-PPDWObserved passing1 · 1✓ 0✗ 0∅
Input domainits own checklistObserved passing1 · 1✓ 0✗ 0∅
Malformed inputits own checklistObserved passing2 · 2✓ 0✗ 0∅

Tests that verify it 2

  • test/node/menumodel-replay.test.mjspassed
  • test/shell.d/menu-test.shpassed

Code it is traced to

Changed functions
  • shell/plugins/menu/MenuModel.js:parseMenuJsonc
Implemented by
  • shell/plugins/menu/MenuModel.js:parseMenuJsonc
Changed files (3)
  • shell/plugins/menu/MenuModel.js
  • test/node/menumodel-replay.test.mjs
  • test/shell.d/menu-test.sh

Behaviour changes attributed to it

1 observed output difference · 2 compatibility findings (2 unapproved) — review them on the change

  • #13492: an array root yields no rows instead of phantom rows keyed 0,1 · 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:a97b50725d21…