From f0ce419fff2e6fe1f24606396959ac838f11c8e9 Mon Sep 17 00:00:00 2001 From: Lucas Tabary-Maujean Date: Wed, 17 Jun 2026 19:31:22 +0200 Subject: [PATCH 1/2] 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. In order to have a sound variant 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). Some issues still need to be addressed w.r.t. parsing. Introducing a variant syntax in the spirit of `call @[weaker_pre]` causes shift/reduce conflicts. --- src/ecHiTacticals.ml | 2 +- src/ecParser.mly | 34 ++++++++++++++++------- src/ecParsetree.ml | 8 +++--- src/phl/ecPhlCall.ml | 10 +++---- src/phl/ecPhlCall.mli | 2 +- src/phl/ecPhlFun.ml | 63 ++++++++++++++++++++++++++----------------- src/phl/ecPhlFun.mli | 8 +++--- 7 files changed, 77 insertions(+), 50 deletions(-) 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 d5c5201bd6..77ba7f968c 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 @@ -2534,13 +2543,13 @@ 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) } + { fun _ -> CI_inv (f) } | bad=form COMMA p=form - { CI_upto (bad,p,None) } + { fun b -> CI_upto (b,bad,p,None) } | bad=form COMMA p=form COMMA q=form - { CI_upto (bad,p,Some q) } + { fun b -> CI_upto (b,bad,p,Some q) } icodepos_r: | IF { (`If :> pcp_match) } @@ -2955,7 +2964,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 +3042,8 @@ direction: | PROC f=sform { Pfun (`Abs f) } -| PROC bad=sform p=sform q=sform? - { Pfun (`Upto (bad, p, q)) } +| PROC c=calloptions bad=sform p=sform q=sform? + { Pfun (`Upto (c, bad, p, q)) } | PROC STAR { Pfun `Code } @@ -3057,11 +3066,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 +3445,11 @@ caseoption: %inline caseoptions: | AT xs=bracket(caseoption+) { xs } +(* FIXME: incongruous notation *) +%inline calloptions: +| PLUS { Some true } +| empty { 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 5b74c02c60..f50029b840 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -594,10 +594,12 @@ type pipattern = and pspattern = unit +type fun_upto_info = bool option * pformula * pformula * 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 +670,7 @@ type fun_info = [ | `Def | `Code | `Abs of pformula - | `Upto of pformula * pformula * pformula option + | `Upto of fun_upto_info ] (* -------------------------------------------------------------------- *) @@ -798,7 +800,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 7c6a843536..fd0a39cb88 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..cd93cf9062 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,7 +623,7 @@ 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 (weakened_pre, bad, p, q) tc = let hyps = FApi.tc1_hyps tc in let ml, mr = EcIdent.create "&1", EcIdent.create "&2" in let env' = LDecl.inv_memenv ml mr hyps in @@ -621,12 +634,12 @@ let process_fun_upto_info (bad, p, q) tc = let env' = LDecl.push_active_ss (EcMemory.abstract m) hyps in TTC.pf_process_form !!tc env' tbool bad in - ({inv=bad;m}, {inv=p;ml;mr}, {inv=q;ml;mr}) + (weakened_pre, {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 From c6c0467e83aa271bc9c8fc957bbd297e21f7fc7d Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Fri, 19 Jun 2026 18:43:48 +0200 Subject: [PATCH 2/2] improve the syntax --- src/ecParser.mly | 28 ++++++++++++---- tests/proc_ll.ec | 85 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 107 insertions(+), 6 deletions(-) create mode 100644 tests/proc_ll.ec diff --git a/src/ecParser.mly b/src/ecParser.mly index 77ba7f968c..564444e5a5 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2324,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)) } @@ -2362,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 @@ -2655,11 +2662,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") } @@ -3445,10 +3452,19 @@ caseoption: %inline caseoptions: | AT xs=bracket(caseoption+) { xs } -(* FIXME: incongruous notation *) + +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: -| PLUS { Some true } -| empty { None } +| AT b=bracket(calloption) { Some b } +| { None } %inline do_repeat: | n=word? NOT { (`All, n) } 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. +