From 07e7aa9004750447c3d491409022b0275d79999c Mon Sep 17 00:00:00 2001 From: Lionel Blatter Date: Wed, 11 Mar 2026 16:19:41 +0100 Subject: [PATCH] Fix asynchile rule --- examples/async-while.ec | 18 ++++---- src/ecPrinting.ml | 4 +- src/phl/ecPhlWhile.ml | 72 ++++++++++++++++++++----------- theories/looping/LoopTransform.ec | 32 ++++++-------- 4 files changed, 69 insertions(+), 57 deletions(-) diff --git a/examples/async-while.ec b/examples/async-while.ec index 2bf8b38eed..de3d4fb165 100644 --- a/examples/async-while.ec +++ b/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. - diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index c3f29cdfac..9d095935e5 100644 --- a/src/ecPrinting.ml +++ b/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[@[@ %a %a:@ @[%a ==>@ %a@ %a]@]]" + Format.fprintf fmt "hoare[@[@ %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[@[@ %a %a:@ @[%a ==>@ %a@ %a]@]]" + Format.fprintf fmt "hoare[@[@ %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 diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index 5fd61874c8..fad82c3854 100644 --- a/src/phl/ecPhlWhile.ml +++ b/src/phl/ecPhlWhile.ml @@ -628,30 +628,42 @@ 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 @@ -659,8 +671,13 @@ let process_async_while (winfos : EP.async_while_info) tc = 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,15 +687,13 @@ 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) @@ -686,22 +701,27 @@ let process_async_while (winfos : EP.async_while_info) tc = 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]) diff --git a/theories/looping/LoopTransform.ec b/theories/looping/LoopTransform.ec index 57dc9a4535..1299e184d7 100644 --- a/theories/looping/LoopTransform.ec +++ b/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.