verification: add NonNull<T> specification for Verus

Recent changes introduced NonNull<T> usage in SlabPage and VirtAddr,
which caused Verus verification to fail because NonNull is not
supported by default in Verus.

Add external type specification for core::ptr::NonNull<T> following
the vstd pattern used for similar types like ManuallyDrop. The spec
uses accept_recursive_types to allow self-referential structures like
SlabPage, and provides an assume_specification for as_ptr with a
non-null guarantee.

Also mark From<NonNull<T>> for VirtAddr as external_body and fix the
allocate_slab_page spec to reference the const generic N instead of
the undefined variable item_size.

Closes coconut-svsm#938
Signed-off-by: Stefano Garzarella <sgarzare@redhat.com>

Author: stefano-garzarella

kernel/src/address.rs

@@ -527,7 +527,7 @@ impl<T> From<*mut T> for VirtAddr {
 
 #[verus_verify]
 impl<T> From<NonNull<T>> for VirtAddr {
-    #[verus_verify]
+    #[verus_verify(external_body)]
     #[inline]
     fn from(value: NonNull<T>) -> Self {
         Self::from(value.as_ptr())

kernel/src/mm/alloc.rs

@@ -1029,9 +1029,10 @@ impl HeapMemoryRegion {
         with Tracked(perm): Tracked<&mut Option<UnitDeallocPerm>>
         requires
             old(self).wf_next_pages(),
+            N as u64 <= PageStorageType::SLAB_MASK,
         ensures
             old(self).ens_allocate_pages_info(self, 0, PageInfo::Slab(SlabPageInfo {
-                item_size: item_size as u64,
+                item_size: N as u64,
             }) , ret, *perm),
     )]
     fn allocate_slab_page<const N: usize>(&mut self) -> Result<VirtAddr, AllocError> {

verification/verify_external/src/lib.rs

@@ -14,12 +14,15 @@
 #![no_std]
 #![allow(unused_braces)]
 #![allow(unexpected_cfgs)]
+#![cfg_attr(verus_keep_ghost, feature(sized_hierarchy))]
 
 // Add spec for convert traits
 pub mod convert;
 
 pub mod hw_spec;
 
+pub mod nonnull;
+
 pub mod ptr;
 
 use verus_builtin_macros::*;

verification/verify_external/src/nonnull.rs

@@ -0,0 +1,4 @@
+// SPDX-License-Identifier: MIT OR Apache-2.0
+
+#[cfg(verus_keep_ghost)]
+include!("nonnull.verus.rs");

verification/verify_external/src/nonnull.verus.rs

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT OR Apache-2.0
+use core::ptr::NonNull;
+use vstd::prelude::*;
+use vstd::raw_ptr::*;
+
+verus! {
+
+/// External type specification for core::ptr::NonNull<T>
+///
+/// We use both external_type_specification and external_body because NonNull
+/// has private fields which are not supported for transparent datatypes.
+/// This pattern is used in vstd for similar types like ManuallyDrop.
+///
+/// We use accept_recursive_types to allow types like SlabPage that have
+/// Option<NonNull<Self>> fields to be verified.
+#[allow(missing_debug_implementations)]
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::accept_recursive_types(T)]
+pub struct ExNonNull<T: core::marker::PointeeSized>(NonNull<T>);
+
+/// Specification for NonNull::as_ptr
+///
+/// Returns the underlying raw pointer. The returned pointer is guaranteed
+/// to be non-null (addr != 0).
+pub assume_specification<T: core::marker::PointeeSized>[ NonNull::<T>::as_ptr ](
+    self_: NonNull<T>,
+) -> (ret: *mut T)
+    ensures
+        ret@.addr != 0,
+    opens_invariants none
+    no_unwind
+;
+
+} // verus!