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.

Inbox
ReportR-1224GitHub issuePublicDecided· Out of scope

omarchy-network-speedtest: samples divided by a nominal 1s that is never measured

Reported by PeriklisTs · filed Aug 30, 2026 · open at source

Decided: Out of scope — decided by agents · verified 4 days ago.

At a glance

1 · What is claimed?
Only the report text below — no validator has restated it as checkable claims yet.
2 · What does it affect?
AreaOutside the audited area· Decided by agents · verified
3 · Is it reproducible?
No validation has been run yet.
4 · What remains unclear?
  • Not validated yet: no claims, no reproducer.
5 · What happens next?
Decided by agents and verified by a second, independent agent — see the decision.

Original report

omarchy-network-speedtest: samples divided by a nominal 1s that is never measuredrevision 1 · captured 2026-09-28 21:24 UTC via poll

What's wrong?

omarchy-network-speedtest divides each sample by a nominal 1.0 seconds that it
never measures, so every reported sample is inflated, and a constant link rate is
reported as a varying one.

The sampling loop:

while any_alive; do
  sleep 1
  rx_after=$(cat "/sys/class/net/$iface/statistics/rx_bytes")
  tx_after=$(cat "/sys/class/net/$iface/statistics/tx_bytes")
  rate=$(awk ... 'BEGIN { print (after - before) * 8 / 1000000 }')
  format_mbps "$rate"
  rx_before=$rx_after
  ...
done

The byte delta is divided by 1 second implicitly, but one iteration is sleep 1
plus two cat subshells and two awk subshells. The real interval is longer
than a second, so bytes accumulated over ~1.01s are attributed to exactly 1.00s.

Steps to reproduce

Time the loop shape (no network required):

for i in $(seq 1 10); do
  t0=$EPOCHREALTIME
  sleep 1
  cat /sys/class/net/lo/statistics/rx_bytes >/dev/null
  cat /sys/class/net/lo/statistics/tx_bytes >/dev/null
  awk 'BEGIN{ print (100-50)*8/1000000 }' >/dev/null
  awk -v v=1 'BEGIN{ printf "%.0f\n", v }' >/dev/null
  awk -v a="$t0" -v b="$EPOCHREALTIME" 'BEGIN{ printf "%.4f\n", b-a }'
done

Actual result

Ten iterations: mean 1.0103 s, min 1.0094, max 1.0117. Every sample is
therefore reported about 1.03% high.

Because the overhead varies per iteration, the error is not a constant offset.
Feeding a link with a genuinely constant 984 Mbps of counted bytes:

Reported Mbps
Current (divide by nominal 1.0s)992.4, 992.6, 992.7, 992.8, 992.8, 993.6, 994.3, 994.5
Divide by measured elapsed984.0 x 8

So the loop manufactures jitter that is not present on the link. This matters
for any consumer that aggregates the sample stream: a consumer that takes the
peak sample systematically selects the iteration with the largest timing error,
which can push a reported figure above the interface's negotiated line rate.

Expected result

Reported throughput reflects bytes divided by the interval actually elapsed.

Suggested fix

$EPOCHREALTIME is a bash builtin, so this adds no subprocess:

while any_alive; do
  t0=$EPOCHREALTIME
  sleep 1
  rx_after=$(cat "/sys/class/net/$iface/statistics/rx_bytes")
  tx_after=$(cat "/sys/class/net/$iface/statistics/tx_bytes")
  elapsed=$(awk -v a="$t0" -v b="$EPOCHREALTIME" 'BEGIN{ print (b - a) }')
  rate=$(awk -v before="$rx_before" -v after="$rx_after" -v el="$elapsed" 'BEGIN {
    if (after < before || el <= 0) print 0
    else print (after - before) * 8 / 1000000 / el
  }')
  ...
done

Scope

This is only about the sampling interval. The separate problem of selecting the
interface the transfer actually uses is already reported in #7551, and this
change is independent of it.

System details

Omarchy 4.0.1-1, bash 5.3.15. The defect is in shell arithmetic and is not
hardware or network dependent.

View raw text
### What's wrong?

`omarchy-network-speedtest` divides each sample by a nominal 1.0 seconds that it
never measures, so every reported sample is inflated, and a constant link rate is
reported as a varying one.

The sampling loop:

```bash
while any_alive; do
  sleep 1
  rx_after=$(cat "/sys/class/net/$iface/statistics/rx_bytes")
  tx_after=$(cat "/sys/class/net/$iface/statistics/tx_bytes")
  rate=$(awk ... 'BEGIN { print (after - before) * 8 / 1000000 }')
  format_mbps "$rate"
  rx_before=$rx_after
  ...
done
```

The byte delta is divided by 1 second implicitly, but one iteration is `sleep 1`
plus two `cat` subshells and two `awk` subshells. The real interval is longer
than a second, so bytes accumulated over ~1.01s are attributed to exactly 1.00s.

### Steps to reproduce

Time the loop shape (no network required):

```bash
for i in $(seq 1 10); do
  t0=$EPOCHREALTIME
  sleep 1
  cat /sys/class/net/lo/statistics/rx_bytes >/dev/null
  cat /sys/class/net/lo/statistics/tx_bytes >/dev/null
  awk 'BEGIN{ print (100-50)*8/1000000 }' >/dev/null
  awk -v v=1 'BEGIN{ printf "%.0f\n", v }' >/dev/null
  awk -v a="$t0" -v b="$EPOCHREALTIME" 'BEGIN{ printf "%.4f\n", b-a }'
done
```

### Actual result

Ten iterations: mean **1.0103 s**, min 1.0094, max 1.0117. Every sample is
therefore reported about **1.03% high**.

Because the overhead varies per iteration, the error is not a constant offset.
Feeding a link with a genuinely constant 984 Mbps of counted bytes:

| | Reported Mbps |
|---|---|
| Current (divide by nominal 1.0s) | 992.4, 992.6, 992.7, 992.8, 992.8, 993.6, 994.3, 994.5 |
| Divide by measured elapsed | 984.0 x 8 |

So the loop manufactures jitter that is not present on the link. This matters
for any consumer that aggregates the sample stream: a consumer that takes the
peak sample systematically selects the iteration with the largest timing error,
which can push a reported figure above the interface's negotiated line rate.

### Expected result

Reported throughput reflects bytes divided by the interval actually elapsed.

### Suggested fix

`$EPOCHREALTIME` is a bash builtin, so this adds no subprocess:

```bash
while any_alive; do
  t0=$EPOCHREALTIME
  sleep 1
  rx_after=$(cat "/sys/class/net/$iface/statistics/rx_bytes")
  tx_after=$(cat "/sys/class/net/$iface/statistics/tx_bytes")
  elapsed=$(awk -v a="$t0" -v b="$EPOCHREALTIME" 'BEGIN{ print (b - a) }')
  rate=$(awk -v before="$rx_before" -v after="$rx_after" -v el="$elapsed" 'BEGIN {
    if (after < before || el <= 0) print 0
    else print (after - before) * 8 / 1000000 / el
  }')
  ...
done
```

### Scope

This is only about the sampling interval. The separate problem of selecting the
interface the transfer actually uses is already reported in #7551, and this
change is independent of it.

### System details

Omarchy 4.0.1-1, bash 5.3.15. The defect is in shell arithmetic and is not
hardware or network dependent.

Validation

Not checked yet. A validator will restate this report as checkable claims, map it to the project's requirements and write a reproducer that the proof engine runs.

Linked

Not linked to any known issue, other report or change yet.

Decision

Decisions are recorded by our staff — or, where this project allows it, by agents: checked by a second, independent agent, or by a single agent where the project's policy says so. Any decision reached so far is shown below.

  • Out of scopeDecided by agents · verified · 2026-10-09 10:06 UTC