Finish evaluability proof of RBop

1 files changed, 1 insertions, 190 deletions

diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v
index 1d59216..bd18855 100644
--- a/src/hls/GiblePargenproofForward.v
+++ b/src/hls/GiblePargenproofForward.v
@@ -30,6 +30,7 @@ Require Import vericert.hls.GibleSeq.
 Require Import vericert.hls.GiblePar.
 Require Import vericert.hls.Gible.
 Require Import vericert.hls.GiblePargenproofEquiv.
+Require Import vericert.hls.GiblePargenproofCommon.
 Require Import vericert.hls.GiblePargen.
 Require Import vericert.hls.Predicate.
 Require Import vericert.hls.Abstr.
@@ -80,22 +81,6 @@ Lemma check_dest_l_dec i r :
   {check_dest_l i r = true} + {check_dest_l i r = false}.
 Proof. destruct (check_dest_l i r); tauto. Qed.
 
-Lemma match_states_list :
-  forall A (rs: Regmap.t A) rs',
-  (forall r, rs !! r = rs' !! r) ->
-  forall l, rs ## l = rs' ## l.
-Proof. induction l; crush. Qed.
-
-Lemma PTree_matches :
-  forall A (v: A) res rs rs',
-  (forall r, rs !! r = rs' !! r) ->
-  forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x.
-Proof.
-  intros; destruct (Pos.eq_dec x res); subst;
-  [ repeat rewrite Regmap.gss by auto
-  | repeat rewrite Regmap.gso by auto ]; auto.
-Qed.
-
 Section CORRECTNESS.
 
   Context (prog: GibleSeq.program) (tprog : GiblePar.program).
@@ -147,155 +132,6 @@ all be evaluable.
     econstructor; eauto.
   Qed.
 
-  Lemma storev_valid_pointer1 :
-    forall chunk m m' s d b z,
-      Mem.storev chunk m s d = Some m' ->
-      Mem.valid_pointer m b z = true ->
-      Mem.valid_pointer m' b z = true.
-  Proof using.
-    intros. unfold Mem.storev in *. destruct_match; try discriminate; subst.
-    apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0.
-    eapply Mem.perm_store_1; eauto.
-  Qed.
-
-  Lemma storev_valid_pointer2 :
-    forall chunk m m' s d b z,
-      Mem.storev chunk m s d = Some m' ->
-      Mem.valid_pointer m' b z = true ->
-      Mem.valid_pointer m b z = true.
-  Proof using.
-    intros. unfold Mem.storev in *. destruct_match; try discriminate; subst.
-    apply Mem.valid_pointer_nonempty_perm. apply Mem.valid_pointer_nonempty_perm in H0.
-    eapply Mem.perm_store_2; eauto.
-  Qed.
-
-  Definition valid_mem m m' :=
-    forall b z, Mem.valid_pointer m b z = Mem.valid_pointer m' b z.
-
-  #[global] Program Instance valid_mem_Equivalence : Equivalence valid_mem.
-  Next Obligation. unfold valid_mem; auto. Qed. (* Reflexivity *)
-  Next Obligation. unfold valid_mem; auto. Qed. (* Symmetry *)
-  Next Obligation. unfold valid_mem; eauto. Qed. (* Transitity *)
-
-  Lemma storev_valid_pointer :
-    forall chunk m m' s d,
-      Mem.storev chunk m s d = Some m' ->
-      valid_mem m m'.
-  Proof using.
-    unfold valid_mem. symmetry.
-    intros. destruct (Mem.valid_pointer m b z) eqn:?;
-                     eauto using storev_valid_pointer1.
-    apply not_true_iff_false.
-    apply not_true_iff_false in Heqb0.
-    eauto using storev_valid_pointer2.
-  Qed.
-
-  Lemma storev_cmpu_bool :
-    forall m m' c v v0,
-      valid_mem m m' ->
-      Val.cmpu_bool (Mem.valid_pointer m) c v v0 = Val.cmpu_bool (Mem.valid_pointer m') c v v0.
-  Proof using.
-    unfold valid_mem.
-    intros. destruct v, v0; crush.
-    { destruct_match; crush.
-      destruct_match; crush.
-      destruct_match; crush.
-      apply orb_true_iff in H1.
-      inv H1. rewrite H in H2. rewrite H2 in Heqb1.
-      simplify. rewrite H0 in Heqb1. crush.
-      rewrite H in H2. rewrite H2 in Heqb1.
-      rewrite H0 in Heqb1. crush.
-      destruct_match; auto. simplify.
-      apply orb_true_iff in H1.
-      inv H1. rewrite <- H in H2. rewrite H2 in Heqb1.
-      simplify. rewrite H0 in Heqb1. crush.
-      rewrite <- H in H2. rewrite H2 in Heqb1.
-      rewrite H0 in Heqb1. crush. }
-
-    { destruct_match; crush.
-      destruct_match; crush.
-      destruct_match; crush.
-      apply orb_true_iff in H1.
-      inv H1. rewrite H in H2. rewrite H2 in Heqb1.
-      simplify. rewrite H0 in Heqb1. crush.
-      rewrite H in H2. rewrite H2 in Heqb1.
-      rewrite H0 in Heqb1. crush.
-      destruct_match; auto. simplify.
-      apply orb_true_iff in H1.
-      inv H1. rewrite <- H in H2. rewrite H2 in Heqb1.
-      simplify. rewrite H0 in Heqb1. crush.
-      rewrite <- H in H2. rewrite H2 in Heqb1.
-      rewrite H0 in Heqb1. crush. }
-
-    { destruct_match; auto. destruct_match; auto; crush.
-      { destruct_match; crush.
-        { destruct_match; crush.
-          setoid_rewrite H in H0; eauto.
-          setoid_rewrite H in H1; eauto.
-          rewrite H0 in Heqb. rewrite H1 in Heqb; crush.
-        }
-        { destruct_match; crush.
-          setoid_rewrite H in Heqb0; eauto.
-          rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } }
-      { destruct_match; crush.
-        { destruct_match; crush.
-          setoid_rewrite H in H0; eauto.
-          setoid_rewrite H in H1; eauto.
-          rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush.
-        }
-        { destruct_match; crush.
-          setoid_rewrite H in Heqb0; eauto.
-          rewrite H0 in Heqb0. rewrite H1 in Heqb0; crush. } } }
-  Qed.
-
-  Lemma storev_eval_condition :
-    forall m m' c rs,
-      valid_mem m m' ->
-      Op.eval_condition c rs m = Op.eval_condition c rs m'.
-  Proof using.
-    intros. destruct c; crush.
-    destruct rs; crush.
-    destruct rs; crush.
-    destruct rs; crush.
-    eapply storev_cmpu_bool; eauto.
-    destruct rs; crush.
-    destruct rs; crush.
-    eapply storev_cmpu_bool; eauto.
-  Qed.
-
-  Lemma eval_operation_valid_pointer :
-    forall A B (ge: Genv.t A B) sp op args m m' v,
-      valid_mem m m' ->
-      Op.eval_operation ge sp op args m' = Some v ->
-      Op.eval_operation ge sp op args m = Some v.
-  Proof.
-    intros * VALID OP. destruct op; auto.
-    - destruct cond; auto; cbn in *.
-      + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
-      + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
-    - destruct c; auto; cbn in *.
-      + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
-      + repeat destruct_match; auto. setoid_rewrite <- storev_cmpu_bool in OP; eauto.
-  Qed.
-
-  Lemma bb_memory_consistency_eval_operation :
-    forall A B (ge: Genv.t A B) sp state i state' args op v,
-      step_instr ge sp (Iexec state) i (Iexec state') ->
-      Op.eval_operation ge sp op args (is_mem state) = Some v ->
-      Op.eval_operation ge sp op args (is_mem state') = Some v.
-  Proof.
-    inversion_clear 1; intro EVAL; auto.
-    cbn in *.
-    eapply eval_operation_valid_pointer. unfold valid_mem. symmetry.
-    eapply storev_valid_pointer; eauto.
-    auto.
-  Qed.
-
-  Lemma truthy_dflt :
-    forall ps p,
-      truthy ps p -> eval_predf ps (dfltp p) = true.
-  Proof. intros. destruct p; cbn; inv H; auto. Qed.
-
   Lemma sem_update_Istore :
     forall A rs args m v f ps ctx addr a0 chunk m' v',
       Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr rs ## args = Some a0 ->
@@ -393,20 +229,6 @@ all be evaluable.
       + auto.
   Qed.
 
-  Lemma exists_sem_pred :
-    forall A B C (ctx: @ctx A) s pr r v,
-      @sem_pred_expr A B C pr s ctx r v ->
-      exists r',
-        NE.In r' r /\ s ctx (snd r') v.
-  Proof.
-    induction r; crush.
-    - inv H. econstructor. split. constructor. auto.
-    - inv H.
-      + econstructor. split. constructor. left; auto. auto.
-      + exploit IHr; eauto. intros HH. inversion_clear HH as [x HH']. inv HH'.
-        econstructor. split. constructor. right. eauto. auto.
-  Qed.
-
   Lemma sem_update_Istore_top:
     forall A f p p' f' rs m pr res args p0 state addr a chunk m',
       Op.eval_addressing (ctx_ge state) (ctx_sp state) addr rs ## args = Some a ->
@@ -451,17 +273,6 @@ all be evaluable.
     + auto.
   Qed.
 
-  Definition predicated_not_inP {A} (p: Gible.predicate) (l: predicated A) :=
-    forall op e, NE.In (op, e) l -> ~ PredIn p op.
-
-  Lemma predicated_not_inP_cons :
-    forall A p (a: (pred_op * A)) l,
-      predicated_not_inP p (NE.cons a l) ->
-      predicated_not_inP p l.
-  Proof.
-    unfold predicated_not_inP; intros. eapply H. econstructor. right; eauto.
-  Qed.
-
   Lemma sem_pexpr_not_in :
     forall G (ctx: @ctx G) p0 ps p e b,
       ~ PredIn p p0 ->