path: root/handwritten_support/riscv_extras.glob

DIGEST 9f6e940694efb436e57a7a26d0b1b3b3
Friscv_extras
R15:23 Sail.Base <> <> lib
R41:46 Coq.Strings.String <> <> lib
R64:67 Coq.Lists.List <> <> lib
def 123:137 <> MEM_fence_rw_rw
binder 140:141 <> rv:1
binder 143:143 <> e:2
R149:152 Coq.Init.Datatypes <> unit ind
R157:161 Sail.Prompt_monad <> monad ind
R163:164 riscv_extras <> rv:1 var
R166:169 Coq.Init.Datatypes <> unit ind
R171:171 riscv_extras <> e:2 var
R176:182 Sail.Prompt_monad <> barrier def
R185:203 Sail.Instr_kinds <> Barrier_RISCV_rw_rw constr
R205:206 Coq.Init.Datatypes <> tt constr
def 221:234 <> MEM_fence_r_rw
binder 238:239 <> rv:3
binder 241:241 <> e:4
R247:250 Coq.Init.Datatypes <> unit ind
R255:259 Sail.Prompt_monad <> monad ind
R261:262 riscv_extras <> rv:3 var
R264:267 Coq.Init.Datatypes <> unit ind
R269:269 riscv_extras <> e:4 var
R274:280 Sail.Prompt_monad <> barrier def
R283:300 Sail.Instr_kinds <> Barrier_RISCV_r_rw constr
R302:303 Coq.Init.Datatypes <> tt constr
def 318:330 <> MEM_fence_r_r
binder 335:336 <> rv:5
binder 338:338 <> e:6
R344:347 Coq.Init.Datatypes <> unit ind
R352:356 Sail.Prompt_monad <> monad ind
R358:359 riscv_extras <> rv:5 var
R361:364 Coq.Init.Datatypes <> unit ind
R366:366 riscv_extras <> e:6 var
R371:377 Sail.Prompt_monad <> barrier def
R380:396 Sail.Instr_kinds <> Barrier_RISCV_r_r constr
R398:399 Coq.Init.Datatypes <> tt constr
def 414:427 <> MEM_fence_rw_w
binder 431:432 <> rv:7
binder 434:434 <> e:8
R440:443 Coq.Init.Datatypes <> unit ind
R448:452 Sail.Prompt_monad <> monad ind
R454:455 riscv_extras <> rv:7 var
R457:460 Coq.Init.Datatypes <> unit ind
R462:462 riscv_extras <> e:8 var
R467:473 Sail.Prompt_monad <> barrier def
R476:493 Sail.Instr_kinds <> Barrier_RISCV_rw_w constr
R495:496 Coq.Init.Datatypes <> tt constr
def 511:523 <> MEM_fence_w_w
binder 528:529 <> rv:9
binder 531:531 <> e:10
R537:540 Coq.Init.Datatypes <> unit ind
R545:549 Sail.Prompt_monad <> monad ind
R551:552 riscv_extras <> rv:9 var
R554:557 Coq.Init.Datatypes <> unit ind
R559:559 riscv_extras <> e:10 var
R564:570 Sail.Prompt_monad <> barrier def
R573:589 Sail.Instr_kinds <> Barrier_RISCV_w_w constr
R591:592 Coq.Init.Datatypes <> tt constr
def 607:620 <> MEM_fence_w_rw
binder 624:625 <> rv:11
binder 627:627 <> e:12
R633:636 Coq.Init.Datatypes <> unit ind
R641:645 Sail.Prompt_monad <> monad ind
R647:648 riscv_extras <> rv:11 var
R650:653 Coq.Init.Datatypes <> unit ind
R655:655 riscv_extras <> e:12 var
R660:666 Sail.Prompt_monad <> barrier def
R669:686 Sail.Instr_kinds <> Barrier_RISCV_w_rw constr
R688:689 Coq.Init.Datatypes <> tt constr
def 704:717 <> MEM_fence_rw_r
binder 721:722 <> rv:13
binder 724:724 <> e:14
R730:733 Coq.Init.Datatypes <> unit ind
R738:742 Sail.Prompt_monad <> monad ind
R744:745 riscv_extras <> rv:13 var
R747:750 Coq.Init.Datatypes <> unit ind
R752:752 riscv_extras <> e:14 var
R757:763 Sail.Prompt_monad <> barrier def
R766:783 Sail.Instr_kinds <> Barrier_RISCV_rw_r constr
R785:786 Coq.Init.Datatypes <> tt constr
def 801:813 <> MEM_fence_r_w
binder 818:819 <> rv:15
binder 821:821 <> e:16
R827:830 Coq.Init.Datatypes <> unit ind
R835:839 Sail.Prompt_monad <> monad ind
R841:842 riscv_extras <> rv:15 var
R844:847 Coq.Init.Datatypes <> unit ind
R849:849 riscv_extras <> e:16 var
R854:860 Sail.Prompt_monad <> barrier def
R863:879 Sail.Instr_kinds <> Barrier_RISCV_r_w constr
R881:882 Coq.Init.Datatypes <> tt constr
def 897:909 <> MEM_fence_w_r
binder 914:915 <> rv:17
binder 917:917 <> e:18
R923:926 Coq.Init.Datatypes <> unit ind
R931:935 Sail.Prompt_monad <> monad ind
R937:938 riscv_extras <> rv:17 var
R940:943 Coq.Init.Datatypes <> unit ind
R945:945 riscv_extras <> e:18 var
R950:956 Sail.Prompt_monad <> barrier def
R959:975 Sail.Instr_kinds <> Barrier_RISCV_w_r constr
R977:978 Coq.Init.Datatypes <> tt constr
def 993:1005 <> MEM_fence_tso
binder 1010:1011 <> rv:19
binder 1013:1013 <> e:20
R1019:1022 Coq.Init.Datatypes <> unit ind
R1027:1031 Sail.Prompt_monad <> monad ind
R1033:1034 riscv_extras <> rv:19 var
R1036:1039 Coq.Init.Datatypes <> unit ind
R1041:1041 riscv_extras <> e:20 var
R1046:1052 Sail.Prompt_monad <> barrier def
R1055:1071 Sail.Instr_kinds <> Barrier_RISCV_tso constr
R1073:1074 Coq.Init.Datatypes <> tt constr
def 1089:1099 <> MEM_fence_i
binder 1106:1107 <> rv:21
binder 1109:1109 <> e:22
R1115:1118 Coq.Init.Datatypes <> unit ind
R1123:1127 Sail.Prompt_monad <> monad ind
R1129:1130 riscv_extras <> rv:21 var
R1132:1135 Coq.Init.Datatypes <> unit ind
R1137:1137 riscv_extras <> e:22 var
R1142:1148 Sail.Prompt_monad <> barrier def
R1151:1165 Sail.Instr_kinds <> Barrier_RISCV_i constr
R1167:1168 Coq.Init.Datatypes <> tt constr
def 1867:1871 <> MEMea
binder 1874:1875 <> rv:23
binder 1877:1877 <> a:24
binder 1879:1879 <> e:25
binder 1882:1889 <> addrsize:26
R1899:1903 Sail.Values <> mword def
R1905:1905 riscv_extras <> a:24 var
binder 1892:1895 <> addr:27
binder 1908:1911 <> size:28
R1935:1939 Sail.Prompt_monad <> monad ind
R1941:1942 riscv_extras <> rv:23 var
R1944:1947 Coq.Init.Datatypes <> unit ind
R1949:1949 riscv_extras <> e:25 var
R1954:1965 Sail.Prompt_monad <> write_mem_ea def
R1993:1996 riscv_extras <> size:28 var
R1988:1991 riscv_extras <> addr:27 var
R1979:1986 riscv_extras <> addrsize:26 var
R1967:1977 Sail.Instr_kinds <> Write_plain constr
def 2010:2022 <> MEMea_release
binder 2025:2026 <> rv:29
binder 2028:2028 <> a:30
binder 2030:2030 <> e:31
binder 2033:2040 <> addrsize:32
R2050:2054 Sail.Values <> mword def
R2056:2056 riscv_extras <> a:30 var
binder 2043:2046 <> addr:33
binder 2059:2062 <> size:34
R2078:2082 Sail.Prompt_monad <> monad ind
R2084:2085 riscv_extras <> rv:29 var
R2087:2090 Coq.Init.Datatypes <> unit ind
R2092:2092 riscv_extras <> e:31 var
R2097:2108 Sail.Prompt_monad <> write_mem_ea def
R2144:2147 riscv_extras <> size:34 var
R2139:2142 riscv_extras <> addr:33 var
R2130:2137 riscv_extras <> addrsize:32 var
R2110:2128 Sail.Instr_kinds <> Write_RISCV_release constr
def 2161:2180 <> MEMea_strong_release
binder 2183:2184 <> rv:35
binder 2186:2186 <> a:36
binder 2188:2188 <> e:37
binder 2191:2198 <> addrsize:38
R2208:2212 Sail.Values <> mword def
R2214:2214 riscv_extras <> a:36 var
binder 2201:2204 <> addr:39
binder 2217:2220 <> size:40
R2229:2233 Sail.Prompt_monad <> monad ind
R2235:2236 riscv_extras <> rv:35 var
R2238:2241 Coq.Init.Datatypes <> unit ind
R2243:2243 riscv_extras <> e:37 var
R2248:2259 Sail.Prompt_monad <> write_mem_ea def
R2302:2305 riscv_extras <> size:40 var
R2297:2300 riscv_extras <> addr:39 var
R2288:2295 riscv_extras <> addrsize:38 var
R2261:2286 Sail.Instr_kinds <> Write_RISCV_strong_release constr
def 2319:2335 <> MEMea_conditional
binder 2338:2339 <> rv:41
binder 2341:2341 <> a:42
binder 2343:2343 <> e:43
binder 2346:2353 <> addrsize:44
R2363:2367 Sail.Values <> mword def
R2369:2369 riscv_extras <> a:42 var
binder 2356:2359 <> addr:45
binder 2372:2375 <> size:46
R2387:2391 Sail.Prompt_monad <> monad ind
R2393:2394 riscv_extras <> rv:41 var
R2396:2399 Coq.Init.Datatypes <> unit ind
R2401:2401 riscv_extras <> e:43 var
R2406:2417 Sail.Prompt_monad <> write_mem_ea def
R2457:2460 riscv_extras <> size:46 var
R2452:2455 riscv_extras <> addr:45 var
R2443:2450 riscv_extras <> addrsize:44 var
R2419:2441 Sail.Instr_kinds <> Write_RISCV_conditional constr
def 2474:2498 <> MEMea_conditional_release
binder 2501:2502 <> rv:47
binder 2504:2504 <> a:48
binder 2506:2506 <> e:49
binder 2509:2516 <> addrsize:50
R2526:2530 Sail.Values <> mword def
R2532:2532 riscv_extras <> a:48 var
binder 2519:2522 <> addr:51
binder 2535:2538 <> size:52
R2542:2546 Sail.Prompt_monad <> monad ind
R2548:2549 riscv_extras <> rv:47 var
R2551:2554 Coq.Init.Datatypes <> unit ind
R2556:2556 riscv_extras <> e:49 var
R2561:2572 Sail.Prompt_monad <> write_mem_ea def
R2620:2623 riscv_extras <> size:52 var
R2615:2618 riscv_extras <> addr:51 var
R2606:2613 riscv_extras <> addrsize:50 var
R2574:2604 Sail.Instr_kinds <> Write_RISCV_conditional_release constr
def 2637:2668 <> MEMea_conditional_strong_release
binder 2671:2672 <> rv:53
binder 2674:2674 <> a:54
binder 2676:2676 <> e:55
binder 2679:2686 <> addrsize:56
R2696:2700 Sail.Values <> mword def
R2702:2702 riscv_extras <> a:54 var
binder 2689:2692 <> addr:57
binder 2705:2708 <> size:58
R2712:2716 Sail.Prompt_monad <> monad ind
R2718:2719 riscv_extras <> rv:53 var
R2721:2724 Coq.Init.Datatypes <> unit ind
R2726:2726 riscv_extras <> e:55 var
R2773:2784 Sail.Prompt_monad <> write_mem_ea def
R2839:2842 riscv_extras <> size:58 var
R2834:2837 riscv_extras <> addr:57 var
R2825:2832 riscv_extras <> addrsize:56 var
R2786:2823 Sail.Instr_kinds <> Write_RISCV_conditional_strong_release constr
def 3812:3815 <> MEMr
binder 3818:3819 <> rv:59
binder 3821:3821 <> e:60
binder 3824:3831 <> addrsize:61
binder 3833:3836 <> size:62
R3853:3857 Sail.Values <> mword def
R3859:3866 riscv_extras <> addrsize:61 var
binder 3839:3844 <> hexRAM:63
binder 3846:3849 <> addr:64
R3895:3903 Sail.Values <> ArithFact class
R3910:3914 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R3906:3909 riscv_extras <> size:62 var
binder 3895:3916 <> H:65
R3921:3925 Sail.Prompt_monad <> monad ind
R3927:3928 riscv_extras <> rv:59 var
R3931:3935 Sail.Values <> mword def
R3939:3941 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R3942:3945 riscv_extras <> size:62 var
R3949:3949 riscv_extras <> e:60 var
R3954:3961 Sail.Prompt_monad <> read_mem def
R3988:3991 riscv_extras <> size:62 var
R3983:3986 riscv_extras <> addr:64 var
R3974:3981 riscv_extras <> addrsize:61 var
R3963:3972 Sail.Instr_kinds <> Read_plain constr
def 4005:4016 <> MEMr_acquire
binder 4019:4020 <> rv:66
binder 4022:4022 <> e:67
binder 4025:4032 <> addrsize:68
binder 4034:4037 <> size:69
R4054:4058 Sail.Values <> mword def
R4060:4067 riscv_extras <> addrsize:68 var
binder 4040:4045 <> hexRAM:70
binder 4047:4050 <> addr:71
R4088:4096 Sail.Values <> ArithFact class
R4103:4107 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R4099:4102 riscv_extras <> size:69 var
binder 4088:4109 <> H:72
R4114:4118 Sail.Prompt_monad <> monad ind
R4120:4121 riscv_extras <> rv:66 var
R4124:4128 Sail.Values <> mword def
R4132:4134 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R4135:4138 riscv_extras <> size:69 var
R4142:4142 riscv_extras <> e:67 var
R4147:4154 Sail.Prompt_monad <> read_mem def
R4189:4192 riscv_extras <> size:69 var
R4184:4187 riscv_extras <> addr:71 var
R4175:4182 riscv_extras <> addrsize:68 var
R4156:4173 Sail.Instr_kinds <> Read_RISCV_acquire constr
def 4206:4224 <> MEMr_strong_acquire
binder 4227:4228 <> rv:73
binder 4230:4230 <> e:74
binder 4233:4240 <> addrsize:75
binder 4242:4245 <> size:76
R4262:4266 Sail.Values <> mword def
R4268:4275 riscv_extras <> addrsize:75 var
binder 4248:4253 <> hexRAM:77
binder 4255:4258 <> addr:78
R4289:4297 Sail.Values <> ArithFact class
R4304:4308 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R4300:4303 riscv_extras <> size:76 var
binder 4289:4310 <> H:79
R4315:4319 Sail.Prompt_monad <> monad ind
R4321:4322 riscv_extras <> rv:73 var
R4325:4329 Sail.Values <> mword def
R4333:4335 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R4336:4339 riscv_extras <> size:76 var
R4343:4343 riscv_extras <> e:74 var
R4348:4355 Sail.Prompt_monad <> read_mem def
R4397:4400 riscv_extras <> size:76 var
R4392:4395 riscv_extras <> addr:78 var
R4383:4390 riscv_extras <> addrsize:75 var
R4357:4381 Sail.Instr_kinds <> Read_RISCV_strong_acquire constr
def 4414:4426 <> MEMr_reserved
binder 4429:4430 <> rv:80
binder 4432:4432 <> e:81
binder 4435:4442 <> addrsize:82
binder 4444:4447 <> size:83
R4464:4468 Sail.Values <> mword def
R4470:4477 riscv_extras <> addrsize:82 var
binder 4450:4455 <> hexRAM:84
binder 4457:4460 <> addr:85
R4497:4505 Sail.Values <> ArithFact class
R4512:4516 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R4508:4511 riscv_extras <> size:83 var
binder 4497:4518 <> H:86
R4523:4527 Sail.Prompt_monad <> monad ind
R4529:4530 riscv_extras <> rv:80 var
R4533:4537 Sail.Values <> mword def
R4541:4543 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R4544:4547 riscv_extras <> size:83 var
R4551:4551 riscv_extras <> e:81 var
R4556:4563 Sail.Prompt_monad <> read_mem def
R4599:4602 riscv_extras <> size:83 var
R4594:4597 riscv_extras <> addr:85 var
R4585:4592 riscv_extras <> addrsize:82 var
R4565:4583 Sail.Instr_kinds <> Read_RISCV_reserved constr
def 4616:4636 <> MEMr_reserved_acquire
binder 4639:4640 <> rv:87
binder 4642:4642 <> e:88
binder 4645:4652 <> addrsize:89
binder 4654:4657 <> size:90
R4674:4678 Sail.Values <> mword def
R4680:4687 riscv_extras <> addrsize:89 var
binder 4660:4665 <> hexRAM:91
binder 4667:4670 <> addr:92
R4699:4707 Sail.Values <> ArithFact class
R4714:4718 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R4710:4713 riscv_extras <> size:90 var
binder 4699:4720 <> H:93
R4725:4729 Sail.Prompt_monad <> monad ind
R4731:4732 riscv_extras <> rv:87 var
R4735:4739 Sail.Values <> mword def
R4743:4745 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R4746:4749 riscv_extras <> size:90 var
R4753:4753 riscv_extras <> e:88 var
R4758:4765 Sail.Prompt_monad <> read_mem def
R4809:4812 riscv_extras <> size:90 var
R4804:4807 riscv_extras <> addr:92 var
R4795:4802 riscv_extras <> addrsize:89 var
R4767:4793 Sail.Instr_kinds <> Read_RISCV_reserved_acquire constr
def 4826:4853 <> MEMr_reserved_strong_acquire
binder 4856:4857 <> rv:94
binder 4859:4859 <> e:95
binder 4862:4869 <> addrsize:96
binder 4871:4874 <> size:97
R4891:4895 Sail.Values <> mword def
R4897:4904 riscv_extras <> addrsize:96 var
binder 4877:4882 <> hexRAM:98
binder 4884:4887 <> addr:99
R4909:4917 Sail.Values <> ArithFact class
R4924:4928 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R4920:4923 riscv_extras <> size:97 var
binder 4909:4930 <> H:100
R4935:4939 Sail.Prompt_monad <> monad ind
R4941:4942 riscv_extras <> rv:94 var
R4945:4949 Sail.Values <> mword def
R4953:4955 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R4956:4959 riscv_extras <> size:97 var
R4963:4963 riscv_extras <> e:95 var
R4968:4975 Sail.Prompt_monad <> read_mem def
R5026:5029 riscv_extras <> size:97 var
R5021:5024 riscv_extras <> addr:99 var
R5012:5019 riscv_extras <> addrsize:96 var
R4977:5010 Sail.Instr_kinds <> Read_RISCV_reserved_strong_acquire constr
def 6053:6056 <> MEMw
binder 6059:6060 <> rv:101
binder 6062:6062 <> e:102
binder 6065:6072 <> addrsize:103
binder 6074:6077 <> size:104
R6094:6098 Sail.Values <> mword def
R6100:6107 riscv_extras <> addrsize:103 var
binder 6080:6085 <> hexRAM:105
binder 6087:6090 <> addr:106
R6115:6119 Sail.Values <> mword def
R6123:6125 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R6126:6129 riscv_extras <> size:104 var
binder 6111:6111 <> v:107
R6162:6166 Sail.Prompt_monad <> monad ind
R6168:6169 riscv_extras <> rv:101 var
R6171:6174 Coq.Init.Datatypes <> bool ind
R6176:6176 riscv_extras <> e:102 var
R6181:6189 Sail.Prompt_monad <> write_mem def
R6222:6222 riscv_extras <> v:107 var
R6217:6220 riscv_extras <> size:104 var
R6212:6215 riscv_extras <> addr:106 var
R6203:6210 riscv_extras <> addrsize:103 var
R6191:6201 Sail.Instr_kinds <> Write_plain constr
def 6236:6247 <> MEMw_release
binder 6250:6251 <> rv:108
binder 6253:6253 <> e:109
binder 6256:6263 <> addrsize:110
binder 6265:6268 <> size:111
R6285:6289 Sail.Values <> mword def
R6291:6298 riscv_extras <> addrsize:110 var
binder 6271:6276 <> hexRAM:112
binder 6278:6281 <> addr:113
R6306:6310 Sail.Values <> mword def
R6314:6316 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R6317:6320 riscv_extras <> size:111 var
binder 6302:6302 <> v:114
R6345:6349 Sail.Prompt_monad <> monad ind
R6351:6352 riscv_extras <> rv:108 var
R6354:6357 Coq.Init.Datatypes <> bool ind
R6359:6359 riscv_extras <> e:109 var
R6364:6372 Sail.Prompt_monad <> write_mem def
R6413:6413 riscv_extras <> v:114 var
R6408:6411 riscv_extras <> size:111 var
R6403:6406 riscv_extras <> addr:113 var
R6394:6401 riscv_extras <> addrsize:110 var
R6374:6392 Sail.Instr_kinds <> Write_RISCV_release constr
def 6427:6445 <> MEMw_strong_release
binder 6448:6449 <> rv:115
binder 6451:6451 <> e:116
binder 6454:6461 <> addrsize:117
binder 6463:6466 <> size:118
R6483:6487 Sail.Values <> mword def
R6489:6496 riscv_extras <> addrsize:117 var
binder 6469:6474 <> hexRAM:119
binder 6476:6479 <> addr:120
R6504:6508 Sail.Values <> mword def
R6512:6514 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R6515:6518 riscv_extras <> size:118 var
binder 6500:6500 <> v:121
R6536:6540 Sail.Prompt_monad <> monad ind
R6542:6543 riscv_extras <> rv:115 var
R6545:6548 Coq.Init.Datatypes <> bool ind
R6550:6550 riscv_extras <> e:116 var
R6555:6563 Sail.Prompt_monad <> write_mem def
R6611:6611 riscv_extras <> v:121 var
R6606:6609 riscv_extras <> size:118 var
R6601:6604 riscv_extras <> addr:120 var
R6592:6599 riscv_extras <> addrsize:117 var
R6565:6590 Sail.Instr_kinds <> Write_RISCV_strong_release constr
def 6625:6640 <> MEMw_conditional
binder 6643:6644 <> rv:122
binder 6646:6646 <> e:123
binder 6649:6656 <> addrsize:124
binder 6658:6661 <> size:125
R6678:6682 Sail.Values <> mword def
R6684:6691 riscv_extras <> addrsize:124 var
binder 6664:6669 <> hexRAM:126
binder 6671:6674 <> addr:127
R6699:6703 Sail.Values <> mword def
R6707:6709 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R6710:6713 riscv_extras <> size:125 var
binder 6695:6695 <> v:128
R6734:6738 Sail.Prompt_monad <> monad ind
R6740:6741 riscv_extras <> rv:122 var
R6743:6746 Coq.Init.Datatypes <> bool ind
R6748:6748 riscv_extras <> e:123 var
R6753:6761 Sail.Prompt_monad <> write_mem def
R6806:6806 riscv_extras <> v:128 var
R6801:6804 riscv_extras <> size:125 var
R6796:6799 riscv_extras <> addr:127 var
R6787:6794 riscv_extras <> addrsize:124 var
R6763:6785 Sail.Instr_kinds <> Write_RISCV_conditional constr
def 6820:6843 <> MEMw_conditional_release
binder 6846:6847 <> rv:129
binder 6849:6849 <> e:130
binder 6852:6859 <> addrsize:131
binder 6861:6864 <> size:132
R6881:6885 Sail.Values <> mword def
R6887:6894 riscv_extras <> addrsize:131 var
binder 6867:6872 <> hexRAM:133
binder 6874:6877 <> addr:134
R6902:6906 Sail.Values <> mword def
R6910:6912 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R6913:6916 riscv_extras <> size:132 var
binder 6898:6898 <> v:135
R6929:6933 Sail.Prompt_monad <> monad ind
R6935:6936 riscv_extras <> rv:129 var
R6938:6941 Coq.Init.Datatypes <> bool ind
R6943:6943 riscv_extras <> e:130 var
R6948:6956 Sail.Prompt_monad <> write_mem def
R7009:7009 riscv_extras <> v:135 var
R7004:7007 riscv_extras <> size:132 var
R6999:7002 riscv_extras <> addr:134 var
R6990:6997 riscv_extras <> addrsize:131 var
R6958:6988 Sail.Instr_kinds <> Write_RISCV_conditional_release constr
def 7023:7053 <> MEMw_conditional_strong_release
binder 7056:7057 <> rv:136
binder 7059:7059 <> e:137
binder 7062:7069 <> addrsize:138
binder 7071:7074 <> size:139
R7091:7095 Sail.Values <> mword def
R7097:7104 riscv_extras <> addrsize:138 var
binder 7077:7082 <> hexRAM:140
binder 7084:7087 <> addr:141
R7112:7116 Sail.Values <> mword def
R7120:7122 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R7123:7126 riscv_extras <> size:139 var
binder 7108:7108 <> v:142
R7132:7136 Sail.Prompt_monad <> monad ind
R7138:7139 riscv_extras <> rv:136 var
R7141:7144 Coq.Init.Datatypes <> bool ind
R7146:7146 riscv_extras <> e:137 var
R7151:7159 Sail.Prompt_monad <> write_mem def
R7219:7219 riscv_extras <> v:142 var
R7214:7217 riscv_extras <> size:139 var
R7209:7212 riscv_extras <> addr:141 var
R7200:7207 riscv_extras <> addrsize:138 var
R7161:7198 Sail.Instr_kinds <> Write_RISCV_conditional_strong_release constr
def 7234:7248 <> shift_bits_left
binder 7251:7251 <> a:143
binder 7253:7253 <> b:144
R7261:7265 Sail.Values <> mword def
R7267:7267 riscv_extras <> a:143 var
binder 7257:7257 <> v:145
R7275:7279 Sail.Values <> mword def
R7281:7281 riscv_extras <> b:144 var
binder 7271:7271 <> n:146
R7286:7290 Sail.Values <> mword def
R7292:7292 riscv_extras <> a:143 var
R7299:7304 Sail.Operators_mwords <> shiftl def
R7309:7320 Sail.Values <> int_of_mword def
R7328:7328 riscv_extras <> n:146 var
R7322:7326 Coq.Init.Datatypes <> false constr
R7306:7306 riscv_extras <> v:145 var
def 7344:7359 <> shift_bits_right
binder 7362:7362 <> a:147
binder 7364:7364 <> b:148
R7372:7376 Sail.Values <> mword def
R7378:7378 riscv_extras <> a:147 var
binder 7368:7368 <> v:149
R7386:7390 Sail.Values <> mword def
R7392:7392 riscv_extras <> b:148 var
binder 7382:7382 <> n:150
R7397:7401 Sail.Values <> mword def
R7403:7403 riscv_extras <> a:147 var
R7410:7415 Sail.Operators_mwords <> shiftr def
R7420:7431 Sail.Values <> int_of_mword def
R7439:7439 riscv_extras <> n:150 var
R7433:7437 Coq.Init.Datatypes <> false constr
R7417:7417 riscv_extras <> v:149 var
def 7455:7476 <> shift_bits_right_arith
binder 7479:7479 <> a:151
binder 7481:7481 <> b:152
R7489:7493 Sail.Values <> mword def
R7495:7495 riscv_extras <> a:151 var
binder 7485:7485 <> v:153
R7503:7507 Sail.Values <> mword def
R7509:7509 riscv_extras <> b:152 var
binder 7499:7499 <> n:154
R7514:7518 Sail.Values <> mword def
R7520:7520 riscv_extras <> a:151 var
R7527:7538 Sail.Operators_mwords <> arith_shiftr def
R7543:7554 Sail.Values <> int_of_mword def
R7562:7562 riscv_extras <> n:154 var
R7556:7560 Coq.Init.Datatypes <> false constr
R7540:7540 riscv_extras <> v:153 var
def 7627:7639 <> internal_pick
binder 7642:7643 <> rv:155
binder 7645:7645 <> a:156
binder 7647:7647 <> e:157
R7656:7659 Coq.Init.Datatypes <> list ind
R7661:7661 riscv_extras <> a:156 var
binder 7651:7652 <> vs:158
R7666:7670 Sail.Prompt_monad <> monad ind
R7672:7673 riscv_extras <> rv:155 var
R7675:7675 riscv_extras <> a:156 var
R7677:7677 riscv_extras <> e:157 var
R7688:7689 riscv_extras <> vs:158 var
R7700:7701 Coq.Init.Datatypes <> ::list_scope:x_'::'_x not
R7708:7714 Sail.Prompt_monad <> returnm def
R7725:7728 Sail.Prompt_monad <> Fail constr
def 7776:7791 <> undefined_string
binder 7794:7795 <> rv:160
binder 7797:7797 <> e:161
R7803:7806 Coq.Init.Datatypes <> unit ind
R7811:7815 Sail.Prompt_monad <> monad ind
R7817:7818 riscv_extras <> rv:160 var
R7820:7825 Coq.Strings.String <> string ind
R7827:7827 riscv_extras <> e:161 var
R7832:7838 Sail.Prompt_monad <> returnm def
def 7862:7875 <> undefined_unit
binder 7878:7879 <> rv:162
binder 7881:7881 <> e:163
R7887:7890 Coq.Init.Datatypes <> unit ind
R7895:7899 Sail.Prompt_monad <> monad ind
R7901:7902 riscv_extras <> rv:162 var
R7904:7907 Coq.Init.Datatypes <> unit ind
R7909:7909 riscv_extras <> e:163 var
R7914:7920 Sail.Prompt_monad <> returnm def
R7922:7923 Coq.Init.Datatypes <> tt constr
def 7937:7949 <> undefined_int
binder 7952:7953 <> rv:164
binder 7955:7955 <> e:165
R7961:7964 Coq.Init.Datatypes <> unit ind
R7969:7973 Sail.Prompt_monad <> monad ind
R7975:7976 riscv_extras <> rv:164 var
R7978:7978 Coq.Numbers.BinNums <> Z ind
R7980:7980 riscv_extras <> e:165 var
R7985:7991 Sail.Prompt_monad <> returnm def
R7996:7997 Sail.Values <> ii def
def 8097:8112 <> undefined_vector
binder 8115:8116 <> rv:166
binder 8118:8118 <> a:167
binder 8120:8120 <> e:168
binder 8123:8125 <> len:169
R8132:8132 riscv_extras <> a:167 var
binder 8128:8128 <> u:170
R8137:8145 Sail.Values <> ArithFact class
R8151:8155 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R8148:8150 riscv_extras <> len:169 var
binder 8137:8157 <> H:171
R8162:8166 Sail.Prompt_monad <> monad ind
R8168:8169 riscv_extras <> rv:166 var
R8172:8174 Sail.Values <> vec def
R8176:8176 riscv_extras <> a:167 var
R8178:8180 riscv_extras <> len:169 var
R8183:8183 riscv_extras <> e:168 var
R8188:8194 Sail.Prompt_monad <> returnm def
R8197:8204 Sail.Values <> vec_init def
R8208:8210 riscv_extras <> len:169 var
R8206:8206 riscv_extras <> u:170 var
def 8316:8334 <> undefined_bitvector
binder 8337:8338 <> rv:172
binder 8340:8340 <> e:173
binder 8343:8345 <> len:174
R8349:8357 Sail.Values <> ArithFact class
R8363:8367 Coq.ZArith.BinInt <> ::Z_scope:x_'>=?'_x not
R8360:8362 riscv_extras <> len:174 var
binder 8349:8369 <> H:175
R8374:8378 Sail.Prompt_monad <> monad ind
R8380:8381 riscv_extras <> rv:172 var
R8384:8388 Sail.Values <> mword def
R8390:8392 riscv_extras <> len:174 var
R8395:8395 riscv_extras <> e:173 var
R8400:8406 Sail.Prompt_monad <> returnm def
R8409:8420 Sail.Values <> mword_of_int def
def 8523:8536 <> undefined_bits
binder 8539:8540 <> rv:176
binder 8542:8542 <> e:177
R8549:8567 riscv_extras <> undefined_bitvector def
R8569:8570 riscv_extras <> rv:176 var
R8572:8572 riscv_extras <> e:177 var
def 8586:8598 <> undefined_bit
binder 8601:8602 <> rv:178
binder 8604:8604 <> e:179
R8610:8613 Coq.Init.Datatypes <> unit ind
R8618:8622 Sail.Prompt_monad <> monad ind
R8624:8625 riscv_extras <> rv:178 var
R8627:8630 Sail.Values <> bitU ind
R8632:8632 riscv_extras <> e:179 var
R8637:8643 Sail.Prompt_monad <> returnm def
R8645:8646 Sail.Values <> BU constr
def 8755:8769 <> undefined_range
binder 8772:8773 <> rv:180
binder 8775:8775 <> e:181
binder 8778:8778 <> i:182
binder 8780:8780 <> j:183
R8784:8792 Sail.Values <> ArithFact class
R8796:8800 Coq.ZArith.BinInt <> ::Z_scope:x_'<=?'_x not
R8795:8795 riscv_extras <> i:182 var
R8801:8801 riscv_extras <> j:183 var
binder 8784:8802 <> H:184
R8807:8811 Sail.Prompt_monad <> monad ind
R8813:8814 riscv_extras <> rv:180 var
R8816:8816 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
R8818:8820 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
R8822:8824 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
R8850:8850 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
R8821:8821 Coq.Numbers.BinNums <> Z ind
binder 8817:8817 <> z:185
R8825:8833 Sail.Values <> ArithFact class
R8837:8841 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not
R8843:8847 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not
R8836:8836 riscv_extras <> i:182 var
R8842:8842 riscv_extras <> z:185 var
R8842:8842 riscv_extras <> z:185 var
R8848:8848 riscv_extras <> j:183 var
R8852:8852 riscv_extras <> e:181 var
R8857:8863 Sail.Prompt_monad <> returnm def
R8866:8873 Sail.Values <> build_ex def
R8875:8875 riscv_extras <> i:182 var
def 8890:8903 <> undefined_atom
binder 8906:8907 <> rv:186
binder 8909:8909 <> e:187
binder 8912:8912 <> i:188
R8916:8920 Sail.Prompt_monad <> monad ind
R8922:8923 riscv_extras <> rv:186 var
R8925:8925 Coq.Numbers.BinNums <> Z ind
R8927:8927 riscv_extras <> e:187 var
R8932:8938 Sail.Prompt_monad <> returnm def
R8940:8940 riscv_extras <> i:188 var
def 8954:8966 <> undefined_nat
binder 8969:8970 <> rv:189
binder 8972:8972 <> e:190
R8978:8981 Coq.Init.Datatypes <> unit ind
R8986:8990 Sail.Prompt_monad <> monad ind
R8992:8993 riscv_extras <> rv:189 var
R8995:8995 Coq.Numbers.BinNums <> Z ind
R8997:8997 riscv_extras <> e:190 var
R9002:9008 Sail.Prompt_monad <> returnm def
R9013:9014 Sail.Values <> ii def
def 9030:9033 <> skip
binder 9036:9037 <> rv:191
binder 9039:9039 <> e:192
R9045:9048 Coq.Init.Datatypes <> unit ind
R9053:9057 Sail.Prompt_monad <> monad ind
R9059:9060 riscv_extras <> rv:191 var
R9062:9065 Coq.Init.Datatypes <> unit ind
R9067:9067 riscv_extras <> e:192 var
R9072:9078 Sail.Prompt_monad <> returnm def
R9080:9081 Coq.Init.Datatypes <> tt constr
def 9132:9140 <> elf_entry
R9145:9148 Coq.Init.Datatypes <> unit ind
R9153:9153 Coq.Numbers.BinNums <> Z ind
def 9247:9256 <> print_bits
binder 9259:9259 <> n:193
binder 9262:9264 <> msg:194
R9272:9276 Sail.Values <> mword def
R9278:9278 riscv_extras <> n:193 var
binder 9267:9268 <> bs:195
R9284:9296 Sail.Values <> prerr_endline def
R9302:9306 Coq.Strings.String <> ::string_scope:x_'++'_x not
R9324:9324 Coq.Strings.String <> ::string_scope:x_'++'_x not
R9299:9301 riscv_extras <> msg:194 var
R9307:9320 Sail.Operators_mwords <> string_of_bits def
R9322:9323 riscv_extras <> bs:195 var
def 9378:9388 <> get_time_ns
R9393:9396 Coq.Init.Datatypes <> unit ind
R9401:9401 Coq.Numbers.BinNums <> Z ind
def 9548:9553 <> eq_bit
R9560:9563 Sail.Values <> bitU ind
binder 9556:9556 <> x:196
R9571:9574 Sail.Values <> bitU ind
binder 9567:9567 <> y:197
R9579:9582 Coq.Init.Datatypes <> bool ind
R9598:9598 riscv_extras <> y:197 var
R9595:9595 riscv_extras <> x:196 var
R9609:9610 Sail.Values <> B0 constr
R9613:9614 Sail.Values <> B0 constr
R9619:9622 Coq.Init.Datatypes <> true constr
R9628:9629 Sail.Values <> B1 constr
R9632:9633 Sail.Values <> B1 constr
R9638:9641 Coq.Init.Datatypes <> true constr
R9647:9648 Sail.Values <> BU constr
R9651:9652 Sail.Values <> BU constr
R9657:9660 Coq.Init.Datatypes <> true constr
R9673:9677 Coq.Init.Datatypes <> false constr
R9702:9708 Coq.ZArith.Zeuclid <> <> lib
def 9722:9734 <> euclid_modulo
R9743:9743 Coq.Numbers.BinNums <> Z ind
binder 9737:9737 <> m:200
binder 9739:9739 <> n:201
R9748:9756 Sail.Values <> ArithFact class
R9760:9763 Coq.ZArith.BinInt <> ::Z_scope:x_'>?'_x not
R9759:9759 riscv_extras <> n:201 var
binder 9748:9765 <> H:202
R9770:9770 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
R9772:9774 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
R9776:9778 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
R9806:9806 Coq.Init.Specif <> ::type_scope:'{'_x_':'_x_'&'_x_'}' not
R9775:9775 Coq.Numbers.BinNums <> Z ind
binder 9771:9771 <> z:203
R9779:9787 Sail.Values <> ArithFact class
R9791:9795 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not
R9797:9801 Sail.Values <> ::Z_scope:x_'<=?'_x_'<=?'_x not
R9796:9796 riscv_extras <> z:203 var
R9796:9796 riscv_extras <> z:203 var
R9803:9803 Coq.ZArith.BinInt <> ::Z_scope:x_'-'_x not
R9802:9802 riscv_extras <> n:201 var
R9833:9846 Coq.ZArith.Zeuclid ZEuclid modulo def
R9815:9820 Coq.Init.Specif <> existT constr
R9833:9846 Coq.ZArith.Zeuclid ZEuclid modulo def
R9815:9820 Coq.Init.Specif <> existT constr
R9939:9941 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9932:9936 Coq.ZArith.BinInt Z abs def
R9939:9941 Coq.Init.Logic <> ::type_scope:x_'='_x not
R9932:9936 Coq.ZArith.BinInt Z abs def
R9956:9963 Coq.ZArith.BinInt Z abs_eq thm
R9956:9963 Coq.ZArith.BinInt Z abs_eq thm
R9956:9963 Coq.ZArith.BinInt Z abs_eq thm
R9956:9963 Coq.ZArith.BinInt Z abs_eq thm
R10013:10034 Coq.ZArith.Zeuclid ZEuclid mod_always_pos thm
R10013:10034 Coq.ZArith.Zeuclid ZEuclid mod_always_pos thm
def 10107:10115 <> mults_vec
binder 10118:10118 <> n:204
R10126:10130 Sail.Values <> mword def
R10132:10132 riscv_extras <> n:204 var
binder 10122:10122 <> l:205
R10140:10144 Sail.Values <> mword def
R10146:10146 riscv_extras <> n:204 var
binder 10136:10136 <> r:206
R10151:10155 Sail.Values <> mword def
R10159:10161 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R10162:10162 riscv_extras <> n:204 var
R10168:10176 Sail.Operators_mwords <> mults_vec def
R10180:10180 riscv_extras <> r:206 var
R10178:10178 riscv_extras <> l:205 var
def 10194:10201 <> mult_vec
binder 10204:10204 <> n:207
R10212:10216 Sail.Values <> mword def
R10218:10218 riscv_extras <> n:207 var
binder 10208:10208 <> l:208
R10226:10230 Sail.Values <> mword def
R10232:10232 riscv_extras <> n:207 var
binder 10222:10222 <> r:209
R10237:10241 Sail.Values <> mword def
R10245:10247 Coq.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R10248:10248 riscv_extras <> n:207 var
R10254:10261 Sail.Operators_mwords <> mult_vec def
R10265:10265 riscv_extras <> r:209 var
R10263:10263 riscv_extras <> l:208 var
def 10281:10293 <> print_endline
R10298:10303 Coq.Strings.String <> string ind
R10308:10311 Coq.Init.Datatypes <> unit ind
R10316:10317 Coq.Init.Datatypes <> tt constr
def 10331:10343 <> prerr_endline
R10348:10353 Coq.Strings.String <> string ind
R10358:10361 Coq.Init.Datatypes <> unit ind
R10366:10367 Coq.Init.Datatypes <> tt constr
def 10381:10392 <> prerr_string
R10397:10402 Coq.Strings.String <> string ind
R10407:10410 Coq.Init.Datatypes <> unit ind
R10415:10416 Coq.Init.Datatypes <> tt constr
def 10430:10436 <> putchar
binder 10439:10439 <> T:210
R10445:10445 riscv_extras <> T:210 var
R10450:10453 Coq.Init.Datatypes <> unit ind
R10458:10459 Coq.Init.Datatypes <> tt constr
R10470:10482 Coq.Numbers.DecimalString <> <> lib
def 10496:10508 <> string_of_int
binder 10510:10510 <> z:211
R10515:10549 Coq.Numbers.DecimalString NilZero string_of_int def
R10552:10559 Coq.ZArith.BinInt Z to_int def
R10561:10561 riscv_extras <> z:211 var
ax 10572:10595 <> sys_enable_writable_misa
R10603:10606 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10599:10602 Coq.Init.Datatypes <> unit ind
R10607:10610 Coq.Init.Datatypes <> bool ind
ax 10619:10632 <> sys_enable_rvc
R10640:10643 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10636:10639 Coq.Init.Datatypes <> unit ind
R10644:10647 Coq.Init.Datatypes <> bool ind
ax 10656:10671 <> sys_enable_fdext
R10679:10682 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10675:10678 Coq.Init.Datatypes <> unit ind
R10683:10686 Coq.Init.Datatypes <> bool ind
ax 10695:10709 <> sys_enable_next
R10717:10720 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10713:10716 Coq.Init.Datatypes <> unit ind
R10721:10724 Coq.Init.Datatypes <> bool ind
prf 10868:10888 <> n_leading_spaces_fact
binder 10891:10894 <> w__0:216
R10910:10913 Coq.Init.Logic <> ::type_scope:x_'->'_x not
R10905:10908 Coq.ZArith.BinInt <> ::Z_scope:x_'>='_x not
R10901:10904 riscv_extras <> w__0:216 var
R10914:10920 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R10933:10934 Coq.Init.Logic <> ::type_scope:'exists'_x_'..'_x_','_x not
R10932:10932 Coq.Numbers.BinNums <> Z ind
binder 10921:10928 <> ex17629_:217
R10958:10961 Coq.Init.Logic <> ::type_scope:x_'/\'_x not
R10943:10945 Coq.Init.Logic <> ::type_scope:x_'='_x not
R10936:10938 Coq.ZArith.BinInt <> ::Z_scope:x_'+'_x not
R10939:10942 riscv_extras <> w__0:216 var
R10947:10949 Coq.ZArith.BinInt <> ::Z_scope:x_'+'_x not
R10950:10957 riscv_extras <> ex17629_:217 var
R10963:10966 Coq.ZArith.BinInt <> ::Z_scope:x_'<='_x not
R10967:10974 riscv_extras <> ex17629_:217 var