Proof of exec_body_simulation_plus

Added exec_body_simulation_star' in order to prove it.
exec_body_simulation_star' could also be used to prove
exec_body_simulation_star directly (without using
exec_body_simulation_plus). However, at least the way I did it the proof
turns out to be longer.

eexec_body_simulation_plus is still required/useful for
exec_bblock_simulation.

1 files changed, 238 insertions, 1 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index e656b199..2ee4d476 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -323,6 +323,29 @@ Proof.
   repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). reflexivity.
 Qed.
 
+Lemma list_length_z_cons A hd (tl : list A):
+  list_length_z (hd :: tl) = list_length_z tl + 1.
+Proof.
+  unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity.
+Qed.
+
+Lemma header_size_lt_block_size bb:
+  list_length_z (header bb) < size bb.
+Proof.
+  rewrite bblock_size_aux.
+  generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT].
+  - destruct (body bb); try contradiction; rewrite list_length_z_cons;
+    repeat rewrite length_agree; omega.
+  - destruct (exit bb); try contradiction; simpl; repeat rewrite length_agree; omega.
+Qed.
+
+Lemma body_size_le_block_size bb:
+  list_length_z (body bb) <= size bb.
+Proof.
+  rewrite bblock_size_aux; repeat rewrite length_agree; omega.
+Qed.
+
+
 Lemma bblock_size_pos bb: size bb >= 1.
 Proof.
   rewrite (bblock_size_aux bb).
@@ -955,6 +978,135 @@ Lemma exec_basic_simulation:
                                   rs2 m2 = Next rs2' m2'
                    /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
 Admitted.
+
+Lemma exec_body_simulation_star': forall
+  b ofs f bb tc bis end_of_body rs_start m_start s_start rs_end m_end
+  (ATPC: rs_start PC = Vptr b ofs)
+  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
+  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
+  (MATCHI: match_internal (end_of_body - list_length_z bis) (State rs_start m_start) s_start)
+  (BOUNDED: 0 <= Ptrofs.unsigned ofs + end_of_body <= Ptrofs.max_unsigned
+            /\ list_length_z bis <= end_of_body)
+  (UNFOLD: unfold (fn_blocks f) = OK tc)
+  (FINDBI: forall n : nat, (n < length bis)%nat ->
+          exists (i : Asm.instruction) (bi : basic),
+             list_nth_z bis (Z.of_nat n) = Some bi
+          /\ basic_to_instruction bi = OK i
+          /\ Asm.find_instr (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis) + Z.of_nat n) tc = Some i)
+  (BODY: exec_body lk ge bis rs_start m_start = Next rs_end m_end),
+  exists s_end, star Asm.step tge s_start E0 s_end
+             /\ match_internal end_of_body (State rs_end m_end) s_end.
+Proof.
+  induction bis as [| bi_next bis IH].
+  - intros; eexists; split.
+    + apply star_refl.
+    + inv BODY;
+      unfold list_length_z in MATCHI; simpl in MATCHI; rewrite Z.sub_0_r in MATCHI;
+      assumption.
+  - intros.
+    exploit internal_functions_unfold; eauto.
+    intros (x & FINDtf & TRANStf & _).
+    assert (x = tc) by congruence; subst x.
+
+    assert (FINDBI' := FINDBI).
+    specialize (FINDBI' 0%nat).
+    destruct FINDBI' as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))); try (simpl; omega).
+    inversion NTHBI; subst bi_next'.
+    simpl in BODY; destruct exec_basic as [s_next|] eqn:BASIC; try discriminate.
+
+    destruct s_next as (rs_next & m_next); simpl in BODY.
+    destruct s_start as (rs_start' & m_start').
+    exploit exec_basic_simulation; eauto.
+    intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT).
+    exploit exec_basic_dont_move_PC; eauto; intros AGPC.
+    inversion MI_NEXT as [? ? ? ? ? M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT OFS_NEXT RS RS']; subst.
+    rewrite ATPC in AGPC; symmetry in AGPC, ATPC_NEXT.
+
+    inversion MATCHI as [? ? ? ? ? M_AGREE RS_AGREE ATPC' OFS RS RS']; subst.
+    symmetry in ATPC'. unfold list_length_z in ATPC'.
+    simpl in ATPC'. rewrite list_length_add_acc in ATPC'.
+    rewrite ATPC in ATPC'.
+    unfold Val.offset_ptr in ATPC'.
+    simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
+    unfold list_length_z in FIND_INSTR; simpl in FIND_INSTR.
+    rewrite list_length_add_acc in FIND_INSTR.
+
+    destruct BOUNDED as [(? & LT_MAX) LT_END_OF_BODY].
+    assert (list_length_z bis < end_of_body).
+    { unfold list_length_z in LT_END_OF_BODY; simpl in LT_END_OF_BODY;
+      rewrite list_length_add_acc in LT_END_OF_BODY; omega. }
+    generalize (Ptrofs.unsigned_range_2 ofs); intros.
+    exploit (Asm.exec_step_internal tge b
+             (Ptrofs.add ofs (Ptrofs.repr (end_of_body - (list_length_z bis + 1))))
+             {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}
+             i_next rs_start' m_start'); eauto.
+    { unfold Ptrofs.add; repeat (rewrite Ptrofs.unsigned_repr);
+      try (split; try omega; rewrite length_agree; omega).
+      rewrite Z.add_sub_assoc; assumption. }
+    intros STEP_NEXT.
+
+    unfold list_length_z in MI_NEXT; simpl in MI_NEXT.
+    rewrite list_length_add_acc in MI_NEXT.
+    (* XXX use better tactics *)
+    replace (end_of_body - (list_length_z bis + 1) + 1)
+       with (end_of_body - list_length_z bis) in MI_NEXT by omega.
+    assert (0 <= Ptrofs.unsigned ofs + end_of_body <= Ptrofs.max_unsigned
+            /\ list_length_z bis <= end_of_body). { split; omega. }
+    exploit IH; eauto.
+    { (* XXX *)
+      intros n NLT.
+      assert (NLT': (n + 1 < length (bi_next :: bis))%nat). { simpl; omega. }
+      specialize (FINDBI (n + 1)%nat NLT').
+      unfold list_length_z in FINDBI. simpl in FINDBI. rewrite list_length_add_acc in FINDBI.
+      destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e. simpl in e. omega. }
+      unfold list_length_z in FINDBI. simpl in FINDBI. rewrite list_length_add_acc in FINDBI.
+      rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI. rewrite Z.add_0_r in FINDBI.
+      replace (Ptrofs.unsigned ofs + end_of_body - (list_length_z bis + 1) + (Z.of_nat n + 1))
+         with (Ptrofs.unsigned ofs + end_of_body - list_length_z bis + Z.of_nat n) in FINDBI by omega.
+      replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega.
+      assumption. }
+    intros IH'.
+    destruct IH' as (? & STEP_REST & MATCH_REST).
+
+    eexists; split.
+    + eapply star_step; eauto.
+    + info_auto.
+Qed.
+
+Lemma find_basic_instructions b ofs f bb tc: forall
+  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
+  (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
+  (UNFOLD: unfold (fn_blocks f) = OK tc),
+  forall n,
+  (n < length (body bb))%nat ->
+  exists (i : Asm.instruction) (bi : basic),
+     list_nth_z (body bb) (Z.of_nat n) = Some bi
+  /\ basic_to_instruction bi = OK i
+  /\ Asm.find_instr (Ptrofs.unsigned ofs
+                     + (list_length_z (header bb))
+                     + Z.of_nat n) tc
+                     = Some i.
+Proof.
+  intros until n; intros NLT.
+  exploit internal_functions_unfold; eauto.
+  intros (tc' & FINDtf & TRANStf & _).
+  assert (tc' = tc) by congruence; subst.
+    exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto.
+    { unfold size; split.
+      - rewrite length_agree; omega.
+      - repeat (rewrite length_agree). repeat (rewrite Nat2Z.inj_add). omega. }
+    intros (i & NTH & FIND_INSTR).
+    exists i; intros.
+    inv NTH.
+    - (* absurd *) apply list_nth_z_range in H; omega.
+    - exists bi;
+      rewrite Z.add_simpl_l in H;
+      rewrite Z.add_assoc in FIND_INSTR;
+      intuition.
+    - (* absurd *) rewrite bblock_size_aux in H0;
+      rewrite H in H0; simpl in H0; repeat rewrite length_agree in H0; omega.
+Qed.
+
 Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall
   (ATPC: rs PC = Vptr b ofs)
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
@@ -964,7 +1116,92 @@ Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall
   (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
   exists s2', plus Asm.step tge s2 E0 s2'
              /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'.
-Admitted.
+Proof.
+  intros.
+  exploit internal_functions_unfold; eauto.
+  intros (tc & FINDtf & TRANStf & _).
+
+  (* Prove an Asm.step given that body bb is not empty *)
+
+  destruct (body bb) as [| bi bis] eqn:BDY; try contradiction.
+  assert (H: (0 < length (body bb))%nat). { rewrite BDY; simpl; omega. }
+  exploit find_basic_instructions; eauto. clear H. rewrite BDY; intros FINDBI.
+  destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))).
+  inversion NTHBI; subst bi_next'.
+  simpl in BODY. destruct exec_basic as [s_next|] eqn:BASIC; try discriminate.
+
+  destruct s_next as (rs_next & m_next); simpl in BODY.
+  destruct s2 as (rs_start' & m_start').
+  exploit exec_basic_simulation; eauto.
+  intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT).
+  exploit exec_basic_dont_move_PC; eauto. intros AGPC.
+  inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS'].
+  subst A. subst B. subst C. subst D. subst E.
+  rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT.
+
+  inv MATCHI. symmetry in AGPC0.
+  unfold list_length_z in AGPC0.
+  simpl in AGPC0. rewrite list_length_add_acc in AGPC0.
+  rewrite ATPC in AGPC0.
+  unfold Val.offset_ptr in AGPC0.
+  simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR.
+  unfold list_length_z in FIND_INSTR; simpl in FIND_INSTR.
+  rewrite list_length_add_acc in FIND_INSTR.
+  rewrite Z.add_0_r in FIND_INSTR.
+  rewrite Z.add_0_r in AGPC0.
+
+  assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
+    by (eapply size_of_blocks_bounds; eauto).
+  generalize (header_size_lt_block_size bb). rewrite length_agree; intros HEADER_LT.
+  generalize (Ptrofs.unsigned_range_2 ofs). intros (A & B).
+  exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb)))))
+           {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}
+           i_next rs_start' m_start'); eauto.
+  { unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr);
+    try rewrite length_agree; try split; try omega.
+    simpl; rewrite <- length_agree; assumption. }
+  intros STEP_NEXT.
+
+  (* Now, use exec_body_simulation_star' to go the rest of the way 0+ steps *)
+  rewrite AGPC in ATPC_NEXT.
+  unfold Val.offset_ptr in ATPC_NEXT.
+  unfold Ptrofs.add in ATPC_NEXT.
+  rewrite Ptrofs.unsigned_repr in ATPC_NEXT. 2: { rewrite length_agree; split; omega. }
+
+  (* give omega more facts to work with *)
+  assert (list_length_z (header bb) + list_length_z (body bb) <= size bb). {
+    rewrite bblock_size_aux. omega. }
+  generalize (body_size_le_block_size bb). rewrite length_agree. intros.
+  assert (0 <= Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb))
+            <= Ptrofs.max_unsigned
+            /\ list_length_z bis <= list_length_z (header bb) + list_length_z (body bb)).
+  { split; try omega. split; try omega.
+    - rewrite length_agree in H0; repeat (rewrite length_agree); omega.
+    - rewrite BDY. rewrite list_length_z_cons; repeat rewrite length_agree; omega. }
+
+  exploit (exec_body_simulation_star' b ofs
+           f bb tc bis (list_length_z (header bb) + list_length_z (body bb))); eauto.
+  - rewrite BDY. unfold list_length_z. simpl.
+    repeat (rewrite list_length_add_acc). repeat (rewrite Z.add_0_r).
+    rewrite Z.add_assoc. rewrite Z.add_sub_swap. rewrite Z.add_simpl_r.
+    apply MI_NEXT.
+  - rewrite Z.add_assoc.
+    intros n NBOUNDS.
+    rewrite BDY.
+    assert (NBOUNDS': (n + 1 < length (body bb))%nat). { rewrite BDY; simpl; omega. }
+    exploit find_basic_instructions; eauto. rewrite BDY; intros FINDBI.
+    simpl in FINDBI. destruct zeq as [e|]. { rewrite Nat2Z.inj_add in e; simpl in e; omega. }
+    rewrite Nat2Z.inj_add in FINDBI; simpl in FINDBI.
+    replace (Z.pred (Z.of_nat n + 1)) with (Z.of_nat n) in FINDBI by omega.
+    rewrite list_length_z_cons, Z.add_assoc, Z.add_sub_swap, Z.add_simpl_r.
+    replace (Ptrofs.unsigned ofs + list_length_z (header bb) + (Z.of_nat n + 1))
+       with (Ptrofs.unsigned ofs + list_length_z (header bb) + 1 + Z.of_nat n) in FINDBI by omega.
+    assumption.
+  - intros (s_end & STAR_STEP & MI_STAR).
+    eexists s_end; split.
+    + eapply plus_left; eauto.
+    + rewrite bblock_size_aux, Z.add_simpl_r. assumption.
+Qed.
 
 Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall
   (ATPC: rs PC = Vptr b ofs)