From 1685bfd6d017a487368ceb3c71cfaf03c9d42c9b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 23 Nov 2020 23:53:22 +0100 Subject: Start of the postpasschedproof, redefining verify schedule lemmas --- aarch64/Asmblockgenproof0.v | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'aarch64/Asmblockgenproof0.v') diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 92c0aa58..172e770d 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -394,7 +394,7 @@ Proof. induction c; simpl; intros. discriminate. destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib. Qed. - +*) (* inspired from Asmgenproof0 *) (* ... skip ... *) @@ -409,11 +409,14 @@ Inductive code_tail: Z -> bblocks -> bblocks -> Prop := code_tail pos c1 c2 -> code_tail (pos + (size bi)) (bi :: c1) c2. +(* Lemma code_tail_pos: forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. Proof. - induction 1. omega. generalize (size_positive bi); intros; omega. -Qed. + induction 1. omega. + Admitted. +(* TODO How to import this module? generalize (bblock_size_pos bi); intros; omega. +Qed. *) Lemma find_bblock_tail: forall c1 bi c2 pos, @@ -424,11 +427,13 @@ Proof. inversion H. destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega. destruct (zeq pos 0). subst pos. - inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega. + inv H. auto. + Admitted. +(* TODO same as above generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega. inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega. eauto. Qed. - + *) Local Hint Resolve code_tail_0 code_tail_S: core. -- cgit