Fix asynchile rule

Author: lyonel2017

examples/async-while.ec

@@ -50,26 +50,24 @@ seq 1 1 : (i{1} = 0 /\ ={glob A, x, i}) => //.
 async while
   [ (fun r => i%r < k%r * r), (i{2} + 1)%r ]
   [ (fun r => i%r < r), (i{2} + 1)%r ]
-    (i{1} < n * k /\ i{2} < n) (!(i{2} < n))
+    (!(i{1} < n * k)) (!(i{2} < n))
   :
     (={glob A, x} /\ i{1} = k * i{2} /\ (0 <= i{1})) => //=.
-+ by move=> &1 &2 />; smt(gt0_k).
-+ by move=> &1 &2 />; smt(gt0_k).
-+ by move=> &2; exfalso=> &1; smt(gt0_k).
-+ by move=> &2; exfalso=> &1 ?; smt(gt0_k).
++ move=> &1 &2 />; smt(gt0_k).
 + move=> v1 v2.
   rcondt {2} 1; 1: by auto => /> /#.
   rcondf{2} 4; 1: by auto; conseq (_: true);auto.
-  wp;while (   ={glob A, x} 
+  wp;while (   ={glob A, x}
          /\ i{1} = k * i{2} + j{2}
          /\ v1 = (i{2} + 1)%r
          /\ 0 <= i{2} <  n
          /\ 0 <= j{2} <= k) => /=; last by auto; smt(gt0_k ge0_n).
   wp; call (_ : true); skip => &1 &2 /= />.
-  rewrite -fromintM !lt_fromint => *. 
-  by have := StdOrder.IntOrder.ler_wpmul2l k _ i{2} (n - 1); smt().
-+ by while true (n * k - i) => //; auto;1: call llA; auto => /#.
+  rewrite -fromintM !lt_fromint => *.
+      by have := StdOrder.IntOrder.ler_wpmul2l k _ i{2} (n - 1); smt().
++ by move=> &2; exfalso=> &1 ? ; smt(gt0_k).
++ by move=> &1; exfalso=> &2 ?; smt(gt0_k).
++  while true (n * k - i) => //; auto;1: call llA; auto => /#.
 + while true (n - i);2: by auto=>/#.
   move=> z;wp; while (true) (k - j);auto;1:call llA;auto => /#.
 qed.
-

src/ecPrinting.ml

@@ -1974,7 +1974,7 @@ and pp_form_core_r
       let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
       let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
       let { main = post; exnmap = (poe, d) } = (hf_po hf).hsi_inv in
-      Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
+      Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a@]@]]"
         (pp_funname ppe) hf.hf_f
         (pp_pl_mem_binding pm ppe) hf.hf_m
         (pp_form ppepr) (hf_pr hf).inv
@@ -1985,7 +1985,7 @@ and pp_form_core_r
       let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in
       let { main = post; exnmap = (poe, d); } = (hs_po hs).hsi_inv in
       let pm = debug_mode || (fst hs.hs_m).id_symb <> "&hr" in
-      Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
+      Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a@]@]]"
         (pp_stmt_for_form ppe) hs.hs_s
         (pp_pl_mem_binding pm ppe) (fst hs.hs_m)
         (pp_form ppe) (hs_pr hs).inv

src/phl/ecPhlWhile.ml

@@ -628,39 +628,56 @@ let process_async_while (winfos : EP.async_while_info) tc =
   let (er, cr), sr = tc1_last_while tc evs.es_sr in
 
   let inv = TTC.tc1_process_prhl_formula tc inv in
+
   let p0  = TTC.tc1_process_prhl_formula tc  p0 in
   let p1  = TTC.tc1_process_prhl_formula tc  p1 in
+
   let f1  = TTC.tc1_process_prhl_form_opt tc None f1 in
   let f2  = TTC.tc1_process_prhl_form_opt tc None f2 in
+
   let t1  = TTC.tc1_process_Xhl_exp tc (Some `Left ) (Some (tfun f1.inv.f_ty tbool)) t1 in
   let t2  = TTC.tc1_process_Xhl_exp tc (Some `Right) (Some (tfun f2.inv.f_ty tbool)) t2 in
+
   let ft1 = ss_inv_generalize_right (ss_inv_of_expr ml t1) mr in
   let ft2 = ss_inv_generalize_left (ss_inv_of_expr mr t2) ml in
+
   let fe1 = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in
   let fe2 = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in
-  let fe  = map_ts_inv2 f_or fe1 fe2 in
+
   let f_app' f = f_app (List.hd f) (List.tl f) tbool in
   let f_imps' f = f_imps (List.tl f) (List.hd f) in
-  let cond1 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
-    (map_ts_inv f_imps' [map_ts_inv f_ands [fe1; fe2;
-    map_ts_inv f_app' [ft1; f1];
-    map_ts_inv f_app' [ft2; f2]];
-    inv; fe; p0]) in
-
-  let cond2 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
-    (map_ts_inv f_imps' [fe1; inv; fe; map_ts_inv1 f_not p0; p1]) in
 
-  let cond3 = EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
-    (map_ts_inv f_imps' [fe2; inv; fe; map_ts_inv1 f_not p0; map_ts_inv1 f_not p1]) in
+  let fe = map_ts_inv2 f_eq fe1 fe2 in
+  let neg_p0 f = map_ts_inv f_imps' [f; map_ts_inv1 f_not p0] in
+  let neg_p1 f = map_ts_inv f_imps' [f; map_ts_inv1 f_not p1] in
+  let fprog =
+    let ft1 = map_ts_inv f_app' [ft1; f1] in
+    let ft2 = map_ts_inv f_app' [ft2; f2] in
+    neg_p0 (neg_p1 (map_ts_inv f_ands [ft1;ft2]))
+  in
+  let flock = map_ts_inv f_ands [fe;fprog] in
+  let fc1 = map_ts_inv f_ands [fe1; p0] in
+  let fc2 = map_ts_inv f_ands [fe2; p1] in
+
+  let cond =
+    EcSubst.f_forall_mems_ts_inv evs.es_ml evs.es_mr
+      (map_ts_inv f_imps'
+         [map_ts_inv f_ors [flock; fc1; fc2]; inv])
+  in
 
   let xwh =
     let v1, v2 = as_seq2 (EcEnv.LDecl.fresh_ids hyps ["v1_"; "v2_"]) in
     let fv1 = {ml;mr;inv=f_local v1 f1.inv.f_ty} in
     let fv2 = {ml;mr;inv=f_local v2 f2.inv.f_ty} in
     let ev1 = e_local v1 f1.inv.f_ty in
     let ev2 = e_local v2 f2.inv.f_ty in
+    let p0 = map_ts_inv f_ands [map_ts_inv1 f_not p0;map_ts_inv1 f_not p1] in
+    let fe = map_ts_inv f_ands [fe1;fe2] in
+    let ft1 = map_ts_inv f_app' [ft1; fv1] in
+    let ft2 = map_ts_inv f_app' [ft2; fv2] in
+    let fprog = map_ts_inv f_ands [ft1;ft2] in
     let eq1 = map_ts_inv2 f_eq fv1 f1 and eq2 = map_ts_inv2 f_eq fv2 f2 in
-    let pr = map_ts_inv f_ands [inv; fe; p0; eq1; eq2] in
+    let pr = map_ts_inv f_ands [inv; fe; fprog; p0; eq1; eq2] in
     let po = inv in
     let wl = s_while (e_and el (e_app t1 [ev1] tbool), cl) in
     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 =
 
   let hr1, hr2 =
     let hr1 =
-      let el = ss_inv_generalize_right (ss_inv_of_expr ml el) mr in
-      let pre = map_ts_inv f_ands [inv; el ; map_ts_inv1 f_not p0; p1] in
+      let pre = map_ts_inv f_ands [inv; fe1 ; p0] in
       EcSubst.f_forall_mems_ss_inv evs.es_mr
         (ts_inv_lower_left2
           (fun pr po -> f_hoareS (snd evs.es_ml) pr cl (POE.lift po)) pre inv)
 
     and hr2 =
-      let er = ss_inv_generalize_left (ss_inv_of_expr mr er) ml in
-      let pre = map_ts_inv f_ands [inv; er; map_ts_inv1 f_not p0; map_ts_inv1 f_not p1] in
+      let pre = map_ts_inv f_ands [inv; fe2; p1] in
       EcSubst.f_forall_mems_ss_inv evs.es_ml
         (ts_inv_lower_right2
           (fun pr po -> f_hoareS (snd evs.es_mr) pr cr (POE.lift po)) pre inv)
 
     in (hr1, hr2)
   in
 
-
   let (c1, ll1), (c2, ll2) =
     try
       let ll1 =
-        let test    = f_ands [fe1.inv; f_not p0.inv; p1.inv] in
-        let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
+        let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml fe1.inv in
         let c       = s_while (test, cl) in
+        let pre = map_ts_inv f_ands [inv; fe1 ; p0] in
         LossLess.xhyps evs m
-          (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})
+          (ts_inv_lower_left3
+             (fun inv f_tr f_r1 -> f_bdHoareS (snd evs.es_ml) inv c f_tr FHeq f_r1)
+             pre {ml;mr;inv=f_true} {ml;mr;inv=f_r1}
+          )
 
       and ll2 =
-        let test    = f_ands [fe1.inv; f_not p0.inv; f_not p1.inv] in
-        let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
+        let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr fe2.inv in
         let c       = s_while (test, cr) in
+        let pre = map_ts_inv f_ands [inv; fe2; p1] in
         LossLess.xhyps evs m
-          (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})
+          (ts_inv_lower_right3
+             (fun inv f_tr f_r1 -> f_bdHoareS (snd evs.es_mr) inv c f_tr FHeq f_r1)
+             pre {ml;mr;inv=f_true} {ml;mr;inv=f_r1}
+          )
 
       in (ll1, ll2)
 
@@ -719,10 +739,10 @@ let process_async_while (winfos : EP.async_while_info) tc =
     f_equivS (snd evs.es_ml) (snd evs.es_mr) (es_pr evs) sl sr (map_ts_inv2 f_and inv post) in
 
   FApi.t_onfsub (function
-    | 6 -> Some (EcLowGoal.t_intros_n c1)
-    | 7 -> Some (EcLowGoal.t_intros_n c2)
+    | 4 -> Some (EcLowGoal.t_intros_n c1)
+    | 5 -> Some (EcLowGoal.t_intros_n c2)
     | _ -> None)
 
     (FApi.xmutate1
        tc `AsyncWhile
-         [cond1; cond2; cond3; hr1; hr2; xwh; ll1; ll2; concl])
+         [cond; xwh; hr1; hr2; ll1; ll2; concl])

theories/looping/LoopTransform.ec

@@ -136,12 +136,9 @@ proof.
     by rcondf{2} ^while; auto => /> /#.
   async while [ (fun r => i%r < r), (i{1}+k{2})%r ] 
               [ (fun r => i%r < r), (i{2} + 1)%r ]
-              ( (i < n){1}) 
-              (true) : 
+              ( !(i < n){1}) (!(i < n){2}) : 
               (={t, glob B} /\ (0 <= i <= n){2} /\ 0 < k{2} /\ n{1} = (k * n){2} /\ i{1} = k{2} * i{2}).
-  + smt(). + smt (). + done. 
-  + move=> &m2; exfalso; smt().
-  + move=> &m1; exfalso; smt().
+  + smt().
   + move=> v1 v2.
     rcondt{2} 1; 1: by auto => /> /#.
     rcondf{2} 4; 1: by auto; conseq (_: true);auto.
@@ -151,9 +148,11 @@ proof.
     + wp;call (_: true);skip => /> &2 h0i hin h0j hjk.
       rewrite !lt_fromint => h1 h2 h3.
       have := IntOrder.ler_wpmul2l k{2} _ i{2} (n{2} - 1); smt().
-    by wp;skip => /> /#.
-  + rcondf 1; skip => /#. 
-  + rcondf 1; skip => /#. 
+                by wp;skip => /> /#.
+  + move=> &m2; exfalso => /#.
+  + move=> &m1; exfalso => /#.
+  + rcondf 1 ; skip => /#.
+  + rcondf 1; skip => /#.
   auto => /> /#.
 qed.
 
@@ -188,17 +187,10 @@ proof.
   seq 2 2: (={glob B, t, n, i}); last by sim;wp;skip.
   async while [ (fun r => i%r < r), (i{1} + step * k{2})%r ] 
               [ (fun r => i%r < r), (i{2} + step * k{2})%r ]
-              ( (i < floor n (step * k0)){1}) 
-              (true) : 
+              (!(i < floor n (step * k0)){1}) 
+              (!(i + step * k <= n){2}) : 
               (={t, glob B, i, n} /\ k{2} = k0 /\ 0 < k{2} /\ (step * k0) %| i{1}).
   + move=> />;smt (lt_floorE floor_le step_gt0). 
-  + move=> /> &2 h1 h2 [[]// | h3].
-    have h4 := le_floorE (step * k0) (i{2} + step * k0) n{2} _ _.
-    + smt (step_gt0). + by apply dvdzD => //; apply dvdzz.
-    smt (step_gt0).
-  + done.
-  + by move=> &m2; exfalso => /#.
-  + by move=> &m1; exfalso => /#.
   + move=> v1 v2.
     rcondt{2} 1. 
     + move=> &1;skip => /> *; smt (step_gt0 lt_floorE floor_le).
@@ -216,10 +208,12 @@ proof.
       split. smt(). 
       have <- := IntOrder.ltr_pmul2l step step_gt0 (j{2} + 1) k0.
       smt (floor_le step_gt0).
-    wp; skip => &1 &2 [#] 6!->> h1 h2 h3 h4 2!->> /=.
+    wp; skip => &1 &2 [#] 6!->> h1 h2 h3 h4 ?????  2!->> /=.
     rewrite le_fromint lt_fromint h2 h1 -lt_floorE /= 2://; 1:smt (step_gt0).
     split; 1: smt(step_gt0).
-    by move=> /> j_R *; rewrite dvdzD 1:/# (_ : j_R = k0) 1:/# dvdzz.
+              by move=> /> j_R *; rewrite dvdzD 1:/# (_ : j_R = k0) 1:/# dvdzz.
+  + by move=> &m2; exfalso => /#.
+  + by move=> &m1; exfalso => /#.
   + rcondf 1; skip => /#.
   + rcondf 1; skip => /#.
   by auto.