1(*
2app load ["bossLib", "metisLib", "arithmeticTheory", "pred_setTheory",
3          "pred_setLib", "stringLib",
4          "listTheory", "state_transformerTheory", "probabilityTheory",
5          "formalizeUseful", "combinTheory", "pairTheory", "realTheory",
6          "realLib", "extra_boolTheory", "jrhUtils", "extra_pred_setTheory", "extra_listTheory",
7          "realSimps", "extra_realTheory", "measureTheory", "numTheory",
8          "simpLib", "seqTheory", "subtypeTheory", "transcTheory",
9          "limTheory", "stringTheory", "rich_listTheory", "stringSimps",
10          "listSimps", "lebesgueTheory", "informationTheory",
11          "extra_stringTheory", "extra_stringLib", "leakageTheory", "leakageLib",
12          "wordsTheory", "wordsLib"];
13*)
14
15open HolKernel Parse boolLib bossLib metisLib arithmeticTheory pred_setTheory
16     pred_setLib stringLib
17     listTheory state_transformerTheory
18     probabilityTheory formalizeUseful extra_numTheory combinTheory
19     pairTheory realTheory realLib extra_boolTheory jrhUtils
20     extra_pred_setTheory realSimps extra_realTheory measureTheory numTheory
21     simpLib seqTheory subtypeTheory extra_listTheory
22     transcTheory limTheory stringTheory rich_listTheory stringSimps listSimps
23     lebesgueTheory informationTheory extra_stringTheory extra_stringLib leakageTheory
24     leakageLib wordsTheory wordsLib;
25
26open real_sigmaTheory;
27
28val _ = new_theory "basic_leakage_examples";
29
30infixr 0 ++ << || THENC ORELSEC ORELSER ##;infix 1 >>;val op ++ = op THEN;val op << = op THENL;val op >> = op THEN1;val op || = op ORELSE;val REVERSE = Tactical.REVERSE;val Simplify = RW_TAC arith_ss;val Suff = PARSE_TAC SUFF_TAC;val Know = PARSE_TAC KNOW_TAC;val Rewr = DISCH_THEN (REWRITE_TAC o wrap);val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap);val Cond =  DISCH_THEN  (fn mp_th =>   let     val cond = fst (dest_imp (concl mp_th))   in     KNOW_TAC cond << [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)]   end);val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]);
31
32val safe_set_ss = (simpLib.++ (bool_ss, PRED_SET_ss));
33
34val set_ss = (simpLib.++ (arith_ss, PRED_SET_ss));
35
36val list_string_ss = (simpLib.++ (list_ss, STRING_ss));
37
38fun TRY2_TAC t1 t2 state = let
39 val (a1,f1) = t1 state handle HOL_ERR _ => ALL_TAC state
40 in if length a1 = 0 then (a1,f1) else t2 state end;
41
42
43val lem1 = prove
44  (``!(s:string) (n:num) (m:num). ((\s'. (if s' = s then n else 0)) =
45                       (\s'. (if s' = s then m else 0))) =
46                      (n = m)``,METIS_TAC []);
47
48val lem2 = prove
49  (``!(s:string) (n:num). ((\s'. (if s' = s then n else 0)) = (\s'. 0)) = (n = 0)``,
50   METIS_TAC []);
51
52val lem3 = prove
53  (``!(s:string) (n:num). ((\s'. 0) = (\s'. (if s' = s then n else 0))) = (n = 0)``,
54   METIS_TAC []);
55
56val lem4 = prove
57  (``!(n1:num)(n2:num)(m1:num)(m2:num).
58        ((\s'. (if s' = "h2" then m1 else (if s' = "h1" then n1 else 0))) =
59         (\s'. (if s' = "h2" then m2 else (if s' = "h1" then n2 else 0)))) =
60        ((n1=n2)/\(m1=m2))``,
61        REPEAT STRIP_TAC ++ EQ_TAC
62            >> (ONCE_REWRITE_TAC [FUN_EQ_THM]
63                ++ SPOSE_NOT_THEN STRIP_ASSUME_TAC
64                ++ Cases_on `n1 = n2`
65                >> (Q.PAT_X_ASSUM `!x. (if x = "h2" then m1 else (if x = "h1" then n1 else 0)) =
66                                     (if x = "h2" then m2 else (if x = "h1" then n2 else 0))`
67                    (MP_TAC o Q.SPEC `"h2"`) ++ RW_TAC std_ss [])
68                ++ Q.PAT_X_ASSUM `!x. (if x = "h2" then m1 else (if x = "h1" then n1 else 0)) =
69                                     (if x = "h2" then m2 else (if x = "h1" then n2 else 0))`
70                    (MP_TAC o Q.SPEC `"h1"`) ++ SRW_TAC [] [])
71            ++ RW_TAC std_ss []);
72
73val lem5 = prove
74  (``!(m1:num)(m2:num)(n2:num).
75        ((\s'. (if s' = "h2" then m1 else 0)) =
76         (\s'. (if s' = "h2" then m2 else (if s' = "h1" then n2 else 0)))) =
77        ((n2=0)/\(m1=m2))``,
78        REPEAT STRIP_TAC ++ EQ_TAC
79            >> (ONCE_REWRITE_TAC [FUN_EQ_THM]
80                ++ SPOSE_NOT_THEN STRIP_ASSUME_TAC
81                ++ Cases_on `n2=0`
82                >> (Q.PAT_X_ASSUM `!x. (if x = "h2" then m1 else 0) =
83                                     (if x = "h2" then m2 else (if x = "h1" then n2 else 0))`
84                    (MP_TAC o Q.SPEC `"h2"`) ++ RW_TAC std_ss [])
85                ++ Q.PAT_X_ASSUM `!x. (if x = "h2" then m1 else 0) =
86                                     (if x = "h2" then m2 else (if x = "h1" then n2 else 0))`
87                    (MP_TAC o Q.SPEC `"h1"`) ++ SRW_TAC [] [])
88            ++ RW_TAC std_ss []);
89
90val lem6 = prove
91  (``!(n:num)(m:num).
92        ((\s'. (if s' = "h2" then m else (if s' = "h1" then n else 0))) =
93         (\s'. 0)) =
94        ((n=0)/\(m=0))``,
95        REPEAT STRIP_TAC ++ EQ_TAC
96            >> (ONCE_REWRITE_TAC [FUN_EQ_THM]
97                ++ SPOSE_NOT_THEN STRIP_ASSUME_TAC
98                ++ Cases_on `n = 0`
99                >> (Q.PAT_X_ASSUM `!x. (if x = "h2" then m else (if x = "h1" then n else 0)) = 0`
100                    (MP_TAC o Q.SPEC `"h2"`) ++ RW_TAC std_ss [])
101                ++ Q.PAT_X_ASSUM `!x. (if x = "h2" then m else (if x = "h1" then n else 0)) = 0`
102                    (MP_TAC o Q.SPEC `"h1"`) ++ SRW_TAC [] [])
103            ++ RW_TAC std_ss []);
104
105val lem7 = prove
106  (``!(s:string) (n:num) (m:num). ((\s'. (if s' = s then [n] else [])) =
107                       (\s'. (if s' = s then [m] else []))) =
108                      (n = m)``,
109        REPEAT STRIP_TAC ++ EQ_TAC
110            >> (RW_TAC list_ss [FUN_EQ_THM] ++ POP_ASSUM (MP_TAC o Q.SPEC `s`)
111                ++ RW_TAC std_ss [])
112            ++ RW_TAC std_ss []);
113
114val lem8 = prove
115  (``!(n1:num) (n2:num) (n3:num) (m1:num) (m2:num) (m3:num).
116        ((\s'. (if (s' = "out") then [n1;n2] else
117                (if (s' = "low") then [n3] else []))) =
118         (\s'. (if (s' = "out") then [m1;m2] else
119                (if (s' = "low") then [m3] else [])))) =
120                      ((n1 = m1) /\ (n2 = m2) /\ (n3 = m3))``,
121        REPEAT STRIP_TAC ++ EQ_TAC
122            >> (RW_TAC list_ss [FUN_EQ_THM]
123                << [POP_ASSUM (MP_TAC o Q.SPEC `"out"`) ++ RW_TAC std_ss [],
124                    POP_ASSUM (MP_TAC o Q.SPEC `"out"`) ++ RW_TAC std_ss [],
125                    POP_ASSUM (MP_TAC o Q.SPEC `"low"`) ++ RW_TAC string_ss []])
126            ++ RW_TAC std_ss []);
127
128(* *************************** *)
129(* Example 1: out = high + low *)
130(* TOTAL LEAKAGE               *)
131(* *************************** *)
132
133val high = Define
134   `(high 0 = {(\s:string. if s = "high" then 0 else 0)}) /\
135    (high (SUC n) = (\s:string. if s = "high" then SUC n else 0)INSERT(high n))`;
136
137val low = Define
138   `(low 0 = {(\s:string. if s = "low" then 0 else 0)}) /\
139    (low (SUC n) = (\s:string. if s = "low" then SUC n else 0)INSERT(low n))`;
140
141val random = Define
142   `random = {(\s:string. (0:num))}`;
143
144val M1 = Define
145   `M1 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out")
146   then (H s "high") + (L s "low") else 0))`;
147
148val example1_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
149
150val leakage_example1 = store_thm
151  ("leakage_example1",
152   ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M1 = 2``,
153CONV_TAC (RATOR_CONV (RAND_CONV (
154        LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``,
155                              ``low (SUC (SUC (SUC 0)))``,
156                              ``random``)
157                        [high, low, random, lem1, lem2, lem3]
158                        [M1, H_def, L_def, FST, SND]
159                        example1_conv example1_conv example1_conv
160                        example1_conv example1_conv example1_conv example1_conv)))
161++ SIMP_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER]
162++ `lg 4 = 2`
163        by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
164++ RW_TAC real_ss []
165++ ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC std_ss [GSYM real_div]
166++ (MP_TAC o Q.SPECL [`32`,`2`,`16`]) REAL_EQ_LDIV_EQ
167++ RW_TAC real_ss []);
168
169(* ******************************** *)
170(* Example 2:    out = high XOR low *)
171(* TOTAL LEAKAGE                    *)
172(* ******************************** *)
173
174val M2 = Define
175   `M2 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out")
176        then w2n (((n2w (H s "high")):word2) ?? (n2w (L s "low"))) else 0))`;
177
178val example2_output_conv = SIMP_CONV arith_ss [lem1,lem2,lem3, w2n_11]
179                                                      THENC (FIND_CONV ``w2n(a ?? b)`` WORD_EVAL_CONV);
180
181val example2_input_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
182
183val leakage_example2 = store_thm
184  ("leakage_example2",
185   ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M2 = 2``,
186CONV_TAC (RATOR_CONV (RAND_CONV (
187        LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``,
188                              ``low (SUC (SUC (SUC 0)))``,
189                              ``random``)
190                        [high, low, random, lem1, lem2, lem3, w2n_11]
191                        [M2, H_def, L_def, FST, SND]
192                        example2_input_conv example2_input_conv example2_input_conv
193                        example2_input_conv example2_input_conv example2_input_conv
194                        example2_output_conv)))
195++ SIMP_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER]
196++ `lg 4 = 2`
197        by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
198++ RW_TAC real_ss []
199++ ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC std_ss [GSYM real_div]
200++ (MP_TAC o Q.SPECL [`32`,`2`,`16`]) REAL_EQ_LDIV_EQ
201++ RW_TAC real_ss []);
202
203(* ********************************** *)
204(* Example 3:  out = h1 XOR h2        *)
205(* 2 BITS: match of bits of h1 and h2 *)
206(* ********************************** *)
207
208val h1 = Define
209   `(h1 0 = {(\s:string. if s = "h1" then 0 else 0)}) /\
210    (h1 (SUC n) = (\s:string. if s = "h1" then SUC n else 0)INSERT(h1 n))`;
211
212val h2 = Define
213   `(h2 l 0 = IMAGE (\s: num state. (\s':string. if s' = "h2" then 0 else s s')) l) /\
214    (h2 l (SUC n) = (IMAGE (\s: num state. (\s':string. if s' = "h2" then (SUC n) else s s')) l) UNION
215                    (h2 l n))`;
216
217val high = Define
218   `high n = h2 (h1 n) n`;
219
220val low = Define
221   `low = {(\s:string. (0:num))}`;
222
223val random = Define
224   `random = {(\s:string. (0:num))}`;
225
226val M3 = Define
227   `M3 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out")
228                then w2n (((n2w (H s "h1")):word2) ?? (n2w (H s "h2"))) else 0))`;
229
230val example3_output_conv = SIMP_CONV string_ss [lem1, lem2, lem3, lem4, lem5, lem6, w2n_11]
231                           THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV))
232                           THENC (TRY_CONV (FIND_CONV ``w2n(a ?? b)`` WORD_EVAL_CONV));
233
234val example3_h_conv = SIMP_CONV arith_ss [lem1, lem2, lem3, lem4, lem5, lem6, w2n_11]
235                          THENC (TRY_CONV (FIND_CONV ``(a ?? b) = (c ?? d)`` WORD_EVAL_CONV));
236
237val example3_lr_conv = SIMP_CONV arith_ss [lem1, lem2, lem3, lem4, lem5, lem6];
238
239val example3_h_input_conv = SIMP_CONV set_ss [high, h1, h2]
240THENC  (FIND_CONV ``x UNION y``
241                        (UNION_CONV (SIMP_CONV set_ss [lem1, lem2, lem3, lem4, lem5, lem6])));
242
243val example3_lr_input_conv = SIMP_CONV set_ss [low, random];
244
245val leakage_example3 = store_thm
246  ("leakage_example3",
247   ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low random) M3 = 2``,
248CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``,
249                              ``low``,
250                              ``random``)
251                        [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6, w2n_11]
252                        [M3, H_def, L_def, FST, SND, w2n_11]
253                        example3_h_input_conv example3_lr_input_conv example3_lr_input_conv
254                        example3_h_conv example3_lr_conv example3_lr_conv
255                        example3_output_conv)))
256++ RW_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER, lg_mul, lg_2]
257++ `lg 4 = 2`
258        by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
259++ `lg 16 = 4`
260        by (`16 = 2 pow 4` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
261++ ONCE_REWRITE_TAC [REAL_MUL_COMM]
262++ RW_TAC real_ss [GSYM real_div]);
263
264(* *************************** *)
265(* Example 4:    out = h1 + h2 *)
266(* PARTIAL LEAKAGE             *)
267(* *************************** *)
268
269val M4 = Define
270   `M4 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out")
271   then (H s "h1") + (H s "h2") else 0))`;
272
273val example4_output_conv = SIMP_CONV string_ss [lem1, lem2, lem3, lem4, lem5, lem6]
274                           THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV));
275
276val example4_dup_conv = SIMP_CONV arith_ss [lem1, lem2, lem3, lem4, lem5, lem6];
277
278val example4_h_input_conv = SIMP_CONV set_ss [high, h1, h2]
279THENC  (FIND_CONV ``x UNION y``
280                        (UNION_CONV (SIMP_CONV set_ss [lem1, lem2, lem3, lem4, lem5, lem6])));
281
282val example4_lr_input_conv = SIMP_CONV set_ss [low, random];
283
284val leakage_example4 = store_thm
285  ("leakage_example4",
286   ``leakage (unif_prog_space ((high (SUC (SUC (SUC 0))))) low random) M4 = inv 16 * (52 - 6 * lg 3)``,
287CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``,
288                              ``low``,
289                              ``random``)
290                        [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6]
291                        [M4, H_def, L_def, FST, SND, w2n_11]
292                        example4_h_input_conv example4_lr_input_conv example4_lr_input_conv
293                        example4_dup_conv example4_dup_conv example4_dup_conv
294                        example4_output_conv)))
295++ RW_TAC real_ss [lg_1, lg_mul, lg_2, lg_inv, GSYM REAL_INV_1OVER, real_div]
296++ `lg 8 = 3` by (`8 = 2 pow 3` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
297++ `lg 4 = 2` by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
298++ `lg 16 = 4` by (`16 = 2 pow 4` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
299++ RW_TAC real_ss [REAL_INV_EQ_0]
300++ REPEAT (POP_ASSUM (K ALL_TAC))
301++ REAL_ARITH_TAC);
302
303(* *************************** *)
304(* Example 5:  intermed. leak  *)
305(* No leakage                  *)
306(* *************************** *)
307
308val assign1 = Define
309   `assign1 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out")
310   then (H s "high") else 0))`;
311
312val assign2 = Define
313   `assign2 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out")
314   then (L s "low") else 0))`;
315
316val M5 = Define
317   `M5 = (\s: ((num,num,num) prog_state). assign2 ((H s, assign1 s), R s))`;
318
319val high = Define
320   `(high 0 = {(\s:string. if s = "high" then 0 else 0)}) /\
321    (high (SUC n) = (\s:string. if s = "high" then SUC n else 0)INSERT(high n))`;
322
323val low = Define
324   `(low 0 = {(\s:string. if s = "low" then 0 else 0)}) /\
325    (low (SUC n) = (\s:string. if s = "low" then SUC n else 0)INSERT(low n))`;
326
327val random = Define
328   `random = {(\s:string. (0:num))}`;
329
330val example5_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
331
332val example5_output_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]
333                           THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV));
334
335val leakage_example5 = store_thm
336  ("leakage_example5",
337   ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5 = 0``,
338CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``,
339                              ``low (SUC (SUC (SUC 0)))``,
340                              ``random``)
341                        [high, low, random, lem1, lem2, lem3]
342                        [M5, assign1, assign2, H_def, L_def, FST, SND]
343                        example5_conv example5_conv example5_conv
344
345                        example5_conv example5_conv example5_conv
346                        example5_output_conv)))
347++ RW_TAC real_ss [REAL_DIV_REFL, lg_1]);
348
349(* *************************** *)
350(* Example 5': intermed. leak  *)
351(* total leakage               *)
352(* *************************** *)
353
354val state_update = Define
355   `state_update name value = (\s:(num list) state. (\n:string. if (n=name) then value else s n))`;
356
357val state_append = Define
358   `state_append name value = (\s:(num list) state.
359        state_update name ((if (value=[]) then [] else [HD value])++(s name)) s)`;
360
361val assign1 = Define
362   `assign1 = (\s: ((num list,num list,num list) prog_state). state_update "out" (H s "high") (L s))`;
363
364val assign2 = Define
365   `assign2 = (\s: ((num list,num list,num list) prog_state). state_append "out" (L s "low") (L s))`;
366
367val M5' = Define
368   `M5' = (\s: ((num list,num list,num list) prog_state). assign2 ((H s, assign1 s), R s))`;
369
370val high = Define
371   `(high 0 = {(\s:string. if s = "high" then [0] else [])}) /\
372    (high (SUC n) = (\s:string. if s = "high" then [SUC n] else [])INSERT(high n))`;
373
374val low = Define
375   `(low 0 = {(\s:string. if s = "low" then [0] else [])}) /\
376    (low (SUC n) = (\s:string. if s = "low" then [SUC n] else [])INSERT(low n))`;
377
378val random = Define
379   `random = {(\s:string. ([]:num list))}`;
380
381val example5'_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ];
382
383val example5'_output_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ]
384                            THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV))
385                            THENC SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND];
386
387val leakage_example5' = store_thm
388  ("leakage_example5'",
389   ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5' = 2``,
390PURE_REWRITE_TAC [M5', state_update, state_append, assign1, assign2]
391++ CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``,
392                              ``low (SUC (SUC (SUC 0)))``,
393                              ``random``)
394                        [high, low, random, lem7, lem8, APPEND]
395                        [H_def, L_def, FST, SND, APPEND]
396                        example5'_conv example5'_conv example5'_conv
397                        example5'_output_conv example5'_output_conv example5'_output_conv
398                        example5'_output_conv)))
399++ RW_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER]
400++ `lg 4 = 2` by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
401++ RW_TAC real_ss []
402++ ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC std_ss [GSYM real_div]
403++ (MP_TAC o Q.SPECL [`32`,`2`,`16`]) REAL_EQ_LDIV_EQ
404++ RW_TAC real_ss []);
405
406(* *********************************** *)
407(* Example 8:    out = high XOR random *)
408(* NO LEAKAGE (hidden prob)            *)
409(* *********************************** *)
410
411val high = Define
412   `(high 0 = {(\s:string. if s = "high" then 0 else 0)}) /\
413    (high (SUC n) = (\s:string. if s = "high" then SUC n else 0)INSERT(high n))`;
414
415val random = Define
416   `(random 0 = {(\s:string. if s = "random" then 0 else 0)}) /\
417    (random (SUC n) = (\s:string. if s = "random" then SUC n else 0)INSERT(random n))`;
418
419val low = Define
420   `low = {(\s:string. (0:num))}`;
421
422val M8 = Define
423   `M8 = (\s: ((num,num,num) prog_state). (\s':string. if (s' = "out")
424        then w2n (((n2w (H s "high")):word2) ?? (n2w (R s "random"))) else 0))`;
425
426val example8_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11];
427
428val example8_output_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11]
429                            THENC (TRY_CONV (FIND_CONV ``(x:string)=(y:string)`` string_EQ_CONV))
430                            THENC (TRY_CONV (FIND_CONV ``w2n(a ?? b)`` WORD_EVAL_CONV))
431                            THENC SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11];
432
433val leakage_example8 = store_thm
434  ("leakage_example8",
435   ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low (random (SUC (SUC (SUC 0))))) M8 = 0``,
436CONV_TAC (RATOR_CONV (RAND_CONV (LEAKAGE_COMPUTE_CONV (``high (SUC (SUC (SUC 0)))``,
437                              ``low``,
438                              ``random (SUC (SUC (SUC 0)))``)
439                        [high, low, random, lem1,lem2]
440                        [M8, H_def, R_def, FST, SND, lem1,lem2, lem3]
441                        example8_conv example8_conv example8_conv
442                        example8_output_conv example8_conv example8_output_conv
443                        example8_output_conv)))
444++ RW_TAC real_ss [lg_mul, lg_2, lg_1, lg_inv, GSYM REAL_INV_1OVER]
445++ `lg 4 = 2`
446        by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
447++ `lg 16 = 4`
448        by (`16 = 2 pow 4` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
449++ ONCE_REWRITE_TAC [REAL_MUL_COMM]
450++ RW_TAC real_ss [GSYM real_div]);
451
452(* *********************************** *)
453(* Example 8':   out = high XOR random *)
454(* TOTAL LEAKAGE (visible prob)        *)
455(* *********************************** *)
456
457val high_thm = prove
458   (``!n. high n = if (n=0) then
459                {(\s:string. if s = "high" then 0 else 0)}
460             else
461                (\s:string. if s = "high" then n else 0)INSERT(high (n-1))``,
462     Induct ++ RW_TAC arith_ss [high]);
463
464val random_thm = prove
465   (``!n. random n = if (n=0) then
466                {(\s:string. if s = "random" then 0 else 0)}
467             else
468                (\s:string. if s = "random" then n else 0)INSERT(random (n-1))``,
469     Induct ++ RW_TAC arith_ss [random]);
470
471val leakage_example8' = store_thm
472  ("leakage_example8'",
473   ``visible_leakage (unif_prog_space (high 3) low (random 3)) M8 = 2``,
474`FINITE (high 3)`
475   by (NTAC 4 (ONCE_REWRITE_TAC [high_thm])
476       ++ RW_TAC set_ss [])
477++ `FINITE (random 3)`
478   by (NTAC 4 (ONCE_REWRITE_TAC [random_thm])
479       ++ RW_TAC set_ss [])
480++ `FINITE (low)` by RW_TAC set_ss [low]
481++ `~ ((high 3) CROSS low CROSS (random 3) = {})`
482        by (RW_TAC std_ss [Once EXTENSION]
483            ++ NTAC 4 (ONCE_REWRITE_TAC [high_thm, random_thm, low])
484            ++ RW_TAC set_ss []
485            ++ Q.EXISTS_TAC `(((\s.0),(\s.0)),(\s.0))`
486            ++ RW_TAC std_ss [])
487++ ASM_SIMP_TAC std_ss
488   [unif_prog_space_visible_leakage_computation_reduce]
489++ NTAC 4 (ONCE_REWRITE_TAC [high_thm, random_thm, low])
490++ RW_TAC set_ss [CROSS_EQNS, lem1, lem2]
491++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [lem1,lem2])))
492++ RW_TAC set_ss [CROSS_EQNS, lem1, lem2, M8, H_def, R_def]
493++ CONV_TAC (FIND_CONV ``x UNION y``
494                        (UNION_CONV (SIMP_CONV set_ss [lem1,lem2, w2n_11]
495                                     THENC (FIND_CONV ``(a ?? b) = (c ?? d)`` WORD_EVAL_CONV))))
496++ CONV_TAC (REPEATC (SIMP_CONV set_ss [REAL_SUM_IMAGE_THM]
497                      THENC (FIND_CONV ``x DELETE y``
498                                        (DELETE_CONV (SIMP_CONV arith_ss [PAIR_EQ,lem1,lem2,lem3, w2n_11]
499                                                      THENC (FIND_CONV ``(a ?? b) = (c ?? d)``
500                                                                        WORD_EVAL_CONV))))
501                      THENC (SIMP_CONV arith_ss [lem1,lem2,lem3, w2n_11]))
502             THENC (FIND_CONV ``(a ?? b) = (c ?? d)`` WORD_EVAL_CONV))
503++ RW_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER]
504++ `lg 4 = 2`
505        by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
506++ ONCE_REWRITE_TAC [REAL_MUL_COMM]
507++ RW_TAC real_ss [GSYM real_div]);
508
509(* *********************************** *)
510
511val flip_example_lem = prove
512  (``!(s:string). ~((\s'. s' = s) = (\s'. F))``,METIS_TAC []);
513
514val M = Define
515   `M = (\s: ((bool,bool,bool) prog_state). (\s':string. if (s' = "out")
516   then (if (R s "r") then (L s "l") else (H s "h")) else F))`;
517
518val hidden_flip_example = store_thm
519  ("hidden_flip_example",
520   ``leakage (unif_prog_space {(\s:string. s = "h");(\s:string.F)}
521                              {(\s:string. s = "l");(\s:string.F)}
522                              {(\s:string. s = "r");(\s:string.F)}) M = 3/2 - (3 * lg 3)/4``,
523`~ ({(\s:string. s = "h");(\s:string.F)} CROSS
524        {(\s:string. s = "l");(\s:string.F)} CROSS
525        {(\s:string. s = "r");(\s:string.F)} = {})`
526        by (RW_TAC set_ss [Once EXTENSION]
527            ++ Q.EXISTS_TAC `(((\s.F),(\s.F)),(\s.F))`
528            ++ RW_TAC std_ss [])
529++ ASM_SIMP_TAC set_ss
530   [unif_prog_space_leakage_computation_reduce]
531++ RW_TAC set_ss [CROSS_EQNS, lem1, flip_example_lem]
532++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [flip_example_lem, lem1])))
533++ RW_TAC set_ss [CROSS_EQNS, lem1, M, H_def, L_def, R_def]
534++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [flip_example_lem, lem1])))
535++ CONV_TAC (REPEATC (SIMP_CONV set_ss [REAL_SUM_IMAGE_THM]
536                      THENC (FIND_CONV ``x DELETE y``
537                                        (DELETE_CONV (SIMP_CONV arith_ss [PAIR_EQ, flip_example_lem])))
538                      THENC SIMP_CONV arith_ss [flip_example_lem]))
539++ SIMP_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER, lg_2, REAL_MUL_LINV]
540++ `lg 4 = 2`
541        by (`4 = 2 pow 2` by RW_TAC real_ss [pow] ++ POP_ORW ++ RW_TAC std_ss [lg_pow])
542++ RW_TAC real_ss [lg_mul, REAL_INV_POS, lg_inv]
543++ Q.ABBREV_TAC `foo = 3 * lg 3`
544++ `3 * (~2 + lg 3) + (~2 + 3 * (~2 + lg 3)) =
545    ~14 + 2 * foo`
546        by (Q.UNABBREV_TAC `foo` ++ REAL_ARITH_TAC)
547++ POP_ORW
548++ RW_TAC real_ss [REAL_ADD_ASSOC, real_sub, REAL_NEG_ADD]
549++ ONCE_REWRITE_TAC [REAL_MUL_COMM]
550++ RW_TAC std_ss [GSYM real_div]
551++ (MP_TAC o Q.SPECL [`(12 + ~(2 * foo))`,`3 / 2 + ~foo / 4`,`8`]) REAL_EQ_LDIV_EQ
552++ RW_TAC real_ss [REAL_ADD_RDISTRIB]
553++ RW_TAC std_ss [real_div, Once (GSYM REAL_MUL_ASSOC)]
554++ `inv 4 * 8 = 2` by (ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC real_ss [GSYM real_div])
555++ POP_ORW
556++ REAL_ARITH_TAC);
557
558
559val visible_flip_example = store_thm
560  ("visible_flip_example",
561   ``visible_leakage (unif_prog_space {(\s:string. s = "h");(\s:string.F)}
562                              {(\s:string. s = "l");(\s:string.F)}
563                              {(\s:string. s = "r");(\s:string.F)}) M = 1/2``,
564`~ ({(\s:string. s = "h");(\s:string.F)} CROSS
565        {(\s:string. s = "l");(\s:string.F)} CROSS
566        {(\s:string. s = "r");(\s:string.F)} = {})`
567        by (RW_TAC set_ss [Once EXTENSION]
568            ++ Q.EXISTS_TAC `(((\s.F),(\s.F)),(\s.F))`
569            ++ RW_TAC std_ss [])
570++ ASM_SIMP_TAC set_ss
571   [unif_prog_space_visible_leakage_computation_reduce]
572++ RW_TAC set_ss [CROSS_EQNS, flip_example_lem]
573++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [flip_example_lem])))
574++ RW_TAC set_ss [CROSS_EQNS, lem1, M, H_def, L_def, R_def]
575++ CONV_TAC (FIND_CONV ``x UNION y`` (UNION_CONV (SIMP_CONV set_ss [flip_example_lem])))
576++ CONV_TAC (REPEATC (SIMP_CONV set_ss [REAL_SUM_IMAGE_THM]
577                      THENC (FIND_CONV ``x DELETE y``
578                                        (DELETE_CONV (SIMP_CONV arith_ss [PAIR_EQ, flip_example_lem])))
579                      THENC SIMP_CONV arith_ss [flip_example_lem]))
580++ SIMP_TAC real_ss [lg_1, lg_inv, GSYM REAL_INV_1OVER, lg_2, REAL_MUL_LINV]
581++ ONCE_REWRITE_TAC [REAL_MUL_COMM] ++ RW_TAC real_ss [GSYM real_div, REAL_INV_1OVER]);
582val _ = export_theory ();
583