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