Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Verus snapshot update #46

Merged
merged 1 commit into from
Apr 2, 2024
Merged

Verus snapshot update #46

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 2 additions & 4 deletions examples/verus-snapshot/source/vstd/source/vstd/array.rs
View file
Open in desktop
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
124 changes: 115 additions & 9 deletions examples/verus-snapshot/source/vstd/source/vstd/invariant.rs
View file
Open in desktop
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
Open in desktop
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
Loading