diff --git a/examples/pcm/agreement.rs b/examples/pcm/agreement.rs deleted file mode 100644 index 7d174d7ea4..0000000000 --- a/examples/pcm/agreement.rs +++ /dev/null @@ -1,175 +0,0 @@ -//! This file implements agreement on a constant value using a custom -//! resource algebra. -//! -//! An agreement resource constitutes knowledge of a constant value. -//! To create an instance of a constant value of type `T`, use -//! `AgreementResource::::alloc()` as in the following example: -//! -//! ``` -//! let tracked r1 = AgreementResource::::alloc(72); -//! assert(r1@ == 72); -//! ``` -//! -//! Knowledge of a constant value can be duplicated with `duplicate`, -//! which creates another agreement resource with the same constant -//! value and the same ID. Here's an example: -//! -//! ``` -//! let tracked r2 = r1.duplicate(); -//! assert(r2.id() == r1.id()); -//! assert(r2@ == r1@); -//! ``` -//! -//! Any two agreement resources with the same `id()` are guaranteed to -//! have equal values. You can establish this by calling -//! `lemma_agreement`, as in the following example: -//! -//! ``` -//! assert(r2.id() == r1.id()); -//! proof { r1.lemma_agreement(&mut r2); } -//! assert(r2@ == r1@); -//! ``` -#![allow(unused_imports)] -use std::result::*; -use verus_builtin::*; -use verus_builtin_macros::*; -use vstd::prelude::*; -use vstd::resource; -use vstd::resource::algebra::ResourceAlgebra; -use vstd::resource::pcm::Resource; -use vstd::resource::pcm::PCM; -use vstd::resource::Loc; - -verus! { - -pub enum AgreementResourceValue { - Empty, - Chosen { c: T }, - Invalid, -} - -impl AgreementResourceValue { - pub open spec fn new(c: T) -> Self { - AgreementResourceValue::::Chosen { c } - } -} - -impl ResourceAlgebra for AgreementResourceValue { - open spec fn valid(self) -> bool { - !(self is Invalid) - } - - open spec fn op(a: Self, b: Self) -> Self { - match (a, b) { - (AgreementResourceValue::::Empty, _) => b, - (_, AgreementResourceValue::::Empty) => a, - (AgreementResourceValue::::Invalid, _) => AgreementResourceValue::::Invalid { }, - (_, AgreementResourceValue::::Invalid) => AgreementResourceValue::::Invalid { }, - ( - AgreementResourceValue::::Chosen { c: c1 }, - AgreementResourceValue::::Chosen { c: c2 }, - ) => if c1 == c2 { - a - } else { - AgreementResourceValue::::Invalid { } - }, - } - } - - proof fn valid_op(a: Self, b: Self) { - } - - proof fn commutative(a: Self, b: Self) { - } - - proof fn associative(a: Self, b: Self, c: Self) { - } -} - - -impl PCM for AgreementResourceValue { - open spec fn unit() -> Self { - AgreementResourceValue::::Empty { } - } - - proof fn op_unit(self) { - } - - proof fn unit_valid() { - } -} - -pub struct AgreementResource { - r: Resource>, -} - -impl AgreementResource { - pub closed spec fn inv(self) -> bool { - self.r.value() is Chosen - } - - pub closed spec fn id(self) -> Loc { - self.r.loc() - } - - pub closed spec fn view(self) -> T - recommends - self.inv(), - { - self.r.value()->c - } - - pub proof fn alloc(c: T) -> (tracked result: AgreementResource) - ensures - result.inv(), - result@ == c, - { - let r_value = AgreementResourceValue::::new(c); - let tracked r = Resource::>::alloc(r_value); - AgreementResource:: { r } - } - - pub proof fn duplicate(tracked self: &mut AgreementResource) -> (tracked result: - AgreementResource) - requires - old(self).inv(), - ensures - final(self).inv(), - result.inv(), - final(self).id() == old(self).id(), - result.id() == old(self).id(), - final(self)@ == result@, - final(self)@ == old(self)@, - { - let tracked r = resource::duplicate(&self.r); - AgreementResource:: { r } - } - - pub proof fn lemma_agreement( - tracked self: &mut AgreementResource, - tracked other: &AgreementResource, - ) - requires - old(self).inv(), - other.inv(), - old(self).id() == other.id(), - ensures - final(self).id() == old(self).id(), - final(self)@ == old(self)@, - final(self)@ == other@, - { - self.r.validate_2(&other.r); - } -} - -pub fn main() { - let tracked r1 = AgreementResource::::alloc(72); - assert(r1@ == 72); - let tracked r2 = r1.duplicate(); - assert(r2@ == r1@); - proof { - r1.lemma_agreement(&mut r2); - } -} - -} // verus! diff --git a/examples/resource/agreement.rs b/examples/resource/agreement.rs new file mode 100644 index 0000000000..6b0dc37537 --- /dev/null +++ b/examples/resource/agreement.rs @@ -0,0 +1,101 @@ +//! This file implements agreement on a constant value using a custom +//! resource algebra. +//! +//! An agreement resource constitutes knowledge of a constant value. +//! To create an instance of a constant value of type `T`, use +//! `AgreementResource::::alloc()` as in the following example: +//! +//! ``` +//! let tracked r1 = AgreementResource::::alloc(72); +//! assert(r1@ == 72); +//! ``` +//! +//! Knowledge of a constant value can be duplicated with `duplicate`, +//! which creates another agreement resource with the same constant +//! value and the same ID. Here's an example: +//! +//! ``` +//! let tracked r2 = r1.duplicate(); +//! assert(r2.loc() == r1.loc()); +//! assert(r2@ == r1@); +//! ``` +//! +//! Any two agreement resources with the same `loc()` are guaranteed to +//! have equal values. You can establish this by calling +//! `lemma_agreement`, as in the following example: +//! +//! ``` +//! assert(r2.loc() == r1.loc()); +//! proof { r1.lemma_agreement(&mut r2); } +//! assert(r2@ == r1@); +//! ``` +#![allow(unused_imports)] +use std::result::*; +use verus_builtin::*; +use verus_builtin_macros::*; +use vstd::prelude::*; +use vstd::resource; +use vstd::resource::agree::lemma_agree; +use vstd::resource::agree::AgreementRA; +use vstd::resource::algebra::Resource; +use vstd::resource::algebra::ResourceAlgebra; +use vstd::resource::Loc; + +verus! { + +pub struct AgreementResource { + r: Resource>, +} + +impl AgreementResource { + pub closed spec fn loc(self) -> Loc { + self.r.loc() + } + + pub closed spec fn view(self) -> T + { + self.r.value()@ + } + + pub proof fn alloc(c: T) -> (tracked result: AgreementResource) + ensures + result@ == c, + { + let carrier = AgreementRA::Agree(c); + let tracked r = Resource::alloc(carrier); + AgreementResource:: { r } + } + + pub proof fn duplicate(tracked self: &AgreementResource) -> (tracked result: AgreementResource) + ensures + result.loc() == self.loc(), + self@ == result@, + { + let tracked r = self.r.duplicate_previous(self.r.value()); + AgreementResource:: { r } + } + + pub proof fn lemma_agreement( + tracked self: &AgreementResource, + tracked other: &AgreementResource, + ) + requires + self.loc() == other.loc(), + ensures + self@ == other@, + { + lemma_agree(&self.r, &other.r); + } +} + +pub fn main() { + let tracked r1 = AgreementResource::::alloc(72); + assert(r1@ == 72); + let tracked r2 = r1.duplicate(); + assert(r2@ == r1@); + proof { + r1.lemma_agreement(&mut r2); + } +} + +} // verus! diff --git a/examples/pcm/count_to_two.rs b/examples/resource/count_to_two.rs similarity index 100% rename from examples/pcm/count_to_two.rs rename to examples/resource/count_to_two.rs diff --git a/examples/pcm/log.rs b/examples/resource/log.rs similarity index 99% rename from examples/pcm/log.rs rename to examples/resource/log.rs index cf7bfbbe1f..0c3ed03cf8 100644 --- a/examples/pcm/log.rs +++ b/examples/resource/log.rs @@ -238,7 +238,7 @@ impl LogResource { ensures final(self)@ is HalfAuthority, final(self).id() == old(self).id(), - final(other).id() == old(self).id(), + final(other).id() == old(other).id(), final(self)@.log() == old(self)@.log() + seq![v], final(other)@ == final(self)@, { diff --git a/examples/pcm/monotonic_counter.rs b/examples/resource/monotonic_counter.rs similarity index 99% rename from examples/pcm/monotonic_counter.rs rename to examples/resource/monotonic_counter.rs index 6c97c702f3..0be8e62946 100644 --- a/examples/pcm/monotonic_counter.rs +++ b/examples/resource/monotonic_counter.rs @@ -285,8 +285,8 @@ impl MonotonicCounterResource { ensures old(self)@ == old(other)@, final(self).id() == old(self).id(), - final(other).id() == old(self).id(), - final(other)@ == final(self)@, + final(other).id() == old(other).id(), + final(self)@ == final(other)@, final(self)@ == (MonotonicCounterResourceValue::HalfRightToAdvance { value: old(self)@->HalfRightToAdvance_value + 1, }), diff --git a/examples/pcm/oneshot.rs b/examples/resource/oneshot.rs similarity index 55% rename from examples/pcm/oneshot.rs rename to examples/resource/oneshot.rs index 2a9db49e19..94db46d55d 100644 --- a/examples/pcm/oneshot.rs +++ b/examples/resource/oneshot.rs @@ -69,26 +69,30 @@ use verus_builtin::*; use verus_builtin_macros::*; use vstd::prelude::*; use vstd::resource; +use vstd::resource::agree::AgreementRA; +use vstd::resource::algebra; use vstd::resource::algebra::ResourceAlgebra; -use vstd::resource::pcm::Resource; +use vstd::resource::frac::FractionRA; +use vstd::resource::pcm; use vstd::resource::pcm::PCM; +use vstd::resource::product::ProductRA; use vstd::resource::update_and_redistribute; use vstd::resource::update_mut; use vstd::resource::Loc; verus! { -// A one-shot resource represents one of the following four resources: -// -// `FullRightToComplete` -- the authority to complete the one-shot; -// -// `HalfRightToComplete` -- half of the authority to complete the -// one-shot, which can be combined with another half to make a full -// authority; or -// -// `Complete` -- knowledge that the one-shot has completed. -// -// `Empty` - no permission at all. +/// A one-shot resource represents one of the following four resources: +/// +/// `FullRightToComplete` -- the authority to complete the one-shot; +/// +/// `HalfRightToComplete` -- half of the authority to complete the +/// one-shot, which can be combined with another half to make a full +/// authority; or +/// +/// `Complete` -- knowledge that the one-shot has completed. +/// +/// `Empty` - no permission at all. pub enum OneShotResourceValue { FullRightToComplete, HalfRightToComplete, @@ -142,7 +146,7 @@ impl PCM for OneShotResourceValue { } pub struct OneShotResource { - r: Resource, + r: pcm::Resource, } impl OneShotResource { @@ -162,7 +166,7 @@ impl OneShotResource { resource@ is FullRightToComplete, { let v = OneShotResourceValue::FullRightToComplete { }; - let tracked mut r = Resource::::alloc(v); + let tracked mut r = pcm::Resource::::alloc(v); OneShotResource { r } } @@ -221,10 +225,10 @@ impl OneShotResource { !(old(other)@ is Empty), ensures old(other)@ is HalfRightToComplete, - final(self)@ is Complete, - final(other)@ is Complete, final(self).id() == old(self).id(), final(other).id() == old(self).id(), + final(self)@ is Complete, + final(other)@ is Complete, { self.r.validate(); other.r.validate(); @@ -266,8 +270,161 @@ impl OneShotResource { } } +/// A one-shot resource represents one of the following four resources: +/// +/// `FullRightToComplete` -- the authority to complete the one-shot; +/// +/// `HalfRightToComplete` -- half of the authority to complete the +/// one-shot, which can be combined with another half to make a full +/// authority; or +/// +/// `Complete` -- knowledge that the one-shot has completed. +/// +/// `Empty` - no permission at all. +pub type OneShotCarrier = ProductRA>>; + +pub struct OneShotResource2 { + r: algebra::Resource>, +} + +impl OneShotResource2 { + pub closed spec fn loc(self) -> Loc { + self.r.loc() + } + + /// The view of the underlying resource + pub closed spec fn view(self) -> Option { + match self.r.value().right { + Some(AgreementRA::Agree(x)) => Some(x), + _ => None + } + } + + pub closed spec fn fraction(self) -> real { + self.r.value().left.frac() + } + + pub proof fn alloc() -> (tracked resource: Self) + ensures + resource@ is None, + resource.fraction() == 1real, + { + let v = OneShotCarrier { left: FractionRA::new(1real), right: None }; + let tracked r = algebra::Resource::>::alloc(v); + OneShotResource2 { r } + } + + /// This function splits full authority to perform a one-shot + /// into two half authorities to perform it. + // TODO(bsdinis): make this using shared ref + pub proof fn split(tracked self) -> (tracked r: (Self, Self)) + requires + self@ is None, + self.fraction() == 1real, + ensures + ({ + let (half1, half2) = r; + &&& half1@ is None + &&& half2@ is None + &&& half1.fraction() == 0.5real + &&& half2.fraction() == 0.5real + &&& half1.loc() == self.loc() + &&& half2.loc() == self.loc() + }), + { + self.r.validate(); + assert(self.r.value().right is None); + let half = OneShotCarrier { left: FractionRA::new(0.5real), right: self.r.value().right }; + assert(self.r.value().left == FractionRA::op(half.left, half.left)); + assert(self.r.value().right == Option::op(half.right, half.right)); + let tracked (r1, r2) = self.r.split(half, half); + (OneShotResource2 { r: r1 }, OneShotResource2 { r: r2 }) + } + + // This function performs a one-shot given a resource representing + // full authority to complete the one-shot. + // + // Upon return, the passed-in resource will have been transformed + // into knowledge that the one-shot has been performed. + pub proof fn shoot(tracked &mut self, v: T) + requires + old(self)@ is None, + old(self).fraction() == 1real, + ensures + final(self)@ == Some(v) + { + let new_carrier = OneShotCarrier { left: self.r.value().left, right: Some(AgreementRA::Agree(v)) }; + // TODO(bsdinis): need the resource lib + // update_mut(&mut self.r, new_carrier); + admit() + } + + // This function performs a one-shot given two resources, the + // first of which represents an incomplete one-shot (and half the + // authority needed to perform it). The resources must have the + // same `loc()`, meaning they're talking about the same one-shot. + // + // Upon return, the passed-in resources will have both been + // transformed into knowledge that the one-shot has been + // performed. + // + // The caller of this function only needs to know that `self` + // provides half authority and that `other` isn't `Empty`. Upon + // return the caller will learn that *both* the resources had + // provided half authority at call time. However, those resources + // were transformed so they don't provide that authority anymore. + pub proof fn shoot_with_two_halves(tracked &mut self, tracked other: &mut Self, v: T) + requires + old(other).loc() == old(self).loc(), + old(self)@ is None, + old(self).fraction() + old(other).fraction() == 1real, + ensures + old(other)@ is None, + final(self).loc() == old(self).loc(), + final(other).loc() == old(self).loc(), + final(self).fraction() == old(self).fraction(), + final(other).fraction() == old(other).fraction(), + final(self)@ == Some(v), + final(other)@ == Some(v), + { + self.r.validate_2(&other.r); + let new_self_carrier = OneShotCarrier { left: self.r.value().left, right: Some(AgreementRA::Agree(v)) }; + let new_other_carrier = OneShotCarrier { left: other.r.value().left, right: Some(AgreementRA::Agree(v)) }; + // TODO(bsdinis): we want the full lib for ras too + // update_and_redistribute(&mut self.r, &mut other.r, v, v); + admit() + } + + // This function duplicates a one-shot resource representing knowledge of completion. + pub proof fn duplicate(tracked self) -> (tracked r: (Self, Self)) + requires + self@ is Some, + ensures + r.0.loc() == self.loc(), + r.1.loc() == self.loc(), + r.0@ == self@, + r.1@ == self@, + { + self.r.validate(); + let half = OneShotCarrier { left: FractionRA::new(self.fraction()/2real), right: self.r.value().right }; + let tracked (r1, r2) = self.r.split(half, half); + (OneShotResource2 { r: r1 }, OneShotResource2 { r: r2 }) + } + + pub proof fn lemma_agree(tracked &mut self, tracked other: &Self) + requires + other.loc() == old(self).loc(), + other@ is Some, + ensures + final(self).loc() == old(self).loc(), + final(self)@ == old(self)@, + { + self.r.validate_2(&other.r); + } +} + // This example illustrates some uses of the one-shot functions. -fn main() { +fn test_manual() { let tracked full = OneShotResource::alloc(); proof { full.perform(); @@ -292,4 +449,33 @@ fn main() { assert(knowledge@ is Complete); } +fn test_combinator() { + let tracked full = OneShotResource2::::alloc(); + proof { + full.shoot(2); + } + assert(full@ == Some(2int)); + let tracked different_oneshot = OneShotResource2::::alloc(); + let tracked (mut half1, mut half2) = different_oneshot.split(); + let ghost id = half1.loc(); + assert(half1.loc() == half2.loc()); + assert(half1@ is None); + assert(half2@ is None); + assert(half1.fraction() == 0.5real); + assert(half2.fraction() == 0.5real); + proof { + half1.shoot_with_two_halves(&mut half2, 3); + } + assert(half1.loc() == id); + assert(half2.loc() == id); + assert(half1@ == Some(3int)); + assert(half2@ == Some(3int)); + /* TODO(bsdinis): need shared refs + let tracked knowledge = half1.duplicate(); + assert(knowledge.loc() == id); + assert(half1.loc() == id); + assert(knowledge@ is Complete); + */ +} + } // verus! diff --git a/source/rust_verify_test/tests/examples.rs b/source/rust_verify_test/tests/examples.rs index 23b234f4f0..93e77855b2 100644 --- a/source/rust_verify_test/tests/examples.rs +++ b/source/rust_verify_test/tests/examples.rs @@ -16,7 +16,7 @@ enum Mode { examples_in_dir!("../../examples"); examples_in_dir!("../../examples/guide"); -examples_in_dir!("../../examples/pcm"); +examples_in_dir!("../../examples/resource"); examples_in_dir!("../../examples/state_machines"); examples_in_dir!("../../examples/summer_school"); examples_in_dir!("../../examples/state_machines/tutorial");