1(* ========================================================================= *) 2(* Create "leakageTheory" setting up the theory of information leakage *) 3(* ========================================================================= *) 4 5(* ------------------------------------------------------------------------- *) 6(* Load and open relevant theories *) 7(* (Comment out "load" and "loadPath"s for compilation) *) 8(* ------------------------------------------------------------------------- *) 9(* 10 11app load ["bossLib", "metisLib", "arithmeticTheory", "pred_setTheory", 12 "listTheory", "state_transformerTheory", "probabilityTheory", 13 "formalizeUseful", "combinTheory", "pairTheory", "realTheory", 14 "realLib", "extra_boolTheory", "jrhUtils", "extra_pred_setTheory", "extra_listTheory", 15 "realSimps", "extra_realTheory", "measureTheory", "numTheory", 16 "simpLib", "seqTheory", "subtypeTheory", "transcTheory", 17 "limTheory", "stringTheory", "rich_listTheory", "stringSimps", 18 "listSimps", "lebesgueTheory", "informationTheory", 19 "extra_stringTheory", "extra_stringLib"]; 20 21*) 22 23open HolKernel Parse boolLib bossLib metisLib arithmeticTheory pred_setTheory 24 listTheory state_transformerTheory 25 probabilityTheory formalizeUseful extra_numTheory combinTheory 26 pairTheory realTheory realLib extra_boolTheory jrhUtils 27 extra_pred_setTheory realSimps extra_realTheory measureTheory numTheory 28 simpLib seqTheory subtypeTheory extra_listTheory 29 transcTheory limTheory stringTheory rich_listTheory stringSimps listSimps 30 lebesgueTheory informationTheory extra_stringTheory extra_stringLib; 31 32open real_sigmaTheory; 33 34(* ------------------------------------------------------------------------- *) 35(* Start a new theory called "information" *) 36(* ------------------------------------------------------------------------- *) 37 38val _ = new_theory "leakage"; 39 40(* ------------------------------------------------------------------------- *) 41(* Helpful proof tools *) 42(* ------------------------------------------------------------------------- *) 43 44val REVERSE = Tactical.REVERSE; 45val Simplify = RW_TAC arith_ss; 46val Suff = PARSE_TAC SUFF_TAC; 47val Know = PARSE_TAC KNOW_TAC; 48val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 49val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 50val Cond = 51 DISCH_THEN 52 (fn mp_th => 53 let 54 val cond = fst (dest_imp (concl mp_th)) 55 in 56 KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] 57 end); 58 59val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 60 61(* ************************************************************************* *) 62(* ************************************************************************* *) 63(* Basic Definitions *) 64(* ************************************************************************* *) 65(* ************************************************************************* *) 66 67val () = type_abbrev ("state", Type `:string -> 'a`); 68 69val () = type_abbrev ("prog_state", Type `:(('a state # 'b state) # 'c state)`); 70 71val () = type_abbrev ("prog", Type `:(('a,'b,'c) prog_state) -> 'd state`); 72 73val high_state_def = Define `H (s:(('a,'b,'c) prog_state)) = FST (FST s)`; 74 75val low_state_def = Define `L (s:(('a,'b,'c) prog_state)) = SND (FST s)`; 76 77val random_state_def = Define `R (s:(('a,'b,'c) prog_state)) = SND s`; 78 79(* ------------------------------------------------------------------------- *) 80(* -------- Interference of a program defined w/ prob_space p ------------- *) 81(* ------------------------------------------------------------------------- *) 82 83 84val leakage_def = Define 85 `leakage p (f:('a,'b,'c,'d) prog) = 86 conditional_mutual_information 2 p 87 ((IMAGE f (p_space p)), POW (IMAGE f (p_space p))) 88 ((IMAGE H (p_space p)), POW (IMAGE H (p_space p))) 89 ((IMAGE L (p_space p)), POW (IMAGE L (p_space p))) 90 f H L`; 91 92val visible_leakage_def = Define 93 `visible_leakage p (f:('a,'b,'c,'d) prog) = 94 conditional_mutual_information 2 p 95 ((IMAGE f (p_space p)), POW (IMAGE f (p_space p))) 96 ((IMAGE H (p_space p)), POW (IMAGE H (p_space p))) 97 ((IMAGE (\s:('a,'b,'c) prog_state. (L s, R s)) (p_space p)), 98 POW (IMAGE (\s:('a,'b,'c) prog_state. (L s, R s)) (p_space p))) 99 f H (\s:('a,'b,'c) prog_state. (L s, R s))`; 100 101 102(* ************************************************************************* *) 103(* Simplification of computation for Interference analysis: *) 104(* program space for uniform distribution for program M w/ finite *) 105(* sets of possible initial input states *) 106(* ************************************************************************* *) 107 108 109val unif_prog_dist_def = Define 110 `unif_prog_dist high low random = 111 (\s. if s IN (high CROSS low) CROSS random then 112 1/(&(CARD ((high CROSS low) CROSS random))) else 0)`; 113 114 115val unif_prog_space_def = Define 116 `unif_prog_space high low random = 117 ((high CROSS low) CROSS random, 118 POW ((high CROSS low) CROSS random), 119 (\s. SIGMA (unif_prog_dist high low random) s))`; 120 121 122(* ************************************************************************* *) 123 124 125 126 127(* ************************************************************************* *) 128(* ************************************************************************* *) 129(* Proofs *) 130(* ************************************************************************* *) 131(* ************************************************************************* *) 132 133 134val prob_space_unif_prog_space = store_thm 135 ("prob_space_unif_prog_space", 136 ``!high low random. FINITE high /\ FINITE low /\ FINITE random /\ 137 ~((high CROSS low) CROSS random={}) ==> 138 prob_space (unif_prog_space high low random)``, 139 RW_TAC std_ss [prob_space_def, unif_prog_space_def, unif_prog_dist_def, 140 measure_def, PSPACE] 141 >- (MATCH_MP_TAC finite_additivity_sufficient_for_finite_spaces2 142 >> RW_TAC std_ss [m_space_def, measurable_sets_def, measure_def, POW_SIGMA_ALGEBRA, 143 FINITE_CROSS, positive_def, REAL_SUM_IMAGE_THM] 144 >- (MATCH_MP_TAC REAL_SUM_IMAGE_POS 145 >> STRONG_CONJ_TAC >- METIS_TAC [IN_POW, FINITE_CROSS, SUBSET_FINITE] 146 >> RW_TAC real_ss [] 147 >> RW_TAC real_ss [] 148 >> MATCH_MP_TAC REAL_LE_DIV 149 >> RW_TAC real_ss [REAL_POS]) 150 >> RW_TAC std_ss [additive_def, measure_def, measurable_sets_def] 151 >> `FINITE s /\ FINITE t` by METIS_TAC [IN_POW, FINITE_CROSS, SUBSET_FINITE] 152 >> RW_TAC std_ss [(UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 153 Q.ISPECL [`(s :('a # 'b) # 'c -> bool)`,`(t :('a # 'b) # 'c -> bool)`]) 154 REAL_SUM_IMAGE_DISJOINT_UNION]) 155 >> `(\s. (if s IN high CROSS low CROSS random then 156 1 / & (CARD (high CROSS low CROSS random)) else 0)) = 157 (\s. inv (& (CARD (high CROSS low CROSS random))) * 158 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)` 159 by (RW_TAC std_ss [FUN_EQ_THM, real_div] >> RW_TAC real_ss []) 160 >> POP_ORW >> RW_TAC std_ss [REAL_SUM_IMAGE_CMUL, FINITE_CROSS, REAL_SUM_IMAGE_EQ_CARD] 161 >> MATCH_MP_TAC REAL_MUL_LINV >> RW_TAC std_ss [REAL_OF_NUM_EQ, REAL_0] 162 >> METIS_TAC [CARD_EQ_0, FINITE_CROSS]); 163 164 165val prob_unif_prog_space = store_thm 166 ("prob_unif_prog_space", 167 ``!high low random P. FINITE high /\ FINITE low /\ FINITE random /\ 168 ~((high CROSS low) CROSS random={}) /\ 169 P SUBSET ((high CROSS low) CROSS random) ==> 170 (prob (unif_prog_space high low random) P = 171 (&(CARD P))/(&((CARD high)*(CARD low)*(CARD random))))``, 172 RW_TAC std_ss [unif_prog_space_def, unif_prog_dist_def, PROB] 173 >> `(\s. (if s IN high CROSS low CROSS random then 174 1 / & (CARD (high CROSS low CROSS random)) else 0)) = 175 (\s. inv (& (CARD (high CROSS low CROSS random))) * 176 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)` 177 by (RW_TAC std_ss [FUN_EQ_THM, real_div] >> RW_TAC real_ss []) 178 >> POP_ORW >> `FINITE P` by METIS_TAC [FINITE_CROSS, SUBSET_FINITE] 179 >> ASM_SIMP_TAC std_ss [REAL_SUM_IMAGE_CMUL] 180 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(P :('a # 'b) # 'c -> bool)`) REAL_SUM_IMAGE_IN_IF] 181 >> `(\x. (if x IN P then 182 (\s. (if s IN high CROSS low CROSS random then 1 else 0)) x else 0)) = 183 (\x. if x IN P then 1 else 0)` by METIS_TAC [SUBSET_DEF] 184 >> POP_ORW 185 >> RW_TAC std_ss [real_div, REAL_SUM_IMAGE_EQ_CARD, REAL_MUL_COMM, 186 FINITE_CROSS, CARD_CROSS, REAL_MUL_ASSOC]); 187 188 189val unif_prog_space_low_distribution = store_thm 190 ("unif_prog_space_low_distribution", 191 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 192 ~((high CROSS low) CROSS random={}) ==> 193 (!l. l IN low ==> (distribution(unif_prog_space high low random) L {l} = 194 ((1:real)/(&(CARD low)))))``, 195 RW_TAC std_ss [distribution_def] 196 >> `p_space (unif_prog_space high low random) = 197 (high CROSS low CROSS random)` 198 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 199 >> RW_TAC std_ss [] 200 >> `(PREIMAGE L {l} INTER (high CROSS low CROSS random)) SUBSET 201 (high CROSS low CROSS random)` 202 by RW_TAC std_ss [SUBSET_DEF, IN_INTER] 203 >> RW_TAC std_ss [prob_unif_prog_space] 204 >> `(PREIMAGE L {l} INTER (high CROSS low CROSS random)) = 205 (IMAGE (\x. ((FST x, l),SND x)) (high CROSS random))` 206 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, 207 low_state_def, IN_CROSS, IN_IMAGE] 208 >> EQ_TAC >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `(FST(FST x),SND x)` 209 >> RW_TAC std_ss [FST, SND, PAIR]) 210 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST, SND]) 211 >> POP_ORW 212 >> `INJ (\x. ((FST x,l),SND x)) (high CROSS random) 213 (IMAGE (\x. ((FST x,l),SND x)) (high CROSS random))` 214 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE] 215 >> METIS_TAC [PAIR, PAIR_EQ]) 216 >> RW_TAC std_ss [(Q.SPECL [`(\(x :'a state # 'c state). ((FST x,(l :'b state)),SND x))`, 217 `((high :'a state -> bool) CROSS (random :'c state -> bool))`, 218 `(IMAGE (\(x :'a state # 'c state). ((FST x,l),SND x)) 219 (high CROSS random))`] o 220 INST_TYPE [``:'b`` |-> ``:('a state # 'b state) # 'c state``, 221 ``:'a`` |-> ``:'a state # 'c state``]) CARD_IMAGE, FINITE_CROSS] 222 >> RW_TAC std_ss [CARD_CROSS, GSYM REAL_MUL] 223 >> Suff `((& (CARD high) * & (CARD random)) * 1) / ((& (CARD high) * & (CARD random)) * & (CARD low)) = 224 1 / & (CARD low)` 225 >- RW_TAC real_ss [REAL_MUL_COMM] 226 >> MATCH_MP_TAC REAL_DIV_LMUL_CANCEL 227 >> RW_TAC real_ss [REAL_ENTIRE, REAL_0, REAL_INJ, CARD_EQ_0] 228 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 229 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]); 230 231 232val unif_prog_space_highlow_distribution = store_thm 233 ("unif_prog_space_highlow_distribution", 234 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 235 ~((high CROSS low) CROSS random={}) ==> 236 (!h l. h IN high /\ l IN low ==> 237 (distribution (unif_prog_space high low random) (\x. (H x,L x)) {(h,l)} = 238 ((1:real)/(&((CARD high)*(CARD low))))))``, 239 RW_TAC std_ss [distribution_def] 240 >> `p_space (unif_prog_space high low random) = 241 (high CROSS low CROSS random)` 242 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 243 >> RW_TAC std_ss [] 244 >> `(PREIMAGE (\x. (H x,L x)) {(h,l)} INTER (high CROSS low CROSS random)) SUBSET 245 (high CROSS low CROSS random)` 246 by RW_TAC std_ss [SUBSET_DEF, IN_INTER] 247 >> RW_TAC std_ss [prob_unif_prog_space] 248 >> `(PREIMAGE (\x. (H x,L x)) {(h,l)} INTER (high CROSS low CROSS random)) = 249 (IMAGE (\x. ((h, l), x)) random)` 250 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, 251 low_state_def, IN_CROSS, IN_IMAGE, high_state_def] 252 >> EQ_TAC >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `SND x` 253 >> RW_TAC std_ss [FST, SND, PAIR]) 254 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST, SND]) 255 >> POP_ORW 256 >> `INJ (\x. ((h,l),x)) random 257 (IMAGE (\x. ((h,l),x)) random)` 258 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE] 259 >> METIS_TAC [PAIR, PAIR_EQ]) 260 >> RW_TAC std_ss [(Q.SPECL [`(\(x :'c state). (((h:'a state),(l :'b state)),x))`, 261 `(random :'c state -> bool)`, 262 `(IMAGE (\(x :'c state). (((h:'a state),(l :'b state)),x)) 263 random)`] o 264 INST_TYPE [``:'b`` |-> ``:('a state # 'b state) # 'c state``, 265 ``:'a`` |-> ``:'c state``]) CARD_IMAGE] 266 >> RW_TAC std_ss [CARD_CROSS, GSYM REAL_MUL] 267 >> Suff `((& (CARD random)) * 1) / ((& (CARD random)) * (& (CARD high) * & (CARD low))) = 268 1 / (& (CARD high) * & (CARD low))` 269 >- RW_TAC real_ss [REAL_MUL_COMM] 270 >> MATCH_MP_TAC REAL_DIV_LMUL_CANCEL 271 >> RW_TAC real_ss [REAL_ENTIRE, REAL_0, REAL_INJ, CARD_EQ_0] 272 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 273 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]); 274 275 276val unif_prog_space_lowrandom_distribution = store_thm 277 ("unif_prog_space_lowrandom_distribution", 278 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 279 ~((high CROSS low) CROSS random={}) ==> 280 (!l r. l IN low /\ r IN random ==> 281 (distribution (unif_prog_space high low random) (\x. (L x,R x)) {(l,r)} = 282 ((1:real)/(&((CARD low)*(CARD random))))))``, 283 RW_TAC std_ss [distribution_def] 284 >> `p_space (unif_prog_space high low random) = 285 (high CROSS low CROSS random)` 286 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 287 >> RW_TAC std_ss [] 288 >> `(PREIMAGE (\x. (L x,R x)) {(l,r)} INTER (high CROSS low CROSS random)) SUBSET 289 (high CROSS low CROSS random)` 290 by RW_TAC std_ss [SUBSET_DEF, IN_INTER] 291 >> RW_TAC std_ss [prob_unif_prog_space] 292 >> `(PREIMAGE (\x. (L x,R x)) {(l,r)} INTER (high CROSS low CROSS random)) = 293 (IMAGE (\x. ((x, l), r)) high)` 294 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, 295 low_state_def, IN_CROSS, IN_IMAGE, random_state_def] 296 >> EQ_TAC >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `FST(FST x)` 297 >> RW_TAC std_ss [FST, SND, PAIR]) 298 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST, SND]) 299 >> POP_ORW 300 >> `INJ (\x. ((x,l),r)) high 301 (IMAGE (\x. ((x,l),r)) high)` 302 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE] 303 >> METIS_TAC [PAIR, PAIR_EQ]) 304 >> RW_TAC std_ss [(Q.SPECL [`(\(x :'a state). (((x:'a state),(l :'b state)),(r:'c state)))`, 305 `(high :'a state -> bool)`, 306 `(IMAGE (\(x :'a state). (((x:'a state),(l :'b state)),(r:'c state))) 307 high)`] o 308 INST_TYPE [``:'b`` |-> ``:('a state # 'b state) # 'c state``, 309 ``:'a`` |-> ``:'a state``]) CARD_IMAGE] 310 >> RW_TAC std_ss [CARD_CROSS, GSYM REAL_MUL] 311 >> Suff `((& (CARD high)) * 1) / ((& (CARD high)) * (& (CARD low) * & (CARD random))) = 312 1 / (& (CARD low) * & (CARD random))` 313 >- RW_TAC real_ss [REAL_MUL_COMM] 314 >> MATCH_MP_TAC REAL_DIV_LMUL_CANCEL 315 >> RW_TAC real_ss [REAL_ENTIRE, REAL_0, REAL_INJ, CARD_EQ_0] 316 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 317 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]); 318 319 320val unif_prog_space_highlowrandom_distribution = store_thm 321 ("unif_prog_space_highlowrandom_distribution", 322 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 323 ~((high CROSS low) CROSS random={}) ==> 324 (!h l r. h IN high /\ l IN low /\ r IN random ==> 325 (distribution (unif_prog_space high low random) (\x. (H x, L x,R x)) {(h,l,r)} = 326 ((1:real)/(&((CARD high)*(CARD low)*(CARD random))))))``, 327 RW_TAC std_ss [distribution_def] 328 >> `p_space (unif_prog_space high low random) = 329 (high CROSS low CROSS random)` 330 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 331 >> RW_TAC std_ss [] 332 >> `(PREIMAGE (\x. (H x,L x,R x)) {(h,l,r)} INTER (high CROSS low CROSS random)) SUBSET 333 (high CROSS low CROSS random)` 334 by RW_TAC std_ss [SUBSET_DEF, IN_INTER] 335 >> RW_TAC std_ss [prob_unif_prog_space] 336 >> `(PREIMAGE (\x. (H x,L x,R x)) {(h,l,r)} INTER (high CROSS low CROSS random)) = 337 {((h,l),r)}` 338 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, 339 low_state_def, IN_CROSS, IN_IMAGE, random_state_def, high_state_def] 340 >> METIS_TAC [FST, SND, PAIR]) 341 >> POP_ORW 342 >> RW_TAC std_ss [CARD_CROSS, CARD_SING]); 343 344 345val unif_prog_space_leakage_reduce = store_thm 346 ("unif_prog_space_leakage_reduce", 347 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 348 ~((high CROSS low) CROSS random={}) ==> 349 (leakage (unif_prog_space high low random) f = 350 SIGMA (\x. (\(x,y,z). 351 joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 352 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 353 & (CARD high * CARD low))) x) 354 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) - 355 SIGMA (\x. (\(x,z). 356 joint_distribution (unif_prog_space high low random) f L {(x,z)} * 357 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} * 358 & (CARD low))) x) 359 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))``, 360 RW_TAC std_ss [leakage_def] 361 >> Q.ABBREV_TAC `foo = 362 SIGMA (\x. (\(x,y,z). 363 joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 364 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 365 & (CARD high * CARD low))) x) 366 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) - 367 SIGMA (\x. (\(x,z). 368 joint_distribution (unif_prog_space high low random) f L {(x,z)} * 369 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} * 370 & (CARD low))) x) 371 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))` 372 >> `random_variable (f :('a, 'b, 'c, 'd) prog) (unif_prog_space high low random) 373 (IMAGE (f :('a, 'b, 'c, 'd) prog) (p_space (unif_prog_space high low random)), 374 POW (IMAGE (f :('a, 'b, 'c, 'd) prog) (p_space (unif_prog_space high low random))))` 375 by (RW_TAC std_ss [random_variable_def, prob_space_unif_prog_space] 376 >> RW_TAC std_ss [p_space_def, events_def] 377 >> MATCH_MP_TAC MEASURABLE_POW_TO_POW_IMAGE 378 >> CONJ_TAC >- METIS_TAC [prob_space_unif_prog_space, prob_space_def] 379 >> RW_TAC std_ss [unif_prog_space_def, measurable_sets_def, m_space_def]) 380 >> `random_variable (H :('a, 'b, 'c, 'a) prog) (unif_prog_space high low random) 381 (IMAGE (H :('a, 'b, 'c, 'a) prog) (p_space (unif_prog_space high low random)), 382 POW (IMAGE (H :('a, 'b, 'c, 'a) prog) (p_space (unif_prog_space high low random))))` 383 by (RW_TAC std_ss [random_variable_def, prob_space_unif_prog_space] 384 >> RW_TAC std_ss [p_space_def, events_def] 385 >> MATCH_MP_TAC MEASURABLE_POW_TO_POW_IMAGE 386 >> CONJ_TAC >- METIS_TAC [prob_space_unif_prog_space, prob_space_def] 387 >> RW_TAC std_ss [unif_prog_space_def, measurable_sets_def, m_space_def]) 388 >> `random_variable (L :('a, 'b, 'c, 'b) prog) (unif_prog_space high low random) 389 (IMAGE (L :('a, 'b, 'c, 'b) prog) (p_space (unif_prog_space high low random)), 390 POW (IMAGE (L :('a, 'b, 'c, 'b) prog) (p_space (unif_prog_space high low random))))` 391 by (RW_TAC std_ss [random_variable_def, prob_space_unif_prog_space] 392 >> RW_TAC std_ss [p_space_def, events_def] 393 >> MATCH_MP_TAC MEASURABLE_POW_TO_POW_IMAGE 394 >> CONJ_TAC >- METIS_TAC [prob_space_unif_prog_space, prob_space_def] 395 >> RW_TAC std_ss [unif_prog_space_def, measurable_sets_def, m_space_def]) 396 >> `FINITE (p_space (unif_prog_space high low random))` 397 by RW_TAC std_ss [unif_prog_space_def, FINITE_CROSS, PSPACE] 398 >> `POW (p_space (unif_prog_space high low random)) = events (unif_prog_space high low random)` 399 by RW_TAC std_ss [unif_prog_space_def, PSPACE, EVENTS] 400 >> RW_TAC std_ss [finite_conditional_mutual_information_reduce] 401 >> `p_space (unif_prog_space high low random) = 402 (high CROSS low CROSS random)` 403 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 404 >> RW_TAC std_ss [] 405 >> `IMAGE L (high CROSS low CROSS random) = low` 406 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_IMAGE, low_state_def, IN_CROSS] 407 >> EQ_TAC 408 >- (RW_TAC std_ss [] >> RW_TAC std_ss []) 409 >> `?x t. (high CROSS low CROSS random = x INSERT t) /\ 410 ~(x IN t)` by METIS_TAC [SET_CASES] 411 >> Know `x' IN (high CROSS low CROSS random)` >- METIS_TAC [EXTENSION, IN_INSERT] 412 >> RW_TAC std_ss [IN_CROSS] 413 >> Q.EXISTS_TAC `((FST (FST x'), x), SND x')` 414 >> RW_TAC std_ss []) 415 >> POP_ORW 416 >> `IMAGE (\x. (H x,L x)) (high CROSS low CROSS random) = high CROSS low` 417 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_IMAGE, low_state_def, high_state_def, IN_CROSS] 418 >> EQ_TAC 419 >- (RW_TAC std_ss [] >> RW_TAC std_ss []) 420 >> `?x t. (high CROSS low CROSS random = x INSERT t) /\ 421 ~(x IN t)` by METIS_TAC [SET_CASES] 422 >> Know `x' IN (high CROSS low CROSS random)` >- METIS_TAC [EXTENSION, IN_INSERT] 423 >> RW_TAC std_ss [IN_CROSS] 424 >> Q.EXISTS_TAC `((FST x, SND x),SND x')` 425 >> RW_TAC std_ss []) 426 >> POP_ORW 427 >> `(IMAGE f (high CROSS low CROSS random) CROSS low) = 428 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)) UNION 429 ((IMAGE f (high CROSS low CROSS random) CROSS low) DIFF 430 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))` 431 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_UNION, IN_DIFF, IN_IMAGE, IN_CROSS] 432 >> EQ_TAC >- (RW_TAC std_ss [] >> METIS_TAC []) 433 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 434 >> METIS_TAC []) 435 >> POP_ORW 436 >> `DISJOINT 437 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)) 438 ((IMAGE f (high CROSS low CROSS random) CROSS low) DIFF 439 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))` 440 by (RW_TAC std_ss [IN_DISJOINT, IN_DIFF] >> DECIDE_TAC) 441 >> `FINITE (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)) /\ 442 FINITE ((IMAGE f (high CROSS low CROSS random) CROSS low) DIFF 443 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))` 444 by METIS_TAC [IMAGE_FINITE, FINITE_CROSS, FINITE_DIFF] 445 >> RW_TAC std_ss [(UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 446 Q.ISPECL [`(IMAGE 447 (\(s :('a, 'b, 'c) prog_state). 448 ((f :('a, 'b, 'c, 'd) prog) s,SND (FST s))) 449 ((high :'a state -> bool) CROSS 450 (low :'b state -> bool) CROSS (random :'c state -> bool)))`, 451 `(IMAGE (f :('a, 'b, 'c, 'd) prog) 452 ((high :'a state -> bool) CROSS 453 (low :'b state -> bool) CROSS 454 (random :'c state -> bool)) CROSS low DIFF 455 IMAGE (\(s :('a, 'b, 'c) prog_state). (f s,SND (FST s))) 456 (high CROSS low CROSS random))`]) 457 REAL_SUM_IMAGE_DISJOINT_UNION] 458 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE (f :('a, 'b, 'c, 'd) prog) 459 ((high :'a state -> bool) CROSS 460 (low :'b state -> bool) CROSS 461 (random :'c state -> bool)) CROSS low DIFF 462 IMAGE (\(s :('a, 'b, 'c) prog_state). (f s,SND (FST s))) 463 (high CROSS low CROSS random))`) REAL_SUM_IMAGE_IN_IF] 464 >> `(\x. 465 (if 466 x IN 467 IMAGE f (high CROSS low CROSS random) CROSS low DIFF 468 IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) 469 then 470 (\(x,z). 471 joint_distribution (unif_prog_space high low random) f L 472 {(x,z)} * 473 logr 2 474 (joint_distribution (unif_prog_space high low random) f L 475 {(x,z)} / 476 distribution (unif_prog_space high low random) L {z})) x 477 else 478 0)) = (\x. 0)` 479 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_DIFF, IN_IMAGE, IN_CROSS] 480 >> RW_TAC std_ss [] 481 >> `x = (FST x, SND x)` by RW_TAC std_ss [PAIR] >> POP_ORW 482 >> RW_TAC std_ss [] 483 >> Suff `joint_distribution (unif_prog_space high low random) f L {x} = 0` 484 >- RW_TAC real_ss [] 485 >> RW_TAC std_ss [joint_distribution_def] 486 >> Suff `PREIMAGE (\x. (f x,L x)) {x} INTER (high CROSS low CROSS random) = {}` 487 >- METIS_TAC [prob_space_unif_prog_space, PROB_EMPTY] 488 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [NOT_IN_EMPTY, IN_INTER, IN_PREIMAGE, IN_SING, IN_CROSS, 489 low_state_def] 490 >> Q.PAT_X_ASSUM `FST x = f x'` (MP_TAC o GSYM) >> RW_TAC std_ss [] 491 >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM (MP_TAC o Q.SPEC `x''`) 492 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 493 >> METIS_TAC [PAIR, PAIR_EQ, FST, SND]) 494 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] >> POP_ASSUM (K ALL_TAC) 495 >> `(IMAGE f (high CROSS low CROSS random) CROSS (high CROSS low)) = 496 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) UNION 497 ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS low)) DIFF 498 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))` 499 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_UNION, IN_DIFF, IN_IMAGE, IN_CROSS] 500 >> EQ_TAC >- (RW_TAC std_ss [] >> METIS_TAC []) 501 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 502 >> METIS_TAC []) 503 >> POP_ORW 504 >> `DISJOINT 505 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) 506 ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS low)) DIFF 507 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))` 508 by (RW_TAC std_ss [IN_DISJOINT, IN_DIFF] >> DECIDE_TAC) 509 >> `FINITE (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) /\ 510 FINITE ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS low)) DIFF 511 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))` 512 by METIS_TAC [IMAGE_FINITE, FINITE_CROSS, FINITE_DIFF] 513 >> RW_TAC std_ss [(UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 514 Q.ISPECL [`(IMAGE 515 (\(s :('a, 'b, 'c) prog_state). 516 ((f :('a, 'b, 'c, 'd) prog) s,FST s)) 517 ((high :'a state -> bool) CROSS 518 (low :'b state -> bool) CROSS (random :'c state -> bool)))`, 519 `(IMAGE (f :('a, 'b, 'c, 'd) prog) 520 ((high :'a state -> bool) CROSS 521 (low :'b state -> bool) CROSS 522 (random :'c state -> bool)) CROSS (high CROSS low) DIFF 523 IMAGE (\(s :('a, 'b, 'c) prog_state). (f s,FST s)) 524 (high CROSS low CROSS random))`]) 525 REAL_SUM_IMAGE_DISJOINT_UNION] 526 >> Q.PAT_X_ASSUM `DISJOINT P Q` (K ALL_TAC) 527 >> Q.PAT_X_ASSUM `DISJOINT P Q` (K ALL_TAC) 528 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE (f :('a, 'b, 'c, 'd) prog) 529 ((high :'a state -> bool) CROSS 530 (low :'b state -> bool) CROSS 531 (random :'c state -> bool)) CROSS (high CROSS low) DIFF 532 IMAGE (\(s :('a, 'b, 'c) prog_state). (f s,FST s)) 533 (high CROSS low CROSS random))`) REAL_SUM_IMAGE_IN_IF] 534 >> `(\x. 535 (if 536 x IN 537 IMAGE f (high CROSS low CROSS random) CROSS 538 (high CROSS low) DIFF 539 IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) 540 then 541 (\(x,y,z). 542 joint_distribution (unif_prog_space high low random) f 543 (\x. (H x,L x)) {(x,y,z)} * 544 logr 2 545 (joint_distribution (unif_prog_space high low random) f 546 (\x. (H x,L x)) {(x,y,z)} / 547 distribution (unif_prog_space high low random) 548 (\x. (H x,L x)) {(y,z)})) x 549 else 550 0)) = (\x. 0)` 551 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_DIFF, IN_IMAGE, IN_CROSS] 552 >> RW_TAC std_ss [] 553 >> `x = (FST x, FST (SND x), SND (SND x))` by METIS_TAC [PAIR] >> POP_ORW 554 >> RW_TAC std_ss [] 555 >> Suff `joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(f x',SND x)} = 0` 556 >- RW_TAC real_ss [] 557 >> RW_TAC std_ss [joint_distribution_def] 558 >> Suff `PREIMAGE (\x. (f x,H x,L x)) {(f x',SND x)} INTER (high CROSS low CROSS random) = {}` 559 >- METIS_TAC [prob_space_unif_prog_space, PROB_EMPTY] 560 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [NOT_IN_EMPTY, IN_INTER, IN_PREIMAGE, IN_SING, IN_CROSS, 561 low_state_def, high_state_def, PAIR] 562 >> Q.PAT_X_ASSUM `FST x = f x'` (MP_TAC o GSYM) >> RW_TAC std_ss [] 563 >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM (MP_TAC o Q.SPEC `x''`) 564 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 565 >> METIS_TAC [PAIR, PAIR_EQ, FST, SND]) 566 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] >> POP_ASSUM (K ALL_TAC) 567 >> NTAC 2 (Q.PAT_X_ASSUM `FINITE (P DIFF Q)` (K ALL_TAC)) 568 >> ASM_SIMP_TAC std_ss [GSYM lg_def] 569 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE 570 (\(s :('a, 'b, 'c) prog_state). 571 ((f :('a, 'b, 'c, 'd) prog) s,SND (FST s))) 572 ((high :'a state -> bool) CROSS 573 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 574 >> `(\x. (if x IN IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) then 575 (\(x,z). joint_distribution (unif_prog_space high low random) f L {(x,z)} * 576 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} / 577 distribution (unif_prog_space high low random) L {z})) x else 0)) = 578 (\x. (if x IN IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) then 579 (\(x,z). joint_distribution (unif_prog_space high low random) f L {(x,z)} * 580 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} * 581 (&(CARD low)))) x else 0))` 582 by (RW_TAC std_ss [FUN_EQ_THM, IN_IMAGE, IN_CROSS] >> RW_TAC std_ss [] 583 >> RW_TAC std_ss [unif_prog_space_low_distribution, GSYM REAL_INV_1OVER, real_div, REAL_INV_INV]) 584 >> POP_ORW 585 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 586 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE 587 (\(s :('a, 'b, 'c) prog_state). 588 ((f :('a, 'b, 'c, 'd) prog) s,FST s)) 589 ((high :'a state -> bool) CROSS 590 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 591 >> `(\x. (if x IN IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) then 592 (\(x,y,z). joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 593 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} / 594 distribution (unif_prog_space high low random) (\x. (H x,L x)) {(y,z)})) x else 0)) = 595 (\x. (if x IN IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) then 596 (\(x,y,z). joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 597 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 598 (&((CARD high)*(CARD low))))) x else 0))` 599 by (RW_TAC std_ss [FUN_EQ_THM, IN_IMAGE, IN_CROSS] >> RW_TAC std_ss [] 600 >> `FST s' = (FST (FST s'), SND (FST s'))` by RW_TAC std_ss [PAIR] >> POP_ORW 601 >> RW_TAC std_ss [unif_prog_space_highlow_distribution, GSYM REAL_INV_1OVER, real_div, REAL_INV_INV]) 602 >> POP_ORW 603 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 604 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] >> RW_TAC std_ss [GSYM real_sub] 605 >> Q.UNABBREV_TAC `foo` >> RW_TAC std_ss []); 606 607val unif_prog_space_visible_leakage_reduce = store_thm 608 ("unif_prog_space_visible_leakage_reduce", 609 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 610 ~((high CROSS low) CROSS random={}) ==> 611 (visible_leakage (unif_prog_space high low random) f = 612 SIGMA 613 (\x. 614 (\(x,y,z). 615 joint_distribution (unif_prog_space high low random) f 616 (\s. (H s,L s,R s)) {(x,y,z)} * 617 lg 618 (joint_distribution (unif_prog_space high low random) f 619 (\s. (H s,L s,R s)) {(x,y,z)} * 620 & (CARD high * CARD low * CARD random))) x) 621 (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) 622 (high CROSS low CROSS random)) - 623SIGMA 624 (\x. 625 (\(x,z). 626 joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) 627 {(x,z)} * 628 lg 629 (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) 630 {(x,z)} * & (CARD low * CARD random))) x) 631 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)))``, 632 RW_TAC std_ss [visible_leakage_def] 633 >> Q.ABBREV_TAC `foo = SIGMA 634 (\x. 635 (\(x,y,z). 636 joint_distribution (unif_prog_space high low random) f 637 (\s. (H s,L s,R s)) {(x,y,z)} * 638 lg 639 (joint_distribution (unif_prog_space high low random) f 640 (\s. (H s,L s,R s)) {(x,y,z)} * 641 & (CARD high * CARD low * CARD random))) x) 642 (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) 643 (high CROSS low CROSS random)) - 644SIGMA 645 (\x. 646 (\(x,z). 647 joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) 648 {(x,z)} * 649 lg 650 (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) 651 {(x,z)} * & (CARD low * CARD random))) x) 652 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))` 653 654 >> `random_variable (f :('a, 'b, 'c, 'd) prog) (unif_prog_space high low random) 655 (IMAGE (f :('a, 'b, 'c, 'd) prog) (p_space (unif_prog_space high low random)), 656 POW (IMAGE (f :('a, 'b, 'c, 'd) prog) (p_space (unif_prog_space high low random))))` 657 by (RW_TAC std_ss [random_variable_def, prob_space_unif_prog_space] 658 >> RW_TAC std_ss [p_space_def, events_def] 659 >> MATCH_MP_TAC MEASURABLE_POW_TO_POW_IMAGE 660 >> CONJ_TAC >- METIS_TAC [prob_space_unif_prog_space, prob_space_def] 661 >> RW_TAC std_ss [unif_prog_space_def, measurable_sets_def, m_space_def]) 662 >> `random_variable (H :('a, 'b, 'c, 'a) prog) (unif_prog_space high low random) 663 (IMAGE (H :('a, 'b, 'c, 'a) prog) (p_space (unif_prog_space high low random)), 664 POW (IMAGE (H :('a, 'b, 'c, 'a) prog) (p_space (unif_prog_space high low random))))` 665 by (RW_TAC std_ss [random_variable_def, prob_space_unif_prog_space] 666 >> RW_TAC std_ss [p_space_def, events_def] 667 >> MATCH_MP_TAC MEASURABLE_POW_TO_POW_IMAGE 668 >> CONJ_TAC >- METIS_TAC [prob_space_unif_prog_space, prob_space_def] 669 >> RW_TAC std_ss [unif_prog_space_def, measurable_sets_def, m_space_def]) 670 >> `random_variable (\s.((L :('a, 'b, 'c, 'b) prog) s,(R :('a, 'b, 'c, 'c) prog) s)) 671 (unif_prog_space high low random) 672 (IMAGE (\s.((L :('a, 'b, 'c, 'b) prog) s,(R :('a, 'b, 'c, 'c) prog) s)) 673 (p_space (unif_prog_space high low random)), 674 POW (IMAGE (\s.((L :('a, 'b, 'c, 'b) prog) s,(R :('a, 'b, 'c, 'c) prog) s)) 675 (p_space (unif_prog_space high low random))))` 676 by (RW_TAC std_ss [random_variable_def, prob_space_unif_prog_space] 677 >> RW_TAC std_ss [p_space_def, events_def] 678 >> MATCH_MP_TAC MEASURABLE_POW_TO_POW_IMAGE 679 >> CONJ_TAC >- METIS_TAC [prob_space_unif_prog_space, prob_space_def] 680 681 >> RW_TAC std_ss [unif_prog_space_def, measurable_sets_def, m_space_def]) 682 683 >> `FINITE (p_space (unif_prog_space high low random))` 684 by RW_TAC std_ss [unif_prog_space_def, FINITE_CROSS, PSPACE] 685 >> `POW (p_space (unif_prog_space high low random)) = events (unif_prog_space high low random)` 686 by RW_TAC std_ss [unif_prog_space_def, PSPACE, EVENTS] 687 >> RW_TAC std_ss [finite_conditional_mutual_information_reduce] 688 >> `p_space (unif_prog_space high low random) = 689 (high CROSS low CROSS random)` 690 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 691 >> RW_TAC std_ss [] 692 >> `IMAGE (\s. (L s,R s)) (high CROSS low CROSS random) = low CROSS random` 693 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_IMAGE, low_state_def, random_state_def, IN_CROSS] 694 >> EQ_TAC 695 >- (RW_TAC std_ss [] >> RW_TAC std_ss []) 696 >> `?x t. (high CROSS low CROSS random = x INSERT t) /\ 697 ~(x IN t)` by METIS_TAC [SET_CASES] 698 >> Know `x' IN (high CROSS low CROSS random)` >- METIS_TAC [EXTENSION, IN_INSERT] 699 >> RW_TAC std_ss [IN_CROSS] 700 >> Q.EXISTS_TAC `((FST (FST x'), FST x), SND x)` 701 >> RW_TAC std_ss []) 702 >> POP_ORW 703 >> `IMAGE (\s. (H s,L s,R s)) (high CROSS low CROSS random) = (high CROSS (low CROSS random))` 704 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_IMAGE, low_state_def, high_state_def, random_state_def, IN_CROSS] 705 >> EQ_TAC 706 >- (RW_TAC std_ss [] >> RW_TAC std_ss []) 707 >> RW_TAC std_ss [IN_CROSS] 708 >> Q.EXISTS_TAC `((FST x, FST(SND x)),SND(SND x))` 709 >> RW_TAC std_ss []) 710 >> POP_ORW 711 >> `(IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random)) = 712 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)) UNION 713 ((IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random)) DIFF 714 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)))` 715 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_UNION, IN_DIFF, IN_IMAGE, IN_CROSS] 716 >> EQ_TAC >- (RW_TAC std_ss [] >> METIS_TAC []) 717 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 718 >> METIS_TAC []) 719 >> POP_ORW 720 >> `DISJOINT 721 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)) 722 ((IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random)) DIFF 723 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)))` 724 by (RW_TAC std_ss [IN_DISJOINT, IN_DIFF] >> DECIDE_TAC) 725 >> `FINITE (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)) /\ 726 FINITE ((IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random)) DIFF 727 (IMAGE (\s. (f s,(SND (FST s),SND s))) (high CROSS low CROSS random)))` 728 by METIS_TAC [IMAGE_FINITE, FINITE_CROSS, FINITE_DIFF] 729 >> RW_TAC std_ss [(UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 730 Q.ISPECL [`(IMAGE 731 (\(s :('a, 'b, 'c) prog_state). 732 ((f :('a, 'b, 'c, 'd) prog) s,SND (FST s),SND s)) 733 ((high :'a state -> bool) CROSS 734 (low :'b state -> bool) CROSS (random :'c state -> bool)))`, 735 `(IMAGE (f :('a, 'b, 'c, 'd) prog) 736 ((high :'a state -> bool) CROSS 737 (low :'b state -> bool) CROSS 738 (random :'c state -> bool)) CROSS (low CROSS random) DIFF 739 IMAGE (\(s :('a, 'b, 'c) prog_state). 740 ((f :('a, 'b, 'c, 'd) prog) s,SND (FST s),SND s)) 741 (high CROSS low CROSS random))`]) 742 REAL_SUM_IMAGE_DISJOINT_UNION] 743 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE (f :('a, 'b, 'c, 'd) prog) 744 ((high :'a state -> bool) CROSS 745 (low :'b state -> bool) CROSS 746 (random :'c state -> bool)) CROSS (low CROSS random) DIFF 747 IMAGE (\(s :('a, 'b, 'c) prog_state). 748 ((f :('a, 'b, 'c, 'd) prog) s,SND (FST s),SND s)) 749 (high CROSS low CROSS random))`) REAL_SUM_IMAGE_IN_IF] 750 >> `(\x. 751 (if 752 x IN 753 IMAGE f (high CROSS low CROSS random) CROSS (low CROSS random) DIFF 754 IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) 755 then 756 (\(x,z). 757 joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * 758 logr 2 759 (joint_distribution (unif_prog_space high low random) f 760 (\s. (L s,R s)) {(x,z)} / 761 distribution (unif_prog_space high low random) 762 (\s. (L s,R s)) {z})) x 763 else 764 0)) = (\x. 0)` 765 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_DIFF, IN_IMAGE, IN_CROSS] 766 >> RW_TAC std_ss [] 767 >> `x = (FST x, SND x)` by RW_TAC std_ss [PAIR] >> POP_ORW 768 >> RW_TAC std_ss [] 769 >> Suff `joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {x} = 0` 770 >- RW_TAC real_ss [] 771 >> RW_TAC std_ss [joint_distribution_def] 772 >> Suff `PREIMAGE (\s. (f s,L s,R s)) {x} INTER 773 (high CROSS low CROSS random) = {}` 774 >- METIS_TAC [prob_space_unif_prog_space, PROB_EMPTY] 775 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [NOT_IN_EMPTY, IN_INTER, IN_PREIMAGE, IN_SING, IN_CROSS, 776 low_state_def, random_state_def] 777 >> Q.PAT_X_ASSUM `FST x = f x'` (MP_TAC o GSYM) >> RW_TAC std_ss [] 778 >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM (MP_TAC o Q.SPEC `x''`) 779 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 780 >> METIS_TAC [PAIR, PAIR_EQ, FST, SND]) 781 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] >> POP_ASSUM (K ALL_TAC) 782 >> `(IMAGE f (high CROSS low CROSS random) CROSS (high CROSS (low CROSS random))) = 783 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)) UNION 784 ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS (low CROSS random))) DIFF 785 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)))` 786 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_UNION, IN_DIFF, IN_IMAGE, IN_CROSS] 787 >> EQ_TAC >- (RW_TAC std_ss [] >> METIS_TAC []) 788 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 789 >> METIS_TAC []) 790 >> POP_ORW 791 >> `DISJOINT 792 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)) 793 ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS (low CROSS random))) DIFF 794 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)))` 795 by (RW_TAC std_ss [IN_DISJOINT, IN_DIFF] >> DECIDE_TAC) 796 >> `FINITE (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)) /\ 797 FINITE ((IMAGE f (high CROSS low CROSS random) CROSS (high CROSS (low CROSS random))) DIFF 798 (IMAGE (\s. (f s,(FST(FST s),(SND(FST s),SND s)))) (high CROSS low CROSS random)))` 799 by METIS_TAC [IMAGE_FINITE, FINITE_CROSS, FINITE_DIFF] 800 >> RW_TAC std_ss [(UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 801 Q.ISPECL [`(IMAGE 802 (\(s :('a, 'b, 'c) prog_state). 803 ((f :('a, 'b, 'c, 'd) prog) s,FST (FST s),SND (FST s), 804 SND s)) 805 ((high :'a state -> bool) CROSS 806 (low :'b state -> bool) CROSS (random :'c state -> bool)))`, 807 `(IMAGE (f :('a, 'b, 'c, 'd) prog) 808 ((high :'a state -> bool) CROSS 809 (low :'b state -> bool) CROSS 810 (random :'c state -> bool)) CROSS (high CROSS (low CROSS random)) DIFF 811 IMAGE (\(s :('a, 'b, 'c) prog_state). 812 ((f :('a, 'b, 'c, 'd) prog) s,FST (FST s),SND (FST s), 813 SND s)) 814 (high CROSS low CROSS random))`]) 815 REAL_SUM_IMAGE_DISJOINT_UNION] 816 >> Q.PAT_X_ASSUM `DISJOINT P Q` (K ALL_TAC) 817 >> Q.PAT_X_ASSUM `DISJOINT P Q` (K ALL_TAC) 818 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE (f :('a, 'b, 'c, 'd) prog) 819 ((high :'a state -> bool) CROSS 820 (low :'b state -> bool) CROSS 821 (random :'c state -> bool)) CROSS (high CROSS (low CROSS random)) DIFF 822 IMAGE (\(s :('a, 'b, 'c) prog_state). 823 ((f :('a, 'b, 'c, 'd) prog) s,FST (FST s),SND (FST s), 824 SND s)) 825 (high CROSS low CROSS random))`) REAL_SUM_IMAGE_IN_IF] 826 >> `(\x. 827 (if 828 x IN 829 IMAGE f (high CROSS low CROSS random) CROSS 830 (high CROSS (low CROSS random)) DIFF 831 IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) 832 then 833 (\(x,y,z). 834 joint_distribution (unif_prog_space high low random) f 835 (\s. (H s,L s,R s)) {(x,y,z)} * 836 logr 2 837 (joint_distribution (unif_prog_space high low random) f 838 (\s. (H s,L s,R s)) {(x,y,z)} / 839 distribution (unif_prog_space high low random) 840 (\s. (H s,L s,R s)) {(y,z)})) x 841 else 842 0)) = (\x. 0)` 843 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_DIFF, IN_IMAGE, IN_CROSS] 844 >> RW_TAC std_ss [] 845 >> `x = (FST x, FST (SND x), SND (SND x))` by METIS_TAC [PAIR] >> POP_ORW 846 >> RW_TAC std_ss [] 847 >> Suff `joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(f x',SND x)} = 0` 848 >- RW_TAC real_ss [] 849 >> RW_TAC std_ss [joint_distribution_def] 850 >> Suff `PREIMAGE (\s. (f s,H s,L s,R s)) {(f x',SND x)} INTER 851 (high CROSS low CROSS random) = {}` 852 >- METIS_TAC [prob_space_unif_prog_space, PROB_EMPTY] 853 >> ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [NOT_IN_EMPTY, IN_INTER, IN_PREIMAGE, IN_SING, IN_CROSS, 854 low_state_def, high_state_def, PAIR, random_state_def] 855 >> Q.PAT_X_ASSUM `FST x = f x'` (MP_TAC o GSYM) >> RW_TAC std_ss [] 856 >> POP_ASSUM (K ALL_TAC) >> POP_ASSUM (MP_TAC o Q.SPEC `x''`) 857 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST,SND] 858 >> METIS_TAC [PAIR, PAIR_EQ, FST, SND]) 859 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] >> POP_ASSUM (K ALL_TAC) 860 >> NTAC 2 (Q.PAT_X_ASSUM `FINITE (P DIFF Q)` (K ALL_TAC)) 861 >> ASM_SIMP_TAC std_ss [GSYM lg_def] 862 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE 863 (\(s :('a, 'b, 'c) prog_state). 864 ((f :('a, 'b, 'c, 'd) prog) s,SND (FST s),SND s)) 865 ((high :'a state -> bool) CROSS 866 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 867 >> `(\x. (if x IN IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) then 868 (\(x,z). joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * 869 lg (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} / 870 distribution (unif_prog_space high low random) (\s. (L s,R s)) {z})) x else 0)) = 871 (\x. (if x IN IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) then 872 (\(x,z). joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * 873 lg (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * 874 (&(CARD low * CARD random)))) x else 0))` 875 by (RW_TAC std_ss [FUN_EQ_THM, IN_IMAGE, IN_CROSS] >> RW_TAC std_ss [] 876 >> RW_TAC std_ss [unif_prog_space_lowrandom_distribution, GSYM REAL_INV_1OVER, real_div, REAL_INV_INV]) 877 >> POP_ORW 878 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 879 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE 880 (\(s :('a, 'b, 'c) prog_state). 881 ((f :('a, 'b, 'c, 'd) prog) s,FST (FST s),SND (FST s), 882 SND s)) 883 ((high :'a state -> bool) CROSS 884 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 885 >> `(\x. (if x IN IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) then 886 (\(x,y,z). joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} * 887 lg (joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} / 888 distribution (unif_prog_space high low random) (\s. (H s,L s,R s)) {(y,z)})) x else 0)) = 889 (\x. (if x IN IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) then 890 (\(x,y,z). joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} * 891 lg (joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} * 892 (&((CARD high)*(CARD low)*(CARD random))))) x else 0))` 893 by (RW_TAC std_ss [FUN_EQ_THM, IN_IMAGE, IN_CROSS] >> RW_TAC std_ss [] 894 >> `FST s' = (FST (FST s'), SND (FST s'))` by RW_TAC std_ss [PAIR] >> POP_ORW 895 >> RW_TAC std_ss [unif_prog_space_highlowrandom_distribution, GSYM REAL_INV_1OVER, real_div, REAL_INV_INV]) 896 >> POP_ORW 897 >> ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_IN_IF] 898 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] >> RW_TAC std_ss [GSYM real_sub] 899 >> Q.UNABBREV_TAC `foo` >> RW_TAC std_ss []); 900 901 902val unif_prog_space_leakage_lemma1 = store_thm 903 ("unif_prog_space_leakage_lemma1", 904 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\ 905 ~((high CROSS low) CROSS random={}) ==> 906 (SIGMA (\x. (\(x,z). 907 joint_distribution (unif_prog_space high low random) f L {(x,z)} * 908 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} * 909 & (CARD low))) x) 910 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))= 911 SIGMA (\x. (\(x,z). 912 ((1/(&(CARD high * CARD low * CARD random)))* 913 (SIGMA (\(h,r). if (f((h,z),r)=x) then 1 else 0) 914 (high CROSS random))) * 915 lg (((1/(&(CARD high * CARD low * CARD random)))* 916 (SIGMA (\(h,r). if (f((h,z),r)=x) then 1 else 0) 917 (high CROSS random))) * 918 & (CARD low))) x) 919 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))``, 920 RW_TAC std_ss [] 921 >> `p_space (unif_prog_space high low random) = 922 (high CROSS low CROSS random)` 923 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 924 >> `FINITE (IMAGE (\s. (f s,SND(FST s))) (high CROSS low CROSS random))` 925 by METIS_TAC [IMAGE_FINITE, FINITE_CROSS] 926 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE 927 (\(s :('a, 'b, 'c) prog_state). 928 ((f :('a, 'b, 'c, 'd) prog) s,SND(FST s))) 929 ((high :'a state -> bool) CROSS 930 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 931 >> Suff `(\x. (if x IN IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) then 932 (\x. (\(x,z). joint_distribution (unif_prog_space high low random) f L {(x,z)} * 933 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} * & (CARD low))) x) x 934 else 0)) = 935 (\x. (if x IN IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random) then 936 (\x. (\(x,z). 1 / & (CARD high * CARD low * CARD random) * 937 SIGMA (\(h,r). (if f ((h,z),r) = x then 1 else 0)) (high CROSS random) * 938 lg (1 / & (CARD high * CARD low * CARD random) * 939 SIGMA (\(h,r). (if f ((h,z),r) = x then 1 else 0)) (high CROSS random) * 940 & (CARD low))) x) x else 0))` 941 >- RW_TAC std_ss [] 942 >> ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_IMAGE, IN_CROSS] 943 >> RW_TAC std_ss [] >> RW_TAC std_ss [] 944 >> Q.ABBREV_TAC `j = joint_distribution (unif_prog_space high low random) f L {(f s',SND (FST s'))}` 945 >> Q.ABBREV_TAC `s = 1 / & (CARD high * CARD low * CARD random) * 946 SIGMA (\(h,r). (if f ((h,SND (FST s')),r) = f s' then 1 else 0)) 947 (high CROSS random)` 948 >> Suff `j = s` 949 >- RW_TAC std_ss [] 950 >> Q.UNABBREV_TAC `j` >> Q.UNABBREV_TAC `s` 951 >> RW_TAC std_ss [joint_distribution_def, unif_prog_space_def, unif_prog_dist_def, PROB, 952 FINITE_CROSS, CARD_CROSS] 953 >> `(\s. (if s IN high CROSS low CROSS random then 954 1 / & (CARD high * CARD low * CARD random) else 0)) = 955 (\s. (1 / & (CARD high * CARD low * CARD random)) * 956 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)` 957 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss []) 958 >> POP_ORW 959 >> RW_TAC std_ss [REAL_SUM_IMAGE_CMUL, FINITE_CROSS, FINITE_INTER] 960 >> RW_TAC std_ss [REAL_EQ_LMUL] 961 >> Cases_on `(1 / & (CARD high * CARD low * CARD random) = 0)` 962 >> RW_TAC std_ss [] 963 >> `PREIMAGE (\x. (f x,L x)) {(f s',SND (FST s'))} = 964 PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')}` 965 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_SING, IN_PREIMAGE] >> METIS_TAC []) 966 >> POP_ORW 967 >> `FINITE (PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')} INTER (high CROSS low CROSS random))` 968 by METIS_TAC [FINITE_INTER, FINITE_CROSS] 969 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(PREIMAGE (f :('a, 'b, 'c, 'd) prog) 970 {f (s' :('a, 'b, 'c) prog_state)} INTER 971 PREIMAGE (L :('a, 'b, 'c, 'b) prog) {SND (FST s')} INTER 972 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS 973 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 974 >> `(\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')} INTER (high CROSS low CROSS random) 975 then (\s. (if s IN high CROSS low CROSS random then 1 else 0)) x else 0)) = 976 (\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')} INTER (high CROSS low CROSS random) 977 then 1 else 0))` 978 by METIS_TAC [IN_INTER] 979 >> POP_ORW 980 >> RW_TAC std_ss [REAL_SUM_IMAGE_EQ_CARD] 981 >> `high CROSS random = IMAGE (\x. (FST (FST x),SND x)) (high CROSS {SND (FST s')} CROSS random)` 982 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_CROSS, IN_IMAGE, IN_SING] 983 >> EQ_TAC >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `((FST x, SND (FST s')),SND x)` 984 >> RW_TAC std_ss [FST,SND,PAIR]) 985 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST, SND]) 986 >> POP_ORW 987 >> `(PREIMAGE f {f s'} INTER PREIMAGE L {SND (FST s')} INTER (high CROSS low CROSS random)) = 988 (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random))` 989 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, low_state_def, IN_CROSS] 990 >> METIS_TAC []) 991 >> POP_ORW 992 >> `INJ (\x. (FST (FST x),SND x)) (high CROSS {SND (FST s')} CROSS random) 993 (IMAGE (\x. (FST (FST x),SND x)) (high CROSS {SND (FST s')} CROSS random))` 994 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE, IN_SING, IN_CROSS] >> METIS_TAC [PAIR]) 995 >> RW_TAC std_ss [REAL_SUM_IMAGE_IMAGE, FINITE_CROSS, FINITE_SING, o_DEF] 996 >> Q.ABBREV_TAC `c = & (CARD (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random)))` 997 >> `(high CROSS {SND (FST s')} CROSS random) = 998 (PREIMAGE f {f s'} INTER 999 (high CROSS {SND (FST s')} CROSS random)) UNION 1000 ((high CROSS {SND (FST s')} CROSS random) DIFF 1001 (PREIMAGE f {f s'} INTER 1002 (high CROSS {SND (FST s')} CROSS random)))` 1003 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_UNION, IN_DIFF] >> DECIDE_TAC) 1004 >> POP_ORW 1005 >> `DISJOINT (PREIMAGE f {f s'} INTER 1006 (high CROSS {SND (FST s')} CROSS random)) 1007 ((high CROSS {SND (FST s')} CROSS random) DIFF 1008 (PREIMAGE f {f s'} INTER 1009 (high CROSS {SND (FST s')} CROSS random)))` 1010 by (RW_TAC std_ss [IN_DISJOINT, IN_INTER, IN_DIFF] >> DECIDE_TAC) 1011 >> RW_TAC std_ss [REAL_SUM_IMAGE_DISJOINT_UNION, FINITE_CROSS, FINITE_SING, FINITE_INTER, FINITE_DIFF] 1012 >> `FINITE (high CROSS {SND (FST s')} CROSS random DIFF 1013 PREIMAGE f {f s'} INTER 1014 (high CROSS {SND (FST s')} CROSS random))` 1015 by RW_TAC std_ss [FINITE_CROSS, FINITE_SING, FINITE_INTER, FINITE_DIFF] 1016 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `((high :'a state -> bool) CROSS 1017 {SND (FST (s' :('a, 'b, 'c) prog_state))} CROSS 1018 (random :'c state -> bool) DIFF 1019 PREIMAGE (f :('a, 'b, 'c, 'd) prog) {f s'} INTER 1020 (high CROSS {SND (FST s')} CROSS random))`) REAL_SUM_IMAGE_IN_IF] 1021 >> `(\x. (if x IN high CROSS {SND (FST s')} CROSS random DIFF 1022 PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random) then 1023 (\x. (if f ((FST (FST x),SND (FST s')),SND x) = f s' then 1 else 0)) x else 0)) = 1024 (\x. 0)` 1025 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_DIFF, IN_INTER, IN_CROSS, IN_SING, IN_PREIMAGE] 1026 >> RW_TAC real_ss [] >> METIS_TAC [PAIR]) 1027 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] 1028 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 1029 >> `FINITE (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random))` 1030 by RW_TAC std_ss [FINITE_INTER, FINITE_CROSS, FINITE_SING] 1031 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(PREIMAGE (f :('a, 'b, 'c, 'd) prog) 1032 {f (s' :('a, 'b, 'c) prog_state)} INTER 1033 ((high :'a state -> bool) CROSS {SND (FST s')} CROSS 1034 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 1035 >> `(\x. (if x IN PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random) then 1036 (\x. (if f ((FST (FST x),SND (FST s')),SND x) = f s' then 1 else 0)) x 1037 else 0)) = 1038 (\x. (if x IN PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS random) then 1039 1 else 0))` 1040 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_INTER, IN_SING, IN_CROSS, IN_PREIMAGE] 1041 >> RW_TAC std_ss [] 1042 >> METIS_TAC [PAIR]) 1043 >> POP_ORW 1044 >> Q.UNABBREV_TAC `c` 1045 >> RW_TAC std_ss [REAL_SUM_IMAGE_EQ_CARD]); 1046 1047 1048val unif_prog_space_visible_leakage_lemma1 = store_thm 1049 ("unif_prog_space_visible_leakage_lemma1", 1050 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\ 1051 ~((high CROSS low) CROSS random={}) ==> 1052 (SIGMA (\x. (\(x,z). 1053 joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * 1054 lg (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * 1055 & (CARD low * CARD random))) x) 1056 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))= 1057 SIGMA (\x. (\(x,z). 1058 ((1/(&(CARD high * CARD low * CARD random)))* 1059 (SIGMA (\h. if (f((h,FST z),SND z)=x) then 1 else 0) high)) * 1060 lg (((1/(&(CARD high * CARD low * CARD random)))* 1061 (SIGMA (\h. if (f((h,FST z),SND z)=x) then 1 else 0) high)) * 1062 & (CARD low * CARD random))) x) 1063 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)))``, 1064 RW_TAC std_ss [] 1065 >> `p_space (unif_prog_space high low random) = 1066 (high CROSS low CROSS random)` 1067 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 1068 >> `FINITE (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))` 1069 by METIS_TAC [IMAGE_FINITE, FINITE_CROSS] 1070 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE 1071 (\(s :('a, 'b, 'c) prog_state). 1072 ((f :('a, 'b, 'c, 'd) prog) s,SND (FST s),SND s)) 1073 ((high :'a state -> bool) CROSS 1074 (low :'b state -> bool) CROSS (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 1075 >> Suff `(\x. (if x IN IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) then 1076 (\x. (\(x,z). joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * 1077 lg (joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(x,z)} * & (CARD low * CARD random))) x) x 1078 else 0)) = 1079 (\x. (if x IN IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random) then 1080 (\x. (\(x,z). 1 / & (CARD high * CARD low * CARD random) * 1081 SIGMA (\h. (if f ((h,FST z),SND z) = x then 1 else 0)) high * 1082 lg (1 / & (CARD high * CARD low * CARD random) * 1083 SIGMA (\h. (if f ((h,FST z),SND z) = x then 1 else 0)) high * 1084 & (CARD low * CARD random))) x) x else 0))` 1085 >- RW_TAC std_ss [] 1086 >> ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_IMAGE, IN_CROSS] 1087 >> RW_TAC std_ss [] >> RW_TAC std_ss [] 1088 >> Q.ABBREV_TAC `j = joint_distribution (unif_prog_space high low random) f (\s. (L s,R s)) {(f s',(SND (FST s'),SND s'))}` 1089 >> Q.ABBREV_TAC `s = 1 / & (CARD high * CARD low * CARD random) * 1090 SIGMA (\h. (if f ((h,SND (FST s')),SND s') = f s' then 1 else 0)) high` 1091 >> Suff `j = s` 1092 >- RW_TAC std_ss [] 1093 >> Q.UNABBREV_TAC `j` >> Q.UNABBREV_TAC `s` 1094 >> RW_TAC std_ss [joint_distribution_def, unif_prog_space_def, unif_prog_dist_def, PROB, 1095 FINITE_CROSS, CARD_CROSS] 1096 >> `(\s. (if s IN high CROSS low CROSS random then 1097 1 / & (CARD high * CARD low * CARD random) else 0)) = 1098 (\s. (1 / & (CARD high * CARD low * CARD random)) * 1099 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)` 1100 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss []) 1101 >> POP_ORW 1102 >> RW_TAC std_ss [REAL_SUM_IMAGE_CMUL, FINITE_CROSS, FINITE_INTER] 1103 >> RW_TAC std_ss [REAL_EQ_LMUL] 1104 >> Cases_on `(1 / & (CARD high * CARD low * CARD random) = 0)` 1105 >> RW_TAC std_ss [] 1106 >> `PREIMAGE (\s. (f s,L s,R s)) {(f s',SND (FST s'),SND s')} = 1107 PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')}` 1108 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_SING, IN_PREIMAGE] >> METIS_TAC []) 1109 >> POP_ORW 1110 >> `FINITE (PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')} INTER (high CROSS low CROSS random))` 1111 by METIS_TAC [FINITE_INTER, FINITE_CROSS] 1112 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(PREIMAGE (f :('a, 'b, 'c, 'd) prog) 1113 {f (s' :('a, 'b, 'c) prog_state)} INTER 1114 PREIMAGE (\(s :('a, 'b, 'c) prog_state). (L s,R s)) {(SND (FST s'),SND s')} INTER 1115 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS 1116 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 1117 >> `(\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')} INTER (high CROSS low CROSS random) 1118 then (\s. (if s IN high CROSS low CROSS random then 1 else 0)) x else 0)) = 1119 (\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')} INTER (high CROSS low CROSS random) 1120 then 1 else 0))` 1121 by METIS_TAC [IN_INTER] 1122 >> POP_ORW 1123 >> RW_TAC std_ss [REAL_SUM_IMAGE_EQ_CARD] 1124 >> `(PREIMAGE f {f s'} INTER PREIMAGE (\s. (L s,R s)) {(SND (FST s'),SND s')} INTER (high CROSS low CROSS random)) = 1125 (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}))` 1126 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, low_state_def, random_state_def, IN_CROSS] 1127 >> METIS_TAC []) 1128 >> POP_ORW 1129 >> Q.ABBREV_TAC `c = CARD 1130 (PREIMAGE f {f s'} INTER 1131 (high CROSS {SND (FST s')} CROSS {SND s'}))` 1132 >> `high = IMAGE (FST o FST) (high CROSS {SND (FST s')} CROSS {SND s'})` 1133 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_CROSS, IN_IMAGE, IN_SING, o_DEF] 1134 >> EQ_TAC >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `((x, SND (FST s')),SND s')` 1135 >> RW_TAC std_ss [FST,SND,PAIR]) 1136 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST, SND]) 1137 >> POP_ORW 1138 >> `INJ (FST o FST) (high CROSS {SND (FST s')} CROSS {SND s'}) 1139 (IMAGE (FST o FST) (high CROSS {SND (FST s')} CROSS {SND s'}))` 1140 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE, IN_SING, IN_CROSS, o_DEF] >> METIS_TAC [PAIR]) 1141 >> RW_TAC std_ss [REAL_SUM_IMAGE_IMAGE, FINITE_CROSS, FINITE_SING, o_DEF] 1142 >> `(high CROSS {SND (FST s')} CROSS {SND s'}) = 1143 (PREIMAGE f {f s'} INTER 1144 (high CROSS {SND (FST s')} CROSS {SND s'})) UNION 1145 ((high CROSS {SND (FST s')} CROSS {SND s'}) DIFF 1146 (PREIMAGE f {f s'} INTER 1147 (high CROSS {SND (FST s')} CROSS {SND s'})))` 1148 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_UNION, IN_DIFF] >> DECIDE_TAC) 1149 >> POP_ORW 1150 >> `DISJOINT (PREIMAGE f {f s'} INTER 1151 (high CROSS {SND (FST s')} CROSS {SND s'})) 1152 ((high CROSS {SND (FST s')} CROSS {SND s'}) DIFF 1153 (PREIMAGE f {f s'} INTER 1154 (high CROSS {SND (FST s')} CROSS {SND s'})))` 1155 by (RW_TAC std_ss [IN_DISJOINT, IN_INTER, IN_DIFF] >> DECIDE_TAC) 1156 >> RW_TAC std_ss [REAL_SUM_IMAGE_DISJOINT_UNION, FINITE_CROSS, FINITE_SING, FINITE_INTER, FINITE_DIFF] 1157 >> `FINITE (high CROSS {SND (FST s')} CROSS {SND s'} DIFF 1158 PREIMAGE f {f s'} INTER 1159 (high CROSS {SND (FST s')} CROSS {SND s'}))` 1160 by RW_TAC std_ss [FINITE_CROSS, FINITE_SING, FINITE_INTER, FINITE_DIFF] 1161 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `((high :'a state -> bool) CROSS 1162 {SND (FST (s' :('a, 'b, 'c) prog_state))} CROSS 1163 ({SND (s' :('a, 'b, 'c) prog_state)}) DIFF 1164 PREIMAGE (f :('a, 'b, 'c, 'd) prog) {f s'} INTER 1165 (high CROSS {SND (FST s')} CROSS {SND (s' :('a, 'b, 'c) prog_state)}))`) REAL_SUM_IMAGE_IN_IF] 1166 >> `(\x. (if x IN high CROSS {SND (FST s')} CROSS {SND s'} DIFF 1167 PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}) then 1168 (\x. (if f ((FST (FST x),SND (FST s')),SND s') = f s' then 1 else 0)) x else 0)) = 1169 (\x. 0)` 1170 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_DIFF, IN_INTER, IN_CROSS, IN_SING, IN_PREIMAGE] 1171 >> RW_TAC real_ss [] >> METIS_TAC [PAIR]) 1172 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] 1173 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 1174 >> `FINITE (PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}))` 1175 by RW_TAC std_ss [FINITE_INTER, FINITE_CROSS, FINITE_SING] 1176 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(PREIMAGE (f :('a, 'b, 'c, 'd) prog) 1177 {f (s' :('a, 'b, 'c) prog_state)} INTER 1178 ((high :'a state -> bool) CROSS {SND (FST s')} CROSS 1179 {SND (s' :('a, 'b, 'c) prog_state)}))`) REAL_SUM_IMAGE_IN_IF] 1180 >> `(\x. (if x IN PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}) then 1181 (\x. (if f ((FST (FST x),SND (FST s')),SND s') = f s' then 1 else 0)) x 1182 else 0)) = 1183 (\x. (if x IN PREIMAGE f {f s'} INTER (high CROSS {SND (FST s')} CROSS {SND s'}) then 1184 1 else 0))` 1185 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_INTER, IN_SING, IN_CROSS, IN_PREIMAGE] 1186 >> RW_TAC std_ss [] 1187 >> METIS_TAC [PAIR]) 1188 >> POP_ORW 1189 >> Q.UNABBREV_TAC `c` 1190 >> RW_TAC std_ss [REAL_SUM_IMAGE_EQ_CARD]); 1191 1192 1193val unif_prog_space_leakage_lemma2 = store_thm 1194 ("unif_prog_space_leakage_lemma2", 1195 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\ 1196 ~((high CROSS low) CROSS random={}) ==> 1197 (SIGMA (\x. (\(x,y,z). 1198 joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 1199 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 1200 & (CARD high * CARD low))) x) 1201 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))= 1202 SIGMA (\x. (\(out,h,l). 1203 ((1/(&(CARD high * CARD low * CARD random)))* 1204 (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) * 1205 lg (((1/(&(CARD high * CARD low * CARD random)))* 1206 (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) * 1207 & (CARD high * CARD low))) x) 1208 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))``, 1209 RW_TAC std_ss [] 1210 >> `p_space (unif_prog_space high low random) = 1211 (high CROSS low CROSS random)` 1212 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 1213 >> `FINITE (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))` 1214 by METIS_TAC [IMAGE_FINITE, FINITE_CROSS] 1215 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE 1216 (\(s :('a, 'b, 'c) prog_state). 1217 ((f :('a, 'b, 'c, 'd) prog) s,FST s)) 1218 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS 1219 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 1220 >> Suff `(\x. (if x IN IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) then 1221 (\x. (\(x,y,z). joint_distribution (unif_prog_space high low random) f 1222 (\x. (H x,L x)) {(x,y,z)} * 1223 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 1224 & (CARD high * CARD low))) x) x else 0)) = 1225 (\x. (if x IN IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random) then 1226 (\x. (\(out,h,l). 1227 1 / & (CARD high * CARD low * CARD random) * 1228 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random * 1229 lg (1 / & (CARD high * CARD low * CARD random) * 1230 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) 1231 random * & (CARD high * CARD low))) x) x else 0))` 1232 >- RW_TAC std_ss [] 1233 >> ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_IMAGE, IN_CROSS] 1234 >> RW_TAC std_ss [] >> `FST s' = (FST(FST s'),SND(FST s'))` by RW_TAC std_ss [PAIR] 1235 >> POP_ORW >> RW_TAC std_ss [] 1236 >> Q.ABBREV_TAC `j = joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(f s',FST s')}` 1237 >> Q.ABBREV_TAC `s = 1 / & (CARD high * CARD low * CARD random) * 1238 SIGMA (\r. (if f (FST s',r) = f s' then 1 else 0)) random` 1239 >> Suff `j = s` 1240 >- RW_TAC std_ss [] 1241 >> Q.UNABBREV_TAC `j` >> Q.UNABBREV_TAC `s` 1242 >> RW_TAC std_ss [joint_distribution_def, unif_prog_space_def, unif_prog_dist_def, PROB, 1243 FINITE_CROSS, CARD_CROSS] 1244 >> `(\s. (if s IN high CROSS low CROSS random then 1245 1 / & (CARD high * CARD low * CARD random) else 0)) = 1246 (\s. (1 / & (CARD high * CARD low * CARD random)) * 1247 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)` 1248 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss []) 1249 >> POP_ORW 1250 >> RW_TAC std_ss [REAL_SUM_IMAGE_CMUL, FINITE_CROSS, FINITE_INTER] 1251 >> RW_TAC std_ss [REAL_EQ_LMUL] 1252 >> Cases_on `(1 / & (CARD high * CARD low * CARD random) = 0)` 1253 >> RW_TAC std_ss [] 1254 >> `PREIMAGE (\x. (f x,H x,L x)) {(f s',FST s')} = 1255 PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'}` 1256 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_SING, IN_PREIMAGE] >> METIS_TAC []) 1257 >> POP_ORW 1258 >> `FINITE (PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER (high CROSS low CROSS random))` 1259 by METIS_TAC [FINITE_INTER, FINITE_CROSS] 1260 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(PREIMAGE (f :('a, 'b, 'c, 'd) prog) 1261 {f (s' :('a, 'b, 'c) prog_state)} INTER 1262 PREIMAGE (\(x :('a, 'b, 'c) prog_state). (H x,L x)) 1263 {FST s'} INTER 1264 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS 1265 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 1266 >> `(\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1267 (high CROSS low CROSS random) 1268 then (\s. (if s IN high CROSS low CROSS random then 1 else 0)) x else 0)) = 1269 (\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1270 (high CROSS low CROSS random) 1271 then 1 else 0))` 1272 by METIS_TAC [IN_INTER] 1273 >> POP_ORW 1274 >> RW_TAC std_ss [REAL_SUM_IMAGE_EQ_CARD] 1275 >> `random = IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)` 1276 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_CROSS, IN_IMAGE, IN_SING] 1277 >> EQ_TAC >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `((FST (FST s'), SND (FST s')), x)` 1278 >> RW_TAC std_ss [FST,SND,PAIR]) 1279 >> RW_TAC std_ss [] >> RW_TAC std_ss [FST, SND]) 1280 >> POP_ORW 1281 >> `(PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER (high CROSS low CROSS random)) = 1282 (PREIMAGE f {f s'} INTER ({FST (FST s')} CROSS {SND (FST s')} CROSS random))` 1283 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_PREIMAGE, IN_SING, 1284 high_state_def, low_state_def, IN_CROSS] 1285 >> METIS_TAC [PAIR]) 1286 >> POP_ORW 1287 >> `INJ SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random) 1288 (IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random))` 1289 by (RW_TAC std_ss [INJ_DEF, IN_IMAGE, IN_SING, IN_CROSS] >> METIS_TAC [PAIR]) 1290 >> RW_TAC std_ss [REAL_SUM_IMAGE_IMAGE, FINITE_CROSS, FINITE_SING, o_DEF] 1291 >> Q.ABBREV_TAC `c = & (CARD (PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1292 (high CROSS low CROSS 1293 IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random))))` 1294 >> `({FST (FST s')} CROSS {SND (FST s')} CROSS random) = 1295 (PREIMAGE f {f s'} INTER 1296 PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1297 (high CROSS low CROSS 1298 IMAGE SND 1299 ({FST (FST s')} CROSS {SND (FST s')} CROSS 1300 random))) UNION 1301 (({FST (FST s')} CROSS {SND (FST s')} CROSS random) DIFF 1302 (PREIMAGE f {f s'} INTER 1303 PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1304 (high CROSS low CROSS 1305 IMAGE SND 1306 ({FST (FST s')} CROSS {SND (FST s')} CROSS 1307 random))))` 1308 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_UNION, IN_DIFF, IN_CROSS, IN_SING, 1309 IN_PREIMAGE, low_state_def, high_state_def, IN_IMAGE, 1310 SND] >> METIS_TAC []) 1311 >> POP_ORW 1312 >> `DISJOINT (PREIMAGE f {f s'} INTER 1313 PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1314 (high CROSS low CROSS 1315 IMAGE SND 1316 ({FST (FST s')} CROSS {SND (FST s')} CROSS 1317 random))) 1318 (({FST (FST s')} CROSS {SND (FST s')} CROSS random) DIFF 1319 (PREIMAGE f {f s'} INTER 1320 PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1321 (high CROSS low CROSS 1322 IMAGE SND 1323 ({FST (FST s')} CROSS {SND (FST s')} CROSS 1324 random))))` 1325 by (RW_TAC std_ss [IN_DISJOINT, IN_INTER, IN_DIFF] >> DECIDE_TAC) 1326 >> `FINITE (PREIMAGE f {f s'} INTER 1327 PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1328 (high CROSS low CROSS 1329 IMAGE SND 1330 ({FST (FST s')} CROSS {SND (FST s')} CROSS random)))` 1331 by METIS_TAC [FINITE_CROSS, FINITE_SING, FINITE_INTER, FINITE_DIFF, IMAGE_FINITE] 1332 >> `FINITE ({FST (FST s')} CROSS {SND (FST s')} CROSS random DIFF 1333 PREIMAGE f {f s'} INTER 1334 PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1335 (high CROSS low CROSS 1336 IMAGE SND 1337 ({FST (FST s')} CROSS {SND (FST s')} CROSS random)))` 1338 by METIS_TAC [FINITE_CROSS, FINITE_SING, FINITE_INTER, FINITE_DIFF, IMAGE_FINITE] 1339 >> RW_TAC std_ss [REAL_SUM_IMAGE_DISJOINT_UNION] 1340 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `({FST (FST (s' :('a, 'b, 'c) prog_state))} CROSS 1341 {SND (FST s')} CROSS (random :'c state -> bool) DIFF 1342 PREIMAGE (f :('a, 'b, 'c, 'd) prog) {f s'} INTER 1343 PREIMAGE (\(x :('a, 'b, 'c) prog_state). (H x,L x)) 1344 {FST s'} INTER 1345 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS 1346 IMAGE (SND :('a, 'b, 'c, 'c) prog) 1347 ({FST (FST s')} CROSS {SND (FST s')} CROSS random)))`) REAL_SUM_IMAGE_IN_IF] 1348 >> `(\x. (if x IN {FST (FST s')} CROSS {SND (FST s')} CROSS random DIFF 1349 PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1350 (high CROSS low CROSS 1351 IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)) then 1352 (\x. (if f (FST s',SND x) = f s' then 1 else 0)) x else 0)) = 1353 (\x. 0)` 1354 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_DIFF, IN_INTER, IN_CROSS, IN_SING, IN_PREIMAGE, 1355 IN_IMAGE, SND, high_state_def, low_state_def] 1356 >> RW_TAC real_ss [] >> METIS_TAC [PAIR]) 1357 >> RW_TAC real_ss [REAL_SUM_IMAGE_0] 1358 >> NTAC 2 (POP_ASSUM (K ALL_TAC)) 1359 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(PREIMAGE (f :('a, 'b, 'c, 'd) prog) 1360 {f (s' :('a, 'b, 'c) prog_state)} INTER 1361 PREIMAGE (\(x :('a, 'b, 'c) prog_state). (H x,L x)) 1362 {FST s'} INTER 1363 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS 1364 IMAGE (SND :('a, 'b, 'c, 'c) prog) 1365 ({FST (FST s')} CROSS {SND (FST s')} CROSS 1366 (random :'c state -> bool))))`) REAL_SUM_IMAGE_IN_IF] 1367 >> `(\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1368 (high CROSS low CROSS 1369 IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)) then 1370 (\x. (if f (FST s',SND x) = f s' then 1 else 0)) x 1371 else 0)) = 1372 (\x. (if x IN PREIMAGE f {f s'} INTER PREIMAGE (\x. (H x,L x)) {FST s'} INTER 1373 (high CROSS low CROSS 1374 IMAGE SND ({FST (FST s')} CROSS {SND (FST s')} CROSS random)) then 1375 1 else 0))` 1376 by (ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_INTER, IN_SING, IN_CROSS, IN_PREIMAGE, 1377 IN_IMAGE, SND, high_state_def, low_state_def] 1378 >> RW_TAC std_ss [] 1379 >> METIS_TAC [PAIR]) 1380 >> POP_ORW 1381 >> Q.UNABBREV_TAC `c` 1382 >> RW_TAC std_ss [REAL_SUM_IMAGE_EQ_CARD]); 1383 1384 1385val unif_prog_space_visible_leakage_lemma2 = store_thm 1386 ("unif_prog_space_visible_leakage_lemma2", 1387 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\ 1388 ~((high CROSS low) CROSS random={}) ==> 1389 (SIGMA (\x. (\(x,y,z). 1390 joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} * 1391 lg (joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} * 1392 & (CARD high * CARD low * CARD random))) x) 1393 (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random))= 1394 SIGMA (\x. (\(out,h,l,r). 1395 ((1/(&(CARD high * CARD low * CARD random)))* 1396 (if (f((h,l),r)=out) then 1 else 0)) * 1397 lg (((1/(&(CARD high * CARD low * CARD random)))* 1398 (if (f((h,l),r)=out) then 1 else 0)) * 1399 & (CARD high * CARD low * CARD random))) x) 1400 (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random)))``, 1401 RW_TAC std_ss [] 1402 >> `p_space (unif_prog_space high low random) = 1403 (high CROSS low CROSS random)` 1404 by RW_TAC std_ss [unif_prog_space_def, PSPACE] 1405 >> `FINITE (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random))` 1406 by METIS_TAC [IMAGE_FINITE, FINITE_CROSS] 1407 >> ONCE_REWRITE_TAC [(UNDISCH o Q.ISPEC `(IMAGE 1408 (\(s :('a, 'b, 'c) prog_state). 1409 ((f :('a, 'b, 'c, 'd) prog) s,FST (FST s),SND (FST s), 1410 SND s)) 1411 ((high :'a state -> bool) CROSS (low :'b state -> bool) CROSS 1412 (random :'c state -> bool)))`) REAL_SUM_IMAGE_IN_IF] 1413 >> Suff `(\x. (if x IN IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) then 1414 (\x. (\(x,y,z). joint_distribution (unif_prog_space high low random) f 1415 (\s. (H s,L s,R s)) {(x,y,z)} * 1416 lg (joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(x,y,z)} * 1417 & (CARD high * CARD low * CARD random))) x) x else 0)) = 1418 (\x. (if x IN IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) (high CROSS low CROSS random) then 1419 (\x. (\(out,h,l,r). 1420 1 / & (CARD high * CARD low * CARD random) * 1421 (if f ((h,l),r) = out then 1 else 0) * 1422 lg (1 / & (CARD high * CARD low * CARD random) * 1423 (if f ((h,l),r) = out then 1 else 0) * & (CARD high * CARD low * CARD random))) x) x else 0))` 1424 >- RW_TAC std_ss [] 1425 >> ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [IN_IMAGE, IN_CROSS] 1426 >> RW_TAC std_ss [] >> `FST s' = (FST(FST s'),SND(FST s'))` by RW_TAC std_ss [PAIR] 1427 >> POP_ORW >> RW_TAC real_ss [] 1428 >> Suff `joint_distribution (unif_prog_space high low random) f (\s. (H s,L s,R s)) {(f s',FST (FST s'),SND (FST s'),SND s')} = 1429 1 / & (CARD high * CARD low * CARD random)` 1430 >- RW_TAC std_ss [] 1431 >> RW_TAC std_ss [joint_distribution_def, unif_prog_space_def, unif_prog_dist_def, PROB, 1432 FINITE_CROSS, CARD_CROSS] 1433 >> `(\s. (if s IN high CROSS low CROSS random then 1434 1 / & (CARD high * CARD low * CARD random) else 0)) = 1435 (\s. (1 / & (CARD high * CARD low * CARD random)) * 1436 (\s. if s IN high CROSS low CROSS random then 1 else 0) s)` 1437 by (RW_TAC std_ss [FUN_EQ_THM] >> RW_TAC real_ss []) 1438 >> POP_ORW 1439 >> RW_TAC std_ss [REAL_SUM_IMAGE_CMUL, FINITE_CROSS, FINITE_INTER] 1440 >> `PREIMAGE (\s. (f s,H s,L s,R s)) 1441 {(f s',FST (FST s'),SND (FST s'),SND s')} = 1442 PREIMAGE f {f s'} INTER 1443 PREIMAGE (\s. (H s,L s,R s)) 1444 {(FST (FST s'),SND (FST s'),SND s')}` 1445 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_SING, IN_PREIMAGE] >> METIS_TAC []) 1446 >> POP_ORW 1447 >> Q.ABBREV_TAC `foo = 1 / & (CARD high * CARD low * CARD random) * 1448 SIGMA (\s. (if s IN high CROSS low CROSS random then 1 else 0)) 1449 (PREIMAGE f {f s'} INTER 1450 PREIMAGE (\s. (H s,L s,R s)) 1451 {(FST (FST s'),SND (FST s'),SND s')} INTER 1452 (high CROSS low CROSS random))` 1453 >> `1 / & (CARD high * CARD low * CARD random) = 1 / & (CARD high * CARD low * CARD random) * 1` 1454 by RW_TAC real_ss [] 1455 >> POP_ORW >> Q.UNABBREV_TAC `foo` 1456 >> RW_TAC std_ss [REAL_EQ_LMUL] 1457 >> Cases_on `(1 / & (CARD high * CARD low * CARD random) = 0)` 1458 >> RW_TAC std_ss [] 1459 >> `(PREIMAGE f {f s'} INTER PREIMAGE (\s. (H s,L s,R s)) {(FST (FST s'),SND (FST s'),SND s')} INTER 1460 (high CROSS low CROSS random)) = {s'}` 1461 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [IN_INTER, IN_SING, IN_PREIMAGE, high_state_def, 1462 low_state_def, random_state_def, IN_CROSS] 1463 >> METIS_TAC [PAIR, FST, SND]) 1464 >> RW_TAC std_ss [REAL_SUM_IMAGE_SING, IN_CROSS]); 1465 1466 1467val unif_prog_space_leakage_lemma3 = store_thm 1468 ("unif_prog_space_leakage_lemma3", 1469 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\ 1470 ~((high CROSS low) CROSS random={}) ==> 1471 (SIGMA (\x. (\(x,z). 1472 joint_distribution (unif_prog_space high low random) f L {(x,z)} * 1473 lg (joint_distribution (unif_prog_space high low random) f L {(x,z)} * 1474 & (CARD low))) x) 1475 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))= 1476 (1/(&(CARD high * CARD low * CARD random)))* 1477 SIGMA (\x. (\(out,l). 1478 ((SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) 1479 (high CROSS random))) * 1480 lg (((1/(&(CARD high * CARD random)))* 1481 (SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) 1482 (high CROSS random))))) x) 1483 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)))``, 1484 RW_TAC std_ss [unif_prog_space_leakage_lemma1] 1485 >> `1 / & (CARD high * CARD low * CARD random) * 1486 SIGMA (\x. 1487 (\(out,l). 1488 SIGMA (\(h,r). (if f ((h,l),r) = out then 1 else 0)) 1489 (high CROSS random) * 1490 lg 1491 (1 / & (CARD high * CARD random) * 1492 SIGMA (\(h,r). (if f ((h,l),r) = out then 1 else 0)) 1493 (high CROSS random))) x) 1494 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random)) = 1495 SIGMA (\x. 1 / & (CARD high * CARD low * CARD random) * 1496 (\(out,l). 1497 SIGMA (\(h,r). (if f ((h,l),r) = out then 1 else 0)) 1498 (high CROSS random) * 1499 lg 1500 (1 / & (CARD high * CARD random) * 1501 SIGMA (\(h,r). (if f ((h,l),r) = out then 1 else 0)) 1502 (high CROSS random))) x) 1503 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))` 1504 by RW_TAC std_ss [IMAGE_FINITE, FINITE_CROSS, GSYM REAL_SUM_IMAGE_CMUL] 1505 >> POP_ORW 1506 >> Suff `(\x. 1507 (\(x,z). 1508 1 / & (CARD high * CARD low * CARD random) * 1509 SIGMA (\(h,r). (if f ((h,z),r) = x then 1 else 0)) 1510 (high CROSS random) * 1511 lg 1512 (1 / & (CARD high * CARD low * CARD random) * 1513 SIGMA (\(h,r). (if f ((h,z),r) = x then 1 else 0)) 1514 (high CROSS random) * & (CARD low))) x) = 1515 (\x. 1516 1 / & (CARD high * CARD low * CARD random) * 1517 (\(out,l). 1518 SIGMA (\(h,r). (if f ((h,l),r) = out then 1 else 0)) 1519 (high CROSS random) * 1520 lg 1521 (1 / & (CARD high * CARD random) * 1522 SIGMA (\(h,r). (if f ((h,l),r) = out then 1 else 0)) 1523 (high CROSS random))) x)` 1524 >- RW_TAC std_ss [] 1525 >> ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [] 1526 >> `x = (FST x, SND x)` by RW_TAC std_ss [PAIR] 1527 >> POP_ORW >> RW_TAC std_ss [] 1528 >> Suff `1 / & (CARD high * CARD low * CARD random) * 1529 SIGMA (\(h,r). (if f ((h,SND x),r) = FST x then 1 else 0)) 1530 (high CROSS random) * & (CARD low) = 1531 1 / & (CARD high * CARD random) * 1532 SIGMA (\(h,r). (if f ((h,SND x),r) = FST x then 1 else 0)) 1533 (high CROSS random)` 1534 >- RW_TAC std_ss [REAL_MUL_ASSOC] 1535 >> Suff `1 / & (CARD high * CARD random) = 1536 & (CARD low) * (1 / & (CARD high * CARD low * CARD random))` 1537 >- (RW_TAC std_ss [] >> REAL_ARITH_TAC) 1538 >> RW_TAC real_ss [real_div] 1539 >> RW_TAC std_ss [GSYM REAL_MUL] 1540 >> `& (CARD high) * & (CARD low) * & (CARD random) = 1541 (& (CARD high) * & (CARD random)) * & (CARD low)` 1542 by METIS_TAC [REAL_MUL_ASSOC, REAL_MUL_COMM] 1543 >> POP_ORW 1544 >> `inv (& (CARD high) * & (CARD random) * & (CARD low)) = 1545 inv (& (CARD high) * & (CARD random)) * inv (& (CARD low))` 1546 by (MATCH_MP_TAC REAL_INV_MUL 1547 >> RW_TAC real_ss [CARD_EQ_0, REAL_ENTIRE] 1548 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1549 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]) 1550 >> POP_ORW 1551 >> `& (CARD low) * (inv (& (CARD high) * & (CARD random)) * inv (& (CARD low))) = 1552 ((inv (& (CARD low))) * ((& (CARD low)))) * (inv (& (CARD high) * & (CARD random)))` 1553 by REAL_ARITH_TAC 1554 >> POP_ORW 1555 >> Suff `inv (& (CARD low)) * & (CARD low) = 1` >- RW_TAC real_ss [] 1556 >> MATCH_MP_TAC REAL_MUL_LINV 1557 >> RW_TAC real_ss [CARD_EQ_0] 1558 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1559 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]); 1560 1561 1562val unif_prog_space_visible_leakage_lemma3 = store_thm 1563 ("unif_prog_space_visible_leakage_lemma3", 1564 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\ 1565 ~((high CROSS low) CROSS random={}) ==> 1566 (SIGMA 1567 (\x. 1568 (\(x,z). 1569 joint_distribution (unif_prog_space high low random) f 1570 (\s. (L s,R s)) {(x,z)} * 1571 lg 1572 (joint_distribution (unif_prog_space high low random) f 1573 (\s. (L s,R s)) {(x,z)} * 1574 & (CARD low * CARD random))) x) 1575 (IMAGE (\s. (f s,SND (FST s),SND s)) 1576 (high CROSS low CROSS random)) = 1577 (1/(&(CARD high * CARD low * CARD random)))* 1578 SIGMA (\x. (\(out,(l,r)). 1579 ((SIGMA (\h. if (f((h,l),r)=out) then 1 else 0) high)) * 1580 lg (((1/(&(CARD high)))* 1581 (SIGMA (\h. if (f((h,l),r)=out) then 1 else 0) high)))) x) 1582 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)))``, 1583 RW_TAC std_ss [unif_prog_space_visible_leakage_lemma1] 1584 >> `1 / & (CARD high * CARD low * CARD random) * 1585 SIGMA 1586 (\x. 1587 (\(out,l,r). 1588 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high * 1589 lg 1590 (1 / & (CARD high) * 1591 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high)) x) 1592 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random)) = 1593 SIGMA 1594 (\x. 1 / & (CARD high * CARD low * CARD random) * 1595 (\(out,l,r). 1596 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high * 1597 lg 1598 (1 / & (CARD high) * 1599 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high)) x) 1600 (IMAGE (\s. (f s,SND (FST s),SND s)) (high CROSS low CROSS random))` 1601 by RW_TAC std_ss [IMAGE_FINITE, FINITE_CROSS, GSYM REAL_SUM_IMAGE_CMUL] 1602 >> POP_ORW 1603 >> Suff `(\x. 1604 (\(x,z). 1605 1 / & (CARD high * CARD low * CARD random) * 1606 SIGMA (\h. (if f ((h,FST z),SND z) = x then 1 else 0)) high * 1607 lg 1608 (1 / & (CARD high * CARD low * CARD random) * 1609 SIGMA (\h. (if f ((h,FST z),SND z) = x then 1 else 0)) high * 1610 & (CARD low * CARD random))) x) = 1611 (\x. 1612 1 / & (CARD high * CARD low * CARD random) * 1613 (\(out,l,r). 1614 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high * 1615 lg 1616 (1 / & (CARD high) * 1617 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high)) x)` 1618 >- RW_TAC std_ss [] 1619 >> ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [] 1620 >> `x = (FST x, SND x)` by RW_TAC std_ss [PAIR] 1621 >> POP_ORW >> RW_TAC std_ss [] 1622 >> `SND x = (FST (SND x), SND (SND x))` by RW_TAC std_ss [PAIR] 1623 >> POP_ORW >> RW_TAC std_ss [] 1624 >> Suff `1 / & (CARD high * CARD low * CARD random) * 1625 SIGMA 1626 (\h. (if f ((h,FST (SND x)),SND (SND x)) = FST x then 1 else 0)) 1627 high * & (CARD low * CARD random) = 1628 1 / & (CARD high) * 1629 SIGMA 1630 (\h. (if f ((h,FST (SND x)),SND (SND x)) = FST x then 1 else 0)) 1631 high` 1632 >- RW_TAC std_ss [REAL_MUL_ASSOC] 1633 >> Suff `1 / & (CARD high) = 1634 & (CARD low * CARD random) * (1 / & (CARD high * CARD low * CARD random))` 1635 >- (RW_TAC std_ss [] >> REAL_ARITH_TAC) 1636 >> RW_TAC real_ss [real_div] 1637 >> RW_TAC std_ss [GSYM REAL_MUL] 1638 >> `& (CARD high) * & (CARD low) * & (CARD random) = 1639 & (CARD high) * (& (CARD low) * & (CARD random))` 1640 by METIS_TAC [REAL_MUL_ASSOC, REAL_MUL_COMM] 1641 >> POP_ORW 1642 >> `inv (& (CARD high) * (& (CARD low) * & (CARD random))) = 1643 inv (& (CARD high)) * inv(& (CARD low) * & (CARD random))` 1644 by (MATCH_MP_TAC REAL_INV_MUL 1645 >> RW_TAC real_ss [CARD_EQ_0, REAL_ENTIRE] 1646 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1647 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]) 1648 >> POP_ORW 1649 >> `& (CARD low) * & (CARD random) * 1650 (inv (& (CARD high)) * inv (& (CARD low) * & (CARD random))) = 1651 inv (& (CARD high)) * (inv (& (CARD low) * & (CARD random) ) * (& (CARD low) * & (CARD random)) )` 1652 by REAL_ARITH_TAC 1653 >> POP_ORW 1654 >> Suff `(inv (& (CARD low) * & (CARD random)) * 1655 (& (CARD low) * & (CARD random))) = 1` >- RW_TAC real_ss [] 1656 >> `inv (& (CARD low) * & (CARD random)) * & (CARD low) * & (CARD random) = 1657 (inv (& (CARD low) * & (CARD random))) * (& (CARD low) * & (CARD random))` 1658 by REAL_ARITH_TAC 1659 >> POP_ORW 1660 >> MATCH_MP_TAC REAL_MUL_LINV 1661 >> RW_TAC real_ss [CARD_EQ_0] 1662 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1663 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]); 1664 1665 1666val unif_prog_space_leakage_lemma4 = store_thm 1667 ("unif_prog_space_leakage_lemma4", 1668 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\ 1669 ~((high CROSS low) CROSS random={}) ==> 1670 (SIGMA (\x. (\(x,y,z). 1671 joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 1672 lg (joint_distribution (unif_prog_space high low random) f (\x. (H x,L x)) {(x,y,z)} * 1673 & (CARD high * CARD low))) x) 1674 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))= 1675 (1/(&(CARD high * CARD low * CARD random)))* 1676 SIGMA (\x. (\(out,h,l). 1677 ((SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) * 1678 lg (((1/(&(CARD random)))* 1679 (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)))) x) 1680 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)))``, 1681 RW_TAC std_ss [unif_prog_space_leakage_lemma2] 1682 >> `1 / & (CARD high * CARD low * CARD random) * 1683 SIGMA 1684 (\x. (\(out,h,l). 1685 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random * 1686 lg 1687 (1 / & (CARD random) * 1688 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random)) x) 1689 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) = 1690 SIGMA 1691 (\x. (1 / & (CARD high * CARD low * CARD random)) * (\(out,h,l). 1692 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random * 1693 lg 1694 (1 / & (CARD random) * 1695 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random)) x) 1696 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random))` 1697 by RW_TAC std_ss [IMAGE_FINITE, FINITE_CROSS, GSYM REAL_SUM_IMAGE_CMUL] 1698 >> POP_ORW 1699 >> Suff `(\x. 1700 (\(out,h,l). 1701 1 / & (CARD high * CARD low * CARD random) * 1702 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random * 1703 lg 1704 (1 / & (CARD high * CARD low * CARD random) * 1705 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random * 1706 & (CARD high * CARD low))) x) = 1707 (\x. 1708 1 / & (CARD high * CARD low * CARD random) * 1709 (\(out,h,l). 1710 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random * 1711 lg 1712 (1 / & (CARD random) * 1713 SIGMA (\r. (if f ((h,l),r) = out then 1 else 0)) random)) x)` 1714 >- RW_TAC std_ss [] 1715 >> ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [] 1716 >> `x = (FST x, FST(SND x), SND(SND x))` by RW_TAC std_ss [PAIR] 1717 >> POP_ORW >> RW_TAC std_ss [] 1718 >> Suff `1 / & (CARD high * CARD low * CARD random) * 1719 SIGMA (\r. (if f (SND x,r) = FST x then 1 else 0)) random * 1720 & (CARD high * CARD low) = 1721 1 / & (CARD random) * 1722 SIGMA (\r. (if f (SND x,r) = FST x then 1 else 0)) random` 1723 >- RW_TAC std_ss [REAL_MUL_ASSOC] 1724 >> Suff `1 / & (CARD random) = 1725 & (CARD high * CARD low) * (1 / & (CARD high * CARD low * CARD random))` 1726 >- (RW_TAC std_ss [] >> REAL_ARITH_TAC) 1727 >> RW_TAC real_ss [real_div] 1728 >> RW_TAC std_ss [GSYM REAL_MUL] 1729 >> `& (CARD high) * & (CARD low) * & (CARD random) = 1730 (& (CARD high) * & (CARD low)) * & (CARD random)` 1731 by METIS_TAC [REAL_MUL_ASSOC, REAL_MUL_COMM] 1732 >> POP_ORW 1733 >> `inv (& (CARD high) * & (CARD low) * & (CARD random)) = 1734 inv (& (CARD high) * & (CARD low)) * inv (& (CARD random))` 1735 by (MATCH_MP_TAC REAL_INV_MUL 1736 >> RW_TAC real_ss [CARD_EQ_0, REAL_ENTIRE] 1737 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1738 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]) 1739 >> POP_ORW 1740 >> Suff `(& (CARD high) * & (CARD low)) * inv (& (CARD high) * & (CARD low)) = 1` 1741 >- METIS_TAC [REAL_MUL_ASSOC, REAL_MUL_COMM, REAL_MUL_LID] 1742 >> MATCH_MP_TAC REAL_MUL_RINV 1743 >> RW_TAC real_ss [CARD_EQ_0] 1744 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1745 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]); 1746 1747 1748val unif_prog_space_visible_leakage_lemma4 = store_thm 1749 ("unif_prog_space_visible_leakage_lemma4", 1750 ``!high low random (f :('a, 'b, 'c, 'd) prog). FINITE high /\ FINITE low /\ FINITE random /\ 1751 ~((high CROSS low) CROSS random={}) ==> 1752 (SIGMA 1753 (\x. 1754 (\(x,y,z). 1755 joint_distribution (unif_prog_space high low random) f 1756 (\s. (H s,L s,R s)) {(x,y,z)} * 1757 lg 1758 (joint_distribution (unif_prog_space high low random) f 1759 (\s. (H s,L s,R s)) {(x,y,z)} * 1760 & (CARD high * CARD low * CARD random))) x) 1761 (IMAGE (\s. (f s,FST (FST s),SND (FST s),SND s)) 1762 (high CROSS low CROSS random)) = 1763 0)``, 1764 RW_TAC std_ss [unif_prog_space_visible_leakage_lemma2] 1765 >> Suff `(\x. 1766 (\(out,h,l,r). 1767 1 / & (CARD high * CARD low * CARD random) * 1768 (if f ((h,l),r) = out then 1 else 0) * 1769 lg 1770 (1 / & (CARD high * CARD low * CARD random) * 1771 (if f ((h,l),r) = out then 1 else 0) * 1772 & (CARD high * CARD low * CARD random))) x) = (\x. 0)` 1773 >- RW_TAC std_ss [REAL_SUM_IMAGE_0, IMAGE_FINITE, FINITE_CROSS] 1774 >> ONCE_REWRITE_TAC [FUN_EQ_THM] >> RW_TAC std_ss [] 1775 >> `x = (FST x, (FST(SND x), (FST(SND(SND x)),SND(SND(SND x)))))` by RW_TAC std_ss [PAIR] 1776 >> POP_ORW >> RW_TAC real_ss [real_div] 1777 >> Suff `inv (& (CARD high * CARD low * CARD random)) * 1778 & (CARD high * CARD low * CARD random) = 1` 1779 >- RW_TAC real_ss [lg_1] 1780 >> MATCH_MP_TAC REAL_MUL_LINV 1781 >> RW_TAC real_ss [CARD_EQ_0] 1782 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 1783 >> FULL_SIMP_TAC std_ss [CROSS_EMPTY]); 1784 1785 1786val unif_prog_space_leakage_computation_reduce = store_thm 1787 ("unif_prog_space_leakage_computation_reduce", 1788 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 1789 ~((high CROSS low) CROSS random={}) ==> 1790 (leakage (unif_prog_space high low random) f = 1791 (1/(&(CARD high * CARD low * CARD random)))* 1792 (SIGMA (\x. (\(out,h,l). 1793 ((SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) * 1794 lg (((1/(&(CARD random)))* 1795 (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)))) x) 1796 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) - 1797 SIGMA (\x. (\(out,l). 1798 ((SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) 1799 (high CROSS random))) * 1800 lg (((1/(&(CARD high * CARD random)))* 1801 (SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) 1802 (high CROSS random))))) x) 1803 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))))``, 1804 RW_TAC std_ss [unif_prog_space_leakage_reduce, unif_prog_space_leakage_lemma3, 1805 unif_prog_space_leakage_lemma4, REAL_SUB_LDISTRIB]); 1806 1807 1808val unif_prog_space_visible_leakage_computation_reduce = store_thm 1809 ("unif_prog_space_visible_leakage_computation_reduce", 1810 ``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 1811 ~((high CROSS low) CROSS random={}) ==> 1812 (visible_leakage (unif_prog_space high low random) f = 1813 ~(1 / & (CARD high * CARD low * CARD random) * 1814 SIGMA 1815 (\x. 1816 (\(out,l,r). 1817 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high * 1818 lg 1819 (1 / & (CARD high) * 1820 SIGMA (\h. (if f ((h,l),r) = out then 1 else 0)) high)) 1821 x) 1822 (IMAGE (\s. (f s,SND (FST s),SND s)) 1823 (high CROSS low CROSS random))))``, 1824 RW_TAC real_ss [unif_prog_space_visible_leakage_reduce, unif_prog_space_visible_leakage_lemma3, 1825 unif_prog_space_visible_leakage_lemma4, REAL_SUB_LDISTRIB, REAL_SUB_LZERO]); 1826 1827 1828val unif_prog_space_leakage_LIST_TO_SET_computation_reduce = store_thm 1829 ("unif_prog_space_leakage_LIST_TO_SET_computation_reduce", 1830 ``!high low random f. ALL_DISTINCT high /\ ALL_DISTINCT low /\ ALL_DISTINCT random /\ 1831 ~(high = []) /\ ~(low = []) /\ ~(random = []) ==> 1832 (leakage (unif_prog_space (LIST_TO_SET high) (LIST_TO_SET low) (LIST_TO_SET random)) f = 1833 (1/(&(LENGTH high * LENGTH low * LENGTH random)))* 1834 ((REAL_SUM (MAP (\x. (\(out,h,l). (\s. s * lg ((1/(&(LENGTH random)))*s)) 1835 (REAL_SUM (MAP (\r. if (f((h,l),r)=out) then 1 else 0) random))) x) 1836 (MAKE_ALL_DISTINCT 1837 (MAP (\s. (f s,FST s)) (LIST_COMBS (LIST_COMBS high low) random))))) - 1838 (REAL_SUM (MAP (\x. (\(out,l). (\s. s * lg ((1/(&(LENGTH high * LENGTH random)))*s)) 1839 (REAL_SUM (MAP (\(h,r). if (f((h,l),r)=out) then 1 else 0) 1840 (LIST_COMBS high random)))) x) 1841 (MAKE_ALL_DISTINCT 1842 (MAP (\s. (f s,SND (FST s))) 1843 (LIST_COMBS (LIST_COMBS high low) random)))))))``, 1844 REPEAT STRIP_TAC 1845 >> (MP_TAC o Q.SPECL [`LIST_TO_SET high`,`LIST_TO_SET low`,`LIST_TO_SET random`,`f`]) 1846 unif_prog_space_leakage_computation_reduce 1847 >> SIMP_TAC std_ss [FINITE_LIST_TO_SET, CROSS_LIST_TO_SET] 1848 >> `~(set (LIST_COMBS (LIST_COMBS high low) random) = {})` 1849 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [NOT_IN_EMPTY] 1850 >> Cases_on `high` >> Cases_on `low` >> Cases_on `random` 1851 >> FULL_SIMP_TAC list_ss [LIST_COMBS_def, MAP] 1852 >> METIS_TAC []) 1853 >> RW_TAC std_ss [CARD_LIST_TO_SET, MAKE_ALL_DISTINCT_ALL_DISTINCT, REAL_EQ_LMUL] 1854 >> POP_ASSUM (K ALL_TAC) 1855 >> Cases_on `(1 / & (LENGTH high * LENGTH low * LENGTH random) = 0)` 1856 >> RW_TAC real_ss [IMAGE_LIST_TO_SET] 1857 >> `(set 1858 (MAP (\s. (f s,SND (FST s))) 1859 (LIST_COMBS (LIST_COMBS high low) random))) = 1860 (set (MAKE_ALL_DISTINCT 1861 (MAP (\s. (f s,SND (FST s))) 1862 (LIST_COMBS (LIST_COMBS high low) random))))` 1863 by RW_TAC std_ss [LIST_TO_SET_MAKE_ALL_DISTINCT] 1864 >> POP_ORW 1865 >> `(set 1866 (MAP (\s. (f s,FST s)) 1867 (LIST_COMBS (LIST_COMBS high low) random))) = 1868 (set (MAKE_ALL_DISTINCT 1869 (MAP (\s. (f s,FST s)) 1870 (LIST_COMBS (LIST_COMBS high low) random))))` 1871 by RW_TAC std_ss [LIST_TO_SET_MAKE_ALL_DISTINCT] 1872 >> POP_ORW 1873 >> RW_TAC std_ss [ALL_DISTINCT_imp_REAL_SUM_IMAGE_of_LIST_TO_SET_eq_REAL_SUM, 1874 ALL_DISTINCT_LIST_COMBS, ALL_DISTINCT_MAKE_ALL_DISTINCT]); 1875 1876 1877val unif_prog_space_visible_leakage_LIST_TO_SET_computation_reduce = store_thm 1878 ("unif_prog_space_visible_leakage_LIST_TO_SET_computation_reduce", 1879 ``!high low random f. ALL_DISTINCT high /\ ALL_DISTINCT low /\ ALL_DISTINCT random /\ 1880 ~(high = []) /\ ~(low = []) /\ ~(random = []) ==> 1881 (visible_leakage (unif_prog_space (LIST_TO_SET high) (LIST_TO_SET low) (LIST_TO_SET random)) f = 1882 ~(1/(&(LENGTH high * LENGTH low * LENGTH random)))* 1883 ((REAL_SUM (MAP (\x. (\(out,l,r). (\s. s * lg ((1/(&(LENGTH high)))*s)) 1884 (REAL_SUM (MAP (\h. if (f((h,l),r)=out) then 1 else 0) high))) x) 1885 (MAKE_ALL_DISTINCT 1886 (MAP (\s. (f s,SND (FST s),SND s)) (LIST_COMBS (LIST_COMBS high low) random)))))))``, 1887 REPEAT STRIP_TAC 1888 >> (MP_TAC o Q.SPECL [`LIST_TO_SET high`,`LIST_TO_SET low`,`LIST_TO_SET random`,`f`]) 1889 unif_prog_space_visible_leakage_computation_reduce 1890 >> SIMP_TAC std_ss [FINITE_LIST_TO_SET, CROSS_LIST_TO_SET] 1891 >> `~(set (LIST_COMBS (LIST_COMBS high low) random) = {})` 1892 by (ONCE_REWRITE_TAC [EXTENSION] >> RW_TAC std_ss [NOT_IN_EMPTY] 1893 >> Cases_on `high` >> Cases_on `low` >> Cases_on `random` 1894 >> FULL_SIMP_TAC list_ss [LIST_COMBS_def, MAP] 1895 >> METIS_TAC []) 1896 >> RW_TAC std_ss [CARD_LIST_TO_SET, MAKE_ALL_DISTINCT_ALL_DISTINCT, REAL_EQ_LMUL, GSYM REAL_MUL_LNEG, 1897 REAL_NEG_EQ0, GSYM REAL_INV_1OVER, REAL_INV_EQ_0] 1898 >> POP_ASSUM (K ALL_TAC) 1899 >> Cases_on `(& (LENGTH high * LENGTH low * LENGTH random) = 0)` >> ASM_REWRITE_TAC [] 1900 >> RW_TAC real_ss [IMAGE_LIST_TO_SET] 1901 >> `(set 1902 (MAP (\s. (f s,SND (FST s),SND s)) 1903 (LIST_COMBS (LIST_COMBS high low) random))) = 1904 (set (MAKE_ALL_DISTINCT 1905 (MAP (\s. (f s,SND (FST s),SND s)) 1906 (LIST_COMBS (LIST_COMBS high low) random))))` 1907 by RW_TAC std_ss [LIST_TO_SET_MAKE_ALL_DISTINCT] 1908 >> POP_ORW 1909 >> RW_TAC std_ss [ALL_DISTINCT_imp_REAL_SUM_IMAGE_of_LIST_TO_SET_eq_REAL_SUM, 1910 ALL_DISTINCT_LIST_COMBS, ALL_DISTINCT_MAKE_ALL_DISTINCT]); 1911 1912 1913val _ = export_theory (); 1914