package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Word0

val nat7 : Datatypes.nat
val nat15 : Datatypes.nat
val nat31 : Datatypes.nat
val nat63 : Datatypes.nat
val nat127 : Datatypes.nat
val nat255 : Datatypes.nat
val wsize_size_minus_1 : Wsize.wsize -> Datatypes.nat
val nat_of_wsize : Wsize.wsize -> Datatypes.nat
val wsize_bits : Wsize.wsize -> BinNums.coq_Z
val wsize_log2 : Wsize.wsize -> Datatypes.nat
val wbase : Wsize.wsize -> BinNums.coq_Z
val nat_of_pelem : Wsize.pelem -> Datatypes.nat
type word = Word.word
val coq_HB_unnamed_factory_2 : Wsize.wsize -> word Eqtype.Equality.axioms_
val coq_HB_unnamed_mixin_4 : Wsize.wsize -> word Eqtype.Coq_hasDecEq.axioms_
val word_word__canonical__eqtype_Equality : Wsize.wsize -> Eqtype.Equality.coq_type
val winit : Wsize.wsize -> (Datatypes.nat -> bool) -> word
val add_word : Wsize.wsize -> word -> word -> word
val sub_word : Wsize.wsize -> word -> word -> word
val mul_word : Wsize.wsize -> word -> word -> word
val opp_word : Wsize.wsize -> word -> word
val word0 : Wsize.wsize -> word
val word1 : Wsize.wsize -> word
val wand : Wsize.wsize -> word -> word -> word
val wor : Wsize.wsize -> word -> word -> word
val wxor : Wsize.wsize -> word -> word -> word
val wlt : Wsize.wsize -> Wsize.signedness -> word -> word -> bool
val wle : Wsize.wsize -> Wsize.signedness -> word -> word -> bool
val wnot : Wsize.wsize -> word -> word
val wandn : Wsize.wsize -> word -> word -> word
val wunsigned : Wsize.wsize -> word -> BinNums.coq_Z
val wsigned : Wsize.wsize -> word -> BinNums.coq_Z
val wrepr : Wsize.wsize -> BinNums.coq_Z -> word
val wshr : Wsize.wsize -> word -> BinNums.coq_Z -> word
val wshl : Wsize.wsize -> word -> BinNums.coq_Z -> word
val wsar : Wsize.wsize -> word -> BinNums.coq_Z -> word
val high_bits : Wsize.wsize -> BinNums.coq_Z -> word
val wmulhu : Wsize.wsize -> word -> word -> word
val wmulhs : Wsize.wsize -> word -> word -> word
val wmulhsu : Wsize.wsize -> word -> word -> word
val wmulhrs : Wsize.wsize -> word -> word -> word
val wmax_unsigned : Wsize.wsize -> BinNums.coq_Z
val half_modulus : Wsize.wsize -> BinNums.coq_Z
val wmin_signed : Wsize.wsize -> BinNums.coq_Z
val wmax_signed : Wsize.wsize -> BinNums.coq_Z
val wbit_n : Wsize.wsize -> word -> Datatypes.nat -> bool
val lsb : Wsize.wsize -> word -> bool
val msb : Wsize.wsize -> word -> bool
val wdwordu : Wsize.wsize -> word -> word -> BinNums.coq_Z
val wdwords : Wsize.wsize -> word -> word -> BinNums.coq_Z
val waddcarry : Wsize.wsize -> word -> word -> bool -> bool * word
val wdaddu : Wsize.wsize -> word -> word -> word -> word -> word * word
val wdadds : Wsize.wsize -> word -> word -> word -> word -> word * word
val wsubcarry : Wsize.wsize -> word -> word -> bool -> bool * word
val wumul : Wsize.wsize -> word -> word -> word * word
val wsmul : Wsize.wsize -> word -> word -> word * word
val wdiv : Wsize.wsize -> word -> word -> word
val wdivi : Wsize.wsize -> word -> word -> word
val wmod : Wsize.wsize -> word -> word -> word
val wmodi : Wsize.wsize -> word -> word -> word
val zero_extend : Wsize.wsize -> Wsize.wsize -> word -> word
val sign_extend : Wsize.wsize -> Wsize.wsize -> word -> word
val truncate_word : Wsize.wsize -> Wsize.wsize -> word -> word Utils0.exec
val wbit : Wsize.wsize -> word -> word -> bool
val wror : Wsize.wsize -> word -> BinNums.coq_Z -> word
val wrol : Wsize.wsize -> word -> BinNums.coq_Z -> word
val check_scale : BinNums.coq_Z -> bool
val split_vec : Wsize.wsize -> Datatypes.nat -> word -> Word.word list
val make_vec : Wsize.wsize -> Wsize.wsize -> word list -> word
val lift1_vec' : Wsize.wsize -> Wsize.wsize -> (word -> word) -> Wsize.wsize -> Wsize.wsize -> word -> word
val lift1_vec : Wsize.wsize -> (word -> word) -> Wsize.wsize -> word -> word
val lift2_vec : Wsize.wsize -> (word -> word -> word) -> Wsize.wsize -> word -> word -> word
val wbswap : Wsize.wsize -> word -> word
val popcnt : Wsize.wsize -> word -> word
val pextr : Wsize.wsize -> word -> word -> word
val bitpdep : Wsize.wsize -> word -> Datatypes.nat -> Seq.bitseq -> bool list
val pdep : Wsize.wsize -> word -> word -> word
val leading_zero_aux : BinNums.coq_Z -> Datatypes.nat -> Datatypes.nat -> Datatypes.nat
val leading_zero : Wsize.wsize -> word -> word
val trailing_zero_aux : BinNums.coq_Z -> Datatypes.nat -> Datatypes.nat
val trailing_zero : Wsize.wsize -> word -> word
val halve_list : 'a1 list -> 'a1 list
val wpmul : Wsize.wsize -> word -> word -> word
val wpmulu : Wsize.wsize -> word -> word -> word
val wpshufb1 : word list -> word -> word
val wpshufb : Wsize.wsize -> word -> word -> word
val wpshufd1 : word -> word -> Datatypes.nat -> Word.word
val wpshufd_128 : word -> BinNums.coq_Z -> word
val wpshufd_256 : word -> BinNums.coq_Z -> word
val wpshufd : Wsize.wsize -> word -> BinNums.coq_Z -> word
val wpshufl_u64 : word -> BinNums.coq_Z -> word
val wpshufl_u128 : word -> BinNums.coq_Z -> word
val wpshufh_u128 : word -> BinNums.coq_Z -> word
val wpshufl_u256 : word -> BinNums.coq_Z -> word
val wpshufh_u256 : word -> BinNums.coq_Z -> word
val wpshuflw : Wsize.wsize -> word -> BinNums.coq_Z -> word
val wpshufhw : Wsize.wsize -> word -> BinNums.coq_Z -> word
val interleave : 'a1 list -> 'a1 list -> 'a1 list
val interleave_gen : (word -> word) -> Wsize.velem -> word -> word -> word
val wpunpckl_128 : Wsize.velem -> word -> word -> word
val wpunpckl_256 : Wsize.velem -> word -> word -> word
val wpunpckh_128 : Wsize.velem -> word -> word -> word
val wpunpckh_256 : Wsize.velem -> word -> word -> word
val wpunpckl : Wsize.wsize -> Wsize.velem -> word -> word -> word
val wpunpckh : Wsize.wsize -> Wsize.velem -> word -> word -> word
val update_at : 'a1 -> 'a1 list -> Datatypes.nat -> 'a1 list
val wpinsr : Wsize.wsize -> word -> word -> word -> word
val winserti128 : word -> word -> word -> word
val wpblendd : Wsize.wsize -> word -> word -> word -> word
val wpbroadcast : Wsize.wsize -> Wsize.wsize -> word -> word
val seq_dup_hi : 'a1 list -> 'a1 list
val seq_dup_lo : 'a1 list -> 'a1 list
val wdup_hi : Wsize.wsize -> Wsize.wsize -> word -> word
val wdup_lo : Wsize.wsize -> Wsize.wsize -> word -> word
val wperm2i128 : word -> word -> word -> word
val wpermd1 : word list -> word -> word
val wpermd : Wsize.wsize -> word -> word -> word
val wpermq : word -> word -> word
val wpsxldq : (word -> BinNums.coq_Z -> word) -> Wsize.wsize -> word -> word -> word
val wpslldq : Wsize.wsize -> word -> word -> word
val wpsrldq : Wsize.wsize -> word -> word -> word
val wpcmps1 : (BinNums.coq_Z -> BinNums.coq_Z -> bool) -> Wsize.wsize -> word -> word -> word
val wpcmpeq : Wsize.wsize -> Wsize.wsize -> word -> word -> word
val wpcmpgt : Wsize.wsize -> Wsize.wsize -> word -> word -> word
val wminmax1 : Wsize.wsize -> (word -> word -> bool) -> word -> word -> word
val wabs : Wsize.velem -> Wsize.wsize -> word -> word
val saturated_signed : Wsize.wsize -> BinNums.coq_Z -> BinNums.coq_Z
val wrepr_saturated_signed : Wsize.wsize -> BinNums.coq_Z -> word
val add_pairs : BinNums.coq_Z list -> BinNums.coq_Z list
val wpmaddubsw : Wsize.wsize -> word -> word -> word
val wpmaddwd : Wsize.wsize -> word -> word -> word
val wpack : Wsize.wsize -> Datatypes.nat -> BinNums.coq_Z list -> word
val movemask : Wsize.velem -> Wsize.wsize -> word -> word
val blendv : Wsize.velem -> Wsize.wsize -> word -> word -> word -> word
val align_word : Wsize.wsize -> Wsize.wsize -> word -> word
val in_uint_range : Wsize.wsize -> BinNums.coq_Z -> bool
val in_sint_range : Wsize.wsize -> BinNums.coq_Z -> bool
val signed : 'a1 -> 'a1 -> Wsize.signedness -> 'a1
val int_of_word : Wsize.signedness -> Wsize.wsize -> word -> BinNums.coq_Z
val sem_word_extend : Wsize.signedness -> Wsize.wsize -> Wsize.wsize -> word -> word