1(* ------------------------------------------------------------------------ *) 2(* ARM Machine Code Semantics *) 3(* ========================== *) 4(* Basic types and operations for the ARM model *) 5(* ------------------------------------------------------------------------ *) 6 7open HolKernel boolLib bossLib Parse; 8open arithmeticTheory bitTheory wordsTheory wordsLib integer_wordTheory; 9 10val _ = new_theory "arm_coretypes"; 11 12val _ = numLib.prefer_num(); 13val _ = wordsLib.prefer_word(); 14 15(* ------------------------------------------------------------------------ *) 16 17val _ = Hol_datatype `RName = 18 RName_0usr | RName_1usr | RName_2usr | RName_3usr 19 | RName_4usr | RName_5usr | RName_6usr | RName_7usr 20 | RName_8usr | RName_8fiq | RName_9usr | RName_9fiq 21 | RName_10usr | RName_10fiq | RName_11usr | RName_11fiq 22 | RName_12usr | RName_12fiq 23 | RName_SPusr | RName_SPfiq | RName_SPirq | RName_SPsvc 24 | RName_SPabt | RName_SPund | RName_SPmon 25 | RName_LRusr | RName_LRfiq | RName_LRirq | RName_LRsvc 26 | RName_LRabt | RName_LRund | RName_LRmon 27 | RName_PC`; 28 29val _ = Hol_datatype `PSRName = 30 CPSR | SPSR_fiq | SPSR_irq | SPSR_svc | SPSR_mon | SPSR_abt | SPSR_und`; 31 32val _ = Hol_datatype `HWInterrupt = 33 NoInterrupt | HW_Reset | HW_Irq | HW_Fiq`; 34 35val _ = Hol_datatype `ARMpsr = 36 <| N : bool; Z : bool; C : bool; V : bool; Q : bool; 37 IT : word8; J : bool; Reserved : word4; GE : word4; 38 E : bool; A : bool; I : bool; F : bool; T : bool; M : word5 |>`; 39 40val _ = Hol_datatype `CP15sctlr = 41 <| IE : bool; TE : bool; AFE : bool; TRE : bool; NMFI : bool; 42 EE : bool; VE : bool; U : bool; FI : bool; DZ : bool; 43 HA : bool; RR : bool; V : bool; I : bool; Z : bool; 44 SW : bool; B : bool; C : bool; A : bool; M : bool |>`; 45 46val _ = Hol_datatype `CP15scr = 47 <| nET : bool; AW : bool; FW : bool; EA : bool; 48 FIQ : bool; IRQ : bool; NS : bool |>`; 49 50val _ = Hol_datatype `CP15nsacr = 51 <| RFR : bool; NSASEDIS : bool; NSD32DIS : bool; cp : 14 word |>`; 52 53val _ = Hol_datatype `CP15reg = 54 <| SCTLR : CP15sctlr; 55 SCR : CP15scr; 56 NSACR : CP15nsacr; 57 VBAR : word32; 58 MVBAR : word32 |>`; 59 60val _ = Hol_datatype `CP14reg = 61 <| TEEHBR : word32 |>`; 62 63val _ = Hol_datatype `ARMarch = 64 ARMv4 | ARMv4T 65 | ARMv5T | ARMv5TE 66 | ARMv6 | ARMv6K | ARMv6T2 67 | ARMv7_A | ARMv7_R`; 68 69val _ = Hol_datatype `ARMextensions = 70 Extension_ThumbEE | Extension_VFP | Extension_AdvanvedSIMD 71 | Extension_Security | Extension_Jazelle | Extension_Multiprocessing`; 72 73val _ = Hol_datatype `ARMinfo = 74 <| arch : ARMarch; 75 extensions : ARMextensions set; 76 unaligned_support : bool |>`; 77 78val _ = Hol_datatype `SRType = 79 SRType_LSL 80 | SRType_LSR 81 | SRType_ASR 82 | SRType_ROR 83 | SRType_RRX`; 84 85val _ = Hol_datatype `InstrSet = 86 InstrSet_ARM | InstrSet_Thumb | InstrSet_Jazelle | InstrSet_ThumbEE`; 87 88val _ = Hol_datatype `Encoding = 89 Encoding_ARM | Encoding_Thumb | Encoding_Thumb2 | Encoding_ThumbEE`; 90 91val _ = Hol_datatype `MemType = 92 MemType_Normal | MemType_Device | MemType_StronglyOrdered`; 93 94val _ = Hol_datatype `MemoryAttributes = 95 <| type : MemType; 96 innerattrs : word2; 97 outerattrs : word2; 98 shareable : bool; 99 outershareable : bool |>`; 100 101(* 102val _ = Hol_datatype `FullAddress = 103 <| physicaladdress : word32; 104 physicaladdressext : word8; 105 NS : bool (* F = Secure; T = Non-secure *) |>`; 106*) 107 108(* For now, assume that a full address is word32 *) 109val _ = type_abbrev("FullAddress", ``:word32``); 110 111val _ = Hol_datatype `AddressDescriptor = 112 <| memattrs : MemoryAttributes; 113 paddress : FullAddress |>`; 114 115val _ = Hol_datatype `MBReqDomain = 116 MBReqDomain_FullSystem 117 | MBReqDomain_OuterShareable 118 | MBReqDomain_InnerShareable 119 | MBReqDomain_Nonshareable`; 120 121val _ = Hol_datatype `MBReqTypes = MBReqTypes_All | MBReqTypes_Writes`; 122 123val _ = Hol_datatype `memory_access = 124 MEM_READ of FullAddress | MEM_WRITE of FullAddress => word8`; 125 126(* Coprocessors *) 127 128val _ = type_abbrev("cpid", ``:word4``); 129 130val _ = type_abbrev ("proc", ``:num``); 131 132val _ = Hol_datatype `iiid = <| proc : num |>`; 133 134val _ = disable_tyabbrev_printing "proc"; 135 136(* ------------------------------------------------------------------------ *) 137 138val _ = overload_on("UInt", ``\w. int_of_num (w2n w)``); 139val _ = overload_on("SInt", ``w2i``); 140 141val align_def = zDefine 142 `align (w : 'a word, n : num) : 'a word = n2w (n * (w2n w DIV n))`; 143 144val aligned_def = zDefine` 145 aligned (w : 'a word, n : num) = (w = align(w,n))`; 146 147val count_leading_zeroes_def = Define` 148 count_leading_zeroes (w : 'a word) = 149 if w = 0w then 150 dimindex(:'a) 151 else 152 dimindex(:'a) - 1 - LOG2 (w2n w)`; 153 154val lowest_set_bit_def = Define` 155 lowest_set_bit (w : 'a word) = 156 if w = 0w then 157 dimindex(:'a) 158 else 159 LEAST i. w ' i`; 160 161val _ = wordsLib.guess_lengths(); 162 163val zero_extend32_def = Define` 164 (zero_extend32 [b:word8] : word32 = w2w b) /\ 165 (zero_extend32 [b1; b2] = w2w (b2 @@ b1))`; 166 167val sign_extend32_def = Define` 168 (sign_extend32 [b:word8] : word32 = sw2sw b) /\ 169 (sign_extend32 [b1; b2] = sw2sw (b2 @@ b1))`; 170 171val word_defs = TotalDefn.multiDefine` 172 (word16 ([b1; b2] : word8 list) = b2 @@ b1) /\ 173 (word32 ([b1; b2; b3; b4] : word8 list) = b4 @@ b3 @@ b2 @@ b1) /\ 174 (word64 ([b1; b2; b3; b4; b5; b6; b7; b8] : word8 list) = 175 word32 [b5; b6; b7; b8] @@ word32 [b1; b2; b3; b4])`; 176 177val bytes_def = Define` 178 (bytes (w, 4) = [(7 >< 0) w; (15 >< 8) w; (23 >< 16) w; (31 >< 24) w]) /\ 179 (bytes (w, 2) = [(7 >< 0) w; (15 >< 8) w]) /\ 180 (bytes (w, 1) = [w2w (w:word32)] : word8 list)`; 181 182val i2bits_def = Define `i2bits (i,N) = n2w (Num (i % 2 ** N))`; 183 184val signed_sat_q_def = Define` 185 signed_sat_q (i:int, N:num) : ('a word # bool) = 186 if dimindex(:'a) < N then 187 ARB 188 else 189 if i > 2 ** (N - 1) - 1 then 190 (i2bits (2 ** (N - 1) - 1, N), T) 191 else if i < ~(2 ** (N - 1)) then 192 (i2bits (~(2 ** (N - 1)), N), T) 193 else 194 (i2bits (i, N), F)`; 195 196val unsigned_sat_q_def = Define` 197 unsigned_sat_q (i:int, N:num) : ('a word # bool) = 198 if dimindex(:'a) < N then 199 ARB 200 else 201 if i > 2 ** N - 1 then 202 (n2w (2 ** N - 1), T) 203 else if i < 0 then 204 (0w, T) 205 else 206 (n2w (Num i), F)`; 207 208val signed_sat_def = Define `signed_sat = FST o signed_sat_q`; 209val unsigned_sat_def = Define `unsigned_sat = FST o unsigned_sat_q`; 210 211val LSL_C_def = zDefine` 212 LSL_C (x: 'a word, shift:num) = 213 if shift = 0 then 214 ARB 215 else 216 let extended_x = w2n x * (2 ** shift) in 217 (x << shift, BIT (dimindex(:'a)) extended_x)`; 218 219val LSR_C_def = zDefine` 220 LSR_C (x: 'a word, shift:num) = 221 if shift = 0 then 222 ARB 223 else 224 (x >>> shift, BIT (shift - 1) (w2n x))`; 225 226val ASR_C_def = zDefine` 227 ASR_C (x: 'a word, shift:num) = 228 if shift = 0 then 229 ARB 230 else 231 (x >> shift, x ' (MIN (dimindex(:'a) - 1) (shift - 1)))`; 232 233val ROR_C_def = zDefine` 234 ROR_C (x: 'a word, shift:num) = 235 if shift = 0 then 236 ARB 237 else let result = x #>> shift in 238 (result, result ' (dimindex(:'a) - 1))`; 239 240val RRX_C_def = Define` 241 RRX_C (x: 'a word, carry_in:bool) = 242 let (carry_out,result) = word_rrx(carry_in,x) in 243 (result,carry_out)`; 244 245val LSL_def = Define `LSL (x: 'a word, shift:num) = x << shift`; 246val LSR_def = Define `LSR (x: 'a word, shift:num) = x >>> shift`; 247val ASR_def = Define `ASR (x: 'a word, shift:num) = x >> shift`; 248val ROR_def = Define `ROR (x: 'a word, shift:num) = x #>> shift`; 249 250val RRX_def = Define` 251 RRX (x: 'a word, carry_in:bool) = SND (word_rrx (carry_in,x))`; 252 253(* ------------------------------------------------------------------------ *) 254 255val ITAdvance_def = zDefine` 256 ITAdvance (IT:word8) = 257 if (2 >< 0) IT = 0b000w:word3 then 258 0b00000000w 259 else 260 ((7 '' 5) IT || w2w (((4 >< 0) IT) : word5 << 1))`; 261 262val ITAdvance_n2w = save_thm("ITAdvance_n2w", 263 ITAdvance_def 264 |> SIMP_RULE (srw_ss()++wordsLib.WORD_EXTRACT_ss) [] 265 |> Q.SPEC `n2w n` 266 |> RIGHT_CONV_RULE EVAL 267 |> GEN_ALL); 268 269val decode_psr_def = Define` 270 decode_psr (psr:word32) = 271 <| N := psr ' 31; 272 Z := psr ' 30; 273 C := psr ' 29; 274 V := psr ' 28; 275 Q := psr ' 27; 276 IT := (( 15 >< 10 ) psr : word6) @@ (( 26 >< 25 ) psr : word2); 277 J := psr ' 24; 278 Reserved := ( 23 >< 20 ) psr; 279 GE := ( 19 >< 16 ) psr; 280 E := psr ' 9; 281 A := psr ' 8; 282 I := psr ' 7; 283 F := psr ' 6; 284 T := psr ' 5; 285 M := ( 4 >< 0 ) psr |>`; 286 287val encode_psr_def = Define` 288 encode_psr (psr:ARMpsr) : word32 = 289 FCP x. 290 if x < 5 then psr.M ' x else 291 if x = 5 then psr.T else 292 if x = 6 then psr.F else 293 if x = 7 then psr.I else 294 if x = 8 then psr.A else 295 if x = 9 then psr.E else 296 if x < 16 then psr.IT ' (x - 8) else 297 if x < 20 then psr.GE ' (x - 16) else 298 if x < 24 then psr.Reserved ' (x - 20) else 299 if x = 24 then psr.J else 300 if x < 27 then psr.IT ' (x - 25) else 301 if x = 27 then psr.Q else 302 if x = 28 then psr.V else 303 if x = 29 then psr.C else 304 if x = 30 then psr.Z else 305 (* x = 31 *) psr.N`; 306 307val version_number_def = Define` 308 (version_number ARMv4 = 4) /\ 309 (version_number ARMv4T = 4) /\ 310 (version_number ARMv5T = 5) /\ 311 (version_number ARMv5TE = 5) /\ 312 (version_number ARMv6 = 6) /\ 313 (version_number ARMv6K = 6) /\ 314 (version_number ARMv6T2 = 6) /\ 315 (version_number ARMv7_A = 7) /\ 316 (version_number ARMv7_R = 7)`; 317 318val thumb2_support_def = Define` 319 thumb2_support = {a | (a = ARMv6T2) \/ version_number a >= 7}`; 320 321val security_support_def = Define` 322 security_support = {(a,e) | ((a = ARMv6K) \/ (a = ARMv7_A)) /\ 323 Extension_Security IN e}`; 324 325val thumbee_support_def = Define` 326 thumbee_support = {(a,e) | (a = ARMv7_A) \/ 327 (a = ARMv7_R) /\ Extension_ThumbEE IN e}`; 328 329val jazelle_support_def = Define` 330 jazelle_support = {(a,e) | version_number a > 6 \/ 331 (a = ARMv5TE) /\ Extension_Jazelle IN e}`; 332 333(* ------------------------------------------------------------------------ *) 334 335infix \\ << 336 337val op \\ = op THEN; 338val op << = op THENL; 339 340val SUC_RULE = CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV; 341 342val rule = 343 SUC_RULE o GEN_ALL o 344 SIMP_RULE arith_ss 345 [GSYM bitTheory.TIMES_2EXP_def, MOD_2EXP_DIMINDEX, w2n_n2w] o 346 Q.SPECL [`n2w n`,`SUC sh`]; 347 348val NUMERIC_LSL_C = save_thm("NUMERIC_LSL_C", rule LSL_C_def); 349val NUMERIC_LSR_C = save_thm("NUMERIC_LSR_C", rule LSR_C_def); 350val NUMERIC_ASR_C = save_thm("NUMERIC_ASR_C", rule ASR_C_def); 351val NUMERIC_ROR_C = save_thm("NUMERIC_ROR_C", rule ROR_C_def); 352 353local 354 val rule = GEN_ALL o SIMP_RULE (srw_ss()) [] o Q.SPEC `n2w a` 355in 356 val align_n2w = save_thm("align_n2w", rule align_def) 357 val aligned_n2w = save_thm("aligned_n2w", rule aligned_def) 358end; 359 360val align_slice = Q.store_thm("align_slice", 361 `!n a:'a word. align (a,2 ** n) = (dimindex(:'a) - 1 '' n) a`, 362 STRIP_TAC \\ Cases 363 \\ SRW_TAC [ARITH_ss] [align_def, word_slice_n2w, SLICE_THM, BITS_THM2, 364 DECIDE ``0 < n ==> (SUC (n - 1) = n)``] 365 \\ FULL_SIMP_TAC (srw_ss()) [dimword_def]); 366 367val MIN_LEM = Q.prove(`!a b. MIN a (MIN a b) = MIN a b`, SRW_TAC [] [MIN_DEF]); 368 369val align_id = Q.store_thm("align_id", 370 `!n a. align (align (a,2 ** n),2 ** n) = align (a,2 ** n)`, 371 SRW_TAC [ARITH_ss,wordsLib.WORD_EXTRACT_ss] 372 [DIMINDEX_GT_0,MIN_LEM,align_slice] 373 \\ SRW_TAC [ARITH_ss] [MIN_DEF] 374 \\ `n = 0` by DECIDE_TAC \\ SRW_TAC [] []); 375 376val align_id_248 = save_thm("align_id_248", 377 numLib.REDUCE_RULE 378 (Drule.LIST_CONJ (List.map (fn t => Q.SPEC t align_id) [`1`,`2`,`3`]))); 379 380val word_index = Q.prove( 381 `!i n. i < dimindex (:'a) ==> ((n2w n : 'a word) ' i = BIT i n)`, 382 ONCE_REWRITE_TAC [word_index_n2w] \\ SRW_TAC [] []); 383 384val BIT_EXISTS = METIS_PROVE [BIT_LOG2] ``!n. ~(n = 0) ==> ?b. BIT b n``; 385 386val LEAST_BIT_INTRO = 387 (SIMP_RULE (srw_ss()) [] o Q.SPEC `\i. BIT i n`) whileTheory.LEAST_INTRO; 388 389val LOWEST_SET_BIT_ELIM = 390 (SIMP_RULE (srw_ss()) [AND_IMP_INTRO] o 391 SIMP_RULE (srw_ss()) [BIT_EXISTS] o Q.DISCH `~(n = 0)` o 392 Q.SPECL [`\x. x < dimindex (:'a)`,`\i. BIT i n`]) whileTheory.LEAST_ELIM; 393 394val LOWEST_SET_BIT_LESS_LEAST = 395 (SIMP_RULE (srw_ss()) [] o Q.SPEC `\i. BIT i n`) whileTheory.LESS_LEAST; 396 397val LOWEST_SET_BIT_LT_DIMINDEX = Q.prove( 398 `!n. ~(n = 0) /\ n < dimword(:'a) ==> (LEAST i. BIT i n) < dimindex(:'a)`, 399 SRW_TAC [] [dimword_def] 400 \\ MATCH_MP_TAC LOWEST_SET_BIT_ELIM 401 \\ SRW_TAC [] [] 402 \\ SPOSE_NOT_THEN STRIP_ASSUME_TAC 403 \\ FULL_SIMP_TAC std_ss [NOT_LESS] 404 \\ IMP_RES_TAC TWOEXP_MONO2 405 \\ `n < 2 ** n'` by DECIDE_TAC 406 \\ METIS_TAC [NOT_BIT_GT_TWOEXP]); 407 408val lowest_set_bit_compute = Q.store_thm("lowest_set_bit_compute", 409 `!w. lowest_set_bit (w:'a word) = 410 if w = 0w then 411 dimindex(:'a) 412 else 413 LOWEST_SET_BIT (w2n w)`, 414 Cases \\ SRW_TAC [] [lowest_set_bit_def, LOWEST_SET_BIT_def] 415 \\ MATCH_MP_TAC LEAST_THM 416 \\ SRW_TAC [] [] 417 \\ IMP_RES_TAC LOWEST_SET_BIT_LT_DIMINDEX 418 \\ FULL_SIMP_TAC (srw_ss()++ARITH_ss) 419 [word_index, LOWEST_SET_BIT_LESS_LEAST] 420 \\ MATCH_MP_TAC LEAST_BIT_INTRO 421 \\ METIS_TAC [BIT_EXISTS]); 422 423val NOT_IN_EMPTY_SPECIFICATION = save_thm("NOT_IN_EMPTY_SPECIFICATION", 424 (GSYM o SIMP_RULE (srw_ss()) [] o Q.SPEC `{}`) pred_setTheory.SPECIFICATION); 425 426(* ------------------------------------------------------------------------ *) 427 428val encode_psr_bit = Q.store_thm("encode_psr_bit", 429 `(!cpsr. encode_psr cpsr ' 31 = cpsr.N) /\ 430 (!cpsr. encode_psr cpsr ' 30 = cpsr.Z) /\ 431 (!cpsr. encode_psr cpsr ' 29 = cpsr.C) /\ 432 (!cpsr. encode_psr cpsr ' 28 = cpsr.V) /\ 433 (!cpsr. encode_psr cpsr ' 27 = cpsr.Q) /\ 434 (!cpsr. encode_psr cpsr ' 26 = cpsr.IT ' 1) /\ 435 (!cpsr. encode_psr cpsr ' 25 = cpsr.IT ' 0) /\ 436 (!cpsr. encode_psr cpsr ' 24 = cpsr.J) /\ 437 (!cpsr. encode_psr cpsr ' 23 = cpsr.Reserved ' 3) /\ 438 (!cpsr. encode_psr cpsr ' 22 = cpsr.Reserved ' 2) /\ 439 (!cpsr. encode_psr cpsr ' 21 = cpsr.Reserved ' 1) /\ 440 (!cpsr. encode_psr cpsr ' 20 = cpsr.Reserved ' 0) /\ 441 (!cpsr. encode_psr cpsr ' 19 = cpsr.GE ' 3) /\ 442 (!cpsr. encode_psr cpsr ' 18 = cpsr.GE ' 2) /\ 443 (!cpsr. encode_psr cpsr ' 17 = cpsr.GE ' 1) /\ 444 (!cpsr. encode_psr cpsr ' 16 = cpsr.GE ' 0) /\ 445 (!cpsr. encode_psr cpsr ' 15 = cpsr.IT ' 7) /\ 446 (!cpsr. encode_psr cpsr ' 14 = cpsr.IT ' 6) /\ 447 (!cpsr. encode_psr cpsr ' 13 = cpsr.IT ' 5) /\ 448 (!cpsr. encode_psr cpsr ' 12 = cpsr.IT ' 4) /\ 449 (!cpsr. encode_psr cpsr ' 11 = cpsr.IT ' 3) /\ 450 (!cpsr. encode_psr cpsr ' 10 = cpsr.IT ' 2) /\ 451 (!cpsr. encode_psr cpsr ' 9 = cpsr.E) /\ 452 (!cpsr. encode_psr cpsr ' 8 = cpsr.A) /\ 453 (!cpsr. encode_psr cpsr ' 7 = cpsr.I) /\ 454 (!cpsr. encode_psr cpsr ' 6 = cpsr.F) /\ 455 (!cpsr. encode_psr cpsr ' 5 = cpsr.T) /\ 456 (!cpsr. encode_psr cpsr ' 4 = cpsr.M ' 4) /\ 457 (!cpsr. encode_psr cpsr ' 3 = cpsr.M ' 3) /\ 458 (!cpsr. encode_psr cpsr ' 2 = cpsr.M ' 2) /\ 459 (!cpsr. encode_psr cpsr ' 1 = cpsr.M ' 1) /\ 460 (!cpsr. encode_psr cpsr ' 0 = cpsr.M ' 0)`, 461 SRW_TAC [fcpLib.FCP_ss] [encode_psr_def]); 462 463val extract_modify = 464 (GEN_ALL o SIMP_CONV (arith_ss++fcpLib.FCP_ss++boolSimps.CONJ_ss) 465 [word_extract_def, word_bits_def, w2w]) 466 ``(h >< l) ($FCP P) = value``; 467 468val encode_psr_bits = Q.store_thm("encode_psr_bits", 469 `(!cpsr. (26 >< 25) (encode_psr cpsr) = (1 >< 0) cpsr.IT) /\ 470 (!cpsr. (23 >< 20) (encode_psr cpsr) = cpsr.Reserved) /\ 471 (!cpsr. (19 >< 16) (encode_psr cpsr) = cpsr.GE) /\ 472 (!cpsr. (15 >< 10) (encode_psr cpsr) = (7 >< 2) cpsr.IT) /\ 473 (!cpsr. ( 4 >< 0 ) (encode_psr cpsr) = cpsr.M)`, 474 REPEAT STRIP_TAC \\ REWRITE_TAC [encode_psr_def, extract_modify] 475 \\ SRW_TAC [ARITH_ss,fcpLib.FCP_ss] [word_extract_def, word_bits_def, w2w]); 476 477(* ------------------------------------------------------------------------ *) 478 479val _ = computeLib.add_persistent_funs 480 ["pair.UNCURRY", 481 "pair.LEX_DEF", 482 "pred_set.IN_CROSS", 483 "pred_set.IN_DELETE", 484 "words.BIT_UPDATE", 485 "NOT_IN_EMPTY_SPECIFICATION", 486 "NUMERIC_LSL_C", 487 "NUMERIC_LSR_C", 488 "NUMERIC_ASR_C", 489 "NUMERIC_ROR_C", 490 "align_n2w", 491 "aligned_n2w", 492 "align_id_248", 493 "lowest_set_bit_compute", 494 "ITAdvance_n2w", 495 "RName_EQ_RName", 496 "RName2num_thm", 497 "num2RName_thm", 498 "PSRName_EQ_PSRName", 499 "PSRName2num_thm", 500 "num2PSRName_thm", 501 "ARMarch_EQ_ARMarch", 502 "ARMarch2num_thm", 503 "num2ARMarch_thm", 504 "SRType_EQ_SRType", 505 "SRType2num_thm", 506 "num2SRType_thm", 507 "InstrSet_EQ_InstrSet", 508 "InstrSet2num_thm", 509 "num2InstrSet_thm", 510 "Encoding_EQ_Encoding", 511 "Encoding2num_thm", 512 "num2Encoding_thm"]; 513 514(* ------------------------------------------------------------------------ *) 515 516val _ = export_theory (); 517