ostd/specs/mm/frame/
memory_region_specs.rs

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

ostd/specs/mm/frame/
memory_region_specs.rs
