Conversation
The block was aligned to the layout and the data handed out 32 bytes into it, after the header, so any request aligned to 64 or more came back aligned to 32 only. FXSAVE needs 16 and never noticed; XSAVE needs 64 and took a general protection fault on the first switch. The data now starts at the header size rounded up to the alignment, with the header directly before it, where free and verify already look. Free computes the same offset from the same layout.
install pacman:<name> fetches each configured repository's database and its detached signature, refuses the install if the database is unsigned or does not verify, and resolves the closure by name and then by what a package provides. Each package is held to the market's pin when chosen, to the database's SHA-256, and to its own OpenPGP signature, then decompressed (zstd, gzip or plain tar; xz is refused by name) and placed through the same verified path as Alpine's. Nothing is guessed: the mirror, Host line, path and repositories are build settings, and the keyring is pinned into the capsule from the file NONOS_PACMAN_KEYRING names. An image built without them refuses every pacman install and says which is missing. RSA goes to the crypto service as an SPKI with the signature padded to the modulus width. The proof crate runs that exact request through the checks the service runs, against GnuPG's RSA-3072 signatures, and tests the desc reader, including file names that would leave the repository.
Streams with padding between them, blocks, the index and the footer, each held to its CRC-32 and to one another: a block's declared sizes to what it decoded, the index to every block, the footer to the header and the index. LZMA2 chunks stored or LZMA, with dictionary, state and property resets; every check type xz writes (none, CRC-32, CRC-64, SHA-256). LZMA2 is the one filter read; a block naming BCJ or any other is refused, never skipped. The vectors are XZ Utils' output for the zstd vectors' inputs, from -0 to -9e, multi-block, odd lc/lp/pb, a 4 KiB dictionary. The test regenerates the inputs from the one generator. Breaking the literal state update or the rep3 shift fails them. A seeded mutation harness damages six vectors 2000 ways each in a debug build.
A package or database compressed with xz is decoded with nonos_xz instead of refused; zstd, gzip and plain tar are unchanged. The bytes are the same verified bytes either way: the checksum and signature are checked on the compressed file before any decompression.
The base64 between the BEGIN and END lines, armor headers skipped, and the CRC-24 line checked when there is one. Padding anywhere but the end and characters outside the alphabet are refused. The vectors are regenerated with an armored RSA key and an armored detached signature; tests check the armored key has the exported key's fingerprints, the armored signature verifies, and a changed checksum line is refused. A seeded harness damages both 4000 ways each.
FNINIT and LDMXCSR reset the x87 unit and the SSE control word and nothing else, so a thread with no saved state began with xmm and the upper ymm halves as the last thread on the CPU left them. The guest state suite caught it: a forked child read a sibling's bytes in ymm0-15 in 254 of 300 rounds. init now restores a constant clean area, FCW 0x037F and MXCSR 0x1F80 with every register zero and an XSAVE header marking every component initial, through XRSTOR, or FXRSTOR where XSAVE is off. The signal path uses the same init, so a handler starts clean too.
The OpenPGP check, the crypto service request, decompression by magic and the SHA-256 hex reader move out of pacman into install, where the Debian backend will use the same code rather than a copy of it. Nothing changes in what they do; the proof crate mounts them from their new places and passes unchanged.
install deb:<name> fetches the suite's Release and Release.gpg (armored or binary) and refuses the install unless it verifies under the archive key pinned from NONOS_DEB_KEYRING. Each component's Packages.xz or Packages.gz must match the size and SHA-256 the Release gives it, and each .deb the SHA-256 its stanza gives, and the market's pin when it is the one chosen. The data member is unpacked through the same verified path as Alpine's and pacman's; maintainer scripts are never run. Needs are groups of alternatives and the first one the index has is taken. Release's Valid-Until is not checked, for want of a trusted clock, and the source says so. The tar reader now strips the ./ dpkg writes before every member name and hard-link target. Without it every file in a .deb was refused as a dot name and nothing was placed; the three .deb tests fail when the stripping is removed. Symlink targets are left as written. The family is now chosen in family.rs, so run.rs is Alpine's alone. Vectors are made with Debian's tools: .debs from dpkg-deb with xz, zstd and gzip data members, a symlink, alternatives and a virtual package, indexed by dpkg-scanpackages, and a Release signed with a throwaway GnuPG key. The proof crate walks the chain an install walks, checks a changed Release fails, refuses pool paths that leave the root, and damages the .debs, Packages, Release and pacman desc records 1500 ways each in a debug build.
The kernel was compiled with SSE and SSE2, so compiled kernel code on the interrupt and syscall paths used xmm registers before the switch saved the thread's state: the timer handler overwrote a guest's xmm0-15 and the save that followed stored the kernel's values. The guest state suite lost every one of 300 rounds in both processes. The kernel target now matches x86_64-unknown-none: every SIMD feature off and the soft-float ABI. Floating point in the kernel becomes soft float; the only vector instructions left are the FPU save and restore and the SIMD exception handler's MXCSR access, all written by hand. Userland keeps its own target, SSE included. The kernel's warnings are the same 47 either way.
The soft-float target covers Rust, but the kernel also links C and assembly compiled apart from it. PQClean's ML-DSA, ML-KEM and SHAKE were built with the compiler's default SSE, and BLAKE3 linked its SSE2 and SSE4.1 assembly: 1548 vector moves in kernel text, the PQClean ones on paths a syscall reaches, such as checking a capsule's signature. The kernel's C and assembly are built with -mno-mmx -mno-sse -mno-sse2 -mno-avx, and BLAKE3 with its portable implementation on every target.
The aarch64 core profile (microkernel-core + nonos-arch-preview) had not compiled at any commit in this history: 4 errors at the root commit, 59 here, with codegen and link failures behind them. It now builds and links. - process::foreign is x86_64 only. Elsewhere foreign_absent.rs answers every SYS_FOREIGN_* and SYS_PEER_* call with ERRNO_NOSYS: no other architecture parks an unknown syscall for a supervisor. - memory::mmu stays x86_64 only. Its users are gated; on aarch64 the boot log states PAN is not enabled and the hardening entry point refuses by name. - mapping_in_asid masks interrupts through the helper its siblings use, AddressSpace::kernel reads the root through arch::paging::read_root, and the aarch64 descriptor backend exports is_executable. - STZG takes its tag from a register holding 0; XZR is not encodable in that field. - linker_aarch64.ld defines the eight __kernel_* section bounds that layout::kernel_sections reads on the boot path. - The lib.rs comment states what the arch gate does and nothing more. x86_64 microkernel-core: all three PT_LOAD segments are byte identical before and after. Only a ThinLTO .llvm symbol suffix in .strtab moves.
The FEAT_PAN probe read ID_AA64MMFR1_EL1[3:0], which is HAFDBS. PAN is [23:20]. A core with HAFDBS and no PAN would have executed MSR PAN and taken an undefined instruction on the first user copy; a core with PAN and no HAFDBS would never have opened the window. The comment on allow() and deny() said MSR PAN was encoded by hand. It was not, and the target spec has no +pan, so LLVM rejects both on the first concrete caller of with_user_access. They are now .inst 0xd500409f and 0xd500419f, which llvm-objdump decodes as msr PAN, #0 and #1.
Seven static_mut_refs warnings: the table getters formed &mut and & to whole static mut items. The address getters now use addr_of!, which creates no reference, and the &'static mut getters borrow through addr_of_mut! with the aliasing rule written as a # Safety contract. The secondary entry is cast through its fn pointer type rather than as a function item.
cause.rs imported two contract types it never names, pl011 re-exported two config types no path reaches, the AP idle path read its CPU id and discarded it, and FP_SIMD_CONTEXT_BYTES had no user.
Add a build-aarch64 lane that runs make nonos-mk-arm, the target a developer runs, then checks the output with check_kernel_elf.py: an AArch64 static executable whose entry is _start inside an executable PT_LOAD, no segment both writable and executable, and the signed manifest and signature sections present. nonos-mk-arm now asks only for the Ed25519 seed that build.rs reads, not an ML-DSA keypair it never uses. nonos-setup skips the aarch64 JSON targets the same way it skips the x86_64 ones.
"not ready, refused" named no reason: the transport error, or which of the seven readiness checks failed, or a release that did not resolve. Each is now printed with the listing, so a refusal says what to fix.
bind, listen and accept4 under a NetBind capability carrying an explicit bind set, loopback and external named apart, no shared ports, accepted sockets confined like their listener, and raw sockets refused by name. With the five properties it must be proved against.
The store asks to install a listing's default release with an empty id. Readiness read that as the first release; get_release looked for a release named "" and found none. Init was told the package was ready, got no release to pin, and refused every store install. get_release now resolves through the same find_release, and the proof crate pins it: an empty id is the first release, a named id is that one, an unknown listing or release is nothing.
The standing pane assumed the gate list was six rows tall, but it also paints the verdict and a note line above them, so the measurement label was drawn over the attestation row. gates::paint now returns the y it ended at and the pane carries on from there.
The personality is spawned as app.linux.install and app.linux.run on endpoints 4938/4939 and 4942/4943, and its manifest listed only app.linux's. The spawn gate refuses an endpoint the manifest does not declare, so every store install stopped at capsule_verify_fail and every run of an installed package would have too. init also prints the spawn error when the installer is refused, which is how this was found.
The installer exits with a code that names why it stopped: the index did not verify, something is in no index, the closure is too large, a package did not download or verify, or the image has no mirror or key for the family. init records every asked-for install as queued, running, refused or, once the installer has ended, installed or failed with that code, read without reaping from the process table or the reap log. MkAppInstallStatus returns that stage for a listing to any caller that holds AppInstall, the capability MkAppInstall already needs; asking changes nothing. It is in the syscall registry, the capability table, the router, the ABI description and libc as mk_app_install_status.
A request no longer ends at "install requested". The store asks the system where each install stands every half second while one is moving, and not at all when none is. The card's one button reads Install, Queued, Installing, then Open once installed, or Retry after a failure, and the detail pane says what happened in a sentence, naming the reason the installer gave. Enter does the next thing: install, wait, or open. On refresh every Linux listing is asked about once, so one installed earlier in the session reads as installed. The pane no longer repeats the verdict as a separate Install label, and the status bar's Enter hint is the button's own word.
The detail pane asks the market for the default release and shows its version and the host its bytes come from under the publisher, and the operator's validation note, such as the size it hashed, below the gates.
The line being typed opened with ">~", which read like a redirect into a file named "~". It is "~ $ " now, path first, the mark in the last command's colour, and a space before the cursor; echoed commands carry the same "$ ". The window opens at 960 by 540, centred on a 1280 by 720 screen, where 760 by 460 was filled by help alone. Bare help was nineteen lines of commands, key bindings and syntax at once. It is now the command groups, with the group names in the accent colour, and three ways to go deeper: help keys, help shell, and help <command> as before. Each page only lists what the shell does: the separators and the alias form were checked against the parser.
The x86_64 backend picks the IOMMU from the firmware tables instead of assuming VT-d: a DMAR remapping unit selects VT-d, else an IVRS table selects AMD-Vi, else none. CPUID is never read, so QEMU's intel-iommu under KVM on an AMD host stays VT-d. select_vendor, capabilities and report_posture state only guarantees in force now. VT-d reports enforcing only while translation is live and the firmware described exactly one unit, because bring-up programs the first unit only. Snoop control is read from ECAP.SC through the new decoder regs::cap::snoop_control, not from the leaf flag. AMD-Vi and machines with no IOMMU report nothing in force. Domain calls are routed by the selected vendor. On VT-d, and before selection has run, they reach the unchanged VT-d functions. Otherwise each is refused with a log line and IommuError::AmdViNotDriven or IommuError::NoIommu. The VT-d tree gains only the decoder. No live DMA outcome changes: MkDmaMap and the direct memory::dma allocators still hand out host-physical addresses and IommuDomain still has no caller. The Cargo.toml comment that claimed otherwise is fixed. x86_64 behaviour changes: B1 init_dma_protection selects first. The VT-d probe and bring-up run only when DMAR described a remapping unit, as the same two calls in the same order. B2 without a DMAR unit, "[VT-D] no remapping units in DMAR; DMA is unrestricted" is no longer printed. An [AMD-VI] or [IOMMU] selection line naming the missing backend replaces it. B3 every boot prints "[IOMMU] vendor= enforcing= aw= ir= snoop= pages= domains=" after the VT-d lines, which are unchanged. B4 after selection on AMD-Vi or IOMMU-less machines the six domain calls return AmdViNotDriven or NoIommu with a log line instead of NotInitialized. Nothing calls them today. The x86_64 core image changes: .text grows by 1408 bytes and .rodata by 448. PT_LOAD count, addresses and flags are unchanged.
…i-up Cell.iommu now names the device QEMU presents: "" for none, "intel-iommu" or "amd-iommu", and qemu.py maps each to its -device argument. Every cell that reaches readiness must print the [IOMMU] posture line with the vendor and enforcing value its device calls for: none 0, intel-vt-d 1, amd-vi 0. The intel-iommu cells keep both existing checks: no "DMA is unrestricted", and the "[VT-D] enumerated devices identity mapped; others denied" line present. The new q35-amdvi-up cell boots the single-CPU image with an amd-iommu and must also carry the [AMD-VI] line that names the hardware the kernel does not drive, so the refusal is asserted rather than assumed. No kernel change; the image is untouched by this commit.
The rule a trust anchor is held to (three independent sources agreeing, recorded with where and when), the two claims a pinned keyring can and cannot make, and the BlackArch finding of 2026-09-27: the keyring tarball is signed by a key its own trusted list does not include, the key strap.sh pins is a different one, and no source outside blackarch.org was reachable. The backend stays keyless and refuses every install.
table() took its second argument as _user_accessible and dropped it, while table_grants_user reads APTable[0] (bit 61), a bit table() never set. Every interior entry the aarch64 backend wrote therefore granted EL0, including the kernel-half entries seed_kernel_half_pdpts builds with false. A table built without user access now sets APTABLE_NO_EL0, as x86_64 clears U/S. - arch_paging_proofs: table_grants_user(table(pa, user)) == user, as a host test on both backends and a Kani harness over every pa and both values. The host test fails on the previous encoder and passes on this one. - Paging.lean is regenerated by the pinned Charon and Aeneas; the only change is table's body. Regenerating from the parent is byte stable. - PagingRefinement: the_aarch64_table_honours_the_request and the_backends_agree_on_tables on the extracted code. The old body is kept as oldAarch64Table, and the_aarch64_table_ignores_the_request and the_backends_disagree_on_tables are restated on it rather than deleted. Checked with Lean 4.30.0-rc2 and the pinned Aeneas: lake build of the extraction corpus completes, 1720 jobs, and each new theorem depends on propext, Classical.choice and Quot.sound only. x86_64 microkernel-core: all three PT_LOAD segments byte identical.
unreachable_pub reported 106 items on the aarch64 build. None hides dead code: every one is used inside the crate. This applies rustc's own suggestion (pub(crate) or pub(super)) to the 56 in the aarch64 tree. Kept pub on purpose: the ten aarch64_exc_* handlers, which vectors.S calls by symbol and so form the assembly ABI. The 40 remaining are in shared files. unreachable_pub on aarch64 goes from 106 to 50. No file this touches is compiled for x86_64.
Off x86_64, clear_low_half returned Ok having done nothing and init then printed "[VM-INIT] low half cleared". aarch64 still executes from that identity map, so it is kept and the log now says "low half kept"; the "cleared" line prints only on x86_64, where the teardown happens. The timer line said "TSC freq" on aarch64, where the rate is CNTFRQ_EL0. The label is a per-architecture constant placed after every panic site, so the call keeps its line and x86_64 keeps its bytes. x86_64 microkernel-core: all three PT_LOAD segments byte identical.
deliver.rs said any thread answered without a handler is marked for its next tick. Only a futex wake and rt_sigreturn do that (Guest::rearm); a thread whose frame could not be placed or written is answered bare and keeps the signal queued for its next answer. The doc now names the two.
Since 6331bf6 keeps empty arguments, `linux ""` made the empty token the program. The PATH search resolved each directory for it, and the launch reported "linux: /bin is a directory". An empty name now gets the usage line, as a missing one does, and as it did before.
6f1f990 ended a thread's stop mark in settle(), when the thread takes a handler answer. Between the post and the take the thread does not read as parked, since parked_nr looks for one with no answer, so a MkForeignInterrupt for another signal marks it and returns 0. settle() then dropped that newer mark with the old one, and the second signal waited for the thread's next call: a handler that spins without calls never got it. answer_raw now drops the mark as it posts a handler answer, under the parked table's lock, and a mark set after that stops the thread at its next tick. Other answers leave the mark as before. The window was read from the code. No guest reaches it yet: a signal does not end a futex wait here, and the personality keeps no signal mask, so no boot shows the second signal lost before this change or delivered after it.
Each part passed once its handler had run, on any thread, so a signal delivered to the wrong thread of the process passed too. The worker and each handler now record their thread id, and a part passes only when its handlers ran on the worker; a handler run elsewhere prints "ran on another thread". Checked on Linux both ways: as written all three parts pass, and with the first signal sent to main instead all three fail so.
The spinning thread set the direction flag after publishing `spinning`, so main could raise the signal before `std` ran, and the handler's check that DF is clear on entry held whatever the kernel did. DF is now set first.
Two more parts, for what 38af0e4 and 314495b change: - A PROT_NONE reservation with a read-write MAP_FIXED mapping over half of it, as Go makes its heap, is written, given MADV_DONTNEED, and then read(2) fills one of its pages from a pipe. The pages must read zero and the read must land. - The ENOMEM part now also checks that the mapped pages of the span with a hole read zero afterwards. On Linux all nine parts pass.
Run from the terminal on 79d6a6a, cwait failed one part, "absolute timer through epoll (1, 76)", where the same image's boot run gave 103 ms. The absolute deadline was taken from the clock before settime, epoll_create1 and epoll_ctl, and the stopwatch started after them; with the desktop running those three calls took about 24 ms, so a timer that fired on time measured 76. The one-shot read started its stopwatch after settime in the same way. Both now time from before the timer is armed: the one-shot from before settime, the absolute one from the clock reading its deadline is made from. A timer firing early still fails. On Linux all 18 parts pass, the two waits at 100 ms each.
A Linux guest was listed as foreign:linux or foreign:fork whatever it ran, with 0 in its syscall and memory columns: its calls trap to the supervisor before the syscall entry counts them, and its pages come from peer calls that never touched its resident count. - MkForeignStart and MkForeignExec name the guest after the last part of argv[0] on its new stack, as Linux's comm, at most 15 bytes of printable ASCII behind a "foreign:" the guest cannot remove. The stack is read under the peer lock and only in the guest's own half. - A forked child takes its parent's name, as a Linux child its comm. - A trapped call counts as one of the guest's syscalls. - MkPeerMap and MkPeerUnmap add and subtract the pages they map and unmap in the guest's resident count. A page filled on first touch of a reservation is not counted yet. exec.rs's context helpers move to exec_swap.rs, keeping it within the line limit. All 11 guest boots pass on this change.
The detail pane wrapped a process's grant chips downward with no bound, while End Process and Force Quit sit at the bottom of the pane. A process with several grants had its chips drawn under Force Quit, whose tinted ground let them show through the label. The chips now stop above the actions. Grants without room are counted in a last "+N more" chip on the final row that fits, so none goes missing unsaid. The chip painters move to insp_chip.rs. For a Linux guest the Mmapped field said "0 KB in 0 regions": its mappings are kept by its supervisor, and the kernel lists none. It now says so in words.
Overview draws its table below the four cards, but the hit test measured rows from the top of the pane. A click on a process row resolved to a slot past the end of the list and selected nothing, and a click on the cards could resolve as a sort. The arrow keys also clamped against a table as tall as the whole pane. The table's rect now comes from one function, table_rect, which the painter, the hit test and the row budget all read.
Share of RAM was a whole percent printed with a ".0" after it, so every process under a hundredth of RAM read 0.0%. It is now computed in tenths: a guest with 11.6 MB of 1580.6 MB reads 0.7%. The Memory screen printed "0 KB" mmapped for a Linux guest, whose mappings its supervisor keeps and the kernel does not list. The cell now says "supervisor", as the detail pane already says "kept by its supervisor".
The grant table stopped at ProcessControl (bit 25). A grant from bit 26 to bit 33 was counted in a process's Authority but drawn as no chip at all: the terminal holds AttestRead and showed "Authority 9" over eight chips. The table now runs through LocalSign, in the kernel's enum order, and moves out of format.rs into format_caps.rs.
When the selected process ended, the selection fell back to the first process in the whole list, even one the filter hides. With the table filtered to "foreign" and every Linux guest gone, the detail pane named app.about while the table was empty, and End Process would have aimed at it. The fallback is now the first row the table shows. When the filter matches none, nothing is selected: the pane reads "No process selected" and End Process asks for a selection first.
The half block U+2580 was drawn from the face, whose glyph stops about a pixel short of the cell's edges. Between rows of half blocks a one-pixel line of the other colour showed, as thin stripes across the flat colours of pictures drawn with them. Block elements (the halves, eighths and quadrants from U+2580 to U+259F, without the shades) are now filled as exact spans of the cell, as the box-drawing lines already run to its edges.
security-packages.txt lists 26 security and networking tools from Alpine main and community (nmap, tcpdump, tshark, masscan, radare2, john, hydra, aircrack-ng, nikto, openssl and more), grouped by use, with the ones that need a live network target marked so an operator knows which want the network capability granted before they reach anything. SECURITY-TOOLSET.md records how a tool reaches the machine through the existing verified pipeline (catalogue measures its BLAKE3, the market serves a signed index, install holds the bytes to the distribution's own signature, the tool runs as a foreign guest at Authority 0), and what each still needs: its measurement enrolled, and the network capability for the tools that reach a target. The catalogue was run against radare2, nmap, openssl and john: it fetched and hashed the real signed bytes and listed each, held back until enrolled.
A dynamically linked tool maps its shared libraries executable, and the personality proves every executable file before any of its pages run, so an unproven library is refused: openssl and file, brought in with their Alpine closure as data, failed at load with "Operation not permitted" on the first library. LINUX_GUEST_LIBS names a library and its path under /linux, the way LINUX_GUEST_PROGRAMS names a program, and gives each a certificate, manifest and trailer so the machine has agreed to run it. With libcrypto, libssl and libmagic proved this way, openssl 3.3.7 and file 5.45 run: openssl prints its version and hashes stdin to the same SHA-256 as the host, and file reads its magic database and names an ELF by the same build id.
A dynamically linked musl guest ran correctly but took a SIGSEGV at exit: openssl 3.3.7 and file 5.45 printed the host's exact output, then ended with status 139. musl loads a library by reserving its whole file, then laying the segments over that reservation. The data segment's file mapping reaches past its filesz into the pages musl then covers with a fixed anonymous mapping to zero the bss. That overlay did nothing here, because peer_map leaves a page already present in place, so the bss kept the file bytes read past the segment (libcrypto's section-header table), and a library global that should be null held .rodata's address 0x30e000. Its teardown read of that global faulted. A fixed anonymous span is zeroed pages by definition, even where frames are already there, so drop those frames first and let the map fill fresh, zeroed ones. A reservation has no frames to drop, so the commit-over-reservation path a runtime uses is unchanged. On a boot, openssl and file now exit 0 with the same output, and no fault is logged.
Guest TCP leaves through the mixnet and nowhere else. When the mixnet holds no gateway, net.sockets answers the connect with E_NO_TRANSPORT (6); the personality turned every non-zero status into ECONNREFUSED, so a program was told a peer had answered and refused it when no packet could have left the machine. Status 6 is now ENETUNREACH, the errno Linux gives when there is no route. Every other refusal stays ECONNREFUSED, and a call that got no reply stays EIO. The mixnet stays the only way out: nothing here opens a direct path.
…ishes them virtio-net wrote descriptors, avail ring slots and the frame itself, then the avail index, with no fence anywhere. The descriptor and ring stores are volatile, but the frame bytes on the TX side are a plain copy, and Rust only orders volatile accesses against each other: the compiler is free to sink the copy past the index store that tells the device to read it. On the RX side the used element and the frame were read after the used index with nothing tying them to it. x86 hardware keeps these in order today; the language does not, and a weakly ordered CPU would not either. A release fence now sits before every avail index store (prime, refill, TX post) and an acquire fence after the used index is seen to move, the same pairing virtio-gpu already used. virtio-gpu had the acquire in the wrong place: after reading the used entry rather than before, so it ordered nothing the entry depended on. It moves ahead of the reads.
Both capsules re-ran their whole setup in a yield loop for ten seconds when no device matched, then exited 0. The broker is filled from PCI during kernel init, before the first capsule starts, so discovery gives the same answer on every pass; the loop only burned the CPU through that part of boot. On a PC, which has neither device, that was ten seconds of every boot. While virtio-net sat in it, net_core's link probes to driver.virtio_net0 went unanswered and each one waited out its timeout. A failed discovery now exits 2, as e1000, rtl8139 and rtl8169 do for an absent chip. The bounded retry stays for a device that is present and fails a later step. Booted with an e1000 on plain VGA, so with neither device present, both now leave with code 2 as they start and the desktop comes up on the GOP framebuffer. With no virtio-net present, net_core had logged "ipc.call unanswered driver.virtio_net0" five times in a boot; with this it logs it none.
…al, take short frames
The driver never answered the stack. It tagged replies with its own magic
(0x4E45_3130) and sent them to KERNEL_REPLY_ENDPOINT, an inbox nothing has read
since the stack moved into capsules. net_core and net_l2 speak NNET
(0x4E4E_4554) and wait for the answer to their own call, which is how
virtio-net replies. Requests are now taken with mk_ipc_recv_from and every
answer goes back to the capsule that asked, with mk_ipc_reply, under the
NNET tag. The ops and payload layouts already matched.
Booted as the only NIC, the e1000 came up and net_core's probe got nothing
("link probe driver.e1000_0 no-answer"). With this it binds and takes the
lease itself: "bind: interface up on driver.e1000_0", "lease 10.0.2.15/24 gw
10.0.2.2", and the mixnet directory fetch connects and handshakes over it as
it does over virtio-net.
TX posted every frame unconditionally and then spun on DD. When the spin ran
out the handler answered E_IO but left the descriptor live with TDT already
moved, and the next call wrote over the same slot without looking. On silicon
the 8254x sets no DD while the link is down (auto-negotiation after SLU, a
pulled cable, a blocking switch port), so every send timed out; after 31 of
them TDT caught up with TDH, which the part reads as an empty ring, and later
posts overwrote buffers it might still be fetching. A frame answered E_IO was
also still sent once the link came up, so a retry went out twice. QEMU's model
sets DD with the link down, which is why it never showed. TX now keeps a clean
index: reclaim walks it over finished descriptors, a ring with no free slot
answers E_AGAIN (one slot always stays empty), and a frame is answered once it
is queued.
The reset wrote CTRL and the receive address within microseconds of RST
clearing. A global reset starts an EEPROM auto-load that rewrites RAL0/RAH0 and
parts of CTRL, so the drawn station address could be replaced by the factory
one afterwards and unicast would go to the wrong filter. The sequence now
follows e1000_reset_hw: mask, stop RX and TX, wait 10 ms for bus-master cycles
in flight, reset, keep off the part for the first millisecond, poll RST clear
against a time bound rather than a spin count, then wait 20 ms for the
auto-load (5 ms on 82540/5/6, 20 on 82541/7) before anything is written.
Frames under 60 bytes were refused. TCTL.PSP has the part pad them, and ARP
(42) and a bare TCP ACK (54) are shorter than that, so IPv4 stopped right after
DHCP. A bare header is now the minimum.
The driver bound its INTx line and never used it: it polls and IMS is never
set. The discovery filter also skipped the NIC when firmware left Interrupt
Line at 0xFF, which UEFI commonly does, and a bound line is masked until acked,
so a shared GSI stayed masked for any other device on it. No line is bound
now, and the capsule gives up the Irq capability in its manifest and in the
kernel's spawn spec.
Release fences sit before the TDT and RDT writes and the ring hand-over, and an
acquire follows the DD reads, as in virtio-net.
e1000_proofs: 14 passed. The host shim gains Deadline, the fixture drops the
IRQ grant, and the request fixture carries the NNET tag. The no-entropy test
still holds the transmitter and receiver to never having been written, so
the quiesce writes TCTL as 0.
…the ring The driver never answered the stack. It tagged replies with its own magic (0x4E52_3839) and sent them to KERNEL_REPLY_ENDPOINT, an inbox nothing has read since the stack moved into capsules. net_core and net_l2 speak NNET (0x4E4E_4554) and wait for the answer to their own call, which is how virtio-net replies. Requests are now taken with mk_ipc_recv_from and every answer goes back to the capsule that asked, with mk_ipc_reply, under the NNET tag. The ops and payload layouts already matched. Discovery skipped any card whose PCI Interrupt Line read 0xFF. OVMF leaves it there, as UEFI firmware commonly does, so booted under OVMF with an RTL8139 as its only NIC the driver exited 2, absent. The line was only ever bound to be acked; the driver polls. It binds none now, sets IMR to 0 so an unserviced source cannot hold a shared INTx asserted for another device, and gives up the Irq capability. The station address was the factory one, read out of IDR: the identifier nonos_mac exists to keep off the wire, where e1000 and rtl8169 already drew theirs. It is now drawn through nonos_mac too, written as dwords with the config lock open as 8139too writes it, read back, and fails closed. The capsule gains Crypto, which CryptoRandom is gated on, in its manifest and in the kernel's spawn spec. Booted under OVMF as the only NIC, it now binds and takes the lease itself: "bind: interface up on driver.rtl8139_0", "lease 10.0.2.15/24 gw 10.0.2.2", and the mixnet directory fetch connects and handshakes over it. QEMU's `info network` shows the card at b6:54:0b:29:cc:83 rather than its configured 52:54:00:12:34:56, so the lease was taken under the drawn address. RCR set no RBLEN bits, so the chip used an 8K+16 ring while every offset here was taken against 32K. After about 8 KB received the chip wrote at the start of the ring and the driver read zeros at 8K: ROK clear, an error, and every later receive failed the same way. QEMU honours RBLEN too (8192 << RBLEN), so this was reachable in emulation. RBLEN is now 10, the 32K+16 ring the allocation was already sized for. With RCR.WRAP set, a frame that crosses the end of the ring is written on past it into the slack, not back at the start, but reads wrapped modulo the ring and took the tail of that frame from offset 0: stale bytes once a lap. Reads are linear now, and a read past the allocation returns zero. The ring proofs held the modulo behaviour; they now hold the linear one, over a buffer the size of the real allocation, and still check that no read leaves it. The chip does not pad short frames and frames under 60 bytes were refused, so ARP (42) and bare TCP ACKs (54) were never sent. A bare header is the minimum now and send zero-pads to 60. A bad header (ROK clear, or a length no good frame carries) returned without moving, so the same header was read forever. Receive now restarts from the top of the ring the way 8139too's rx_err does. A good frame too big for the caller (a tagged full-size one) is skipped instead of stalling, and 0xFFF0 (still arriving) is left for the next poll. TX walked TSD0-3 with a cursor that stayed put when a send failed, while the chip's own pointer moved on, so every later send waited on a descriptor the chip would never look at again. TX is now four slots with a cursor and a reclaim index, as 8139too keeps cur_tx and dirty_tx: a slot is finished on TOK, TUN or TABT, an abort writes TCR.CLRABT to restart the transmitter, a full ring answers E_AGAIN, and the early-TX threshold starts at 256 bytes rather than 8. Rx and Tx are enabled before RCR and TCR are written, as 8139too and the BSD drivers do. rtl8139_proofs: 7 passed.
The driver never answered the stack. It tagged replies with its own magic (0x4E52_3639) and sent them to KERNEL_REPLY_ENDPOINT, an inbox nothing has read since the stack moved into capsules. net_core and net_l2 speak NNET (0x4E4E_4554) and wait for the answer to their own call, which is how virtio-net replies. Requests are now taken with mk_ipc_recv_from and every answer goes back to the capsule that asked, with mk_ipc_reply, under the NNET tag. The ops and payload layouts already matched. It could not have come up on any card in any case. The station address is drawn with CryptoRandom, which is gated on the Crypto capability, and neither the manifest nor the kernel's spawn spec granted it: the draw failed closed and bring-up stopped with "no entropy for station address". Both grant it now, as they already did for e1000 and rtl8821ce. Discovery skipped any card whose PCI Interrupt Line read 0xFF, which is what UEFI firmware commonly leaves there, so on those PCs a present RTL8111/8168 was reported absent. The line was only ever bound to be acked; the driver polls. It binds none now, sets IMR to 0 so an unserviced source cannot hold a shared INTx asserted for another device, and gives up the Irq capability. The TX doorbell wrote TPPoll bit 7, which polls the high-priority ring. Only the normal-priority ring (TNPDS) is ever set up; THPDS is never written. On a real card the part fetched a descriptor from whatever THPDS held after reset, the real descriptor kept OWN, the first send timed out and every later one saw "busy". No frame was ever transmitted. The doorbell is bit 6, NPQ, as in Linux r8169. Both rings could fall a slot behind the part for good. On an RX descriptor error the slot was re-armed but the cursor stayed, while the part had already moved on; low-rate traffic like ARP then sat unread until fifteen more frames wrapped the ring. On TX the cursor moved only after a clean completion, so a TER or a slow completion (link still negotiating) left it on a slot the part had left. The RX cursor now advances past a bad descriptor, and the TX cursor advances the moment OWN is handed over; the OWN check on the next slot is the full-ring test, answered with E_AGAIN. The station address went into IDR with byte writes. The part takes IDR as dwords; byte writes are dropped on silicon, the readback check failed, and bring-up stopped there. It is now two 32-bit writes, high dword first, each read back to post it, as rtl_rar_set does. RxConfig and TxConfig were written with the receiver and transmitter off. On the 8169 and 8168B-F those writes can be lost and the accept bits never take. TE|RE now go on first, then the two configs, still after the station address, so the part is never enabled under the factory one (the bring-up proof that watches for that still passes). Frames under 60 bytes were refused. ARP (42) and a bare TCP ACK (54) are shorter than that; they are now zero-padded to 60, which also covers the 8168 revisions that pad short frames wrong. No QEMU model exists for this chip. rtl8169_proofs: 8 passed; the bring-up proof now holds IMR at 0.
"bind: interface up" did not say which interface. With a wired port and a WiFi link both present the choice is the first thing to know, and on a boot with one NIC it is what ties the lease that follows to a driver. The line now names the candidate, for example "bind: interface up on driver.e1000_0".
No profile carried e1000, rtl8139 or rtl8169, so none of them had ever been booted with the stack. This target is the desktop profile plus those three, under the same attestation. QEMU models the e1000 and the RTL8139, so each can be booted as the only NIC and has to take the lease itself; the RTL8169 has no QEMU model and shows that a driver whose chip is absent exits and the boot goes on.
…yout
Setup polled CSR_GP_CNTRL bit 1 for MAC clock ready. In the v1 CSR layout
that every family probed here uses, bit 1 is undefined and the flag is bit 0,
so the poll timed out on every card and the capsule exited before serving
anything. RF-kill was read from INIT_DONE, the bit setup had just set itself,
so the airplane-mode switch was never reported; it is HW_RF_KILL_SW, bit 27,
set while the radio is allowed on. Bz-family parts (BE200) use the v2 layout
and are still not handled.
The legacy firmware parser read the version at offset 8, which is the start of
the 64-byte name ("Core", "rele", "jenk" in the bundled images), so every image
was refused as an unknown API. The header is 88 bytes: version at 72, build at
76, TLVs from 88. The section types were one off (20/21/33): 19 is the runtime
image, 20 INIT, 32 paging, so the INIT and WoWLAN images were staged and the
runtime one never was. The gen3 path already had 19. The API ceiling moves to
86 to take the newest bundled image.
Checked against the six bundled .ucode files: the version at 72 is the API in
each file name (29, 36, 46, 77, 84, 86) and the TLV walk from 88 ends exactly
at the end of every file. The blob test written for this was never declared in
the proofs crate; it is wired in now and runs against the real 7265D-29 image
(four runtime sections, 364400 bytes). iwlwifi_proofs: 76 passed.
This gets the capsule past its first register and its firmware file. It does
not boot the firmware: the per-family load paths, the RX and TX queues and the
post-ALIVE command sequence are still to be written.
The GTK KDE in message 3 carries the key's index, and find_gtk threw it away. The driver then installed every group key in CAM slot 1. With the sec engine looking group-addressed frames up by the CCMP KeyID, that works until the AP rekeys: hostapd starts at 1 and swaps between 1 and 2 on every rekey, so after the first one every broadcast frame (ARP requests, DHCP, router adverts) came in under index 2, found an empty slot, and was dropped. The index now travels from the supplicant through the MLME and the join outcome to install_gtk and the session that removes it. TX data frames were also tagged SEC_TYPE_CCMP in the descriptor after the station had already encrypted them in software (header, CCMP header, MIC). rtw88 sets the security type only for frames with a hardware key; a frame tagged for hardware CCMP after software encryption risks being encrypted twice and failing the AP's MIC check. The tag is now zero. nonos_wifi_core_proofs gains a handshake test that drives the real supplicant with the KDE naming index 1, 2 and 3 (and with the Tx bit set) and holds it to the index sent: 14 passed. rtl8821ce_proofs does not build on main (sec.rs wants a crate::constants the proofs crate never declares, and its tests look for the firmware under the capsule directory rather than nonos-bootloader/firmware/realtek, where it is), so these edits are checked by the capsule build.
#582 gained nine commits on 30 September. Four are already here as the same commits. The other five are earlier forms of 07d9c92, d7b2019, f5fe356, 2b5c726 and 5b40bbc, which this branch carries in the split form linux/next-waits gave them. The tree here already holds all of it, so the merge keeps it as it is, and #582 and this branch now merge into main in either order.
Brings the wired NIC, virtio and wifi fixes into the integration branch, and with them main as of eb2c0cc. Two files met both lines. The drivers branch maps a connect with no transport to ENETUNREACH against main's connect.rs, which still builds the host body inline; this branch moved that into host_body.rs. The resolution keeps host_body.rs and routes both connect paths through the new outcome(). errno.rs keeps this branch's constants and adds ENETUNREACH. With this recorded here, the drivers PR and this one merge into main in either order.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Base:
main. This is the integration branch for the Linux lane. It merges the open lane and fix PRs, so it builds and boots as one image:linux/go-guests, throughlinux/next-waitsui/shield-swap-terminalsetup/wait-for-desktopamd/iommu-runtime-selectarch/aarch64-trap-namesiommu/snoop-and-bus-masterdrivers/net-real-hardware, which brings main up to eb2c0cc. Itsconnect.rsanderrno.rsmeet this branch's; the merge keepshost_body.rsand routes both connect paths through the newoutcome().It also records #582's nine newest commits. Four are here as the same commits; five are earlier forms of commits this branch carries in the split form
linux/next-waitsgave them. So #582, #592 and this one merge into main in any order.On top of those it carries 76 commits of its own, listed below. Its diff against main shrinks as each of those PRs merges; merging this one lands them all.
Its own commits
Terminal runs Linux programs
tool.linux, not in the embedded tools' registry).linux <prog> [args]runs a program from the Linux tree. A bare name is found along the guest'sPATH, and every argument is passed on.Signals to a running thread
MkForeignExecrefuses a thread stopped at a tick, and a syscall numbered as a stop code gets ENOSYS.Waits and pipes
readvandwritevwait on a pipe asreadandwritedo.Memory
madvisedoes what Linux promises, or refuses. On a span with a hole it advises what is mapped, then returns ENOMEM.mprotect's commit andmremap's growth keep the mark.forkcopies each region a megabyte at a time.Store and VFS
Process Manager
Kernel
Also
Proof guests (C)
cpipe: bytes through a pipe between two processes.csig: signals for threads that were parked.cpreempt: a handler reaching a spinning thread, with DF set.cmadv: madvise against Linux's rules.cwait: waits, timers,pthread_kill.Checked
capsule_linux,capsule_terminal,capsule_process_manager,capsule_market.dceba0e6f(Lean verification: prove 164 more functions and fix the kernel bugs the proofs found #591). The one clash, themodlist inuserland/kernel_proofs/src/lib.rs, keeps both sides.950541d8a, the kernel compiles (microkernel-corecheck) andkernel_proofspasses (89).capsule_linux, the NIC and virtio drivers,net_core,capsule_terminalandcapsule_process_managercompile; Lean verification: prove 164 more functions and fix the kernel bugs the proofs found #591 touched none of them.4c3f164bc.