feat: variant for up-to-bad call/proc tactics

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 6534f3d (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`

Author: loutr

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

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) }

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)

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

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

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 =

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