@@ -259,7 +259,6 @@ impl VirtAddr {
259259 /// An implementation of steps_between that returns u64. Note that this
260260 /// function always returns the exact bound, so it doesn't need to return a
261261 /// lower and upper bound like steps_between does.
262- #[ cfg( any( feature = "instructions" , feature = "step_trait" ) ) ]
263262 pub ( crate ) fn steps_between_u64 ( start : & Self , end : & Self ) -> Option < u64 > {
264263 let mut steps = end. 0 . checked_sub ( start. 0 ) ?;
265264
@@ -488,6 +487,13 @@ impl Step for VirtAddr {
488487 }
489488}
490489
490+ #[ cfg( kani) ]
491+ impl kani:: Arbitrary for VirtAddr {
492+ fn any ( ) -> Self {
493+ Self :: new_truncate ( kani:: any ( ) )
494+ }
495+ }
496+
491497/// A passed `u64` was not a valid physical address.
492498///
493499/// This means that bits 52 to 64 were not all null.
@@ -711,6 +717,13 @@ impl Sub<PhysAddr> for PhysAddr {
711717 }
712718}
713719
720+ #[ cfg( kani) ]
721+ impl kani:: Arbitrary for PhysAddr {
722+ fn any ( ) -> Self {
723+ Self :: new_truncate ( kani:: any ( ) )
724+ }
725+ }
726+
714727/// Align address downwards.
715728///
716729/// Returns the greatest `x` with alignment `align` so that `x <= addr`.
@@ -993,10 +1006,8 @@ mod proofs {
9931006 // step starting from any address.
9941007 #[ kani:: proof]
9951008 fn forward_base_case ( ) {
996- let start_raw: u64 = kani:: any ( ) ;
997- let Ok ( start) = VirtAddr :: try_new ( start_raw) else {
998- return ;
999- } ;
1009+ let start = kani:: any :: < VirtAddr > ( ) ;
1010+ let start_raw = start. as_u64 ( ) ;
10001011
10011012 // Adding 0 to any address should always yield the same address.
10021013 let same = Step :: forward ( start, 0 ) ;
@@ -1030,10 +1041,7 @@ mod proofs {
10301041 // same as taking one combined large step.
10311042 #[ kani:: proof]
10321043 fn forward_induction_step ( ) {
1033- let start_raw: u64 = kani:: any ( ) ;
1034- let Ok ( start) = VirtAddr :: try_new ( start_raw) else {
1035- return ;
1036- } ;
1044+ let start = kani:: any :: < VirtAddr > ( ) ;
10371045
10381046 let count1: usize = kani:: any ( ) ;
10391047 let count2: usize = kani:: any ( ) ;
@@ -1060,10 +1068,7 @@ mod proofs {
10601068 // for all inputs for which `forward_checked` succeeds.
10611069 #[ kani:: proof]
10621070 fn forward_implies_backward ( ) {
1063- let start_raw: u64 = kani:: any ( ) ;
1064- let Ok ( start) = VirtAddr :: try_new ( start_raw) else {
1065- return ;
1066- } ;
1071+ let start = kani:: any :: < VirtAddr > ( ) ;
10671072 let count: usize = kani:: any ( ) ;
10681073
10691074 // If `forward_checked` succeeds...
@@ -1080,10 +1085,7 @@ mod proofs {
10801085 // succeeds, `forward` succeeds as well.
10811086 #[ kani:: proof]
10821087 fn backward_implies_forward ( ) {
1083- let end_raw: u64 = kani:: any ( ) ;
1084- let Ok ( end) = VirtAddr :: try_new ( end_raw) else {
1085- return ;
1086- } ;
1088+ let end = kani:: any :: < VirtAddr > ( ) ;
10871089 let count: usize = kani:: any ( ) ;
10881090
10891091 // If `backward_checked` succeeds...
@@ -1105,10 +1107,7 @@ mod proofs {
11051107 // `steps_between` for all inputs for which `forward_checked` succeeds.
11061108 #[ kani:: proof]
11071109 fn forward_implies_steps_between ( ) {
1108- let start: u64 = kani:: any ( ) ;
1109- let Ok ( start) = VirtAddr :: try_new ( start) else {
1110- return ;
1111- } ;
1110+ let start = kani:: any :: < VirtAddr > ( ) ;
11121111 let count: usize = kani:: any ( ) ;
11131112
11141113 // If `forward_checked` succeeds...
@@ -1124,14 +1123,8 @@ mod proofs {
11241123 // succeeds, `forward` succeeds as well.
11251124 #[ kani:: proof]
11261125 fn steps_between_implies_forward ( ) {
1127- let start: u64 = kani:: any ( ) ;
1128- let Ok ( start) = VirtAddr :: try_new ( start) else {
1129- return ;
1130- } ;
1131- let end: u64 = kani:: any ( ) ;
1132- let Ok ( end) = VirtAddr :: try_new ( end) else {
1133- return ;
1134- } ;
1126+ let start = kani:: any :: < VirtAddr > ( ) ;
1127+ let end = kani:: any :: < VirtAddr > ( ) ;
11351128
11361129 // If `steps_between` succeeds...
11371130 let Some ( count) = Step :: steps_between ( & start, & end) . 1 else {
0 commit comments