sail2_operators_bitlists.lem

open import Pervasives_extra
open import Machine_word
open import Sail2_values
open import Sail2_operators
open import Sail2_prompt_monad
open import Sail2_prompt

(* Specialisation of operators to bit lists *)

val uint_maybe : list bitU -> maybe integer
let uint_maybe v = unsigned v
let uint_fail v = maybe_fail "uint" (unsigned v)
let uint_nondet v =
  bools_of_bits_nondet v >>= (fun bs ->
  return (int_of_bools false bs))
let uint v = maybe_failwith (uint_maybe v)

val sint_maybe : list bitU -> maybe integer
let sint_maybe v = signed v
let sint_fail v = maybe_fail "sint" (signed v)
let sint_nondet v =
  bools_of_bits_nondet v >>= (fun bs ->
  return (int_of_bools true bs))
let sint v = maybe_failwith (sint_maybe v)

val extz_vec : integer -> list bitU -> list bitU
let extz_vec = extz_bv

val exts_vec : integer -> list bitU -> list bitU
let exts_vec = exts_bv

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

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

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

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

val vector_truncate : list bitU -> integer -> list bitU
let vector_truncate bs len = extz_bv len bs

val vector_truncateLSB : list bitU -> integer -> list bitU
let vector_truncateLSB bs len = 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
let inline vec_of_bits bits = bits
let inline vec_of_bits_maybe bits = Just bits
let inline vec_of_bits_fail bits = return bits
let inline vec_of_bits_nondet bits = return bits
let inline vec_of_bits_failwith bits = bits

val access_vec_inc : list bitU -> integer -> bitU
let access_vec_inc = access_bv_inc

val access_vec_dec : list bitU -> integer -> bitU
let access_vec_dec = access_bv_dec

val update_vec_inc : list bitU -> integer -> bitU -> list bitU
let update_vec_inc = update_bv_inc
let update_vec_inc_maybe v i b = Just (update_vec_inc v i b)
let update_vec_inc_fail v i b = return (update_vec_inc v i b)
let update_vec_inc_nondet v i b = return (update_vec_inc v i b)

val update_vec_dec : list bitU -> integer -> bitU -> list bitU
let update_vec_dec = update_bv_dec
let update_vec_dec_maybe v i b = Just (update_vec_dec v i b)
let update_vec_dec_fail v i b = return (update_vec_dec v i b)
let update_vec_dec_nondet v i b = return (update_vec_dec v i b)

val subrange_vec_inc : list bitU -> integer -> integer -> list bitU
let subrange_vec_inc = subrange_bv_inc

val subrange_vec_dec : list bitU -> integer -> integer -> list bitU
let subrange_vec_dec = subrange_bv_dec

val update_subrange_vec_inc : list bitU -> integer -> integer -> list bitU -> list bitU
let update_subrange_vec_inc = update_subrange_bv_inc

val update_subrange_vec_dec : list bitU -> integer -> integer -> list bitU -> list bitU
let update_subrange_vec_dec = update_subrange_bv_dec

val concat_vec : list bitU -> list bitU -> list bitU
let concat_vec = concat_bv

val cons_vec : bitU -> list bitU -> list bitU
let cons_vec = cons_bv
let cons_vec_maybe b v = Just (cons_vec b v)
let cons_vec_fail b v = return (cons_vec b v)
let cons_vec_nondet b v = return (cons_vec b v)

val cast_unit_vec : bitU -> list bitU
let cast_unit_vec = cast_unit_bv
let cast_unit_vec_maybe b = Just (cast_unit_vec b)
let cast_unit_vec_fail b = return (cast_unit_vec b)
let cast_unit_vec_nondet b = return (cast_unit_vec b)

val vec_of_bit : integer -> bitU -> list bitU
let vec_of_bit = bv_of_bit
let vec_of_bit_maybe len b = Just (vec_of_bit len b)
let vec_of_bit_fail len b = return (vec_of_bit len b)
let vec_of_bit_nondet len b = return (vec_of_bit len b)

val msb : list bitU -> bitU
let msb = most_significant

val int_of_vec_maybe : bool -> list bitU -> maybe integer
let int_of_vec_maybe = int_of_bv
let int_of_vec_fail sign v = maybe_fail "int_of_vec" (int_of_vec_maybe sign v)
let int_of_vec_nondet sign v = bools_of_bits_nondet v >>= (fun v -> return (int_of_bools sign v))
let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v)

val string_of_bits : list bitU -> string
let string_of_bits = string_of_bv

val string_of_bits_subrange : list bitU -> integer -> integer -> string
let string_of_bits_subrange = string_of_bv_subrange

val decimal_string_of_bits : list bitU -> string
let decimal_string_of_bits = decimal_string_of_bv

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 = binop_list and_bit
let or_vec  = binop_list or_bit
let xor_vec = binop_list xor_bit
let not_vec = 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 op sign l r =
  let len = 2 * length l in
  let l' = if sign then exts_bv len l else extz_bv len l in
  let r' = if sign then exts_bv len r else extz_bv len r in
  arith_op_bv op sign l' 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   = arith_op_bv integerAdd false
let adds_vec  = arith_op_bv integerAdd true
let sub_vec   = arith_op_bv integerMinus false
let subs_vec  = arith_op_bv integerMinus true
let mult_vec  = arith_op_double_bl integerMult false
let mults_vec = arith_op_double_bl integerMult 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 = arith_op_bv_int integerAdd false l r
let sub_vec_int   l r = arith_op_bv_int integerMinus false l r
let mult_vec_int  l r = arith_op_double_bl integerMult false l (of_int (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 = arith_op_int_bv integerAdd false l r
let sub_int_vec   l r = arith_op_int_bv integerMinus false l r
let mult_int_vec  l r = arith_op_double_bl integerMult false (of_int (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       l r = arith_op_bv_bool integerAdd false l r
let add_vec_bit_maybe  l r = arith_op_bv_bit integerAdd false l r
let add_vec_bit_fail   l r = maybe_fail "add_vec_bit" (add_vec_bit_maybe l r)
let add_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (add_vec_bool l r))
let add_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (add_vec_bit_maybe l r)

let adds_vec_bool       l r = arith_op_bv_bool integerAdd true l r
let adds_vec_bit_maybe  l r = arith_op_bv_bit integerAdd true l r
let adds_vec_bit_fail   l r = maybe_fail "adds_vec_bit" (adds_vec_bit_maybe l r)
let adds_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (adds_vec_bool l r))
let adds_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (adds_vec_bit_maybe l r)

let sub_vec_bool        l r = arith_op_bv_bool integerMinus false l r
let sub_vec_bit_maybe   l r = arith_op_bv_bit integerMinus false l r
let sub_vec_bit_fail    l r = maybe_fail "sub_vec_bit" (sub_vec_bit_maybe l r)
let sub_vec_bit_nondet  l r = bool_of_bitU_nondet r >>= (fun r -> return (sub_vec_bool l r))
let sub_vec_bit         l r = fromMaybe (repeat [BU] (length l)) (sub_vec_bit_maybe l r)

let subs_vec_bool       l r = arith_op_bv_bool integerMinus true l r
let subs_vec_bit_maybe  l r = arith_op_bv_bit integerMinus true l r
let subs_vec_bit_fail   l r = maybe_fail "sub_vec_bit" (subs_vec_bit_maybe l r)
let subs_vec_bit_nondet l r = bool_of_bitU_nondet r >>= (fun r -> return (subs_vec_bool l r))
let subs_vec_bit        l r = fromMaybe (repeat [BU] (length l)) (subs_vec_bit_maybe 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       = shiftl_bv
let shiftr       = shiftr_bv
let arith_shiftr = arith_shiftr_bv
let rotl         = rotl_bv
let rotr         = rotr_bv

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 = fromMaybe (repeat [BU] (length l)) (mod_bv l r)
let mod_vec_maybe  l r = mod_bv l r
let mod_vec_fail   l r = maybe_fail "mod_vec" (mod_bv l r)
let mod_vec_nondet l r = of_bits_nondet (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 = fromMaybe (repeat [BU] (length l)) (quot_bv l r)
let quot_vec_maybe  l r = quot_bv l r
let quot_vec_fail   l r = maybe_fail "quot_vec" (quot_bv l r)
let quot_vec_nondet l r = of_bits_nondet (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 = fromMaybe (repeat [BU] (length l)) (quots_bv l r)
let quots_vec_maybe  l r = quots_bv l r
let quots_vec_fail   l r = maybe_fail "quots_vec" (quots_bv l r)
let quots_vec_nondet l r = of_bits_nondet (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 = fromMaybe (repeat [BU] (length l)) (mod_bv_int l r)
let mod_vec_int_maybe  l r = mod_bv_int l r
let mod_vec_int_fail   l r = maybe_fail "mod_vec_int" (mod_bv_int l r)
let mod_vec_int_nondet l r = of_bits_nondet (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 = fromMaybe (repeat [BU] (length l)) (quot_bv_int l r)
let quot_vec_int_maybe  l r = quot_bv_int l r
let quot_vec_int_fail   l r = maybe_fail "quot_vec_int" (quot_bv_int l r)
let quot_vec_int_nondet l r = of_bits_nondet (quot_vec_int l r)

val replicate_bits : list bitU -> integer -> list bitU
let replicate_bits = replicate_bits_bv

val duplicate : bitU -> integer -> list bitU
let duplicate = duplicate_bit_bv
let duplicate_maybe b n = Just (duplicate b n)
let duplicate_fail b n = return (duplicate b n)
let duplicate_nondet b n =
  bool_of_bitU_nondet b >>= (fun b ->
  return (duplicate (bitU_of_bool b) n))

val reverse_endianness : list bitU -> list bitU
let reverse_endianness v = reverse_endianness_list v

val get_slice_int : integer -> integer -> integer -> list bitU
let get_slice_int = get_slice_int_bv

val set_slice_int : integer -> integer -> integer -> list bitU -> integer
let set_slice_int = set_slice_int_bv

val slice : list bitU -> integer -> integer -> list bitU
let slice v lo len =
  subrange_vec_dec v (lo + len - 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 =
  update_subrange_vec_dec out (n + slice_len - 1) n v

val eq_vec    : list bitU -> list bitU -> bool
val neq_vec   : list bitU -> list bitU -> bool
let eq_vec    = eq_bv
let neq_vec   = neq_bv

let inline count_leading_zeros v = count_leading_zero_bits v