Merge branch 'vst_on_iris' of https://github.com/PrincetonUniversity/VST

 into vst_on_iris

progs64/verif_append2.v

@@ -210,7 +210,7 @@ forward_if.
    iIntros "[H1 H2]".
    iIntros (cts2) "H3".
    iSpecialize ("H2" $! (a :: cts2)).
-   rewrite app_ass.
+   rewrite -app_assoc.
    iApply ("H2").
    unfold listrep at -1; fold listrep. iExists u0. iFrame.
  + (* after the loop *)

progs64/verif_bst.v

@@ -312,7 +312,7 @@ Proof.
   rewrite (field_at_data_at _ t_struct_tree [StructField _left]).
   unfold treebox_rep at 1. Exists p1. cancel.
 
-  iIntros "(? & ? & ? & ? & ? & ?) Hleft".
+  iIntros "(? & ? & ? & ?) Hleft".
   clear p1.
   unfold treebox_rep.
   iExists p.
@@ -324,7 +324,7 @@ Proof.
   iFrame.
   unfold_data_at (data_at _ _ _ p).
   rewrite (field_at_data_at _ t_struct_tree [StructField _left]).
-  iFrame.
+  iStopProof; cancel.
 Qed.
 
 Lemma bst_right_entail: forall (t1 t2 t2': tree val) k (v p1 p2 p b: val),
@@ -343,7 +343,7 @@ Proof.
   rewrite (field_at_data_at _ t_struct_tree [StructField _right]).
   unfold treebox_rep at 1. Exists p2. cancel.
 
-  iIntros "(? & ? & ? & ? & ? & ?) Hright".
+  iIntros "(? & ? & ? & ?) Hright".
   clear p2.
   unfold treebox_rep.
   iExists p.
@@ -355,7 +355,7 @@ Proof.
   iFrame.
   unfold_data_at (data_at _ _ _ p).
   rewrite (field_at_data_at _ t_struct_tree [StructField _right]).
-  iFrame.
+  iStopProof; cancel.
 Qed.
 
 Lemma if_trueb: forall {A: Type} b (a1 a2: A), b = true -> (if b then a1 else a2) = a1.
@@ -823,7 +823,7 @@ Lemma subsume_insert:
 Proof.
 do_funspec_sub. destruct w as [[[b x] v] m]. simpl.
 rewrite <- fupd_intro.
-monPred.unseal. Intros.
+Intros.
 destruct args. inv H1.
 destruct args. inv H1.
 destruct args. inv H1.
@@ -842,7 +842,7 @@ Lemma subsume_treebox_new:
 Proof.
 do_funspec_sub.
 rewrite <- fupd_intro.
-monPred.unseal. Intros.
+Intros.
 Exists tt (emp : mpred). entailer!!.
 intros tau ? ?. Exists (eval_id ret_temp tau). entailer!!.
 unfold tmap_rep.
@@ -859,7 +859,7 @@ Lemma subsume_treebox_free:
 Proof.
 do_funspec_sub. destruct w as [m p]. clear H.
 rewrite <- fupd_intro.
-simpl; monPred.unseal. Intros.
+Intros.
 subst.
 unfold env_set, eval_id in *. simpl in *. 
 unfold tmap_rep.

progs64/verif_field_loadstore.v

@@ -1,14 +1,11 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.field_loadstore.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
-Section Spec.
-
-Context  `{!default_VSTGS Σ}.
-
 Definition t_struct_b := Tstruct _b noattr.
 
 Definition sub_spec (sub_id: ident) :=
@@ -73,5 +70,3 @@ Proof.
   forward.
   entailer!.
 Qed.
-
-End Spec.

progs64/verif_float.v

@@ -1,14 +1,11 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.float.
 
 #[export] Instance CompSpecs : compspecs.
 Proof. make_compspecs prog. Defined.
 
-Section Spec.
-
-Context  `{!default_VSTGS Σ}.
-
 Definition main_spec :=
  DECLARE _main
   WITH gv: globals
@@ -40,8 +37,8 @@ unfold data_at.
 entailer!.
 simpl.
 unfold field_at, data_at_rec, at_offset. simpl.
-  repeat (rewrite ->prop_true_andp by (auto with field_compatible)).
-fold noattr; fold tint; fold tfloat; fold tdouble. 
+  repeat (rewrite prop_true_andp by (auto with field_compatible)).
+fold noattr; fold tint; fold tfloat; fold tdouble.
 repeat match goal with |- context [field_offset ?A ?B ?C] =>
   set (aa :=field_offset A B C); compute in aa; subst aa
 end.
@@ -58,5 +55,3 @@ forward.
 forward.
 forward.
 Qed.
-
-End Spec.

progs64/verif_global.v

@@ -1,14 +1,11 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.global.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs.  mk_varspecs prog. Defined.
 
-Section Spec.
-
-Context `{!default_VSTGS Σ}.
-
 Definition h_spec :=
  DECLARE _h
   WITH gv: globals
@@ -44,5 +41,3 @@ rewrite data_at_tuint_tint.
 forward_call gv.
 forward.
 Qed.
-
-End Spec.

progs64/verif_incr.v

@@ -1,4 +1,3 @@
-(* Do not edit this file, it was generated automatically *)
 Require Import VST.concurrency.conclib.
 Require Import VST.concurrency.lock_specs.
 Require Import VST.atomics.SC_atomics.

progs64/verif_logical_compare.v

@@ -1,18 +1,18 @@
 (* Do not edit this file, it was generated automatically *)
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.logical_compare.
-Import -(notations) compcert.lib.Maps.
 
 #[export] Instance CompSpecs : compspecs. Proof. make_compspecs prog. Defined.
 
 (****  START *)
+
 Definition logical_and_result v1 v2 : int :=
    if Int.eq v1 Int.zero then Int.zero else v2.
 
 Definition logical_or_result v1 v2 : int :=
   if Int.eq v1 Int.zero then v2 else Int.one.
 
-Print attr.
 Fixpoint quick_shortcut_logical (s: statement) : option ident :=
 match s with
 | Sifthenelse _
@@ -68,14 +68,14 @@ match s with
 end.
 
 Lemma semax_shortcut_logical:
-  forall {Espec : ext_spec unit} {cs: compspecs} Delta P Q R tid s v Qtemp Qvar GV el,
+  forall Espec {cs: compspecs} E Delta P Q R tid s v Qtemp Qvar GV el,
    quick_shortcut_logical s = Some tid ->
    typeof_temp Delta tid = Some tint ->
    local2ptree Q = (Qtemp, Qvar, nil, GV) ->
    Qtemp !! tid = None ->
    shortcut_logical (msubst_eval_expr Delta Qtemp Qvar GV) tid s = Some (v, el) ->
-   ENTAIL Delta, PROPx P (LOCALx Q (SEPx R)) ⊢ fold_right (fun e q => tc_expr Delta e ∧ q) True el ->
-   semax ⊤ Delta (PROPx P (LOCALx Q (SEPx R)))
+   ENTAIL Delta, PROPx P (LOCALx Q (SEPx R)) |-- fold_right (fun e q => tc_expr Delta e && q) TT el ->
+   semax(OK_spec := Espec)(C := cs) E Delta (PROPx P (LOCALx Q (SEPx R)))
           s (normal_ret_assert (PROPx P (LOCALx (temp tid (Vint v) :: Q) (SEPx R)))).
 Admitted.
 

progs64/verif_message.v

@@ -1,5 +1,6 @@
 (* Do not edit this file, it was generated automatically *)
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.message.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.

progs64/verif_min.v

@@ -9,6 +9,7 @@
 *)
 
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.min.
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs.  mk_varspecs prog. Defined.
@@ -30,7 +31,7 @@ destruct H.
 subst a.
 simpl.
 apply Z.le_min_l.
-simpl. rewrite ->Z.le_min_r.
+simpl. rewrite Z.le_min_r.
 apply IHal.
 apply H.
 Qed.
@@ -78,10 +79,6 @@ Qed.
 #[export] Hint Extern 3 (is_int I32 _ (Znth _ (map Vint _))) =>
   (apply  is_int_I32_Znth_map_Vint; rewrite ?Zlength_map; lia) : core.
 
-Section Spec.
-
-Context `{!default_VSTGS Σ}.
-
 Definition minimum_spec :=
  DECLARE _minimum
   WITH a: val, n: Z, al: list Z
@@ -105,13 +102,12 @@ start_function.
 assert_PROP (Zlength al = n) by (entailer!; list_solve).
 forward.  (* min = a[0]; *)
 forward_for_simple_bound n
-  (∃ i:Z,
+  (EX i:Z,
     PROP()
     LOCAL(temp _min (Vint (Int.repr (fold_right Z.min (Znth 0 al) (sublist 0 i al))));
           temp _a a;
           temp _n (Vint (Int.repr n)))
     SEP(data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)).
-
 * (* Prove that the precondition implies the loop invariant *)
   entailer!!.
 * (* Prove that the loop body preserves the loop invariant *)
@@ -124,8 +120,8 @@ forward_for_simple_bound n
           |apply Forall_sublist; auto]).
  autorewrite with sublist.
  subst POSTCONDITION; unfold abbreviate.
- rewrite ->(sublist_split 0 i (i+1)) by lia.
- rewrite ->(sublist_one i (i+1) al) by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
+ rewrite (sublist_one i (i+1) al) by lia.
  rewrite fold_min_another.
  forward_if.
  +
@@ -177,8 +173,8 @@ rename a0 into i.
  autorewrite with sublist.
  apply semax_post_flipped' with (Inv 1 (Z.gt n) i).
  unfold Inv.
- rewrite -> (sublist_split 0 i (i+1)) by lia.
- rewrite -> (sublist_one i (i+1) al) by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
+ rewrite (sublist_one i (i+1) al) by lia.
  rewrite fold_min_another.
  forward_if.
  +
@@ -188,8 +184,7 @@ rename a0 into i.
  forward. (* skip; *)
  entailer!!. rewrite Z.min_l; auto; lia.
  +
- intros.
- Exists i. apply ENTAIL_refl.
+Exists i. apply ENTAIL_refl.
 *
  rename a0 into i.
  forward.
@@ -208,7 +203,7 @@ Definition minimum_spec2 :=
     PARAMS (a; Vint (Int.repr n))
     SEP   (data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)
   POST [ tint ]
-   ∃ j: Z,
+   EX j: Z,
     PROP (In j al; Forall (fun x => j<=x) al)
     RETURN (Vint (Int.repr j))
     SEP   (data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a).
@@ -222,7 +217,7 @@ start_function.
 assert_PROP (Zlength al = n) by (entailer!; list_solve).
 forward.  (* min = a[0]; *)
 forward_for_simple_bound n
-  (∃ i:Z, ∃ j:Z,
+  (EX i:Z, EX j:Z,
     PROP(
          In j (sublist 0 (Z.max 1 i) al);
          Forall (Z.le j) (sublist 0 i al))
@@ -235,7 +230,7 @@ forward_for_simple_bound n
 Exists (Znth 0 al).
 autorewrite with sublist.
 entailer!!.
-rewrite -> sublist_one by lia.
+rewrite sublist_one by lia.
 constructor; auto.
 * (* Show that the loop body preserves the loop invariant *)
 Intros.
@@ -250,9 +245,9 @@ forward_if.
  forward. (* min = j; *)
  Exists (Znth i al).
  entailer!!.
- rewrite -> Z.max_r by lia.
- rewrite -> (sublist_split 0 i (i+1)) by lia.
- rewrite -> (sublist_one i (i+1) al) by lia.
+ rewrite Z.max_r by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
+ rewrite (sublist_one i (i+1) al) by lia.
  split.
  apply in_app; right; constructor; auto.
  apply Forall_app; split.
@@ -263,23 +258,21 @@ forward_if.
  forward. (* skip; *)
  Exists j.
  entailer!!.
- rewrite -> Z.max_r by lia.
+ rewrite Z.max_r by lia.
  split.
  destruct (zlt 1 i).
- rewrite -> Z.max_r in H3 by lia.
- rewrite -> (sublist_split 0 i (i+1)) by lia.
+ rewrite Z.max_r in H3 by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
  apply in_app; left; auto.
- rewrite -> Z.max_l in H3 by lia.
- rewrite -> (sublist_split 0 1 (i+1)) by lia.
+ rewrite Z.max_l in H3 by lia.
+ rewrite (sublist_split 0 1 (i+1)) by lia.
  apply in_app; left; auto.
- rewrite -> (sublist_split 0 i (i+1)) by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
  apply Forall_app. split; auto.
- rewrite -> sublist_one by lia.
+ rewrite sublist_one by lia.
  repeat constructor. lia.
 * (* After the loop *)
  Intros x.
  autorewrite with sublist in *.
  forward. (* return *)
 Qed.
-
-End Spec.

progs64/verif_min64.v

@@ -5,7 +5,8 @@
     forward store with 64-bit integer array subscript.
 *)
 
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.min64.
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs.  mk_varspecs prog. Defined.
@@ -27,7 +28,7 @@ destruct H.
 subst a.
 simpl.
 apply Z.le_min_l.
-simpl. rewrite -> Z.le_min_r.
+simpl. rewrite Z.le_min_r.
 apply IHal.
 apply H.
 Qed.

progs64/verif_nest2.v

@@ -1,14 +1,11 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.nest2.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
-Section Spec.
-
-Context `{!default_VSTGS Σ}.
-
 Definition t_struct_b := Tstruct _b noattr.
 
 Definition get_spec :=
@@ -78,5 +75,3 @@ unfold_repinj.
 Time forward. (* 1.23 sec *)
 entailer!!.
 Time Qed.  (*  28 sec -> 3.45 sec *)
-
-End Spec.