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