1open HolKernel Parse boolLib bossLib listTheory rich_listTheory bitTheory
2     markerTheory pairTheory arithmeticTheory wordsTheory wordsLib
3     Serpent_Bitslice_UtilityTheory Serpent_Bitslice_SBoxTheory;
4
5val _ = new_theory "Serpent_Bitslice_KeySchedule";
6
7(*number of rounds*)
8val R_def = Define `R = 32`;
9
10(* PHI: Constant used in the key schedule *)
11
12val PHI_def = Define `PHI = 0x9e3779b9w : word32`;
13
14val short2longKey_def = Define
15`short2longKey k kl = let nw256 = n2w (k MOD  (2**kl)) in
16  nw256 || (1w<<kl) : word256`;
17
18(*used in making preKey*)
19val (makeSubKeyBitSlice_def,makeSubKeyBitSlice_termi) = Defn.tstore_defn(
20Hol_defn "makeSubKeyBitSlice"
21`makeSubKeyBitSlice (w_1::w_2::w_3::w_4::w_5::w_6::w_7::w_8::t) i
22 = let nl =((w_1 ?? w_3 ??  w_5 ?? w_8 ?? PHI ?? (n2w:num->word32) (131-i)) #>>
23            (32-11))
24       ::(w_1::w_2::w_3::w_4::w_5::w_6::w_7::w_8::t)
25   in
26   if i = 0
27      then nl
28      else makeSubKeyBitSlice nl (i-1)`,
29 WF_REL_TAC `measure SND`);
30
31
32(*reversed preKey*)
33val makeRevPreKey_def = Define
34`makeRevPreKey longKey = let keySlices = word256to32l longKey in
35 myBUTLASTN 8 (makeSubKeyBitSlice keySlices 131)`;
36
37
38val revPreKey2SubKey_def = Define
39`revPreKey2SubKey revPreKey
40 = let w = REVERSE revPreKey
41  in
42  RND03 (EL 0 w, EL 1 w, EL 2 w, EL 3 w)::
43  RND02(EL 4 w, EL 5 w, EL 6 w, EL 7 w)::
44  RND01(EL  8 w, EL  9 w, EL 10 w, EL 11 w)::
45  RND00(EL 12 w, EL 13 w, EL 14 w, EL 15 w)::
46  RND31(EL 16 w, EL 17 w, EL 18 w, EL 19 w)::
47  RND30(EL 20 w, EL 21 w, EL 22 w, EL 23 w)::
48  RND29(EL 24 w, EL 25 w, EL 26 w, EL 27 w)::
49  RND28(EL 28 w, EL 29 w, EL 30 w, EL 31 w)::
50  RND27(EL 32 w, EL 33 w, EL 34 w, EL 35 w)::
51  RND26(EL 36 w, EL 37 w, EL 38 w, EL 39 w)::
52  RND25(EL 40 w, EL 41 w, EL 42 w, EL 43 w)::
53  RND24(EL 44 w, EL 45 w, EL 46 w, EL 47 w)::
54  RND23(EL 48 w, EL 49 w, EL 50 w, EL 51 w)::
55  RND22(EL 52 w, EL 53 w, EL 54 w, EL 55 w)::
56  RND21(EL 56 w, EL 57 w, EL 58 w, EL 59 w)::
57  RND20(EL 60 w, EL 61 w, EL 62 w, EL 63 w)::
58  RND19(EL 64 w, EL 65 w, EL 66 w, EL 67 w)::
59  RND18(EL 68 w, EL 69 w, EL 70 w, EL 71 w)::
60  RND17(EL 72 w, EL 73 w, EL 74 w, EL 75 w)::
61  RND16(EL 76 w, EL 77 w, EL 78 w, EL 79 w)::
62  RND15(EL 80 w, EL 81 w, EL 82 w, EL 83 w)::
63  RND14(EL 84 w, EL 85 w, EL 86 w, EL 87 w)::
64  RND13(EL 88 w, EL 89 w, EL 90 w, EL 91 w)::
65  RND12(EL 92 w, EL 93 w, EL 94 w, EL 95 w)::
66  RND11(EL 96 w, EL 97 w, EL 98 w, EL 99 w)::
67  RND10(EL 100 w, EL 101 w, EL 102 w, EL 103 w)::
68  RND09(EL 104 w, EL 105 w, EL 106 w, EL 107 w)::
69  RND08(EL 108 w, EL 109 w, EL 110 w, EL 111 w)::
70  RND07(EL 112 w, EL 113 w, EL 114 w, EL 115 w)::
71  RND06(EL 116 w, EL 117 w, EL 118 w, EL 119 w)::
72  RND05(EL 120 w, EL 121 w, EL 122 w, EL 123 w)::
73  RND04(EL 124 w, EL 125 w, EL 126 w, EL 127 w)::
74  RND03(EL 128 w, EL 129 w, EL 130 w, EL 131 w)::[]`;
75
76
77val makeKey_def = Define
78`makeKey userKey kl
79 = let longKey = short2longKey userKey kl
80  in
81  let revPreKey = makeRevPreKey longKey
82  in
83  revPreKey2SubKey revPreKey`;
84
85val makeSubKeyBitSliceLength = Q.store_thm(
86"makeSubKeyBitSliceLength",
87`!longKey n.
88    (LENGTH longKey>= 8)
89    ==>
90    (LENGTH (makeSubKeyBitSlice longKey n ) = n+LENGTH longKey+1)`,
91  Induct_on `n` THENL [
92    FULL_SIMP_TAC list_ss [makeSubKeyBitSlice_def,LENGTH,LET_THM] THEN
93    RW_TAC std_ss [] THEN
94    `?v_1 v_2 v_3 v_4 v_5 v_6 v_7 v_8 t.
95       longKey = (v_1::v_2::v_3::v_4::v_5::v_6::v_7::v_8::t)`
96      by METIS_TAC [listInstGreaterEq8] THEN
97    FULL_SIMP_TAC list_ss [makeSubKeyBitSlice_def] THEN
98    METIS_TAC [LENGTH,SUC_ONE_ADD,ADD_COMM],
99    RW_TAC std_ss [] THEN
100    `?v_1 v_2 v_3 v_4 v_5 v_6 v_7 v_8 t.
101       longKey = (v_1::v_2::v_3::v_4::v_5::v_6::v_7::v_8::t)`
102      by METIS_TAC [listInstGreaterEq8] THEN
103    FULL_SIMP_TAC list_ss [makeSubKeyBitSlice_def] THEN
104    RW_TAC list_ss [] THEN
105    FULL_SIMP_TAC list_ss [Abbrev_def]]);
106
107val makeRevPreKeyLength = Q.store_thm(
108"makeRevPreKeyLength",
109`!userKey.
110    LENGTH (makeRevPreKey userKey) = 132`,
111  RW_TAC std_ss [makeRevPreKey_def,LET_THM] THEN
112  `LENGTH (word256to32l userKey) = 8` by METIS_TAC [word256to32lLength] THEN
113  `LENGTH (word256to32l userKey)>= 8` by RW_TAC arith_ss [] THEN
114  `LENGTH  (makeSubKeyBitSlice (word256to32l userKey) 131) =
115     131+LENGTH (word256to32l userKey) +1`
116     by METIS_TAC [makeSubKeyBitSliceLength,LENGTH_REVERSE] THEN
117  `8 <=  LENGTH (makeSubKeyBitSlice (word256to32l userKey) 131)`
118     by FULL_SIMP_TAC arith_ss [] THEN
119  FULL_SIMP_TAC list_ss [LENGTH_myBUTLASTN,LENGTH_REVERSE]);
120
121(*only length matters in functional correctness*)
122val makeKeyLength = Q.store_thm(
123"makeKeyLength",
124`!userKey kl.
125    LENGTH (makeKey userKey kl) = 33`,
126  RW_TAC list_ss [makeKey_def,revPreKey2SubKey_def,LET_THM]);
127
128val _ = export_theory();
129