diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 18:59:00 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 18:59:00 +0100 |
| commit | 5e569a91cbdf0357cc2df3fb542291e2ba2a8f70 (patch) | |
| tree | 8f3b8b537fc4a2f7fc91d1c076c265392c6724e0 /backend/CSE3proof.v | |
| parent | 2e47c928161eebb252fea056495a70d22884efc9 (diff) | |
| download | compcert-kvx-5e569a91cbdf0357cc2df3fb542291e2ba2a8f70.tar.gz compcert-kvx-5e569a91cbdf0357cc2df3fb542291e2ba2a8f70.zip | |
progress on inductiveness proof
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 20 |
1 files changed, 18 insertions, 2 deletions
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. |