diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-23 23:53:22 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-23 23:53:22 +0100 |
| commit | 1685bfd6d017a487368ceb3c71cfaf03c9d42c9b (patch) | |
| tree | 399b9a64b88b2375363fed789b299f6194f05351 /aarch64/Asmblockgenproof0.v | |
| parent | f0b44f733f49dc77d2acda09d99390373048ba50 (diff) | |
| download | compcert-kvx-1685bfd6d017a487368ceb3c71cfaf03c9d42c9b.tar.gz compcert-kvx-1685bfd6d017a487368ceb3c71cfaf03c9d42c9b.zip | |
Start of the postpasschedproof, redefining verify schedule lemmas
Diffstat (limited to 'aarch64/Asmblockgenproof0.v')
| -rw-r--r-- | aarch64/Asmblockgenproof0.v | 15 |
1 files changed, 10 insertions, 5 deletions
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. |