Stronger precondition in pRHL tactics eager-seq and eager-while

src/ecCoreFol.ml

@@ -214,6 +214,9 @@ let f_lambda b  f     = f_quant Llambda b f
 let f_forall_mems bds f =
   f_forall (List.map (fun (m, mt) -> (m, GTmem mt)) bds) f
 
+let f_exists_mems bds f =
+  f_exists (List.map (fun (m, mt) -> (m, GTmem mt)) bds) f
+
 (* -------------------------------------------------------------------- *)
 let ty_fbool1 = toarrow (List.make 1 tbool) tbool
 let ty_fbool2 = toarrow (List.make 2 tbool) tbool

src/ecCoreFol.mli

@@ -109,6 +109,7 @@ val f_forall : bindings -> form -> form
 val f_lambda : bindings -> form -> form
 
 val f_forall_mems : (EcIdent.t * memtype) list -> form -> form
+val f_exists_mems : (EcIdent.t * memtype) list -> form -> form
 
 val f_hoareF_r : sHoareF -> form
 val f_hoareS_r : sHoareS -> form

src/ecSubst.ml

@@ -1161,6 +1161,9 @@ let ss_inv_generalize_as_right ({inv;m}: ss_inv) (ml: memory) (mr: memory) : ts_
 let f_forall_mems_ss_inv menv inv =
   f_forall_mems [menv] (ss_inv_rebind inv (fst menv)).inv
 
+let f_exists_mems_ss_inv menv inv =
+  f_exists_mems [menv] (ss_inv_rebind inv (fst menv)).inv
+
 let ts_inv_rebind_left ({inv;ml;mr}: ts_inv) (m: memory) : ts_inv =
   if ml = m then
     { inv; ml; mr }
@@ -1192,6 +1195,9 @@ let ts_inv_rebind ({inv;ml;mr}: ts_inv) (ml': memory) (mr': memory) : ts_inv =
 let f_forall_mems_ts_inv menvl menvr inv =
   f_forall_mems [menvl; menvr] (ts_inv_rebind inv (fst menvl) (fst menvr)).inv
 
+let f_exists_mems_ts_inv menvl menvr inv =
+  f_exists_mems [menvl; menvr] (ts_inv_rebind inv (fst menvl) (fst menvr)).inv
+
 let ss_inv_forall_ml_ts_inv menvl inv =
   let inv' = f_forall_mems [menvl] (ts_inv_rebind_left inv (fst menvl)).inv in
   { inv=inv'; m=inv.mr}
@@ -1200,6 +1206,14 @@ let ss_inv_forall_mr_ts_inv menvr inv =
   let inv' = f_forall_mems [menvr] (ts_inv_rebind_right inv (fst menvr)).inv in
   { inv=inv'; m=inv.ml }
 
+let ss_inv_exists_ml_ts_inv menvl inv =
+  let inv' = f_exists_mems [menvl] (ts_inv_rebind_left inv (fst menvl)).inv in
+  { inv=inv'; m=inv.mr}
+
+let ss_inv_exists_mr_ts_inv menvr inv =
+  let inv' = f_exists_mems [menvr] (ts_inv_rebind_right inv (fst menvr)).inv in
+  { inv=inv'; m=inv.ml }
+
 (* -------------------------------------------------------------------- *)
 let hs_inv_rebind ({hsi_inv;hsi_m}: hs_inv) (m': memory) : hs_inv =
   if m' = hsi_m then

src/ecSubst.mli

@@ -87,16 +87,23 @@ val open_tydecl : tydecl -> ty list -> ty_body
 val ss_inv_rebind : ss_inv -> memory -> ss_inv
 val ss_inv_generalize_as_left : ss_inv -> memory -> memory -> ts_inv
 val ss_inv_generalize_as_right : ss_inv -> memory -> memory -> ts_inv
+
 val f_forall_mems_ss_inv : memenv -> ss_inv -> form
+val f_exists_mems_ss_inv : memenv -> ss_inv -> form
 
 val ts_inv_rebind : ts_inv -> memory -> memory -> ts_inv
 val ts_inv_rebind_left : ts_inv -> memory -> ts_inv
 val ts_inv_rebind_right : ts_inv -> memory -> ts_inv
+
 val f_forall_mems_ts_inv : memenv -> memenv -> ts_inv -> form
+val f_exists_mems_ts_inv : memenv -> memenv -> ts_inv -> form
 
 val ss_inv_forall_ml_ts_inv : memenv -> ts_inv -> ss_inv
 val ss_inv_forall_mr_ts_inv : memenv -> ts_inv -> ss_inv
 
+val ss_inv_exists_ml_ts_inv : memenv -> ts_inv -> ss_inv
+val ss_inv_exists_mr_ts_inv : memenv -> ts_inv -> ss_inv
+
 (* -------------------------------------------------------------------- *)
 val hs_inv_rebind : hs_inv -> memory -> hs_inv
 

src/phl/ecPhlEager.ml

@@ -168,7 +168,12 @@ let t_eager_seq_r (i, j) s (r2, r1) tc =
 
   let (_, ml_ty), (_, mr_ty) = (eC.es_ml, eC.es_mr) in
   let c1, c2 = s_split env i c and c1', c2' = s_split env j c' in
-  let eqMem1 = eq_on_form_and_stmt env r1 (stmt c1')
+  let h = EcIdent.create "h" in
+  let existsP = EcSubst.ss_inv_exists_ml_ts_inv (h, ml_ty) (es_pr eC) in
+  let eqMem1 =
+    map_ts_inv2 f_and
+      (eq_on_form_and_stmt env r1 (stmt c1'))
+      (ss_inv_generalize_left existsP r1.ml)
   and eqQ1 = eq_on_sided_form env (es_po eC) in
 
   let a =
@@ -243,7 +248,13 @@ let t_eager_while_r i tc =
   if (not (ER.EqTest.for_expr env e (sub_to_left_mem _e))) then
     tc_error !!tc "eager: both while guards must be syntactically equal";
 
-  let eqMem1 = eq_on_form_and_stmt env i c' and eqI = eq_on_sided_form env i in
+  let h = EcIdent.create "h" in
+  let existsI = EcSubst.ss_inv_exists_ml_ts_inv (h, ml_ty) (es_pr es) in
+  let eqMem1 =
+    map_ts_inv2 f_and
+      (eq_on_form_and_stmt env i c')
+      (ss_inv_generalize_left existsI i.ml)
+  and eqI = eq_on_sided_form env i in
 
   let el = ss_inv_of_expr ml e and er = ss_inv_of_expr mr e in
 

src/phl/ecPhlEager.mli

@@ -10,14 +10,15 @@ val process_seq : pcodegap1 pair -> pstmt -> pformula doption -> backward
     {v
   (a) S; c₁ ~ c₁'; S : P ==> R₂
   (b) S; c₂ ~ c₂'; S : R₁ ==> Q
-  (c) c₁' ~ c₁' : Eq ==> R₁
+  (c) c₁' ~ c₁' : Eq /\ ∃m. P m m₂ ==> R₁
   (d) c₂ ~ c₂ : R₂ ==> ={Q.1}
  -----------------------------------
   S; c₁; c₂ ~ c₁'; c₂'; S : P ==> Q
     v}
     where [R₁] and [R₂] are provided manually (and equal if a single value was
     provided), as well as [S]. The predicate [={Q.1}] means equality on all free
-    variables bound to the first memory in [Q]. *)
+    variables bound to the first memory in [Q]. Memory [m₂] is the implicitly
+    lambda-quantified memory of the right program. *)
 
 val t_eager_seq : codegap1 pair -> stmt -> ts_inv pair -> backward
 (** Internal variant of [eager seq] *)
@@ -43,15 +44,15 @@ val process_while : pformula -> backward
   (a) I => ={e, I.1}
   (b) S; c ~ c'; S : I /\ e{1} ==> I
   (c) forall b &2, S : e = b ==> e = b
-  (d) c' ~ c' : Eq ==> I
+  (d) c' ~ c' : Eq /\ ∃m. I m m₂ ==> I
   (e) c ~ c : I ==> I
   (f) S ~ S : I /\ !e{1} ==> I
  --------------------------------------------------------
   S; while e do c ~ while e do c'; S : I ==> I /\ !e{1}
     v}
-    Where the invariant [I] is manually provided.
-    Please note that the guard [e] is syntactically identical in both
-    programs. *)
+    Where the invariant [I] is manually provided. Please note that the guard [e]
+    is syntactically identical in both programs. Memory [m₂] is the implicitly
+    lambda-quantified memory of the right program. *)
 
 val t_eager_while : ts_inv -> backward
 (** Internal variant of [eager while] *)