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
Evaluated against proof baseline 1e43373 · baseline since moved to 18528a6 (quattro unchanged at 035ce29)
The proof baseline moved since this evaluation (7 commits, proof records only); the evidence still applies.
What moved (13 files)
- 1 requirement: 1 with meaning changes (SW-REQ-261009-GW3G)
- 5 known issues: 1 with meaning changes, 4 only changed who may see them (disclosure)
- 6 other proof records (evidence captures, reproducers, reviews, checklists)
- 1 project setting no check reads (workflow-only)
- Proof baseline 1e433732 → 18528a61 (quattro unchanged at 035ce29f)
Accept the change: the evidence is ready under the approved policy.
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 of Oct 12, 2026, 00:50 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}
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 observed passing in this run
- 1 covered by an open known issue (accepted as debt, not fixed)
- 1 recorded as not applying to the requirement
- 2 requirements
- 1 with every own check passing
- 1 settled through more specific requirements, an open known issue accepted as debt, or a recorded not-applicable decision
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
- 3 possible problems raised by the AI review that no test settles yet:
- Question: should a library call on a stub value in a user module still drop every bind loaded after it?
- Question: an unguarded numeric index on a stub list still ends the scan. Not fixed by this PR; should it be?
- Question: is a 10s wait plus a partial bind list the intended outcome for a config the stub still cannot finish?
- 9 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: bin/omarchy-menu-keybindings
What remains unresolved?
Nothing this change must still do.
| What needs to happen | Why it matters | Who can act | 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?
Accept the change: the evidence is ready under the approved policy.
No maintainer decision is recorded yet. Acceptance is not possible yet: the change moved after this evaluation.
proof.yaml @1e433732 · The maintainers (a maintainer or above) · merge:e1ff55c9
Next decision: human judgement — the evidence is ready for acceptance · readiness: ready
The project's maintainers decide; this page is a read-only view of the audit.
1 recorded decision on this change
- Assessment: recommend acceptancestalebuger · GitHub login · external auditor · 2026-10-06
The change moved after this evaluation (head, base or approved policy); the decision must be re-made on a fresh evaluation.
Recommend accepting with one suggestion: the keybindings menu's Lua bind scan now gets through the shipped config, so a user's own binds and rebinds from bindings.lua are back in the menu (the reported failure). At head 7b49d0bb, merged onto quattro-proof as e1ff55c9 (upstream quattro 035ce29), the test report shows 69 passed and 0 failed, including the PR's new scan test (3/3); that test fails with the quattro script, whose scan of the test config hangs until the 10s limit, and on the shipped config the quattro scan dies at default/hypr/qconsole.lua:123. The behaviour comparison found no difference in its 213 inputs, and the 10s time box leaves no lua running. Two patterns still end the scan before hypr.bindings and drop every later bind: a user module that hands a stub value to a library call that checks its argument type (string.format with %d, math.floor, string.lower, a numeric for limit), and, new with this head because a numeric key now answers nil, a direct first-element index such as hl.get_monitors()[1].name. Loading each module under its own pcall closes both; with that change the shipped config gives byte-identical records, and the suggested tests fail on this head and pass 5/5 with it. KI-MENU-KEYBINDINGS-SCAN-DOFILE-ABORT stays open for those cases.
History4 evidence packages for this change — each an immutable record of the commit it evaluated
- 7b49d0bbReadyAt headshown on this pageproducer not signed · digest-checkedAdmitted Oct 6, 2026 · 6 days ago
- 7b49d0bbNot ready yetAt headproducer not signed · digest-checkedAdmitted Oct 6, 2026 · 6 days ago
- 7b49d0bbNot ready yetAt headproducer not signed · digest-checkedAdmitted Oct 5, 2026 · 6 days ago
- 7b49d0bbNot ready yetAt headproducer not signed · digest-checkedAdmitted Oct 5, 2026 · 6 days ago