vstd/resource/
seq.rs

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

vstd/resource/
seq.rs
