Proof Portal
Omarchy
ProbeLabs65 findings · 95 requirementsA 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.
Make the keybindings menu's Lua bind scan safe against load-time config reads
These open items prevent a ready verdict. 04 “What remains unresolved?” lists each one and who can act on it.
What am I accepting?
Declared by the change request: Make the keybindings menu's Lua bind scan safe against load-time config reads
2 requirements reached only through a trace to a whole changed file · all re-confirmed (trace review re-stamped, no text change)
- Binds Hyprland reports as dispatcher __lua are shown with resolved keys from the source-derived cache and remain dispatchable.re-confirmedSW-REQ-260922-0W96
- 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 6, 2026, 07:40 UTC)
Problem
omarchy-menu-keybindings learns about Lua-only binds by dofile-ing the user's hyprland.lua under a stub hl whose every lookup returns a truthy noop table. Real configs read compositor state at load time, and the stub cannot survive that:
- Runaway `lua` at 100 % CPU.
for _, m in ipairs(hl.get_monitors())never terminates, becausenoop[1],noop[2], … are all non-nil. The menu exits, but theluachild keeps spinning undersystemd --useruntil reboot. Found one on my laptop that had run for 27 hours after a singleSUPER+K(PIDsomarchy-menu-keybindings→lua, 60 % of a core,dofile(hyprland.lua)never returned).
local noop = setmetatable({}, { __index = function() return noop end, __call = function() return noop end })
for _, m in ipairs(noop) do end -- never returns- Silently dropped binds. On current quattro,
default/hypr/qconsole.lua:64doesmonitor.scale <= 0, which under the stub raises attempt to compare table with number. The scan ispcall'd, so it just stops there — every Lua bind declared after thatrequireis missing from the menu (DEBUG=1showslua bind scan failed: …qconsole.lua:64).
Fix
noop.__indexanswersnilfor numeric keys (soipairs/numeric loops end),__lenis 0, and__lt/__le, arithmetic,__concat,__tostringdegrade to harmless values instead of raising. String-key lookups behave as before.- The scan is wrapped in
timeout 10so a config the stub still cannot satisfy can never outlive the menu.
Test
test/shell.d/menu-keybindings-lua-scan-test.sh extracts the embedded scan and runs it against a fixture hyprland.lua that iterates monitors, compares monitor.scale, does arithmetic/concatenation on stub fields, and then declares two binds. Without the fix it hangs for the full 10 s timeout and fails; with it the scan returns in milliseconds and both binds are reported. Also verified on my own config: the scan now completes with no scan failed and lists the Lua binds that were previously lost after qconsole.lua.
Fixes #7025
Fixes #12052
Fixes #12124
No compatibility finding from the test, MC/DC or removed-behaviour checks · 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).
Sources checked · 0 findings from 4 sources
Existing test changed
checked0 findingsAn 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
checked0 findingsThe 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, 92 at the head.
Removed behaviour
checked0 findingsA removed or replaced expression had behaviour no test preserves.
Observed behaviour differs
ran · not applicable to this change0 findingsBase 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}
2 requirements are in reach (2 whose traced file changed); none is intended to change — each must keep holding.
What could it affect?
2 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.
Scope and interface boundaries · no interface contract crossed
Engine scope reading: One focused change All 2 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?
3 obligation checks across 2 requirements — every one is passing or accounted for; none is open. The breakdown below says how each is settled.
- 3 obligation checks
- 1 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
- 2 requirements
- 2 settled through more specific requirements, an open known issue accepted as debt, or a recorded not-applicable decision
No test of the requirements in scope is tagged with an obligation class (<requirement>:<class>:<evidence>), so none of the 2 obligation cells in scope has an observed outcome.
No requirement needs attention on this evaluation.
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 3 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?
1 item needs work before this change can be ready.
| What needs to happen | Why it matters | Who can act | Inspect |
|---|---|---|---|
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 2 obligation cells in scope has an observed outcome. | Prevents a ready verdict · Medium severityOrigin not compared | Change author | Inspect |
| What needs to happen | Why it matters | Who can act | Inspect |
|---|---|---|---|
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 2 obligation cells in scope has an observed outcome. | Prevents a ready verdict · Medium severityOrigin not compared | Change author | Inspect |
Missing evidenceCoverage unmeasuredCoverage of some changed files was not measured by a fresh artifact. | For information · Low severityOrigin not compared | — | Inspect |
Missing evidenceChanged files out of scope1 changed file is outside the approved verification scope, so the audit does not verify it; listed for transparency. | For information · Info severityOrigin not compared | — | Inspect |
Missing evidenceNote the checks that did not run13 checks were skipped by configuration and produced no verdict. | For information · Info severityOrigin not compared | — | Inspect |
Partial inputNote that call-level effects were not analyzedChange effects (new calls, side effects, reachability) were not analyzed for this change. | For information · Info severityOrigin not compared | — | Inspect |
Who decides?
Produce the missing execution evidence (1 gap) for the claims this change touches.
proof.yaml @1e433732 · Change author · merge:60750dc8
Next decision: more evidence — execution evidence is missing · readiness: not ready yet
Evaluation's next step: Produce the missing execution evidence (1 gap) for the claims this change touches.
Decisions are recorded by people with authority over the change; this page is read-only.