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