Draft: Verify page allocator

[lgaeher]

Description of the changes

This WIP MR verifies the page allocator implementation.
In the process, this refactors some parts of the functions in minor ways, most notably by pulling out parts of add_memory_region into a separate function find_largest_page_size.

This also fixes two potential bugs that were caught while verifying the implementation:

• MemoryLayout::confidential_address_at_offset_bounded does not correctly check the upper bound (https://github.com/IBM/ACE-RISCV/blob/main/security-monitor/src/core/memory_layout/mod.rs#L161); interestingly, when I wrote it's specification, I didn't catch that; the spec correctly abstracts the incorrect code, but contradicts the pre-existing comment describing the intended behaviour
  Potential impact: PageAllocator::add_memory_region uses the check in this method for checking whether it exceeds the given memory regions. If there was another confidential memory region after the page token region, we would create overlapping memory regions. Currently not an issue, as page_allocator_end = confidential_memory_end, but could be critical in combination with other bugs or with future changes.

• In the second loop inside PageAllocator::add_memory_region (https://github.com/IBM/ACE-RISCV/blob/main/security-monitor/src/core/page_allocator/allocator.rs#L182), now in PageAllocator::find_largest_page_size, the condition is slightly wrong, leading us to not decrease the page size to allocate at in some cases.
  Potential impact: the tail part of the memory region is potentially wasted when it could be allocated.

Type of change

• [ x ] Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• [ x ] Formal verification
• Breaking change (fix or feature that would cause existing functionality to not work as expected)
• [ x ] Refactorization (non-breaking change which improves code quality)

How to test this PR?

The changes to the implementation should be tested by checking that the security monitor is still able to spin up a VM.

The verification CI will currently fail; I will fix this as this MR progresses.

[wojciechozga]

Great work on identifying two bugs, especially the one in unsafe Rust and verifying the page allocator implementation! This really highlights the strength of the RefinedRust approach and the need to apply formal methods in security-critical, low-level firmware.

As part of this MR, could you update the README to include:

• Information about which parts of the code have been formally verified.
• A short section noting that the formal verification efforts led to the discovery of two bugs.

This will help others understand the scope and impact of the current verification process.