diff options
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 0288f11c..1ce519f0 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -457,6 +457,20 @@ Lemma find_instr_bblock_tail: Proof. Admitted. +Lemma list_nth_z_find_label: + forall (ll : list label) il n l, + list_nth_z ll n = Some l -> + Asm.find_instr n ((unfold_label ll) ++ il) = Some (Asm.Plabel l). +Proof. + induction ll. + - intros. inversion H. + - intros. simpl. + destruct (zeq n 0) as [Z | NZ]. + + inversion H as (H'). rewrite Z in H'. simpl in H'. inv H'. reflexivity. + + simpl in H. destruct (zeq n 0). { contradiction. } + apply IHll; auto. +Qed. + Lemma find_instr_bblock: forall n lb pos bb tlb (FINDBB: find_bblock pos lb = Some bb) @@ -480,9 +494,11 @@ Proof. * (* nth instruction is a label *) eexists; split. { eapply is_nth_label; eauto. } rewrite UNFOLD in UNFOLD_cons. inversion UNFOLD_cons. - admit. + symmetry in LBL. + rewrite <- UNFOLD_BBLOCK. + rewrite <- app_assoc. + apply list_nth_z_find_label; auto. * admit. - + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. inversion UNFOLD as (UNFOLD'). apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')). |