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, 1313 insertions, 0 deletions

diff --git a/build/riscv.glob b/build/riscv.glob
new file mode 100644
index 0000000..7206a6e
--- /dev/null
+++ b/build/riscv.glob
@@ -0,0 +1,1313 @@
+DIGEST c6db294320f7a6b05e7783002664d787
+Friscv
+R49:57 Sail.Base <> <> lib
+R75:83 Sail.Real <> <> lib
+R101:111 riscv_types <> <> lib
+def 199:205 <> is_none
+binder 208:208 <> a:1
+R225:230 Coq.Init.Datatypes <> option ind
+R232:232 riscv <> a:1 var
+binder 219:221 <> opt:2
+R237:240 Coq.Init.Datatypes <> bool ind
+R254:256 riscv <> opt:2 var
+R265:268 Coq.Init.Datatypes <> Some constr
+R275:279 Coq.Init.Datatypes <> false constr
+R283:286 Coq.Init.Datatypes <> None constr
+R291:294 Coq.Init.Datatypes <> true constr
+def 313:319 <> is_some
+binder 322:322 <> a:4
+R339:344 Coq.Init.Datatypes <> option ind
+R346:346 riscv <> a:4 var
+binder 333:335 <> opt:5
+R351:354 Coq.Init.Datatypes <> bool ind
+R368:370 riscv <> opt:5 var
+R379:382 Coq.Init.Datatypes <> Some constr
+R389:392 Coq.Init.Datatypes <> true constr
+R396:399 Coq.Init.Datatypes <> None constr
+R404:408 Coq.Init.Datatypes <> false constr
+def 427:433 <> eq_unit
+R440:443 Coq.Init.Datatypes <> unit ind
+R451:454 Coq.Init.Datatypes <> unit ind
+R459:459 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R465:467 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R472:474 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R492:492 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R468:471 Coq.Init.Datatypes <> bool ind
+binder 460:464 <> _bool:7
+R475:483 Sail.Values <> ArithFact class
+R486:490 riscv <> _bool:7 var
+R497:504 Sail.Values <> build_ex def
+R507:510 Coq.Init.Datatypes <> true constr
+def 526:532 <> neq_int
+R539:539 Coq.Numbers.BinNums <> Z ind
+binder 535:535 <> x:8
+R547:547 Coq.Numbers.BinNums <> Z ind
+binder 543:543 <> y:9
+R552:552 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R558:560 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R565:567 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R610:610 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R561:564 Coq.Init.Datatypes <> bool ind
+binder 553:557 <> _bool:10
+R568:576 Sail.Values <> ArithFact class
+R579:586 Coq.Bool.Bool <> eqb def
+R589:592 Coq.Init.Datatypes <> negb def
+R596:599 Coq.ZArith.BinInt <> ::Z_scope:x_'=?'_x not
+R595:595 riscv <> x:8 var
+R600:600 riscv <> y:9 var
+R604:608 riscv <> _bool:10 var
+R618:625 Sail.Values <> build_ex def
+R628:631 Coq.Init.Datatypes <> negb def
+R634:638 Coq.ZArith.BinInt Z eqb def
+R640:640 riscv <> x:8 var
+R642:642 riscv <> y:9 var
+def 659:666 <> neq_bool
+R673:676 Coq.Init.Datatypes <> bool ind
+binder 669:669 <> x:11
+R684:687 Coq.Init.Datatypes <> bool ind
+binder 680:680 <> y:12
+R692:695 Coq.Init.Datatypes <> bool ind
+R700:703 Coq.Init.Datatypes <> negb def
+R706:713 Coq.Bool.Bool <> eqb def
+R715:715 riscv <> x:11 var
+R717:717 riscv <> y:12 var
+def 733:736 <> __id
+R743:743 Coq.Numbers.BinNums <> Z ind
+binder 739:739 <> x:13
+R748:748 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R756:758 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R760:762 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R787:787 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
+R759:759 Coq.Numbers.BinNums <> Z ind
+binder 749:755 <> _retval:14
+R763:771 Sail.Values <> ArithFact class
+R781:784 Coq.ZArith.BinInt <> ::Z_scope:x_'=?'_x not
+R774:780 riscv <> _retval:14 var
+R785:785 riscv <> x:13 var
+R792:799 Sail.Values <> build_ex def
+R802:802 riscv <> x:13 var
+def 818:825 <> fdiv_int
+R832:832 Coq.Numbers.BinNums <> Z ind
+binder 828:828 <> n:15
+R840:840 Coq.Numbers.BinNums <> Z ind
+binder 836:836 <> m:16
+R845:845 Coq.Numbers.BinNums <> Z ind
+R856:870 Coq.Bool.Sumbool <> sumbool_of_bool def
+R873:876 Coq.Init.Datatypes <> andb def
+R891:895 Coq.ZArith.BinInt Z gtb def
+R897:897 riscv <> m:16 var
+R879:883 Coq.ZArith.BinInt Z ltb def
+R885:885 riscv <> n:15 var
+R950:964 Coq.Bool.Sumbool <> sumbool_of_bool def
+R967:970 Coq.Init.Datatypes <> andb def
+R985:989 Coq.ZArith.BinInt Z ltb def
+R991:991 riscv <> m:16 var
+R973:977 Coq.ZArith.BinInt Z gtb def
+R979:979 riscv <> n:15 var
+R1041:1046 Coq.ZArith.BinInt Z quot def
+R1048:1048 riscv <> n:15 var
+R1050:1050 riscv <> m:16 var
+R1002:1006 Coq.ZArith.BinInt Z sub def
+R1009:1014 Coq.ZArith.BinInt Z quot def
+R1017:1021 Coq.ZArith.BinInt Z sub def
+R1023:1023 riscv <> n:15 var
+R1028:1028 riscv <> m:16 var
+R908:912 Coq.ZArith.BinInt Z sub def
+R915:920 Coq.ZArith.BinInt Z quot def
+R923:927 Coq.ZArith.BinInt Z add def
+R929:929 riscv <> n:15 var
+R934:934 riscv <> m:16 var
+def 1065:1072 <> fmod_int
+R1079:1079 Coq.Numbers.BinNums <> Z ind
+binder 1075:1075 <> n:17
+R1087:1087 Coq.Numbers.BinNums <> Z ind
+binder 1083:1083 <> m:18
+R1092:1092 Coq.Numbers.BinNums <> Z ind
+R1097:1101 Coq.ZArith.BinInt Z sub def
+R1103:1103 riscv <> n:17 var
+R1106:1110 Coq.ZArith.BinInt Z mul def
+R1112:1112 riscv <> m:18 var
+R1115:1122 riscv <> fdiv_int def
+R1124:1124 riscv <> n:17 var
+R1126:1126 riscv <> m:18 var
+def 1143:1157 <> concat_str_bits
+R1164:1164 Coq.Numbers.BinNums <> Z ind
+binder 1160:1160 <> n:19
+R1174:1179 Coq.Strings.String <> string ind
+binder 1168:1170 <> str:20
+R1187:1191 Sail.Values <> mword def
+R1193:1193 riscv <> n:19 var
+binder 1183:1183 <> x:21
+R1198:1203 Coq.Strings.String <> string ind
+R1211:1223 Coq.Strings.String <> append def
+R1225:1227 riscv <> str:20 var
+R1230:1243 Sail.Operators_mwords <> string_of_bits def
+R1245:1245 riscv <> x:21 var
+def 1261:1274 <> concat_str_dec
+R1283:1288 Coq.Strings.String <> string ind
+binder 1277:1279 <> str:22
+R1296:1296 Coq.Numbers.BinNums <> Z ind
+binder 1292:1292 <> x:23
+R1301:1306 Coq.Strings.String <> string ind
+R1311:1323 Coq.Strings.String <> append def
+R1325:1327 riscv <> str:22 var
+R1330:1336 Sail.String <> dec_str def
+R1338:1338 riscv <> x:23 var
+def 1356:1364 <> sail_mask
+R1372:1372 Coq.Numbers.BinNums <> Z ind
+binder 1367:1368 <> v0:24
+R1382:1382 Coq.Numbers.BinNums <> Z ind
+binder 1376:1378 <> len:25
+R1390:1394 Sail.Values <> mword def
+R1396:1397 riscv <> v0:24 var
+binder 1386:1386 <> v:26
+R1402:1410 Sail.Values <> ArithFact class
+R1413:1413 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R1423:1428 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R1437:1437 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R1417:1421 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R1414:1416 riscv <> len:25 var
+R1431:1435 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R1429:1430 riscv <> v0:24 var
+binder 1402:1438 <> H:27
+R1443:1447 Sail.Values <> mword def
+R1449:1451 riscv <> len:25 var
+R1462:1476 Coq.Bool.Sumbool <> sumbool_of_bool def
+R1479:1483 Coq.ZArith.BinInt Z leb def
+R1485:1487 riscv <> len:25 var
+R1490:1501 Sail.Values <> length_mword def
+R1503:1503 riscv <> v:26 var
+R1539:1549 Sail.Operators_mwords <> zero_extend def
+R1553:1555 riscv <> len:25 var
+R1551:1551 riscv <> v:26 var
+R1512:1526 Sail.Operators_mwords <> vector_truncate def
+R1530:1532 riscv <> len:25 var
+R1528:1528 riscv <> v:26 var
+def 1570:1578 <> sail_ones
+R1585:1585 Coq.Numbers.BinNums <> Z ind
+binder 1581:1581 <> n:28
+R1590:1598 Sail.Values <> ArithFact class
+R1602:1606 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R1601:1601 riscv <> n:28 var
+binder 1590:1608 <> H:29
+R1613:1617 Sail.Values <> mword def
+R1619:1619 riscv <> n:28 var
+R1624:1630 Sail.Operators_mwords <> not_vec def
+R1633:1637 Sail.Operators_mwords <> zeros def
+R1639:1639 riscv <> n:28 var
+def 1655:1664 <> slice_mask
+R1671:1671 Coq.Numbers.BinNums <> Z ind
+binder 1667:1667 <> n:30
+R1679:1679 Coq.Numbers.BinNums <> Z ind
+binder 1675:1675 <> i:31
+R1687:1687 Coq.Numbers.BinNums <> Z ind
+binder 1683:1683 <> l:32
+R1692:1700 Sail.Values <> ArithFact class
+R1704:1708 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R1703:1703 riscv <> n:30 var
+binder 1692:1710 <> H:33
+R1715:1719 Sail.Values <> mword def
+R1721:1721 riscv <> n:30 var
+R1732:1746 Coq.Bool.Sumbool <> sumbool_of_bool def
+R1749:1753 Coq.ZArith.BinInt Z geb def
+R1755:1755 riscv <> l:32 var
+R1757:1757 riscv <> n:30 var
+R1821:1829 riscv <> sail_mask def
+R1843:1846 riscv_types <> bits def
+R1834:1835 bbv.HexNotationWord <> :::'''b'_x not
+R1831:1831 riscv <> n:30 var
+R1811:1814 riscv_types <> bits def
+R1816:1816 riscv <> n:30 var
+binder 1805:1807 <> one:34
+R1859:1864 Sail.Operators_mwords <> shiftl def
+R1895:1895 riscv <> i:31 var
+R1867:1873 Sail.Operators_mwords <> sub_vec def
+R1890:1892 riscv <> one:34 var
+R1876:1881 Sail.Operators_mwords <> shiftl def
+R1887:1887 riscv <> l:32 var
+R1883:1885 riscv <> one:34 var
+R1765:1770 Sail.Operators_mwords <> shiftl def
+R1786:1786 riscv <> i:31 var
+R1773:1781 riscv <> sail_ones def
+R1783:1783 riscv <> n:30 var
+def 1910:1913 <> EXTS
+R1920:1920 Coq.Numbers.BinNums <> Z ind
+binder 1916:1916 <> n:35
+R1928:1928 Coq.Numbers.BinNums <> Z ind
+binder 1924:1924 <> m:36
+R1936:1940 Sail.Values <> mword def
+R1942:1942 riscv <> n:35 var
+binder 1932:1932 <> v:37
+R1947:1955 Sail.Values <> ArithFact class
+R1959:1963 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R1958:1958 riscv <> m:36 var
+R1964:1964 riscv <> n:35 var
+binder 1947:1965 <> H:38
+R1970:1974 Sail.Values <> mword def
+R1976:1976 riscv <> m:36 var
+R1981:1991 Sail.Operators_mwords <> sign_extend def
+R1995:1995 riscv <> m:36 var
+R1993:1993 riscv <> v:37 var
+def 2010:2013 <> EXTZ
+R2020:2020 Coq.Numbers.BinNums <> Z ind
+binder 2016:2016 <> n:39
+R2028:2028 Coq.Numbers.BinNums <> Z ind
+binder 2024:2024 <> m:40
+R2036:2040 Sail.Values <> mword def
+R2042:2042 riscv <> n:39 var
+binder 2032:2032 <> v:41
+R2047:2055 Sail.Values <> ArithFact class
+R2059:2063 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
+R2058:2058 riscv <> m:40 var
+R2064:2064 riscv <> n:39 var
+binder 2047:2065 <> H:42
+R2070:2074 Sail.Values <> mword def
+R2076:2076 riscv <> m:40 var
+R2081:2091 Sail.Operators_mwords <> zero_extend def
+R2095:2095 riscv <> m:40 var
+R2093:2093 riscv <> v:41 var
+def 2110:2117 <> zero_reg
+R2121:2127 riscv_types <> regtype def
+R2132:2135 riscv <> EXTZ def
+R2150:2154 Sail.Values <> mword def
+R2141:2142 bbv.HexNotationWord <> :::'Ox'_x not
+R2172:2179 riscv <> zero_reg def
+def 2200:2214 <> regval_from_reg
+R2221:2225 Sail.Values <> mword def
+binder 2217:2217 <> r:43
+R2233:2237 Sail.Values <> mword def
+R2245:2245 riscv <> r:43 var
+def 2260:2274 <> regval_into_reg
+R2281:2285 Sail.Values <> mword def
+binder 2277:2277 <> v:44
+R2293:2297 Sail.Values <> mword def
+R2305:2305 riscv <> v:44 var
+def 2320:2321 <> rX
+R2328:2328 Coq.Numbers.BinNums <> Z ind
+binder 2324:2324 <> r:45
+R2333:2341 Sail.Values <> ArithFact class
+R2344:2344 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R2352:2357 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R2365:2365 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R2346:2350 Coq.ZArith.BinInt <> ::Z_scope:x_'<=?'_x not
+R2351:2351 riscv <> r:45 var
+R2359:2362 Coq.ZArith.BinInt <> ::Z_scope:x_'<?'_x not
+R2358:2358 riscv <> r:45 var
+binder 2333:2366 <> H:46
+R2371:2371 riscv_types <> M def
+R2374:2378 Sail.Values <> mword def
+R2403:2403 riscv <> r:45 var
+binder 2394:2398 <> l__32:47
+R2411:2411 Sail.Prompt_monad <> :::x_'>>='_x not
+R5981:5986 Sail.Prompt_monad <> :::x_'>>='_x not
+R2415:2429 Coq.Bool.Sumbool <> sumbool_of_bool def
+R2432:2436 Coq.ZArith.BinInt Z eqb def
+R2438:2442 riscv <> l__32:47 var
+R2481:2495 Coq.Bool.Sumbool <> sumbool_of_bool def
+R2498:2502 Coq.ZArith.BinInt Z eqb def
+R2504:2508 riscv <> l__32:47 var
+R2582:2596 Coq.Bool.Sumbool <> sumbool_of_bool def
+R2599:2603 Coq.ZArith.BinInt Z eqb def
+R2605:2609 riscv <> l__32:47 var
+R2683:2697 Coq.Bool.Sumbool <> sumbool_of_bool def
+R2700:2704 Coq.ZArith.BinInt Z eqb def
+R2706:2710 riscv <> l__32:47 var
+R2784:2798 Coq.Bool.Sumbool <> sumbool_of_bool def
+R2801:2805 Coq.ZArith.BinInt Z eqb def
+R2807:2811 riscv <> l__32:47 var
+R2885:2899 Coq.Bool.Sumbool <> sumbool_of_bool def
+R2902:2906 Coq.ZArith.BinInt Z eqb def
+R2908:2912 riscv <> l__32:47 var
+R2986:3000 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3003:3007 Coq.ZArith.BinInt Z eqb def
+R3009:3013 riscv <> l__32:47 var
+R3087:3101 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3104:3108 Coq.ZArith.BinInt Z eqb def
+R3110:3114 riscv <> l__32:47 var
+R3188:3202 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3205:3209 Coq.ZArith.BinInt Z eqb def
+R3211:3215 riscv <> l__32:47 var
+R3289:3303 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3306:3310 Coq.ZArith.BinInt Z eqb def
+R3312:3316 riscv <> l__32:47 var
+R3390:3404 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3407:3411 Coq.ZArith.BinInt Z eqb def
+R3413:3417 riscv <> l__32:47 var
+R3505:3519 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3522:3526 Coq.ZArith.BinInt Z eqb def
+R3528:3532 riscv <> l__32:47 var
+R3620:3634 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3637:3641 Coq.ZArith.BinInt Z eqb def
+R3643:3647 riscv <> l__32:47 var
+R3735:3749 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3752:3756 Coq.ZArith.BinInt Z eqb def
+R3758:3762 riscv <> l__32:47 var
+R3850:3864 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3867:3871 Coq.ZArith.BinInt Z eqb def
+R3873:3877 riscv <> l__32:47 var
+R3965:3979 Coq.Bool.Sumbool <> sumbool_of_bool def
+R3982:3986 Coq.ZArith.BinInt Z eqb def
+R3988:3992 riscv <> l__32:47 var
+R4080:4094 Coq.Bool.Sumbool <> sumbool_of_bool def
+R4097:4101 Coq.ZArith.BinInt Z eqb def
+R4103:4107 riscv <> l__32:47 var
+R4195:4209 Coq.Bool.Sumbool <> sumbool_of_bool def
+R4212:4216 Coq.ZArith.BinInt Z eqb def
+R4218:4222 riscv <> l__32:47 var
+R4310:4324 Coq.Bool.Sumbool <> sumbool_of_bool def
+R4327:4331 Coq.ZArith.BinInt Z eqb def
+R4333:4337 riscv <> l__32:47 var
+R4425:4439 Coq.Bool.Sumbool <> sumbool_of_bool def
+R4442:4446 Coq.ZArith.BinInt Z eqb def
+R4448:4452 riscv <> l__32:47 var
+R4540:4554 Coq.Bool.Sumbool <> sumbool_of_bool def
+R4557:4561 Coq.ZArith.BinInt Z eqb def
+R4563:4567 riscv <> l__32:47 var
+R4655:4669 Coq.Bool.Sumbool <> sumbool_of_bool def
+R4672:4676 Coq.ZArith.BinInt Z eqb def
+R4678:4682 riscv <> l__32:47 var
+R4770:4784 Coq.Bool.Sumbool <> sumbool_of_bool def
+R4787:4791 Coq.ZArith.BinInt Z eqb def
+R4793:4797 riscv <> l__32:47 var
+R4885:4899 Coq.Bool.Sumbool <> sumbool_of_bool def
+R4902:4906 Coq.ZArith.BinInt Z eqb def
+R4908:4912 riscv <> l__32:47 var
+R5000:5014 Coq.Bool.Sumbool <> sumbool_of_bool def
+R5017:5021 Coq.ZArith.BinInt Z eqb def
+R5023:5027 riscv <> l__32:47 var
+R5115:5129 Coq.Bool.Sumbool <> sumbool_of_bool def
+R5132:5136 Coq.ZArith.BinInt Z eqb def
+R5138:5142 riscv <> l__32:47 var
+R5230:5244 Coq.Bool.Sumbool <> sumbool_of_bool def
+R5247:5251 Coq.ZArith.BinInt Z eqb def
+R5253:5257 riscv <> l__32:47 var
+R5345:5359 Coq.Bool.Sumbool <> sumbool_of_bool def
+R5362:5366 Coq.ZArith.BinInt Z eqb def
+R5368:5372 riscv <> l__32:47 var
+R5460:5474 Coq.Bool.Sumbool <> sumbool_of_bool def
+R5477:5481 Coq.ZArith.BinInt Z eqb def
+R5483:5487 riscv <> l__32:47 var
+R5575:5589 Coq.Bool.Sumbool <> sumbool_of_bool def
+R5592:5596 Coq.ZArith.BinInt Z eqb def
+R5598:5602 riscv <> l__32:47 var
+R5690:5704 Coq.Bool.Sumbool <> sumbool_of_bool def
+R5707:5711 Coq.ZArith.BinInt Z eqb def
+R5713:5717 riscv <> l__32:47 var
+R5805:5819 Coq.Bool.Sumbool <> sumbool_of_bool def
+R5822:5826 Coq.ZArith.BinInt Z eqb def
+R5828:5832 riscv <> l__32:47 var
+R5960:5964 Sail.Prompt_monad <> :::x_'>>='_x not
+R5917:5927 Sail.Prompt_monad <> assert_exp' def
+R5929:5933 Coq.Init.Datatypes <> false constr
+R5974:5977 Sail.Prompt_monad <> exit def
+R5979:5980 Coq.Init.Datatypes <> tt constr
+R5895:5895 riscv_types <> M def
+R5898:5902 Sail.Values <> mword def
+R5872:5872 riscv_types <> M def
+R5875:5879 Sail.Values <> mword def
+R5851:5858 Sail.Prompt_monad <> read_reg def
+R5860:5866 riscv_types <> x31_ref def
+R5780:5780 riscv_types <> M def
+R5783:5787 Sail.Values <> mword def
+R5757:5757 riscv_types <> M def
+R5760:5764 Sail.Values <> mword def
+R5736:5743 Sail.Prompt_monad <> read_reg def
+R5745:5751 riscv_types <> x30_ref def
+R5665:5665 riscv_types <> M def
+R5668:5672 Sail.Values <> mword def
+R5642:5642 riscv_types <> M def
+R5645:5649 Sail.Values <> mword def
+R5621:5628 Sail.Prompt_monad <> read_reg def
+R5630:5636 riscv_types <> x29_ref def
+R5550:5550 riscv_types <> M def
+R5553:5557 Sail.Values <> mword def
+R5527:5527 riscv_types <> M def
+R5530:5534 Sail.Values <> mword def
+R5506:5513 Sail.Prompt_monad <> read_reg def
+R5515:5521 riscv_types <> x28_ref def
+R5435:5435 riscv_types <> M def
+R5438:5442 Sail.Values <> mword def
+R5412:5412 riscv_types <> M def
+R5415:5419 Sail.Values <> mword def
+R5391:5398 Sail.Prompt_monad <> read_reg def
+R5400:5406 riscv_types <> x27_ref def
+R5320:5320 riscv_types <> M def
+R5323:5327 Sail.Values <> mword def
+R5297:5297 riscv_types <> M def
+R5300:5304 Sail.Values <> mword def
+R5276:5283 Sail.Prompt_monad <> read_reg def
+R5285:5291 riscv_types <> x26_ref def
+R5205:5205 riscv_types <> M def
+R5208:5212 Sail.Values <> mword def
+R5182:5182 riscv_types <> M def
+R5185:5189 Sail.Values <> mword def
+R5161:5168 Sail.Prompt_monad <> read_reg def
+R5170:5176 riscv_types <> x25_ref def
+R5090:5090 riscv_types <> M def
+R5093:5097 Sail.Values <> mword def
+R5067:5067 riscv_types <> M def
+R5070:5074 Sail.Values <> mword def
+R5046:5053 Sail.Prompt_monad <> read_reg def
+R5055:5061 riscv_types <> x24_ref def
+R4975:4975 riscv_types <> M def
+R4978:4982 Sail.Values <> mword def
+R4952:4952 riscv_types <> M def
+R4955:4959 Sail.Values <> mword def
+R4931:4938 Sail.Prompt_monad <> read_reg def
+R4940:4946 riscv_types <> x23_ref def
+R4860:4860 riscv_types <> M def
+R4863:4867 Sail.Values <> mword def
+R4837:4837 riscv_types <> M def
+R4840:4844 Sail.Values <> mword def
+R4816:4823 Sail.Prompt_monad <> read_reg def
+R4825:4831 riscv_types <> x22_ref def
+R4745:4745 riscv_types <> M def
+R4748:4752 Sail.Values <> mword def
+R4722:4722 riscv_types <> M def
+R4725:4729 Sail.Values <> mword def
+R4701:4708 Sail.Prompt_monad <> read_reg def
+R4710:4716 riscv_types <> x21_ref def
+R4630:4630 riscv_types <> M def
+R4633:4637 Sail.Values <> mword def
+R4607:4607 riscv_types <> M def
+R4610:4614 Sail.Values <> mword def
+R4586:4593 Sail.Prompt_monad <> read_reg def
+R4595:4601 riscv_types <> x20_ref def
+R4515:4515 riscv_types <> M def
+R4518:4522 Sail.Values <> mword def
+R4492:4492 riscv_types <> M def
+R4495:4499 Sail.Values <> mword def
+R4471:4478 Sail.Prompt_monad <> read_reg def
+R4480:4486 riscv_types <> x19_ref def
+R4400:4400 riscv_types <> M def
+R4403:4407 Sail.Values <> mword def
+R4377:4377 riscv_types <> M def
+R4380:4384 Sail.Values <> mword def
+R4356:4363 Sail.Prompt_monad <> read_reg def
+R4365:4371 riscv_types <> x18_ref def
+R4285:4285 riscv_types <> M def
+R4288:4292 Sail.Values <> mword def
+R4262:4262 riscv_types <> M def
+R4265:4269 Sail.Values <> mword def
+R4241:4248 Sail.Prompt_monad <> read_reg def
+R4250:4256 riscv_types <> x17_ref def
+R4170:4170 riscv_types <> M def
+R4173:4177 Sail.Values <> mword def
+R4147:4147 riscv_types <> M def
+R4150:4154 Sail.Values <> mword def
+R4126:4133 Sail.Prompt_monad <> read_reg def
+R4135:4141 riscv_types <> x16_ref def
+R4055:4055 riscv_types <> M def
+R4058:4062 Sail.Values <> mword def
+R4032:4032 riscv_types <> M def
+R4035:4039 Sail.Values <> mword def
+R4011:4018 Sail.Prompt_monad <> read_reg def
+R4020:4026 riscv_types <> x15_ref def
+R3940:3940 riscv_types <> M def
+R3943:3947 Sail.Values <> mword def
+R3917:3917 riscv_types <> M def
+R3920:3924 Sail.Values <> mword def
+R3896:3903 Sail.Prompt_monad <> read_reg def
+R3905:3911 riscv_types <> x14_ref def
+R3825:3825 riscv_types <> M def
+R3828:3832 Sail.Values <> mword def
+R3802:3802 riscv_types <> M def
+R3805:3809 Sail.Values <> mword def
+R3781:3788 Sail.Prompt_monad <> read_reg def
+R3790:3796 riscv_types <> x13_ref def
+R3710:3710 riscv_types <> M def
+R3713:3717 Sail.Values <> mword def
+R3687:3687 riscv_types <> M def
+R3690:3694 Sail.Values <> mword def
+R3666:3673 Sail.Prompt_monad <> read_reg def
+R3675:3681 riscv_types <> x12_ref def
+R3595:3595 riscv_types <> M def
+R3598:3602 Sail.Values <> mword def
+R3572:3572 riscv_types <> M def
+R3575:3579 Sail.Values <> mword def
+R3551:3558 Sail.Prompt_monad <> read_reg def
+R3560:3566 riscv_types <> x11_ref def
+R3480:3480 riscv_types <> M def
+R3483:3487 Sail.Values <> mword def
+R3457:3457 riscv_types <> M def
+R3460:3464 Sail.Values <> mword def
+R3436:3443 Sail.Prompt_monad <> read_reg def
+R3445:3451 riscv_types <> x10_ref def
+R3365:3365 riscv_types <> M def
+R3368:3372 Sail.Values <> mword def
+R3348:3348 riscv_types <> M def
+R3351:3355 Sail.Values <> mword def
+R3328:3335 Sail.Prompt_monad <> read_reg def
+R3337:3342 riscv_types <> x9_ref def
+R3264:3264 riscv_types <> M def
+R3267:3271 Sail.Values <> mword def
+R3247:3247 riscv_types <> M def
+R3250:3254 Sail.Values <> mword def
+R3227:3234 Sail.Prompt_monad <> read_reg def
+R3236:3241 riscv_types <> x8_ref def
+R3163:3163 riscv_types <> M def
+R3166:3170 Sail.Values <> mword def
+R3146:3146 riscv_types <> M def
+R3149:3153 Sail.Values <> mword def
+R3126:3133 Sail.Prompt_monad <> read_reg def
+R3135:3140 riscv_types <> x7_ref def
+R3062:3062 riscv_types <> M def
+R3065:3069 Sail.Values <> mword def
+R3045:3045 riscv_types <> M def
+R3048:3052 Sail.Values <> mword def
+R3025:3032 Sail.Prompt_monad <> read_reg def
+R3034:3039 riscv_types <> x6_ref def
+R2961:2961 riscv_types <> M def
+R2964:2968 Sail.Values <> mword def
+R2944:2944 riscv_types <> M def
+R2947:2951 Sail.Values <> mword def
+R2924:2931 Sail.Prompt_monad <> read_reg def
+R2933:2938 riscv_types <> x5_ref def
+R2860:2860 riscv_types <> M def
+R2863:2867 Sail.Values <> mword def
+R2843:2843 riscv_types <> M def
+R2846:2850 Sail.Values <> mword def
+R2823:2830 Sail.Prompt_monad <> read_reg def
+R2832:2837 riscv_types <> x4_ref def
+R2759:2759 riscv_types <> M def
+R2762:2766 Sail.Values <> mword def
+R2742:2742 riscv_types <> M def
+R2745:2749 Sail.Values <> mword def
+R2722:2729 Sail.Prompt_monad <> read_reg def
+R2731:2736 riscv_types <> x3_ref def
+R2658:2658 riscv_types <> M def
+R2661:2665 Sail.Values <> mword def
+R2641:2641 riscv_types <> M def
+R2644:2648 Sail.Values <> mword def
+R2621:2628 Sail.Prompt_monad <> read_reg def
+R2630:2635 riscv_types <> x2_ref def
+R2557:2557 riscv_types <> M def
+R2560:2564 Sail.Values <> mword def
+R2540:2540 riscv_types <> M def
+R2543:2547 Sail.Values <> mword def
+R2520:2527 Sail.Prompt_monad <> read_reg def
+R2529:2534 riscv_types <> x1_ref def
+R2452:2458 Sail.Prompt_monad <> returnm def
+R2460:2467 riscv <> zero_reg def
+R5995:6001 riscv_types <> regtype def
+binder 5991:5991 <> v:48
+R6009:6015 Sail.Prompt_monad <> returnm def
+R6018:6032 riscv <> regval_from_reg def
+R6034:6034 riscv <> v:48 var
+def 6050:6051 <> wX
+R6058:6058 Coq.Numbers.BinNums <> Z ind
+binder 6054:6054 <> r:49
+R6069:6073 Sail.Values <> mword def
+binder 6062:6065 <> in_v:50
+R6081:6089 Sail.Values <> ArithFact class
+R6092:6092 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R6100:6105 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R6113:6113 Coq.Init.Datatypes <> ::bool_scope:x_'&&'_x not
+R6094:6098 Coq.ZArith.BinInt <> ::Z_scope:x_'<=?'_x not
+R6099:6099 riscv <> r:49 var
+R6107:6110 Coq.ZArith.BinInt <> ::Z_scope:x_'<?'_x not
+R6106:6106 riscv <> r:49 var
+binder 6081:6114 <> H:51
+R6119:6119 riscv_types <> M def
+R6122:6125 Coq.Init.Datatypes <> unit ind
+R6143:6157 riscv <> regval_into_reg def
+R6159:6162 riscv <> in_v:50 var
+binder 6138:6138 <> v:52
+R6182:6182 riscv <> r:49 var
+binder 6174:6177 <> l__0:53
+R8815:8815 riscv_types <> M def
+R8818:8821 Coq.Init.Datatypes <> unit ind
+R6194:6208 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6211:6215 Coq.ZArith.BinInt Z eqb def
+R6217:6220 riscv <> l__0:53 var
+R6253:6267 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6270:6274 Coq.ZArith.BinInt Z eqb def
+R6276:6279 riscv <> l__0:53 var
+R6332:6346 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6349:6353 Coq.ZArith.BinInt Z eqb def
+R6355:6358 riscv <> l__0:53 var
+R6411:6425 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6428:6432 Coq.ZArith.BinInt Z eqb def
+R6434:6437 riscv <> l__0:53 var
+R6490:6504 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6507:6511 Coq.ZArith.BinInt Z eqb def
+R6513:6516 riscv <> l__0:53 var
+R6569:6583 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6586:6590 Coq.ZArith.BinInt Z eqb def
+R6592:6595 riscv <> l__0:53 var
+R6648:6662 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6665:6669 Coq.ZArith.BinInt Z eqb def
+R6671:6674 riscv <> l__0:53 var
+R6727:6741 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6744:6748 Coq.ZArith.BinInt Z eqb def
+R6750:6753 riscv <> l__0:53 var
+R6806:6820 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6823:6827 Coq.ZArith.BinInt Z eqb def
+R6829:6832 riscv <> l__0:53 var
+R6885:6899 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6902:6906 Coq.ZArith.BinInt Z eqb def
+R6908:6911 riscv <> l__0:53 var
+R6964:6978 Coq.Bool.Sumbool <> sumbool_of_bool def
+R6981:6985 Coq.ZArith.BinInt Z eqb def
+R6987:6990 riscv <> l__0:53 var
+R7045:7059 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7062:7066 Coq.ZArith.BinInt Z eqb def
+R7068:7071 riscv <> l__0:53 var
+R7126:7140 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7143:7147 Coq.ZArith.BinInt Z eqb def
+R7149:7152 riscv <> l__0:53 var
+R7207:7221 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7224:7228 Coq.ZArith.BinInt Z eqb def
+R7230:7233 riscv <> l__0:53 var
+R7288:7302 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7305:7309 Coq.ZArith.BinInt Z eqb def
+R7311:7314 riscv <> l__0:53 var
+R7369:7383 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7386:7390 Coq.ZArith.BinInt Z eqb def
+R7392:7395 riscv <> l__0:53 var
+R7450:7464 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7467:7471 Coq.ZArith.BinInt Z eqb def
+R7473:7476 riscv <> l__0:53 var
+R7531:7545 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7548:7552 Coq.ZArith.BinInt Z eqb def
+R7554:7557 riscv <> l__0:53 var
+R7612:7626 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7629:7633 Coq.ZArith.BinInt Z eqb def
+R7635:7638 riscv <> l__0:53 var
+R7693:7707 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7710:7714 Coq.ZArith.BinInt Z eqb def
+R7716:7719 riscv <> l__0:53 var
+R7774:7788 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7791:7795 Coq.ZArith.BinInt Z eqb def
+R7797:7800 riscv <> l__0:53 var
+R7855:7869 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7872:7876 Coq.ZArith.BinInt Z eqb def
+R7878:7881 riscv <> l__0:53 var
+R7936:7950 Coq.Bool.Sumbool <> sumbool_of_bool def
+R7953:7957 Coq.ZArith.BinInt Z eqb def
+R7959:7962 riscv <> l__0:53 var
+R8017:8031 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8034:8038 Coq.ZArith.BinInt Z eqb def
+R8040:8043 riscv <> l__0:53 var
+R8098:8112 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8115:8119 Coq.ZArith.BinInt Z eqb def
+R8121:8124 riscv <> l__0:53 var
+R8179:8193 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8196:8200 Coq.ZArith.BinInt Z eqb def
+R8202:8205 riscv <> l__0:53 var
+R8260:8274 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8277:8281 Coq.ZArith.BinInt Z eqb def
+R8283:8286 riscv <> l__0:53 var
+R8341:8355 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8358:8362 Coq.ZArith.BinInt Z eqb def
+R8364:8367 riscv <> l__0:53 var
+R8422:8436 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8439:8443 Coq.ZArith.BinInt Z eqb def
+R8445:8448 riscv <> l__0:53 var
+R8503:8517 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8520:8524 Coq.ZArith.BinInt Z eqb def
+R8526:8529 riscv <> l__0:53 var
+R8584:8598 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8601:8605 Coq.ZArith.BinInt Z eqb def
+R8607:8610 riscv <> l__0:53 var
+R8665:8679 Coq.Bool.Sumbool <> sumbool_of_bool def
+R8682:8686 Coq.ZArith.BinInt Z eqb def
+R8688:8691 riscv <> l__0:53 var
+R8786:8790 Sail.Prompt_monad <> :::x_'>>='_x not
+R8743:8753 Sail.Prompt_monad <> assert_exp' def
+R8755:8759 Coq.Init.Datatypes <> false constr
+R8800:8803 Sail.Prompt_monad <> exit def
+R8805:8806 Coq.Init.Datatypes <> tt constr
+R8725:8725 riscv_types <> M def
+R8728:8731 Coq.Init.Datatypes <> unit ind
+R8702:8710 Sail.Prompt_monad <> write_reg def
+R8720:8720 riscv <> v:52 var
+R8712:8718 riscv_types <> x31_ref def
+R8644:8644 riscv_types <> M def
+R8647:8650 Coq.Init.Datatypes <> unit ind
+R8621:8629 Sail.Prompt_monad <> write_reg def
+R8639:8639 riscv <> v:52 var
+R8631:8637 riscv_types <> x30_ref def
+R8563:8563 riscv_types <> M def
+R8566:8569 Coq.Init.Datatypes <> unit ind
+R8540:8548 Sail.Prompt_monad <> write_reg def
+R8558:8558 riscv <> v:52 var
+R8550:8556 riscv_types <> x29_ref def
+R8482:8482 riscv_types <> M def
+R8485:8488 Coq.Init.Datatypes <> unit ind
+R8459:8467 Sail.Prompt_monad <> write_reg def
+R8477:8477 riscv <> v:52 var
+R8469:8475 riscv_types <> x28_ref def
+R8401:8401 riscv_types <> M def
+R8404:8407 Coq.Init.Datatypes <> unit ind
+R8378:8386 Sail.Prompt_monad <> write_reg def
+R8396:8396 riscv <> v:52 var
+R8388:8394 riscv_types <> x27_ref def
+R8320:8320 riscv_types <> M def
+R8323:8326 Coq.Init.Datatypes <> unit ind
+R8297:8305 Sail.Prompt_monad <> write_reg def
+R8315:8315 riscv <> v:52 var
+R8307:8313 riscv_types <> x26_ref def
+R8239:8239 riscv_types <> M def
+R8242:8245 Coq.Init.Datatypes <> unit ind
+R8216:8224 Sail.Prompt_monad <> write_reg def
+R8234:8234 riscv <> v:52 var
+R8226:8232 riscv_types <> x25_ref def
+R8158:8158 riscv_types <> M def
+R8161:8164 Coq.Init.Datatypes <> unit ind
+R8135:8143 Sail.Prompt_monad <> write_reg def
+R8153:8153 riscv <> v:52 var
+R8145:8151 riscv_types <> x24_ref def
+R8077:8077 riscv_types <> M def
+R8080:8083 Coq.Init.Datatypes <> unit ind
+R8054:8062 Sail.Prompt_monad <> write_reg def
+R8072:8072 riscv <> v:52 var
+R8064:8070 riscv_types <> x23_ref def
+R7996:7996 riscv_types <> M def
+R7999:8002 Coq.Init.Datatypes <> unit ind
+R7973:7981 Sail.Prompt_monad <> write_reg def
+R7991:7991 riscv <> v:52 var
+R7983:7989 riscv_types <> x22_ref def
+R7915:7915 riscv_types <> M def
+R7918:7921 Coq.Init.Datatypes <> unit ind
+R7892:7900 Sail.Prompt_monad <> write_reg def
+R7910:7910 riscv <> v:52 var
+R7902:7908 riscv_types <> x21_ref def
+R7834:7834 riscv_types <> M def
+R7837:7840 Coq.Init.Datatypes <> unit ind
+R7811:7819 Sail.Prompt_monad <> write_reg def
+R7829:7829 riscv <> v:52 var
+R7821:7827 riscv_types <> x20_ref def
+R7753:7753 riscv_types <> M def
+R7756:7759 Coq.Init.Datatypes <> unit ind
+R7730:7738 Sail.Prompt_monad <> write_reg def
+R7748:7748 riscv <> v:52 var
+R7740:7746 riscv_types <> x19_ref def
+R7672:7672 riscv_types <> M def
+R7675:7678 Coq.Init.Datatypes <> unit ind
+R7649:7657 Sail.Prompt_monad <> write_reg def
+R7667:7667 riscv <> v:52 var
+R7659:7665 riscv_types <> x18_ref def
+R7591:7591 riscv_types <> M def
+R7594:7597 Coq.Init.Datatypes <> unit ind
+R7568:7576 Sail.Prompt_monad <> write_reg def
+R7586:7586 riscv <> v:52 var
+R7578:7584 riscv_types <> x17_ref def
+R7510:7510 riscv_types <> M def
+R7513:7516 Coq.Init.Datatypes <> unit ind
+R7487:7495 Sail.Prompt_monad <> write_reg def
+R7505:7505 riscv <> v:52 var
+R7497:7503 riscv_types <> x16_ref def
+R7429:7429 riscv_types <> M def
+R7432:7435 Coq.Init.Datatypes <> unit ind
+R7406:7414 Sail.Prompt_monad <> write_reg def
+R7424:7424 riscv <> v:52 var
+R7416:7422 riscv_types <> x15_ref def
+R7348:7348 riscv_types <> M def
+R7351:7354 Coq.Init.Datatypes <> unit ind
+R7325:7333 Sail.Prompt_monad <> write_reg def
+R7343:7343 riscv <> v:52 var
+R7335:7341 riscv_types <> x14_ref def
+R7267:7267 riscv_types <> M def
+R7270:7273 Coq.Init.Datatypes <> unit ind
+R7244:7252 Sail.Prompt_monad <> write_reg def
+R7262:7262 riscv <> v:52 var
+R7254:7260 riscv_types <> x13_ref def
+R7186:7186 riscv_types <> M def
+R7189:7192 Coq.Init.Datatypes <> unit ind
+R7163:7171 Sail.Prompt_monad <> write_reg def
+R7181:7181 riscv <> v:52 var
+R7173:7179 riscv_types <> x12_ref def
+R7105:7105 riscv_types <> M def
+R7108:7111 Coq.Init.Datatypes <> unit ind
+R7082:7090 Sail.Prompt_monad <> write_reg def
+R7100:7100 riscv <> v:52 var
+R7092:7098 riscv_types <> x11_ref def
+R7024:7024 riscv_types <> M def
+R7027:7030 Coq.Init.Datatypes <> unit ind
+R7001:7009 Sail.Prompt_monad <> write_reg def
+R7019:7019 riscv <> v:52 var
+R7011:7017 riscv_types <> x10_ref def
+R6943:6943 riscv_types <> M def
+R6946:6949 Coq.Init.Datatypes <> unit ind
+R6921:6929 Sail.Prompt_monad <> write_reg def
+R6938:6938 riscv <> v:52 var
+R6931:6936 riscv_types <> x9_ref def
+R6864:6864 riscv_types <> M def
+R6867:6870 Coq.Init.Datatypes <> unit ind
+R6842:6850 Sail.Prompt_monad <> write_reg def
+R6859:6859 riscv <> v:52 var
+R6852:6857 riscv_types <> x8_ref def
+R6785:6785 riscv_types <> M def
+R6788:6791 Coq.Init.Datatypes <> unit ind
+R6763:6771 Sail.Prompt_monad <> write_reg def
+R6780:6780 riscv <> v:52 var
+R6773:6778 riscv_types <> x7_ref def
+R6706:6706 riscv_types <> M def
+R6709:6712 Coq.Init.Datatypes <> unit ind
+R6684:6692 Sail.Prompt_monad <> write_reg def
+R6701:6701 riscv <> v:52 var
+R6694:6699 riscv_types <> x6_ref def
+R6627:6627 riscv_types <> M def
+R6630:6633 Coq.Init.Datatypes <> unit ind
+R6605:6613 Sail.Prompt_monad <> write_reg def
+R6622:6622 riscv <> v:52 var
+R6615:6620 riscv_types <> x5_ref def
+R6548:6548 riscv_types <> M def
+R6551:6554 Coq.Init.Datatypes <> unit ind
+R6526:6534 Sail.Prompt_monad <> write_reg def
+R6543:6543 riscv <> v:52 var
+R6536:6541 riscv_types <> x4_ref def
+R6469:6469 riscv_types <> M def
+R6472:6475 Coq.Init.Datatypes <> unit ind
+R6447:6455 Sail.Prompt_monad <> write_reg def
+R6464:6464 riscv <> v:52 var
+R6457:6462 riscv_types <> x3_ref def
+R6390:6390 riscv_types <> M def
+R6393:6396 Coq.Init.Datatypes <> unit ind
+R6368:6376 Sail.Prompt_monad <> write_reg def
+R6385:6385 riscv <> v:52 var
+R6378:6383 riscv_types <> x2_ref def
+R6311:6311 riscv_types <> M def
+R6314:6317 Coq.Init.Datatypes <> unit ind
+R6289:6297 Sail.Prompt_monad <> write_reg def
+R6306:6306 riscv <> v:52 var
+R6299:6304 riscv_types <> x1_ref def
+R6230:6236 Sail.Prompt_monad <> returnm def
+R6238:6239 Coq.Init.Datatypes <> tt constr
+def 8837:8843 <> rX_bits
+R8850:8854 Sail.Values <> mword def
+binder 8846:8846 <> i:54
+R8861:8861 riscv_types <> M def
+R8864:8868 Sail.Values <> mword def
+R8903:8903 riscv_types <> M def
+R8906:8910 Sail.Values <> mword def
+R8878:8879 riscv <> rX def
+R8882:8887 Coq.Init.Specif <> projT1 def
+R8890:8893 Sail.Operators_mwords <> uint def
+R8895:8895 riscv <> i:54 var
+def 8929:8935 <> wX_bits
+R8942:8946 Sail.Values <> mword def
+binder 8938:8938 <> i:55
+R8959:8963 Sail.Values <> mword def
+binder 8952:8955 <> data:56
+R8971:8971 riscv_types <> M def
+R8974:8977 Coq.Init.Datatypes <> unit ind
+R9017:9017 riscv_types <> M def
+R9020:9023 Coq.Init.Datatypes <> unit ind
+R8987:8988 riscv <> wX def
+R9008:9011 riscv <> data:56 var
+R8991:8996 Coq.Init.Specif <> projT1 def
+R8999:9002 Sail.Operators_mwords <> uint def
+R9004:9004 riscv <> i:55 var
+def 9039:9050 <> reg_name_abi
+R9057:9061 Sail.Values <> mword def
+binder 9053:9053 <> r:57
+R9068:9068 riscv_types <> M def
+R9071:9076 Coq.Strings.String <> string ind
+R9097:9097 riscv <> r:57 var
+binder 9089:9092 <> b__0:58
+R11305:11305 riscv_types <> M def
+R11308:11313 Coq.Strings.String <> string ind
+R9109:9114 Sail.Operators_mwords <> eq_vec def
+R9135:9139 Sail.Values <> mword def
+R9122:9123 bbv.HexNotationWord <> :::'''b'_x not
+R9116:9119 riscv <> b__0:58 var
+R9176:9181 Sail.Operators_mwords <> eq_vec def
+R9202:9206 Sail.Values <> mword def
+R9189:9190 bbv.HexNotationWord <> :::'''b'_x not
+R9183:9186 riscv <> b__0:58 var
+R9241:9246 Sail.Operators_mwords <> eq_vec def
+R9267:9271 Sail.Values <> mword def
+R9254:9255 bbv.HexNotationWord <> :::'''b'_x not
+R9248:9251 riscv <> b__0:58 var
+R9306:9311 Sail.Operators_mwords <> eq_vec def
+R9332:9336 Sail.Values <> mword def
+R9319:9320 bbv.HexNotationWord <> :::'''b'_x not
+R9313:9316 riscv <> b__0:58 var
+R9371:9376 Sail.Operators_mwords <> eq_vec def
+R9397:9401 Sail.Values <> mword def
+R9384:9385 bbv.HexNotationWord <> :::'''b'_x not
+R9378:9381 riscv <> b__0:58 var
+R9436:9441 Sail.Operators_mwords <> eq_vec def
+R9462:9466 Sail.Values <> mword def
+R9449:9450 bbv.HexNotationWord <> :::'''b'_x not
+R9443:9446 riscv <> b__0:58 var
+R9501:9506 Sail.Operators_mwords <> eq_vec def
+R9527:9531 Sail.Values <> mword def
+R9514:9515 bbv.HexNotationWord <> :::'''b'_x not
+R9508:9511 riscv <> b__0:58 var
+R9566:9571 Sail.Operators_mwords <> eq_vec def
+R9592:9596 Sail.Values <> mword def
+R9579:9580 bbv.HexNotationWord <> :::'''b'_x not
+R9573:9576 riscv <> b__0:58 var
+R9631:9636 Sail.Operators_mwords <> eq_vec def
+R9657:9661 Sail.Values <> mword def
+R9644:9645 bbv.HexNotationWord <> :::'''b'_x not
+R9638:9641 riscv <> b__0:58 var
+R9696:9701 Sail.Operators_mwords <> eq_vec def
+R9722:9726 Sail.Values <> mword def
+R9709:9710 bbv.HexNotationWord <> :::'''b'_x not
+R9703:9706 riscv <> b__0:58 var
+R9761:9766 Sail.Operators_mwords <> eq_vec def
+R9787:9791 Sail.Values <> mword def
+R9774:9775 bbv.HexNotationWord <> :::'''b'_x not
+R9768:9771 riscv <> b__0:58 var
+R9826:9831 Sail.Operators_mwords <> eq_vec def
+R9852:9856 Sail.Values <> mword def
+R9839:9840 bbv.HexNotationWord <> :::'''b'_x not
+R9833:9836 riscv <> b__0:58 var
+R9891:9896 Sail.Operators_mwords <> eq_vec def
+R9917:9921 Sail.Values <> mword def
+R9904:9905 bbv.HexNotationWord <> :::'''b'_x not
+R9898:9901 riscv <> b__0:58 var
+R9956:9961 Sail.Operators_mwords <> eq_vec def
+R9982:9986 Sail.Values <> mword def
+R9969:9970 bbv.HexNotationWord <> :::'''b'_x not
+R9963:9966 riscv <> b__0:58 var
+R10021:10026 Sail.Operators_mwords <> eq_vec def
+R10047:10051 Sail.Values <> mword def
+R10034:10035 bbv.HexNotationWord <> :::'''b'_x not
+R10028:10031 riscv <> b__0:58 var
+R10086:10091 Sail.Operators_mwords <> eq_vec def
+R10112:10116 Sail.Values <> mword def
+R10099:10100 bbv.HexNotationWord <> :::'''b'_x not
+R10093:10096 riscv <> b__0:58 var
+R10151:10156 Sail.Operators_mwords <> eq_vec def
+R10177:10181 Sail.Values <> mword def
+R10164:10165 bbv.HexNotationWord <> :::'''b'_x not
+R10158:10161 riscv <> b__0:58 var
+R10216:10221 Sail.Operators_mwords <> eq_vec def
+R10242:10246 Sail.Values <> mword def
+R10229:10230 bbv.HexNotationWord <> :::'''b'_x not
+R10223:10226 riscv <> b__0:58 var
+R10281:10286 Sail.Operators_mwords <> eq_vec def
+R10307:10311 Sail.Values <> mword def
+R10294:10295 bbv.HexNotationWord <> :::'''b'_x not
+R10288:10291 riscv <> b__0:58 var
+R10346:10351 Sail.Operators_mwords <> eq_vec def
+R10372:10376 Sail.Values <> mword def
+R10359:10360 bbv.HexNotationWord <> :::'''b'_x not
+R10353:10356 riscv <> b__0:58 var
+R10411:10416 Sail.Operators_mwords <> eq_vec def
+R10437:10441 Sail.Values <> mword def
+R10424:10425 bbv.HexNotationWord <> :::'''b'_x not
+R10418:10421 riscv <> b__0:58 var
+R10476:10481 Sail.Operators_mwords <> eq_vec def
+R10502:10506 Sail.Values <> mword def
+R10489:10490 bbv.HexNotationWord <> :::'''b'_x not
+R10483:10486 riscv <> b__0:58 var
+R10541:10546 Sail.Operators_mwords <> eq_vec def
+R10567:10571 Sail.Values <> mword def
+R10554:10555 bbv.HexNotationWord <> :::'''b'_x not
+R10548:10551 riscv <> b__0:58 var
+R10606:10611 Sail.Operators_mwords <> eq_vec def
+R10632:10636 Sail.Values <> mword def
+R10619:10620 bbv.HexNotationWord <> :::'''b'_x not
+R10613:10616 riscv <> b__0:58 var
+R10671:10676 Sail.Operators_mwords <> eq_vec def
+R10697:10701 Sail.Values <> mword def
+R10684:10685 bbv.HexNotationWord <> :::'''b'_x not
+R10678:10681 riscv <> b__0:58 var
+R10736:10741 Sail.Operators_mwords <> eq_vec def
+R10762:10766 Sail.Values <> mword def
+R10749:10750 bbv.HexNotationWord <> :::'''b'_x not
+R10743:10746 riscv <> b__0:58 var
+R10801:10806 Sail.Operators_mwords <> eq_vec def
+R10827:10831 Sail.Values <> mword def
+R10814:10815 bbv.HexNotationWord <> :::'''b'_x not
+R10808:10811 riscv <> b__0:58 var
+R10867:10872 Sail.Operators_mwords <> eq_vec def
+R10893:10897 Sail.Values <> mword def
+R10880:10881 bbv.HexNotationWord <> :::'''b'_x not
+R10874:10877 riscv <> b__0:58 var
+R10933:10938 Sail.Operators_mwords <> eq_vec def
+R10959:10963 Sail.Values <> mword def
+R10946:10947 bbv.HexNotationWord <> :::'''b'_x not
+R10940:10943 riscv <> b__0:58 var
+R10998:11003 Sail.Operators_mwords <> eq_vec def
+R11024:11028 Sail.Values <> mword def
+R11011:11012 bbv.HexNotationWord <> :::'''b'_x not
+R11005:11008 riscv <> b__0:58 var
+R11063:11068 Sail.Operators_mwords <> eq_vec def
+R11089:11093 Sail.Values <> mword def
+R11076:11077 bbv.HexNotationWord <> :::'''b'_x not
+R11070:11073 riscv <> b__0:58 var
+R11128:11133 Sail.Operators_mwords <> eq_vec def
+R11154:11158 Sail.Values <> mword def
+R11141:11142 bbv.HexNotationWord <> :::'''b'_x not
+R11135:11138 riscv <> b__0:58 var
+R11270:11274 Sail.Prompt_monad <> :::x_'>>='_x not
+R11196:11206 Sail.Prompt_monad <> assert_exp' def
+R11208:11212 Coq.Init.Datatypes <> false constr
+R11290:11293 Sail.Prompt_monad <> exit def
+R11295:11296 Coq.Init.Datatypes <> tt constr
+R11168:11174 Sail.Prompt_monad <> returnm def
+R11103:11109 Sail.Prompt_monad <> returnm def
+R11038:11044 Sail.Prompt_monad <> returnm def
+R10973:10979 Sail.Prompt_monad <> returnm def
+R10907:10913 Sail.Prompt_monad <> returnm def
+R10841:10847 Sail.Prompt_monad <> returnm def
+R10776:10782 Sail.Prompt_monad <> returnm def
+R10711:10717 Sail.Prompt_monad <> returnm def
+R10646:10652 Sail.Prompt_monad <> returnm def
+R10581:10587 Sail.Prompt_monad <> returnm def
+R10516:10522 Sail.Prompt_monad <> returnm def
+R10451:10457 Sail.Prompt_monad <> returnm def
+R10386:10392 Sail.Prompt_monad <> returnm def
+R10321:10327 Sail.Prompt_monad <> returnm def
+R10256:10262 Sail.Prompt_monad <> returnm def
+R10191:10197 Sail.Prompt_monad <> returnm def
+R10126:10132 Sail.Prompt_monad <> returnm def
+R10061:10067 Sail.Prompt_monad <> returnm def
+R9996:10002 Sail.Prompt_monad <> returnm def
+R9931:9937 Sail.Prompt_monad <> returnm def
+R9866:9872 Sail.Prompt_monad <> returnm def
+R9801:9807 Sail.Prompt_monad <> returnm def
+R9736:9742 Sail.Prompt_monad <> returnm def
+R9671:9677 Sail.Prompt_monad <> returnm def
+R9606:9612 Sail.Prompt_monad <> returnm def
+R9541:9547 Sail.Prompt_monad <> returnm def
+R9476:9482 Sail.Prompt_monad <> returnm def
+R9411:9417 Sail.Prompt_monad <> returnm def
+R9346:9352 Sail.Prompt_monad <> returnm def
+R9281:9287 Sail.Prompt_monad <> returnm def
+R9216:9222 Sail.Prompt_monad <> returnm def
+R9149:9155 Sail.Prompt_monad <> returnm def
+def 11329:11342 <> init_base_regs
+R11346:11347 Coq.Init.Datatypes <> tt constr
+R11351:11354 Coq.Init.Datatypes <> unit ind
+binder 11346:11354 <> pat:59
+R11359:11359 riscv_types <> M def
+R11362:11365 Coq.Init.Datatypes <> unit ind
+R12382:12382 riscv_types <> M def
+R12385:12388 Coq.Init.Datatypes <> unit ind
+R12348:12351 Sail.Prompt_monad <> :::x_'>>'_x not
+R12315:12321 Sail.Prompt_monad <> :::x_'>>'_x not
+R12282:12288 Sail.Prompt_monad <> :::x_'>>'_x not
+R12249:12255 Sail.Prompt_monad <> :::x_'>>'_x not
+R12216:12222 Sail.Prompt_monad <> :::x_'>>'_x not
+R12183:12189 Sail.Prompt_monad <> :::x_'>>'_x not
+R12150:12156 Sail.Prompt_monad <> :::x_'>>'_x not
+R12117:12123 Sail.Prompt_monad <> :::x_'>>'_x not
+R12084:12090 Sail.Prompt_monad <> :::x_'>>'_x not
+R12051:12057 Sail.Prompt_monad <> :::x_'>>'_x not
+R12018:12024 Sail.Prompt_monad <> :::x_'>>'_x not
+R11985:11991 Sail.Prompt_monad <> :::x_'>>'_x not
+R11952:11958 Sail.Prompt_monad <> :::x_'>>'_x not
+R11919:11925 Sail.Prompt_monad <> :::x_'>>'_x not
+R11886:11892 Sail.Prompt_monad <> :::x_'>>'_x not
+R11853:11859 Sail.Prompt_monad <> :::x_'>>'_x not
+R11820:11826 Sail.Prompt_monad <> :::x_'>>'_x not
+R11787:11793 Sail.Prompt_monad <> :::x_'>>'_x not
+R11754:11760 Sail.Prompt_monad <> :::x_'>>'_x not
+R11721:11727 Sail.Prompt_monad <> :::x_'>>'_x not
+R11688:11694 Sail.Prompt_monad <> :::x_'>>'_x not
+R11655:11661 Sail.Prompt_monad <> :::x_'>>'_x not
+R11623:11629 Sail.Prompt_monad <> :::x_'>>'_x not
+R11591:11597 Sail.Prompt_monad <> :::x_'>>'_x not
+R11559:11565 Sail.Prompt_monad <> :::x_'>>'_x not
+R11527:11533 Sail.Prompt_monad <> :::x_'>>'_x not
+R11495:11501 Sail.Prompt_monad <> :::x_'>>'_x not
+R11463:11469 Sail.Prompt_monad <> :::x_'>>'_x not
+R11431:11437 Sail.Prompt_monad <> :::x_'>>'_x not
+R11399:11405 Sail.Prompt_monad <> :::x_'>>'_x not
+R11374:11382 Sail.Prompt_monad <> write_reg def
+R11391:11398 riscv <> zero_reg def
+R11384:11389 riscv_types <> x1_ref def
+R11406:11414 Sail.Prompt_monad <> write_reg def
+R11423:11430 riscv <> zero_reg def
+R11416:11421 riscv_types <> x2_ref def
+R11438:11446 Sail.Prompt_monad <> write_reg def
+R11455:11462 riscv <> zero_reg def
+R11448:11453 riscv_types <> x3_ref def
+R11470:11478 Sail.Prompt_monad <> write_reg def
+R11487:11494 riscv <> zero_reg def
+R11480:11485 riscv_types <> x4_ref def
+R11502:11510 Sail.Prompt_monad <> write_reg def
+R11519:11526 riscv <> zero_reg def
+R11512:11517 riscv_types <> x5_ref def
+R11534:11542 Sail.Prompt_monad <> write_reg def
+R11551:11558 riscv <> zero_reg def
+R11544:11549 riscv_types <> x6_ref def
+R11566:11574 Sail.Prompt_monad <> write_reg def
+R11583:11590 riscv <> zero_reg def
+R11576:11581 riscv_types <> x7_ref def
+R11598:11606 Sail.Prompt_monad <> write_reg def
+R11615:11622 riscv <> zero_reg def
+R11608:11613 riscv_types <> x8_ref def
+R11630:11638 Sail.Prompt_monad <> write_reg def
+R11647:11654 riscv <> zero_reg def
+R11640:11645 riscv_types <> x9_ref def
+R11662:11670 Sail.Prompt_monad <> write_reg def
+R11680:11687 riscv <> zero_reg def
+R11672:11678 riscv_types <> x10_ref def
+R11695:11703 Sail.Prompt_monad <> write_reg def
+R11713:11720 riscv <> zero_reg def
+R11705:11711 riscv_types <> x11_ref def
+R11728:11736 Sail.Prompt_monad <> write_reg def
+R11746:11753 riscv <> zero_reg def
+R11738:11744 riscv_types <> x12_ref def
+R11761:11769 Sail.Prompt_monad <> write_reg def
+R11779:11786 riscv <> zero_reg def
+R11771:11777 riscv_types <> x13_ref def
+R11794:11802 Sail.Prompt_monad <> write_reg def
+R11812:11819 riscv <> zero_reg def
+R11804:11810 riscv_types <> x14_ref def
+R11827:11835 Sail.Prompt_monad <> write_reg def
+R11845:11852 riscv <> zero_reg def
+R11837:11843 riscv_types <> x15_ref def
+R11860:11868 Sail.Prompt_monad <> write_reg def
+R11878:11885 riscv <> zero_reg def
+R11870:11876 riscv_types <> x16_ref def
+R11893:11901 Sail.Prompt_monad <> write_reg def
+R11911:11918 riscv <> zero_reg def
+R11903:11909 riscv_types <> x17_ref def
+R11926:11934 Sail.Prompt_monad <> write_reg def
+R11944:11951 riscv <> zero_reg def
+R11936:11942 riscv_types <> x18_ref def
+R11959:11967 Sail.Prompt_monad <> write_reg def
+R11977:11984 riscv <> zero_reg def
+R11969:11975 riscv_types <> x19_ref def
+R11992:12000 Sail.Prompt_monad <> write_reg def
+R12010:12017 riscv <> zero_reg def
+R12002:12008 riscv_types <> x20_ref def
+R12025:12033 Sail.Prompt_monad <> write_reg def
+R12043:12050 riscv <> zero_reg def
+R12035:12041 riscv_types <> x21_ref def
+R12058:12066 Sail.Prompt_monad <> write_reg def
+R12076:12083 riscv <> zero_reg def
+R12068:12074 riscv_types <> x22_ref def
+R12091:12099 Sail.Prompt_monad <> write_reg def
+R12109:12116 riscv <> zero_reg def
+R12101:12107 riscv_types <> x23_ref def
+R12124:12132 Sail.Prompt_monad <> write_reg def
+R12142:12149 riscv <> zero_reg def
+R12134:12140 riscv_types <> x24_ref def
+R12157:12165 Sail.Prompt_monad <> write_reg def
+R12175:12182 riscv <> zero_reg def
+R12167:12173 riscv_types <> x25_ref def
+R12190:12198 Sail.Prompt_monad <> write_reg def
+R12208:12215 riscv <> zero_reg def
+R12200:12206 riscv_types <> x26_ref def
+R12223:12231 Sail.Prompt_monad <> write_reg def
+R12241:12248 riscv <> zero_reg def
+R12233:12239 riscv_types <> x27_ref def
+R12256:12264 Sail.Prompt_monad <> write_reg def
+R12274:12281 riscv <> zero_reg def
+R12266:12272 riscv_types <> x28_ref def
+R12289:12297 Sail.Prompt_monad <> write_reg def
+R12307:12314 riscv <> zero_reg def
+R12299:12305 riscv_types <> x29_ref def
+R12322:12330 Sail.Prompt_monad <> write_reg def
+R12340:12347 riscv <> zero_reg def
+R12332:12338 riscv_types <> x30_ref def
+R12352:12360 Sail.Prompt_monad <> write_reg def
+R12370:12377 riscv <> zero_reg def
+R12362:12368 riscv_types <> x31_ref def
+def 12404:12419 <> initial_regstate
+R12423:12430 riscv_types <> regstate rec
+R12438:12440 riscv_types <> x31 proj
+R12438:12440 riscv_types <> x31 proj
+R12485:12487 riscv_types <> x30 proj
+R12532:12534 riscv_types <> x29 proj
+R12579:12581 riscv_types <> x28 proj
+R12626:12628 riscv_types <> x27 proj
+R12673:12675 riscv_types <> x26 proj
+R12720:12722 riscv_types <> x25 proj
+R12767:12769 riscv_types <> x24 proj
+R12814:12816 riscv_types <> x23 proj
+R12861:12863 riscv_types <> x22 proj
+R12908:12910 riscv_types <> x21 proj
+R12955:12957 riscv_types <> x20 proj
+R13002:13004 riscv_types <> x19 proj
+R13049:13051 riscv_types <> x18 proj
+R13096:13098 riscv_types <> x17 proj
+R13143:13145 riscv_types <> x16 proj
+R13190:13192 riscv_types <> x15 proj
+R13237:13239 riscv_types <> x14 proj
+R13284:13286 riscv_types <> x13 proj
+R13331:13333 riscv_types <> x12 proj
+R13378:13380 riscv_types <> x11 proj
+R13425:13427 riscv_types <> x10 proj
+R13472:13473 riscv_types <> x9 proj
+R13518:13519 riscv_types <> x8 proj
+R13564:13565 riscv_types <> x7 proj
+R13610:13611 riscv_types <> x6 proj
+R13656:13657 riscv_types <> x5 proj
+R13702:13703 riscv_types <> x4 proj
+R13748:13749 riscv_types <> x3 proj
+R13794:13795 riscv_types <> x2 proj
+R13840:13841 riscv_types <> x1 proj
+R13886:13893 riscv_types <> instbits proj
+R13938:13943 riscv_types <> nextPC proj
+R13988:13989 riscv_types <> PC proj
+R12470:12474 Sail.Values <> mword def
+R12446:12447 bbv.HexNotationWord <> :::'Ox'_x not
+R12517:12521 Sail.Values <> mword def
+R12493:12494 bbv.HexNotationWord <> :::'Ox'_x not
+R12564:12568 Sail.Values <> mword def
+R12540:12541 bbv.HexNotationWord <> :::'Ox'_x not
+R12611:12615 Sail.Values <> mword def
+R12587:12588 bbv.HexNotationWord <> :::'Ox'_x not
+R12658:12662 Sail.Values <> mword def
+R12634:12635 bbv.HexNotationWord <> :::'Ox'_x not
+R12705:12709 Sail.Values <> mword def
+R12681:12682 bbv.HexNotationWord <> :::'Ox'_x not
+R12752:12756 Sail.Values <> mword def
+R12728:12729 bbv.HexNotationWord <> :::'Ox'_x not
+R12799:12803 Sail.Values <> mword def
+R12775:12776 bbv.HexNotationWord <> :::'Ox'_x not
+R12846:12850 Sail.Values <> mword def
+R12822:12823 bbv.HexNotationWord <> :::'Ox'_x not
+R12893:12897 Sail.Values <> mword def
+R12869:12870 bbv.HexNotationWord <> :::'Ox'_x not
+R12940:12944 Sail.Values <> mword def
+R12916:12917 bbv.HexNotationWord <> :::'Ox'_x not
+R12987:12991 Sail.Values <> mword def
+R12963:12964 bbv.HexNotationWord <> :::'Ox'_x not
+R13034:13038 Sail.Values <> mword def
+R13010:13011 bbv.HexNotationWord <> :::'Ox'_x not
+R13081:13085 Sail.Values <> mword def
+R13057:13058 bbv.HexNotationWord <> :::'Ox'_x not
+R13128:13132 Sail.Values <> mword def
+R13104:13105 bbv.HexNotationWord <> :::'Ox'_x not
+R13175:13179 Sail.Values <> mword def
+R13151:13152 bbv.HexNotationWord <> :::'Ox'_x not
+R13222:13226 Sail.Values <> mword def
+R13198:13199 bbv.HexNotationWord <> :::'Ox'_x not
+R13269:13273 Sail.Values <> mword def
+R13245:13246 bbv.HexNotationWord <> :::'Ox'_x not
+R13316:13320 Sail.Values <> mword def
+R13292:13293 bbv.HexNotationWord <> :::'Ox'_x not
+R13363:13367 Sail.Values <> mword def
+R13339:13340 bbv.HexNotationWord <> :::'Ox'_x not
+R13410:13414 Sail.Values <> mword def
+R13386:13387 bbv.HexNotationWord <> :::'Ox'_x not
+R13457:13461 Sail.Values <> mword def
+R13433:13434 bbv.HexNotationWord <> :::'Ox'_x not
+R13503:13507 Sail.Values <> mword def
+R13479:13480 bbv.HexNotationWord <> :::'Ox'_x not
+R13549:13553 Sail.Values <> mword def
+R13525:13526 bbv.HexNotationWord <> :::'Ox'_x not
+R13595:13599 Sail.Values <> mword def
+R13571:13572 bbv.HexNotationWord <> :::'Ox'_x not
+R13641:13645 Sail.Values <> mword def
+R13617:13618 bbv.HexNotationWord <> :::'Ox'_x not
+R13687:13691 Sail.Values <> mword def
+R13663:13664 bbv.HexNotationWord <> :::'Ox'_x not
+R13733:13737 Sail.Values <> mword def
+R13709:13710 bbv.HexNotationWord <> :::'Ox'_x not
+R13779:13783 Sail.Values <> mword def
+R13755:13756 bbv.HexNotationWord <> :::'Ox'_x not
+R13825:13829 Sail.Values <> mword def
+R13801:13802 bbv.HexNotationWord <> :::'Ox'_x not
+R13871:13875 Sail.Values <> mword def
+R13847:13848 bbv.HexNotationWord <> :::'Ox'_x not
+R13923:13927 Sail.Values <> mword def
+R13899:13900 bbv.HexNotationWord <> :::'Ox'_x not
+R13973:13977 Sail.Values <> mword def
+R13949:13950 bbv.HexNotationWord <> :::'Ox'_x not
+R14019:14023 Sail.Values <> mword def
+R13995:13996 bbv.HexNotationWord <> :::'Ox'_x not
+R14045:14060 riscv <> initial_regstate def