CoursePisa2014: modules_clean.ec

File modules_clean.ec, 769 bytes (added by François Dupressoir, 3 years ago)

Exercise sheet 1 for day 3

Line 
1require import Real.
2
3module type Adv = {
4  proc main () : bool
5}.
6
7(* Build adversary *)
8module Neg_main (A:Adv) = {
9  proc main () : bool = {
10(* FILL ME *)
11  }
12
13}.
14
15equiv Neg_A (A<:Adv) :
16    Neg_main(A).main ~ A.main : ={glob A} ==> res{1} = !res{2}.
17proof.
18(* FILL ME *)
19qed.
20
21lemma Neg_A_Pr (A<:Adv) &m:
22   Pr[Neg_main(A).main() @ &m : res] = Pr[A.main() @ &m : !res].
23proof.
24(* FILL ME *)
25qed.
26
27lemma Neg_A_Pr_minus (A<:Adv) &m:
28   islossless A.main =>
29   Pr[Neg_main(A).main() @ &m : res] = 1%r - Pr[A.main() @ &m : res].
30proof.
31(* FILL ME *)
32qed.
33
34lemma abs_val (P:real -> bool):
35  (forall &m (A<:Adv), P (Pr[A.main() @ &m : res] - 1%r/2%r)) =>
36  forall &m (A<:Adv), islossless A.main =>
37    P (`|Pr[A.main() @ &m : res] - 1%r/2%r|).
38proof.
39(* FILL ME *)
40qed.
41