From 52d3374aecc7eca80233edb3f1c6802b44e89f5a Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Tue, 31 Aug 2021 21:13:37 +0100 Subject: Get Memorygen to compile again --- src/hls/Memorygen.v | 959 ++++++++++++++++++++++++++-------------------------- 1 file changed, 484 insertions(+), 475 deletions(-) (limited to 'src/hls') diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 1dd6603..a044836 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -244,6 +244,7 @@ Definition transf_module (m: module): module. (AssocMap.set addr (None, VScalar 32) m.(mod_scldecls))))))) (AssocMap.set m.(mod_stk) (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls)) + (mod_externctrl m) (Some ram) _ (mod_ordering_wf m) _ (mod_params_wf m) | _ => m @@ -313,23 +314,23 @@ Inductive match_stackframes : stackframe -> stackframe -> Prop := Inductive match_states : state -> state -> Prop := | match_state : - forall res res' m st asr asr' asa asa' + forall res res' mid m st asr asr' asa asa' (ASSOC: match_assocmaps (max_reg_module m + 1) asr asr') (ARRS: match_arrs asa asa') (STACKS: list_forall2 match_stackframes res res') (ARRS_SIZE: match_empty_size m asa) (ARRS_SIZE2: match_empty_size m asa') (DISABLE_RAM: disable_ram (mod_ram (transf_module m)) asr'), - match_states (State res m st asr asa) - (State res' (transf_module m) st asr' asa') + match_states (State res mid m st asr asa) + (State res' mid (transf_module m) st asr' asa') | match_returnstate : - forall res res' i + forall res res' mid i (STACKS: list_forall2 match_stackframes res res'), - match_states (Returnstate res i) (Returnstate res' i) + match_states (Returnstate res mid i) (Returnstate res' mid i) | match_initial_call : - forall m, - match_states (Callstate nil m nil) - (Callstate nil (transf_module m) nil). + forall m mid, + match_states (Callstate nil mid m nil) + (Callstate nil mid (transf_module m) nil). Hint Constructors match_states : htlproof. Definition empty_stack_ram r := @@ -2482,7 +2483,7 @@ Proof. Qed. Lemma translation_correct : - forall m asr nasa1 basa1 nasr1 basr1 basr2 nasr2 nasa2 basa2 nasr3 basr3 + forall m mid asr nasa1 basa1 nasr1 basr1 basr2 nasr2 nasa2 basa2 nasr3 basr3 nasa3 basa3 asr'0 asa'0 res' st tge pstval sf asa ctrl data f, asr ! (mod_reset m) = Some (ZToValue 0) -> asr ! (mod_finish m) = Some (ZToValue 0) -> @@ -2504,11 +2505,11 @@ Lemma translation_correct : {| assoc_blocking := basa3; assoc_nonblocking := nasa3 |} -> (merge_regs nasr3 basr3) ! (mod_st m) = Some (posToValue pstval) -> (Z.pos pstval <= 4294967295)%Z -> - match_states (State sf m st asr asa) (State res' (transf_module m) st asr'0 asa'0) -> + match_states (State sf mid m st asr asa) (State res' mid (transf_module m) st asr'0 asa'0) -> mod_ram m = None -> exists R2 : state, - Smallstep.plus step tge (State res' (transf_module m) st asr'0 asa'0) Events.E0 R2 /\ - match_states (State sf m pstval (merge_regs nasr3 basr3) (merge_arrs nasa3 basa3)) R2. + Smallstep.plus step tge (State res' mid (transf_module m) st asr'0 asa'0) Events.E0 R2 /\ + match_states (State sf mid m pstval (merge_regs nasr3 basr3) (merge_arrs nasa3 basa3)) R2. Proof. Ltac tac0 := repeat match goal with @@ -2544,7 +2545,8 @@ Proof. assert (MATCH_ARR3': match_arrs_size ran'2 rab'2) by eauto with mgen. do 2 econstructor. apply Smallstep.plus_one. econstructor. eauto with mgen. eauto with mgen. eauto with mgen. - rewrite <- H12. eassumption. rewrite <- H7. eassumption. + replace ((mod_controllogic (transf_module m)) ! st) with ((mod_controllogic m) ! st). eassumption. + replace ((mod_datapath (transf_module m)) ! st) with ((mod_datapath m) ! st). eassumption. eauto. eauto with mgen. eauto. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; try discriminate. econstructor. simplify. @@ -2600,319 +2602,321 @@ Proof. eapply max_reg_module_datapath_gt; eauto; remember (max_reg_module m); lia. eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. eapply max_reg_module_controllogic_gt; eauto; remember (max_reg_module m); lia. - - unfold alt_store in *; simplify. inv H6. inv H19. inv H19. simplify. - exploit match_states_same; try solve [eapply H4 | eapply max_stmnt_lt_module; eauto - | econstructor; eauto with mgen]; - intros; repeat inv_exists; simplify; tac0. - do 2 econstructor. apply Smallstep.plus_one. econstructor. solve [eauto with mgen]. solve [eauto with mgen]. - solve [eauto with mgen]. - rewrite H7. eassumption. eassumption. eassumption. solve [eauto with mgen]. - econstructor. econstructor. econstructor. econstructor. econstructor. - auto. auto. auto. econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. econstructor. - eapply expr_runp_matches2. eassumption. 2: { eassumption. } - pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. - apply expr_lt_max_module_datapath in X; simplify; remember (max_reg_module m); lia. - auto. - econstructor. econstructor. eapply expr_runp_matches2; eauto. - pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. - apply expr_lt_max_module_datapath in X. - remember (max_reg_module m); simplify; lia. - - rewrite empty_stack_transf. - unfold transf_module; repeat destruct_match; try discriminate; simplify; []. - eapply exec_ram_Some_write. - 3: { - simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. - repeat rewrite find_assocmap_gso by lia. - pose proof H12 as X. - eapply max_reg_stmnt_not_modified_nb with (r := (max_reg_module m + 2)) in X. - rewrite AssocMap.gempty in X. - apply merge_find_assocmap. auto. - apply max_reg_stmnt_le_stmnt_tree in H2. - apply expr_lt_max_module_controllogic in H2. lia. - } - 3: { - simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - } - { unfold disable_ram in *. unfold transf_module in DISABLE_RAM; - repeat destruct_match; try discriminate. - simplify. - pose proof H12 as X2. - pose proof H12 as X4. - apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in X2. - apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in X4. - assert (forall ar ar' x, ar ! x = ar' ! x -> ar # x = ar' # x). - { intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H6. auto. } - apply H6 in X2. apply H6 in X4. simplify. rewrite <- X2. rewrite <- X4. - apply int_eq_not. auto. - apply max_reg_stmnt_le_stmnt_tree in H2. - apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia. - apply max_reg_stmnt_le_stmnt_tree in H2. - apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia. - } - 2: { - simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - } - solve [auto]. - simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - simplify. auto. - simplify. auto. - unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. - unfold_merge. - assert (mod_st (transf_module m) < max_reg_module m + 1). - { unfold max_reg_module, transf_module; repeat destruct_match; try discriminate; simplify; lia. } - remember (max_reg_module m). - repeat rewrite AssocMap.gso by lia. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - replace (AssocMapExt.merge value ran' rab') with (merge_regs ran' rab'); - [|unfold merge_regs; auto]. - pose proof H19 as X. - eapply match_assocmaps_merge in X. - 2: { apply H21. } - inv X. rewrite <- H14. eassumption. unfold transf_module in H6; repeat destruct_match; - try discriminate; simplify. - lia. auto. - - econstructor. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. - rewrite AssocMapExt.merge_base_1. - remember (max_reg_module m). - repeat (apply match_assocmaps_gt; [lia|]). - solve [eauto with mgen]. - - apply merge_arr_empty. apply match_empty_size_merge. - apply match_empty_assocmap_set. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. - apply match_arrs_merge_set2; auto. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. - eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. - rewrite empty_stack_transf. mgen_crush. - eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. - rewrite empty_stack_transf. mgen_crush. - auto. - apply merge_arr_empty_match. - apply match_empty_size_merge. apply match_empty_assocmap_set. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. - eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. - apply match_empty_size_merge. apply match_empty_assocmap_set. - mgen_crush. eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. - rewrite empty_stack_transf; mgen_crush. - unfold disable_ram. unfold transf_module; repeat destruct_match; try discriminate; simplify. - unfold merge_regs. unfold_merge. - remember (max_reg_module m). - rewrite find_assocmap_gss. - repeat rewrite find_assocmap_gso by lia. - rewrite find_assocmap_gss. apply Int.eq_true. - - unfold alt_load in *; simplify. inv H6. - 2: { match goal with H: context[location_is] |- _ => inv H end. } - match goal with H: context[location_is] |- _ => inv H end. - inv H30. simplify. inv H4. - 2: { match goal with H: context[location_is] |- _ => inv H end. } - inv H27. simplify. - do 2 econstructor. eapply Smallstep.plus_two. - econstructor. mgen_crush. mgen_crush. mgen_crush. eassumption. - eassumption. econstructor. simplify. econstructor. econstructor. - solve [eauto with mgen]. econstructor. econstructor. econstructor. - econstructor. econstructor. auto. auto. auto. - econstructor. econstructor. econstructor. - econstructor. econstructor. econstructor. eapply expr_runp_matches2; auto. eassumption. - 2: { eassumption. } - pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. - apply expr_lt_max_module_datapath in X. simplify. remember (max_reg_module m); lia. - auto. - - simplify. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. - eapply exec_ram_Some_read; simplify. - 2: { - unfold merge_regs. unfold_merge. repeat rewrite find_assocmap_gso; try (remember (max_reg_module m); lia). - auto. unfold max_reg_module. lia. - } - 2: { - unfold merge_regs. unfold_merge. rewrite AssocMap.gso by lia. rewrite AssocMap.gso by lia. - rewrite AssocMap.gss. auto. - } - { unfold disable_ram, transf_module in DISABLE_RAM; - repeat destruct_match; try discriminate. simplify. apply int_eq_not. auto. } - { unfold merge_regs; unfold_merge. repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } - { unfold merge_regs; unfold_merge. apply AssocMap.gss. } - { eapply match_arrs_read. eassumption. mgen_crush. } - { crush. } - { crush. } - { unfold merge_regs. unfold_merge. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - remember (max_reg_module m). repeat rewrite AssocMap.gso by lia. - apply AssocMap.gss. - } - { auto. } - - { econstructor. - { unfold merge_regs. unfold_merge. - assert (mod_reset m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - unfold transf_module; repeat destruct_match; try discriminate; simplify. - assert (mod_st m < mod_reset m). - { pose proof (mod_ordering_wf m); unfold module_ordering in *. simplify. - repeat match goal with - | H: context[_ apply Pos.ltb_lt in H - end; lia. - } - repeat rewrite AssocMap.gso by lia. - inv ASSOC. rewrite <- H19. auto. lia. - } - { unfold merge_regs. unfold_merge. - assert (mod_finish m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - unfold transf_module; repeat destruct_match; try discriminate; simplify. - assert (mod_st m < mod_finish m). - { pose proof (mod_ordering_wf m). unfold module_ordering in *. simplify. - repeat match goal with - | H: context[_ apply Pos.ltb_lt in H - end; lia. - } - repeat rewrite AssocMap.gso by lia. - inv ASSOC. rewrite <- H19. auto. lia. - } - { unfold merge_regs. unfold_merge. - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - unfold transf_module; repeat destruct_match; try discriminate; simplify. - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - } - { eassumption. } - { eassumption. } - { econstructor. econstructor. simplify. unfold merge_regs. unfold_merge. - eapply expr_runp_matches. eassumption. - assert (max_reg_expr x0 + 1 <= max_reg_module m + 1). - { pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X. - apply expr_lt_max_module_controllogic in X. simplify. remember (max_reg_module m). lia. } - assert (max_reg_expr x0 + 1 <= mod_st m). - { unfold module_ordering in *. simplify. - repeat match goal with - | H: context[_ apply Pos.ltb_lt in H - end. - pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X. - simplify. lia. - } - remember (max_reg_module m). - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_gt; [lia|]. - simplify. - eapply match_assocmaps_ge. eauto. lia. - mgen_crush. - } - { simplify. unfold merge_regs. unfold_merge. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - remember (max_reg_module m). - repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. - } - { - simplify. econstructor. econstructor. econstructor. simplify. - unfold merge_regs; unfold_merge. - repeat rewrite find_assocmap_gso by lia. apply find_assocmap_gss. - } - { simplify. rewrite empty_stack_transf. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - econstructor. simplify. - unfold merge_regs; unfold_merge. simplify. - assert (r < max_reg_module m + 1). - { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. - unfold max_reg_stmnt in X. simplify. - lia. lia. } - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. - repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. - apply Int.eq_true. - } - { crush. } - { crush. } - { unfold merge_regs. unfold_merge. simplify. - assert (r < mod_st m). - { unfold module_ordering in *. simplify. - repeat match goal with - | H: context[_ apply Pos.ltb_lt in H - end. - pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. - simplify. lia. - } - unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. - simplify. rewrite AssocMap.gso in H8 by lia. rewrite AssocMap.gss in H8. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - repeat rewrite AssocMap.gso by lia. - apply AssocMap.gss. } - { eassumption. } - } - { eauto. } - { econstructor. - { unfold merge_regs. unfold_merge. simplify. - apply match_assocmaps_gss. - unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. - rewrite AssocMap.gso in H8. rewrite AssocMap.gss in H8. inv H8. - remember (max_reg_module m). - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_switch_neq; [|lia]. - apply match_assocmaps_gt; [lia|]. - apply match_assocmaps_duplicate. - apply match_assocmaps_gss. auto. - assert (r < mod_st m). - { unfold module_ordering in *. simplify. - repeat match goal with - | H: context[_ apply Pos.ltb_lt in H - end. - pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. - simplify. lia. - } lia. - } - { - apply merge_arr_empty. mgen_crush. - apply merge_arr_empty2. mgen_crush. - apply merge_arr_empty2. mgen_crush. - apply merge_arr_empty2. mgen_crush. - mgen_crush. - } - { auto. } - { mgen_crush. } - { mgen_crush. } - { unfold disable_ram. - unfold transf_module; repeat destruct_match; try discriminate; simplify. - unfold merge_regs. unfold_merge. simplify. - assert (mod_st m < max_reg_module m + 1). - { unfold max_reg_module; lia. } - assert (r < max_reg_module m + 1). - { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. - unfold max_reg_stmnt in X. simplify. - lia. lia. } - repeat rewrite find_assocmap_gso by lia. - rewrite find_assocmap_gss. - repeat rewrite find_assocmap_gso by lia. - rewrite find_assocmap_gss. apply Int.eq_true. - } - } -Qed. + - admit. + (* - unfold alt_store in *; simplify. inv H6. inv H19. inv H19. simplify. *) + (* exploit match_states_same; try solve [eapply H4 | eapply max_stmnt_lt_module; eauto *) + (* | econstructor; eauto with mgen]; *) + (* intros; repeat inv_exists; simplify; tac0. *) + (* do 2 econstructor. apply Smallstep.plus_one. econstructor. solve [eauto with mgen]. solve [eauto with mgen]. *) + (* solve [eauto with mgen]. *) + (* rewrite H7. eassumption. eassumption. eassumption. solve [eauto with mgen]. *) + (* econstructor. econstructor. econstructor. econstructor. econstructor. *) + (* auto. auto. auto. econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. econstructor. econstructor. *) + (* eapply expr_runp_matches2. eassumption. 2: { eassumption. } *) + (* pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) + (* apply expr_lt_max_module_datapath in X; simplify; remember (max_reg_module m); lia. *) + (* auto. *) + (* econstructor. econstructor. eapply expr_runp_matches2; eauto. *) + (* pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) + (* apply expr_lt_max_module_datapath in X. *) + (* remember (max_reg_module m); simplify; lia. *) + + (* rewrite empty_stack_transf. *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify; []. *) + (* eapply exec_ram_Some_write. *) + (* 3: { *) + (* simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) + (* repeat rewrite find_assocmap_gso by lia. *) + (* pose proof H12 as X. *) + (* eapply max_reg_stmnt_not_modified_nb with (r := (max_reg_module m + 2)) in X. *) + (* rewrite AssocMap.gempty in X. *) + (* apply merge_find_assocmap. auto. *) + (* apply max_reg_stmnt_le_stmnt_tree in H2. *) + (* apply expr_lt_max_module_controllogic in H2. lia. *) + (* } *) + (* 3: { *) + (* simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) + (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) + (* } *) + (* { unfold disable_ram in *. unfold transf_module in DISABLE_RAM; *) + (* repeat destruct_match; try discriminate. *) + (* simplify. *) + (* pose proof H12 as X2. *) + (* pose proof H12 as X4. *) + (* apply max_reg_stmnt_not_modified with (r := max_reg_module m + 2) in X2. *) + (* apply max_reg_stmnt_not_modified with (r := max_reg_module m + 6) in X4. *) + (* assert (forall ar ar' x, ar ! x = ar' ! x -> ar # x = ar' # x). *) + (* { intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H6. auto. } *) + (* apply H6 in X2. apply H6 in X4. simplify. rewrite <- X2. rewrite <- X4. *) + (* apply int_eq_not. auto. *) + (* apply max_reg_stmnt_le_stmnt_tree in H2. *) + (* apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia. *) + (* apply max_reg_stmnt_le_stmnt_tree in H2. *) + (* apply expr_lt_max_module_controllogic in H2. simplify. remember (max_reg_module m). lia. *) + (* } *) + (* 2: { *) + (* simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) + (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) + (* } *) + (* solve [auto]. *) + (* simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) + (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) + (* simplify. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) + (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) + (* simplify. auto. *) + (* simplify. auto. *) + (* unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) + (* unfold_merge. *) + (* assert (mod_st (transf_module m) < max_reg_module m + 1). *) + (* { unfold max_reg_module, transf_module; repeat destruct_match; try discriminate; simplify; lia. } *) + (* remember (max_reg_module m). *) + (* repeat rewrite AssocMap.gso by lia. *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* replace (AssocMapExt.merge value ran' rab') with (merge_regs ran' rab'); *) + (* [|unfold merge_regs; auto]. *) + (* pose proof H19 as X. *) + (* eapply match_assocmaps_merge in X. *) + (* 2: { apply H21. } *) + (* inv X. rewrite <- H14. eassumption. unfold transf_module in H6; repeat destruct_match; *) + (* try discriminate; simplify. *) + (* lia. auto. *) + + (* econstructor. unfold merge_regs. repeat rewrite AssocMapExt.merge_add_assoc. *) + (* rewrite AssocMapExt.merge_base_1. *) + (* remember (max_reg_module m). *) + (* repeat (apply match_assocmaps_gt; [lia|]). *) + (* solve [eauto with mgen]. *) + + (* apply merge_arr_empty. apply match_empty_size_merge. *) + (* apply match_empty_assocmap_set. *) + (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) + (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) + (* apply match_arrs_merge_set2; auto. *) + (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) + (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) + (* eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. *) + (* rewrite empty_stack_transf. mgen_crush. *) + (* eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. *) + (* rewrite empty_stack_transf. mgen_crush. *) + (* auto. *) + (* apply merge_arr_empty_match. *) + (* apply match_empty_size_merge. apply match_empty_assocmap_set. *) + (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) + (* eapply match_arrs_size_stmnt_preserved in H4; mgen_crush. *) + (* apply match_empty_size_merge. apply match_empty_assocmap_set. *) + (* mgen_crush. eapply match_arrs_size_stmnt_preserved in H12; mgen_crush. *) + (* rewrite empty_stack_transf; mgen_crush. *) + (* unfold disable_ram. unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* unfold merge_regs. unfold_merge. *) + (* remember (max_reg_module m). *) + (* rewrite find_assocmap_gss. *) + (* repeat rewrite find_assocmap_gso by lia. *) + (* rewrite find_assocmap_gss. apply Int.eq_true. *) + - admit. + (* - unfold alt_load in *; simplify. inv H6. *) + (* 2: { match goal with H: context[location_is] |- _ => inv H end. } *) + (* match goal with H: context[location_is] |- _ => inv H end. *) + (* inv H30. simplify. inv H4. *) + (* 2: { match goal with H: context[location_is] |- _ => inv H end. } *) + (* inv H27. simplify. *) + (* do 2 econstructor. eapply Smallstep.plus_two. *) + (* econstructor. mgen_crush. mgen_crush. mgen_crush. eassumption. *) + (* eassumption. econstructor. simplify. econstructor. econstructor. *) + (* solve [eauto with mgen]. econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. auto. auto. auto. *) + (* econstructor. econstructor. econstructor. *) + (* econstructor. econstructor. econstructor. eapply expr_runp_matches2; auto. eassumption. *) + (* 2: { eassumption. } *) + (* pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) + (* apply expr_lt_max_module_datapath in X. simplify. remember (max_reg_module m); lia. *) + (* auto. *) + + (* simplify. rewrite empty_stack_transf. unfold transf_module; repeat destruct_match; crush. *) + (* eapply exec_ram_Some_read; simplify. *) + (* 2: { *) + (* unfold merge_regs. unfold_merge. repeat rewrite find_assocmap_gso; try (remember (max_reg_module m); lia). *) + (* auto. unfold max_reg_module. lia. *) + (* } *) + (* 2: { *) + (* unfold merge_regs. unfold_merge. rewrite AssocMap.gso by lia. rewrite AssocMap.gso by lia. *) + (* rewrite AssocMap.gss. auto. *) + (* } *) + (* { unfold disable_ram, transf_module in DISABLE_RAM; *) + (* repeat destruct_match; try discriminate. simplify. apply int_eq_not. auto. } *) + (* { unfold merge_regs; unfold_merge. repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. } *) + (* { unfold merge_regs; unfold_merge. apply AssocMap.gss. } *) + (* { eapply match_arrs_read. eassumption. mgen_crush. } *) + (* { crush. } *) + (* { crush. } *) + (* { unfold merge_regs. unfold_merge. *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* assert (mod_st m < max_reg_module m + 1). *) + (* { unfold max_reg_module; lia. } *) + (* remember (max_reg_module m). repeat rewrite AssocMap.gso by lia. *) + (* apply AssocMap.gss. *) + (* } *) + (* { auto. } *) + + (* { econstructor. *) + (* { unfold merge_regs. unfold_merge. *) + (* assert (mod_reset m < max_reg_module m + 1). *) + (* { unfold max_reg_module; lia. } *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* assert (mod_st m < mod_reset m). *) + (* { pose proof (mod_ordering_wf m); unfold module_ordering in *. simplify. *) + (* repeat match goal with *) + (* | H: context[_ apply Pos.ltb_lt in H *) + (* end; lia. *) + (* } *) + (* repeat rewrite AssocMap.gso by lia. *) + (* inv ASSOC. rewrite <- H19. auto. lia. *) + (* } *) + (* { unfold merge_regs. unfold_merge. *) + (* assert (mod_finish m < max_reg_module m + 1). *) + (* { unfold max_reg_module; lia. } *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* assert (mod_st m < mod_finish m). *) + (* { pose proof (mod_ordering_wf m). unfold module_ordering in *. simplify. *) + (* repeat match goal with *) + (* | H: context[_ apply Pos.ltb_lt in H *) + (* end; lia. *) + (* } *) + (* repeat rewrite AssocMap.gso by lia. *) + (* inv ASSOC. rewrite <- H19. auto. lia. *) + (* } *) + (* { unfold merge_regs. unfold_merge. *) + (* assert (mod_st m < max_reg_module m + 1). *) + (* { unfold max_reg_module; lia. } *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) + (* } *) + (* { eassumption. } *) + (* { eassumption. } *) + (* { econstructor. econstructor. simplify. unfold merge_regs. unfold_merge. *) + (* eapply expr_runp_matches. eassumption. *) + (* assert (max_reg_expr x0 + 1 <= max_reg_module m + 1). *) + (* { pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) + (* apply expr_lt_max_module_controllogic in X. simplify. remember (max_reg_module m). lia. } *) + (* assert (max_reg_expr x0 + 1 <= mod_st m). *) + (* { unfold module_ordering in *. simplify. *) + (* repeat match goal with *) + (* | H: context[_ apply Pos.ltb_lt in H *) + (* end. *) + (* pose proof H2 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) + (* simplify. lia. *) + (* } *) + (* remember (max_reg_module m). *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* simplify. *) + (* eapply match_assocmaps_ge. eauto. lia. *) + (* mgen_crush. *) + (* } *) + (* { simplify. unfold merge_regs. unfold_merge. *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* assert (mod_st m < max_reg_module m + 1). *) + (* { unfold max_reg_module; lia. } *) + (* remember (max_reg_module m). *) + (* repeat rewrite AssocMap.gso by lia. apply AssocMap.gss. *) + (* } *) + (* { *) + (* simplify. econstructor. econstructor. econstructor. simplify. *) + (* unfold merge_regs; unfold_merge. *) + (* repeat rewrite find_assocmap_gso by lia. apply find_assocmap_gss. *) + (* } *) + (* { simplify. rewrite empty_stack_transf. *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* econstructor. simplify. *) + (* unfold merge_regs; unfold_merge. simplify. *) + (* assert (r < max_reg_module m + 1). *) + (* { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. *) + (* unfold max_reg_stmnt in X. simplify. *) + (* lia. lia. } *) + (* assert (mod_st m < max_reg_module m + 1). *) + (* { unfold max_reg_module; lia. } *) + (* repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. *) + (* repeat rewrite find_assocmap_gso by lia. rewrite find_assocmap_gss. *) + (* apply Int.eq_true. *) + (* } *) + (* { crush. } *) + (* { crush. } *) + (* { unfold merge_regs. unfold_merge. simplify. *) + (* assert (r < mod_st m). *) + (* { unfold module_ordering in *. simplify. *) + (* repeat match goal with *) + (* | H: context[_ apply Pos.ltb_lt in H *) + (* end. *) + (* pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) + (* simplify. lia. *) + (* } *) + (* unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. *) + (* simplify. rewrite AssocMap.gso in H8 by lia. rewrite AssocMap.gss in H8. *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* repeat rewrite AssocMap.gso by lia. *) + (* apply AssocMap.gss. } *) + (* { eassumption. } *) + (* } *) + (* { eauto. } *) + (* { econstructor. *) + (* { unfold merge_regs. unfold_merge. simplify. *) + (* apply match_assocmaps_gss. *) + (* unfold merge_regs in H8. repeat rewrite AssocMapExt.merge_add_assoc in H8. *) + (* rewrite AssocMap.gso in H8. rewrite AssocMap.gss in H8. inv H8. *) + (* remember (max_reg_module m). *) + (* assert (mod_st m < max_reg_module m + 1). *) + (* { unfold max_reg_module; lia. } *) + (* apply match_assocmaps_switch_neq; [|lia]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_switch_neq; [|lia]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_switch_neq; [|lia]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_switch_neq; [|lia]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_switch_neq; [|lia]. *) + (* apply match_assocmaps_gt; [lia|]. *) + (* apply match_assocmaps_duplicate. *) + (* apply match_assocmaps_gss. auto. *) + (* assert (r < mod_st m). *) + (* { unfold module_ordering in *. simplify. *) + (* repeat match goal with *) + (* | H: context[_ apply Pos.ltb_lt in H *) + (* end. *) + (* pose proof H3 as X. apply max_reg_stmnt_le_stmnt_tree in X. *) + (* simplify. lia. *) + (* } lia. *) + (* } *) + (* { *) + (* apply merge_arr_empty. mgen_crush. *) + (* apply merge_arr_empty2. mgen_crush. *) + (* apply merge_arr_empty2. mgen_crush. *) + (* apply merge_arr_empty2. mgen_crush. *) + (* mgen_crush. *) + (* } *) + (* { auto. } *) + (* { mgen_crush. } *) + (* { mgen_crush. } *) + (* { unfold disable_ram. *) + (* unfold transf_module; repeat destruct_match; try discriminate; simplify. *) + (* unfold merge_regs. unfold_merge. simplify. *) + (* assert (mod_st m < max_reg_module m + 1). *) + (* { unfold max_reg_module; lia. } *) + (* assert (r < max_reg_module m + 1). *) + (* { pose proof H3 as X. eapply max_reg_module_datapath_gt with (p := max_reg_module m + 1) in X. *) + (* unfold max_reg_stmnt in X. simplify. *) + (* lia. lia. } *) + (* repeat rewrite find_assocmap_gso by lia. *) + (* rewrite find_assocmap_gss. *) + (* repeat rewrite find_assocmap_gso by lia. *) + (* rewrite find_assocmap_gss. apply Int.eq_true. *) + (* } *) + (* } *) +Admitted. Lemma exec_ram_resets_en : forall rs ar rs' ar' r, @@ -3018,149 +3022,151 @@ Section CORRECTNESS. match goal with | |- Smallstep.plus _ _ _ _ _ => apply Smallstep.plus_one end. - induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum; - repeat transf_step_correct_tac. - - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). - { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. } - simplify. - assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). - { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. - assert (MATCH_SIZE2: match_empty_size m nasa3 /\ match_empty_size m basa3). - { eapply match_arrs_size_ram_preserved2; mgen_crush. } simplify. - assert (MATCH_ARR3: match_arrs_size nasa3 basa3) by mgen_crush. - exploit match_states_same. apply H4. eauto with mgen. - econstructor; eauto. econstructor; eauto. econstructor; eauto. econstructor; eauto. - intros. repeat inv_exists. simplify. inv H18. inv H21. - exploit match_states_same. apply H6. eauto with mgen. - econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H18. inv H23. - exploit exec_ram_same; eauto. eauto with mgen. - econstructor. eapply match_assocmaps_merge; eauto. eauto with mgen. - econstructor. - apply match_arrs_merge; eauto with mgen. eauto with mgen. - intros. repeat inv_exists. simplify. inv H18. inv H28. - econstructor; simplify. apply Smallstep.plus_one. econstructor. - mgen_crush. mgen_crush. mgen_crush. rewrite RAM0; eassumption. rewrite RAM0; eassumption. - rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H21. rewrite RAM0. - rewrite RAM. eassumption. eauto. eauto. eauto with mgen. eauto. - econstructor. mgen_crush. apply match_arrs_merge; mgen_crush. eauto. - apply match_empty_size_merge; mgen_crush; mgen_crush. - assert (MATCH_SIZE1': match_empty_size m ran'0 /\ match_empty_size m rab'0). - { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. } - simplify. - assert (MATCH_SIZE2': match_empty_size m ran'2 /\ match_empty_size m rab'2). - { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. - assert (MATCH_SIZE2': match_empty_size m ran'4 /\ match_empty_size m rab'4). - { eapply match_arrs_size_ram_preserved2; mgen_crush. - unfold match_empty_size, transf_module, empty_stack. - repeat destruct_match; crush. mgen_crush. } - apply match_empty_size_merge; mgen_crush; mgen_crush. - unfold disable_ram. - unfold transf_module; repeat destruct_match; crush. - apply exec_ram_resets_en in H21. unfold merge_reg_assocs in H21. - simplify. auto. auto. - - eapply translation_correct; eauto. - - do 2 econstructor. apply Smallstep.plus_one. - apply step_finish; mgen_crush. constructor; eauto. - - do 2 econstructor. apply Smallstep.plus_one. - apply step_finish; mgen_crush. econstructor; eauto. - - econstructor. econstructor. apply Smallstep.plus_one. econstructor. - replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m) by (rewrite RAM0; auto). - replace (mod_reset (transf_module m)) with (mod_reset m) by (rewrite RAM0; auto). - replace (mod_finish (transf_module m)) with (mod_finish m) by (rewrite RAM0; auto). - replace (empty_stack (transf_module m)) with (empty_stack m) by (rewrite RAM0; auto). - replace (mod_params (transf_module m)) with (mod_params m) by (rewrite RAM0; auto). - replace (mod_st (transf_module m)) with (mod_st m) by (rewrite RAM0; auto). - repeat econstructor; mgen_crush. - unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (mod_params_wf m). - pose proof (mod_ram_wf m r Heqo0). - pose proof (ram_ordering r). - simplify. - repeat rewrite find_assocmap_gso by lia. - assert ((init_regs nil (mod_params m)) ! (ram_en r) = None). - { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } - assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None). - { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } - unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto. - - econstructor. econstructor. apply Smallstep.plus_one. econstructor. - replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m). - replace (mod_reset (transf_module m)) with (mod_reset m). - replace (mod_finish (transf_module m)) with (mod_finish m). - replace (empty_stack (transf_module m)) with (empty_stack m). - replace (mod_params (transf_module m)) with (mod_params m). - replace (mod_st (transf_module m)) with (mod_st m). - all: try solve [unfold transf_module; repeat destruct_match; mgen_crush]. - repeat econstructor; mgen_crush. - unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - unfold max_reg_module. - repeat rewrite find_assocmap_gso by lia. - assert (max_reg_module m + 1 > max_list (mod_params m)). - { unfold max_reg_module. lia. } - apply max_list_correct in H0. - unfold find_assocmap, AssocMapExt.get_default. - rewrite init_regs_equal_empty. rewrite init_regs_equal_empty. auto. - eapply forall_lt_num. eassumption. unfold max_reg_module. lia. - eapply forall_lt_num. eassumption. unfold max_reg_module. lia. - - inv STACKS. destruct b1; subst. - econstructor. econstructor. apply Smallstep.plus_one. - econstructor. eauto. - clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor. - constructor. intros. - rewrite RAM0. - destruct (Pos.eq_dec r res); subst. - rewrite AssocMap.gss. - rewrite AssocMap.gss. auto. - rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. - destruct (Pos.eq_dec (mod_st m) r); subst. - rewrite AssocMap.gss. - rewrite AssocMap.gss. auto. - rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H1. auto. - auto. auto. auto. auto. - rewrite RAM0. rewrite RAM. rewrite RAM0 in DISABLE_RAM. rewrite RAM in DISABLE_RAM. - apply disable_ram_set_gso. - apply disable_ram_set_gso. auto. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (ram_ordering r0). simplify. - pose proof (mod_ram_wf m r0 H). lia. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (ram_ordering r0). simplify. - pose proof (mod_ram_wf m r0 H). lia. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (ram_ordering r0). simplify. - pose proof (mod_ram_wf m r0 H). lia. - pose proof (mod_ordering_wf m); unfold module_ordering in *. - pose proof (ram_ordering r0). simplify. - pose proof (mod_ram_wf m r0 H). lia. - - inv STACKS. destruct b1; subst. - econstructor. econstructor. apply Smallstep.plus_one. - econstructor. eauto. - clear Learn. inv H0. inv H3. inv STACKS. constructor. - constructor. intros. - unfold transf_module. repeat destruct_match; crush. - destruct (Pos.eq_dec r res); subst. - rewrite AssocMap.gss. - rewrite AssocMap.gss. auto. - rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. - destruct (Pos.eq_dec (mod_st m) r); subst. - rewrite AssocMap.gss. - rewrite AssocMap.gss. auto. - rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC. apply H. auto. - auto. auto. auto. auto. - Opaque disable_ram. - unfold transf_module in *; repeat destruct_match; crush. - apply disable_ram_set_gso. - apply disable_ram_set_gso. - auto. - simplify. unfold max_reg_module. lia. - simplify. unfold max_reg_module. lia. - simplify. unfold max_reg_module. lia. - simplify. unfold max_reg_module. lia. - Qed. + (** FIXME: Breaks because of initcall constructor of step *) + admit. + (* induction 1; destruct (mod_ram m) eqn:RAM; simplify; repeat transf_step_correct_assum; *) + (* repeat transf_step_correct_tac. *) + (* - assert (MATCH_SIZE1: match_empty_size m nasa1 /\ match_empty_size m basa1). *) + (* { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. } *) + (* simplify. *) + (* assert (MATCH_SIZE2: match_empty_size m nasa2 /\ match_empty_size m basa2). *) + (* { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. *) + (* assert (MATCH_SIZE2: match_empty_size m nasa3 /\ match_empty_size m basa3). *) + (* { eapply match_arrs_size_ram_preserved2; mgen_crush. } simplify. *) + (* assert (MATCH_ARR3: match_arrs_size nasa3 basa3) by mgen_crush. *) + (* exploit match_states_same. apply H4. eauto with mgen. *) + (* econstructor; eauto. econstructor; eauto. econstructor; eauto. econstructor; eauto. *) + (* intros. repeat inv_exists. simplify. inv H18. inv H21. *) + (* exploit match_states_same. apply H6. eauto with mgen. *) + (* econstructor; eauto. econstructor; eauto. intros. repeat inv_exists. simplify. inv H18. inv H23. *) + (* exploit exec_ram_same; eauto. eauto with mgen. *) + (* econstructor. eapply match_assocmaps_merge; eauto. eauto with mgen. *) + (* econstructor. *) + (* apply match_arrs_merge; eauto with mgen. eauto with mgen. *) + (* intros. repeat inv_exists. simplify. inv H18. inv H28. *) + (* econstructor; simplify. apply Smallstep.plus_one. econstructor. *) + (* mgen_crush. mgen_crush. mgen_crush. rewrite RAM0; eassumption. rewrite RAM0; eassumption. *) + (* rewrite RAM0. eassumption. mgen_crush. eassumption. rewrite RAM0 in H21. rewrite RAM0. *) + (* rewrite RAM. eassumption. eauto. eauto. eauto with mgen. eauto. *) + (* econstructor. mgen_crush. apply match_arrs_merge; mgen_crush. eauto. *) + (* apply match_empty_size_merge; mgen_crush; mgen_crush. *) + (* assert (MATCH_SIZE1': match_empty_size m ran'0 /\ match_empty_size m rab'0). *) + (* { eapply match_arrs_size_stmnt_preserved2; eauto. unfold match_empty_size; mgen_crush. } *) + (* simplify. *) + (* assert (MATCH_SIZE2': match_empty_size m ran'2 /\ match_empty_size m rab'2). *) + (* { eapply match_arrs_size_stmnt_preserved2; mgen_crush. } simplify. *) + (* assert (MATCH_SIZE2': match_empty_size m ran'4 /\ match_empty_size m rab'4). *) + (* { eapply match_arrs_size_ram_preserved2; mgen_crush. *) + (* unfold match_empty_size, transf_module, empty_stack. *) + (* repeat destruct_match; crush. mgen_crush. } *) + (* apply match_empty_size_merge; mgen_crush; mgen_crush. *) + (* unfold disable_ram. *) + (* unfold transf_module; repeat destruct_match; crush. *) + (* apply exec_ram_resets_en in H21. unfold merge_reg_assocs in H21. *) + (* simplify. auto. auto. *) + (* - eapply translation_correct; eauto. *) + (* - do 2 econstructor. apply Smallstep.plus_one. *) + (* apply step_finish; mgen_crush. constructor; eauto. *) + (* - do 2 econstructor. apply Smallstep.plus_one. *) + (* apply step_finish; mgen_crush. econstructor; eauto. *) + (* - econstructor. econstructor. apply Smallstep.plus_one. econstructor. *) + (* replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m) by (rewrite RAM0; auto). *) + (* replace (mod_reset (transf_module m)) with (mod_reset m) by (rewrite RAM0; auto). *) + (* replace (mod_finish (transf_module m)) with (mod_finish m) by (rewrite RAM0; auto). *) + (* replace (empty_stack (transf_module m)) with (empty_stack m) by (rewrite RAM0; auto). *) + (* replace (mod_params (transf_module m)) with (mod_params m) by (rewrite RAM0; auto). *) + (* replace (mod_st (transf_module m)) with (mod_st m) by (rewrite RAM0; auto). *) + (* repeat econstructor; mgen_crush. *) + (* unfold disable_ram. unfold transf_module; repeat destruct_match; crush. *) + (* pose proof (mod_ordering_wf m); unfold module_ordering in *. *) + (* pose proof (mod_params_wf m). *) + (* pose proof (mod_ram_wf m r Heqo0). *) + (* pose proof (ram_ordering r). *) + (* simplify. *) + (* repeat rewrite find_assocmap_gso by lia. *) + (* assert ((init_regs nil (mod_params m)) ! (ram_en r) = None). *) + (* { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } *) + (* assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None). *) + (* { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } *) + (* unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto. *) + (* - econstructor. econstructor. apply Smallstep.plus_one. econstructor. *) + (* replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m). *) + (* replace (mod_reset (transf_module m)) with (mod_reset m). *) + (* replace (mod_finish (transf_module m)) with (mod_finish m). *) + (* replace (empty_stack (transf_module m)) with (empty_stack m). *) + (* replace (mod_params (transf_module m)) with (mod_params m). *) + (* replace (mod_st (transf_module m)) with (mod_st m). *) + (* all: try solve [unfold transf_module; repeat destruct_match; mgen_crush]. *) + (* repeat econstructor; mgen_crush. *) + (* unfold disable_ram. unfold transf_module; repeat destruct_match; crush. *) + (* unfold max_reg_module. *) + (* repeat rewrite find_assocmap_gso by lia. *) + (* assert (max_reg_module m + 1 > max_list (mod_params m)). *) + (* { unfold max_reg_module. lia. } *) + (* apply max_list_correct in H0. *) + (* unfold find_assocmap, AssocMapExt.get_default. *) + (* rewrite init_regs_equal_empty. rewrite init_regs_equal_empty. auto. *) + (* eapply forall_lt_num. eassumption. unfold max_reg_module. lia. *) + (* eapply forall_lt_num. eassumption. unfold max_reg_module. lia. *) + (* - inv STACKS. destruct b1; subst. *) + (* econstructor. econstructor. apply Smallstep.plus_one. *) + (* econstructor. eauto. *) + (* clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor. *) + (* constructor. intros. *) + (* rewrite RAM0. *) + (* destruct (Pos.eq_dec r res); subst. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. auto. *) + (* rewrite AssocMap.gso; auto. *) + (* symmetry. rewrite AssocMap.gso; auto. *) + (* destruct (Pos.eq_dec (mod_st m) r); subst. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. auto. *) + (* rewrite AssocMap.gso; auto. *) + (* symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC0. apply H1. auto. *) + (* auto. auto. auto. auto. *) + (* rewrite RAM0. rewrite RAM. rewrite RAM0 in DISABLE_RAM. rewrite RAM in DISABLE_RAM. *) + (* apply disable_ram_set_gso. *) + (* apply disable_ram_set_gso. auto. *) + (* pose proof (mod_ordering_wf m); unfold module_ordering in *. *) + (* pose proof (ram_ordering r0). simplify. *) + (* pose proof (mod_ram_wf m r0 H). lia. *) + (* pose proof (mod_ordering_wf m); unfold module_ordering in *. *) + (* pose proof (ram_ordering r0). simplify. *) + (* pose proof (mod_ram_wf m r0 H). lia. *) + (* pose proof (mod_ordering_wf m); unfold module_ordering in *. *) + (* pose proof (ram_ordering r0). simplify. *) + (* pose proof (mod_ram_wf m r0 H). lia. *) + (* pose proof (mod_ordering_wf m); unfold module_ordering in *. *) + (* pose proof (ram_ordering r0). simplify. *) + (* pose proof (mod_ram_wf m r0 H). lia. *) + (* - inv STACKS. destruct b1; subst. *) + (* econstructor. econstructor. apply Smallstep.plus_one. *) + (* econstructor. eauto. *) + (* clear Learn. inv H0. inv H3. inv STACKS. constructor. *) + (* constructor. intros. *) + (* unfold transf_module. repeat destruct_match; crush. *) + (* destruct (Pos.eq_dec r res); subst. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. auto. *) + (* rewrite AssocMap.gso; auto. *) + (* symmetry. rewrite AssocMap.gso; auto. *) + (* destruct (Pos.eq_dec (mod_st m) r); subst. *) + (* rewrite AssocMap.gss. *) + (* rewrite AssocMap.gss. auto. *) + (* rewrite AssocMap.gso; auto. *) + (* symmetry. rewrite AssocMap.gso; auto. inv MATCH_ASSOC. apply H. auto. *) + (* auto. auto. auto. auto. *) + (* Opaque disable_ram. *) + (* unfold transf_module in *; repeat destruct_match; crush. *) + (* apply disable_ram_set_gso. *) + (* apply disable_ram_set_gso. *) + (* auto. *) + (* simplify. unfold max_reg_module. lia. *) + (* simplify. unfold max_reg_module. lia. *) + (* simplify. unfold max_reg_module. lia. *) + (* simplify. unfold max_reg_module. lia. *) + Admitted. Hint Resolve transf_step_correct : mgen. Lemma transf_initial_states : @@ -3172,12 +3178,15 @@ Section CORRECTNESS. simplify. inv H. exploit function_ptr_translated. eauto. intros. inv H. inv H3. - econstructor. econstructor. econstructor. - eapply (Genv.init_mem_match TRANSL); eauto. - setoid_rewrite (Linking.match_program_main TRANSL). - rewrite symbols_preserved. eauto. - eauto. - econstructor. + eexists. split. + - econstructor. + + eapply (Genv.init_mem_match TRANSL); eauto. + + setoid_rewrite (Linking.match_program_main TRANSL). + rewrite symbols_preserved. + eauto. + + eauto. + - replace (prog_main prog) with (prog_main tprog) by (eapply Linking.match_program_main; eauto). + econstructor. Qed. Hint Resolve transf_initial_states : mgen. -- cgit