suggestion of translation from find_bblock to find_instr

1 files changed, 22 insertions, 0 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 6b73c5d6..342b98d0 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -75,6 +75,28 @@ Lemma functions_translated:
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
 Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
+Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop :=
+  | is_nth_label l: 
+     list_nth_z (header bb) n = Some l -> 
+     i = Asm.Plabel l ->
+     is_nth_inst bb n i
+  | is_nth_basic bi: 
+     list_nth_z (body bb) (n - list_length_z (header bb)) = Some bi ->
+     basic_to_instruction bi = OK i ->
+     is_nth_inst bb n i
+  | is_nth_ctlflow cfi:
+     (exit bb) = Some cfi ->
+     n = size bb - 1 ->
+     i = control_to_instruction cfi ->
+     is_nth_inst bb n i.
+
+Lemma find_bblock_find_instr_correct pos n lb tlb bb:
+  find_bblock pos lb = Some bb -> 
+  unfold lb = OK tlb ->
+  0 <= n < size bb ->
+  exists i, is_nth_inst bb n i /\ Asm.find_instr (pos+n) tlb = Some i.
+Admitted.
+
 (* Asmblock and Asm share the same definition of state *)
 Definition match_states (s1 s2 : state) := s1 = s2.