From 1153ff98a18c1730b17444ce3dc4953b886cf9f0 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 20 May 2019 10:23:43 +0200 Subject: m --- mppa_k1c/Machblockgenproof.v | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index f0618cfe..64eeadbc 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -704,10 +704,16 @@ Lemma cfi_dist_end_block i c: (* TODO: raccourcir *) (exists cfi, trans_inst i = MB_cfi cfi) -> dist_end_block_code (i :: c) = 0. Proof. - pose t'. + unfold dist_end_block_code. intro H. destruct H as [cfi H]. - destruct i;simpl in H;try(congruence). - + destruct (e (Mcall s s0) c) as [bl Ht]. + destruct i;simpl in H;try(congruence); ( + remember (trans_code _) as bl; + rewrite <- is_trans_code_inv in Heqbl; + inversion Heqbl; subst; simpl in * |- *; try (reflexivity || congruence)). +Qed. +(* + - simpl. + destruct (e (Mcall s s0) c) as [bl Ht]. unfold dist_end_block_code, trans_code; simpl. rewrite Ht. unfold trans_code_rev, add_to_code; simpl. @@ -743,7 +749,7 @@ Proof. unfold trans_code_rev, add_to_code; simpl. destruct bl; vm_compute; eauto. Qed. - +*) Theorem transf_program_correct: forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog). Proof. -- cgit