1(*---------------------------------------------------------------------------*)
2(* Multiplication by a constant. Recursive, iterative, and table-lookup      *)
3(* versions.                                                                 *)
4(*---------------------------------------------------------------------------*)
5
6(* For interactive work
7  load "wordsLib";
8  quietdec := true;
9  open wordsTheory bitTheory wordsLib arithmeticTheory;
10  quietdec := false;
11*)
12
13open HolKernel Parse boolLib bossLib
14     wordsTheory bitTheory wordsLib arithmeticTheory;
15
16val _ = new_theory "Mult";
17
18(*---------------------------------------------------------------------------
19    Multiply a byte (representing a polynomial) by x.
20
21 ---------------------------------------------------------------------------*)
22
23val xtime_def = Define
24  `xtime (w : word8) =
25     w << 1 ?? (if word_msb w then 0x1Bw else 0w)`;
26
27val MSB_lem = Q.prove (
28  `!a b. word_msb (a ?? b) = ~(word_msb a = word_msb b)`,
29  SRW_TAC [WORD_BIT_EQ_ss] []);
30
31val xtime_distrib = Q.store_thm
32("xtime_distrib",
33 `!a b. xtime (a ?? b) = xtime a ?? xtime b`,
34  SRW_TAC [] [xtime_def, MSB_lem] THEN FULL_SIMP_TAC std_ss []);
35
36(*---------------------------------------------------------------------------*)
37(* Multiplication by a constant                                              *)
38(*---------------------------------------------------------------------------*)
39
40val _ = set_fixity "**" (Infixl 675);
41
42val (ConstMult_def,ConstMult_ind) =
43 Defn.tprove
44  (Hol_defn "ConstMult"
45     `b1 ** b2 =
46        if b1 = 0w:word8 then 0w else
47        if word_lsb b1
48           then b2 ?? ((b1 >>> 1) ** xtime b2)
49           else       ((b1 >>> 1) ** xtime b2)`,
50   WF_REL_TAC `measure (w2n o FST)`);
51
52val _ = save_thm("ConstMult_def",ConstMult_def);
53val _ = save_thm("ConstMult_ind",ConstMult_ind);
54val _ = computeLib.add_persistent_funs ["ConstMult_def"];
55
56val ConstMultDistrib = Q.store_thm
57("ConstMultDistrib",
58 `!x y z. x ** (y ?? z) = (x ** y) ?? (x ** z)`,
59 recInduct ConstMult_ind
60   THEN REPEAT STRIP_TAC
61   THEN ONCE_REWRITE_TAC [ConstMult_def]
62   THEN SRW_TAC [] [xtime_distrib]);
63
64(*---------------------------------------------------------------------------*)
65(* Iterative version                                                         *)
66(*---------------------------------------------------------------------------*)
67
68val defn = Hol_defn
69  "IterConstMult"
70  `IterConstMult (b1,b2,acc) =
71     if b1 = 0w:word8 then (b1,b2,acc)
72     else IterConstMult (b1 >>> 1, xtime b2,
73                         if word_lsb b1 then (b2 ?? acc) else acc)`;
74
75val (IterConstMult_def,IterConstMult_ind) =
76 Defn.tprove
77  (defn, WF_REL_TAC `measure (w2n o FST)`);
78
79val _ = save_thm("IterConstMult_def",IterConstMult_def);
80val _ = save_thm("IterConstMult_ind",IterConstMult_ind);
81val _ = computeLib.add_persistent_funs ["IterConstMult_def"];
82
83(*---------------------------------------------------------------------------*)
84(* Equivalence between recursive and iterative forms.                        *)
85(*---------------------------------------------------------------------------*)
86
87val ConstMultEq = Q.store_thm
88("ConstMultEq",
89 `!b1 b2 acc. (b1 ** b2) ?? acc = SND(SND(IterConstMult (b1,b2,acc)))`,
90 recInduct IterConstMult_ind THEN RW_TAC std_ss []
91   THEN ONCE_REWRITE_TAC [ConstMult_def,IterConstMult_def]
92   THEN FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [] []);
93
94(*---------------------------------------------------------------------------*)
95(* Tabled versions                                                           *)
96(*---------------------------------------------------------------------------*)
97
98fun UNROLL_RULE 0 def = def
99  | UNROLL_RULE n def =
100     SIMP_RULE arith_ss [LSR_ADD]
101     (GEN_REWRITE_RULE (RHS_CONV o DEPTH_CONV) empty_rewrites [def]
102                       (UNROLL_RULE (n - 1) def))
103val instantiate =
104 SIMP_RULE (srw_ss()) [WORD_XOR_CLAUSES, GSYM xtime_distrib] o
105 ONCE_REWRITE_CONV [UNROLL_RULE 4 ConstMult_def]
106
107val IterMult2 = UNROLL_RULE 1 IterConstMult_def
108
109(*---------------------------------------------------------------------------*)
110(* mult_unroll                                                               *)
111(*    |- (2w ** x = xtime x) /\                                              *)
112(*       (3w ** x = x # xtime x) /\                                          *)
113(*       (9w ** x = x # xtime (xtime (xtime x)))      /\                     *)
114(*       (11w ** x = x # xtime (x # xtime (xtime x))) /\                     *)
115(*       (13w ** x = x # xtime (xtime (x # xtime x))) /\                     *)
116(*       (14w ** x = xtime (x # xtime (x # xtime x)))                        *)
117(*---------------------------------------------------------------------------*)
118
119val mult_unroll = save_thm("mult_unroll",
120  LIST_CONJ (map instantiate
121    [``0x2w ** x``, ``0x3w ** x``, ``0x9w ** x``,
122     ``0xBw ** x``, ``0xDw ** x``, ``0xEw ** x``]));
123
124val eval_mult = WORD_EVAL_RULE o PURE_REWRITE_CONV [mult_unroll, xtime_def]
125
126fun mk_word8 i = wordsSyntax.mk_n2w(numSyntax.term_of_int i, ``:8``);
127
128(*---------------------------------------------------------------------------*)
129(* Construct specialized multiplication tables.                              *)
130(*---------------------------------------------------------------------------*)
131
132val mult_tables =
133  LIST_CONJ (List.concat (map (fn x => List.tabulate(256,
134       fn i => let val y = mk_word8 i in eval_mult ``^x ** ^y`` end))
135  [``0x2w:word8``, ``0x3w:word8``, ``0x9w:word8``,
136   ``0xBw:word8``, ``0xDw:word8``, ``0xEw:word8``]));
137
138(*---------------------------------------------------------------------------*)
139(* Multiplication by constant implemented by one-step rewrites.              *)
140(*---------------------------------------------------------------------------*)
141
142val _ = save_thm ("mult_tables", mult_tables)
143
144(*---------------------------------------------------------------------------*)
145(* Multiplication by constant implemented by lookup into balanced binary     *)
146(* tree. Lookup is done bit-by-bit.                                          *)
147(*---------------------------------------------------------------------------*)
148
149(*
150val _ = save_thm ("mult_ifs", mult_ifs)
151*)
152
153(*---------------------------------------------------------------------------*)
154(* Exponentiation                                                            *)
155(*---------------------------------------------------------------------------*)
156
157val PolyExp_def =
158 Define
159   `PolyExp x n = if n=0 then 1w else x ** PolyExp x (n-1)`;
160
161
162val _ = export_theory();
163