Initial; working SAIL RISC-V regs

The register definition along with read/write functions for registers
are lowered to Coq. The FIRRTL annotation does not work as expected.

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