Lines Matching defs:random
138 val random = Define
139 `random = {(\s:string. (0:num))}`;
145 val example1_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
149 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M1 = 2``,
153 ``random``)
154 [high, low, random, lem1, lem2, lem3]
178 val example2_input_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
182 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M2 = 2``,
186 ``random``)
187 [high, low, random, lem1, lem2, lem3, w2n_11]
220 val random = Define
221 `random = {(\s:string. (0:num))}`;
240 val example3_lr_input_conv = SIMP_CONV set_ss [low, random];
244 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low random) M3 = 2``,
247 ``random``)
248 [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6, w2n_11]
279 val example4_lr_input_conv = SIMP_CONV set_ss [low, random];
283 ``leakage (unif_prog_space ((high (SUC (SUC (SUC 0))))) low random) M4 = inv 16 * (52 - 6 * lg 3)``,
286 ``random``)
287 [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6]
324 val random = Define
325 `random = {(\s:string. (0:num))}`;
327 val example5_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3];
329 val example5_output_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]
334 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5 = 0``,
337 ``random``)
338 [high, low, random, lem1, lem2, lem3]
375 val random = Define
376 `random = {(\s:string. ([]:num list))}`;
378 val example5'_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ];
380 val example5'_output_conv = SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND, PAIR_EQ]
382 THENC SIMP_CONV list_string_ss [high, low, random, lem7, lem8, APPEND];
386 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) (low (SUC (SUC (SUC 0)))) random) M5' = 2``,
390 ``random``)
391 [high, low, random, lem7, lem8, APPEND]
404 (* Example 8: out = high XOR random *)
412 val random = Define
413 `(random 0 = {(\s:string. if s = "random" then 0 else 0)}) /\
414 (random (SUC n) = (\s:string. if s = "random" then SUC n else 0)INSERT(random n))`;
421 then w2n (((n2w (H s "high")):word2) ?? (n2w (R s "random"))) else 0))`;
423 val example8_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11];
425 val example8_output_conv = SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11]
428 THENC SIMP_CONV arith_ss [high, low, random, lem1, lem2, lem3, w2n_11];
432 ``leakage (unif_prog_space (high (SUC (SUC (SUC 0)))) low (random (SUC (SUC (SUC 0))))) M8 = 0``,
435 ``random (SUC (SUC (SUC 0)))``)
436 [high, low, random, lem1,lem2]
450 (* Example 8': out = high XOR random *)
462 (``!n. random n = if (n=0) then
463 {(\s:string. if s = "random" then 0 else 0)}
465 (\s:string. if s = "random" then n else 0)INSERT(random (n-1))``,
466 Induct ++ RW_TAC arith_ss [random]);
470 ``visible_leakage (unif_prog_space (high 3) low (random 3)) M8 = 2``,
474 ++ `FINITE (random 3)`
478 ++ `~ ((high 3) CROSS low CROSS (random 3) = {})`