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 <gxdelerue@proton.me>

Author: strub

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) =

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

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 =

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
 

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

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

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 "<program logic> (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
 

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
 

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