diff options
Diffstat (limited to 'kvx/lib/Machblockgenproof.v')
| -rw-r--r-- | kvx/lib/Machblockgenproof.v | 138 |
1 files changed, 69 insertions, 69 deletions
diff --git a/kvx/lib/Machblockgenproof.v b/kvx/lib/Machblockgenproof.v index dfb97bfe..fc722887 100644 --- a/kvx/lib/Machblockgenproof.v +++ b/kvx/lib/Machblockgenproof.v @@ -146,16 +146,16 @@ Lemma parent_sp_preserved: forall s, Mach.parent_sp s = parent_sp (trans_stack s). Proof. - unfold parent_sp. unfold Mach.parent_sp. destruct s; simpl; auto. - unfold trans_stackframe. destruct s; simpl; auto. + unfold parent_sp. unfold Mach.parent_sp. destruct s; cbn; auto. + unfold trans_stackframe. destruct s; cbn; auto. Qed. Lemma parent_ra_preserved: forall s, Mach.parent_ra s = parent_ra (trans_stack s). Proof. - unfold parent_ra. unfold Mach.parent_ra. destruct s; simpl; auto. - unfold trans_stackframe. destruct s; simpl; auto. + unfold parent_ra. unfold Mach.parent_ra. destruct s; cbn; auto. + unfold trans_stackframe. destruct s; cbn; auto. Qed. Lemma external_call_preserved: @@ -175,11 +175,11 @@ Proof. destruct i; try (constructor 2; split; auto; discriminate ). destruct (peq l0 l) as [P|P]. - constructor. subst l0; split; auto. - revert H. unfold Mach.find_label. simpl. rewrite peq_true. + revert H. unfold Mach.find_label. cbn. rewrite peq_true. intros H; injection H; auto. - constructor 2. split. + intro F. injection F. intros. contradict P; auto. - + revert H. unfold Mach.find_label. simpl. rewrite peq_false; auto. + + revert H. unfold Mach.find_label. cbn. rewrite peq_false; auto. Qed. Lemma find_label_is_end_block_not_label i l c bl: @@ -192,24 +192,24 @@ Proof. remember (is_label l _) as b. cutrewrite (b = false); auto. subst; unfold is_label. - destruct i; simpl in * |- *; try (destruct (in_dec l nil); intuition). + destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition). inversion H. destruct (in_dec l (l0::nil)) as [H6|H6]; auto. - simpl in H6; intuition try congruence. + cbn in H6; intuition try congruence. Qed. Lemma find_label_at_begin l bh bl: In l (header bh) -> find_label l (bh :: bl) = Some (bh::bl). Proof. - unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; simpl; auto. + unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; cbn; auto. Qed. Lemma find_label_add_label_diff l bh bl: ~(In l (header bh)) -> find_label l (bh::bl) = find_label l bl. Proof. - unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; simpl; auto. + unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; cbn; auto. Qed. Definition concat (h: list label) (c: code): code := @@ -227,18 +227,18 @@ Proof. rewrite <- is_trans_code_inv in * |-. induction Heqbl. + (* Tr_nil *) - intros; exists (l::nil); simpl in * |- *; intuition. + intros; exists (l::nil); cbn in * |- *; intuition. discriminate. + (* Tr_end_block *) intros. exploit Mach_find_label_split; eauto. clear H0; destruct 1 as [(H0&H2)|(H0&H2)]. - - subst. rewrite find_label_at_begin; simpl; auto. + - subst. rewrite find_label_at_begin; cbn; auto. inversion H as [mbi H1 H2| | ]. subst. inversion Heqbl. subst. - exists (l :: nil); simpl; eauto. + exists (l :: nil); cbn; eauto. - exploit IHHeqbl; eauto. destruct 1 as (h & H3 & H4). exists h. @@ -251,21 +251,21 @@ Proof. - subst. inversion H0 as [H1]. clear H0. - erewrite find_label_at_begin; simpl; eauto. + erewrite find_label_at_begin; cbn; eauto. subst_is_trans_code Heqbl. - exists (l :: nil); simpl; eauto. + exists (l :: nil); cbn; eauto. - subst; assert (H: l0 <> l); try congruence; clear H0. exploit IHHeqbl; eauto. clear IHHeqbl Heqbl. intros (h & H3 & H4). - simpl; unfold is_label, add_label; simpl. - destruct (in_dec l (l0::header bh)) as [H5|H5]; simpl in H5. + cbn; unfold is_label, add_label; cbn. + destruct (in_dec l (l0::header bh)) as [H5|H5]; cbn in H5. * destruct H5; try congruence. - exists (l0::h); simpl; intuition. + exists (l0::h); cbn; intuition. rewrite find_label_at_begin in H4; auto. apply f_equal. inversion H4 as [H5]. clear H4. - destruct (trans_code c'); simpl in * |- *; - inversion H5; subst; simpl; auto. + destruct (trans_code c'); cbn in * |- *; + inversion H5; subst; cbn; auto. * exists h. intuition. erewrite <- find_label_add_label_diff; eauto. + (* Tr_add_basic *) @@ -318,12 +318,12 @@ Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exe Lemma size_add_label l bh: size (add_label l bh) = size bh + 1. Proof. - unfold add_label, size; simpl; omega. + unfold add_label, size; cbn; omega. Qed. Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1. Proof. - intro H. unfold add_basic, size; rewrite H; simpl. omega. + intro H. unfold add_basic, size; rewrite H; cbn. omega. Qed. @@ -418,8 +418,8 @@ Proof. + exists lbl. unfold trans_inst in H1. destruct i; congruence. - + unfold add_basic in H; simpl in H; congruence. - + unfold cfi_bblock in H; simpl in H; congruence. + + unfold add_basic in H; cbn in H; congruence. + + unfold cfi_bblock in H; cbn in H; congruence. Qed. Local Hint Resolve Mlabel_is_not_basic: core. @@ -433,11 +433,11 @@ Proof. intros b bl H; remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]; inversion H as [|d0 d1 d2 H0 H1| |]; subst; - try (rewrite <- Heqti in * |- *); simpl in * |- *; + try (rewrite <- Heqti in * |- *); cbn in * |- *; try congruence. + (* label at end block *) inversion H1; subst. inversion H0; subst. - assert (X:i=Mlabel lbl). { destruct i; simpl in Heqti; congruence. } + assert (X:i=Mlabel lbl). { destruct i; cbn in Heqti; congruence. } subst. repeat econstructor; eauto. + (* label at mid block *) exploit IHc; eauto. @@ -451,12 +451,12 @@ Proof. assert (X:(trans_inst i) = MB_basic bi ). { repeat econstructor; congruence. } repeat econstructor; congruence. - exists (i::c), c, c. - repeat econstructor; eauto; inversion H0; subst; repeat econstructor; simpl; try congruence. + repeat econstructor; eauto; inversion H0; subst; repeat econstructor; cbn; try congruence. * exploit (add_to_new_block_is_label i0); eauto. - intros (l & H8); subst; simpl; congruence. + intros (l & H8); subst; cbn; congruence. * exploit H3; eauto. * exploit (add_to_new_block_is_label i0); eauto. - intros (l & H8); subst; simpl; congruence. + intros (l & H8); subst; cbn; congruence. + (* basic at mid block *) inversion H1; subst. exploit IHc; eauto. @@ -476,7 +476,7 @@ Lemma step_simu_header st f sp rs m s c h c' t: starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> s = Mach.State st f sp c' rs m /\ t = E0. Proof. - induction 1; simpl; intros hs; try (inversion hs; tauto). + induction 1; cbn; intros hs; try (inversion hs; tauto). inversion hs as [|n1 s1 t1 t2 s2 t3 s3 H1]. inversion H1. subst. auto. Qed. @@ -487,21 +487,21 @@ Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' -> exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'. Proof. - destruct i; simpl in * |-; + destruct i; cbn in * |-; (discriminate || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)). - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro. destruct H3 as (tf & A & B). subst. eapply A. - all: simpl; rewrite <- parent_sp_preserved; auto. - - eapply exec_MBop; eauto. rewrite <- H. destruct o; simpl; auto. destruct (rs ## l); simpl; auto. + all: cbn; rewrite <- parent_sp_preserved; auto. + - eapply exec_MBop; eauto. rewrite <- H. destruct o; cbn; auto. destruct (rs ## l); cbn; auto. unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBstore; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. Qed. @@ -511,7 +511,7 @@ Lemma star_step_simu_body_step s f sp c bdy c': starN (Mach.step (inv_trans_rao rao)) ge (length bdy) (Mach.State s f sp c rs m) t s' -> exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp bdy rs m rs' m'. Proof. - induction 1; simpl. + induction 1; cbn. + intros. inversion H. exists rs. exists m. auto. + intros. inversion H0. exists rs. exists m. auto. + intros. inversion H1; subst. @@ -531,15 +531,15 @@ Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved f Lemma match_states_concat_trans_code st f sp c rs m h: match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m). Proof. - intros; constructor 1; simpl. + intros; constructor 1; cbn. + intros (t0 & s1' & H0) t s'. remember (trans_code _) as bl. destruct bl as [|bh bl]. { rewrite <- is_trans_code_inv in Heqbl; inversion Heqbl; inversion H0; congruence. } clear H0. - simpl; constructor 1; - intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; simpl in * |- *; - eapply exec_bblock; eauto; simpl; + cbn; constructor 1; + intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; cbn in * |- *; + eapply exec_bblock; eauto; cbn; inversion X2 as [cfi d1 d2 d3 H1|]; subst; eauto; inversion H1; subst; eauto. + intros H r; constructor 1; intro X; inversion X. @@ -551,7 +551,7 @@ Lemma step_simu_cfi_step (i: Mach.instruction) (cfi: control_flow_inst) (c: Mach Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp (i::c) rs m) t s' -> exists s2, cfi_step rao tge cfi (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s' s2. Proof. - destruct i; simpl in * |-; + destruct i; cbn in * |-; (intro H; intro Htc;apply is_trans_code_inv in Htc;rewrite Htc;inversion_clear H;intro X; inversion_clear X). * eapply ex_intro. intuition auto. @@ -561,8 +561,8 @@ Proof. intuition auto. eapply exec_MBtailcall;eauto. - rewrite <-H; exploit (find_function_ptr_same); eauto. - - simpl; rewrite <- parent_sp_preserved; auto. - - simpl; rewrite <- parent_ra_preserved; auto. + - cbn; rewrite <- parent_sp_preserved; auto. + - cbn; rewrite <- parent_ra_preserved; auto. * eapply ex_intro. intuition auto. eapply exec_MBbuiltin ;eauto. @@ -605,7 +605,7 @@ Proof. inversion H1; subst. exploit (step_simu_cfi_step); eauto. intros [s2 [Hcfi1 Hcfi3]]. - inversion H4. subst; simpl. + inversion H4. subst; cbn. autorewrite with trace_rewrite. exists s2. split;eauto. @@ -616,7 +616,7 @@ Lemma simu_end_block: starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' -> exists s2', step rao tge (trans_state s1) t s2' /\ match_states s1' s2'. Proof. - destruct s1; simpl. + destruct s1; cbn. + (* State *) remember (trans_code _) as tc. rewrite <- is_trans_code_inv in Heqtc. @@ -624,7 +624,7 @@ Proof. destruct tc as [|b bl]. { (* nil => absurd *) inversion Heqtc. subst. - unfold dist_end_block_code; simpl. + unfold dist_end_block_code; cbn. inversion_clear H; inversion_clear H0. } @@ -659,7 +659,7 @@ Proof. intros t s1' H; inversion_clear H. eapply ex_intro; constructor 1; eauto. inversion H1; subst; clear H1. - inversion_clear H0; simpl. + inversion_clear H0; cbn. - (* function_internal*) cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto. eapply exec_function_internal; eauto. @@ -674,7 +674,7 @@ Proof. intros t s1' H; inversion_clear H. eapply ex_intro; constructor 1; eauto. inversion H1; subst; clear H1. - inversion_clear H0; simpl. + inversion_clear H0; cbn. eapply exec_return. Qed. @@ -685,10 +685,10 @@ dist_end_block_code (i :: c) = 0. Proof. unfold dist_end_block_code. intro H. destruct H as [cfi H]. - destruct i;simpl in H;try(congruence); ( + destruct i;cbn in H;try(congruence); ( remember (trans_code _) as bl; rewrite <- is_trans_code_inv in Heqbl; - inversion Heqbl; subst; simpl in * |- *; try (congruence)). + inversion Heqbl; subst; cbn in * |- *; try (congruence)). Qed. Theorem transf_program_correct: @@ -697,23 +697,23 @@ Proof. apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state). (* simu_mid_block *) - intros s1 t s1' H1 H2. - destruct H1; simpl in * |- *; omega || (intuition auto); - destruct H2; eapply cfi_dist_end_block; simpl; eauto. + destruct H1; cbn in * |- *; omega || (intuition auto); + destruct H2; eapply cfi_dist_end_block; cbn; eauto. (* public_preserved *) - apply senv_preserved. (* match_initial_states *) - - intros. simpl. + - intros. cbn. eapply ex_intro; constructor 1. eapply match_states_trans_state. destruct H. split. apply init_mem_preserved; auto. rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved. (* match_final_states *) - - intros. simpl. destruct H. split with (r := r); auto. + - intros. cbn. destruct H. split with (r := r); auto. (* final_states_end_block *) - - intros. simpl in H0. + - intros. cbn in H0. inversion H0. - inversion H; simpl; auto. + inversion H; cbn; auto. all: try (subst; discriminate). apply cfi_dist_end_block; exists MBreturn; eauto. (* simu_end_block *) @@ -733,8 +733,8 @@ Proof. intro H; destruct c as [|i' c]. { inversion H. } remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]. - - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; simpl in * |- *; try congruence ). - exists nil; simpl; eexists. eapply Tr_add_label; eauto. + - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ). + exists nil; cbn; eexists. eapply Tr_add_label; eauto. - (*i=basic*) destruct i'. 10: { exists (add_to_new_bblock (MB_basic bi)::nil). exists b. @@ -742,11 +742,11 @@ Proof. rewrite Heqti. eapply Tr_end_block; eauto. rewrite <-Heqti. - eapply End_basic. inversion H; try(simpl; congruence). - simpl in H5; congruence. } - all: try(exists nil; simpl; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). + eapply End_basic. inversion H; try(cbn; congruence). + cbn in H5; congruence. } + all: try(exists nil; cbn; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). - (*i=cfi*) - destruct i; try(simpl in Heqti; congruence). + destruct i; try(cbn in Heqti; congruence). all: exists (add_to_new_bblock (MB_cfi cfi)::nil); exists b; cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; rewrite Heqti; @@ -768,13 +768,13 @@ Qed. (* FIXME: these two lemma should go into [Coqlib.v] *) Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). Proof. - induction l1; simpl; auto with coqlib. + induction l1; cbn; auto with coqlib. Qed. Hint Resolve is_tail_app: coqlib. Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. Proof. - induction l1; simpl; auto with coqlib. + induction l1; cbn; auto with coqlib. intros l2 l3 H; inversion H; eauto with coqlib. Qed. Hint Resolve is_tail_app_inv: coqlib. @@ -787,17 +787,17 @@ Proof. - intros; subst. remember (trans_code (Mcall _ _::c)) as tc2. rewrite <- is_trans_code_inv in Heqtc2. - inversion Heqtc2; simpl in * |- *; subst; try congruence. + inversion Heqtc2; cbn in * |- *; subst; try congruence. subst_is_trans_code H1. eapply ex_intro; eauto with coqlib. - intros; exploit IHis_tail; eauto. clear IHis_tail. intros (b & Hb). inversion Hb; clear Hb. * exploit (trans_code_monotonic i c2); eauto. intros (l' & b' & Hl'); rewrite Hl'. - exists b'; simpl; eauto with coqlib. + exists b'; cbn; eauto with coqlib. * exploit (trans_code_monotonic i c2); eauto. intros (l' & b' & Hl'); rewrite Hl'. - simpl; eapply ex_intro. + cbn; eapply ex_intro. eapply is_tail_trans; eauto with coqlib. Qed. |