From 6621c441c0c88464d4fd705609e132a0cb2833e5 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Wed, 20 Aug 2025 07:47:30 -0700 Subject: [PATCH 1/2] reviewer-fix --- kernel/src/allocator.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kernel/src/allocator.rs b/kernel/src/allocator.rs index 9f2d49f3df..7ca352c534 100644 --- a/kernel/src/allocator.rs +++ b/kernel/src/allocator.rs @@ -23,7 +23,7 @@ pub(crate) enum AllocateAppMemoryError { flash_size: int )] #[flux_rs::invariant(memory_start + memory_size <= u32::MAX)] -#[flux_rs::invariant(kernel_break < memory_start + memory_size)] +#[flux_rs::invariant(kernel_break <= memory_start + memory_size)] #[flux_rs::invariant(flash_start + flash_size < memory_start)] #[flux_rs::invariant(app_break >= high_water_mark)] #[flux_rs::invariant(app_break <= kernel_break)] @@ -124,7 +124,7 @@ impl AppMemoryAllocator { self.breaks.app_break } - #[flux_rs::sig(fn (&Self[@b]) -> FluxPtrU8{p: p == b.breaks.kernel_break && p < b.breaks.memory_start + b.breaks.memory_size })] + #[flux_rs::sig(fn (&Self[@b]) -> FluxPtrU8{p: p == b.breaks.kernel_break && p <= b.breaks.memory_start + b.breaks.memory_size })] pub(crate) fn kernel_break(&self) -> FluxPtrU8 { self.breaks.kernel_break } @@ -256,7 +256,7 @@ impl AppMemoryAllocator { let new_break = FluxPtrU8::from(new_break_unaligned & alignment_mask); // Verify there is space for this allocation - if new_break < self.app_break() || new_break > self.kernel_break() { + if new_break < self.app_break() || new_break >= self.kernel_break() { None } else { // Allocation is valid. From dc6044e2011f9140589756acc32a1848d6402149 Mon Sep 17 00:00:00 2001 From: vrindisbacher Date: Wed, 20 Aug 2025 19:59:26 -0700 Subject: [PATCH 2/2] remove lemmas --- kernel/src/allocator.rs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/kernel/src/allocator.rs b/kernel/src/allocator.rs index 7ca352c534..f14deae922 100644 --- a/kernel/src/allocator.rs +++ b/kernel/src/allocator.rs @@ -612,12 +612,6 @@ impl AppMemoryAllocator { mpu::Permissions::ReadWriteOnly, ); let memory_end = breaks.memory_start.wrapping_add(breaks.memory_size); - ram_regions - .fst - .lemma_no_overlap_le_addr_implies_no_overlap_addr(breaks.app_break, memory_end); - ram_regions - .snd - .lemma_no_overlap_le_addr_implies_no_overlap_addr(breaks.app_break, memory_end); app_regions .get(FLASH_REGION_NUMBER)