ps2server: the i8042 driver leaves the kernel, and the owner of input merges every source

Cargo.toml

@@ -33,7 +33,6 @@ members = [
     "kernel/microcode",
     "kernel/pci",
     "kernel/phys",
-    "kernel/ps2",
     "kernel/sim",
     "kernel/smmu",
     "kernel/usbhid",
@@ -53,6 +52,7 @@ members = [
     "lib/fat32/check",
     "lib/gpt",
     "lib/hda",
+    "lib/input",
     "lib/inspect",
     "lib/logkeeper-api",
     "lib/logstream",
@@ -113,6 +113,8 @@ members = [
     "system/netstack/udp",
     "system/netstack/wire",
     "system/pkg",
+    "system/ps2server",
+    "system/ps2server/ps2",
     "system/shell",
     "system/soundserver",
     "system/soundserver/mixer",
@@ -211,6 +213,9 @@ toyos-fat32 = { path = "lib/fat32" }
 # not published until they have both passed on it.
 toyos-fat32-check = { path = "lib/fat32/check" }
 toyos-gpt = { path = "lib/gpt" }
+# The `input` port's name and the one program the image may give it to, so the
+# gate on every manifest reads what its owners and its source read.
+toyos-input = { path = "lib/input" }
 toyos-keymap = { path = "sdk/keymap" }
 # The form a program's line takes in a boot's log and the port `logkeeper` serves it
 # on, so the judges reading the log and `logkeeper` writing it read one declaration.

build/build.rs

@@ -597,12 +597,14 @@ const SUPERVISOR_SERVED: &[&str] = &[toyos_swap::PORT, "power", toyos_manifest::
 /// The ports that one row alone may receive, each with that row: the swap
 /// port, whose holder replaces any service's binary, the grants port, whose
 /// holder writes which folder of the home a package sees, the prompt port,
-/// whose holder draws above every window and has every key while it does, and
-/// the clipboard port, whose holder is sent every copy made in the session.
+/// whose holder draws above every window and has every key while it does, the
+/// input port, whose holder types into the focused window, and the clipboard
+/// port, whose holder is sent every copy made in the session.
 const HELD_ALONE: &[(&str, &str)] = &[
     (toyos_swap::PORT, toyos_swap::HOLDER),
     (toyos_manifest::grants::PORT, toyos_manifest::grants::HOLDER),
     (toyos_manifest::consent::PROMPT, toyos_manifest::consent::SERVER),
+    (toyos_input::wire::PORT, toyos_input::wire::HOLDER),
     (toyos_manifest::clipboard::PORT, toyos_manifest::clipboard::HOLDER),
 ];
 
@@ -3143,6 +3145,23 @@ mod tests {
         }
     }
 
+    /// The input port reaches ps2server alone, and never `[apps]`: a
+    /// connector types into the focused window.
+    #[test]
+    fn only_ps2server_holds_the_input_port() {
+        let gate = |text: &str| held_by_their_holders_alone(&toml::from_str(text).unwrap());
+        assert_eq!(gate("[programs.ps2server]\nreceives = [\"input\"]\n[programs.compositor]\nserves = [\"input\"]\n"), Ok(()));
+        for (text, said) in [
+            ("[programs.paint]\nreceives = [\"input\"]\n", "`paint` receives `input`, which only `ps2server` may hold"),
+            ("[apps]\nreceives = [\"input\"]\n", "`[apps] receives` names `input`"),
+        ] {
+            match gate(text) {
+                Err(why) if why.contains(said) => {}
+                other => panic!("{text:?}: {other:?}, not {said:?}"),
+            }
+        }
+    }
+
     /// `[apps] folder` is one of the two accesses, spelled as the manifest
     /// spells it, and nothing else reaches a manifest.
     #[test]

images/console.toml

@@ -17,7 +17,7 @@
 assets = ["assets"]
 
 [boot]
-start = ["logkeeper", "diskserver", "fileserver", "console", "acpiserver"]
+start = ["logkeeper", "diskserver", "fileserver", "console", "acpiserver", "ps2server"]
 
 # `/system/bin/console` owns the screen and provides the surface its shell and the
 # shell's children inherit. No compositor here, so nothing receives one.
@@ -41,8 +41,12 @@ service = true
 devices = ["acpi"]
 receives = ["power"]
 
+# `input` makes it the owner of input, as the compositor is where there is one,
+# and a row that serves a machine-wide port is a service.
 [programs.console]
+service = true
 provides = ["surface"]
+serves = ["input"]
 receives = ["log"]
 starts = ["shell"]
 devices = ["framebuffer", "keyboard", "mouse"]
@@ -51,6 +55,17 @@ devices = ["framebuffer", "keyboard", "mouse"]
 receives = ["surface"]
 starts = ["toybox", "shell"]
 
+# The i8042, driven from userland: its ports and its two lines are this
+# program's `isa` claim, and the keys and pointer reports it decodes go to the
+# owner of input over `input`, which no other row may receive
+# (`build/build.rs`). Started again when it ends other than by exit 0, which it
+# says only on a machine with nothing to serve.
+[programs.ps2server]
+restart = true
+receives = ["input"]
+devices = ["isa:0060,0064:1,12"]
+
+
 # `power` because `bin/shutdown` below is this binary, and on the machine this
 # image exists for — no serial port, a prompt on the panel — there is no other
 # way to turn it off: it asks the supervisor, which has `logkeeper` make the log whole first.

images/diag.toml

@@ -5,8 +5,7 @@
 # phase boundary and returns immediately once anything claims
 # DEVICE_FRAMEBUFFER. On the image that was flashed to the T14 the compositor
 # claimed it tens of milliseconds after the last checkpoint, so every line the
-# kernel logged — including the one `i8042:` line that says why the integrated
-# keyboard is dead — was on screen for about a tenth of a second and then gone.
+# kernel logged was on screen for about a tenth of a second and then gone.
 #
 # `/system/bin/supervisor` is in every image and holds the one `SysCap`, so the
 # guarantee is that this config declares no `devices`, which

images/system.toml

@@ -19,7 +19,7 @@ assets = ["assets"]
 # while the compositor had no way to ask for a program's *declared* authority —
 # the launcher gives it one, and starting a service from `[boot] start` is not
 # the thing that needed fixing.
-start = ["logkeeper", "diskserver", "fileserver", "compositor", "soundserver", "netstack", "filepicker", "acpiserver", "vdagent"]
+start = ["logkeeper", "diskserver", "fileserver", "compositor", "soundserver", "netstack", "filepicker", "acpiserver", "vdagent", "ps2server"]
 
 # What every program launched out of `/apps` holds, whatever its own directory
 # says. A package is unpacked by `/system/bin/pkg` into a writable directory, so
@@ -70,15 +70,26 @@ receives = ["power"]
 # shell. `prompt` is the layer above every window, which `filepicker` alone
 # reaches: serving it makes the sessions its launches open the screen's, whose
 # packages may ask the person at it for a folder. `clipboard` is sent every copy
-# made in the session, and `vdagent` alone receives it.
+# made in the session, and `vdagent` alone receives it. `input` is where a source
+# of keys and pointer reports reaches the owner of input, which it is.
 [programs.compositor]
 service = true
-serves = ["compositor", "prompt", "clipboard"]
+serves = ["compositor", "prompt", "clipboard", "input"]
 receives = ["soundserver", "filepicker"]
 devices = ["framebuffer", "keyboard", "mouse"]
 starts = ["terminal", "files", "/apps"]
 login = true
 
+# The i8042, driven from userland: its ports and its two lines are this
+# program's `isa` claim, and the keys and pointer reports it decodes go to the
+# owner of input over `input`, which no other row may receive
+# (`build/build.rs`). Started again when it ends other than by exit 0, which it
+# says only on a machine with nothing to serve.
+[programs.ps2server]
+restart = true
+receives = ["input"]
+devices = ["isa:0060,0064:1,12"]
+
 [programs.soundserver]
 service = true
 serves = ["soundserver"]

issues/the-kernel-is-small-interrupts-post-and-threads-wait.md

@@ -17,18 +17,17 @@ kernel's part of a restart, and named module tests hold each program's
 
 ## What is left, in order
 
-1. **ps2server**: stage 7 step 2, with stage 6 step 3.
-2. **Step 9's file half** (stage 4), once libc is a file server's client
+1. **Step 9's file half** (stage 4), once libc is a file server's client
    (`issues/c-programs-name-no-file-a-file-server-holds.md`).
-3. **Step 8's exit** (stage 4). Its empty view needs step 9's file half:
+2. **Step 8's exit** (stage 4). Its empty view needs step 9's file half:
    until then the kernel serves `/system` and `/tmp` to every process.
-4. **P1 of the Wi-Fi track** (`issues/there-is-no-wifi.md`): a BAR stays
+3. **P1 of the Wi-Fi track** (`issues/there-is-no-wifi.md`): a BAR stays
    where firmware put it, handed over in 4 KiB pages with its MSI-X table's
    page, under the owner's Q2 ruling. The orchestrator ruled on #900 that
    this route serves usbd's claim (step 10).
-5. **usbd's whole xHCI**: step 10, with stage 6 step 4, step 4's tail and
+4. **usbd's whole xHCI**: step 10, with stage 6 step 4, step 4's tail and
    step 9's block half, which serve the stick until usbd does.
-6. **Stage 6 step 5, then stage 5's windows.**
+5. **Stage 6 step 5, then stage 5's windows.**
 
 Beside that order, each waiting on something outside it:
 - stage 1's NVMe boot-time measurement, on a ROOT on the T14's NVMe, which
@@ -300,7 +299,7 @@ Beside that order, each waiting on something outside it:
    3. **The i8042's thread is ps2server's** (stage 7 step 2): `irq_ring`'s
       `I8042`, `keyboard_controller::service` and the idle loop's
       `verdict_due` go with the kernel's driver. **Exit**: that step's.
-      **Not started.**
+      **Done** (#899).
    4. **xHCI's thread is usbd's** (stage 4 step 10): `Xhci`,
       `poll_if_pending` and `port_work_pending` go with the kernel's driver,
       and `irq_ring` and `sync::OwedLock`, whose one user is `XHCI`, with
@@ -314,7 +313,7 @@ Beside that order, each waiting on something outside it:
       are met. **Not started.**
 7. **The i8042 leaves the kernel.** Owner ruling, 2026-09-28: drivers are
    userland, and a dead kernel takes no input, with no emergency way.
-   **Partly done**: step 1.
+   **Done**.
    1. **The panic console takes no input, and an `isa` claim grants a process
       exact ports and its ISA lines.** **Done** (#592).
    2. **ps2server**, the server over that claim, delivering to the owner
@@ -337,7 +336,7 @@ Beside that order, each waiting on something outside it:
       and ps2server's restart mid-packet held by `toyos-ps2`'s
       `a_lost_scancode_byte_never_wedges_the_prefix_state` and
       `a_stream_truncated_at_any_offset_resyncs_within_two_packets`.
-      **Not started.**
+      **Done** (#899).
 
 ## Standing
 

kernel/Cargo.toml

@@ -496,7 +496,6 @@ toyos-phys = { path = "phys" }
 toyos-smmu = { path = "smmu" }
 toyos-tco = { path = "../lib/tco" }
 toyos-tsc = { path = "../lib/tsc" }
-toyos-ps2 = { path = "ps2" }
 toyos-rootimage = { path = "../lib/rootimage" }
 toyos-quiesce = { path = "../lib/quiesce" }
 toyos-random = { path = "../lib/random" }

kernel/loom/src/lib.rs

@@ -1,15 +1,14 @@
 //! Loom harness for the kernel's memory-ordering primitives.
 //!
-//! `kernel/src/sync.rs`, `kernel/src/shootdown.rs`,
-//! `kernel/src/sched/reap_gate.rs` and `kernel/src/arch/x86_64/i8042/tally.rs` are
-//! compiled into this crate with `feature = "loom"` on, so their atomics and
+//! `kernel/src/sync.rs`, `kernel/src/shootdown.rs` and
+//! `kernel/src/sched/reap_gate.rs` are compiled into this crate with `feature = "loom"` on, so their atomics and
 //! cells resolve to loom's instrumented ones and the models drive the real
 //! primitives rather than transliterations of them — a transliteration is
 //! exactly the divergence risk a model checker is meant to remove. What the
 //! kernel files name through `crate::` is supplied below: the lock takes a
 //! preempt count and a log macro from its environment, and neither is what the
-//! models are about; `shootdown.rs`, `reap_gate.rs` and `tally.rs` name nothing
-//! at all, which is why none of the three has a shim here.
+//! models are about; `shootdown.rs` and `reap_gate.rs` name nothing at all,
+//! which is why neither has a shim here.
 //!
 //! Scope for the lock, stated because it is narrower than the file: the models
 //! drive `try_lock` and `LockGuard::drop`. `lock()`'s spin cannot be modelled —
@@ -379,13 +378,6 @@ pub mod sleeplock;
 #[path = "../../src/log/handoff.rs"]
 pub mod log_handoff;
 
-/// The i8042's interrupt tally. `tests/i8042_tally.rs` is the only model whose
-/// subject is a *driver*, and it is here for the reason the others are: the
-/// property is "no reader ever sees this pair disagree", which is a claim about
-/// instants that no guest test can express and that x86's TSO hides.
-#[path = "../../src/arch/x86_64/i8042/tally.rs"]
-pub mod i8042_tally;
-
 /// The panic snapshot's owner and access state, driven together by
 /// `tests/panic_capture.rs`.
 #[path = "../../src/drivers/panic_console/latch.rs"]