From ef0ff5378bacd0edf6ef32bed9ac67db44842d05 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Oct 2020 13:06:57 +0200 Subject: exec_body_simulation_plus_gen proof OK --- aarch64/Asmgenproof.v | 46 +++++++++++++++++++++++++++++++++++----------- 1 file changed, 35 insertions(+), 11 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 87392139..df83e6a7 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1371,6 +1371,24 @@ Proof. eexists; eexists; intuition eauto. Qed. +Lemma header_body_tail_bound: forall (a: basic) (li: list basic) bb ofs + (BOUNDBB : Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) + (BDYLENPOS : 0 <= list_length_z (body bb) - list_length_z (a :: li) < + list_length_z (body bb)), +0 <= list_length_z (header bb) + list_length_z (body bb) - list_length_z (a :: li) <= +Ptrofs.max_unsigned. +Proof. + intros. + assert (HBBPOS: list_length_z (header bb) >= 0) by eapply list_length_z_pos. + assert (HBBSIZE: list_length_z (header bb) < size bb) by eapply header_size_lt_block_size. + assert (OFSBOUND: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. + assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by omega. + unfold size in BBSIZE. + rewrite !Nat2Z.inj_add in BBSIZE. + rewrite <- !list_length_z_nat in BBSIZE. + omega. +Qed. + (* A more general version of the exec_body_simulation_plus lemma below. This generalization is necessary for the induction proof inside the body. *) @@ -1403,14 +1421,10 @@ Proof. destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong. destruct s as (rs1 & m1); simpl in *. destruct s2 as (rs2 & m2); simpl in *. - assert (BOUNDBB: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) + assert (BOUNDBBMAX: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) by (eapply size_of_blocks_bounds; eauto). + exploit header_body_tail_bound; eauto. intros BDYTAIL. exploit exec_basic_simulation; eauto. - { assert (list_length_z (header bb) >= 0) by eapply list_length_z_pos. - assert (list_length_z (header bb) < size bb) by eapply header_size_lt_block_size. - destruct BOUNDBB. - (*assert (size bb < Ptrofs.max_unsigned) by omega.*) - admit. (* TODO *) } intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). (* Code from the star' lemma bellow. We need this to exploit exec_step_internal. *) exploit exec_basic_dont_move_PC; eauto. intros AGPC. @@ -1425,10 +1439,20 @@ Proof. simpl in FIND_INSTR. (* Execute internal step. *) exploit (Asm.exec_step_internal tge b); eauto. - { (* unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr); - try rewrite list_length_z_nat; try split; try omega. - simpl; rewrite <- list_length_z_nat; assumption. *) - admit. (* TODO *) } + { + rewrite Ptrofs.add_unsigned. + repeat (rewrite Ptrofs.unsigned_repr); try omega. + 2: { + assert (BOUNDOFS: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. + assert (list_length_z (body bb) <= size bb) by eapply body_size_le_block_size. + assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. } + omega. } + try rewrite list_length_z_nat; try split; + simpl; rewrite <- !list_length_z_nat; + replace (Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb) - + list_length_z (a :: li))) with (Ptrofs.unsigned ofs + list_length_z (header bb) + + (list_length_z (body bb) - list_length_z (a :: li))) by omega; + try assumption; try omega. } (* This is our STEP hypothesis. *) intros STEP_NEXT. @@ -1459,7 +1483,7 @@ Proof. + intros (s2' & LAST_STEPS & LAST_MATCHS). eexists. split; eauto. eapply plus_left'; eauto. -Admitted. +Qed. Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall (ATPC: rs PC = Vptr b ofs) -- cgit