From 8573889ca84a84475761b4d75d55547a2995c831 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 7 Apr 2021 01:11:04 +0100 Subject: Basically done with proof --- src/hls/HTL.v | 14 ++++++++++++++ src/hls/HTLPargen.v | 10 ++++++---- src/hls/HTLgen.v | 10 ++++++---- src/hls/HTLgenproof.v | 4 ++-- src/hls/HTLgenspec.v | 4 ++-- src/hls/Memorygen.v | 38 ++++++++++++++++++++++++++++++++------ 6 files changed, 62 insertions(+), 18 deletions(-) diff --git a/src/hls/HTL.v b/src/hls/HTL.v index e614246..61ea541 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -92,6 +92,7 @@ Record module: Type := mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r'; + mod_params_wf : Forall (Pos.gt mod_st) mod_params; }. Definition fundef := AST.fundef module. @@ -338,3 +339,16 @@ Proof. inversion 1 as [ Hv | Hv ]; unfold max_reg_module; apply max_reg_stmnt_le_stmnt_tree in Hv; lia. Qed. + +Lemma max_list_correct l st : st > max_list l -> Forall (Pos.gt st) l. +Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed. + +Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True}. + refine ( + match bool_dec (max_list l left _ + | _ => _ + end + ); auto. + apply max_list_correct. apply Pos.ltb_lt in e. lia. +Qed. diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 50defee..7ce6c7a 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -817,9 +817,10 @@ Definition transf_module (f: function) : mon HTL.module. Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned, - decide_order (st_st current_state) fin rtrn stack start rst clk + decide_order (st_st current_state) fin rtrn stack start rst clk, + max_list_dec (fn_params f) (st_st current_state) with - | left LEDATA, left LECTRL, left MORD => + | left LEDATA, left LECTRL, left MORD, left WFPARAMS => ret (HTL.mkmodule f.(fn_params) current_state.(st_datapath) @@ -838,8 +839,9 @@ Definition transf_module (f: function) : mon HTL.module. None (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)) MORD - _) - | _, _, _ => error (Errors.msg "More than 2^32 states.") + _ + WFPARAMS) + | _, _, _, _ => error (Errors.msg "More than 2^32 states.") end else error (Errors.msg "Stack size misalignment.")); discriminate. Defined. diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index b55d7a3..4d60a24 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -608,9 +608,10 @@ Definition transf_module (f: function) : mon HTL.module. do current_state <- get; match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned, - decide_order (st_st current_state) fin rtrn stack start rst clk + decide_order (st_st current_state) fin rtrn stack start rst clk, + max_list_dec (RTL.fn_params f) (st_st current_state) with - | left LEDATA, left LECTRL, left MORD => + | left LEDATA, left LECTRL, left MORD, left WFPARAMS => ret (HTL.mkmodule f.(RTL.fn_params) current_state.(st_datapath) @@ -629,8 +630,9 @@ Definition transf_module (f: function) : mon HTL.module. None (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)) MORD - _) - | _, _, _ => error (Errors.msg "More than 2^32 states.") + _ + WFPARAMS) + | _, _, _, _ => error (Errors.msg "More than 2^32 states.") end else error (Errors.msg "Stack size misalignment.")); discriminate. Defined. diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 3b5496f..1aac3b7 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -2602,7 +2602,7 @@ Section CORRECTNESS. constructor. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. - destruct wf as [HCTRL HDATA]. apply HCTRL. + destruct wf1 as [HCTRL HDATA]. apply HCTRL. apply AssocMapExt.elements_iff. eexists. match goal with H: control ! pc = Some _ |- _ => apply H end. @@ -2632,7 +2632,7 @@ Section CORRECTNESS. unfold state_st_wf in WF; big_tac; eauto. - destruct wf as [HCTRL HDATA]. apply HCTRL. + destruct wf1 as [HCTRL HDATA]. apply HCTRL. apply AssocMapExt.elements_iff. eexists. match goal with H: control ! pc = Some _ |- _ => apply H end. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 6a10fa2..16bdcaf 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -178,12 +178,12 @@ 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 wf1 wf2 wf3, + 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 scldecls arrdecls None wf1 wf2 wf3) -> + 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) -> diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 8453263..06e0aec 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -207,9 +207,9 @@ Definition transf_module (m: module): module. (AssocMap.set m.(mod_stk) (None, VArray 32 (2 ^ Nat.log2_up new_size))%nat m.(mod_arrdecls)) (Some ram) - _ _ _ + _ (mod_ordering_wf m) _ (mod_params_wf m) | _, _ => m - end). apply is_wf. exact (mod_ordering_wf m). + end). apply is_wf. inversion 1; subst. auto using module_ram_wf'. Defined. @@ -3139,10 +3139,18 @@ Proof. Qed. Hint Resolve disable_ram_set_gso : mgen. -Lemma disable_ram_None : forall rs, disable_ram None rs. +Lemma disable_ram_None rs : disable_ram None rs. Proof. unfold disable_ram; auto. Qed. Hint Resolve disable_ram_None : mgen. +Lemma init_regs_equal_empty l st : + Forall (Pos.gt st) l -> (init_regs nil l) ! st = None. +Proof. induction l; simplify; apply AssocMap.gempty. Qed. + +Lemma forall_lt_num : + forall l p p', Forall (Pos.gt p) l -> p < p' -> Forall (Pos.gt p') l. +Proof. induction l; crush; inv H; constructor; [lia | eauto]. Qed. + Section CORRECTNESS. Context (prog tprog: program). @@ -3259,7 +3267,17 @@ Section CORRECTNESS. replace (mod_st (transf_module m)) with (mod_st m) by (rewrite RAM0; auto). repeat econstructor; mgen_crush. unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - admit. + pose proof (mod_ordering_wf m); unfold module_ordering in *. + pose proof (mod_params_wf m). + pose proof (mod_ram_wf m r Heqo0). + pose proof (ram_ordering r). + simplify. + repeat rewrite find_assocmap_gso by lia. + assert ((init_regs nil (mod_params m)) ! (ram_en r) = None). + { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } + assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None). + { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } + unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto. - econstructor. econstructor. apply Smallstep.plus_one. econstructor. replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m). replace (mod_reset (transf_module m)) with (mod_reset m). @@ -3270,7 +3288,15 @@ Section CORRECTNESS. all: try solve [unfold transf_module; repeat destruct_match; mgen_crush]. repeat econstructor; mgen_crush. unfold disable_ram. unfold transf_module; repeat destruct_match; crush. - admit. + unfold max_reg_module. + repeat rewrite find_assocmap_gso by lia. + assert (max_reg_module m + 1 > max_list (mod_params m)). + { unfold max_reg_module. lia. } + apply max_list_correct in H0. + unfold find_assocmap, AssocMapExt.get_default. + rewrite init_regs_equal_empty. rewrite init_regs_equal_empty. auto. + eapply forall_lt_num. eassumption. unfold max_reg_module. lia. + eapply forall_lt_num. eassumption. unfold max_reg_module. lia. - inv STACKS. destruct b1; subst. econstructor. econstructor. apply Smallstep.plus_one. econstructor. eauto. @@ -3329,7 +3355,7 @@ Section CORRECTNESS. simplify. unfold max_reg_module. lia. simplify. unfold max_reg_module. lia. simplify. unfold max_reg_module. lia. - Admitted. + Qed. Hint Resolve transf_step_correct : mgen. Lemma transf_initial_states : -- cgit