From 5ef3aca2c38c04e07c35ce887b5b605b88bf1b36 Mon Sep 17 00:00:00 2001
From: jaybosamiya <5683582+jaybosamiya@users.noreply.github.com>
Date: Wed, 1 Jan 2025 01:09:05 +0000
Subject: [PATCH] chore: update to latest Verus snapshot

---
 examples/verus-snapshot/source/vstd/atomic.rs  | 11 +++++++++--
 .../verus-snapshot/source/vstd/atomic_ghost.rs |  4 ++++
 .../source/vstd/std_specs/option.rs            | 18 ++++++++++++++++++
 3 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/examples/verus-snapshot/source/vstd/atomic.rs b/examples/verus-snapshot/source/vstd/atomic.rs
index e64a9c4..f456bc5 100644
--- a/examples/verus-snapshot/source/vstd/atomic.rs
+++ b/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,
diff --git a/examples/verus-snapshot/source/vstd/atomic_ghost.rs b/examples/verus-snapshot/source/vstd/atomic_ghost.rs
index 21a427b..c47c29f 100644
--- a/examples/verus-snapshot/source/vstd/atomic_ghost.rs
+++ b/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);
diff --git a/examples/verus-snapshot/source/vstd/std_specs/option.rs b/examples/verus-snapshot/source/vstd/std_specs/option.rs
index ca21775..c7d3f9d 100644
--- a/examples/verus-snapshot/source/vstd/std_specs/option.rs
+++ b/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!