From 6222d882c90e7d419236344ba91ad1a90b2c44ff Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 28 Mar 2021 12:55:09 +0100 Subject: Finish main match proof in store --- src/hls/Memorygen.v | 605 +++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 555 insertions(+), 50 deletions(-) diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 9c2bfff..50986a7 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -331,6 +331,7 @@ Inductive match_stackframes : stackframe -> stackframe -> Prop := match_assocmaps (max_reg_module m + 1) asr asr' -> match_arrs asa asa' -> match_empty_size m asa -> + match_empty_size m asa' -> match_stackframes (Stackframe r m pc asr asa) (Stackframe r (transf_module m) pc asr' asa'). @@ -340,7 +341,8 @@ Inductive match_states : state -> state -> Prop := (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_SIZE: match_empty_size m asa) + (ARRS_SIZE2: match_empty_size m asa'), match_states (State res m st asr asa) (State res' (transf_module m) st asr' asa') | match_returnstate : @@ -359,6 +361,10 @@ Definition empty_stack_ram r := Definition empty_stack' len st := AssocMap.set st (Array.arr_repeat None len) (AssocMap.empty arr). +Definition match_empty_size' l s (ar : assocmap_arr) : Prop := + match_arrs_size (empty_stack' l s) ar. +Hint Unfold match_empty_size : mgen. + Definition merge_reg_assocs r := Verilog.mkassociations (Verilog.merge_regs (assoc_nonblocking r) (assoc_blocking r)) empty_assocmap. @@ -401,6 +407,14 @@ Lemma match_arrs_size_equiv : forall a, match_arrs_size a a. Proof. intros; repeat econstructor; eauto. Qed. Hint Resolve match_arrs_size_equiv : mgen. +Lemma match_stacks_equiv : + forall m s l, + mod_stk m = s -> + mod_stk_len m = l -> + empty_stack' l s = empty_stack m. +Proof. unfold empty_stack', empty_stack; mgen_crush. Qed. +Hint Rewrite match_stacks_equiv : mgen. + Lemma match_assocmaps_max1 : forall p p' a b, match_assocmaps (Pos.max p' p) a b -> @@ -726,6 +740,17 @@ Proof. Qed. Hint Resolve match_assocmaps_gss : mgen. +Lemma match_assocmaps_gt : + forall p s ra ra' v, + p <= s -> + match_assocmaps p ra ra' -> + match_assocmaps p ra (ra' # s <- v). +Proof. + intros. inv H0. constructor. + intros. rewrite AssocMap.gso; try lia. apply H1; auto. +Qed. +Hint Resolve match_assocmaps_gt : mgen. + Lemma match_reg_assocs_block : forall p rab rab' r rhsval, match_reg_assocs p rab rab' -> @@ -1136,7 +1161,9 @@ Lemma max_index : forall A d i d_s, d ! i = Some d_s -> @max_pc A d + 1 > i. Proof. - unfold max_pc; eauto using max_index_list, PTree.elements_correct, PTree.elements_keys_norepet. + unfold max_pc; + eauto using max_index_list, + PTree.elements_correct, PTree.elements_keys_norepet. Qed. Lemma transf_code_not_changed : @@ -1154,45 +1181,6 @@ Proof. eauto using forall_gt, PTree.elements_keys_norepet, max_index. Qed. -Lemma transf_code_store : - forall state ram d c d' c' i d_s c_s rs1 ar1 rs2 ar2 p trs1 tar1, - transf_code state ram d c = (d', c') -> - (forall r e1 e2, - (forall e2 r, e1 <> Vvari r e2) -> - d_s = Vnonblock (Vvari r e1) e2) -> - d!i = Some d_s -> - c!i = Some c_s -> - exec_all d_s c_s rs1 ar1 rs2 ar2 -> - match_reg_assocs p rs1 trs1 -> - match_arr_assocs ar1 tar1 -> - Pos.max (max_stmnt_tree c) (max_stmnt_tree d) < p -> - exists d_s' c_s' trs2 tar2, - d'!i = Some d_s' /\ c'!i = Some c_s' - /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 - /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) - /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) - (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2). -Proof. - Admitted. - -Lemma transf_code_all : - forall state ram d c d' c' i d_s c_s rs1 ar1 rs2 ar2 tar1 trs1 p, - transf_code state ram d c = (d', c') -> - d!i = Some d_s -> - c!i = Some c_s -> - exec_all d_s c_s rs1 ar1 rs2 ar2 -> - match_reg_assocs p rs1 trs1 -> - match_arr_assocs ar1 tar1 -> - Pos.max (max_stmnt_tree c) (max_stmnt_tree d) < p -> - exists d_s' c_s' trs2 tar2, - d'!i = Some d_s' /\ c'!i = Some c_s' - /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 - /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) - /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) - (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2). -Proof. - Admitted. - (*Lemma transf_all : forall state d c d' c' ram, transf_code state ram d c = (d', c') -> @@ -1832,6 +1820,511 @@ Proof. Qed. Hint Resolve match_arrs_size_ram_preserved2 : mgen. +(*Lemma match_arrs_merge_set' : + forall s i v l m ran ran' rab', + match_empty_size' l m rab -> + match_empty_size' l m ran -> + match_arrs ran (merge_arrs (arr_assocmap_set s i v (empty_stack' l m)) (merge_arrs ran' rab')) -> +. +Proof. + inversion 1; inversion 1; unfold merge_arrs, arr_assocmap_set; subst; simplify. + destruct (empty_stack' l m) ! s eqn:?. do 5 masrp_tac. + Admitted. + +Lemma set_merge_assoc : + forall s i v ran rab, + arr_assocmap_set s i v (merge_arrs ran rab) = merge_arrs (arr_assocmap_set s i v ran) rab. +Admitted. + +Lemma merge_arrs_idem : + forall l m s i v ran rab, + merge_arrs (empty_stack' l m) (merge_arrs (arr_assocmap_set s i v ran) rab) + = merge_arrs (arr_assocmap_set s i v ran) rab. +Admitted.*) + +Lemma empty_stack_m : + forall m, empty_stack m = empty_stack' (mod_stk_len m) (mod_stk m). +Proof. unfold empty_stack, empty_stack'; mgen_crush. Qed. +Hint Rewrite empty_stack_m : mgen. + +Ltac clear_forall := + repeat match goal with + | H: context[forall _, _] |- _ => clear H + end. + +Lemma list_combine_none : + forall n l, + length l = n -> + list_combine Verilog.merge_cell (list_repeat None n) l = l. +Proof. + induction n; intros; crush. + - symmetry. apply length_zero_iff_nil. auto. + - destruct l; crush. + rewrite list_repeat_cons. + crush. f_equal. + eauto. +Qed. + +Lemma combine_none : + forall n a, + a.(arr_length) = n -> + arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. +Proof. + intros. + unfold combine. + crush. + + rewrite <- (arr_wf a) in H. + apply list_combine_none. + assumption. +Qed. + +Lemma combine_none2 : + forall n a addr, + arr_length a = n -> + array_get_error addr (combine Verilog.merge_cell (arr_repeat None n) a) + = array_get_error addr a. +Proof. intros; auto using array_get_error_equal, combine_none. Qed. + +Lemma list_combine_lookup_first : + forall l1 l2 n, + length l1 = length l2 -> + nth_error l1 n = Some None -> + nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. +Proof. + induction l1; intros; crush. + + rewrite nth_error_nil in H0. + discriminate. + + destruct l2 eqn:EQl2. crush. + simpl in H. invert H. + destruct n; simpl in *. + invert H0. simpl. reflexivity. + eauto. +Qed. + +Lemma combine_lookup_first : + forall a1 a2 n, + a1.(arr_length) = a2.(arr_length) -> + array_get_error n a1 = Some None -> + array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. +Proof. + intros. + + unfold array_get_error in *. + apply list_combine_lookup_first; eauto. + rewrite a1.(arr_wf). rewrite a2.(arr_wf). + assumption. +Qed. + +Lemma list_combine_lookup_second : + forall l1 l2 n x, + length l1 = length l2 -> + nth_error l1 n = Some (Some x) -> + nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). +Proof. + induction l1; intros; crush; auto. + + destruct l2 eqn:EQl2. crush. + simpl in H. invert H. + destruct n; simpl in *. + invert H0. simpl. reflexivity. + eauto. +Qed. + +Lemma combine_lookup_second : + forall a1 a2 n x, + a1.(arr_length) = a2.(arr_length) -> + array_get_error n a1 = Some (Some x) -> + array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). +Proof. + intros. + + unfold array_get_error in *. + apply list_combine_lookup_second; eauto. + rewrite a1.(arr_wf). rewrite a2.(arr_wf). + assumption. +Qed. + +Lemma match_get_arrs2 : + forall a i v l, + length a = l -> + list_combine merge_cell (list_set i (Some v) (list_repeat None l)) a = + list_combine merge_cell (list_repeat None l) (list_set i (Some v) a). +Proof. + induction a; crush; subst. + - destruct i. unfold list_repeat. unfold list_repeat'. auto. + unfold list_repeat. unfold list_repeat'. auto. + - destruct i. + rewrite list_repeat_cons. simplify. auto. + rewrite list_repeat_cons. simplify. f_equal. apply IHa. auto. +Qed. + +Lemma match_get_arrs : + forall addr i v x4 x x3, + x4 = arr_length x -> + x4 = arr_length x3 -> + array_get_error addr (combine merge_cell (array_set i (Some v) (arr_repeat None x4)) + (combine merge_cell x x3)) + = array_get_error addr (combine merge_cell (arr_repeat None x4) + (array_set i (Some v) (combine merge_cell x x3))). +Proof. + intros. apply array_get_error_equal. unfold combine. simplify. + destruct x; destruct x3; simplify. + apply match_get_arrs2. rewrite list_combine_length. subst. + rewrite H0. lia. +Qed. + +Lemma combine_array_set' : + forall a b i v, + length a = length b -> + list_combine merge_cell (list_set i (Some v) a) b = + list_set i (Some v) (list_combine merge_cell a b). +Proof. + induction a; simplify; crush. + - destruct i; crush. + - destruct i; destruct b; crush. + f_equal. apply IHa. auto. +Qed. + +Lemma combine_array_set : + forall a b i v addr, + arr_length a = arr_length b -> + array_get_error addr (combine merge_cell (array_set i (Some v) a) b) + = array_get_error addr (array_set i (Some v) (combine merge_cell a b)). +Proof. + intros. destruct a; destruct b. unfold array_set. simplify. + unfold array_get_error. simplify. f_equal. + apply combine_array_set'. crush. +Qed. + +Lemma array_get_combine' : + forall a b a' b' addr, + length a = length b -> + length a = length b' -> + length a = length a' -> + nth_error a addr = nth_error a' addr -> + nth_error b addr = nth_error b' addr -> + nth_error (list_combine merge_cell a b) addr = + nth_error (list_combine merge_cell a' b') addr. +Proof. + induction a; crush. + - destruct b; crush; destruct b'; crush; destruct a'; crush. + - destruct b; crush; destruct b'; crush; destruct a'; crush; + destruct addr; crush; apply IHa. +Qed. + +Lemma array_get_combine : + forall a b a' b' addr, + arr_length a = arr_length b -> + arr_length a = arr_length b' -> + arr_length a = arr_length a' -> + array_get_error addr a = array_get_error addr a' -> + array_get_error addr b = array_get_error addr b' -> + array_get_error addr (combine merge_cell a b) + = array_get_error addr (combine merge_cell a' b'). +Proof. + intros; unfold array_get_error, combine in *; destruct a; destruct b; + destruct a'; destruct b'; simplify; apply array_get_combine'; crush. +Qed. + +Lemma match_empty_size_exists_Some : + forall m rab s v, + match_empty_size m rab -> + rab ! s = Some v -> + exists v', (empty_stack m) ! s = Some v' /\ arr_length v = arr_length v'. +Proof. inversion 1; intros; repeat masrp_tac. Qed. + +Lemma match_empty_size_exists_None : + forall m rab s, + match_empty_size m rab -> + rab ! s = None -> + (empty_stack m) ! s = None. +Proof. inversion 1; intros; repeat masrp_tac. Qed. + +Lemma match_empty_size_exists_None' : + forall m rab s, + match_empty_size m rab -> + (empty_stack m) ! s = None -> + rab ! s = None. +Proof. inversion 1; intros; repeat masrp_tac. Qed. + +Lemma match_empty_size_exists_Some' : + forall m rab s v, + match_empty_size m rab -> + (empty_stack m) ! s = Some v -> + exists v', rab ! s = Some v' /\ arr_length v = arr_length v'. +Proof. inversion 1; intros; repeat masrp_tac. Qed. + +Lemma match_arrs_Some : + forall ra ra' s v, + match_arrs ra ra' -> + ra ! s = Some v -> + exists v', ra' ! s = Some v' + /\ (forall addr, array_get_error addr v = array_get_error addr v') + /\ arr_length v = arr_length v'. +Proof. inversion 1; intros; repeat masrp_tac. intros. rewrite H5. auto. Qed. + +Lemma match_arrs_None : + forall ra ra' s, + match_arrs ra ra' -> + ra ! s = None -> + ra' ! s = None. +Proof. inversion 1; intros; repeat masrp_tac. Qed. + +Ltac learn_next := + match goal with + | H: match_empty_size _ ?rab, H2: ?rab ! _ = Some _ |- _ => + let H3 := fresh "H" in + learn H2 as H3; eapply match_empty_size_exists_Some in H3; + eauto; inv_exists; simplify + | H: match_empty_size _ ?rab, H2: ?rab ! _ = None |- _ => + let H3 := fresh "H" in + learn H2 as H3; eapply match_empty_size_exists_None in H3; eauto + end. + +Ltac learn_empty := + match goal with + | H: match_empty_size _ _, H2: (empty_stack _) ! _ = Some _ |- _ => + let H3 := fresh "H" in + learn H as H3; eapply match_empty_size_exists_Some' in H3; + [| eassumption]; inv_exists; simplify + | H: match_arrs ?ar _, H2: ?ar ! _ = Some _ |- _ => + let H3 := fresh "H" in + learn H as H3; eapply match_arrs_Some in H3; + [| eassumption]; inv_exists; simplify + | H: match_empty_size _ _, H2: (empty_stack _) ! _ = None |- _ => + let H3 := fresh "H" in + learn H as H3; eapply match_empty_size_exists_None' in H3; + [| eassumption]; simplify + end. + +Lemma empty_set_none : + forall m ran rab s i v s0, + match_empty_size m ran -> + match_empty_size m rab -> + (arr_assocmap_set s i v ran) ! s0 = None -> + (arr_assocmap_set s i v rab) ! s0 = None. +Proof. + unfold arr_assocmap_set; inversion 1; subst; simplify. + destruct (Pos.eq_dec s s0); subst. + destruct ran ! s0 eqn:?. + rewrite AssocMap.gss in H4. inv H4. + learn_next. learn_empty. rewrite H6; auto. + destruct ran ! s eqn:?. rewrite AssocMap.gso in H4. + learn_next. learn_empty. rewrite H6. rewrite AssocMap.gso. + repeat match goal with + | H: Learnt _ |- _ => clear H + end. clear Heqo. clear H5. clear H6. + learn_next. repeat learn_empty. auto. auto. auto. + pose proof Heqo. learn_next; repeat learn_empty. + repeat match goal with + | H: Learnt _ |- _ => clear H + end. + pose proof H4. learn_next; repeat learn_empty. + rewrite H7. auto. +Qed. + +Lemma match_arrs_size_assoc : + forall a b, + match_arrs_size a b -> + match_arrs_size b a. +Proof. inversion 1; constructor; crush; split; apply H2. Qed. +Hint Resolve match_arrs_size_assoc : mgen. + +Lemma match_arrs_merge_set2 : + forall rab rab' ran ran' s m i v, + match_empty_size m rab -> + match_empty_size m ran -> + match_empty_size m rab' -> + match_empty_size m ran' -> + match_arrs rab rab' -> + match_arrs ran ran' -> + match_arrs (merge_arrs (arr_assocmap_set s i v ran) rab) + (merge_arrs (arr_assocmap_set s i v (empty_stack m)) + (merge_arrs ran' rab')). +Proof. + simplify. + constructor; intros. + unfold arr_assocmap_set in *. destruct (Pos.eq_dec s s0); subst. + destruct ran ! s0 eqn:?. unfold merge_arrs in *. rewrite AssocMap.gcombine in *; auto. + learn_next. repeat learn_empty. + econstructor. simplify. rewrite H6. rewrite AssocMap.gcombine by auto. + rewrite AssocMap.gss. simplify. setoid_rewrite H9. setoid_rewrite H7. simplify. + intros. rewrite AssocMap.gss in H5. setoid_rewrite H13 in H5. + simplify. pose proof (empty_arr m s0). inv H5. inv_exists. setoid_rewrite H5 in H6. inv H6. + unfold arr_repeat in H8. simplify. rewrite list_repeat_len in H8. rewrite list_repeat_len in H10. + rewrite match_get_arrs. crush. rewrite combine_none2. rewrite combine_array_set; try congruence. + apply array_get_error_each. rewrite combine_length; try congruence. + rewrite combine_length; try congruence. + apply array_get_combine; crush. + rewrite <- array_set_len. rewrite combine_length; crush. crush. crush. + setoid_rewrite H21 in H6; discriminate. rewrite combine_length. + rewrite <- array_set_len; crush. + unfold merge_arr in *. rewrite AssocMap.gss in H5. setoid_rewrite H13 in H5. + inv H5. rewrite combine_length. rewrite <- array_set_len; crush. + rewrite <- array_set_len; crush. + rewrite combine_length; crush. + destruct rab ! s0 eqn:?. learn_next. repeat learn_empty. + rewrite H11 in Heqo. discriminate. + unfold merge_arrs in H5. rewrite AssocMap.gcombine in H5; auto. rewrite Heqo in H5. + rewrite Heqo0 in H5. crush. + + destruct ran ! s eqn:?. + learn_next. repeat learn_empty. rewrite H6. + unfold merge_arrs in *. rewrite AssocMap.gcombine in H5; auto. + rewrite AssocMap.gcombine; auto. rewrite AssocMap.gso in H5; auto. + rewrite AssocMap.gso; auto. + destruct ran ! s0 eqn:?. + learn_next. + repeat match goal with + | H: Learnt _ |- _ => clear H + end. + repeat learn_empty. + repeat match goal with + | H: Learnt _ |- _ => clear H + end. + rewrite AssocMap.gcombine; auto. setoid_rewrite Heqo0 in H5. setoid_rewrite H29 in H5. + simplify. + pose proof (empty_arr m s0). inv H5. inv_exists. rewrite H5 in H21. inv H21. + econstructor. simplify. setoid_rewrite H23. rewrite H25. setoid_rewrite H5. + simplify. intros. rewrite combine_none2. apply array_get_combine; solve [crush]. + crush. rewrite list_combine_length. rewrite (arr_wf x5). rewrite (arr_wf x6). + rewrite <- H26. rewrite <- H28. rewrite list_repeat_len. lia. rewrite list_combine_length. + rewrite (arr_wf a). rewrite (arr_wf x7). rewrite combine_length. rewrite arr_repeat_length. + rewrite H24. rewrite <- H32. rewrite list_repeat_len. lia. + rewrite arr_repeat_length. rewrite combine_length. rewrite <- H26. symmetry. apply list_repeat_len. + congruence. + rewrite H37 in H21; discriminate. + repeat match goal with + | H: Learnt _ |- _ => clear H + end. eapply match_empty_size_exists_None in H0; eauto. + clear H6. repeat learn_empty. setoid_rewrite Heqo0 in H5. + setoid_rewrite H29 in H5. discriminate. + pose proof (match_arrs_merge ran ran' rab rab'). + eapply match_empty_size_match in H; [|apply H0]. + apply H6 in H; auto. inv H. apply H7 in H5. inv_exists. simplify. + learn_next. rewrite H9. econstructor. simplify. + apply merge_arr_empty''; mgen_crush. apply match_empty_size_merge; auto. + auto. auto. + unfold merge_arrs in *. rewrite AssocMap.gcombine in H5; auto. rewrite AssocMap.gcombine; auto. + destruct (arr_assocmap_set s i v ran) ! s0 eqn:?; destruct rab ! s0 eqn:?; crush. + learn_next. repeat learn_empty. + repeat match goal with + | H: Learnt _ |- _ => clear H + end. + erewrite empty_set_none. rewrite AssocMap.gcombine; auto. + simplify. rewrite H7. rewrite H8. auto. apply H0. mgen_crush. auto. +Qed. + +Lemma transf_not_store' : + forall state ram n d c i c_s d' c' n' tar1 trs1 p ar1 ar2 rs1 rs2 r e1 e2, + d!i = Some (Vnonblock (Vvari r e1) e2) -> + c!i = Some c_s -> + transf_maps state ram i (n, d, c) = (n', d', c') -> + exec_all (Vnonblock (Vvari (ram_mem ram) e1) e2) c_s rs1 ar1 rs2 ar2 -> + match_reg_assocs p rs1 trs1 -> + match_arr_assocs ar1 tar1 -> + Pos.max (max_stmnt_tree c) (max_stmnt_tree d) < p -> + exists d_s' c_s' trs2 tar2, + d'!i = Some d_s' /\ c'!i = Some c_s' + /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 + /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) + /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) + (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2). +Proof. + intros; unfold transf_maps; simplify; repeat destruct_match; mgen_crush. + inv H1. unfold exec_all in *. repeat inv_exists. simplify. + exploit match_states_same. apply H0. instantiate (1 := p). + admit. eassumption. eassumption. intros. + repeat inv_exists. simplify. + inv H1. inv H12. inv H12. + inv H. inv H7. simplify. + do 4 econstructor. + simplify. rewrite AssocMap.gss. auto. eauto. + unfold exec_all_ram. + do 5 econstructor. simplify. eassumption. + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. econstructor. + econstructor. econstructor. econstructor. eapply expr_runp_matches2. + eassumption. assert (max_reg_expr e2 < p) by admit. eauto. + unfold nonblock_reg. simplify. auto. auto. + econstructor. econstructor. unfold nonblock_reg. simplify. + eapply expr_runp_matches2. eassumption. assert (max_reg_expr e1 < p) by admit. eauto. + auto. auto. + eapply exec_ram_Some_write. + 3: { + unfold nonblock_reg. simplify. unfold merge_regs. + apply AssocMapExt.merge_correct_1. rewrite AssocMap.gso by admit. + rewrite AssocMap.gso by admit. rewrite AssocMap.gso by admit. + rewrite AssocMap.gss. auto. + } + crush. + 2: { + unfold nonblock_reg; simplify. apply AssocMapExt.merge_correct_1. + rewrite AssocMap.gso by admit. rewrite AssocMap.gso by admit. + rewrite AssocMap.gss. auto. + } + crush. + unfold nonblock_reg; simplify. + apply AssocMapExt.merge_correct_1. + rewrite AssocMap.gso by admit. rewrite AssocMap.gss. auto. + unfold nonblock_reg; simplify. + apply AssocMapExt.merge_correct_1. + rewrite AssocMap.gss. auto. + unfold nonblock_reg; simplify. + unfold merge_reg_assocs. simplify. econstructor. + unfold merge_regs. mgen_crush. apply match_assocmaps_merge. + apply match_assocmaps_gt. admit. + apply match_assocmaps_gt. admit. + apply match_assocmaps_gt. admit. + apply match_assocmaps_gt. admit. auto. auto. auto with mgen. + constructor. unfold nonblock_arr. simplify. + assert (exists m, ram_size ram = mod_stk_len m + /\ ram_mem ram = mod_stk m) by admit. + inv H7. inv H9. rewrite H7. rewrite H11. + rewrite <- empty_stack_m. + apply match_arrs_merge_set2. admit. admit. admit. admit. auto. auto. + auto with mgen. +Admitted. + +Lemma transf_code_store : + forall state ram d c d' c' i d_s c_s rs1 ar1 rs2 ar2 p trs1 tar1 r e1 e2, + transf_code state ram d c = (d', c') -> + d!i = Some (Vnonblock (Vvari r e1) e2) -> + c!i = Some c_s -> + exec_all d_s c_s rs1 ar1 rs2 ar2 -> + match_reg_assocs p rs1 trs1 -> + match_arr_assocs ar1 tar1 -> + Pos.max (max_stmnt_tree c) (max_stmnt_tree d) < p -> + exists d_s' c_s' trs2 tar2, + d'!i = Some d_s' /\ c'!i = Some c_s' + /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 + /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) + /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) + (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2). +Proof. + Admitted. + +Lemma transf_code_all : + forall state ram d c d' c' i d_s c_s rs1 ar1 rs2 ar2 tar1 trs1 p, + transf_code state ram d c = (d', c') -> + d!i = Some d_s -> + c!i = Some c_s -> + exec_all d_s c_s rs1 ar1 rs2 ar2 -> + match_reg_assocs p rs1 trs1 -> + match_arr_assocs ar1 tar1 -> + Pos.max (max_stmnt_tree c) (max_stmnt_tree d) < p -> + exists d_s' c_s' trs2 tar2, + d'!i = Some d_s' /\ c'!i = Some c_s' + /\ exec_all_ram ram d_s' c_s' trs1 tar1 trs2 tar2 + /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) + /\ match_arr_assocs (merge_arr_assocs (ram_mem ram) (ram_size ram) ar2) + (merge_arr_assocs (ram_mem ram) (ram_size ram) tar2). +Proof. + Admitted. + Section CORRECTNESS. Context (prog tprog: program). @@ -1917,9 +2410,20 @@ Section CORRECTNESS. 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. eauto. - econstructor. mgen_crush. apply match_arrs_merge; mgen_crush. eauto. eauto. - apply match_empty_size_merge; mgen_crush. + 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. unfold match_empty_size. mgen_crush. + unfold match_empty_size. mgen_crush. apply match_empty_size_merge; mgen_crush. } + apply match_empty_size_merge; mgen_crush; mgen_crush. - exploit transf_code_all; eauto. unfold exec_all. do 3 eexists. simplify. apply H4. apply H6. econstructor. apply ASSOC. eauto with mgen. econstructor. apply ARRS. @@ -1939,6 +2443,7 @@ Section CORRECTNESS. eauto with mgen. auto. assert (match_empty_size m (merge_arrs nasa2 basa2)) by admit. eauto with mgen. + admit. - do 2 econstructor. apply Smallstep.plus_one. apply step_finish; mgen_crush. constructor; eauto. - do 2 econstructor. apply Smallstep.plus_one. @@ -1963,7 +2468,7 @@ Section CORRECTNESS. - inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. - clear Learn. inv H0. inv H3. inv STACKS. inv H4. constructor. + clear Learn. inv H0. inv H3. inv STACKS. inv H3. constructor. constructor. intros. rewrite RAM0. destruct (Pos.eq_dec r res); subst. @@ -1975,12 +2480,12 @@ Section CORRECTNESS. rewrite AssocMap.gss. rewrite AssocMap.gss. auto. rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. eauto. - eauto. eauto. + symmetry. rewrite AssocMap.gso; auto. inv H8. apply H1. auto. + auto. auto. auto. auto. - inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. - clear Learn. inv H0. inv H3. inv STACKS. inv H4. constructor. + 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. @@ -1992,8 +2497,8 @@ Section CORRECTNESS. rewrite AssocMap.gss. rewrite AssocMap.gss. auto. rewrite AssocMap.gso; auto. - symmetry. rewrite AssocMap.gso; auto. eauto. - eauto. eauto. + symmetry. rewrite AssocMap.gso; auto. inv H6. apply H. auto. + auto. auto. auto. auto. Admitted. Hint Resolve transf_step_correct : mgen. -- cgit