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

ostd/specs/mm/
tlb.rs
