Introduce Verus

Cargo.toml

@@ -64,6 +64,8 @@ members = [
     "crates/private/tests/root-task/panicking",
     "crates/private/tests/root-task/ring-test-harness",
     "crates/private/tests/root-task/tls",
+    "crates/private/tests/root-task/verus/core",
+    "crates/private/tests/root-task/verus/task",
     "crates/sel4",
     "crates/sel4-async/block-io",
     "crates/sel4-async/block-io/fat",

crates/private/tests/root-task/verus/core/Cargo.nix

@@ -0,0 +1,19 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ mk, verusSource }:
+
+mk {
+  package.name = "tests-root-task-verus-core";
+  dependencies = {
+    builtin = verusSource;
+    builtin_macros = verusSource;
+    vstd = verusSource // { default-features = false; };
+  };
+  package.metadata.verus = {
+    verify = true;
+  };
+}

crates/private/tests/root-task/verus/core/Cargo.toml

@@ -0,0 +1,31 @@
+#
+# Copyright 2023, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+#
+# This file is generated from './Cargo.nix'. You can edit this file directly
+# if you are not using this project's Cargo manifest management tools.
+# See 'hacking/cargo-manifest-management/README.md' for more information.
+#
+
+[package]
+name = "tests-root-task-verus-core"
+version = "0.1.0"
+authors = ["Nick Spinale <[email protected]>"]
+edition = "2021"
+license = "BSD-2-Clause"
+metadata = { verus = { verify = true } }
+
+[dependencies.builtin]
+git = "https://github.com/coliasgroup/verus.git"
+tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+
+[dependencies.builtin_macros]
+git = "https://github.com/coliasgroup/verus.git"
+tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+
+[dependencies.vstd]
+git = "https://github.com/coliasgroup/verus.git"
+tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+default-features = false

crates/private/tests/root-task/verus/core/src/lib.rs

@@ -0,0 +1,23 @@
+//
+// Copyright 2024, Colias Group, LLC
+//
+// SPDX-License-Identifier: BSD-2-Clause
+//
+
+#![no_std]
+
+use vstd::prelude::*;
+
+verus! {
+    pub fn max(a: u64, b: u64) -> (ret: u64)
+        ensures
+            ret == a || ret == b,
+            ret >= a && ret >= b,
+    {
+        if a >= b {
+            a
+        } else {
+            b
+        }
+    }
+}

crates/private/tests/root-task/verus/task/Cargo.nix

@@ -0,0 +1,18 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ mk, localCrates }:
+
+mk {
+  package.name = "tests-root-task-verus-task";
+  dependencies = {
+    inherit (localCrates)
+      sel4
+      sel4-root-task
+      tests-root-task-verus-core
+    ;
+  };
+}

crates/private/tests/root-task/verus/task/Cargo.toml

@@ -0,0 +1,22 @@
+#
+# Copyright 2023, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+#
+# This file is generated from './Cargo.nix'. You can edit this file directly
+# if you are not using this project's Cargo manifest management tools.
+# See 'hacking/cargo-manifest-management/README.md' for more information.
+#
+
+[package]
+name = "tests-root-task-verus-task"
+version = "0.1.0"
+authors = ["Nick Spinale <[email protected]>"]
+edition = "2021"
+license = "BSD-2-Clause"
+
+[dependencies]
+sel4 = { path = "../../../../../sel4" }
+sel4-root-task = { path = "../../../../../sel4-root-task" }
+tests-root-task-verus-core = { path = "../core" }

crates/private/tests/root-task/verus/task/src/main.rs

@@ -0,0 +1,18 @@
+//
+// Copyright 2024, Colias Group, LLC
+//
+// SPDX-License-Identifier: BSD-2-Clause
+//
+
+#![no_std]
+#![no_main]
+
+use sel4_root_task::{debug_println, root_task};
+
+#[root_task(heap_size = 1024 * 1024)]
+fn main(_: &sel4::BootInfoPtr) -> ! {
+    assert_eq!(tests_root_task_verus_core::max(13, 37), 37);
+
+    debug_println!("TEST_PASS");
+    sel4::init_thread::suspend_self()
+}

crates/sel4-externally-shared/src/lib.rs

@@ -52,7 +52,7 @@ impl<'a, T: ?Sized> ExternallySharedPtrExt<'a, T> for ExternallySharedPtr<'a, T,
         T: Atomic,
     {
         let p = self.as_raw_ptr();
-        assert_eq!(p.as_ptr().align_offset(T::ALIGNMENT), 0);
+        assert_eq!(p.as_ptr().cast::<()>().align_offset(T::ALIGNMENT), 0);
         unsafe { AtomicPtr::new(p) }
     }
 }

crates/sel4-runtime-common/src/ctors.rs

@@ -25,7 +25,9 @@ pub unsafe fn run_ctors() {
     // Cast to usize for comparison, otherwise rustc seems to apply an erroneous optimization
     // assuming __init_array_start != __init_array_end.
     if start as usize != end as usize {
-        if !start.is_aligned() || !end.is_aligned() {
+        if start.cast::<()>().align_offset(mem::size_of::<Ctor>()) != 0
+            || end.cast::<()>().align_offset(mem::size_of::<Ctor>()) != 0
+        {
             abort!("'.init_array' section is not properly aligned");
         }
 

crates/sel4/src/invocations.rs

@@ -11,7 +11,7 @@ use core::mem;
 use sel4_config::{sel4_cfg, sel4_cfg_if};
 
 use crate::{
-    cap::*, ipc_buffer, sys, AbsoluteCPtr, CNodeCapData, CPtr, CapRights, Error, InvocationContext,
+    cap::*, sys, AbsoluteCPtr, CNodeCapData, CPtr, CapRights, Error, InvocationContext,
     ObjectBlueprint, Result, UserContext, Word,
 };
 

hacking/cargo-manifest-management/manifest-scope.nix

@@ -11,6 +11,8 @@ let
   filterOutEmptyFeatureList = attrs:
     builtins.removeAttrs attrs (lib.optional ((attrs.features or null) == []) "features");
 
+  mkKeepRef = rev: "keep/${builtins.substring 0 32 rev}";
+
 in rec {
   inherit lib;
 
@@ -180,12 +182,12 @@ in rec {
 
   volatileSource = {
     git = "https://github.com/coliasgroup/volatile.git";
-    tag = "keep/aa7512906e9b76066ed928eb6986b0f9"; # branch coliasgroup
+    tag = mkKeepRef "aa7512906e9b76066ed928eb6986b0f9b1750e91"; # branch coliasgroup
   };
 
   fatSource = {
     git = "https://github.com/coliasgroup/rust-embedded-fat.git";
-    tag = "keep/e1465a43c9f550ef58701a275b313310"; # branch sel4
+    tag = mkKeepRef "e1465a43c9f550ef58701a275b3133105deb9183"; # branch sel4
   };
 
   ringWith = features: {
@@ -216,6 +218,11 @@ in rec {
 
   dafnySource = {
     git = "https://github.com/coliasgroup/dafny.git";
-    tag = "keep/02d0a578fdf594a38c7c72d7ad56e1a6"; # branch dev
+    tag = mkKeepRef "02d0a578fdf594a38c7c72d7ad56e1a62e464f44"; # branch dev
+  };
+
+  verusSource = {
+    git = "https://github.com/coliasgroup/verus.git";
+    tag = mkKeepRef "fdac1c3c52e639bf3e835802f63b43520379b1a1"; # branch dev
   };
 }