diff --git a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs index fc5f065..f5cffae 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs @@ -117,12 +117,24 @@ macro_rules! atomic_types { pub open spec fn points_to(&self, v: $value_ty) -> bool { self.view().value == v } + + #[verifier::inline] + pub open spec fn value(&self) -> $value_ty { + self.view().value + } + + #[verifier::inline] + pub open spec fn id(&self) -> AtomicCellId { + self.view().patomic + } } } }; } +pub type AtomicCellId = int; + macro_rules! atomic_common_methods { ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => { verus!{ diff --git a/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs b/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs index 17b6013..be798e5 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/pcm.rs @@ -157,7 +157,20 @@ impl Resource

{ // Operations with shared references #[verifier::external_body] - pub proof fn join_shared<'a>( + pub proof fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out: + &'a Self) + requires + self.loc() == other.loc(), + ensures + out.loc() == self.loc(), + incl(self.value(), out.value()), + incl(other.value(), out.value()), + { + unimplemented!(); + } + + #[verifier::external_body] + pub proof fn join_shared_to_target<'a>( tracked &'a self, tracked other: &'a Self, target: P, @@ -169,7 +182,7 @@ impl Resource

{ out.loc() == self.loc(), out.value() == target, { - unimplemented!(); + self.join_shared(other).weaken(target) } #[verifier::external_body] diff --git a/examples/verus-snapshot/source/vstd/source/vstd/seq.rs b/examples/verus-snapshot/source/vstd/source/vstd/seq.rs index 5461d7c..3f95960 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/seq.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/seq.rs @@ -66,12 +66,14 @@ impl Seq { /// Appends the value `a` to the end of the sequence. /// This always increases the length of the sequence by 1. + /// This often requires annotating the type of the element literal in the sequence, + /// e.g., `10int`. /// /// ## Example /// /// ```rust /// proof fn push_test() { - /// assert(seq![10, 11, 12].push(13) =~= seq![10, 11, 12, 13]); + /// assert(seq![10int, 11, 12].push(13) =~= seq![10, 11, 12, 13]); /// } /// ``` #[rustc_diagnostic_item = "verus::vstd::seq::Seq::push"] @@ -117,9 +119,9 @@ impl Seq { /// /// ```rust /// proof fn subrange_test() { - /// let s = seq![10, 11, 12, 13, 14]; - /// // ^-------^ - /// // 0 1 2 3 4 5 + /// let s = seq![10int, 11, 12, 13, 14]; + /// // ^-------^ + /// // 0 1 2 3 4 5 /// let sub = s.subrange(2, 4); /// assert(sub =~= seq![12, 13]); /// } @@ -359,7 +361,15 @@ macro_rules! seq_internal { [$($elem:expr),* $(,)?] => { $crate::vstd::seq::Seq::empty() $(.push($elem))* - } + }; + [$elem:expr; $n:expr] => { + $crate::vstd::seq::Seq::new( + $n, + $crate::vstd::prelude::closure_to_fn_spec( + |_x: _| $elem + ), + ) + }; } /// Creates a [`Seq`] containing the given elements. @@ -367,7 +377,7 @@ macro_rules! seq_internal { /// ## Example /// /// ```rust -/// let s = seq![11, 12, 13]; +/// let s = seq![11int, 12, 13]; /// /// assert(s.len() == 3); /// assert(s[0] == 11); diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs index b18a652..396dbe2 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs @@ -19,21 +19,6 @@ pub struct ExVec(Vec); #[verifier::external_body] pub struct ExGlobal(alloc::alloc::Global); -impl View for Vec { - type V = Seq; - - spec fn view(&self) -> Seq; -} - -impl DeepView for Vec { - type V = Seq; - - open spec fn deep_view(&self) -> Seq { - let v = self.view(); - Seq::new(v.len(), |i: int| v[i].deep_view()) - } -} - pub trait VecAdditionalSpecFns: View> { spec fn spec_index(&self, i: int) -> T recommends diff --git a/examples/verus-snapshot/source/vstd/source/vstd/storage_protocol.rs b/examples/verus-snapshot/source/vstd/source/vstd/storage_protocol.rs index 4a52a4d..415a4b7 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/storage_protocol.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/storage_protocol.rs @@ -14,7 +14,7 @@ broadcast use super::set::group_set_axioms, super::map::group_map_axioms; /// [_Leaf: Modularity for Temporary Sharing in Separation Logic_](https://dl.acm.org/doi/10.1145/3622798). /// /// The reference for the laws and operations we're embedding here can be found at: -/// +/// /// /// The reference version requires two monoids, the "protocol monoid" and the "base monoid". /// In this interface, we fix the base monoid to be of the form [`Map`](crate::map::Map). @@ -39,14 +39,12 @@ pub tracked struct StorageResource { pub trait Protocol: Sized { spec fn op(self, other: Self) -> Self; - /// Note that `inv`, in contrast to [`PCM::valid`](crate::pcm::PCM::valid), is not + /// Note that `rel`, in contrast to [`PCM::valid`](crate::pcm::PCM::valid), is not /// necessarily closed under inclusion. - spec fn inv(self) -> bool; + spec fn rel(self, s: Map) -> bool; spec fn unit() -> Self; - spec fn interp(self) -> Map; - proof fn commutative(a: Self, b: Self) ensures Self::op(a, b) == Self::op(b, a), @@ -61,23 +59,14 @@ pub trait Protocol: Sized { ensures Self::op(a, Self::unit()) == a, ; - // Don't need this - any Map is always valid - //proof fn inv_implies_valid(self) - // requires self.inv(), - // ensures self.interp().valid(); - } pub open spec fn incl>(a: P, b: P) -> bool { exists|c| P::op(a, c) == b } -pub open spec fn conjunct_shared>(a: P, b: P, c: P) -> bool { - forall|p: P| p.inv() && #[trigger] incl(a, p) && #[trigger] incl(b, p) ==> #[trigger] incl(c, p) -} - pub open spec fn guards>(p: P, b: Map) -> bool { - forall|q: P| #![all_triggers] P::op(p, q).inv() ==> b.submap_of(P::op(p, q).interp()) + forall|q: P, t: Map| #![all_triggers] P::rel(P::op(p, q), t) ==> b.submap_of(t) } pub open spec fn exchanges>( @@ -86,52 +75,51 @@ pub open spec fn exchanges>( p2: P, b2: Map, ) -> bool { - forall|q: P| + forall|q: P, t1: Map| #![all_triggers] - P::op(p1, q).inv() ==> P::op(p2, q).inv() && P::op(p1, q).interp().dom().disjoint(b1.dom()) - && P::op(p2, q).interp().dom().disjoint(b2.dom()) && P::op( - p1, - q, - ).interp().union_prefer_right(b1) =~= P::op(p2, q).interp().union_prefer_right(b2) + P::rel(P::op(p1, q), t1) ==> exists|t2: Map| + #![all_triggers] + P::rel(P::op(p2, q), t2) && t1.dom().disjoint(b1.dom()) && t2.dom().disjoint(b2.dom()) + && t1.union_prefer_right(b1) =~= t2.union_prefer_right(b2) } pub open spec fn exchanges_nondeterministic>( p1: P, - b1: Map, + s1: Map, new_values: Set<(P, Map)>, ) -> bool { - forall|q: P| + forall|q: P, t1: Map| #![all_triggers] - P::op(p1, q).inv() ==> exists|p2, b2| + P::rel(P::op(p1, q), t1) ==> exists|p2: P, s2: Map, t2: Map| #![all_triggers] - new_values.contains((p2, b2)) && P::op(p2, q).inv() && P::op( - p1, - q, - ).interp().dom().disjoint(b1.dom()) && P::op(p2, q).interp().dom().disjoint(b2.dom()) - && P::op(p1, q).interp().union_prefer_right(b1) =~= P::op( - p2, - q, - ).interp().union_prefer_right(b2) + new_values.contains((p2, s2)) && P::rel(P::op(p2, q), t2) && t1.dom().disjoint(s1.dom()) + && t2.dom().disjoint(s2.dom()) && t1.union_prefer_right(s1) + =~= t2.union_prefer_right(s2) } pub open spec fn deposits>(p1: P, b1: Map, p2: P) -> bool { - forall|q: P| + forall|q: P, t1: Map| #![all_triggers] - P::op(p1, q).inv() ==> P::op(p2, q).inv() && P::op(p1, q).interp().dom().disjoint(b1.dom()) - && P::op(p1, q).interp().union_prefer_right(b1) =~= P::op(p2, q).interp() + P::rel(P::op(p1, q), t1) ==> exists|t2: Map| + #![all_triggers] + P::rel(P::op(p2, q), t2) && t1.dom().disjoint(b1.dom()) && t1.union_prefer_right(b1) + =~= t2 } pub open spec fn withdraws>(p1: P, p2: P, b2: Map) -> bool { - forall|q: P| + forall|q: P, t1: Map| #![all_triggers] - P::op(p1, q).inv() ==> P::op(p2, q).inv() && P::op(p2, q).interp().dom().disjoint(b2.dom()) - && P::op(p1, q).interp() =~= P::op(p2, q).interp().union_prefer_right(b2) + P::rel(P::op(p1, q), t1) ==> exists|t2: Map| + #![all_triggers] + P::rel(P::op(p2, q), t2) && t2.dom().disjoint(b2.dom()) && t1 =~= t2.union_prefer_right( + b2, + ) } pub open spec fn updates>(p1: P, p2: P) -> bool { - forall|q: P| + forall|q: P, t1: Map| #![all_triggers] - P::op(p1, q).inv() ==> P::op(p2, q).inv() && P::op(p1, q).interp() =~= P::op(p2, q).interp() + P::rel(P::op(p1, q), t1) ==> P::rel(P::op(p2, q), t1) } pub open spec fn set_op>(s: Set<(P, Map)>, t: P) -> Set< @@ -146,35 +134,35 @@ impl> StorageResource { pub open spec fn loc(self) -> Loc; #[verifier::external_body] - pub proof fn alloc(value: P) -> (tracked out: Self) + pub proof fn alloc(p: P, tracked s: Map) -> (tracked out: Self) requires - value.inv(), + P::rel(p, s), ensures - out.value() == value, + out.value() == p, { unimplemented!(); } #[verifier::external_body] - pub proof fn join(tracked self, tracked other: Self) -> (tracked out: Self) + pub proof fn join(tracked a: Self, tracked b: Self) -> (tracked out: Self) requires - self.loc() == other.loc(), + a.loc() == b.loc(), ensures - out.loc() == self.loc(), - out.value() == P::op(self.value(), other.value()), + out.loc() == a.loc(), + out.value() == P::op(a.value(), b.value()), { unimplemented!(); } #[verifier::external_body] - pub proof fn split(tracked self, left: P, right: P) -> (tracked out: (Self, Self)) + pub proof fn split(tracked self, a_value: P, b_value: P) -> (tracked out: (Self, Self)) requires - self.value() == P::op(left, right), + self.value() == P::op(a_value, b_value), ensures out.0.loc() == self.loc(), out.1.loc() == self.loc(), - out.0.value() == left, - out.1.value() == right, + out.0.value() == a_value, + out.1.value() == b_value, { unimplemented!(); } @@ -184,9 +172,12 @@ impl> StorageResource { /// is valid if there exists another element `x` that, added to it, /// meets the invariant. #[verifier::external_body] - pub proof fn is_valid(tracked &self) -> (x: P) + pub proof fn validate(tracked a: &Self) -> (out: (P, Map)) ensures - P::op(self.value(), x).inv(), + ({ + let (q, t) = out; + P::rel(P::op(a.value(), q), t) + }), { unimplemented!(); } @@ -194,20 +185,21 @@ impl> StorageResource { // Updates and guards /// Most general kind of update, potentially depositing and withdrawing pub proof fn exchange( - tracked self, - tracked base: Map, - new_value: P, - new_base: Map, + tracked p: Self, + tracked s: Map, + new_p_value: P, + new_s_value: Map, ) -> (tracked out: (Self, Map)) requires - exchanges(self.value(), base, new_value, new_base), + exchanges(p.value(), s, new_p_value, new_s_value), ensures - out.0.loc() == self.loc(), - out.0.value() == new_value, - out.1 == new_base, + ({ + let (new_p, new_s) = out; + new_p.loc() == p.loc() && new_p.value() == new_p_value && new_s == new_s_value + }), { - let s = set![(new_value, new_base)]; - self.exchange_nondeterministic(base, s) + let se = set![(new_p_value, new_s_value)]; + Self::exchange_nondeterministic(p, s, se) } pub proof fn deposit(tracked self, tracked base: Map, new_value: P) -> (tracked out: Self) @@ -217,7 +209,7 @@ impl> StorageResource { out.loc() == self.loc(), out.value() == new_value, { - self.exchange(base, new_value, Map::empty()).0 + Self::exchange(self, base, new_value, Map::empty()).0 } pub proof fn withdraw(tracked self, new_value: P, new_base: Map) -> (tracked out: ( @@ -231,7 +223,7 @@ impl> StorageResource { out.0.value() == new_value, out.1 == new_base, { - self.exchange(Map::tracked_empty(), new_value, new_base) + Self::exchange(self, Map::tracked_empty(), new_value, new_base) } /// "Normal" update, no depositing or withdrawing @@ -242,22 +234,24 @@ impl> StorageResource { out.loc() == self.loc(), out.value() == new_value, { - self.exchange(Map::tracked_empty(), new_value, Map::empty()).0 + Self::exchange(self, Map::tracked_empty(), new_value, Map::empty()).0 } pub proof fn exchange_nondeterministic( - tracked self, - tracked base: Map, + tracked p: Self, + tracked s: Map, new_values: Set<(P, Map)>, ) -> (tracked out: (Self, Map)) requires - exchanges_nondeterministic(self.value(), base, new_values), + exchanges_nondeterministic(p.value(), s, new_values), ensures - out.0.loc() == self.loc(), - new_values.contains((out.0.value(), out.1)), + ({ + let (new_p, new_s) = out; + new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s)) + }), { - P::op_unit(self.value()); - let tracked (selff, unit) = self.split(self.value(), P::unit()); + P::op_unit(p.value()); + let tracked (selff, unit) = p.split(p.value(), P::unit()); let new_values0 = set_op(new_values, P::unit()); super::set_lib::assert_sets_equal!(new_values0, new_values, v => { P::op_unit(v.0); @@ -270,32 +264,29 @@ impl> StorageResource { assert(new_values.contains(v)); } }); - selff.exchange_nondeterministic_with_shared(&unit, base, new_values) + Self::exchange_nondeterministic_with_shared(selff, &unit, s, new_values) } #[verifier::external_body] - pub proof fn guard(tracked &self, b: Map) -> (tracked out: &Map) + pub proof fn guard(tracked p: &Self, s_value: Map) -> (tracked s: &Map) requires - guards(self.value(), b), + guards(p.value(), s_value), ensures - out == b, + s == s_value, { unimplemented!(); } // Operations with shared references #[verifier::external_body] - pub proof fn join_shared<'a>( - tracked &'a self, - tracked other: &'a Self, - target: P, - ) -> (tracked out: &'a Self) + pub proof fn join_shared<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked out: + &'a Self) requires self.loc() == other.loc(), - conjunct_shared(self.value(), other.value(), target), ensures out.loc() == self.loc(), - out.value() == target, + incl(self.value(), out.value()), + incl(other.value(), out.value()), { unimplemented!(); } @@ -312,12 +303,18 @@ impl> StorageResource { } #[verifier::external_body] - pub proof fn is_valid_2(tracked &mut self, tracked other: &Self) -> (x: P) + pub proof fn validate_with_shared(tracked p: &mut Self, tracked x: &Self) -> (res: ( + P, + Map, + )) requires - old(self).loc() == other.loc(), + old(p).loc() == x.loc(), ensures - *self == *old(self), - P::op(P::op(self.value(), other.value()), x).inv(), + *p == *old(p), + ({ + let (q, t) = res; + { P::rel(P::op(P::op(p.value(), x.value()), q), t) } + }), { unimplemented!(); } @@ -325,27 +322,22 @@ impl> StorageResource { // See `logic_exchange_with_extra_guard` // https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/protocol.v#L720 pub proof fn exchange_with_shared( - tracked self, - tracked other: &Self, - tracked base: Map, - new_value: P, - new_base: Map, + tracked p: Self, + tracked x: &Self, + tracked s: Map, + new_p_value: P, + new_s_value: Map, ) -> (tracked out: (Self, Map)) requires - self.loc() == other.loc(), - exchanges( - P::op(self.value(), other.value()), - base, - P::op(new_value, other.value()), - new_base, - ), + p.loc() == x.loc(), + exchanges(P::op(p.value(), x.value()), s, P::op(new_p_value, x.value()), new_s_value), ensures - out.0.loc() == self.loc(), - out.0.value() == new_value, - out.1 == new_base, + out.0.loc() == p.loc(), + out.0.value() == new_p_value, + out.1 == new_s_value, { - let s = set![(new_value, new_base)]; - self.exchange_nondeterministic_with_shared(other, base, s) + let se = set![(new_p_value, new_s_value)]; + Self::exchange_nondeterministic_with_shared(p, x, s, se) } // See `logic_exchange_with_extra_guard_nondeterministic` @@ -353,21 +345,23 @@ impl> StorageResource { /// Most general kind of update, potentially depositing and withdrawing #[verifier::external_body] pub proof fn exchange_nondeterministic_with_shared( - tracked self, - tracked other: &Self, - tracked base: Map, + tracked p: Self, + tracked x: &Self, + tracked s: Map, new_values: Set<(P, Map)>, ) -> (tracked out: (Self, Map)) requires - self.loc() == other.loc(), + p.loc() == x.loc(), exchanges_nondeterministic( - P::op(self.value(), other.value()), - base, - set_op(new_values, other.value()), + P::op(p.value(), x.value()), + s, + set_op(new_values, x.value()), ), ensures - out.0.loc() == self.loc(), - new_values.contains((out.0.value(), out.1)), + ({ + let (new_p, new_s) = out; + new_p.loc() == p.loc() && new_values.contains((new_p.value(), new_s)) + }), { unimplemented!(); } diff --git a/examples/verus-snapshot/source/vstd/source/vstd/view.rs b/examples/verus-snapshot/source/vstd/source/vstd/view.rs index b3347e5..5a6ae24 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/view.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/view.rs @@ -97,6 +97,43 @@ impl DeepView for alloc::sync::Arc { } } +// Note: the view for Vec is declared here, not in std_specs/vec.rs, +// because "pub mod std_specs" is marked #[cfg(verus_keep_ghost)] +// and we want to keep the View impl regardless of verus_keep_ghost. +#[cfg(all(feature = "alloc", any(verus_keep_ghost, feature = "allocator")))] +impl View for alloc::vec::Vec { + type V = Seq; + + spec fn view(&self) -> Seq; +} + +#[cfg(all(feature = "alloc", any(verus_keep_ghost, feature = "allocator")))] +impl DeepView for alloc::vec::Vec { + type V = Seq; + + open spec fn deep_view(&self) -> Seq { + let v = self.view(); + Seq::new(v.len(), |i: int| v[i].deep_view()) + } +} + +#[cfg(all(feature = "alloc", not(verus_keep_ghost), not(feature = "allocator")))] +impl View for alloc::vec::Vec { + type V = Seq; + + spec fn view(&self) -> Seq; +} + +#[cfg(all(feature = "alloc", not(verus_keep_ghost), not(feature = "allocator")))] +impl DeepView for alloc::vec::Vec { + type V = Seq; + + open spec fn deep_view(&self) -> Seq { + let v = self.view(); + Seq::new(v.len(), |i: int| v[i].deep_view()) + } +} + macro_rules! declare_identity_view { ($t:ty) => { #[cfg_attr(verus_keep_ghost, verifier::verify)] diff --git a/examples/verus-snapshot/source/vstd/source/vstd/vstd.rs b/examples/verus-snapshot/source/vstd/source/vstd/vstd.rs index 272235b..d3e335d 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/vstd.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/vstd.rs @@ -9,7 +9,7 @@ #![allow(unused_attributes)] #![allow(rustdoc::invalid_rust_codeblocks)] #![cfg_attr(verus_keep_ghost, feature(core_intrinsics))] -#![cfg_attr(verus_keep_ghost, feature(allocator_api))] +#![cfg_attr(any(verus_keep_ghost, feature = "allocator"), feature(allocator_api))] #![cfg_attr(verus_keep_ghost, feature(step_trait))] #![cfg_attr(verus_keep_ghost, feature(ptr_metadata))] #![cfg_attr(verus_keep_ghost, feature(strict_provenance))]