Skip to content

Commit 12a2ed1

Browse files
Cameron-LowCameron-Low
authored
Improve transitivity* and replace*
1 parent 39ed501 commit 12a2ed1

File tree

7 files changed

+136
-162
lines changed

7 files changed

+136
-162
lines changed

‎examples/ChaChaPoly/chacha_poly.ec‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1123,8 +1123,8 @@ section PROOFS.
11231123
={glob A} ==> ={res, Mem.lc} /\ StLSke.gs{1} = RO.m{2}.
11241124
proof.
11251125
proc *.
1126-
transitivity*{1} { r <@ G3(StLSke(St)).main(); } => //; 1:smt(); 1: by sim.
1127-
transitivity* {2} { r <@ G3(OChaChaPoly(IFinRO)).main(); } => //; 1:smt().
1126+
transitivity* {1} { r <@ G3(StLSke(St)).main(); }; 1: by sim.
1127+
transitivity* {2} { r <@ G3(OChaChaPoly(IFinRO)).main(); }.
11281128
+ inline *; wp.
11291129
call (_: StLSke.gs{1} = OCC.gs{2} /\ ={Mem.k, Mem.log, Mem.lc}).
11301130
+ by proc; inline *; auto => /> &2; case: (p{2}).

‎src/phl/ecPhlOutline.ml‎

Lines changed: 1 addition & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -8,96 +8,8 @@ open EcUnifyProc
88

99
open EcCoreGoal
1010
open EcCoreGoal.FApi
11-
open EcLowGoal
1211
open EcLowPhlGoal
1312

14-
(*---------------------------------------------------------------------------------------*)
15-
(*
16-
Transitivity star with (ideally) lossless pre-conditions over the intermediate
17-
programs, and automatic discharging of the first two goals.
18-
*)
19-
(* FIXME: Move to ecPhlTrans *)
20-
21-
let t_equivS_trans_eq side s tc =
22-
let env = tc1_env tc in
23-
let es = tc1_as_equivS tc in
24-
let c,m = match side with `Left -> es.es_sl, es.es_ml | `Right -> es.es_sr, es.es_mr in
25-
26-
let mem_pre = split_sided (EcMemory.memory m) es.es_pr in
27-
let fv_pr = EcPV.PV.fv env (EcMemory.memory m) es.es_pr in
28-
let fv_po = EcPV.PV.fv env (fst m) es.es_po in
29-
let fv_r = EcPV.s_read env c in
30-
let mk_eqs fv =
31-
let vfv, gfv = EcPV.PV.elements fv in
32-
let veq = List.map (fun (x,ty) -> f_eq (f_pvar x ty mleft) (f_pvar x ty mright)) vfv in
33-
let geq = List.map (fun mp -> f_eqglob mp mleft mp mright) gfv in
34-
f_ands (veq @ geq) in
35-
let pre = mk_eqs (EcPV.PV.union (EcPV.PV.union fv_pr fv_po) fv_r) in
36-
let pre = f_and pre (odfl f_true mem_pre) in
37-
let post = mk_eqs fv_po in
38-
let c1, c2 =
39-
if side = `Left then (pre, post), (es.es_pr, es.es_po)
40-
else (es.es_pr, es.es_po), (pre, post)
41-
in
42-
43-
let exists_subtac (tc : tcenv1) =
44-
(* Ideally these are guaranteed fresh *)
45-
let pl = EcIdent.create "&p__1" in
46-
let pr = EcIdent.create "&p__2" in
47-
let h = EcIdent.create "__" in
48-
let tc = t_intros_i_1 [pl; pr; h] tc in
49-
let goal = tc1_goal tc in
50-
51-
let p = match side with | `Left -> pl | `Right -> pr in
52-
let b = match side with | `Left -> true | `Right -> false in
53-
54-
let handle_exists () =
55-
(* Pairing up the correct variables for the exists intro *)
56-
let vs, fm = EcFol.destr_exists goal in
57-
let eqs_pre, _ =
58-
let l, r = EcFol.destr_and fm in
59-
if b then l, r else r, l
60-
in
61-
let eqs, _ = destr_and eqs_pre in
62-
let eqs = destr_ands ~deep:false eqs in
63-
let doit eq =
64-
let l, r = destr_eq eq in
65-
let l, r = if b then r, l else l, r in
66-
let v = EcFol.destr_local l in
67-
v, r
68-
in
69-
let eqs = List.map doit eqs in
70-
let exvs =
71-
List.map
72-
(fun (id, _) ->
73-
let v = List.assoc id eqs in
74-
Fsubst.f_subst_mem (EcMemory.memory m) p v)
75-
vs
76-
in
77-
78-
as_tcenv1 (t_exists_intro_s (List.map paformula exvs) tc)
79-
in
80-
81-
let tc =
82-
if EcFol.is_exists goal then
83-
handle_exists ()
84-
else
85-
tc
86-
in
87-
88-
t_seq
89-
(t_generalize_hyp ?clear:(Some `Yes) h)
90-
EcHiGoal.process_done
91-
tc
92-
in
93-
94-
let tc = t_seqsub
95-
(EcPhlTrans.t_equivS_trans (EcMemory.memtype m, s) c1 c2)
96-
[exists_subtac; EcHiGoal.process_done; t_id; t_id]
97-
tc
98-
in
99-
tc
100-
10113
(*---------------------------------------------------------------------------------------*)
10214
(*
10315
This is the improved transitivity star from above but allows for a range of code
@@ -121,7 +33,7 @@ let t_outline_stmt side start_pos end_pos s tc =
12133
let code_pref, _, _ = s_split_i env start_pos (stmt rest) in
12234

12335
let new_prog = s_seq (s_seq (stmt code_pref) s) (stmt code_suff) in
124-
let tc = t_equivS_trans_eq side new_prog tc in
36+
let tc = EcPhlTrans.t_equivS_trans_eq side new_prog tc in
12537

12638
(* The middle goal, showing equivalence with the replaced code, ideally solves. *)
12739
let tp = match side with | `Left -> 1 | `Right -> 2 in

‎src/phl/ecPhlOutline.mli‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,6 @@ open EcParsetree
44
open EcModules
55
open EcPath
66

7-
val t_equivS_trans_eq : side -> stmt -> backward
8-
97
val t_outline_stmt : side -> codepos1 -> codepos1 -> stmt -> backward
108
val t_outline_proc : side -> codepos1 -> codepos1 -> xpath -> lvalue option -> backward
119

‎src/phl/ecPhlRwEquiv.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ let t_rewrite_equiv side dir cp (equiv : equivF) equiv_pt rargslv tc =
7171
let prog = s_call (rlv, new_func, rargs) in
7272
let prog = s_seq prefix (s_seq prog suffix) in
7373

74-
let tc = EcPhlOutline.t_equivS_trans_eq side prog tc in
74+
let tc = EcPhlTrans.t_equivS_trans_eq side prog tc in
7575

7676
(* One of the goals can be simplified, often fully, using the provided equiv *)
7777
let tp = match side with | `Left -> 1 | `Right -> 2 in

‎src/phl/ecPhlTrans.ml‎

Lines changed: 125 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -82,85 +82,144 @@ let t_equivS_trans = FApi.t_low3 "equiv-trans" Low.t_equivS_trans_r
8282
let t_equivF_trans = FApi.t_low3 "equiv-trans" Low.t_equivF_trans_r
8383

8484
(* -------------------------------------------------------------------- *)
85-
let process_replace_stmt s p c p1 q1 p2 q2 tc =
85+
let t_equivS_trans_eq side s tc =
86+
let env = FApi.tc1_env tc in
8687
let es = tc1_as_equivS tc in
87-
let ct = match s with `Left -> es.es_sl | `Right -> es.es_sr in
88-
let mt = snd (match s with `Left -> es.es_ml | `Right -> es.es_mr) in
89-
(* Translation of the stmt *)
90-
let regexpstmt = trans_block p in
91-
let map = match RegexpStmt.search regexpstmt ct.s_node with
92-
| None -> Mstr.empty
93-
| Some m -> m in
94-
let c = TTC.tc1_process_prhl_stmt tc s ~map c in
95-
t_equivS_trans (mt, c) (p1, q1) (p2, q2) tc
88+
let c, m = match side with `Left -> es.es_sl, es.es_ml | `Right -> es.es_sr, es.es_mr in
89+
90+
let mem_pre = EcFol.split_sided (EcMemory.memory m) es.es_pr in
91+
let fv_pr = EcPV.PV.fv env (EcMemory.memory m) es.es_pr in
92+
let fv_po = EcPV.PV.fv env (fst m) es.es_po in
93+
let fv_r = EcPV.s_read env c in
94+
let mk_eqs fv =
95+
let vfv, gfv = EcPV.PV.elements fv in
96+
let veq = List.map (fun (x,ty) -> f_eq (f_pvar x ty mleft) (f_pvar x ty mright)) vfv in
97+
let geq = List.map (fun mp -> f_eqglob mp mleft mp mright) gfv in
98+
f_ands (veq @ geq) in
99+
let pre = mk_eqs (EcPV.PV.union (EcPV.PV.union fv_pr fv_po) fv_r) in
100+
let pre = f_and pre (odfl f_true mem_pre) in
101+
let post = mk_eqs fv_po in
102+
let c1, c2 =
103+
if side = `Left then (pre, post), (es.es_pr, es.es_po)
104+
else (es.es_pr, es.es_po), (pre, post)
105+
in
106+
107+
let exists_subtac (tc : tcenv1) =
108+
(* Ideally these are guaranteed fresh *)
109+
let pl = EcIdent.create "&p__1" in
110+
let pr = EcIdent.create "&p__2" in
111+
let h = EcIdent.create "__" in
112+
let tc = EcLowGoal.t_intros_i_1 [pl; pr; h] tc in
113+
let goal = FApi.tc1_goal tc in
114+
115+
let p = match side with | `Left -> pl | `Right -> pr in
116+
let b = match side with | `Left -> true | `Right -> false in
117+
118+
let handle_exists () =
119+
(* Pairing up the correct variables for the exists intro *)
120+
let vs, fm = EcFol.destr_exists goal in
121+
let eqs_pre, _ =
122+
let l, r = EcFol.destr_and fm in
123+
if b then l, r else r, l
124+
in
125+
let eqs, _ = destr_and eqs_pre in
126+
let eqs = destr_ands ~deep:false eqs in
127+
let doit eq =
128+
let l, r = EcFol.destr_eq eq in
129+
let l, r = if b then r, l else l, r in
130+
let v = EcFol.destr_local l in
131+
v, r
132+
in
133+
let eqs = List.map doit eqs in
134+
let exvs =
135+
List.map
136+
(fun (id, _) ->
137+
let v = List.assoc id eqs in
138+
Fsubst.f_subst_mem (EcMemory.memory m) p v)
139+
vs
140+
in
141+
142+
FApi.as_tcenv1 (EcLowGoal.t_exists_intro_s (List.map paformula exvs) tc)
143+
in
144+
145+
let tc =
146+
if EcFol.is_exists goal then
147+
handle_exists ()
148+
else
149+
tc
150+
in
151+
152+
FApi.t_seq
153+
(EcLowGoal.t_generalize_hyp ?clear:(Some `Yes) h)
154+
EcHiGoal.process_done
155+
tc
156+
in
157+
158+
FApi.t_seqsub
159+
(t_equivS_trans (EcMemory.memtype m, s) c1 c2)
160+
[exists_subtac; EcHiGoal.process_done; EcLowGoal.t_id; EcLowGoal.t_id]
161+
tc
96162

97163
(* -------------------------------------------------------------------- *)
98-
let process_trans_stmt s c p1 q1 p2 q2 tc =
164+
let process_trans_stmt tf s ?pat c tc =
165+
let hyps = FApi.tc1_hyps tc in
99166
let es = tc1_as_equivS tc in
100167
let mt = snd (match s with `Left -> es.es_ml | `Right -> es.es_mr) in
168+
101169
(* Translation of the stmt *)
102-
let c = TTC.tc1_process_prhl_stmt tc s c in
103-
t_equivS_trans (mt,c) (p1, q1) (p2, q2) tc
170+
let map =
171+
match pat with
172+
| None -> Mstr.empty
173+
| Some p -> begin
174+
let regexpstmt = trans_block p in
175+
let ct = match s with `Left -> es.es_sl | `Right -> es.es_sr in
176+
match RegexpStmt.search regexpstmt ct.s_node with
177+
| None -> Mstr.empty
178+
| Some m -> m
179+
end
180+
in
181+
let c = TTC.tc1_process_prhl_stmt tc s ~map c in
182+
183+
match tf with
184+
| TFeq ->
185+
t_equivS_trans_eq s c tc
186+
| TFform (p1, q1, p2, q2) ->
187+
let p1, q1 =
188+
let hyps = LDecl.push_all [es.es_ml; (mright, mt)] hyps in
189+
TTC.pf_process_form !!tc hyps tbool p1, TTC.pf_process_form !!tc hyps tbool q1
190+
in
191+
let p2, q2 =
192+
let hyps = LDecl.push_all [(mleft, mt); es.es_mr] hyps in
193+
TTC.pf_process_form !!tc hyps tbool p2, TTC.pf_process_form !!tc hyps tbool q2
194+
in
195+
t_equivS_trans (mt, c) (p1, q1) (p2, q2) tc
104196

105197
(* -------------------------------------------------------------------- *)
106198
let process_trans_fun f p1 q1 p2 q2 tc =
107-
let env = FApi.tc1_env tc in
199+
let env, hyps, _ = FApi.tc1_eflat tc in
200+
let ef = tc1_as_equivF tc in
108201
let f = EcTyping.trans_gamepath env f in
202+
let (_, prmt), (_, pomt) = Fun.hoareF_memenv f env in
203+
let (prml, prmr), (poml, pomr) = Fun.equivF_memenv ef.ef_fl ef.ef_fr env in
204+
let process ml mr fo =
205+
TTC.pf_process_form !!tc (LDecl.push_all [ml; mr] hyps) tbool fo in
206+
let p1 = process prml (mright, prmt) p1 in
207+
let q1 = process poml (mright, pomt) q1 in
208+
let p2 = process (mleft,prmt) prmr p2 in
209+
let q2 = process (mleft,pomt) pomr q2 in
109210
t_equivF_trans f (p1, q1) (p2, q2) tc
110211

111212
(* -------------------------------------------------------------------- *)
112213
let process_equiv_trans (tk, tf) tc =
113-
let env, hyps, _ = FApi.tc1_eflat tc in
114-
115-
let (p1, q1, p2, q2) =
214+
match tk with
215+
| TKfun f -> begin
116216
match tf with
117-
| TFform(p1, q1, p2, q2) ->
118-
begin match tk with
119-
| TKfun f ->
120-
let ef = tc1_as_equivF tc in
121-
let f = EcTyping.trans_gamepath env f in
122-
let (_, prmt), (_, pomt) = Fun.hoareF_memenv f env in
123-
let (prml, prmr), (poml, pomr) = Fun.equivF_memenv ef.ef_fl ef.ef_fr env in
124-
let process ml mr fo =
125-
TTC.pf_process_form !!tc (LDecl.push_all [ml; mr] hyps) tbool fo in
126-
let p1 = process prml (mright, prmt) p1 in
127-
let q1 = process poml (mright, pomt) q1 in
128-
let p2 = process (mleft,prmt) prmr p2 in
129-
let q2 = process (mleft,pomt) pomr q2 in
130-
(p1,q1,p2,q2)
131-
| TKstmt (s, _) | TKparsedStmt (s, _, _) ->
132-
let es = tc1_as_equivS tc in
133-
let mt = snd (match s with `Left -> es.es_ml | `Right -> es.es_mr) in
134-
let p1, q1 =
135-
let hyps = LDecl.push_all [es.es_ml; (mright, mt)] hyps in
136-
TTC.pf_process_form !!tc hyps tbool p1,
137-
TTC.pf_process_form !!tc hyps tbool q1 in
138-
let p2, q2 =
139-
let hyps = LDecl.push_all [(mleft, mt); es.es_mr] hyps in
140-
TTC.pf_process_form !!tc hyps tbool p2,
141-
TTC.pf_process_form !!tc hyps tbool q2 in
142-
(p1,q1,p2,q2)
143-
end
144217
| TFeq ->
145-
let side =
146-
match tk with
147-
| TKfun _ -> tc_error !!tc "transitivity * does not work on functions"
148-
| TKstmt(s,_) -> s
149-
| TKparsedStmt(s,_,_) -> s in
150-
let es = tc1_as_equivS tc in
151-
let c,m = match side with `Left -> es.es_sl, es.es_ml | `Right -> es.es_sr, es.es_mr in
152-
let fv = EcPV.PV.fv env (fst m) es.es_po in
153-
let fvr = EcPV.s_read env c in
154-
let mk_eqs fv =
155-
let vfv, gfv = EcPV.PV.elements fv in
156-
let veq = List.map (fun (x,ty) -> f_eq (f_pvar x ty mleft) (f_pvar x ty mright)) vfv in
157-
let geq = List.map (fun mp -> f_eqglob mp mleft mp mright) gfv in
158-
f_ands (veq @ geq) in
159-
let pre = mk_eqs (EcPV.PV.union fvr fv) in
160-
let post = mk_eqs fv in
161-
if side = `Left then (pre, post, es.es_pr, es.es_po)
162-
else (es.es_pr, es.es_po, pre, post) in
163-
match tk with
164-
| TKfun f -> process_trans_fun f p1 q1 p2 q2 tc
165-
| TKstmt (s, c) -> process_trans_stmt s c p1 q1 p2 q2 tc
166-
| TKparsedStmt (s, p, c) -> process_replace_stmt s p c p1 q1 p2 q2 tc
218+
tc_error !!tc "transitivity * does not work on functions"
219+
| TFform (p1, q1, p2, q2) ->
220+
process_trans_fun f p1 q1 p2 q2 tc
221+
end
222+
| TKstmt (side, stmt) ->
223+
process_trans_stmt tf side stmt tc
224+
| TKparsedStmt (side, pat, stmt) ->
225+
process_trans_stmt tf side ~pat:pat stmt tc

‎src/phl/ecPhlTrans.mli‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,11 @@ val t_equivF_trans :
3232
-> EcFol.form * EcFol.form
3333
-> EcCoreGoal.FApi.backward
3434

35+
(*---------------------------------------------------------------------------------------*)
36+
(* Completely change the code of `side` *)
37+
val t_equivS_trans_eq :
38+
side -> EcModules.stmt -> EcCoreGoal.FApi.backward
39+
3540
(* -------------------------------------------------------------------- *)
3641
val process_equiv_trans :
3742
trans_kind * trans_formula -> backward

‎theories/crypto/PROM.ec‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -918,7 +918,7 @@ equiv RO_FinRO_D : MainD(D,RO).distinguish ~ MainD(D,FinRO).distinguish :
918918
={glob D, arg} ==> ={res, glob D}.
919919
proof.
920920
proc *.
921-
transitivity*{1} {r <@ MainD(D, GenFinRO(LRO)).distinguish(x); } => //;1:smt().
921+
transitivity*{1} {r <@ MainD(D, GenFinRO(LRO)).distinguish(x); }.
922922
+ inline MainD(D, RO).distinguish MainD(D, GenFinRO(LRO)).distinguish; wp.
923923
call (_: ={glob RO});2..4: by sim.
924924
+ by apply RO_LFinRO_init.
@@ -989,7 +989,7 @@ proc.
989989
transitivity*{2} {
990990
Vars.r <@ S.sample(dout,FinFrom.enum);
991991
FunRO.f <- tofun Vars.r;
992-
}; 1,2: smt(); last first.
992+
}; last first.
993993
- inline*; rnd : *0 *0; skip => />.
994994
by split => *; rewrite dmap_id dfun_dmap.
995995
rewrite equiv[{2} 1 Sample_Loop_first_eq].

0 commit comments

Comments
 (0)