ostd/specs/mm/
tlb.rs

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

ostd/specs/mm/
tlb.rs
