Rewriting in the pre-condition of PL logics

Allows rewriting inside the pre-condition of any PL logic.

Syntax: `proc rewrite @pre ...`

The side conditions generated by the rewriting have to be
checked under the initial pre-condition.

This tactic is outside of the TCB.

Author: strub

src/ecAst.ml

@@ -472,7 +472,13 @@ let inv_of_inv (inv: inv) : form =
   match inv with
   | Inv_ss ss -> ss.inv
   | Inv_ts ts -> ts.inv
-  | _ -> failwith "expected single or two sided invarinat"
+  | _ -> failwith "expected single or two sided invariant"
+
+let memories_of_inv (inv : inv) : memory list =
+  match inv with
+  | Inv_ss ss -> [ss.m]
+  | Inv_ts ts -> [ts.ml; ts.mr]
+  | Inv_hs hs -> [hs.hsi_m]
 
 let lift_ss_inv (f: ss_inv -> 'a) : inv -> 'a =
   let f inv = match inv with

src/ecAst.mli

@@ -419,6 +419,7 @@ type inv =
   | Inv_hs of hs_inv
 
 val inv_of_inv : inv -> form
+val memories_of_inv : inv -> memory list
 
 val lift_ss_inv : (ss_inv -> 'a) -> inv -> 'a
 val lift_ss_inv2 : (ss_inv -> ss_inv -> 'a) -> inv -> inv -> 'a

src/ecHiGoal.ml

@@ -1403,8 +1403,8 @@ let rec process_mintros_1 ?(cf = true) ttenv pis gs =
 
   and intro1_dup (_ : ST.state) (tc : tcenv1) =
     try
-      let pt = PT.pt_of_uglobal !!tc (FApi.tc1_hyps tc) LG.p_ip_dup in
-      EcLowGoal.Apply.t_apply_bwd_r ~mode:fmrigid ~canview:false pt tc
+      EcLowGoal.t_duplicate_top_assumtion tc
+
     with EcLowGoal.Apply.NoInstance _ ->
       tc_error !!tc "no top-assumption to duplicate"
 

src/ecHiTacticals.ml

@@ -230,6 +230,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Plossless                 -> EcPhlHiAuto.t_lossless
     | Prepl_stmt infos          -> EcPhlTrans.process_equiv_trans infos
     | Pprocrewrite (s, p, f)    -> EcPhlRewrite.process_rewrite s p f
+    | Pprocrewriteat (x, f)     -> EcPhlRewrite.process_rewrite_at x f
     | Pchangestmt (s, p, c)     -> EcPhlRewrite.process_change_stmt s p c
     | Prwprgm infos             -> EcPhlRwPrgm.process_rw_prgm infos
     | Phoaresplit               -> EcPhlHoare.process_hoaresplit

src/ecLowGoal.ml

@@ -845,6 +845,12 @@ module Apply = struct
 
 end
 
+(* -------------------------------------------------------------------- *)
+let t_duplicate_top_assumtion (tc : tcenv1) =
+  let hlemma = EcCoreLib.CI_Logic.p_ip_dup in
+  let pt = PT.pt_of_uglobal !!tc (FApi.tc1_hyps tc) hlemma in
+  Apply.t_apply_bwd_r ~mode:EcMatching.fmrigid ~canview:false pt tc
+
 (* -------------------------------------------------------------------- *)
 type genclear = [`Clear | `TryClear | `NoClear]
 

src/ecLowGoal.mli

@@ -158,6 +158,9 @@ val t_right : ?reduce:lazyred -> FApi.backward
 
 val t_or_intro_prind : ?reduce:lazyred -> side -> FApi.backward
 
+(* -------------------------------------------------------------------- *)
+val t_duplicate_top_assumtion : FApi.backward
+
 (* -------------------------------------------------------------------- *)
 val t_split : ?i: int -> ?closeonly:bool -> ?reduce:lazyred -> FApi.backward
 val t_split_prind : ?reduce:lazyred -> FApi.backward

src/ecLowPhlGoal.ml

@@ -268,7 +268,6 @@ let get_post f =
   | FequivS es   -> Some (Inv_ts (es_po es))
   | _            -> None
 
-
 let tc1_get_post tc =
   match get_post (FApi.tc1_goal tc) with
   | None   -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc
@@ -304,6 +303,33 @@ let set_pre ~pre f =
     f_equivS (snd es.es_ml) (snd es.es_mr) pre es.es_sl es.es_sr (es_po es)
  | _            -> assert false
 
+(* -------------------------------------------------------------------- *)
+let get_memenvs_pre (env : env) (f : form) =
+  match f.f_node with
+  | FhoareF hf   -> Some [fst (EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f env)]
+  | FhoareS hs   -> Some [hs.hs_m]
+  | FeHoareF hf  -> Some [fst (EcEnv.Fun.hoareF_memenv hf.ehf_m hf.ehf_f env)]
+  | FeHoareS hs  -> Some [hs.ehs_m]
+  | FbdHoareF hf -> Some [fst (EcEnv.Fun.hoareF_memenv hf.bhf_m hf.bhf_f env)]
+  | FbdHoareS hs -> Some [hs.bhs_m]
+  | FequivF ef   -> Some (List.of_pair (fst (EcEnv.Fun.equivF_memenv ef.ef_ml ef.ef_mr ef.ef_fl ef.ef_fr env)))
+  | FequivS es   -> Some [es.es_ml; es.es_mr]
+  | _            -> None
+
+(* -------------------------------------------------------------------- *)
+let push_memenvs_pre (hyps : LDecl.hyps) (f : form) =
+  match get_memenvs_pre (LDecl.toenv hyps) f with
+  | Some [m] ->
+    let m = (EcIdent.create "&hr", snd m) in
+    let hyps = EcEnv.LDecl.push_active_ss m hyps in
+    ([m], hyps)
+  | Some [ml; mr] ->
+    let ml = (EcIdent.create "&1", snd ml) in
+    let mr = (EcIdent.create "&2", snd mr) in
+    let hyps = EcEnv.LDecl.push_active_ts ml mr hyps in
+    ([ml; mr], hyps)
+  | _ -> assert false
+
 (* -------------------------------------------------------------------- *)
 exception InvalidSplit of codepos1
 

src/ecParser.mly

@@ -3201,6 +3201,9 @@ interleave_info:
 | PROC REWRITE side=side? pos=codepos SLASHEQ
     { Pprocrewrite (side, pos, `Simpl) }
 
+| PROC REWRITE AT tg=ident f=pterm
+    { Pprocrewriteat (tg, f) }
+
 | HOARE SPLIT
     { Phoaresplit }
 

src/ecParsetree.ml

@@ -789,6 +789,7 @@ type phltactic =
   | Pbdhoare_split of bdh_split
   | Prwprgm of rwprgm
   | Pprocrewrite   of side option * pcodepos * prrewrite
+  | Pprocrewriteat of psymbol * ppterm
   | Pchangestmt    of side option * pcodepos_range * pstmt
   | Phoaresplit
 

src/ecSubst.ml

@@ -1201,3 +1201,12 @@ let hs_inv_rebind ({hsi_inv;hsi_m}: hs_inv) (m': memory) : hs_inv =
   else
     let hsi_inv = POE.map (subst_form (add_memory empty hsi_m m')) hsi_inv in
     { hsi_inv; hsi_m = m' }
+
+(* -------------------------------------------------------------------- *)
+let inv_rebind (inv : inv) (ms : memory list) : inv =
+  match inv, ms with
+  | Inv_ss ss, [m] -> Inv_ss (ss_inv_rebind ss m)
+  | Inv_ts ts, [ml; mr] -> Inv_ts (ts_inv_rebind ts ml mr)
+  | Inv_hs hs, [m] -> Inv_hs (hs_inv_rebind hs m)
+  | _, _ -> assert false
+