From bfb153137cb8f4e592563fcc69e4e199584fe9d4 Mon Sep 17 00:00:00 2001 From: Gustavo2622 Date: Tue, 10 Feb 2026 15:58:03 +0000 Subject: [PATCH] Add support for cfold of symbolic assignments Co-authored-by: Pierre-Yves Strub --- doc/tactics/cfold.rst | 123 +++++++++++++++++++++++++++++++++++++++++ src/ecPV.ml | 2 + src/ecPV.mli | 8 ++- src/phl/ecPhlCodeTx.ml | 29 +++++----- tests/cfold.ec | 18 ++++++ 5 files changed, 163 insertions(+), 17 deletions(-) create mode 100644 doc/tactics/cfold.rst diff --git a/doc/tactics/cfold.rst b/doc/tactics/cfold.rst new file mode 100644 index 0000000000..9fced8007e --- /dev/null +++ b/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. diff --git a/src/ecPV.ml b/src/ecPV.ml index f2fb14ad06..ed6d2a6433 100644 --- a/src/ecPV.ml +++ b/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 = diff --git a/src/ecPV.mli b/src/ecPV.mli index 6821864cc3..0e9df4354b 100644 --- a/src/ecPV.mli +++ b/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 (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index 4f2bb1469e..2968953af1 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/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"; diff --git a/tests/cfold.ec b/tests/cfold.ec index f0edc8a5a3..3d6d435623 100644 --- a/tests/cfold.ec +++ b/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.