New tactic: rewrite equiv

The main idea is to provide a way to rewrite a procedure call, somewhere
in a program, into a different procedure call, using an equiv.

There is a variant provided to handle cases where the function to be
rewritten to has different arguments and/or left-value than the instance
provided.

Syntax and variants:

 - Same arguments:
   `rewrite equiv[{m} p d lem]`

 - Different arguments:
   `rewrite equiv[{m} p d lem (a1, a2, ... :@ lv?)]`

with

 - `m`: 1 or 2
 - `p`: code position
 - `d`: direction, either `-` or nothing
 - `lem`: equiv for the rewrite
 - `ai`: an expression representing a function argument
 - `lv`: a left-value

For example usage see: `tests/rwequiv.ec` or instances in the stdlib.

examples/ChaChaPoly/chacha_poly.ec

@@ -1130,8 +1130,7 @@ section PROOFS.
       + by proc; inline *; auto => /> &2; case: (p{2}).
       + by proc; auto.
       by auto; conseq (_: ={RO.m}) => //; sim.
-    transitivity*{1} { r <@ G3(GenChaChaPoly(OCC(IFinRO))).main(); } => //;1:smt().
-    + by symmetry; call (CCP_OCCP IFinRO G3).
+    rewrite equiv[{1} 1 -(CCP_OCCP IFinRO G3)].
     inline *; sim (_: ={Mem.lc, Mem.log, Mem.k} /\ OCC.gs{1} = RO.m{2}).
     proc; inline *;auto.
   qed.

examples/Dice4_6.ec

@@ -69,12 +69,11 @@ transitivity D4.sample (true ==> res{1} = finv res{2})
     by apply: dinter_uni; rewrite supp_dinter /#.
   by rewrite !supp_dinter /#.
 proc *.
-rewrite equiv [{1} D4_Sample () r () r].
-rewrite equiv [{1} D4_6.sampleE_sampleWi () r ((), 5) r].
-+ by auto=> />; exact: dinter_ll.
-rewrite equiv [{2} D6_Sample () r ((), 5) r]; sim.
+rewrite equiv[{1} 1 D4_Sample].
+rewrite equiv[{1} 1 D4_6.sampleE_sampleWi ((), 5 :@ r)].
++ by auto; rewrite dinter_ll.
+rewrite equiv[{1} 1 -D6_Sample ( :@ r)]; sim.
 qed.
-
 lemma prD6 : forall k &m, Pr[D6.sample() @ &m : res = k] =
       if 1 <= k <= 4 then 1%r/4%r else 0%r.
 proof.

examples/MEE-CBC/CBC.eca

@@ -187,9 +187,9 @@ section Random_Ideal.
   equiv Random_Ideal: Random.enc ~ Ideal.enc: size p{1} = size p{2} ==> ={res}.
   proof.
   proc.
-  rewrite equiv [{2} Sampling.Sample_LoopSnoc_eq (size p + 1)  r (size p + 1) c].
-  + auto=> /#.
-  by wp; while (i0{1} = i{2} /\ c{2} = l{1} /\ size p{2} + 1 = n{1}); auto=> /#.
+  outline {2} [1] { r <@ Sampling.Sample.sample(size p + 1); }.
+  rewrite equiv[{2} 1 Sampling.Sample_LoopSnoc_eq].
+  by inline; wp; while (={i} /\ c{1} = l{2} /\ size p{1} + 1 = n{2}); auto=> /#.
   qed.
 end section Random_Ideal.
 

src/ecHiGoal.ml

@@ -855,192 +855,6 @@ let process_rewrite1_r ttenv ?target ri tc =
   | RWTactic `Field ->
       process_algebra `Solve `Field [] tc
 
-  | RWEquiv (side, name, (argsl, resl), (argsr, resr)) ->
-      (* Check which direction we wish to go in *)
-      let tc = match side with
-        | `Left  -> tc
-        | `Right -> as_tcenv1 (EcPhlSym.t_equiv_sym tc)
-      in
-
-      (* Extract the context *)
-      let env, hyps, goal = FApi.tc1_eflat tc in
-      let goal = EcFol.destr_equivS goal in
-
-      (* Get the symbol of name and retrieve it's equiv *)
-      let sym_of_name = string_of_qsymbol (unloc name) in
-      let equiv =
-        let f =
-          (* Check if the name is in the local context *)
-          if LDecl.hyp_exists sym_of_name hyps then
-            let _, f = LDecl.hyp_by_name sym_of_name hyps in
-            f
-          else
-            let _, lem = EcEnv.Ax.lookup (unloc name) env in
-            assert (List.is_empty lem.ax_tparams);
-            lem.ax_spec
-        in
-        (* TODO: how do we handle errors? *)
-        try EcFol.destr_equivF f with
-          | DestrError _ -> raise (LowRewrite.RewriteError LRW_NothingToRewrite)
-      in
-      (* Type our res and args in the given memory *)
-      let sided_env m (p : EcModules.function_) args res =
-        let subenv = EcEnv.Memory.push_active m env in
-        let ue = EcUnify.UniEnv.create (Some []) in
-
-        let args, ret_ty =
-          EcTyping.trans_args subenv ue (loc args) p.f_sig (unloc args) in
-        let res =
-          EcTyping.transexpcast subenv `InProc ue ret_ty res in
-
-        let subs = try EcUnify.UniEnv.close ue with
-          | EcUnify.UninstanciateUni ->
-            EcTyping.tyerror ri.pl_loc env EcTyping.FreeTypeVariables in
-
-        let sty = f_subst_init ~tu:subs () in
-        let es = e_subst sty in
-        (List.map es args, es res)
-      in
-
-      (* Construct a left value from an expression *)
-      let lv res =
-        let as_pvar e =
-          match e.e_node with
-          | Evar pv -> (pv, e_ty e)
-          | _ -> assert false in
-
-        match res.e_node with
-        | Evar pv ->
-          LvVar (pv, e_ty res)
-        | Etuple pvs ->
-          LvTuple (List.map as_pvar pvs)
-        | _ -> assert false
-      in
-
-      let meml = goal.es_ml in
-      let procl = EcEnv.Fun.by_xpath equiv.ef_fl env in
-      let argsl, resl = sided_env meml procl argsl resl in
-      let lvl = lv resl in
-
-      let memr = goal.es_mr in
-      let procr = EcEnv.Fun.by_xpath equiv.ef_fr env in
-      let argsr, resr = sided_env memr procr argsr resr in
-      let lvr = lv resr in
-
-      (* Construct minimal pre/post conditions for the new intermediate memory *)
-      (* Note: this only allows overwriting existing memories instead of creating new ones *)
-      let prpo ml mr args =
-        (* Extract the conjuncts of the pre-condition that are specific to the left memory *)
-        let ml_pr = split_sided ml goal.es_pr in
-        let ml_pr = odfl f_true ml_pr in
-
-        let eq_args =
-          f_eq
-            (EcFol.form_of_expr ml (e_tuple args))
-            (EcFol.form_of_expr mr (e_tuple args)) in
-
-        (* Extract all used variables from the pre/post conditions *)
-        let eqs_pr = EcFol.one_sided_vs ml (f_and goal.es_pr eq_args) in
-        let eqs_po = EcFol.one_sided_vs ml goal.es_po in
-
-        (* Construct equalities between variables in the left memory and the intermediate memory *)
-        let eqs_pr = List.unique (eqs_pr @ eqs_po) in
-        let eqs_pr = List.map (fun v -> f_eq (Fsubst.f_subst_mem ml mr v) v) eqs_pr in
-        let eqs_pr = f_ands eqs_pr in
-
-        let eqs_po = List.unique eqs_po in
-        let eqs_po = List.map (fun v -> f_eq (Fsubst.f_subst_mem ml mr v) v) eqs_po in
-        let eqs_po = f_ands eqs_po in
-
-        f_and eqs_pr (f_and eq_args ml_pr) , eqs_po
-      in
-
-      (* Construct the proc calls that we want in each transitivity *)
-      let progl = EcModules.s_call (Some lvl, equiv.ef_fl, argsl) in
-      let progr = EcModules.s_call (Some lvr, equiv.ef_fr, argsr) in
-
-      (* Here we build the chain of transitivity calls, and discharge intermediate goals when possible*)
-      let tc =
-        EcPhlTrans.t_equivS_trans
-           (EcMemory.memtype meml, progl)
-           (prpo (EcMemory.memory meml) mright argsl)
-           (goal.es_pr, goal.es_po)
-           tc in
-      let p = process_tfocus tc (Some [Some 4,Some 4], None) in
-      let tc =
-        t_onselect
-          p
-          (EcPhlTrans.t_equivS_trans
-             (EcMemory.memtype memr, progr)
-             (goal.es_pr, goal.es_po)
-             (prpo (EcMemory.memory memr) mleft argsr))
-          tc in
-
-      (* Two more goals (1 and 4) can be solved in general (with the same proof):
-          - by move=> &1 &2 H; exists var1{1} var2{1} ... varn{1}; move: H => //.
-          for 4 we use {2}.
-      *)
-      let tc =
-        let ongoal (b : bool) (tc : tcenv1) =
-          let pl = EcIdent.create "&p1" in
-          let pr = EcIdent.create "&p2" in
-          let h  = EcIdent.create "__" in
-          let tc = t_intros_i_1 [pl; pr; h] tc in
-
-          let mem, p = if b then (meml, pl) else (memr, pr) in
-
-          let goal = FApi.tc1_goal tc in
-
-          let tc =
-            if EcFol.is_exists goal then
-              (* Pairing up the correct variables for the exists intro *)
-              let vs, fm = EcFol.destr_exists (FApi.tc1_goal tc) in
-              let eqsprfm, _ =
-                let l, r = EcFol.destr_and fm in
-                if b then l, r else r, l
-              in
-              let eqsfm, _ = destr_and eqsprfm in
-              let eqsfm = destr_ands ~deep:false eqsfm in
-              let eqsmp = List.map destr_eq eqsfm in
-              let eqsmp = List.map (fst_map destr_local) eqsmp in
-              let exvs = List.map (fun v -> List.assoc v eqsmp) (List.fst vs) in
-              let exvs = List.map (Fsubst.f_subst_mem (EcMemory.memory mem) p) exvs in
-
-              FApi.as_tcenv1 (t_exists_intro_s (List.map paformula exvs) tc)
-            else
-              tc
-          in
-
-          t_generalize_hyp ?clear:(Some `Yes) h tc
-        in
-
-        t_onselecti
-          (fun _ -> true)
-          (function 0 -> ongoal true | 3 -> ongoal false | _ -> t_id)
-          tc
-      in
-
-      let p = process_tfocus tc (Some [Some 6,Some 6], None) in
-      let pterm =
-        { fp_mode = `Implicit;
-          fp_head = FPNamed (name, None);
-          fp_args = []; } in
-      let tc =
-        t_onselect
-          p
-          (t_seq (EcPhlCall.process_call None pterm) EcPhlAuto.t_auto)
-          tc in
-
-      let p = process_tfocus tc (Some [Some 3, Some 3; Some (-1), Some (-1)], None) in
-      let tc =
-        t_onselect
-          p
-          (t_seq (EcPhlInline.process_inline (`ByName (None, None, ([], None)))) ((t_try (t_seq EcPhlAuto.t_auto process_done))))
-          tc
-      in
-
-      t_onall process_trivial tc
-
 (* -------------------------------------------------------------------- *)
 let process_rewrite1 ttenv ?target ri tc =
   EcCoreGoal.reloc (loc ri) (process_rewrite1_r ttenv ?target ri) tc

src/ecHiTacticals.ml

@@ -214,6 +214,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pprbounded                -> EcPhlPr.t_prbounded true
     | Psim (cm, info)           -> EcPhlEqobs.process_eqobs_in cm info
     | Ptrans_stmt info          -> EcPhlTrans.process_equiv_trans info
+    | Prw_equiv info            -> EcPhlRwEquiv.process_rewrite_equiv info
     | Psymmetry                 -> EcPhlSym.t_equiv_sym
     | Peager_seq infos          -> curry3 EcPhlEager.process_seq infos
     | Peager_if                 -> EcPhlEager.process_if