https://github.com/mars-research/atmosphere/blob/bd485f22f1d5e4d1623e133700dc233086059603/kernel/verified/util/page_ptr_util_u.rs#L310 Spotted when checking out VeruSAGE (which has the same typo). Seems like one of the `i` should be `j`. Also, it seems this does not need to be an axiom…
atmosphere/kernel/verified/util/page_ptr_util_u.rs
Line 310 in bd485f2
Spotted when checking out VeruSAGE (which has the same typo). Seems like one of the
ishould bej.Also, it seems this does not need to be an axiom…