From 082643e763a4c28c03bdc8bd30bb89135852f49e Mon Sep 17 00:00:00 2001 From: Vasilito Date: Sat, 18 Apr 2026 21:38:30 +0100 Subject: [PATCH] Expose proof helpers in runtime surfaces --- local/AGENTS.md | 18 +++++++- .../system/redbear-info/source/src/main.rs | 42 +++++++++++++++++++ local/scripts/build-redbear.sh | 10 +++++ 3 files changed, 68 insertions(+), 2 deletions(-) diff --git a/local/AGENTS.md b/local/AGENTS.md index 166ce16d..03c823e8 100644 --- a/local/AGENTS.md +++ b/local/AGENTS.md @@ -181,7 +181,11 @@ redox-master/ ← git pull updates mainline Redox │ │ ├── finalize-wifi-validation-run.sh ← Analyze a Wi-Fi capture bundle and package the final evidence set │ │ ├── validate-vm-network-baseline.sh ← Static repo-level VM networking baseline check │ │ ├── test-vm-network-qemu.sh ← QEMU launcher for the VirtIO VM networking baseline -│ │ └── test-vm-network-runtime.sh ← In-guest runtime check for the VM networking baseline +│ │ ├── test-vm-network-runtime.sh ← In-guest runtime check for the VM networking baseline +│ │ ├── test-ps2-qemu.sh ← QEMU launcher for the bounded PS/2 + serio runtime proof +│ │ ├── test-timer-qemu.sh ← QEMU launcher for the bounded monotonic timer runtime proof +│ │ ├── test-lowlevel-controllers-qemu.sh ← Sequential wrapper for bounded low-level controller proofs +│ │ └── test-usb-maturity-qemu.sh ← Sequential wrapper for bounded USB maturity proofs │ └── docs/ ← Integration docs ``` @@ -214,14 +218,24 @@ redox-master/ ← git pull updates mainline Redox ./local/scripts/test-xhci-irq-qemu.sh --check ./local/scripts/test-msix-qemu.sh ./local/scripts/test-iommu-qemu.sh +./local/scripts/test-ps2-qemu.sh --check +./local/scripts/test-timer-qemu.sh --check +./local/scripts/test-lowlevel-controllers-qemu.sh ./local/scripts/test-usb-storage-qemu.sh ./local/scripts/test-usb-qemu.sh --check +./local/scripts/test-usb-maturity-qemu.sh # The current xHCI proof checks for an interrupt-driven mode in boot logs. # The current MSI-X proof uses the live virtio-net path in QEMU. # The current IOMMU proof runs a guest-driven first-use self-test and checks that discovered # AMD-Vi units initialize and drain events successfully in QEMU. -# The USB storage proof currently verifies whether usbscsid autospawns without hitting crash-class errors. +# The current PS/2 proof checks serio node visibility and then hands off to the existing Phase 3 +# input-path checker inside the guest. +# The current timer proof checks that /scheme/time/CLOCK_MONOTONIC advances across two guest reads. +# The aggregate low-level wrapper runs xHCI, IOMMU, PS/2, and timer proofs in sequence. +# The USB storage proof now verifies usbscsid autospawn plus bounded sector-0 readback against a +# host-seeded pattern, while guest-side write verification is still open. +# The aggregate USB wrapper runs xHCI mode, full USB stack, and USB storage readback proofs in sequence. # Legacy Phase 4 Wayland runtime validation (historical P0-P6 numbering; script still works) ./local/scripts/build-redbear.sh redbear-wayland diff --git a/local/recipes/system/redbear-info/source/src/main.rs b/local/recipes/system/redbear-info/source/src/main.rs index 040aee08..59b58369 100644 --- a/local/recipes/system/redbear-info/source/src/main.rs +++ b/local/recipes/system/redbear-info/source/src/main.rs @@ -343,6 +343,26 @@ const INTEGRATIONS: &[IntegrationCheck] = &[ note: "Functional when the iommu scheme is registered in /scheme.", functional_probe: Some(probe_iommu_scheme), }, + IntegrationCheck { + name: "redbear-phase-ps2-check", + category: "Validation", + description: "Bounded PS/2 + serio runtime proof helper", + artifact_path: Some("/usr/bin/redbear-phase-ps2-check"), + control_path: Some("/scheme/serio/0"), + test_hint: "redbear-phase-ps2-check", + note: "Functional when the PS/2 proof helper is installed and both serio keyboard/mouse nodes are visible.", + functional_probe: Some(probe_serio_surface), + }, + IntegrationCheck { + name: "redbear-phase-timer-check", + category: "Validation", + description: "Bounded monotonic timer runtime proof helper", + artifact_path: Some("/usr/bin/redbear-phase-timer-check"), + control_path: Some("/scheme/time/4"), + test_hint: "redbear-phase-timer-check", + note: "Functional when the monotonic time scheme node is visible for bounded runtime timer proof.", + functional_probe: Some(probe_time_surface), + }, IntegrationCheck { name: "udev-shim", category: "System", @@ -2140,6 +2160,28 @@ fn probe_iommu_scheme( probe_named_scheme(runtime, "iommu") } +fn probe_serio_surface( + runtime: &Runtime, + _network: &NetworkReport, + _hardware: &HardwareReport, + _check: &IntegrationCheck, +) -> Option { + (runtime.exists("/scheme/serio/0") && runtime.exists("/scheme/serio/1")).then(|| { + "serio keyboard and mouse nodes are visible for PS/2 proof".to_string() + }) +} + +fn probe_time_surface( + runtime: &Runtime, + _network: &NetworkReport, + _hardware: &HardwareReport, + _check: &IntegrationCheck, +) -> Option { + runtime + .exists("/scheme/time/4") + .then(|| "monotonic time scheme node is visible for runtime proof".to_string()) +} + fn probe_rtl8125_path( _runtime: &Runtime, network: &NetworkReport, diff --git a/local/scripts/build-redbear.sh b/local/scripts/build-redbear.sh index c667718c..794100f1 100755 --- a/local/scripts/build-redbear.sh +++ b/local/scripts/build-redbear.sh @@ -213,6 +213,16 @@ if [ "$CONFIG" = "redbear-minimal" ] || [ "$CONFIG" = "redbear-desktop" ]; then echo " ./local/scripts/validate-vm-network-baseline.sh" echo " ./local/scripts/test-vm-network-qemu.sh $CONFIG" fi +if [ "$CONFIG" = "redbear-desktop" ] || [ "$CONFIG" = "redbear-full" ] || [ "$CONFIG" = "redbear-wayland" ] || [ "$CONFIG" = "redbear-kde" ]; then + echo "" + echo "To validate bounded low-level controller proofs:" + echo " ./local/scripts/test-lowlevel-controllers-qemu.sh $CONFIG" + echo " # or run individual checks: test-xhci-irq-qemu.sh, test-iommu-qemu.sh, test-ps2-qemu.sh, test-timer-qemu.sh" + echo "" + echo "To validate bounded USB maturity proofs:" + echo " ./local/scripts/test-usb-maturity-qemu.sh $CONFIG" + echo " # or run individual checks: test-usb-qemu.sh --check, test-usb-storage-qemu.sh" +fi if [ "$CONFIG" = "redbear-wayland" ]; then echo "" echo "To validate the bounded Phase 4 Wayland runtime harness:"