path: root/prover_snapshots/coq/duopod/riscv_duopod.v

(*Generated by Sail from riscv_duopod.*)
Require Import Sail.Base.
Require Import Sail.Real.
Require Import riscv_duopod_types.
Require Import mem_metadata.
Require Import riscv_extras.
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 _shl_int_general (m : Z) (n : Z) : Z :=
   if sumbool_of_bool (Z.geb n 0) then shl_int m n else shr_int m (Z.opp n).

Definition _shr_int_general (m : Z) (n : Z) : Z :=
   if sumbool_of_bool (Z.geb n 0) then shr_int m n else shl_int m (Z.opp n).

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 read_kind_of_num (arg_ : Z) `{ArithFact ((0 <=? arg_) && (arg_ <=? 11))} : read_kind :=
   let l__33 := arg_ in
   if sumbool_of_bool (Z.eqb l__33 0) then Read_plain
   else if sumbool_of_bool (Z.eqb l__33 1) then Read_reserve
   else if sumbool_of_bool (Z.eqb l__33 2) then Read_acquire
   else if sumbool_of_bool (Z.eqb l__33 3) then Read_exclusive
   else if sumbool_of_bool (Z.eqb l__33 4) then Read_exclusive_acquire
   else if sumbool_of_bool (Z.eqb l__33 5) then Read_stream
   else if sumbool_of_bool (Z.eqb l__33 6) then Read_RISCV_acquire
   else if sumbool_of_bool (Z.eqb l__33 7) then Read_RISCV_strong_acquire
   else if sumbool_of_bool (Z.eqb l__33 8) then Read_RISCV_reserved
   else if sumbool_of_bool (Z.eqb l__33 9) then Read_RISCV_reserved_acquire
   else if sumbool_of_bool (Z.eqb l__33 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__23 := arg_ in
   if sumbool_of_bool (Z.eqb l__23 0) then Write_plain
   else if sumbool_of_bool (Z.eqb l__23 1) then Write_conditional
   else if sumbool_of_bool (Z.eqb l__23 2) then Write_release
   else if sumbool_of_bool (Z.eqb l__23 3) then Write_exclusive
   else if sumbool_of_bool (Z.eqb l__23 4) then Write_exclusive_release
   else if sumbool_of_bool (Z.eqb l__23 5) then Write_RISCV_release
   else if sumbool_of_bool (Z.eqb l__23 6) then Write_RISCV_strong_release
   else if sumbool_of_bool (Z.eqb l__23 7) then Write_RISCV_conditional
   else if sumbool_of_bool (Z.eqb l__23 8) then Write_RISCV_conditional_release
   else if sumbool_of_bool (Z.eqb l__23 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__20 := arg_ in
   if sumbool_of_bool (Z.eqb l__20 0) then A64_FullShare
   else if sumbool_of_bool (Z.eqb l__20 1) then A64_InnerShare
   else if sumbool_of_bool (Z.eqb l__20 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__18 := arg_ in
   if sumbool_of_bool (Z.eqb l__18 0) then A64_barrier_all
   else if sumbool_of_bool (Z.eqb l__18 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__16 := arg_ in
   if sumbool_of_bool (Z.eqb l__16 0) then Transaction_start
   else if sumbool_of_bool (Z.eqb l__16 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__6 := arg_ in
   if sumbool_of_bool (Z.eqb l__6 0) then Cache_op_D_IVAC
   else if sumbool_of_bool (Z.eqb l__6 1) then Cache_op_D_ISW
   else if sumbool_of_bool (Z.eqb l__6 2) then Cache_op_D_CSW
   else if sumbool_of_bool (Z.eqb l__6 3) then Cache_op_D_CISW
   else if sumbool_of_bool (Z.eqb l__6 4) then Cache_op_D_ZVA
   else if sumbool_of_bool (Z.eqb l__6 5) then Cache_op_D_CVAC
   else if sumbool_of_bool (Z.eqb l__6 6) then Cache_op_D_CVAU
   else if sumbool_of_bool (Z.eqb l__6 7) then Cache_op_D_CIVAC
   else if sumbool_of_bool (Z.eqb l__6 8) then Cache_op_I_IALLUIS
   else if sumbool_of_bool (Z.eqb l__6 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 not_bit (b : bitU) : bitU := if eq_bit b B1 then B0 else B1.

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



Definition string_of_bit (b : bitU) : M (string) :=
   (match b with | B0 => returnm "0b0" | B1 => returnm "0b1" | _ => exit tt  : M (string) end)
    : M (string).

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 ('b"0"  : 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 'b"1"  : mword 1 else 'b"0"  : mword 1.

Definition bit_to_bool (b : bitU) : M (bool) :=
   (match b with | B1 => returnm true | B0 => returnm false | _ => 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.

Axiom spc_forwards_matches : forall  (_ : unit) , bool.

Axiom spc_backwards_matches : forall  (_ : string) , bool.

Axiom opt_spc_forwards_matches : forall  (_ : unit) , bool.

Axiom opt_spc_backwards_matches : forall  (_ : string) , bool.

Axiom def_spc_forwards_matches : forall  (_ : unit) , bool.

Axiom def_spc_backwards_matches : forall  (_ : string) , bool.

Axiom hex_bits_forwards : forall {n : Z} (_ : (Z * mword n)) , string.

Axiom hex_bits_backwards : forall {n : Z} (_ : string) , (Z * mword n).

Axiom hex_bits_forwards_matches : forall {n : Z} (_ : (Z * mword n)) , bool.

Axiom hex_bits_backwards_matches : forall  (_ : string) , bool.

Axiom hex_bits_matches_prefix : forall
{n : Z}
(_ : string)
,
option (((Z * mword n) * {n : Z & ArithFact (n >=? 0)})).

Fixpoint _rec_n_leading_spaces (s : string) (_reclimit : Z) (_acc : Acc (Zwf 0) _reclimit)
{struct _acc} : M ({n : Z & ArithFact (n >=? 0)}).
exact (
   assert_exp' (Z.geb _reclimit 0) "recursion limit reached" >>= fun _ =>
   let p0_ := s in
   (if generic_eq p0_ "" then returnm (build_ex 0)
    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 (Z.add 1 w__0))
       else returnm (build_ex 0))
       : M ({n : Z & ArithFact (n >=? 0)}))
    : M ({n : Z & ArithFact (n >=? 0)})
).
Defined.


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__5 := n in
   returnm (if sumbool_of_bool (Z.eqb l__5 0) then None else Some (tt, build_ex n)).

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)).

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 rX (r : mword 5) : M (mword 64) :=
   let b__0 := r in
   (if eq_vec b__0 ('b"00000"  : mword 5) then returnm (EXTZ 64 (Ox"0"  : mword 4))
    else
      read_reg Xs_ref >>= fun w__0 : vec (mword 64) 32 =>
      returnm (vec_access_dec w__0 (projT1 (uint r))))
    : M (mword 64).

Definition wX (r : mword 5) (v : mword 64) : M (unit) :=
   (if neq_vec r ('b"00000"  : mword 5) then
      read_reg Xs_ref >>= fun w__0 : vec (mword 64) 32 =>
      write_reg Xs_ref (vec_update_dec w__0 (projT1 (uint r)) v)
       : M (unit)
    else returnm tt)
    : M (unit).

Definition read_mem (addr : mword 64) (width : Z) `{ArithFact (width >=? 0)} : M (mword (8 * width)) :=
   (MEMr 64 width (EXTZ 64 (Ox"0"  : 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 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 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 rs1) >>= fun rs1_val =>
       let imm_ext : xlenbits := EXTS 64 imm in
       let result := add_vec rs1_val imm_ext in
       (wX 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) ('b"000"  : mword (14 - 12 + 1)))
        (eq_vec (subrange_vec_dec v__0 6 0) ('b"0010011"  : 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) ('b"011"  : mword (14 - 12 + 1)))
             (eq_vec (subrange_vec_dec v__0 6 0) ('b"0000011"  : 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 [Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64;Ox"0000000000000000"  : mword 64;
                       Ox"0000000000000000"
                        : mword 64;Ox"0000000000000000"  : mword 64]); 
   nextPC := (Ox"0000000000000000"  : mword 64); 
   PC := (Ox"0000000000000000"  : mword 64) |}.
Hint Unfold initial_regstate : sail.