From 5e569a91cbdf0357cc2df3fb542291e2ba2a8f70 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 13 Mar 2020 18:59:00 +0100
Subject: progress on inductiveness proof

---
 backend/CSE3proof.v | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index e18456d2..3cc48cca 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -365,6 +365,19 @@ Qed.
 
 Hint Resolve sem_rhs_sop : cse3.
 
+Lemma sem_rhs_sload :
+  forall sp chunk addr rs args m a v,
+  eval_addressing ge sp addr rs ## args = Some a ->
+  Mem.loadv chunk m a = Some v ->
+  sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m v.
+Proof.
+  intros. simpl.
+  rewrite H. rewrite H0.
+  reflexivity.
+Qed.
+
+Hint Resolve sem_rhs_sload : cse3.
+                                                                             
 Ltac IND_STEP :=
         match goal with
         REW: (fn_code ?fn) ! ?mpc = Some ?minstr,
@@ -410,8 +423,11 @@ Proof.
     exists (State ts tf sp pc' (rs # dst <- v) m). split.
     + admit.
     + econstructor; eauto.
-      eapply wt_exec_Iload with (f:=f); try eassumption.
-      eauto with wt.
+      * eapply wt_exec_Iload with (f:=f); try eassumption.
+        eauto with wt.
+      * IND_STEP.
+        apply oper_sound; eauto with cse3.
+        
   - (* Iload notrap1 *)
     exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
     + admit.
-- 
cgit