vstd/
pcm_lib.rs

1#![allow(unused_imports)]
2use super::map::*;
3use super::modes::*;
4use super::pcm::*;
5use super::prelude::*;
6use super::seq::*;
7
8verus! {
9
10broadcast use super::group_vstd_default;
11
12/// Combines a list of values into one value using P::op().
13pub open spec fn combine_values<P: PCM>(values: Seq<P>) -> P
14    decreases values.len(),
15{
16    if values.len() == 0 {
17        P::unit()
18    } else {
19        P::op(values[0], combine_values(values.skip(1)))
20    }
21}
22
23/// Provides four quantified facts about a partially commutative
24/// monoid: that it's closed under inclusion, that it's commutative,
25/// that it's a monoid, and that its unit element is valid. Note that,
26/// to avoid trigger loops, it doesn't provide associativity.
27pub proof fn lemma_pcm_properties<P: PCM>()
28    ensures
29        forall|a: P, b: P| (#[trigger] P::op(a, b)).valid() ==> a.valid(),
30        forall|a: P, b: P| (#[trigger] P::op(a, b)) == P::op(b, a),
31        forall|a: P| (#[trigger] P::op(a, P::unit())) == a,
32        P::valid(P::unit()),
33{
34    assert forall|a: P, b: P| (#[trigger] P::op(a, b)).valid() implies a.valid() by {
35        P::closed_under_incl(a, b);
36    }
37    assert forall|a: P, b: P| (#[trigger] P::op(a, b)) == P::op(b, a) by {
38        P::commutative(a, b);
39    }
40    assert forall|a: P| P::op(a, P::unit()) == a by {
41        P::op_unit(a);
42    }
43    assert(P::valid(P::unit())) by {
44        P::unit_valid();
45    }
46}
47
48/// Produces a new resource with value `new_value` given an immutable
49/// reference to a resource `r` whose value has a duplicable part
50/// `new_value`. More precisely, produces a resource with value
51/// `new_value` given that `r.value() == P::op(r.value(), new_value)`.
52pub proof fn copy_duplicable_part<P: PCM>(tracked r: &Resource<P>, new_value: P) -> (tracked out:
53    Resource<P>)
54    requires
55        r.value() == P::op(r.value(), new_value),
56    ensures
57        out.loc() == r.loc(),
58        out.value() == new_value,
59{
60    lemma_pcm_properties::<P>();
61    let tracked u = Resource::<P>::create_unit(r.loc());
62    u.update_with_shared(r, new_value)
63}
64
65/// Duplicates `r`, returning an identical resource. The value of
66/// `r` must be duplicable, i.e., `r.value()` must be equal to
67/// `P::op(r.value(), r.value())`.
68pub proof fn duplicate<P: PCM>(tracked r: &Resource<P>) -> (tracked other: Resource<P>)
69    requires
70        P::op(r.value(), r.value()) == r.value(),
71    ensures
72        other.loc() == r.loc(),
73        other.value() == r.value(),
74{
75    copy_duplicable_part(r, r.value())
76}
77
78/// Incorporates the resources of `r2` into `r1`, consuming `r2`.
79pub proof fn incorporate<P: PCM>(tracked r1: &mut Resource<P>, tracked r2: Resource<P>)
80    requires
81        old(r1).loc() == r2.loc(),
82    ensures
83        r1.loc() == old(r1).loc(),
84        r1.value() == P::op(old(r1).value(), r2.value()),
85{
86    let tracked mut r3 = Resource::<P>::create_unit(r1.loc());
87    tracked_swap(r1, &mut r3);
88    let tracked mut r4 = r3.join(r2);
89    tracked_swap(r1, &mut r4);
90}
91
92/// Splits the value of `r` into `left` and `right`. At the end, `r`
93/// ends up with `left` as its value and the function returns a new
94/// resource with value `right`.
95pub proof fn split_mut<P: PCM>(tracked r: &mut Resource<P>, left: P, right: P) -> (tracked other:
96    Resource<P>)
97    requires
98        old(r).value() == P::op(left, right),
99    ensures
100        r.loc() == other.loc() == old(r).loc(),
101        r.value() == left,
102        other.value() == right,
103{
104    let tracked mut r3 = Resource::<P>::create_unit(r.loc());
105    tracked_swap(r, &mut r3);
106    let tracked (mut r1, r2) = r3.split(left, right);
107    tracked_swap(r, &mut r1);
108    r2
109}
110
111/// Extracts the resource from `r`, leaving `r` empty (i.e., having
112/// value `P::unit`) and returning a new resource holding the previous
113/// value of `r`.
114pub proof fn extract<P: PCM>(tracked r: &mut Resource<P>) -> (tracked other: Resource<P>)
115    ensures
116        other.loc() == r.loc() == old(r).loc(),
117        r.value() == P::unit(),
118        other.value() == old(r).value(),
119{
120    lemma_pcm_properties::<P>();
121    split_mut(r, P::unit(), r.value())
122}
123
124/// Updates `r` to have new value `new_value`. This must be a
125/// frame-preserving update. That is, `new_value` must be compatible
126/// with all frames `old(r).value()` was compatible with.
127pub proof fn update_mut<P: PCM>(tracked r: &mut Resource<P>, new_value: P)
128    requires
129        frame_preserving_update(old(r).value(), new_value),
130    ensures
131        r.loc() == old(r).loc(),
132        r.value() == new_value,
133{
134    let tracked mut r3 = Resource::<P>::create_unit(r.loc());
135    tracked_swap(r, &mut r3);
136    let tracked mut r4 = r3.update(new_value);
137    tracked_swap(r, &mut r4);
138}
139
140/// Redistribute the values held by resources `r1` and `r2` such that they
141/// have the same combination as before. The new value of `r1` will be `v1`
142/// and the new value of `r2` will be `v2`.
143pub proof fn redistribute<P: PCM>(
144    tracked r1: &mut Resource<P>,
145    tracked r2: &mut Resource<P>,
146    v1: P,
147    v2: P,
148)
149    requires
150        old(r1).loc() == old(r2).loc(),
151        P::op(old(r1).value(), old(r2).value()) == P::op(v1, v2),
152    ensures
153        r1.loc() == r2.loc() == old(r1).loc(),
154        r1.value() == v1,
155        r2.value() == v2,
156{
157    lemma_pcm_properties::<P>();
158    let tracked r2_extracted = extract(r2);
159    incorporate(r1, r2_extracted);
160    let tracked r2_new = split_mut(r1, v1, v2);
161    incorporate(r2, r2_new);
162}
163
164/// Update the values held by resources `r1` and `r2` such that their
165/// values' combination is updated in a frame-preserving way (i.e.,
166/// that combination must be updatable in a frame-preserving way to
167/// the combination of `v1` and `v2`). The new value of `r1` will be
168/// `v1` and the new value of `r2` will be `v2`.
169pub proof fn update_and_redistribute<P: PCM>(
170    tracked r1: &mut Resource<P>,
171    tracked r2: &mut Resource<P>,
172    v1: P,
173    v2: P,
174)
175    requires
176        old(r1).loc() == old(r2).loc(),
177        frame_preserving_update(P::op(old(r1).value(), old(r2).value()), P::op(v1, v2)),
178    ensures
179        r1.loc() == r2.loc() == old(r1).loc(),
180        r1.value() == v1,
181        r2.value() == v2,
182{
183    lemma_pcm_properties::<P>();
184    let tracked r2_extracted = extract(r2);
185    incorporate(r1, r2_extracted);
186    update_mut(r1, P::op(v1, v2));
187    let tracked r2_new = split_mut(r1, v1, v2);
188    incorporate(r2, r2_new);
189}
190
191/// Validates that the three given resources have values that combine
192/// to form a valid value. Although `r1` and `r2` are mutable, they
193/// don't change. (They change during the function but are restored to
194/// the way they were by the time the function returns.)
195pub proof fn validate_3<P: PCM>(
196    tracked r1: &mut Resource<P>,
197    tracked r2: &mut Resource<P>,
198    tracked r3: &Resource<P>,
199)
200    requires
201        old(r1).loc() == old(r2).loc() == r3.loc(),
202    ensures
203        r1.loc() == r2.loc() == r3.loc(),
204        r1.value() == old(r1).value(),
205        r2.value() == old(r2).value(),
206        P::op(r1.value(), P::op(r2.value(), r3.value())).valid(),
207{
208    lemma_pcm_properties::<P>();
209    P::associative(r1.value(), r2.value(), r3.value());
210    let tracked mut r2_extracted = extract(r2);
211    incorporate(r1, r2_extracted);
212    r1.validate();
213    r1.validate_2(r3);
214    let tracked r2_split = split_mut(r1, old(r1).value(), old(r2).value());
215    incorporate(r2, r2_split);
216    assume(false);
217}
218
219// This is a helper function used by `validate_multiple_resources` but
220// not meant for public export.
221proof fn aggregate_resources_from_map_starting_at_offset<P: PCM>(
222    tracked m: &mut Map<int, Resource<P>>,
223    id: int,
224    values: Seq<P>,
225    offset: int,
226) -> (tracked all: Resource<P>)
227    requires
228        0 <= offset < values.len(),
229        forall|i|
230            #![trigger old(m).dom().contains(i)]
231            0 <= i < offset ==> !old(m).dom().contains(i),
232        forall|i|
233            #![trigger old(m).dom().contains(i)]
234            offset <= i < values.len() ==> old(m).dom().contains(i),
235        forall|i|
236            #![trigger old(m)[i]]
237            offset <= i < values.len() ==> old(m)[i].loc() == id && old(m)[i].value() == values[i],
238    ensures
239        forall|i| #![trigger m.dom().contains(i)] 0 <= i < values.len() ==> !m.dom().contains(i),
240        all.loc() == id,
241        all.value() == combine_values(values.skip(offset)),
242    decreases values.len() - offset,
243{
244    assert(m.dom().contains(offset));
245    assert(m[offset].loc() == id && m[offset].value() == values[offset]);
246    let tracked p = m.tracked_remove(offset);
247    if offset == values.len() - 1 {
248        assert(combine_values(values.skip(offset)) == values[offset]) by {
249            lemma_pcm_properties::<P>();  // needed to show that combining with unit is identity
250            reveal_with_fuel(combine_values, 2);
251        };
252        p
253    } else {
254        assert(combine_values(values.skip(offset)) == P::op(
255            values[offset],
256            combine_values(values.skip(offset + 1)),
257        )) by {
258            assert(values[offset] =~= values.skip(offset)[0]);
259            assert(values.skip(offset + 1) =~= values.skip(offset).skip(1));
260        }
261        assert forall|i|
262            #![trigger m.dom().contains(i)]
263            offset + 1 <= i < values.len() implies m.dom().contains(i) && m[i].loc() == id
264            && m[i].value() == values[i] by {
265            assert(m.dom().contains(i));
266            assert(m[i].loc() == id && m[i].value() == values[i]);
267        }
268        let tracked most = aggregate_resources_from_map_starting_at_offset(
269            m,
270            id,
271            values,
272            offset + 1,
273        );
274        assert(most.loc() == id);
275        assert(most.value() == combine_values(values.skip(offset + 1)));
276        p.join(most)
277    }
278}
279
280// This is a helper function used by `validate_multiple_resources` but
281// not meant for public export.
282proof fn store_resources_into_map_starting_at_offset<P: PCM>(
283    tracked m: &mut Map<int, Resource<P>>,
284    id: int,
285    values: Seq<P>,
286    offset: int,
287    tracked p: Resource<P>,
288)
289    requires
290        0 <= offset <= values.len(),
291        forall|i| #![trigger old(m).dom().contains(i)] 0 <= i < offset ==> old(m).dom().contains(i),
292        forall|i|
293            #![trigger old(m)[i]]
294            0 <= i < offset ==> old(m)[i].loc() == id && old(m)[i].value() == values[i],
295        forall|i|
296            #![trigger old(m).dom().contains(i)]
297            offset <= i < values.len() ==> !old(m).dom().contains(i),
298        p.loc() == id,
299        p.value() == combine_values(values.skip(offset)),
300    ensures
301        forall|i| #![trigger m.dom().contains(i)] 0 <= i < values.len() ==> m.dom().contains(i),
302        forall|i|
303            #![trigger m[i]]
304            0 <= i < values.len() ==> m[i].loc() == id && m[i].value() == values[i],
305    decreases values.len() - offset,
306{
307    if offset != values.len() {
308        assert(combine_values(values.skip(offset)) == P::op(
309            values[offset],
310            combine_values(values.skip(offset + 1)),
311        )) by {
312            assert(values[offset] =~= values.skip(offset)[0]);
313            assert(values.skip(offset + 1) =~= values.skip(offset).skip(1));
314        }
315        let tracked (p_first, p_rest) = p.split(
316            values[offset],
317            combine_values(values.skip(offset + 1)),
318        );
319        m.tracked_insert(offset, p_first);
320        store_resources_into_map_starting_at_offset(m, id, values, offset + 1, p_rest);
321    }
322}
323
324/// Validates that a given sequence of resources has values that
325/// combine to form a valid value. Although that sequence consists of
326/// mutable references, none of those resources change. (They change
327/// in the middle of the function, but are restored by the time it
328/// completes.) The sequence of resources is specified using the
329/// following input parameters:
330///
331/// `m` -- a map from integers to resources, mapping 0 to the first
332/// resource, 1 to the second, etc.
333///
334/// `loc` -- the `loc()` shared by all the resources in `m`
335///
336/// `values` -- the sequence of resources
337pub proof fn validate_multiple<P: PCM>(
338    tracked m: &mut Map<int, Resource<P>>,
339    loc: int,
340    values: Seq<P>,
341)
342    requires
343        forall|i|
344            #![trigger old(m).dom().contains(i)]
345            0 <= i < values.len() ==> old(m).dom().contains(i),
346        forall|i|
347            #![trigger old(m)[i]]
348            0 <= i < values.len() ==> old(m)[i].loc() == loc && old(m)[i].value() == values[i],
349    ensures
350        forall|i| #![trigger m.dom().contains(i)] 0 <= i < values.len() ==> m.dom().contains(i),
351        forall|i|
352            #![trigger m[i]]
353            0 <= i < values.len() ==> m[i].loc() == loc && m[i].value() == values[i],
354        combine_values(values).valid(),
355{
356    if values.len() == 0 {
357        lemma_pcm_properties::<P>();
358    } else {
359        let tracked agg = aggregate_resources_from_map_starting_at_offset(m, loc, values, 0);
360        assert(agg.value() == combine_values(values)) by {
361            assert(values =~= values.skip(0));
362        }
363        agg.validate();
364        store_resources_into_map_starting_at_offset(m, loc, values, 0, agg);
365    }
366}
367
368/// Validates that the four given resources have values that combine
369/// to form a valid value. Although the inputs `r1`, `r2`, `r3`, and
370/// `r4` are mutable, they don't change. (They change during the
371/// function but are restored to the way they were by the time the
372/// function returns.)
373pub proof fn validate_4<P: PCM>(
374    tracked r1: &mut Resource<P>,
375    tracked r2: &mut Resource<P>,
376    tracked r3: &mut Resource<P>,
377    tracked r4: &mut Resource<P>,
378)
379    requires
380        old(r1).loc() == old(r2).loc() == old(r3).loc() == old(r4).loc(),
381    ensures
382        r1.loc() == r2.loc() == r3.loc() == r4.loc() == old(r1).loc(),
383        r1.value() == old(r1).value(),
384        r2.value() == old(r2).value(),
385        r3.value() == old(r3).value(),
386        r4.value() == old(r4).value(),
387        P::op(r1.value(), P::op(r2.value(), P::op(r3.value(), r4.value()))).valid(),
388{
389    lemma_pcm_properties::<P>();
390    let tracked mut m: Map<int, Resource<P>> = Map::<int, Resource<P>>::tracked_empty();
391    let values: Seq<P> = seq![r1.value(), r2.value(), r3.value(), r4.value()];
392    m.tracked_insert(0, extract(r1));
393    m.tracked_insert(1, extract(r2));
394    m.tracked_insert(2, extract(r3));
395    m.tracked_insert(3, extract(r4));
396    assert(combine_values(values) == P::op(
397        old(r1).value(),
398        P::op(old(r2).value(), P::op(old(r3).value(), old(r4).value())),
399    )) by {
400        lemma_pcm_properties::<P>();
401        reveal_with_fuel(combine_values, 5);
402    }
403    validate_multiple(&mut m, r1.loc(), values);
404    incorporate(r1, m.tracked_remove(0));
405    incorporate(r2, m.tracked_remove(1));
406    incorporate(r3, m.tracked_remove(2));
407    incorporate(r4, m.tracked_remove(3));
408}
409
410/// Validates that the five given resources have values that combine
411/// to form a valid value. Although the inputs are mutable, they don't
412/// change. (They change during the function but are restored to the
413/// way they were by the time the function returns.)
414pub proof fn validate_5<P: PCM>(
415    tracked r1: &mut Resource<P>,
416    tracked r2: &mut Resource<P>,
417    tracked r3: &mut Resource<P>,
418    tracked r4: &mut Resource<P>,
419    tracked r5: &mut Resource<P>,
420)
421    requires
422        old(r1).loc() == old(r2).loc() == old(r3).loc() == old(r4).loc() == old(r5).loc(),
423    ensures
424        r1.loc() == r2.loc() == r3.loc() == r4.loc() == r5.loc() == old(r1).loc(),
425        r1.value() == old(r1).value(),
426        r2.value() == old(r2).value(),
427        r3.value() == old(r3).value(),
428        r4.value() == old(r4).value(),
429        r5.value() == old(r5).value(),
430        P::op(
431            r1.value(),
432            P::op(r2.value(), P::op(r3.value(), P::op(r4.value(), r5.value()))),
433        ).valid(),
434{
435    lemma_pcm_properties::<P>();
436    let tracked mut m: Map<int, Resource<P>> = Map::<int, Resource<P>>::tracked_empty();
437    let values: Seq<P> = seq![r1.value(), r2.value(), r3.value(), r4.value(), r5.value()];
438    m.tracked_insert(0, extract(r1));
439    m.tracked_insert(1, extract(r2));
440    m.tracked_insert(2, extract(r3));
441    m.tracked_insert(3, extract(r4));
442    m.tracked_insert(4, extract(r5));
443    assert(combine_values(values) == P::op(
444        old(r1).value(),
445        P::op(old(r2).value(), P::op(old(r3).value(), P::op(old(r4).value(), old(r5).value()))),
446    )) by {
447        lemma_pcm_properties::<P>();
448        reveal_with_fuel(combine_values, 6);
449    }
450    validate_multiple(&mut m, r1.loc(), values);
451    incorporate(r1, m.tracked_remove(0));
452    incorporate(r2, m.tracked_remove(1));
453    incorporate(r3, m.tracked_remove(2));
454    incorporate(r4, m.tracked_remove(3));
455    incorporate(r5, m.tracked_remove(4));
456}
457
458} // verus!
vstd/pcm_lib.rs

vstd/
pcm_lib.rs
