From 63b89659963931372b12c62153614d9c330b83ee Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 23 Mar 2026 14:38:22 +0100 Subject: [PATCH] Improve rewrite framing with formula-level read tracking It adds form/exnpost folding and formula read-analysis utilities, exposes statement-logic read extraction in ecLowPhlGoal, and updates ecPhlRewrite to build rewrite obligations from the actual framed precondition and written variables instead of relying on coarser statement-wide equality assumptions. Also increases test coverage for the proc change tactic. Co-Authored-By: Gustavo Delerue --- src/ecAst.ml | 12 +- src/ecAst.mli | 2 + src/ecCoreFol.ml | 45 +++---- src/ecCoreFol.mli | 14 +++ src/ecFol.ml | 19 +++ src/ecFol.mli | 3 + src/ecLowPhlGoal.ml | 35 ++++++ src/ecPV.ml | 77 ++++++++++++ src/ecPV.mli | 9 ++ src/phl/ecPhlRewrite.ml | 121 ++++++++++++++----- tests/procchange.ec | 261 +++++++++++++++++++++++++++++++++++++--- 11 files changed, 526 insertions(+), 72 deletions(-) diff --git a/src/ecAst.ml b/src/ecAst.ml index 42936f792c..3c7ac5fcbe 100644 --- a/src/ecAst.ml +++ b/src/ecAst.ml @@ -638,10 +638,14 @@ module POE = struct let to_list (poe : exnpost) = to_list_pre (destruct poe) - let iter (f : form -> unit) (poe : exnpost) = - f poe.main; - Mp.iter (fun _ -> f) (fst poe.exnmap); - oiter f (snd poe.exnmap) + let fold (tx : 'a -> form -> 'a) (state : 'a) (poe : exnpost) = + let state = tx state poe.main in + let state = Mp.fold (fun _ f state -> tx state f) (fst poe.exnmap) state in + let state = ofold (fun f state -> tx state f) state (snd poe.exnmap) in + state + + let iter (tx : form -> unit) (poe : exnpost) = + fold (fun () f -> tx f) () poe let iter2 (f : form -> form -> unit) (poe1 : exnpost) (poe2 : exnpost) = let merge (a : form option) (b : form option) = diff --git a/src/ecAst.mli b/src/ecAst.mli index 61afbb830a..13aabe0faa 100644 --- a/src/ecAst.mli +++ b/src/ecAst.mli @@ -401,6 +401,8 @@ module POE : sig val forall2 : (form -> form -> bool) -> exnpost -> exnpost -> bool + val fold : ('a -> form -> 'a) -> 'a -> exnpost -> 'a + val iter : (form -> unit) -> exnpost -> unit val iter2 : (form -> form -> unit) -> exnpost -> exnpost -> unit diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml index 54d61478c0..aae2bacbeb 100644 --- a/src/ecCoreFol.ml +++ b/src/ecCoreFol.ml @@ -535,33 +535,36 @@ let f_map gt g fp = f_pr_r { pr with pr_args = args'; pr_event = {m=pr.pr_event.m; inv=ev'}; } (* -------------------------------------------------------------------- *) -let f_iter g f = +let f_fold (tx : 'a -> form -> 'a) (state : 'a) (f : form) = match f.f_node with | Fint _ | Flocal _ | Fpvar _ | Fglob _ - | Fop _ -> () - - | Fquant (_ , _ , f1) -> g f1 - | Fif (f1, f2, f3) -> g f1;g f2; g f3 - | Fmatch (b, fs, _) -> List.iter g (b :: fs) - | Flet (_, f1, f2) -> g f1;g f2 - | Fapp (e, es) -> List.iter g (e :: es) - | Ftuple es -> List.iter g es - | Fproj (e, _) -> g e - - | FhoareF hf -> g (hf_pr hf).inv; POE.iter g (hf_po hf).hsi_inv - | FhoareS hs -> g (hs_pr hs).inv; POE.iter g (hs_po hs).hsi_inv - | FeHoareF hf -> g (ehf_pr hf).inv; g (ehf_po hf).inv - | FeHoareS hs -> g (ehs_pr hs).inv; g (ehs_po hs).inv - | FbdHoareF bhf -> g (bhf_pr bhf).inv; g (bhf_po bhf).inv; g (bhf_bd bhf).inv - | FbdHoareS bhs -> g (bhs_pr bhs).inv; g (bhs_po bhs).inv; g (bhs_bd bhs).inv - | FequivF ef -> g (ef_pr ef).inv; g (ef_po ef).inv - | FequivS es -> g (es_pr es).inv; g (es_po es).inv - | FeagerF eg -> g (eg_pr eg).inv; g (eg_po eg).inv - | Fpr pr -> g pr.pr_args; g pr.pr_event.inv + | Fop _ -> state + + | Fquant (_ , _ , f1) -> tx state f1 + | Fif (f1, f2, f3) -> List.fold_left tx state [f1; f2; f3] + | Fmatch (b, fs, _) -> List.fold_left tx state (b :: fs) + | Flet (_, f1, f2) -> List.fold_left tx state [f1; f2] + | Fapp (f, fs) -> List.fold_left tx state (f :: fs) + | Ftuple fs -> List.fold_left tx state fs + | Fproj (f, _) -> tx state f + + | FhoareF hf -> POE.fold tx (tx state (hf_pr hf).inv) (hf_po hf).hsi_inv + | FhoareS hs -> POE.fold tx (tx state (hs_pr hs).inv) (hs_po hs).hsi_inv + | FeHoareF hf -> List.fold_left tx state [(ehf_pr hf).inv; (ehf_po hf).inv] + | FeHoareS hs -> List.fold_left tx state [(ehs_pr hs).inv; (ehs_po hs).inv] + | FbdHoareF bhf -> List.fold_left tx state [(bhf_pr bhf).inv; (bhf_po bhf).inv; (bhf_bd bhf).inv] + | FbdHoareS bhs -> List.fold_left tx state [(bhs_pr bhs).inv; (bhs_po bhs).inv; (bhs_bd bhs).inv] + | FequivF ef -> List.fold_left tx state [(ef_pr ef).inv; (ef_po ef).inv] + | FequivS es -> List.fold_left tx state [(es_pr es).inv; (es_po es).inv] + | FeagerF eg -> List.fold_left tx state [(eg_pr eg).inv; (eg_po eg).inv] + | Fpr pr -> List.fold_left tx state [pr.pr_args; pr.pr_event.inv] +(* -------------------------------------------------------------------- *) +let f_iter (tx : form -> unit) (f : form) = + f_fold (fun () f -> tx f) () f (* -------------------------------------------------------------------- *) let form_exists g f = diff --git a/src/ecCoreFol.mli b/src/ecCoreFol.mli index 1f2afcb856..b270d12d5e 100644 --- a/src/ecCoreFol.mli +++ b/src/ecCoreFol.mli @@ -76,6 +76,8 @@ val f_node : form -> f_node (* not recursive *) val f_map : (EcTypes.ty -> EcTypes.ty) -> (form -> form) -> form -> form val f_iter : (form -> unit) -> form -> unit +val f_fold : ('a -> form -> 'a) -> 'a -> form -> 'a + val form_exists: (form -> bool) -> form -> bool val form_forall: (form -> bool) -> form -> bool @@ -108,9 +110,15 @@ val f_lambda : bindings -> form -> form val f_forall_mems : (EcIdent.t * memtype) list -> form -> form +val f_hoareF_r : sHoareF -> form +val f_hoareS_r : sHoareS -> form + val f_hoareF : ss_inv -> xpath -> hs_inv -> form val f_hoareS : memtype -> ss_inv -> stmt -> hs_inv -> form +val f_eHoareF_r : eHoareF -> form +val f_eHoareS_r : eHoareS -> form + val f_eHoareF : ss_inv -> xpath -> ss_inv -> form val f_eHoareS : memtype -> ss_inv -> EcCoreModules.stmt -> ss_inv -> form @@ -119,10 +127,16 @@ val f_eHoareS : memtype -> ss_inv -> EcCoreModules.stmt -> ss_inv -> form (* soft-constructors - bd hoare *) val hoarecmp_opp : hoarecmp -> hoarecmp +val f_bdHoareF_r : bdHoareF -> form +val f_bdHoareS_r : bdHoareS -> form + val f_bdHoareF : ss_inv -> xpath -> ss_inv -> hoarecmp -> ss_inv -> form val f_bdHoareS : memtype -> ss_inv -> stmt -> ss_inv -> hoarecmp -> ss_inv -> form (* soft-constructors - equiv *) +val f_equivF_r : equivF -> form +val f_equivS_r : equivS -> form + val f_equivF : ts_inv -> xpath -> xpath -> ts_inv -> form val f_equivS : memtype -> memtype -> ts_inv -> stmt -> stmt -> ts_inv -> form diff --git a/src/ecFol.ml b/src/ecFol.ml index 57322210d9..7a9fbf4942 100644 --- a/src/ecFol.ml +++ b/src/ecFol.ml @@ -1104,6 +1104,25 @@ let rec one_sided_vs mem fp = | Fapp (f, args) -> one_sided_vs mem f @ List.concat_map (one_sided_vs mem) args | _ -> [] +(* -------------------------------------------------------------------- *) +let filter_topand_form (test : form -> bool) = + let rec doit (f : form) = + match sform_of_form f with + | SFand (mode, (f1, f2)) -> begin + match doit f1, doit f2 with + | None, None -> None + | Some f, None | None, Some f -> Some f + | Some f1, Some f2 -> begin + match mode with + | `Sym -> Some (f_and f1 f2) + | `Asym -> Some (f_anda f1 f2) + end + end + | _ -> + if test f then Some f else None + in fun f -> doit f + +(* -------------------------------------------------------------------- *) let rec dump_f f = let dump_quant q = match q with diff --git a/src/ecFol.mli b/src/ecFol.mli index 080a4d3dea..6be1d1aafc 100644 --- a/src/ecFol.mli +++ b/src/ecFol.mli @@ -260,5 +260,8 @@ module DestrReal : sig val abs : form -> form end +(* -------------------------------------------------------------------- *) +val filter_topand_form : (form -> bool) -> form -> form option + (* -------------------------------------------------------------------- *) val dump_f : form -> string diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 00687ebd81..6daabbfd6d 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -330,6 +330,41 @@ let push_memenvs_pre (hyps : LDecl.hyps) (f : form) = ([ml; mr], hyps) | _ -> assert false +(* -------------------------------------------------------------------- *) +type logicS = [ + | `Hoare of sHoareS + | `BdHoare of bdHoareS + | `Equiv of equivS + | `EHoare of eHoareS +] + +let get_logicS (f : form) : logicS = + match f.f_node with + | FhoareS hs -> `Hoare hs + | FbdHoareS hs -> `BdHoare hs + | FequivS hs -> `Equiv hs + | FeHoareS hs -> `EHoare hs + | _ -> destr_error " (S)" + +let hoareS_read (env : env) (hs : sHoareS) : EcPV.pmvs = + EcPV.form_read env PMVS.empty (f_hoareS_r hs) + +let bdHoareS_read (env : env) (hs : bdHoareS) : pmvs = + form_read env PMVS.empty (f_bdHoareS_r hs) + +let equivS_read (env : env) (hs : equivS) : pmvs = + form_read env PMVS.empty (f_equivS_r hs) + +let eHoareS_read (env : env) (hs : eHoareS) : pmvs = + form_read env PMVS.empty (f_eHoareS_r hs) + +let logicS_read (env : env) (f : logicS) = + match f with + | `Hoare hs -> hoareS_read env hs + | `BdHoare hs -> bdHoareS_read env hs + | `Equiv hs -> equivS_read env hs + | `EHoare hs -> eHoareS_read env hs + (* -------------------------------------------------------------------- *) exception InvalidSplit of codepos1 diff --git a/src/ecPV.ml b/src/ecPV.ml index c1c297d754..590ab1a2e7 100644 --- a/src/ecPV.ml +++ b/src/ecPV.ml @@ -630,6 +630,83 @@ 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 +(* -------------------------------------------------------------------- *) +type pmvs = PV.t Mid.t + +module PMVS : sig + val empty : pmvs +end = struct + let empty : pmvs = + Mid.empty +end + +(* -------------------------------------------------------------------- *) +let form_read (env : env) (pvs : pmvs) = + let rec doit (bds : Sid.t) (pvs : pmvs) (f : form) = + match f.f_node with + | Fpvar (_, m) when Sid.mem m bds -> + pvs + + | Fpvar (pv, m) -> + Mid.change + (fun pvs -> + pvs + |> Option.value ~default:PV.empty + |> PV.add env pv f.f_ty + |> Option.some) + m pvs + + | Fquant (_, subbds, f) -> + let bds = + List.fold_left + (fun bds -> function _ -> bds) + bds subbds in + doit bds pvs f + + | FhoareF hs -> + let bds = Sid.add hs.hf_m bds in + POE.fold (doit bds) (doit bds pvs (hf_pr hs).inv) (hf_po hs).hsi_inv + + | FhoareS hs -> + let bds = Sid.add (fst hs.hs_m) bds in + POE.fold (doit bds) (doit bds pvs (hs_pr hs).inv) (hs_po hs).hsi_inv + + | FbdHoareF hs -> + let subbds = Sid.add hs.bhf_m bds in + List.fold_left + (doit subbds) (doit bds pvs (bhf_bd hs).inv) + [(bhf_pr hs).inv; (bhf_po hs).inv] + + | FbdHoareS hs -> + let subbds = Sid.add (fst hs.bhs_m) bds in + List.fold_left + (doit subbds) (doit bds pvs (bhs_bd hs).inv) + [(bhs_pr hs).inv; (bhs_po hs).inv] + + | FequivF hs -> + let bds = List.fold_left ((^~) Sid.add) bds [] in + List.fold_left (doit bds) pvs [(ef_pr hs).inv; (ef_po hs).inv] + + | FequivS hs -> + let bds = List.fold_left ((^~) Sid.add) bds [] in + List.fold_left (doit bds) pvs [(es_pr hs).inv; (es_po hs).inv] + + | FeHoareF hs -> + let bds = Sid.add hs.ehf_m bds in + List.fold_left (doit bds) pvs [(ehf_pr hs).inv; (ehf_po hs).inv] + + | FeHoareS hs -> + let bds = Sid.add (fst hs.ehs_m) bds in + List.fold_left (doit bds) pvs [(ehs_pr hs).inv; (ehs_po hs).inv] + + | Fpr pr -> + let pvs = doit bds pvs pr.pr_args in + let pvs = doit (Sid.add pr.pr_mem bds) pvs pr.pr_event.inv in + pvs + + | _ -> f_fold (doit bds) pvs f + in fun f -> doit Sid.empty pvs f + (* -------------------------------------------------------------------- *) exception EqObsInError diff --git a/src/ecPV.mli b/src/ecPV.mli index 0e9df4354b..ac1e64cbb5 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 +(* -------------------------------------------------------------------- *) +type pmvs = PV.t EcIdent.Mid.t + +module PMVS : sig + val empty : pmvs +end + +val form_read : env -> pmvs -> form -> pmvs + (* -------------------------------------------------------------------- *) exception EqObsInError diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml index 07bc76cc7f..331d1c9477 100644 --- a/src/phl/ecPhlRewrite.ml +++ b/src/phl/ecPhlRewrite.ml @@ -6,6 +6,7 @@ open EcCoreGoal open EcEnv open EcModules open EcFol +open EcMatching module L = EcLocation module PT = EcProofTerm @@ -230,6 +231,44 @@ let process_rewrite_at |> 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; + - the original program-logic goal with the selected range rewritten. *) let t_change_stmt (side : side option) (pos : EcMatching.Position.codepos_range) @@ -239,48 +278,76 @@ let t_change_stmt let env = FApi.tc1_env tc in let me, stmt = EcLowPhlGoal.tc1_get_stmt side tc in - let (zpr, _), (stmt, epilog) = EcMatching.Zipper.zipper_and_split_of_cpos_range env pos stmt in + let (zpr, _), (stmt, epilog) = + EcMatching.Zipper.zipper_and_split_of_cpos_range env pos stmt in + + (* 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 pvs = EcPV.is_write env (stmt @ s.s_node) in - let pvs, globs = EcPV.PV.elements pvs in + (* Keep only the top-level conjuncts of the current precondition that talk + about the active memory and are independent from the surrounding writes. *) + let frame = + let filter (f : form) = + let pvs = EcPV.form_read env EcPV.PMVS.empty f in + let pvs_me = EcIdent.Mid.find_def EcPV.PV.empty (fst me) pvs in + let pvs = EcIdent.Mid.remove (fst me) pvs in - let pre_pvs, pre_globs = EcPV.PV.elements @@ EcPV.PV.inter + EcIdent.Mid.is_empty pvs + && (EcPV.PV.indep env modi pvs_me) in + + EcFol.filter_topand_form + filter + (inv_of_inv (EcLowPhlGoal.tc1_get_pre tc)) in + + let written = EcPV.PV.empty in + let written = EcPV.is_write_r env written stmt in + let written = EcPV.is_write_r env written s.s_node in + + (* The local equivalence goal relates shared reads in the precondition and + all possible writes in the postcondition. *) + let wr_pvs, wr_globs = EcPV.PV.elements written in + + let pr_pvs, pr_globs = EcPV.PV.elements @@ EcPV.PV.inter (EcPV.is_read env stmt) (EcPV.is_read env s.s_node) in - let mleft = EcIdent.create "&1" in (* FIXME: PR: is this how we want to do this? *) - let mright = EcIdent.create "&2" in - - let eq = - List.map - (fun (pv, ty) -> f_eq (f_pvar pv ty mleft).inv (f_pvar pv ty mright).inv) - pvs - @ - List.map - (fun mp -> f_eqglob mp mleft mp mright) - globs in - - let pre_eq = - List.map - (fun (pv, ty) -> f_eq (f_pvar pv ty mleft).inv (f_pvar pv ty mright).inv) - pre_pvs - @ - List.map - (fun mp -> f_eqglob mp mleft mp mright) - pre_globs - in + let ml = EcIdent.create "&1" in + let mr = EcIdent.create "&2" in + + let frame = omap (fun frame -> + let subst = EcSubst.add_memory EcSubst.empty (fst me) ml in + EcSubst.subst_form subst frame) frame in + + let mk_pv_eq ((pv, ty) : prog_var * ty) = + f_eq (f_pvar pv ty ml).inv (f_pvar pv ty mr).inv + + and mk_glob_eq (mp : EcPath.mpath) = + f_eqglob mp ml mp mr + + in + + let pr_eq = List.map mk_pv_eq pr_pvs @ List.map mk_glob_eq pr_globs in + let po_eq = List.map mk_pv_eq wr_pvs @ List.map mk_glob_eq wr_globs in + (* 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=mleft; mr=mright; inv=f_ands pre_eq} + { ml; mr; inv = ofold f_and (f_ands pr_eq) frame; } (EcAst.stmt stmt) s - {ml=mleft; mr=mright; inv=f_ands eq} + { ml; mr; inv = f_ands po_eq; } in let stmt = EcMatching.Zipper.zip { zpr with z_tail = s.s_node @ epilog } in + (* Second subgoal: continue with the original goal after rewriting the + selected statement range. *) let goal2 = EcLowPhlGoal.hl_set_stmt side (FApi.tc1_goal tc) diff --git a/tests/procchange.ec b/tests/procchange.ec index 6863802f09..25eb8f40aa 100644 --- a/tests/procchange.ec +++ b/tests/procchange.ec @@ -1,6 +1,22 @@ +(* Tests for the proc change tactic. + proc change replaces a range of program statements with semantically + equivalent code, generating an equivalence sub-goal to justify the + replacement. + + The file is organised in three sections: + 1. Basic instruction types — assign, sample, if, while (equiv and hoare). + 2. Statements inside while bodies. + 3. Precondition framing — tests that the tactic correctly determines + whether the precondition can reach the change site. *) require import AllCore Distr. (* -------------------------------------------------------------------- *) +(* Section 1: basic instruction types. + Each theory changes a single instruction (or range) and checks that + the generated equivalence sub-goal can be discharged. *) + +(* proc change on an equiv goal: replace a range of assignments [1..3] + with a single equivalent assignment on the left-hand side. *) theory ProcChangeAssignEquiv. module M = { proc f(x : int) = { @@ -20,7 +36,8 @@ theory ProcChangeAssignEquiv. abort. end ProcChangeAssignEquiv. -theory ProcChangeAssignHoareEquiv. +(* -------------------------------------------------------------------- *) +theory ProcChangeAssignHoare. module M = { proc f(x : int) = { x <- x + 0; @@ -32,9 +49,11 @@ theory ProcChangeAssignHoareEquiv. proc. proc change [1..1] : { x <- x ; }. wp. skip. smt(). abort. -end ProcChangeAssignHoareEquiv. +end ProcChangeAssignHoare. (* -------------------------------------------------------------------- *) +(* proc change on a sampling instruction in an equiv goal: + simplify x <$ dunit (x + 0) to x <$ dunit x. *) theory ProcChangeSampleEquiv. module M = { proc f(x : int) = { @@ -51,6 +70,8 @@ theory ProcChangeSampleEquiv. end ProcChangeSampleEquiv. (* -------------------------------------------------------------------- *) +(* proc change on an if statement in an equiv goal: + simplify the condition x + 0 = y to x = y. *) theory ProcChangeIfEquiv. module M = { proc f(x : int, y : int) = { @@ -76,6 +97,8 @@ theory ProcChangeIfEquiv. end ProcChangeIfEquiv. (* -------------------------------------------------------------------- *) +(* proc change on a while statement in an equiv goal: simplify the + loop condition x + 0 <> y to x <> y (the body also changes). *) theory ProcChangeWhileEquiv. module M = { proc f(x : int, y : int) = { @@ -101,6 +124,14 @@ end ProcChangeWhileEquiv. (* -------------------------------------------------------------------- *) +(* Section 2: proc change applied to individual statements inside a + while body. Position ^while.N selects statement N of the loop body; + [^while.N..^while.M] selects a range; ^while.N-K is an offset variant. *) + +(* Three consecutive uses of proc change on the same equiv goal: + (a) ^while.2 — change a single statement at position 2 in the body. + (b) [^while.1..^while.2] — change a two-statement range. + (c) [^while.1-1] — offset-range form selecting one statement. *) theory ProcChangeInWhileEquiv. module M = { proc f(x : int, y : int) = { @@ -128,23 +159,6 @@ theory ProcChangeInWhileEquiv. abort. end ProcChangeInWhileEquiv. - -(* -------------------------------------------------------------------- *) -theory ProcChangeAssignHoare. - module M = { - proc f(x : int) = { - x <- x + 0; - } - }. - - lemma L : hoare[M.f: true ==> true]. - proof. - proc. - proc change [1..1] : { x <- x; }. - wp; skip; smt(). - abort. -end ProcChangeAssignHoare. - (* -------------------------------------------------------------------- *) theory ProcChangeSampleHoare. module M = { @@ -210,6 +224,7 @@ end ProcChangeWhileHoare. (* -------------------------------------------------------------------- *) +(* proc change on a single statement inside a while body, hoare goal. *) theory ProcChangeInWhileHoare. module M = { proc f(x : int, y : int) = { @@ -218,7 +233,7 @@ theory ProcChangeInWhileHoare. } } }. - + lemma L : hoare[M.f : true ==> true]. proof. proc. @@ -229,3 +244,209 @@ theory ProcChangeInWhileHoare. abort. end ProcChangeInWhileHoare. +(* -------------------------------------------------------------------- *) +(* Section 3: precondition framing. + proc change checks whether the precondition value of each variable + can "reach" the change site — i.e., that no earlier statement in the + same path writes to that variable first. If the check passes the + tactic succeeds; otherwise it fails. *) + +(* Positive flat case: change statement 2 (x <- x + 1 → x <- 4). + Only y is written before position 2, so x = 3 from the precondition + propagates freely to the change site. *) +theory ProcChangeFrameTest. + module M = { + proc f(x: int, y: int) = { + y <- 0; + x <- x + 1; + } + }. + + lemma L : hoare[M.f : x = 3 ==> true]. + proof. + proc. + simplify. + proc change 2 : { + x <- 4; + }; by auto. +qed. + +(* -------------------------------------------------------------------- *) +(* Negative flat case: change statement 3 (x <- x + 1 → x <- 4) fails. + Statement 2 (x <- 4) writes x before the change site, so the + precondition x = 3 cannot propagate to position 3. *) +theory ProcChangeFrameFailTest. + module M = { + proc f(x: int, y: int) = { + y <- 0; + x <- 4; + x <- x + 1; + } + }. + + lemma L : hoare[M.f : x = 3 ==> true]. + proof. + proc. + simplify. + fail proc change 3 : { + x <- 4; + }; by auto. +abort. + + +(* -------------------------------------------------------------------- *) +(* Positive if-block case: change ^if.1 (x <- x + 1 → x <- 4) inside + the true branch. No write to x precedes ^if.1 in this branch, so + the precondition x = 3 reaches the change site. *) +theory ProcChangeBlockFrameTest. + module M = { + proc f(x: int, y: int) = { + y <- 0; + if( y = 0) { + x <- x + 1; + x <- 4; + } else { + x <- 4; + } + } + }. + + lemma L : hoare[M.f : x = 3 ==> true]. + proof. + proc. + simplify. + proc change ^if.1 : { + x <- 4; + }; by auto. +qed. + +(* -------------------------------------------------------------------- *) +(* Negative if-block case: change ^if.2 (x <- x + 1 → x <- 4) fails. + Statement ^if.1 (x <- 4) writes x before ^if.2 in the same branch, + blocking the precondition x = 3 from propagating. *) +theory ProcChangeBlockFailFrameTest. + module M = { + proc f(x: int, y: int) = { + y <- 0; + if( y = 0) { + x <- 4; + x <- x + 1; + } else { + x <- 4; + } + } + }. + + lemma L : hoare[M.f : x = 3 ==> true]. + proof. + proc. + simplify. + fail proc change ^if.2 : { + x <- 4; + }; by auto. +abort. + +(* -------------------------------------------------------------------- *) +(* Positive while case: change ^while.1 (x <- x + 1 → x <- 4). + No write to x precedes ^while.1 inside the loop body (y <- 1 writes + y, not x), so the precondition x = 3 propagates. *) +theory ProcChangeWhileFrameTest. + module M = { + proc f(x: int, y: int) = { + y <- 0; + while(y = 0) { + x <- x + 1; + y <- 1; + } + } + }. + + lemma L : hoare[M.f : x = 3 ==> true]. + proof. + proc. + simplify. + proc change ^while.1 : { + x <- 4; + }; by auto. +qed. + +(* -------------------------------------------------------------------- *) +(* Negative while case — write after the change site: + change ^while.1 (x <- x + 1 → x <- 4) fails. + ^while.2 (x <- 4) writes x after the change site inside the same + loop iteration, so x entering ^while.1 on a subsequent iteration + would be 4, not the precondition value 3. *) +theory ProcChangeWhileFrameFailWriteAfterTest. + module M = { + proc f(x: int, y: int) = { + y <- 0; + while(y = 0) { + x <- x + 1; + x <- 4; + y <- 1; + } + } + }. + + lemma L : hoare[M.f : x = 3 ==> true]. + proof. + proc. + simplify. + fail proc change ^while.1 : { + x <- 4; + }; by auto. +abort. + + +(* -------------------------------------------------------------------- *) +(* Negative while case — write before the change site: + change ^while.2 (x <- x + 1 → x <- 4) fails. + ^while.1 (x <- 4) writes x before ^while.2 in the loop body, + blocking the precondition x = 3 from reaching the change site. *) +theory ProcChangeWhileFrameFailWriteBeforeTest. + module M = { + proc f(x: int, y: int) = { + y <- 0; + while(y = 0) { + x <- 4; + x <- x + 1; + y <- 1; + } + } + }. + + lemma L : hoare[M.f : x = 3 ==> true]. + proof. + proc. + simplify. + fail proc change ^while.2 : { + x <- 4; + }; by auto. +abort. + +(* -------------------------------------------------------------------- *) +(* Negative while case — write outside (before) the loop: + change ^while.1 (x <- x + 1 → x <- 4) fails. + Statement 2 (x <- 4) writes x before the while loop is entered, + so the precondition x = 3 is overwritten before the change site. *) +theory ProcChangeWhileFrameFailWriteOutsideTest. + module M = { + proc f(x: int, y: int) = { + y <- 0; + x <- 4; + while(y = 0) { + x <- x + 1; + y <- 1; + } + } + }. + + lemma L : hoare[M.f : x = 3 ==> true]. + proof. + proc. + simplify. + fail proc change ^while.1 : { + x <- 4; + }; by auto. +abort. +