fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type uint128 = {
  1. low : FStar_UInt64.t;
  2. high : FStar_UInt64.t;
}
val __proj__Mkuint128__item__low : uint128 -> FStar_UInt64.t
val __proj__Mkuint128__item__high : uint128 -> FStar_UInt64.t
type t = uint128
val uint_to_t : Prims.unit FStar_UInt.uint_t -> t
val constant_time_carry : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt64.t
val add : t -> t -> t
val add_underspec : t -> t -> t
val add_mod : t -> t -> t
val sub : t -> t -> t
val sub_underspec : t -> t -> t
val sub_mod_impl : t -> t -> t
val sub_mod : t -> t -> t
val logand : t -> t -> t
val logxor : t -> t -> t
val logor : t -> t -> t
val lognot : t -> t
val __uint_to_t : Prims.int -> t
val u32_64 : FStar_UInt32.t
val add_u64_shift_left_respec : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt32.t -> FStar_UInt64.t
val shift_left_small : t -> FStar_UInt32.t -> t
val shift_left_large : t -> FStar_UInt32.t -> t
val shift_left : t -> FStar_UInt32.t -> t
val add_u64_shift_right : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt32.t -> FStar_UInt64.t
val add_u64_shift_right_respec : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt32.t -> FStar_UInt64.t
val shift_right_small : t -> FStar_UInt32.t -> t
val shift_right_large : t -> FStar_UInt32.t -> t
val shift_right : t -> FStar_UInt32.t -> t
val eq : t -> t -> Prims.bool
val gt : t -> t -> Prims.bool
val lt : t -> t -> Prims.bool
val gte : t -> t -> Prims.bool
val lte : t -> t -> Prims.bool
val eq_mask : t -> t -> t
val gte_mask : t -> t -> t
val uint64_to_uint128 : FStar_UInt64.t -> t
val uint128_to_uint64 : t -> FStar_UInt64.t
val u64_l32_mask : FStar_UInt64.t
val u64_mod_32 : FStar_UInt64.t -> FStar_UInt64.t
val u32_32 : FStar_UInt32.t
val mul32 : FStar_UInt64.t -> FStar_UInt32.t -> t
val mul_wide_low : FStar_UInt64.t -> FStar_UInt64.t -> Prims.int
val mul_wide_high : FStar_UInt64.t -> FStar_UInt64.t -> Prims.int
val mul_wide : FStar_UInt64.t -> FStar_UInt64.t -> t