From 30bfa950afa3806948c073d3c9ec4468d33ea940 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Mon, 11 Dec 2023 11:58:49 +0100
Subject: [PATCH] New tactic: "proc change"

This tactic allows to change an expression in a statement by some
other expression. When applied, the user has to prove that the two
expressions are equal (generalizing over all the program variables)

This tactic applies to any program logic.

The syntax is:

    proc change <side?> <codepos> : <form>

This tactic is in the TCB.

Test plan:

 - unit test (tests/prochange.ec)
---
 src/ecHiTacticals.ml     |  1 +
 src/ecParser.mly         |  3 +++
 src/ecParsetree.ml       |  1 +
 src/phl/ecPhlRewrite.ml  | 43 ++++++++++++++++++++++++++++++++++++++++
 src/phl/ecPhlRewrite.mli |  6 ++++++
 tests/procchange.ec      | 14 +++++++++++++
 6 files changed, 68 insertions(+)
 create mode 100644 src/phl/ecPhlRewrite.ml
 create mode 100644 src/phl/ecPhlRewrite.mli
 create mode 100644 tests/procchange.ec

diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
index 01a8b64b29..bf955ece95 100644
--- a/src/ecHiTacticals.ml
+++ b/src/ecHiTacticals.ml
@@ -227,6 +227,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pauto                     -> EcPhlAuto.t_auto ~conv:`Conv
     | Plossless                 -> EcPhlHiAuto.t_lossless
     | Prepl_stmt infos          -> EcPhlTrans.process_equiv_trans infos
+    | Pprocchange (s, p, f)     -> EcPhlRewrite.process_change s p f
   in
 
   try  tx tc
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 80c45b123d..2fed133d40 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -3233,6 +3233,9 @@ phltactic:
 | LOSSLESS
     { Plossless }
 
+| PROC CHANGE side=side? pos=codepos COLON f=sform
+    { Pprocchange (side, pos, f) }
+
 bdhoare_split:
 | b1=sform b2=sform b3=sform?
     { BDH_split_bop (b1,b2,b3) }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 32868eb6b8..95af725e7c 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -749,6 +749,7 @@ type phltactic =
   | Prw_equiv      of rw_eqv_info
   | Psymmetry
   | Pbdhoare_split of bdh_split
+  | Pprocchange    of side option * codepos * pformula
 
     (* Eager *)
   | Peager_seq       of (eager_info * codepos1 pair * pformula)
diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml
new file mode 100644
index 0000000000..4c4dd5cb8b
--- /dev/null
+++ b/src/phl/ecPhlRewrite.ml
@@ -0,0 +1,43 @@
+(* -------------------------------------------------------------------- *)
+open EcParsetree
+open EcAst
+open EcCoreGoal
+open EcModules
+open EcFol
+
+(* -------------------------------------------------------------------- *)
+let process_change
+    (side : side option)
+    (pos  : codepos)
+    (form : pformula)
+    (tc   : tcenv1)
+=
+  let concl = FApi.tc1_goal tc in
+
+  let change i =
+    let (e, mk) =
+      match i.i_node with
+      | Sasgn (lv, e) -> (e, (fun e -> i_asgn (lv, e)))
+      | Srnd  (lv, e) -> (e, (fun e -> i_rnd  (lv, e)))
+      | _             -> assert false in
+
+    let m, e' = EcProofTyping.tc1_process_Xhl_form ?side tc e.e_ty form in
+    let mid = EcMemory.memory m in
+    let e' = expr_of_form mid e' in
+
+    let f  = form_of_expr mid e in
+    let f' = form_of_expr mid e' in
+
+    ([f_forall_mems [m] (f_eq f f')], [mk e'])
+  in
+
+  let kinds = [`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] in
+
+  if not (EcLowPhlGoal.is_program_logic concl kinds) then
+    assert false;
+
+  let s = EcLowPhlGoal.tc1_get_stmt side tc in
+  let goals, s = EcMatching.Zipper.map pos change s in
+  let concl = EcLowPhlGoal.hl_set_stmt side concl s in
+
+  FApi.xmutate1 tc `ProcChange (goals @ [concl])
diff --git a/src/phl/ecPhlRewrite.mli b/src/phl/ecPhlRewrite.mli
new file mode 100644
index 0000000000..d74d849096
--- /dev/null
+++ b/src/phl/ecPhlRewrite.mli
@@ -0,0 +1,6 @@
+(* -------------------------------------------------------------------- *)
+open EcParsetree
+open EcCoreGoal.FApi
+
+(* -------------------------------------------------------------------- *)
+val process_change : side option -> codepos -> pformula -> backward
diff --git a/tests/procchange.ec b/tests/procchange.ec
new file mode 100644
index 0000000000..90d4fdf2bd
--- /dev/null
+++ b/tests/procchange.ec
@@ -0,0 +1,14 @@
+require import AllCore.
+
+module M = {
+  proc f(x : int) = {
+    x <- x + 0;
+  }
+}.
+
+lemma L : equiv[M.f ~ M.f : true ==> true].
+proof.
+proc.
+proc change {1} 1 : x.
+- smt().
+abort.