ostd/arch/x86/mm/
mod.rs

1// SPDX-License-Identifier: MPL-2.0
2#![expect(dead_code)]
3
4use vstd::{arithmetic::power2::*, prelude::*};
5use vstd_extra::{
6    panic::{may_panic, panic_diverge},
7    prelude::*,
8};
9
10use alloc::fmt;
11use core::ops::Range;
12
13//use cfg_if::cfg_if;
14pub(crate) use util::{__memcpy_fallible, __memset_fallible};
15//use x86_64::{instructions::tlb, structures::paging::PhysFrame, VirtAddr};
16
17use crate::{
18    mm::{
19        page_prop::{CachePolicy, PageFlags, PageProperty, PrivilegedPageFlags as PrivFlags},
20        page_table::{PageTableEntryTrait, PageTableFrag},
21        Paddr, PagingConstsTrait, PagingLevel, PodOnce, Vaddr, MAX_PADDR,
22    },
23    Pod,
24};
25
26mod util;
27
28verus! {
29
30/* Const-generic page-table layouts and the architecture model share these
31 * executable constants without depending on definitions in specs::arch::x86.
32 * PAGE_SIZE, NR_ENTRIES, and NR_LEVELS move here unchanged from that module.
33 * The other names expose the literals already returned by the accessors below.
34 * Origin Rust:
35 * pub const PAGE_SIZE: usize = 4096;
36 * pub const NR_ENTRIES: usize = 512;
37 * pub const NR_LEVELS: usize = 4;
38 * Origin Rust: <none; new executable code> for PTE_SIZE, ADDRESS_WIDTH,
39 * HIGHEST_TRANSLATION_LEVEL, and VA_SIGN_EXT.
40 */
41/// Size of a base page on x86-64.
42pub const PAGE_SIZE: usize = 4096;
43
44/// Size of an x86-64 page-table entry.
45pub const PTE_SIZE: usize = 8;
46
47/// Number of entries in an x86-64 page-table node.
48pub const NR_ENTRIES: usize = 512;
49
50/// Number of translation levels used by the current x86-64 configuration.
51pub const NR_LEVELS: usize = 4;
52
53/// Width of canonical virtual addresses used by the current configuration.
54pub const ADDRESS_WIDTH: usize = 48;
55
56/// Highest level at which a PTE may directly map a page.
57pub const HIGHEST_TRANSLATION_LEVEL: PagingLevel = 2;
58
59/// Whether virtual addresses use sign extension.
60pub const VA_SIGN_EXT: bool = true;
61
62#[verifier::allow(autoderive_clone_without_spec)]
63#[derive(Clone, Debug, Default)]
64pub struct PagingConsts {}
65
66/* Origin Rust:
67 * impl PagingConstsTrait for PagingConsts {
68 *     const BASE_PAGE_SIZE: usize = 4096;
69 *     const NR_LEVELS: PagingLevel = 4;
70 *     const ADDRESS_WIDTH: usize = 48;
71 *     const VA_SIGN_EXT: bool = true;
72 *     const HIGHEST_TRANSLATION_LEVEL: PagingLevel = 2;
73 *     const PTE_SIZE: usize = core::mem::size_of::<PageTableEntry>();
74 * }
75 */
76impl PagingConstsTrait for PagingConsts {
77    #[verifier::inline]
78    open spec fn BASE_PAGE_SIZE_spec() -> usize {
79        PAGE_SIZE
80    }
81
82    #[inline(always)]
83    fn BASE_PAGE_SIZE() -> usize
84    {
85        PAGE_SIZE
86    }
87
88    #[verifier::inline]
89    open spec fn NR_LEVELS_spec() -> PagingLevel {
90        NR_LEVELS as PagingLevel
91    }
92
93    #[inline(always)]
94    fn NR_LEVELS() -> PagingLevel
95    {
96        NR_LEVELS as PagingLevel
97    }
98
99    #[verifier::inline]
100    open spec fn ADDRESS_WIDTH_spec() -> usize {
101        ADDRESS_WIDTH
102    }
103
104    #[inline(always)]
105    fn ADDRESS_WIDTH() -> usize
106    {
107        ADDRESS_WIDTH
108    }
109
110    #[verifier::inline]
111    open spec fn HIGHEST_TRANSLATION_LEVEL_spec() -> PagingLevel {
112        HIGHEST_TRANSLATION_LEVEL
113    }
114
115    #[inline(always)]
116    fn HIGHEST_TRANSLATION_LEVEL() -> PagingLevel
117    {
118        HIGHEST_TRANSLATION_LEVEL
119    }
120
121    #[verifier::inline]
122    open spec fn VA_SIGN_EXT_spec() -> bool {
123        VA_SIGN_EXT
124    }
125
126    #[inline(always)]
127    fn VA_SIGN_EXT() -> bool {
128        VA_SIGN_EXT
129    }
130
131    #[verifier::inline]
132    open spec fn PTE_SIZE_spec() -> usize {
133        PTE_SIZE
134    }
135
136    #[inline(always)]
137    fn PTE_SIZE() -> (res: usize)
138    {
139        PTE_SIZE
140    }
141
142    proof fn lemma_paging_consts_requirements()
143    {
144        assert(Self::BASE_PAGE_SIZE() == PAGE_SIZE) by (compute_only);
145        assert(Self::NR_LEVELS() == NR_LEVELS as PagingLevel) by (compute_only);
146        assert(Self::HIGHEST_TRANSLATION_LEVEL() == HIGHEST_TRANSLATION_LEVEL) by (compute_only);
147        assert(Self::PTE_SIZE() == PTE_SIZE) by (compute_only);
148        assert(Self::ADDRESS_WIDTH() == ADDRESS_WIDTH) by (compute_only);
149        lemma_pow2_is_pow2_to64();
150        lemma2_to64();
151        lemma2_to64_rest();
152
153        vstd::layout::unsigned_int_max_values();
154        lemma_usize_pow2_ilog2(12);
155        lemma_usize_pow2_ilog2(9);
156        lemma_pow2_adds(9, 39);
157    }
158}
159
160pub proof fn lemma_nr_subpage_per_huge_eq_nr_entries()
161    ensures
162        crate::mm::nr_subpage_per_huge::<PagingConsts>() == NR_ENTRIES,
163{
164    assert(crate::mm::nr_subpage_per_huge::<PagingConsts>() == 4096usize / 8usize);
165    assert(NR_ENTRIES == 512usize);
166}
167}
168
169bitflags::bitflags! {
170    //#[derive(Pod)]
171    //#[repr(C)]
172    /// Possible flags for a page table entry.
173    pub struct PageTableFlags: usize {
174        /// Specifies whether the mapped frame or page table is loaded in memory.
175        const PRESENT =         1usize << 0;
176        /// Controls whether writes to the mapped frames are allowed.
177        const WRITABLE =        1usize << 1;
178        /// Controls whether accesses from userspace (i.e. ring 3) are permitted.
179        const USER =            1usize << 2;
180        /// If this bit is set, a “write-through” policy is used for the cache, else a “write-back”
181        /// policy is used.
182        const WRITE_THROUGH =   1usize << 3;
183        /// Disables caching for the pointed entry is cacheable.
184        const NO_CACHE =        1usize << 4;
185        /// Whether this entry has been used for linear-address translation.
186        const ACCESSED =        1usize << 5;
187        /// Whether the memory area represented by this entry is modified.
188        const DIRTY =           1usize << 6;
189        /// In level 2 or 3 it indicates that it map to a huge page.
190        /// In level 1, it is the PAT (page attribute table) bit.
191        /// We use this bit in level 1, 2 and 3 to indicate that this entry is
192        /// "valid". For levels above 3, `PRESENT` is used for "valid".
193        const HUGE =            1usize << 7;
194        /// Indicates that the mapping is present in all address spaces, so it isn't flushed from
195        /// the TLB on an address space switch.
196        const GLOBAL =          1usize << 8;
197        /// TDX shared bit.
198        #[cfg(feature = "cvm_guest")]
199        const SHARED =          1usize << 51;
200
201        /// Ignored by the hardware. Free to use.
202        const HIGH_IGN1 =       1usize << 52;
203        /// Ignored by the hardware. Free to use.
204        const HIGH_IGN2 =       1usize << 53;
205
206        /// Forbid execute codes on the page. The NXE bits in EFER msr must be set.
207        const NO_EXECUTE =      1usize << 63;
208    }
209}
210
211verus! {
212
213/// Flush any TLB entry that contains the map of the given virtual address.
214///
215/// This flush performs regardless of the global-page bit. So it can flush both global
216/// and non-global entries.
217#[verifier::external_body]
218pub(crate) fn tlb_flush_addr(vaddr: Vaddr) {
219    //tlb::flush(VirtAddr::new(vaddr as u64));
220    unimplemented!()
221}
222
223/// Flush any TLB entry that intersects with the given address range.
224#[verifier::external_body]
225pub(crate) fn tlb_flush_addr_range(range: &Range<Vaddr>) {
226    // for vaddr in range.clone().step_by(PAGE_SIZE) {
227    //    tlb_flush_addr(vaddr);
228    //}
229    unimplemented!()
230}
231
232/// Flush all TLB entries except for the global-page entries.
233#[verifier::external_body]
234pub(crate) fn tlb_flush_all_excluding_global() {
235    //tlb::flush_all();
236    unimplemented!()
237}
238
239/// Flush all TLB entries, including global-page entries.
240#[verifier::external_body]
241pub(crate) fn tlb_flush_all_including_global() {
242    /* // SAFETY: updates to CR4 here only change the global-page bit, the side effect
243    // is only to invalidate the TLB, which doesn't affect the memory safety.
244    unsafe {
245        // To invalidate all entries, including global-page
246        // entries, disable global-page extensions (CR4.PGE=0).
247        x86_64::registers::control::Cr4::update(|cr4| {
248            *cr4 -= x86_64::registers::control::Cr4Flags::PAGE_GLOBAL;
249        });
250        x86_64::registers::control::Cr4::update(|cr4| {
251            *cr4 |= x86_64::registers::control::Cr4Flags::PAGE_GLOBAL;
252        });
253    }*/
254}
255
256#[derive(Clone, Copy/*, Pod, Default*/)]
257#[derive(Debug)]
258#[repr(C)]
259pub struct PageTableEntry(usize);
260
261global layout PageTableEntry is size == 8, align == 8;
262
263#[verus_verify]
264unsafe impl Pod for PageTableEntry {
265
266}
267
268impl PageTableEntry {
269    pub proof fn lemma_layout()
270        ensures
271            core::mem::size_of::<PageTableEntry>() == 8,
272            core::mem::align_of::<PageTableEntry>() == 8,
273            core::mem::size_of::<PageTableEntry>() % core::mem::align_of::<PageTableEntry>() == 0,
274    {
275        broadcast use VERUS_layout_of_PageTableEntry;
276    }
277
278    pub closed spec fn default_spec() -> Self {
279        Self(0)
280    }
281}
282
283impl Default for PageTableEntry {
284    fn default() -> (ret: Self)
285        ensures
286            ret.paddr() == 0,
287        returns
288            Self::default_spec(),
289    {
290        proof {
291            lemma_page_property_flag_constants();
292            assert(Self::default_spec().paddr_spec() == 0) by (compute);
293        }
294        Self(usize::default())
295    }
296}
297
298/// Activates the given level 4 page table.
299/// The cache policy of the root page table node is controlled by `root_pt_cache`.
300///
301/// # Safety
302///
303/// Changing the level 4 page table is unsafe, because it's possible to violate memory safety by
304/// changing the page mapping.
305#[verifier::external_body]
306pub unsafe fn activate_page_table(root_paddr: Paddr, root_pt_cache: CachePolicy) {
307    /*let addr = PhysFrame::from_start_address(x86_64::PhysAddr::new(root_paddr as u64)).unwrap();
308    let flags = match root_pt_cache {
309        CachePolicy::Writeback => x86_64::registers::control::Cr3Flags::empty(),
310        CachePolicy::Writethrough => x86_64::registers::control::Cr3Flags::PAGE_LEVEL_WRITETHROUGH,
311        CachePolicy::Uncacheable => x86_64::registers::control::Cr3Flags::PAGE_LEVEL_CACHE_DISABLE,
312        _ => panic!("unsupported cache policy for the root page table"),
313    };
314
315    // SAFETY: The safety is upheld by the caller.
316    unsafe { x86_64::registers::control::Cr3::write(addr, flags) };*/
317    unimplemented!()
318}
319
320pub uninterp spec fn current_page_table_paddr_spec() -> Paddr;
321
322} // verus!
323
324#[verus_verify]
325#[verifier::external_body]
326#[verifier::when_used_as_spec(current_page_table_paddr_spec)]
327#[verus_spec(
328    returns
329        current_page_table_paddr_spec(),
330)]
331pub fn current_page_table_paddr() -> Paddr {
332    /* x86_64::registers::control::Cr3::read_raw()
333    .0
334    .start_address()
335    .as_u64() as Paddr*/
336    unimplemented!()
337}
338
339verus! {
340
341impl PageTableEntry {
342    //cfg_if! {
343    //if #[cfg(feature = "cvm_guest")] {
344    //    const PHYS_ADDR_MASK: usize = 0x7_FFFF_FFFF_F000;
345    //} else {
346    const PHYS_ADDR_MASK: usize = 0xF_FFFF_FFFF_F000;
347
348    //}
349    //}
350    // const PROP_MASK: usize = !Self::PHYS_ADDR_MASK & !PageTableFlags::HUGE.bits();
351    const PROP_MASK: usize = !Self::PHYS_ADDR_MASK & !0x80usize;
352}
353
354/// Parse a bit-flag bits `val` in the representation of `from` to `to` in bits.
355macro_rules! parse_flags {
356    ($val:expr, $from:expr, $to:expr) => {
357        ($val as usize & $from.bits() as usize) >> $from.bits().ilog2() << $to.bits().ilog2()
358    };
359}
360
361impl PodOnce for PageTableEntry {
362
363}
364
365impl PageTableEntryTrait for PageTableEntry {
366    fn new_absent() -> Self {
367        proof {
368            lemma_auxiliary_bit_properties(0);
369            Self::lemma_page_table_entry_properties();
370            assert(Self::default_spec() == Self::new_absent_spec());
371        }
372        Self::default()
373    }
374
375    fn is_present(&self) -> bool {
376        // For PT child, `PRESENT` should be set; for huge page, `HUGE` should
377        // be set; for the leaf child page, `PAT`, which is the same bit as
378        // the `HUGE` bit in upper levels, should be set.
379        self.0 & PageTableFlags::PRESENT().bits() != 0 || self.0 & PageTableFlags::HUGE().bits()
380            != 0
381    }
382
383    open spec fn new_page_req(paddr: Paddr, _level: PagingLevel, prop: PageProperty) -> bool {
384        &&& prop.inv()
385        &&& prop.flags.bits() & PageFlags::R().bits() == PageFlags::R().bits()
386        &&& (!(prop.cache is Writeback || prop.cache is Writethrough || prop.cache is Uncacheable)
387            ==> may_panic())
388    }
389
390    fn new_page(paddr: Paddr, _level: PagingLevel, prop: PageProperty) -> Self {
391        let flags = PageTableFlags::HUGE().bits();
392        let mut pte = Self(paddr & Self::PHYS_ADDR_MASK | flags);
393        proof {
394            lemma_auxiliary_bit_properties(paddr);
395            assert(pte.set_prop_req(prop));
396            assert((paddr & Self::PHYS_ADDR_MASK | flags) & Self::PHYS_ADDR_MASK
397                == paddr & Self::PHYS_ADDR_MASK) by (bit_vector)
398                requires
399                    flags == PageTableFlags::HUGE().bits();
400            assert(paddr < MAX_PADDR ==> (paddr & Self::PHYS_ADDR_MASK | flags)
401                & Self::PHYS_ADDR_MASK == paddr & !((PAGE_SIZE - 1) as usize))
402                by (bit_vector)
403                requires
404                    flags == PageTableFlags::HUGE().bits();
405            assert(((paddr & Self::PHYS_ADDR_MASK | flags) & PageTableFlags::HUGE().bits()) != 0)
406                by (bit_vector)
407                requires
408                    flags == PageTableFlags::HUGE().bits();
409            assert(pte.is_last(_level));
410        }
411        pte.set_prop(prop);
412        pte
413    }
414
415    fn new_pt(paddr: Paddr) -> (res: Self) {
416        // In x86 if it's an intermediate PTE, it's better to have the same permissions
417        // as the most permissive child (to reduce hardware page walk accesses). But we
418        // don't have a mechanism to keep it generic across architectures, thus just
419        // setting it to be the most permissive.
420        let flags = PageTableFlags::PRESENT().bits()
421            | PageTableFlags::WRITABLE().bits()
422            | PageTableFlags::USER().bits();
423        proof {
424            Self::lemma_page_table_entry_properties();
425            lemma_auxiliary_bit_properties(paddr);
426            assert(paddr < MAX_PADDR ==> paddr & Self::PHYS_ADDR_MASK == paddr & !((PAGE_SIZE
427                - 1) as usize)) by (bit_vector);
428            assert((Self(paddr & Self::PHYS_ADDR_MASK | flags)) == Self::new_pt(paddr));
429        }
430        Self(paddr & Self::PHYS_ADDR_MASK | flags)
431    }
432
433    fn paddr(&self) -> Paddr {
434        proof {
435            self.lemma_paddr_is_page_aligned();
436        }
437        self.0 & Self::PHYS_ADDR_MASK
438    }
439
440    fn prop(&self) -> PageProperty {
441        proof {
442            lemma_auxiliary_bit_properties(self.0);
443            lemma_page_property_flag_constants();
444        }
445        let flags = (parse_flags!(self.0, PageTableFlags::PRESENT(), PageFlags::R()))
446            | (parse_flags!(self.0, PageTableFlags::WRITABLE(), PageFlags::W()))
447            | (parse_flags!(!self.0, PageTableFlags::NO_EXECUTE(), PageFlags::X()))
448            | (parse_flags!(self.0, PageTableFlags::ACCESSED(), PageFlags::ACCESSED()))
449            | (parse_flags!(self.0, PageTableFlags::DIRTY(), PageFlags::DIRTY()))
450            | (parse_flags!(self.0, PageTableFlags::HIGH_IGN1(), PageFlags::AVAIL1()))
451            | (parse_flags!(self.0, PageTableFlags::HIGH_IGN2(), PageFlags::AVAIL2()));
452        let priv_flags = (parse_flags!(self.0, PageTableFlags::USER(), PrivFlags::USER()))
453            | (parse_flags!(self.0, PageTableFlags::GLOBAL(), PrivFlags::GLOBAL()));
454        #[cfg(feature = "cvm_guest")]
455        let priv_flags =
456            priv_flags | (parse_flags!(self.0, PageTableFlags::SHARED(), PrivFlags::SHARED()));
457        let cache = if self.0 & PageTableFlags::NO_CACHE().bits() != 0 {
458            CachePolicy::Uncacheable
459        } else if self.0 & PageTableFlags::WRITE_THROUGH().bits() != 0 {
460            CachePolicy::Writethrough
461        } else {
462            CachePolicy::Writeback
463        };
464        proof {
465            lemma_parse_flags_collorary(self.0);
466            lemma_x86_page_flags_wf(self.0, flags);
467            assert(flags & PageFlags::all().bits() as usize == flags);
468            #[cfg(not(feature = "cvm_guest"))]
469            {
470                lemma_x86_priv_flags_wf(self.0, priv_flags);
471            }
472            #[cfg(feature = "cvm_guest")]
473            {
474                lemma_parse_shared_to_priv_shared_equiv_if(self.0);
475                lemma_x86_priv_flags_cvm_wf(self.0, priv_flags);
476            }
477            let spec_prop = self.prop();
478            assert(cache == spec_prop.cache);
479            assert(PageFlags::from_bits(flags as u8)->0 == spec_prop.flags);
480            assert(PrivFlags::from_bits(priv_flags as u8)->0 == spec_prop.priv_flags);
481        }
482        PageProperty {
483            flags: PageFlags::from_bits(flags as u8).unwrap(),
484            cache,
485            priv_flags: PrivFlags::from_bits(priv_flags as u8).unwrap(),
486        }
487    }
488
489    open spec fn set_prop_req(self, prop: PageProperty) -> bool {
490        &&& prop.inv()
491        &&& prop.flags.bits() & PageFlags::R().bits() == PageFlags::R().bits()
492        &&& (!(prop.cache is Writeback || prop.cache is Writethrough || prop.cache is Uncacheable)
493            ==> may_panic())
494    }
495
496    fn set_prop(&mut self, prop: PageProperty)
497        ensures
498            old(self).is_present() ==> final(self).as_usize() == Self::raw_set_prop_spec(
499                old(self).as_usize(),
500                prop,
501            ),
502    {
503        proof {
504            lemma_auxiliary_bit_properties(0);
505            lemma_page_property_flag_constants();
506        }
507        if !self.is_present() {
508            return;
509        }
510        let mut flags = PageTableFlags::empty().bits();
511        flags = flags |
512            (parse_flags!(prop.flags.bits(), PageFlags::R(), PageTableFlags::PRESENT()))
513            | (parse_flags!(prop.flags.bits(), PageFlags::W(), PageTableFlags::WRITABLE()))
514            | (parse_flags!(!prop.flags.bits(), PageFlags::X(), PageTableFlags::NO_EXECUTE()))
515            | (parse_flags!(
516                prop.flags.bits(),
517                PageFlags::ACCESSED(),
518                PageTableFlags::ACCESSED()
519            ))
520            | (parse_flags!(prop.flags.bits(), PageFlags::DIRTY(), PageTableFlags::DIRTY()))
521            | (parse_flags!(
522                prop.flags.bits(),
523                PageFlags::AVAIL1(),
524                PageTableFlags::HIGH_IGN1()
525            ))
526            | (parse_flags!(
527                prop.flags.bits(),
528                PageFlags::AVAIL2(),
529                PageTableFlags::HIGH_IGN2()
530            ))
531            | (parse_flags!(
532                prop.priv_flags.bits(),
533                PrivFlags::USER(),
534                PageTableFlags::USER()
535            ))
536            | (parse_flags!(
537                prop.priv_flags.bits(),
538                PrivFlags::GLOBAL(),
539                PageTableFlags::GLOBAL()
540            ));
541        #[cfg(feature = "cvm_guest")]
542        {
543            flags = flags |
544            parse_flags!(
545                prop.priv_flags.bits(),
546                PrivFlags::SHARED(),
547                PageTableFlags::SHARED()
548            );
549        }
550        proof {
551            let ghost cache_flags = if prop.cache is Writethrough {
552                PageTableFlags::WRITE_THROUGH().bits()
553            } else if prop.cache is Uncacheable {
554                PageTableFlags::NO_CACHE().bits()
555            } else {
556                0usize
557            };
558            match prop.cache {
559                CachePolicy::Writeback => {
560                    assert(flags == flags | cache_flags) by (bit_vector)
561                        requires
562                            cache_flags == 0usize;
563                },
564                _ => {},
565            }
566        }
567        match prop.cache {
568            CachePolicy::Writeback => {},
569            CachePolicy::Writethrough => {
570                flags |= PageTableFlags::WRITE_THROUGH().bits();
571            },
572            CachePolicy::Uncacheable => {
573                flags |= PageTableFlags::NO_CACHE().bits();
574            },
575            _ => {
576                //panic!("unsupported cache policy");
577                panic_diverge();
578            },
579        }
580        proof {
581            assert(flags == PageProperty::encode_prop_flags_spec(prop));
582        }
583        self.0 = self.0 & !Self::PROP_MASK | flags;
584        proof {
585            lemma_x86_set_prop_roundtrip(old(self).0, flags, prop);
586        }
587    }
588
589    fn is_last(&self, _level: PagingLevel) -> bool {
590        self.0 & PageTableFlags::HUGE().bits() != 0
591    }
592
593    fn as_usize(self) -> usize {
594        self.0
595    }
596
597    open spec fn new_absent_spec() -> Self {
598        Self::default_spec()
599    }
600
601    open spec fn is_present_spec(&self) -> bool {
602        self.as_usize() & PageTableFlags::PRESENT().bits() != 0 || self.as_usize()
603            & PageTableFlags::HUGE().bits() != 0
604    }
605
606    closed spec fn paddr_spec(&self) -> Paddr {
607        self.as_usize() & Self::PHYS_ADDR_MASK
608    }
609
610    closed spec fn prop_spec(&self) -> PageProperty {
611        PageProperty {
612            flags: PageFlags::from_bits(PageProperty::decode_page_flags_spec(self.0))->0,
613            cache: PageProperty::decode_cache_spec(self.0),
614            priv_flags: PrivFlags::from_bits(PageProperty::decode_priv_flags_spec(self.0))->0,
615        }
616    }
617
618    closed spec fn new_pt_spec(paddr: Paddr) -> Self {
619        let flags = PageTableFlags::PRESENT().bits() | PageTableFlags::WRITABLE().bits()
620            | PageTableFlags::USER().bits();
621        Self(paddr & Self::PHYS_ADDR_MASK | flags)
622    }
623
624    closed spec fn new_page_spec(paddr: Paddr, level: PagingLevel, prop: PageProperty) -> Self {
625        let flags = PageTableFlags::HUGE().bits();
626        let pte = paddr & Self::PHYS_ADDR_MASK | flags;
627        match prop.cache {
628            CachePolicy::Writeback |
629            CachePolicy::Writethrough |
630            CachePolicy::Uncacheable => Self(Self::raw_set_prop_spec(pte, prop)),
631            _ => arbitrary(),
632        }
633    }
634
635    open spec fn is_last_spec(&self, _level: PagingLevel) -> bool {
636        self.as_usize() & PageTableFlags::HUGE().bits() != 0
637    }
638
639    closed spec fn as_usize_spec(self) -> usize {
640        self.0
641    }
642
643    proof fn lemma_page_table_entry_properties() {
644        Self::lemma_layout();
645        lemma_page_property_flag_constants();
646        lemma_auxiliary_bit_properties(0);
647
648        assert forall|level: PagingLevel|
649            1 < level implies !(#[trigger]Self::new_absent().is_last(level))
650        by {
651            assert(Self::new_absent().as_usize() == 0);
652        }
653
654        assert forall|paddr: Paddr, level: PagingLevel, prop: PageProperty|
655            #![trigger Self::new_page(paddr, level, prop)]
656            Self::new_page_req(paddr, level, prop) && (prop.cache is Writeback
657                || prop.cache is Writethrough || prop.cache is Uncacheable) implies {
658                &&& Self::new_page(paddr, level, prop).is_present()
659                &&& (paddr < MAX_PADDR ==> Self::new_page(paddr, level, prop).paddr() == paddr
660                    & !((PAGE_SIZE - 1) as usize))
661                &&& (paddr < MAX_PADDR && paddr % PAGE_SIZE == 0 ==> Self::new_page(
662                    paddr,
663                    level,
664                    prop,
665                ).paddr() == paddr)
666                &&& Self::new_page(paddr, level, prop).prop() == prop
667                &&& Self::new_page(paddr, level, prop).is_last(level)
668            }
669        by {
670            let raw = paddr & Self::PHYS_ADDR_MASK | PageTableFlags::HUGE().bits();
671            let flags = PageProperty::encode_prop_flags_spec(prop);
672            lemma_auxiliary_bit_properties(paddr);
673            lemma_auxiliary_bit_properties(raw);
674            lemma_x86_set_prop_roundtrip(raw, flags, prop);
675            assert(raw & Self::PHYS_ADDR_MASK == paddr & Self::PHYS_ADDR_MASK) by (bit_vector)
676                requires
677                    raw == (paddr & 0xF_FFFF_FFFF_F000usize | 0x80usize),
678                    Self::PHYS_ADDR_MASK == 0xF_FFFF_FFFF_F000usize;
679            assert(paddr < MAX_PADDR ==> raw & Self::PHYS_ADDR_MASK == paddr & !((PAGE_SIZE
680                - 1) as usize)) by (bit_vector)
681                requires
682                    raw == (paddr & 0xF_FFFF_FFFF_F000usize | 0x80usize),
683                    Self::PHYS_ADDR_MASK == 0xF_FFFF_FFFF_F000usize,
684                    PAGE_SIZE == 4096usize,
685                    MAX_PADDR == 0x8000_0000usize;
686            assert(raw & PageTableFlags::HUGE().bits() != 0) by (bit_vector)
687                requires
688                    raw == (paddr & 0xF_FFFF_FFFF_F000usize | 0x80usize),
689                    PageTableFlags::HUGE().bits() == 0x80usize;
690            assert(PageTableEntry(raw).is_last(level));
691            assert(Self::new_page(paddr, level, prop).is_last(level));
692        }
693
694        assert forall|paddr: Paddr| #![trigger Self::new_pt(paddr)] {
695                &&& Self::new_pt(paddr).is_present()
696                &&& (paddr < MAX_PADDR ==> Self::new_pt(paddr).paddr() == paddr & !((PAGE_SIZE
697                    - 1) as usize))
698                &&& (paddr < MAX_PADDR && paddr % PAGE_SIZE == 0 ==> Self::new_pt(paddr).paddr()
699                    == paddr)
700                &&& forall|level: PagingLevel| !Self::new_pt(paddr).is_last(level)
701            }
702        by {
703            let flags = PageTableFlags::PRESENT().bits() | PageTableFlags::WRITABLE().bits()
704                | PageTableFlags::USER().bits();
705            lemma_auxiliary_bit_properties(paddr);
706            assert(flags == 0x7usize) by (bit_vector)
707                requires
708                    flags == 0x1usize | 0x2usize | 0x4usize;
709            assert(paddr < MAX_PADDR ==> (paddr & Self::PHYS_ADDR_MASK | flags)
710                & Self::PHYS_ADDR_MASK == paddr & !((PAGE_SIZE - 1) as usize)) by (bit_vector)
711                requires
712                    Self::PHYS_ADDR_MASK == 0xF_FFFF_FFFF_F000usize,
713                    flags == 0x7usize,
714                    PAGE_SIZE == 4096usize,
715                    MAX_PADDR == 0x8000_0000usize;
716            assert((paddr & Self::PHYS_ADDR_MASK | flags) & PageTableFlags::PRESENT().bits() != 0)
717                by (bit_vector)
718                requires
719                    Self::PHYS_ADDR_MASK == 0xF_FFFF_FFFF_F000usize,
720                    flags == 0x7usize,
721                    PageTableFlags::PRESENT().bits() == 0x1usize;
722            assert forall|level: PagingLevel| !Self::new_pt(paddr).is_last(level) by {
723                assert((paddr & Self::PHYS_ADDR_MASK | flags) & PageTableFlags::HUGE().bits()
724                    == 0) by (bit_vector)
725                    requires
726                        Self::PHYS_ADDR_MASK == 0xF_FFFF_FFFF_F000usize,
727                        flags == 0x7usize,
728                        PageTableFlags::HUGE().bits() == 0x80usize;
729            }
730        }
731    }
732
733    proof fn lemma_paddr_is_page_aligned(self) {
734        lemma_auxiliary_bit_properties(self.0);
735    }
736}
737
738impl PageTableEntry {
739    pub closed spec fn raw_set_prop_spec(old_raw: usize, prop: PageProperty) -> usize {
740        old_raw & !Self::PROP_MASK | PageProperty::encode_prop_flags_spec(prop)
741    }
742}
743
744// Auxiliary definitions and lemmas about bit properties of page table entries and flags.
745impl PageProperty {
746    closed spec fn encode_prop_flags_spec(prop: Self) -> usize {
747        let flags = PageTableFlags::empty().bits()
748            | parse_flags!(prop.flags.bits(), PageFlags::R(), PageTableFlags::PRESENT())
749            | parse_flags!(prop.flags.bits(), PageFlags::W(), PageTableFlags::WRITABLE())
750            | parse_flags!(!prop.flags.bits(), PageFlags::X(), PageTableFlags::NO_EXECUTE())
751            | parse_flags!(prop.flags.bits(), PageFlags::ACCESSED(), PageTableFlags::ACCESSED())
752            | parse_flags!(prop.flags.bits(), PageFlags::DIRTY(), PageTableFlags::DIRTY())
753            | parse_flags!(prop.flags.bits(), PageFlags::AVAIL1(), PageTableFlags::HIGH_IGN1())
754            | parse_flags!(prop.flags.bits(), PageFlags::AVAIL2(), PageTableFlags::HIGH_IGN2())
755            | parse_flags!(prop.priv_flags.bits(), PrivFlags::USER(), PageTableFlags::USER())
756            | parse_flags!(prop.priv_flags.bits(), PrivFlags::GLOBAL(), PageTableFlags::GLOBAL());
757        #[cfg(feature = "cvm_guest")]
758        let flags = flags
759            | parse_flags!(prop.priv_flags.bits(), PrivFlags::SHARED(), PageTableFlags::SHARED());
760        flags | if prop.cache is Writeback {
761            0
762        } else if prop.cache is Writethrough {
763            PageTableFlags::WRITE_THROUGH().bits()
764        } else {
765            PageTableFlags::NO_CACHE().bits()
766        }
767    }
768
769    closed spec fn decode_page_flags_spec(raw: usize) -> u8 {
770        let flags = if raw & PageTableFlags::PRESENT().bits() != 0 {
771            PageFlags::R().bits()
772        } else {
773            0
774        } | if raw & PageTableFlags::WRITABLE().bits() != 0 {
775            PageFlags::W().bits()
776        } else {
777            0
778        } | if !raw & PageTableFlags::NO_EXECUTE().bits() != 0 {
779            PageFlags::X().bits()
780        } else {
781            0
782        } | if raw & PageTableFlags::ACCESSED().bits() != 0 {
783            PageFlags::ACCESSED().bits()
784        } else {
785            0
786        } | if raw & PageTableFlags::DIRTY().bits() != 0 {
787            PageFlags::DIRTY().bits()
788        } else {
789            0
790        } | if raw & PageTableFlags::HIGH_IGN1().bits() != 0 {
791            PageFlags::AVAIL1().bits()
792        } else {
793            0
794        } | if raw & PageTableFlags::HIGH_IGN2().bits() != 0 {
795            PageFlags::AVAIL2().bits()
796        } else {
797            0
798        };
799        flags
800    }
801
802    closed spec fn decode_priv_flags_spec(raw: usize) -> u8 {
803        let priv_flags = if raw & PageTableFlags::USER().bits() != 0 {
804            PrivFlags::USER().bits()
805        } else {
806            0
807        } | if raw & PageTableFlags::GLOBAL().bits() != 0 {
808            PrivFlags::GLOBAL().bits()
809        } else {
810            0
811        };
812        #[cfg(feature = "cvm_guest")]
813        let priv_flags = priv_flags | if raw & PageTableFlags::SHARED().bits() != 0 {
814            PrivFlags::SHARED().bits()
815        } else {
816            0
817        };
818        priv_flags
819    }
820
821    closed spec fn decode_cache_spec(raw: usize) -> CachePolicy {
822        if raw & PageTableFlags::NO_CACHE().bits() != 0 {
823            CachePolicy::Uncacheable
824        } else if raw & PageTableFlags::WRITE_THROUGH().bits() != 0 {
825            CachePolicy::Writethrough
826        } else {
827            CachePolicy::Writeback
828        }
829    }
830}
831
832#[verifier::bit_vector]
833proof fn lemma_auxiliary_bit_properties(addr: usize)
834    ensures
835        addr % PAGE_SIZE == 0 ==> addr == (addr & !((PAGE_SIZE - 1) as usize)),
836        (addr & PageTableEntry::PHYS_ADDR_MASK) % PAGE_SIZE == 0,
837        addr < MAX_PADDR ==> (addr & PageTableEntry::PHYS_ADDR_MASK) < MAX_PADDR,
838{
839}
840
841proof fn lemma_page_property_flag_constants()
842    ensures
843        0 & PageTableEntry::PHYS_ADDR_MASK == 0,
844        0usize % PAGE_SIZE == 0,
845        0 < MAX_PADDR,
846        0 & PageTableFlags::PRESENT().bits() == 0,
847        0 & PageTableFlags::HUGE().bits() == 0,
848        PageTableFlags::PRESENT().bits() == 0x1,
849        PageTableFlags::WRITABLE().bits() == 0x2,
850        PageTableFlags::USER().bits() == 0x4,
851        PageTableFlags::WRITE_THROUGH().bits() == 0x8,
852        PageTableFlags::NO_CACHE().bits() == 0x10,
853        PageTableFlags::ACCESSED().bits() == 0x20,
854        PageTableFlags::DIRTY().bits() == 0x40,
855        PageTableFlags::HUGE().bits() == 0x80,
856        PageTableFlags::GLOBAL().bits() == 0x100,
857        #[cfg(feature = "cvm_guest")]
858        (PageTableFlags::SHARED().bits() == 0x0200_0000_0000_0000),
859        PageTableFlags::HIGH_IGN1().bits() == 0x0010_0000_0000_0000,
860        PageTableFlags::HIGH_IGN2().bits() == 0x0020_0000_0000_0000,
861        PageTableFlags::NO_EXECUTE().bits() == 0x8000000000000000,
862        PageTableFlags::PRESENT().bits().ilog2() == 0,
863        PageTableFlags::WRITABLE().bits().ilog2() == 1,
864        PageTableFlags::USER().bits().ilog2() == 2,
865        PageTableFlags::WRITE_THROUGH().bits().ilog2() == 3,
866        PageTableFlags::NO_CACHE().bits().ilog2() == 4,
867        PageTableFlags::ACCESSED().bits().ilog2() == 5,
868        PageTableFlags::DIRTY().bits().ilog2() == 6,
869        PageTableFlags::HUGE().bits().ilog2() == 7,
870        PageTableFlags::GLOBAL().bits().ilog2() == 8,
871        #[cfg(feature = "cvm_guest")]
872        (PageTableFlags::SHARED().bits().ilog2() == 51),
873        PageTableFlags::HIGH_IGN1().bits().ilog2() == 52,
874        PageTableFlags::HIGH_IGN2().bits().ilog2() == 53,
875        PageTableFlags::NO_EXECUTE().bits().ilog2() == 63,
876        PageFlags::R().bits() == 0x1,
877        PageFlags::W().bits() == 0x2,
878        PageFlags::X().bits() == 0x4,
879        PageFlags::ACCESSED().bits() == 0x8,
880        PageFlags::DIRTY().bits() == 0x10,
881        PageFlags::AVAIL1().bits() == 0x40,
882        PageFlags::AVAIL2().bits() == 0x80,
883        PageFlags::all().bits() == 0xDFu8,
884        PageFlags::R().bits().ilog2() == 0,
885        PageFlags::W().bits().ilog2() == 1,
886        PageFlags::X().bits().ilog2() == 2,
887        PageFlags::ACCESSED().bits().ilog2() == 3,
888        PageFlags::DIRTY().bits().ilog2() == 4,
889        PageFlags::AVAIL1().bits().ilog2() == 6,
890        PageFlags::AVAIL2().bits().ilog2() == 7,
891        PrivFlags::USER().bits() == 0x1,
892        PrivFlags::GLOBAL().bits() == 0x2,
893        #[cfg(not(all(target_arch = "x86_64", feature = "cvm_guest")))]
894        PrivFlags::all().bits() == 0x3u8,
895        PrivFlags::USER().bits().ilog2() == 0,
896        PrivFlags::GLOBAL().bits().ilog2() == 1,
897        #[cfg(all(target_arch = "x86_64", feature = "cvm_guest"))]
898        (PrivFlags::SHARED().bits() == 0x80),
899        #[cfg(all(target_arch = "x86_64", feature = "cvm_guest"))]
900        (PrivFlags::all().bits() == 0x83u8),
901        #[cfg(all(target_arch = "x86_64", feature = "cvm_guest"))]
902        (PrivFlags::SHARED().bits().ilog2() == 7),
903{
904    lemma_usize_ilog2_to32();
905    lemma_u8_ilog2_to8();
906    lemma_u64_ilog2_to64();
907    assert(0 & PageTableEntry::PHYS_ADDR_MASK == 0) by (compute_only);
908    assert(0usize % PAGE_SIZE == 0) by (compute_only);
909    assert(0 < MAX_PADDR) by (compute_only);
910    assert(PageTableFlags::PRESENT().bits() == 0x1) by (compute);
911    assert(PageTableFlags::WRITABLE().bits() == 0x2) by (compute);
912    assert(PageTableFlags::USER().bits() == 0x4) by (compute);
913    assert(PageTableFlags::WRITE_THROUGH().bits() == 0x8) by (compute);
914    assert(PageTableFlags::NO_CACHE().bits() == 0x10) by (compute);
915    assert(PageTableFlags::ACCESSED().bits() == 0x20) by (compute);
916    assert(PageTableFlags::DIRTY().bits() == 0x40) by (compute);
917    assert(PageTableFlags::HUGE().bits() == 0x80) by (compute);
918    assert(PageTableFlags::GLOBAL().bits() == 0x100) by (compute);
919    assert(0 & PageTableFlags::PRESENT().bits() == 0) by (bit_vector);
920    assert(0 & PageTableFlags::HUGE().bits() == 0) by (bit_vector);
921    #[cfg(feature = "cvm_guest")]
922    {
923        assert(PageTableFlags::SHARED().bits() == 0x0200_0000_0000_0000) by (compute);
924    }
925    assert(PageTableFlags::HIGH_IGN1().bits() == 0x0010_0000_0000_0000) by (compute);
926    assert(PageTableFlags::HIGH_IGN2().bits() == 0x0020_0000_0000_0000) by (compute);
927    assert(PageTableFlags::NO_EXECUTE().bits() == 0x8000000000000000) by (compute);
928    broadcast use PageFlags::lemma_consts;
929    broadcast use PrivFlags::lemma_consts;
930
931    PageFlags::lemma_all_constant();
932    assert((0u8 | 0x1u8 | 0x2u8 | 0x4u8 | 0x3u8 | 0x5u8 | 0x7u8 | 0x8u8 | 0x10u8
933        | 0x40u8 | 0x80u8) == 0xDFu8) by (bit_vector);
934    #[cfg(not(all(target_arch = "x86_64", feature = "cvm_guest")))]
935    {
936        PrivFlags::lemma_all_constant();
937        assert((0u8 | 0x1u8 | 0x2u8 | 0u8) == 0x3u8) by (bit_vector);
938    }
939    #[cfg(all(target_arch = "x86_64", feature = "cvm_guest"))]
940    {
941        PrivFlags::lemma_all_constant();
942        assert((0u8 | 0x1u8 | 0x2u8 | 0x80u8) == 0x83u8) by (bit_vector);
943    }
944}
945
946#[cfg(all(target_arch = "x86_64", feature = "cvm_guest"))]
947proof fn lemma_parse_shared_to_priv_shared_equiv_if(v: usize)
948    ensures
949        parse_flags!(v, PageTableFlags::SHARED(), PrivFlags::SHARED()) == if v
950            & PageTableFlags::SHARED().bits() != 0 {
951            PrivFlags::SHARED().bits() as usize
952        } else {
953            0usize
954        },
955{
956    lemma_page_property_flag_constants();
957    assert(parse_flags!(v, PageTableFlags::SHARED(), PrivFlags::SHARED()) == ((v
958        & 0x0200_0000_0000_0000usize) >> 51 << 7)) by (compute);
959    assert(((v & 0x0200_0000_0000_0000usize) >> 51 << 7) == (if (v & 0x0200_0000_0000_0000usize)
960        != 0 {
961        0x80usize
962    } else {
963        0usize
964    })) by (bit_vector);
965}
966
967proof fn lemma_parse_flags_equiv_if(v: usize)
968    ensures
969        parse_flags!(v, PageTableFlags::PRESENT(), PageFlags::R()) == if v
970            & PageTableFlags::PRESENT().bits() != 0 {
971            PageFlags::R().bits()
972        } else {
973            0
974        },
975        parse_flags!(v, PageTableFlags::WRITABLE(), PageFlags::W()) == if v
976            & PageTableFlags::WRITABLE().bits() != 0 {
977            PageFlags::W().bits()
978        } else {
979            0
980        },
981        parse_flags!(!v, PageTableFlags::NO_EXECUTE(), PageFlags::X()) == if !v
982            & PageTableFlags::NO_EXECUTE().bits() != 0 {
983            PageFlags::X().bits()
984        } else {
985            0
986        },
987        parse_flags!(v, PageTableFlags::ACCESSED(), PageFlags::ACCESSED()) == if v
988            & PageTableFlags::ACCESSED().bits() != 0 {
989            PageFlags::ACCESSED().bits()
990        } else {
991            0
992        },
993        parse_flags!(v, PageTableFlags::DIRTY(), PageFlags::DIRTY()) == if v
994            & PageTableFlags::DIRTY().bits() != 0 {
995            PageFlags::DIRTY().bits()
996        } else {
997            0
998        },
999        parse_flags!(v, PageTableFlags::HIGH_IGN1(), PageFlags::AVAIL1()) == if v
1000            & PageTableFlags::HIGH_IGN1().bits() != 0 {
1001            PageFlags::AVAIL1().bits()
1002        } else {
1003            0
1004        },
1005        parse_flags!(v, PageTableFlags::HIGH_IGN2(), PageFlags::AVAIL2()) == if v
1006            & PageTableFlags::HIGH_IGN2().bits() != 0 {
1007            PageFlags::AVAIL2().bits()
1008        } else {
1009            0
1010        },
1011        parse_flags!(v, PageTableFlags::USER(), PrivFlags::USER()) == if v
1012            & PageTableFlags::USER().bits() != 0 {
1013            PrivFlags::USER().bits()
1014        } else {
1015            0
1016        },
1017        parse_flags!(v, PageTableFlags::GLOBAL(), PrivFlags::GLOBAL()) == if v
1018            & PageTableFlags::GLOBAL().bits() != 0 {
1019            PrivFlags::GLOBAL().bits()
1020        } else {
1021            0
1022        },
1023{
1024    lemma_page_property_flag_constants();
1025    assert(((v & 0x1usize) >> 0 << 0) == (if (v & 0x1usize) != 0 {
1026        0x1usize
1027    } else {
1028        0usize
1029    })) by (bit_vector);
1030    assert(((v & 0x2usize) >> 1 << 1) == (if (v & 0x2usize) != 0 {
1031        0x2usize
1032    } else {
1033        0usize
1034    })) by (bit_vector);
1035    assert((((!v & 0x8000_0000_0000_0000usize) >> 63) << 2) == (if (!v & 0x8000_0000_0000_0000usize)
1036        != 0 {
1037        0x4usize
1038    } else {
1039        0usize
1040    })) by (bit_vector);
1041    assert(((v & 0x20usize) >> 5 << 3) == (if (v & 0x20usize) != 0 {
1042        0x8usize
1043    } else {
1044        0usize
1045    })) by (bit_vector);
1046    assert(((v & 0x40usize) >> 6 << 4) == (if (v & 0x40usize) != 0 {
1047        0x10usize
1048    } else {
1049        0usize
1050    })) by (bit_vector);
1051    assert(((v & 0x0010_0000_0000_0000usize) >> 52 << 6) == (if (v & 0x0010_0000_0000_0000usize)
1052        != 0 {
1053        0x40usize
1054    } else {
1055        0usize
1056    })) by (bit_vector);
1057    assert(((v & 0x0020_0000_0000_0000usize) >> 53 << 7) == (if (v & 0x0020_0000_0000_0000usize)
1058        != 0 {
1059        0x80usize
1060    } else {
1061        0usize
1062    })) by (bit_vector);
1063    assert(((v & 0x4usize) >> 2 << 0) == (if (v & 0x4usize) != 0 {
1064        0x1usize
1065    } else {
1066        0usize
1067    })) by (bit_vector);
1068    assert(((v & 0x100usize) >> 8 << 1) == (if (v & 0x100usize) != 0 {
1069        0x2usize
1070    } else {
1071        0usize
1072    })) by (bit_vector);
1073}
1074
1075proof fn lemma_parse_flags_collorary(v: usize)
1076    ensures
1077        (parse_flags!(v, PageTableFlags::PRESENT(), PageFlags::R())) | (
1078        parse_flags!(v, PageTableFlags::WRITABLE(), PageFlags::W())) | (
1079        parse_flags!(!v, PageTableFlags::NO_EXECUTE(), PageFlags::X())) | (
1080        parse_flags!(v, PageTableFlags::ACCESSED(), PageFlags::ACCESSED())) | (
1081        parse_flags!(v, PageTableFlags::DIRTY(), PageFlags::DIRTY())) | (
1082        parse_flags!(v, PageTableFlags::HIGH_IGN1(), PageFlags::AVAIL1())) | (
1083        parse_flags!(v, PageTableFlags::HIGH_IGN2(), PageFlags::AVAIL2())) ==
1084        PageProperty::decode_page_flags_spec(v),
1085        (parse_flags!(v, PageTableFlags::USER(), PrivFlags::USER())) | (
1086        parse_flags!(v, PageTableFlags::GLOBAL(), PrivFlags::GLOBAL())) ==
1087        PageProperty::decode_priv_flags_spec(v),
1088{
1089    lemma_parse_flags_equiv_if(v);
1090}
1091
1092#[verifier::bit_vector]
1093proof fn lemma_x86_page_flags_wf(v: usize, flags: usize)
1094    requires
1095        flags == (if v & 0x1usize != 0 {
1096            0x1usize
1097        } else {
1098            0
1099        } | if v & 0x2usize != 0 {
1100            0x2usize
1101        } else {
1102            0
1103        } | if !v & 0x8000_0000_0000_0000usize != 0 {
1104            0x4usize
1105        } else {
1106            0
1107        } | if v & 0x20usize != 0 {
1108            0x8usize
1109        } else {
1110            0
1111        } | if v & 0x40usize != 0 {
1112            0x10usize
1113        } else {
1114            0
1115        } | if v & 0x0010_0000_0000_0000usize != 0 {
1116            0x40usize
1117        } else {
1118            0
1119        } | if v & 0x0020_0000_0000_0000usize != 0 {
1120            0x80usize
1121        } else {
1122            0
1123        }),
1124    ensures
1125        flags <= 255usize,
1126        flags & 0xDFusize == flags,
1127{
1128}
1129
1130#[verifier::bit_vector]
1131proof fn lemma_x86_priv_flags_wf(v: usize, priv_flags: usize)
1132    requires
1133        priv_flags == (if v & 0x4usize != 0 {
1134            0x1usize
1135        } else {
1136            0
1137        } | if v & 0x100usize != 0 {
1138            0x2usize
1139        } else {
1140            0
1141        }),
1142    ensures
1143        priv_flags <= 255usize,
1144        priv_flags & 0x3usize == priv_flags,
1145{
1146}
1147
1148#[cfg(feature = "cvm_guest")]
1149#[verifier::bit_vector]
1150proof fn lemma_x86_priv_flags_cvm_wf(v: usize, priv_flags: usize)
1151    requires
1152        priv_flags == (if v & 0x4usize != 0 {
1153            0x1usize
1154        } else {
1155            0
1156        } | if v & 0x100usize != 0 {
1157            0x2usize
1158        } else {
1159            0
1160        } | if v & 0x0200_0000_0000_0000usize != 0 {
1161            0x80usize
1162        } else {
1163            0
1164        }),
1165    ensures
1166        priv_flags <= 255usize,
1167        priv_flags & 0x83usize == priv_flags,
1168{
1169}
1170
1171/// It is the same as `PageProperty::encode_prop_flags_spec`, but all constants are expanded to support bit_vector.
1172closed spec fn encode_prop_flags_bv_spec(
1173    pbits: usize,
1174    priv_bits: usize,
1175    cache_flags: usize,
1176) -> usize {
1177    (if pbits & 0x1usize != 0 { 0x1usize } else { 0 })
1178        | (if pbits & 0x2usize != 0 { 0x2usize } else { 0 })
1179        | (if !pbits & 0x4usize != 0 { 0x8000_0000_0000_0000usize } else { 0 })
1180        | (if pbits & 0x8usize != 0 { 0x20usize } else { 0 })
1181        | (if pbits & 0x10usize != 0 { 0x40usize } else { 0 })
1182        | (if pbits & 0x40usize != 0 { 0x0010_0000_0000_0000usize } else { 0 })
1183        | (if pbits & 0x80usize != 0 { 0x0020_0000_0000_0000usize } else { 0 })
1184        | (if priv_bits & 0x1usize != 0 { 0x4usize } else { 0 })
1185        | (if priv_bits & 0x2usize != 0 { 0x100usize } else { 0 })
1186        | cache_flags
1187}
1188
1189proof fn lemma_encode_prop_flags_matches(
1190    pbits: u8,
1191    priv_bits: u8,
1192    cache_flags: usize,
1193)
1194    requires
1195        cache_flags == 0usize || cache_flags == 0x8usize || cache_flags == 0x10usize,
1196    ensures
1197        (PageTableFlags::empty().bits()
1198            | parse_flags!(pbits, PageFlags::R(), PageTableFlags::PRESENT())
1199            | parse_flags!(pbits, PageFlags::W(), PageTableFlags::WRITABLE())
1200            | parse_flags!(!pbits, PageFlags::X(), PageTableFlags::NO_EXECUTE())
1201            | parse_flags!(pbits, PageFlags::ACCESSED(), PageTableFlags::ACCESSED())
1202            | parse_flags!(pbits, PageFlags::DIRTY(), PageTableFlags::DIRTY())
1203            | parse_flags!(pbits, PageFlags::AVAIL1(), PageTableFlags::HIGH_IGN1())
1204            | parse_flags!(pbits, PageFlags::AVAIL2(), PageTableFlags::HIGH_IGN2())
1205            | parse_flags!(priv_bits, PrivFlags::USER(), PageTableFlags::USER())
1206            | parse_flags!(priv_bits, PrivFlags::GLOBAL(), PageTableFlags::GLOBAL())
1207            | cache_flags)
1208            == encode_prop_flags_bv_spec(pbits as usize, priv_bits as usize, cache_flags),
1209{
1210    lemma_page_property_flag_constants();
1211    assert((0usize
1212        | ((pbits as usize & 0x1usize) >> 0 << 0)
1213        | ((pbits as usize & 0x2usize) >> 1 << 1)
1214        | (((!pbits) as usize & 0x4usize) >> 2 << 63)
1215        | ((pbits as usize & 0x8usize) >> 3 << 5)
1216        | ((pbits as usize & 0x10usize) >> 4 << 6)
1217        | ((pbits as usize & 0x40usize) >> 6 << 52)
1218        | ((pbits as usize & 0x80usize) >> 7 << 53)
1219        | ((priv_bits as usize & 0x1usize) >> 0 << 2)
1220        | ((priv_bits as usize & 0x2usize) >> 1 << 8)
1221        | cache_flags)
1222        == encode_prop_flags_bv_spec(pbits as usize, priv_bits as usize, cache_flags)) by (bit_vector);
1223}
1224
1225#[verifier::bit_vector]
1226proof fn lemma_x86_set_prop_decode_bits(
1227    old_raw: usize,
1228    flags: usize,
1229    pbits: usize,
1230    priv_bits: usize,
1231    cache_flags: usize,
1232)
1233    requires
1234        pbits & 0xDFusize == pbits,
1235        priv_bits & 0x3usize == priv_bits,
1236        cache_flags == 0usize || cache_flags == 0x8usize || cache_flags == 0x10usize,
1237        flags == encode_prop_flags_bv_spec(pbits, priv_bits, cache_flags),
1238    ensures
1239        flags & PageTableEntry::PHYS_ADDR_MASK == 0,
1240        pbits & 0x1usize == 0x1usize ==> flags & 0x1usize == 0x1usize,
1241        {
1242            let new_raw = old_raw
1243                & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits())
1244                | flags;
1245            let decoded_flags = (if new_raw & 0x1usize != 0 { 0x1usize } else { 0 })
1246                | (if new_raw & 0x2usize != 0 { 0x2usize } else { 0 })
1247                | (if !new_raw & 0x8000_0000_0000_0000usize != 0 { 0x4usize } else { 0 })
1248                | (if new_raw & 0x20usize != 0 { 0x8usize } else { 0 })
1249                | (if new_raw & 0x40usize != 0 { 0x10usize } else { 0 })
1250                | (if new_raw & 0x0010_0000_0000_0000usize != 0 { 0x40usize } else { 0 })
1251                | (if new_raw & 0x0020_0000_0000_0000usize != 0 { 0x80usize } else { 0 });
1252            decoded_flags == pbits
1253        },
1254        {
1255            let new_raw = old_raw
1256                & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits())
1257                | flags;
1258            let decoded_priv_flags = (if new_raw & 0x4usize != 0 { 0x1usize } else { 0 })
1259                | (if new_raw & 0x100usize != 0 { 0x2usize } else { 0 });
1260            decoded_priv_flags == priv_bits
1261        },
1262        {
1263            let new_raw = old_raw
1264                & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits())
1265                | flags;
1266            new_raw & 0x10usize != 0 <==> cache_flags == 0x10usize
1267        },
1268        {
1269            let new_raw = old_raw
1270                & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits())
1271                | flags;
1272            new_raw & 0x8usize != 0 <==> cache_flags == 0x8usize
1273        },
1274{
1275}
1276
1277proof fn lemma_x86_set_prop_roundtrip(old_raw: usize, flags: usize, prop: PageProperty)
1278    requires
1279        prop.inv(),
1280        prop.flags.bits() & PageFlags::R().bits() == PageFlags::R().bits(),
1281        prop.cache is Writeback || prop.cache is Writethrough || prop.cache is Uncacheable,
1282        flags == PageProperty::encode_prop_flags_spec(prop),
1283    ensures
1284        PageTableEntry(
1285            old_raw & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits()) | flags,
1286        ).prop() == prop,
1287        PageTableEntry(
1288            old_raw & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits()) | flags,
1289        ).paddr() == PageTableEntry(old_raw).paddr(),
1290        PageTableEntry(
1291            old_raw & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits()) | flags,
1292        ).is_present(),
1293        forall|level: PagingLevel|
1294            #[trigger] PageTableEntry(old_raw).is_last(level) ==> PageTableEntry(
1295                old_raw & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits())
1296                    | flags,
1297            ).is_last(level),
1298{
1299    lemma_page_property_flag_constants();
1300    let pbits_u8 = prop.flags.bits();
1301    let priv_bits_u8 = prop.priv_flags.bits();
1302    let pbits = pbits_u8 as usize;
1303    let priv_bits = priv_bits_u8 as usize;
1304    let cache_flags = if prop.cache is Writethrough {
1305        PageTableFlags::WRITE_THROUGH().bits()
1306    } else if prop.cache is Uncacheable {
1307        PageTableFlags::NO_CACHE().bits()
1308    } else {
1309        0usize
1310    };
1311    lemma_encode_prop_flags_matches(pbits_u8, priv_bits_u8, cache_flags);
1312    let new_raw = old_raw & !(!PageTableEntry::PHYS_ADDR_MASK & !PageTableFlags::HUGE().bits())
1313        | flags;
1314    lemma_x86_set_prop_decode_bits(old_raw, flags, pbits, priv_bits, cache_flags);
1315    lemma_x86_set_prop_preserves_entry_bits(old_raw, new_raw, flags);
1316    let decoded_flags = PageProperty::decode_page_flags_spec(new_raw);
1317    let decoded_priv_flags = PageProperty::decode_priv_flags_spec(new_raw);
1318    PageFlags::lemma_from_bits_bits(decoded_flags as u8);
1319    PrivFlags::lemma_from_bits_bits(decoded_priv_flags as u8);
1320    PageFlags::lemma_eq_from_bits(PageTableEntry(new_raw).prop().flags, prop.flags);
1321    PrivFlags::lemma_eq_from_bits(PageTableEntry(new_raw).prop().priv_flags, prop.priv_flags);
1322}
1323
1324#[verifier::bit_vector]
1325proof fn lemma_x86_set_prop_preserves_entry_bits(old_raw: usize, new_raw: usize, flags: usize)
1326    requires
1327        new_raw == old_raw & !(!PageTableEntry::PHYS_ADDR_MASK & !0x80usize) | flags,
1328        flags & PageTableEntry::PHYS_ADDR_MASK == 0,
1329        flags & 0x1usize == 0x1usize,
1330    ensures
1331        (new_raw & PageTableEntry::PHYS_ADDR_MASK) == (old_raw & PageTableEntry::PHYS_ADDR_MASK),
1332        new_raw & 0x1usize != 0 || new_raw & 0x80usize != 0,
1333        old_raw & 0x80usize != 0 ==> new_raw & 0x80usize != 0,
1334{
1335}
1336
1337} // verus!
1338  /*
1339  impl fmt::Debug for PageTableEntry {
1340      fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
1341          let mut f = f.debug_struct("PageTableEntry");
1342          f.field("raw", &format_args!("{:#x}", self.0))
1343              .field("paddr", &format_args!("{:#x}", self.paddr()))
1344              .field("present", &self.is_present())
1345              .field(
1346                  "flags",
1347                  &PageTableFlags::from_bits_truncate(self.0 & !Self::PHYS_ADDR_MASK),
1348              )
1349              .field("prop", &self.prop())
1350              .finish()
1351      }
1352  }
1353  */
ostd/arch/x86/mm/mod.rs

ostd/arch/x86/mm/
mod.rs
