Proof Portal

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

Dispatch Lua function keybindings from the menu

by vdvoorder3 changed files2 requirements by changed function · 1 by whole-file tracemerge:8eb6c64c (merge of head 03cbacb8)
Behaviour changes need a reviewer's approval

Approve each of the 2 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.

What am I accepting?

Declared by the change request: Dispatch Lua function keybindings from the menu

ChangeDispatch Lua function keybindings from the menu
1 added2 affected requirements are not intended to change — each must keep holdingCompare exact intent

Linked to a function this change edits — it must keep holding:

  • Binds Hyprland reports as dispatcher __lua are shown with resolved keys from the source-derived cache and remain dispatchable.re-confirmedSW-REQ-260922-0W96
1 more requirement reached only through a trace to a whole changed file · re-confirmed (trace review re-stamped, no text change)
  • A code:N binding shows the keysym resolved from the compiled keymap, or the built-in fallback table when xkbcli cannot resolve it; GRAVE displays as ~.re-confirmedSW-REQ-260922-9DMS
Pull request description · as submitted at evaluation (Oct 5, 2026, 19:50 UTC)

Super + K lists Lua function bindings, but selecting one did nothing. For example, a user who zooms in, searches for Reset zoom, and presses Enter gets no reset or message; the script exits 1. Five of the 232 default bindings on Omarchy 4.0.2 are affected: Zoom in, Reset zoom, and the three universal clipboard actions. User-defined function binds have the same failure.

The menu replays the Lua config to recover each action, but a plain Lua function leaves no expression to replay. Hyprland reports these binds as __lua with a registry ref. When an expression is available from the source, the expression still wins. Otherwise, the menu records the bind's modifier mask, submap, key, keycode, and description. The record is stored base64-encoded, because later steps rewrite text in that field for display (key names for code:NN, the Omarchy bin path).

A config reload can assign the same registry ref to a different function. At dispatch time, the menu rereads hyprctl binds and requires exactly one __lua bind to match the recorded identity. The menu calls the ref currently attached to that bind through the existing hl.dispatch path, and refuses a blank or nonnumeric ref.

A reload also starts Hyprland's Lua state over. Before the lookup, each pick writes a mark of its own into a table in the Lua registry, and the call checks for that mark. A reload between the lookup and the call removes the mark, so the call raises an error and nothing runs. Overlapping picks keep separate marks, and a pick removes its own mark whether it is called or refused.

The picked row is now matched through the environment instead of awk -v, which reads a backslash in a description as an escape and then matches no row. This affected every bind kind. When two rows read the same and one of them is a function bind, the pick is refused, because the menu cannot tell which row was picked.

The cache version moves from v14 to v19 so cached rows with blank dispatcher fields are rebuilt. Open pull requests already use v15 to v18.

PR #11733 is a broader rewrite of the keybindings scan across 11 files. This PR keeps that work separate and fixes the current script.

Testing

  • bash test/shell.d/keybindings-menu-test.sh: all 33 passed (16 existing and 17 new). The stubbed hyprctl dispatch runs the dispatched expression in lua, so the tests assert which function was called.
  • Each new test fails against a version of the script with the matching defect: no mark check, one shared mark, no mark cleanup, a cleanup that empties the table, a lookup that ignores the submap or accepts two matches, awk -v for the picked row, the first of two identical rows dispatched, and a picked row that is not dispatched.
  • bash test/shell.d/bin-style-test.sh: passed.
  • git diff --check: passed.
  • Live on Omarchy with Hyprland 0.56.2, running the script with only the picker stubbed: Reset zoom changed zoom_factor from 1.5 to 1, Zoom in changed it from 1 to 2, and two menus started together both exited 0. No mark was left in the Lua registry afterwards.
  • ./test/shell: 279 of 290 test files passed. The 11 failures also fail on the unchanged base commit 821ae589; four of them require an omarchy-pkgs checkout that is not present on this machine.
  • ./test/cli: one check fails, "vscode generated theme references current theme file". It fails the same way on 821ae589 (#13131).

Not included

  • A reload between writing the mark and reading hyprctl binds refuses that pick once. Nothing runs, and picking again works.
  • A reload while the menu is open keeps the row valid as long as one bind still has the same chord, submap, and description. The menu calls whatever function that bind has now, as the key press would.
  • Function binds whose rows read the same are refused: the same chord and description in two submaps, or a press and a release bind. The picker returns only the row text. Telling such rows apart needs a row id carried through the picker, which is a separate change.
  • A function that returns { ok = false } still makes the script exit 0, because hyprctl dispatch prints ok for it.
  • The source cache is keyed by modifier mask, description, and key. A function bind that shares all three with a bind the source resolves takes that bind's expression. That keying predates this PR.
  • The comma-delimited binding record format remains unchanged. A description or key containing a comma already breaks the row for every bind kind, and none of the shipped defaults has one. Reworking the record framing would also require changes to parse_binding_records, static_bindings, and every test that reads rendered rows, so that belongs in a separate change.
SW-REQ-261005-4MKB · approved → proposed clause

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

  • SW-REQ-261005-4MKBnew in this change
    menuadded
    v1 · previously approved

    New requirement — no prior clause.

    v2 · proposed in this change

    A picked keybindings menu row for a Lua function bind calls the function through the registry ref Hyprland reports. The call happens only when one reported bind, and no other, matches the row and Hyprland did not reload its Lua state after the lookup.

    when function_bind_picked the keybindings_menu shall eventually satisfy function_bind_called <=> (one_bind_matches_identity & !lua_state_reloaded)

    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 changes2 unapproved compatibility changes

2 changes between base and head need a reviewer's approval (or a fix) · Behaviour comparison not applicable: it doesn't exercise the files this change touches (it runs shell/plugins/menu/Menu.qml, shell/plugins/menu/MenuModel.js; 213 inputs over 5 partitions).

2 behaviour changes — 0 explained, 2 with a note to read — each was checked against the requirements.

  • 1

    Binds Hyprland reports as dispatcher __lua are shown with resolved keys from the source-derived cache and remain dispatchable.

    “Same evidence under a new name. At the head, keybindings-menu-test.sh still witnesses SW-REQ-260922-0W96 rows 1-3 (line 1, scenarios 1 2 3, meets policy); only the witness name changed from…” Read the full note

    Same evidence under a new name. At the head, keybindings-menu-test.sh still witnesses SW-REQ-260922-0W96 rows 1-3 (line 1, scenarios 1 2 3, meets policy); only the witness name changed from keybindings-menu-test.sh:1 to type. The engine's generic name extractor reads `if type(action)` (test line 333, inside the hyprctl stub heredoc the PR adds) as a declaration named type; the base file matched no pattern, so it fell back to file:line. Nothing was lost.

    explained in a note per buger's note · SW-REQ-260922-0W96 · a recorded decision outcome (MC/DC) changed · see the finding

  • 1

    A code:N binding shows the keysym resolved from the compiled keymap, or the built-in fallback table when xkbcli cannot resolve it; GRAVE displays as ~.

    “Same evidence under a new name. At the head, keybindings-menu-test.sh still witnesses SW-REQ-260922-9DMS rows 1-3 (line 1, scenarios 1 2 3, meets policy); only the witness name changed from…” Read the full note

    Same evidence under a new name. At the head, keybindings-menu-test.sh still witnesses SW-REQ-260922-9DMS rows 1-3 (line 1, scenarios 1 2 3, meets policy); only the witness name changed from keybindings-menu-test.sh:1 to type. The engine's generic name extractor reads `if type(action)` (test line 333, inside the hyprctl stub heredoc the PR adds) as a declaration named type; the base file matched no pattern, so it fell back to file:line. Nothing was lost.

    explained in a note per buger's note · SW-REQ-260922-9DMS · a recorded decision outcome (MC/DC) changed · see the finding

Every finding, with base → head and the evidence · 2 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: the change modifies or deletes no existing test file.

MC/DC evidence changed

checked2 findings

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

  • unapprovedflagged for maintainerstest/shell.d/keybindings-menu-test.sh
    cf-4c5e34efd4c84e91

    MC/DC witness test keybindings-menu-test.sh:1 of SW-REQ-260922-0W96 no longer witnesses it at the head

    Base
    witness test/shell.d/keybindings-menu-test.sh:1:keybindings-menu-test.sh:1 (scenarios [1 2 3])
    Head

    Absent at head.

    Decision
    SW-REQ-260922-0W96
    Evidence
    proof evidence package assemble --base 1e43373287afbd6dca4674ad463d5b5db7812358 --baseline-run run-f5b0e01eb640a6060da0ed190e5b67f7b2a10542a9df1c0447c67ee1b6bd4fa0

    Auditor's note by buger (external auditor) on 2026-10-07 (on an earlier evaluation): Same evidence under a new name. At the head, keybindings-menu-test.sh still witnesses SW-REQ-260922-0W96 rows 1-3 (line 1, scenarios 1 2 3, meets policy); only the witness name changed from keybindings-menu-test.sh:1 to type. The engine's generic name extractor reads `if type(action)` (test line 333, inside the hyprctl stub heredoc the PR adds) as a declaration named type; the base file matched no pattern, so it fell back to file:line. Nothing was lost. — a note for the maintainers, not an approval.

  • unapprovedflagged for maintainerstest/shell.d/keybindings-menu-test.sh
    cf-8507c81c0f32c95a

    MC/DC witness test keybindings-menu-test.sh:1 of SW-REQ-260922-9DMS no longer witnesses it at the head

    Base
    witness test/shell.d/keybindings-menu-test.sh:1:keybindings-menu-test.sh:1 (scenarios [1 2 3])
    Head

    Absent at head.

    Decision
    SW-REQ-260922-9DMS
    Evidence
    proof evidence package assemble --base 1e43373287afbd6dca4674ad463d5b5db7812358 --baseline-run run-f5b0e01eb640a6060da0ed190e5b67f7b2a10542a9df1c0447c67ee1b6bd4fa0

    Auditor's note by buger (external auditor) on 2026-10-07 (on an earlier evaluation): Same evidence under a new name. At the head, keybindings-menu-test.sh still witnesses SW-REQ-260922-9DMS rows 1-3 (line 1, scenarios 1 2 3, meets policy); only the witness name changed from keybindings-menu-test.sh:1 to type. The engine's generic name extractor reads `if type(action)` (test line 333, inside the hyprctl stub heredoc the PR adds) as a declaration named type; the base file matched no pattern, so it fell back to file:line. Nothing was lost. — a note for the maintainers, not an approval.

Removed behaviour

checked0 findings

A removed or replaced expression had behaviour no test preserves.

Observed behaviour differs

ran · not applicable to this change0 findings

Base and head produced different output on the same recorded input. Run: 213 input(s) over 5 partition(s). It runs shell/plugins/menu/Menu.qml, shell/plugins/menu/MenuModel.js; this change touches none of them, so "0 findings" here says nothing about this change.

Partitions: corpus (corpus, 17), data (data, 176), lifecycle (corpus, 14), 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}

What could it affect?

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

3 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 3 requirements; areas are disjoint groups, not samples.View this scope’s evidence
Scope and interface boundaries · no interface contract crossed · 7 open spec-gap candidates

Engine scope reading: One focused change All 3 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.

Spec-gap candidates (to judge, not verdicts)
  • New code with no requirement — 7 open of 7

Each candidate is listed under What remains unresolved.

Why should I believe it works?

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

  • 4 obligation checks
  • 2 covered by more specific requirements
  • 1 covered by an open known issue (accepted as debt, not fixed)
  • 1 recorded as not applying to the requirement
  • 3 requirements
  • 3 settled through more specific requirements, an open known issue accepted as debt, or a recorded not-applicable decision
Test report: 68 passed · 0 failed · 0 skipped · 0/0 tagged tests joinedmerge:8eb6c64c
Configure/emit test results — no outcome can be joined

No test of the requirements in scope is tagged with an obligation class (<requirement>:<class>:<evidence>), so none of the 3 obligation cells in scope has an observed outcome.

Required work

No requirement needs attention on this evaluation.

✓ Supported× Mismatch≠ Conflicting◷ Stale○ Not observed / no linked test↳ Child spec◇ Accepted debt– Doesn't apply— 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: bin/omarchy-menu-keybindings
  • Whether 2 relevant tests actually run the changed code
  • Side effects of the changed functions (what they now call or write) — not reported in this package
  • 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: bin/omarchy-menu-keybindings

What remains unresolved?

3 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 itMC/DC evidence changed at test/shell.d/keybindings-menu-test.sh: MC/DC witness test keybindings-menu-test.sh:1 of SW-REQ-260922-0W96 no longer witnesses it at the head (base "witness test/shell.d/keybindings-menu-test.sh:1:keybindings-"… → head ""); not approved as a compatibility change.
Prevents a ready verdict · High severityIntroduced by this changeReviewerInspect
Unresolved findingApprove the backward-compatibility change, or fix itMC/DC evidence changed at test/shell.d/keybindings-menu-test.sh: MC/DC witness test keybindings-menu-test.sh:1 of SW-REQ-260922-9DMS no longer witnesses it at the head (base "witness test/shell.d/keybindings-menu-test.sh:1:keybindings-"… → head ""); not approved as a compatibility change.
Prevents a ready verdict · High severityIntroduced by this changeReviewerInspect
Missing evidenceConfigure/emit test results — no outcome can be joinedNo test of the requirements in scope is tagged with an obligation class (<requirement>:<class>:<evidence>), so none of the 3 obligation cells in scope has an observed outcome.
Prevents a ready verdict · Medium severityOrigin not comparedChange authorInspect

Who decides?

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

Behaviour changes need a reviewer's approval

proof.yaml @1e433732 · Reviewer · merge:8eb6c64c

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 @1e43373287afbd6dca4674ad463d5b5db7812358
Policy digest
sha256:19ad4c0c6f4aa212c59917968707493bbf687a2badfa6754165c7cf20f03d281
Policy in this change
Unchanged
Enforcement
Portal or forge
Evaluated revision
8eb6c64ca15b64e8696f8771796a93b9d76c848a (merge of head 03cbacb8 into base 1e433732)
Proof · review by exceptionEvery fact above comes from the evaluated evidence package.Legacy full view
Behaviour changes need a reviewer's approvalBound to merge:8eb6c64c