PR: Allow symbolic assignments for cfold

doc/tactics/cfold.rst

@@ -0,0 +1,123 @@
+
+========================================================================
+Tactic: `cfold`
+========================================================================
+
+The `cfold`` tactic is part of the family of tactics that operate by 
+rewriting the program into a semantically equivalent form. 
+More concretely, given an assignment of the form::
+
+  a <- b;
+
+the tactic propagates this (known) values of a through the program 
+and inlining this (known) value whenever ``a`` would be used.
+
+For example, the following excerpt::
+
+  a <- 3;
+  c <- a + 1;
+  a <- a + 2;
+  b <- a; 
+
+would be converted into::
+
+  c <- 4; (* 3 + 1 *)
+  b <- 5; (* a = 3 + 2 = 5 at this point *)
+  a <- 5; (* we need to make sure a has the
+             correct value at the end of execution *)
+
+.. contents::
+   :local:
+
+------------------------------------------------------------------------
+Syntax
+------------------------------------------------------------------------
+
+The general form of the tactic is:
+
+.. admonition:: Syntax
+
+   ``cfold {side}? {codepos} {n}?``
+
+Where:
+
+- ``{side}`` is optional and only applicable in relational goals
+  to specify on which of the two programs the tactic is to be applied.
+
+- ``{codepos}`` specifies the instruction on which the tactic will begin.
+  The tactic will proceed to propagate the assignment as far as possible,
+  even through other assignments to the same variable as long as it can or 
+  until it reaches the line limit (if given).
+
+- ``{n}`` is an optional integer argument corresponding to the number of 
+  lines of the program to process in the folding. This serves to limit the 
+  scope of the tactic application and prevent it from acting in the whole 
+  program when this would not be desirable.
+
+.. ecproof::
+   :title: Cfold example
+
+   require import AllCore.
+
+   module M = {
+     proc f(a : int) = {
+       var x, y : int;
+
+       x <- a + 1;
+       y <- 2 * x;
+       x <- 3 * y;
+
+       return x;
+     }
+   }.
+
+   lemma L : hoare[M.f : witness a ==> witness res].
+   proof.
+     proc.
+     (*$*) cfold 1.
+
+     (* The goal is the same but the program is now rewritten *)
+     admit.
+   qed.
+
+
+The propagated variable is then set at the end of the part of the program 
+where the tactic was applied (in this case, the end of the program, since
+the tactic applied to its entirety), and it is set to the value which the 
+tactic accumulated.
+
+Here is an example of using the parameter ``{n}`` for limiting tactic 
+application:
+
+.. ecproof::
+   :title: Cfold line restriction 
+
+   require import AllCore.
+
+   module M = {
+     proc f() = {
+       var x, y : int;
+       var i : int;
+
+       i <- 0;
+
+       while (i < 10) {
+         x <- i + 1;
+         y <- 2 * x;
+         x <- 3 * y;
+         i <- i + 1;
+       }
+
+       return x;
+     }
+   }.
+
+   lemma L : hoare[M.f : witness ==> witness res].
+   proof.
+     proc.
+
+     unroll for 2.
+     (*$*) cfold 1 27.
+     (* The goal is the same but the program is now rewritten *)
+     admit.
+   qed.

src/ecPV.ml

@@ -111,6 +111,8 @@ module Mpv = struct
       check_glob env mp m;
       raise Not_found
 
+  let pvs { s_pv } = s_pv
+
   type esubst = (expr, unit) t
 
   let rec esubst env (s : esubst) e =

src/ecPV.mli

@@ -53,10 +53,12 @@ module Mpv : sig
 
   val find_glob : env -> mpath -> ('a,'b) t -> 'b
 
-  val esubst : env -> (expr, unit) t -> expr -> expr 
+  val pvs : ('a,'b) t -> 'a Mnpv.t
+
+  val esubst  : env -> (expr, unit) t -> expr -> expr 
   val issubst : env -> (expr, unit) t -> instr list -> instr list
-  val isubst : env -> (expr, unit) t -> instr -> instr 
-  val ssubst : env -> (expr, unit) t -> stmt -> stmt
+  val isubst  : env -> (expr, unit) t -> instr -> instr 
+  val ssubst  : env -> (expr, unit) t -> stmt -> stmt
 end
 
 (* -------------------------------------------------------------------- *)

src/phl/ecPhlCodeTx.ml

@@ -196,19 +196,23 @@ let cfold_stmt ?(simplify = true) (pf, hyps) (me : memenv) (olen : int option) (
       e
     ) else identity in
 
-  let is_const_expression (e : expr) =
-    PV.is_empty (e_read env e) in
-
   let for_instruction ((subst as subst0) : (expr, unit) Mpv.t) (i : instr) =
     let wr = EcPV.i_write env i in
     let i = Mpv.isubst env subst i in
 
     let (subst, asgn) =
-      List.fold_left_map (fun subst ((pv, _) as pvty) ->
-        match Mpv.find env pv subst with
-        | e -> Mpv.remove env pv subst, Some (pvty, e)
-        | exception Not_found -> subst, None
-      ) subst (fst (PV.elements wr)) in
+      List.fold_left_map (fun subst (pv, e) ->
+        let exception Remove in
+
+        try
+          if PV.mem_pv env pv wr then raise Remove;
+          let rd = EcPV.e_read env e in
+          if PV.mem_pv env pv rd then raise Remove;
+          subst, None
+
+        with Remove ->
+          Mpv.remove env pv subst, Some ((pv, e.e_ty), e)
+      ) subst (EcPV.Mnpv.bindings (Mpv.pvs subst)) in
 
     let asgn = List.filter_map identity asgn in
 
@@ -227,7 +231,7 @@ let cfold_stmt ?(simplify = true) (pf, hyps) (me : memenv) (olen : int option) (
         try
           match i.i_node with
           | Sasgn (lv, e) ->
-            (* We already removed the variables of `lv` from the substitution *)
+            (* We already removed the variables of `lv` & the rhs from the substitution *)
             (* We are only interested in the variables of `lv` that are in `wr` *)
             let es =
               match simplify e, lv with
@@ -237,8 +241,8 @@ let cfold_stmt ?(simplify = true) (pf, hyps) (me : memenv) (olen : int option) (
 
             let lv = lv_to_ty_list lv in
 
-            let tosubst, asgn2 = List.partition (fun ((pv, _), e) ->
-              Mpv.mem env pv subst0 && is_const_expression e
+            let tosubst, asgn2 = List.partition (fun ((pv, _), _) ->
+              Mpv.mem env pv subst0
             ) (List.combine lv es) in
 
             let subst =
@@ -292,9 +296,6 @@ let cfold_stmt ?(simplify = true) (pf, hyps) (me : memenv) (olen : int option) (
         | e, _ -> [e] in
       let lv = lv_to_ty_list lv in
 
-      if not (List.for_all is_const_expression es) then
-        tc_error pf "right-values are not closed expressions";
-
       if not (List.for_all (is_loc -| fst) lv) then
         tc_error pf "left-values must be made of local variables only";
 

tests/cfold.ec

@@ -111,3 +111,21 @@ theory CfoldWhileUnroll.
   by auto => />.
   qed.
 end CfoldWhileUnroll.
+
+module CfoldSymbolic = {
+  proc f(a : int) = {
+    var x, y : int;
+
+    x <- a + 1;
+    y <- 2 * x;
+    x <- 3 * y;
+
+    return x;
+  }
+}.
+
+lemma L : hoare[CfoldSymbolic.f : witness a ==> witness res].
+proof.
+proc.
+cfold 1.
+abort.