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

ostd/specs/mm/
tlb.rs
