Introduce zero-varaint enum through external_type_specification

Author: rikosellic

ostd/src/sync/guard.rs

@@ -12,20 +12,19 @@ use crate::{
 #[verus_verify]
 pub trait SpinGuardian {
     /// The guard type for holding a spin lock or a spin-based write lock.
-    //type Guard: AsAtomicModeGuard + GuardTransfer;
-    type Guard;
+    type Guard: /*AsAtomicModeGuard + */GuardTransfer;
     /// The guard type for holding a spin-based read lock.
-    //type ReadGuard: AsAtomicModeGuard + GuardTransfer;
-    type ReadGuard;
+    type ReadGuard: /*AsAtomicModeGuard +*/GuardTransfer;
 
     /// Creates a new guard.
     fn guard() -> Self::Guard;
     /// Creates a new read guard.
     fn read_guard() -> Self::ReadGuard;
 }
 
-/*
+
 /// The Guard can be transferred atomically.
+#[verus_verify]
 pub trait GuardTransfer {
     /// Atomically transfers the current guard to a new instance.
     ///
@@ -35,13 +34,16 @@ pub trait GuardTransfer {
     /// The original guard must be dropped immediately after calling this method.
     fn transfer_to(&mut self) -> Self;
 }
-*/
-/// A guardian that disables preemption while holding a lock.
-#[verus_verify]
-// pub enum PreemptDisabled {}
-pub struct PreemptDisabled;
 
+/// A guardian that disables preemption while holding a lock.
 #[verifier::external]
+pub enum PreemptDisabled {}
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExPreemptDisabled(PreemptDisabled);
+
+#[verus_verify]
 impl SpinGuardian for PreemptDisabled {
     type Guard = DisabledPreemptGuard;
     type ReadGuard = DisabledPreemptGuard;
@@ -63,7 +65,13 @@ impl SpinGuardian for PreemptDisabled {
 /// IRQ handlers are allowed to get executed while holding the
 /// lock. For example, if a lock is never used in the interrupt
 /// context, then it is ok not to use this guardian in the process context.
+#[verifier::external]
 pub enum LocalIrqDisabled {}
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExLocalIrqDisabled(LocalIrqDisabled);
+
 /*
 impl SpinGuardian for LocalIrqDisabled {
     type Guard = DisabledLocalIrqGuard;

ostd/src/sync/mod.rs

@@ -10,10 +10,7 @@ mod spin;
 mod wait;
 //pub(crate) use self::rcu::finish_grace_period;
 pub use self::{
-    guard::{
-        /*GuardTransfer,*/
-        LocalIrqDisabled, PreemptDisabled, /*SpinGuardian, WriteIrqDisabled*/
-    },
+    guard::{GuardTransfer, LocalIrqDisabled, PreemptDisabled, SpinGuardian, /*WriteIrqDisabled*/},
     //mutex::{ArcMutexGuard, Mutex, MutexGuard},
     rcu::{non_null /*, Rcu, RcuDrop, RcuOption, RcuOptionReadGuard, RcuReadGuard*/},
     rwarc::{RoArc, RwArc},

ostd/src/sync/rwlock.rs

@@ -21,8 +21,8 @@ use core::{
 };
 
 use super::{
-    guard::{/*GuardTransfer,*/ SpinGuardian},
-    //PreemptDisabled,
+    PreemptDisabled,
+    guard::{GuardTransfer, SpinGuardian},
 };
 //use crate::task::atomic_mode::AsAtomicModeGuard;
 
@@ -170,7 +170,7 @@ struct_with_invariants! {
 /// ```
 ///
 /// [`SpinLock`]: super::SpinLock
-pub struct RwLock<T  /* : ?Sized*/ , Guard  /* = PreemptDisabled*/ > {
+pub struct RwLock<T  /* : ?Sized*/ , Guard /* = PreemptDisabled*/ > {
     guard: PhantomData<Guard>,
     /// The internal representation of the lock state is as follows:
     /// - **Bit 63:** Writer lock.

ostd/src/task/preempt/guard.rs

@@ -1,13 +1,13 @@
 // SPDX-License-Identifier: MPL-2.0
 use vstd::prelude::*;
 
-// use crate::{sync::GuardTransfer, task::atomic_mode::InAtomicMode};
+use crate::{sync::GuardTransfer/*, task::atomic_mode::InAtomicMode*/};
 
 /// A guard for disable preempt.
+#[verus_verify]
 #[clippy::has_significant_drop]
 #[must_use]
 #[derive(Debug)]
-#[verus_verify]
 pub struct DisabledPreemptGuard {
     // This private field prevents user from constructing values of this type directly.
     _private: (),
@@ -25,13 +25,16 @@ impl DisabledPreemptGuard {
         Self { _private: () }
     }
 }
-
+*/
+#[verus_verify]
 impl GuardTransfer for DisabledPreemptGuard {
+    #[verifier::external_body]
     fn transfer_to(&mut self) -> Self {
         disable_preempt()
     }
 }
 
+/*
 impl Drop for DisabledPreemptGuard {
     fn drop(&mut self) {
         super::cpu_local::dec_guard_count();