Proof Portal

Project overview

Omarchy

ProbeLabsviewing a historical run

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.

Viewing historical run 67b0e44Oct 1, 2026, 12:54 PMquattro-proofBack to current
All requirements
RequirementSW-REQ-260922-JREHSoftwareReview

A file chooser exit status above 1 sends a critical 'Could not share' notification and exits 1; an empty pick exits 0 silently.

This requirement changed after its last recorded review, so approval is stale. Automated checks pass and 2/2 obligations are satisfied.
PriorityshallTypeguaranteeCategoryfunctionalComponentmenuAssuranceCFindingsnone open

Specification

The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.

Description

A file chooser exit status above 1 sends a critical 'Could not share' notification and exits 1; an empty pick exits 0 silently.

FRETish formula
when chooser_failed the share_script shall eventually satisfy critical_notification_exit_one
View full formal model

Rationale & tags

Why this requirement exists, and how it is categorised.

bin/omarchy-menu-share lines 28-38; command substitution preserves the chooser's real exit status.

Verification & provenance

How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).

Assurance levelC
Formalizationvalid
Realizabilityrealizable
Vacuitychecked_ok
Strategyfretish

Review

Status
in_review
Reviewer
Kimi Zero Warnings · AI agent
Reviewed
Sep 27, 2026, 21:25 UTC

History

Created
Sep 22, 2026, 13:34 UTC · Kimi Dogfood · AI agent
Modified
Sep 30, 2026, 07:29 UTC · Leonid Bugaev

Hazard review

Reviewed Sep 30, 2026, 07:29 UTCby agent:opencode-hazard-ccatalog v1.10.1
  • scenarioreviewedboundaryedge_caseerror_handling

    Worst case: a chooser that writes a pick then exits above 1 makes the share drop a file the user explicitly chose - defined fail-safe (nothing is sent without a clean success), though the critical message (chooser did not open) can be mildly misleading about the real failure. boundary: the status 1 vs above-1 partition is the entire trigger; status 1 and the portal client EXIT_NOTHING_PICKED both land in the silent exit-0 arm because the chooser taxonomy calls both a decision rather than a fault. edge_case: a newline inside a picked filename splits readarray entries along the line protocol and the bad entry fails at the send step, never sending a wrong file; a notification-send failure under set -e aborts nonzero anyway.

  • propertyreviewedtotality

    Every chooser ending the portal client can emit (picked, cancelled, nothing-picked, crashed) resolves to exactly one share-script ending - detached send, silent exit 0, silent exit 0, critical notification with exit 1 - and the tests witness the failure and cancel quadrants.

  • structuralnot applicable

    Bash orchestration only: command substitution capturing the chooser, one readarray line split, string emptiness test; no parsing of chooser payloads beyond the line protocol, no arithmetic, no encoding transforms.

  • domainreviewed

    The traced file does reach the network, but through the systemd-run detached localsend send that is SW-REQ-260922-8ERH own send contract, not the chooser-failure arm this requirement governs; the arm itself performs only the portal call. Disposition stays reviewed rather than not_applicable because of that egress sink.

Change history

Every recorded revision of this requirement's source file — newest first, each with its commit message and the diff for that change.

Review history

Human and AI-agent approvals of this requirement — the 'why was this approved' lineage, each with the reviewer's justification and the code it cites.

  1. Kimi Zero Warnings · AI agentApprovedSpec conformanceSep 27, 2026 · 5 days agoREVIEW-52

    Read omarchy-menu-share. The file-chooser result is handled by exit status: above 1 sends a critical 'Could not share' notification and exits 1, while an empty pick exits 0 silently — the two arms match the chooser_failed condition and its complement exactly. Formula conforms to the code.

    Cited code (1)

Obligations

What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.

1 obligation · 1 suppressed

Browse the catalogue
Suppressed

Behavior when operations fail or dependencies are unavailable.

No evidence required — this obligation is excused for this requirement.

Code signals

Static-analysis signals from external scanners that bear on this requirement's obligations — the source location, the obligation each touches, and its closure status.

  • Coveredbuiltinstrict_mode_missing
    Obligation: Error handling · Scenario

    Behavior when operations fail or dependencies are unavailable.

    script runs pipelines without `set -e`/`set -o pipefail`

Formula evidence

The formal formula behind this requirement, the variables it is written over, and the tests that exercise it (each term is explained inline).

FRETish formula

when chooser_failed the share_script shall eventually satisfy critical_notification_exit_one

Witnesses· 2 scenarios total

  • menu-share-test.sh:1
    exercises 2 condition scenarios

MC/DC truth table· 3 rows

Each row assigns the formula's conditions (T/F) and shows the Result— the formula's value for that input row, not a test pass/fail. A row proves a condition when flipping only that condition flips the outcome. The test that covers each row is linked.

Covereda test exercises this rowExempteda reviewed mcdc:ignoreNo-actionfalse-result row satisfied by designUncoveredneeds a covering test
#chooser_failedcritical_notification_exit_oneResultProvesCovering test
1FFTchooser_failed
2TFFchooser_failedExempted · defensive — the status>1 arm unconditionally sends the critical notification and exits 1 mcdc:witness-out-of-process (reviewed: REVIEW-M4)
3TTTcritical_notification_exit_one

Its place

How this requirement connects — what proves it, what it affects, and what it rests on. Authored links only here; automatically derived links come from the audit index.

Loading graph…

Trace evidence

The concrete artifacts linked to this requirement — implementing code, verifying tests, documents, and the findings raised against it.

No findings affect this requirement

Nothing was flagged against this requirement in the pinned run.

Impact

Blast radius — authored trace links only (automatically derived links come from the audit index and aren't shown here).

If you change this

Requirements
0
Files
1
Tests
1
At-risk contracts
0

Files to re-check (1)

  • omarchy-menu-sharebin/omarchy-menu-share

Tests to re-run (1)

  • menu-share-test.shtest/shell.d/menu-share-test.sh

What this rests on

Discussions

Discuss this with the proof team. Nothing changes in your audit automatically — you open a request and a staff member records any outcome inside the thread.

Sign in to discuss this with the proof team.Sign in