ostd/specs/mm/
tlb.rs

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

ostd/specs/mm/
tlb.rs
