Nexus OS Docs

Appearance

Nexus-Linux NipCell ​

Proof-mode boot proven

The Nexus-Linux NipCell is the bridge between the sovereign Rumpk kernel and foreign Linux driver worlds. Linux runs inside a cell, loads normal Linux drivers or bridge modules, and communicates with Rumpk through ION Rings.

This is not a Linux distribution. Linux is a contained hardware and compatibility daemon.

Current proof status ​

The M9 proof now boots a real ARM64 Linux Image from a staged Rumpk EL2 handoff in QEMU. The proof reaches Linux /init, validates the mapped ION header, and loads all four bridge modules:

ComponentProof status
ARM64 Linux Image direct QEMU bootProven
Rumpk AArch64 default bootProven, 17/17
NipCell host testsProven, 15/15
Staged EL2 Linux guest bootProven, 33/33
nexus_ion bridge moduleLoads in proof-mode guest
nexus_net bridge moduleReports network bridge ready on nx0
nexus_blk bridge moduleReports block bridge ready (nxblk0 major=252)
nexus_input bridge moduleReports input bridge ready

The proof log records:

  • Stage-2 ION map 0x90000000 -> 0x5F000000, size 0x01000000;
  • seeded ION header magic 0x494F4E52;
  • Stage-2 translation sync before eret;
  • guest IRQ ownership left with Linux;
  • Linux command line with ion_base=0x90000000;
  • ARM arch timer online;
  • Run /init as init process;
  • ION header validation;
  • all four bridge modules ready.

Reproduce the proof ​

Run this from a source checkout:

bash
cd nexus-forge/core/rumpk
zig build test-nipcell --summary all
zig build -Darch=aarch64 \
  -Dproof-stage-linux-image=true \
  -Dproof-el2-vmentry-smoke=true \
  -Dproof-el2-eret-attempt=true \
  --summary all
./run_aarch64.sh el2-staged-eret-attempt \
  2>&1 | tee /tmp/nexus-m9-staged-eret-m9-pass.log
zig build -Darch=aarch64 --summary all
./run_aarch64.sh test \
  2>&1 | tee /tmp/nexus-m9-default-aarch64-test.log

Expected results:

text
15/15 test-nipcell tests pass.
The proof build passes.
=== EL2 Staged ERET Attempt Result: 33/33 ===
The restored default AArch64 path reports === Result: 17/17 ===.

What this proves ​

The proof demonstrates that Rumpk can stage and enter a Linux guest through the EL2 handoff, provide a Linux-consumable DTB, map the production carve-out and shared ION window through Stage-2, and let Linux load the Nexus bridge modules against the seeded ION header.

The proof also checks negative conditions:

  • no halt before eret;
  • no fallback to Nim handoff;
  • no EL2 diagnostic trap;
  • no timer panic;
  • no invalid ION magic;
  • no unresolved module symbols.

What remains open ​

The default production start path is still deliberately fail-closed. Public claims must keep this boundary clear.

Open work:

  • Wire the staged EL2 handoff into the default nipcell_start_result() path.
  • Define the guest console policy. The proof reaches /init, but Linux still warns that it cannot open an initial console.
  • Add a DTB reserved-memory entry or equivalent allocator guard for the ION shared window.
  • Trim or gate verbose EL2 proof diagnostics before release.
  • Prove real cross-boundary Block Valve exchange over the mapped guest ION rings.