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#[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
23pub ghost struct InstanceId(pub int);
27
28pub trait ValueToken<Value> : Sized {
42 spec fn instance_id(&self) -> InstanceId;
43 spec fn value(&self) -> Value;
44
45 proof fn agree(tracked &self, tracked other: &Self)
47 requires self.instance_id() == other.instance_id(),
48 ensures self.value() == other.value();
49
50 proof fn arbitrary() -> (tracked s: Self);
53}
54
55pub trait UniqueValueToken<Value> : ValueToken<Value> {
59 proof fn unique(tracked &mut self, tracked other: &Self)
64 ensures
65 self.instance_id() != other.instance_id(),
66 *self == *old(self);
67}
68
69pub 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 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 proof fn arbitrary() -> (tracked s: Self);
98}
99
100pub trait UniqueKeyValueToken<Key, Value> : KeyValueToken<Key, Value> {
104 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
114pub 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 proof fn arbitrary() -> (tracked s: Self);
152}
153
154pub 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 proof fn arbitrary() -> (tracked s: Self);
174}
175
176pub trait ElementToken<Element> : Sized {
195 spec fn instance_id(&self) -> InstanceId;
196 spec fn element(&self) -> Element;
197
198 proof fn arbitrary() -> (tracked s: Self);
201}
202
203pub trait UniqueElementToken<Element> : ElementToken<Element> {
207 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
217pub trait SimpleToken : Sized {
228 spec fn instance_id(&self) -> InstanceId;
229
230 proof fn arbitrary() -> (tracked s: Self);
233}
234
235pub trait UniqueSimpleToken : SimpleToken {
239 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
493spec 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}