Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404use super::super::super::modes::*;use super::super::super::prelude::*;use super::super::Loc;use super::super::imap::*;
verus! {
broadcast use super::super::super::group_vstd_default;
pub open spec fn seq_to_map<V>(s: Seq<V>, off: int) -> IMap<int, V> { IMap::new(|i: int| off <= i < off + s.len(), |i: int| s[i - off])}
/** An implementation of a resource for owning a subrange of a sequence.
`GhostSeqAuth<T>` represents authoritative ownership of the entiresequence, and `GhostSubseq<T>` represents client ownership of somesubrange of that sequence. Updating the authoritative `GhostSeqAuth<T>`requires a `GhostSubseq<T>` covering the relevant positions.`GhostSubseq<K, T>`s can be combined or split.
### Example
```fn example_use() { let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0);
// Split the subsequence into a multiple subseqs. let tracked sub2 = sub.split(3);
// In general, we might need to call agree() to establish the fact that // a subseq has the same values as the auth seq. Here, Verus doesn't need // agree because it can track where both the auth and subseq came from. proof { sub.agree(&auth); } proof { sub2.agree(&auth); }
assert(sub[0] == auth[0]); assert(sub2[0] == auth[3]);
// Update the sequence using ownership of subseqs. // The update() method on GhostSubseq updates the entire subrange. proof { sub.update(&mut auth, seq![10u64, 11u64, 12u64]); } assert(auth[0] == 10u64); assert(sub[0] == 10u64);
// The update_subrange_with() method on GhostSeqAuth allows updating // arbitrary parts of a subseq's subrange. proof { auth.update_subrange_with(&mut sub2, 4, seq![24u64, 25u64]); } assert(auth[3] == 3u64); assert(auth[4] == 24u64); assert(sub2[1] == 24u64);
// Not shown in this simple example is the main use case of this resource: // maintaining an invariant between GhostSeqAuth<V> and some exec-mode // shared state with a seq view (e.g., the contents of a file or a disk), // which states that the Seq<V> view of GhostSeqAuth<V> is the same as the // view of the state (e.g., file or disk contents), and then handing out a // GhostSubseq<V> to different clients that might need to operate on // different subranges of the shared state (e.g., different concurrent // transactions that operate on different parts of the file/disk).}```*/
pub tracked struct GhostSeqAuth<V> { ghost off: nat, ghost len: nat, auth: GhostIMapAuth<int, V>,}
pub tracked struct GhostSubseq<V> { ghost off: nat, ghost len: nat, frac: GhostISubmap<int, V>,}
impl<V> GhostSeqAuth<V> { #[verifier::type_invariant] spec fn inv(self) -> bool { &&& self.auth@.dom() =~= ISet::new(|i: int| self.off <= i < self.off + self.len) }
pub closed spec fn id(self) -> Loc { self.auth.id() }
pub closed spec fn view(self) -> Seq<V> { Seq::new(self.len, |i: int| self.auth@[self.off + i]) }
pub open spec fn len(self) -> nat { self@.len() }
pub open spec fn spec_index(self, idx: int) -> V recommends 0 <= idx < self.len(), { self@[idx] }
pub closed spec fn off(self) -> nat { self.off }
pub open spec fn subrange_abs(self, start_inclusive: int, end_exclusive: int) -> Seq<V> recommends self.off() <= start_inclusive <= end_exclusive <= self.off() + self@.len(), { self@[start_inclusive - self.off()..end_exclusive - self.off()] }
pub proof fn new(s: Seq<V>, off: nat) -> (tracked result: (GhostSeqAuth<V>, GhostSubseq<V>)) ensures result.0.off() == off, result.0@ =~= s, result.1.id() == result.0.id(), result.1.off() == off, result.1@ =~= s, { let tracked (mauth, mfrac) = GhostIMapAuth::<int, V>::new(seq_to_map(s, off as int)); let tracked auth = GhostSeqAuth { off: off, len: s.len(), auth: mauth }; let tracked frac = GhostSubseq { off: off, len: s.len(), frac: mfrac }; (auth, frac) }
pub proof fn dummy() -> (tracked result: Self) { let tracked (auth, subseq) = Self::new(Seq::empty(), 0); auth }
pub proof fn agree(tracked self: &GhostSeqAuth<V>, tracked frac: &GhostSubseq<V>) requires self.id() == frac.id(), ensures frac@.len() > 0 ==> { &&& frac@ =~= self@[frac.off() - self.off()..frac.off() - self.off() + frac@.len()] &&& frac.off() >= self.off() &&& frac.off() + frac@.len() <= self.off() + self@.len() }, { frac.agree(self) }
pub proof fn update_subrange_with( tracked self: &mut GhostSeqAuth<V>, tracked frac: &mut GhostSubseq<V>, off: int, v: Seq<V>, ) requires old(self).id() == old(frac).id(), old(frac).off() <= off, off + v.len() <= old(frac).off() + old(frac)@.len(), ensures final(self).id() == old(self).id(), final(frac).id() == old(frac).id(), final(frac).off() == old(frac).off(), final(self)@ =~= old(self)@.update_subrange_with(off - final(self).off(), v), final(frac)@ =~= old(frac)@.update_subrange_with(off - final(frac).off(), v), final(self).off() == old(self).off(), final(frac).off() == old(frac).off(), { let tracked mut mid = frac.split(off - frac.off()); let tracked mut end = mid.split(v.len() as int); mid.update(self, v); frac.combine(mid); frac.combine(end); }}
impl<V> GhostSubseq<V> { #[verifier::type_invariant] spec fn inv(self) -> bool { &&& self.frac@.dom() =~= ISet::new(|i: int| self.off <= i < self.off + self.len) }
pub closed spec fn view(self) -> Seq<V> { Seq::new(self.len, |i: int| self.frac@[self.off + i]) }
pub open spec fn len(self) -> nat { self@.len() }
pub open spec fn spec_index(self, idx: int) -> V recommends 0 <= idx < self.len(), { self@[idx] }
pub open spec fn subrange_abs(self, start_inclusive: int, end_exclusive: int) -> Seq<V> recommends self.off() <= start_inclusive <= end_exclusive <= self.off() + self@.len(), { self@[start_inclusive - self.off()..end_exclusive - self.off()] }
pub closed spec fn off(self) -> nat { self.off }
pub closed spec fn id(self) -> Loc { self.frac.id() }
pub proof fn agree(tracked self: &GhostSubseq<V>, tracked auth: &GhostSeqAuth<V>) requires self.id() == auth.id(), ensures self@.len() > 0 ==> { &&& self@ =~= auth@[self.off() - auth.off()..self.off() - auth.off() + self@.len()] &&& self.off() >= auth.off() &&& self.off() + self@.len() <= auth.off() + auth@.len() }, { use_type_invariant(self); use_type_invariant(auth);
self.frac.agree(&auth.auth);
if self@.len() > 0 { assert(self.frac@.contains_key(self.off as int)); assert(auth.auth@.contains_key(self.off as int));
assert(self.frac@.contains_key(self.off + self.len - 1)); assert(auth.auth@.contains_key(self.off + self.len - 1)); assert(self.off - auth.off + self.len - 1 < auth@.len());
assert forall|i: int| 0 <= i < self.len implies #[trigger] self.frac@[self.off + i] == auth@[self.off - auth.off + i] by { assert(self.frac@.contains_key(self.off + i)); assert(auth.auth@.contains_key(self.off + i)); }; } }
pub proof fn agree_map(tracked self: &GhostSubseq<V>, tracked auth: &GhostIMapAuth<int, V>) requires self.id() == auth.id(), ensures forall|i| 0 <= i < self@.len() ==> #[trigger] auth@.contains_key(self.off() + i) && auth@[self.off() + i] == self@[i], { use_type_invariant(self);
self.frac.agree(&auth);
assert forall|i: int| 0 <= i < self.len implies #[trigger] auth@.contains_key(self.off + i) && self.frac@[self.off + i] == auth@[self.off + i] by { assert(self.frac@.contains_key(self.off + i)); }; }
pub proof fn update( tracked self: &mut GhostSubseq<V>, tracked auth: &mut GhostSeqAuth<V>, v: Seq<V>, ) requires old(self).id() == old(auth).id(), v.len() == old(self)@.len(), ensures final(self).id() == final(auth).id(), final(self).off() == old(self).off(), final(auth).id() == old(auth).id(), final(self)@ =~= v, final(auth)@ =~= old(auth)@.update_subrange_with( final(self).off() - final(auth).off(), v, ), final(self).off() == old(self).off(), final(auth).off() == old(auth).off(), { use_type_invariant(&*self); use_type_invariant(&*auth);
self.update_map(&mut auth.auth, v); }
pub proof fn update_map( tracked self: &mut GhostSubseq<V>, tracked auth: &mut GhostIMapAuth<int, V>, v: Seq<V>, ) requires old(self).id() == old(auth).id(), v.len() == old(self)@.len(), ensures final(self).id() == final(auth).id(), final(self).off() == old(self).off(), final(auth).id() == old(auth).id(), final(self)@ =~= v, final(auth)@ =~= IMap::new( |i: int| old(auth)@.contains_key(i), |i: int| if final(self).off() <= i < final(self).off() + v.len() { v[i - final(self).off()] } else { old(auth)@[i] }, ), { use_type_invariant(&*self);
let vmap = seq_to_map(v, self.off as int); assert(self.frac@.dom() == vmap.dom()); self.frac.agree(auth); self.frac.update(auth, vmap); }
pub proof fn split(tracked self: &mut GhostSubseq<V>, n: int) -> (tracked result: GhostSubseq< V, >) requires 0 <= n <= old(self)@.len(), ensures final(self).id() == old(self).id(), final(self).off() == old(self).off(), result.id() == final(self).id(), result.off() == old(self).off() + n, final(self)@ =~= old(self)@[0..n], result@ =~= old(self)@[n..old(self)@.len()], { let tracked mut mself = Self::dummy(); tracked_swap(self, &mut mself);
use_type_invariant(&mself); let tracked mut mselffrac = mself.frac;
let tracked mfrac = mselffrac.split( ISet::new(|i: int| mself.off + n <= i < mself.off + mself.len), ); let tracked result = GhostSubseq { off: (mself.off + n) as nat, len: (mself.len - n) as nat, frac: mfrac, };
*self = Self { off: mself.off, len: n as nat, frac: mselffrac }; result }
pub proof fn combine(tracked self: &mut GhostSubseq<V>, tracked r: GhostSubseq<V>) requires r.id() == old(self).id(), r.off() == old(self).off() + old(self)@.len(), ensures final(self).id() == old(self).id(), final(self)@ =~= old(self)@ + r@, final(self).off() == old(self).off(), { let tracked mut mself = Self::dummy(); tracked_swap(self, &mut mself);
use_type_invariant(&mself); use_type_invariant(&r); let tracked mut mselffrac = mself.frac;
mselffrac.combine(r.frac); *self = Self { frac: mselffrac, off: mself.off, len: mself.len + r.len }; }
pub proof fn disjoint(tracked &mut self, tracked other: &GhostSubseq<V>) requires old(self).id() == other.id(), ensures final(self).id() == old(self).id(), final(self).off() == old(self).off(), final(self)@ == old(self)@, final(self)@.len() == 0 || other@.len() == 0 || final(self).off() + final(self)@.len() <= other.off() || other.off() + other@.len() <= final(self).off(), { use_type_invariant(&*self); use_type_invariant(other);
self.frac.disjoint(&other.frac); assert(self@.len() == 0 || self.frac@.contains_key(self.off() as int)); assert(other@.len() == 0 || other.frac@.contains_key(other.off() as int)); }
pub proof fn dummy() -> (tracked result: Self) { let tracked (auth, subseq) = GhostSeqAuth::<V>::new(Seq::empty(), 0); subseq }
// Helper to lift GhostISubmap into GhostSubseq. pub proof fn new(off: nat, len: nat, tracked f: GhostISubmap<int, V>) -> (tracked result: GhostSubseq<V>) requires f@.dom() == ISet::new(|i: int| off <= i < off + len), ensures result.id() == f.id(), result.off() == off, result@ == Seq::new(len, |i| f@[off + i]), { GhostSubseq { off: off, len: len, frac: f } }}
} // verus!