NON-OS/nonos-micro-kernel
Watch
2
0
Fork
You've already forked nonos-micro-kernel
 0
Code Issues Pull requests 29 Projects Releases 1 Packages Wiki Activity

Desktop capsule correctness, and a measurement harness that reports the tail #12

Open
nonos-sync wants to merge 24 commits from nonos-sync/gh-476 into main AGit
pull from: nonos-sync/gh-476
merge into: NON-OS:main
Conversation 0 Commits 24 Files changed 378 +9917 -1142
nonos-sync commented 2026-09-11 11:22:38 -04:00
Member
Copy link

22 commits, one concern each, all building standalone. Boot checked on every pass.

Started as UI work on the wallet and process manager. Most of the visual faults had a real defect behind them, so it ended up mostly correctness.

Trust surface

capsule_attest answered OP_PROOF_CAPSULE_LIST from 17 capsule names with capability masks typed into the source, served as a proof. Now reads the live process table. MkProcStat needs no capability so the mask stays CoreExec|IPC|Memory: an attestation service needing more authority to report on authority would be answering its own question.

Its invariants were prose with nothing checking them. Each now names how it is settled (holders of a bit, only init holding a bit, every capsule masked) or reports unchecked. Never a pass where it cannot be settled at runtime.

capsule_about gets a Verify screen: live checks over one read of the process table, the TPM attestation document with its challenge verified, the boot record with the kernel's own caveat that reading it re-verifies nothing, and the claims this window cannot settle with where each is settled instead.

Measurement

Kernel had a microbenchmark harness reporting min/avg over 256 runs. min is the statistic that cannot regress: make 1 call in 50 twenty times slower and it does not move.

nonos-bench is shared by the kernel harness and a new bench terminal command. p50/p95/p99/max, nearest rank so every figure was measured. Reads are lfenced both sides since rdtsc is not a barrier and an unserialised pair can close before the work retires. Counter overhead calibrated against an empty body and subtracted using the floor. Kernel buffer 256 -> 1024, since at 256 the p99 is the third slowest run.

Capabilities that existed and nothing called

Four fixes here are the same shape.

  • MkAttestDoc: implemented in the kernel, absent from libc. No capsule had ever asked for a signed statement of what the machine is running.
  • MkFutexWait: never exposed, so capsules waited by looping on mk_yield, which returns immediately when nothing else wants the CPU. capsule_login held 88% of a core for the life of the session.
  • spawn_next documents that a full instance table means the caller focuses an existing window. The caller logged the error and dropped it, so the wallet opened twice per boot then silently stopped responding.
  • The kernel benchmark harness above.

No compiler warning and no test covers this class.

Apps

  • CPU percentages held until the sample window is long enough to divide by. A 4 tick window gave every process that ran at all 25.0%, and the total read 100% on an idle machine.
  • Peak CPU printed 255%, which is u8::MAX after a saturating cast, recorded during boot and kept as the peak.
  • Send takes amounts at chain precision. Was a u32 of milli-ETH with no decimal key, so 0.0005 could not be entered.
  • sign_eth_transfer took value_wei: u64, capping a send at 18.4 ETH. The wire already carried a 256 bit word.
  • Broadcast is armed before it sends. The process manager asks twice before ending a process.
  • Nym holds the whole active set. NODE_CAP was 128, so every client entered the mixnet through the same prefix of gateways. The full set is 40 KB.

Presentation

  • One type ramp, no step below the toolkit floor. 95 of 125 text calls were authored under it and 12 distinct sizes rendered identically.
  • Sections measure from the row above them, and the quick action hit test reads the same geometry as the painter instead of a literal it had drifted from.
  • Empty account screen offers generate and import, whose keys already worked and were never mentioned.

Proofs

New crates for the attestation document parser, benchmark reduction and wallet keypad, in verify.yml with clippy denied on warnings.

Parser proofs drive malformed input, not the happy path: every truncation refused, trailing bytes refused, u32::MAX length fields refused without panicking, replayed challenge parsed but never reported fresh. The type ramp is asserted against the font floor so the flattening cannot come back silently.

Not done

  • desktop_shell still makes ~40 timed out vfs_pool calls per boot while package staging holds the block device.
  • Spawn to first instruction and per capsule attestation verify are still millisecond markers.
  • Benchmark figures for publication need named hardware. QEMU gates structure only.
  • Boot frame deadline went 1s -> 3s and now logs when it gives up. One clean boot is not proof the editor window fault is gone.

Opened on GitHub by eKisNonos as pull request 476. Review and merge happen there while this repository is kept in step from GitHub; this copy follows it, and is marked merged or closed when it is.

22 commits, one concern each, all building standalone. Boot checked on every pass. Started as UI work on the wallet and process manager. Most of the visual faults had a real defect behind them, so it ended up mostly correctness. ### Trust surface `capsule_attest` answered `OP_PROOF_CAPSULE_LIST` from 17 capsule names with capability masks typed into the source, served as a proof. Now reads the live process table. `MkProcStat` needs no capability so the mask stays CoreExec|IPC|Memory: an attestation service needing more authority to report on authority would be answering its own question. Its invariants were prose with nothing checking them. Each now names how it is settled (holders of a bit, only init holding a bit, every capsule masked) or reports unchecked. Never a pass where it cannot be settled at runtime. `capsule_about` gets a Verify screen: live checks over one read of the process table, the TPM attestation document with its challenge verified, the boot record with the kernel's own caveat that reading it re-verifies nothing, and the claims this window cannot settle with where each is settled instead. ### Measurement Kernel had a microbenchmark harness reporting min/avg over 256 runs. `min` is the statistic that cannot regress: make 1 call in 50 twenty times slower and it does not move. `nonos-bench` is shared by the kernel harness and a new `bench` terminal command. p50/p95/p99/max, nearest rank so every figure was measured. Reads are `lfence`d both sides since `rdtsc` is not a barrier and an unserialised pair can close before the work retires. Counter overhead calibrated against an empty body and subtracted using the floor. Kernel buffer 256 -> 1024, since at 256 the p99 is the third slowest run. ### Capabilities that existed and nothing called Four fixes here are the same shape. - `MkAttestDoc`: implemented in the kernel, absent from libc. No capsule had ever asked for a signed statement of what the machine is running. - `MkFutexWait`: never exposed, so capsules waited by looping on `mk_yield`, which returns immediately when nothing else wants the CPU. `capsule_login` held 88% of a core for the life of the session. - `spawn_next` documents that a full instance table means the caller focuses an existing window. The caller logged the error and dropped it, so the wallet opened twice per boot then silently stopped responding. - The kernel benchmark harness above. No compiler warning and no test covers this class. ### Apps - CPU percentages held until the sample window is long enough to divide by. A 4 tick window gave every process that ran at all 25.0%, and the total read 100% on an idle machine. - Peak CPU printed 255%, which is `u8::MAX` after a saturating cast, recorded during boot and kept as the peak. - Send takes amounts at chain precision. Was a `u32` of milli-ETH with no decimal key, so 0.0005 could not be entered. - `sign_eth_transfer` took `value_wei: u64`, capping a send at 18.4 ETH. The wire already carried a 256 bit word. - Broadcast is armed before it sends. The process manager asks twice before ending a process. - Nym holds the whole active set. `NODE_CAP` was 128, so every client entered the mixnet through the same prefix of gateways. The full set is 40 KB. ### Presentation - One type ramp, no step below the toolkit floor. 95 of 125 text calls were authored under it and 12 distinct sizes rendered identically. - Sections measure from the row above them, and the quick action hit test reads the same geometry as the painter instead of a literal it had drifted from. - Empty account screen offers generate and import, whose keys already worked and were never mentioned. ### Proofs New crates for the attestation document parser, benchmark reduction and wallet keypad, in `verify.yml` with clippy denied on warnings. Parser proofs drive malformed input, not the happy path: every truncation refused, trailing bytes refused, `u32::MAX` length fields refused without panicking, replayed challenge parsed but never reported fresh. The type ramp is asserted against the font floor so the flattening cannot come back silently. ### Not done - `desktop_shell` still makes ~40 timed out `vfs_pool` calls per boot while package staging holds the block device. - Spawn to first instruction and per capsule attestation verify are still millisecond markers. - Benchmark figures for publication need named hardware. QEMU gates structure only. - Boot frame deadline went 1s -> 3s and now logs when it gives up. One clean boot is not proof the editor window fault is gone. --- Opened on GitHub by eKisNonos as [pull request 476](https://github.com/NON-OS/nonos-micro-kernel/pull/476). Review and merge happen there while this repository is kept in step from GitHub; this copy follows it, and is marked merged or closed when it is.
NODE_CAP was 128, so the client kept a prefix of the directory and every
node in it entered the mixnet through the same few gateways. The active
set is 60 mix, 180 entry and 179 exit, a node is 76 bytes on the wire,
so the whole network is under 40 KB. Cap raised to 512 with per role
budgets that cover each active set with room to grow.

Route selection drew with a modulo over a 32 bit seed, which favours the
low indices. Replaced with a multiply shift draw that is uniform over any
length.

Dropped mixnet/encode.rs and mixnet/route.rs. The encoder there built a
header that would have delivered to the wrong gateway; nothing called it
and nothing should have.
Kill ring, word navigation, history designators, tree, type and which,
per command usage, match highlighting in grep, and uniq, tac and rev in
the pipeline filters.

The window was 520x300, which is 58 columns at the shipped face, so the
help table wrapped in a way that read as a rendering fault. Sized to
760x460.

The toolbar drew five tools and three of them dispatched nowhere. Cut to
the three that work.

Suggestions use Damerau distance so a transposition costs one edit, and
offer both candidates on a tie rather than picking the first.

121 host proofs over the shipping files.
mode_for_path returned Document for every file, so a .rs file opened with
no syntax colour and no line numbers. It returns Code now, and the
formatting ribbon is drawn only for the mode that uses it.

The tab modified marker read !undo.is_empty(), which never cleared on
save, so a saved file kept its dot. Tracks a dirty flag set by push_undo
and cleared on write.

Removed the settings sections whose toggles were wired to nothing, and
the LANGUAGE constant in the status bar that was a fixed string. The two
switches that survive are the two that act.

Added go to line and quick open, both proved on the host: name matches
rank above path matches, which is the ordering a reader expects.
MENUBAR_H was defined in three places with two values, 28 in two of them
against a real bar of 46, so a dragged window slid under it. One
definition in app_skeleton, read by everyone.

Maximise left the menu bar visible, which is not what the control says it
does. It takes the whole display now.

Placement was a cascade from the top left. A lone window opens centred,
and the cascade steps from there rather than shifting the first window by
half its own run.
refresh listed / rather than /home/nonos, so the desktop showed the root
of the store instead of the user's own files. The path is one constant
now, read by the lister, the click router and the drop handler.

The launchpad button drew a 3x3 grid of dots. It draws the mark, from the
same 512x556 rasterisation the wallet uses. The old asset was 128x139 and
visibly soft at dock size.
A refresh landing four ticks after the last one gives every process that
ran at all a quarter of the window, so four busy processes each read 25.0
percent and the total read 100 on a machine doing nothing. The round
numbers were the tell.

Below a 32 tick floor the previous figures are held rather than
recomputed, so the column stays still between real samples instead of
flickering between quantised values.

The sparkline says 'idle, last 32s' where the series is flat, rather than
drawing a line along the axis that reads as a broken chart.
The fourth overview card read '20, of 44 processes' over a bar. That
number is already on screen as a column of shields and it answers a
question nobody asks: whether twenty capsules are privileged matters far
less than which authority they hold. One capsule with raw hardware reach
is a different machine from one with debug.

It carries all four sensitive classes with their own counts, and the
change in each since the window opened, which is the event worth seeing.

Counts come from Monitor::posture, which the security screen already
reads, and the class order and colours from risk_strip::CLASSES, so a
row's slots and this card cannot disagree.
Twenty shortcuts worked and nothing on screen said so. A reader could
find them by reading the source and nowhere else.

? opens the list and the status strip says which key opens it, because an
overlay nobody knows about is no better than none.

The dispatcher matched on bare hex, so a help screen written by hand
would have drifted from it the day someone rebound a key. Both walk one
binding table now. The digit row goes through the same apply as every
other key, so Act::Screen is a case something dispatches rather than a
variant the table mentions and nothing produces.
Two syscalls the kernel dispatches and no capsule could reach.

MkAttestDoc returns the TPM signed statement of what the machine is
running: a root over the capsule registry, bound to a challenge. It was
implemented, reachable from the dispatch table, and absent from libc, so
nothing had ever asked for one.

MkFutexWait is a timed sleep. mk_yield is not one: on a machine where
nothing else wants the processor it returns immediately, so a retry loop
built from yields runs flat out. mk_idle_ms parks on a private word
nobody wakes, which is a sleep the scheduler can account for.
wait_for_setup retried in a loop of 64 yields. On an idle machine that is
a spin with extra steps: login held 88 percent of the core for as long as
the desktop was up, waiting on a step that would not arrive any sooner
for the spinning. The process manager showed it ready rather than
sleeping, and the cpu screen showed saturation breached.

Both wait 250 ms now. Four wakeups a second, and it answers just as fast.

The driver settle loops are left alone: those are bounded hardware delays
on real silicon paths, not open ended waits.
OP_PROOF_CAPSULE_LIST served seventeen capsule names with capability
masks typed beside them. That list was right on the day it was written
and became a fiction the moment a capsule was added, renamed or
regranted, and it was served under the word proof.

It reads MkProcStat now, which needs no capability, so the mask stays at
CoreExec, IPC and Memory. An attestation service that had to be trusted
with more authority in order to report on authority would be answering
its own question.

The invariants carried claims and mechanisms as prose and nothing checked
them. Each now names how it is settled: holders of a bit, only init
holding a bit, every capsule carrying a mask, or not settleable at
runtime. The last reports unchecked, never a pass. Added the admin
invariant, which the security monitor already tested and the proof
service did not.
spawn_next says in its own comment that a full slot table means the
caller focuses an existing window instead. The caller logged
EndpointCollision to a serial line nobody reads and dropped the request,
so the wallet opened twice per boot and every click after that did
nothing at all, with no way to tell that from a crash.

It hands back a live instance pid now and init delivers the focus frame
to it, which restores, raises and focuses. The collision error survives
for what it actually describes, a slot registered to an owner that cannot
be found.

The rejection line names the app. A boot frame that never lands says so
too, with the instance named: a capsule that is spawned, attested, listed
in the process table and never draws is the failure a reader cannot
diagnose from silence. Deadline raised to 3s, since a boot busy with
package staging plainly exceeds one.
Four cards, ordered so the evidence a reader can watch being taken comes
first.

Checked now runs against one read of the process table, so the four
verdicts describe the same instant: no capsule holds Debug, only init
holds Admin, every capsule carries a kernel recorded mask, and this
window holds exactly what its manifest declares. That last one turns the
hardcoded MASK constant into an assertion the system tests rather than a
claim it makes.

Signed by the hardware asks for a TPM attestation document once per
screen open, checks the challenge came back unchanged, and reports a
machine without a TPM as having declined. A refusal is not a pass.

Recorded at boot carries the kernel's own caveat: the syscall hands back
what the bootloader measured and re-verifies none of it.

Not checkable from here names the three claims this window cannot settle
and where each is settled instead, so the list is not a selected truth.

Verdicts are three shapes, not three colours, because colour is gone for
a colour blind reader and gone again in a filtered screenshot.

12 host proofs on the document parser: every truncation refused, trailing
bytes refused, u32::MAX length fields refused without panicking, and a
replayed challenge parsed but never read as fresh.
The toolkit clamps anything under 17px up to 17. Ninety five of the
window's hundred and twenty five pieces of text were authored below it:
11.0, 11.5, 12.1, 12.6, 13.0, 13.2, 13.4, 13.8, 14.0, 14.2, 14.9 and
16.1 all rendered at the same height. Twenty five sizes asked for,
thirteen drawn, and no hierarchy anywhere on screen.

This ramp existed and was part of the problem: LABEL at 12.1, SMALL at
13.8 and BODY at 14.9 are three steps that render identically.

No step is below the floor now. The bottom three still coincide there,
because a caption cannot be smaller than body text on this display, and
they are told apart by colour instead. The upper steps are spaced far
enough to read as different rather than as a mistake.

scale_tests asserts every step against the floor, that the ramp only
climbs, and that the upper steps are far enough apart. Setting LABEL back
to 12.1 fails two of them.
send_amount_milli_eth was a u32 of thousandths of an ether with no
decimal point key, so the smallest amount expressible was 0.001. An exact
0.0005 or a single wei could not be entered at all, while staking and
swapping already took u128 with a point. The send screen had a cut down
third copy of an arithmetic that existed twice in better form.

One keypad now, shared. The figure is kept as typed, digits with a count
of places, and scaled only when the chain asks, so nothing rounds on the
way in and the amount signed is the amount shown.

sign_eth_transfer took value_wei as u64, capping a send at 18.4 ETH. The
wire already carries a 256 bit word built from a u128, so the narrowing
bought nothing and is gone.

24 host proofs: 0.0005 and one wei expressible, digits past the token's
precision refused rather than absorbed, backspace retracing the keys
pressed, and a max shortcut figure replaced by the next keystroke rather
than appended to.
With no account every figure resolved to an em dash, so the largest thing
on screen was a punctuation mark and nothing said how to fix it. The keys
to generate or import existed and worked and were never mentioned. The
card is now the one instruction that matters, with both actions as
buttons wired to generate and import.

The two cards on the home row differed by forty eight pixels in height,
which left a hole under the shorter one that read as something failing to
load. Both are the same height, and the sections below measure from the
taller of the pair rather than from the account card alone.

Rows inside both cards sat twenty pixels under their captions, correct
for the thirteen point text they were placed for and three short of the
seventeen the font draws, so every label overlapped its value. Derived
from the line box now.

The quick action hit test was pinned to a literal row the painter had
moved, so the targets sat ten pixels above the cards. Painter and hit
test read one geometry module.

Every rail entry drew the same twelve pixel square. Six identical squares
is a placeholder that shipped. One glyph each now.

Broadcast is armed before it sends. The process manager asks twice before
ending a process and this asked once before spending money.
The numbers this system published about itself were build and boot wall
clock. An IPC round trip is the operation every capsule pays for
thousands of times a second and nobody had measured it.

nonos-bench is a no_std crate with no dependencies so both sides share
one reduction. Two harnesses reporting different statistics about one
machine is how a regression hides between them.

Percentiles, not a minimum and a mean. min is defensible and is also the
figure that cannot regress: make one call in fifty twenty times slower
and min is untouched while avg barely moves, and that call is the one a
person notices. Nearest rank, so every figure published was measured
rather than interpolated.

rdtsc is not a barrier, so both reads are fenced: an unserialised pair can
close before the work retires and report a number smaller than the work
took. No profile sets CR4.TSD, so a capsule at CPL=3 reads the same
counter the kernel does.

The counter costs tens of cycles, the same order as a syscall. Calibrated
against an empty body and subtracted, using the floor rather than the
median, since the cheapest pair is the one least disturbed.

The kernel harness reported min, avg and max over 256 runs, which is what
the roadmap says not to do, and at 256 the p99 is the third slowest run
and moves on noise. 1024 now, same reduction, same sort.

bench in the terminal reports the overhead it subtracted then syscall
entry and exit, a state reading syscall, and a scheduler round trip.

12 host proofs, including that one slow sample in a hundred moves p99 and
max and not the median, and that the shared sort is a permutation.
The receive pump ran on every pass whether or not anything was waiting,
which cost a steady share of the core for no work. It is gated on the
receiver being attentive now, with a three tier wait: short while traffic
is settling, longer once it is quiet.

Moved nonos-capsule-tokio-smoke out of the desktop GUI profile into its
own feature. It is a smoke test and it was spawning in the shipped
desktop image.
verify.yml runs the wallet, attestation document and benchmark summary
proofs alongside the terminal ones, with clippy denied on warnings.
MkBatteryStatus returned a fixed 100, marked in the source as a
placeholder. A capsule cannot tell that from a full battery, so the
desktop drew a full icon on a machine with no battery driver at all.

The reading comes from the ACPI _BST and _BIF objects, evaluating those
needs an AML interpreter, and the kernel scans AML for device resources
without executing it. Until that lands there is no figure to give, and
the errno says so.
admissible listed install verdicts the installer never returns, apps
carried two entries with no capsule behind them, and the file manager
theme resolved colours through a table with one live row.
The completion list and the dispatcher are edited by different changes at
different times, and terminal_line_proofs exists to catch exactly that:
bench dispatched and could not be tab completed, so it was a command
nobody would find.

The hygiene gate matches the word placeholder in a comment. Both hits
were comments describing the removal of one, but weakening the gate to
allow the word is the wrong trade.

EVIDENCE.json counted 34 proof crates against 38 in the tree.
A path dependency with no version reads as a wildcard, and cargo deny
refuses wildcards. Every other path dependency here carries one.
This pull request can be merged automatically.
You are not authorized to merge this pull request.
View command line instructions

Checkout

From your project repository, check out a new branch and test the changes.
git fetch -u origin +refs/pull/12/head:nonos-sync/gh-476
git switch nonos-sync/gh-476
Sign in to join this conversation.
Reviewers
No reviewers
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
NON-OS/nonos-micro-kernel!12
No description provided.