1(*---------------------------------------------------------------------------*)
2(* Multipliation by a constant. Recursive, iterative, and table-lookup       *)
3(* versions.                                                                 *)
4(*---------------------------------------------------------------------------*)
5
6(* For interactive work
7  app load ["tablesTheory"];
8  open word8Theory pairTheory;
9*)
10
11open HolKernel Parse boolLib bossLib word8Theory tablesTheory;
12
13val _ = new_theory "Mult";
14
15val [a,c] = CONJUNCTS XOR8_AC;
16
17(*---------------------------------------------------------------------------*)
18(*  Name some more constants                                                 *)
19(*---------------------------------------------------------------------------*)
20
21val NINE_def   = Define   `NINE = (F,F,F,F,T,F,F,T)`;
22val ONE_B_def  = Define  `ONE_B = (F,F,F,T,T,F,T,T)`;
23val EIGHTY_def = Define `EIGHTY = (T,F,F,F,F,F,F,F)`;
24val B_HEX_def  = Define  `B_HEX = (F,F,F,F,T,F,T,T)`;
25val D_HEX_def  = Define  `D_HEX = (F,F,F,F,T,T,F,T)`;
26val E_HEX_def  = Define  `E_HEX = (F,F,F,F,T,T,T,F)`;
27
28
29(*---------------------------------------------------------------------------
30    Multiply a byte (representing a polynomial) by x.
31
32   xtime b = (LeftShift b)
33                #
34             (case BYTE_COMPARE b EIGHTY
35               of LESS  -> ZERO
36               || other -> ONE_B)
37
38 ---------------------------------------------------------------------------*)
39
40val xtime_def = Define
41  `xtime ((b7,b6,b5,b4,b3,b2,b1,b0) :word8)
42     =
43   if b7 then (b6,b5,b4,~b3,~b2,b1,~b0,T)
44         else (b6,b5,b4,b3,b2,b1,b0,F)`;
45
46val xtime_distrib = Q.store_thm
47("xtime_distrib",
48 `!a b. xtime (a # b) = (xtime a) # (xtime b)`,
49 SIMP_TAC std_ss [FORALL_BYTE_VARS,XOR8_def]
50   THEN RW_TAC std_ss [xtime_def, XOR8_def, XOR_def]
51   THEN DECIDE_TAC);
52
53(*---------------------------------------------------------------------------*)
54(* Multiplication by a constant                                              *)
55(*---------------------------------------------------------------------------*)
56
57val _ = set_fixity "**" (Infixl 675);
58
59val (ConstMult_def,ConstMult_ind) =
60 Defn.tprove
61  (Hol_defn "ConstMult"
62     `b1 ** b2 =
63        if b1 = ZERO then ZERO else
64        if (b1 & ONE) = ONE
65           then b2 # (RightShift b1 ** xtime b2)
66           else      (RightShift b1 ** xtime b2)`,
67   WF_REL_TAC `measure (BYTE_TO_NUM o FST)` THEN
68   NTAC 10 PairRules.PSTRIP_TAC             THEN
69   SIMP_TAC arith_ss [FORALL_BYTE_VARS]     THEN
70   RW_TAC arith_ss [ZERO_def,RightShift_def,BYTE_TO_NUM_def] THEN
71   RW_TAC arith_ss [B2N_def]);
72
73val _ = save_thm("ConstMult_def",ConstMult_def);
74val _ = save_thm("ConstMult_ind",ConstMult_ind);
75val _ = computeLib.add_persistent_funs ["ConstMult_def"];
76
77val ConstMultDistrib = Q.store_thm
78("ConstMultDistrib",
79 `!x y z. x ** (y # z) = (x ** y) # (x ** z)`,
80 recInduct ConstMult_ind
81   THEN REPEAT STRIP_TAC
82   THEN ONCE_REWRITE_TAC [ConstMult_def]
83   THEN RW_TAC std_ss [XOR8_ZERO,xtime_distrib,AC a c]);
84
85(*---------------------------------------------------------------------------*)
86(* Iterative version                                                         *)
87(*---------------------------------------------------------------------------*)
88
89val defn = Hol_defn
90  "IterConstMult"
91  `IterConstMult (b1,b2,acc) =
92     if b1 = ZERO then (b1,b2,acc)
93     else IterConstMult (RightShift b1, xtime b2,
94                         if (b1 & ONE) = ONE
95                          then (b2 # acc) else acc)`;
96
97val (IterConstMult_def,IterConstMult_ind) =
98 Defn.tprove
99  (defn,
100   WF_REL_TAC `measure (BYTE_TO_NUM o FST)` THEN
101   NTAC 10 PairRules.PSTRIP_TAC             THEN
102   SIMP_TAC arith_ss [FORALL_BYTE_VARS]     THEN
103   RW_TAC arith_ss [ZERO_def,RightShift_def,BYTE_TO_NUM_def] THEN
104   RW_TAC arith_ss [B2N_def]);
105
106val _ = save_thm("IterConstMult_def",IterConstMult_def);
107val _ = save_thm("IterConstMult_ind",IterConstMult_ind);
108val _ = computeLib.add_persistent_funs ["IterConstMult_def"];
109
110(*---------------------------------------------------------------------------*)
111(* Equivalence between recursive and iterative forms.                        *)
112(*---------------------------------------------------------------------------*)
113
114val ConstMultEq = Q.store_thm
115("ConstMultEq",
116 `!b1 b2 acc. (b1 ** b2) # acc = SND(SND(IterConstMult (b1,b2,acc)))`,
117 recInduct IterConstMult_ind THEN RW_TAC std_ss []
118   THEN ONCE_REWRITE_TAC [ConstMult_def,IterConstMult_def]
119   THEN RW_TAC std_ss [XOR8_ZERO,AC a c]
120   THEN FULL_SIMP_TAC std_ss [AC a c]);
121
122
123(*---------------------------------------------------------------------------*)
124(* Specialized version, with partially evaluated multiplication. Uses tables *)
125(* from tablesTheory.                                                        *)
126(*---------------------------------------------------------------------------*)
127
128val TableConstMult_def =
129 Define
130  `tcm x = if x = TWO then GF256_by_2
131            else if x = THREE then GF256_by_3
132            else if x = NINE then GF256_by_9
133            else if x = B_HEX then GF256_by_11
134            else if x = D_HEX then GF256_by_13
135            else if x = E_HEX then GF256_by_14
136            else ARB`;
137
138val tcm_thm = Q.store_thm
139 ("tcm_thm",
140 `(tcm TWO   = GF256_by_2)  /\
141  (tcm THREE = GF256_by_3) /\
142  (tcm NINE  = GF256_by_9)  /\
143  (tcm B_HEX = GF256_by_11) /\
144  (tcm D_HEX = GF256_by_13) /\
145  (tcm E_HEX = GF256_by_14)`,
146 EVAL_TAC);
147
148(*---------------------------------------------------------------------------*)
149(* Directly looking up answers in specialized tables is equivalent to        *)
150(* the multiplication algorithm each time. And should be much faster!        *)
151(*---------------------------------------------------------------------------*)
152
153val MultEquiv = Count.apply Q.store_thm
154 ("MultEquiv",
155  `!b. (tcm TWO b   = TWO ** b) /\
156       (tcm THREE b = THREE ** b)/\
157       (tcm NINE b  = NINE ** b)/\
158       (tcm B_HEX b = B_HEX ** b)/\
159       (tcm D_HEX b = D_HEX ** b)/\
160       (tcm E_HEX b = E_HEX ** b)`,
161 SIMP_TAC std_ss [FORALL_BYTE_BITS] THEN EVAL_TAC);
162
163(*---------------------------------------------------------------------------*)
164(* Exponentiation                                                            *)
165(*---------------------------------------------------------------------------*)
166
167val PolyExp_def =
168 Define
169   `PolyExp x n = if n=0 then ONE else x ** PolyExp x (n-1)`;
170
171
172val _ = export_theory();
173