finish page allocator verification

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

Author: lgaeher

.github/workflows/verify.yml

@@ -17,7 +17,7 @@ jobs:
     - name: Install opam dependencies
       run: sudo apt update -y && sudo apt install -y pkg-config git rsync tar unzip m4 time curl ocaml build-essential bubblewrap gawk libgmp-dev python3 python-is-python3 libmpfr-dev && python3 -m pip install setuptools
     - name: Install opam
-      run: curl "https://github.com/ocaml/opam/releases/download/2.1.5/opam-2.1.5-x86_64-linux" -Lo /usr/local/bin/opam && chmod +x /usr/local/bin/opam
+      run: curl "https://github.com/ocaml/opam/releases/download/2.5.0/opam-2.5.0-x86_64-linux" -Lo /usr/local/bin/opam && chmod +x /usr/local/bin/opam
     - name: Setup opam
       run: opam init -y
     - name: Setup opam switch
@@ -63,12 +63,14 @@ jobs:
           python3 .github/workflows/prune_dune_modules.py verification/rust_proofs/ace/proofs/dune \
             proof_core_page_allocator_allocator_PageAllocator_add_memory_region \
             proof_core_page_allocator_allocator_PageStorageTreeNode_store_page_token \
+            proof_core_page_allocator_allocator_PageStorageTreeNode_acquire_page_token \
             proof_core_page_allocator_allocator_PageStorageTreeNode_divide_page_token_if_necessary \
+            proof_core_page_allocator_allocator_PageStorageTreeNode_try_to_merge_page_tokens \
             proof_core_page_allocator_allocator_PageAllocator_find_largest_page_size \
             proof_core_page_allocator_page_Page_T_write \
             proof_core_page_allocator_page_Page_core_page_allocator_page_Allocated_read \
-            proof_core_page_allocator_allocator_PageStorageTreeNode_store_page_token \
-            proof_core_page_allocator_page_Page_core_page_allocator_page_UnAllocated_divide
+            proof_core_page_allocator_page_Page_core_page_allocator_page_UnAllocated_divide \
+            proof_core_page_allocator_page_Page_core_page_allocator_page_UnAllocated_merge
     - name: Compile Rocq proofs
       run: |
           (

rust-toolchain.toml

@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2025-09-12"
+channel = "nightly-2026-03-23"
 targets = [ "riscv64gc-unknown-none-elf" ]

security-monitor/rust-crates/pointers_utility/src/lib.rs

@@ -16,13 +16,17 @@ mod error;
 use core::mem::size_of;
 pub use crate::error::PointerError;
 
+// !start spec(pointers_utility.ptr_byte_offset)
 /// Calculates the offset in bytes between two pointers. 
 #[rr::only_spec]
-#[rr::returns("wrap_to_it (pointer1.2 - pointer2.2) isize")]
+#[rr::returns("wrap_to_it (pointer1.(loc_a) - pointer2.(loc_a)) isize")]
+// !end spec
+// !start code(pointers_utility.ptr_byte_offset)
 pub fn ptr_byte_offset(pointer1: *const usize, pointer2: *const usize) -> isize {
     // TODO: we should use wrapping arithmetic here, as it might overflow
     (pointer1.addr() as isize) - (pointer2.addr() as isize)
 }
+// !end code
 
 /// Aligns the pointer to specific size while making sure that the aligned pointer
 /// is still within the memory region owned by the original pointer. Check `ptr_byte_add_mut`
@@ -32,14 +36,17 @@ pub fn ptr_align(pointer: *mut usize, align_in_bytes: usize, owned_region_end: *
     ptr_byte_add_mut(pointer, offset_to_align, owned_region_end)
 }
 
+// !start spec(pointers_utility.ptr_byte_add_mut)
 /// Calculates the offset from a mutable raw pointer. This function guarantees that
 /// the returning pointer did not overflow and is within the owned memory region excluding
 /// the one-past-the-end address. The returned pointer is guaranteed to be valid for accesses
 /// of size one, if the original pointer is valid. Additional checks are required for making
 /// larger memory accesses.
 #[rr::ok]
-#[rr::requires("pointer.2 + offset_in_bytes < owned_region_end.2")]
+#[rr::requires("pointer.(loc_a) + offset_in_bytes < owned_region_end.(loc_a)")]
 #[rr::ensures("ret = (pointer +ₗ offset_in_bytes)")]
+// !end spec 
+// !start code(pointers_utility.ptr_byte_add_mut)
 pub fn ptr_byte_add_mut(
     pointer: *mut usize, offset_in_bytes: usize, owned_region_end: *const usize,
 ) -> Result<*mut usize, PointerError> {
@@ -54,17 +61,22 @@ pub fn ptr_byte_add_mut(
     }
     Ok(incremented_pointer)
 }
+// !end code
 
+// !start spec(pointers_utility.ptr_byte_add)
 /// Calculates the offset from a raw pointer. This function guarantees that
 /// the returning pointer did not overflow and is within the owned memory region excluding
 /// the one-past-the-end address. The returned pointer is guaranteed to be valid for accesses
 /// of size one, if the original pointer is valid. Additional checks are required for making
 /// larger memory accesses.
 #[rr::ok]
-#[rr::requires("pointer.2 + offset_in_bytes < owned_region_end.2")]
+#[rr::requires("pointer.(loc_a) + offset_in_bytes < owned_region_end.(loc_a)")]
 #[rr::ensures("ret = (pointer +ₗ offset_in_bytes)")]
+// !end spec
+// !start code(pointers_utility.ptr_byte_add)
 pub fn ptr_byte_add(
     pointer: *const usize, offset_in_bytes: usize, owned_region_end: *const usize,
 ) -> Result<*const usize, PointerError> {
     Ok(ptr_byte_add_mut(pointer as *mut usize, offset_in_bytes, owned_region_end)?)
 }
+// !end code

security-monitor/src/core/architecture/riscv/mmu/page_size.rs

@@ -14,6 +14,7 @@
 #[rr::derive_instantiate("PEq_refl" := #proof "intros ??; solve_goal")]
 #[rr::derive_instantiate("PEq_sym" := #proof "intros ???; solve_goal")]
 #[rr::derive_instantiate("PEq_trans" := #proof "intros ????; solve_goal")]
+#[rr::derive_instantiate("PEq_leibniz" := #proof "intros ? [] []; simpl; done")]
 // POrd
 #[rr::derive_instantiate("POrd" := "λ a b, Some (page_size_cmp a b)")]
 #[rr::derive_instantiate("POrd_eq_cons" := #proof "intros ? [] []; simpl; done")]
@@ -23,7 +24,6 @@
 #[rr::derive_instantiate("Ord_lt_trans" := #proof "intros ????; solve_goal")]
 #[rr::derive_instantiate("Ord_eq_trans" := #proof "intros ????; solve_goal")]
 #[rr::derive_instantiate("Ord_gt_trans" := #proof "intros ????; solve_goal")]
-#[rr::derive_instantiate("Ord_leibniz" := #proof "intros ? [] []; simpl; done")]
 #[rr::derive_instantiate("Ord_antisym" := #proof "intros ???; solve_goal")]
 pub enum PageSize {
     #[rr::pattern("Size4KiB")]

security-monitor/src/core/memory_layout/confidential_memory_address.rs

@@ -3,6 +3,7 @@
 // SPDX-License-Identifier: Apache-2.0
 use crate::error::Error;
 use pointers_utility::{ptr_byte_add_mut, ptr_byte_offset};
+use super::MemoryLayout;
 
 /// The wrapper over a raw pointer that is guaranteed to be an address located in the confidential memory region.
 #[repr(transparent)]
@@ -15,7 +16,7 @@ use pointers_utility::{ptr_byte_add_mut, ptr_byte_offset};
 #[rr::exists("MEMORY_CONFIG")]
 #[rr::invariant(#iris "once_status \"MEMORY_LAYOUT\" (Some MEMORY_CONFIG)")]
 /// Invariant: The address is in the confidential part of the memory layout.
-#[rr::invariant("(MEMORY_CONFIG.(conf_start).2 ≤ l.2 < MEMORY_CONFIG.(conf_end).2)%Z")]
+#[rr::invariant("(MEMORY_CONFIG.(conf_start).(loc_a) ≤ l.(loc_a) < MEMORY_CONFIG.(conf_end).(loc_a))%Z")]
 pub struct ConfidentialMemoryAddress(#[rr::field("l")] *mut usize);
 
 /// Verification: We require the ghost state for the global memory layout to be available.
@@ -25,7 +26,7 @@ impl ConfidentialMemoryAddress {
     /// Precondition: The global memory layout is initialized.
     #[rr::requires(#iris "once_status \"MEMORY_LAYOUT\" (Some MEMORY_CONFIG)")]
     /// Precondition: The address is in the confidential region of the global memory layout.
-    #[rr::requires("(MEMORY_CONFIG.(conf_start).2 ≤ address.2 < MEMORY_CONFIG.(conf_end).2)%Z")]
+    #[rr::requires("(MEMORY_CONFIG.(conf_start).(loc_a) ≤ address.(loc_a) < MEMORY_CONFIG.(conf_end).(loc_a))%Z")]
     #[rr::returns("address")]
     // TODO this should be unsafe
     pub(super) fn new(address: *mut usize) -> Self {
@@ -37,20 +38,22 @@ impl ConfidentialMemoryAddress {
         self.0 as *const u8
     }
 
-    #[rr::returns("self.2")]
+
+    #[rr::returns("self.(loc_a)")]
     pub fn as_usize(&self) -> usize {
         self.0.addr()
     }
 
-    #[rr::only_spec]
+    // Precondition: Theh alignment is a power of two.
+    #[rr::requires("is_power_of_two (Z.to_nat align)")]
     /// Postcondition: Verifies that the pointer is aligned to the given alignment.
     #[rr::returns("bool_decide (self `aligned_to` (Z.to_nat align))")]
     pub fn is_aligned_to(&self, align: usize) -> bool {
         self.0.is_aligned_to(align)
     }
 
     /// Postcondition: Compute the offset.
-    #[rr::returns("wrap_to_it (pointer.2 - self.2) isize")]
+    #[rr::returns("wrap_to_it (pointer.(loc_a) - self.(loc_a)) isize")]
     pub fn offset_from(&self, pointer: *const usize) -> isize {
         ptr_byte_offset(pointer, self.0)
     }
@@ -61,20 +64,23 @@ impl ConfidentialMemoryAddress {
     /// # Safety
     ///
     /// The caller must ensure that the address at given offset is still within the confidential memory region.
-    // TODO: can we require the offset to be a multiple of usize? (woz: yes we can)
-    #[rr::only_spec]
     #[rr::params("MEMORY_CONFIG")]
     /// Precondition: The global memory layout is initialized.
-    #[rr::requires(#iris "once_status \"MEMORY_LAYOUT\" (Some MEMORY_CONFIG)")]
+    #[rr::requires(#iris "once_initialized π \"MEMORY_LAYOUT\" (Some MEMORY_CONFIG)")]
     #[rr::ok]
     /// Precondition: The offset address is in the given range.
-    #[rr::requires("self.2 + offset_in_bytes < upper_bound.2")]
+    #[rr::requires("self.(loc_a) + offset_in_bytes < upper_bound.(loc_a)")]
     /// Precondition: The maximum (and thus the offset address) is in the confidential memory range.
-    #[rr::requires("upper_bound.2 ≤ MEMORY_CONFIG.(conf_end).2")]
+    #[rr::requires("upper_bound.(loc_a) ≤ MEMORY_CONFIG.(conf_end).(loc_a)")]
     /// Postcondition: The offset pointer is in the confidential memory range.
     #[rr::ensures("ret = self +ₗ offset_in_bytes")]
     pub fn add(&self, offset_in_bytes: usize, upper_bound: *const usize) -> Result<ConfidentialMemoryAddress, Error> {
-        let pointer = ptr_byte_add_mut(self.0, offset_in_bytes, upper_bound).map_err(#[rr::verify] |_| Error::AddressNotInConfidentialMemory())?;
+        let memory_layout = MemoryLayout::read();
+        ensure!(upper_bound <= memory_layout.confidential_memory_end, Error::AddressNotInConfidentialMemory())?;
+        let pointer = ptr_byte_add_mut(self.0, offset_in_bytes, upper_bound).map_err(
+            #[rr::verify]
+            |_| Error::AddressNotInConfidentialMemory(),
+        )?;
         Ok(Self::new(pointer))
     }
 

security-monitor/src/core/memory_layout/mod.rs

@@ -28,11 +28,11 @@ static MEMORY_LAYOUT: Once<MemoryLayout> = Once::new();
 /// non-confidential memory.
 #[rr::refined_by("ml" : "memory_layout")]
 /// Invariant: The starts of the region have addresses less-or-equal-to the ends of the regions.
-#[rr::invariant("ml.(non_conf_start).2 ≤ ml.(non_conf_end).2")]
-#[rr::invariant("ml.(conf_start).2 ≤ ml.(conf_end).2")]
+#[rr::invariant("ml.(non_conf_start).(loc_a) ≤ ml.(non_conf_end).(loc_a)")]
+#[rr::invariant("ml.(conf_start).(loc_a) ≤ ml.(conf_end).(loc_a)")]
 /// Invariant: the non-confidential memory region comes before the confidential memory region.
 // TODO: this could be generalized to the regions being disjoint
-#[rr::invariant("ml.(non_conf_end).2 ≤ ml.(conf_start).2")]
+#[rr::invariant("ml.(non_conf_end).(loc_a) ≤ ml.(conf_start).(loc_a)")]
 /// Invariant: the bounds of the confidential memory region are aligned to 4KiB pages
 #[rr::invariant("ml.(conf_start) `aligned_to` (page_size_in_bytes_nat Size4KiB)")]
 #[rr::invariant("ml.(conf_end) `aligned_to` (page_size_in_bytes_nat Size4KiB)")]
@@ -68,19 +68,19 @@ impl MemoryLayout {
     /// This function must be called only once by the initialization procedure during the boot of the system.
     #[rr::only_spec]
     /// Precondition: The non-confidential memory should have positive size.
-    #[rr::requires("non_confidential_memory_start.2 < non_confidential_memory_end.2")]
+    #[rr::requires("non_confidential_memory_start.(loc_a) < non_confidential_memory_end.(loc_a)")]
     /// Precondition: The non-condidential memory should preceed and not overlap with confidential memory.
-    #[rr::requires("non_confidential_memory_end.2 ≤ confidential_memory_start.2")]
+    #[rr::requires("non_confidential_memory_end.(loc_a) ≤ confidential_memory_start.(loc_a)")]
     /// Precondition: The confidential memory should have positive size.
-    #[rr::requires("confidential_memory_start.2 < confidential_memory_end.2")]
+    #[rr::requires("confidential_memory_start.(loc_a) < confidential_memory_end.(loc_a)")]
     /// Precondition: The global MEMORY_LAYOUT has not been initialized yet.
     #[rr::requires(#iris "once_initialized π \"MEMORY_LAYOUT\" None")]
     /// Postcondition: There exists a result -- failure is always an option
     #[rr::exists("res", "maybe_mem_layout")]
     /// Postcondition: failure due to low memory can occur if there is no sufficiently aligned
     /// confidential address
     #[rr::ensures(
-        "if_Err res (λ err, (confidential_memory_start.2 - confidential_memory_end.2 ≤ page_size_in_bytes_Z Size4KiB)%Z ∧ err = error_Error_NotEnoughMemory)"
+        "if_Err res (λ err, (confidential_memory_start.(loc_a) - confidential_memory_end.(loc_a) ≤ page_size_in_bytes_Z Size4KiB)%Z ∧ err = error_Error_NotEnoughMemory)"
     )]
     /// Postcondition: if we return Ok, we get a new confidential memory range that is correctly
     /// aligned for the smallest page size and is a subrange of [conf_start, conf_end)
@@ -90,9 +90,9 @@ impl MemoryLayout {
             maybe_mem_layout = Some mem_layout ∧
             mem_layout.(conf_start) `aligned_to` (page_size_in_bytes_nat Size4KiB) ∧
             mem_layout.(conf_end) `aligned_to` (page_size_in_bytes_nat Size4KiB) ∧
-            confidential_memory_start.2 ≤ mem_layout.(conf_start).2 ∧
-            mem_layout.(conf_end).2 ≤ confidential_memory_end.2 ∧
-            mem_layout.(conf_start).2 ≤ mem_layout.(conf_end).2 ∧
+            confidential_memory_start.(loc_a) ≤ mem_layout.(conf_start).(loc_a) ∧
+            mem_layout.(conf_end).(loc_a) ≤ confidential_memory_end.(loc_a) ∧
+            mem_layout.(conf_start).(loc_a) ≤ mem_layout.(conf_end).(loc_a) ∧
             ok = *[ mem_layout.(conf_start); mem_layout.(conf_end)])%Z"
     )]
     /// Postcondition: if we return Ok, the MEMORY_LAYOUT has been initialized.
@@ -138,7 +138,7 @@ impl MemoryLayout {
     #[rr::only_spec]
     #[rr::ok]
     /// Precondition: The offset address is in confidential memory.
-    #[rr::requires("address.2 + offset_in_bytes < self.(conf_end).2")]
+    #[rr::requires("address.(loc_a) + offset_in_bytes < self.(conf_end).(loc_a)")]
     /// Postcondition: The offset pointer is in confidential memory.
     #[rr::ensures("ret = address +ₗ offset_in_bytes")]
     pub fn confidential_address_at_offset(
@@ -152,9 +152,9 @@ impl MemoryLayout {
     #[rr::only_spec]
     #[rr::ok]
     /// Precondition: The offset address is in confidential memory.
-    #[rr::requires("address.2 + offset_in_bytes < upper_bound.2")]
+    #[rr::requires("address.(loc_a) + offset_in_bytes < upper_bound.(loc_a)")]
     /// Precondition: The bounds we are checking are within confidential memory.
-    #[rr::requires("upper_bound.2 ≤ self.(conf_end).2")]
+    #[rr::requires("upper_bound.(loc_a) ≤ self.(conf_end).(loc_a)")]
     /// Postcondition: Then we can correctly offset the address and ensure it is in confidential
     /// memory.
     #[rr::ensures("ret = address +ₗ offset_in_bytes")]
@@ -170,7 +170,7 @@ impl MemoryLayout {
     #[rr::only_spec]
     #[rr::ok]
     /// Precondition: The offset address is in non-confidential memory.
-    #[rr::requires("address.2 + offset_in_bytes < self.(non_conf_end).2")]
+    #[rr::requires("address.(loc_a) + offset_in_bytes < self.(non_conf_end).(loc_a)")]
     /// Postcondition: Then we can correctly offset the address and ensure it is in
     /// non-confidential memory.
     #[rr::ensures("ret = address +ₗ offset_in_bytes")]
@@ -183,7 +183,7 @@ impl MemoryLayout {
 
     /// Returns true if the raw pointer is inside the non-confidential memory.
     #[rr::only_spec]
-    #[rr::returns("bool_decide (self.(non_conf_start).2 ≤ address.2 ∧ address.2 < self.(non_conf_end).2)")]
+    #[rr::returns("bool_decide (self.(non_conf_start).(loc_a) ≤ address.(loc_a) ∧ address.(loc_a) < self.(non_conf_end).(loc_a))")]
     pub fn is_in_non_confidential_range(&self, address: *const usize) -> bool {
         self.non_confidential_memory_start as *const usize <= address && address < self.non_confidential_memory_end
     }
@@ -219,7 +219,7 @@ impl MemoryLayout {
 
     /// Get the boundaries of confidential memory as a (start, end) tuple.
     #[rr::only_spec]
-    #[rr::returns(" *[self.(conf_start).2; self.(conf_end).2]")]
+    #[rr::returns(" *[self.(conf_start).(loc_a); self.(conf_end).(loc_a)]")]
     pub fn confidential_memory_boundary(&self) -> (usize, usize) {
         (self.confidential_memory_start as usize, self.confidential_memory_end as usize)
     }