diff options
Diffstat (limited to 'handwritten_support/riscv_extras.glob')
| -rw-r--r-- | handwritten_support/riscv_extras.glob | 875 |
1 files changed, 875 insertions, 0 deletions
diff --git a/handwritten_support/riscv_extras.glob b/handwritten_support/riscv_extras.glob new file mode 100644 index 0000000..980acb4 --- /dev/null +++ b/handwritten_support/riscv_extras.glob @@ -0,0 +1,875 @@ +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 |