From 37e7523248189306f5f00c4e6c786d7a810d7fec Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 12 Mar 2026 04:23:24 +0100 Subject: [PATCH] Forward call with framed pre --- src/ecHiTacticals.ml | 1 + src/ecMatching.ml | 4 + src/ecMatching.mli | 1 + src/ecParser.mly | 3 + src/ecParsetree.ml | 4 + src/phl/ecPhlExists.ml | 224 ++++++++++++++++++++++++++++++++++++++++ src/phl/ecPhlExists.mli | 1 + 7 files changed, 238 insertions(+) diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 8c4c4eae2f..6e150767e6 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -207,6 +207,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Phrex_elim -> EcPhlExists.t_hr_exists_elim | Phrex_intro (fs, b) -> EcPhlExists.process_exists_intro ~elim:b fs | Phecall (oside, x) -> EcPhlExists.process_ecall oside x + | Phecallfwd x -> EcPhlExists.process_ecallfwd x | Pexfalso -> EcPhlAuto.t_exfalso | Pbydeno (mode, info) -> EcPhlDeno.process_deno mode info | Pbyupto -> EcPhlUpto.process_uptobad diff --git a/src/ecMatching.ml b/src/ecMatching.ml index a14e8859b3..efbe257050 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -372,6 +372,10 @@ module EV = struct | Some (`Set _) -> true | _ -> false + let map (f : 'a -> 'a) (m : 'a evmap) = + { ev_map = Mid.map (omap f) m.ev_map + ; ev_unset = m.ev_unset } + let doget (x : ident) (m : 'a evmap) = match get x m with | Some (`Set a) -> a diff --git a/src/ecMatching.mli b/src/ecMatching.mli index 66c6bc2006..cd1a01301e 100644 --- a/src/ecMatching.mli +++ b/src/ecMatching.mli @@ -150,6 +150,7 @@ module EV : sig val isset : ident -> 'a evmap -> bool val set : ident -> 'a -> 'a evmap -> 'a evmap val get : ident -> 'a evmap -> [`Unset | `Set of 'a] option + val map : ('a -> 'a) -> 'a evmap -> 'a evmap val doget : ident -> 'a evmap -> 'a val fold : (ident -> 'a -> 'b -> 'b) -> 'a evmap -> 'b -> 'b val filled : 'a evmap -> bool diff --git a/src/ecParser.mly b/src/ecParser.mly index 3577c6d759..235e96f0f8 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3118,6 +3118,9 @@ interleave_info: | ECALL s=side? x=paren(p=qident tvi=tvars_app? fs=sform* { (p, tvi, fs) }) { Phecall (s, x) } +| ECALL RRARROW pterm=paren(p=qident tvi=tvars_app? fs=loc(gpterm_arg)* { (p, tvi, fs) }) + { Phecallfwd pterm } + | EXFALSO { Pexfalso } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 54fe47aa6c..aff4deab8f 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -736,6 +736,9 @@ type matchmode = [ (* -------------------------------------------------------------------- *) type prrewrite = [`Rw of ppterm | `Simpl] +(* -------------------------------------------------------------------- *) +type pecallfwd = pqsymbol * ptyannot option * ppt_arg located list + (* -------------------------------------------------------------------- *) type phltactic = | Pskip @@ -775,6 +778,7 @@ type phltactic = | Phrex_elim | Phrex_intro of (pformula list * bool) | Phecall of (oside * (pqsymbol * ptyannot option * pformula list)) + | Phecallfwd of pecallfwd | Pexfalso | Pbydeno of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option)) | PPr of (pformula * pformula) option diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml index 90f017cbb1..a6452d856f 100644 --- a/src/phl/ecPhlExists.ml +++ b/src/phl/ecPhlExists.ml @@ -239,3 +239,227 @@ let process_ecall oside (l, tvi, fs) tc = let tc = FApi.t_focus (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) tc in FApi.t_last EcPhlAuto.t_auto (FApi.t_rotate `Right 1 tc) + +(* -------------------------------------------------------------------- *) +let process_ecallfwd ((ctt_path, ctt_tvi, ctt_args) : APT.pecallfwd) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let env = EcEnv.LDecl.toenv hyps in + + (* Check that we are in a Hoare statement and that first instruction + * is a call statement. *) + let concl = tc1_as_hoareS tc in + let (lvalue, funname, _), _ = pf_first_call !!tc concl.hs_s in + + let lvalue = + match lvalue with + | Some lvalue -> lvalue + | None -> + tc_error !!tc "the call must have a left-value" in + + (* Type-check contract (lemma) - apply it fully to find the Hoare contract *) + let ptenv = PT.ptenv_of_penv (LDecl.push_active_ss concl.hs_m hyps) !!tc in + let contract = + let rec apply_all (contract : PT.pt_ev) = + if is_some (TTC.destruct_product ~reduce:true hyps contract.ptev_ax) then + apply_all (PT.apply_pterm_to_hole contract) + else contract + in + let contract = PT.process_pterm ptenv (APT.FPNamed (ctt_path, ctt_tvi)) in + let contract, _ = PT.process_pterm_args_app contract ctt_args in + apply_all contract + in + + let rec collect_pvars_from_pt (pt : proofterm) = + match pt with + | PTApply { pt_args = args } -> begin + args + |> List.to_seq + |> Seq.map collect_pvars_from_ptarg + |> Seq.fold_left EcPV.PV.union EcPV.PV.empty + end + | PTQuant (_, pt) -> + collect_pvars_from_pt pt + + and collect_pvars_from_ptarg (ptarg : pt_arg) = + match ptarg with + | PAFormula f -> collect_pvars_from_form f + | PAMemory _ -> EcPV.PV.empty + | PAModule _ -> EcPV.PV.empty + | PASub pt -> odfl EcPV.PV.empty (omap collect_pvars_from_pt pt) + + and collect_pvars_from_form (f : form) = + let pvs = ref EcPV.PV.empty in + let rec doit (f : form) = + match f.f_node with + | Fpvar (pv, _) -> + pvs := EcPV.PV.add env pv f.f_ty !pvs + | _ -> EcFol.f_iter doit f + in doit f; !pvs + in + + begin + let contract = + try + destr_hoareF contract.ptev_ax + with DestrError _ -> + tc_error_lazy ~loc:(L.loc ctt_path) !!tc (fun fmt -> + Format.fprintf fmt + "contract %a should be a Hoare statement" + EcSymbols.pp_qsymbol (L.unloc ctt_path) + ) + in + + if not (EcReduction.EqTest.for_xp env funname contract.hf_f) then begin + tc_error_lazy ~loc:(L.loc ctt_path) !!tc (fun fmt -> + let ppe = EcPrinting.PPEnv.ofenv env in + Format.fprintf fmt + "contract %a should be for the procedure %a, not %a" + EcSymbols.pp_qsymbol (L.unloc ctt_path) + (EcPrinting.pp_funname ppe) funname + (EcPrinting.pp_funname ppe) contract.hf_f + ) + end; + + if not (POE.is_empty (hf_po contract).hsi_inv) then + tc_error ~loc:(L.loc ctt_path) !!tc + "contract must have an empty exception post-condition"; + end; + + let pvs = collect_pvars_from_pt contract.ptev_pt in + let pvs, _ = EcPV.PV.elements pvs in + let ids = List.map (fun (pv, ty) -> + (EcIdent.create (Format.sprintf "%s_" (EcTypes.symbol_of_pv pv)), ty) + ) pvs in + let pvs_as_inv = List.map (fun (pv, ty) -> + Inv_ss (f_pvar pv ty (fst concl.hs_m)) + ) pvs in + + let tc = t_hr_exists_intro_r pvs_as_inv tc in + let tc = FApi.t_focus (t_hr_exists_elim_r ~bound:(List.length ids)) tc in + let tc = FApi.t_focus (t_intros_i (List.fst ids)) tc in + + let subst = List.fold_left (fun subst ((pv, ty), x) -> + EcPV.PVM.add env pv (fst concl.hs_m) (f_local x ty) subst + ) EcPV.PVM.empty (List.combine pvs (List.fst ids)) in + + let contract = + let hyps = List.fold_left (fun hyps (x, ty) -> + EcEnv.LDecl.add_local x (LD_var (ty, None)) hyps + ) contract.ptev_env.pte_hy ids in + + { contract with + ptev_env = { contract.ptev_env with pte_hy = hyps} } in + + let rec subst_pt (pt : proofterm) = + match pt with + | PTApply { pt_head; pt_args } -> + PTApply + { pt_head = subst_pt_head pt_head + ; pt_args = List.map subst_pt_arg pt_args } + | PTQuant _ -> assert false + + and subst_pt_head (pth : pt_head) = + match pth with + | PTHandle _ + | PTLocal _ + | PTGlobal _ -> pth + | PTCut (f, cs) -> PTCut (subst_form f, cs) + | PTTerm pt -> PTTerm (subst_pt pt) + + and subst_pt_arg (pta : pt_arg) = + match pta with + | PAFormula f -> PAFormula (subst_form f) + | PAMemory _ -> pta + | PAModule _ -> pta + | PASub pt -> PASub (omap subst_pt pt) + + and subst_pt_ev (ptev : PT.pt_ev) = + let ptev_env = subst_pt_env ptev.ptev_env in + let ptev_ax = subst_form ptev.ptev_ax in + let ptev_pt = subst_pt ptev.ptev_pt in + PT.{ ptev_env; ptev_ax; ptev_pt; } + + and subst_pt_env (ptenv : PT.pt_env) = + { pte_pe = ptenv.pte_pe + ; pte_hy = ptenv.pte_hy + ; pte_ue = EcUnify.UniEnv.copy ptenv.pte_ue + ; pte_ev = ref (subst_mevmap !(ptenv.pte_ev)) } + + and subst_mevmap (evm : EcMatching.mevmap) = + { evm with + evm_form = EcMatching.EV.map subst_form evm.evm_form; } + + and subst_form (f : form) = + EcPV.PVM.subst env subst f + in + + let contract = subst_pt_ev contract in + + let seqf = + let inv = destr_hoareF contract.ptev_ax in + let inv = POE.lower (hf_po inv) in + let inv = ss_inv_rebind inv (fst concl.hs_m) in + let lv = + List.map + (fun (pv, ty) -> (f_pvar pv ty inv.m).inv) + (EcModules.lv_to_ty_list lvalue) in + let sargs = + EcPV.PVM.add + env EcTypes.pv_res inv.m + (f_tuple lv) EcPV.PVM.empty in + + { inv = EcPV.PVM.subst env sargs inv.inv; m = inv.m; } in + + let seqf_frame = + let wr = EcPV.lp_write env lvalue in + + let rec doit (f : form) = + match sform_of_form f with + | SFand (mode, (f1, f2)) -> begin + match doit f1, doit f2 with + | None, None -> None + | Some f, None | None, Some f -> Some f + | Some f1, Some f2 -> begin + match mode with + | `Sym -> Some (f_and f1 f2) + | `Asym -> Some (f_anda f1 f2) + end + end + + | _ -> begin + let pvs = + let pvs = ref EcPV.PV.empty in + let rec f_read (f : form) = + match f.f_node with + | Fpvar (pv, _) -> pvs := EcPV.PV.add env pv f.f_ty !pvs + | _ -> f_iter f_read f + in f_read f; !pvs in + + if EcPV.PV.indep env pvs wr then + Some f + else None + end + + in { inv = odfl f_true (doit (hs_pr concl).inv); m = (hs_pr concl).m; } in + + let tc = + FApi.t_first + (EcPhlSeq.t_hoare_seq (Zpr.cpos 1) (map_ss_inv2 f_and seqf seqf_frame)) + tc in + + let tc = FApi.t_first EcPhlHoare.t_hoaresplit tc in + let tc = FApi.t_first (EcPhlConseq.t_conseqauto ~delta:false ?tsolve:None) tc in + let tc = FApi.t_first EcPhlTAuto.t_hoare_true tc in + + let tc = FApi.t_first (EcPhlCall.t_call None contract.ptev_ax) tc in + let tc = FApi.t_sub [ + EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true contract.ptev_pt; + EcPhlSkip.t_skip; + t_id + ] tc in + + let tc = + FApi.t_firsts + (t_generalize_hyps ~clear:`Yes (List.fst ids)) 2 tc in + + tc diff --git a/src/phl/ecPhlExists.mli b/src/phl/ecPhlExists.mli index 685af80a7d..f6135942d4 100644 --- a/src/phl/ecPhlExists.mli +++ b/src/phl/ecPhlExists.mli @@ -11,3 +11,4 @@ val t_hr_exists_intro : inv list -> backward (* -------------------------------------------------------------------- *) val process_exists_intro : elim:bool -> pformula list -> backward val process_ecall : oside -> pqsymbol * ptyannot option * pformula list -> backward +val process_ecallfwd : pecallfwd -> backward