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