From 274f32429e43efa5b4031d2dfe1c32f30a7fff3f Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 19 Jun 2021 23:51:34 +0200 Subject: finish main proof --- scheduling/BTL_Schedulerproof.v | 146 +++++++++++++++++++++++++++++++++++----- 1 file changed, 128 insertions(+), 18 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 1a4c5757..13ea61a6 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -296,32 +296,145 @@ Qed. End SYMBOLIC_CTX. -Lemma iblock_step_eqregs stk sp f ib: - forall rs rs' m s t +Lemma tr_inputs_eqregs_list f tbl: forall rs rs' r' ores, + (forall r : positive, rs # r = rs' # r) -> + (tr_inputs f tbl ores rs) # r' = + (tr_inputs f tbl ores rs') # r'. +Proof. + induction tbl as [|pc tbl IHtbl]; + intros; destruct ores; simpl; + rewrite !tr_inputs_get; autodestruct. +Qed. + +Lemma find_function_eqregs rs rs' ros fd: + (forall r : positive, rs # r = rs' # r) -> + find_function tpge ros rs = Some fd -> + find_function tpge ros rs' = Some fd. +Proof. + intros EQREGS; destruct ros; simpl. + rewrite EQREGS; auto. + autodestruct. +Qed. + +Lemma args_eqregs (args: list reg): forall (rs rs': regset), + (forall r : positive, rs # r = rs' # r) -> + rs ## args = rs' ## args. +Proof. + induction args; simpl; trivial. + intros rs rs' EQREGS; rewrite EQREGS. + apply f_equal; eauto. +Qed. + +Lemma f_arg_eqregs (rs rs': regset): + (forall r : positive, rs # r = rs' # r) -> + (fun r : positive => rs # r) = (fun r : positive => rs' # r). +Proof. + intros EQREGS; apply functional_extensionality; eauto. +Qed. + +Lemma eqregs_update (rs rs': regset) v dest: + (forall r, rs # r = rs' # r) -> + (forall r, (rs # dest <- v) # r = (rs' # dest <- v) # r). +Proof. + intros EQREGS r; destruct (Pos.eq_dec dest r); subst. + * rewrite !Regmap.gss; reflexivity. + * rewrite !Regmap.gso; auto. +Qed. + +Local Hint Resolve equiv_stack_refl tr_inputs_eqregs_list find_function_eqregs eqregs_update: core. + +Lemma iblock_istep_eqregs_None sp ib: forall rs m rs' rs1 m1 (EQREGS: forall r, rs # r = rs' # r) - (STEP: iblock_step tr_inputs tpge stk f sp rs m ib s t), - iblock_step tr_inputs tpge stk f sp rs' m ib s t. + (ISTEP: iblock_istep tpge sp rs m ib rs1 m1 None), + exists rs1', + iblock_istep tpge sp rs' m ib rs1' m1 None + /\ (forall r, rs1 # r = rs1' # r). Proof. + induction ib; intros; inv ISTEP. + - repeat econstructor; eauto. + - repeat econstructor; eauto. + erewrite args_eqregs; eauto. + - repeat econstructor; eauto. + erewrite args_eqregs; eauto. + - repeat econstructor; eauto. + erewrite args_eqregs; eauto. + rewrite <- EQREGS; eauto. + - exploit IHib1; eauto. + intros (rs1' & ISTEP1 & EQREGS1). + exploit IHib2; eauto. + intros (rs2' & ISTEP2 & EQREGS2). + eexists; split. econstructor; eauto. + eauto. + - destruct b. + 1: exploit IHib1; eauto. + 2: exploit IHib2; eauto. + all: + intros (rs1' & ISTEP & EQREGS'); + eexists; split; try eapply exec_cond; + try erewrite args_eqregs; eauto. +Qed. -Admitted. +Lemma iblock_step_eqregs stk sp f ib: forall rs rs' m t s + (EQREGS: forall r, rs # r = rs' # r) + (STEP: iblock_step tr_inputs tpge stk f sp rs m ib t s), + exists s', + iblock_step tr_inputs tpge stk f sp rs' m ib t s' + /\ equiv_state s s'. +Proof. + induction ib; intros; + destruct STEP as (rs2 & m2 & fin & ISTEP & FSTEP); inv ISTEP. + - inv FSTEP; + eexists; split; repeat econstructor; eauto. + + destruct (or); simpl; try rewrite EQREGS; constructor; eauto. + + erewrite args_eqregs; eauto. repeat econstructor; eauto. + + erewrite args_eqregs; eauto. econstructor; eauto. + + erewrite f_arg_eqregs; eauto. + + destruct res; simpl; eauto. + + rewrite <- EQREGS; auto. + - exploit IHib1; eauto. + + econstructor. do 2 eexists; split; eauto. + + intros (s' & STEP & EQUIV). clear FSTEP. + destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP). + repeat (econstructor; eauto). + - exploit iblock_istep_eqregs_None; eauto. + intros (rs1' & ISTEP1 & EQREGS1). + exploit IHib2; eauto. + + econstructor. do 2 eexists; split; eauto. + + intros (s' & STEP & EQUIV). clear FSTEP. + destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP). + eexists; split; eauto. + econstructor; do 2 eexists; split; eauto. + eapply exec_seq_continue; eauto. + - destruct b. + 1: exploit IHib1; eauto. + 3: exploit IHib2; eauto. + 1,3: econstructor; do 2 eexists; split; eauto. + all: + intros (s' & STEP & EQUIV); clear FSTEP; + destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP); + eexists; split; eauto; econstructor; + do 2 eexists; split; eauto; + eapply exec_cond; try erewrite args_eqregs; eauto. +Qed. -Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s pc - (STEP: iblock_step tr_inputs pge stk1 f1 sp rs m ibf.(entry) t s) +Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s1 pc + (STEP: iblock_step tr_inputs pge stk1 f1 sp rs m ibf.(entry) t s1) (PC: (fn_code f1) ! pc = Some ibf) (EQREGS: forall r : positive, rs # r = rs' # r) (STACKS: list_forall2 match_stackframes stk1 stk2) (TRANSF: match_function f1 f2) - :exists ibf' s', - (fn_code f2) ! pc = Some ibf' - /\ iblock_step tr_inputs tpge stk2 f2 sp rs' m ibf'.(entry) t s' - /\ match_states s s'. + :exists ibf' s2, + (fn_code f2) ! pc = Some ibf' + /\ iblock_step tr_inputs tpge stk2 f2 sp rs' m ibf'.(entry) t s2 + /\ match_states s1 s2. Proof. exploit symbolic_simu_ok; eauto. intros (ib2 & PC' & SYMBS). exploit symbolic_simu_correct; repeat (eauto; simpl). - intros (s' & STEP2 & MS). - exists ib2; exists s'. repeat split; auto. - eapply iblock_step_eqregs; eauto. -Admitted. + intros (s2 & STEP2 & MS). + exploit iblock_step_eqregs; eauto. intros (s3 & STEP3 & EQUIV). + clear STEP2. exists ib2; exists s3. repeat split; auto. + eapply match_states_equiv; eauto. +Qed. Local Hint Constructors step: core. @@ -353,9 +466,6 @@ Proof. eexists; split. + econstructor. + inv H1. econstructor; eauto. - intros; destruct (Pos.eq_dec res' r); subst. - * rewrite !Regmap.gss; reflexivity. - * rewrite !Regmap.gso; auto. Qed. Theorem transf_program_correct: -- cgit