vstd/
tokens.rs

1use super::multiset::*;
2use super::prelude::*;
3use core::marker::PhantomData;
4
5pub mod frac;
6pub mod map;
7pub mod seq;
8
9use verus as verus_;
10verus_! {
11
12// Note that the tokenized_state_machine! macro creates trusted implementations
13// of all these traits. Therefore all the proof functions in here are trusted.
14// The 'collection types', (MapToken, SetToken, MultisetToken) are verified, but the properties
15// of these types is still assumed by the Verus macro, so they're still mostly trusted.
16
17#[verusfmt::skip]
18broadcast use {
19    super::set_lib::group_set_lib_default,
20    super::set::group_set_axioms,
21    super::map::group_map_axioms };
22
23/// Unique identifier for every VerusSync instance.
24/// Every "Token" and "Instance" object has an `InstanceId`. These ID values must agree
25/// to perform any token operation.
26pub ghost struct InstanceId(pub int);
27
28/// Interface for VerusSync tokens created for a field marked with the
29/// `variable`, `option` or `persistent_option` strategies.
30///
31/// | VerusSync Strategy  | Field type  | Token trait            |
32/// |---------------------|-------------|------------------------|
33/// | `variable`          | `V`         | [`UniqueValueToken<V>`](`UniqueValueToken`)        |
34/// | `option`            | `Option<V>` | [`UniqueValueToken<V>`](`UniqueValueToken`)        |
35/// | `persistent_option` | `Option<V>` | `ValueToken<V> + Copy` |
36///
37/// For the cases where the tokens are not `Copy`, then token is necessarily _unique_
38/// per-instance; the sub-trait, [`UniqueValueToken<V>`](`UniqueValueToken`), provides
39/// an additional lemma to prove uniqueness.
40
41pub trait ValueToken<Value> : Sized {
42    spec fn instance_id(&self) -> InstanceId;
43    spec fn value(&self) -> Value;
44
45    /// All tokens (for the same instance) must agree on the value.
46    proof fn agree(tracked &self, tracked other: &Self)
47        requires self.instance_id() == other.instance_id(),
48        ensures self.value() == other.value();
49
50    /// Return an arbitrary token. It's not possible to do anything interesting
51    /// with this token because it doesn't have a specified instance.
52    proof fn arbitrary() -> (tracked s: Self);
53}
54
55/// Interface for VerusSync tokens created for a field marked with the `variable` or `option` strategies.
56///
57/// See the super-trait [`ValueToken`](ValueToken) for more information.
58pub trait UniqueValueToken<Value> : ValueToken<Value> {
59    /// The token for a given instance must be unique; in other words, if we have two
60    /// tokens, they must be for distinct instances.
61    /// Though the first argument is mutable, the value is not really mutated;
62    /// this is only used to ensure unique ownership of the argument.
63    proof fn unique(tracked &mut self, tracked other: &Self)
64        ensures
65            self.instance_id() != other.instance_id(),
66            *self == *old(self);
67}
68
69/// Interface for VerusSync tokens created for a field marked with the
70/// `map` or `persistent_map` strategies.
71///
72/// | VerusSync Strategy  | Field type  | Token trait            |
73/// |---------------------|-------------|------------------------|
74/// | `map`               | `Map<K, V>` | [`UniqueKeyValueToken<K, V>`](`UniqueKeyValueToken`) |
75/// | `persistent_map`    | `Map<K, V>` | `KeyValueToken<V> + Copy` |
76///
77/// For the cases where the tokens are not `Copy`, then token is necessarily _unique_
78/// per-instance, per-key; the sub-trait, [`UniqueKeyValueToken<V>`](`UniqueKeyValueToken`), provides
79/// an additional lemma to prove uniqueness.
80///
81/// Each token represents a _single_ key-value pair.
82/// To work with a collection of `KeyValueToken`s, use [`MapToken`].
83
84pub trait KeyValueToken<Key, Value> : Sized {
85    spec fn instance_id(&self) -> InstanceId;
86    spec fn key(&self) -> Key;
87    spec fn value(&self) -> Value;
88
89    /// All tokens, for the same instance and _key_, must agree on the value.
90    proof fn agree(tracked &self, tracked other: &Self)
91        requires self.instance_id() == other.instance_id(),
92                 self.key() == other.key(),
93        ensures self.value() == other.value();
94
95    /// Return an arbitrary token. It's not possible to do anything interesting
96    /// with this token because it doesn't have a specified instance.
97    proof fn arbitrary() -> (tracked s: Self);
98}
99
100/// Interface for VerusSync tokens created for a field marked with the `map` strategy.
101///
102/// See the super-trait [`KeyValueToken`](KeyValueToken) for more information.
103pub trait UniqueKeyValueToken<Key, Value> : KeyValueToken<Key, Value> {
104    /// The token for a given instance and key must be unique; in other words, if we have two
105    /// tokens, they must be for distinct instances or keys.
106    /// Though the first argument is mutable, the value is not really mutated;
107    /// this is only used to ensure unique ownership of the argument.
108    proof fn unique(tracked &mut self, tracked other: &Self)
109        ensures
110            self.instance_id() != other.instance_id() || self.key() != other.key(),
111            *self == *old(self);
112}
113
114/// Interface for VerusSync tokens created for a field marked with the `count` strategy.
115///
116/// | VerusSync Strategy  | Field type  | Token trait            |
117/// |---------------------|-------------|------------------------|
118/// | `count`             | `nat`       | `CountToken`           |
119///
120/// These tokens are "fungible" in the sense that they can be combined and split, numbers
121/// combining additively.
122///
123/// (For the `persistent_count` strategy, see [`MonotonicCountToken`].)
124pub trait CountToken : Sized {
125    spec fn instance_id(&self) -> InstanceId;
126    spec fn count(&self) -> nat;
127
128    proof fn join(tracked &mut self, tracked other: Self)
129        requires
130            old(self).instance_id() == other.instance_id(),
131        ensures
132            self.instance_id() == old(self).instance_id(),
133            self.count() == old(self).count() + other.count();
134
135    proof fn split(tracked &mut self, count: nat) -> (tracked token: Self)
136        requires
137            count <= old(self).count()
138        ensures
139            self.instance_id() == old(self).instance_id(),
140            self.count() == old(self).count() - count,
141            token.instance_id() == old(self).instance_id(),
142            token.count() == count;
143
144    proof fn weaken_shared(tracked &self, count: nat) -> (tracked s: &Self)
145        requires count <= self.count(),
146        ensures s.instance_id() == self.instance_id(),
147            s.count() == count;
148
149    /// Return an arbitrary token. It's not possible to do anything interesting
150    /// with this token because it doesn't have a specified instance.
151    proof fn arbitrary() -> (tracked s: Self);
152}
153
154/// Interface for VerusSync tokens created for a field marked with the `persistent_count` strategy.
155///
156/// | VerusSync Strategy  | Field type  | Token trait                   |
157/// |---------------------|-------------|-------------------------------|
158/// | `persistent_count`  | `nat`       | `MonotonicCountToken + Copy`  |
159///
160/// A token represents a "lower bound" on the field value, which increases monotonically.
161
162pub trait MonotonicCountToken : Sized {
163    spec fn instance_id(&self) -> InstanceId;
164    spec fn count(&self) -> nat;
165
166    proof fn weaken(tracked &self, count: nat) -> (tracked s: Self)
167        requires count <= self.count(),
168        ensures s.instance_id() == self.instance_id(),
169            s.count() == count;
170
171    /// Return an arbitrary token. It's not possible to do anything interesting
172    /// with this token because it doesn't have a specified instance.
173    proof fn arbitrary() -> (tracked s: Self);
174}
175
176/// Interface for VerusSync tokens created for a field marked with the
177/// `set`, `persistent_set` or `multiset` strategies.
178///
179/// | VerusSync Strategy  | Field type  | Token trait            |
180/// |---------------------|-------------|------------------------|
181/// | `set`               | `Set<V>`    | [`UniqueElementToken<V>`](`UniqueElementToken`) |
182/// | `persistent_set`    | `Set<V>`    | `ElementToken<V> + Copy` |
183/// | `multiset`          | `Multiset<V>` | `ElementToken<V>`      |
184///
185/// Each token represents a single element of the set or multiset.
186///
187///  * For the `set` strategy, the token for any given element is unique.
188///  * For the `persistent_set` strategy, the token for any given element is not unique, but is `Copy`.
189///  * For the `multiset` strategy, the tokens are neither unique nor `Copy`, as the specific
190///    multiplicity of each element must be exact.
191///
192/// To work with a collection of `ElementToken`s, use [`SetToken`] or [`MultisetToken`].
193
194pub trait ElementToken<Element> : Sized {
195    spec fn instance_id(&self) -> InstanceId;
196    spec fn element(&self) -> Element;
197
198    /// Return an arbitrary token. It's not possible to do anything interesting
199    /// with this token because it doesn't have a specified instance.
200    proof fn arbitrary() -> (tracked s: Self);
201}
202
203/// Interface for VerusSync tokens created for a field marked with the `set` strategy.
204///
205/// See the super-trait [`ElementToken`](ElementToken) for more information.
206pub trait UniqueElementToken<Element> : ElementToken<Element> {
207    /// The token for a given instance and element must be unique; in other words, if we have two
208    /// tokens, they must be for distinct instances or elements.
209    /// Though the first argument is mutable, the value is not really mutated;
210    /// this is only used to ensure unique ownership of the argument.
211    proof fn unique(tracked &mut self, tracked other: &Self)
212        ensures
213            self.instance_id() == other.instance_id() ==> self.element() != other.element(),
214            *self == *old(self);
215}
216
217/// Interface for VerusSync tokens created for a field marked with the `bool` or
218/// `persistent_bool` strategy.
219///
220/// | VerusSync Strategy  | Field type  | Token trait            |
221/// |---------------------|-------------|------------------------|
222/// | `bool`              | `bool`      | [`UniqueSimpleToken<V>`](`UniqueSimpleToken`) |
223/// | `persistent_bool`   | `bool`      | `SimpleToken<V> + Copy` |
224///
225/// The token contains no additional data; its presence indicates that the boolean field
226/// is `true`.
227pub trait SimpleToken : Sized {
228    spec fn instance_id(&self) -> InstanceId;
229
230    /// Return an arbitrary token. It's not possible to do anything interesting
231    /// with this token because it doesn't have a specified instance.
232    proof fn arbitrary() -> (tracked s: Self);
233}
234
235/// Interface for VerusSync tokens created for a field marked with the `bool` strategy.
236///
237/// See the super-trait [`SimpleToken`](SimpleToken) for more information.
238pub trait UniqueSimpleToken : SimpleToken {
239    /// The token for a given instance must be unique; in other words, if we have two
240    /// tokens, they must be for distinct instances.
241    /// Though the first argument is mutable, the value is not really mutated;
242    /// this is only used to ensure unique ownership of the argument.
243    proof fn unique(tracked &mut self, tracked other: &Self)
244        ensures
245            self.instance_id() != other.instance_id(),
246            *self == *old(self);
247}
248
249#[verifier::reject_recursive_types(Key)]
250pub tracked struct MapToken<Key, Value, Token>
251    where Token: KeyValueToken<Key, Value>
252{
253    ghost _v: PhantomData<Value>,
254    ghost inst: InstanceId,
255    tracked m: Map<Key, Token>,
256}
257
258impl<Key, Value, Token> MapToken<Key, Value, Token>
259    where Token: KeyValueToken<Key, Value>
260{
261    #[verifier::type_invariant]
262    spec fn wf(self) -> bool {
263        forall |k| #[trigger] self.m.dom().contains(k) ==> self.m[k].key() == k
264            && self.m[k].instance_id() == self.inst
265    }
266
267    pub closed spec fn instance_id(self) -> InstanceId {
268        self.inst
269    }
270
271    pub closed spec fn map(self) -> Map<Key, Value> {
272        Map::new(
273            |k: Key| self.m.dom().contains(k),
274            |k: Key| self.m[k].value(),
275        )
276    }
277
278    #[verifier::inline]
279    pub open spec fn dom(self) -> Set<Key> {
280        self.map().dom()
281    }
282
283    #[verifier::inline]
284    pub open spec fn spec_index(self, k: Key) -> Value {
285        self.map()[k]
286    }
287
288    #[verifier::inline]
289    pub open spec fn index(self, k: Key) -> Value {
290        self.map()[k]
291    }
292
293    pub proof fn empty(instance_id: InstanceId) -> (tracked s: Self)
294        ensures
295            s.instance_id() == instance_id,
296            s.map() === Map::empty(),
297    {
298        let tracked s = Self { inst: instance_id, m: Map::tracked_empty(), _v: PhantomData };
299        assert(s.map() =~= Map::empty());
300        return s;
301    }
302
303    pub proof fn insert(tracked &mut self, tracked token: Token)
304        requires
305            old(self).instance_id() == token.instance_id(),
306        ensures
307            self.instance_id() == old(self).instance_id(),
308            self.map() == old(self).map().insert(token.key(), token.value()),
309    {
310        use_type_invariant(&*self);
311        self.m.tracked_insert(token.key(), token);
312        assert(self.map() =~= old(self).map().insert(token.key(), token.value()));
313    }
314
315    pub proof fn remove(tracked &mut self, key: Key) -> (tracked token: Token)
316        requires
317            old(self).map().dom().contains(key)
318        ensures
319            self.instance_id() == old(self).instance_id(),
320            self.map() == old(self).map().remove(key),
321            token.instance_id() == self.instance_id(),
322            token.key() == key,
323            token.value() == old(self).map()[key]
324    {
325        use_type_invariant(&*self);
326        let tracked t = self.m.tracked_remove(key);
327        assert(self.map() =~= old(self).map().remove(key));
328        t
329    }
330
331    pub proof fn into_map(tracked self) -> (tracked map: Map<Key, Token>)
332        ensures
333            map.dom() == self.map().dom(),
334            forall |key|
335                #![trigger(map.dom().contains(key))]
336                #![trigger(map.index(key))]
337              map.dom().contains(key)
338                ==> map[key].instance_id() == self.instance_id()
339                 && map[key].key() == key
340                 && map[key].value() == self.map()[key]
341    {
342        use_type_invariant(&self);
343        let tracked MapToken { inst, m, _v } = self;
344        assert(m.dom() =~= self.map().dom());
345        return m;
346    }
347
348    pub proof fn from_map(instance_id: InstanceId, tracked map: Map<Key, Token>) -> (tracked s: Self)
349        requires
350            forall |key| #[trigger] map.dom().contains(key) ==> map[key].instance_id() == instance_id,
351            forall |key| #[trigger] map.dom().contains(key) ==> map[key].key() == key,
352        ensures
353            s.instance_id() == instance_id,
354            s.map().dom() == map.dom(),
355            forall |key| #[trigger] map.dom().contains(key)
356                ==> s.map()[key] == map[key].value()
357    {
358        let tracked s = MapToken { inst: instance_id, m: map, _v: PhantomData };
359        assert(map.dom() == s.map().dom());
360        s
361    }
362}
363
364#[verifier::reject_recursive_types(Element)]
365pub tracked struct SetToken<Element, Token>
366    where Token: ElementToken<Element>
367{
368    ghost inst: InstanceId,
369    tracked m: Map<Element, Token>,
370}
371
372impl<Element, Token> SetToken<Element, Token>
373    where Token: ElementToken<Element>
374{
375    #[verifier::type_invariant]
376    spec fn wf(self) -> bool {
377        forall |k| #[trigger] self.m.dom().contains(k) ==> self.m[k].element() == k
378            && self.m[k].instance_id() == self.inst
379    }
380
381    pub closed spec fn instance_id(self) -> InstanceId {
382        self.inst
383    }
384
385    pub closed spec fn set(self) -> Set<Element> {
386        Set::new(
387            |e: Element| self.m.dom().contains(e),
388        )
389    }
390
391    #[verifier::inline]
392    pub open spec fn contains(self, element: Element) -> bool {
393        self.set().contains(element)
394    }
395
396    pub proof fn empty(instance_id: InstanceId) -> (tracked s: Self)
397        ensures
398            s.instance_id() == instance_id,
399            s.set() === Set::empty(),
400    {
401        let tracked s = Self { inst: instance_id, m: Map::tracked_empty() };
402        assert(s.set() =~= Set::empty());
403        return s;
404    }
405
406    pub proof fn insert(tracked &mut self, tracked token: Token)
407        requires
408            old(self).instance_id() == token.instance_id(),
409        ensures
410            self.instance_id() == old(self).instance_id(),
411            self.set() == old(self).set().insert(token.element()),
412    {
413        use_type_invariant(&*self);
414        self.m.tracked_insert(token.element(), token);
415        assert(self.set() =~= old(self).set().insert(token.element()));
416    }
417
418    pub proof fn remove(tracked &mut self, element: Element) -> (tracked token: Token)
419        requires
420            old(self).set().contains(element)
421        ensures
422            self.instance_id() == old(self).instance_id(),
423            self.set() == old(self).set().remove(element),
424            token.instance_id() == self.instance_id(),
425            token.element() == element,
426    {
427        use_type_invariant(&*self);
428        let tracked t = self.m.tracked_remove(element);
429        assert(self.set() =~= old(self).set().remove(element));
430        t
431    }
432
433    pub proof fn into_map(tracked self) -> (tracked map: Map<Element, Token>)
434        ensures
435            map.dom() == self.set(),
436            forall |key|
437                #![trigger(map.dom().contains(key))]
438                #![trigger(map.index(key))]
439                map.dom().contains(key)
440                    ==> map[key].instance_id() == self.instance_id()
441                     && map[key].element() == key
442    {
443        use_type_invariant(&self);
444        let tracked SetToken { inst, m } = self;
445        assert(m.dom() =~= self.set());
446        return m;
447    }
448
449    pub proof fn from_map(instance_id: InstanceId, tracked map: Map<Element, Token>) -> (tracked s: Self)
450        requires
451            forall |key| #[trigger] map.dom().contains(key) ==> map[key].instance_id() == instance_id,
452            forall |key| #[trigger] map.dom().contains(key) ==> map[key].element() == key,
453        ensures
454            s.instance_id() == instance_id,
455            s.set() == map.dom(),
456    {
457        let tracked s = SetToken { inst: instance_id, m: map };
458        assert(s.set() =~= map.dom());
459        s
460    }
461}
462
463pub tracked struct MultisetToken<Element, Token>
464    where Token: ElementToken<Element>
465{
466    ghost _v: PhantomData<Element>,
467    ghost inst: InstanceId,
468    tracked m: Map<int, Token>,
469}
470
471spec fn map_values<K, V>(m: Map<K, V>) -> Multiset<V> {
472    m.dom().fold(Multiset::empty(), |multiset: Multiset<V>, k: K| multiset.insert(m[k]))
473}
474
475proof fn map_values_insert_not_in<K, V>(m: Map<K, V>, k: K, v: V)
476    requires
477        !m.dom().contains(k)
478    ensures
479        map_values(m.insert(k, v)) == map_values(m).insert(v)
480{
481    assume(false);
482}
483
484proof fn map_values_remove<K, V>(m: Map<K, V>, k: K)
485    requires
486        m.dom().contains(k)
487    ensures
488        map_values(m.remove(k)) == map_values(m).remove(m[k])
489{
490    assume(false);
491}
492
493//proof fn map_values_empty_empty<K, V>()
494//    ensures map_values(Map::<K, V>::empty()) == Multiset::empty(),
495
496spec fn fresh(m: Set<int>) -> int {
497    m.find_unique_maximal(|a: int, b: int| a <= b) + 1
498}
499
500proof fn fresh_is_fresh(s: Set<int>)
501    requires s.finite(),
502    ensures !s.contains(fresh(s))
503{
504    assume(false);
505}
506
507proof fn get_key_for_value<K, V>(m: Map<K, V>, value: V) -> (k: K)
508    requires map_values(m).contains(value), m.dom().finite(),
509    ensures m.dom().contains(k), m[k] == value,
510{
511    assume(false);
512    arbitrary()
513}
514
515impl<Element, Token> MultisetToken<Element, Token>
516    where Token: ElementToken<Element>
517{
518    #[verifier::type_invariant]
519    spec fn wf(self) -> bool {
520        self.m.dom().finite() &&
521        forall |k| #[trigger] self.m.dom().contains(k)
522            ==> self.m[k].instance_id() == self.inst
523    }
524
525    pub closed spec fn instance_id(self) -> InstanceId {
526        self.inst
527    }
528
529    spec fn map_elems(m: Map<int, Token>) -> Map<int, Element> {
530        m.map_values(|t: Token| t.element())
531    }
532
533    pub closed spec fn multiset(self) -> Multiset<Element> {
534        map_values(Self::map_elems(self.m))
535    }
536
537    pub proof fn empty(instance_id: InstanceId) -> (tracked s: Self)
538        ensures
539            s.instance_id() == instance_id,
540            s.multiset() === Multiset::empty(),
541    {
542        let tracked s = Self { inst: instance_id, m: Map::tracked_empty(), _v: PhantomData, };
543        broadcast use super::set::fold::lemma_fold_empty;
544        assert(Self::map_elems(Map::empty()) =~= Map::empty());
545        return s;
546    }
547
548    pub proof fn insert(tracked &mut self, tracked token: Token)
549        requires
550            old(self).instance_id() == token.instance_id(),
551        ensures
552            self.instance_id() == old(self).instance_id(),
553            self.multiset() == old(self).multiset().insert(token.element()),
554    {
555        use_type_invariant(&*self);
556        let f = fresh(self.m.dom());
557        fresh_is_fresh(self.m.dom());
558        map_values_insert_not_in(
559            Self::map_elems(self.m),
560            f,
561            token.element());
562        self.m.tracked_insert(f, token);
563        assert(Self::map_elems(self.m) =~= Self::map_elems(old(self).m).insert(
564            f, token.element()));
565        assert(self.multiset() =~= old(self).multiset().insert(token.element()));
566    }
567
568    pub proof fn remove(tracked &mut self, element: Element) -> (tracked token: Token)
569        requires
570            old(self).multiset().contains(element)
571        ensures
572            self.instance_id() == old(self).instance_id(),
573            self.multiset() == old(self).multiset().remove(element),
574            token.instance_id() == self.instance_id(),
575            token.element() == element,
576    {
577        use_type_invariant(&*self);
578        assert(Self::map_elems(self.m).dom() =~= self.m.dom());
579        let k = get_key_for_value(Self::map_elems(self.m), element);
580        map_values_remove(Self::map_elems(self.m), k);
581        let tracked t = self.m.tracked_remove(k);
582        assert(Self::map_elems(self.m) =~= Self::map_elems(old(self).m).remove(k));
583        assert(self.multiset() =~= old(self).multiset().remove(element));
584        t
585    }
586}
587
588pub open spec fn option_value_eq_option_token<Value, Token: ValueToken<Value>>(
589    opt_value: Option<Value>,
590    opt_token: Option<Token>,
591    instance_id: InstanceId,
592) -> bool {
593    match opt_value {
594        Some(val) => opt_token.is_some()
595            && opt_token.unwrap().value() == val
596            && opt_token.unwrap().instance_id() == instance_id,
597        None => opt_token.is_none(),
598    }
599}
600
601pub open spec fn option_value_le_option_token<Value, Token: ValueToken<Value>>(
602    opt_value: Option<Value>,
603    opt_token: Option<Token>,
604    instance_id: InstanceId,
605) -> bool {
606    match opt_value {
607        Some(val) => opt_token.is_some()
608            && opt_token.unwrap().value() == val
609            && opt_token.unwrap().instance_id() == instance_id,
610        None => true,
611    }
612}
613
614pub open spec fn bool_value_eq_option_token<Token: SimpleToken>(
615    b: bool,
616    opt_token: Option<Token>,
617    instance_id: InstanceId,
618) -> bool {
619    if b {
620        opt_token.is_some() && opt_token.unwrap().instance_id() == instance_id
621    } else {
622        opt_token.is_none()
623    }
624}
625
626pub open spec fn bool_value_le_option_token<Token: SimpleToken>(
627    b: bool,
628    opt_token: Option<Token>,
629    instance_id: InstanceId,
630) -> bool {
631    b ==>
632        opt_token.is_some() && opt_token.unwrap().instance_id() == instance_id
633}
634
635}