From a57ba1a8a0036853cac31d9401a6f71b877e70c1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 8 Sep 2019 14:50:34 +0200 Subject: a couple "Admitted" and the Coq compiles --- mppa_k1c/PostpassSchedulingproof.v | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 21af276b..867c10c5 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -96,36 +96,42 @@ Proof. Qed. Lemma exec_load_offset_pc_var: - forall t rs m rd ra ofs rs' m' v, - exec_load_offset t rs m rd ra ofs = Next rs' m' -> - exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall trap t rs m rd ra ofs rs' m' v, + exec_load_offset trap t rs m rd ra ofs = Next rs' m' -> + exec_load_offset trap t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_reg_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_load_reg t rs m rd ra ro = Next rs' m' -> - exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. + forall trap t rs m rd ra ro rs' m' v, + exec_load_reg trap t rs m rd ra ro = Next rs' m' -> + exec_load_reg trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_regxs_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_load_regxs t rs m rd ra ro = Next rs' m' -> - exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. + forall trap t rs m rd ra ro rs' m' v, + exec_load_regxs trap t rs m rd ra ro = Next rs' m' -> + exec_load_regxs trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - discriminate. + - unfold parexec_incorrect_load in *. + destruct trap; try discriminate. + inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. Qed. Lemma exec_load_offset_q_pc_var: -- cgit