Verus 37/39, rivet artifacts updated, Mathlib integration

BUILD.bazel

@@ -23,8 +23,6 @@ load("//bzl:defs.bzl",
 # Excluded (Verus limitations or proof issues needing rework):
 #   poll.rs: mutable array indexing (Verus limitation)
 #   sched.rs: function pointer types (Verus limitation)
-#   userspace.rs: derived PartialEq on enums not visible to Verus + complex bitwise proofs
-#   mem_domain.rs: spec/exec type boundary issues in overlaps_spec (u64 vs int)
 VERUS_SRCS = [
     "src/lib.rs",
     "src/error.rs",
@@ -61,6 +59,8 @@ VERUS_SRCS = [
     "src/ring_buf.rs",
     "src/event.rs",
     "src/work.rs",
+    "src/userspace.rs",
+    "src/mem_domain.rs",
 ]
 
 PLAIN_SRCS = ["//plain:srcs"]

MODULE.bazel

@@ -60,12 +60,14 @@ git_override(
     module_name = "rules_lean",
     remote = "https://github.com/pulseengine/rules_lean.git",
     commit = "2fe64f13f8df31678a27483286868a67636d7217",
+    patches = ["//patches:rules_lean_mathlib_timeout.patch"],
+    patch_strip = 1,
 )
 
-# Lean 4 toolchain (Mathlib available via lean.mathlib() but not currently used)
+# Lean 4 toolchain + Mathlib (mathlib declared by rules_lean, just use_repo it)
 lean = use_extension("@rules_lean//lean:extensions.bzl", "lean")
 lean.toolchain(version = "4.27.0")
-use_repo(lean, "lean_toolchains")
+use_repo(lean, "lean_toolchains", "mathlib")
 register_toolchains("@lean_toolchains//:all")
 
 # Nix integration for Rocq toolchain

patches/BUILD.bazel

@@ -0,0 +1 @@
+exports_files(["rules_lean_mathlib_timeout.patch"])

patches/rules_lean_mathlib_timeout.patch

@@ -0,0 +1,11 @@
+--- a/lean/private/repo.bzl
++++ b/lean/private/repo.bzl
+@@ -162,7 +162,7 @@
+     result = rctx.execute(
+         [str(lake), "update"],
+         environment = env,
+-        timeout = 600,
++        timeout = 1800,
+         quiet = False,
+     )
+     if result.return_code != 0:

plain/condvar.rs

@@ -1,40 +1,205 @@
-//! Verified condition variable for Zephyr RTOS.
-//!
-//! This is a formally verified port of zephyr/kernel/condvar.c.
-//! All safety-critical properties are proven with Verus (SMT/Z3).
-//!
-//! Source mapping:
-//!   z_impl_k_condvar_init      -> CondVar::init          (condvar.c:21-30)
-//!   z_impl_k_condvar_signal    -> CondVar::signal         (condvar.c:44-61)
-//!   z_impl_k_condvar_broadcast -> CondVar::broadcast      (condvar.c:73-96)
-//!   z_impl_k_condvar_wait      -> CondVar::wait_blocking  (condvar.c:99-121)
-//!
-//! Omitted (not safety-relevant):
-//!   - CONFIG_OBJ_CORE_CONDVAR — debug/tracing
-//!   - CONFIG_USERSPACE (z_vrfy_*) — syscall marshaling
-//!   - SYS_PORT_TRACING_* — instrumentation
-//!   - Timeout handling (modeled as immediate blocking)
-//!
-//! ASIL-D verified properties:
-//!   C1: After init, wait queue is empty
-//!   C2: Signal wakes at most one waiter (highest priority)
-//!   C3: Signal on empty condvar is a no-op
-//!   C4: Broadcast wakes all waiters, returns woken count
-//!   C5: Broadcast on empty condvar returns 0
-//!   C6: Wait adds thread to wait queue (blocking path)
-//!   C7: Signal/broadcast preserve wait queue ordering
-//!   C8: No arithmetic overflow in broadcast woken count
-// Inlined error constants (standalone file for rocq_of_rust)
-const OK: i32 = 0;
-const EINVAL: i32 = -22;
-const EAGAIN: i32 = -11;
-const EBUSY: i32 = -16;
-const EPERM: i32 = -1;
-const ENOMEM: i32 = -12;
-const ENOMSG: i32 = -42;
-const EPIPE: i32 = -32;
-const ECANCELED: i32 = -125;
-const EBADF: i32 = -9;
+// === Standalone stubs (generated by verus-strip --standalone) ===
+
+// Error codes (from crate::error)
+pub const OK: i32 = 0;
+pub const EINVAL: i32 = -22;
+pub const EAGAIN: i32 = -11;
+pub const EBUSY: i32 = -16;
+pub const EPERM: i32 = -1;
+pub const ENOMEM: i32 = -12;
+pub const ENOMSG: i32 = -42;
+pub const EPIPE: i32 = -32;
+pub const ECANCELED: i32 = -125;
+pub const EBADF: i32 = -9;
+pub const EOVERFLOW: i32 = -75;
+pub const ETIMEDOUT: i32 = -110;
+pub const ENOSPC: i32 = -28;
+pub const ENOENT: i32 = -2;
+pub const EADDRINUSE: i32 = -98;
+
+// Priority (from crate::priority)
+pub const MAX_PRIORITY: u32 = 32;
+
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub struct Priority {
+    pub value: u32,
+}
+
+impl Priority {
+    pub fn new(value: u32) -> Option<Self> {
+        if value < MAX_PRIORITY {
+            Some(Priority { value })
+        } else {
+            None
+        }
+    }
+    pub fn get(&self) -> u32 {
+        self.value
+    }
+}
+
+// Thread types (from crate::thread)
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub struct ThreadId {
+    pub id: u32,
+}
+
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum ThreadState {
+    Ready,
+    Running,
+    Blocked,
+    Suspended,
+}
+
+#[derive(Debug, Copy, Clone)]
+pub struct Thread {
+    pub id: ThreadId,
+    pub priority: Priority,
+    pub state: ThreadState,
+    pub return_value: i32,
+}
+
+impl Thread {
+    pub fn new(id: u32, priority: Priority) -> Self {
+        Thread {
+            id: ThreadId { id },
+            priority,
+            state: ThreadState::Ready,
+            return_value: 0,
+        }
+    }
+    pub fn dispatch(&mut self) {
+        self.state = ThreadState::Running;
+    }
+    pub fn block(&mut self) {
+        self.state = ThreadState::Blocked;
+    }
+    pub fn wake(&mut self, return_value: i32) {
+        self.return_value = return_value;
+        self.state = ThreadState::Ready;
+    }
+    pub fn is_blocked(&self) -> bool {
+        matches!(self.state, ThreadState::Blocked)
+    }
+}
+
+// WaitQueue (from crate::wait_queue)
+pub const MAX_WAITERS: u32 = 64;
+
+#[derive(Debug)]
+pub struct WaitQueue {
+    pub entries: [Option<Thread>; 64],
+    pub len: u32,
+}
+
+impl WaitQueue {
+    pub fn new() -> Self {
+        WaitQueue {
+            entries: [
+                None, None, None, None, None, None, None, None,
+                None, None, None, None, None, None, None, None,
+                None, None, None, None, None, None, None, None,
+                None, None, None, None, None, None, None, None,
+                None, None, None, None, None, None, None, None,
+                None, None, None, None, None, None, None, None,
+                None, None, None, None, None, None, None, None,
+                None, None, None, None, None, None, None, None,
+            ],
+            len: 0,
+        }
+    }
+    pub fn len(&self) -> u32 {
+        self.len
+    }
+    pub fn is_empty(&self) -> bool {
+        self.len == 0
+    }
+    pub fn unpend_first(&mut self, return_value: i32) -> Option<Thread> {
+        if self.len == 0 {
+            return None;
+        }
+        let thread = self.entries[0];
+        let mut i: u32 = 0;
+        while i < self.len - 1 {
+            self.entries[i as usize] = self.entries[(i + 1) as usize];
+            i = i + 1;
+        }
+        self.entries[(self.len - 1) as usize] = None;
+        self.len = self.len - 1;
+        match thread {
+            Some(mut t) => {
+                t.state = ThreadState::Ready;
+                t.return_value = return_value;
+                Some(t)
+            }
+            None => None,
+        }
+    }
+    pub fn pend(&mut self, thread: Thread) -> bool {
+        if self.len >= MAX_WAITERS {
+            return false;
+        }
+        let mut insert_pos: u32 = self.len;
+        let mut i: u32 = 0;
+        while i < self.len {
+            let entry_pri = self.entries[i as usize].unwrap().priority.get();
+            let thr_pri = thread.priority.get();
+            if thr_pri < entry_pri {
+                insert_pos = i;
+                break;
+            }
+            i = i + 1;
+        }
+        let mut j: u32 = self.len;
+        while j > insert_pos {
+            self.entries[j as usize] = self.entries[(j - 1) as usize];
+            j = j - 1;
+        }
+        self.entries[insert_pos as usize] = Some(thread);
+        self.len = self.len + 1;
+        true
+    }
+    pub fn unpend_all(&mut self, _return_value: i32) -> u32 {
+        let count = self.len;
+        let mut i: u32 = 0;
+        while i < count {
+            self.entries[i as usize] = None;
+            i = i + 1;
+        }
+        self.len = 0;
+        count
+    }
+}
+
+// === End stubs ===
+
+// Verified condition variable for Zephyr RTOS.
+//
+// This is a formally verified port of zephyr/kernel/condvar.c.
+// All safety-critical properties are proven with Verus (SMT/Z3).
+//
+// Source mapping:
+//   z_impl_k_condvar_init      -> CondVar::init          (condvar.c:21-30)
+//   z_impl_k_condvar_signal    -> CondVar::signal         (condvar.c:44-61)
+//   z_impl_k_condvar_broadcast -> CondVar::broadcast      (condvar.c:73-96)
+//   z_impl_k_condvar_wait      -> CondVar::wait_blocking  (condvar.c:99-121)
+//
+// Omitted (not safety-relevant):
+//   - CONFIG_OBJ_CORE_CONDVAR — debug/tracing
+//   - CONFIG_USERSPACE (z_vrfy_*) — syscall marshaling
+//   - SYS_PORT_TRACING_* — instrumentation
+//   - Timeout handling (modeled as immediate blocking)
+//
+// ASIL-D verified properties:
+//   C1: After init, wait queue is empty
+//   C2: Signal wakes at most one waiter (highest priority)
+//   C3: Signal on empty condvar is a no-op
+//   C4: Broadcast wakes all waiters, returns woken count
+//   C5: Broadcast on empty condvar returns 0
+//   C6: Wait adds thread to wait queue (blocking path)
+//   C7: Signal/broadcast preserve wait queue ordering
+//   C8: No arithmetic overflow in broadcast woken count
 /// Result of a signal operation.
 #[derive(Debug)]
 pub enum SignalResult {
@@ -162,4 +327,4 @@ impl CondVar {
     pub fn has_waiters(&self) -> bool {
         self.wait_q.len() > 0
     }
-}
+}