Skip to content

Commit

Permalink
chore: update to latest Verus snapshot
Browse files Browse the repository at this point in the history
  • Loading branch information
@jaybosamiya @github-actions
jaybosamiya authored and github-actions[bot] committed Apr 1, 2024
1 parent ddcaf3b commit 210a29c
Show file tree
Hide file tree
Showing 17 changed files with 233 additions and 264 deletions.
6 changes: 2 additions & 4 deletions examples/verus-snapshot/source/vstd/source/vstd/array.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,7 @@ pub exec fn array_index_get<T, const N: usize>(ar: &[T; N], i: usize) -> (out: &
}

#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn array_len_matches_n<T, const N: usize>(ar: &[T; N])
pub broadcast proof fn array_len_matches_n<T, const N: usize>(ar: &[T; N])
ensures
(#[trigger] ar@.len()) == N,
{
Expand All @@ -69,8 +68,7 @@ pub open spec fn array_index<T, const N: usize>(ar: &[T; N], i: int) -> T {
pub open spec fn spec_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T]);

#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
pub broadcast proof fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
ensures
(#[trigger] spec_array_as_slice(ar))@ == ar@,
{
Expand Down
8 changes: 1 addition & 7 deletions examples/verus-snapshot/source/vstd/source/vstd/atomic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -471,13 +471,7 @@ macro_rules! atomic_bool_methods {
};
}

make_bool_atomic!(
PAtomicBool,
PermissionBool,
PermissionDataBool,
AtomicBool,
bool
);
make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool);

make_unsigned_integer_atomic!(
PAtomicU8,
Expand Down
26 changes: 4 additions & 22 deletions examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,33 +114,15 @@ 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
);
declare_atomic_type!(AtomicUsize, PAtomicUsize, PermissionUsize, usize, AtomicPredUsize);

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);
declare_atomic_type!(
AtomicIsize,
PAtomicIsize,
PermissionIsize,
isize,
AtomicPredIsize
);

declare_atomic_type!(
AtomicBool,
PAtomicBool,
PermissionBool,
bool,
AtomicPredBool
);
declare_atomic_type!(AtomicIsize, PAtomicIsize, PermissionIsize, isize, AtomicPredIsize);

declare_atomic_type!(AtomicBool, PAtomicBool, PermissionBool, bool, AtomicPredBool);

/// Performs a given atomic operation on a given atomic
/// while providing access to its ghost state.
Expand Down
124 changes: 115 additions & 9 deletions examples/verus-snapshot/source/vstd/source/vstd/invariant.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -233,6 +233,57 @@ declare_invariant_impl!(LocalInvariant);
#[cfg_attr(verus_keep_ghost, verifier::proof)]
pub struct InvariantBlockGuard;

// In the "Logical Paradoxes" section of the Iris 4.1 Reference
// (`https://plv.mpi-sws.org/iris/appendix-4.1.pdf`), they show that
// opening invariants carries the risk of unsoundness. One solution to
// this, described in the paper "Later Credits: Resourceful Reasoning
// for the Later Modality" by Spies et al. (available at
// `https://plv.mpi-sws.org/later-credits/paper-later-credits.pdf`) is
// to use "later credits". That is, require the expenditure of a later
// credit, only obtainable in exec mode, when opening an invariant. So
// we require the relinquishment of a tracked
// `OpenInvariantCredit` to open an invariant, and we provide an
// exec-mode function `create_open_invariant_credit` to obtain one.

verus! {

#[doc(hidden)]
#[cfg_attr(verus_keep_ghost, verifier::proof)]
#[verifier::external_body]
pub struct OpenInvariantCredit {}

// It's intentional that `create_open_invariant_credit` uses `exec` mode. This prevents
// creation of an infinite number of credits to open invariants infinitely often.
#[cfg(verus_keep_ghost)]
#[rustc_diagnostic_item = "verus::vstd::invariant::create_open_invariant_credit"]
#[verifier::external_body]
#[inline(always)]
pub fn create_open_invariant_credit() -> Tracked<OpenInvariantCredit>
opens_invariants none
{
Tracked::<OpenInvariantCredit>::assume_new()
}

#[cfg(verus_keep_ghost)]
#[rustc_diagnostic_item = "verus::vstd::invariant::spend_open_invariant_credit_in_proof"]
#[doc(hidden)]
#[inline(always)]
pub proof fn spend_open_invariant_credit_in_proof(tracked credit: OpenInvariantCredit) {
}

#[cfg(verus_keep_ghost)]
#[rustc_diagnostic_item = "verus::vstd::invariant::spend_open_invariant_credit"]
#[doc(hidden)]
#[inline(always)]
pub fn spend_open_invariant_credit(credit: Tracked<OpenInvariantCredit>)
opens_invariants none
{
proof {
spend_open_invariant_credit_in_proof(credit.get());
}
}

} // verus!
// NOTE: These 3 methods are removed in the conversion to VIR; they are only used
// for encoding and borrow-checking.
// In the VIR these are all replaced by the OpenInvariant block.
Expand All @@ -250,7 +301,6 @@ pub struct InvariantBlockGuard;
//
// The purpose of the `guard` object, used below, is to ensure the borrow on `i` will
// last the entire block.

#[cfg(verus_keep_ghost)]
#[rustc_diagnostic_item = "verus::vstd::invariant::open_atomic_invariant_begin"]
#[doc(hidden)]
Expand Down Expand Up @@ -317,32 +367,60 @@ pub fn open_invariant_end<V>(_guard: &InvariantBlockGuard, _v: V) {
/// **Note:** Rather than using `open_atomic_invariant!` directly, we generally recommend
/// using the [`atomic_ghost` APIs](crate::atomic_ghost).
///
/// It's not legal to use `open_atomic_invariant!` in proof mode. In proof mode, you need
/// to use `open_atomic_invariant_in_proof!` instead. This takes one extra parameter,
/// an open-invariant credit, which you can get by calling
/// `create_open_invariant_credit()` before you enter proof mode.
/// ### Example
///
/// TODO fill this in
// TODO the first argument here should be macro'ed in ghost context, not exec
// TODO the `$eexpr` argument here should be macro'ed in ghost context, not exec

#[macro_export]
macro_rules! open_atomic_invariant {
[$($tail:tt)*] => {
::builtin_macros::verus_exec_inv_macro_exprs!($crate::invariant::open_atomic_invariant_internal!($($tail)*))
#[cfg(verus_keep_ghost_body)]
let credit = $crate::invariant::create_open_invariant_credit();
::builtin_macros::verus_exec_inv_macro_exprs!(
$crate::invariant::open_atomic_invariant_internal!(credit => $($tail)*)
)
};
}

#[macro_export]
macro_rules! open_atomic_invariant_in_proof {
[$($tail:tt)*] => {
::builtin_macros::verus_ghost_inv_macro_exprs!($crate::invariant::open_atomic_invariant_internal!($($tail)*))
::builtin_macros::verus_ghost_inv_macro_exprs!($crate::invariant::open_atomic_invariant_in_proof_internal!($($tail)*))
};
}

#[macro_export]
macro_rules! open_atomic_invariant_internal {
($eexpr:expr => $iident:ident => $bblock:block) => {
($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => {
#[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ {
#[cfg(verus_keep_ghost_body)]
$crate::invariant::spend_open_invariant_credit($credit_expr);
#[cfg(verus_keep_ghost_body)]
#[allow(unused_mut)] let (guard, mut $iident) =
$crate::invariant::open_atomic_invariant_begin($eexpr);
$bblock
#[cfg(verus_keep_ghost_body)]
$crate::invariant::open_invariant_end(guard, $iident);
}
}
}

#[macro_export]
macro_rules! open_atomic_invariant_in_proof_internal {
($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => {
#[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ {
#[cfg(verus_keep_ghost_body)]
#[allow(unused_mut)] let (guard, mut $iident) = $crate::invariant::open_atomic_invariant_begin($eexpr);
$crate::invariant::spend_open_invariant_credit_in_proof($credit_expr);
#[cfg(verus_keep_ghost_body)]
#[allow(unused_mut)] let (guard, mut $iident) =
$crate::invariant::open_atomic_invariant_begin($eexpr);
$bblock
#[cfg(verus_keep_ghost_body)]
$crate::invariant::open_invariant_end(guard, $iident);
Expand All @@ -353,6 +431,8 @@ macro_rules! open_atomic_invariant_internal {
pub use open_atomic_invariant;
pub use open_atomic_invariant_in_proof;
#[doc(hidden)]
pub use open_atomic_invariant_in_proof_internal;
#[doc(hidden)]
pub use open_atomic_invariant_internal;

/// Macro used to temporarily "open" a [`LocalInvariant`] object, obtaining the stored
Expand Down Expand Up @@ -439,6 +519,11 @@ pub use open_atomic_invariant_internal;
/// The default for an `exec`-mode function is to open any, while the default
/// for a `proof`-mode function is to open none.
///
/// It's not legal to use `open_local_invariant!` in proof mode. In proof mode, you need
/// to use `open_local_invariant_in_proof!` instead. This takes one extra parameter,
/// an open-invariant credit, which you can get by calling
/// `create_open_invariant_credit()` before you enter proof mode.
///
/// ### Example
///
/// TODO fill this in
Expand All @@ -450,22 +535,41 @@ pub use open_atomic_invariant_internal;
#[macro_export]
macro_rules! open_local_invariant {
[$($tail:tt)*] => {
#[cfg(verus_keep_ghost_body)]
let credit = $crate::invariant::create_open_invariant_credit();
::builtin_macros::verus_exec_inv_macro_exprs!(
$crate::invariant::open_local_invariant_internal!($($tail)*))
$crate::invariant::open_local_invariant_internal!(credit => $($tail)*))
};
}

#[macro_export]
macro_rules! open_local_invariant_in_proof {
[$($tail:tt)*] => {
::builtin_macros::verus_ghost_inv_macro_exprs!($crate::invariant::open_local_invariant_internal!($($tail)*))
::builtin_macros::verus_ghost_inv_macro_exprs!($crate::invariant::open_local_invariant_in_proof_internal!($($tail)*))
};
}

#[macro_export]
macro_rules! open_local_invariant_internal {
($eexpr:expr => $iident:ident => $bblock:block) => {
($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => {
#[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ {
#[cfg(verus_keep_ghost_body)]
$crate::invariant::spend_open_invariant_credit($credit_expr);
#[cfg(verus_keep_ghost_body)]
#[allow(unused_mut)] let (guard, mut $iident) = $crate::invariant::open_local_invariant_begin($eexpr);
$bblock
#[cfg(verus_keep_ghost_body)]
$crate::invariant::open_invariant_end(guard, $iident);
}
}
}

#[macro_export]
macro_rules! open_local_invariant_in_proof_internal {
($credit_expr:expr => $eexpr:expr => $iident:ident => $bblock:block) => {
#[cfg_attr(verus_keep_ghost, verifier::invariant_block)] /* vattr */ {
#[cfg(verus_keep_ghost_body)]
$crate::invariant::spend_open_invariant_credit_in_proof($credit_expr);
#[cfg(verus_keep_ghost_body)]
#[allow(unused_mut)] let (guard, mut $iident) = $crate::invariant::open_local_invariant_begin($eexpr);
$bblock
Expand All @@ -478,4 +582,6 @@ macro_rules! open_local_invariant_internal {
pub use open_local_invariant;
pub use open_local_invariant_in_proof;
#[doc(hidden)]
pub use open_local_invariant_in_proof_internal;
#[doc(hidden)]
pub use open_local_invariant_internal;
33 changes: 11 additions & 22 deletions examples/verus-snapshot/source/vstd/source/vstd/map.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,8 +189,7 @@ impl<K, V> Map<K, V> {
// Trusted axioms
/* REVIEW: this is simpler than the two separate axioms below -- would this be ok?
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_index_decreases<K, V>(m: Map<K, V>, key: K)
pub broadcast proof fn axiom_map_index_decreases<K, V>(m: Map<K, V>, key: K)
requires
m.dom().contains(key),
ensures
Expand All @@ -200,8 +199,7 @@ pub proof fn axiom_map_index_decreases<K, V>(m: Map<K, V>, key: K)
*/

#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, key: K)
pub broadcast proof fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, key: K)
requires
m.dom().finite(),
m.dom().contains(key),
Expand All @@ -213,8 +211,7 @@ pub proof fn axiom_map_index_decreases_finite<K, V>(m: Map<K, V>, key: K)
// REVIEW: this is currently a special case that is hard-wired into the verifier
// It implements a version of https://github.com/FStarLang/FStar/pull/2954 .
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_index_decreases_infinite<K, V>(m: Map<K, V>, key: K)
pub broadcast proof fn axiom_map_index_decreases_infinite<K, V>(m: Map<K, V>, key: K)
requires
m.dom().contains(key),
ensures
Expand All @@ -224,8 +221,7 @@ pub proof fn axiom_map_index_decreases_infinite<K, V>(m: Map<K, V>, key: K)

/// The domain of the empty map is the empty set
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_empty<K, V>()
pub broadcast proof fn axiom_map_empty<K, V>()
ensures
#[trigger] Map::<K, V>::empty().dom() == Set::<K>::empty(),
{
Expand All @@ -234,26 +230,23 @@ pub proof fn axiom_map_empty<K, V>()
/// The domain of a map after inserting a key-value pair is equivalent to inserting the key into
/// the original map's domain set.
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_insert_domain<K, V>(m: Map<K, V>, key: K, value: V)
pub broadcast proof fn axiom_map_insert_domain<K, V>(m: Map<K, V>, key: K, value: V)
ensures
#[trigger] m.insert(key, value).dom() == m.dom().insert(key),
{
}

/// Inserting `value` at `key` in `m` results in a map that maps `key` to `value`
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_insert_same<K, V>(m: Map<K, V>, key: K, value: V)
pub broadcast proof fn axiom_map_insert_same<K, V>(m: Map<K, V>, key: K, value: V)
ensures
#[trigger] m.insert(key, value)[key] == value,
{
}

/// Inserting `value` at `key2` does not change the value mapped to by any other keys in `m`
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_insert_different<K, V>(m: Map<K, V>, key1: K, key2: K, value: V)
pub broadcast proof fn axiom_map_insert_different<K, V>(m: Map<K, V>, key1: K, key2: K, value: V)
requires
m.dom().contains(key1),
key1 != key2,
Expand All @@ -265,8 +258,7 @@ pub proof fn axiom_map_insert_different<K, V>(m: Map<K, V>, key1: K, key2: K, va
/// The domain of a map after removing a key-value pair is equivalent to removing the key from
/// the original map's domain set.
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_remove_domain<K, V>(m: Map<K, V>, key: K)
pub broadcast proof fn axiom_map_remove_domain<K, V>(m: Map<K, V>, key: K)
ensures
#[trigger] m.remove(key).dom() == m.dom().remove(key),
{
Expand All @@ -275,8 +267,7 @@ pub proof fn axiom_map_remove_domain<K, V>(m: Map<K, V>, key: K)
/// Removing a key-value pair from a map does not change the value mapped to by
/// any other keys in the map.
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)
pub broadcast proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)
requires
m.dom().contains(key1),
key1 != key2,
Expand All @@ -287,8 +278,7 @@ pub proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)

/// Two maps are equivalent if their domains are equivalent and every key in their domains map to the same value.
#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>)
pub broadcast proof fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>)
ensures
#[trigger] (m1 =~= m2) <==> {
&&& m1.dom() =~= m2.dom()
Expand All @@ -298,8 +288,7 @@ pub proof fn axiom_map_ext_equal<K, V>(m1: Map<K, V>, m2: Map<K, V>)
}

#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>)
pub broadcast proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>)
ensures
#[trigger] (m1 =~~= m2) <==> {
&&& m1.dom() =~~= m2.dom()
Expand Down
Loading

0 comments on commit 210a29c

Please sign in to comment.