proc change: well-formed goals when introducing fresh locals

When `proc change` bound new local variables, both generated subgoals
were ill-formed: the local-equivalence goal carried the fresh local in
the memtype of the original (un-replaced) fragment, and the continuation
goal rewrote the side to a statement using the fresh local while keeping
the un-extended memtype, leaving a program that referenced a variable
absent from its memory type.

Thread the extended memtype to the side that runs the replacement: in
the local-equivalence goal it goes on the right (the new fragment) while
the left keeps the original memtype; in the continuation goal it goes on
the rewritten side. `hl_set_stmt` gains an optional `?mt` to override the
active side's memtype.

Author: strub

src/ecLowPhlGoal.ml

@@ -235,13 +235,18 @@ let tc1_process_codepos1 tc (side, cpos) =
   EcTyping.trans_codepos1 env cpos
 
 (* -------------------------------------------------------------------- *)
-let hl_set_stmt (side : side option) (f : form) (s : stmt) =
+(* [mt] overrides the memtype of the active side (the one whose statement is
+   being replaced), e.g. when the new statement [s] mentions fresh locals.
+   The memory identifier is untouched, so the pre/post-conditions keep
+   referring to it. *)
+let hl_set_stmt ?(mt : memtype option) (side : side option) (f : form) (s : stmt) =
+  let mtof (dfl : memenv) = odfl (snd dfl) mt in
   match side, f.f_node with
-  | None       , FhoareS   hs -> f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs)
-  | None       , FeHoareS  hs -> f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s (ehs_po hs)
-  | None       , FbdHoareS hs -> f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) s (bhs_po hs) hs.bhs_cmp (bhs_bd hs)
-  | Some `Left , FequivS   es -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) s es.es_sr (es_po es)
-  | Some `Right, FequivS   es -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) es.es_sl s (es_po es)
+  | None       , FhoareS   hs -> f_hoareS (mtof hs.hs_m) (hs_pr hs) s (hs_po hs)
+  | None       , FeHoareS  hs -> f_eHoareS (mtof hs.ehs_m) (ehs_pr hs) s (ehs_po hs)
+  | None       , FbdHoareS hs -> f_bdHoareS (mtof hs.bhs_m) (bhs_pr hs) s (bhs_po hs) hs.bhs_cmp (bhs_bd hs)
+  | Some `Left , FequivS   es -> f_equivS (mtof es.es_ml) (snd es.es_mr) (es_pr es) s es.es_sr (es_po es)
+  | Some `Right, FequivS   es -> f_equivS (snd es.es_ml) (mtof es.es_mr) (es_pr es) es.es_sl s (es_po es)
   | _          , _            -> assert false
 
 (* -------------------------------------------------------------------- *)

src/phl/ecPhlRewrite.ml

@@ -230,29 +230,27 @@ let process_rewrite_at
   |> FApi.t_sub [t_pre; t_post; EcLowGoal.t_id]
 
 (* -------------------------------------------------------------------- *)
-(* [t_change_stmt side pos ?me s] replaces a code range with [s] by
+(* [t_change_stmt side pos ?mt s] 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 observable afterwards;
    - the original program-logic goal with the selected range rewritten.
 
-   If [me] is provided, it is used as the memory environment (e.g. when
-   fresh local variables have been bound); otherwise, the memory
-   environment is taken from the goal. *)
+   If [mt] is provided, it is used as the memtype of the selected side (e.g.
+   when fresh local variables have been bound); otherwise, the memtype is
+   taken from the goal. *)
 let t_change_stmt
    (side : side option)
    (pos  : EcMatching.Position.codegap_range)
-  ?(me   : memenv option)
+  ?(mt   : memtype option)
    (s    : stmt)
    (tc   : tcenv1)
 =
   let env = FApi.tc1_env tc in
 
-  let me, stmt =
-    let metc, stmt = EcLowPhlGoal.tc1_get_stmt side tc in
-    (odfl metc me, stmt)
-  in
+  let (mid, metc), stmt = EcLowPhlGoal.tc1_get_stmt side tc in
+  let mt = odfl metc mt in
 
   let zpr, (_,stmt, epilog), _nmr =
     EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt in
@@ -269,8 +267,8 @@ let t_change_stmt
   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 pvs_me = EcIdent.Mid.find_def EcPV.PV.empty mid pvs in
+      let pvs = EcIdent.Mid.remove mid pvs in
 
          EcIdent.Mid.is_empty pvs
       && (EcPV.PV.indep env modi pvs_me) in
@@ -293,7 +291,7 @@ let t_change_stmt
         EcLowPhlGoal.logicS_post_read env
           (EcLowPhlGoal.get_logicS (FApi.tc1_goal tc))
       in
-      EcIdent.Mid.find_def EcPV.PV.empty (fst me) pvs
+      EcIdent.Mid.find_def EcPV.PV.empty mid pvs
     in
 
     EcPV.PV.union obs goal
@@ -314,7 +312,7 @@ let t_change_stmt
   let mr = EcIdent.create "&2" in
 
   let frame = omap (fun frame ->
-    let subst = EcSubst.add_memory EcSubst.empty (fst me) ml in
+    let subst = EcSubst.add_memory EcSubst.empty mid ml in
     EcSubst.subst_form subst frame) frame in
 
   let mk_pv_eq ((pv, ty) : prog_var * ty) =
@@ -329,10 +327,13 @@ let t_change_stmt
   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. *)
+     observable behavior required by the outer proof. The left program is the
+     original fragment, which only mentions the pre-existing locals
+     ([metc]); the right program is the replacement, which may use the
+     freshly bound locals ([mt]). *)
   let goal1 =
     f_equivS
-      (snd me) (snd me)
+      metc mt
       { ml; mr; inv = ofold f_and (f_ands pr_eq) frame; }
       (EcAst.stmt stmt) s
       { ml; mr; inv = f_ands po_eq; }
@@ -341,10 +342,11 @@ let t_change_stmt
   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. *)
+     selected statement range. The rewritten side also takes [mt], as the new
+     statement may mention the fresh locals. *)
   let goal2 =
    EcLowPhlGoal.hl_set_stmt
-     side (FApi.tc1_goal tc)
+     ~mt side (FApi.tc1_goal tc)
      stmt in
 
   FApi.xmutate1 tc `ProcChangeStmt [goal1; goal2]
@@ -401,4 +403,4 @@ let process_change_stmt
   let hyps = EcEnv.LDecl.push_active_ss me hyps in
   let s = EcProofTyping.process_stmt hyps s in
 
-  t_change_stmt side pos ~me s tc
+  t_change_stmt side pos ~mt:(snd me) s tc