diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/common/Vericertlib.v | 35 | ||||
| -rw-r--r-- | src/hls/HTLgenproof.v | 53 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v | 155 |
3 files changed, 184 insertions, 59 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index a36e86c..805dbda 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -238,6 +238,41 @@ Ltac maybe t := t + idtac. Global Opaque Nat.div. Global Opaque Z.mul. +Inductive Ascending : list positive -> Prop := + | Ascending_nil : Ascending nil + | Ascending_single : forall x, Ascending (x::nil) + | Ascending_cons : forall x y l, (x < y)%positive -> Ascending (y::l) -> Ascending (x::y::l). + +Lemma map_fst_split : forall A B (l : list (A * B)), List.map fst l = fst (List.split l). +Proof. + induction l; crush. + destruct a; destruct (split l). + crush. +Qed. + +Lemma Ascending_Forall : forall l x, Ascending (x :: l) -> Forall (fun y => x < y)%positive l. +Proof. + induction l; crush. + inv H. + specialize (IHl _ H4). + apply Forall_cons. + - crush. + - apply Forall_impl with (P:=(fun y : positive => (a < y)%positive)); crush. +Qed. + +Lemma Ascending_NoDup : forall l, Ascending l -> NoDup l. +Proof. + induction 1; simplify. + - constructor. + - constructor. crush. constructor. + - constructor; auto. + intro contra. inv contra; crush. + auto_apply Ascending_Forall. + rewrite Forall_forall in *. + specialize (H2 x ltac:(auto)). + lia. +Qed. + (* Definition const (A B : Type) (a : A) (b : B) : A := a. Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *) diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 5bfa1f0..13a4345 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1690,7 +1690,7 @@ Section CORRECTNESS. (forall n param, nth_error fn_params n = Some param -> externctrl!param = Some (fn, HTL.ctrl_param n)). Proof. - intros * [Hlen Htr] * Hfn_params. + intros * [Hlen [Hnodup Hmapped]] * Hfn_params. assert (H : exists arg, nth_error args n = Some arg). { apply length_nth_error. @@ -1698,7 +1698,7 @@ Section CORRECTNESS. lia. } destruct H as [ arg H ]. - edestruct (Htr _ _ H) as [? [? ?]]. + edestruct (Hmapped _ _ H) as [? [? ?]]. enough (Some x = Some param) by crush. congruence. @@ -1734,7 +1734,7 @@ Section CORRECTNESS. forall v : value, ~ In (r, v) (List.combine params argvals). Proof. unfold "~". - intros * Hordering [Hlen Hmapped] Hclk * contra. + intros * Hordering [Hlen [Hnodup Hmapped]] Hclk * contra. apply in_combine_l in contra. apply In_nth_error in contra. destruct contra as [? ?]. @@ -1791,13 +1791,39 @@ Section CORRECTNESS. intros * Hmapped Hrst contra. inv Hmapped. edestruct (In_nth_error _ _ contra) as [n ?]. - edestruct (nth_error_same_length params args); crush; eauto. - edestruct H0 as [? [? ?]]; eauto. + edestruct (nth_error_same_length params args); eauto. + edestruct H0 as [? [? [? ?]]]; eauto. replace x0 with r in *; crush. apply option_inv. transitivity (nth_error params n); crush. Qed. + Lemma param_reg_lower : forall params r clk args externctrl fn, + externctrl_params_mapped args params externctrl fn -> + externctrl_ordering externctrl clk -> + (r < clk)%positive -> + ~ In r params. + Proof. + unfold externctrl_ordering. + intros * [Hlen [Hnodup Hmapped]] Hordering Hlt contra. + destruct (In_nth_error _ _ contra) as [n Hparam]. + destruct (nth_error_same_length params args _ _ ltac:(crush) Hparam). + destruct (Hmapped n _ ltac:(eassumption)) as [r' [? ?]]. + replace r' with r in *. + - specialize (Hordering r ltac:(eauto)). + lia. + - enough (Some r = Some r') by crush. + transitivity (nth_error params n); crush. + Qed. + + Lemma not_in_combine_l : forall A B (x : A) (y : B) l1 l2, + ~ In x l1 -> + ~ In (x, y) (List.combine l1 l2). + Proof. eauto using in_combine_l. Qed. + + Ltac not_in_params := + intros; try apply not_in_combine_l; eapply param_reg_lower; eauto; lia. + Lemma transl_icall_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) (rs : RTL.regset) (m : mem) sig fn fd args dst pc', @@ -1847,25 +1873,25 @@ Section CORRECTNESS. * trivial. * trivial. * apply merge_st. - -- admit. + -- eapply param_reg_lower; eauto. lia. -- not_control_reg. * eauto. + eapply HTL.step_module; trivial. * simpl. apply AssocMapExt.merge_correct_2; auto. - rewrite assign_all_out by admit. + rewrite assign_all_out by not_in_params. rewrite AssocMap.gso by not_control_reg. rewrite AssocMap.gso by lia. apply AssocMap.gempty. * simpl. apply AssocMapExt.merge_correct_2; auto. - rewrite assign_all_out by admit. + rewrite assign_all_out by not_in_params. rewrite AssocMap.gso by not_control_reg. rewrite AssocMap.gso by lia. apply AssocMap.gempty. * simpl. apply AssocMapExt.merge_correct_1; auto. - rewrite assign_all_out by admit. + rewrite assign_all_out by not_in_params. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gss. * eauto. @@ -1875,12 +1901,13 @@ Section CORRECTNESS. -- simpl. econstructor; econstructor; simpl. replace (Verilog.merge_regs ((empty_assocmap # st1 <- (posToValue x0)) # x1 <- (ZToValue 1)) ## x4 <- (asr ## args) asr) # x3 with (ZToValue 0) by admit. + (* TODO: Externctrl finish is false *) trivial. -- auto. -- econstructor. * simpl. apply AssocMapExt.merge_correct_1; auto. - rewrite assign_all_out by admit. + rewrite assign_all_out by not_in_params. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gss. * unfold join. @@ -1895,7 +1922,7 @@ Section CORRECTNESS. apply AssocMapExt.merge_correct_2. big_tac; [ apply AssocMap.gempty | not_control_reg]. apply merge_st. - -- admit. + -- not_in_params. -- not_control_reg. * auto. + eapply HTL.step_initcall. @@ -1924,13 +1951,13 @@ Section CORRECTNESS. * (* Match constants *) constructor; big_tac. -- apply AssocMapExt.merge_correct_2; crush. - rewrite assign_all_out by admit. + rewrite assign_all_out by not_in_params. rewrite AssocMap.gso by not_control_reg. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gempty. -- not_control_reg. -- apply AssocMapExt.merge_correct_2; crush. - rewrite assign_all_out by admit. + rewrite assign_all_out by not_in_params. rewrite AssocMap.gso by not_control_reg. rewrite AssocMap.gso by not_control_reg. apply AssocMap.gempty. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 70d35d8..3c52657 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -78,6 +78,7 @@ Hint Constructors tr_instr : htlspec. Definition externctrl_params_mapped (args params : list reg) externctrl (fn : ident) := length args = length params /\ + NoDup params /\ forall n arg, List.nth_error args n = Some arg -> exists r, List.nth_error params n = Some r /\ externctrl ! r = Some (fn, ctrl_param n). @@ -312,7 +313,7 @@ Ltac some_incr := | [ INCR : st_prop _ _ |- _ ] => inversion INCR end. -Lemma helper__map_externctrl_params_args : forall args param_pairs fn s s' k i, +Lemma xmap_externctrl_params_args : forall args param_pairs fn s s' k i, xmap_externctrl_params k fn args s = OK param_pairs s' i -> snd (List.split param_pairs) = args. Proof. @@ -324,13 +325,14 @@ Qed. Lemma map_externctrl_params_args : forall args param_pairs fn s s' i, map_externctrl_params fn args s = OK param_pairs s' i -> snd (List.split param_pairs) = args. -Proof. sauto use: helper__map_externctrl_params_args. Qed. +Proof. sauto use: xmap_externctrl_params_args. Qed. -Lemma helper__map_externctrl_params_spec : forall args n param_pairs k fn s s' i, +Lemma helper__map_externctrl_params_spec : forall args param_pairs k fn s s' i, xmap_externctrl_params k fn args s = OK param_pairs s' i -> - (n < length args)%nat -> - exists r, (List.nth_error (fst (List.split param_pairs)) n = Some r) /\ - (s'.(st_externctrl) ! r = Some (fn, ctrl_param (n+k))). + forall n, + (n < length args)%nat -> + exists r, (List.nth_error (fst (List.split param_pairs)) n = Some r) /\ + (s'.(st_externctrl) ! r = Some (fn, ctrl_param (n+k))). Proof. induction args. - sauto use: nth_error_nil. @@ -339,20 +341,77 @@ Proof. destruct n; simplify. + destruct (split x0). simpl. exists x. crush. monad_crush. - + destruct (IHargs n _ _ _ _ _ _ EQ1 ltac:(lia)). + + destruct (IHargs _ _ _ _ _ _ EQ1 n ltac:(lia)). destruct (split _). simpl in *. eexists. replace (S (n + k))%nat with (n + S k)%nat by lia. eassumption. - Qed. +Qed. + +Set Nested Proofs Allowed. + +Lemma xmap_externctrl_params_ascending : + forall args param_pairs k fn s s' i, + xmap_externctrl_params k fn args s = OK param_pairs s' i -> + Ascending (fst (List.split param_pairs)). +Proof. + assert ( + forall args param_pairs k fn s s' i, + xmap_externctrl_params k fn args s = OK param_pairs s' i -> + Ascending (List.map fst param_pairs)). { + induction args. + - simplify. monadInv H. simpl. constructor. + - intros. + monadInv H. + simpl. + exploit IHargs; try eassumption; intros. + destruct args; monadInv EQ1. + + constructor. + + simpl in *. + constructor. + * monadInv EQ. + monadInv EQ0. + lia. + * assumption. + } + intros. + rewrite <- map_fst_split. + eauto. +Qed. -Lemma map_externctrl_params_spec : forall args n param_pairs fn s s' i, +Lemma map_externctrl_params_spec : forall args param_pairs fn s s' i, map_externctrl_params fn args s = OK param_pairs s' i -> - (n < length args)%nat -> - exists r, (List.nth_error (fst (List.split param_pairs)) n = Some r) /\ - (s'.(st_externctrl) ! r = Some (fn, ctrl_param n)). -Proof. sauto use: helper__map_externctrl_params_spec. Qed. + externctrl_params_mapped (snd (List.split param_pairs)) (fst (List.split param_pairs)) (st_externctrl s') fn. +Proof. + intros. + unfold map_externctrl_params in *. + specialize (helper__map_externctrl_params_spec _ _ _ _ _ _ _ H); intro Hspec. + repeat split. + - rewrite split_length_r, split_length_l. trivial. + - eauto using xmap_externctrl_params_ascending, Ascending_NoDup. + - intros. + specialize (Hspec n). + erewrite (map_externctrl_params_args args) in *; eauto. + replace (n + 0)%nat with n in * by lia. + assert (n < Datatypes.length args)%nat by eauto using nth_error_length. + eauto. +Qed. Hint Resolve map_externctrl_params_spec : htlspec. +Lemma externctrl_params_mapped_trans : forall s s' args params fn, + externctrl_params_mapped args params (st_externctrl s) fn -> + st_prop s s' -> + externctrl_params_mapped args params (st_externctrl s') fn. +Proof. + unfold externctrl_params_mapped. + intros * [Hlen [Hnodup Hmapped]] INCR. + repeat split; eauto. + intros n arg Hntharg. + edestruct Hmapped as [? [Hnthparam Hparam]]; try eassumption. + exists x. split. assumption. + inv INCR. + destruct (H4 x); crush. +Qed. + Lemma iter_expand_instr_spec : forall l prog fin rtrn stack s s' i x c, HTLMonadExtra.collectlist (transf_instr (Globalenvs.Genv.globalenv prog) fin rtrn stack) l s = OK x s' i -> @@ -394,33 +453,38 @@ Proof. repeat (eapply ex_intro). - repeat (apply conj). - * monad_crush. - * monad_crush. - * monad_crush. - * transitivity (length x1). - replace l0 with (snd (List.split x1)). - apply split_length_r. - eapply map_externctrl_params_args; eassumption. - auto using split_length_l. - * intros. - destruct (map_externctrl_params_args _ _ _ _ _ _ EQ1); eauto using nth_error_length. - destruct (map_externctrl_params_spec _ n0 _ _ _ _ _ EQ1); eauto using nth_error_length. - exists x8. simplify; eauto. - monad_crush. - * eapply create_state_max; eassumption. - * replace x5 with (st_freshreg s6) in * by intro_step. + split. { monad_crush. } + split. { monad_crush. } + split. { monad_crush. } + split. { + apply (externctrl_params_mapped_trans s3 s'). + erewrite <- (map_externctrl_params_args l0 x1). + eapply map_externctrl_params_spec. + - eauto. + - eauto. + - saturate_incr. eauto. + } + split. { eapply create_state_max; eassumption. } + split. { + replace x5 with (st_freshreg s6) in * by intro_step. replace l0 with (snd (split x1)) by eauto using map_externctrl_params_args. rewrite combine_split. monad_crush. - * monad_crush. - * replace x6 with (st_freshreg s7) in * by intro_step. + } + split. { + monad_crush. + } + split. { + replace x6 with (st_freshreg s7) in * by intro_step. replace x5 with (st_freshreg s6) in * by intro_step. replace x4 with (st_freshreg s5) in * by intro_step. monad_crush. - * replace x4 with (st_freshreg s5) in * by intro_step. + } + { + replace x4 with (st_freshreg s5) in * by intro_step. monad_crush. + } + (* Icond *) tr_code_simple_tac. + (* Ireturn *) inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. @@ -461,20 +525,19 @@ Proof. inversion Htrans. replace (st_st s'). repeat (eapply ex_intro). - repeat (apply conj). - * eapply map_incr_some; inversion Htrans; eauto with htlspec. - * eapply map_incr_some; inversion Htrans; eauto with htlspec. - * eapply map_incr_some; inversion Htrans; eauto with htlspec. - * inv H5. eassumption. - * intros. - destruct H5. - destruct (H21 n0 ltac:(auto) ltac:(auto)) as [r [? ?]]. - eexists. split; eauto with htlspec. - * eauto with htlspec. - * eauto with htlspec. - * eauto with htlspec. - * eauto with htlspec. - * eauto with htlspec. + split. { + eapply map_incr_some; inversion Htrans; eauto with htlspec. + } + split. { + eapply map_incr_some; inversion Htrans; eauto with htlspec. + } + split. { + eapply map_incr_some; inversion Htrans; eauto with htlspec. + } + split. { + eauto using externctrl_params_mapped_trans. + } + eauto 10 with htlspec. + eapply tr_code_return; eauto with htlspec. inversion Htrans. simplify. eexists. |