add tactic 'simplify if' performing if conversion

doc/tactics/simplify-if.rst

@@ -0,0 +1,139 @@
+========================================================================
+Tactic: `simplify if`
+========================================================================
+
+The `simplify if` transformation performs an if-conversion on program statements,
+i.e., it rewrites `if` statements into conditional expressions. This transformation
+preserves the program semantics.
+
+This conversion helps prevent the weakest precondition from growing exponentially
+with the number of `if` statements.
+
+To illustrate this issue, consider the following example, which shows how the
+weakest precondition can grow exponentially:
+
+.. ecproof::
+   :title: Weakest precondition grows exponentially.
+
+   require import AllCore.
+
+   module M = {
+     proc f (j:int) : int * int = {
+       var i, x, y;
+       x <- 0;
+       y <- 0;
+       i <- 0; 
+       while (i < 6) {
+         if (i = j) x <- i;
+         else y <- y + i;
+         i <- i + 1;
+       }
+       return (x, y);
+     } 
+   }.
+
+   hoare fP j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
+   proof.
+     proc.
+     unroll for ^while.
+     (*$*) time wp. (* The size of the condition grow exponentially in the value of the bound (here 6). *)
+     skip.
+     move => />. 
+     smt().
+   qed.
+
+Since the tactic preserves semantics, it can be applied to all program logics.
+
+.. admonition:: Syntax
+
+   `simplify if side? codepos?`
+
+The `side` argument is required when the goal is an `equiv` judgment; it specifies
+on which side the transformation should be applied.
+The `codepos` argument allows you to indicate which `if` statement the transformation
+should target.  
+
+.. contents::
+   :local:
+
+------------------------------------------------------------------------
+Variant: Transform at a given code possition 
+------------------------------------------------------------------------
+The tactic applies only if the branches of the selected `if` statement consist solely of
+assignments.
+
+.. ecproof::
+   :title: Hoare logic example selecting where to apply the transformation.
+
+   require import AllCore.
+
+   module M = {
+     proc f (j:int) : int * int = {
+       var i, x, y;
+       x <- 0;
+       y <- 0;
+       i <- 0; 
+       while (i < 6) {
+         if (i = j) x <- i;
+         else y <- y + i;
+         i <- i + 1;
+       }
+       return (x, y);
+     } 
+   }.
+
+   hoare fP_simplify2 j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
+   proof.
+     proc.
+     unroll for ^while.
+     (* You can select a particular occurence of if using codepos *)
+     (*$*) simplify if ^if. (* Apply the transformation on the first if *)
+     simplify if ^if{2}.  (* Apply the transformation on the second if *)
+     simplify if ^if{-2}. (* Apply the trnasformation of the penultimate if *)
+     time wp.  
+     skip.
+     move => />. 
+     smt().
+   qed.
+
+------------------------------------------------------------------------
+Variant: Transform as much as possible
+------------------------------------------------------------------------
+
+.. admonition:: Syntax
+
+  `simplify if`
+
+This variant attempts to find a position where the transformation can be applied and
+applies it. The process is repeated until no applicable position remains.
+
+.. ecproof::
+   :title: Hoare logic example.
+
+   require import AllCore.
+
+   module M = {
+     proc f (j:int) : int * int = {
+       var i, x, y;
+       x <- 0;
+       y <- 0;
+       i <- 0; 
+       while (i < 6) {
+         if (i = j) x <- i;
+         else y <- y + i;
+         i <- i + 1;
+       }
+       return (x, y);
+     } 
+   }.
+
+   hoare fP_simplify j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
+   proof.
+     proc.
+     unroll for ^while.
+     (*$*)simplify if. (* if instruction are transformed into single assignment *)
+     time wp.  (* The size of the wp is now linear in the number of instruction *)
+     skip.
+     move => />. 
+     smt().
+   qed.

examples/tactics/simplify_if.ec

@@ -0,0 +1,62 @@
+require import AllCore.
+
+module M = {
+  proc f (j:int) : int * int = {
+    var i, x, y;
+    x <- 0;
+    y <- 0;
+    i <- 0; 
+    while (i < 6) {
+      if (i = j) x <- i;
+      else y <- y + i;
+      i <- i + 1;
+    }
+    return (x, y);
+  } 
+}.
+
+hoare fP j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
+proof.
+  proc.
+  unroll for ^while.
+  time wp. (* The size of the condition grow exponentially in the value of the bound (here 6). *)
+  skip.
+  move => />. 
+  smt().
+qed.
+
+hoare fP_simplify j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
+proof.
+  proc.
+  unroll for ^while.
+  simplify if. (* if instruction are transformed into single assignment *)
+  time wp.  (* The size of the wp is now linear in the number of instruction *)
+  skip.
+  move => />. 
+  smt().
+qed.
+
+hoare fP_simplify2 j_: M.f : j = j_ ==> res = if 0 <= j_ < 6 then (j_, 15 - j_) else (0,15).
+proof.
+  proc.
+  unroll for ^while.
+  (* You can select a particular occurence of if using codepos *)
+  simplify if ^if. (* Apply the transformation on the first if *)
+  simplify if ^if{2}. (* Apply the transformation on the second if *)
+  simplify if ^if{-2}. (* Apply the trnasformation of the penultimate if *)
+  time wp.  
+  skip.
+  move => />. 
+  smt().
+qed.
+
+
+
+
+
+
+
+
+
+
+

flake.nix

@@ -107,7 +107,7 @@
           buildInputs =
               devPackages
            ++ [ pkgs.git scope'.why3 packages.provers ]
-           ++ (with pkgs.python3Packages; [ pyyaml ]);
+           ++ (with pkgs.python3Packages; [ pyyaml pip ]);
         };
       });
 }

src/ecHiTacticals.ml

@@ -194,6 +194,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pinterleave info          -> EcPhlSwap.process_interleave info
     | Pcfold info               -> EcPhlCodeTx.process_cfold info
     | Pkill info                -> EcPhlCodeTx.process_kill info
+    | PsimplifyIf info          -> EcPhlCodeTx.process_transform_if info
     | Pasgncase info            -> EcPhlCodeTx.process_case info
     | Palias info               -> EcPhlCodeTx.process_alias info
     | Pset info                 -> EcPhlCodeTx.process_set info
@@ -231,7 +232,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Prepl_stmt infos          -> EcPhlTrans.process_equiv_trans infos
     | Pprocrewrite (s, p, f)    -> EcPhlRewrite.process_rewrite s p f
     | Pprocrewriteat (x, f)     -> EcPhlRewrite.process_rewrite_at x f
-    | Pchangestmt (s, b, p, c)  -> EcPhlRewrite.process_change_stmt s b p c 
+    | Pchangestmt (s, b, p, c)  -> EcPhlRewrite.process_change_stmt s b p c
     | Prwprgm infos             -> EcPhlRwPrgm.process_rw_prgm infos
     | Phoaresplit               -> EcPhlHoare.process_hoaresplit
   in
@@ -246,7 +247,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
         | `Gap gap -> Format.fprintf fmt "%a" EcPrinting.(pp_codegap1 ppe) gap
         | `Instr i -> Format.fprintf fmt "%a" EcPrinting.(pp_codepos1 ppe) i
         ) is)
-          
+
 
 (* -------------------------------------------------------------------- *)
 and process_sub (ttenv : ttenv) tts tc =

src/ecLowPhlGoal.ml

@@ -789,7 +789,7 @@ let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s)
       ((me, Zpr.zip zpr, gs) : memenv * _ * form list)
   with InvalidCPos -> tc_error (fst cenv) "invalid code position"
 
-let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
+let t_code_transform (side : oside) cpos tr tx tc =
   let pf = FApi.tc1_penv tc in
 
   match side with
@@ -799,27 +799,32 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
       match concl.f_node with
       | FhoareS hs ->
           let pr, po = hs_pr hs, hs_po hs in
+          (* FIXME: This is very suspicious why only main is provided ? *)
           let po = po.hsi_inv.main in
           let (me, stmt, cs) =
             tx (pf, hyps) cpos (pr.inv, po) (hs.hs_m, hs.hs_s) in
           let concl =
-            f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs)
+            f_hoareS (snd me) pr stmt (hs_po hs)
           in
           FApi.xmutate1 tc (tr None) (cs @ [concl])
 
-      | FbdHoareS bhs when bdhoare ->
+      | FbdHoareS bhs ->
           let pr, po = bhs_pr bhs, bhs_po bhs in
           let (me, stmt, cs) =
             tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in
-          let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs)
-                      bhs.bhs_cmp (bhs_bd bhs) in
+          let concl = f_bdHoareS (snd me) pr stmt po bhs.bhs_cmp (bhs_bd bhs) in
+          FApi.xmutate1 tc (tr None) (cs @ [concl])
+
+      | FeHoareS ehs ->
+          let pr, po = ehs_pr ehs, ehs_po ehs in
+          let (me, stmt, cs) =
+            tx (pf, hyps) cpos (pr.inv, po.inv) (ehs.ehs_m, ehs.ehs_s) in
+          let concl = f_eHoareS (snd me) pr stmt po in
           FApi.xmutate1 tc (tr None) (cs @ [concl])
 
       | _ ->
         let kinds =
-            (if bdhoare then [`PHoare `Stmt] else [])
-          @ [`Hoare `Stmt] in
-
+            [`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt ] in
         tc_error_noXhl ~kinds:kinds pf
   end