easycrypt-rewinding/RewTransformations.ec at main · dfirsov/easycrypt-rewinding · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
pragma Goals:printall.
require import AllCore.
require import RewBasics.


type ct.                        (* some countable type *)


op ct_sbits : ct -> sbits.
axiom iis:  injective ct_sbits.

op unct: sbits -> ct.


axiom unct_ct x : unct (ct_sbits x) = x.


section.

declare module A <: Rew.
declare module B <: Rew{-A}.

declare axiom RewProp_A :
  exists (f : glob A -> sbits),
  injective f /\
  (forall &m, Pr[ A.getState() @ &m : (glob A) = ((glob A){m})
                                   /\ res = f ((glob A){m} ) ] = 1%r) /\
  (forall &m b (x: glob A), b = f x =>
    Pr[A.setState(b) @ &m : glob A = x] = 1%r) /\
  islossless A.setState.

declare axiom RewProp_B :
  exists (f : glob B -> sbits),
  injective f /\
  (forall &m, Pr[ B.getState() @ &m : (glob B) = ((glob B){m})
                                   /\ res = f ((glob B){m} ) ] = 1%r) /\
  (forall &m b (x: glob B), b = f x =>
    Pr[B.setState(b) @ &m : glob B = x] = 1%r) /\
  islossless B.setState.


local module T(A : Rew, B : Rew) : Rew = {

  var x : ct

  proc getState(): sbits = {
    var stateA, stateB : sbits;
    stateA <@ A.getState();
    stateB <@ B.getState();
    return pair_sbits (ct_sbits(x),pair_sbits(stateA, stateB));
  }
  proc setState(state: sbits): unit = {
     A.setState(fst (unpair (snd (unpair state))));
     B.setState(snd (unpair (snd (unpair state))));
     x <- unct (fst (unpair state));
  }

}.


local lemma rewindable_T :
    exists (f : glob T(A,B) -> sbits),
    injective f /\
    (forall (glT : glob T(A,B)),
  phoare[ T(A,B).getState : (glob T(A,B)) = glT ==> (glob T(A,B)) = glT  /\ res = f glT ] = 1%r) /\
    (forall (glT: glob T(A,B)),
  phoare[T(A,B).setState: state = f glT ==> glob T(A,B) = glT] = 1%r).
proof. elim (rewindable_A A RewProp_A).
move => fA [s1 [s2 [s3] ]] s4.
elim (rewindable_A B RewProp_B).
move => fB [t1 [t2 [t3]]] t4.
exists (fun (gc : glob T(A,B)) =>  pair_sbits (ct_sbits (gc.`1), pair_sbits(fA gc.`3 , fB gc.`2) ) ).
progress. move => y z. smt(ips unct_ct).
proc.
have : phoare[ A.getState : (glob A) = (glT.`3) ==> (glob A) = (glT.`3) /\ res = fA (glT.`3)] = 1%r.
apply s2. move => h.
have : phoare[ B.getState : (glob B) = (glT.`2) ==> (glob B) = (glT.`2) /\ res = fB (glT.`2)] = 1%r.
apply t2. move => h'.
call h'.
call h.
skip. progress.
proc. wp.
call (t3 glT.`2).
call (s3 glT.`3).
skip.
progress.
smt(unpair_pair) . smt(unpair_pair). smt(unpair_pair unct_ct).
qed.


local lemma trans_rew :
  exists (f : glob T(A,B) -> sbits),
  injective f /\
  (forall &m, Pr[ T(A,B).getState() @ &m : (glob T(A,B)) = ((glob T(A,B)){m})
                                   /\ res = f ((glob T(A,B)){m} ) ] = 1%r) /\
  (forall &m b (x: glob T(A,B)), b = f x =>
    Pr[T(A,B).setState(b) @ &m : glob T(A,B) = x] = 1%r) /\
  islossless T(A,B).setState.
proof.
elim rewindable_T.
progress.
exists f.
progress.
byphoare (_: (glob T(A,B)) = (glob T(A,B)){m} ==> _) .  proc*. call (H0 (glob T(A,B)){m}).
skip.  progress. auto. auto.
byphoare (_: arg = f x  ==> _).
proc*. call (H1 x).  skip.  progress. auto. auto.
proc.  wp.
elim RewProp_B. progress.
elim RewProp_A. progress.
call H5.
call H9.
skip. auto.
qed.


end section.