From 286de65e4fcfaa9c9e0adafef78fc57270cfccb1 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Wed, 25 Feb 2026 16:45:39 +0000 Subject: [PATCH] PR: Add framing to proc change --- src/ecCoreFol.ml | 202 ++++++++++++++++++++++++++++++++++++++++ src/ecCoreFol.mli | 1 + src/phl/ecPhlConseq.mli | 3 + src/phl/ecPhlRewrite.ml | 41 +++++++- tests/procchange.ec | 49 +++++++++- 5 files changed, 294 insertions(+), 2 deletions(-) diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml index 03dd1f64ec..45b6140594 100644 --- a/src/ecCoreFol.ml +++ b/src/ecCoreFol.ml @@ -525,6 +525,208 @@ let f_map gt g fp = let ev' = g pr.pr_event.inv in f_pr_r { pr with pr_args = args'; pr_event = {m=pr.pr_event.m; inv=ev'}; } +let f_filter_map (gt: ty -> ty option) (g: form -> form option) (fp: form) : form option = + let filter_map_ss_inv1 (g: form -> form option) ({inv; m}: ss_inv) : ss_inv option = + match g inv with + | Some inv when inv.f_ty = tbool -> Some {inv; m} + | None -> None + | _ -> assert false + in + + let filter_map_ts_inv1 (g: form -> form option) ({inv; ml; mr}: ts_inv) : ts_inv option = + match g inv with + | Some inv when inv.f_ty = tbool -> Some {inv; ml; mr} + | None -> None + | _ -> assert false + in + + match fp.f_node with + | Fquant(q, b, f) -> + let map_gty ((x, gty) as b1) = + let gty' = + match gty with + | GTty ty -> begin match gt ty with + | Some ty' -> if ty == ty' then Some gty else Some (GTty ty') + | None -> None + end + | _ -> Some gty + in + Option.map (fun gty' -> if gty == gty' then b1 else (x, gty')) gty' + in + + begin try + let b' = List.Smart.map (map_gty |- Option.get) b in + let f' = Option.get (g f) in + + Some (f_quant q b' f') + with Invalid_argument _ -> None + end + + | Fint _ -> Some fp + | Fglob _ -> Some fp + + | Fif (f1, f2, f3) -> + begin try + let f1 = Option.get (g f1) in + let f2 = Option.get (g f2) in + let f3 = Option.get (g f3) in + Some (f_if f1 f2 f3) + with Invalid_argument _ -> + None + end + + | Fmatch (b, fs, ty) -> + begin try + let b = Option.get (g b) in + let fs = List.map (g |- Option.get) fs in + let ty = Option.get (gt ty) in + Some (f_match b fs ty) + with Invalid_argument _ -> + None + end + + | Flet (lp, f1, f2) -> + begin try + let f1 = Option.get (g f1) in + let f2 = Option.get (g f2) in + Some (f_let lp f1 f2) + with Invalid_argument _ -> + None + end + + | Flocal id -> + Option.map (fun ty -> f_local id ty) (gt fp.f_ty) + + | Fpvar (id, s) -> + Option.map (fun ty -> (f_pvar id ty s).inv) (gt fp.f_ty) + + | Fop (p, tys) -> + begin try + let tys' = List.Smart.map (gt |- Option.get) tys in + let ty' = Option.get @@ gt fp.f_ty in + Some (f_op p tys' ty') + with Invalid_argument _ -> + None + end + + | Fapp (f, fs) -> + begin try + let f' = Option.get @@ g f in + let fs' = List.Smart.map (g |- Option.get) fs in + let ty' = Option.get @@ gt fp.f_ty in + Some (f_app f' fs' ty') + with Invalid_argument _ -> + None + end + + | Ftuple fs -> + let fs' = try + Some (List.Smart.map (g |- Option.get) fs) + with Invalid_argument _ -> + None + in Option.map (fun fs -> f_tuple fs) fs' + + | Fproj (f, i) -> + begin try + let f' = Option.get @@ g f in + let ty' = Option.get @@ gt fp.f_ty in + Some (f_proj f' i ty') + with Invalid_argument _ -> + None + end + + | FhoareF hf -> + let pr' = filter_map_ss_inv1 g (hf_pr hf) in + let po' = filter_map_ss_inv1 g (hf_po hf) in + begin try + Some (f_hoareF (Option.get pr') hf.hf_f (Option.get po')) + with Invalid_argument _ -> + None + end + + | FhoareS hs -> + begin try + let pr' = Option.get (filter_map_ss_inv1 g (hs_pr hs)) in + let po' = Option.get (filter_map_ss_inv1 g (hs_po hs)) in + Some (f_hoareS (snd hs.hs_m) pr' hs.hs_s po') + with Invalid_argument _ -> + None + end + + | FeHoareF hf -> + begin try + let pr' = Option.get (filter_map_ss_inv1 g (ehf_pr hf)) in + let po' = Option.get (filter_map_ss_inv1 g (ehf_po hf)) in + Some (f_eHoareF pr' hf.ehf_f po') + with Invalid_argument _ -> + None + end + + | FeHoareS hs -> + begin try + let pr' = Option.get @@ filter_map_ss_inv1 g (ehs_pr hs) in + let po' = Option.get @@ filter_map_ss_inv1 g (ehs_po hs) in + Some (f_eHoareS (snd hs.ehs_m) pr' hs.ehs_s po') + with Invalid_argument _ -> + None + end + + | FbdHoareF bhf -> + begin try + let pr' = Option.get @@ filter_map_ss_inv1 g (bhf_pr bhf) in + let po' = Option.get @@ filter_map_ss_inv1 g (bhf_po bhf) in + let bd' = Option.get @@ filter_map_ss_inv1 g (bhf_bd bhf) in + Some (f_bdHoareF pr' bhf.bhf_f po' bhf.bhf_cmp bd') + with Invalid_argument _ -> + None + end + + | FbdHoareS bhs -> + begin try + let pr' = Option.get @@ filter_map_ss_inv1 g (bhs_pr bhs) in + let po' = Option.get @@ filter_map_ss_inv1 g (bhs_po bhs) in + let bd' = Option.get @@ filter_map_ss_inv1 g (bhs_bd bhs) in + Some (f_bdHoareS (snd bhs.bhs_m) pr' bhs.bhs_s po' bhs.bhs_cmp bd') + with Invalid_argument _ -> + None + end + + | FequivF ef -> + begin try + let pr' = Option.get @@ filter_map_ts_inv1 g (ef_pr ef) in + let po' = Option.get @@ filter_map_ts_inv1 g (ef_po ef) in + Some (f_equivF pr' ef.ef_fl ef.ef_fr po') + with Invalid_argument _ -> + None + end + + | FequivS es -> + begin try + let pr' = Option.get @@ filter_map_ts_inv1 g (es_pr es) in + let po' = Option.get @@ filter_map_ts_inv1 g (es_po es) in + Some (f_equivS (snd es.es_ml) (snd es.es_mr) pr' es.es_sl es.es_sr po') + with Invalid_argument _ -> + None + end + + | FeagerF eg -> + begin try + let pr' = Option.get @@ filter_map_ts_inv1 g (eg_pr eg) in + let po' = Option.get @@ filter_map_ts_inv1 g (eg_po eg) in + Some (f_eagerF pr' eg.eg_sl eg.eg_fl eg.eg_fr eg.eg_sr po') + with Invalid_argument _ -> + None + end + + | Fpr pr -> + begin try + let args' = Option.get @@ g pr.pr_args in + let ev' = Option.get @@ g pr.pr_event.inv in + Some (f_pr_r { pr with pr_args = args'; pr_event = {m=pr.pr_event.m; inv=ev'}; }) + with Invalid_argument _ -> + None + end + (* -------------------------------------------------------------------- *) let f_iter g f = match f.f_node with diff --git a/src/ecCoreFol.mli b/src/ecCoreFol.mli index 0977a33a50..49bff22e14 100644 --- a/src/ecCoreFol.mli +++ b/src/ecCoreFol.mli @@ -75,6 +75,7 @@ val f_node : form -> f_node (* -------------------------------------------------------------------- *) (* not recursive *) val f_map : (EcTypes.ty -> EcTypes.ty) -> (form -> form) -> form -> form +val f_filter_map : (EcTypes.ty -> EcTypes.ty option) -> (form -> form option) -> form -> form option val f_iter : (form -> unit) -> form -> unit val form_exists: (form -> bool) -> form -> bool val form_forall: (form -> bool) -> form -> bool diff --git a/src/phl/ecPhlConseq.mli b/src/phl/ecPhlConseq.mli index 4641358139..00886639d6 100644 --- a/src/phl/ecPhlConseq.mli +++ b/src/phl/ecPhlConseq.mli @@ -53,3 +53,6 @@ val process_conseq_opt : val t_conseqauto : ?delta:bool -> ?tsolve:FApi.backward -> FApi.backward val process_concave : pformula option tuple2 gppterm * pformula -> FApi.backward + +val cond_hoareS_notmod : ?mk_other:bool -> tcenv1 -> ss_inv -> form * memory list * (memory * ss_inv) list + diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml index 57abab3d51..142776738f 100644 --- a/src/phl/ecPhlRewrite.ml +++ b/src/phl/ecPhlRewrite.ml @@ -169,6 +169,31 @@ let process_rewrite | `Rw rw -> process_rewrite_rw side pos rw tc | `Simpl -> process_rewrite_simpl side pos tc +(* Frames pre *) +let hoareS_frame_pre (env: env) (pre: ss_inv) (s: stmt) : ss_inv = + let modi = EcPV.s_write env s in + let cond, _, _ = EcLowPhlGoal.generalize_mod_ env modi pre in + cond + +(* FIXME: rename *) +let restr_pre_mem (m: memory) (f: form) : form = + let fs = EcFol.destr_ands ~deep:true f in + List.filter_map (fun f -> + f_filter_map (fun t -> Some t) (fun f -> + match f.f_node with + | Fpvar (_, m') when m' <> m -> None + | _ -> Some f + ) f) fs |> List.fold_left f_and f_true + + +(* FIXME: unsound *) +let equivS_frame_pre_ss (env: env) (pre: ts_inv) (side: side) (s: stmt) : ss_inv = + let pre = match side with + | `Left -> {inv=restr_pre_mem pre.ml pre.inv;m = pre.ml} + | `Right -> {inv=restr_pre_mem pre.mr pre.inv;m = pre.mr} + in + hoareS_frame_pre env pre s + (* -------------------------------------------------------------------- *) let t_change_stmt (side : side option) @@ -211,10 +236,24 @@ let t_change_stmt pre_globs in + (* FIXME: make this generate the intermediate goal like the conseq one *) + (* FIXME: make the equiv case work *) + let pre = match zpr.z_path, FApi.tc1_goal tc, side with + | ZTop, {f_node = FhoareS hs}, None -> + (EcSubst.ss_inv_rebind + (hoareS_frame_pre env (hs_pr hs) (rstmt zpr.z_head)) + mleft).inv + | ZTop, {f_node = FequivS es}, Some s -> + (EcSubst.ss_inv_rebind + (equivS_frame_pre_ss env (es_pr es) s (rstmt zpr.z_head)) mleft).inv + | _ -> f_true + in + let pre = f_and pre (f_ands pre_eq) in + let goal1 = f_equivS (snd me) (snd me) - {ml=mleft; mr=mright; inv=f_ands pre_eq} + {ml=mleft; mr=mright; inv=pre} (EcAst.stmt stmt) s {ml=mleft; mr=mright; inv=f_ands eq} in diff --git a/tests/procchange.ec b/tests/procchange.ec index 6863802f09..76b88af2f5 100644 --- a/tests/procchange.ec +++ b/tests/procchange.ec @@ -1,4 +1,4 @@ -require import AllCore Distr. +require import AllCore Int Distr. (* -------------------------------------------------------------------- *) theory ProcChangeAssignEquiv. @@ -229,3 +229,50 @@ theory ProcChangeInWhileHoare. abort. end ProcChangeInWhileHoare. +theory ProcChangeHoareFrame. + module M = { + proc foo(uc: int) = { + var foo; + foo <- 1; + foo <- foo + uc; + return uc; + } + }. + + lemma minimalexamplelemma (a: int): + hoare [M.foo: arg = a ==> res = a]. + proof. + proc. + proc change [1..2] : { foo <- 1 + a; }. auto. auto. + qed. +end ProcChangeHoareFrame. + +theory ProcChangeEquivFrame. + module M = { + proc foo1(uc: int) = { + var foo; + foo <- 1; + foo <- foo + uc; + return uc; + } + + proc foo2(uc: int) = { + var foo; + uc <- uc + 1; + foo <- 0; + foo <- foo + uc; + uc <- uc - 1; + return uc; + } + }. + + lemma minimalexamplelemma (a: int): + equiv [M.foo1 ~ M.foo2 : ={arg} /\ arg{1} = a ==> ={res} /\ res{1} = a]. + proof. + proc. + proc change {1} [1..2] : { foo <- 1 + a; }. auto. + conseq (_: ={uc} /\ uc{1} = a /\ uc{2} = a ==> ); 1:auto. + proc change {2} [1..1] : { uc <- a + 1; }. auto. + fail proc change {2} [2..3] : { foo <- a + 1; }; smt(). + abort. +end ProcChangeEquivFrame.