diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-10 18:34:11 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-10 18:34:11 +0100 |
commit | 772ab903121839b805a49557652a4c3e1b6af0ae (patch) | |
tree | 67ebe65845be6b66136cb72e5cf1656d54beeca7 | |
parent | 990dadb1d15c54815132896b481c12b609238525 (diff) | |
download | vericert-772ab903121839b805a49557652a4c3e1b6af0ae.tar.gz vericert-772ab903121839b805a49557652a4c3e1b6af0ae.zip |
Clean up HTLgenspec
-rw-r--r-- | src/hls/HTLgenspec.v | 257 |
1 files changed, 130 insertions, 127 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index bf18c8a..1dfd264 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -34,9 +34,114 @@ Require Import vericert.hls.AssocMap. From Hammer Require Import Tactics. +(** * Relational specification of the translation *) + +(** We now define inductive predicates that characterise the fact that the +statemachine that is created by the translation contains the correct +translations for each of the elements *) + +(** [tr_instr] describes the translation of instructions that are directly translated into a single state *) +Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -> control_stmnt -> Prop := +| tr_instr_Inop : + forall n, + Z.pos n <= Int.max_unsigned -> + tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) +| tr_instr_Iop : + forall n op args dst s s' e i, + Z.pos n <= Int.max_unsigned -> + translate_instr op args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) +| tr_instr_Icond : + forall n1 n2 cond args s s' i c, + Z.pos n1 <= Int.max_unsigned -> + Z.pos n2 <= Int.max_unsigned -> + translate_condition cond args s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) +| tr_instr_Iload : + forall mem addr args s s' i c dst n, + Z.pos n <= Int.max_unsigned -> + translate_arr_access mem addr args stk s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (Vnonblock (Vvar dst) c) (state_goto st n) +| tr_instr_Istore : + forall mem addr args s s' i c src n, + Z.pos n <= Int.max_unsigned -> + translate_arr_access mem addr args stk s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) + (state_goto st n). +(*| tr_instr_Ijumptable : + 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. + +Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts : datapath) (trans : controllogic) + (externctrl : AssocMap.t (ident * controlsignal)) (fin rtrn st stk : reg) : Prop := +| tr_code_single : + forall s t, + c!pc = Some i -> + stmnts!pc = Some s -> + trans!pc = Some t -> + tr_instr fin rtrn st stk i s t -> + tr_code c pc i stmnts trans externctrl fin rtrn st stk +| tr_code_call : + forall sig fn args dst n, + c!pc = Some (RTL.Icall sig (inr fn) args dst n) -> + Z.pos n <= Int.max_unsigned -> + + (exists pc2 fn_rst fn_return fn_finish fn_params, + externctrl ! fn_rst = Some (fn, ctrl_reset) /\ + externctrl ! fn_return = Some (fn, ctrl_return) /\ + externctrl ! fn_finish = Some (fn, ctrl_finish) /\ + (forall n arg, List.nth_error args n = Some arg -> + exists r, In (r, arg) (List.combine fn_params args) /\ + externctrl ! r = Some (fn, ctrl_param n)) /\ + + stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) /\ + trans!pc = Some (state_goto st pc2) /\ + stmnts!pc2 = Some (join fn_return fn_rst dst) /\ + trans!pc2 = Some (state_wait st fn_finish n)) -> + + tr_code c pc i stmnts trans externctrl fin rtrn st stk +| tr_code_return : + forall r, + c!pc = Some (RTL.Ireturn r) -> + + (exists pc2, + stmnts!pc = Some (return_val fin rtrn r) /\ + trans!pc = Some (state_goto st pc2) /\ + stmnts!pc2 = Some (idle fin) /\ + trans!pc2 = Some Vskip) -> + + tr_code c pc i stmnts trans externctrl fin rtrn st stk. +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 externctrl wf, + m = (mkmodule f.(RTL.fn_params) + data + control + f.(RTL.fn_entrypoint) + st stk stk_len fin rtrn start rst clk scldecls arrdecls externctrl wf) -> + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code f.(RTL.fn_code) pc i data control externctrl fin rtrn st stk) -> + stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> + Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> + (st > (RTL.max_reg_function f))%positive -> + (fin > (RTL.max_reg_function f))%positive -> + (rtrn > (RTL.max_reg_function f))%positive -> + (stk > (RTL.max_reg_function f))%positive -> + (start > (RTL.max_reg_function f))%positive -> + (rst > (RTL.max_reg_function f))%positive -> + (clk > (RTL.max_reg_function f))%positive -> + tr_module f m. +Hint Constructors tr_module : htlspec. + Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. Hint Resolve Maps.PTree.elements_correct : htlspec. Hint Resolve Maps.PTree.gss : htlspec. +Hint Resolve PTree.elements_complete : htlspec. Hint Resolve -> Z.leb_le : htlspec. Hint Unfold block : htlspec. @@ -176,109 +281,20 @@ Ltac monad_crush := Ltac full_split := repeat match goal with [ |- _ /\ _ ] => split end. -(** * Relational specification of the translation *) - -(** We now define inductive predicates that characterise the fact that the -statemachine that is created by the translation contains the correct -translations for each of the elements *) - -(** [tr_instr] describes the translation of instructions that are directly translated into a single state *) -Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -> control_stmnt -> Prop := -| tr_instr_Inop : - forall n, - Z.pos n <= Int.max_unsigned -> - tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) -| tr_instr_Iop : - forall n op args dst s s' e i, - Z.pos n <= Int.max_unsigned -> - translate_instr op args s = OK e s' i -> - tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) -| tr_instr_Icond : - forall n1 n2 cond args s s' i c, - Z.pos n1 <= Int.max_unsigned -> - Z.pos n2 <= Int.max_unsigned -> - translate_condition cond args s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) -| tr_instr_Iload : - forall mem addr args s s' i c dst n, - Z.pos n <= Int.max_unsigned -> - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (Vnonblock (Vvar dst) c) (state_goto st n) -| tr_instr_Istore : - forall mem addr args s s' i c src n, - Z.pos n <= Int.max_unsigned -> - translate_arr_access mem addr args stk s = OK c s' i -> - tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n). -(*| tr_instr_Ijumptable : - 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. - -Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts : datapath) (trans : controllogic) - (externctrl : AssocMap.t (ident * controlsignal)) (fin rtrn st stk : reg) : Prop := -| tr_code_single : - forall s t, - c!pc = Some i -> - stmnts!pc = Some s -> - trans!pc = Some t -> - tr_instr fin rtrn st stk i s t -> - tr_code c pc i stmnts trans externctrl fin rtrn st stk -| tr_code_call : - forall sig fn args dst n, - c!pc = Some (RTL.Icall sig (inr fn) args dst n) -> - Z.pos n <= Int.max_unsigned -> - - (exists pc2 fn_rst fn_return fn_finish fn_params, - externctrl ! fn_rst = Some (fn, ctrl_reset) /\ - externctrl ! fn_return = Some (fn, ctrl_return) /\ - externctrl ! fn_finish = Some (fn, ctrl_finish) /\ - (forall n arg, List.nth_error args n = Some arg -> - exists r, In (r, arg) (List.combine fn_params args) /\ - externctrl ! r = Some (fn, ctrl_param n)) /\ - - stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) /\ - trans!pc = Some (state_goto st pc2) /\ - stmnts!pc2 = Some (join fn_return fn_rst dst) /\ - trans!pc2 = Some (state_wait st fn_finish n)) -> - - tr_code c pc i stmnts trans externctrl fin rtrn st stk -| tr_code_return : - forall r, - c!pc = Some (RTL.Ireturn r) -> +Ltac some_monad_inv := + multimatch goal with + | [ EQ : _ ?s = OK ?x _ _ |- context[?x] ] => monadInv EQ + | [ EQ : _ ?s = OK (?x, _) _ _ |- context[?x] ] => monadInv EQ + | [ EQ : _ ?s = OK (_, ?x) _ _ |- context[?x] ] => monadInv EQ + | [ EQ : _ ?s = OK (_, ?x) _ _ |- context[?x] ] => monadInv EQ + end. - (exists pc2, - stmnts!pc = Some (return_val fin rtrn r) /\ - trans!pc = Some (state_goto st pc2) /\ - stmnts!pc2 = Some (idle fin) /\ - trans!pc2 = Some Vskip) -> +Ltac some_incr := + saturate_incr; + multimatch goal with + | [ INCR : st_prop _ _ |- _ ] => inversion INCR + end. - tr_code c pc i stmnts trans externctrl fin rtrn st stk. -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 externctrl wf, - m = (mkmodule f.(RTL.fn_params) - data - control - f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls externctrl wf) -> - (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> - tr_code f.(RTL.fn_code) pc i data control externctrl fin rtrn st stk) -> - stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> - Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> - 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> - (st > (RTL.max_reg_function f))%positive -> - (fin > (RTL.max_reg_function f))%positive -> - (rtrn > (RTL.max_reg_function f))%positive -> - (stk > (RTL.max_reg_function f))%positive -> - (start > (RTL.max_reg_function f))%positive -> - (rst > (RTL.max_reg_function f))%positive -> - (clk > (RTL.max_reg_function f))%positive -> - tr_module f m. -Hint Constructors tr_module : htlspec. Lemma xmap_externctrl_params_combine : forall args k fn s param_pairs s' i, xmap_externctrl_params k fn args s = OK param_pairs s' i -> @@ -402,17 +418,15 @@ Proof. insterU H4. destruct H4 as [r [? ?]]. eexists. split; eauto with htlspec. - + eapply tr_code_return; eauto with htlspec. inversion Htrans. simplify. eexists. replace (st_st s'). repeat split; eauto with htlspec. - Unshelve. eauto. -Qed. + Unshelve. all: eauto. +Qed. Hint Resolve tr_code_trans : htlspec. -Hint Resolve PTree.elements_complete : htlspec. Theorem transl_module_correct : forall i f m, @@ -427,30 +441,19 @@ Proof. unfold transf_module in *. unfold stack_correct in *. - unfold_match Heqr. - destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; - destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; - destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; - crush. + destruct_match; simplify; crush. monadInv Heqr. - repeat unfold_match EQ9. monadInv EQ9. + repeat destruct_match; crush. + repeat match goal with + | [ EQ : ret _ _ = OK _ _ _ |- _ ] => monadInv EQ + | [ EQ : OK _ _ _ = OK _ _ _ |- _ ] => monadInv EQ + | [ EQ : get _ = OK _ _ _ |- _ ] => monadInv EQ + end. - monadInv EQ7. econstructor; eauto with htlspec; try lia; - try ( - multimatch goal with - | [ EQ : _ ?s = OK ?x _ _ |- context[?x] ] => monadInv EQ - | [ EQ : _ ?s = OK (?x, _) _ _ |- context[?x] ] => monadInv EQ - | [ EQ : _ ?s = OK (_, ?x) _ _ |- context[?x] ] => monadInv EQ - end; - saturate_incr; - multimatch goal with - | [ INCR : st_prop (max_state f) _ |- _ ] => inversion INCR - end; - simplify; unfold Ple in *; lia - ). - monadInv EQ6. simpl in EQ7. - monadInv EQ7. - simplify. unfold Ple in *. lia. + try solve [some_monad_inv; repeat ((simpl in *; some_monad_inv) + idtac); + some_incr; simplify; + unfold Ple in *; lia + ]. Qed. |