Additions to proof-libs needed for the GCD example

[abentkamp]

While working on verifying the GCD crate, I need to add these definitions and lemmas to the proof-libs.

An open question: Is there a way to generalize over all instances of shift_right_trailing_zeros_nonzero_lemma as I have managed to do for shift_right_le?

And generally, I am not sure if we want these kinds of specific lemmas in the proof-libs.

[maximebuyse]

core::cmp and core::num are already switched to Rust definitions from core models in hax-evit. We shouldn't modify the hand-written F* core lib at this point. @abentkamp could you do a PR to hax-evit instead with modifications to the rust models (and F* rust_primitives)?

[W95Psp]

I think shiftval _ U32 is incorrect: 0u8 has 8 trailing zeros, but 8u32 doesn't fit in shiftval U8 U32.
Indeed, shiftval U8 U32 is defined as a number smaller than bits U8, which is 8.

So here, you can replace shiftval _ _ by (n:u32 {n <= bits U8})

[W95Psp]

(I meant using shiftval as a return type here, not the definition of shiftval)

[abentkamp]

Thanks, good catch. Anyway, I'll have to do this differently in the Rust core models, I think.

[W95Psp]

Is this lemma actually required?
It should really follow automatically from shift_right_lemma 🤔

[abentkamp]

I looked into this some more. Here is what is missing from making it work via shift_right_lemma:

val div_le
    (a:nat) (b:nat):
    Lemma (requires (b > 0))
          (ensures (a / b <= a))
          [SMTPat (a / b)]    

[W95Psp]

On the F* side, you could define:

val trailing_zeros: #t:inttype -> int_t t -> (n:u32{v n >= 0 /\ v n <= bits t})

unfold let impl_u8__trailing_zeros (n:u8) = trailing_zeros n
unfold let impl_u16__trailing_zeros (n:u16) = trailing_zeros n
unfold let impl_u32__trailing_zeros (n:u32) = trailing_zeros n
unfold let impl_u64__trailing_zeros (n:u64) = trailing_zeros n
unfold let impl_u128__trailing_zeros (n:u128) = trailing_zeros n
unfold let impl_usize__trailing_zeros (n:usize) = trailing_zeros n

val shift_right_trailing_zeros_nonzero_lemma #t (a: int_t t):
    Lemma (requires (v a <> 0))
          (ensures (v (shift_right a (trailing_zeros a)) <> 0))
          [SMTPat (shift_right a (trailing_zeros a))]

But not clear how this fits the Rust core models story, though.