path: root/build/riscv.glob

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