Skip to content

Commit 4a9cd91

Browse files
lyonel2017strub
lyonel2017
authored and
strub
committed
Fix async while obligations and document the tactic
1 parent 78cf6eb commit 4a9cd91

6 files changed

Lines changed: 249 additions & 57 deletions

File tree

‎doc/tactics/async-while.rst‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
========================================================================
2+
Tactic: ``async while`` Tactic
3+
========================================================================
4+
5+
The ``async while`` tactic applies to probabilistic relational Hoare Logic
6+
goals where the programs contains a ``while`` loop.
7+
Unlike the ``while`` tactic, the ``async while`` tactic allows to reason
8+
on loops which are not in lockstep.
9+
10+
------------------------------------------------------------------------
11+
Syntax
12+
------------------------------------------------------------------------
13+
14+
The general form of the tactic is:
15+
16+
.. admonition:: Syntax
17+
18+
``async while [f1,k1] [f2,k2] (L1) (L2) : (I)``
19+
20+
Here:
21+
22+
- ``L1`` and ``L2`` are the left and right condition to control if we
23+
consider the lockstep case, or the oneside case,
24+
- ``k1`` and ``k2`` are natural number
25+
- ``f1`` and ``f2`` are the unrolling condition, initial by the parameter
26+
``k1`` and ``k2``.
27+
28+
Concretely, the tactic implements the following rule::
29+
30+
I => (b1 <=> b2 /\ (!L1 /\ !L2 => f1 k1 /\ f2 k2)) \/ (L1 /\ b1) \/ (L2 /\ b2)
31+
equiv[ while (b1 /\ f1 k1) {c1} ~ while (b2 /\ f2 k2) {c2}:
32+
I /\ b1 <=> b2 /\ !L1 /\ !L2 /\ f1 k1 /\ f2 k2 ==> I ]
33+
hoare[ c1: I /\ b1 /\ L1 /\ ==> I ]
34+
hoare[ c2: I /\ b2 /\ L2 /\ ==> I ]
35+
phoare[ while b1 {c1}: I /\ b1 /\ L1 /\ ==> True ]
36+
phoare[ while b2 {c2}: I /\ b2 /\ L2 /\ ==> True ]
37+
(Pre => I) /\ (I /\ !b1 /\ !b2 => Post)
38+
-------------------------------------------------------------------------------
39+
equiv[while b1 {c1} ~ while b2 {c2}: Pre ==> Post]
40+
41+
The following example shows ``async while`` on a prhl goal. The program
42+
increments ``x`` until it reaches ``10``.
43+
44+
.. ecproof::
45+
46+
require import AllCore.
47+
48+
module M = {
49+
proc up_to_10(x : int) : int = {
50+
while (x < 10) {
51+
x <- x + 1;
52+
}
53+
return x;
54+
}
55+
proc up_to_10_by_2(x : int) : int = {
56+
while (x < 10) {
57+
x <- x + 1;
58+
if ( x < 10) x <- x + 1;
59+
}
60+
return x;
61+
}
62+
63+
}.
64+
65+
lemma asynctwhile_example :
66+
equiv[M.up_to_10 ~ M.up_to_10_by_2 : ={x} ==> ={res}].
67+
proof.
68+
proc.
69+
async while
70+
[ (fun r => x <= r + 1), (x{1} ) ]
71+
[ (fun r => x <= r ), (x{2} ) ]
72+
(!(x{1} < 10)) (!(x{2} < 10))
73+
: (x{1} = x{2}).
74+
+ move=> &1 &2 => /#.
75+
+ move => v1 v2 //=.
76+
unroll {1} 1.
77+
unroll {1} 2.
78+
unroll {2} 1.
79+
rcondt {1} 1; auto.
80+
rcondt {2} 1; auto.
81+
sp 1 1.
82+
if => //.
83+
sp 1 1.
84+
while (!(x{1} < 10 /\ (x{1} < 10 /\ (x{1} <= v1 + 1))) /\
85+
!(x{2} < 10 /\ (x{2} < 10 /\ (x{2} <= v2 ))) /\ ={x}); auto => /#.
86+
while (!(x{1} < 10 /\ (x{1} < 10 /\ (x{1} <= v1 + 1))) /\
87+
!(x{2} < 10 /\ (x{2} < 10 /\ (x{2} <= v2 ))) /\ ={x}); auto => /#.
88+
+ move => &2; exfalso=> &1 ? /#.
89+
+ move => &1; exfalso=> &2 ? /#.
90+
+ exfalso => /#.
91+
+ exfalso => /#.
92+
+ by auto.
93+
qed.

‎examples/async-while.ec‎

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -50,26 +50,24 @@ seq 1 1 : (i{1} = 0 /\ ={glob A, x, i}) => //.
5050
async while
5151
[ (fun r => i%r < k%r * r), (i{2} + 1)%r ]
5252
[ (fun r => i%r < r), (i{2} + 1)%r ]
53-
(i{1} < n * k /\ i{2} < n) (!(i{2} < n))
53+
(!(i{1} < n * k)) (!(i{2} < n))
5454
:
5555
(={glob A, x} /\ i{1} = k * i{2} /\ (0 <= i{1})) => //=.
56-
+ by move=> &1 &2 />; smt(gt0_k).
57-
+ by move=> &1 &2 />; smt(gt0_k).
58-
+ by move=> &2; exfalso=> &1; smt(gt0_k).
59-
+ by move=> &2; exfalso=> &1 ?; smt(gt0_k).
56+
+ move=> &1 &2 />; smt(gt0_k).
6057
+ move=> v1 v2.
6158
rcondt {2} 1; 1: by auto => /> /#.
6259
rcondf{2} 4; 1: by auto; conseq (_: true);auto.
63-
wp;while ( ={glob A, x}
60+
wp;while ( ={glob A, x}
6461
/\ i{1} = k * i{2} + j{2}
6562
/\ v1 = (i{2} + 1)%r
6663
/\ 0 <= i{2} < n
6764
/\ 0 <= j{2} <= k) => /=; last by auto; smt(gt0_k ge0_n).
6865
wp; call (_ : true); skip => &1 &2 /= />.
69-
rewrite -fromintM !lt_fromint => *.
70-
by have := StdOrder.IntOrder.ler_wpmul2l k _ i{2} (n - 1); smt().
71-
+ by while true (n * k - i) => //; auto;1: call llA; auto => /#.
66+
rewrite -fromintM !lt_fromint => *.
67+
by have := StdOrder.IntOrder.ler_wpmul2l k _ i{2} (n - 1); smt().
68+
+ by move=> &2; exfalso=> &1 ? ; smt(gt0_k).
69+
+ by move=> &1; exfalso=> &2 ?; smt(gt0_k).
70+
+ while true (n * k - i) => //; auto;1: call llA; auto => /#.
7271
+ while true (n - i);2: by auto=>/#.
7372
move=> z;wp; while (true) (k - j);auto;1:call llA;auto => /#.
7473
qed.
75-

‎examples/async_while.ec‎

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
require import AllCore.
2+
3+
module M = {
4+
proc up_to_10(x : int) : int = {
5+
while (x < 10) {
6+
x <- x + 1;
7+
}
8+
return x;
9+
}
10+
proc up_to_10_by_2(x : int) : int = {
11+
while (x < 10) {
12+
x <- x + 1;
13+
if ( x < 10) x <- x + 1;
14+
}
15+
return x;
16+
}
17+
18+
}.
19+
20+
lemma asynctwhile_example :
21+
equiv[M.up_to_10 ~ M.up_to_10_by_2 : ={x} ==> ={res}].
22+
proof.
23+
proc.
24+
async while
25+
[ (fun r => x <= r + 1), (x{1} ) ]
26+
[ (fun r => x <= r ), (x{2} ) ]
27+
(!(x{1} < 10)) (!(x{2} < 10))
28+
: (x{1} = x{2}).
29+
+ move=> &1 &2 => /#.
30+
+ move => v1 v2 //=.
31+
unroll {1} 1.
32+
unroll {1} 2.
33+
unroll {2} 1.
34+
rcondt {1} 1; auto.
35+
rcondt {2} 1; auto.
36+
sp 1 1.
37+
if => //.
38+
sp 1 1.
39+
while (!(x{1} < 10 /\ (x{1} < 10 /\ (x{1} <= v1 + 1))) /\
40+
!(x{2} < 10 /\ (x{2} < 10 /\ (x{2} <= v2 ))) /\ ={x}); auto => /#.
41+
while (!(x{1} < 10 /\ (x{1} < 10 /\ (x{1} <= v1 + 1))) /\
42+
!(x{2} < 10 /\ (x{2} < 10 /\ (x{2} <= v2 ))) /\ ={x}); auto => /#.
43+
+ move => &2; exfalso=> &1 ? /#.
44+
+ move => &1; exfalso=> &2 ? /#.
45+
+ exfalso => /#.
46+
+ exfalso => /#.
47+
+ by auto.
48+
qed.
49+
50+
module M1 = {
51+
proc spin_once(i1:bool): bool = {
52+
while (i1) {
53+
i1 <- !i1;
54+
}
55+
return i1;
56+
}
57+
58+
proc spin(i2:bool): bool = {
59+
while (i2) {
60+
}
61+
return i2;
62+
}
63+
}.
64+
65+
op b0:bool.
66+
op b1:bool.
67+
op b2:bool.
68+
op b3:bool.
69+
op b4:bool.
70+
op f1:int -> bool.
71+
op n1:int.
72+
op f2:int -> bool.
73+
op n2:int.
74+
75+
equiv L: M1.spin_once ~ M1.spin:
76+
b0 ==> b4.
77+
proof.
78+
proc.
79+
async while [f1,n1] [f2,n2] (b1) (b2) : (b3).
80+
- admit. (* soundness condition*)
81+
- admit. (*left*)
82+
- admit. (*right*)
83+
- admit. (*lockstep equiv*)
84+
- admit. (*losless left*)
85+
- admit. (*losless right*)
86+
- admit. (*invariant implies post*)
87+
qed.

‎src/ecPrinting.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1986,7 +1986,7 @@ and pp_form_core_r
19861986
let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
19871987
let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
19881988
let { main = post; exnmap = (poe, d) } = (hf_po hf).hsi_inv in
1989-
Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
1989+
Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a@]@]]"
19901990
(pp_funname ppe) hf.hf_f
19911991
(pp_pl_mem_binding pm ppe) hf.hf_m
19921992
(pp_form ppepr) (hf_pr hf).inv
@@ -1997,7 +1997,7 @@ and pp_form_core_r
19971997
let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in
19981998
let { main = post; exnmap = (poe, d); } = (hs_po hs).hsi_inv in
19991999
let pm = debug_mode || (fst hs.hs_m).id_symb <> "&hr" in
2000-
Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
2000+
Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a@]@]]"
20012001
(pp_stmt_for_form ppe) hs.hs_s
20022002
(pp_pl_mem_binding pm ppe) (fst hs.hs_m)
20032003
(pp_form ppe) (hs_pr hs).inv

‎src/phl/ecPhlWhile.ml‎

Lines changed: 46 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -628,39 +628,56 @@ let process_async_while (winfos : EP.async_while_info) tc =
628628
let (er, cr), sr = tc1_last_while tc evs.es_sr in
629629

630630
let inv = TTC.tc1_process_prhl_formula tc inv in
631+
631632
let p0 = TTC.tc1_process_prhl_formula tc p0 in
632633
let p1 = TTC.tc1_process_prhl_formula tc p1 in
634+
633635
let f1 = TTC.tc1_process_prhl_form_opt tc None f1 in
634636
let f2 = TTC.tc1_process_prhl_form_opt tc None f2 in
637+
635638
let t1 = TTC.tc1_process_Xhl_exp tc (Some `Left ) (Some (tfun f1.inv.f_ty tbool)) t1 in
636639
let t2 = TTC.tc1_process_Xhl_exp tc (Some `Right) (Some (tfun f2.inv.f_ty tbool)) t2 in
640+
637641
let ft1 = ss_inv_generalize_right (ss_inv_of_expr ml t1) mr in
638642
let ft2 = ss_inv_generalize_left (ss_inv_of_expr mr t2) ml in
643+
639644
let fe1 = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in
640645
let fe2 = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in
641-
let fe = map_ts_inv2 f_or fe1 fe2 in
646+
642647
let f_app' f = f_app (List.hd f) (List.tl f) tbool in
643648
let f_imps' f = f_imps (List.tl f) (List.hd f) in
644-
let cond1 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
645-
(map_ts_inv f_imps' [map_ts_inv f_ands [fe1; fe2;
646-
map_ts_inv f_app' [ft1; f1];
647-
map_ts_inv f_app' [ft2; f2]];
648-
inv; fe; p0]) in
649-
650-
let cond2 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
651-
(map_ts_inv f_imps' [fe1; inv; fe; map_ts_inv1 f_not p0; p1]) in
652649

653-
let cond3 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
654-
(map_ts_inv f_imps' [fe2; inv; fe; map_ts_inv1 f_not p0; map_ts_inv1 f_not p1]) in
650+
let fe = map_ts_inv2 f_eq fe1 fe2 in
651+
let neg_p0 f = map_ts_inv f_imps' [f; map_ts_inv1 f_not p0] in
652+
let neg_p1 f = map_ts_inv f_imps' [f; map_ts_inv1 f_not p1] in
653+
let fprog =
654+
let ft1 = map_ts_inv f_app' [ft1; f1] in
655+
let ft2 = map_ts_inv f_app' [ft2; f2] in
656+
neg_p0 (neg_p1 (map_ts_inv f_ands [ft1;ft2]))
657+
in
658+
let flock = map_ts_inv f_ands [fe;fprog] in
659+
let fc1 = map_ts_inv f_ands [fe1; p0] in
660+
let fc2 = map_ts_inv f_ands [fe2; p1] in
661+
662+
let cond =
663+
EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
664+
(map_ts_inv f_imps'
665+
[map_ts_inv f_ors [flock; fc1; fc2]; inv])
666+
in
655667

656668
let xwh =
657669
let v1, v2 = as_seq2 (EcEnv.LDecl.fresh_ids hyps ["v1_"; "v2_"]) in
658670
let fv1 = {ml;mr;inv=f_local v1 f1.inv.f_ty} in
659671
let fv2 = {ml;mr;inv=f_local v2 f2.inv.f_ty} in
660672
let ev1 = e_local v1 f1.inv.f_ty in
661673
let ev2 = e_local v2 f2.inv.f_ty in
674+
let p0 = map_ts_inv f_ands [map_ts_inv1 f_not p0;map_ts_inv1 f_not p1] in
675+
let fe = map_ts_inv f_ands [fe1;fe2] in
676+
let ft1 = map_ts_inv f_app' [ft1; fv1] in
677+
let ft2 = map_ts_inv f_app' [ft2; fv2] in
678+
let fprog = map_ts_inv f_ands [ft1;ft2] in
662679
let eq1 = map_ts_inv2 f_eq fv1 f1 and eq2 = map_ts_inv2 f_eq fv2 f2 in
663-
let pr = map_ts_inv f_ands [inv; fe; p0; eq1; eq2] in
680+
let pr = map_ts_inv f_ands [inv; fe; fprog; p0; eq1; eq2] in
664681
let po = inv in
665682
let wl = s_while (e_and el (e_app t1 [ev1] tbool), cl) in
666683
let wr = s_while (e_and er (e_app t2 [ev2] tbool), cr) in
@@ -670,38 +687,41 @@ let process_async_while (winfos : EP.async_while_info) tc =
670687

671688
let hr1, hr2 =
672689
let hr1 =
673-
let el = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in
674-
let pre = map_ts_inv f_ands [inv; el ; map_ts_inv1 f_not p0; p1] in
690+
let pre = map_ts_inv f_ands [inv; fe1 ; p0] in
675691
EcSubst.f_forall_mems_ss_inv evs.es_mr
676692
(ts_inv_lower_left2
677693
(fun pr po -> f_hoareS (snd evs.es_ml) pr cl (POE.lift po)) pre inv)
678694

679695
and hr2 =
680-
let er = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in
681-
let pre = map_ts_inv f_ands [inv; er; map_ts_inv1 f_not p0; map_ts_inv1 f_not p1] in
696+
let pre = map_ts_inv f_ands [inv; fe2; p1] in
682697
EcSubst.f_forall_mems_ss_inv evs.es_ml
683698
(ts_inv_lower_right2
684699
(fun pr po -> f_hoareS (snd evs.es_mr) pr cr (POE.lift po)) pre inv)
685700

686701
in (hr1, hr2)
687702
in
688703

689-
690704
let (c1, ll1), (c2, ll2) =
691705
try
692706
let ll1 =
693-
let test = f_ands [fe1.inv; f_not p0.inv; p1.inv] in
694-
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
707+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml fe1.inv in
695708
let c = s_while (test, cl) in
709+
let pre = map_ts_inv f_ands [inv; fe1 ; p0] in
696710
LossLess.xhyps evs m
697-
(ts_inv_lower_left3 (fun inv f_tr f_r1 -> f_bdHoareS (snd evs.es_ml) inv c f_tr FHeq f_r1) inv {ml;mr;inv=f_true} {ml;mr;inv=f_r1})
711+
(ts_inv_lower_left3
712+
(fun inv f_tr f_r1 -> f_bdHoareS (snd evs.es_ml) inv c f_tr FHeq f_r1)
713+
pre {ml;mr;inv=f_true} {ml;mr;inv=f_r1}
714+
)
698715

699716
and ll2 =
700-
let test = f_ands [fe1.inv; f_not p0.inv; f_not p1.inv] in
701-
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
717+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr fe2.inv in
702718
let c = s_while (test, cr) in
719+
let pre = map_ts_inv f_ands [inv; fe2; p1] in
703720
LossLess.xhyps evs m
704-
(ts_inv_lower_right3 (fun inv f_tr f_r1 -> f_bdHoareS (snd evs.es_mr) inv c f_tr FHeq f_r1) inv {ml;mr;inv=f_true} {ml;mr;inv=f_r1})
721+
(ts_inv_lower_right3
722+
(fun inv f_tr f_r1 -> f_bdHoareS (snd evs.es_mr) inv c f_tr FHeq f_r1)
723+
pre {ml;mr;inv=f_true} {ml;mr;inv=f_r1}
724+
)
705725

706726
in (ll1, ll2)
707727

@@ -719,10 +739,10 @@ let process_async_while (winfos : EP.async_while_info) tc =
719739
f_equivS (snd evs.es_ml) (snd evs.es_mr) (es_pr evs) sl sr (map_ts_inv2 f_and inv post) in
720740

721741
FApi.t_onfsub (function
722-
| 6 -> Some (EcLowGoal.t_intros_n c1)
723-
| 7 -> Some (EcLowGoal.t_intros_n c2)
742+
| 4 -> Some (EcLowGoal.t_intros_n c1)
743+
| 5 -> Some (EcLowGoal.t_intros_n c2)
724744
| _ -> None)
725745

726746
(FApi.xmutate1
727747
tc `AsyncWhile
728-
[cond1; cond2; cond3; hr1; hr2; xwh; ll1; ll2; concl])
748+
[cond; xwh; hr1; hr2; ll1; ll2; concl])

0 commit comments

Comments
 (0)