Address issue #773 by removing the problematic line in normalize1

PrincetonUniversity · May 7, 2024 · 4cd0f6c · 4cd0f6c
1 parent 36d993e
commit 4cd0f6c
Show file tree

Hide file tree

Showing 11 changed files with 18 additions and 9 deletions.
diff --git a/floyd/call_lemmas.v b/floyd/call_lemmas.v
@@ -1534,6 +1534,7 @@ Proof.
     apply bi.pure_mono; simpl; auto.
   - apply bi.exist_elim; intros.
     rewrite /PROPx /=.
+    split => rho; monPred.unseal.
     normalize.
 Qed.
 

diff --git a/floyd/client_lemmas.v b/floyd/client_lemmas.v
@@ -694,6 +694,7 @@ Proof.
 unfold PROPx in *.
 intros.
 rewrite fold_right_cons.
+go_lowerx.
 normalize.
 rewrite -H //.
 monPred.unseal.

diff --git a/floyd/forward.v b/floyd/forward.v
@@ -4455,8 +4455,10 @@ Lemma compute_close_precondition_entails2:
   close_precondition ids (PROPx P (LAMBDAx gv vals (SEPx R)))
   ⊢  (PROPx(Σ:=Σ) P (LOCALx ((map gvars gv)++Q) (SEPx R))).
 Proof.
-intros. rewrite <- insert_locals. unfold close_precondition; normalize. raise_rho. super_unfold_lift. 
-unfold GLOBALSx, PARAMSx, argsassert2assert, PROPx, LOCALx, SEPx. normalize.
+intros. rewrite <- insert_locals. 
+  unfold close_precondition; split => rho; monPred.unseal; normalize. raise_rho. super_unfold_lift.
+ unfold GLOBALSx, PARAMSx, argsassert2assert, PROPx, LOCALx, SEPx.
+  normalize. 
   apply bi.and_intro; [|by done].
   rewrite bi.pure_and; apply bi.and_intro.
   { apply bi.pure_intro.

diff --git a/floyd/forward_lemmas.v b/floyd/forward_lemmas.v
@@ -388,7 +388,8 @@ destruct Post as [?P ?P ?P ?P]; simpl; normalize.
 intros vl; destruct Post as [?P ?P ?P ?P]; simpl; normalize.
 *
 eapply semax_pre_simple; [ | apply semax_break].
-destruct Post as [?P ?P ?P ?P]; simpl; normalize.
+destruct Post as [?P ?P ?P ?P]; simpl.
+split => rho; monPred.unseal; normalize.
 eapply derives_trans; [ | apply H1].
 rewrite (bi.and_comm (Q rho)).
 simpl.

diff --git a/floyd/go_lower.v b/floyd/go_lower.v
@@ -448,6 +448,7 @@ Proof.
   intros.
   erewrite local2ptree_soundness by eassumption.
   rewrite assoc msubst_eval_lvalue_eq //.
+  split => rho; monPred.unseal.
   normalize.
   apply bi.pure_elim_r; intros ->; done.
 Qed.
@@ -460,6 +461,7 @@ Proof.
   intros.
   erewrite local2ptree_soundness by eassumption.
   rewrite assoc msubst_eval_expr_eq //.
+  split => rho; monPred.unseal.
   normalize.
   apply bi.pure_elim_r; intros ->; done.
 Qed.

diff --git a/floyd/loadstore_mapsto.v b/floyd/loadstore_mapsto.v
@@ -344,6 +344,7 @@ Proof.
     with (eval_expr (Ecast e2 t1)).
     Opaque eval_lvalue eval_expr.
     unfold local, lift1; unfold_lift; simpl.
+    go_lowerx.
     normalize.
     Transparent eval_lvalue eval_expr.
     subst t1.

diff --git a/floyd/local2ptree_denote.v b/floyd/local2ptree_denote.v
@@ -437,10 +437,8 @@ Lemma LOCALx_shuffle_derives': forall P Q Q' R,
 Proof.
   intros.
   induction Q'.
-  {
-    unfold PROPx, LOCALx.
+  { go_lowerx.
     normalize.
-    solve_andp.
   }
   pose proof (H a (or_introl _ eq_refl)).
   rewrite <- insert_local'.
@@ -841,8 +839,9 @@ assert (forall rho, local(Σ:=Σ) (tc_environ Delta) rho ⊢ ⌜Map.get (ve_of r
 clear - H2 H2' H3 TC.
 rewrite -insert_SEP.
 unfold func_ptr.
+split => rho; monPred.unseal.
 normalize.
-iIntros "(%H0 & H1 & H2)". iSplit. 2: { done. }
+iIntros "(%H0 & H1 & H2)".  iSplit. 2: { done. }
 rewrite H3.
 iPoseProof (in_local _ Delta (l ++ P) _ (SEPx R) H2 with "[H1]") as "H3".
 { rewrite /PROPx /LOCALx. iSplit;  done. }

diff --git a/floyd/local2ptree_typecheck.v b/floyd/local2ptree_typecheck.v
@@ -130,6 +130,7 @@ Proof.
     - eapply derives_trans; [eapply msubst_eval_expr_eq; eauto |].
       apply bi.impl_intro_r.
       unfold local, lift1; unfold_lift.
+      split => rho; monPred.unseal;
       normalize.
     - and_elim_rightmost.
   + simpl msubst_denote_tc_assert; simpl denote_tc_assert.

diff --git a/floyd/sc_set_load_store.v b/floyd/sc_set_load_store.v
@@ -85,6 +85,7 @@ Proof.
   rewrite <- insert_local.
   eapply derives_trans; [| apply bi.and_mono; [apply derives_refl | apply remove_localdef_temp_PROP]].
   (* TODO maybe normalize shouldn't unfold local? *)
+  split => rho; monPred.unseal.
   Opaque local. normalize. Transparent local.
   apply (bi.exist_intro' _ _ x).
   rewrite bi.and_comm -bi.and_assoc bi.and_comm.

diff --git a/floyd/seplog_tactics.v b/floyd/seplog_tactics.v
@@ -1332,7 +1332,9 @@ Ltac safe_done :=
 
 Ltac normalize1 :=
          match goal with
+         (* SEE ISSUE   https://github.com/PrincetonUniversity/VST/issues/773
             | |- bi_entails(PROP := monPredI _ _) _ _ => let rho := fresh "rho" in split => rho; monPred.unseal
+	  *)
             | |- context [((⌜?P⌝ ∧ ?Q) ∗ ?R)%I] => rewrite -> (sepcon_andp_prop' Q P R)
             | |- context [(?P ∗ (⌜?Q⌝ ∧ ?R))%I] => rewrite -> (sepcon_andp_prop P Q R)
             | |- context [((?Q ∧ ⌜?P⌝) ∗ ?R)%I] => rewrite -> (sepcon_andp_prop2' P Q R)

diff --git a/progs64/verif_io.v b/progs64/verif_io.v
@@ -222,7 +222,6 @@ Proof.
     entailer!.
   - forward.
     entailer!.
-  - entailer!.
 Qed.
 
 Lemma chars_of_Z_eq : forall n, chars_of_Z n =
@@ -269,7 +268,6 @@ Proof.
   - forward_call (i, tr).
     { rewrite -> chars_of_Z_intr by lia; cancel. }
     entailer!.
-  - entailer!.
 Qed.
 
 Lemma read_sum_eq : forall n d, read_sum n d ≈