Add support for cfold of symbolic assignments

Co-authored-by: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>

Author: Gustavo2622

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.