diff options
Diffstat (limited to 'snapshot/riscv.v')
| -rw-r--r-- | snapshot/riscv.v | 1181 |
1 files changed, 1181 insertions, 0 deletions
diff --git a/snapshot/riscv.v b/snapshot/riscv.v new file mode 100644 index 0000000..472a43b --- /dev/null +++ b/snapshot/riscv.v @@ -0,0 +1,1181 @@ +(*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. + + |