implement Step for PhysAddr and PhysFrame

[Freax13]

This PR adds Step implementations for PhysAddr and PhysFrame. This PR also adds kani harnesses to prove the correctness of these new implementations and the unsafe code within them.

Closes #212

[josephlr]

I did a quick look, while nothing seems wrong, there are two things I want to take a closer look at:

• How the Physical Address stuff interacts with the memory encryption bit. If the C-bit isn't bit 52 (it's usually bit 47), could a valid physical address underflow into an invalid physical address?
• how the kani::proof stuff works.

[Freax13]

• How the Physical Address stuff interacts with the memory encryption bit. If the C-bit isn't bit 52 (it's usually bit 47), could a valid physical address underflow into an invalid physical address?

No because PhysAddr and PhysFrame are guaranteed not to contain the C-bit/S-bit.

[Freax13]

rebased

[phil-opp]

No because PhysAddr and PhysFrame are guaranteed not to contain the C-bit/S-bit.

With the right count it's still possible to end up on an address that has the bits set, no? So the new_unsafe in backward_checked might violate this invariant.

[Freax13]

No because PhysAddr and PhysFrame are guaranteed not to contain the C-bit/S-bit.

With the right count it's still possible to end up on an address that has the bits set, no? So the new_unsafe in backward_checked might violate this invariant.

Hmm, yeah, you're right.

Maybe a better solution would be not to allow any bits above the C-bit/S-bit to be set.

• TDX already requires this: "GPA bits higher than the SHARED bit are considered reserved and must be 0. Address translation with any of the reserved bits set to 1 cause a #PF with PFEC (Page Fault Error Code) RSVD bit set." (Architecture Specification: Intel® Trust Domain Extensions (Intel® TDX) Module, 13.11.1. GPAW-Relate EPT Violations).
• AMD CPUs don't have the same restriction, however in practice, the C-bit is always the upmost supported physical adddress bit. Client parts and server parts up until Rome support 48 physical address bits and use bit 47 as the C-bit. Server parts starting with Milan support 52 physical address bits and always use bit 51 as the C-bit. Thinking about this, this makes sense: If the CPU allowed bits higher than the C-bit to be used for address bits, this would fragment the physical address space and make large parts of it effectively unusable.

Technically, adding this restriction would be a breaking change, however, any address that that didn't satisfy this restriction would be unusable in practice anyway, so we could also consider this a non-breaking fix instead of a breaking change.