From c50b4607f501a991e18088f75d04ff6d5bce66a8 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 31 Oct 2021 18:58:32 +0000 Subject: Add construction of state in sem --- src/hls/Abstr.v | 170 ++++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 147 insertions(+), 23 deletions(-) (limited to 'src/hls') diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index a0b7f4d..d1b008e 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -366,13 +366,15 @@ Section SEMANTICS. Context {A : Type}. Record ctx : Type := mk_ctx { - ctx_rs: regset; - ctx_ps: predset; - ctx_mem: mem; + ctx_is: instr_state; ctx_sp: val; ctx_ge: Genv.t A unit; }. +Definition ctx_rs ctx := is_rs (ctx_is ctx). +Definition ctx_ps ctx := is_ps (ctx_is ctx). +Definition ctx_mem ctx := is_mem (ctx_is ctx). + Inductive sem_value : ctx -> expression -> val -> Prop := | Sbase_reg: forall r ctx, @@ -656,11 +658,36 @@ Lemma ge_preserved_same: Proof. unfold ge_preserved; auto. Qed. #[local] Hint Resolve ge_preserved_same : core. +Inductive match_states : instr_state -> instr_state -> Prop := +| match_states_intro: + forall ps ps' rs rs' m m', + (forall x, rs !! x = rs' !! x) -> + (forall x, ps !! x = ps' !! x) -> + m = m' -> + match_states (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). + +Lemma match_states_refl x : match_states x x. +Proof. destruct x; constructor; crush. Qed. + +Lemma match_states_commut x y : match_states x y -> match_states y x. +Proof. inversion 1; constructor; crush. Qed. + +Lemma match_states_trans x y z : + match_states x y -> match_states y z -> match_states x z. +Proof. repeat inversion 1; constructor; crush. Qed. + +#[global] +Instance match_states_Equivalence : Equivalence match_states := + { Equivalence_Reflexive := match_states_refl ; + Equivalence_Symmetric := match_states_commut ; + Equivalence_Transitive := match_states_trans ; }. + Inductive similar {A B} : @ctx A -> @ctx B -> Prop := | similar_intro : - forall rs ps mem sp ge tge, + forall ist ist' sp ge tge, ge_preserved ge tge -> - similar (mk_ctx rs ps mem sp ge) (mk_ctx rs ps mem sp tge). + match_states ist ist' -> + similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge). Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool := match pe1, pe2 with @@ -977,7 +1004,7 @@ Section CORRECT. induction e using expression_ind2 with (P0 := fun p => forall v v', sem_val_list ictx p v -> sem_val_list octx p v' -> v = v'); - inv HSIM; repeat progress simplify; + inv HSIM; match goal with H: context [match_states] |- _ => inv H end; repeat progress simplify; try solve [match goal with | H: sem_value _ _ _, H2: sem_value _ _ _ |- _ => inv H; inv H2; auto | H: sem_mem _ _ _, H2: sem_mem _ _ _ |- _ => inv H; inv H2; auto @@ -990,23 +1017,54 @@ Section CORRECT. IH: forall _ _, sem_val_list _ _ _ -> sem_val_list _ _ _ -> _ = _ |- _ => assert (X: l1 = l2) by (apply IH; auto) | H: ge_preserved _ _ |- _ => inv H + | |- context [ctx_rs] => unfold ctx_rs; cbn + | H: context [ctx_mem] |- _ => unfold ctx_mem in H; cbn end; crush. - - inv H1. inv H0. simplify. - assert (lv0 = lv). apply IHe; eauto. subst. - inv H. rewrite H1 in H13. - assert (a0 = a1) by crush. subst. - assert (m'1 = m'0). apply IHe0; eauto. subst. - crush. - - inv H0. inv H1. simplify. - assert (lv = lv0). { apply IHe2; eauto. } subst. - assert (a1 = a0). { inv H. rewrite H1 in H12. crush. } subst. - assert (v0 = v1). { apply IHe1; auto. } subst. - assert (m'0 = m'1). { apply IHe3; auto. } subst. - crush. - - inv H0. inv H1. f_equal. apply IHe; auto. + - repeat match goal with H: sem_value _ _ _ |- _ => inv H end; simplify; + assert (lv0 = lv) by (apply IHe; eauto); subst; + match goal with H: ge_preserved _ _ |- _ => inv H end; + match goal with H: context [Op.eval_addressing _ _ _ _ = Op.eval_addressing _ _ _ _] |- _ + => rewrite H in * end; + assert (a0 = a1) by crush; + assert (m'2 = m'1) by (apply IHe0; eauto); crush. + - inv H0; inv H3. simplify. + assert (lv = lv0) by ( apply IHe2; eauto). subst. + assert (a1 = a0). { inv H. rewrite H3 in *. crush. } + assert (v0 = v1). { apply IHe1; auto. } + assert (m'1 = m'2). { apply IHe3; auto. } crush. + - inv H0. inv H3. f_equal. apply IHe; auto. apply IHe0; auto. Qed. + Lemma sem_value_mem_corr: + forall e v m, + (sem_value ictx e v -> sem_value octx e v) + /\ (sem_mem ictx e m -> sem_mem octx e m). + Proof using HSIM. + induction e using expression_ind2 + with (P0 := fun p => forall v, + sem_val_list ictx p v -> sem_val_list octx p v); + inv HSIM; match goal with H: context [match_states] |- _ => inv H end; repeat progress simplify. + - inv H0. unfold ctx_rs, ctx_ps, ctx_mem in *; cbn. rewrite H1. constructor. + - inv H0. unfold ctx_rs, ctx_ps, ctx_mem in *; cbn. constructor. + - inv H0. apply IHe in H6. econstructor; try eassumption. + unfold ctx_rs, ctx_ps, ctx_mem in *; cbn in *. inv H. crush. + - inv H0. + - inv H0. eapply IHe in H10. eapply IHe0 in H8; auto. + econstructor; try eassumption. + unfold ctx_rs, ctx_ps, ctx_mem in *; cbn in *. inv H; crush. + - inv H0. + - inv H0. + - inv H0. eapply IHe1 in H11; auto. eapply IHe2 in H12; auto. eapply IHe3 in H9; auto. + econstructor; try eassumption. + unfold ctx_rs, ctx_ps, ctx_mem in *; cbn in *. inv H; crush. + - inv H0. + - inv H0. + - inv H0. econstructor. + - inv H0. eapply IHe in H6; auto. eapply IHe0 in H8. + econstructor; eassumption. + Qed. + Lemma sem_value_det: forall e v v', sem_value ictx e v -> sem_value octx e v' -> v = v'. @@ -1014,6 +1072,13 @@ Section CORRECT. intros. eapply sem_value_mem_det; eauto; apply Mem.empty. Qed. + Lemma sem_value_corr: + forall e v, + sem_value ictx e v -> sem_value octx e v. + Proof using HSIM. + intros. eapply sem_value_mem_corr; eauto; apply Mem.empty. + Qed. + Lemma sem_mem_det: forall e v v', sem_mem ictx e v -> sem_mem octx e v' -> v = v'. @@ -1021,6 +1086,13 @@ Section CORRECT. intros. eapply sem_value_mem_det; eauto; apply (Vint (Int.repr 0%Z)). Qed. + Lemma sem_mem_corr: + forall e v, + sem_mem ictx e v -> sem_mem octx e v. + Proof using HSIM. + intros. eapply sem_value_mem_corr; eauto; apply (Vint (Int.repr 0%Z)). + Qed. + Lemma sem_val_list_det: forall e l l', sem_val_list ictx e l -> sem_val_list octx e l' -> l = l'. @@ -1031,12 +1103,34 @@ Section CORRECT. apply IHe; eauto. Qed. + Lemma sem_val_list_corr: + forall e l, + sem_val_list ictx e l -> sem_val_list octx e l. + Proof using HSIM. + induction e; simplify. + - inv H; constructor. + - inv H. apply sem_value_corr in H3; auto; try apply Mem.empty; + apply IHe in H5; constructor; assumption. + Qed. + Lemma sem_pred_det: forall e v v', sem_pred ictx e v -> sem_pred octx e v' -> v = v'. Proof using HSIM. - try solve [inversion 1]; pose proof sem_value_det; pose proof sem_val_list_det; inv HSIM; simplify. - inv H2; inv H3; auto. assert (lv = lv0) by (eapply H0; eauto). crush. + try solve [inversion 1]; pose proof sem_value_det; pose proof sem_val_list_det; inv HSIM; + match goal with H: match_states _ _ |- _ => inv H end; simplify. + inv H2; inv H5; auto. assert (lv = lv0) by (eapply H0; eauto). subst. unfold ctx_mem in *. + crush. + Qed. + + Lemma sem_pred_corr: + forall e v, + sem_pred ictx e v -> sem_pred octx e v. + Proof using HSIM. + try solve [inversion 1]; pose proof sem_value_corr; pose proof sem_val_list_corr; inv HSIM; + match goal with H: match_states _ _ |- _ => inv H end; simplify. + inv H2; auto. apply H0 in H5. econstructor; eauto. + unfold ctx_ps; cbn. rewrite H4. constructor. Qed. #[local] Opaque PTree.set. @@ -1116,7 +1210,7 @@ Section CORRECT. sem_pred_tree isem ictx h t v -> sem_pred_tree osem octx h' t' v' -> v = v'. - Proof. + Proof using HSIM SEMSIM. intros. inv H4. inv H5. destruct (Pos.eq_dec e e0); subst. { eapply norm_expr_constant in H3; [|eassumption]. @@ -1133,7 +1227,11 @@ Section CORRECT. pose proof H0. eapply norm_expr_forall_impl in H0; [| | | |eassumption]; try eassumption. unfold "⇒" in H0. unfold eval_predf in *. apply H0 in H6. rewrite negate_correct in H6. apply negb_true_iff in H6. - inv HSIM. crush. } + inv HSIM. match goal with H: match_states _ _ |- _ => inv H end. + unfold ctx_ps, ctx_mem, ctx_rs in *. simplify. + pose proof eval_predf_pr_equiv pr0 ps ps' H17. unfold eval_predf in *. + rewrite H5 in H6. crush. + } { unfold beq_pred_expr in H. repeat (destruct_match; []). inv H2. rewrite Heqp0 in H3. inv H3. simplify. eapply forall_ptree_true in H3. 2: { eapply H11. } @@ -1224,6 +1322,25 @@ Section CORRECT. End SEM_PRED. + Section SEM_PRED_CORR. + + Context (B: Type). + Context (isem: @ctx fd -> expression -> B -> Prop). + Context (osem: @ctx tfd -> expression -> B -> Prop). + Context (SEMCORR: forall e v, isem ictx e v -> osem octx e v). + + Lemma sem_pred_tree_corr: + forall x x' v t t' h h', + beq_pred_expr x x' = true -> + predicated_mutexcl x -> predicated_mutexcl x' -> + norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x (PTree.empty _) = (t, h) -> + norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x' h = (t', h') -> + sem_pred_tree isem ictx h t v -> + sem_pred_tree osem octx h' t' v. + Proof using SEMCORR. Admitted. + + End SEM_PRED_CORR. + Inductive match_instr_state : instr_state -> instr_state -> Prop := | match_instr_state_intro : forall i1 i2, is_mem i1 = is_mem i2 -> @@ -1257,6 +1374,13 @@ Section CORRECT. } Admitted. + Lemma check_correct2: + forall (fa fb : forest) i, + check fa fb = true -> + sem ictx fa i -> + exists i', sem octx fb i' /\ match_instr_state i i'. + Proof. Admitted. + End CORRECT. Lemma get_empty: -- cgit From 0bc9bc9f6318a820352a1af1f3ec8f7d7d4a1821 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 1 Nov 2021 09:11:43 +0000 Subject: Add Admitted theorems for existence proofs --- src/hls/Abstr.v | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'src/hls') diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index d1b008e..abc4181 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1341,18 +1341,11 @@ Section CORRECT. End SEM_PRED_CORR. - Inductive match_instr_state : instr_state -> instr_state -> Prop := - | match_instr_state_intro : forall i1 i2, - is_mem i1 = is_mem i2 -> - (forall x, (is_rs i1) !! x = (is_rs i2) !! x) -> - (forall x, (is_ps i1) !! x = (is_ps i2) !! x) -> - match_instr_state i1 i2. - Lemma check_correct: forall (fa fb : forest) i i', check fa fb = true -> sem ictx fa i -> sem octx fb i' -> - match_instr_state i i'. + match_states i i'. Proof using HSIM. intros. unfold check, get_forest in *; intros; @@ -1378,7 +1371,7 @@ Admitted. forall (fa fb : forest) i, check fa fb = true -> sem ictx fa i -> - exists i', sem octx fb i' /\ match_instr_state i i'. + exists i', sem octx fb i' /\ match_states i i'. Proof. Admitted. End CORRECT. -- cgit From 04db0fb8a8a891200fd4767d780efc5a897f72a0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 1 Nov 2021 09:12:12 +0000 Subject: Add RTLBlockInstr proofs --- src/hls/RTLBlockInstr.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'src/hls') diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 7e204e7..6b4b5be 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -111,6 +111,29 @@ Proof. unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0. Qed. +#[local] Open Scope pred_op. + +Lemma eval_predf_Pand : + forall ps p p', + eval_predf ps (p ∧ p') = eval_predf ps p && eval_predf ps p'. +Proof. unfold eval_predf; split; simplify; auto with bool. Qed. + +Lemma eval_predf_Por : + forall ps p p', + eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'. +Proof. unfold eval_predf; split; simplify; auto with bool. Qed. + +Lemma eval_predf_pr_equiv : + forall p ps ps', + (forall x, ps !! x = ps' !! x) -> + eval_predf ps p = eval_predf ps' p. +Proof. + induction p; simplify; auto; + try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto); + [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por]; + erewrite IHp1; try eassumption; erewrite IHp2; eauto. +Qed. + Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := match rl, vl with | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs) -- cgit From 352c05e9350f84dc8fe3ba5d10b7b76c184e5f84 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 1 Nov 2021 09:12:43 +0000 Subject: Add work on RTLPargenproof.v --- src/hls/RTLPargen.v | 282 +++++++++++++++++++++++++---------------------- src/hls/RTLPargenproof.v | 23 ++-- 2 files changed, 165 insertions(+), 140 deletions(-) (limited to 'src/hls') diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 30a35f3..da8d527 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -131,21 +131,10 @@ Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Pro /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl = Op.eval_addressing tge sp addr vl). -Lemma ge_preserved_same: - forall A B ge, @ge_preserved A B A B ge ge. -Proof. unfold ge_preserved; auto. Qed. #[local] Hint Resolve ge_preserved_same : rtlpar. Ltac rtlpar_crush := crush; eauto with rtlpar. -Inductive match_states : instr_state -> instr_state -> Prop := -| match_states_intro: - forall ps ps' rs rs' m m', - (forall x, rs !! x = rs' !! x) -> - (forall x, ps !! x = ps' !! x) -> - m = m' -> - match_states (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). - Inductive match_states_ld : instr_state -> instr_state -> Prop := | match_states_ld_intro: forall ps ps' rs rs' m m', @@ -154,13 +143,13 @@ Inductive match_states_ld : instr_state -> instr_state -> Prop := Mem.extends m m' -> match_states_ld (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). -Lemma sems_det: +(*Lemma sems_det: forall A ge tge sp f rs ps m, ge_preserved ge tge -> forall v v' mv mv', (@sem_value A (mk_ctx rs ps m sp ge) f v /\ @sem_value A (mk_ctx rs ps m sp tge) f v' -> v = v') /\ (@sem_mem A (mk_ctx rs ps m sp ge) f mv /\ @sem_mem A (mk_ctx rs ps m sp tge) f mv' -> mv = mv'). -Proof. Abort. +Proof. Abort.*) (*Lemma sem_value_det: forall A ge tge sp st f v v', @@ -422,24 +411,11 @@ RTLBlock to abstract translation Correctness of translation from RTLBlock to the abstract interpretation language. |*) -Lemma match_states_refl x : match_states x x. -Proof. destruct x; constructor; crush. Qed. - -Lemma match_states_commut x y : match_states x y -> match_states y x. -Proof. inversion 1; constructor; crush. Qed. - -Lemma match_states_trans x y z : - match_states x y -> match_states y z -> match_states x z. -Proof. repeat inversion 1; constructor; crush. Qed. - Ltac inv_simp := repeat match goal with | H: exists _, _ |- _ => inv H end; simplify. -Lemma abstract_interp_empty A ge sp st : @sem A ge sp st empty st. -Proof. destruct st; repeat constructor. Qed. - Lemma abstract_interp_empty3 : forall A ge sp st st', @sem A ge sp st empty st' -> @@ -543,11 +519,6 @@ Lemma abstr_comp : x = update x0 i. Proof. induction l; intros; crush; eapply IHl; eauto. Qed. -Lemma abstract_seq : - forall l f i, - abstract_sequence f (l ++ i :: nil) = update (abstract_sequence f l) i. -Proof. induction l; crush. Qed. - Lemma check_list_l_false : forall l x r, check_dest_l (l ++ x :: nil) r = false -> @@ -583,19 +554,7 @@ Proof. apply check_list_l_false in H. tauto. Qed. -Lemma rtlblock_trans_correct' : - forall bb ge sp st x st'', - RTLBlock.step_instr_list ge sp st (bb ++ x :: nil) st'' -> - exists st', RTLBlock.step_instr_list ge sp st bb st' - /\ step_instr ge sp st' x st''. -Proof. - induction bb. - crush. exists st. - split. constructor. inv H. inv H6. auto. - crush. inv H. exploit IHbb. eassumption. inv_simp. - econstructor. split. - econstructor; eauto. eauto. -Qed. + Lemma sem_update_RBnop : forall A ge sp st f st', @@ -790,25 +749,6 @@ Proof. eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store. Qed. -Lemma rtlblock_trans_correct : - forall bb ge sp st st', - RTLBlock.step_instr_list ge sp st bb st' -> - forall tst, - match_states st tst -> - exists tst', sem ge sp tst (abstract_sequence empty bb) tst' - /\ match_states st' tst'. -Proof. - induction bb using rev_ind; simplify. - { econstructor. simplify. apply abstract_interp_empty. - inv H. auto. } - { apply rtlblock_trans_correct' in H. inv_simp. - rewrite abstract_seq. - exploit IHbb; try eassumption; []; inv_simp. - exploit sem_update. apply H1. apply match_states_commut; eassumption. - eauto. inv_simp. econstructor. split. apply H3. - auto. } -Qed. - Lemma abstr_sem_val_mem : forall A B ge tge st tst sp a, ge_preserved ge tge -> @@ -940,6 +880,62 @@ Lemma step_instr_seq_same : st = st'. Proof. inversion 1; auto. Qed. +Lemma sem_update' : + forall A ge sp st a x st', + sem ge sp st (update (abstract_sequence empty a) x) st' -> + exists st'', + @step_instr A ge sp st'' x st' /\ + sem ge sp st (abstract_sequence empty a) st''. +Proof. + Admitted. + +Lemma sem_separate : + forall A (ge: @RTLBlockInstr.genv A) b a sp st st', + sem ge sp st (abstract_sequence empty (a ++ b)) st' -> + exists st'', + sem ge sp st (abstract_sequence empty a) st'' + /\ sem ge sp st'' (abstract_sequence empty b) st'. +Proof. + induction b using rev_ind; simplify. + { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. } + { simplify. rewrite app_assoc in H. rewrite abstract_seq in H. + exploit sem_update'; eauto; inv_simp. + exploit IHb; eauto; inv_simp. + econstructor; split; eauto. + rewrite abstract_seq. + eapply sem_update2; eauto. + } +Qed. + +Lemma rtlpar_trans_correct : + forall bb ge sp sem_st' sem_st st, + sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> + match_states sem_st st -> + exists st', RTLPar.step_instr_block ge sp st bb st' + /\ match_states sem_st' st'. +Proof. + induction bb using rev_ind. + { repeat econstructor. eapply abstract_interp_empty3 in H. + inv H. inv H0. constructor; congruence. } + { simplify. inv H0. repeat rewrite concat_app in H. simplify. + rewrite app_nil_r in H. + exploit sem_separate; eauto; inv_simp. + repeat econstructor. admit. admit. + } +Admitted. + +(*Lemma abstract_execution_correct_ld: + forall bb bb' cfi ge tge sp st st' tst, + RTLBlock.step_instr_list ge sp st bb st' -> + ge_preserved ge tge -> + schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> + match_states_ld st tst -> + exists tst', RTLPar.step_instr_block tge sp tst bb' tst' + /\ match_states st' tst'. +Proof. + intros.*) +*) + Lemma match_states_list : forall A (rs: Regmap.t A) rs', (forall r, rs !! r = rs' !! r) -> @@ -958,18 +954,53 @@ Qed. Lemma step_instr_matches : forall A a ge sp st st', - @step_instr A ge sp st a st' -> - forall tst, match_states st tst -> - exists tst', step_instr ge sp tst a tst' - /\ match_states st' tst'. + @step_instr A ge sp st a st' -> + forall tst, + match_states st tst -> + exists tst', step_instr ge sp tst a tst' + /\ match_states st' tst'. Proof. induction 1; simplify; match goal with H: match_states _ _ |- _ => inv H end; - repeat econstructor; try erewrite match_states_list; + try solve [repeat econstructor; try erewrite match_states_list; try apply PTree_matches; eauto; match goal with H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto - end. + end]. + - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. + repeat econstructor; try erewrite match_states_list; eauto. + erewrite <- eval_predf_pr_equiv; eassumption. + apply PTree_matches; assumption. + repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto. + erewrite <- eval_predf_pr_equiv; eassumption. + econstructor; auto. + match goal with H: eval_pred _ _ _ _ |- _ => inv H end. + repeat econstructor; try erewrite match_states_list; eauto. + - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. + repeat econstructor; try erewrite match_states_list; eauto. + erewrite <- eval_predf_pr_equiv; eassumption. + apply PTree_matches; assumption. + repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto. + erewrite <- eval_predf_pr_equiv; eassumption. + econstructor; auto. + match goal with H: eval_pred _ _ _ _ |- _ => inv H end. + repeat econstructor; try erewrite match_states_list; eauto. + - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end. + repeat econstructor; try erewrite match_states_list; eauto. + match goal with + H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto + end. + erewrite <- eval_predf_pr_equiv; eassumption. + repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto. + match goal with + H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto + end. + erewrite <- eval_predf_pr_equiv; eassumption. + match goal with H: eval_pred _ _ _ _ |- _ => inv H end. + repeat econstructor; try erewrite match_states_list; eauto. + match goal with + H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto + end. Qed. Lemma step_instr_list_matches : @@ -980,8 +1011,8 @@ Lemma step_instr_list_matches : /\ match_states st' tst'. Proof. induction a; intros; inv H; - try (exploit step_instr_matches; eauto; []; inv_simp; - exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto. + try (exploit step_instr_matches; eauto; []; simplify; + exploit IHa; eauto; []; simplify); repeat econstructor; eauto. Qed. Lemma step_instr_seq_matches : @@ -992,8 +1023,8 @@ Lemma step_instr_seq_matches : /\ match_states st' tst'. Proof. induction a; intros; inv H; - try (exploit step_instr_list_matches; eauto; []; inv_simp; - exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto. + try (exploit step_instr_list_matches; eauto; []; simplify; + exploit IHa; eauto; []; simplify); repeat econstructor; eauto. Qed. Lemma step_instr_block_matches : @@ -1004,66 +1035,71 @@ Lemma step_instr_block_matches : /\ match_states st' tst'. Proof. induction bb; intros; inv H; - try (exploit step_instr_seq_matches; eauto; []; inv_simp; - exploit IHbb; eauto; []; inv_simp); repeat econstructor; eauto. + try (exploit step_instr_seq_matches; eauto; []; simplify; + exploit IHbb; eauto; []; simplify); repeat econstructor; eauto. Qed. -Lemma sem_update' : - forall A ge sp st a x st', - sem ge sp st (update (abstract_sequence empty a) x) st' -> - exists st'', - @step_instr A ge sp st'' x st' /\ - sem ge sp st (abstract_sequence empty a) st''. +Lemma rtlblock_trans_correct' : + forall bb ge sp st x st'', + RTLBlock.step_instr_list ge sp st (bb ++ x :: nil) st'' -> + exists st', RTLBlock.step_instr_list ge sp st bb st' + /\ step_instr ge sp st' x st''. Proof. - Admitted. + induction bb. + crush. exists st. + split. constructor. inv H. inv H6. auto. + crush. inv H. exploit IHbb. eassumption. simplify. + econstructor. split. + econstructor; eauto. eauto. +Qed. -Lemma sem_separate : - forall A (ge: @RTLBlockInstr.genv A) b a sp st st', - sem ge sp st (abstract_sequence empty (a ++ b)) st' -> - exists st'', - sem ge sp st (abstract_sequence empty a) st'' - /\ sem ge sp st'' (abstract_sequence empty b) st'. +Lemma abstract_interp_empty A st : @sem A st empty (ctx_is st). +Proof. destruct st, ctx_is. simpl. repeat econstructor. Qed. + +Lemma abstract_seq : + forall l f i, + abstract_sequence f (l ++ i :: nil) = update (abstract_sequence f l) i. +Proof. induction l; crush. Qed. + +Lemma sem_update : + forall A ge sp st x st' st'' st''' f, + sem (mk_ctx st sp ge) f st' -> + match_states st' st''' -> + @step_instr A ge sp st''' x st'' -> + exists tst, sem (mk_ctx st sp ge) (update f x) tst /\ match_states st'' tst. +Proof. Admitted. + +Lemma rtlblock_trans_correct : + forall bb ge sp st st', + RTLBlock.step_instr_list ge sp st bb st' -> + forall tst, + match_states st tst -> + exists tst', sem (mk_ctx tst sp ge) (abstract_sequence empty bb) tst' + /\ match_states st' tst'. Proof. - induction b using rev_ind; simplify. - { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. } - { simplify. rewrite app_assoc in H. rewrite abstract_seq in H. - exploit sem_update'; eauto; inv_simp. - exploit IHb; eauto; inv_simp. - econstructor; split; eauto. + induction bb using rev_ind; simplify. + { econstructor. simplify. apply abstract_interp_empty. + inv H. auto. } + { apply rtlblock_trans_correct' in H. simplify. rewrite abstract_seq. - eapply sem_update2; eauto. - } + exploit IHbb; try eassumption; []; simplify. + exploit sem_update. apply H1. symmetry; eassumption. + eauto. simplify. econstructor. split. apply H3. + auto. } Qed. -Lemma rtlpar_trans_correct : - forall bb ge sp sem_st' sem_st st, - sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> - match_states sem_st st -> - exists st', RTLPar.step_instr_block ge sp st bb st' - /\ match_states sem_st' st'. -Proof. - induction bb using rev_ind. - { repeat econstructor. eapply abstract_interp_empty3 in H. - inv H. inv H0. constructor; congruence. } - { simplify. inv H0. repeat rewrite concat_app in H. simplify. - rewrite app_nil_r in H. - exploit sem_separate; eauto; inv_simp. - repeat econstructor. admit. admit. - } -Admitted. - Lemma abstract_execution_correct: - forall bb bb' cfi ge tge sp st st' tst, + forall bb bb' cfi cfi' ge tge sp st st' tst, RTLBlock.step_instr_list ge sp st bb st' -> ge_preserved ge tge -> - schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> + schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi') = true -> match_states st tst -> exists tst', RTLPar.step_instr_block tge sp tst bb' tst' /\ match_states st' tst'. Proof. intros. - unfold schedule_oracle in *. simplify. - exploit rtlblock_trans_correct; try eassumption; []; inv_simp. + unfold schedule_oracle in *. simplify. unfold empty_trees in H4. + exploit rtlblock_trans_correct; try eassumption; []; simplify. exploit abstract_execution_correct'; try solve [eassumption | apply state_lessdef_match_sem; eassumption]. apply match_states_commut. eauto. inv_simp. @@ -1074,18 +1110,6 @@ Proof. econstructor; congruence. Qed. -(*Lemma abstract_execution_correct_ld: - forall bb bb' cfi ge tge sp st st' tst, - RTLBlock.step_instr_list ge sp st bb st' -> - ge_preserved ge tge -> - schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> - match_states_ld st tst -> - exists tst', RTLPar.step_instr_block tge sp tst bb' tst' - /\ match_states st' tst'. -Proof. - intros.*) -*) - (*| Top-level functions =================== diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index bb1cf97..fc3272a 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -(*Require Import compcert.backend.Registers. +Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Linking. @@ -36,20 +36,22 @@ Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) := Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: - forall f tf res sp pc rs rs', + forall f tf res sp pc rs rs' ps ps', transl_function f = OK tf -> (forall x, rs !! x = rs' !! x) -> - match_stackframes (Stackframe res f sp pc rs) - (Stackframe res tf sp pc rs'). + (forall x, ps !! x = ps' !! x) -> + match_stackframes (Stackframe res f sp pc rs ps) + (Stackframe res tf sp pc rs' ps). Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: - forall sf f sp pc rs rs' m sf' tf + forall sf f sp pc rs rs' m sf' tf ps ps' (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') - (REG: forall x, rs !! x = rs' !! x), - match_states (State sf f sp pc rs m) - (State sf' tf sp pc rs' m) + (REG: forall x, rs !! x = rs' !! x) + (REG: forall x, ps !! x = ps' !! x), + match_states (State sf f sp pc rs ps m) + (State sf' tf sp pc rs' ps' m) | match_returnstate: forall stack stack' v m (STACKS: list_forall2 match_stackframes stack stack'), @@ -284,7 +286,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. match_states s r -> exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. - induction 1; repeat semantics_simpl; + (*induction 1; repeat semantics_simpl; try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)]. { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). eapply eval_builtin_args_eq. eapply REG. @@ -301,7 +303,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. unfold regmap_optget. destruct or. rewrite REG. constructor; eauto. constructor; eauto. } - Qed. + Qed.*) Admitted. Theorem transl_step_correct : forall (S1 : RTLBlock.state) t S2, @@ -377,4 +379,3 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. -*) -- cgit