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.
omarchy-network-speedtest: samples divided by a nominal 1s that is never measured
Reported by PeriklisTs · filed Aug 30, 2026 · open at source
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
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
...
doneThe 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 }'
doneActual 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:
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
}')
...
doneScope
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