Skip to content

Commit 54cb0d0

Browse files
lyonel2017lyonel2017
committed
Add one side while rule with lossless
1 parent 13acf05 commit 54cb0d0

File tree

2 files changed

+206
-97
lines changed

2 files changed

+206
-97
lines changed

‎examples/RWhileSampling.ec

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
require import Real Distr.
2+
3+
type t.
4+
5+
op sample: t distr.
6+
axiom sample_ll: is_lossless sample.
7+
8+
op test: t -> bool.
9+
axiom pr_ntest: 0%r < mu sample (predC test).
10+
11+
module Sample = {
12+
proc sample () : bool = {
13+
var r : t;
14+
var ret : bool;
15+
16+
ret <- true;
17+
r <$ sample;
18+
19+
while (test r) {
20+
r <$ sample;
21+
}
22+
return ret;
23+
}
24+
proc idle () : bool = {
25+
var ret : bool;
26+
27+
ret <- true;
28+
29+
return ret;
30+
}
31+
}.
32+
33+
lemma Sample_lossless:
34+
equiv[Sample.sample ~ Sample.idle : true ==> ={res}].
35+
proof.
36+
proc; seq 2 1: (={ret}) => //.
37+
auto; split.
38+
+ exact/sample_ll.
39+
by auto.
40+
while {1} (={ret}).
41+
* by auto; rewrite sample_ll.
42+
* auto.
43+
seq 0 : true => //=.
44+
while true (if test r then 1 else 0) 1 (mu sample (predC test))=> //.
45+
+ by move=> _ r; case: (test r).
46+
+ move=> ih; seq 1: true=> //.
47+
by auto; rewrite sample_ll.
48+
+ by auto; rewrite sample_ll.
49+
rewrite pr_ntest=> /= z; conseq (: true ==> !test r).
50+
- smt().
51+
by rnd; auto=> />.
52+
auto.
53+
qed.

‎src/phl/ecPhlWhile.ml

Lines changed: 153 additions & 97 deletions
Original file line numberDiff line numberDiff line change
@@ -339,6 +339,147 @@ let t_equiv_while_disj_r side vrnt inv tc =
339339

340340
FApi.xmutate1 tc `While [b_concl; concl]
341341

342+
(* -------------------------------------------------------------------- *)
343+
module LossLess = struct
344+
exception CannotTranslate
345+
346+
let form_of_expr env mother mh =
347+
let map = ref (Mid.add mother (EcPV.PVMap.create env) Mid.empty) in
348+
349+
let rec aux fp =
350+
match fp.f_node with
351+
| Fint z -> e_int z
352+
| Flocal x -> e_local x fp.f_ty
353+
354+
| Fop (p, tys) -> e_op p tys fp.f_ty
355+
| Fapp (f, fs) -> e_app (aux f) (List.map aux fs) fp.f_ty
356+
| Ftuple fs -> e_tuple (List.map aux fs)
357+
| Fproj (f, i) -> e_proj (aux f) i fp.f_ty
358+
359+
| Fif (c, f1, f2) ->
360+
e_if (aux c) (aux f1) (aux f2)
361+
362+
| Fmatch (c, bs, ty) ->
363+
e_match (aux c) (List.map aux bs) ty
364+
365+
| Flet (lp, f1, f2) ->
366+
e_let lp (aux f1) (aux f2)
367+
368+
| Fquant (kd, bds, f) ->
369+
e_quantif (auxkd kd) (List.map auxbd bds) (aux f)
370+
371+
| Fpvar (pv, m) ->
372+
if EcIdent.id_equal m mh then
373+
e_var pv fp.f_ty
374+
else
375+
let bds = odfl (EcPV.PVMap.create env) (Mid.find_opt m !map) in
376+
let idx =
377+
match EcPV.PVMap.find pv bds with
378+
| None ->
379+
let pfx = EcIdent.name m in
380+
let pfx = String.sub pfx 1 (String.length pfx - 1) in
381+
let x = symbol_of_pv pv in
382+
let x = EcIdent.create (x ^ "_" ^ pfx) in
383+
let bds = EcPV.PVMap.add pv (x, fp.f_ty) bds in
384+
map := Mid.add m bds !map; x
385+
| Some (x, _) -> x
386+
387+
in e_local idx fp.f_ty
388+
389+
| Fglob _
390+
| FhoareF _ | FhoareS _
391+
| FeHoareF _ | FeHoareS _
392+
| FbdHoareF _ | FbdHoareS _
393+
| FequivF _ | FequivS _
394+
| FeagerF _ | Fpr _ -> raise CannotTranslate
395+
396+
and auxkd (kd : quantif) : equantif =
397+
match kd with
398+
| Lforall -> `EForall
399+
| Lexists -> `EExists
400+
| Llambda -> `ELambda
401+
402+
and auxbd ((x, bd) : binding) =
403+
match bd with
404+
| GTty ty -> (x, ty)
405+
| _ -> raise CannotTranslate
406+
407+
in fun f -> let e = aux f in (e, !map)
408+
409+
let xhyps evs =
410+
let mtypes = Mid.of_list [evs.es_ml; evs.es_mr] in
411+
412+
fun m fp ->
413+
let fp =
414+
Mid.fold (fun mh pvs fp ->
415+
let mty = Mid.find_opt mh mtypes in
416+
let fp =
417+
EcPV.Mnpv.fold (fun pv (x, ty) fp ->
418+
f_let1 x (f_pvar pv ty mh) fp)
419+
(EcPV.PVMap.raw pvs) fp
420+
in f_forall_mems [mh, oget mty] fp)
421+
m fp
422+
and cnt =
423+
Mid.fold
424+
(fun _ pvs i -> i + 1 + EcPV.Mnpv.cardinal (EcPV.PVMap.raw pvs))
425+
m 0
426+
in (cnt, fp)
427+
end
428+
429+
(* -------------------------------------------------------------------- *)
430+
let t_equiv_ll_while_disj_r side inv tc =
431+
let env = FApi.tc1_env tc in
432+
let es = tc1_as_equivS tc in
433+
let s, m_side, m_other =
434+
match side with
435+
| `Left -> es.es_sl, es.es_ml, es.es_mr
436+
| `Right -> es.es_sr, es.es_mr, es.es_ml in
437+
let (e, c), s = tc1_last_while tc s in
438+
let e = form_of_expr (EcMemory.memory m_side) e in
439+
440+
let (_,ll) =
441+
try
442+
let evs = tc1_as_equivS tc in
443+
let ml = EcMemory.memory evs.es_ml in
444+
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id ml mhr in
445+
let inv = Fsubst.f_subst subst inv in
446+
let e, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml e in
447+
let c = s_while (e, c) in
448+
LossLess.xhyps evs m
449+
(f_bdHoareS (mhr, EcMemory.memtype evs.es_ml) inv c f_true FHeq f_r1)
450+
with LossLess.CannotTranslate ->
451+
tc_error !!tc
452+
"while linking predicates cannot be converted to expressions" in
453+
454+
(* 1. The body preserves the invariant and the loop is lossless. *)
455+
456+
let m_other' = (EcIdent.create "&m", EcMemory.memtype m_other) in
457+
458+
let smem = Fsubst.f_subst_id in
459+
let smem = Fsubst.f_bind_mem smem (EcMemory.memory m_side ) mhr in
460+
let smem = Fsubst.f_bind_mem smem (EcMemory.memory m_other) (EcMemory.memory m_other') in
461+
462+
let b_pre = f_and_simpl inv e in
463+
let b_pre = Fsubst.f_subst smem b_pre in
464+
let b_post = inv in
465+
let b_post = Fsubst.f_subst smem b_post in
466+
let b_concl = f_bdHoareS (mhr, EcMemory.memtype m_side) b_pre c b_post FHeq f_r1 in
467+
let b_concl = b_concl in
468+
let b_concl = f_forall_mems [m_other'] b_concl in
469+
470+
(* 2. WP of the while *)
471+
let post = f_imps_simpl [f_not_simpl e; inv] es.es_po in
472+
let modi = s_write env c in
473+
let post = generalize_mod env (EcMemory.memory m_side) modi post in
474+
let post = f_and_simpl inv post in
475+
let concl =
476+
match side with
477+
| `Left -> f_equivS_r { es with es_sl = s; es_po=post; }
478+
| `Right -> f_equivS_r { es with es_sr = s; es_po=post; }
479+
in
480+
481+
FApi.xmutate1 tc `While [b_concl; ll; concl]
482+
342483
(* -------------------------------------------------------------------- *)
343484
let t_equiv_while_r inv tc =
344485
let env = FApi.tc1_env tc in
@@ -374,6 +515,7 @@ let t_bdhoare_while_rev_geq = FApi.t_low4 "bdhoare-while" t_bdhoare_while_rev_ge
374515
let t_bdhoare_while_rev = FApi.t_low1 "bdhoare-while" t_bdhoare_while_rev_r
375516
let t_equiv_while = FApi.t_low1 "equiv-while" t_equiv_while_r
376517
let t_equiv_while_disj = FApi.t_low3 "equiv-while" t_equiv_while_disj_r
518+
let t_equiv_ll_while_disj = FApi.t_low2 "equiv-while" t_equiv_ll_while_disj_r
377519

378520
(* -------------------------------------------------------------------- *)
379521
let process_while side winfos tc =
@@ -400,7 +542,6 @@ let process_while side winfos tc =
400542
| Some vrnt, None ->
401543
let _, phi = TTC.tc1_process_Xhl_formula tc phi in
402544
let _, vrnt = TTC.tc1_process_Xhl_form tc tint vrnt in
403-
404545
t_bdhoare_while phi vrnt tc
405546

406547
| Some vrnt, Some (`Bd (k, eps)) ->
@@ -410,7 +551,6 @@ let process_while side winfos tc =
410551
let _, eps = TTC.tc1_process_Xhl_form tc treal eps in
411552

412553
t_bdhoare_while_rev_geq phi vrnt k eps tc
413-
414554
| None, None ->
415555
let _, phi = TTC.tc1_process_Xhl_formula tc phi in
416556
t_bdhoare_while_rev phi tc
@@ -430,79 +570,16 @@ let process_while side winfos tc =
430570
(TTC.tc1_process_prhl_formula tc phi)
431571
tc
432572

573+
| Some side, None ->
574+
t_equiv_ll_while_disj side
575+
(TTC.tc1_process_prhl_formula tc phi)
576+
tc
577+
433578
| _ -> tc_error !!tc "invalid arguments"
434579
end
435580

436581
| _ -> tc_error !!tc "expecting a hoare[...]/equiv[...]"
437582

438-
(* -------------------------------------------------------------------- *)
439-
module ASyncWhile = struct
440-
exception CannotTranslate
441-
442-
let form_of_expr env mother mh =
443-
let map = ref (Mid.add mother (EcPV.PVMap.create env) Mid.empty) in
444-
445-
let rec aux fp =
446-
match fp.f_node with
447-
| Fint z -> e_int z
448-
| Flocal x -> e_local x fp.f_ty
449-
450-
| Fop (p, tys) -> e_op p tys fp.f_ty
451-
| Fapp (f, fs) -> e_app (aux f) (List.map aux fs) fp.f_ty
452-
| Ftuple fs -> e_tuple (List.map aux fs)
453-
| Fproj (f, i) -> e_proj (aux f) i fp.f_ty
454-
455-
| Fif (c, f1, f2) ->
456-
e_if (aux c) (aux f1) (aux f2)
457-
458-
| Fmatch (c, bs, ty) ->
459-
e_match (aux c) (List.map aux bs) ty
460-
461-
| Flet (lp, f1, f2) ->
462-
e_let lp (aux f1) (aux f2)
463-
464-
| Fquant (kd, bds, f) ->
465-
e_quantif (auxkd kd) (List.map auxbd bds) (aux f)
466-
467-
| Fpvar (pv, m) ->
468-
if EcIdent.id_equal m mh then
469-
e_var pv fp.f_ty
470-
else
471-
let bds = odfl (EcPV.PVMap.create env) (Mid.find_opt m !map) in
472-
let idx =
473-
match EcPV.PVMap.find pv bds with
474-
| None ->
475-
let pfx = EcIdent.name m in
476-
let pfx = String.sub pfx 1 (String.length pfx - 1) in
477-
let x = symbol_of_pv pv in
478-
let x = EcIdent.create (x ^ "_" ^ pfx) in
479-
let bds = EcPV.PVMap.add pv (x, fp.f_ty) bds in
480-
map := Mid.add m bds !map; x
481-
| Some (x, _) -> x
482-
483-
in e_local idx fp.f_ty
484-
485-
| Fglob _
486-
| FhoareF _ | FhoareS _
487-
| FeHoareF _ | FeHoareS _
488-
| FbdHoareF _ | FbdHoareS _
489-
| FequivF _ | FequivS _
490-
| FeagerF _ | Fpr _ -> raise CannotTranslate
491-
492-
and auxkd (kd : quantif) : equantif =
493-
match kd with
494-
| Lforall -> `EForall
495-
| Lexists -> `EExists
496-
| Llambda -> `ELambda
497-
498-
and auxbd ((x, bd) : binding) =
499-
match bd with
500-
| GTty ty -> (x, ty)
501-
| _ -> raise CannotTranslate
502-
503-
in fun f -> let e = aux f in (e, !map)
504-
end
505-
506583
(* -------------------------------------------------------------------- *)
507584
let process_async_while (winfos : EP.async_while_info) tc =
508585
let e_and e1 e2 =
@@ -587,52 +664,31 @@ let process_async_while (winfos : EP.async_while_info) tc =
587664
in (hr1, hr2)
588665
in
589666

590-
let xhyps =
591-
let mtypes = Mid.of_list [evs.es_ml; evs.es_mr] in
592-
593-
fun m fp ->
594-
let fp =
595-
Mid.fold (fun mh pvs fp ->
596-
let mty = Mid.find_opt mh mtypes in
597-
let fp =
598-
EcPV.Mnpv.fold (fun pv (x, ty) fp ->
599-
f_let1 x (f_pvar pv ty mh) fp)
600-
(EcPV.PVMap.raw pvs) fp
601-
in f_forall_mems [mh, oget mty] fp)
602-
m fp
603-
and cnt =
604-
Mid.fold
605-
(fun _ pvs i -> i + 1 + EcPV.Mnpv.cardinal (EcPV.PVMap.raw pvs))
606-
m 0
607-
in (cnt, fp)
608-
in
609-
610667
let (c1, ll1), (c2, ll2) =
611668
try
612669
let ll1 =
613670
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id ml mhr in
614671
let inv = Fsubst.f_subst subst inv in
615672
let test = f_ands [fe1; f_not p0; p1] in
616-
let test, m = ASyncWhile.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
673+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
617674
let c = s_while (test, cl) in
618-
xhyps m
675+
LossLess.xhyps evs m
619676
(f_bdHoareS (mhr, EcMemory.memtype evs.es_ml) inv c f_true FHeq f_r1)
620677

621678
and ll2 =
622679
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id mr mhr in
623680
let inv = Fsubst.f_subst subst inv in
624681
let test = f_ands [fe1; f_not p0; f_not p1] in
625-
let test, m = ASyncWhile.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
682+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
626683
let c = s_while (test, cr) in
627-
xhyps m
684+
LossLess.xhyps evs m
628685
(f_bdHoareS (mhr, EcMemory.memtype evs.es_mr) inv c f_true FHeq f_r1)
629686

630687
in (ll1, ll2)
631688

632-
with ASyncWhile.CannotTranslate ->
689+
with LossLess.CannotTranslate ->
633690
tc_error !!tc
634-
"async-while linking predicates cannot be converted to expressions"
635-
in
691+
"async-while linking predicates cannot be converted to expressions" in
636692

637693
let concl =
638694
let post = f_imps [f_not fe1; f_not fe2; inv] evs.es_po in

0 commit comments

Comments
 (0)