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