From b01a71865d74c30b076d5ccff5ca69b65a685e73 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 25 Mar 2021 22:07:33 +0000 Subject: Add proofs of size preservation of statements and ram --- src/hls/Memorygen.v | 139 ++++++++++++++++++++++++++++++++++------------------ 1 file changed, 92 insertions(+), 47 deletions(-) diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 81a980f..9c2bfff 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -1699,16 +1699,97 @@ Proof. Qed. Hint Resolve match_get_merge : mgen. +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. + +Lemma match_empty_assocmap_set : + forall m r i rhsval asa, + match_empty_size m asa -> + match_empty_size m (arr_assocmap_set r i rhsval asa). +Proof. + inversion 1; subst; simplify. + constructor. intros. + repeat masrp_tac. + intros. do 5 masrp_tac; try solve [repeat masrp_tac]. + apply H1 in H3. inv_exists. simplify. + econstructor. simplify. apply H3. congruence. + repeat masrp_tac. destruct (Pos.eq_dec r s); subst. + rewrite AssocMap.gss in H8. discriminate. + rewrite AssocMap.gso in H8; auto. apply H2 in H8. auto. + destruct (Pos.eq_dec r s); subst. apply H1 in H5. inv_exists. simplify. + rewrite H5 in H8. discriminate. + rewrite AssocMap.gso; auto. + apply H2 in H5. auto. apply H2 in H5. auto. + Unshelve. auto. +Qed. +Hint Resolve match_empty_assocmap_set : 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. + forall m f rs1 ar1 ar2 c rs2, + stmnt_runp f rs1 ar1 c 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. + induction 1; inversion 1; inversion 1; eauto; simplify; try solve [repeat masrp_tac]. + subst. apply IHstmnt_runp2; apply IHstmnt_runp1; auto. + apply IHstmnt_runp2; apply IHstmnt_runp1; auto. + apply match_empty_assocmap_set. auto. + apply match_empty_assocmap_set. auto. +Qed. + +Lemma match_arrs_size_stmnt_preserved2 : + forall m f rs1 na ba na' ba' c rs2, + stmnt_runp f rs1 {| assoc_nonblocking := na; assoc_blocking := ba |} c 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_stmnt_preserved; mgen_crush. +Qed. +Hint Resolve match_arrs_size_stmnt_preserved2 : mgen. Lemma match_arrs_size_ram_preserved : forall m rs1 ar1 ar2 ram rs2, @@ -1718,42 +1799,6 @@ Lemma match_arrs_size_ram_preserved : 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. @@ -1851,10 +1896,10 @@ 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_preserved; eauto. unfold match_empty_size; mgen_crush. } + { 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_preserved; mgen_crush. } simplify. + { 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. unfold match_empty_size. mgen_crush. unfold match_empty_size. mgen_crush. apply match_empty_size_merge; mgen_crush. } simplify. -- cgit