1(* ========================================================================= *) 2(* LEAKAGE COMPUTATION CONVERSIONS *) 3(* ========================================================================= *) 4 5structure leakageLib :> leakageLib = 6struct 7 8open HolKernel Parse boolTheory boolLib bossLib metisLib arithmeticTheory 9 pred_setTheory pred_setLib pairTheory extra_pred_setTheory 10 listTheory numTheory simpLib extra_listTheory formalizeUseful 11 stringTheory rich_listTheory stringSimps realTheory realLib 12 listSimps extra_stringTheory extra_stringLib leakageTheory; 13 14open real_sigmaTheory; 15 16val safe_set_ss = (simpLib.++ (bool_ss, PRED_SET_ss)); 17 18val set_ss = (simpLib.++ (arith_ss, PRED_SET_ss)); 19 20val Suff = PARSE_TAC SUFF_TAC; 21 22fun REPEAT_SAFE_EVAL tm = 23 let val t = EVAL tm in 24 if (snd (dest_thm t)) = (mk_eq (tm,tm)) then 25 ALL_CONV tm 26 else 27 t 28 end; 29 30 31fun FIND_CONV (t:term) (c:term->thm) = 32 DEPTH_CONV (test_eq t THENC c); 33 34fun ONCE_FIND_CONV (t:term) (c:term->thm) = 35 ONCE_DEPTH_CONV (test_eq t THENC c); 36 37fun UNFOLD_CONV (defs :thm list) (c:term->thm) = 38 REPEATC (ONCE_REWRITE_CONV defs 39 THENC c); 40 41fun MAKE_ALL_DISTINCT_CONV (c:term->thm) = 42 UNFOLD_CONV [MAKE_ALL_DISTINCT_def] c; 43 44fun MEM_CONV (c:term->thm) = 45 UNFOLD_CONV [MEM] c; 46 47fun F_UNCHANGED_CONV (conv:term->thm) tm = 48 if tm = ``F`` then ALL_CONV tm else conv tm; 49 50fun T_UNCHANGED_CONV (conv:term->thm) tm = 51 if tm = ``T`` then ALL_CONV tm else conv tm; 52 53fun T_F_UNCHANGED_CONV (conv:term->thm) tm = 54 T_UNCHANGED_CONV (F_UNCHANGED_CONV conv) tm; 55 56 57val CROSS_NON_EMPTY_IMP = prove 58 (``!P Q. FINITE P /\ FINITE Q /\ ~(P={}) /\ ~(Q={}) ==> ~(P CROSS Q = {})``, 59 REPEAT STRIP_TAC 60 THEN (MP_TAC o Q.SPEC `P`) SET_CASES 61 THEN RW_TAC std_ss [] 62 THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC 63 THEN (MP_TAC o Q.ISPEC `Q:'b->bool`) SET_CASES 64 THEN RW_TAC std_ss [] 65 THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC 66 THEN FULL_SIMP_TAC std_ss [Once EXTENSION, NOT_IN_EMPTY, IN_INSERT, IN_CROSS] 67 THEN METIS_TAC [PAIR, FST, SND, PAIR_EQ]); 68 69val CROSS_HLR_NON_EMPTY_IMP = prove 70 (``!h l r. FINITE h /\ FINITE l /\ FINITE r /\ ~(h={}) /\ ~(l={}) /\ ~(r={}) ==> ~((h CROSS l) CROSS r = {})``, 71 METIS_TAC [CROSS_NON_EMPTY_IMP, FINITE_CROSS]); 72 73val unif_prog_space_leakage_computation_reduce_COMPUTE = prove (``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ ~((high CROSS low) CROSS random={}) ==> (leakage (unif_prog_space high low random) f = (1/(&(CARD high * CARD low * CARD random)))* (SIGMA (\(out,h,l). (\x. x * lg (((1/(&(CARD random)))* x))) (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) 74 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) - 75 SIGMA (\(out,l). (\x. x * lg (((1/(&(CARD high * CARD random)))* x))) 76 (SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) (high CROSS random))) 77 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))))``, METIS_TAC [unif_prog_space_leakage_computation_reduce]); 78 79fun LEAKAGE_COMPUTE_PROVE_FINITE (t:term) (tl:Abbrev.thm list) = 80 (prove ((mk_comb ((inst [alpha |-> fst(dom_rng(type_of t))]``FINITE``),t)), 81 CONV_TAC (SIMP_CONV set_ss tl))); 82 83fun LEAKAGE_COMPUTE_FINITE_HLR ((h:term),(l:term),(r:term)) (tl:Abbrev.thm list) = 84 [LEAKAGE_COMPUTE_PROVE_FINITE h tl, LEAKAGE_COMPUTE_PROVE_FINITE l tl, LEAKAGE_COMPUTE_PROVE_FINITE r tl]; 85 86fun LEAKAGE_COMPUTE_CROSS_NOT_EMPTY ((h:term),(l:term),(r:term)) (tl:Abbrev.thm list) = 87 (prove (mk_comb (``$~:bool->bool``, 88mk_comb ((mk_comb ((inst [alpha |-> ((pairSyntax.mk_prod((pairSyntax.mk_prod((fst(dom_rng(type_of h))),(fst(dom_rng(type_of l))))),(fst(dom_rng(type_of r)))))-->bool)] ``$=``), 89 (mk_comb (mk_comb ((inst [alpha |-> (pairSyntax.mk_prod((fst(dom_rng(type_of h))),(fst(dom_rng(type_of l))))),beta |-> fst(dom_rng(type_of r))]``$CROSS``),(mk_comb (mk_comb ((inst [alpha |-> fst(dom_rng(type_of h)),beta |-> fst(dom_rng(type_of l))]``$CROSS``), h),l))),r)))), 90(inst [alpha |-> (pairSyntax.mk_prod((pairSyntax.mk_prod((fst(dom_rng(type_of h))),(fst(dom_rng(type_of l))))),(fst(dom_rng(type_of r)))))] ``{}``))), 91 MATCH_MP_TAC CROSS_HLR_NON_EMPTY_IMP 92 THEN ONCE_REWRITE_TAC [EXTENSION] 93 THEN RW_TAC set_ss (append [NOT_IN_EMPTY, EXISTS_OR_THM] tl))); 94 95fun LEAKAGE_COMPUTE_INITIAL_REDUCE ((h:term),(l:term),(r:term)) (tl:Abbrev.thm list) = 96 let val finite = LEAKAGE_COMPUTE_FINITE_HLR (h,l,r) tl in 97 let val cross = LEAKAGE_COMPUTE_CROSS_NOT_EMPTY (h,l,r) (append finite tl) in 98 SIMP_CONV bool_ss (unif_prog_space_leakage_computation_reduce_COMPUTE::cross::finite) 99 end end; 100 101fun COMPUTE_CARD (tm:term) (expand_conv:Abbrev.term->Abbrev.thm) (remove_dups_conv:Abbrev.term->Abbrev.thm) = 102 (((RAND_CONV expand_conv) THENC 103 REPEATC (SIMP_CONV bool_ss [Once CARD_DEF, FINITE_INSERT, FINITE_EMPTY, FINITE_SING] 104 THENC (FIND_CONV ``x IN y`` (IN_CONV remove_dups_conv) 105 THENC SIMP_CONV bool_ss []))) 106 THENC SIMP_CONV arith_ss []) 107 (mk_comb (inst [alpha |-> (fst(dom_rng(type_of tm)))] ``CARD``, tm)); 108 109fun COMPUTE_HLR_CARDS ((h:term),(l:term),(r:term)) 110 (h_expand_conv:Abbrev.term->Abbrev.thm) 111 (l_expand_conv:Abbrev.term->Abbrev.thm) 112 (r_expand_conv:Abbrev.term->Abbrev.thm) 113 (h_dups_conv:Abbrev.term->Abbrev.thm) 114 (l_dups_conv:Abbrev.term->Abbrev.thm) 115 (r_dups_conv:Abbrev.term->Abbrev.thm) = 116 [COMPUTE_CARD h h_expand_conv h_dups_conv, COMPUTE_CARD l l_expand_conv l_dups_conv, COMPUTE_CARD r r_expand_conv r_dups_conv]; 117 118fun LEAKAGE_COMPUTE_REDUCE_CARDS ((h:term),(l:term),(r:term)) (tl:Abbrev.thm list) 119 (h_expand_conv:Abbrev.term->Abbrev.thm) 120 (l_expand_conv:Abbrev.term->Abbrev.thm) 121 (r_expand_conv:Abbrev.term->Abbrev.thm) 122 (h_dups_conv:Abbrev.term->Abbrev.thm) 123 (l_dups_conv:Abbrev.term->Abbrev.thm) 124 (r_dups_conv:Abbrev.term->Abbrev.thm) = 125 LEAKAGE_COMPUTE_INITIAL_REDUCE (h,l,r) tl 126 THENC SIMP_CONV bool_ss (COMPUTE_HLR_CARDS (h,l,r) h_expand_conv l_expand_conv r_expand_conv h_dups_conv l_dups_conv r_dups_conv); 127 128fun LEAKAGE_COMPUTE_HLR_CROSS ((h:term),(l:term),(r:term)) (tl:Abbrev.thm list) 129 (h_expand_conv:Abbrev.term->Abbrev.thm) 130 (l_expand_conv:Abbrev.term->Abbrev.thm) 131 (r_expand_conv:Abbrev.term->Abbrev.thm) 132 (h_dups_conv:Abbrev.term->Abbrev.thm) 133 (l_dups_conv:Abbrev.term->Abbrev.thm) 134 (r_dups_conv:Abbrev.term->Abbrev.thm) = 135 FIND_CONV 136 (mk_comb((mk_comb((inst [alpha |-> (pairSyntax.mk_prod((fst(dom_rng(type_of h))), 137 (fst(dom_rng(type_of l))))), beta |-> (fst(dom_rng(type_of r)))] ``$CROSS``), 138 mk_comb(mk_comb((inst [alpha |-> (fst(dom_rng(type_of h))), beta |-> (fst(dom_rng(type_of l)))] ``$CROSS``),h),l))), r)) 139 (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV h_expand_conv) 140 THENC RAND_CONV l_expand_conv 141 THENC SIMP_CONV bool_ss [CROSS_EQNS, PAIR_EQ, IMAGE_UNION, IMAGE_INSERT, IMAGE_EMPTY, UNION_EMPTY] 142 THENC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV bool_ss [PAIR_EQ] 143 THENC (TRY_CONV h_dups_conv) 144 THENC (TRY_CONV l_dups_conv)))))) 145 THENC (RAND_CONV r_expand_conv) 146 THENC SIMP_CONV bool_ss [CROSS_EQNS, PAIR_EQ, IMAGE_UNION, IMAGE_INSERT, IMAGE_EMPTY, UNION_EMPTY] 147 THENC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV bool_ss [PAIR_EQ] 148 THENC (TRY_CONV h_dups_conv) 149 THENC (TRY_CONV l_dups_conv) 150 THENC (TRY_CONV r_dups_conv))))); 151 152val lg_times_compute_simp_lem = prove 153 (``!x y. x * lg (y * x) = (\x. x * lg (y * x)) x``, 154 RW_TAC std_ss []); 155 156fun LEAKAGE_COMPUTE_IMAGE_HLR_CROSS ((h:term),(l:term),(r:term)) (tl:Abbrev.thm list) (prog_tl:Abbrev.thm list) 157 (h_expand_conv:Abbrev.term->Abbrev.thm) 158 (l_expand_conv:Abbrev.term->Abbrev.thm) 159 (r_expand_conv:Abbrev.term->Abbrev.thm) 160 (h_dups_conv:Abbrev.term->Abbrev.thm) 161 (l_dups_conv:Abbrev.term->Abbrev.thm) 162 (r_dups_conv:Abbrev.term->Abbrev.thm) = 163 LEAKAGE_COMPUTE_HLR_CROSS (h,l,r) tl h_expand_conv l_expand_conv r_expand_conv h_dups_conv l_dups_conv r_dups_conv 164 THENC (RAND_CONV (RAND_CONV (RAND_CONV ( 165 IMAGE_CONV (SIMP_CONV bool_ss prog_tl THENC EVAL) NO_CONV)))) 166 THENC (RAND_CONV (RATOR_CONV (RAND_CONV (RAND_CONV ( 167 IMAGE_CONV (SIMP_CONV bool_ss prog_tl THENC EVAL) NO_CONV))))) 168 THENC (RAND_CONV (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV ( 169 ONCE_REWRITE_CONV [lg_times_compute_simp_lem] 170 THENC (FIND_CONV r (r_expand_conv THENC 171 SIMP_CONV bool_ss [CROSS_EQNS, PAIR_EQ, IMAGE_UNION, IMAGE_INSERT, IMAGE_EMPTY, UNION_EMPTY] 172 THENC (FIND_CONV ``x UNION y`` 173 (UNION_CONV (SIMP_CONV bool_ss [] THENC r_dups_conv))))))))))); 174 175fun RECURSIVE_UNWIND_SUM (dups_conv:Abbrev.term->Abbrev.thm) (item_conv:Abbrev.term->Abbrev.thm) (tm:term) = 176 if (rand tm) = (inst [alpha |-> fst(dom_rng(type_of (rand tm)))] ``{}``) then REWRITE_CONV [REAL_SUM_IMAGE_THM] tm else 177 ((fn (tm:term) => (let val s = snd(dest_comb(snd (dest_comb tm))) in 178 let val f = snd(dest_comb (fst(dest_comb tm))) in 179 let val fin_thm = prove (mk_comb((inst [alpha |-> fst(dom_rng(type_of s))] ``FINITE``),s), 180 CONV_TAC (SIMP_CONV set_ss [])) in 181 REWRITE_CONV [REWRITE_RULE [fin_thm] 182 (ISPEC s ((CONV_RULE SWAP_VARS_CONV) (CONJUNCT2 (ISPEC f REAL_SUM_IMAGE_THM))))] tm 183 end 184 end 185 end)) 186 THENC (TRY_CONV (RATOR_CONV (RAND_CONV item_conv))) 187 THENC (RAND_CONV (RAND_CONV (DELETE_CONV dups_conv))) 188 THENC (RAND_CONV (RECURSIVE_UNWIND_SUM dups_conv item_conv))) tm; 189 190fun LEAKAGE_COMPUTE_UNWIND_OUTER_SUM 191 (h_dups_conv:Abbrev.term->Abbrev.thm) 192 (l_dups_conv:Abbrev.term->Abbrev.thm) 193 (o_dups_conv:Abbrev.term->Abbrev.thm) = 194 RAND_CONV (RATOR_CONV (RAND_CONV ( 195 ONCE_REWRITE_CONV [lg_times_compute_simp_lem] THENC 196 RECURSIVE_UNWIND_SUM (SIMP_CONV bool_ss [PAIR_EQ] 197 THENC (TRY_CONV o_dups_conv) 198 THENC (TRY_CONV h_dups_conv) 199 THENC (TRY_CONV l_dups_conv)) 200 PairRules.PBETA_CONV)) 201 THENC (RAND_CONV (ONCE_REWRITE_CONV [lg_times_compute_simp_lem] THENC 202 RECURSIVE_UNWIND_SUM (SIMP_CONV bool_ss [PAIR_EQ] 203 THENC (TRY_CONV o_dups_conv) 204 THENC (TRY_CONV l_dups_conv)) 205 PairRules.PBETA_CONV))) 206 THENC REWRITE_CONV [REAL_ADD_RID]; 207 208fun LEAKAGE_COMPUTE_UNWIND_INNER_SUM ((h:term),(r:term)) (tl:Abbrev.thm list) (prog_tl:Abbrev.thm list) 209 (h_expand_conv:Abbrev.term->Abbrev.thm) 210 (r_expand_conv:Abbrev.term->Abbrev.thm) 211 (h_dups_conv:Abbrev.term->Abbrev.thm) 212 (r_dups_conv:Abbrev.term->Abbrev.thm) 213 (o_dups_conv:Abbrev.term->Abbrev.thm) = 214 let val h_cross_r = (RATOR_CONV(RAND_CONV (h_expand_conv)) THENC (RAND_CONV r_expand_conv) 215 THENC SIMP_CONV bool_ss [CROSS_EQNS, PAIR_EQ, IMAGE_UNION, IMAGE_INSERT, IMAGE_EMPTY, UNION_EMPTY] 216 THENC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV bool_ss [PAIR_EQ] 217 THENC (TRY_CONV h_dups_conv) 218 THENC (TRY_CONV r_dups_conv))))) 219 (mk_comb(mk_comb((inst [alpha |-> (fst(dom_rng(type_of h))), 220 beta |-> (fst(dom_rng(type_of r)))] ``$CROSS``),h),r)) 221 in 222 RAND_CONV (RATOR_CONV(RAND_CONV (FIND_CONV ``REAL_SUM_IMAGE f s`` ( 223 RECURSIVE_UNWIND_SUM r_dups_conv 224 ((TRY_CONV BETA_CONV) THENC 225 RATOR_CONV (RATOR_CONV (RAND_CONV (LHS_CONV (SIMP_CONV bool_ss prog_tl THENC (TRY_CONV PairRules.PBETA_CONV)) THENC o_dups_conv))) 226 THENC SIMP_CONV bool_ss [])))) 227 THENC (RAND_CONV (REWRITE_CONV [h_cross_r] THENC 228 FIND_CONV ``REAL_SUM_IMAGE f s`` ( 229 RECURSIVE_UNWIND_SUM (SIMP_CONV bool_ss [PAIR_EQ] THENC 230 (TRY_CONV h_dups_conv) THENC 231 (TRY_CONV r_dups_conv)) 232 ((TRY_CONV PairRules.PBETA_CONV) THENC 233 RATOR_CONV (RATOR_CONV (RAND_CONV (LHS_CONV (SIMP_CONV bool_ss prog_tl THENC (TRY_CONV PairRules.PBETA_CONV)) THENC o_dups_conv))) 234 THENC SIMP_CONV bool_ss []))))) THENC REWRITE_CONV [REAL_ADD_RID] 235 end; 236 237fun LEAKAGE_COMPUTE_CONV ((h:term),(l:term),(r:term)) (tl:Abbrev.thm list) (prog_tl:Abbrev.thm list) 238 (h_expand_conv:Abbrev.term->Abbrev.thm) 239 (l_expand_conv:Abbrev.term->Abbrev.thm) 240 (r_expand_conv:Abbrev.term->Abbrev.thm) 241 (h_dups_conv:Abbrev.term->Abbrev.thm) 242 (l_dups_conv:Abbrev.term->Abbrev.thm) 243 (r_dups_conv:Abbrev.term->Abbrev.thm) 244 (o_dups_conv:Abbrev.term->Abbrev.thm) = 245 LEAKAGE_COMPUTE_REDUCE_CARDS (h,l,r) tl h_expand_conv l_expand_conv r_expand_conv h_dups_conv l_dups_conv r_dups_conv 246 THENC LEAKAGE_COMPUTE_IMAGE_HLR_CROSS (h,l,r) tl prog_tl h_expand_conv l_expand_conv r_expand_conv h_dups_conv l_dups_conv r_dups_conv 247 THENC LEAKAGE_COMPUTE_UNWIND_OUTER_SUM h_dups_conv l_dups_conv o_dups_conv 248 THENC LEAKAGE_COMPUTE_UNWIND_INNER_SUM (h,r) tl prog_tl h_expand_conv r_expand_conv h_dups_conv r_dups_conv o_dups_conv 249 THENC (SIMP_CONV real_ss []); 250 251 252end 253