From ec27a06b2b46f909dd74b36d0004321dc5d38f0f Mon Sep 17 00:00:00 2001 From: mbbarbosa Date: Wed, 3 Jun 2026 22:52:50 +0100 Subject: [PATCH] feat(phl): support backward ecall on bdHoare/phoare goals MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extend backward `ecall` to bdHoare statement goals, so a bdHoare/phoare contract can be applied to the last call of a phoare goal — mirroring the existing hoare backward `ecall`. - ecPhlExists.ml: add `t_ecall_bdhoare_bwd` / `process_ecall_bdhoare`, and dispatch `FbdHoareS` in `process_ecall` (phoare added to the no-xhl error kinds). Program-variable contract arguments are handled via the existing ecall abstraction machinery; a trivial probability split routes the suffix call through `t_bdhoare_seq`, lifting the hoare prefix subgoal via `t_hoareS_conseq_bdhoare`. The split is sound only for lossless [= 1%r] goals and contracts, so both are checked up-front and out-of-scope uses are rejected with an explanatory message instead of failing deep inside t_call. - ecPhlConseq.mli: expose `t_hoareS_conseq_bdhoare`. - tests/phoare-ecall-bwd.ec: cover the lossless backward ecall plus the forward/side/non-lossless rejections. --- src/phl/ecPhlConseq.mli | 2 + src/phl/ecPhlExists.ml | 167 +++++++++++++++++++++++++++++++++++++- tests/phoare-ecall-bwd.ec | 93 +++++++++++++++++++++ 3 files changed, 261 insertions(+), 1 deletion(-) create mode 100644 tests/phoare-ecall-bwd.ec diff --git a/src/phl/ecPhlConseq.mli b/src/phl/ecPhlConseq.mli index ede40923c..3d4774daf 100644 --- a/src/phl/ecPhlConseq.mli +++ b/src/phl/ecPhlConseq.mli @@ -23,6 +23,8 @@ val t_bdHoareF_conseq_bd : hoarecmp -> ss_inv -> FApi.backward val t_hoareS_conseq_conj : ss_inv -> hs_inv -> ss_inv -> hs_inv -> FApi.backward +val t_hoareS_conseq_bdhoare : FApi.backward + (* -------------------------------------------------------------------- *) val t_equivF_conseq_nm : ts_inv -> ts_inv -> FApi.backward val t_equivS_conseq_nm : ts_inv -> ts_inv -> FApi.backward diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml index 7d983d1d7..108ffebbc 100644 --- a/src/phl/ecPhlExists.ml +++ b/src/phl/ecPhlExists.ml @@ -449,6 +449,166 @@ let t_ecall_hoare_bwd ((cttpt, _) : proofterm * form) (tc : tcenv1) = EcPhlAuto.t_auto ?conv:None; (* Kill the conseq from the call rule *) ] tc +(* -------------------------------------------------------------------- *) +(* Backward ecall on bdHoare/phoare goals (ecall without ->>). + * + * Mirrors t_ecall_hoare_bwd but for a bdHoare goal and a bdHoare/phoare + * contract. We abstract program-variable arguments of the contract pterm + * into fresh local idents, dispatch to [t_call None ctt] (which routes + * via [t_call]'s (FbdHoareF, FbdHoareS) arm to [t_bdhoare_call]), then + * re-generalize over the abstracted idents in the residual goals. + * + * The prefix is split from the call with [t_bdhoare_seq] under a fixed + * trivial probability split (f1=f2=1%r, g1=g2=0%r, pR=true). That split + * only discharges the resulting bound side-conditions when the goal — and + * the contract — are lossless [= 1%r]; both are checked up-front so that + * out-of-scope goals are rejected cleanly rather than failing deep inside + * [t_call]. The residual goal handed back to the user is the prefix, lifted + * to a lossless bdHoare goal so that further ecalls keep dispatching here. + *) +let t_ecall_bdhoare_bwd ((cttpt, _) : proofterm * form) (tc : tcenv1) = + let hyps = FApi.tc1_hyps tc in + let env = EcEnv.LDecl.toenv hyps in + let concl = destr_bdHoareS (FApi.tc1_goal tc) in + let m = fst (concl.bhs_m) in + let call, _ = pf_last_call !!tc concl.bhs_s in + + (* The trivial probability split below (f1=f2=1, g1=g2=0) only discharges + * the bound side-conditions when the goal is [= 1%r] (lossless). For any + * other comparison or bound the construction would fail opaquely deep in + * [t_call]/[apply]; reject up-front with an explanatory message instead. *) + if concl.bhs_cmp <> FHeq || not (f_equal (bhs_bd concl).inv f_r1) then + tc_error !!tc + "backward ecall on phoare goals is only supported for lossless `= 1%%r' goals"; + + let pvs = PT.collect_pvars_from_pt cttpt in + let ids, _, pvs_as_inv, subst = abstract_pvs hyps [m] pvs in + + let cttpt = + let pt_head, pt_args = + match cttpt with + | PTApply { pt_head; pt_args } -> (pt_head, pt_args) + | _ -> assert false in + let pt_args = List.map (PT.subst_pv_pt_arg env subst) pt_args in + PTApply { pt_head; pt_args } in + + let cttpt, ctt = EcLowGoal.LowApply.check `Elim cttpt (`Hyps (hyps, !!tc)) in + + let ctt = + EcReduction.h_red_opt EcReduction.full_red hyps ctt + |> odfl ctt in + + let ids_subst = + List.fold_left2 + (fun s (id, _) pv -> EcSubst.add_flocal s id (inv_of_inv pv)) + EcSubst.empty ids pvs_as_inv in + + let hf = destr_bdHoareF ctt in + + (* The suffix call subgoal is synthesized with bound [= 1%r]; only a + * lossless [= 1%r] contract applies to it. *) + if hf.bhf_cmp <> FHeq || not (f_equal (bhf_bd hf).inv f_r1) then + tc_error !!tc + "backward ecall on phoare goals requires a lossless `= 1%%r' contract"; + + let fpre, fpost = + (ss_inv_rebind (bhf_pr hf) m).inv, (ss_inv_rebind (bhf_po hf) m).inv + in + + let post = + EcPhlCall.compute_hoare_call_post + hyps m (fpre, POE.empty fpost) call + (POE.empty (bhs_po concl).inv) in + let post = EcSubst.subst_form ids_subst post in + + (* Trivial probability split for FHeq with bound 1%r (lossless body): + pR = true, f1=f2=1%r, g1=g2=0%r. Yields: + - cond_phi : f_hoareS pre s1 post (user-level prefix, as hoare) + - condf1 : pre s1 true 1%r (lossless prefix, trivial for det. code) + - condf2 : phi s2 bhs_po 1%r (suffix bdhoare, target of t_call) + - condg1 : pre s1 false 0%r (trivial) + - condbd : 1*1+0*0 = bd (trivial when bd=1%r) + - condnm : forall r1 r2 ... (trivial) *) + let seq_info = + let phi = { m; inv = post } in + let pR = { m; inv = f_true } in + let f1 = { m; inv = f_r1 } in + let f2 = { m; inv = f_r1 } in + let g1 = { m; inv = f_r0 } in + let g2 = { m; inv = f_r0 } in + (phi, pR, f1, f2, g1, g2) + in + + let tc = EcPhlSeq.t_bdhoare_seq (GapBefore cpos1_last) seq_info tc in + (* Subgoal order from t_bdhoare_seq (with f1≠0, f2≠0, g1=0): + [cond_phi; condf1; condf2; condg1; condbd; condnm] + We apply the exists+intros+t_call pipeline to condf2 (the suffix). + The intros chain leaves a single bdhoare goal on which t_call produces + two subgoals (contract obligation + conseq); we then dispatch via + t_seqsub. *) + let condf2_tactic = + FApi.t_seqs [ + t_hr_exists_intro_r pvs_as_inv; + t_hr_exists_elim_r ~bound:(List.length ids); + t_intros_i (List.fst ids); + FApi.t_seqsub + (EcPhlCall.t_call None ctt) + [ EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true cttpt; + EcPhlAuto.t_auto ?conv:None; ]; + ] + in + + (* t_bdhoare_seq_r auto-closes condnm via t_try, so the count is 5 (or 6 if + that auto fails). Use t_onalli with an index-based dispatcher to be + robust to either count. Order (0-indexed): + 0 -> cond_phi (HOARE prefix): lift to BDHOARE [pre ==> phi] FHeq 1%r + via t_hoareS_conseq_bdhoare. This is sound under losslessness of + the prefix — which the user proves as part of the residual goal. + Subsequent ecalls then dispatch through our bdhoare arm and accept + phoare contracts. + 2 -> condf2 (suffix call dance) + others -> auto (trivial bound conditions). *) + let tc = + FApi.t_onalli + (fun i -> + if i = 0 then EcPhlConseq.t_hoareS_conseq_bdhoare + else if i = 2 then condf2_tactic + else EcPhlAuto.t_auto ?conv:None) + tc + in + + tc + +(* -------------------------------------------------------------------- *) +let process_ecall_bdhoare + (dir : APT.pdirection) + (pterm : APT.pecall) + (tc : tcenv1) += + if dir <> `Backward then + tc_error !!tc "forward ecall on bdHoare/phoare goals is not supported"; + + let (ctt_path, ctt_tvi, ctt_args) = pterm in + let hyps = FApi.tc1_hyps tc in + let concl = destr_bdHoareS (FApi.tc1_goal tc) in + + (* Type-check contract (lemma) - apply it fully to find the bdHoare contract *) + let ptenv = PT.ptenv_of_penv (LDecl.push_active_ss concl.bhs_m hyps) !!tc 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 + let contract = PT.apply_pterm_to_max_holes hyps contract in + + assert (PT.can_concretize contract.PT.ptev_env); + let contract = PT.concretize contract in + + let call, _ = pf_last_call !!tc concl.bhs_s in + + check_contract_type + ~phoare:true ~noexn:false ~loc:(L.loc ctt_path) ~name:(L.unloc ctt_path) + !!tc hyps (`Single call) (snd contract); + + t_ecall_bdhoare_bwd contract tc + (* -------------------------------------------------------------------- *) let process_ecall_hoare (dir : APT.pdirection) @@ -626,7 +786,12 @@ let process_ecall tc_error !!tc "cannot provide a side for Hoare goals"; process_ecall_hoare dir pterm tc + | FbdHoareS _ -> + if Option.is_some oside then + tc_error !!tc "cannot provide a side for bdHoare/phoare goals"; + process_ecall_bdhoare dir pterm tc + | FequivS _ -> process_ecall_equiv dir oside pterm tc - | _ -> tc_error_noXhl ~kinds:[`Hoare `Stmt; `Equiv `Stmt] !!tc + | _ -> tc_error_noXhl ~kinds:[`Hoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] !!tc diff --git a/tests/phoare-ecall-bwd.ec b/tests/phoare-ecall-bwd.ec new file mode 100644 index 000000000..fcd8097f2 --- /dev/null +++ b/tests/phoare-ecall-bwd.ec @@ -0,0 +1,93 @@ +require import AllCore Distr DBool. + +(* ================================================================== *) +(* Backward ecall on bdHoare/phoare goals. *) +(* *) +(* Only lossless [= 1%r] goals with a lossless [= 1%r] contract are *) +(* supported: the construction routes the suffix call through a *) +(* trivial probability split that is sound only at bound 1%r. *) +(* ================================================================== *) + +module M = { + proc f(x : int) : int = { + return x + 1; + } + + proc g(x : int) : int = { + var y, r : int; + y <- x + 1; + r <@ f(y); + return r; + } + + proc h(x : int) : int = { + var b : bool; + b <$ dbool; + return b ? 1 : 0; + } + + proc gh(x : int) : int = { + var r : int; + r <@ h(x); + return r; + } +}. + +(* ================================================================== *) +(* Test 1: Backward ecall, lossless contract *) +(* ================================================================== *) +lemma f_spec : phoare[ M.f : x = 1 ==> res = 2 ] = 1%r. +proof. by proc; auto. qed. + +(* The call is the last instruction, with a non-empty deterministic + prefix. ecall consumes the call and leaves the (lossless) prefix. *) +lemma g_spec : phoare[ M.g : x = 0 ==> res = 2 ] = 1%r. +proof. +proc. +ecall (f_spec). +auto. +qed. + +(* ================================================================== *) +(* Test 2: Forward ecall on phoare (negative test) *) +(* ================================================================== *) +lemma g_fwd : phoare[ M.g : x = 0 ==> res = 2 ] = 1%r. +proof. +proc. +fail ecall ->> (f_spec). +abort. + +(* ================================================================== *) +(* Test 3: side annotation on phoare (negative test) *) +(* ================================================================== *) +lemma g_side : phoare[ M.g : x = 0 ==> res = 2 ] = 1%r. +proof. +proc. +fail ecall{1} (f_spec). +abort. + +(* ================================================================== *) +(* Test 4: non-[= 1%r] goal is rejected up-front (negative test) *) +(* ================================================================== *) +lemma h_le : phoare[ M.h : true ==> res = 1 ] <= (1%r / 2%r). +proof. admit. qed. + +(* The goal bound is [<= 1/2], not [= 1%r]: the goal guard fires + before the construction reaches t_call. *) +lemma gh_le : phoare[ M.gh : true ==> res = 1 ] <= (1%r / 2%r). +proof. +proc. +fail ecall (h_le). +abort. + +(* ================================================================== *) +(* Test 5: non-[= 1%r] contract is rejected up-front (neg. test) *) +(* ================================================================== *) + +(* The goal is lossless [= 1%r] but the contract is [<= 1/2]: the + contract guard fires rather than failing opaquely inside apply. *) +lemma gh_eq : phoare[ M.gh : true ==> res = 1 ] = 1%r. +proof. +proc. +fail ecall (h_le). +abort.