From a3be6358778bb02b03b62486a60b9fd9ef1f1c04 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 12 Mar 2020 11:37:59 +0100
Subject: more lemmas

---
 backend/CSE3analysisproof.v | 38 ++++++++++++++++++++++++++++++++++++--
 1 file changed, 36 insertions(+), 2 deletions(-)

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 7ef44c22..f5dd7bf9 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -7,6 +7,7 @@ Require Import Globalenvs Values.
 Require Import Linking Values Memory Globalenvs Events Smallstep.
 Require Import Registers Op RTL.
 Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet.
+Require Import RTLtyping.
 Require Import Lia.
 
 Theorem loadv_storev_really_same:
@@ -644,10 +645,10 @@ Section SOUNDNESS.
   Hint Resolve oper_sound : cse3.
 
   Theorem store2_sound:
-    forall chunk addr args a src rel rs m m' v,
+    forall chunk addr args a src rel rs m m',
       sem_rel rel rs m ->
       eval_addressing genv sp addr (rs ## args) = Some a ->
-      Mem.storev chunk m a v = Some m' ->
+      Mem.storev chunk m a (rs # src) = Some m' ->
       sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m'.
   Proof.
     unfold store2.
@@ -656,4 +657,37 @@ Section SOUNDNESS.
   Qed.
   
   Hint Resolve store2_sound : cse3.
+
+  Theorem store1_sound:
+    forall no chunk addr args a src rel tenv rs m m',
+      sem_rel rel rs m ->
+      wt_regset tenv rs ->
+      eval_addressing genv sp addr (rs ## args) = Some a ->
+      Mem.storev chunk m a (rs#src) = Some m' ->
+      sem_rel (store1 (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'.
+  Proof.
+    unfold store1.
+    intros until m'.
+    intros REL WT ADDR STORE.
+    assert (sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m') as REL' by eauto with cse3.
+    destruct loadv_storev_compatible_type eqn:COMPATIBLE.
+    2: auto; fail.
+    destruct eq_find as [eq_id | ] eqn:FIND.
+    2: auto; fail.
+    intros i eq CONTAINS CATALOG.
+    destruct (peq i eq_id).
+    { subst i.
+      rewrite eq_find_sound with (no:=no) (eq0:={| eq_lhs := src; eq_op := SLoad chunk addr; eq_args := args |}) in CATALOG; trivial.
+      inv CATALOG.
+      unfold sem_eq.
+      simpl.
+      rewrite ADDR.
+      rewrite loadv_storev_really_same with (m1:=m) (v:=rs#src) (ty:=(tenv src)); trivial.
+    }
+    unfold sem_rel in REL'.
+    rewrite PSet.gaddo in CONTAINS by congruence.
+    eauto.
+  Qed.
+  
+  Hint Resolve store2_sound : cse3.
 End SOUNDNESS.
-- 
cgit