We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
2 parents 64d0f1d + 9e81a94 commit fcb8adbCopy full SHA for fcb8adb
hax-lib/proof-libs/fstar/core/Core_models.Num.fsti
@@ -161,7 +161,7 @@ val impl_u64__from_be_bytes: t_Array u8 (sz 8) -> u64
161
val impl_u64__to_le_bytes: u64 -> t_Array u8 (sz 8)
162
val impl_u64__to_be_bytes: (x: u64) -> Pure (t_Array u8 (sz 8))
163
(requires True) (ensures (fun res -> impl_u64__from_be_bytes res =. x))
164
-val impl_u64__rotate_right: u64 -> u64 -> u64
+val impl_u64__rotate_right: u64 -> u32 -> u64
165
let impl_u64__overflowing_sub (x y: u64): u64 * bool
166
= let sub = v x - v y in
167
let borrow = sub < 0 in
0 commit comments