Skip to content

Commit 9e81a94

Browse files
authored
Change impl_u64__rotate_right second parameter type to u32
https://doc.rust-lang.org/std/primitive.u64.html#method.rotate_right
1 parent 64d0f1d commit 9e81a94

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

hax-lib/proof-libs/fstar/core/Core_models.Num.fsti

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ val impl_u64__from_be_bytes: t_Array u8 (sz 8) -> u64
161161
val impl_u64__to_le_bytes: u64 -> t_Array u8 (sz 8)
162162
val impl_u64__to_be_bytes: (x: u64) -> Pure (t_Array u8 (sz 8))
163163
(requires True) (ensures (fun res -> impl_u64__from_be_bytes res =. x))
164-
val impl_u64__rotate_right: u64 -> u64 -> u64
164+
val impl_u64__rotate_right: u64 -> u32 -> u64
165165
let impl_u64__overflowing_sub (x y: u64): u64 * bool
166166
= let sub = v x - v y in
167167
let borrow = sub < 0 in

0 commit comments

Comments
 (0)