Begin proof of exec_exit_simulation_plus

Mostly proving the absurd cases following inversion of is_nth_inst

1 files changed, 42 insertions, 0 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 9e12655a..4b18e712 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -759,6 +759,26 @@ Lemma exec_body_dont_move_PC bb rs m rs' m': forall
   rs PC = rs' PC.
 Admitted.
 
+Lemma list_nth_z_range_exceeded A (l : list A) n:
+  n >= list_length_z l ->
+  list_nth_z l n = None.
+Proof.
+  intros N.
+  remember (list_nth_z l n) as opt eqn:H. symmetry in H.
+  destruct opt; auto.
+  exploit list_nth_z_range; eauto. omega.
+Qed.
+
+Lemma last_instruction_cannot_be_label bb:
+  list_nth_z (header bb) (size bb - 1) = None.
+Proof.
+  assert (list_length_z (header bb) <= size bb - 1). {
+    rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). omega.
+  }
+  remember (list_nth_z (header bb) (size bb - 1)) as label_opt; destruct label_opt; auto;
+  exploit list_nth_z_range; eauto; omega.
+Qed.
+
 Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
@@ -767,6 +787,28 @@ Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall
   (EXIT: exec_exit ge f (Ptrofs.repr (size bb)) rs m (exit bb) t rs' m')
   (ATPC: rs PC = Vptr b ofs),
   plus Asm.step tge s2 t (State rs' m').
+Proof.
+  intros. apply plus_one.
+  exploit internal_functions_unfold; eauto.
+  intros (tc & FINDtf & TRANStf & _).
+
+  exploit (find_instr_bblock (size bb - 1)); eauto.
+  { generalize (bblock_size_pos bb). omega. }
+  intros (i' & NTH & FIND_INSTR).
+  inv NTH.
+  + rewrite last_instruction_cannot_be_label in *. discriminate.
+  + destruct (exit bb) as [ctrl |] eqn:NEMPTY_EXIT'. 2: { contradiction. }
+    rewrite bblock_size_aux in *. rewrite NEMPTY_EXIT' in *. simpl in *.
+    (* XXX: Is there a better way to simplify this expression i.e. automatically? *)
+    replace (list_length_z (header bb) + list_length_z (body bb) + 1 - 1 -
+       list_length_z (header bb)) with (list_length_z (body bb)) in H by omega.
+    rewrite list_nth_z_range_exceeded in H; try omega. discriminate.
+  + destruct cfi.
+    * (* controlf low instruction *)
+      rewrite H in EXIT.
+      inv EXIT.
+      admit.
+    * (* builtin *) admit.
 Admitted.
 
 Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall