Some of these optimizations were already present in the PR that introduced the Step implementation but were removed over safety concerns. To address these concerns, this PR also adds some kani proof harnesses to prove the correctness of the implementations. The proof harnesses are run in CI.
This PR optimizes the
Stepmethods forVirtAddr.Some of these optimizations were already present in the PR that introduced the
Stepimplementation but were removed over safety concerns. To address these concerns, this PR also adds some kani proof harnesses to prove the correctness of the implementations. The proof harnesses are run in CI.