feat(phl): add simplify if tactic

doc/tactics/simplify-if.rst

@@ -0,0 +1,142 @@
+========================================================================
+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 position
+------------------------------------------------------------------------
+
+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,51 @@
+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.

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

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
 

src/ecMatching.ml

@@ -68,7 +68,7 @@ module Position = struct
   *)
 
   (* Branch selection *)
-  type codepos_brsel    = [`Cond of bool | `Match of EcSymbols.symbol]
+  type codepos_brsel    = [`Cond of bool | `Match of EcSymbols.symbol | `MatchByPos of int]
   type nm_codepos_brsel = [`Cond of bool | `Match of int]
 
   (* Linear code position inside a block *)
@@ -354,21 +354,23 @@ module Position = struct
     try  List.findi (fun _ n -> EcSymbols.sym_equal sel n) cnames |> fst
     with Not_found -> raise InvalidCPos 
 
+  let select_match_arm on_error env e (br:codepos_brsel) =
+    match br with
+    | `Match ms -> select_match_arm_idx env e ms
+    | `MatchByPos ix -> ix
+    | _ -> on_error ()
+
   (* Get the block pointed to by brsel for a given instruction *)
   let normalize_brsel (env: env) (i: instr) (br: codepos_brsel) : (env * stmt) * nm_codepos_brsel =
     match i.i_node, br with
     | (Sif (_, t, _),  `Cond true)  -> (env, t), `Cond true
     | (Sif (_, _, f),  `Cond false) -> (env, f), `Cond false
     | (Swhile (_, s),  `Cond true)  -> (env, s), `Cond true
-    | (Smatch (e, ss), `Match ms)  -> 
-      let ix = select_match_arm_idx env e ms in
+    | (Smatch (e, ss), _)  ->
+      let ix = select_match_arm (fun _ -> assert false) env e br in
       let (locals, s) = List.at ss ix in
       let env = EcEnv.Var.bind_locals locals env in
-      begin try 
-        (env, s), `Match ix
-      with Invalid_argument _ -> 
-        raise InvalidCPos
-      end
+      (env, s), `Match ix
     | _ -> assert false
 
   let select_branch (env: env) (i: instr) (br: codepos_brsel) : stmt = 
@@ -515,6 +517,34 @@ module Position = struct
   let iter_blocks ~(start : nm_codegap1) ~(block_size : int) (s : stmt)
       (f : int -> nm_codegap1 -> nm_codegap1 -> unit) : unit =
     fold_blocks ~start ~block_size s (fun idx g1 g2 () -> f idx g1 g2) ()
+
+  let find_first_matching_instr (test : instr -> bool) (s : stmt) =
+    let exception Found of codepos in
+
+    let rec find_pos rpath n (s : instr list) =
+      match s with
+      | [] -> ()
+      | i :: s ->
+          if test i then raise (Found (List.rev rpath, cpos1 n));
+          find_pos_sub rpath n i;
+          find_pos rpath (n + 1) s
+
+    and find_pos_sub rpath n i =
+      match i.i_node with
+      | Sif (_, s1, s2) ->
+          find_pos ((cpos1 n, `Cond true ) :: rpath) 0 s1.s_node;
+          find_pos ((cpos1 n, `Cond false) :: rpath) 0 s2.s_node
+      | Swhile (_, s) ->
+          find_pos ((cpos1 n, `Cond true) :: rpath) 0 s.s_node
+      | Smatch (_, bs) ->
+          List.iteri (fun i (_, s) ->
+            find_pos ((cpos1 n, `MatchByPos i) :: rpath) 0 s.s_node
+          ) bs
+      | _ -> ()
+    in
+
+    try find_pos [] 0 s.s_node; None
+    with Found r -> Some r
 end
 
 (* -------------------------------------------------------------------- *)
@@ -572,8 +602,8 @@ module Zipper = struct
       | Sif (e, ifs1, ifs2), `Cond false ->
           (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), `Cond false, env
 
-      | Smatch (e, bs), `Match cn ->
-          let ix = select_match_arm_idx env e cn in
+      | Smatch (e, bs), _ ->
+          let ix = select_match_arm (fun () -> raise InvalidCPos) env e sub in
           let prebr, (locals, body), postbr = List.pivot_at ix bs in
           let env = EcEnv.Var.bind_locals locals env in
           (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), `Match ix, env

src/ecMatching.mli

@@ -31,7 +31,7 @@ module Position : sig
   ]
 
   (* Branch selection *)
-  type codepos_brsel  = [`Cond of bool | `Match of EcSymbols.symbol]
+  type codepos_brsel  = [`Cond of bool | `Match of EcSymbols.symbol | `MatchByPos of int]
   type nm_codepos_brsel = [`Cond of bool | `Match of int]
 
   (* Linear code position inside a block *)
@@ -218,6 +218,8 @@ module Position : sig
   val disjoint : nm_codegap1_range -> nm_codegap1_range -> bool
 
   val nm_codepos1_in_nm_codegap1_range : nm_codepos1 -> nm_codegap1_range -> bool
+
+  val find_first_matching_instr : (instr -> bool) -> stmt -> codepos option
 end
 
 (* -------------------------------------------------------------------- *)

src/ecParser.mly

@@ -3119,6 +3119,9 @@ direction:
 | ALIAS s=side? x=lident CEQ p=sform_h AT o=codepos
     { Psetmatch (s, o, x, p) }
 
+| SIMPLIFY IF s=side? o=codepos?
+    { PsimplifyIf (s, o) }
+
 | WEAKMEM s=side? h=loc(ipcore_name) p=param_decl
     { Pweakmem(s, h, p) }
 

src/ecParsetree.ml

@@ -802,6 +802,7 @@ type phltactic =
   | Poutline       of outline_info
   | Pinterleave    of interleave_info located
   | Pkill          of (oside * pcodepos * int option)
+  | PsimplifyIf    of (oside * pcodepos option)
   | Pasgncase      of (oside * pcodepos)
   | Prnd           of oside * psemrndpos option * rnd_tac_info_f
   | Prndsem        of bool * oside * pcodegap1

src/ecPrinting.ml

@@ -2470,7 +2470,8 @@ let pp_codepos_brsel (fmt: Format.formatter) (br: CP.codepos_brsel) =
   (match br with
   | `Cond true -> "."
   | `Cond false -> "?"
-  | `Match cp -> Format.sprintf "#%s." cp)
+  | `Match cp -> Format.sprintf "#%s." cp
+  | `MatchByPos ix -> Format.sprintf "#%i" ix)
 
 let pp_codepos_step (ppe: PPEnv.t) (fmt: Format.formatter) ((cp, br): CP.codepos_step) = 
   Format.fprintf fmt "%a%a" (pp_codepos1 ppe) cp pp_codepos_brsel br