vstd/
shared.rs

1#![allow(non_snake_case)]
2
3use super::prelude::*;
4
5#[cfg(verus_keep_ghost)]
6use verus_state_machines_macros::*;
7
8#[cfg(verus_keep_ghost)]
9tokenized_state_machine_vstd!(Dupe<T> {
10    fields {
11        #[sharding(storage_option)]
12        pub storage: Option<T>,
13
14        #[sharding(constant)]
15        pub val: T,
16    }
17
18    init!{
19        initialize_one(t: T) {
20            // Initialize with a single reader
21            init storage = Option::Some(t);
22            init val = t;
23        }
24    }
25
26    #[invariant]
27    pub fn agreement(&self) -> bool {
28        self.storage == Option::Some(self.val)
29    }
30
31    property!{
32        borrow() {
33            guard storage >= Some(pre.val);
34        }
35    }
36
37     #[inductive(initialize_one)]
38     fn initialize_one_inductive(post: Self, t: T) { }
39});
40
41#[cfg(verus_keep_ghost)]
42verus! {
43
44/// A `tracked ghost` container that you can put a ghost object in.
45/// A `Shared<T>` is duplicable and lets you get a `&T` out.
46pub tracked struct Shared<T> {
47    tracked inst: Dupe::Instance<T>,
48}
49
50impl<T> Shared<T> {
51    pub closed spec fn view(self) -> T {
52        self.inst.val()
53    }
54
55    pub proof fn new(tracked t: T) -> (tracked s: Self)
56        ensures
57            s@ == t,
58    {
59        let tracked inst = Dupe::Instance::initialize_one(t, Option::Some(t));
60        Shared { inst }
61    }
62
63    pub proof fn clone(tracked &self) -> (tracked other: Self)
64        ensures
65            self@ == other@,
66    {
67        Shared { inst: self.inst.clone() }
68    }
69
70    pub proof fn borrow(tracked &self) -> (tracked t: &T)
71        ensures
72            *t == self@,
73    {
74        self.inst.borrow()
75    }
76}
77
78} // verus!
vstd/shared.rs

vstd/
shared.rs
