diff options
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 64 |
1 files changed, 34 insertions, 30 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 556e3cc..75d5321 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -33,8 +33,8 @@ Require Import vericert.hls.HTLgen. Require Import vericert.hls.AssocMap. Require Import vericert.hls.FunctionalUnits. -Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. -Hint Resolve Maps.PTree.elements_correct : htlspec. +#[local] Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. +#[local] Hint Resolve Maps.PTree.elements_correct : htlspec. Remark bind_inversion: forall (A B: Type) (f: mon A) (g: A -> mon B) @@ -164,7 +164,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) -Hint Constructors tr_instr : htlspec. +#[local] Hint Constructors tr_instr : htlspec. Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) (fin rtrn st stk : reg) : Prop := @@ -175,16 +175,16 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts t trans!pc = Some t -> tr_instr fin rtrn st stk i s t -> tr_code c pc i stmnts trans fin rtrn st stk. -Hint Constructors tr_code : htlspec. +#[local] Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3 wf4, m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk initial_funct_units scldecls arrdecls wf) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3 wf4) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> @@ -198,70 +198,70 @@ Inductive tr_module (f : RTL.function) : module -> Prop := rst = ((RTL.max_reg_function f) + 6)%positive -> clk = ((RTL.max_reg_function f) + 7)%positive -> tr_module f m. -Hint Constructors tr_module : htlspec. +#[local] Hint Constructors tr_module : htlspec. Lemma create_reg_datapath_trans : forall sz s s' x i iop, create_reg iop sz s = OK x s' i -> s.(st_datapath) = s'.(st_datapath). Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_datapath_trans : htlspec. +#[local] Hint Resolve create_reg_datapath_trans : htlspec. Lemma create_reg_controllogic_trans : forall sz s s' x i iop, create_reg iop sz s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic). Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_controllogic_trans : htlspec. +#[local] Hint Resolve create_reg_controllogic_trans : htlspec. Lemma declare_reg_datapath_trans : forall sz s s' x i iop r, declare_reg iop r sz s = OK x s' i -> s.(st_datapath) = s'.(st_datapath). Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_datapath_trans : htlspec. +#[local] Hint Resolve create_reg_datapath_trans : htlspec. Lemma declare_reg_controllogic_trans : forall sz s s' x i iop r, declare_reg iop r sz s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic). Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_reg_controllogic_trans : htlspec. +#[local] Hint Resolve create_reg_controllogic_trans : htlspec. Lemma declare_reg_freshreg_trans : forall sz s s' x i iop r, declare_reg iop r sz s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg). Proof. inversion 1; auto. Qed. -Hint Resolve declare_reg_freshreg_trans : htlspec. +#[local] Hint Resolve declare_reg_freshreg_trans : htlspec. Lemma create_arr_datapath_trans : forall sz ln s s' x i iop, create_arr iop sz ln s = OK x s' i -> s.(st_datapath) = s'.(st_datapath). Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_arr_datapath_trans : htlspec. +#[local] Hint Resolve create_arr_datapath_trans : htlspec. Lemma create_arr_controllogic_trans : forall sz ln s s' x i iop, create_arr iop sz ln s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic). Proof. intros. monadInv H. trivial. Qed. -Hint Resolve create_arr_controllogic_trans : htlspec. +#[local] Hint Resolve create_arr_controllogic_trans : htlspec. Lemma get_refl_x : forall s s' x i, get s = OK x s' i -> s = x. Proof. inversion 1. trivial. Qed. -Hint Resolve get_refl_x : htlspec. +#[local] Hint Resolve get_refl_x : htlspec. Lemma get_refl_s : forall s s' x i, get s = OK x s' i -> s = s'. Proof. inversion 1. trivial. Qed. -Hint Resolve get_refl_s : htlspec. +#[local] Hint Resolve get_refl_s : htlspec. Ltac inv_incr := repeat match goal with @@ -350,7 +350,7 @@ Lemma translate_eff_addressing_freshreg_trans : Proof. destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. Qed. -Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. +#[local] Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. Lemma translate_comparison_freshreg_trans : forall op args s r s' i, @@ -359,7 +359,7 @@ Lemma translate_comparison_freshreg_trans : Proof. destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. Qed. -Hint Resolve translate_comparison_freshreg_trans : htlspec. +#[local] Hint Resolve translate_comparison_freshreg_trans : htlspec. Lemma translate_comparisonu_freshreg_trans : forall op args s r s' i, @@ -368,7 +368,7 @@ Lemma translate_comparisonu_freshreg_trans : Proof. destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. Qed. -Hint Resolve translate_comparisonu_freshreg_trans : htlspec. +#[local] Hint Resolve translate_comparisonu_freshreg_trans : htlspec. Lemma translate_comparison_imm_freshreg_trans : forall op args s r s' i n, @@ -377,7 +377,7 @@ Lemma translate_comparison_imm_freshreg_trans : Proof. destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. Qed. -Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. +#[local] Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. Lemma translate_comparison_immu_freshreg_trans : forall op args s r s' i n, @@ -386,7 +386,7 @@ Lemma translate_comparison_immu_freshreg_trans : Proof. destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. Qed. -Hint Resolve translate_comparison_immu_freshreg_trans : htlspec. +#[local] Hint Resolve translate_comparison_immu_freshreg_trans : htlspec. Lemma translate_condition_freshreg_trans : forall op args s r s' i, @@ -395,7 +395,7 @@ Lemma translate_condition_freshreg_trans : Proof. destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. Qed. -Hint Resolve translate_condition_freshreg_trans : htlspec. +#[local] Hint Resolve translate_condition_freshreg_trans : htlspec. Lemma translate_instr_freshreg_trans : forall op args s r s' i, @@ -405,7 +405,7 @@ Proof. destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. monadInv H1. eauto with htlspec. Qed. -Hint Resolve translate_instr_freshreg_trans : htlspec. +#[local] Hint Resolve translate_instr_freshreg_trans : htlspec. Lemma translate_arr_access_freshreg_trans : forall mem addr args st s r s' i, @@ -414,35 +414,35 @@ Lemma translate_arr_access_freshreg_trans : Proof. intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. Qed. -Hint Resolve translate_arr_access_freshreg_trans : htlspec. +#[local] Hint Resolve translate_arr_access_freshreg_trans : htlspec. Lemma add_instr_freshreg_trans : forall n n' st s r s' i, add_instr n n' st s = OK r s' i -> s.(st_freshreg) = s'.(st_freshreg). Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_instr_freshreg_trans : htlspec. +#[local] Hint Resolve add_instr_freshreg_trans : htlspec. Lemma add_branch_instr_freshreg_trans : forall n n0 n1 e s r s' i, add_branch_instr e n n0 n1 s = OK r s' i -> s.(st_freshreg) = s'.(st_freshreg). Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_branch_instr_freshreg_trans : htlspec. +#[local] Hint Resolve add_branch_instr_freshreg_trans : htlspec. Lemma add_node_skip_freshreg_trans : forall n1 n2 s r s' i, add_node_skip n1 n2 s = OK r s' i -> s.(st_freshreg) = s'.(st_freshreg). Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_node_skip_freshreg_trans : htlspec. +#[local] Hint Resolve add_node_skip_freshreg_trans : htlspec. Lemma add_instr_skip_freshreg_trans : forall n1 n2 s r s' i, add_instr_skip n1 n2 s = OK r s' i -> s.(st_freshreg) = s'.(st_freshreg). Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. -Hint Resolve add_instr_skip_freshreg_trans : htlspec. +#[local] Hint Resolve add_instr_skip_freshreg_trans : htlspec. Lemma transf_instr_freshreg_trans : forall fin ret st instr s v s' i, @@ -460,7 +460,7 @@ Proof. congruence. (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*) Qed. -Hint Resolve transf_instr_freshreg_trans : htlspec. +#[local] Hint Resolve transf_instr_freshreg_trans : htlspec. Lemma collect_trans_instr_freshreg_trans : forall fin ret st l s s' i, @@ -590,7 +590,7 @@ Proof. intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. destruct H2. inv H2. contradiction. assumption. assumption. Qed. -Hint Resolve iter_expand_instr_spec : htlspec. +#[local] Hint Resolve iter_expand_instr_spec : htlspec. Lemma create_arr_inv : forall w x y z a b c d, create_arr w x y z = OK (a, b) c d -> @@ -649,5 +649,9 @@ Proof. replace (st_datapath s10) with (st_datapath s3) by congruence. replace (st_st s10) with (st_st s3) by congruence. eapply iter_expand_instr_spec; eauto with htlspec. + rewrite H5. rewrite H7. apply EQ2. apply PTree.elements_complete. + eauto with htlspec. + erewrite <- collect_declare_freshreg_trans; try eassumption. + lia. Qed. |