Add specifications for NonZero (#2471)

Author: rikosellic

source/rust_verify_test/tests/std.rs

@@ -1604,3 +1604,45 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_fails(err, 20)
 }
+
+test_verify_one_file! {
+    #[test] nonzero verus_code! {
+
+        use vstd::prelude::*;
+        use vstd::std_specs::nonzero::*;
+        use std::num::{NonZeroU64, NonZeroI32};
+
+        fn test() {
+            let x = NonZeroI32::new(-20).unwrap();
+            assert(x@ == -20);
+
+            let x1 = x.clone();
+            assert(x1@ == -20);
+
+            let x2 = unsafe { NonZeroI32::new_unchecked(30)};
+            assert(x2@ == 30);
+
+            // assert(x1 < x2); SpecOrd is not supported.
+
+            let b = x1 < x2;
+            assert(b);
+
+            let x3 = x2.get();
+            assert(x3 == 30);
+        }
+
+        fn test_bitor() {
+            let x = NonZeroU64::new(0x1011).unwrap();
+            let y = NonZeroU64::new(0x100).unwrap();
+            let z = x | y;
+            assert(0x1011 | 0x100 == 0x1111) by (compute_only);
+            assert(z@ == 0x1111);
+
+            let z1 = x | 0x1000;
+            assert(0x1011 == 0x1011 | 0x1000) by (compute_only);
+            assert(z1@ == x@);
+            assert(z1 == x);
+        }
+
+    } => Ok(())
+}

source/vstd/std_specs/mod.rs

@@ -36,6 +36,9 @@ pub mod vecdeque;
 #[cfg(feature = "alloc")]
 pub mod smart_ptrs;
 
+#[cfg(feature = "nonzero_internals")]
+pub mod nonzero;
+
 // This struct is a hack that exists purely to create
 // a rustdoc page dedicated to 'assume_specification' specs
 pub struct VstdSpecsForRustStdLib;

source/vstd/std_specs/nonzero.rs

@@ -0,0 +1,177 @@
+use super::super::prelude::*;
+use super::cmp::{
+    OrdSpec, OrdSpecImpl, PartialEqSpec, PartialEqSpecImpl, PartialOrdSpec, PartialOrdSpecImpl,
+};
+use super::convert::FromSpecImpl;
+use super::ops::{BitOrSpec, BitOrSpecImpl};
+use core::cmp::Ordering;
+use core::num::{NonZero, ZeroablePrimitive};
+use core::ops::BitOr;
+
+verus! {
+
+#[verifier::external_trait_specification]
+#[verifier::external_trait_extension(ZeroablePrimitiveSpec via ZeroablePrimitiveSpecImpl)]
+#[verifier::external_trait_private_bound(core::num::nonzero::private::Sealed)]
+pub trait ExZeroablePrimitive: Sized + Copy {
+    type ExternalTraitSpecificationFor: ZeroablePrimitive;
+
+    spec fn is_zero(self) -> bool;
+}
+
+macro_rules! impl_zeroable_primitive_spec_impl {
+    ($($t:ty),*) => {
+        $(
+            verus! {
+                impl ZeroablePrimitiveSpecImpl for $t {
+                    open spec fn is_zero(self) -> bool {
+                        self == 0
+                    }
+                }
+            }
+        )*
+    };
+}
+
+// The implementators of `ZeroablePrimitive` coincide with `Integer`.
+impl_zeroable_primitive_spec_impl!(char, u8, u16, u32, u64, usize, i8, i16, i32, i64, isize);
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::reject_recursive_types(T)]
+pub struct ExNonZero<T: ZeroablePrimitive>(NonZero<T>);
+
+impl<T: ZeroablePrimitive> View for NonZero<T> {
+    type V = T;
+
+    uninterp spec fn view(&self) -> Self::V;
+}
+
+// Need this to define `BitOrSpecImpl`
+pub uninterp spec fn nonzero_from_primitive<T: ZeroablePrimitive>(n: T) -> NonZero<T>;
+
+pub broadcast axiom fn axiom_nonzero_from_primitive_view_eq<T: ZeroablePrimitive>(n: T)
+    requires
+        !n.is_zero(),
+    ensures
+        #[trigger] nonzero_from_primitive(n)@ == n,
+;
+
+pub broadcast axiom fn axiom_view_nonzero_from_primitive_eq<T: ZeroablePrimitive>(n: NonZero<T>)
+    ensures
+        #[trigger] nonzero_from_primitive(n@) == n,
+;
+
+pub broadcast axiom fn axiom_nonzero_is_not_zero<T: ZeroablePrimitive>(n: NonZero<T>)
+    ensures
+        !(#[trigger] n@).is_zero(),
+;
+
+pub assume_specification<T: ZeroablePrimitive>[ NonZero::<T>::new ](n: T) -> (ret: Option<
+    NonZero<T>,
+>)
+    ensures
+        match ret {
+            Some(nz) => nz@ == n && !n.is_zero(),
+            None => n.is_zero(),
+        },
+    opens_invariants none
+    no_unwind
+;
+
+pub assume_specification<T: ZeroablePrimitive>[ NonZero::<T>::new_unchecked ](n: T) -> (ret:
+    NonZero<T>)
+    requires
+        !n.is_zero(),
+    ensures
+        ret@ == n,
+    opens_invariants none
+    no_unwind
+;
+
+#[verifier::inline]
+pub open spec fn nonzero_spec_get<T: ZeroablePrimitive>(n: NonZero<T>) -> T {
+    n@
+}
+
+#[verifier::when_used_as_spec(nonzero_spec_get)]
+pub assume_specification<T: ZeroablePrimitive>[ NonZero::<T>::get ](n: NonZero<T>) -> T
+    returns
+        n@,
+    opens_invariants none
+    no_unwind
+;
+
+impl<T: ZeroablePrimitive + PartialEqSpec> PartialEqSpecImpl for NonZero<T> {
+    open spec fn obeys_eq_spec() -> bool {
+        true
+    }
+
+    open spec fn eq_spec(&self, other: &Self) -> bool {
+        self.get().eq_spec(&other.get())
+    }
+}
+
+// Ord is not implemented because of the [`Destruct`](https://doc.rust-lang.org/std/marker/trait.Destruct.html) trait bound.
+impl<T: ZeroablePrimitive + PartialOrdSpec> PartialOrdSpecImpl for NonZero<T> {
+    open spec fn obeys_partial_cmp_spec() -> bool {
+        true
+    }
+
+    open spec fn partial_cmp_spec(&self, other: &Self) -> Option<Ordering> {
+        self.get().partial_cmp_spec(&other.get())
+    }
+}
+
+impl<T: ZeroablePrimitive + BitOrSpec<Output = T>> BitOrSpecImpl<T> for NonZero<T> {
+    open spec fn obeys_bitor_spec() -> bool {
+        true
+    }
+
+    open spec fn bitor_req(self, rhs: T) -> bool {
+        self.get().bitor_req(rhs)
+    }
+
+    open spec fn bitor_spec(self, rhs: T) -> Self::Output {
+        nonzero_from_primitive(self.get().bitor_spec(rhs))
+    }
+}
+
+impl<T: ZeroablePrimitive + BitOrSpec<Output = T>> BitOrSpecImpl<NonZero<T>> for NonZero<T> {
+    open spec fn obeys_bitor_spec() -> bool {
+        true
+    }
+
+    open spec fn bitor_req(self, rhs: NonZero<T>) -> bool {
+        self.get().bitor_req(rhs.get())
+    }
+
+    open spec fn bitor_spec(self, rhs: NonZero<T>) -> Self::Output {
+        nonzero_from_primitive(self.get().bitor_spec(rhs.get()))
+    }
+}
+
+impl<T: ZeroablePrimitive> FromSpecImpl<NonZero<T>> for T {
+    open spec fn obeys_from_spec() -> bool {
+        true
+    }
+
+    open spec fn from_spec(nz: NonZero<T>) -> Self {
+        nz.get()
+    }
+}
+
+pub assume_specification<T: ZeroablePrimitive>[ <NonZero<T> as Clone>::clone ](
+    nz: &NonZero<T>,
+) -> NonZero<T>
+    returns
+        nz,
+;
+
+pub broadcast group group_nonzero_axioms {
+    axiom_nonzero_from_primitive_view_eq,
+    axiom_view_nonzero_from_primitive_eq,
+    axiom_nonzero_is_not_zero,
+}
+
+} // verus!

source/vstd/vstd.rs

@@ -21,6 +21,7 @@
 #![cfg_attr(verus_keep_ghost, feature(derive_eq_internals))]
 #![cfg_attr(verus_keep_ghost, feature(slice_index_methods))]
 #![cfg_attr(all(feature = "alloc", verus_keep_ghost), feature(liballoc_internals))]
+#![cfg_attr(verus_keep_ghost, feature(nonzero_internals))]
 
 #[cfg(feature = "alloc")]
 extern crate alloc;
@@ -145,6 +146,11 @@ pub broadcast group group_vstd_default {
     std_specs::hash::group_hash_axioms,
     #[cfg(feature = "alloc")]
     std_specs::btree::group_btree_axioms,
+    //
+    // std_specs for nonzero_internals
+    //
+    #[cfg(feature = "nonzero_internals")]
+    std_specs::nonzero::group_nonzero_axioms,
 }
 
 } // verus!

source/vstd_build/src/main.rs

@@ -140,6 +140,8 @@ fn main() {
         child_args.push("--cfg".to_string());
         child_args.push("feature=\"alloc\"".to_string());
     }
+    child_args.push("--cfg".to_string());
+    child_args.push("feature=\"nonzero_internals\"".to_string());
     child_args.push(VSTD_RS_PATH.to_string());
 
     let cmd = verus_target_path.join("rust_verify");