vstd/tokens/
seq.rs

1use super::super::modes::*;
2use super::super::prelude::*;
3use super::map::*;
4
5verus! {
6
7broadcast use super::super::group_vstd_default;
8
9pub open spec fn seq_to_map<V>(s: Seq<V>, off: int) -> Map<int, V> {
10    Map::new(|i: int| off <= i < off + s.len(), |i: int| s[i - off])
11}
12
13/** An implementation of a resource for owning a subrange of a sequence.
14
15`GhostSeqAuth<T>` represents authoritative ownership of the entire
16sequence, and `GhostSubseq<T>` represents client ownership of some
17subrange of that sequence.  Updating the authoritative `GhostSeqAuth<T>`
18requires a `GhostSubseq<T>` covering the relevant positions.
19`GhostSubseq<K, T>`s can be combined or split.
20
21### Example
22
23```
24fn example_use() {
25    let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0);
26
27    // Split the subsequence into a multiple subseqs.
28    let tracked sub2 = sub.split(3);
29
30    // In general, we might need to call agree() to establish the fact that
31    // a subseq has the same values as the auth seq.  Here, Verus doesn't need
32    // agree because it can track where both the auth and subseq came from.
33    proof { sub.agree(&auth); }
34    proof { sub2.agree(&auth); }
35
36    assert(sub[0] == auth[0]);
37    assert(sub2[0] == auth[3]);
38
39    // Update the sequence using ownership of subseqs.
40    // The update() method on GhostSubseq updates the entire subrange.
41    proof { sub.update(&mut auth, seq![10u64, 11u64, 12u64]); }
42    assert(auth[0] == 10u64);
43    assert(sub[0] == 10u64);
44
45    // The update_subrange_with() method on GhostSeqAuth allows updating
46    // arbitrary parts of a subseq's subrange.
47    proof { auth.update_subrange_with(&mut sub2, 4, seq![24u64, 25u64]); }
48    assert(auth[3] == 3u64);
49    assert(auth[4] == 24u64);
50    assert(sub2[1] == 24u64);
51
52    // Not shown in this simple example is the main use case of this resource:
53    // maintaining an invariant between GhostSeqAuth<V> and some exec-mode
54    // shared state with a seq view (e.g., the contents of a file or a disk),
55    // which states that the Seq<V> view of GhostSeqAuth<V> is the same as the
56    // view of the state (e.g., file or disk contents), and then handing out a
57    // GhostSubseq<V> to different clients that might need to operate on
58    // different subranges of the shared state (e.g., different concurrent
59    // transactions that operate on different parts of the file/disk).
60}
61```
62*/
63
64pub struct GhostSeqAuth<V> {
65    ghost off: nat,
66    ghost len: nat,
67    auth: GhostMapAuth<int, V>,
68}
69
70pub struct GhostSubseq<V> {
71    ghost off: nat,
72    ghost len: nat,
73    frac: GhostSubmap<int, V>,
74}
75
76impl<V> GhostSeqAuth<V> {
77    #[verifier::type_invariant]
78    spec fn inv(self) -> bool {
79        &&& self.auth@.dom() =~= Set::new(|i: int| self.off <= i < self.off + self.len)
80    }
81
82    pub closed spec fn id(self) -> int {
83        self.auth.id()
84    }
85
86    pub closed spec fn view(self) -> Seq<V> {
87        Seq::new(self.len, |i: int| self.auth@[self.off + i])
88    }
89
90    pub open spec fn len(self) -> nat {
91        self@.len()
92    }
93
94    pub open spec fn spec_index(self, idx: int) -> V
95        recommends
96            0 <= idx < self.len(),
97    {
98        self@[idx]
99    }
100
101    pub closed spec fn off(self) -> nat {
102        self.off
103    }
104
105    pub open spec fn subrange_abs(self, start_inclusive: int, end_exclusive: int) -> Seq<V>
106        recommends
107            self.off() <= start_inclusive <= end_exclusive <= self.off() + self@.len(),
108    {
109        self@.subrange(start_inclusive - self.off(), end_exclusive - self.off())
110    }
111
112    pub proof fn new(s: Seq<V>, off: nat) -> (tracked result: (GhostSeqAuth<V>, GhostSubseq<V>))
113        ensures
114            result.0.off() == off,
115            result.0@ =~= s,
116            result.1.id() == result.0.id(),
117            result.1.off() == off,
118            result.1@ =~= s,
119    {
120        let tracked (mauth, mfrac) = GhostMapAuth::<int, V>::new(seq_to_map(s, off as int));
121        let tracked auth = GhostSeqAuth { off: off, len: s.len(), auth: mauth };
122        let tracked frac = GhostSubseq { off: off, len: s.len(), frac: mfrac };
123        (auth, frac)
124    }
125
126    pub proof fn dummy() -> (tracked result: Self) {
127        let tracked (auth, subseq) = Self::new(Seq::empty(), 0);
128        auth
129    }
130
131    pub proof fn agree(tracked self: &GhostSeqAuth<V>, tracked frac: &GhostSubseq<V>)
132        requires
133            self.id() == frac.id(),
134        ensures
135            frac@.len() > 0 ==> {
136                &&& frac@ =~= self@.subrange(
137                    frac.off() as int - self.off(),
138                    frac.off() - self.off() + frac@.len() as int,
139                )
140                &&& frac.off() >= self.off()
141                &&& frac.off() + frac@.len() <= self.off() + self@.len()
142            },
143    {
144        frac.agree(self)
145    }
146
147    pub proof fn update_subrange_with(
148        tracked self: &mut GhostSeqAuth<V>,
149        tracked frac: &mut GhostSubseq<V>,
150        off: int,
151        v: Seq<V>,
152    )
153        requires
154            old(self).id() == old(frac).id(),
155            old(frac).off() <= off,
156            off + v.len() <= old(frac).off() + old(frac)@.len(),
157        ensures
158            self.id() == old(self).id(),
159            frac.id() == old(frac).id(),
160            frac.off() == old(frac).off(),
161            self@ =~= old(self)@.update_subrange_with(off - self.off(), v),
162            frac@ =~= old(frac)@.update_subrange_with(off - frac.off(), v),
163            self.off() == old(self).off(),
164            frac.off() == old(frac).off(),
165    {
166        let tracked mut mid = frac.split(off - frac.off());
167        let tracked mut end = mid.split(v.len() as int);
168        mid.update(self, v);
169        frac.combine(mid);
170        frac.combine(end);
171    }
172}
173
174impl<V> GhostSubseq<V> {
175    #[verifier::type_invariant]
176    spec fn inv(self) -> bool {
177        &&& self.frac@.dom() =~= Set::new(|i: int| self.off <= i < self.off + self.len)
178    }
179
180    pub closed spec fn view(self) -> Seq<V> {
181        Seq::new(self.len, |i: int| self.frac@[self.off + i])
182    }
183
184    pub open spec fn len(self) -> nat {
185        self@.len()
186    }
187
188    pub open spec fn spec_index(self, idx: int) -> V
189        recommends
190            0 <= idx < self.len(),
191    {
192        self@[idx]
193    }
194
195    pub open spec fn subrange_abs(self, start_inclusive: int, end_exclusive: int) -> Seq<V>
196        recommends
197            self.off() <= start_inclusive <= end_exclusive <= self.off() + self@.len(),
198    {
199        self@.subrange(start_inclusive - self.off(), end_exclusive - self.off())
200    }
201
202    pub closed spec fn off(self) -> nat {
203        self.off
204    }
205
206    pub closed spec fn id(self) -> int {
207        self.frac.id()
208    }
209
210    pub proof fn agree(tracked self: &GhostSubseq<V>, tracked auth: &GhostSeqAuth<V>)
211        requires
212            self.id() == auth.id(),
213        ensures
214            self@.len() > 0 ==> {
215                &&& self@ =~= auth@.subrange(
216                    self.off() as int - auth.off(),
217                    self.off() - auth.off() + self@.len() as int,
218                )
219                &&& self.off() >= auth.off()
220                &&& self.off() + self@.len() <= auth.off() + auth@.len()
221            },
222    {
223        use_type_invariant(self);
224        use_type_invariant(auth);
225
226        self.frac.agree(&auth.auth);
227
228        if self@.len() > 0 {
229            assert(self.frac@.contains_key(self.off as int));
230            assert(auth.auth@.contains_key(self.off as int));
231
232            assert(self.frac@.contains_key(self.off + self.len - 1));
233            assert(auth.auth@.contains_key(self.off + self.len - 1));
234            assert(self.off - auth.off + self.len - 1 < auth@.len());
235
236            assert forall|i: int| 0 <= i < self.len implies #[trigger] self.frac@[self.off + i]
237                == auth@[self.off - auth.off + i] by {
238                assert(self.frac@.contains_key(self.off + i));
239                assert(auth.auth@.contains_key(self.off + i));
240            };
241        }
242    }
243
244    pub proof fn agree_map(tracked self: &GhostSubseq<V>, tracked auth: &GhostMapAuth<int, V>)
245        requires
246            self.id() == auth.id(),
247        ensures
248            forall|i|
249                0 <= i < self@.len() ==> #[trigger] auth@.contains_key(self.off() + i)
250                    && auth@[self.off() + i] == self@[i],
251    {
252        use_type_invariant(self);
253
254        self.frac.agree(&auth);
255
256        assert forall|i: int| 0 <= i < self.len implies #[trigger] auth@.contains_key(self.off + i)
257            && self.frac@[self.off + i] == auth@[self.off + i] by {
258            assert(self.frac@.contains_key(self.off + i));
259        };
260    }
261
262    pub proof fn update(
263        tracked self: &mut GhostSubseq<V>,
264        tracked auth: &mut GhostSeqAuth<V>,
265        v: Seq<V>,
266    )
267        requires
268            old(self).id() == old(auth).id(),
269            v.len() == old(self)@.len(),
270        ensures
271            self.id() == auth.id(),
272            self.off() == old(self).off(),
273            auth.id() == old(auth).id(),
274            self@ =~= v,
275            auth@ =~= old(auth)@.update_subrange_with(self.off() - auth.off(), v),
276            self.off() == old(self).off(),
277            auth.off() == old(auth).off(),
278    {
279        use_type_invariant(&*self);
280        use_type_invariant(&*auth);
281
282        self.update_map(&mut auth.auth, v);
283    }
284
285    pub proof fn update_map(
286        tracked self: &mut GhostSubseq<V>,
287        tracked auth: &mut GhostMapAuth<int, V>,
288        v: Seq<V>,
289    )
290        requires
291            old(self).id() == old(auth).id(),
292            v.len() == old(self)@.len(),
293        ensures
294            self.id() == auth.id(),
295            self.off() == old(self).off(),
296            auth.id() == old(auth).id(),
297            self@ =~= v,
298            auth@ =~= Map::new(
299                |i: int| old(auth)@.contains_key(i),
300                |i: int|
301                    if self.off() <= i < self.off() + v.len() {
302                        v[i - self.off()]
303                    } else {
304                        old(auth)@[i]
305                    },
306            ),
307    {
308        use_type_invariant(&*self);
309
310        let vmap = seq_to_map(v, self.off as int);
311        assert(self.frac@.dom() == vmap.dom());
312        self.frac.agree(auth);
313        self.frac.update(auth, vmap);
314    }
315
316    pub proof fn split(tracked self: &mut GhostSubseq<V>, n: int) -> (tracked result: GhostSubseq<
317        V,
318    >)
319        requires
320            0 <= n <= old(self)@.len(),
321        ensures
322            self.id() == old(self).id(),
323            self.off() == old(self).off(),
324            result.id() == self.id(),
325            result.off() == old(self).off() + n,
326            self@ =~= old(self)@.subrange(0, n),
327            result@ =~= old(self)@.subrange(n, old(self)@.len() as int),
328    {
329        let tracked mut mself = Self::dummy();
330        tracked_swap(self, &mut mself);
331
332        use_type_invariant(&mself);
333        let tracked mut mselffrac = mself.frac;
334
335        let tracked mfrac = mselffrac.split(
336            Set::new(|i: int| mself.off + n <= i < mself.off + mself.len),
337        );
338        let tracked result = GhostSubseq {
339            off: (mself.off + n) as nat,
340            len: (mself.len - n) as nat,
341            frac: mfrac,
342        };
343
344        *self = Self { off: mself.off, len: n as nat, frac: mselffrac };
345        result
346    }
347
348    pub proof fn combine(tracked self: &mut GhostSubseq<V>, tracked r: GhostSubseq<V>)
349        requires
350            r.id() == old(self).id(),
351            r.off() == old(self).off() + old(self)@.len(),
352        ensures
353            self.id() == old(self).id(),
354            self@ =~= old(self)@ + r@,
355            self.off() == old(self).off(),
356    {
357        let tracked mut mself = Self::dummy();
358        tracked_swap(self, &mut mself);
359
360        use_type_invariant(&mself);
361        use_type_invariant(&r);
362        let tracked mut mselffrac = mself.frac;
363
364        mselffrac.combine(r.frac);
365        *self = Self { frac: mselffrac, off: mself.off, len: mself.len + r.len };
366    }
367
368    pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubseq<V>)
369        requires
370            old(self).id() == other.id(),
371        ensures
372            self.id() == old(self).id(),
373            self.off() == old(self).off(),
374            self@ == old(self)@,
375            self@.len() == 0 || other@.len() == 0 || self.off() + self@.len() <= other.off()
376                || other.off() + other@.len() <= self.off(),
377    {
378        use_type_invariant(&*self);
379        use_type_invariant(other);
380
381        self.frac.disjoint(&other.frac);
382        assert(self@.len() == 0 || self.frac@.contains_key(self.off() as int));
383        assert(other@.len() == 0 || other.frac@.contains_key(other.off() as int));
384    }
385
386    pub proof fn dummy() -> (tracked result: Self) {
387        let tracked (auth, subseq) = GhostSeqAuth::<V>::new(Seq::empty(), 0);
388        subseq
389    }
390
391    // Helper to lift GhostSubmap into GhostSubseq.
392    pub proof fn new(off: nat, len: nat, tracked f: GhostSubmap<int, V>) -> (tracked result:
393        GhostSubseq<V>)
394        requires
395            f@.dom() == Set::new(|i: int| off <= i < off + len),
396        ensures
397            result.id() == f.id(),
398            result.off() == off,
399            result@ == Seq::new(len, |i| f@[off + i]),
400    {
401        GhostSubseq { off: off, len: len, frac: f }
402    }
403}
404
405} // verus!
vstd/tokens/seq.rs

vstd/tokens/
seq.rs
