Skip to content

Commit 267f827

Browse files
lyonel2017strub
lyonel2017
authored and
strub
committed
Fix async while obligations and document the tactic
1 parent 15e14e5 commit 267f827

5 files changed

Lines changed: 247 additions & 55 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/phl/ecPhlWhile.ml‎

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

631631
let inv = TTC.tc1_process_prhl_formula tc inv in
632+
632633
let p0 = TTC.tc1_process_prhl_formula tc p0 in
633634
let p1 = TTC.tc1_process_prhl_formula tc p1 in
635+
634636
let f1 = TTC.tc1_process_prhl_form_opt tc None f1 in
635637
let f2 = TTC.tc1_process_prhl_form_opt tc None f2 in
638+
636639
let t1 = TTC.tc1_process_Xhl_exp tc (Some `Left ) (Some (tfun f1.inv.f_ty tbool)) t1 in
637640
let t2 = TTC.tc1_process_Xhl_exp tc (Some `Right) (Some (tfun f2.inv.f_ty tbool)) t2 in
641+
638642
let ft1 = ss_inv_generalize_right (ss_inv_of_expr ml t1) mr in
639643
let ft2 = ss_inv_generalize_left (ss_inv_of_expr mr t2) ml in
644+
640645
let fe1 = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in
641646
let fe2 = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in
642-
let fe = map_ts_inv2 f_or fe1 fe2 in
647+
643648
let f_app' f = f_app (List.hd f) (List.tl f) tbool in
644649
let f_imps' f = f_imps (List.tl f) (List.hd f) in
645-
let cond1 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
646-
(map_ts_inv f_imps' [map_ts_inv f_ands [fe1; fe2;
647-
map_ts_inv f_app' [ft1; f1];
648-
map_ts_inv f_app' [ft2; f2]];
649-
inv; fe; p0]) in
650-
651-
let cond2 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
652-
(map_ts_inv f_imps' [fe1; inv; fe; map_ts_inv1 f_not p0; p1]) in
653650

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

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

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

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

687702
in (hr1, hr2)
688703
in
689704

690-
691705
let (c1, ll1), (c2, ll2) =
692706
try
693707
let ll1 =
694-
let test = f_ands [fe1.inv; f_not p0.inv; p1.inv] in
695-
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
708+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml fe1.inv in
696709
let c = s_while (test, cl) in
710+
let pre = map_ts_inv f_ands [inv; fe1 ; p0] in
697711
LossLess.xhyps evs m
698-
(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})
712+
(ts_inv_lower_left3
713+
(fun inv f_tr f_r1 -> f_bdHoareS (snd evs.es_ml) inv c f_tr FHeq f_r1)
714+
pre {ml;mr;inv=f_true} {ml;mr;inv=f_r1}
715+
)
699716

700717
and ll2 =
701-
let test = f_ands [fe1.inv; f_not p0.inv; f_not p1.inv] in
702-
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
718+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr fe2.inv in
703719
let c = s_while (test, cr) in
720+
let pre = map_ts_inv f_ands [inv; fe2; p1] in
704721
LossLess.xhyps evs m
705-
(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})
722+
(ts_inv_lower_right3
723+
(fun inv f_tr f_r1 -> f_bdHoareS (snd evs.es_mr) inv c f_tr FHeq f_r1)
724+
pre {ml;mr;inv=f_true} {ml;mr;inv=f_r1}
725+
)
706726

707727
in (ll1, ll2)
708728

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

722742
FApi.t_onfsub (function
723-
| 6 -> Some (EcLowGoal.t_intros_n c1)
724-
| 7 -> Some (EcLowGoal.t_intros_n c2)
743+
| 4 -> Some (EcLowGoal.t_intros_n c1)
744+
| 5 -> Some (EcLowGoal.t_intros_n c2)
725745
| _ -> None)
726746

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

0 commit comments

Comments
 (0)