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

ostd/specs/mm/
tlb.rs
