Proof of barg_proj_refines_eq

1 files changed, 43 insertions, 5 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index f5821810..f2ead16e 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -1312,6 +1312,47 @@ Proof.
     erewrite IHlist_refines; eauto.
 Qed.
 
+Lemma sval_refines_proj ge ge' sp rs m hsv sv hsv' sv':
+  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
+  sval_refines ge sp rs m hsv sv ->
+  sval_refines ge' sp rs m hsv' sv' ->
+  hsval_proj hsv = hsval_proj hsv' ->
+  seval_sval ge sp sv rs m = seval_sval ge' sp sv' rs m.
+Proof.
+  intros GFS REF REF' PROJ.
+  rewrite <- REF. rewrite <- REF'. unfold seval_hsval.
+  erewrite <- seval_preserved; [| eapply GFS].
+  congruence.
+Qed.
+
+Lemma barg_proj_refines_eq_single ge ge' sp rs0 m0:
+  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
+  forall hsv sv, barg_refines ge sp rs0 m0 hsv sv ->
+  forall hsv' sv', barg_refines ge' sp rs0 m0 hsv' sv' ->
+  barg_proj hsv = barg_proj hsv' ->
+  seval_builtin_sval ge sp sv rs0 m0 = seval_builtin_sval ge' sp sv' rs0 m0.
+Proof.
+  intro GFS. induction 1.
+  all: try (simpl; intros hsv' sv' BREF' BPROJ';
+    destruct hsv'; simpl in BPROJ'; try discriminate;
+    inv BPROJ'; inv BREF'; simpl; try reflexivity;
+    erewrite sval_refines_proj; eauto).
+(* BA_splitlong *)
+  - simpl. intros hsv' sv' BREF' BPROJ'.
+    destruct hsv'; simpl in BPROJ'; try discriminate.
+    inv BPROJ'. inv BREF'. simpl.
+    erewrite IHbarg_refines2; eauto.
+    erewrite IHbarg_refines1. 2: eapply H5.
+    all: eauto.
+(* BA_addptr *)
+  - simpl. intros hsv' sv' BREF' BPROJ'.
+    destruct hsv'; simpl in BPROJ'; try discriminate.
+    inv BPROJ'. inv BREF'. simpl.
+    erewrite IHbarg_refines2; eauto.
+    erewrite IHbarg_refines1. 2: eapply H5.
+    all: eauto.
+Qed.
+
 Lemma barg_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv,
   (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
   list_forall2 (barg_refines ge sp rs0 m0) lhsv lsv ->
@@ -1326,12 +1367,9 @@ Proof.
   - simpl. intros. destruct lhsv'; try discriminate.
     simpl in H2. inv H2. destruct lsv'; [inv H|].
     inv H. simpl.
-    assert (SVALEQ: seval_builtin_sval ge sp b1 rs0 m0 = seval_builtin_sval ge' sp b0 rs0 m0). {
-      admit.
-(*       rewrite <- H10. rewrite <- H1. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence. *)
-    } rewrite SVALEQ.
+    erewrite barg_proj_refines_eq_single; eauto.
     erewrite IHlist_forall2; eauto.
-Admitted.
+Qed.
 
 Definition final_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (f1 f2: sfval): Prop :=
   match f1 with