From d83b2c7b8dfb19955ffba369593ab001c61f623b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 25 Mar 2026 18:09:07 +0100 Subject: [PATCH] Tighten proc-change observability Restrict proc-change local postconditions to variables observable from the continuation or the goal post, instead of equating all writes from the replaced fragment. --- src/ecLowPhlGoal.ml | 13 ++ src/ecPV.ml | 43 +++++++ src/ecPV.mli | 9 ++ src/phl/ecPhlRewrite.ml | 72 +++++------ tests/procchange.ec | 261 +++++++++++++++++++++++++++++++++++----- 5 files changed, 323 insertions(+), 75 deletions(-) diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 6daabbfd6..07bc36471 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -365,6 +365,19 @@ let logicS_read (env : env) (f : logicS) = | `Equiv hs -> equivS_read env hs | `EHoare hs -> eHoareS_read env hs +let logicS_post_read (env : env) (f : logicS) = + let add pvs inv = EcPV.form_read env pvs inv in + + match f with + | `Hoare hs -> + POE.fold add EcPV.PMVS.empty (hs_po hs).hsi_inv + | `EHoare hs -> + add EcPV.PMVS.empty (ehs_po hs).inv + | `BdHoare hs -> + add (add EcPV.PMVS.empty (bhs_po hs).inv) (bhs_bd hs).inv + | `Equiv es -> + add EcPV.PMVS.empty (es_po es).inv + (* -------------------------------------------------------------------- *) exception InvalidSplit of codepos1 diff --git a/src/ecPV.ml b/src/ecPV.ml index 590ab1a2e..a9ffeb67e 100644 --- a/src/ecPV.ml +++ b/src/ecPV.ml @@ -7,6 +7,7 @@ open EcTypes open EcModules open EcFol open EcEnv +open EcMatching (* -------------------------------------------------------------------- *) type alias_clash = @@ -630,6 +631,48 @@ let is_read env is = is_read_r env PV.empty is let s_read env s = s_read_r env PV.empty s let f_read env f = f_read_r env PV.empty f +(* -------------------------------------------------------------------- *) +let zpr_pv (kind : [ `Read | `Write ]) (span : [ `Before | `After ]) (env : env) = + let pv_of_stmt = + match kind with + | `Read -> is_read_r + | `Write -> is_write_r ?except:None + in + + let rec doit (ctxt : instr option) (pvs : PV.t) (zpr : Zipper.spath) = + let (head, tail), ipath = zpr in + let stail = List.ocons ctxt tail in + let s = stmt (List.rev_append head stail) in + + let pvs = + let s = match span with `Before -> head | `After -> tail in + pv_of_stmt env pvs s in + + let parent, pvs = + match ipath with + | Zipper.ZTop -> + None, pvs + + | Zipper.ZIfThen (e, ps, se) -> + Some (ps, i_if (e, s, se)), pvs + + | Zipper.ZIfElse (e, st, ps) -> + Some (ps, i_if (e, st, s)), pvs + + | Zipper.ZMatch (e, ps, mpi) -> + let bs = + List.rev_append mpi.prebr ((mpi.locals, s) :: mpi.postbr) + in Some (ps, i_match (e, bs)), pvs + + | Zipper.ZWhile (e, ps) -> + let wi = i_while (e, s) in + Some (ps, wi), pv_of_stmt env pvs [wi] + in + + ofold (fun (zpr, ctxt) pvs -> doit (Some ctxt) pvs zpr) pvs parent + + in fun pvs zpr -> doit None pvs zpr + (* -------------------------------------------------------------------- *) type pmvs = PV.t Mid.t diff --git a/src/ecPV.mli b/src/ecPV.mli index ac1e64cbb..fe5d269fe 100644 --- a/src/ecPV.mli +++ b/src/ecPV.mli @@ -148,6 +148,15 @@ val is_read : instr list pvaccess0 val s_read : stmt pvaccess0 val f_read : xpath pvaccess0 +(* -------------------------------------------------------------------- *) +val zpr_pv : + [ `Read | `Write ] + -> [ `Before | `After ] + -> env + -> PV.t + -> EcMatching.Zipper.spath + -> PV.t + (* -------------------------------------------------------------------- *) type pmvs = PV.t EcIdent.Mid.t diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml index 331d1c947..b12461179 100644 --- a/src/phl/ecPhlRewrite.ml +++ b/src/phl/ecPhlRewrite.ml @@ -6,7 +6,6 @@ open EcCoreGoal open EcEnv open EcModules open EcFol -open EcMatching module L = EcLocation module PT = EcProofTerm @@ -230,44 +229,11 @@ let process_rewrite_at EcPhlConseq.t_conseq pre post tc |> FApi.t_sub [t_pre; t_post; EcLowGoal.t_id] -(* -------------------------------------------------------------------- *) -let zpr_write (env : env) = - let rec doit (ctxt : instr option) (pvs : EcPV.PV.t) (zpr : Zipper.spath) = - let (head, tail), ipath = zpr in - let tail = List.ocons ctxt tail in - let s = stmt (List.rev_append head tail) in - - let pvs = EcPV.is_write_r env pvs head in - - let parent, pvs = - match ipath with - | Zipper.ZTop -> - None, pvs - - | Zipper.ZIfThen (e, ps, se) -> - Some (ps, i_if (e, s, se)), pvs - - | Zipper.ZIfElse (e, st, ps) -> - Some (ps, i_if (e, st, s)), pvs - - | Zipper.ZMatch (e, ps, mpi) -> - let bs = - List.rev_append mpi.prebr ((mpi.locals, s) :: mpi.postbr) - in Some (ps, i_match (e, bs)), pvs - - | Zipper.ZWhile (e, ps) -> - Some (ps, i_while (e, s)), EcPV.is_write_r env pvs tail - in - - ofold (fun (zpr, ctxt) pvs -> doit (Some ctxt) pvs zpr) pvs parent - - in fun pvs zpr -> doit None pvs zpr - (* -------------------------------------------------------------------- *) (* [change] replaces a code range with [s] by generating: - a local equivalence goal showing that the original fragment and [s] agree under the framed precondition on the variables they both read, - and produce the same values for everything they may write; + and produce the same values for everything observable afterwards; - the original program-logic goal with the selected range rewritten. *) let t_change_stmt (side : side option) @@ -284,9 +250,9 @@ let t_change_stmt (* Collect the variables that may be modified by the surrounding context, excluding the fragment being replaced. *) let modi = - let zpr = - (zpr.z_head, List.drop (List.length stmt) zpr.z_tail), zpr.z_path - in zpr_write env EcPV.PV.empty zpr in + let zpr = { zpr with z_tail = epilog } in + let zpr = (zpr.z_head, zpr.z_tail), zpr.z_path in + EcPV.zpr_pv `Write `Before env EcPV.PV.empty zpr in (* Keep only the top-level conjuncts of the current precondition that talk about the active memory and are independent from the surrounding writes. *) @@ -307,8 +273,26 @@ let t_change_stmt let written = EcPV.is_write_r env written stmt in let written = EcPV.is_write_r env written s.s_node in + let obs = + let zpr = { zpr with z_tail = epilog } in + let zpr = (zpr.z_head, zpr.z_tail), zpr.z_path in + let obs = EcPV.zpr_pv `Read `After env EcPV.PV.empty zpr in + + let goal = + let pvs = + EcLowPhlGoal.logicS_post_read env + (EcLowPhlGoal.get_logicS (FApi.tc1_goal tc)) + in + EcIdent.Mid.find_def EcPV.PV.empty (fst me) pvs + in + + EcPV.PV.union obs goal + in + + let written = EcPV.PV.inter written obs in + (* The local equivalence goal relates shared reads in the precondition and - all possible writes in the postcondition. *) + the writes that remain observable in the continuation/postcondition. *) let wr_pvs, wr_globs = EcPV.PV.elements written in let pr_pvs, pr_globs = EcPV.PV.elements @@ EcPV.PV.inter @@ -337,11 +321,11 @@ let t_change_stmt (* First subgoal: prove that the replacement fragment preserves the observable behavior required by the outer proof. *) let goal1 = - f_equivS - (snd me) (snd me) - { ml; mr; inv = ofold f_and (f_ands pr_eq) frame; } - (EcAst.stmt stmt) s - { ml; mr; inv = f_ands po_eq; } + f_equivS + (snd me) (snd me) + { ml; mr; inv = ofold f_and (f_ands pr_eq) frame; } + (EcAst.stmt stmt) s + { ml; mr; inv = f_ands po_eq; } in let stmt = EcMatching.Zipper.zip { zpr with z_tail = s.s_node @ epilog } in diff --git a/tests/procchange.ec b/tests/procchange.ec index 25eb8f40a..f656c52da 100644 --- a/tests/procchange.ec +++ b/tests/procchange.ec @@ -264,12 +264,12 @@ theory ProcChangeFrameTest. lemma L : hoare[M.f : x = 3 ==> true]. proof. - proc. - simplify. + proc=> /=. proc change 2 : { x <- 4; }; by auto. -qed. + qed. +end ProcChangeFrameTest. (* -------------------------------------------------------------------- *) (* Negative flat case: change statement 3 (x <- x + 1 → x <- 4) fails. @@ -281,18 +281,18 @@ theory ProcChangeFrameFailTest. y <- 0; x <- 4; x <- x + 1; + return x; } }. - lemma L : hoare[M.f : x = 3 ==> true]. + lemma L : hoare[M.f : x = 3 ==> res = 0]. proof. - proc. - simplify. + proc=> /=. fail proc change 3 : { x <- 4; }; by auto. -abort. - + abort. +end ProcChangeFrameFailTest. (* -------------------------------------------------------------------- *) (* Positive if-block case: change ^if.1 (x <- x + 1 → x <- 4) inside @@ -313,12 +313,12 @@ theory ProcChangeBlockFrameTest. lemma L : hoare[M.f : x = 3 ==> true]. proof. - proc. - simplify. + proc=> /=. proc change ^if.1 : { x <- 4; }; by auto. -qed. + qed. +end ProcChangeBlockFrameTest. (* -------------------------------------------------------------------- *) (* Negative if-block case: change ^if.2 (x <- x + 1 → x <- 4) fails. @@ -334,17 +334,18 @@ theory ProcChangeBlockFailFrameTest. } else { x <- 4; } + return x; } }. - lemma L : hoare[M.f : x = 3 ==> true]. + lemma L : hoare[M.f : x = 3 ==> res = 0]. proof. - proc. - simplify. + proc=> /=. fail proc change ^if.2 : { x <- 4; }; by auto. -abort. + abort. +end ProcChangeBlockFailFrameTest. (* -------------------------------------------------------------------- *) (* Positive while case: change ^while.1 (x <- x + 1 → x <- 4). @@ -363,12 +364,12 @@ theory ProcChangeWhileFrameTest. lemma L : hoare[M.f : x = 3 ==> true]. proof. - proc. - simplify. + proc=> /=. proc change ^while.1 : { x <- 4; }; by auto. -qed. + qed. +end ProcChangeWhileFrameTest. (* -------------------------------------------------------------------- *) (* Negative while case — write after the change site: @@ -390,13 +391,14 @@ theory ProcChangeWhileFrameFailWriteAfterTest. lemma L : hoare[M.f : x = 3 ==> true]. proof. - proc. - simplify. - fail proc change ^while.1 : { + proc=> /=. + proc change ^while.1 : { x <- 4; - }; by auto. -abort. + }. + by auto. + abort. +end ProcChangeWhileFrameFailWriteAfterTest. (* -------------------------------------------------------------------- *) (* Negative while case — write before the change site: @@ -412,17 +414,18 @@ theory ProcChangeWhileFrameFailWriteBeforeTest. x <- x + 1; y <- 1; } + return x; } }. - lemma L : hoare[M.f : x = 3 ==> true]. + lemma L : hoare[M.f : x = 3 ==> res = 0]. proof. - proc. - simplify. + proc=> /=. fail proc change ^while.2 : { x <- 4; }; by auto. -abort. + abort. +end ProcChangeWhileFrameFailWriteBeforeTest. (* -------------------------------------------------------------------- *) (* Negative while case — write outside (before) the loop: @@ -438,15 +441,211 @@ theory ProcChangeWhileFrameFailWriteOutsideTest. x <- x + 1; y <- 1; } + return x; } }. - lemma L : hoare[M.f : x = 3 ==> true]. + lemma L : hoare[M.f : x = 3 ==> res = 0]. proof. - proc. - simplify. + proc=> /=. fail proc change ^while.1 : { x <- 4; }; by auto. -abort. + abort. +end ProcChangeWhileFrameFailWriteOutsideTest. + +(* -------------------------------------------------------------------- *) +(* observability through the context/post. + These tests exercise the variable selection performed by [zpr_pv] + and the post-side read analysis used by proc change. *) + +(* The continuation reads only x, so y can be changed freely in the + replacement block. *) +theory ProcChangeContextReadXOnlyTest. + module M = { + proc f(x : int, y : int) = { + x <- 1; + y <- 2; + x <- x + 1; + return x; + } + }. + + lemma L : hoare[M.f : true ==> res = 2]. + proof. + proc=> /=. + proc change [1..2] : { + x <- 1; + y <- 99; + }; by auto. + qed. +end ProcChangeContextReadXOnlyTest. + +(* -------------------------------------------------------------------- *) +(* The continuation reads only y, so x can be changed freely in the + replacement block. *) +theory ProcChangeContextReadYOnlyTest. + module M = { + proc f(x : int, y : int) = { + x <- 1; + y <- 2; + y <- y + 1; + return y; + } + }. + + lemma L : hoare[M.f : true ==> res = 3]. + proof. + proc=> /=. + proc change [1..2] : { + x <- 99; + y <- 2; + }; by auto. + qed. +end ProcChangeContextReadYOnlyTest. + +(* -------------------------------------------------------------------- *) +(* The continuation reads x, so changing x in the replacement block is + observable and proc change must fail. *) +theory ProcChangeContextReadXFailTest. + module M = { + proc f(x : int, y : int) = { + x <- 1; + y <- 2; + x <- x + 1; + return x; + } + }. + + lemma L : hoare[M.f : true ==> res = 2]. + proof. + proc=> /=. + proc change [1..2] : { + x <- 99; + y <- 2; + }. + fail by auto. + abort. +end ProcChangeContextReadXFailTest. + +(* -------------------------------------------------------------------- *) +(* The continuation reads y, so changing y in the replacement block is + observable and proc change must fail. *) +theory ProcChangeContextReadYFailTest. + module M = { + proc f(x : int, y : int) = { + x <- 1; + y <- 2; + y <- y + 1; + return y; + } + }. + + lemma L : hoare[M.f : true ==> res = 3]. + proof. + proc=> /=. + proc change [1..2] : { + x <- 1; + y <- 99; + }. + fail by auto. + abort. +end ProcChangeContextReadYFailTest. + +(* -------------------------------------------------------------------- *) +(* With no continuation, the post mentions only x, so y can vary in the + replacement block. *) +theory ProcChangePostReadXOnlyTest. + module M = { + var x : int + var y : int + + proc f() = { + x <- 1; + y <- 2; + } + }. + + lemma L : hoare[M.f : true ==> M.x = 1]. + proof. + proc=> /=. + proc change [1..2] : { + M.x <- 1; + M.y <- 99; + }; by auto. + qed. +end ProcChangePostReadXOnlyTest. + +(* -------------------------------------------------------------------- *) +(* With no continuation, the post mentions x, so changing x in the + replacement block is observable and proc change must fail. *) +theory ProcChangePostReadXFailTest. + module M = { + var x : int + var y : int + + proc f() = { + x <- 1; + y <- 2; + } + }. + + lemma L : hoare[M.f : true ==> M.x = 1]. + proof. + proc=> /=. + proc change [1..2] : { + M.x <- 99; + M.y <- 2; + }. + fail by auto. + abort. +end ProcChangePostReadXFailTest. + +(* -------------------------------------------------------------------- *) +(* With no continuation, the post mentions only y, so x can vary in the + replacement block. *) +theory ProcChangePostReadYOnlyTest. + module M = { + var x : int + var y : int + + proc f() = { + x <- 1; + y <- 2; + } + }. + + lemma L : hoare[M.f : true ==> M.y = 2]. + proof. + proc=> /=. + proc change [1..2] : { + M.x <- 99; + M.y <- 2; + }; by auto. + qed. +end ProcChangePostReadYOnlyTest. + +(* -------------------------------------------------------------------- *) +(* With no continuation, the post mentions y, so changing y in the + replacement block is observable and proc change must fail. *) +theory ProcChangePostReadYFailTest. + module M = { + var x : int + var y : int + proc f() = { + x <- 1; + y <- 2; + } + }. + + lemma L : hoare[M.f : true ==> M.y = 2]. + proof. + proc=> /=. + proc change [1..2] : { + M.x <- 1; + M.y <- 99; + }. + fail by auto. + abort. +end ProcChangePostReadYFailTest.