From 47ca6ff6963bc70da772f1b38f51d277f8599844 Mon Sep 17 00:00:00 2001 From: Lucas Tabary-Maujean Date: Wed, 17 Jun 2026 19:31:22 +0200 Subject: [PATCH] feat: variant for up-to-bad call/proc tactics MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The premise: ∀O. is_lossless O => is_lossless A(O) (1) of the current up-to-bad tactics happens to be too restrictive in some cases. At first glance, it seems that it would be possible to allow another variant of the tactic that instead requires is_lossless A(O_1) ∧ is_lossless A(O_2) (2) (possibly as two differents subgoals), which can be proved in some concrete instances of A, O_1, O_2, while (1) is not. Simply introducing a variant of the tactic that replaces (1) with (2) is not satisfactory and is not ensured to be sound. This is because commit 6534f3dc36b49905705dd30fc9e0432c2f63bd17 (yes, some archeology was required) changed the premises of this tactic, which implicitly changes the proof of soundness of the tactic. This PR provides a way to use a different set of premises, which restores the original conditions required for applying up-to-bad tactics, as well as changes condition (1) with (2) (which is the original goal). feat(parser): improve the syntax of new up-to-bad call variant fix(Parsetree): use a record type for `fun_upto_info` --- src/ecHiTacticals.ml | 2 +- src/ecParser.mly | 62 +++++++++++++++++++++++-------- src/ecParsetree.ml | 15 ++++++-- src/phl/ecPhlCall.ml | 10 ++--- src/phl/ecPhlCall.mli | 2 +- src/phl/ecPhlFun.ml | 74 ++++++++++++++++++++++--------------- src/phl/ecPhlFun.mli | 8 ++-- tests/proc_ll.ec | 85 +++++++++++++++++++++++++++++++++++++++++++ 8 files changed, 197 insertions(+), 61 deletions(-) create mode 100644 tests/proc_ll.ec diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 0595c5d9e8..ed9e0a3747 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -188,7 +188,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Pfusion info -> EcPhlLoopTx.process_fusion info | Punroll info -> EcPhlLoopTx.process_unroll info | Psplitwhile info -> EcPhlLoopTx.process_splitwhile info - | Pcall (side, info) -> EcPhlCall.process_call side info + | Pcall info -> EcPhlCall.process_call info | Pcallconcave info -> EcPhlCall.process_call_concave info | Pswap sw -> EcPhlSwap.process_swap sw | Pinline info -> EcPhlInline.process_inline info diff --git a/src/ecParser.mly b/src/ecParser.mly index f33d99e5b4..411a9c5daa 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -21,6 +21,15 @@ pty_locality = locality; } + let map_gppterm f a = + let fp_head = match a.fp_head with + | FPNamed _ as x -> x + | FPCut x -> FPCut (f x) + in + { a with fp_head } + + let apply_gppterm x = map_gppterm (fun f -> f x) + let opdef_of_opbody ty b = match b with | None -> PO_abstr ty @@ -2315,6 +2324,13 @@ intro_pattern: | cm=crushmode { IPCrush cm } +gpterm_head0(F): +| p=qident tvi=tvars_app? + { (false, FPNamed (p, tvi)) } + +| LPAREN exp=iboption(AT) UNDERSCORE? COLON f=F RPAREN + { (exp, FPCut f) } + gpterm_head(F): | exp=iboption(AT) p=qident tvi=tvars_app? { (exp, FPNamed (p, tvi)) } @@ -2353,7 +2369,7 @@ gpterm_arg: { EA_tactic `DoneSmt } gpterm(F): -| hd=gpterm_head(F) +| hd=gpterm_head0(F) { mk_pterm (fst hd) (snd hd) [] } | LPAREN hd=gpterm_head(F) args=loc(gpterm_arg)* RPAREN @@ -2534,13 +2550,15 @@ conseq_xt: call_info: | f1=form LONGARROW f2=form poe=hoare_epost(none) - { CI_spec (f1, { pnormal = f2; pexcept = poe}) } + { fun _ -> CI_spec (f1, { pnormal = f2; pexcept = poe}) } | f=form - { CI_inv (f) } -| bad=form COMMA p=form - { CI_upto (bad,p,None) } -| bad=form COMMA p=form COMMA q=form - { CI_upto (bad,p,Some q) } + { fun _ -> CI_inv (f) } +| fui_bad=form COMMA fui_pre=form + { fun fui_is_ll_variant -> + CI_upto {fui_is_ll_variant; fui_bad; fui_pre; fui_pos = None} } +| fui_bad=form COMMA fui_pre=form COMMA pos=form + { fun fui_is_ll_variant -> + CI_upto {fui_is_ll_variant; fui_bad; fui_pre; fui_pos = Some pos} } icodepos_r: | IF { (`If :> pcp_match) } @@ -2646,11 +2664,11 @@ s_codegap1_before_(I): | LBRACKET cps=codepos1 DOTDOT cpe=codepos1 RBRACKET { (GapBefore cps, GapAfter cpe) } -| LBRACKET cps=codepos1 PLUSGT cpo=loc(mparen(sword)) RBRACKET { +| LBRACKET cps=codepos1 PLUSGT cpo=loc(mparen(sword)) RBRACKET { if unloc cpo > 0 then begin let (offset, base) = cps in (GapBefore cps, GapAfter (offset + unloc cpo, base)) - end else + end else parse_error (loc cpo) (Some "cannot give negative offset for codepos range end") } @@ -2955,7 +2973,7 @@ eager_tac: { Peager_fun_abs f } | CALL info=gpterm(call_info) - { Peager_call info } + { Peager_call (apply_gppterm None info) } form_or_double_form: | f=sform @@ -3033,8 +3051,8 @@ direction: | PROC f=sform { Pfun (`Abs f) } -| PROC bad=sform p=sform q=sform? - { Pfun (`Upto (bad, p, q)) } +| PROC fui_is_ll_variant=calloptions fui_bad=sform fui_pre=sform fui_pos=sform? + { Pfun (`Upto { fui_is_ll_variant; fui_bad; fui_pre; fui_pos }) } | PROC STAR { Pfun `Code } @@ -3057,11 +3075,11 @@ direction: | ASYNC WHILE info=async_while_tac_info { Pasyncwhile info } -| CALL s=side? info=gpterm(call_info) - { Pcall (s, info) } +| CALL c=calloptions s=side? info=gpterm(call_info) + { Pcall (s, apply_gppterm c info) } | CALL SLASH fc=sform info=gpterm(call_info) - { Pcallconcave (fc,info) } + { Pcallconcave (fc, apply_gppterm None info) } | RCONDT s=side? i=codepos1 { Prcond (s, true, i) } @@ -3436,6 +3454,20 @@ caseoption: %inline caseoptions: | AT xs=bracket(caseoption+) { xs } + +calloption: +| b=boption(MINUS) x=lident { + match unloc x with + | "ll" -> (not b) + | _ -> + parse_error x.pl_loc + (Some ("invalid option: " ^ (unloc x) ^ ", [-]ll expected")) + } + +%inline calloptions: +| AT b=bracket(calloption) { Some b } +| { None } + %inline do_repeat: | n=word? NOT { (`All, n) } | n=word? QUESTION { (`Maybe, n) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 1ecbbe97be..7865bc9fb1 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -586,18 +586,25 @@ type pswap_kind = { type interleave_info = oside * (int * int) * ((int * int) list) * int +type pspattern = unit + type pipattern = | PtAny | PtAsgn of psymbol list | PtIf of pspattern * [`NoElse | `MaybeElse | `Else of pspattern] | PtWhile of pspattern -and pspattern = unit +type fun_upto_info = { + fui_is_ll_variant : bool option; + fui_bad : pformula; + fui_pre : pformula; + fui_pos : pformula option; +} type call_info = | CI_spec of (pformula * phoare_post) | CI_inv of pformula - | CI_upto of (pformula * pformula * pformula option) + | CI_upto of fun_upto_info type p_seq_xt_info = | PSeqNone @@ -668,7 +675,7 @@ type fun_info = [ | `Def | `Code | `Abs of pformula - | `Upto of pformula * pformula * pformula option + | `Upto of fun_upto_info ] (* -------------------------------------------------------------------- *) @@ -798,7 +805,7 @@ type phltactic = | Pfusion of (oside * pcodepos * (int * (int * int))) | Punroll of (oside * pcodepos * [`While | `For of bool]) | Psplitwhile of (pexpr * oside * pcodepos) - | Pcall of oside * call_info gppterm + | Pcall of (oside * call_info gppterm) | Pcallconcave of (pformula * call_info gppterm) | Prcond of (oside * bool * pcodepos1) | Prmatch of (oside * symbol * pcodepos1) diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 25cc4fc50a..fda5058072 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -531,7 +531,7 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr = let ensure_none_poe tc poe = if not (is_none poe) then tc_error !!tc "exception are not supported" -let process_call side info tc = +let process_call (side, info) tc = let process_spec_2 tc side pre post = let (hyps, concl) = FApi.tc1_flat tc in match concl.f_node, side with @@ -649,7 +649,7 @@ let process_call side info tc = let ml, mr = fst es.es_ml, fst es.es_mr in let (_,fl,_) = fst (tc1_last_call tc es.es_sl) in let (_,fr,_) = fst (tc1_last_call tc es.es_sr) in - let bad,invP,invQ = EcPhlFun.process_fun_upto_info info tc in + let weakened_pre,bad,invP,invQ = EcPhlFun.process_fun_upto_info info tc in let bad2 = ss_inv_generalize_as_right bad ml mr in let invP = ts_inv_rebind invP ml mr in let invQ = ts_inv_rebind invQ ml mr in @@ -664,7 +664,7 @@ let process_call side info tc = let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in let pre = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands (eq_params::lpre)) in let post = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands [eq_res;eqglob;invP]) in - (bad,invP,invQ, f_equivF pre fl fr post) + (weakened_pre,bad,invP,invQ, f_equivF pre fl fr post) | _ -> tc_error !!tc "the conclusion is not an equiv" in @@ -691,10 +691,10 @@ let process_call side info tc = end | CI_upto info -> - let bad, p, q, form = process_upto tc side info in + let weakened_pre, bad, p, q, form = process_upto tc side info in let t_tr = FApi.t_or (t_assumption `Conv) t_trivial in subtactic := (fun tc -> - FApi.t_firsts t_tr 3 (EcPhlFun.t_equivF_abs_upto bad p q tc)); + FApi.t_firsts t_tr 3 (EcPhlFun.t_equivF_abs_upto weakened_pre bad p q tc)); form in diff --git a/src/phl/ecPhlCall.mli b/src/phl/ecPhlCall.mli index 2cb7d1cd62..5d6b6e55f1 100644 --- a/src/phl/ecPhlCall.mli +++ b/src/phl/ecPhlCall.mli @@ -41,6 +41,6 @@ val t_equiv_call1 : side -> ss_inv -> ss_inv -> backward val t_call : oside -> form -> backward (* -------------------------------------------------------------------- *) -val process_call : oside -> call_info gppterm -> backward +val process_call : oside * call_info gppterm -> backward val process_call_concave : pformula * call_info gppterm -> backward diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index ebee1e8fea..6b1449c3c4 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -1,6 +1,5 @@ (* -------------------------------------------------------------------- *) open EcUtils -open EcParsetree open EcPath open EcAst open EcTypes @@ -309,7 +308,9 @@ let t_equivF_abs = FApi.t_low1 "equiv-fun-abs" t_equivF_abs_r (* -------------------------------------------------------------------- *) module UpToLow = struct (* ------------------------------------------------------------------ *) - let equivF_abs_upto pf env fl fr (bad: ss_inv) (invP: ts_inv) (invQ: ts_inv) = + let equivF_abs_upto pf env weakened_pre fl fr (bad: ss_inv) (invP: ts_inv) (invQ: ts_inv) = + let weakened_pre = Option.value ~default:false weakened_pre in + let (topl, _fl, oil, sigl), (topr, _fr, oir, sigr) = EcLowPhlGoal.abstract_info2 env fl fr in @@ -345,23 +346,38 @@ module UpToLow = struct let pre = map_ts_inv EcFol.f_ands [map_ts_inv1 EcFol.f_not bad2; eq_params; invP] in let post = map_ts_inv3 EcFol.f_if_simpl bad2 invQ (map_ts_inv2 f_and eq_res invP) in let cond1 = f_equivF pre o_l o_r post in - let cond2 = - let f_r1 = {m=invQ.ml; inv=f_r1} in - let concl = ts_inv_lower_left1 (fun bq -> (f_bdHoareF bq o_l bq FHeq f_r1)) invQ in - f_forall_mems_ss_inv (mr, abstract_mt) - (map_ss_inv2 f_imp bad concl) in - let cond3 = - let f_r1 = {m=invQ.mr; inv=f_r1} in - let bq = map_ts_inv2 f_and bad2 invQ in - f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_bdHoareF bq o_r bq FHeq f_r1) bq) in - - [cond1; cond2; cond3] + if not weakened_pre then + let cond2 = + let f_r1 = {m=invQ.ml; inv=f_r1} in + let concl = ts_inv_lower_left1 (fun bq -> (f_bdHoareF bq o_l bq FHeq f_r1)) invQ in + f_forall_mems_ss_inv (mr, abstract_mt) + (map_ss_inv2 f_imp bad concl) in + let cond3 = + let f_r1 = {m=invQ.mr; inv=f_r1} in + let bq = map_ts_inv2 f_and bad2 invQ in + f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_bdHoareF bq o_r bq FHeq f_r1) bq) in + + [cond1; cond2; cond3] + else + let cond2 = + let concl = ts_inv_lower_left1 (fun bq -> (f_hoareF bq o_l (POE.lift bq))) invQ in + f_forall_mems_ss_inv (mr, abstract_mt) + (map_ss_inv2 f_imp bad concl) in + let cond3 = + let bq = map_ts_inv2 f_and bad2 invQ in + f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_hoareF bq o_r (POE.lift bq)) bq) in + + [cond1; cond2; cond3] in let sg = List.map2 ospec (OI.allowed oil) (OI.allowed oir) in let sg = List.flatten sg in - let lossless_a = lossless_hyps env topl fl.x_sub in - let sg = lossless_a :: sg in + let lossless_a = if not weakened_pre then + [ lossless_hyps env topl fl.x_sub ] + else + [ f_losslessF fl; f_losslessF fr ] + in + let sg = lossless_a @ sg in let eq_params = ts_inv_eqparams @@ -378,17 +394,17 @@ module UpToLow = struct end (* -------------------------------------------------------------------- *) -let t_equivF_abs_upto_r bad invP invQ tc = +let t_equivF_abs_upto_r weakened_pre bad invP invQ tc = let env = FApi.tc1_env tc in let ef = tc1_as_equivF tc in let pre, post, sg = - UpToLow.equivF_abs_upto !!tc env ef.ef_fl ef.ef_fr bad invP invQ + UpToLow.equivF_abs_upto !!tc env weakened_pre ef.ef_fl ef.ef_fr bad invP invQ in let tactic tc = FApi.xmutate1 tc `FunUpto sg in FApi.t_last tactic (EcPhlConseq.t_equivF_conseq pre post tc) -let t_equivF_abs_upto = FApi.t_low3 "equiv-fun-abs-upto" t_equivF_abs_upto_r +let t_equivF_abs_upto = t_equivF_abs_upto_r (* -------------------------------------------------------------------- *) module ToCodeLow = struct @@ -594,9 +610,6 @@ let t_fun_r (inv: inv) tc = let t_fun = FApi.t_low1 "fun" t_fun_r -(* -------------------------------------------------------------------- *) -type p_upto_info = pformula * pformula * (pformula option) - (* -------------------------------------------------------------------- *) let process_fun_def tc = let t_cont tcenv = @@ -610,23 +623,24 @@ let process_fun_to_code tc = t_fun_to_code_r tc (* -------------------------------------------------------------------- *) -let process_fun_upto_info (bad, p, q) tc = +let process_fun_upto_info info tc = + let open EcParsetree in let hyps = FApi.tc1_hyps tc in - let ml, mr = EcIdent.create "&1", EcIdent.create "&2" in + let ml, mr = (EcIdent.create "&1", EcIdent.create "&2") in let env' = LDecl.inv_memenv ml mr hyps in - let p = TTC.pf_process_form !!tc env' tbool p in - let q = q |> omap (TTC.pf_process_form !!tc env' tbool) |> odfl f_true in + let p = TTC.pf_process_form !!tc env' tbool info.fui_pre in + let q = info.fui_pos |> omap (TTC.pf_process_form !!tc env' tbool) |> odfl f_true in let m = EcIdent.create "&hr" in - let bad = + let bad = let env' = LDecl.push_active_ss (EcMemory.abstract m) hyps in - TTC.pf_process_form !!tc env' tbool bad + TTC.pf_process_form !!tc env' tbool info.fui_bad in - ({inv=bad;m}, {inv=p;ml;mr}, {inv=q;ml;mr}) + (info.fui_is_ll_variant, { inv = bad; m }, { inv = p; ml; mr }, { inv = q; ml; mr }) (* -------------------------------------------------------------------- *) let process_fun_upto info g = - let (bad, p, q) = process_fun_upto_info info g in - t_equivF_abs_upto bad p q g + let (weakened_pre, bad, p, q) = process_fun_upto_info info g in + t_equivF_abs_upto weakened_pre bad p q g (* -------------------------------------------------------------------- *) let process_fun_abs inv tc = diff --git a/src/phl/ecPhlFun.mli b/src/phl/ecPhlFun.mli index 1e2f1fee24..cecc8baace 100644 --- a/src/phl/ecPhlFun.mli +++ b/src/phl/ecPhlFun.mli @@ -15,12 +15,10 @@ val subst_pre : -> EcPV.PVM.subst (* -------------------------------------------------------------------- *) -type p_upto_info = pformula * pformula * (pformula option) - val process_fun_def : FApi.backward val process_fun_abs : pformula -> FApi.backward -val process_fun_upto_info : p_upto_info -> tcenv1 -> ss_inv * ts_inv * ts_inv -val process_fun_upto : p_upto_info -> FApi.backward +val process_fun_upto_info : fun_upto_info -> tcenv1 -> bool option * ss_inv * ts_inv * ts_inv +val process_fun_upto : fun_upto_info -> FApi.backward val process_fun_to_code : FApi.backward (* -------------------------------------------------------------------- *) @@ -49,7 +47,7 @@ val t_bdhoareF_fun_def : FApi.backward val t_equivF_fun_def : FApi.backward (* -------------------------------------------------------------------- *) -val t_equivF_abs_upto : ss_inv -> ts_inv -> ts_inv -> FApi.backward +val t_equivF_abs_upto : bool option -> ss_inv -> ts_inv -> ts_inv -> FApi.backward (* -------------------------------------------------------------------- *) val t_fun : inv -> FApi.backward diff --git a/tests/proc_ll.ec b/tests/proc_ll.ec new file mode 100644 index 0000000000..4c19adad07 --- /dev/null +++ b/tests/proc_ll.ec @@ -0,0 +1,85 @@ +require import AllCore. + +module type O = { + proc o (x:int) : int +}. + +module type A (O:O) = { + proc f () : bool +}. + +module O1 = { + var bad : bool + var s : int + proc o (x:int) = { + if (x = 10) { + bad <- true; + x <- 100; + } + s <- s + x; + return x; + } + +}. + +module O2 = { + import var O1 + + proc o (x:int) = { + if (x = 10) { + bad <- true; + x <- 200; + } + s <- s + x; + return x; + } +}. + +section SECTION. + +declare module A <: A {-O1}. + +equiv proc_ll : A(O1).f ~ A(O2).f : + if O1.bad{2} then ={O1.bad} + else ={glob A, O1.bad, O1.s} + ==> + if O1.bad{2} then ={O1.bad} + else ={res, glob A, O1.bad, O1.s}. +proof. + proc @[ll] O1.bad (={O1.bad, O1.s}) (={O1.bad}) => />. + (* A(O1).f is lossless *) + + admit. + (* A(O2).f is lossless *) + + admit. + (* ???? *) + + smt(). + (* Oracle are upto bad *) + + by proc; auto => />. + (* O1 preserves invariant once bad is set *) + + by move=> &2 h; proc; auto => />; rewrite h. + (* O2 preserves invariant once bad is set *) + by move=> &1; proc; auto => />; rewrite h. +qed. + +equiv proc_ll1 : A(O1).f ~ A(O2).f : + if O1.bad{2} then ={O1.bad} + else ={glob A, O1.bad, O1.s} + ==> + if O1.bad{2} then ={O1.bad} + else ={res, glob A, O1.bad, O1.s}. +proof. + proc *. + call @[ll] (_: O1.bad, ={O1.bad, O1.s}, ={O1.bad}). + (* A(O1).f is lossless *) + + admit. + (* A(O2).f is lossless *) + + admit. + (* Oracle are upto bad *) + + by proc; auto => />. + (* O1 preserves invariant once bad is set *) + + by move=> &2 h; proc; auto => />; rewrite h. + (* O2 preserves invariant once bad is set *) + + by move=> &1; proc; auto => />; rewrite h. + by auto. +qed. +