From 1685bfd6d017a487368ceb3c71cfaf03c9d42c9b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 23 Nov 2020 23:53:22 +0100 Subject: Start of the postpasschedproof, redefining verify schedule lemmas --- aarch64/PostpassScheduling.v | 132 +++++++++++++++++++++++++++++-------------- 1 file changed, 91 insertions(+), 41 deletions(-) (limited to 'aarch64/PostpassScheduling.v') diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index a9473789..fa7e2776 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -18,6 +18,7 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. +Require Import IterList. (*Require Peephole.*) Local Open Scope error_monad_scope. @@ -28,6 +29,10 @@ Axiom schedule: bblock -> (list basic) * option control. Extract Constant schedule => "PostpassSchedulingOracle.schedule". +Section verify_schedule. + +Variable lk: aarch64_linker. + (* (** * Concat all bundles into one big basic block *) @@ -216,22 +221,22 @@ Definition verify_schedule (bb bb' : bblock) : res unit := | false => Error (msg "PostpassScheduling.verify_schedule") end. -(*Definition verify_size bb lbb := if (Z.eqb (size bb) (size_blocks lbb)) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size").*) +Definition verify_size bb bb' := if (Z.eqb (size bb) (size bb')) then OK tt else Error (msg "PostpassScheduling:verify_size: wrong size"). -(*Lemma verify_size_size:*) - (*forall bb lbb, verify_size bb lbb = OK tt -> size bb = size_blocks lbb.*) -(*Proof.*) - (*intros. unfold verify_size in H. destruct (size bb =? size_blocks lbb) eqn:SIZE; try discriminate.*) - (*apply Z.eqb_eq. assumption.*) -(*Qed.*) +Lemma verify_size_size: + forall bb bb', verify_size bb bb' = OK tt -> size bb = size bb'. +Proof. + intros. unfold verify_size in H. destruct (size bb =? size bb') eqn:SIZE; try discriminate. + apply Z.eqb_eq. assumption. +Qed. -(*Lemma verify_schedule_no_header:*) - (*forall bb bb',*) - (*verify_schedule (no_header bb) bb' = verify_schedule bb bb'.*) -(*Proof.*) - (*intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv.*) - (*reflexivity.*) -(*Qed.*) +(* Lemma verify_schedule_no_header: + forall bb bb', + verify_schedule (no_header bb) bb' = verify_schedule bb bb'. +Proof. + intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv. + reflexivity. +Qed. *) (*Lemma stick_header_verify_schedule:*) @@ -354,14 +359,22 @@ Definition do_schedule (bb: bblock) : res bblock := (*end.*) Definition verified_schedule (bb : bblock) : res bblock := - let bb' := no_header bb in + let nhbb := no_header bb in (* TODO remove? let bb'' := Peephole.optimize_bblock bb' in *) - do lb <- do_schedule bb'; + do nhbb' <- do_schedule nhbb; (*do tbb <- concat_all lbb;*) - (*do sizecheck <- verify_size bb lbb;*) - do schedcheck <- verify_schedule bb' lb; (* TODO Keep this one *) - (*do parcheck <- verify_par res;*) - OK (stick_header (header bb) lb). + let bb' := stick_header (header bb) nhbb' in + do sizecheck <- verify_size bb bb'; + do schedcheck <- verify_schedule bb bb'; (* TODO Keep this one *) + OK (bb'). + +(* Definition verified_schedule_nob (bb : bblock) : res (list bblock) := + let nhbb := no_header bb in + do bb' <- do_schedule nhbb; + do sizecheck <- verify_size nhbb bb'; + do schedcheck <- verify_schedule nhbb bb'; + do res <- stick_header_code (header bb) bb'; + OK res. *) (*Lemma verified_schedule_nob_size:*) (*forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb.*) @@ -393,21 +406,38 @@ Definition verified_schedule (bb : bblock) : res bblock := (*Qed.*) -(*Definition verified_schedule (bb : bblock) : res (list bblock) :=*) - (*verified_schedule_nob bb.*) +(* Definition verified_schedule (bb : bblock) : res (list bblock) := + verified_schedule_nob bb. *) (* TODO Remove? match exit bb with | Some (PExpand (Pbuiltin ef args res)) => OK (bb::nil) (* Special case for ensuring the lemma verified_schedule_builtin_idem *) | _ => verified_schedule_nob bb end.*) -(*Lemma verified_schedule_size:*) - (*forall bb lbb, verified_schedule bb = OK lbb -> size bb = size_blocks lbb.*) -(*Proof.*) - (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) - (*all: try (apply verified_schedule_nob_size; auto; fail).*) - (*inv H. simpl. omega.*) -(*Qed.*) +Lemma verified_schedule_size: + forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'. +Proof. + intros. unfold verified_schedule in H. + monadInv H. + unfold do_schedule in EQ. + destruct schedule in EQ. + destruct (size (no_header bb) =? 1) eqn:TRIVB. + - inv EQ. unfold size. simpl. reflexivity. + - unfold schedule_to_bblock in EQ. + destruct o in EQ. + + inv EQ. unfold verify_size in EQ1. unfold size in *. simpl in *. + rewrite Z.eqb_neq in TRIVB. + destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =? + Z.of_nat (Datatypes.length (header bb) + Datatypes.length l + 1)) eqn:ESIZE; try discriminate. + rewrite Z.eqb_eq in ESIZE; repeat rewrite Nat2Z.inj_add in *; + rewrite ESIZE. reflexivity. + + unfold make_bblock_from_basics in EQ. destruct l in EQ; try discriminate. + inv EQ. unfold verify_size in EQ1; unfold size in *; simpl in *. + destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =? + Z.of_nat (Datatypes.length (header bb) + Datatypes.S (Datatypes.length l) + 0)) eqn:ESIZE; try discriminate. + rewrite Z.eqb_eq in ESIZE. repeat rewrite Nat2Z.inj_add in *. + rewrite ESIZE. reflexivity. +Qed. (*Lemma verified_schedule_no_header_in_middle:*) (*forall lbb bb,*) @@ -447,18 +477,37 @@ Definition verified_schedule (bb : bblock) : res bblock := (*destruct (bblock_simub _ _); auto; try discriminate.*) (*Qed.*) -(*Theorem verified_schedule_correct:*) - (*forall ge f bb lbb,*) - (*verified_schedule bb = OK lbb ->*) - (*exists tbb,*) - (*is_concat tbb lbb*) - (*/\ bblock_simu ge f bb tbb.*) -(*Proof.*) - (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) - (*all: try (eapply verified_schedule_nob_correct; eauto; fail).*) - (*inv H. eexists. split; simpl; auto. constructor; auto. simpl; auto. constructor; auto.*) -(*Qed.*) - +Theorem verified_schedule_correct: + forall ge f bb bb', + verified_schedule bb = OK bb' -> + bblock_simu lk ge f bb bb'. +Proof. +(* intros. + assert (size bb = size bb'). { apply verified_schedule_size. auto. } + unfold verified_schedule in H. monadInv H. + eapply bblock_simub_correct. + unfold do_schedule in EQ. + unfold verify_schedule in EQ0. + + destruct (bblock_simub _ _) in *; try discriminate. + destruct schedule. + simpl. unfold bblock_simub. + + eapply bblock_simub_correct. + destruct (bblock_simub); try discriminate. + + destruct schedule. + unfold bblock_simu, exec_bblock. destruct (exit bb). destruct c. destruct i. + + - intros rs m rs' m' t (rs1 & m1 & EBDY & EXT). + + eexists; eexists; split. + simpl. unfold exec_body. + + all: try (eapply verified_schedule_nob_correct; eauto; fail). + inv H. eexists; eexists; split; simpl; auto. constructor; auto. simpl; auto. constructor; auto. +Qed. *) +Admitted. (*Lemma verified_schedule_builtin_idem:*) (*forall bb ef args res lbb,*) (*exit bb = Some (PExpand (Pbuiltin ef args res)) ->*) @@ -468,6 +517,7 @@ Definition verified_schedule (bb : bblock) : res bblock := (*intros. unfold verified_schedule in H0. rewrite H in H0. inv H0. reflexivity.*) (*Qed.*) +End verify_schedule. Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) := match lbb with -- cgit