ostd/specs/mm/frame/
memory_region_specs.rs

1use vstd::prelude::*;
2use vstd_extra::prelude::*;
3
4use crate::specs::arch::MAX_PADDR;
5
6verus! {
7
8pub ghost struct MemRegionModel {
9    pub ghost base: int,
10    pub ghost end: int,
11    pub ghost typ: int,
12}
13
14impl Inv for MemRegionModel {
15    open spec fn inv(self) -> bool {
16        0 <= self.base <= self.end <= MAX_PADDR && 0 <= self.typ < 9
17    }
18}
19
20impl MemRegionModel {
21    pub open spec fn is_sub_region(self, old_region: Self) -> bool {
22        self.typ == old_region.typ && old_region.base <= self.base <= self.end <= old_region.end
23    }
24
25    pub open spec fn is_separate(self, region: Self) -> bool {
26        self.end <= region.base || region.end <= self.base
27    }
28
29    pub open spec fn bad() -> Self {
30        MemRegionModel { base: 0, end: 0, typ: 0 }
31    }
32}
33
34pub ghost struct MemoryRegionArrayModel<const LEN: usize> {
35    pub ghost regions: Seq<MemRegionModel>,
36}
37
38impl<const LEN: usize> Inv for MemoryRegionArrayModel<LEN> {
39    open spec fn inv(self) -> bool {
40        &&& self.regions.len() <= LEN
41    }
42}
43
44impl<const LEN: usize> MemoryRegionArrayModel<LEN> {
45    pub open spec fn new() -> Self {
46        MemoryRegionArrayModel { regions: Seq::empty() }
47    }
48
49    pub open spec fn push(self, region: MemRegionModel) -> Self {
50        MemoryRegionArrayModel { regions: self.regions.push(region) }
51    }
52
53    pub open spec fn full(self) -> bool {
54        self.regions.len() == LEN
55    }
56}
57
58} // verus!
ostd/specs/mm/frame/memory_region_specs.rs

ostd/specs/mm/frame/
memory_region_specs.rs
