Skip to content

Make casts from existing single sided formulas to two sided ones use a more robust pattern #851

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

Merged
strub merged 1 commit into from
Dec 19, 2025
Merged

Make casts from existing single sided formulas to two sided ones use a more robust pattern #851

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
12 changes: 6 additions & 6 deletions src/phl/ecPhlApp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,13 +124,13 @@ 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 ->
let p' = ss_inv_generalize_right (EcSubst.ss_inv_rebind pre ml) mr in
let q' = ss_inv_generalize_right (EcSubst.ss_inv_rebind post ml) mr in
| `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 ->
let p' = ss_inv_generalize_left (EcSubst.ss_inv_rebind pre mr) ml in
let q' = ss_inv_generalize_left (EcSubst.ss_inv_rebind post mr) ml in
| `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'
in
let generalize_mod_side= sideif side generalize_mod_left generalize_mod_right in
Expand Down
58 changes: 30 additions & 28 deletions src/phl/ecPhlConseq.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -719,10 +719,10 @@ let t_equivS_conseq_conj pre1 post1 pre2 post2 pre' post' tc =
let (_, hyps, _) = FApi.tc1_eflat tc in
let es = tc1_as_equivS tc in
let (ml, mtl), (mr, mtr) = es.es_ml, es.es_mr in
let pre1' = ss_inv_generalize_right (ss_inv_rebind pre1 ml) mr in
let post1' = ss_inv_generalize_right (ss_inv_rebind post1 ml) mr in
let pre2' = ss_inv_generalize_left (ss_inv_rebind pre2 mr) ml in
let post2' = ss_inv_generalize_left (ss_inv_rebind post2 mr) ml in
let pre1' = ss_inv_generalize_as_left pre1 ml mr in
let post1' = ss_inv_generalize_as_left post1 ml mr in
let pre2' = ss_inv_generalize_as_right pre2 ml mr in
let post2' = ss_inv_generalize_as_right post2 ml mr in
if not (ts_inv_alpha_eq hyps (es_pr es) (map_ts_inv f_ands [pre';pre1';pre2'])) then
tc_error !!tc "invalid pre-condition";
if not (ts_inv_alpha_eq hyps (es_po es) (map_ts_inv f_ands [post';post1';post2'])) then
Expand All @@ -737,15 +737,17 @@ let t_equivF_conseq_conj pre1 post1 pre2 post2 pre' post' tc =
let (_, hyps, _) = FApi.tc1_eflat tc in
let ef = tc1_as_equivF tc in
let ml, mr = ef.ef_ml, ef.ef_mr in
let pre1' = ss_inv_generalize_right (ss_inv_rebind pre1 ml) mr in
let post1' = ss_inv_generalize_right (ss_inv_rebind post1 ml) mr in
let pre2' = ss_inv_generalize_left (ss_inv_rebind pre2 mr) ml in
let post2' = ss_inv_generalize_left (ss_inv_rebind post2 mr) ml in
let pre'' = map_ts_inv f_ands [pre'; pre1'; pre2'] in
let post'' = map_ts_inv f_ands [post'; post1'; post2'] in
if not (ts_inv_alpha_eq hyps (ef_pr ef) pre'')
let pre1' = ss_inv_generalize_as_left pre1 ml mr in
let post1' = ss_inv_generalize_as_left post1 ml mr in
let pre2' = ss_inv_generalize_as_right pre2 ml mr in
let post2' = ss_inv_generalize_as_right post2 ml mr in
let pre'' = ts_inv_rebind pre' ml mr in
let pre_and = map_ts_inv f_ands [pre''; pre1'; pre2'] in
let post'' = ts_inv_rebind post' ml mr in
let post_and = map_ts_inv f_ands [post''; post1'; post2'] in
if not (ts_inv_alpha_eq hyps (ef_pr ef) pre_and)
then tc_error !!tc "invalid pre-condition";
if not (ts_inv_alpha_eq hyps (ef_po ef) post'')
if not (ts_inv_alpha_eq hyps (ef_po ef) post_and)
then tc_error !!tc "invalid post-condition";
let concl1 = f_hoareF pre1 ef.ef_fl post1 in
let concl2 = f_hoareF pre2 ef.ef_fr post2 in
Expand All @@ -760,12 +762,12 @@ let t_equivS_conseq_bd side pr po tc =
let m,s,s',prs,pos =
match side with
| `Left ->
let pos = ss_inv_generalize_right (ss_inv_rebind po ml) mr in
let prs = ss_inv_generalize_right (ss_inv_rebind pr ml) mr in
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 ->
let pos = ss_inv_generalize_left (ss_inv_rebind po mr) ml in
let prs = ss_inv_generalize_left (ss_inv_rebind pr mr) ml in
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
in
if not (List.is_empty s'.s_node) then begin
Expand Down Expand Up @@ -1180,10 +1182,10 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
let hs2 = pf_as_hoareS !!tc f2 in
let hs3 = pf_as_hoareS !!tc f3 in
let (ml, mr) = (fst es.es_ml, fst es.es_mr) in
let hs2_pr = ss_inv_generalize_right (ss_inv_rebind (hs_pr hs2) ml) mr in
let hs2_po = ss_inv_generalize_right (ss_inv_rebind (hs_po hs2) ml) mr in
let hs3_pr = ss_inv_generalize_left (ss_inv_rebind (hs_pr hs3) mr) ml in
let hs3_po = ss_inv_generalize_left (ss_inv_rebind (hs_po hs3) mr) ml in
let hs2_pr = ss_inv_generalize_as_left (hs_pr hs2) ml mr in
let hs2_po = ss_inv_generalize_as_left (hs_po hs2) ml mr in
let hs3_pr = ss_inv_generalize_as_right (hs_pr hs3) ml mr in
let hs3_po = ss_inv_generalize_as_right (hs_po hs3) ml mr in
let pre = map_ts_inv f_ands [es_pr es; hs2_pr; hs3_pr] in
let post = map_ts_inv f_ands [es_po es; hs2_po; hs3_po] in
let tac = if notmod then t_equivS_conseq_nm else t_equivS_conseq in
Expand Down Expand Up @@ -1238,8 +1240,8 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
| FequivS es, None, Some ((_, f2) as nf2), None ->
let hs = pf_as_bdhoareS !!tc f2 in
let (ml, mr) = (fst es.es_ml, fst es.es_mr) in
let pre = ss_inv_generalize_right (ss_inv_rebind (bhs_pr hs) ml) mr in
let post = ss_inv_generalize_right (ss_inv_rebind (bhs_po hs) ml) mr in
let pre = ss_inv_generalize_as_left (bhs_pr hs) ml mr in
let post = ss_inv_generalize_as_left (bhs_po hs) ml mr in
let tac = if notmod then t_equivS_conseq_nm else t_equivS_conseq in

check_is_detbound `Second (bhs_bd hs).inv;
Expand All @@ -1256,8 +1258,8 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
| FequivS es, None, None, Some ((_, f3) as nf3) ->
let hs = pf_as_bdhoareS !!tc f3 in
let (ml, mr) = (fst es.es_ml, fst es.es_mr) in
let pre = ss_inv_generalize_left (ss_inv_rebind (bhs_pr hs) mr) ml in
let post = ss_inv_generalize_left (ss_inv_rebind (bhs_po hs) mr) ml in
let pre = ss_inv_generalize_as_right (bhs_pr hs) ml mr in
let post = ss_inv_generalize_as_right (bhs_po hs) ml mr in
let tac = if notmod then t_equivS_conseq_nm else t_equivS_conseq in

check_is_detbound `Third (bhs_bd hs).inv;
Expand Down Expand Up @@ -1285,11 +1287,11 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
let hs2 = pf_as_hoareF !!tc f2 in
let hs3 = pf_as_hoareF !!tc f3 in
let (ml, mr) = (ef.ef_ml, ef.ef_mr) in
let hs2_pr = ss_inv_generalize_right (ss_inv_rebind (hf_pr hs2) ml) mr in
let hs3_pr = ss_inv_generalize_left (ss_inv_rebind (hf_pr hs3) mr) ml in
let hs2_pr = ss_inv_generalize_as_left (hf_pr hs2) ml mr in
let hs3_pr = ss_inv_generalize_as_right (hf_pr hs3) ml mr in
let pre = map_ts_inv f_ands [ef_pr ef; hs2_pr; hs3_pr] in
let hs2_po = ss_inv_generalize_right (ss_inv_rebind (hf_po hs2) ml) mr in
let hs3_po = ss_inv_generalize_left (ss_inv_rebind (hf_po hs3) mr) ml in
let hs2_po = ss_inv_generalize_as_left (hf_po hs2) ml mr in
let hs3_po = ss_inv_generalize_as_right (hf_po hs3) ml mr in
let post = map_ts_inv f_ands [ef_po ef; hs2_po; hs3_po] in
let tac = if notmod then t_equivF_conseq_nm else t_equivF_conseq in
t_on1seq 2
Expand Down
13 changes: 13 additions & 0 deletions tests/conseq_equiv_phoare_at_equiv.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
module Foo = {
proc foo(i : int) = {
}
}.

lemma foo_corr : hoare [ Foo.foo : true ==> true] by proc;auto.

lemma foo_eq : equiv [ Foo.foo ~ Foo.foo : ={arg} ==> true ] by sim.

lemma foo_eq_corr:
equiv [ Foo.foo ~ Foo.foo : ={arg} ==> ={res} ].
conseq foo_eq foo_corr.
qed.