(*Generated by Sail from riscv.*)
Require Import Sail.Base.
Require Import Sail.Real.
Require Import riscv_types.
Import ListNotations.
Open Scope string.
Open Scope bool.
Open Scope Z.


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)} := build_ex (true).

Definition neq_int (x : Z) (y : Z) : {_bool : bool & ArithFact (Bool.eqb (negb (x =? y)) _bool)} :=
   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 fdiv_int (n : Z) (m : Z) : Z :=
   if sumbool_of_bool (andb (Z.ltb n 0) (Z.gtb m 0)) then Z.sub (Z.quot (Z.add n 1) m) 1
   else if sumbool_of_bool (andb (Z.gtb n 0) (Z.ltb m 0)) then Z.sub (Z.quot (Z.sub n 1) m) 1
   else Z.quot n m.

Definition fmod_int (n : Z) (m : Z) : Z := Z.sub n (Z.mul m (fdiv_int n m)).

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 ('b"1"  : bits 1) in
     shiftl (sub_vec (shiftl one l) one) i.

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 zero_reg : regtype := EXTZ 64 (Ox"0"  : mword 4).
Hint Unfold zero_reg : sail.
Definition regval_from_reg (r : mword 64) : mword 64 := r.

Definition regval_into_reg (v : mword 64) : mword 64 := v.

Definition rX (r : Z) `{ArithFact ((0 <=? r) && (r <? 32))} : M (mword 64) :=
   let l__32 := r in
   (if sumbool_of_bool (Z.eqb l__32 0) then returnm zero_reg
    else if sumbool_of_bool (Z.eqb l__32 1) then ((read_reg x1_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 2) then ((read_reg x2_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 3) then ((read_reg x3_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 4) then ((read_reg x4_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 5) then ((read_reg x5_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 6) then ((read_reg x6_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 7) then ((read_reg x7_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 8) then ((read_reg x8_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 9) then ((read_reg x9_ref)  : M (mword 64))  : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 10) then
      ((read_reg x10_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 11) then
      ((read_reg x11_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 12) then
      ((read_reg x12_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 13) then
      ((read_reg x13_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 14) then
      ((read_reg x14_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 15) then
      ((read_reg x15_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 16) then
      ((read_reg x16_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 17) then
      ((read_reg x17_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 18) then
      ((read_reg x18_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 19) then
      ((read_reg x19_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 20) then
      ((read_reg x20_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 21) then
      ((read_reg x21_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 22) then
      ((read_reg x22_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 23) then
      ((read_reg x23_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 24) then
      ((read_reg x24_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 25) then
      ((read_reg x25_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 26) then
      ((read_reg x26_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 27) then
      ((read_reg x27_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 28) then
      ((read_reg x28_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 29) then
      ((read_reg x29_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 30) then
      ((read_reg x30_ref)  : M (mword 64))
       : M (mword 64)
    else if sumbool_of_bool (Z.eqb l__32 31) then
      ((read_reg x31_ref)  : M (mword 64))
       : M (mword 64)
    else assert_exp' false "invalid register number" >>= fun _ => exit tt) >>= fun v : regtype =>
   returnm (regval_from_reg v).

Definition wX (r : Z) (in_v : mword 64) `{ArithFact ((0 <=? r) && (r <? 32))} : M (unit) :=
   let v := regval_into_reg in_v in
   let l__0 := r in
   (if sumbool_of_bool (Z.eqb l__0 0) then returnm tt
    else if sumbool_of_bool (Z.eqb l__0 1) then write_reg x1_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 2) then write_reg x2_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 3) then write_reg x3_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 4) then write_reg x4_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 5) then write_reg x5_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 6) then write_reg x6_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 7) then write_reg x7_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 8) then write_reg x8_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 9) then write_reg x9_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 10) then write_reg x10_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 11) then write_reg x11_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 12) then write_reg x12_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 13) then write_reg x13_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 14) then write_reg x14_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 15) then write_reg x15_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 16) then write_reg x16_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 17) then write_reg x17_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 18) then write_reg x18_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 19) then write_reg x19_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 20) then write_reg x20_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 21) then write_reg x21_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 22) then write_reg x22_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 23) then write_reg x23_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 24) then write_reg x24_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 25) then write_reg x25_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 26) then write_reg x26_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 27) then write_reg x27_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 28) then write_reg x28_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 29) then write_reg x29_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 30) then write_reg x30_ref v  : M (unit)
    else if sumbool_of_bool (Z.eqb l__0 31) then write_reg x31_ref v  : M (unit)
    else assert_exp' false "invalid register number" >>= fun _ => exit tt)
    : M (unit).

Definition rX_bits (i : mword 5) : M (mword 64) := (rX (projT1 (uint i)))  : M (mword 64).

Definition wX_bits (i : mword 5) (data : mword 64) : M (unit) :=
   (wX (projT1 (uint i)) data)  : M (unit).

Definition reg_name_abi (r : mword 5) : M (string) :=
   let b__0 := r in
   (if eq_vec b__0 ('b"00000"  : mword 5) then returnm "zero"
    else if eq_vec b__0 ('b"00001"  : mword 5) then returnm "ra"
    else if eq_vec b__0 ('b"00010"  : mword 5) then returnm "sp"
    else if eq_vec b__0 ('b"00011"  : mword 5) then returnm "gp"
    else if eq_vec b__0 ('b"00100"  : mword 5) then returnm "tp"
    else if eq_vec b__0 ('b"00101"  : mword 5) then returnm "t0"
    else if eq_vec b__0 ('b"00110"  : mword 5) then returnm "t1"
    else if eq_vec b__0 ('b"00111"  : mword 5) then returnm "t2"
    else if eq_vec b__0 ('b"01000"  : mword 5) then returnm "fp"
    else if eq_vec b__0 ('b"01001"  : mword 5) then returnm "s1"
    else if eq_vec b__0 ('b"01010"  : mword 5) then returnm "a0"
    else if eq_vec b__0 ('b"01011"  : mword 5) then returnm "a1"
    else if eq_vec b__0 ('b"01100"  : mword 5) then returnm "a2"
    else if eq_vec b__0 ('b"01101"  : mword 5) then returnm "a3"
    else if eq_vec b__0 ('b"01110"  : mword 5) then returnm "a4"
    else if eq_vec b__0 ('b"01111"  : mword 5) then returnm "a5"
    else if eq_vec b__0 ('b"10000"  : mword 5) then returnm "a6"
    else if eq_vec b__0 ('b"10001"  : mword 5) then returnm "a7"
    else if eq_vec b__0 ('b"10010"  : mword 5) then returnm "s2"
    else if eq_vec b__0 ('b"10011"  : mword 5) then returnm "s3"
    else if eq_vec b__0 ('b"10100"  : mword 5) then returnm "s4"
    else if eq_vec b__0 ('b"10101"  : mword 5) then returnm "s5"
    else if eq_vec b__0 ('b"10110"  : mword 5) then returnm "s6"
    else if eq_vec b__0 ('b"10111"  : mword 5) then returnm "s7"
    else if eq_vec b__0 ('b"11000"  : mword 5) then returnm "s8"
    else if eq_vec b__0 ('b"11001"  : mword 5) then returnm "s9"
    else if eq_vec b__0 ('b"11010"  : mword 5) then returnm "s10"
    else if eq_vec b__0 ('b"11011"  : mword 5) then returnm "s11"
    else if eq_vec b__0 ('b"11100"  : mword 5) then returnm "t3"
    else if eq_vec b__0 ('b"11101"  : mword 5) then returnm "t4"
    else if eq_vec b__0 ('b"11110"  : mword 5) then returnm "t5"
    else if eq_vec b__0 ('b"11111"  : mword 5) then returnm "t6"
    else
      assert_exp' false "Pattern match failure at riscv_regs.sail 160:2 - 193:3" >>= fun _ =>
      exit tt)
    : M (string).

Definition init_base_regs '(tt : unit) : M (unit) :=
   write_reg x1_ref zero_reg >>
   write_reg x2_ref zero_reg >>
   write_reg x3_ref zero_reg >>
   write_reg x4_ref zero_reg >>
   write_reg x5_ref zero_reg >>
   write_reg x6_ref zero_reg >>
   write_reg x7_ref zero_reg >>
   write_reg x8_ref zero_reg >>
   write_reg x9_ref zero_reg >>
   write_reg x10_ref zero_reg >>
   write_reg x11_ref zero_reg >>
   write_reg x12_ref zero_reg >>
   write_reg x13_ref zero_reg >>
   write_reg x14_ref zero_reg >>
   write_reg x15_ref zero_reg >>
   write_reg x16_ref zero_reg >>
   write_reg x17_ref zero_reg >>
   write_reg x18_ref zero_reg >>
   write_reg x19_ref zero_reg >>
   write_reg x20_ref zero_reg >>
   write_reg x21_ref zero_reg >>
   write_reg x22_ref zero_reg >>
   write_reg x23_ref zero_reg >>
   write_reg x24_ref zero_reg >>
   write_reg x25_ref zero_reg >>
   write_reg x26_ref zero_reg >>
   write_reg x27_ref zero_reg >>
   write_reg x28_ref zero_reg >>
   write_reg x29_ref zero_reg >>
   write_reg x30_ref zero_reg >> write_reg x31_ref zero_reg  : M (unit).

Definition initial_regstate : regstate :=
{| x31 := (Ox"0000000000000000"  : mword 64); 
   x30 := (Ox"0000000000000000"  : mword 64); 
   x29 := (Ox"0000000000000000"  : mword 64); 
   x28 := (Ox"0000000000000000"  : mword 64); 
   x27 := (Ox"0000000000000000"  : mword 64); 
   x26 := (Ox"0000000000000000"  : mword 64); 
   x25 := (Ox"0000000000000000"  : mword 64); 
   x24 := (Ox"0000000000000000"  : mword 64); 
   x23 := (Ox"0000000000000000"  : mword 64); 
   x22 := (Ox"0000000000000000"  : mword 64); 
   x21 := (Ox"0000000000000000"  : mword 64); 
   x20 := (Ox"0000000000000000"  : mword 64); 
   x19 := (Ox"0000000000000000"  : mword 64); 
   x18 := (Ox"0000000000000000"  : mword 64); 
   x17 := (Ox"0000000000000000"  : mword 64); 
   x16 := (Ox"0000000000000000"  : mword 64); 
   x15 := (Ox"0000000000000000"  : mword 64); 
   x14 := (Ox"0000000000000000"  : mword 64); 
   x13 := (Ox"0000000000000000"  : mword 64); 
   x12 := (Ox"0000000000000000"  : mword 64); 
   x11 := (Ox"0000000000000000"  : mword 64); 
   x10 := (Ox"0000000000000000"  : mword 64); 
   x9 := (Ox"0000000000000000"  : mword 64); 
   x8 := (Ox"0000000000000000"  : mword 64); 
   x7 := (Ox"0000000000000000"  : mword 64); 
   x6 := (Ox"0000000000000000"  : mword 64); 
   x5 := (Ox"0000000000000000"  : mword 64); 
   x4 := (Ox"0000000000000000"  : mword 64); 
   x3 := (Ox"0000000000000000"  : mword 64); 
   x2 := (Ox"0000000000000000"  : mword 64); 
   x1 := (Ox"0000000000000000"  : mword 64); 
   instbits := (Ox"0000000000000000"  : mword 64); 
   nextPC := (Ox"0000000000000000"  : mword 64); 
   PC := (Ox"0000000000000000"  : mword 64) |}.
Hint Unfold initial_regstate : sail.