diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 20:56:49 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 20:56:49 +0100 |
| commit | 7e4b3b10367e71e74b8eca57d94e4413336411bf (patch) | |
| tree | eeba336ea92df6a1f21f9320fed96207e5970788 /backend/CSE3proof.v | |
| parent | 1e2fc0d53845b530e14a3c5293fbadfaf8285c35 (diff) | |
| download | compcert-kvx-7e4b3b10367e71e74b8eca57d94e4413336411bf.tar.gz compcert-kvx-7e4b3b10367e71e74b8eca57d94e4413336411bf.zip | |
moving forward in proofs
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 6744ee93..3fbac9ea 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -402,6 +402,17 @@ Proof. Qed. Hint Resolve sem_rhs_sload_notrap2 : cse3. + +Lemma sem_rel_top: + forall ctx sp rs m, sem_rel (genv:=ge) (sp:=sp) (ctx:=ctx) RELATION.top rs m. +Proof. + unfold sem_rel, RELATION.top. + intros. + rewrite HashedSet.PSet.gempty in *. + discriminate. +Qed. + +Hint Resolve sem_rel_top : cse3. Ltac IND_STEP := match goal with @@ -476,6 +487,7 @@ Proof. * admit. + econstructor; eauto. IND_STEP. + apply store_sound with (a0:=a) (m0:=m); eauto with cse3. - (* Icall *) destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. @@ -499,7 +511,8 @@ Proof. * eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. * eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. - eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. + * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt. + * IND_STEP. - (* Icond *) econstructor. split. + eapply exec_Icond; try eassumption. @@ -507,12 +520,17 @@ Proof. admit. * reflexivity. + econstructor; eauto. + destruct b; IND_STEP. + - (* Ijumptable *) econstructor. split. + eapply exec_Ijumptable; try eassumption. erewrite transf_function_at by eauto. simpl. admit. + econstructor; eauto. + assert (In pc' tbl) as IN_LIST by (eapply list_nth_z_in; eassumption). + IND_STEP. + - (* Ireturn *) destruct or. -- econstructor. split. @@ -556,6 +574,7 @@ Proof. assumption. * apply checked_is_inductive_allstep. apply transf_function_invariants_inductive with (tf:=tf); auto. + - (* external *) simpl in FUN. inv FUN. |