Skip to content

Commit e6c14f7

Browse files
lyonel2017strub
lyonel2017
authored and
strub
committed
Add one sided while rule with lossless proof:
{I} while b do c {T} {I}c{I} P => I /\ (not b => I => Q) ------------------------------------------------------------- {P} while b do c ~ skip {Q} {I} while b do c {T} {I}c{I} P => I /\ (not b => I => Q) ------------------------------------------------------------- {P} skip ~ while b do c {Q}
1 parent ab8e28b commit e6c14f7

File tree

2 files changed

+232
-95
lines changed

2 files changed

+232
-95
lines changed

‎examples/RWhileSampling.ec‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
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});auto.
37+
split.
38+
+ by 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+
+ by smt().
51+
by rnd; auto.
52+
by auto.
53+
qed.
54+
55+
lemma Sample_lossless2:
56+
equiv[Sample.idle ~ Sample.sample : true ==> ={res}].
57+
proof.
58+
proc; seq 1 2: (={ret});auto.
59+
split.
60+
+ by exact /sample_ll.
61+
by auto.
62+
while {2} (={ret}).
63+
+ by auto; rewrite sample_ll.
64+
+ auto.
65+
seq 0 : true => //=.
66+
while true (if test r then 1 else 0) 1 (mu sample (predC test)) => //.
67+
+ by move => _ r; case: (test r).
68+
+ move => ih; seq 1: true => //.
69+
by auto; rewrite sample_ll.
70+
+ by auto; rewrite sample_ll.
71+
rewrite pr_ntest=> /= z; conseq (: true ==> !test r).
72+
+ by smt().
73+
by rnd; auto.
74+
by auto.
75+
qed.

‎src/phl/ecPhlWhile.ml‎

Lines changed: 157 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -339,6 +339,152 @@ 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 m_side 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 m_other) ml e in
447+
let c = s_while (e, c) in
448+
LossLess.xhyps evs m
449+
(f_bdHoareS (mhr, EcMemory.memtype m_side) inv c f_true FHeq f_r1)
450+
with LossLess.CannotTranslate ->
451+
tc_error !!tc
452+
"while linking predicates cannot be converted to expressions"
453+
in
454+
455+
(* 1. The body preserves the invariant and the loop is lossless. *)
456+
457+
let m_other' = (EcIdent.create "&m", EcMemory.memtype m_other) in
458+
459+
let smem = Fsubst.f_subst_id in
460+
let smem = Fsubst.f_bind_mem smem (EcMemory.memory m_side ) mhr in
461+
let smem =
462+
Fsubst.f_bind_mem smem (EcMemory.memory m_other) (EcMemory.memory m_other')
463+
in
464+
465+
let b_pre = f_and_simpl inv e in
466+
let b_pre = Fsubst.f_subst smem b_pre in
467+
let b_post = inv in
468+
let b_post = Fsubst.f_subst smem b_post in
469+
let b_concl =
470+
f_bdHoareS (mhr, EcMemory.memtype m_side) b_pre c b_post FHeq f_r1
471+
in
472+
let b_concl = b_concl in
473+
let b_concl = f_forall_mems [m_other'] b_concl in
474+
475+
(* 2. WP of the while *)
476+
let post = f_imps_simpl [f_not_simpl e; inv] es.es_po in
477+
let modi = s_write env c in
478+
let post = generalize_mod env (EcMemory.memory m_side) modi post in
479+
let post = f_and_simpl inv post in
480+
let concl =
481+
match side with
482+
| `Left -> f_equivS_r { es with es_sl = s; es_po=post; }
483+
| `Right -> f_equivS_r { es with es_sr = s; es_po=post; }
484+
in
485+
486+
FApi.xmutate1 tc `While [b_concl; ll; concl]
487+
342488
(* -------------------------------------------------------------------- *)
343489
let t_equiv_while_r inv tc =
344490
let env = FApi.tc1_env tc in
@@ -374,6 +520,7 @@ let t_bdhoare_while_rev_geq = FApi.t_low4 "bdhoare-while" t_bdhoare_while_rev_ge
374520
let t_bdhoare_while_rev = FApi.t_low1 "bdhoare-while" t_bdhoare_while_rev_r
375521
let t_equiv_while = FApi.t_low1 "equiv-while" t_equiv_while_r
376522
let t_equiv_while_disj = FApi.t_low3 "equiv-while" t_equiv_while_disj_r
523+
let t_equiv_ll_while_disj = FApi.t_low2 "equiv-while" t_equiv_ll_while_disj_r
377524

378525
(* -------------------------------------------------------------------- *)
379526
let process_while side winfos tc =
@@ -400,7 +547,6 @@ let process_while side winfos tc =
400547
| Some vrnt, None ->
401548
let _, phi = TTC.tc1_process_Xhl_formula tc phi in
402549
let _, vrnt = TTC.tc1_process_Xhl_form tc tint vrnt in
403-
404550
t_bdhoare_while phi vrnt tc
405551

406552
| Some vrnt, Some (`Bd (k, eps)) ->
@@ -410,7 +556,6 @@ let process_while side winfos tc =
410556
let _, eps = TTC.tc1_process_Xhl_form tc treal eps in
411557

412558
t_bdhoare_while_rev_geq phi vrnt k eps tc
413-
414559
| None, None ->
415560
let _, phi = TTC.tc1_process_Xhl_formula tc phi in
416561
t_bdhoare_while_rev phi tc
@@ -430,79 +575,16 @@ let process_while side winfos tc =
430575
(TTC.tc1_process_prhl_formula tc phi)
431576
tc
432577

578+
| Some side, None ->
579+
t_equiv_ll_while_disj side
580+
(TTC.tc1_process_prhl_formula tc phi)
581+
tc
582+
433583
| _ -> tc_error !!tc "invalid arguments"
434584
end
435585

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

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-
506588
(* -------------------------------------------------------------------- *)
507589
let process_async_while (winfos : EP.async_while_info) tc =
508590
let e_and e1 e2 =
@@ -587,49 +669,29 @@ let process_async_while (winfos : EP.async_while_info) tc =
587669
in (hr1, hr2)
588670
in
589671

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-
610672
let (c1, ll1), (c2, ll2) =
611673
try
612674
let ll1 =
613675
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id ml mhr in
614676
let inv = Fsubst.f_subst subst inv in
615677
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
678+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
617679
let c = s_while (test, cl) in
618-
xhyps m
680+
LossLess.xhyps evs m
619681
(f_bdHoareS (mhr, EcMemory.memtype evs.es_ml) inv c f_true FHeq f_r1)
620682

621683
and ll2 =
622684
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id mr mhr in
623685
let inv = Fsubst.f_subst subst inv in
624686
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
687+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
626688
let c = s_while (test, cr) in
627-
xhyps m
689+
LossLess.xhyps evs m
628690
(f_bdHoareS (mhr, EcMemory.memtype evs.es_mr) inv c f_true FHeq f_r1)
629691

630692
in (ll1, ll2)
631693

632-
with ASyncWhile.CannotTranslate ->
694+
with LossLess.CannotTranslate ->
633695
tc_error !!tc
634696
"async-while linking predicates cannot be converted to expressions"
635697
in

0 commit comments

Comments
 (0)