1(*---------------------------------------------------------------------------*)
2(* Multiplication 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 = BYTE F F F F T F F T`;
22val ONE_B_def  = Define  `ONE_B = BYTE F F F T T F T T`;
23val EIGHTY_def = Define `EIGHTY = BYTE T F F F F F F F`;
24val B_HEX_def  = Define  `B_HEX = BYTE F F F F T F T T`;
25val D_HEX_def  = Define  `D_HEX = BYTE F F F F T T F T`;
26val E_HEX_def  = Define  `E_HEX = BYTE 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 (BYTE b7 b6 b5 b4 b3 b2 b1 b0)
42     =
43   if b7 then (BYTE b6 b5 b4 (~b3) (~b2) b1 (~b0) T)
44         else (BYTE 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   SIMP_TAC arith_ss [FORALL_BYTE_VARS]     THEN
69   RW_TAC arith_ss [ZERO_def,RightShift_def,BYTE_TO_NUM_def] THEN
70   RW_TAC arith_ss [B2N_def]);
71
72val _ = save_thm("ConstMult_def",ConstMult_def);
73val _ = save_thm("ConstMult_ind",ConstMult_ind);
74val _ = computeLib.add_persistent_funs ["ConstMult_def"];
75
76val ConstMultDistrib = Q.store_thm
77("ConstMultDistrib",
78 `!x y z. x ** (y # z) = (x ** y) # (x ** z)`,
79 recInduct ConstMult_ind
80   THEN REPEAT STRIP_TAC
81   THEN ONCE_REWRITE_TAC [ConstMult_def]
82   THEN RW_TAC std_ss [XOR8_ZERO,xtime_distrib,AC a c]);
83
84(*---------------------------------------------------------------------------*)
85(* Iterative version                                                         *)
86(*---------------------------------------------------------------------------*)
87
88val defn = Hol_defn
89  "IterConstMult"
90  `IterConstMult (b1,b2,acc) =
91     if b1 = ZERO then (b1,b2,acc)
92     else IterConstMult (RightShift b1, xtime b2,
93                         if (b1 & ONE) = ONE
94                          then (b2 # acc) else acc)`;
95
96val (IterConstMult_def,IterConstMult_ind) =
97 Defn.tprove
98  (defn,
99   WF_REL_TAC `measure (BYTE_TO_NUM o FST)` THEN
100   SIMP_TAC arith_ss [FORALL_BYTE_VARS]     THEN
101   RW_TAC arith_ss [ZERO_def,RightShift_def,BYTE_TO_NUM_def] THEN
102   RW_TAC arith_ss [B2N_def]);
103
104val _ = save_thm("IterConstMult_def",IterConstMult_def);
105val _ = save_thm("IterConstMult_ind",IterConstMult_ind);
106val _ = computeLib.add_persistent_funs ["IterConstMult_def"];
107
108(*---------------------------------------------------------------------------*)
109(* Equivalence between recursive and iterative forms.                        *)
110(*---------------------------------------------------------------------------*)
111
112val ConstMultEq = Q.store_thm
113("ConstMultEq",
114 `!b1 b2 acc. (b1 ** b2) # acc = SND(SND(IterConstMult (b1,b2,acc)))`,
115 recInduct IterConstMult_ind THEN RW_TAC std_ss []
116   THEN ONCE_REWRITE_TAC [ConstMult_def,IterConstMult_def]
117   THEN RW_TAC std_ss [XOR8_ZERO,AC a c]
118   THEN FULL_SIMP_TAC std_ss [AC a c]);
119
120
121(*---------------------------------------------------------------------------*)
122(* Specialized version, with partially evaluated multiplication. Uses tables *)
123(* from tablesTheory.                                                        *)
124(*---------------------------------------------------------------------------*)
125
126val TableConstMult_def =
127 Define
128  `tcm x = if x = TWO then GF256_by_2
129            else if x = THREE then GF256_by_3
130            else if x = NINE then GF256_by_9
131            else if x = B_HEX then GF256_by_11
132            else if x = D_HEX then GF256_by_13
133            else if x = E_HEX then GF256_by_14
134            else ARB`;
135
136val tcm_thm = Q.store_thm
137 ("tcm_thm",
138 `(tcm TWO   = GF256_by_2)  /\
139  (tcm THREE = GF256_by_3)  /\
140  (tcm NINE  = GF256_by_9)  /\
141  (tcm B_HEX = GF256_by_11) /\
142  (tcm D_HEX = GF256_by_13) /\
143  (tcm E_HEX = GF256_by_14)`,
144 EVAL_TAC);
145
146(*---------------------------------------------------------------------------*)
147(* Directly looking up answers in specialized tables is equivalent to        *)
148(* the multiplication algorithm each time. And should be much faster!        *)
149(*---------------------------------------------------------------------------*)
150
151val MultEquiv = Count.apply Q.store_thm
152 ("MultEquiv",
153  `!b. (tcm TWO b   = TWO ** b)   /\
154       (tcm THREE b = THREE ** b) /\
155       (tcm NINE b  = NINE ** b)  /\
156       (tcm B_HEX b = B_HEX ** b) /\
157       (tcm D_HEX b = D_HEX ** b) /\
158       (tcm E_HEX b = E_HEX ** b)`,
159 SIMP_TAC std_ss [FORALL_BYTE_BITS] THEN EVAL_TAC);
160
161(*---------------------------------------------------------------------------*)
162(* Exponentiation                                                            *)
163(*---------------------------------------------------------------------------*)
164
165val PolyExp_def =
166 Define
167   `PolyExp x n = if n=0 then ONE else x ** PolyExp x (n-1)`;
168
169
170val _ = export_theory();
171