1(* For interactive work
2  quietdec := true;
3  app load ["wordsLib"];
4  open pairTheory wordsTheory listTheory;
5  quietdec := false;
6*)
7
8open HolKernel Parse boolLib bossLib pairTheory wordsTheory;
9
10val _ = new_theory "MARS_Data";
11
12(*---------------------------------------------------------------------------*)
13(* Type Definitions                                                          *)
14(*---------------------------------------------------------------------------*)
15
16val _ = type_abbrev("block", ``:word32 # word32 # word32 # word32``);
17val _ = type_abbrev("key",   ``:word32 # word32 # word32 # word32``);
18
19val _ = type_abbrev("keysched",
20     ``:word32 # word32 # word32 # word32 # word32 # word32 # word32 #
21        word32 # word32 # word32 # word32 # word32 # word32 # word32 #
22        word32 # word32 # word32 # word32 # word32 # word32 # word32 #
23        word32 # word32 # word32 # word32 # word32 # word32 # word32 #
24        word32 # word32 # word32 # word32 # word32 # word32 # word32 #
25        word32 # word32 # word32 # word32 # word32``);
26
27(*---------------------------------------------------------------------------*)
28(* Case analysis on a block, a key schedule                                  *)
29(*---------------------------------------------------------------------------*)
30
31val FORALL_BLOCK = Q.store_thm
32  ("FORALL_BLOCK",
33    `(!b:block. P b) = !v0 v1 v2 v3. P (v0,v1,v2,v3)`,
34    SIMP_TAC std_ss [FORALL_PROD]);
35
36val FORALL_KEYSCHEDS = Q.prove(
37 `(!x:keysched. P x) =
38   !k0 k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 k15 k16 k17 k18
39     k19 k20 k21 k22 k23 k24 k25 k26 k27 k28 k29 k30 k31 k32 k33 k34
40     k35 k36 k37 k38 k39.
41   P(k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,
42    k19,k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,
43    k35,k36,k37,k38,k39)`,
44  SIMP_TAC std_ss [FORALL_PROD]);
45
46(* --------------------------------------------------------------------------*)
47(* Functions for processing keys                                             *)
48(*---------------------------------------------------------------------------*)
49
50val ROTKEYS_def = Define`
51  ROTKEYS
52    (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,
53     k19,k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,k35,
54     k36,k37,k38,k39) =
55   (k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,k19,k20,
56    k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,k35,k36,k37,
57    k38,k39,k0,k1) : keysched`;
58
59val ROTKEYS18_def = Define`
60  ROTKEYS18
61    (k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,k19,k20,
62     k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,k35,k36,k37,
63     k38,k39,k0,k1) =
64   (k36,k37,k38,k39,k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,
65    k16,k17,k18,k19,k20,k21,k22, k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,
66    k33,k34,k35) : keysched`;
67
68val INVROTKEYS_def = Define`
69  INVROTKEYS
70     (k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,k19,k20,
71      k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,k35,k36,k37,
72      k38,k39,k0,k1) =
73   (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,k19,
74    k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,k35,k36,
75    k37,k38,k39) : keysched`;
76
77val ROTKEYS_Inversion = Q.store_thm
78  ("ROTKEYS_Inversion",
79  `!k:keysched. (INVROTKEYS(ROTKEYS(k)) = k) /\
80                (ROTKEYS(INVROTKEYS(k)) = k)`,
81  SIMP_TAC std_ss [FORALL_KEYSCHEDS] THEN
82  REWRITE_TAC [ROTKEYS_def,INVROTKEYS_def]);
83
84val GETKEYS_def = Define`
85  GETKEYS
86    ((k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,k16,k17,k18,
87      k19,k20,k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,k31,k32,k33,k34,
88      k35,k36,k37,k38,k39):keysched) =
89    (k0,k1)`;
90
91val LIST_TO_KEYS_def = Define`
92   (LIST_TO_KEYS [] acc = acc:keysched) /\
93   (LIST_TO_KEYS (h::t) (k0,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,
94                         k11,k12,k13,k14,k15,k16,k17,k18,k19,k20,
95                         k21,k22,k23,k24,k25,k26,k27,k28,k29,k30,
96                         k31,k32,k33,k34,k35,k36,k37,k38,k39) =
97      LIST_TO_KEYS t (h,k1,k2,k3,k4,k5,k6,k7,k8,k9,k10,k11,k12,k13,k14,k15,
98                      k16,k17,k18,k19,k20,k21,k22,k23,k24,k25,k26,k27,k28,
99                      k29,k30,k31,k32,k33,k34,k35,k36,k37,k38,k39))`;
100
101val DUMMY_KEYS_def = Define`
102   DUMMY_KEYS =
103      (0w,0w,0w,0w,0w,0w,0w,0w,0w,0w,
104       0w,0w,0w,0w,0w,0w,0w,0w,0w,0w,
105       0w,0w,0w,0w,0w,0w,0w,0w,0w,0w,
106       0w,0w,0w,0w,0w,0w,0w,0w,0w,0w) : keysched`;
107
108val _ = export_theory();
109