ostd/specs/mm/
tlb.rs

1use vstd::prelude::*;
2use vstd_extra::ownership::*;
3
4use crate::specs::mm::page_table::*;
5
6use crate::mm::{Paddr, Vaddr, tlb::TlbFlushOp};
7
8verus! {
9
10pub ghost struct TlbModel {
11    pub pending: Seq<TlbFlushOp>,
12    pub mappings: Set<Mapping>,
13}
14
15impl Inv for TlbModel {
16    open spec fn inv(self) -> bool {
17        &&& mappings_well_formed(self.mappings)
18        &&& mappings_disjoint_vaddrs(self.mappings)
19        &&& mappings_disjoint_paddrs(self.mappings)
20    }
21}
22
23impl TlbModel {
24    pub open spec fn update(self, pt: PageTableView, va: Vaddr) -> Self {
25        let m = pt.mappings.filter(|m: Mapping| m.va_range.start <= va < m.va_range.end).choose();
26        TlbModel { pending: self.pending, mappings: self.mappings.insert(m) }
27    }
28
29    pub axiom fn tracked_update(&mut self, pt: PageTableView, va: Vaddr)
30        requires
31            old(self).inv(),
32            forall|m: Mapping|
33                old(self).mappings has m ==> !(m.va_range.start <= va < m.va_range.end),
34            exists|m: Mapping| pt.mappings has m ==> m.va_range.start <= va < m.va_range.end,
35        ensures
36            *final(self) == old(self).update(pt, va),
37    ;
38
39    pub open spec fn flush(self, va: Vaddr) -> Self {
40        let m = self.mappings.filter(|m: Mapping| m.va_range.start <= va < m.va_range.end);
41        TlbModel { pending: self.pending, mappings: self.mappings - m }
42    }
43
44    pub axiom fn tracked_flush(&mut self, va: Vaddr)
45        requires
46            old(self).inv(),
47        ensures
48            *final(self) == old(self).flush(va),
49    ;
50
51    pub open spec fn consistent_with_pt(self, pt: PageTableView) -> bool {
52        self.mappings <= pt.mappings
53    }
54
55    pub proof fn lemma_flush_preserves_inv(self, va: Vaddr)
56        requires
57            self.inv(),
58        ensures
59            self.flush(va).inv(),
60    {
61    }
62
63    pub proof fn lemma_update_preserves_consistent(self, pt: PageTableView, va: Vaddr)
64        requires
65            pt.inv(),
66            self.inv(),
67            self.consistent_with_pt(pt),
68            exists|m: Mapping| pt.mappings has m && m.va_range.start <= va < m.va_range.end,
69        ensures
70            self.update(pt, va).consistent_with_pt(pt),
71    {
72        let filtered = pt.mappings.filter(|m: Mapping| m.va_range.start <= va < m.va_range.end);
73        let m = filtered.choose();
74
75        let witness: Mapping = choose|a: Mapping|
76            pt.mappings has a && a.va_range.start <= va < a.va_range.end;
77        assert(filtered.contains(witness));
78
79        if self.mappings.contains(m) {
80        } else {
81            assert(filtered.contains(m));
82            assert(pt.mappings.contains(m));
83        }
84    }
85
86    pub open spec fn issue_tlb_flush(self, op: TlbFlushOp) -> Self {
87        TlbModel { pending: self.pending.push(op), mappings: self.mappings }
88    }
89
90    pub proof fn tracked_issue_tlb_flush(tracked &mut self, tracked op: TlbFlushOp)
91        requires
92            old(self).inv(),
93        ensures
94            *final(self) == old(self).issue_tlb_flush(op),
95            final(self).inv(),
96    {
97        self.pending.tracked_push(op);
98    }
99
100    pub open spec fn dispatch_tlb_flush_spec(self) -> Self {
101        let op = self.pending.last();
102        let popped = TlbModel {
103            pending: self.pending[..self.pending.len() - 1],
104            mappings: self.mappings,
105        };
106        match op {
107            TlbFlushOp::All => popped,
108            TlbFlushOp::Address(va) => popped.flush(va),
109            TlbFlushOp::Range(range) => popped.flush(range.start),
110        }
111    }
112}
113
114} // verus!
ostd/specs/mm/tlb.rs

ostd/specs/mm/
tlb.rs
