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