Verus snapshot update (#110)

Automated verus snapshot update by GitHub Actions.

examples/verus-snapshot/source/vstd/atomic.rs

@@ -1,10 +1,13 @@
 #![allow(unused_imports)]
 
 use core::sync::atomic::{
-    AtomicBool, AtomicI16, AtomicI32, AtomicI64, AtomicI8, AtomicIsize, AtomicPtr, AtomicU16,
-    AtomicU32, AtomicU64, AtomicU8, AtomicUsize, Ordering,
+    AtomicBool, AtomicI16, AtomicI32, AtomicI8, AtomicIsize, AtomicPtr, AtomicU16, AtomicU32,
+    AtomicU8, AtomicUsize, Ordering,
 };
 
+#[cfg(target_has_atomic = "64")]
+use core::sync::atomic::{AtomicI64, AtomicU64};
+
 use super::modes::*;
 use super::pervasive::*;
 use super::prelude::*;
@@ -582,6 +585,8 @@ make_unsigned_integer_atomic!(
     wrapping_add_u32,
     wrapping_sub_u32
 );
+
+#[cfg(target_has_atomic = "64")]
 make_unsigned_integer_atomic!(
     PAtomicU64,
     PermissionU64,
@@ -628,6 +633,8 @@ make_signed_integer_atomic!(
     wrapping_add_i32,
     wrapping_sub_i32
 );
+
+#[cfg(target_has_atomic = "64")]
 make_signed_integer_atomic!(
     PAtomicI64,
     PermissionI64,

examples/verus-snapshot/source/vstd/atomic_ghost.rs

@@ -191,13 +191,17 @@ macro_rules! declare_atomic_type_generic {
     };
 }
 
+#[cfg(target_has_atomic = "64")]
 declare_atomic_type!(AtomicU64, PAtomicU64, PermissionU64, u64, AtomicPredU64);
+
 declare_atomic_type!(AtomicU32, PAtomicU32, PermissionU32, u32, AtomicPredU32);
 declare_atomic_type!(AtomicU16, PAtomicU16, PermissionU16, u16, AtomicPredU16);
 declare_atomic_type!(AtomicU8, PAtomicU8, PermissionU8, u8, AtomicPredU8);
 declare_atomic_type!(AtomicUsize, PAtomicUsize, PermissionUsize, usize, AtomicPredUsize);
 
+#[cfg(target_has_atomic = "64")]
 declare_atomic_type!(AtomicI64, PAtomicI64, PermissionI64, i64, AtomicPredI64);
+
 declare_atomic_type!(AtomicI32, PAtomicI32, PermissionI32, i32, AtomicPredI32);
 declare_atomic_type!(AtomicI16, PAtomicI16, PermissionI16, i16, AtomicPredI16);
 declare_atomic_type!(AtomicI8, PAtomicI8, PermissionI8, i8, AtomicPredI8);

examples/verus-snapshot/source/vstd/std_specs/option.rs

@@ -188,4 +188,22 @@ pub fn ex_option_clone<T: Clone>(opt: &Option<T>) -> (res: Option<T>)
     opt.clone()
 }
 
+// ok_or
+#[verifier::inline]
+pub open spec fn spec_ok_or<T, E>(option: Option<T>, err: E) -> Result<T, E> {
+    match option {
+        Some(t) => Ok(t),
+        None => Err(err),
+    }
+}
+
+#[verifier::external_fn_specification]
+#[verifier::when_used_as_spec(spec_ok_or)]
+pub fn ex_ok_or<T, E>(option: Option<T>, err: E) -> (res: Result<T, E>)
+    ensures
+        res == spec_ok_or(option, err),
+{
+    option.ok_or(err)
+}
+
 } // verus!