libsail 0.15 · OCaml Package

val concat_bv : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'c ->
  'd ->
  Sail2_values.bitU list

val cons_bv : 
  'a Sail2_values.bitvector_class ->
  Sail2_values.bitU ->
  'b ->
  Sail2_values.bitU list

val cast_unit_bv : Sail2_values.bitU -> Sail2_values.bitU list

val bv_of_bit : Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list

val most_significant : 
  'a Sail2_values.bitvector_class ->
  'b ->
  Sail2_values.bitU

val get_max_representable_in : bool -> Nat_big_num.num -> Nat_big_num.num

val get_min_representable_in : 'a -> Nat_big_num.num -> Nat_big_num.num

val arith_op_bv_int : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  'a0 ->
  Nat_big_num.num ->
  'a1

val arith_op_int_bv : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  Nat_big_num.num ->
  'a0 ->
  'a1

val arith_op_bv_bool : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  'a0 ->
  bool ->
  'a1

val arith_op_bv_bit : 
  'a Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  'a0 ->
  Sail2_values.bitU ->
  'a1 option

type shift =

| LL_shift
| RR_shift
| RR_shift_arith
| LL_rot
| RR_rot

val invert_shift : shift -> shift

val shift_op_bv : 
  'a Sail2_values.bitvector_class ->
  shift ->
  'b ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val shiftl_bv : 
  'a Sail2_values.bitvector_class ->
  'a0 ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val shiftr_bv : 
  'a Sail2_values.bitvector_class ->
  'a0 ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val arith_shiftr_bv : 
  'a Sail2_values.bitvector_class ->
  'a0 ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val rotl_bv : 
  'a Sail2_values.bitvector_class ->
  'a0 ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val rotr_bv : 
  'a Sail2_values.bitvector_class ->
  'a0 ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val shiftl_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

val shiftr_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

val arith_shiftr_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

val rotl_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

val rotr_mword : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Lem.mword

val arith_op_no0 : 
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num option

val arith_op_bv_no0 : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  Nat_big_num.num ->
  'c ->
  'd ->
  'b0 option

val mod_bv : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b0 ->
  'b0 ->
  'a0 option

val quot_bv : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b0 ->
  'b0 ->
  'a0 option

val quots_bv : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b0 ->
  'b0 ->
  'a0 option

val mod_mword : Lem.mword -> Lem.mword -> Lem.mword

val quot_mword : Lem.mword -> Lem.mword -> Lem.mword

val quots_mword : Lem.mword -> Lem.mword -> Lem.mword

val arith_op_bv_int_no0 : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  Nat_big_num.num ->
  'c ->
  Nat_big_num.num ->
  'b0 option

val quot_bv_int : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b0 ->
  Nat_big_num.num ->
  'a0 option

val mod_bv_int : 
  'a Sail2_values.bitvector_class ->
  'b Sail2_values.bitvector_class ->
  'b0 ->
  Nat_big_num.num ->
  'a0 option

val mod_mword_int : 
  'a Lem_machine_word.size_class ->
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  Lem.mword

val quot_mword_int : 
  'a Lem_machine_word.size_class ->
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  Lem.mword

val quots_mword_int : 
  'a Lem_machine_word.size_class ->
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  Lem.mword

val replicate_bits_bv : 
  'a Sail2_values.bitvector_class ->
  'b ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val duplicate_bit_bv : 
  'a Sail2_values.bitU_class ->
  'b ->
  Nat_big_num.num ->
  Sail2_values.bitU list

val eq_bv : 'a Sail2_values.bitvector_class -> 'b -> 'c -> bool

val neq_bv : 'a Sail2_values.bitvector_class -> 'b -> 'c -> bool

val get_slice_int_bv : 
  'a Sail2_values.bitvector_class ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a0

val set_slice_int_bv : 
  'a Sail2_values.bitvector_class ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'b ->
  Nat_big_num.num

package libsail