Skip to content

linux: personality, store install, desktop and kernel fixes - #567

Closed
eKisNonos wants to merge 209 commits into
mainfrom
linux/store-install
Closed

eKisNonos wants to merge 209 commits into
mainfrom
linux/store-install

Conversation

@eKisNonos

@eKisNonos eKisNonos commented Sep 27, 2026 •

Copy link
Copy Markdown
Contributor

Since the last update

Linux personality

  • ptrace, process_vm_readv/writev, capget/capset, mount/umount2, chroot, unshare, setns refused with EPERM, the io_uring family with ENOSYS, each with a one-line reason in the log. The suite now reports calls served=1500 unserved=0: the two former gaps are named refusals.

Package families

  • zstd (userland/zstd): RFC 8878 decoder. Vectors are zstd 1.5.5's own output, --fast=5 to --ultra -22 and a 128 MiB window; the test regenerates inputs independently.
  • xz (userland/xz): .xz container and LZMA2, every check type. BCJ and other filters refused, never skipped. Vectors from XZ Utils.
  • OpenPGP (userland/openpgp): v4 detached signatures, RSA and Ed25519, keys and subkeys, ASCII armor. MD5/SHA-1, v3/v5/v6 and unknown critical subpackets refused by name. Vectors from GnuPG 2.4.4; RSA checked through the exact request the capsule sends the crypto service.
  • pacman (install pacman:<name>): signed database required, per-package SHA-256 and detached signature, market pin.
  • Debian (install deb:<name>): Release.gpg over Release, Release over Packages, Packages over each .deb, market pin. Maintainer scripts never run. Valid-Until not checked (no trusted clock, and the source says so.
  • Mirrors, paths, repositories and keyrings are build settings (NONOS_PACMAN_*, NONOS_DEB_*); an image built without them refuses and says which is missing.
  • Tar reader strips dpkg's ./ from member names; without it nothing from a .deb was placed.
  • Every new parser has a seeded mutation harness run in a debug build. It is not coverage-guided: no libFuzzer is vendored.

Kernel

  • CPU features detected before SSE/XSAVE bring-up (every boot stopped at "SSE not supported")
  • Heap: over-aligned allocations were only 32-aligned (data sat after a 32-byte header); XSAVE faulted on it.
  • FPU area kept off kernel stacks; a new thread starts with every FPU register cleared.
  • The kernel is built soft-float, and its C and BLAKE3 without SSE. Kernel code used xmm on the interrupt path before the thread state was saved; the guest state suite lost 300 of 300 rounds in both processes. It now holds.

Evidence

Guest suites at 4de4cd6 (no xmm or ymm in kernel text, checked with objdump), TCG, one vCPU:
fingerprint 4/0, native 6/0, bounds 5/0, fs 11/0, proc 2/0, separation 3/0, exec 3/0, dynamic 1/0, state 1/0 (tried/escaped), life fork ok, calls served=1500 unserved=0.

Not done, and why

  • Signal delivery in the personality: the kernel half (MkForeignContext, MkForeignSignal) is in; the personality half is not.
  • A real apk, pacman or deb install

eKisNonos and others added 30 commits September 20, 2026 12:00
Reads the signed marketplace index, lists what the running image can
install, and installs through the queue init already owns.

The install buttons did nothing: the painter and the hit test each
computed their own rectangles, so a click never matched a row. Both
derive from one geometry module now and the click path reaches the
same install::ask as Enter.

Search filters as typed, the list scrolls with a real scrollbar, and
selection survives a refresh.

init gains an install queue and a wake path so a store request is
serviced on arrival rather than on the next supervisor spin. The
surface registry can attach frames to a surface a capsule owns.

Scrollbar arithmetic mirrored in python: empty, shorter than the
viewport, thumb at both ends, single row overflow.
Release encode, decode and signing move into marketplace_abi, so the
tool that writes the index and the capsule that reads it share a codec
instead of having one each.

install_ready checks arch and readiness against the running image
rather than the index, and adds a seventh gate for whether a release
carries a zk trailer for its own measurement. The other six are
signatures over the artifact.

The catalogue generator reads what is on disk and writes JSON; the CLI
encodes the binary the market ingests. Signing is a separate step with
the operator seed, which is not in any build rule.
IconId::Store points table.rs at assets/icons/store.a8, which only
existed on the app-store branch, so every build of this branch failed
to read it. Add the mask and its SVG source here so the table stands
on its own.
text::line returns the drawn width, so the bare match evaluated to i32
where the function body expects (), failing the capsule build.
nonos-data/marketplace/index.bin has no make rule, so naming it as a
hard prerequisite failed every build on a checkout without it (CI:
No rule to make target). Wrapping it in $(wildcard) keeps the rebuild
on a newer catalogue where it exists and drops the prerequisite where
it does not.
The branch's manifest predated the switch to in-process Ed25519 and
dropped the dependency while verify/crypto.rs imports it, so the
capsule failed with an unresolved import. Restore main's manifest and
add only the app_skeleton dependency boot_index.rs needs.
Twenty-five syscalls were published as caps = ["valid_token"] while the
cap table demands a hardware, dev-root or time capability. Twenty-two take
any one of Admin or a hardware capability, now published with caps_any; the
dev-root and time calls need one capability, published with caps.
The cap table gates MDRO with MDRQ and MDRC on can_enrol_dev_root. The old
syscall caps check cannot resolve that predicate and wants valid_token, so
this fails it until abi/caps-check-fail-closed lands; the fixed check passes.
Every lane was pinned to -accel hvf -cpu host, which only macOS has, so
no Linux host could boot an image. KVM when /dev/kvm opens read-write,
hvf on macOS, TCG otherwise, the rule the boot matrix already uses; the
display and audio backends follow the host too.
The trailer's magic picked the verifier for every root, so a Pedersen
trailer was checked against the vendor root too. A local root's leaf is a
commitment to a secret this kernel holds; the vendor root's is not, so there
the trailer may no longer choose the weaker proof.
MkLocalSign let a LocalSign holder prove any capability it held, including
LocalSign itself, so one signer could hand out the right to sign. A local
proof now names nothing beyond AMBIENT_CAPS. crypto_proofs checks a minted
trailer and its refusals against the kernel's own verifier files.
An Alpine package index is signed that way, and the capsule offered SHA-1
only without the prefix, so the index could not be checked at all. The
rsa crate rebuilds the whole padded block and compares it. Nothing here
signs, so offering SHA-1 verification mints nothing new with it.
resolve.rs names super::root, which the crate never mounted, so it did not
build and nothing noticed because no workflow ran it. It mounts root.rs,
follows the rename of absolute to visible, adds the /linux confinement and
Phdr::file_range tests, and joins the proof-crate matrix.
A signature over a package covers the compressed bytes of one member, so a
verifier needs to know where each one starts and ends. members() refuses a
file with any byte that belongs to no member, where gunzip ends the stream
and ignores the rest.
The index's .SIGN.RSA entry is checked against Alpine's x86_64 keys by the
crypto service, the package's control member against the index's C: SHA-1,
and its data against the control member's datahash. Only a Verified value
reaches the store, so unauthenticated bytes are refused, not kept unvouched.
Without the operator-key rotation: NOX_OPERATOR_V1 keeps main's key, now
read from .keys/marketplace_operator_ed25519.pub. The capsule embedded an
index nothing built, so tools/nonos-market-index writes one, signed and
verified when the operator seed is present and empty otherwise. nonos-mk
moves to 78dae45 for the zk_trailer_hash field; the icon table is 49 long.
A release naming x86_64-linux counted as having its attestation, so any
release could claim the exemption for itself. It now needs the linux.
namespace too, which is where the store routes it: to the installer that
authenticates the bytes before the machine mints their proof.
Conflicts were both sides adding: the install and app-store capsules sit
together in Cargo.toml, mk and userspace, and init/mod.rs names the
install queue once. The init loop and install queue are taken as the PR
wrote them; the commit after this replaces its wake path.
The scheduler takes every ready process's priority lock from the timer
interrupt. wake.rs and boost_init_for_drain took init's with interrupts on
from syscall context, so a tick inside either spun forever on one CPU. The
install queue now raises through the guarded setter the window queue uses.
MkAppInstall took a package name and the store's own readiness flag. It now
takes a listing and release; init asks the market for readiness and the
release's package hash, and the installer refuses bytes of any other BLAKE3.
The index keeps each record's D: and p: lines, so dependencies come too.
…each

CryptoMachineKey derives the machine key for any label a Crypto holder
names, so a key the kernel keeps for itself needs a label no syscall can
ask for. Kernel labels start with a zero byte, and the syscall refuses any
label that does.
The local signing identity was random each boot, so consent was too. It is
now derived from the machine key, and first-boot setup, which alone holds
EnrolDevRoot, grants the local root as a named step and keeps a token only
this machine can make; later boots restore it. The desktop profile now
includes setup and the market, and builds every capsule it embeds.
MkAppLaunch queues a run for init, which spawns the personality to start
the program the installer recorded outside /linux. Whether it may start is
the exec gate's answer. The store drops its console-code enrolment, which
it never held the capability for, and gains an o key to open.
A live install reached "mirror 10.0.2.2 is on the local network: reached
directly" and then "no package index", and no packet for the mirror left
the machine. Nothing said whether the socket was refused, the connect was,
or the reply was not a 200. Each now logs the step and the status
net.sockets gave, or that it gave no reply, and a GET that yields no 200
body names the mirror and the path.
…ce checks

kali.<name> in the package list becomes a listing linux.kali.<name>. The
tool fetches Kali's Release and Release.gpg and verifies them with gpgv
against the pinned 2025 archive key and no other, holds the Packages file
to the Release's SHA-256 (xz before gz, the installer's order; Kali
publishes gz only), and the .deb to the Packages SHA-256. Only then is
the .deb hashed with BLAKE3 for the listing. A Release that does not verify
lists nothing.

An Alpine name inside a namespace another family owns (kali., blackarch.)
is refused, so the kernel's mapping never reads it as the wrong family.

Checked on 2026-09-27: jq 1.8.2-1 from kali-rolling, 88168 bytes.
`help` listed install under apps and again under tools. The builtin that
installs from the market answers to the name first, so the tools entry
could never run, the case the note on sd already describes.
Every installer fetch stopped at "socket got no reply": net.sockets serves
only holders of Network (services/registry/policy.rs), and the Linux
capsule never held it (0x300001939 has no bit 2). The mixnet attempts
before the local-network path failed at the same call, which was read as
the mixnet being down.

Network is now an optional capability in the signed manifest, inside the
certificate ceiling, and the install role asks for it when it is spawned.
The run role does not, so a guest program runs without it; its own sockets
are the socket model's to grant.
With Kali listed beside Alpine the store showed two cards reading "jq /
Linux", told apart only by opening each. The line under the name now says
Alpine Linux, Kali Linux or BlackArch, read off the listing's namespace.
allocate_with_guards took a physical range from phys::alloc_contiguous and
used the address as a virtual one: it unmapped VA == PA for both guards in
whichever address space was live, and handed back PA + 4 KiB as a kernel
pointer. With 2 GiB of RAM those addresses are where capsule images load,
so the first caller would have unmapped a running process's pages. Nothing
calls it; it was exported from security:: waiting for one.
With Network granted, the installer's connect came back status 4, bad
length. net.sockets reads handle u32, port u16, host length u16, then the
host (connect/parse_host.rs); the capsule sent the length as one byte and
the host a byte early, in both the installer's dial and a guest's own
connect by name. No connect by host from this capsule could ever have
succeeded.

One encoder now builds the body for both, and a test feeds its output to
net.sockets' own parser, mounted from its source, and shows the old
one-byte layout is what that parser refused.
net.core answers a receive on a quiet socket and on a finished one alike,
with nothing, and the installer took nothing as the end. On a live boot
that cut Alpine's APKINDEX short, whose signature then failed over the
bytes that had arrived ("package index signature did not verify"), and
left Kali's Release empty while the mirror was still fetching it upstream
("no 200 reply", though the mirror served 33088 bytes with a 200).

A read now ends when the header's Content-Length has arrived, and an
empty read is waited through until 120 s pass with no byte. A body short
of its length is refused, bytes past it are dropped, and the status is the
status line's second word exactly: "HTTP/1.1 500 x 200" used to pass as a
200. Each fetch logs its path and size.

Alpine's own index, as the mirror served it today (v3.20 main x86_64,
signed 2026-07-16 by 6165ee59, sha256 fe41d278..e5eb), is now a vector:
the capsule's signature check passes it under the pinned key with a real
RSA verifier and refuses it with one byte flipped, so the parse and the
check are shown sound apart from the device.
…indexes

The inflater refused any output past 4 MiB, a compile-time bound shared by
every caller. Alpine's community index inflates to 8.2 MB and Kali's main
Packages to 85 MB, so on a live boot both downloaded whole, the Kali
Release verified under the pinned key, and the index was then refused by
the inflater: "package index signature did not verify" for Alpine,
"no verified Debian index" for Kali. The same index verifies on the host.

gunzip_within, members_within and inflate_counted_within take the bound;
the existing names keep 4 MiB, so no other caller's limit moved. The bound
is still checked as output grows, symbol by symbol, so a small stream that
expands without end stops at it. The installer passes 128 MiB, inside its
320 MiB heap.

A 18 KB vector of two members inflating to 6 MiB (make_large.py) shows the
default refusing it, the installer's bound opening it whole, and a bound
one byte short still refusing.
A live boot installed Kali's jq and its closure, then stopped at
"interpreter missing or broken". jq names /lib64/ld-linux-x86-64.so.2;
libc6 ships the loader under /usr, and /lib64 is a link into /usr that
base-files lays down on every Debian system. base-files is in no
program's closure, and the loader was read by its literal path in any
case, without the links every other open follows.

The interpreter is now followed through the guest's link table and read
and proved at the path it resolves to, never the link's. A Debian install
adds the merged-/usr links (/bin, /sbin, /lib, /lib64) the tree does not
already have. An interpreter that fails its proof is named with the reason,
where before only "nothing vouches for the interpreter" was said.
The store named a Linux listing by the distribution it came from: "Alpine
Linux" and "Kali Linux" under the card, "Kali rolling" and "jq@1.8.2-1
from kali.download" in the detail pane. That is plumbing on the shelf. A
card now says "Linux app", the detail pane gives the version, and the
catalogue no longer puts a distribution in the publisher field.

Where the bytes come from is still in the signed listing, as the package
URL, and still checked at install against the distribution's own
signatures; it is provenance, not a label.
A Wayland program asks libwayland-client for the display, and the library
will not look without XDG_RUNTIME_DIR; WAYLAND_DISPLAY names the socket.
Neither was set, so an installed GUI app would have stopped at "cannot
connect to display" before drawing anything. /run is private to each guest,
and any path ending in wayland-0 reaches the personality's compositor.
Handlers were recorded and never raised: a program that installs one and
depends on it firing hung. The kernel already hands a supervisor what it
needs (MkForeignContext reads a parked thread's registers, MkForeignSignal
resumes it into a handler or back out), so the work was the frame the
personality builds between them.

rt_sigaction now keeps the whole disposition, handler, flags, restorer and
mask, per process as on Linux. kill, tkill and tgkill queue a caught
signal against a thread and drop one whose default is to ignore; an
uncaught, non-ignored default still ends the thread. On that thread's next
return from a syscall, serve::deliver builds an x86-64 rt_sigframe on its
stack with the syscall's result already in the saved rax, and enters the
handler; rt_sigreturn reads the ucontext back and resumes where the signal
interrupted. Only the trapping thread is delivered to; a signal for a
thread parked elsewhere waits until it next traps, and asynchronous
preemption of a thread running in userspace is not served.

The frame layout is proved by a round trip: build a frame, read the
sigcontext back the way rt_sigreturn does, the registers are identical;
plus offset checks, a too-low stack refused, and a mutation target on the
reader. A `signal` guest installs a handler, raises SIGUSR1 at itself and
exits zero only when the handler ran and returned.
A guest's anonymous mmap backed every page of its span with a real frame at
once. A runtime that reserves a large region with PROT_NONE and commits a
fraction of it, which is how Go lays out its heap arena, would have spent
frames on address space nobody touched, and the guest's window is under two
gigabytes, so a few such reservations exhausted it.

A PROT_NONE anonymous mapping is now a reservation: the span is recorded
and no frame is mapped. The kernel demand-fills a zeroed page on first
access, as it does for any not-present user page, so the reservation costs
only what the guest touches; a fixed read-write mapping over it, which is
how the runtime commits, backs the pages it uses. Fork copies a backed span
and reserves an unbacked one without copying frames that do not exist.
Two cgo-free static Go programs as guests: hello brings the runtime up and
forces a GC, conc runs eight goroutines over channels behind a wait group.
Neither uses cgo, a loader or the netpoller, so each proves the runtime's
threads, memory and signals with nothing but the syscalls already served.
Built here with the container's Go toolchain.

The NONOS_LINUX_GUESTS store packs every test guest and had grown past the
vfs load budget once these were added. That store is about guests, not
media, so it no longer carries the movie samples; the normal image, which
does not set NONOS_LINUX_GUESTS, still ships them.
The boot image's table of contents was capped at 64 entries. The
Linux-guest test image packs a signed set per guest, four files each, and
with the Go guests added it needs more than 64. The table decodes into a
heap vector and every byte is still held under MAX_TOTAL_BYTES, so the
count only sizes the table: 128 entries reserve 16 KiB. The pack tool and
the vfs move together.
The store the guest image packs carries a signed set per guest, and with
the demo capsules and the desktop's egui proof it ran past the vfs load
budget. Those demos are the desktop's, not the guests', so the test image
leaves them out the same way it leaves out the movie samples: the entries
are grouped behind a variable the guest makefile empties, and the normal
image still packs them.
The mapping area sat between 512 MiB and 1 GiB, so a runtime that reserves a wide address range up front, as Go's page allocator does for its summary, ran out of room and aborted. Move the base to 4 GiB, above the stack and images, raise the limit toward the top of user space, and cap every map, reserve, unmap and protect at that top rather than at the stack. A reservation still backs no frames until it is touched, so the width costs nothing.
@senseix21

Copy link
Copy Markdown
Collaborator

Reviewed at 1910df85d (draft, 209 commits, 1043 files, +31683/−2747, 127 commits behind main, last pushed 2026-09-28).

Verdict: Comment. The draft status is right and the body is honest about what is not done. Nine lanes are red — but only one of the nine is a substantive finding, six are one line each, and the shape of the rest is the problem worth leading with: the trivial failures are currently hiding the gates that would actually judge this change.

Before that, the part that deserves to be said first.

It boots, and the evidence says so rather than asserting it

From nonos-benchmarks-36366081290-1/boot-log.json: zk_attest_ok: 24, zk_attest_fail: 0, fatal: 0, panic: 0, the full spawn chain through app.setup_wizard and proof_io, first GPU flush at 8647 ms, userspace_entry_ms 2531. On a 209-commit change that rewrites CPU feature detection, over-aligned heap allocation and FPU save/restore — the three things most able to make a kernel stop coming up at all — the machine still boots clean under TCG on one vCPU. That is the hardest thing here to get right and it is right.

Critical

1. The only substantive build failure is a ring 0 budget overrun, and it is not declared anywhere.

nonos-verify build is the single cause of three red lanes (build / build, production-build / build, and benchmark / benchmark via build-verify-fast). It fails exactly one check of eight. From ci-reports-build/build/tcb-budget.txt:

[tcb] 4513 files, 133901 lines of ring 0 code
[tcb] baseline 132664, delta +1237
::error::tcb grew past its baseline: 133901 against 132664. Fix the change, or justify moving the baseline in the PR.

Where it went, net src/ lines over 7837afaeff..1910df85d: userspace +535, hardware +442, arch +394, process +380, syscall +259, memory +206. The largest single blocks are src/hardware/broker/confine/{map,attach,table,detach}.rs and src/hardware/broker/dma/map/{transaction,fail}.rs (~340 lines of per-device DMA confinement), src/arch/x86_64/iommu/tables/{publish,touched}.rs (~100), src/arch/x86_64/cpu/xstate.rs (75), and src/userspace/init/linux_jobs/* (~250).

Most of that plausibly belongs in ring 0 — DMA confinement and a job supervisor are not things a capsule can do for itself — so the resolution is probably to move the baseline rather than shrink the change. But the gate asks for the justification in the PR, and the body does not mention ring 0 growth at all. The part worth noticing: the DMA confinement is not Linux personality. On a change already at 1043 files, it is the piece a reviewer would most want argued for on its own.

2. The new assumption register ships red, and its failure blinds the four gates that are about this PR's subject matter.

b3fbb1757 adds tools/nonos-assumptions and verification/ASSUMPTIONS.md and wires it into verify.yml:118. On this head it reports 102 found, 10 stated, 33 unlisted, 0 stale. All 33 are lean-axiom: ids and all are Aeneas opaque models of core/alloc primitives — core.sync.atomic.AtomicU64Align8U64.load, core.core_arch.x86.cpuid.__cpuid, alloc.string.String.new, core.mem.size_of — against a register carrying exactly one lean-axiom row (core.option.Option.ok_or, line 89).

The gate is a good idea and the direction is right. Two problems with how it lands.

First, what the red costs. abi-contracts runs these as sequential steps in one job with no if: always(), so steps 10–14 skip: "No new control that exists and does not run", "Linux syscall coverage does not fall", "Wayland coverage does not fall", "Every served Linux call says what it discloses", "Every mutant still removes the control it names". Those four are precisely the gates that exist to judge a Linux personality change, and a missing table row is hiding all of them.

Second, it does not survive the rebase. I ran this PR's own tools/nonos-assumptions against main at dceba0e6f with this PR's register: 122 found, 10 stated, 53 unlisted, 0 stale. main went from 5 to 591 files under verification/extraction/lean/NonosExtraction/ in the 127 commits this branch is behind, and each new extraction file brings more per-function opaque models. One hand-written markdown row per Aeneas-generated core shim gets worse every time the Lean corpus grows.

Smallest corrective action, two parts: keep the register hand-written for the kinds a human must read (stated, crate, prim, hw, tool) and reduce lean-axiom to a generated block or one row per module of opaque core models — an opaque model of AtomicU64::load teaches a reader nothing that stated:extraction does not already say. Then put if: always() on the steps after it, so one row cannot hide five gates.

Important

3. hygiene is red on a single false positive, and it hides five more steps.

Reproducing nonos-verify hygiene's scanner (nonos-verify/src/hygiene/{patterns,roots,scan}.rs) over src and userland at this head gives exactly one violation:

userland/capsule_wallet_nonos/src/wallet/etna/parts/fact.rs:18:placeholder-comment

The line is //! capitals on the left, the value on the right. Never a placeholder value. — a doc comment flagged for containing the word "placeholder" while stating the rule the scanner enforces. The file is new in this PR (1aaa149bc), and the same scanner over main's tree returns nothing, so this PR is what turns the lane red.

Same skip cascade as Critical 2: hygiene steps 6–10 skip, including "No new exported function that nothing calls" — the ratchet that would have caught Important 4 below.

Smallest corrective action: reword to "Never a stand-in value". The scanner matching a substring inside a negated sentence is an accepted cost of the approach, not worth changing for one line.

4. The new crypto_proofs mirror includes the attestation verifier but no caller, so the Pedersen path compiles dead.

crypto-proofs fails with five dead-code errors under -D warnings, all in userland/crypto_proofs/src/security/capsule_attest/: POLICY_EPOCH and POLICY_TREE_DEPTH (layout.rs:17,18), TRAILER_MAGIC and parse (trailer.rs:26,28), verify (against_pedersen.rs:24).

They are all live in the kernel — src/security/capsule_attest/against_root.rs:36,57 calls against_pedersen::verify, which calls trailer::parse. The mirror's mod.rs #[path]-includes error.rs, layout.rs, trailer.rs and against_pedersen.rs but not against_root.rs, and the only caller of verify inside the mirror is #[cfg(test)] mod local_root_tests (local_root_tests.rs:21). So the plain lib target has no live root for the chain and the lane rejects it.

Smallest corrective action: pub use against_pedersen::verify; in the mirror's mod.rs. One line, gives the lib target a root, and leaves mod.rs as declarations only.

5. The help width ratchet is now unenforced, and the commit that added it recorded why that matters.

runnable-proofs fails two tests in userland/terminal_line_proofs/src/usage_tests.rs:

  • :98 — only parsed 3 help rows (expected ≥ 15)
  • :111 — unaligned help row: "Type a command and press Enter. Tab completes."

help_rows() (:73) parses literal out.writeln(b"…") lines out of capsule_terminal/src/command/builtin/help.rs as text. This PR restructured that file into GROUPS and DEEPER tables rendered by row() with explicit padding, plus help_tools::tools and help_pages::{KEYS,SHELL}. Three literal writeln calls survive — one banner and two blanks — so the harness now parses the banner and nothing else, and the banner is neither lowercase-labelled nor nine-space indented.

Not a product defect. But what is being given up is specific, and that test's own doc comment is the record of it: it used to assert against COLS, the 96-column line buffer, and "passed while help was visibly clipped in a default window". Somebody went to the trouble of narrowing it to 80. Both the 80-column bound and the alignment rule are now unchecked.

Smallest corrective action: assert on behaviour rather than source text — a unit test in capsule_terminal that calls help::run against a fake Output and checks the emitted lines. That survives the next restructure of help.rs; re-teaching a text parser about GROUPS and DEEPER does not.

Minor

  1. evidence-manifest: verification/evidence/EVIDENCE.json is stale, and the error states the fix — ./verification/evidence/collect-evidence.sh > verification/evidence/EVIDENCE.json, then commit.
  2. proof-crates (capsule_linux_proofs) fails on one lint. userland/capsule_linux_proofs/src/tests/mutation_tests.rs:35 is let mut s = 0xDEB5_EEDu64;, which trips unusual_byte_groupings under -D warnings. 0x0DEB_5EED_u64 is the same value and keeps the joke.
  3. The build report records build-aarch64 as a gap ("kernel target json present, build lane not wired") and riscv64 likewise. Worth knowing here because linux: land the Linux lane on main; terminal linux command, signals to running threads, pipe waits, madvise, VFS store, Process Manager #593 — the only PR in this stack on a current base — meets that unwired lane as a hard break rather than a gap.

Questions

  1. Is the ring 0 growth in Critical 1 meant to be in this PR? src/hardware/broker/confine/ and src/arch/x86_64/iommu/tables/ read as a separate change that happens to share a branch.
  2. The body says signal delivery's personality half is not done. linux: process lifecycle and signals as Linux has them #585 and linux: land the Linux lane on main; terminal linux command, signals to running threads, pipe waits, madvise, VFS store, Process Manager #593 each implement per-thread signal stacks and rt_sigframe independently on top of this exact head. Which of those two is the one you intend to keep?

Verified correct

  • Boot is measured, not claimed. 24 of 24 capsules attest, no fatal, no panic, through app.setup_wizard and proof_io. The per-capsule attest samples are tight too (23 samples, min 182 ms, avg 200 ms, max 305 ms), so nothing in the new spawn path is intermittently slow.
  • The FPU work holds where it would show. build-x86_64-capsules, symbol-scan and section-size all pass on the release ELF. The body's claim that kernel text carries no xmm or ymm is exactly the kind symbol-scan exists to keep honest, and it is the lane that would have gone red if the soft-float build had regressed.
  • The proof floor did not move to pay for the new tests. proof-coverage passes against scripts/baselines/proof-coverage.txt, so 2648 new lines of capsule_linux_proofs did not come at the cost of extracted-code theorem lines.
  • 0 stale in the register, in both trees. The bidirectional claim in tools/nonos-assumptions' docstring — that a row nothing rests on fails too — holds for every kind except lean-axiom, on this head and against main.
  • The refusals are refusals, not gaps. calls served=1500 unserved=0 with ptrace, process_vm_readv/writev, capget/capset, mount/umount2, chroot, unshare and setns on EPERM and the io_uring family on ENOSYS, each with a logged reason, is the right shape for a personality that is not trying to become a kernel.
  • boot-smoke, extraction, kani, lean, adversarial, attestation, attestation-attack, boot-proofs, evidence tooling and all seven dark-features-compile variants pass, along with 58 of 59 proof-crates matrix entries.

The stack

Every one of #582, #584, #585, #586, #587, #588 and #593 has its merge base at exactly 1910df85d. #582, #584, #585, #586 and #588 are independent siblings of each other; #587 is stacked on #585; #593 is stacked on #582 and is the only one rebased onto current main. So this PR is the trunk and nothing downstream can land before it.

That is what makes the six one-line fixes above the highest-leverage work in the lane. They are not polish — they are what stands between this trunk and a set of gate verdicts anyone can read, including the four Linux-specific gates that have not actually run yet.

CI at this head

Nine failures, none of them cancelled-run noise. One cause covers three (nonos-verify build / tcb-budget → build, production-build, benchmark). One line each for hygiene, evidence-manifest and proof-crates (capsule_linux_proofs). One table for abi-contracts, one re-export for crypto-proofs, one stale harness for runnable-proofs. Everything else green.

@eKisNonos

Copy link
Copy Markdown
Contributor Author

Superseded. This work is integrated into the 0.9.2 release and ships in the current tree. Closing as part of the 0.9.2 consolidation.

@eKisNonos eKisNonos closed this Oct 2, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants