Finish page allocator verification

[lgaeher]

Description of the changes

This finishes the page allocator verification using RefinedRust.

I made some minor changes in the implementation in the process.
In Page::merge, I rearranged the assertion checks a bit, as this made the verification easier.
In ConfidentialMemoryAddress::add (and NonConfidentialMemoryAddress::add), I added a new check to ensure that the upper bound stays within the respective memory range. (If we don't want to actually check that at runtime, I can also remove this again and make it a precondition of the function. Then we should make those functions unsafe, however.)

This also bumps the RefinedRust version, and therefore bumps to a current nightly version of Rust.

Type of change

• 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)
• Refactorization (non-breaking change which improves code quality)

How to test this PR?

CI should pass.

[wojciechozga]

Thank you for this effort, it is a big milestone.