vstd/resource/impls/
seq.rs

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

vstd/resource/impls/
seq.rs
