From 4f23a6dd8fe63f25c2951e1b8c5b43526ccc966b Mon Sep 17 00:00:00 2001 From: Philipp Erhardt Date: Sun, 1 Mar 2026 09:37:47 +0000 Subject: [PATCH 1/4] Update Rust version --- .devcontainer/Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index 3c9491b..761c3b0 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -85,7 +85,7 @@ ENV CARGO_HOME=/usr/local/cargo ENV KANI_HOME=/usr/local/kani ENV PATH="/usr/local/cargo/bin:${PATH}" -ARG RUST_VERSION=1.90.0 +ARG RUST_VERSION=1.93.1 RUN --mount=type=cache,target=/usr/local/cargo/registry \ curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \ | sh -s -- -y --no-modify-path --default-toolchain ${RUST_VERSION} && \ From 2855d266e819fbb3770b5197a6b7c0d9c186d7a4 Mon Sep 17 00:00:00 2001 From: Philipp Erhardt Date: Sun, 1 Mar 2026 09:38:30 +0000 Subject: [PATCH 2/4] Dev container: fix cacheFrom for podman --- .devcontainer/devcontainer.json | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 1269dcc..89b2ba7 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -5,8 +5,7 @@ "dockerfile": "Dockerfile", "context": "..", "cacheFrom": [ - "ghcr.io/osirisrtos/osiris/devcontainer:main", - "ghcr.io/osirisrtos/osiris/devcontainer:main-cache" + "ghcr.io/osirisrtos/osiris/devcontainer", ] }, "privileged": false, From 35817801751917bc4456e73014cb822ec3d1baa0 Mon Sep 17 00:00:00 2001 From: Philipp Erhardt Date: Sun, 1 Mar 2026 10:19:34 +0000 Subject: [PATCH 3/4] Fix kani compilation Also restoring MIN_RANGE_SIZE that seems to have been deleted accidentally in 86e35b25ebfc37dcf0d493424e46637b1a383e39 --- interface/src/lib.rs | 22 +++++++++++++++++++ src/mem.rs | 51 ++++++++++++++++++-------------------------- src/mem/alloc.rs | 1 + 3 files changed, 44 insertions(+), 30 deletions(-) diff --git a/interface/src/lib.rs b/interface/src/lib.rs index 1a334a8..ad78f0a 100644 --- a/interface/src/lib.rs +++ b/interface/src/lib.rs @@ -17,6 +17,28 @@ pub struct MemMapEntry { pub ty: u32, } +#[cfg(kani)] +impl kani::Arbitrary for MemMapEntry { + fn any() -> Self { + let size: u32 = kani::any_where(|&x| x % size_of::() as u32 == 0); + let length = kani::any(); + let addr = kani::any(); + + kani::assume(addr > 0); + + MemMapEntry { + size, + addr, + length, + ty: kani::any(), + } + } + + fn any_array() -> [Self; MAX_ARRAY_LENGTH] { + [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) + } +} + #[repr(C)] #[derive(Debug, Clone, Copy, bytemuck::Pod, bytemuck::Zeroable)] pub struct InitDescriptor { diff --git a/src/mem.rs b/src/mem.rs index b1ec789..e38b3a2 100644 --- a/src/mem.rs +++ b/src/mem.rs @@ -95,35 +95,10 @@ pub fn align_up(size: usize) -> usize { // VERIFICATION ------------------------------------------------------------------------------------------------------- #[cfg(kani)] mod verification { - use crate::MemMapEntry; + use crate::mem::alloc::MAX_ADDR; use super::*; - use kani::Arbitrary; - - impl Arbitrary for MemMapEntry { - fn any() -> Self { - let size = size_of::() as u32; - let length = kani::any(); - let addr = kani::any(); - - kani::assume( - length < alloc::MAX_ADDR as u64 - && length > alloc::BestFitAllocator::MIN_RANGE_SIZE as u64, - ); - kani::assume(addr < alloc::MAX_ADDR as u64 - length && addr > 0); - - MemMapEntry { - size, - addr, - length, - ty: kani::any(), - } - } - - fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) - } - } + use interface::{Args, InitDescriptor, MemMapEntry}; fn mock_ptr_write(dst: *mut T, src: T) { // Just a noop @@ -135,6 +110,7 @@ mod verification { let mmap: [MemMapEntry; _] = kani::any(); kani::assume(mmap.len() > 0 && mmap.len() <= 8); + // Apply constraints to all for entry in mmap.iter() { // Ensure aligned. kani::assume(entry.addr % align_of::() as u64 == 0); @@ -142,6 +118,14 @@ mod verification { kani::assume(entry.addr > 0); kani::assume(entry.length > 0); + kani::assume( + entry.length < alloc::MAX_ADDR as u64 + && entry.length > alloc::BestFitAllocator::MIN_RANGE_SIZE as u64, + ); + kani::assume(entry.addr < alloc::MAX_ADDR as u64 - entry.length && entry.addr > 0); + } + + for entry in mmap.iter() { // Ensure non overlapping entries for other in mmap.iter() { if entry.addr != other.addr { @@ -153,13 +137,20 @@ mod verification { } } - let mmap_len = mmap.len(); + let mmap_len = mmap.len() as u64; let boot_info = BootInfo { - implementer: core::ptr::null(), - variant: core::ptr::null(), + magic: interface::BOOT_INFO_MAGIC, + version: kani::any(), mmap, mmap_len, + args: Args { + init: InitDescriptor { + begin: kani::any(), + len: kani::any(), + entry_offset: kani::any(), + }, + }, }; assert!(init_memory(&boot_info).is_ok()); diff --git a/src/mem/alloc.rs b/src/mem/alloc.rs index d02c2fd..710ad03 100644 --- a/src/mem/alloc.rs +++ b/src/mem/alloc.rs @@ -45,6 +45,7 @@ pub struct BestFitAllocator { /// Implementation of the BestFitAllocator. impl BestFitAllocator { + pub const MIN_RANGE_SIZE: usize = size_of::() + Self::align_up() + 1; /// Creates a new BestFitAllocator. /// /// Returns the new BestFitAllocator. From b6dbc491da5392c6a6c00c8eb6583c84e680ccb3 Mon Sep 17 00:00:00 2001 From: Philipp Erhardt Date: Sun, 1 Mar 2026 10:44:53 +0000 Subject: [PATCH 4/4] Use latest tag --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b57322c..96f89e9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -39,7 +39,7 @@ jobs: id: set_output run: | REPO=$(echo "${GITHUB_REPOSITORY}" | tr '[:upper:]' '[:lower:]') - CONTAINER_NAME="ghcr.io/${REPO}/devcontainer:main" + CONTAINER_NAME="ghcr.io/${REPO}/devcontainer:latest" echo "container_name=$CONTAINER_NAME" >> $GITHUB_OUTPUT echo "container_without_tag=ghcr.io/${REPO}/devcontainer" >> $GITHUB_OUTPUT