Skip to content

Commit 6efa7ff

Browse files
rikosellicrikosellic
committed
Adjust library
1 parent 4b33d71 commit 6efa7ff

3 files changed

Lines changed: 94 additions & 189 deletions

File tree

‎vstd_extra/src/resource/ghost_resource/csum.rs‎

Lines changed: 29 additions & 188 deletions
Original file line numberDiff line numberDiff line change
@@ -6,203 +6,44 @@ use vstd::storage_protocol::*;
66
use crate::resource::storage_protocol::csum::*;
77
use crate::sum::*;
88

9+
use super::excl::UniqueTokenStorage;
10+
911
verus! {
1012

11-
/// `SumResource` is a storage resource that stores either an A or a B, but not both.
12-
pub tracked struct SumResource<A, B> {
13-
tracked r: StorageResource<(), Sum<A, B>, CsumP<A, B>>,
13+
pub tracked struct SumResource<K,A,B,W,V> {
14+
pub r: StorageResource<K, Sum<W, V>, CsumP<A, B>>,
1415
}
1516

16-
impl<A, B> SumResource<A, B> {
17-
pub closed spec fn id(self) -> Loc {
18-
self.r.loc()
19-
}
20-
21-
pub closed spec fn protocol_monoid(self) -> CsumP<A, B> {
22-
self.r.value()
23-
}
24-
25-
pub open spec fn is_empty(self) -> bool {
26-
self.protocol_monoid() is Unit
27-
}
28-
29-
pub open spec fn is_left(self) -> bool {
30-
self.protocol_monoid() is Cinl
31-
}
32-
33-
pub open spec fn is_right(self) -> bool {
34-
self.protocol_monoid() is Cinr
35-
}
36-
37-
pub open spec fn resource(self) -> Sum<A, B> {
38-
self.protocol_monoid().to_sum()
39-
}
40-
41-
pub proof fn is_exclusive(tracked &mut self, tracked other: &Self)
42-
requires
43-
old(self).is_left() || old(self).is_right(),
44-
other.is_left() || other.is_right(),
45-
ensures
46-
*self == *old(self),
47-
self.id() != other.id(),
48-
{
49-
if (self.id() == other.id()) {
50-
self.r.validate_with_shared(&other.r);
51-
}
52-
}
53-
54-
pub proof fn alloc_empty() -> (tracked res: Self)
55-
ensures
56-
res.is_empty(),
57-
{
58-
let tracked r = StorageResource::alloc(CsumP::Unit, Map::tracked_empty());
59-
SumResource { r }
60-
}
61-
62-
pub proof fn alloc_left(tracked a: A) -> (tracked res: Self)
63-
ensures
64-
res.is_left(),
65-
res.resource() is Left,
66-
res.resource()->Left_0 == a,
67-
{
68-
let tracked mut m = Map::tracked_empty();
69-
m.tracked_insert((), Sum::Left(a));
70-
let tracked r = StorageResource::alloc(CsumP::Cinl(a), m);
71-
SumResource { r }
72-
}
73-
74-
pub proof fn alloc_right(tracked b: B) -> (tracked res: Self)
75-
ensures
76-
res.is_right(),
77-
res.resource() is Right,
78-
res.resource()->Right_0 == b,
79-
{
80-
let tracked mut m = Map::tracked_empty();
81-
m.tracked_insert((), Sum::Right(b));
82-
let tracked r = StorageResource::alloc(CsumP::Cinr(b), m);
83-
SumResource { r }
84-
}
85-
86-
pub proof fn tracked_take(tracked self) -> (tracked res: Sum<A, B>)
87-
requires
88-
self.is_left() || self.is_right(),
89-
ensures
90-
res == self.resource(),
91-
{
92-
self.protocol_monoid().lemma_csum_withdraws();
93-
let tracked r = self.r;
94-
let tracked (_, mut m) = r.withdraw(
95-
CsumP::Unit,
96-
map![() => self.protocol_monoid().to_sum()],
97-
);
98-
m.tracked_remove(())
99-
}
17+
impl <K,W,V,A:Protocol<K,W>,B:Protocol<K,V>> SumResource<K,A,B,W,V> {
10018

101-
pub proof fn tracked_take_left(tracked self) -> (tracked res: A)
102-
requires
103-
self.is_left(),
104-
ensures
105-
res == self.resource()->Left_0,
106-
{
107-
let tracked sum = self.tracked_take();
108-
sum.tracked_take_left()
109-
}
110-
111-
pub proof fn tracked_take_right(tracked self) -> (tracked res: B)
112-
requires
113-
self.is_right(),
114-
ensures
115-
res == self.resource()->Right_0,
116-
{
117-
let tracked sum = self.tracked_take();
118-
sum.tracked_take_right()
119-
}
120-
121-
pub proof fn split_left(tracked self) -> (tracked res: (Self, Self))
122-
requires
123-
self.is_left(),
124-
ensures
125-
res.0.is_empty(),
126-
res.1.is_left(),
127-
res.0.id() == self.id(),
128-
res.1.id() == self.id(),
129-
res.1.protocol_monoid() == self.protocol_monoid(),
130-
res.1.resource() == self.resource(),
131-
{
132-
self.protocol_monoid().lemma_csum_withdraws();
133-
let tracked r = self.r;
134-
let tracked (r1, r2) = r.split(CsumP::Unit, CsumP::Cinl(self.resource()->Left_0));
135-
(SumResource { r: r1 }, SumResource { r: r2 })
136-
}
137-
138-
pub proof fn split_right(tracked self) -> (tracked res: (Self, Self))
139-
requires
140-
self.is_right(),
141-
ensures
142-
res.0.is_empty(),
143-
res.1.is_right(),
144-
res.0.id() == self.id(),
145-
res.1.id() == self.id(),
146-
res.1.protocol_monoid() == self.protocol_monoid(),
147-
res.1.resource() == self.resource(),
148-
{
149-
self.protocol_monoid().lemma_csum_withdraws();
150-
let tracked r = self.r;
151-
let tracked (r1, r2) = r.split(CsumP::Unit, CsumP::Cinr(self.resource()->Right_0));
152-
(SumResource { r: r1 }, SumResource { r: r2 })
153-
}
154-
155-
pub proof fn split_and_take_left(tracked self) -> (tracked res: (Self, A))
156-
requires
157-
self.is_left(),
158-
ensures
159-
res.0.is_empty(),
160-
res.0.id() == self.id(),
161-
res.1 == self.resource()->Left_0,
162-
{
163-
let tracked (r1, r2) = self.split_left();
164-
(r1, r2.tracked_take_left())
165-
}
166-
167-
pub proof fn split_and_take_right(tracked self) -> (tracked res: (Self, B))
168-
requires
169-
self.is_right(),
170-
ensures
171-
res.0.is_empty(),
172-
res.0.id() == self.id(),
173-
res.1 == self.resource()->Right_0,
174-
{
175-
let tracked (r1, r2) = self.split_right();
176-
(r1, r2.tracked_take_right())
177-
}
19+
pub open spec fn id(self) -> Loc {
20+
self.r.loc()
21+
}
17822

179-
pub proof fn tracked_borrow(tracked &self) -> (tracked res: &Sum<A, B>)
180-
requires
181-
self.is_left() || self.is_right(),
182-
ensures
183-
*res == self.resource(),
184-
{
185-
StorageResource::guard(&self.r, map![() => self.resource()]).tracked_borrow(())
186-
}
23+
pub open spec fn protocol_monoid(self) -> CsumP<A, B> {
24+
self.r.value()
25+
}
18726

188-
pub proof fn tracked_borrow_left(tracked &self) -> (tracked res: &A)
189-
requires
190-
self.is_left(),
191-
ensures
192-
*res == self.resource()->Left_0,
193-
{
194-
self.tracked_borrow().tracked_borrow_left()
195-
}
27+
pub open spec fn is_empty(self) -> bool {
28+
self.protocol_monoid() is Unit
29+
}
19630

197-
pub proof fn tracked_borrow_right(tracked &self) -> (tracked res: &B)
198-
requires
199-
self.is_right(),
200-
ensures
201-
*res == self.resource()->Right_0,
202-
{
203-
self.tracked_borrow().tracked_borrow_right()
204-
}
31+
pub open spec fn is_left(self) -> bool {
32+
self.protocol_monoid() is Cinl
33+
}
20534

35+
pub open spec fn is_right(self) -> bool {
36+
self.protocol_monoid() is Cinr
37+
}
38+
39+
pub proof fn alloc_left(a:A, tracked s: Map<K, W>) -> (tracked res: Self)
40+
requires
41+
A::rel(a, s),
42+
ensures
43+
res.protocol_monoid() == CsumP::Cinl(a),
44+
{
45+
46+
}
20647
}
20748

20849
} // verus!

‎vstd_extra/src/resource/storage_protocol/csum.rs‎

Lines changed: 56 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,61 @@ pub ghost enum CsumP<A, B> {
1717
CsumInvalid,
1818
}
1919

20+
impl<K,W,V,A:Protocol<K,W>,B:Protocol<K,V>> Protocol<K, Sum<W, V>> for CsumP<A, B> {
21+
open spec fn op(self, other: Self) -> Self {
22+
match (self, other) {
23+
(CsumP::Unit, x) => x,
24+
(x, CsumP::Unit) => x,
25+
(CsumP::Cinl(a1), CsumP::Cinl(a2)) => CsumP::Cinl(A::op(a1, a2)),
26+
(CsumP::Cinr(b1), CsumP::Cinr(b2)) => CsumP::Cinr(B::op(b1, b2)),
27+
_ => CsumP::CsumInvalid,
28+
}
29+
}
30+
31+
open spec fn rel(self, s: Map<K, Sum<W, V>>) -> bool {
32+
match self {
33+
CsumP::Unit => s.is_empty(),
34+
CsumP::Cinl(a) => exists |m:Map<K, W>| #[trigger] A::rel(a, m) && s == m.map_values(|w| Sum::<W,V>::Left(w)),
35+
CsumP::Cinr(b) => exists |m:Map<K, V>| #[trigger] B::rel(b, m) && s == m.map_values(|v| Sum::<W,V>::Right(v)),
36+
CsumP::CsumInvalid => false,
37+
}
38+
}
39+
40+
open spec fn unit() -> Self {
41+
CsumP::Unit
42+
}
43+
44+
proof fn commutative(a: Self, b: Self) {
45+
if a is Cinl && b is Cinl {
46+
A::commutative(a->Cinl_0, b->Cinl_0);
47+
} else if a is Cinr && b is Cinr {
48+
B::commutative(a->Cinr_0, b->Cinr_0);
49+
}
50+
}
51+
52+
proof fn associative(a: Self, b: Self, c: Self) {
53+
if a is Cinl && b is Cinl && c is Cinl {
54+
A::associative(a->Cinl_0, b->Cinl_0, c->Cinl_0);
55+
} else if a is Cinr && b is Cinr && c is Cinr {
56+
B::associative(a->Cinr_0, b->Cinr_0, c->Cinr_0);
57+
}
58+
}
59+
60+
proof fn op_unit(a: Self) {}
61+
62+
}
63+
64+
impl<A, B> CsumP<A, B> {
65+
pub open spec fn to_sum(self) -> Sum<A, B> {
66+
match self {
67+
CsumP::Cinl(a) => Sum::Left(a),
68+
CsumP::Cinr(b) => Sum::Right(b),
69+
_ => arbitrary(),
70+
}
71+
}
72+
}
73+
74+
/*
2075
/// This protocol monoid allows exclusive ownership of either an A or a B, but not both. s
2176
impl<A, B> Protocol<(), Sum<A, B>> for CsumP<A, B> {
2277
open spec fn op(self, other: Self) -> Self {
@@ -77,6 +132,6 @@ impl<A, B> CsumP<A, B> {
77132
) && Self::rel(Self::op(self, q), res_map));
78133
}
79134
}
80-
}
135+
}*/
81136

82137
} // verus!

‎vstd_extra/src/sum.rs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,15 @@ impl<L, R> Sum<L, R> {
7272
Self::Right(right) => right,
7373
}
7474
}
75+
76+
pub open spec fn lift_map_left<K>(m: Map<K, L>) -> Map<K, Self> {
77+
m.map_values(|w| Sum::<L,R>::Left(w))
78+
}
79+
80+
pub open spec fn lift_map_right<K>(m: Map<K, R>) -> Map<K, Self> {
81+
m.map_values(|v| Sum::<L,R>::Right(v))
82+
}
83+
7584
}
7685

7786
impl<L: Inv, R: Inv> Inv for Sum<L, R> {

0 commit comments

Comments
 (0)