diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-06 22:15:54 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-06 22:15:54 +0100 |
| commit | 246553dadbf6a089bd92bcdea645cff95e26f3ed (patch) | |
| tree | 57c43986550badec34ef71b31e7c607a1f8483b5 /aarch64/PostpassSchedulingproof.v | |
| parent | 972f6b9890ea3644626fc097e460035028b940eb (diff) | |
| download | compcert-kvx-246553dadbf6a089bd92bcdea645cff95e26f3ed.tar.gz compcert-kvx-246553dadbf6a089bd92bcdea645cff95e26f3ed.zip | |
Asmgen proof completely proved with ldp/stp
Diffstat (limited to 'aarch64/PostpassSchedulingproof.v')
| -rw-r--r-- | aarch64/PostpassSchedulingproof.v | 43 |
1 files changed, 21 insertions, 22 deletions
diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index 140b3aa2..48840602 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -99,28 +99,27 @@ Lemma transf_find_bblock: verified_schedule bb = OK tbb /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb. Proof. -Admitted. - (*intros.*) - (*monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.*) - (*monadInv EQ. simpl in *.*) - (*generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0.*) - (*induction (fn_blocks f).*) - (*- intros. simpl in *. discriminate.*) - (*- intros. simpl in *.*) - (*monadInv EQ0. simpl.*) - (*destruct (zlt z 0); try discriminate.*) - (*destruct (zeq z 0).*) - (*+ inv H. eauto.*) - (*+ monadInv EQ0.*) - (*exploit IHb; eauto.*) - (*intros (tbb & SCH & FIND).*) - (*eexists; split; eauto.*) - (*inv FIND.*) - (*unfold verify_size in EQ0.*) - (*destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.*) - (*rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.*) - (*reflexivity.*) -(*Qed.*) + intros. + monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0. + monadInv EQ. simpl in *. + generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0. + induction (fn_blocks f). + - intros. simpl in *. discriminate. + - intros. simpl in *. + monadInv EQ0. simpl. + destruct (zlt z 0); try discriminate. + destruct (zeq z 0). + + inv H. eauto. + + monadInv EQ0. + exploit IHb; eauto. + intros (tbb & SCH & FIND). + eexists; split; eauto. + inv FIND. + unfold verify_size in EQ0. + destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate. + rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE. + reflexivity. +Qed. Lemma stick_header_neutral: forall a, a = (stick_header (header a) (no_header a)). |