path: root/snapshot/riscv.v

(*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 reg_name_forwards (arg_ : mword 5) : M (string) :=
  let b__0 := arg_ 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 unknown location" >>= fun _ => exit tt)
  : M (string).

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

Definition reg_name_forwards_matches (arg_ : mword 5) : bool :=
  let b__0 := arg_ in
  if eq_vec b__0 ('b"00000"  : mword 5) then true
  else if eq_vec b__0 ('b"00001"  : mword 5) then true
  else if eq_vec b__0 ('b"00010"  : mword 5) then true
  else if eq_vec b__0 ('b"00011"  : mword 5) then true
  else if eq_vec b__0 ('b"00100"  : mword 5) then true
  else if eq_vec b__0 ('b"00101"  : mword 5) then true
  else if eq_vec b__0 ('b"00110"  : mword 5) then true
  else if eq_vec b__0 ('b"00111"  : mword 5) then true
  else if eq_vec b__0 ('b"01000"  : mword 5) then true
  else if eq_vec b__0 ('b"01001"  : mword 5) then true
  else if eq_vec b__0 ('b"01010"  : mword 5) then true
  else if eq_vec b__0 ('b"01011"  : mword 5) then true
  else if eq_vec b__0 ('b"01100"  : mword 5) then true
  else if eq_vec b__0 ('b"01101"  : mword 5) then true
  else if eq_vec b__0 ('b"01110"  : mword 5) then true
  else if eq_vec b__0 ('b"01111"  : mword 5) then true
  else if eq_vec b__0 ('b"10000"  : mword 5) then true
  else if eq_vec b__0 ('b"10001"  : mword 5) then true
  else if eq_vec b__0 ('b"10010"  : mword 5) then true
  else if eq_vec b__0 ('b"10011"  : mword 5) then true
  else if eq_vec b__0 ('b"10100"  : mword 5) then true
  else if eq_vec b__0 ('b"10101"  : mword 5) then true
  else if eq_vec b__0 ('b"10110"  : mword 5) then true
  else if eq_vec b__0 ('b"10111"  : mword 5) then true
  else if eq_vec b__0 ('b"11000"  : mword 5) then true
  else if eq_vec b__0 ('b"11001"  : mword 5) then true
  else if eq_vec b__0 ('b"11010"  : mword 5) then true
  else if eq_vec b__0 ('b"11011"  : mword 5) then true
  else if eq_vec b__0 ('b"11100"  : mword 5) then true
  else if eq_vec b__0 ('b"11101"  : mword 5) then true
  else if eq_vec b__0 ('b"11110"  : mword 5) then true
  else if eq_vec b__0 ('b"11111"  : mword 5) then true
  else false.

Definition reg_name_backwards_matches (arg_ : string) : bool :=
  let p0_ := arg_ in
  if generic_eq p0_ "zero" then true
  else if generic_eq p0_ "ra" then true
  else if generic_eq p0_ "sp" then true
  else if generic_eq p0_ "gp" then true
  else if generic_eq p0_ "tp" then true
  else if generic_eq p0_ "t0" then true
  else if generic_eq p0_ "t1" then true
  else if generic_eq p0_ "t2" then true
  else if generic_eq p0_ "fp" then true
  else if generic_eq p0_ "s1" then true
  else if generic_eq p0_ "a0" then true
  else if generic_eq p0_ "a1" then true
  else if generic_eq p0_ "a2" then true
  else if generic_eq p0_ "a3" then true
  else if generic_eq p0_ "a4" then true
  else if generic_eq p0_ "a5" then true
  else if generic_eq p0_ "a6" then true
  else if generic_eq p0_ "a7" then true
  else if generic_eq p0_ "s2" then true
  else if generic_eq p0_ "s3" then true
  else if generic_eq p0_ "s4" then true
  else if generic_eq p0_ "s5" then true
  else if generic_eq p0_ "s6" then true
  else if generic_eq p0_ "s7" then true
  else if generic_eq p0_ "s8" then true
  else if generic_eq p0_ "s9" then true
  else if generic_eq p0_ "s10" then true
  else if generic_eq p0_ "s11" then true
  else if generic_eq p0_ "t3" then true
  else if generic_eq p0_ "t4" then true
  else if generic_eq p0_ "t5" then true
  else if generic_eq p0_ "t6" then true
  else false.

Definition _s124_ (_s125_ : string) : option string :=
  let _s126_ := _s125_ in
  if string_startswith _s126_ "t6" then
    match (string_drop _s126_ (projT1 (string_length "t6"))) with | s_ => Some s_ end
  else None.

Definition _s120_ (_s121_ : string) : option string :=
  let _s122_ := _s121_ in
  if string_startswith _s122_ "t5" then
    match (string_drop _s122_ (projT1 (string_length "t5"))) with | s_ => Some s_ end
  else None.

Definition _s116_ (_s117_ : string) : option string :=
  let _s118_ := _s117_ in
  if string_startswith _s118_ "t4" then
    match (string_drop _s118_ (projT1 (string_length "t4"))) with | s_ => Some s_ end
  else None.

Definition _s112_ (_s113_ : string) : option string :=
  let _s114_ := _s113_ in
  if string_startswith _s114_ "t3" then
    match (string_drop _s114_ (projT1 (string_length "t3"))) with | s_ => Some s_ end
  else None.

Definition _s108_ (_s109_ : string) : option string :=
  let _s110_ := _s109_ in
  if string_startswith _s110_ "s11" then
    match (string_drop _s110_ (projT1 (string_length "s11"))) with | s_ => Some s_ end
  else None.

Definition _s104_ (_s105_ : string) : option string :=
  let _s106_ := _s105_ in
  if string_startswith _s106_ "s10" then
    match (string_drop _s106_ (projT1 (string_length "s10"))) with | s_ => Some s_ end
  else None.

Definition _s100_ (_s101_ : string) : option string :=
  let _s102_ := _s101_ in
  if string_startswith _s102_ "s9" then
    match (string_drop _s102_ (projT1 (string_length "s9"))) with | s_ => Some s_ end
  else None.

Definition _s96_ (_s97_ : string) : option string :=
  let _s98_ := _s97_ in
  if string_startswith _s98_ "s8" then
    match (string_drop _s98_ (projT1 (string_length "s8"))) with | s_ => Some s_ end
  else None.

Definition _s92_ (_s93_ : string) : option string :=
  let _s94_ := _s93_ in
  if string_startswith _s94_ "s7" then
    match (string_drop _s94_ (projT1 (string_length "s7"))) with | s_ => Some s_ end
  else None.

Definition _s88_ (_s89_ : string) : option string :=
  let _s90_ := _s89_ in
  if string_startswith _s90_ "s6" then
    match (string_drop _s90_ (projT1 (string_length "s6"))) with | s_ => Some s_ end
  else None.

Definition _s84_ (_s85_ : string) : option string :=
  let _s86_ := _s85_ in
  if string_startswith _s86_ "s5" then
    match (string_drop _s86_ (projT1 (string_length "s5"))) with | s_ => Some s_ end
  else None.

Definition _s80_ (_s81_ : string) : option string :=
  let _s82_ := _s81_ in
  if string_startswith _s82_ "s4" then
    match (string_drop _s82_ (projT1 (string_length "s4"))) with | s_ => Some s_ end
  else None.

Definition _s76_ (_s77_ : string) : option string :=
  let _s78_ := _s77_ in
  if string_startswith _s78_ "s3" then
    match (string_drop _s78_ (projT1 (string_length "s3"))) with | s_ => Some s_ end
  else None.

Definition _s72_ (_s73_ : string) : option string :=
  let _s74_ := _s73_ in
  if string_startswith _s74_ "s2" then
    match (string_drop _s74_ (projT1 (string_length "s2"))) with | s_ => Some s_ end
  else None.

Definition _s68_ (_s69_ : string) : option string :=
  let _s70_ := _s69_ in
  if string_startswith _s70_ "a7" then
    match (string_drop _s70_ (projT1 (string_length "a7"))) with | s_ => Some s_ end
  else None.

Definition _s64_ (_s65_ : string) : option string :=
  let _s66_ := _s65_ in
  if string_startswith _s66_ "a6" then
    match (string_drop _s66_ (projT1 (string_length "a6"))) with | s_ => Some s_ end
  else None.

Definition _s60_ (_s61_ : string) : option string :=
  let _s62_ := _s61_ in
  if string_startswith _s62_ "a5" then
    match (string_drop _s62_ (projT1 (string_length "a5"))) with | s_ => Some s_ end
  else None.

Definition _s56_ (_s57_ : string) : option string :=
  let _s58_ := _s57_ in
  if string_startswith _s58_ "a4" then
    match (string_drop _s58_ (projT1 (string_length "a4"))) with | s_ => Some s_ end
  else None.

Definition _s52_ (_s53_ : string) : option string :=
  let _s54_ := _s53_ in
  if string_startswith _s54_ "a3" then
    match (string_drop _s54_ (projT1 (string_length "a3"))) with | s_ => Some s_ end
  else None.

Definition _s48_ (_s49_ : string) : option string :=
  let _s50_ := _s49_ in
  if string_startswith _s50_ "a2" then
    match (string_drop _s50_ (projT1 (string_length "a2"))) with | s_ => Some s_ end
  else None.

Definition _s44_ (_s45_ : string) : option string :=
  let _s46_ := _s45_ in
  if string_startswith _s46_ "a1" then
    match (string_drop _s46_ (projT1 (string_length "a1"))) with | s_ => Some s_ end
  else None.

Definition _s40_ (_s41_ : string) : option string :=
  let _s42_ := _s41_ in
  if string_startswith _s42_ "a0" then
    match (string_drop _s42_ (projT1 (string_length "a0"))) with | s_ => Some s_ end
  else None.

Definition _s36_ (_s37_ : string) : option string :=
  let _s38_ := _s37_ in
  if string_startswith _s38_ "s1" then
    match (string_drop _s38_ (projT1 (string_length "s1"))) with | s_ => Some s_ end
  else None.

Definition _s32_ (_s33_ : string) : option string :=
  let _s34_ := _s33_ in
  if string_startswith _s34_ "fp" then
    match (string_drop _s34_ (projT1 (string_length "fp"))) with | s_ => Some s_ end
  else None.

Definition _s28_ (_s29_ : string) : option string :=
  let _s30_ := _s29_ in
  if string_startswith _s30_ "t2" then
    match (string_drop _s30_ (projT1 (string_length "t2"))) with | s_ => Some s_ end
  else None.

Definition _s24_ (_s25_ : string) : option string :=
  let _s26_ := _s25_ in
  if string_startswith _s26_ "t1" then
    match (string_drop _s26_ (projT1 (string_length "t1"))) with | s_ => Some s_ end
  else None.

Definition _s20_ (_s21_ : string) : option string :=
  let _s22_ := _s21_ in
  if string_startswith _s22_ "t0" then
    match (string_drop _s22_ (projT1 (string_length "t0"))) with | s_ => Some s_ end
  else None.

Definition _s16_ (_s17_ : string) : option string :=
  let _s18_ := _s17_ in
  if string_startswith _s18_ "tp" then
    match (string_drop _s18_ (projT1 (string_length "tp"))) with | s_ => Some s_ end
  else None.

Definition _s12_ (_s13_ : string) : option string :=
  let _s14_ := _s13_ in
  if string_startswith _s14_ "gp" then
    match (string_drop _s14_ (projT1 (string_length "gp"))) with | s_ => Some s_ end
  else None.

Definition _s8_ (_s9_ : string) : option string :=
  let _s10_ := _s9_ in
  if string_startswith _s10_ "sp" then
    match (string_drop _s10_ (projT1 (string_length "sp"))) with | s_ => Some s_ end
  else None.

Definition _s4_ (_s5_ : string) : option string :=
  let _s6_ := _s5_ in
  if string_startswith _s6_ "ra" then
    match (string_drop _s6_ (projT1 (string_length "ra"))) with | s_ => Some s_ end
  else None.

Definition _s0_ (_s1_ : string) : option string :=
  let _s2_ := _s1_ in
  if string_startswith _s2_ "zero" then
    match (string_drop _s2_ (projT1 (string_length "zero"))) with | s_ => Some s_ end
  else None.

Definition reg_name_matches_prefix (arg_ : string)
  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)}))) :=
  let _s3_ := arg_ in
  (if match (_s0_ _s3_) with | Some s_ => true | _ => false end then
     (match (_s0_ _s3_) with
      | Some s_ =>
        returnm (Some
                   ('b"00000"
                    : mword 5, build_ex
                                 (projT1
                                    (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
      | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
      end)
     : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s4_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s4_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"00001"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s8_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s8_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"00010"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s12_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s12_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"00011"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s16_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s16_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"00100"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s20_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s20_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"00101"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s24_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s24_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"00110"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s28_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s28_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"00111"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s32_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s32_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"01000"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s36_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s36_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"01001"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s40_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s40_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"01010"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s44_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s44_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"01011"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s48_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s48_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"01100"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s52_ _s3_) with | Some s_ => true | _ => false end then
               (match (_s52_ _s3_) with
                | Some s_ =>
                  returnm (Some
                             ('b"01101"
                              : mword 5, build_ex
                                           (projT1
                                              (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
                | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
                end)
               : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s56_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s56_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"01110"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s60_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s60_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"01111"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s64_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s64_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"10000"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s68_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s68_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"10001"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s72_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s72_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"10010"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s76_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s76_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"10011"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s80_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s80_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"10100"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s84_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s84_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"10101"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s88_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s88_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"10110"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s92_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s92_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"10111"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s96_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s96_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"11000"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s100_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s100_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"11001"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s104_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s104_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"11010"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s108_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s108_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"11011"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s112_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s112_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"11100"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s116_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s116_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"11101"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s120_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s120_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"11110"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s124_ _s3_) with | Some s_ => true | _ => false end then
          (match (_s124_ _s3_) with
           | Some s_ =>
             returnm (Some
                        ('b"11111"
                         : mword 5, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)})))
        else returnm None) : M (option ((mword 5 * {n : Z & ArithFact (n >=? 0)}))).

Definition creg_name_forwards (arg_ : mword 3) : M (string) :=
  let b__0 := arg_ in
  (if eq_vec b__0 ('b"000"  : mword 3) then returnm "s0"
   else if eq_vec b__0 ('b"001"  : mword 3) then returnm "s1"
   else if eq_vec b__0 ('b"010"  : mword 3) then returnm "a0"
   else if eq_vec b__0 ('b"011"  : mword 3) then returnm "a1"
   else if eq_vec b__0 ('b"100"  : mword 3) then returnm "a2"
   else if eq_vec b__0 ('b"101"  : mword 3) then returnm "a3"
   else if eq_vec b__0 ('b"110"  : mword 3) then returnm "a4"
   else if eq_vec b__0 ('b"111"  : mword 3) then returnm "a5"
   else assert_exp' false "Pattern match failure at unknown location" >>= fun _ => exit tt)
  : M (string).

Definition creg_name_backwards (arg_ : string) : M (mword 3) :=
  let p0_ := arg_ in
  (if generic_eq p0_ "s0" then returnm ('b"000"  : mword 3)
   else if generic_eq p0_ "s1" then returnm ('b"001"  : mword 3)
   else if generic_eq p0_ "a0" then returnm ('b"010"  : mword 3)
   else if generic_eq p0_ "a1" then returnm ('b"011"  : mword 3)
   else if generic_eq p0_ "a2" then returnm ('b"100"  : mword 3)
   else if generic_eq p0_ "a3" then returnm ('b"101"  : mword 3)
   else if generic_eq p0_ "a4" then returnm ('b"110"  : mword 3)
   else if generic_eq p0_ "a5" then returnm ('b"111"  : mword 3)
   else assert_exp' false "Pattern match failure at unknown location" >>= fun _ => exit tt)
  : M (mword 3).

Definition creg_name_forwards_matches (arg_ : mword 3) : bool :=
  let b__0 := arg_ in
  if eq_vec b__0 ('b"000"  : mword 3) then true
  else if eq_vec b__0 ('b"001"  : mword 3) then true
  else if eq_vec b__0 ('b"010"  : mword 3) then true
  else if eq_vec b__0 ('b"011"  : mword 3) then true
  else if eq_vec b__0 ('b"100"  : mword 3) then true
  else if eq_vec b__0 ('b"101"  : mword 3) then true
  else if eq_vec b__0 ('b"110"  : mword 3) then true
  else if eq_vec b__0 ('b"111"  : mword 3) then true
 else false.

Definition creg_name_backwards_matches (arg_ : string) : bool :=
  let p0_ := arg_ in
  if generic_eq p0_ "s0" then true
  else if generic_eq p0_ "s1" then true
  else if generic_eq p0_ "a0" then true
  else if generic_eq p0_ "a1" then true
  else if generic_eq p0_ "a2" then true
  else if generic_eq p0_ "a3" then true
  else if generic_eq p0_ "a4" then true
  else if generic_eq p0_ "a5" then true
  else false.

Definition _s156_ (_s157_ : string) : option string :=
  let _s158_ := _s157_ in
  if string_startswith _s158_ "a5" then
    match (string_drop _s158_ (projT1 (string_length "a5"))) with | s_ => Some s_ end
  else None.

Definition _s152_ (_s153_ : string) : option string :=
  let _s154_ := _s153_ in
  if string_startswith _s154_ "a4" then
    match (string_drop _s154_ (projT1 (string_length "a4"))) with | s_ => Some s_ end
  else None.

Definition _s148_ (_s149_ : string) : option string :=
  let _s150_ := _s149_ in
  if string_startswith _s150_ "a3" then
    match (string_drop _s150_ (projT1 (string_length "a3"))) with | s_ => Some s_ end
  else None.

Definition _s144_ (_s145_ : string) : option string :=
  let _s146_ := _s145_ in
  if string_startswith _s146_ "a2" then
    match (string_drop _s146_ (projT1 (string_length "a2"))) with | s_ => Some s_ end
  else None.

Definition _s140_ (_s141_ : string) : option string :=
  let _s142_ := _s141_ in
  if string_startswith _s142_ "a1" then
    match (string_drop _s142_ (projT1 (string_length "a1"))) with | s_ => Some s_ end
  else None.

Definition _s136_ (_s137_ : string) : option string :=
  let _s138_ := _s137_ in
  if string_startswith _s138_ "a0" then
    match (string_drop _s138_ (projT1 (string_length "a0"))) with | s_ => Some s_ end
  else None.

Definition _s132_ (_s133_ : string) : option string :=
  let _s134_ := _s133_ in
  if string_startswith _s134_ "s1" then
    match (string_drop _s134_ (projT1 (string_length "s1"))) with | s_ => Some s_ end
  else None.

Definition _s128_ (_s129_ : string) : option string :=
  let _s130_ := _s129_ in
  if string_startswith _s130_ "s0" then
    match (string_drop _s130_ (projT1 (string_length "s0"))) with | s_ => Some s_ end
  else None.

Definition creg_name_matches_prefix (arg_ : string)
  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)}))) :=
  let _s131_ := arg_ in
  (if match (_s128_ _s131_) with | Some s_ => true | _ => false end then
     (match (_s128_ _s131_) with
      | Some s_ =>
        returnm (Some
                   ('b"000"
                    : mword 3, build_ex
                                 (projT1
                                    (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
      | _ => exit tt  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
      end)
     : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s132_ _s131_) with | Some s_ => true | _ => false end then
          (match (_s132_ _s131_) with
           | Some s_ =>
             returnm (Some
                        ('b"001"
                         : mword 3, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s136_ _s131_) with | Some s_ => true | _ => false end then
          (match (_s136_ _s131_) with
           | Some s_ =>
             returnm (Some
                        ('b"010"
                         : mword 3, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
           end)
               : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s140_ _s131_) with | Some s_ => true | _ => false end then
          (match (_s140_ _s131_) with
           | Some s_ =>
             returnm (Some
                        ('b"011"
                         : mword 3, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s144_ _s131_) with | Some s_ => true | _ => false end then
          (match (_s144_ _s131_) with
           | Some s_ =>
             returnm (Some
                        ('b"100"
                         : mword 3, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s148_ _s131_) with | Some s_ => true | _ => false end then
          (match (_s148_ _s131_) with
           | Some s_ =>
             returnm (Some
                        ('b"101"
                         : mword 3, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s152_ _s131_) with | Some s_ => true | _ => false end then
          (match (_s152_ _s131_) with
           | Some s_ =>
             returnm (Some
                        ('b"110"
                         : mword 3, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
   else if match (_s156_ _s131_) with | Some s_ => true | _ => false end then
          (match (_s156_ _s131_) with
           | Some s_ =>
             returnm (Some
                        ('b"111"
                         : mword 3, build_ex
                                      (projT1
                                         (sub_nat (projT1 (string_length arg_)) (projT1 (string_length s_))))))
           | _ => exit tt  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
           end)
          : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)})))
   else returnm None)
  : M (option ((mword 3 * {n : Z & ArithFact (n >=? 0)}))).

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.