(*Generated by Sail from riscv_duopod.*)
Require Import Sail2_instr_kinds.
Require Import Sail2_values.
Require Import Sail2_string.
Require Import Sail2_real.
Require Import Sail2_operators_mwords.
Require Import Sail2_prompt_monad.
Require Import Sail2_prompt.
Require Import Sail2_state.
Require Import riscv_duopod_types.
Require Import riscv_extras.
Import ListNotations.
Open Scope string.
Open Scope bool.
Section Content.

Definition is_none {a : Type} (opt : option a) 
: bool :=
   
   match opt with | Some (_) => false | None => true end.

Definition is_some {a : Type} (opt : option a) 
: bool :=
   
   match opt with | Some (_) => true | None => false end.

Definition eq_unit (_ : unit) (_ : unit) 
: {_bool : bool & ArithFact (_bool = true)} :=
   
   build_ex(true).

Definition neq_int (x : Z) (y : Z) 
: {_bool : bool & ArithFact (iff (_bool = true) (x <> y))} :=
   
   build_ex(negb (Z.eqb x y)).

Definition neq_bool (x : bool) (y : bool)  : bool :=  negb (Bool.eqb x y).

Definition __id (x : Z)  : {_retval : Z & ArithFact (_retval = x)} :=  build_ex(x).

Definition concat_str_bits {n : Z} (str : string) (x : mword n) 
: string :=
   
   String.append str (string_of_bits x).

Definition concat_str_dec (str : string) (x : Z)  : string :=  String.append str (dec_str x).



Definition sail_mask {v0 : Z} (len : Z) (v : mword v0) `{ArithFact (len >= 0 /\ v0 >= 0)} 
: mword len :=
   
   if sumbool_of_bool ((Z.leb len (length_mword v))) then vector_truncate v len
   else zero_extend v len.

Definition sail_ones (n : Z) `{ArithFact (n >= 0)}  : mword n :=  not_vec (zeros n).

Definition slice_mask (n : Z) (i : Z) (l : Z) `{ArithFact (n >= 0)} 
: mword n :=
   
   if sumbool_of_bool ((Z.geb l n)) then shiftl (sail_ones n) i
   else
     let one : bits n := sail_mask n ((vec_of_bits [B1]  : mword 1)  : bits 1) in
     shiftl (sub_vec (shiftl one l) one) i.

Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} 
: read_kind :=
   
   let l__34 := arg_ in
   if sumbool_of_bool ((Z.eqb l__34 0)) then Read_plain
   else if sumbool_of_bool ((Z.eqb l__34 1)) then Read_reserve
   else if sumbool_of_bool ((Z.eqb l__34 2)) then Read_acquire
   else if sumbool_of_bool ((Z.eqb l__34 3)) then Read_exclusive
   else if sumbool_of_bool ((Z.eqb l__34 4)) then Read_exclusive_acquire
   else if sumbool_of_bool ((Z.eqb l__34 5)) then Read_stream
   else if sumbool_of_bool ((Z.eqb l__34 6)) then Read_RISCV_acquire
   else if sumbool_of_bool ((Z.eqb l__34 7)) then Read_RISCV_strong_acquire
   else if sumbool_of_bool ((Z.eqb l__34 8)) then Read_RISCV_reserved
   else if sumbool_of_bool ((Z.eqb l__34 9)) then Read_RISCV_reserved_acquire
   else if sumbool_of_bool ((Z.eqb l__34 10)) then Read_RISCV_reserved_strong_acquire
   else Read_X86_locked.

Definition num_of_read_kind (arg_ : read_kind) 
: {e : Z & ArithFact (0 <= e /\ e <= 11)} :=
   
   build_ex(match arg_ with
            | Read_plain => 0
            | Read_reserve => 1
            | Read_acquire => 2
            | Read_exclusive => 3
            | Read_exclusive_acquire => 4
            | Read_stream => 5
            | Read_RISCV_acquire => 6
            | Read_RISCV_strong_acquire => 7
            | Read_RISCV_reserved => 8
            | Read_RISCV_reserved_acquire => 9
            | Read_RISCV_reserved_strong_acquire => 10
            | Read_X86_locked => 11
            end).

Definition write_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 10)} 
: write_kind :=
   
   let l__24 := arg_ in
   if sumbool_of_bool ((Z.eqb l__24 0)) then Write_plain
   else if sumbool_of_bool ((Z.eqb l__24 1)) then Write_conditional
   else if sumbool_of_bool ((Z.eqb l__24 2)) then Write_release
   else if sumbool_of_bool ((Z.eqb l__24 3)) then Write_exclusive
   else if sumbool_of_bool ((Z.eqb l__24 4)) then Write_exclusive_release
   else if sumbool_of_bool ((Z.eqb l__24 5)) then Write_RISCV_release
   else if sumbool_of_bool ((Z.eqb l__24 6)) then Write_RISCV_strong_release
   else if sumbool_of_bool ((Z.eqb l__24 7)) then Write_RISCV_conditional
   else if sumbool_of_bool ((Z.eqb l__24 8)) then Write_RISCV_conditional_release
   else if sumbool_of_bool ((Z.eqb l__24 9)) then Write_RISCV_conditional_strong_release
   else Write_X86_locked.

Definition num_of_write_kind (arg_ : write_kind) 
: {e : Z & ArithFact (0 <= e /\ e <= 10)} :=
   
   build_ex(match arg_ with
            | Write_plain => 0
            | Write_conditional => 1
            | Write_release => 2
            | Write_exclusive => 3
            | Write_exclusive_release => 4
            | Write_RISCV_release => 5
            | Write_RISCV_strong_release => 6
            | Write_RISCV_conditional => 7
            | Write_RISCV_conditional_release => 8
            | Write_RISCV_conditional_strong_release => 9
            | Write_X86_locked => 10
            end).

Definition a64_barrier_domain_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 3)} 
: a64_barrier_domain :=
   
   let l__21 := arg_ in
   if sumbool_of_bool ((Z.eqb l__21 0)) then A64_FullShare
   else if sumbool_of_bool ((Z.eqb l__21 1)) then A64_InnerShare
   else if sumbool_of_bool ((Z.eqb l__21 2)) then A64_OuterShare
   else A64_NonShare.

Definition num_of_a64_barrier_domain (arg_ : a64_barrier_domain) 
: {e : Z & ArithFact (0 <= e /\ e <= 3)} :=
   
   build_ex(match arg_ with
            | A64_FullShare => 0
            | A64_InnerShare => 1
            | A64_OuterShare => 2
            | A64_NonShare => 3
            end).

Definition a64_barrier_type_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 2)} 
: a64_barrier_type :=
   
   let l__19 := arg_ in
   if sumbool_of_bool ((Z.eqb l__19 0)) then A64_barrier_all
   else if sumbool_of_bool ((Z.eqb l__19 1)) then A64_barrier_LD
   else A64_barrier_ST.

Definition num_of_a64_barrier_type (arg_ : a64_barrier_type) 
: {e : Z & ArithFact (0 <= e /\ e <= 2)} :=
   
   build_ex(match arg_ with | A64_barrier_all => 0 | A64_barrier_LD => 1 | A64_barrier_ST => 2 end).

Definition trans_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 2)} 
: trans_kind :=
   
   let l__17 := arg_ in
   if sumbool_of_bool ((Z.eqb l__17 0)) then Transaction_start
   else if sumbool_of_bool ((Z.eqb l__17 1)) then Transaction_commit
   else Transaction_abort.

Definition num_of_trans_kind (arg_ : trans_kind) 
: {e : Z & ArithFact (0 <= e /\ e <= 2)} :=
   
   build_ex(match arg_ with
            | Transaction_start => 0
            | Transaction_commit => 1
            | Transaction_abort => 2
            end).

Definition cache_op_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 10)} 
: cache_op_kind :=
   
   let l__7 := arg_ in
   if sumbool_of_bool ((Z.eqb l__7 0)) then Cache_op_D_IVAC
   else if sumbool_of_bool ((Z.eqb l__7 1)) then Cache_op_D_ISW
   else if sumbool_of_bool ((Z.eqb l__7 2)) then Cache_op_D_CSW
   else if sumbool_of_bool ((Z.eqb l__7 3)) then Cache_op_D_CISW
   else if sumbool_of_bool ((Z.eqb l__7 4)) then Cache_op_D_ZVA
   else if sumbool_of_bool ((Z.eqb l__7 5)) then Cache_op_D_CVAC
   else if sumbool_of_bool ((Z.eqb l__7 6)) then Cache_op_D_CVAU
   else if sumbool_of_bool ((Z.eqb l__7 7)) then Cache_op_D_CIVAC
   else if sumbool_of_bool ((Z.eqb l__7 8)) then Cache_op_I_IALLUIS
   else if sumbool_of_bool ((Z.eqb l__7 9)) then Cache_op_I_IALLU
   else Cache_op_I_IVAU.

Definition num_of_cache_op_kind (arg_ : cache_op_kind) 
: {e : Z & ArithFact (0 <= e /\ e <= 10)} :=
   
   build_ex(match arg_ with
            | Cache_op_D_IVAC => 0
            | Cache_op_D_ISW => 1
            | Cache_op_D_CSW => 2
            | Cache_op_D_CISW => 3
            | Cache_op_D_ZVA => 4
            | Cache_op_D_CVAC => 5
            | Cache_op_D_CVAU => 6
            | Cache_op_D_CIVAC => 7
            | Cache_op_I_IALLUIS => 8
            | Cache_op_I_IALLU => 9
            | Cache_op_I_IVAU => 10
            end).

Definition neq_vec {n : Z} (x : mword n) (y : mword n)  : bool :=  negb (eq_vec x y).



Definition cast_unit_vec (b : bitU) 
: M (mword 1) :=
   
   (match b with
    | B0 => returnm ((vec_of_bits [B0]  : mword 1)  : mword 1)
    | B1 => returnm ((vec_of_bits [B1]  : mword 1)  : mword 1)
    | _ => exit tt  : M (mword 1)
    end)
    : M (mword 1).

Definition get_config_print_instr '(tt : unit)  : bool :=  false.

Definition get_config_print_reg '(tt : unit)  : bool :=  false.

Definition get_config_print_mem '(tt : unit)  : bool :=  false.

Definition get_config_print_platform '(tt : unit)  : bool :=  false.

Definition EXTS {n : Z} (m : Z) (v : mword n) `{ArithFact (m >= n)}  : mword m :=  sign_extend v m.

Definition EXTZ {n : Z} (m : Z) (v : mword n) `{ArithFact (m >= n)}  : mword m :=  zero_extend v m.

Definition zeros_implicit (n : Z) `{ArithFact (n >= 0)}  : mword n :=  zeros n.

Definition zeros (n : Z) `{ArithFact (n >= 0)} 
: mword n :=
   
   autocast (replicate_bits (vec_of_bits [B0]  : mword 1) n).

Definition ones (n : Z) `{ArithFact (n >= 0)}  : mword n :=  sail_ones n.

Definition bool_to_bits (x : bool) 
: mword 1 :=
   
   if sumbool_of_bool (x) then (vec_of_bits [B1]  : mword 1)
   else (vec_of_bits [B0]  : mword 1).

Definition bit_to_bool (b : bitU) 
: M (bool) :=
   
   (match b with
    | B1 => returnm (projT1 (build_ex true  : {_bool : bool & ArithFact (_bool = true)}))
    | B0 => returnm (projT1 (build_ex false  : {_bool : bool & ArithFact (not (_bool = true))}))
    | _ => exit tt  : M (bool)
    end)
    : M (bool).

Definition to_bits (l : Z) (n : Z) `{ArithFact (l >= 0)}  : mword l :=  get_slice_int l n 0.

Definition zopz0zI_s {n : Z} (x : mword n) (y : mword n) `{ArithFact (n > 0)} 
: bool :=
   
   Z.ltb (projT1 (sint x)) (projT1 (sint y)).

Definition zopz0zKzJ_s {n : Z} (x : mword n) (y : mword n) `{ArithFact (n > 0)} 
: bool :=
   
   Z.geb (projT1 (sint x)) (projT1 (sint y)).

Definition zopz0zI_u {n : Z} (x : mword n) (y : mword n) 
: bool :=
   
   Z.ltb (projT1 (uint x)) (projT1 (uint y)).

Definition zopz0zKzJ_u {n : Z} (x : mword n) (y : mword n) 
: bool :=
   
   Z.geb (projT1 (uint x)) (projT1 (uint y)).

Definition zopz0zIzJ_u {n : Z} (x : mword n) (y : mword n) 
: bool :=
   
   Z.leb (projT1 (uint x)) (projT1 (uint y)).

Definition shift_right_arith64 (v : mword 64) (shift : mword 6) 
: mword 64 :=
   
   let v128 : bits 128 := EXTS 128 v in
   subrange_vec_dec (shift_bits_right v128 shift) 63 0.

Definition shift_right_arith32 (v : mword 32) (shift : mword 5) 
: mword 32 :=
   
   let v64 : bits 64 := EXTS 64 v in
   subrange_vec_dec (shift_bits_right v64 shift) 31 0.

Fixpoint _rec_n_leading_spaces (s : string) (_reclimit : Z)  (_acc : Acc (Zwf 0) _reclimit)
{struct _acc} : M ({n : Z & ArithFact (n >= 0)}) :=
   
   assert_exp' (Z.geb _reclimit 0) "recursion limit reached" >>= fun _ =>
   let p0_ := s in
   (if ((generic_eq p0_ "")) then returnm (build_ex (0  : Z))
    else
      let p0_ := string_take s 1 in
      (if ((generic_eq p0_ " ")) then
         (_rec_n_leading_spaces (string_drop s 1) (Z.sub _reclimit 1) (_limit_reduces _acc)) >>= fun '(existT _ w__0 _ : {n : Z & ArithFact (n >=
           0)}) =>
         returnm (build_ex
         (projT1
         (build_ex
         (Z.add 1 w__0)
          : {_atom : Z & ArithFact (exists ex4231_ , _atom = (1 + ex4231_) /\ 0 <= ex4231_)})))
       else returnm (build_ex (0  : Z)))
       : M ({n : Z & ArithFact (n >= 0)}))
    : M ({n : Z & ArithFact (n >= 0)}).

Definition n_leading_spaces (s : string) 
: M ({n : Z & ArithFact (n >= 0)}) :=
   
   (_rec_n_leading_spaces s ((projT1 (string_length s))  : Z) (Zwf_guarded _))
    : M ({n : Z & ArithFact (n >= 0)}).

Definition spc_forwards '(tt : unit)  : string :=  " ".

Definition spc_backwards (s : string)  : unit :=  tt.

Definition spc_matches_prefix (s : string) 
: M (option ((unit * {n : Z & ArithFact (n >= 0)}))) :=
   
   (n_leading_spaces s) >>= fun '(existT _ n _) =>
   let l__6 := n in
   returnm ((if sumbool_of_bool ((Z.eqb l__6 0)) then None
             else Some ((tt, build_ex n)))
    : option ((unit * {n : Z & ArithFact (n >= 0)}))).

Definition opt_spc_forwards '(tt : unit)  : string :=  "".

Definition opt_spc_backwards (s : string)  : unit :=  tt.

Definition opt_spc_matches_prefix (s : string) 
: M (option ((unit * {n : Z & ArithFact (n >= 0)}))) :=
   
   (n_leading_spaces s) >>= fun '(existT _ w__0 _ : {n : Z & ArithFact (n >= 0)}) =>
   returnm ((Some
               ((tt, build_ex
               w__0)))
    : option ((unit * {n : Z & ArithFact (n >= 0)}))).

Definition def_spc_forwards '(tt : unit)  : string :=  " ".

Definition def_spc_backwards (s : string)  : unit :=  tt.

Definition def_spc_matches_prefix (s : string) 
: M (option ((unit * {n : Z & ArithFact (n >= 0)}))) :=
   
   (opt_spc_matches_prefix s)
    : M (option ((unit * {n : Z & ArithFact (n >= 0)}))).

Definition hex_bits_1_forwards_matches (bv : mword 1)  : bool :=  true.

Definition hex_bits_1_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_1_matches_prefix s) with
           | Some ((g__79, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_1_backwards (s : string) 
: M (mword 1) :=
   
   (match (hex_bits_1_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 1)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 49:2 - 51:3" >>= fun _ =>
          exit tt)
        : M (mword 1)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 49:2 - 51:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 1).

Definition hex_bits_2_forwards_matches (bv : mword 2)  : bool :=  true.

Definition hex_bits_2_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_2_matches_prefix s) with
           | Some ((g__78, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_2_backwards (s : string) 
: M (mword 2) :=
   
   (match (hex_bits_2_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 2)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 68:2 - 70:3" >>= fun _ =>
          exit tt)
        : M (mword 2)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 68:2 - 70:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 2).

Definition hex_bits_3_forwards_matches (bv : mword 3)  : bool :=  true.

Definition hex_bits_3_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_3_matches_prefix s) with
           | Some ((g__77, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_3_backwards (s : string) 
: M (mword 3) :=
   
   (match (hex_bits_3_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 3)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 87:2 - 89:3" >>= fun _ =>
          exit tt)
        : M (mword 3)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 87:2 - 89:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 3).

Definition hex_bits_4_forwards_matches (bv : mword 4)  : bool :=  true.

Definition hex_bits_4_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_4_matches_prefix s) with
           | Some ((g__76, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_4_backwards (s : string) 
: M (mword 4) :=
   
   (match (hex_bits_4_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 4)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 106:2 - 108:3" >>= fun _ =>
          exit tt)
        : M (mword 4)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 106:2 - 108:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 4).

Definition hex_bits_5_forwards_matches (bv : mword 5)  : bool :=  true.

Definition hex_bits_5_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_5_matches_prefix s) with
           | Some ((g__75, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_5_backwards (s : string) 
: M (mword 5) :=
   
   (match (hex_bits_5_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 5)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 125:2 - 127:3" >>= fun _ =>
          exit tt)
        : M (mword 5)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 125:2 - 127:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 5).

Definition hex_bits_6_forwards_matches (bv : mword 6)  : bool :=  true.

Definition hex_bits_6_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_6_matches_prefix s) with
           | Some ((g__74, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_6_backwards (s : string) 
: M (mword 6) :=
   
   (match (hex_bits_6_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 6)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 144:2 - 146:3" >>= fun _ =>
          exit tt)
        : M (mword 6)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 144:2 - 146:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 6).

Definition hex_bits_7_forwards_matches (bv : mword 7)  : bool :=  true.

Definition hex_bits_7_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_7_matches_prefix s) with
           | Some ((g__73, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_7_backwards (s : string) 
: M (mword 7) :=
   
   (match (hex_bits_7_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 7)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 163:2 - 165:3" >>= fun _ =>
          exit tt)
        : M (mword 7)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 163:2 - 165:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 7).

Definition hex_bits_8_forwards_matches (bv : mword 8)  : bool :=  true.

Definition hex_bits_8_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_8_matches_prefix s) with
           | Some ((g__72, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_8_backwards (s : string) 
: M (mword 8) :=
   
   (match (hex_bits_8_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 8)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 182:2 - 184:3" >>= fun _ =>
          exit tt)
        : M (mword 8)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 182:2 - 184:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 8).

Definition hex_bits_9_forwards_matches (bv : mword 9)  : bool :=  true.

Definition hex_bits_9_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_9_matches_prefix s) with
           | Some ((g__71, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_9_backwards (s : string) 
: M (mword 9) :=
   
   (match (hex_bits_9_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 9)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 201:2 - 203:3" >>= fun _ =>
          exit tt)
        : M (mword 9)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 201:2 - 203:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 9).

Definition hex_bits_10_forwards_matches (bv : mword 10)  : bool :=  true.

Definition hex_bits_10_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_10_matches_prefix s) with
           | Some ((g__70, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_10_backwards (s : string) 
: M (mword 10) :=
   
   (match (hex_bits_10_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 10)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 220:2 - 222:3" >>= fun _ =>
          exit tt)
        : M (mword 10)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 220:2 - 222:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 10).

Definition hex_bits_11_forwards_matches (bv : mword 11)  : bool :=  true.

Definition hex_bits_11_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_11_matches_prefix s) with
           | Some ((g__69, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_11_backwards (s : string) 
: M (mword 11) :=
   
   (match (hex_bits_11_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 11)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 239:2 - 241:3" >>= fun _ =>
          exit tt)
        : M (mword 11)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 239:2 - 241:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 11).

Definition hex_bits_12_forwards_matches (bv : mword 12)  : bool :=  true.

Definition hex_bits_12_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_12_matches_prefix s) with
           | Some ((g__68, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_12_backwards (s : string) 
: M (mword 12) :=
   
   (match (hex_bits_12_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 12)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 258:2 - 260:3" >>= fun _ =>
          exit tt)
        : M (mword 12)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 258:2 - 260:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 12).

Definition hex_bits_13_forwards_matches (bv : mword 13)  : bool :=  true.

Definition hex_bits_13_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_13_matches_prefix s) with
           | Some ((g__67, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_13_backwards (s : string) 
: M (mword 13) :=
   
   (match (hex_bits_13_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 13)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 277:2 - 279:3" >>= fun _ =>
          exit tt)
        : M (mword 13)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 277:2 - 279:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 13).

Definition hex_bits_14_forwards_matches (bv : mword 14)  : bool :=  true.

Definition hex_bits_14_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_14_matches_prefix s) with
           | Some ((g__66, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_14_backwards (s : string) 
: M (mword 14) :=
   
   (match (hex_bits_14_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 14)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 296:2 - 298:3" >>= fun _ =>
          exit tt)
        : M (mword 14)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 296:2 - 298:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 14).

Definition hex_bits_15_forwards_matches (bv : mword 15)  : bool :=  true.

Definition hex_bits_15_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_15_matches_prefix s) with
           | Some ((g__65, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_15_backwards (s : string) 
: M (mword 15) :=
   
   (match (hex_bits_15_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 15)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 315:2 - 317:3" >>= fun _ =>
          exit tt)
        : M (mword 15)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 315:2 - 317:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 15).

Definition hex_bits_16_forwards_matches (bv : mword 16)  : bool :=  true.

Definition hex_bits_16_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_16_matches_prefix s) with
           | Some ((g__64, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_16_backwards (s : string) 
: M (mword 16) :=
   
   (match (hex_bits_16_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 16)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 334:2 - 336:3" >>= fun _ =>
          exit tt)
        : M (mword 16)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 334:2 - 336:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 16).

Definition hex_bits_17_forwards_matches (bv : mword 17)  : bool :=  true.

Definition hex_bits_17_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_17_matches_prefix s) with
           | Some ((g__63, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_17_backwards (s : string) 
: M (mword 17) :=
   
   (match (hex_bits_17_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 17)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 353:2 - 355:3" >>= fun _ =>
          exit tt)
        : M (mword 17)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 353:2 - 355:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 17).

Definition hex_bits_18_forwards_matches (bv : mword 18)  : bool :=  true.

Definition hex_bits_18_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_18_matches_prefix s) with
           | Some ((g__62, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_18_backwards (s : string) 
: M (mword 18) :=
   
   (match (hex_bits_18_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 18)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 372:2 - 374:3" >>= fun _ =>
          exit tt)
        : M (mword 18)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 372:2 - 374:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 18).

Definition hex_bits_19_forwards_matches (bv : mword 19)  : bool :=  true.

Definition hex_bits_19_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_19_matches_prefix s) with
           | Some ((g__61, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_19_backwards (s : string) 
: M (mword 19) :=
   
   (match (hex_bits_19_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 19)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 391:2 - 393:3" >>= fun _ =>
          exit tt)
        : M (mword 19)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 391:2 - 393:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 19).

Definition hex_bits_20_forwards_matches (bv : mword 20)  : bool :=  true.

Definition hex_bits_20_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_20_matches_prefix s) with
           | Some ((g__60, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_20_backwards (s : string) 
: M (mword 20) :=
   
   (match (hex_bits_20_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 20)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 410:2 - 412:3" >>= fun _ =>
          exit tt)
        : M (mword 20)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 410:2 - 412:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 20).

Definition hex_bits_21_forwards_matches (bv : mword 21)  : bool :=  true.

Definition hex_bits_21_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_21_matches_prefix s) with
           | Some ((g__59, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_21_backwards (s : string) 
: M (mword 21) :=
   
   (match (hex_bits_21_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 21)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 429:2 - 431:3" >>= fun _ =>
          exit tt)
        : M (mword 21)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 429:2 - 431:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 21).

Definition hex_bits_22_forwards_matches (bv : mword 22)  : bool :=  true.

Definition hex_bits_22_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_22_matches_prefix s) with
           | Some ((g__58, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_22_backwards (s : string) 
: M (mword 22) :=
   
   (match (hex_bits_22_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 22)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 448:2 - 450:3" >>= fun _ =>
          exit tt)
        : M (mword 22)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 448:2 - 450:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 22).

Definition hex_bits_23_forwards_matches (bv : mword 23)  : bool :=  true.

Definition hex_bits_23_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_23_matches_prefix s) with
           | Some ((g__57, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_23_backwards (s : string) 
: M (mword 23) :=
   
   (match (hex_bits_23_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 23)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 467:2 - 469:3" >>= fun _ =>
          exit tt)
        : M (mword 23)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 467:2 - 469:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 23).

Definition hex_bits_24_forwards_matches (bv : mword 24)  : bool :=  true.

Definition hex_bits_24_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_24_matches_prefix s) with
           | Some ((g__56, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_24_backwards (s : string) 
: M (mword 24) :=
   
   (match (hex_bits_24_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 24)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 486:2 - 488:3" >>= fun _ =>
          exit tt)
        : M (mword 24)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 486:2 - 488:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 24).

Definition hex_bits_25_forwards_matches (bv : mword 25)  : bool :=  true.

Definition hex_bits_25_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_25_matches_prefix s) with
           | Some ((g__55, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_25_backwards (s : string) 
: M (mword 25) :=
   
   (match (hex_bits_25_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 25)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 505:2 - 507:3" >>= fun _ =>
          exit tt)
        : M (mword 25)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 505:2 - 507:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 25).

Definition hex_bits_26_forwards_matches (bv : mword 26)  : bool :=  true.

Definition hex_bits_26_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_26_matches_prefix s) with
           | Some ((g__54, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_26_backwards (s : string) 
: M (mword 26) :=
   
   (match (hex_bits_26_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 26)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 524:2 - 526:3" >>= fun _ =>
          exit tt)
        : M (mword 26)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 524:2 - 526:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 26).

Definition hex_bits_27_forwards_matches (bv : mword 27)  : bool :=  true.

Definition hex_bits_27_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_27_matches_prefix s) with
           | Some ((g__53, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_27_backwards (s : string) 
: M (mword 27) :=
   
   (match (hex_bits_27_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 27)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 543:2 - 545:3" >>= fun _ =>
          exit tt)
        : M (mword 27)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 543:2 - 545:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 27).

Definition hex_bits_28_forwards_matches (bv : mword 28)  : bool :=  true.

Definition hex_bits_28_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_28_matches_prefix s) with
           | Some ((g__52, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_28_backwards (s : string) 
: M (mword 28) :=
   
   (match (hex_bits_28_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 28)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 562:2 - 564:3" >>= fun _ =>
          exit tt)
        : M (mword 28)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 562:2 - 564:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 28).

Definition hex_bits_29_forwards_matches (bv : mword 29)  : bool :=  true.

Definition hex_bits_29_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_29_matches_prefix s) with
           | Some ((g__51, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_29_backwards (s : string) 
: M (mword 29) :=
   
   (match (hex_bits_29_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 29)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 581:2 - 583:3" >>= fun _ =>
          exit tt)
        : M (mword 29)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 581:2 - 583:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 29).

Definition hex_bits_30_forwards_matches (bv : mword 30)  : bool :=  true.

Definition hex_bits_30_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_30_matches_prefix s) with
           | Some ((g__50, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_30_backwards (s : string) 
: M (mword 30) :=
   
   (match (hex_bits_30_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 30)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 600:2 - 602:3" >>= fun _ =>
          exit tt)
        : M (mword 30)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 600:2 - 602:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 30).

Definition hex_bits_31_forwards_matches (bv : mword 31)  : bool :=  true.

Definition hex_bits_31_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_31_matches_prefix s) with
           | Some ((g__49, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_31_backwards (s : string) 
: M (mword 31) :=
   
   (match (hex_bits_31_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 31)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 619:2 - 621:3" >>= fun _ =>
          exit tt)
        : M (mword 31)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 619:2 - 621:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 31).

Definition hex_bits_32_forwards_matches (bv : mword 32)  : bool :=  true.

Definition hex_bits_32_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_32_matches_prefix s) with
           | Some ((g__48, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_32_backwards (s : string) 
: M (mword 32) :=
   
   (match (hex_bits_32_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 32)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 638:2 - 640:3" >>= fun _ =>
          exit tt)
        : M (mword 32)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 638:2 - 640:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 32).

Definition hex_bits_33_forwards_matches (bv : mword 33)  : bool :=  true.

Definition hex_bits_33_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_33_matches_prefix s) with
           | Some ((g__47, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_33_backwards (s : string) 
: M (mword 33) :=
   
   (match (hex_bits_33_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 33)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 657:2 - 659:3" >>= fun _ =>
          exit tt)
        : M (mword 33)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 657:2 - 659:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 33).

Definition hex_bits_48_forwards_matches (bv : mword 48)  : bool :=  true.

Definition hex_bits_48_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_48_matches_prefix s) with
           | Some ((g__46, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_48_backwards (s : string) 
: M (mword 48) :=
   
   (match (hex_bits_48_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 48)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 676:2 - 678:3" >>= fun _ =>
          exit tt)
        : M (mword 48)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 676:2 - 678:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 48).

Definition hex_bits_64_forwards_matches (bv : mword 64)  : bool :=  true.

Definition hex_bits_64_backwards_matches (s : string) 
: bool :=
   
   match s with
   | s =>
      if ((match (hex_bits_64_matches_prefix s) with
           | Some ((g__45, existT _ n _)) =>
              if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then true else false
           | _ => false
           end)) then
        true
      else false
   end.

Definition hex_bits_64_backwards (s : string) 
: M (mword 64) :=
   
   (match (hex_bits_64_matches_prefix s) with
    | Some ((bv, existT _ n _)) =>
       (if sumbool_of_bool ((Z.eqb n (projT1 (string_length s)))) then returnm (bv  : mword 64)
        else
          assert_exp' false "Pattern match failure at model/prelude_mapping.sail 695:2 - 697:3" >>= fun _ =>
          exit tt)
        : M (mword 64)
    | _ =>
       assert_exp' false "Pattern match failure at model/prelude_mapping.sail 695:2 - 697:3" >>= fun _ =>
       exit tt
    end)
    : M (mword 64).

Definition default_meta : mem_meta := tt.
Hint Unfold default_meta : sail.
Definition __WriteRAM_Meta (addr : mword 64) (width : Z) (meta : unit) 
: M (unit) :=
   
   returnm (tt
    : unit).

Definition __ReadRAM_Meta (addr : mword 64) (width : Z)  : M (unit) :=  returnm (tt  : unit).

Definition write_ram
(wk : write_kind) (addr : mword 64) (width : Z) (data : mword (8 * width)) (meta : unit)
`{ArithFact (0 < width /\ width <= 16)} 
: M (bool) :=
   
   (write_mem wk 64 addr width data) >>= fun ret : bool =>
   (if sumbool_of_bool (ret) then (__WriteRAM_Meta addr width meta)  : M (unit)
    else returnm (tt  : unit)) >>
   returnm (ret
    : bool).

Definition write_ram_ea (wk : write_kind) (addr : mword 64) (width : Z)
`{ArithFact (0 < width /\ width <= 16)} 
: M (unit) :=
   
   (write_mem_ea wk 64 addr width)
    : M (unit).

Definition read_ram (rk : read_kind) (addr : mword 64) (width : Z)
`{ArithFact (0 < width /\ width <= 16)} 
: M (mword (8 * width)) :=
   
   (read_mem rk 64 addr width)
    : M (mword (8 * width)).

Axiom __TraceMemoryWrite : forall {m : Z} (n : Z) (_ : mword m) (_ : mword (8 * n)) , unit.

Axiom __TraceMemoryRead : forall {m : Z} (n : Z) (_ : mword m) (_ : mword (8 * n)) , unit.

Definition regbits_to_regno (b : mword 5) 
: {n : Z & ArithFact (0 <= n /\ n < 32)} :=
   
   build_ex(let 'r := projT1 (uint b) in
   r).

Definition rX (l__5 : Z) `{ArithFact (0 <= l__5 /\ l__5 < 32)} 
: M (mword 64) :=
   
   (if sumbool_of_bool ((Z.eqb l__5 0)) then
      returnm ((EXTZ 64 (vec_of_bits [B0;B0;B0;B0]  : mword 4))
       : mword 64)
    else if sumbool_of_bool ((Z.gtb l__5 0)) then
      read_reg Xs_ref >>= fun w__0 : vec (mword 64) 32 =>
      returnm ((vec_access_dec w__0 l__5)
       : mword 64)
    else
      assert_exp' false "Pattern match failure at model/riscv_duopod.sail 22:0 - 23:27" >>= fun _ =>
      exit tt)
    : M (mword 64).

Definition wX (r : Z) (v : mword 64) `{ArithFact (0 <= r /\ r < 32)} 
: M (unit) :=
   
   (if sumbool_of_bool ((projT1 (neq_int r 0))) then
      read_reg Xs_ref >>= fun w__0 : vec (mword 64) 32 =>
      write_reg Xs_ref (vec_update_dec w__0 r v)
       : M (unit)
    else returnm (tt  : unit))
    : M (unit).

Definition read_mem (addr : mword 64) (width : Z) `{ArithFact (width >= 0)} 
: M (mword (8 * width)) :=
   
   (MEMr 64 width (EXTZ 64 (vec_of_bits [B0;B0;B0;B0]  : mword 4)) addr)
    : M (mword (8 * width)).

Definition iop_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 5)} 
: iop :=
   
   let l__0 := arg_ in
   if sumbool_of_bool ((Z.eqb l__0 0)) then RISCV_ADDI
   else if sumbool_of_bool ((Z.eqb l__0 1)) then RISCV_SLTI
   else if sumbool_of_bool ((Z.eqb l__0 2)) then RISCV_SLTIU
   else if sumbool_of_bool ((Z.eqb l__0 3)) then RISCV_XORI
   else if sumbool_of_bool ((Z.eqb l__0 4)) then RISCV_ORI
   else RISCV_ANDI.

Definition num_of_iop (arg_ : iop) 
: {e : Z & ArithFact (0 <= e /\ e <= 5)} :=
   
   build_ex(match arg_ with
            | RISCV_ADDI => 0
            | RISCV_SLTI => 1
            | RISCV_SLTIU => 2
            | RISCV_XORI => 3
            | RISCV_ORI => 4
            | RISCV_ANDI => 5
            end).

Definition execute_LOAD (imm : mword 12) (rs1 : mword 5) (rd : mword 5) 
: M (unit) :=
   
   (rX (projT1 (regbits_to_regno rs1))) >>= fun w__0 : mword 64 =>
   let addr : xlenbits := add_vec w__0 (EXTS 64 imm) in
   (read_mem addr 8) >>= fun result : xlenbits =>
   (wX (projT1 (regbits_to_regno rd)) result)
    : M (unit).

Definition execute_ITYPE (arg0 : mword 12) (arg1 : mword 5) (arg2 : mword 5) (arg3 : iop) 
: M (unit) :=
   
   let merge_var := (arg0, arg1, arg2, arg3) in
   (match merge_var with
    | (imm, rs1, rd, RISCV_ADDI) =>
       (rX (projT1 (regbits_to_regno rs1))) >>= fun rs1_val =>
       let imm_ext : xlenbits := EXTS 64 imm in
       let result := add_vec rs1_val imm_ext in
       (wX (projT1 (regbits_to_regno rd)) result)
        : M (unit)
    | _ => exit tt  : M (unit)
    end)
    : M (unit).

Definition execute (merge_var : ast) 
: M (unit) :=
   
   (match merge_var with
    | ITYPE ((imm, rs1, rd, arg3)) => (execute_ITYPE imm rs1 rd arg3)  : M (unit)
    | LOAD ((imm, rs1, rd)) => (execute_LOAD imm rs1 rd)  : M (unit)
    end)
    : M (unit).

Definition decode (v__0 : mword 32) 
: option ast :=
   
   if ((andb (eq_vec (subrange_vec_dec v__0 14 12) (vec_of_bits [B0;B0;B0]  : mword (14 - 12 + 1)))
          (eq_vec (subrange_vec_dec v__0 6 0)
             (vec_of_bits [B0;B0;B1;B0;B0;B1;B1]  : mword (6 - 0 + 1))))) then
     let imm : bits 12 := subrange_vec_dec v__0 31 20 in
     let rs1 : regbits := subrange_vec_dec v__0 19 15 in
     let rd : regbits := subrange_vec_dec v__0 11 7 in
     let imm : bits 12 := subrange_vec_dec v__0 31 20 in
     Some
       (ITYPE
          ((imm, rs1, rd, RISCV_ADDI)))
   else if ((andb
               (eq_vec (subrange_vec_dec v__0 14 12) (vec_of_bits [B0;B1;B1]  : mword (14 - 12 + 1)))
               (eq_vec (subrange_vec_dec v__0 6 0)
                  (vec_of_bits [B0;B0;B0;B0;B0;B1;B1]  : mword (6 - 0 + 1))))) then
     let imm : bits 12 := subrange_vec_dec v__0 31 20 in
     let rs1 : regbits := subrange_vec_dec v__0 19 15 in
     let rd : regbits := subrange_vec_dec v__0 11 7 in
     let imm : bits 12 := subrange_vec_dec v__0 31 20 in
     Some
       (LOAD
          ((imm, rs1, rd)))
   else None.

Definition initial_regstate : regstate :=
{| Xs :=
     (vec_of_list_len [(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0]
                         : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0]
                                       : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0]
                                                     : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0]
                                                                   : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                             B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                             B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                             B0]
                                                                                 : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                           B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                           B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                           B0]
                                                                                               : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                         B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                         B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                         B0]
                                                                                                             : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                       B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                       B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                       B0]
                                                                                                                           : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                     B0]
                                                                                                                                         : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                   B0]
                                                                                                                                                       : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                 B0]
                                                                                                                                                                     : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                               B0]
                                                                                                                                                                                   : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                             B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                             B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                             B0]
                                                                                                                                                                                                 : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                           B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                           B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                           B0]
                                                                                                                                                                                                               : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                         B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                         B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                         B0]
                                                                                                                                                                                                                             : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                       B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                       B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                       B0]
                                                                                                                                                                                                                                           : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                     B0]
                                                                                                                                                                                                                                                         : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                   B0]
                                                                                                                                                                                                                                                                       : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                 B0]
                                                                                                                                                                                                                                                                                     : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                               B0]
                                                                                                                                                                                                                                                                                                   : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                                             B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                                             B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                                                                                                                                                             B0]
                                                                                                                                                                                                                                                                                                                 : mword 64);
                       (vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                     B0]
                         : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                   B0]
                                       : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                 B0]
                                                     : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                               B0]
                                                                   : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                             B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                             B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                             B0]
                                                                                 : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                           B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                           B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                           B0]
                                                                                               : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                         B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                         B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                         B0]
                                                                                                             : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                       B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                       B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                       B0]
                                                                                                                           : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                     B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                     B0]
                                                                                                                                         : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                   B0]
                                                                                                                                                       : mword 64);(vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                 B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                                                                                                                                                                                 B0]
                                                                                                                                                                     : mword 64)]); 
   nextPC :=
     (vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0]
       : mword 64); 
   PC :=
     (vec_of_bits [B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;
                   B0]
       : mword 64) |}.
Hint Unfold initial_regstate : sail.

End Content.
