CoursePisa2014: conseq_clean.ec

File conseq_clean.ec, 2.4 KB (added by François Dupressoir, 3 years ago)

exercise sheet on byequiv, byphoare, bypr and conseq

Line 
1require import Pair.
2require import Distr.
3require import Real.
4
5(** Anticipating on the lecture on modules, the following type
6    contains all modules that implement at least:
7      - a procedure f that takes no argument of type x and returns a
8    boolean, and
9      - a procedure g that takes a boolean and returns a boolean.    **)
10module type MT = {
11  proc f(): bool * bool
12  proc g(): bool
13}.
14
15(** We can now quantify over modules of type MT, knowing that they
16    have the desired procedures: forall (M <: MT), ...              **)
17(* Prove the following lemmas using "rewrite Pr [<lemma>]". You may
18   use smt to conclude the proofs.                                  *)
19lemma Pr0 (M <: MT) &m: Pr[M.f() @ &m: false] = 0%r.
20proof.
21(* FILL ME *)
22qed.
23
24lemma Pr_And (M <: MT) &m:
25  Pr[M.f() @ &m: fst res \/ snd res] <= Pr[M.f() @ &m: fst res] + Pr[M.f() @ &m: snd res].
26proof.
27(* FILL ME *)
28qed.
29
30(** Prove the following lemmas *)
31lemma eq_pr (M <: MT) &m:
32  equiv[M.f ~ M.g: true ==> res{2} = (fst res /\ snd res){1}] =>
33  Pr[M.f() @ &m: fst res /\ snd res] = Pr[M.g() @ &m: res].
34proof.
35(* FILL ME *)
36qed.
37
38(* Useful tactic: cut:= <lemma> <instances> *)
39lemma pr_eq (M <: MT) &m:
40  (exists d, forall b,
41    phoare[M.f: true ==> (fst res /\ snd res) = b] = (mu d ((=) b)) /\
42    phoare[M.g: true ==> res = b] = (mu d ((=) b))) =>
43  equiv[M.f ~ M.g: true ==> res{2} = (fst res /\ snd res){1}].
44proof.
45(* FILL ME *)
46qed.
47
48(** Using conseq **)
49module type T = { proc f(b:bool): bool }.
50
51lemma pr_conseq (M <: T):
52  islossless M.f =>
53  (forall b', hoare  [M.f: b = b' ==> res = b']) =>
54  forall b', phoare [M.f: b = b' ==> res = b'] = 1%r.
55proof.
56(* FILL ME *)
57qed.
58
59(** Going back to probability lemmas... Make a creative use of the
60    limited set of mu-related lemmas that can be used with "rewrite
61    Pr" (mu_false, mu_or, mu_eq, mu_supp) to prove the following
62    lemmas. Liberal use of the cut rule is justified. **)
63type t.
64
65module type MT' = {
66  proc f(): bool * t
67}.
68
69lemma FundamentalLemma (M1 <: MT) (M2 <: MT') (F:t -> bool) &m:
70  equiv [M1.g ~ M2.f: true ==> !F (snd res){2} => res{1} = fst res{2}] =>
71  Pr[M1.g() @ &m: res] <= Pr[M2.f() @ &m: fst res] + Pr[M2.f() @ &m: F (snd res)].
72proof.
73(* FILL ME *)
74qed.
75
76lemma SplitProb (M <: MT') (F:t -> bool) &m:
77  Pr[M.f() @ &m: fst res] = Pr[M.f() @ &m: fst res /\ F (snd res)] + Pr[M.f() @ &m: fst res /\ !F (snd res)].
78proof.
79(* FILL ME *)
80qed.
81