1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78

#![allow(non_snake_case)]

use super::prelude::*;

#[cfg(verus_keep_ghost)]
use state_machines_macros::*;

#[cfg(verus_keep_ghost)]
tokenized_state_machine_vstd!(Dupe<T> {
    fields {
        #[sharding(storage_option)]
        pub storage: Option<T>,

        #[sharding(constant)]
        pub val: T,
    }

    init!{
        initialize_one(t: T) {
            // Initialize with a single reader
            init storage = Option::Some(t);
            init val = t;
        }
    }

    #[invariant]
    pub fn agreement(&self) -> bool {
        self.storage == Option::Some(self.val)
    }

    property!{
        borrow() {
            guard storage >= Some(pre.val);
        }
    }

     #[inductive(initialize_one)]
     fn initialize_one_inductive(post: Self, t: T) { }
});

#[cfg(verus_keep_ghost)]
verus! {

/// A `tracked ghost` container that you can put a ghost object in.
/// A `Shared<T>` is duplicable and lets you get a `&T` out.
pub tracked struct Shared<T> {
    tracked inst: Dupe::Instance<T>,
}

impl<T> Shared<T> {
    pub closed spec fn view(self) -> T {
        self.inst.val()
    }

    pub proof fn new(tracked t: T) -> (tracked s: Self)
        ensures
            s@ == t,
    {
        let tracked inst = Dupe::Instance::initialize_one(t, Option::Some(t));
        Shared { inst }
    }

    pub proof fn clone(tracked &self) -> (tracked other: Self)
        ensures
            self@ == other@,
    {
        Shared { inst: self.inst.clone() }
    }

    pub proof fn borrow(tracked &self) -> (tracked t: &T)
        ensures
            *t == self@,
    {
        self.inst.borrow()
    }
}

} // verus!