Source file sail2_operators_bitlists.ml

(*Generated by Lem from sail2_operators_bitlists.lem.*)
open Lem_pervasives_extra
open Lem_machine_word
open Sail2_values
open Sail2_operators
open Sail2_prompt_monad
open Sail2_prompt

(* Specialisation of operators to bit lists *)

(*val uint_maybe : list bitU -> maybe integer*)
let uint_maybe v:(Nat_big_num.num)option=  (unsigned_of_bits (Lem_list.map (fun b->b) v))
let uint_fail dict_Sail2_values_Bitvector_a v:('c,(Nat_big_num.num),'b)monad=  (maybe_fail "uint" (
  dict_Sail2_values_Bitvector_a.unsigned_method v))
let uint_nondet dict_Sail2_values_Register_Value_b v:('b,(Nat_big_num.num),'a)monad=  (bind
  (bools_of_bits_nondet 
  dict_Sail2_values_Register_Value_b v) (fun bs ->
  return (int_of_bools false bs)))
let uint v:Nat_big_num.num=  (maybe_failwith (uint_maybe v))

(*val sint_maybe : list bitU -> maybe integer*)
let sint_maybe v:(Nat_big_num.num)option=  (signed_of_bits (Lem_list.map (fun b->b) v))
let sint_fail dict_Sail2_values_Bitvector_a v:('c,(Nat_big_num.num),'b)monad=  (maybe_fail "sint" (
  dict_Sail2_values_Bitvector_a.signed_method v))
let sint_nondet dict_Sail2_values_Register_Value_b v:('b,(Nat_big_num.num),'a)monad=  (bind
  (bools_of_bits_nondet 
  dict_Sail2_values_Register_Value_b v) (fun bs ->
  return (int_of_bools true bs)))
let sint v:Nat_big_num.num=  (maybe_failwith (sint_maybe v))

(*val extz_vec : integer -> list bitU -> list bitU*)
let extz_vec:Nat_big_num.num ->(bitU)list ->(bitU)list= 
  (extz_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val exts_vec : integer -> list bitU -> list bitU*)
let exts_vec:Nat_big_num.num ->(bitU)list ->(bitU)list= 
  (exts_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val zero_extend : list bitU -> integer -> list bitU*)
let zero_extend bits len:(bitU)list=  (extz_bits len bits)

(*val sign_extend : list bitU -> integer -> list bitU*)
let sign_extend bits len:(bitU)list=  (exts_bits len bits)

(*val zeros : integer -> list bitU*)
let zeros len:(bitU)list=  (repeat [B0] len)

(*val ones : integer -> list bitU*)
let ones len:(bitU)list=  (repeat [B1] len)

(*val vector_truncate : list bitU -> integer -> list bitU*)
let vector_truncate bs len:(bitU)list=  (extz_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) len bs)

(*val vector_truncateLSB : list bitU -> integer -> list bitU*)
let vector_truncateLSB bs len:(bitU)list=  (take_list len bs)

(*val vec_of_bits_maybe    : list bitU -> maybe (list bitU)*)
(*val vec_of_bits_fail     : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e*)
(*val vec_of_bits_nondet   : forall 'rv 'e. list bitU -> monad 'rv (list bitU) 'e*)
(*val vec_of_bits_failwith : list bitU -> list bitU*)
(*val vec_of_bits          : list bitU -> list bitU*)

(*val access_vec_inc : list bitU -> integer -> bitU*)
let access_vec_inc:(bitU)list ->Nat_big_num.num ->bitU= 
  (access_bv_inc
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val access_vec_dec : list bitU -> integer -> bitU*)
let access_vec_dec:(bitU)list ->Nat_big_num.num ->bitU= 
  (access_bv_dec
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val update_vec_inc : list bitU -> integer -> bitU -> list bitU*)
let update_vec_inc:(bitU)list ->Nat_big_num.num ->bitU ->(bitU)list= 
  (update_bv_inc
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let update_vec_inc_maybe v i b:((bitU)list)option=  (Some (update_vec_inc v i b))
let update_vec_inc_fail v i b:('b,((bitU)list),'a)monad=  (return (update_vec_inc v i b))
let update_vec_inc_nondet v i b:('b,((bitU)list),'a)monad=  (return (update_vec_inc v i b))

(*val update_vec_dec : list bitU -> integer -> bitU -> list bitU*)
let update_vec_dec:(bitU)list ->Nat_big_num.num ->bitU ->(bitU)list= 
  (update_bv_dec
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let update_vec_dec_maybe v i b:((bitU)list)option=  (Some (update_vec_dec v i b))
let update_vec_dec_fail v i b:('b,((bitU)list),'a)monad=  (return (update_vec_dec v i b))
let update_vec_dec_nondet v i b:('b,((bitU)list),'a)monad=  (return (update_vec_dec v i b))

(*val subrange_vec_inc : list bitU -> integer -> integer -> list bitU*)
let subrange_vec_inc:(bitU)list ->Nat_big_num.num ->Nat_big_num.num ->(bitU)list= 
  (subrange_bv_inc
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val subrange_vec_dec : list bitU -> integer -> integer -> list bitU*)
let subrange_vec_dec:(bitU)list ->Nat_big_num.num ->Nat_big_num.num ->(bitU)list= 
  (subrange_bv_dec
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val update_subrange_vec_inc : list bitU -> integer -> integer -> list bitU -> list bitU*)
let update_subrange_vec_inc:(bitU)list ->Nat_big_num.num ->Nat_big_num.num ->(bitU)list ->(bitU)list= 
  (update_subrange_bv_inc
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict)
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val update_subrange_vec_dec : list bitU -> integer -> integer -> list bitU -> list bitU*)
let update_subrange_vec_dec:(bitU)list ->Nat_big_num.num ->Nat_big_num.num ->(bitU)list ->(bitU)list= 
  (update_subrange_bv_dec
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict)
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val concat_vec : list bitU -> list bitU -> list bitU*)
let concat_vec:(bitU)list ->(bitU)list ->(bitU)list= 
  (concat_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict)
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val cons_vec : bitU -> list bitU -> list bitU*)
let cons_vec:bitU ->(bitU)list ->(bitU)list= 
  (cons_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let cons_vec_maybe b v:((bitU)list)option=  (Some (cons_vec b v))
let cons_vec_fail b v:('b,((bitU)list),'a)monad=  (return (cons_vec b v))
let cons_vec_nondet b v:('b,((bitU)list),'a)monad=  (return (cons_vec b v))

(*val cast_unit_vec : bitU -> list bitU*)
let cast_unit_vec:bitU ->(bitU)list=  cast_unit_bv
let cast_unit_vec_maybe b:((bitU)list)option=  (Some (cast_unit_vec b))
let cast_unit_vec_fail b:('b,((bitU)list),'a)monad=  (return (cast_unit_vec b))
let cast_unit_vec_nondet b:('b,((bitU)list),'a)monad=  (return (cast_unit_vec b))

(*val vec_of_bit : integer -> bitU -> list bitU*)
let vec_of_bit:Nat_big_num.num ->bitU ->(bitU)list=  bv_of_bit
let vec_of_bit_maybe len b:((bitU)list)option=  (Some (vec_of_bit len b))
let vec_of_bit_fail len b:('b,((bitU)list),'a)monad=  (return (vec_of_bit len b))
let vec_of_bit_nondet len b:('b,((bitU)list),'a)monad=  (return (vec_of_bit len b))

(*val msb : list bitU -> bitU*)
let msb:(bitU)list ->bitU= 
  (most_significant
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val int_of_vec_maybe : bool -> list bitU -> maybe integer*)
let int_of_vec_maybe:bool ->(bitU)list ->(Nat_big_num.num)option= 
  (int_of_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let int_of_vec_fail sign v:('b,(Nat_big_num.num),'a)monad=  (maybe_fail "int_of_vec" (int_of_vec_maybe sign v))
let int_of_vec_nondet dict_Sail2_values_Register_Value_b sign v:('b,(Nat_big_num.num),'a)monad=  (bind (bools_of_bits_nondet 
  dict_Sail2_values_Register_Value_b v) (fun v -> return (int_of_bools sign v)))
let int_of_vec sign v:Nat_big_num.num=  (maybe_failwith (int_of_vec_maybe sign v))

(*val string_of_bits : list bitU -> string*)
let string_of_bits:(bitU)list ->string= 
  (string_of_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val string_of_bits_subrange : list bitU -> integer -> integer -> string*)
let string_of_bits_subrange:(bitU)list ->Nat_big_num.num ->Nat_big_num.num ->string= 
  (string_of_bv_subrange
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val decimal_string_of_bits : list bitU -> string*)
let decimal_string_of_bits:(bitU)list ->string= 
  (decimal_string_of_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val and_vec : list bitU -> list bitU -> list bitU*)
(*val or_vec  : list bitU -> list bitU -> list bitU*)
(*val xor_vec : list bitU -> list bitU -> list bitU*)
(*val not_vec : list bitU -> list bitU*)
let and_vec:(bitU)list ->(bitU)list ->(bitU)list=  (binop_list and_bit)
let or_vec:(bitU)list ->(bitU)list ->(bitU)list=   (binop_list or_bit)
let xor_vec:(bitU)list ->(bitU)list ->(bitU)list=  (binop_list xor_bit)
let not_vec:(bitU)list ->(bitU)list=  (Lem_list.map not_bit)

(*val arith_op_double_bl : forall 'a 'b. Bitvector 'a =>
  (integer -> integer -> integer) -> bool -> 'a -> 'a -> list bitU*)
let arith_op_double_bl dict_Sail2_values_Bitvector_a op sign l r:(bitU)list=
   (let len = (Nat_big_num.mul( (Nat_big_num.of_int 2)) (
  dict_Sail2_values_Bitvector_a.length_method l)) in
  let l' = (if sign then exts_bv 
  dict_Sail2_values_Bitvector_a len l else extz_bv dict_Sail2_values_Bitvector_a len l) in
  let r' = (if sign then exts_bv 
  dict_Sail2_values_Bitvector_a len r else extz_bv dict_Sail2_values_Bitvector_a len r) in
  Lem_list.map (fun b->b) (arith_op_bits op sign (Lem_list.map (fun b->b) l') (Lem_list.map (fun b->b) r')))

(*val add_vec   : list bitU -> list bitU -> list bitU*)
(*val adds_vec  : list bitU -> list bitU -> list bitU*)
(*val sub_vec   : list bitU -> list bitU -> list bitU*)
(*val subs_vec  : list bitU -> list bitU -> list bitU*)
(*val mult_vec  : list bitU -> list bitU -> list bitU*)
(*val mults_vec : list bitU -> list bitU -> list bitU*)
let add_vec:(bitU)list ->(bitU)list ->(bitU)list=    (fun l r->Lem_list.map (fun b->b) (arith_op_bits Nat_big_num.add false (Lem_list.map (fun b->b) l) (Lem_list.map (fun b->b) r)))
let adds_vec:(bitU)list ->(bitU)list ->(bitU)list=   (fun l r->Lem_list.map (fun b->b) (arith_op_bits Nat_big_num.add true (Lem_list.map (fun b->b) l) (Lem_list.map (fun b->b) r)))
let sub_vec:(bitU)list ->(bitU)list ->(bitU)list=    (fun l r->Lem_list.map (fun b->b) (arith_op_bits Nat_big_num.sub false (Lem_list.map (fun b->b) l) (Lem_list.map (fun b->b) r)))
let subs_vec:(bitU)list ->(bitU)list ->(bitU)list=   (fun l r->Lem_list.map (fun b->b) (arith_op_bits Nat_big_num.sub true (Lem_list.map (fun b->b) l) (Lem_list.map (fun b->b) r)))
let mult_vec:(bitU)list ->(bitU)list ->(bitU)list=   (arith_op_double_bl 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) Nat_big_num.mul false)
let mults_vec:(bitU)list ->(bitU)list ->(bitU)list=  (arith_op_double_bl 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) Nat_big_num.mul true)

(*val add_vec_int       : list bitU -> integer -> list bitU*)
(*val sub_vec_int       : list bitU -> integer -> list bitU*)
(*val mult_vec_int      : list bitU -> integer -> list bitU*)
let add_vec_int   l r:(bitU)list=  (arith_op_bv_int 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) Nat_big_num.add false l r)
let sub_vec_int   l r:(bitU)list=  (arith_op_bv_int 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) Nat_big_num.sub false l r)
let mult_vec_int  l r:(bitU)list=  (arith_op_double_bl 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) Nat_big_num.mul false l (Lem_list.map (fun b->b) (bits_of_int (Nat_big_num.of_int (List.length l)) r)))

(*val add_int_vec       : integer -> list bitU -> list bitU*)
(*val sub_int_vec       : integer -> list bitU -> list bitU*)
(*val mult_int_vec      : integer -> list bitU -> list bitU*)
let add_int_vec   l r:(bitU)list=  (arith_op_int_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) Nat_big_num.add false l r)
let sub_int_vec   l r:(bitU)list=  (arith_op_int_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) Nat_big_num.sub false l r)
let mult_int_vec  l r:(bitU)list=  (arith_op_double_bl 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) Nat_big_num.mul false (Lem_list.map (fun b->b) (bits_of_int (Nat_big_num.of_int (List.length r)) l)) r)

(*val add_vec_bit      : list bitU -> bitU -> list bitU*)
(*val adds_vec_bit     : list bitU -> bitU -> list bitU*)
(*val sub_vec_bit      : list bitU -> bitU -> list bitU*)
(*val subs_vec_bit     : list bitU -> bitU -> list bitU*)

let add_vec_bool dict_Sail2_values_Bitvector_a       l r:'a=  (arith_op_bv_bool 
  dict_Sail2_values_Bitvector_a Nat_big_num.add false l r)
let add_vec_bit_maybe dict_Sail2_values_Bitvector_a  l r:'a option=  (arith_op_bv_bit 
  dict_Sail2_values_Bitvector_a Nat_big_num.add false l r)
let add_vec_bit_fail dict_Sail2_values_Bitvector_a   l r:('d,'a,'c)monad=  (maybe_fail "add_vec_bit" (add_vec_bit_maybe 
  dict_Sail2_values_Bitvector_a l r))
let add_vec_bit_nondet dict_Sail2_values_Bitvector_a dict_Sail2_values_Register_Value_d l r:('d,'a,'c)monad=  (bind (bool_of_bitU_nondet 
  dict_Sail2_values_Register_Value_d r) (fun r -> return (add_vec_bool 
  dict_Sail2_values_Bitvector_a l r)))
let add_vec_bit        l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (add_vec_bit_maybe 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))

let adds_vec_bool dict_Sail2_values_Bitvector_a       l r:'a=  (arith_op_bv_bool 
  dict_Sail2_values_Bitvector_a Nat_big_num.add true l r)
let adds_vec_bit_maybe dict_Sail2_values_Bitvector_a  l r:'a option=  (arith_op_bv_bit 
  dict_Sail2_values_Bitvector_a Nat_big_num.add true l r)
let adds_vec_bit_fail dict_Sail2_values_Bitvector_a   l r:('d,'a,'c)monad=  (maybe_fail "adds_vec_bit" (adds_vec_bit_maybe 
  dict_Sail2_values_Bitvector_a l r))
let adds_vec_bit_nondet dict_Sail2_values_Bitvector_a dict_Sail2_values_Register_Value_d l r:('d,'a,'c)monad=  (bind (bool_of_bitU_nondet 
  dict_Sail2_values_Register_Value_d r) (fun r -> return (adds_vec_bool 
  dict_Sail2_values_Bitvector_a l r)))
let adds_vec_bit        l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (adds_vec_bit_maybe 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))

let sub_vec_bool dict_Sail2_values_Bitvector_a        l r:'a=  (arith_op_bv_bool 
  dict_Sail2_values_Bitvector_a Nat_big_num.sub false l r)
let sub_vec_bit_maybe dict_Sail2_values_Bitvector_a   l r:'a option=  (arith_op_bv_bit 
  dict_Sail2_values_Bitvector_a Nat_big_num.sub false l r)
let sub_vec_bit_fail dict_Sail2_values_Bitvector_a    l r:('d,'a,'c)monad=  (maybe_fail "sub_vec_bit" (sub_vec_bit_maybe 
  dict_Sail2_values_Bitvector_a l r))
let sub_vec_bit_nondet dict_Sail2_values_Bitvector_a dict_Sail2_values_Register_Value_d  l r:('d,'a,'c)monad=  (bind (bool_of_bitU_nondet 
  dict_Sail2_values_Register_Value_d r) (fun r -> return (sub_vec_bool 
  dict_Sail2_values_Bitvector_a l r)))
let sub_vec_bit         l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (sub_vec_bit_maybe 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))

let subs_vec_bool dict_Sail2_values_Bitvector_a       l r:'a=  (arith_op_bv_bool 
  dict_Sail2_values_Bitvector_a Nat_big_num.sub true l r)
let subs_vec_bit_maybe dict_Sail2_values_Bitvector_a  l r:'a option=  (arith_op_bv_bit 
  dict_Sail2_values_Bitvector_a Nat_big_num.sub true l r)
let subs_vec_bit_fail dict_Sail2_values_Bitvector_a   l r:('d,'a,'c)monad=  (maybe_fail "sub_vec_bit" (subs_vec_bit_maybe 
  dict_Sail2_values_Bitvector_a l r))
let subs_vec_bit_nondet dict_Sail2_values_Bitvector_a dict_Sail2_values_Register_Value_d l r:('d,'a,'c)monad=  (bind (bool_of_bitU_nondet 
  dict_Sail2_values_Register_Value_d r) (fun r -> return (subs_vec_bool 
  dict_Sail2_values_Bitvector_a l r)))
let subs_vec_bit        l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (subs_vec_bit_maybe 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))

(*val add_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
val add_overflow_vec_signed  : list bitU -> list bitU -> (list bitU * bitU * bitU)
val sub_overflow_vec         : list bitU -> list bitU -> (list bitU * bitU * bitU)
val sub_overflow_vec_signed  : list bitU -> list bitU -> (list bitU * bitU * bitU)
val mult_overflow_vec        : list bitU -> list bitU -> (list bitU * bitU * bitU)
val mult_overflow_vec_signed : list bitU -> list bitU -> (list bitU * bitU * bitU)
let add_overflow_vec         = add_overflow_bv
let add_overflow_vec_signed  = add_overflow_bv_signed
let sub_overflow_vec         = sub_overflow_bv
let sub_overflow_vec_signed  = sub_overflow_bv_signed
let mult_overflow_vec        = mult_overflow_bv
let mult_overflow_vec_signed = mult_overflow_bv_signed

val add_overflow_vec_bit         : list bitU -> bitU -> (list bitU * bitU * bitU)
val add_overflow_vec_bit_signed  : list bitU -> bitU -> (list bitU * bitU * bitU)
val sub_overflow_vec_bit         : list bitU -> bitU -> (list bitU * bitU * bitU)
val sub_overflow_vec_bit_signed  : list bitU -> bitU -> (list bitU * bitU * bitU)
let add_overflow_vec_bit         = add_overflow_bv_bit
let add_overflow_vec_bit_signed  = add_overflow_bv_bit_signed
let sub_overflow_vec_bit         = sub_overflow_bv_bit
let sub_overflow_vec_bit_signed  = sub_overflow_bv_bit_signed*)

(*val shiftl       : list bitU -> integer -> list bitU*)
(*val shiftr       : list bitU -> integer -> list bitU*)
(*val arith_shiftr : list bitU -> integer -> list bitU*)
(*val rotl         : list bitU -> integer -> list bitU*)
(*val rotr         : list bitU -> integer -> list bitU*)
let shiftl:(bitU)list ->Nat_big_num.num ->(bitU)list= 
  (shiftl_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let shiftr:(bitU)list ->Nat_big_num.num ->(bitU)list= 
  (shiftr_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let arith_shiftr:(bitU)list ->Nat_big_num.num ->(bitU)list= 
  (arith_shiftr_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let rotl:(bitU)list ->Nat_big_num.num ->(bitU)list= 
  (rotl_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let rotr:(bitU)list ->Nat_big_num.num ->(bitU)list= 
  (rotr_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val mod_vec        : list bitU -> list bitU -> list bitU*)
(*val mod_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)*)
(*val mod_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e*)
(*val mod_vec_nondet : forall 'rv 'e. Register_Value 'rv => list bitU -> list bitU -> monad 'rv (list bitU) 'e*)
let mod_vec        l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (mod_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let mod_vec_maybe  l r:((bitU)list)option=  (mod_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r)
let mod_vec_fail   l r:('rv,((bitU)list),'e)monad=  (maybe_fail "mod_vec" (mod_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let mod_vec_nondet dict_Sail2_values_Register_Value_rv l r:('rv,((bitU)list),'e)monad=  (of_bits_nondet 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) dict_Sail2_values_Register_Value_rv (mod_vec l r))

(*val quot_vec        : list bitU -> list bitU -> list bitU*)
(*val quot_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)*)
(*val quot_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e*)
(*val quot_vec_nondet : forall 'rv 'e. Register_Value 'rv => list bitU -> list bitU -> monad 'rv (list bitU) 'e*)
let quot_vec        l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (quot_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let quot_vec_maybe  l r:((bitU)list)option=  (quot_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r)
let quot_vec_fail   l r:('rv,((bitU)list),'e)monad=  (maybe_fail "quot_vec" (quot_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let quot_vec_nondet dict_Sail2_values_Register_Value_rv l r:('rv,((bitU)list),'e)monad=  (of_bits_nondet 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) dict_Sail2_values_Register_Value_rv (quot_vec l r))

(*val quots_vec        : list bitU -> list bitU -> list bitU*)
(*val quots_vec_maybe  : list bitU -> list bitU -> maybe (list bitU)*)
(*val quots_vec_fail   : forall 'rv 'e. list bitU -> list bitU -> monad 'rv (list bitU) 'e*)
(*val quots_vec_nondet : forall 'rv 'e. Register_Value 'rv => list bitU -> list bitU -> monad 'rv (list bitU) 'e*)
let quots_vec        l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (quots_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let quots_vec_maybe  l r:((bitU)list)option=  (quots_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r)
let quots_vec_fail   l r:('rv,((bitU)list),'e)monad=  (maybe_fail "quots_vec" (quots_bv 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let quots_vec_nondet dict_Sail2_values_Register_Value_rv l r:('rv,((bitU)list),'e)monad=  (of_bits_nondet 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) dict_Sail2_values_Register_Value_rv (quots_vec l r))

(*val mod_vec_int        : list bitU -> integer -> list bitU*)
(*val mod_vec_int_maybe  : list bitU -> integer -> maybe (list bitU)*)
(*val mod_vec_int_fail   : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e*)
(*val mod_vec_int_nondet : forall 'rv 'e. Register_Value 'rv => list bitU -> integer -> monad 'rv (list bitU) 'e*)
let mod_vec_int        l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (mod_bv_int 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let mod_vec_int_maybe  l r:((bitU)list)option=  (mod_bv_int 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r)
let mod_vec_int_fail   l r:('rv,((bitU)list),'e)monad=  (maybe_fail "mod_vec_int" (mod_bv_int 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let mod_vec_int_nondet dict_Sail2_values_Register_Value_rv l r:('rv,((bitU)list),'e)monad=  (of_bits_nondet 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) dict_Sail2_values_Register_Value_rv (mod_vec_int l r))

(*val quot_vec_int        : list bitU -> integer -> list bitU*)
(*val quot_vec_int_maybe  : list bitU -> integer -> maybe (list bitU)*)
(*val quot_vec_int_fail   : forall 'rv 'e. list bitU -> integer -> monad 'rv (list bitU) 'e*)
(*val quot_vec_int_nondet : forall 'rv 'e. Register_Value 'rv => list bitU -> integer -> monad 'rv (list bitU) 'e*)
let quot_vec_int        l r:(bitU)list=  (Lem.option_default (repeat [BU] (Nat_big_num.of_int (List.length l))) (quot_bv_int 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let quot_vec_int_maybe  l r:((bitU)list)option=  (quot_bv_int 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r)
let quot_vec_int_fail   l r:('rv,((bitU)list),'e)monad=  (maybe_fail "quot_vec_int" (quot_bv_int 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) (instance_Sail2_values_Bitvector_list_dict
   instance_Sail2_values_BitU_Sail2_values_bitU_dict) l r))
let quot_vec_int_nondet dict_Sail2_values_Register_Value_rv l r:('rv,((bitU)list),'e)monad=  (of_bits_nondet 
  (instance_Sail2_values_Bitvector_list_dict
     instance_Sail2_values_BitU_Sail2_values_bitU_dict) dict_Sail2_values_Register_Value_rv (quot_vec_int l r))

(*val replicate_bits : list bitU -> integer -> list bitU*)
let replicate_bits:(bitU)list ->Nat_big_num.num ->(bitU)list= 
  (replicate_bits_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val duplicate : bitU -> integer -> list bitU*)
let duplicate:bitU ->Nat_big_num.num ->(bitU)list= 
  (duplicate_bit_bv instance_Sail2_values_BitU_Sail2_values_bitU_dict)
let duplicate_maybe b n:((bitU)list)option=  (Some (duplicate b n))
let duplicate_fail b n:('b,((bitU)list),'a)monad=  (return (duplicate b n))
let duplicate_nondet dict_Sail2_values_Register_Value_b b n:('b,((bitU)list),'a)monad=  (bind
  (bool_of_bitU_nondet 
  dict_Sail2_values_Register_Value_b b) (fun b ->
  return (duplicate (bitU_of_bool b) n)))

(*val reverse_endianness : list bitU -> list bitU*)
let reverse_endianness v:(bitU)list=  (reverse_endianness_list v)

(*val get_slice_int : integer -> integer -> integer -> list bitU*)
let get_slice_int:Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num ->(bitU)list= 
  (get_slice_int_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val set_slice_int : integer -> integer -> integer -> list bitU -> integer*)
let set_slice_int:Nat_big_num.num ->Nat_big_num.num ->Nat_big_num.num ->(bitU)list ->Nat_big_num.num= 
  (set_slice_int_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))

(*val slice : list bitU -> integer -> integer -> list bitU*)
let slice v lo len:(bitU)list=
   (subrange_vec_dec v ( Nat_big_num.sub (Nat_big_num.add lo len)( (Nat_big_num.of_int 1))) lo)

(*val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU*)
let set_slice (_out_len:ii) (slice_len:ii) out (n:ii) v:(bitU)list=
   (update_subrange_vec_dec out ( Nat_big_num.sub (Nat_big_num.add n slice_len)( (Nat_big_num.of_int 1))) n v)

(*val eq_vec    : list bitU -> list bitU -> bool*)
(*val neq_vec   : list bitU -> list bitU -> bool*)
let eq_vec:(bitU)list ->(bitU)list ->bool= 
  (eq_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))
let neq_vec:(bitU)list ->(bitU)list ->bool= 
  (neq_bv
     (instance_Sail2_values_Bitvector_list_dict
        instance_Sail2_values_BitU_Sail2_values_bitU_dict))