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