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