Skip to content

fix alpha-conversion problems in ehoare #872

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
bgregoir wants to merge 1 commit into
base: main
Choose a base branch
from
Open

fix alpha-conversion problems in ehoare #872

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 6 additions & 5 deletions src/phl/ecPhlApp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,12 +26,13 @@ let t_hoare_app_r i phi tc =
let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r

(* -------------------------------------------------------------------- *)
let t_ehoare_app_r i f tc =
let t_ehoare_app_r i phi tc =
let env = FApi.tc1_env tc in
let hs = tc1_as_ehoareS tc in
let s1, s2 = s_split env i hs.ehs_s in
let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) f in
let b = f_eHoareS (snd hs.ehs_m) f (stmt s2) (ehs_po hs) in
let phi = ss_inv_rebind phi (fst hs.ehs_m) in
let a = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) (stmt s1) phi in
let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in
FApi.xmutate1 tc `HlApp [a; b]

let t_ehoare_app = FApi.t_low2 "hoare-app" t_ehoare_app_r
Expand Down Expand Up @@ -124,11 +125,11 @@ let t_equiv_app_onesided side i pre post tc =
let (ml, mr) = fst es.es_ml, fst es.es_mr in
let s, s', p', q' =
match side with
| `Left ->
| `Left ->
let p' = ss_inv_generalize_as_left pre ml mr in
let q' = ss_inv_generalize_as_left post ml mr in
es.es_sl, es.es_sr, p', q'
| `Right ->
| `Right ->
let p' = ss_inv_generalize_as_right pre ml mr in
let q' = ss_inv_generalize_as_right post ml mr in
es.es_sr, es.es_sl, p', q'
Expand Down
38 changes: 22 additions & 16 deletions src/phl/ecPhlConseq.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,11 +39,11 @@ let bd_goal_r fcmp fbd cmp bd =
| FHle, (FHle | FHeq) -> Some (map_ss_inv2 f_real_le bd fbd)
| FHge, (FHge | FHeq) -> Some (map_ss_inv2 f_real_le fbd bd)
| FHeq, FHeq -> Some (map_ss_inv2 f_eq bd fbd)
| FHeq, FHge -> Some (map_ss_inv2 f_and
(map_ss_inv1 ((EcUtils.flip f_eq) f_r1) fbd)
| FHeq, FHge -> Some (map_ss_inv2 f_and
(map_ss_inv1 ((EcUtils.flip f_eq) f_r1) fbd)
(map_ss_inv1 ((EcUtils.flip f_eq) f_r1) bd))
| FHeq, FHle -> Some (map_ss_inv2 f_and
(map_ss_inv1 ((EcUtils.flip f_eq) f_r0) fbd)
| FHeq, FHle -> Some (map_ss_inv2 f_and
(map_ss_inv1 ((EcUtils.flip f_eq) f_r0) fbd)
(map_ss_inv1 ((EcUtils.flip f_eq) f_r0) bd))
| _ , _ -> None

Expand Down Expand Up @@ -453,6 +453,9 @@ let t_bdHoareS_conseq_nm = gen_conseq_nm t_bdHoareS_notmod t_bdHoareS_conseq
let t_ehoareF_concave (fc: ss_inv) pre post tc =
let env = FApi.tc1_env tc in
let hf = tc1_as_ehoareF tc in
let pre = ss_inv_rebind pre hf.ehf_m in
let post = ss_inv_rebind post hf.ehf_m in
let fc = ss_inv_rebind fc hf.ehf_m in
let f = hf.ehf_f in
let mpr,mpo = Fun.hoareF_memenv hf.ehf_m f env in
let fsig = (Fun.by_xpath f env).f_sig in
Expand Down Expand Up @@ -491,6 +494,9 @@ let t_ehoareS_concave (fc: ss_inv) (* xreal -> xreal *) pre post tc =
let hs = tc1_as_ehoareS tc in
let s = hs.ehs_s in
let m = fst hs.ehs_m in
let pre = ss_inv_rebind pre m in
let post = ss_inv_rebind post m in
let fc = ss_inv_rebind fc m in
(* ensure that f only depend of notmod *)
let modi = s_write env s in
let fv = PV.fv env m fc.inv in
Expand Down Expand Up @@ -614,7 +620,7 @@ let process_concave ((info, fc) : pformula option tuple2 gppterm * pformula) tc

let pre = map_ss_inv1 (fun gpre -> pre |> omap (TTC.pf_process_form !!tc penv txreal) |> odfl gpre) gpre in
let post = map_ss_inv1 (fun gpost -> post |> omap (TTC.pf_process_form !!tc qenv txreal) |> odfl gpost) gpost in

fmake pre post

in
Expand Down Expand Up @@ -665,9 +671,9 @@ let t_hoareS_conseq_conj pre post pre' post' tc =
let hs = tc1_as_hoareS tc in
let pre'' = map_ss_inv2 f_and pre' pre in
let post'' = map_ss_inv2 f_and post' post in
if not (ss_inv_alpha_eq hyps (hs_pr hs) pre'')
if not (ss_inv_alpha_eq hyps (hs_pr hs) pre'')
then tc_error !!tc "invalid pre-condition";
if not (ss_inv_alpha_eq hyps (hs_po hs) post'')
if not (ss_inv_alpha_eq hyps (hs_po hs) post'')
then tc_error !!tc "invalid post-condition";
let concl1 = f_hoareS (snd hs.hs_m) pre hs.hs_s post in
let concl2 = f_hoareS (snd hs.hs_m) pre' hs.hs_s post' in
Expand All @@ -679,7 +685,7 @@ let t_hoareF_conseq_conj pre post pre' post' tc =
let hf = tc1_as_hoareF tc in
let pre'' = map_ss_inv2 f_and pre' pre in
let post'' = map_ss_inv2 f_and post' post in
if not (ss_inv_alpha_eq hyps (hf_pr hf) pre'')
if not (ss_inv_alpha_eq hyps (hf_pr hf) pre'')
then tc_error !!tc "invalid pre-condition";
if not (ss_inv_alpha_eq hyps (hf_po hf) post'')
then tc_error !!tc "invalid post-condition";
Expand All @@ -696,7 +702,7 @@ let t_bdHoareS_conseq_conj ~add post post' tc =
if not (ss_inv_alpha_eq hyps (bhs_po hs) postc) then
tc_error !!tc "invalid post-condition";
let concl1 = f_hoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post in
let concl2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s posth
let concl2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s posth
hs.bhs_cmp (bhs_bd hs) in
FApi.xmutate1 tc `HlConseqBd [concl1; concl2]

Expand Down Expand Up @@ -765,7 +771,7 @@ let t_equivS_conseq_bd side pr po tc =
let pos = ss_inv_generalize_as_left po ml mr in
let prs = ss_inv_generalize_as_left pr ml mr in
es.es_ml, es.es_sl, es.es_sr, prs, pos
| `Right ->
| `Right ->
let pos = ss_inv_generalize_as_right po ml mr in
let prs = ss_inv_generalize_as_right pr ml mr in
es.es_mr, es.es_sr, es.es_sl, prs, pos
Expand Down Expand Up @@ -921,7 +927,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
let tac = if notmod then t_hoareS_conseq_nm else t_hoareS_conseq in

t_on1seq 2
(tac (map_ss_inv2 f_and (hs_pr hs) (hs_pr hs2))
(tac (map_ss_inv2 f_and (hs_pr hs) (hs_pr hs2))
(map_ss_inv2 f_and (hs_po hs) (hs_po hs2)))
(FApi.t_seqsub
(t_hoareS_conseq_conj (hs_pr hs2) (hs_po hs2) (hs_pr hs) (hs_po hs))
Expand Down Expand Up @@ -962,7 +968,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
let po2 = ss_inv_rebind (hf_po hs2) hf.hf_m in
(* check that the pre- and post-conditions are well formed *)
t_on1seq 2
((tac (map_ss_inv2 f_and pr1 pr2)
((tac (map_ss_inv2 f_and pr1 pr2)
(map_ss_inv2 f_and po1 po2)))
(FApi.t_seqsub
(t_hoareF_conseq_conj pr2 po2 pr1 po1)
Expand Down Expand Up @@ -1162,7 +1168,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
Some ((_, {f_node = FequivF ef}) as nef), Some((_, f2) as nf2), _ ->
let hf2 = pf_as_bdhoareF !!tc f2 in
FApi.t_seqsub
(t_bdHoareF_conseq_equiv hf2.bhf_f (ef_pr ef) (ef_po ef)
(t_bdHoareF_conseq_equiv hf2.bhf_f (ef_pr ef) (ef_po ef)
(bhf_pr hf2) (bhf_po hf2) (bhf_bd hf2))
[t_id; t_id; t_apply_r nef; t_apply_r nf2] tc

Expand Down Expand Up @@ -1467,7 +1473,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
let f, pr, po = match f1 with
| None -> hf.hf_f, hf_pr hf, hf_po hf
| Some f1 -> match (snd f1).f_node with
| FequivF ef when side = `Left ->
| FequivF ef when side = `Left ->
ef.ef_fr, {m; inv=f_true}, {m; inv=f_true}
| _ -> hf.hf_f, hf_pr hf, hf_po hf
in
Expand All @@ -1482,7 +1488,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
| Some f1 -> match (snd f1).f_node with
| FequivF ef when side = `Left ->
let f_xreal_1 = f_r2xr f_r1 in
ef.ef_fr, {m=ef.ef_mr; inv=f_xreal_1},
ef.ef_fr, {m=ef.ef_mr; inv=f_xreal_1},
{m=ef.ef_mr; inv=f_xreal_1}, ef.ef_mr
| _ -> hf.ehf_f, ehf_pr hf, ehf_po hf, hf.ehf_m
in
Expand All @@ -1502,7 +1508,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
let f, pr, po, m = match f1 with
| None -> bhf.bhf_f, bhf_pr bhf, bhf_po bhf, bhf.bhf_m
| Some f1 -> match (snd f1).f_node with
| FequivF ef when side = `Left -> ef.ef_fr,
| FequivF ef when side = `Left -> ef.ef_fr,
{m=ef.ef_mr;inv=f_true}, {m=ef.ef_mr;inv=f_true}, ef.ef_mr
| _ -> bhf.bhf_f, bhf_pr bhf, bhf_po bhf, bhf.bhf_m
in
Expand Down
3 changes: 2 additions & 1 deletion src/phl/ecPhlDeno.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,8 @@ let t_phoare_deno_r pre post tc =

(* -------------------------------------------------------------------- *)
let t_ehoare_deno_r pre post tc =
assert (pre.m = post.m);
let m = pre.m in
assert (m = post.m);
let env, _, concl = FApi.tc1_eflat tc in

let f, bd =
Expand All @@ -111,6 +111,7 @@ let t_ehoare_deno_r pre post tc =

(* forall m, ev%r%xr <= post *)
let ev = pr.pr_event in
let ev = ss_inv_rebind ev m in
let concl_po = map_ss_inv2 f_xreal_le (map_ss_inv1 f_b2xr ev) post in
let concl_po = f_forall_mems_ss_inv mpo concl_po in

Expand Down