examples/diningcryptos/basic_leakage_examplesScript.sml

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)))) =
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))`
75         ((\s'. (if s' = "h2" then m1 else 0)) =
76          (\s'. (if s' = "h2" then m2 else (if s' = "h1" then n2 else 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))`
92         ((\s'. (if s' = "h2" then m else (if s' = "h1" then n else 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`
204 (* Example 3:  out = h1 XOR h2        *)
205 (* 2 BITS: match of bits of h1 and h2 *)
212 val 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))`;
218    `high n = h2 (h1 n) n`;
228                 then w2n (((n2w (H s "h1")):word2) ?? (n2w (H s "h2"))) else 0))`;
239 val example3_h_input_conv = SIMP_CONV set_ss [high, h1, h2]
251                         [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6, w2n_11]
265 (* Example 4:    out = h1 + h2 *)
271    then (H s "h1") + (H s "h2") else 0))`;
278 val example4_h_input_conv = SIMP_CONV set_ss [high, h1, h2]
290                         [high, low, random, h1, h2, lem1, lem2, lem3, lem4, lem5, lem6]