From 3c4b9a3b7f4d4e99ab77b9cf126bf1739bc5c17a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 25 Mar 2021 13:38:40 +0000 Subject: Work more on size-preserving lemmas --- src/hls/Memorygen.v | 233 +++++++++++++++++++++++++++++----------------------- 1 file changed, 129 insertions(+), 104 deletions(-) diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 47c38ff..81a980f 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -258,7 +258,7 @@ Definition transf_module (m: module): module := let d_in := max_reg+3 in let d_out := max_reg+4 in let wr_en := max_reg+5 in - let new_size := (2 ^ Nat.log2_up m.(mod_stk_len))%nat in + let new_size := (mod_stk_len m) in let ram := mk_ram new_size (mod_stk m) en addr d_in d_out wr_en in match transf_code (mod_st m) ram (mod_datapath m) (mod_controllogic m), (mod_ram m) with | (nd, nc), None => @@ -907,7 +907,7 @@ Proof. repeat match_states_same_tac. eauto. mgen_crush. Qed. -Definition behaviour_correct d c d' c' r := +(*Definition behaviour_correct d c d' c' r := forall p rs1 ar1 rs2 ar2 trs1 tar1 d_s c_s i v v', PTree.get i d = Some d_s -> PTree.get i c = Some c_s -> @@ -924,6 +924,7 @@ Definition behaviour_correct d c d' c' r := /\ match_reg_assocs p (merge_reg_assocs rs2) (merge_reg_assocs trs2) /\ match_arr_assocs (merge_arr_assocs (ram_mem r) (ram_size r) ar2) (merge_arr_assocs (ram_mem r) (ram_size r) tar2). +*) Lemma match_reg_assocs_merge : forall p rs rs', @@ -952,7 +953,7 @@ Proof. Qed. Hint Resolve match_reg_assocs_merge : mgen. -Lemma behaviour_correct_equiv : +(*Lemma behaviour_correct_equiv : forall d c r, forall_ram (fun x => max_stmnt_tree d < x /\ max_stmnt_tree c < x) r -> behaviour_correct d c d c r. @@ -995,6 +996,7 @@ Proof. } inv H11; auto.*) Admitted. +*) Lemma stmnt_runp_gtassoc : forall st rs1 ar1 rs2 ar2 f, @@ -1191,11 +1193,11 @@ Lemma transf_code_all : Proof. Admitted. -Lemma transf_all : +(*Lemma transf_all : forall state d c d' c' ram, transf_code state ram d c = (d', c') -> behaviour_correct d c d' c' ram. -Proof. Abort. +Proof. Abort.*) Definition match_prog (p: program) (tp: program) := Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp. @@ -1254,13 +1256,13 @@ Proof. econstructor; eapply match_assocmaps_trans; eauto. Qed. -Lemma transf_maps_correct: +(*Lemma transf_maps_correct: forall state ram n d c n' d' c' i, transf_maps state ram i (n, d, c) = (n', d', c') -> behaviour_correct d c d' c' ram. -Proof. Abort. +Proof. Abort.*) -Lemma transf_maps_correct2: +(*Lemma transf_maps_correct2: forall state l ram n d c n' d' c', fold_right (transf_maps state ram) (n, d, c) l = (n', d', c') -> behaviour_correct d c d' c' ram. @@ -1273,7 +1275,7 @@ Proof. Abort. eapply behaviour_correct_trans. eapply transf_maps_correct. apply H. eapply IHl. apply Heqp. -Qed.*) +Qed.*)*) Lemma empty_arrs_match : forall m, @@ -1297,7 +1299,7 @@ Lemma transf_module_code : forall m, mod_ram m = None -> transf_code (mod_st m) - {| ram_size := 2 ^ Nat.log2_up (mod_stk_len m); + {| ram_size := mod_stk_len m; ram_mem := mod_stk m; ram_en := max_reg_module m + 2; ram_addr := max_reg_module m + 1; @@ -1619,90 +1621,6 @@ Proof. rewrite Heqo. rewrite Heqo0. auto. Qed. -Definition match_arr_assocs_size ar := - match_arrs_size (assoc_nonblocking ar) (assoc_blocking ar). - -Lemma match_arrs_size_stmnt_preserved : - forall f rs1 ar1 c rs2 ar2, - stmnt_runp f rs1 ar1 c rs2 ar2 -> - match_arr_assocs_size ar1 -> - match_arr_assocs_size ar2. -Proof. - induction 1; inversion 1; eauto. - - unfold Verilog.arr in *. constructor. - intros. unfold block_arr in *. simplify. destruct (Pos.eq_dec r s); subst. - simplify. unfold arr_assocmap_set. apply H2 in H7. inv_exists. - simplify. unfold Verilog.arr in *. - rewrite H6. - eexists. rewrite AssocMap.gss. split. auto. rewrite <- array_set_len; auto. - unfold arr_assocmap_set. destruct (assoc_blocking asa) ! r eqn:?. - unfold Verilog.arr in *. rewrite Heqo. apply H2 in H7. inv_exists. simplify. - eexists. simplify. rewrite AssocMap.gso; auto. eauto. auto. - unfold Verilog.arr in *. rewrite Heqo. apply H2 in H7. inv_exists; simplify. - eexists; split; eauto. - - intros. unfold block_arr in *. simplify. destruct (Pos.eq_dec r s); subst. - Admitted. - -Lemma match_arrs_size_stmnt_preserved2 : - forall f rs1 bar nar bar' nar' c rs2, - stmnt_runp f rs1 {| assoc_nonblocking := nar; assoc_blocking := bar |} - c rs2 {| assoc_nonblocking := nar'; assoc_blocking := bar' |} -> - match_arrs_size nar bar -> - match_arrs_size nar' bar'. -Proof. - intros. remember {| assoc_blocking := bar; assoc_nonblocking := nar |} as ar1. - remember {| assoc_blocking := bar'; assoc_nonblocking := nar' |} as ar2. - assert (H1: nar' = assoc_nonblocking ar2). rewrite Heqar2. auto. - assert (H2: bar' = assoc_blocking ar2). rewrite Heqar2. auto. - rewrite H1. rewrite H2. eapply match_arrs_size_stmnt_preserved; eauto. - unfold match_arr_assocs_size. rewrite Heqar1. auto. -Qed. - -Lemma match_arrs_size_stmnt_preserved3 : - forall m f rs1 bar nar bar' nar' c rs2, - stmnt_runp f rs1 {| assoc_nonblocking := nar; assoc_blocking := bar |} - c rs2 {| assoc_nonblocking := nar'; assoc_blocking := bar' |} -> - match_empty_size m nar -> - match_empty_size m bar -> - match_empty_size m nar' /\ match_empty_size m bar'. -Proof. - induction 1; inversion 1; inversion 1; eauto. - Admitted. - -Lemma match_arrs_size_ram_preserved : - forall rs1 ar1 ram rs2 ar2, - exec_ram rs1 ar1 ram rs2 ar2 -> - match_arr_assocs_size ar1 -> - match_arr_assocs_size ar2. -Proof. Admitted. - -Lemma match_arrs_size_ram_preserved2 : - forall rs1 nar bar ram rs2 nar' bar', - exec_ram rs1 {| assoc_nonblocking := nar; assoc_blocking := bar |} ram - rs2 {| assoc_nonblocking := nar'; assoc_blocking := bar' |} -> - match_arrs_size nar bar -> - match_arrs_size nar' bar'. -Proof. - intros. remember {| assoc_blocking := bar; assoc_nonblocking := nar |} as ar1. - remember {| assoc_blocking := bar'; assoc_nonblocking := nar' |} as ar2. - assert (H1: nar' = assoc_nonblocking ar2). rewrite Heqar2. auto. - assert (H2: bar' = assoc_blocking ar2). rewrite Heqar2. auto. - rewrite H1. rewrite H2. eapply match_arrs_size_ram_preserved; eauto. - unfold match_arr_assocs_size. rewrite Heqar1. auto. -Qed. - -Lemma match_arrs_size_ram_preserved3 : - forall m rs1 bar nar bar' nar' ram rs2, - exec_ram rs1 {| assoc_nonblocking := nar; assoc_blocking := bar |} - ram rs2 {| assoc_nonblocking := nar'; assoc_blocking := bar' |} -> - match_empty_size m nar -> - match_empty_size m bar -> - match_empty_size m nar' /\ match_empty_size m bar'. -Proof. - induction 1; inversion 1; inversion 1; eauto. - Admitted. - Lemma match_empty_size_merge : forall nasa2 basa2 m, match_empty_size m nasa2 -> @@ -1716,7 +1634,30 @@ Proof. eexists. simplify. unfold merge_arr. unfold Verilog.arr in *. rewrite H6. rewrite H9. auto. rewrite H8. symmetry. apply combine_length. congruence. intros. - Admitted. + destruct (nasa2 ! s) eqn:?; destruct (basa2 ! s) eqn:?. + unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. + unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. inv H0. + apply H2 in Heqo. apply H4 in Heqo0. repeat inv_exists; simplify. + eexists. simplify. eauto. rewrite list_combine_length. + rewrite (arr_wf a). rewrite (arr_wf a0). lia. + unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. + unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. + apply H2 in Heqo. inv_exists; simplify. + econstructor; eauto. + unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. + unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. + inv H0. apply H4 in Heqo0. inv_exists; simplify. econstructor; eauto. + unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. + unfold merge_arr in *. setoid_rewrite Heqo in H0. setoid_rewrite Heqo0 in H0. + discriminate. + split; intros. + unfold merge_arrs in H0. rewrite AssocMap.gcombine in H0 by auto. + unfold merge_arr in *. repeat destruct_match; crush. apply H5 in Heqo0; auto. + pose proof H0. + apply H5 in H0. + apply H3 in H6. unfold merge_arrs. rewrite AssocMap.gcombine by auto. + setoid_rewrite H0. setoid_rewrite H6. auto. +Qed. Lemma match_empty_size_match : forall m nasa2 basa2, @@ -1758,6 +1699,94 @@ Proof. Qed. Hint Resolve match_get_merge : mgen. +Lemma match_arrs_size_stmnt_preserved : + forall m f rs1 bar nar bar' nar' c rs2, + stmnt_runp f rs1 {| assoc_nonblocking := nar; assoc_blocking := bar |} + c rs2 {| assoc_nonblocking := nar'; assoc_blocking := bar' |} -> + match_empty_size m nar -> + match_empty_size m bar -> + match_empty_size m nar' /\ match_empty_size m bar'. +Proof. + induction 1; inversion 1; inversion 1; eauto. + Admitted. + +Lemma match_arrs_size_ram_preserved : + forall m rs1 ar1 ar2 ram rs2, + exec_ram rs1 ar1 ram rs2 ar2 -> + match_empty_size m (assoc_nonblocking ar1) -> + match_empty_size m (assoc_blocking ar1) -> + match_empty_size m (assoc_nonblocking ar2) + /\ match_empty_size m (assoc_blocking ar2). +Proof. + Ltac masrp_tac := + match goal with + | H: context[forall s arr, ?ar ! s = Some arr -> _], H2: ?ar ! _ = Some _ |- _ => + let H3 := fresh "H" in + learn H; pose proof H2 as H3; apply H in H3; repeat inv_exists + | H: context[forall s, ?ar ! s = None <-> _], H2: ?ar ! _ = None |- _ => + let H3 := fresh "H" in + learn H; pose proof H2 as H3; apply H in H3 + | H: context[forall s, _ <-> ?ar ! s = None], H2: ?ar ! _ = None |- _ => + let H3 := fresh "H" in + learn H; pose proof H2 as H3; apply H in H3 + | ra: arr_associations |- _ => + let ra1 := fresh "ran" in let ra2 := fresh "rab" in destruct ra as [ra1 ra2] + | |- _ ! _ = _ => solve [mgen_crush] + | |- _ = _ => congruence + | |- _ <> _ => lia + | H: ?ar ! ?s = _ |- context[match ?ar ! ?r with _ => _ end] => learn H; destruct (Pos.eq_dec s r); subst + | H: ?ar ! ?s = _ |- context[match ?ar ! ?s with _ => _ end] => setoid_rewrite H + | |- context[match ?ar ! ?s with _ => _ end] => destruct (ar ! s) eqn:? + | H: ?s <> ?r |- context[(_ # ?r <- _) ! ?s] => rewrite AssocMap.gso + | H: ?r <> ?s |- context[(_ # ?r <- _) ! ?s] => rewrite AssocMap.gso + | |- context[(_ # ?s <- _) ! ?s] => rewrite AssocMap.gss + | H: context[match ?ar ! ?r with _ => _ end ! ?s] |- _ => + destruct (ar ! r) eqn:?; destruct (Pos.eq_dec r s); subst + | H: ?ar ! ?s = _, H2: context[match ?ar ! ?s with _ => _ end] |- _ => + setoid_rewrite H in H2 + | H: context[match ?ar ! ?s with _ => _ end] |- _ => destruct (ar ! s) eqn:? + | H: ?s <> ?r, H2: context[(_ # ?r <- _) ! ?s] |- _ => rewrite AssocMap.gso in H2 + | H: ?r <> ?s, H2: context[(_ # ?r <- _) ! ?s] |- _ => rewrite AssocMap.gso in H2 + | H: context[(_ # ?s <- _) ! ?s] |- _ => rewrite AssocMap.gss in H + | |- context[match_empty_size] => constructor + | |- context[arr_assocmap_set] => unfold arr_assocmap_set + | H: context[arr_assocmap_set] |- _ => unfold arr_assocmap_set in H + | |- exists _, _ => econstructor + | |- _ <-> _ => split + end; simplify. + induction 1; inversion 1; inversion 1; subst; simplify; try solve [repeat masrp_tac]. + masrp_tac. masrp_tac. solve [repeat masrp_tac]. + masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. + masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. masrp_tac. + masrp_tac. apply H7 in H9; inv_exists; simplify. repeat masrp_tac. auto. + repeat masrp_tac. + repeat masrp_tac. + repeat masrp_tac. + destruct (Pos.eq_dec (ram_mem r) s); subst; repeat masrp_tac. + destruct (Pos.eq_dec (ram_mem r) s); subst; repeat masrp_tac. + apply H8 in H17; auto. apply H8 in H17; auto. + Unshelve. eauto. +Qed. +Hint Resolve match_arrs_size_ram_preserved : mgen. + +Lemma match_arrs_size_ram_preserved2 : + forall m rs1 na na' ba ba' ram rs2, + exec_ram rs1 {| assoc_nonblocking := na; assoc_blocking := ba |} ram rs2 + {| assoc_nonblocking := na'; assoc_blocking := ba' |} -> + match_empty_size m na -> match_empty_size m ba -> + match_empty_size m na' /\ match_empty_size m ba'. +Proof. + intros. + remember ({| assoc_blocking := ba; assoc_nonblocking := na |}) as ar1. + remember ({| assoc_blocking := ba'; assoc_nonblocking := na' |}) as ar2. + assert (X1: na' = (assoc_nonblocking ar2)) by (rewrite Heqar2; auto). rewrite X1. + assert (X2: ba' = (assoc_blocking ar2)) by (rewrite Heqar2; auto). rewrite X2. + assert (X3: na = (assoc_nonblocking ar1)) by (rewrite Heqar1; auto). rewrite X3 in *. + assert (X4: ba = (assoc_blocking ar1)) by (rewrite Heqar1; auto). rewrite X4 in *. + eapply match_arrs_size_ram_preserved; mgen_crush. +Qed. +Hint Resolve match_arrs_size_ram_preserved2 : mgen. + Section CORRECTNESS. Context (prog tprog: program). @@ -1822,15 +1851,14 @@ Section CORRECTNESS. 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_preserved3; eauto. unfold match_empty_size; mgen_crush. } + { eapply match_arrs_size_stmnt_preserved; 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_preserved3; mgen_crush. } simplify. + { eapply match_arrs_size_stmnt_preserved; mgen_crush. } simplify. assert (MATCH_SIZE2: match_empty_size m nasa3 /\ match_empty_size m basa3). - { eapply match_arrs_size_ram_preserved3; mgen_crush. unfold match_empty_size. mgen_crush. + { eapply match_arrs_size_ram_preserved2; mgen_crush. unfold match_empty_size. mgen_crush. unfold match_empty_size. mgen_crush. apply match_empty_size_merge; mgen_crush. } simplify. - assert (MATCH_ARR3: match_arrs_size nasa3 basa3). - { eapply match_arrs_size_ram_preserved2; eauto; apply match_empty_size_merge; eauto. } + 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. @@ -1860,10 +1888,7 @@ Section CORRECTNESS. assert (assoc_blocking ! (mod_st (transf_module m)) = Some (posToValue st)) by admit; auto. unfold empty_stack in *. simplify. unfold transf_module in *. simplify. repeat destruct_match; crush. - unfold merge_arr_assocs, merge_reg_assocs, empty_stack' in *. simplify. - assert (2 ^ Nat.log2_up (mod_stk_len m) = (mod_stk_len m))%nat by admit. - rewrite H7 in H17. rewrite H7. - eassumption. + unfold merge_arr_assocs, merge_reg_assocs, empty_stack' in *. simplify. eassumption. econstructor. mgen_crush. simplify. assert (match_empty_size m (merge_arrs nasa2 basa2)) by admit. eauto with mgen. auto. -- cgit