CoursePisa2014: Upto.ec

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

Exercise sheet 3 for day 3

Line 
1require import Pred.
2require import FMap.
3require import FSet.
4
5type from.
6type to.
7
8op dsample : to distr. (* Distribution to use on the target type *)
9
10(* A signature for random oracles from "from" to "to". *)
11module type Oracle =  {
12  proc init():unit
13  proc o(x:from):to
14}.
15
16module type AdvRO = { proc o(x:from):to }.
17
18theory ROM.
19  (* Bare random oracle for use in schemes *)
20  module RO:Oracle = {
21    var m : (from, to) map
22
23    proc init() : unit = {
24      m = FMap.empty;
25    }
26
27    proc o(x:from) : to = {
28      var y : to;
29      y = $dsample;
30      if (!in_dom x m) m.[x] = y;
31      return oget (m.[x]);
32    }
33  }.
34
35  lemma lossless_init : islossless RO.init.
36  proof.
37(* FILL ME *)
38  qed.
39
40  (* use the rnd tactic with predicate True *)
41  lemma lossless_o : mu dsample True = 1%r => islossless RO.o.
42  proof.
43(* FILL ME *)
44  qed.
45
46  equiv upto_o v: RO.o ~ RO.o :
47    !mem v (dom RO.m){2} /\ ={x} /\ eq_except RO.m{1} RO.m{2} v ==>
48    !mem v (dom RO.m){2} => ={res} /\ eq_except RO.m{1} RO.m{2} v.
49  proof.
50(* FILL ME *)
51  qed.
52
53  lemma lossless_o_in_dom v:
54    mu dsample True = 1%r =>
55    phoare[ RO.o: mem v (dom RO.m) ==> mem v (dom RO.m)] = 1%r.
56  proof.
57(* FILL ME *)
58  qed.
59
60  theory UpTo.
61    type result.
62
63    module type Adv (RO:AdvRO)= {
64      proc a1 () : from
65      proc a2 (to:to) : result
66    }.
67
68    module Gfail(A:Adv) = {
69      module A_ = A(RO)
70
71      proc main () : from * result = {
72        var fr, to, r;
73
74        RO.init();
75        fr = A_.a1();
76        to = RO.o(fr);
77        r  = A_.a2(to);
78        return (fr, r);
79      }
80    }.
81
82    module Gfail'(A:Adv) = {
83      module A_ = A(RO)
84
85      proc main () : from * result = {
86        var fr, to, r;
87
88        RO.init();
89        fr = A_.a1();
90        to = $dsample;
91        r  = A_.a2(to);
92        return (fr, r);
93      }
94    }.
95
96    (* use the call tactic for abstract procedures with up to failure *)
97    lemma Fail (A<:Adv{RO}):
98      mu dsample True = 1%r =>
99      (forall (RO0 <: AdvRO {A}), islossless RO0.o => islossless A(RO0).a2) =>
100      equiv [Gfail(A).main ~ Gfail'(A).main:
101               ={glob A} ==>
102               let (fr,xxx) = res{2} in
103                 !(mem fr (dom RO.m)){2} => ={res, glob A} /\ eq_except RO.m{1} RO.m{2} fr].
104    proof.
105(* FILL ME *)
106    qed.
107  end UpTo.
108end ROM.
109