diff options
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 929 |
1 files changed, 419 insertions, 510 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 16bdcaf..70d35d8 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -21,19 +21,143 @@ Require Import Coq.micromega.Lia. Require compcert.backend.RTL. Require compcert.common.Errors. +Require compcert.common.Globalenvs. Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require compcert.verilog.Op. Require Import vericert.common.Vericertlib. +Require Import vericert.common.ListExtra. Require Import vericert.hls.Verilog. Require Import vericert.hls.ValueInt. Require Import vericert.hls.HTL. Require Import vericert.hls.HTLgen. 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. + +Definition externctrl_params_mapped (args params : list reg) externctrl (fn : ident) := + length args = length 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). +Hint Transparent externctrl_params_mapped : htlspec. + +Inductive tr_code (ge : RTL.genv) (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : controllogic) + (externctrl : AssocMap.t (ident * controlsignal)) (fin rtrn st stk : reg) : RTL.instruction -> Prop := +| tr_code_single : + forall i 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 ge c pc stmnts trans externctrl fin rtrn st stk i +| tr_code_call : + forall sig fn args dst n, + c!pc = Some (RTL.Icall sig (inr fn) args dst n) -> + (exists fd, find_func ge fn = Some (AST.Internal fd)) -> + 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) /\ + externctrl_params_mapped args fn_params externctrl fn /\ + Z.pos pc2 <= Int.max_unsigned /\ + stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) /\ + trans!pc = Some (state_goto st pc2) /\ + stmnts!pc2 = Some (join fn_finish fn_rst fn_return dst) /\ + trans!pc2 = Some (state_wait st fn_finish n)) -> + + tr_code ge c pc stmnts trans externctrl fin rtrn st stk (RTL.Icall sig (inr fn) args dst n) +| tr_code_return : + forall r, + c!pc = Some (RTL.Ireturn r) -> + + (exists pc2, + stmnts!pc = Some (do_return fin rtrn r) /\ + trans!pc = Some (state_goto st pc2) /\ + stmnts!pc2 = Some (idle fin) /\ + trans!pc2 = Some Vskip) -> + + tr_code ge c pc stmnts trans externctrl fin rtrn st stk (RTL.Ireturn r). +Hint Constructors tr_code : htlspec. + +Definition externctrl_ordering (externctrl : AssocMap.t (ident * controlsignal)) clk := + forall n, (exists x, externctrl!n = Some x) -> (n > clk)%positive. + +Inductive tr_module (ge : RTL.genv) (f : RTL.function) : module -> Prop := + tr_module_intro : + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls externctrl 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 externctrl None wf1 wf2 wf3 wf4) -> + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code ge f.(RTL.fn_code) pc data control externctrl fin rtrn st stk i) -> + 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 > st)%positive -> + (rtrn > fin)%positive -> + (stk > rtrn)%positive -> + (start > stk)%positive -> + (rst > start)%positive -> + (clk > rst)%positive -> + externctrl_ordering externctrl clk -> + tr_module ge 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. +Hint Unfold nonblock : htlspec. Remark bind_inversion: forall (A B: Type) (f: mon A) (g: A -> mon B) @@ -41,13 +165,7 @@ Remark bind_inversion: bind f g s1 = OK y s3 i -> exists x, exists s2, exists i1, exists i2, f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2. -Proof. - intros until i. unfold bind. destruct (f s1); intros. - discriminate. - exists a; exists s'; exists s. - destruct (g a s'); inv H. - exists s0; auto. -Qed. +Proof. unfold bind. sauto. Qed. Remark bind2_inversion: forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) @@ -55,15 +173,12 @@ Remark bind2_inversion: bind2 f g s1 = OK z s3 i -> exists x, exists y, exists s2, exists i1, exists i2, f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2. -Proof. - unfold bind2; intros. - exploit bind_inversion; eauto. - intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q. - exists x; exists y; exists s2; exists i1; exists i2; auto. -Qed. +Proof. sauto using bind_inversion. Qed. Ltac monadInv1 H := match type of H with + | ((match ?x with | _ => _ end) = OK _ _ _) => + destruct x eqn:?; try discriminate; try monadInv1 H | (OK _ _ _ = OK _ _ _) => inversion H; clear H; try subst | (Error _ _ = OK _ _ _) => @@ -98,6 +213,7 @@ Ltac monadInv1 H := Ltac monadInv H := match type of H with | (ret _ _ = OK _ _ _) => monadInv1 H + | (OK _ _ = OK _ _ _) => monadInv1 H | (error _ _ = OK _ _ _) => monadInv1 H | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H @@ -119,538 +235,331 @@ Ltac monadInv H := ((progress simpl in H) || unfold F in H); monadInv1 H 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 *) - -Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> 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_Ireturn_None : - tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z))) - (block rtrn (Vlit (ZToValue 0%Z)))) Vskip -| tr_instr_Ireturn_Some : - forall r, - tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) - (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip -| 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) (nonblock 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 trans : PTree.t stmnt) - (fin rtrn st stk : reg) : Prop := - tr_code_intro : - 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 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 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 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) -> - Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> - 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> - st = ((RTL.max_reg_function f) + 1)%positive -> - fin = ((RTL.max_reg_function f) + 2)%positive -> - rtrn = ((RTL.max_reg_function f) + 3)%positive -> - stk = ((RTL.max_reg_function f) + 4)%positive -> - start = ((RTL.max_reg_function f) + 5)%positive -> - 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. - -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. - -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. - -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. - -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. - -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. - -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. - -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. - -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. - -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. - -Ltac inv_incr := - repeat match goal with - | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); eapply create_reg_datapath_trans in H; - eapply create_reg_controllogic_trans in H1 - | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); eapply create_arr_datapath_trans in H; - eapply create_arr_controllogic_trans in H1 - | [ H: get ?s = OK _ _ _ |- _ ] => - let H1 := fresh "H" in - assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; - subst - | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H - | [ H: st_incr _ _ |- _ ] => destruct st_incr +Ltac rewrite_states := + match goal with + | [ H: ?x ?s = ?x ?s' |- _ ] => + let c1 := fresh "c" in + let c2 := fresh "c" in + learn (?x ?s) as c1; learn (?x ?s') as c2; try subst end. -Lemma collect_controllogic_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_datapath_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_freshreg_trans : - forall A f l cs cs' ci, - (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> - @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). -Proof. - induction l; intros; monadInv H0. - - trivial. - - apply H in EQ. rewrite EQ. eauto. -Qed. - -Lemma collect_declare_controllogic_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_controllogic) = s'.(st_controllogic). -Proof. - intros. eapply collect_controllogic_trans; try eassumption. - intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. -Qed. - -Lemma collect_declare_datapath_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_datapath) = s'.(st_datapath). -Proof. - intros. eapply collect_datapath_trans; try eassumption. - intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. -Qed. - -Lemma collect_declare_freshreg_trans : - forall io n l s s' i, - HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. eapply collect_freshreg_trans; try eassumption. - inversion 1. auto. -Qed. +Ltac saturate_incr := + repeat match goal with + | [INCR1 : st_prop ?s1 ?s2, INCR2 : st_prop ?s2 ?s3 |- _] => + let INCR3 := fresh "INCR" in + learn (st_trans s1 s2 s3 INCR1 INCR2) + end. -Ltac unfold_match H := - match type of H with - | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate +(** Used to solve goals that follow directly from a single monadic operation *) +Ltac intro_step := + match goal with + | [ H : _ = OK _ _ _ |- _ ] => solve [ monadInv H; simplify; eauto with htlspec ] end. -Lemma translate_eff_addressing_freshreg_trans : - forall op args s r s' i, - translate_eff_addressing op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. - -Lemma translate_comparison_freshreg_trans : - forall op args s r s' i, - translate_comparison op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_freshreg_trans : htlspec. +(** Used to transfer a result about one of the maps in the state from one + state to a latter one *) +Ltac trans_step s1 s2 := + saturate_incr; + match goal with + | [ INCR : st_prop s1 s2 |- _ ] => try solve [inversion INCR; crush]; destruct INCR + end; + solve [ + match goal with + | [ MAP_INCR : HTLgen.map_incr ?map _ _ |- (?map _) ! ?idx = _ ] => + destruct MAP_INCR with idx; try crush_trans; crush + end + ]. + +(* FIXME: monad_crush can be slow when there are a lot of intermediate states. *) + +(* Try to prove a goal about a state by first proving it for an earlier state and then transfering it to the final. *) +Ltac monad_crush := + match goal with + | [ finalstate : st, prevstate : st |- _] => + match goal with + | [ |- context f[finalstate]] => + let inter := context f[prevstate] in + try solve [ + match inter with + | context f[finalstate] => + let inter := context f[prevstate] in + solve [assert inter by intro_step; trans_step prevstate finalstate] + end + ]; + solve [assert inter by intro_step; trans_step prevstate finalstate] + end + end. -Lemma translate_comparisonu_freshreg_trans : - forall op args s r s' i, - translate_comparisonu op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparisonu_freshreg_trans : htlspec. +Ltac full_split := repeat match goal with [ |- _ /\ _ ] => split end. -Lemma translate_comparison_imm_freshreg_trans : - forall op args s r s' i n, - translate_comparison_imm op args n s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. +Ltac relevant_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. -Lemma translate_comparison_immu_freshreg_trans : - forall op args s r s' i n, - translate_comparison_immu op args n s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. -Qed. -Hint Resolve translate_comparison_immu_freshreg_trans : htlspec. +Ltac any_monad_inv := + relevant_monad_inv + + multimatch goal with + | [ EQ : _ ?s = OK _ _ _ |- _ ] => monadInv EQ + end. -Lemma translate_condition_freshreg_trans : - forall op args s r s' i, - translate_condition op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. -Qed. -Hint Resolve translate_condition_freshreg_trans : htlspec. +Ltac some_incr := + saturate_incr; + multimatch goal with + | [ INCR : st_prop _ _ |- _ ] => inversion INCR + end. -Lemma translate_instr_freshreg_trans : - forall op args s r s' i, - translate_instr op args s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). +Lemma helper__map_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. - destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. - monadInv H1. eauto with htlspec. + induction args. + - sauto. + - intros. monadInv H. sauto. Qed. -Hint Resolve translate_instr_freshreg_trans : htlspec. -Lemma translate_arr_access_freshreg_trans : - forall mem addr args st s r s' i, - translate_arr_access mem addr args st s = OK r s' i -> - s.(st_freshreg) = s'.(st_freshreg). -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. - -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. - -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. - -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. - -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. - -Lemma transf_instr_freshreg_trans : - forall fin ret st instr s v s' i, - transf_instr fin ret st instr s = OK v s' i -> - s.(st_freshreg) = s'.(st_freshreg). -Proof. - intros. destruct instr eqn:?. subst. unfold transf_instr in H. - destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. - - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. - apply declare_reg_freshreg_trans in EQ1. congruence. - - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. - apply declare_reg_freshreg_trans in EQ1. congruence. - - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. - - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. - congruence. - (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*) -Qed. -Hint Resolve transf_instr_freshreg_trans : htlspec. +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. -Lemma collect_trans_instr_freshreg_trans : - forall fin ret st l s s' i, - HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> - s.(st_freshreg) = s'.(st_freshreg). +Lemma helper__map_externctrl_params_spec : forall args n 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))). Proof. - intros. eapply collect_freshreg_trans; try eassumption. - eauto with htlspec. -Qed. - -Ltac rewrite_states := - match goal with - | [ H: ?x ?s = ?x ?s' |- _ ] => - let c1 := fresh "c" in - let c2 := fresh "c" in - remember (?x ?s) as c1; remember (?x ?s') as c2; try subst - end. - -Ltac inv_add_instr' H := - match type of H with - | ?f _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H - | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H - end; repeat unfold_match H; inversion H. - -Ltac inv_add_instr := - match goal with - | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr - | H: context[add_instr_skip _ _ _] |- _ => - inv_add_instr' H - | H: context[add_instr_skip _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_instr _ _ _ _] |- _ => - inv_add_instr' H - | H: context[add_instr _ _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_branch_instr _ _ _ _ _] |- _ => - inv_add_instr' H - | H: context[add_branch_instr _ _ _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - | H: context[add_node_skip _ _ _] |- _ => - inv_add_instr' H - | H: context[add_node_skip _ _] |- _ => - monadInv H; inv_incr; inv_add_instr - end. - -Ltac destruct_optional := - match goal with H: option ?r |- _ => destruct H end. + induction args. + - sauto use: nth_error_nil. + - intros. + monadInv H. + destruct n; simplify. + + destruct (split x0). simpl. + exists x. crush. monad_crush. + + destruct (IHargs n _ _ _ _ _ _ EQ1 ltac:(lia)). + destruct (split _). simpl in *. + eexists. replace (S (n + k))%nat with (n + S k)%nat by lia. + eassumption. + Qed. + +Lemma map_externctrl_params_spec : forall args n 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. +Hint Resolve map_externctrl_params_spec : htlspec. Lemma iter_expand_instr_spec : - forall l fin rtrn stack s s' i x c, - HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> + 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 -> list_norepet (List.map fst l) -> (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> - (forall pc instr, In (pc, instr) l -> - c!pc = Some instr -> - tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). + (forall pc instr, In (pc, instr) l -> c!pc = Some instr -> + tr_code (Globalenvs.Genv.globalenv prog) c pc s'.(st_datapath) s'.(st_controllogic) s'.(st_externctrl) fin rtrn s'.(st_st) stack instr). Proof. - induction l; simpl; intros; try contradiction. - destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. + (** Used to solve the simpler cases of tr_code: those involving tr_instr *) + Ltac tr_code_simple_tac := + eapply tr_code_single; + match goal with + | [ H : (?pc, _) = (?pc, ?instr) \/ In (?pc, ?instr) _ |- _ ] => + inversion H; + do 2 + match goal with + | [ H' : In (_, _) _ |- _ ] => solve [ eapply in_map with (f:=fst) in H'; contradiction ] + | [ H' : (pc, _) = (pc, instr) |- _ ] => inversion H' + end; + simplify; eauto with htlspec + end; + monad_crush. + + induction l; crush. + destruct a as [pc1 instr1]; simplify. inv H0. monadInv H. destruct (peq pc pc1). - subst. - destruct instr1 eqn:?; try discriminate; - try destruct_optional; inv_add_instr; econstructor; try assumption. - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. - apply Z.leb_le. assumption. - eapply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. - econstructor. apply Z.leb_le; assumption. - apply EQ1. eapply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply Z.leb_le; assumption. - apply EQ1. eapply in_map with (f := fst) in H14. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct H2. - * inversion H2. - replace (st_st s2) with (st_st s0) by congruence. - econstructor. apply Z.leb_le; assumption. - eauto with htlspec. - * apply in_map with (f := fst) in H2. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct H2. - * inversion H2. - replace (st_st s2) with (st_st s0) by congruence. - econstructor; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN). - eauto with htlspec. - * apply in_map with (f := fst) in H2. contradiction. - - (*+ destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. - + inversion H2. - * inversion H14. constructor. congruence. - * apply in_map with (f := fst) in H14. contradiction. - *) - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. - + inversion H2. - * inversion H9. - replace (st_st s2) with (st_st s0) by congruence. - eauto with htlspec. - * apply in_map with (f := fst) in H9. contradiction. - - - eapply IHl. apply EQ0. assumption. - destruct H2. inversion H2. subst. contradiction. - intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption. + destruct instr1 eqn:instr_eq; + repeat destruct_match; try discriminate; try monadInv1 EQ. + + (* Inop *) tr_code_simple_tac. + + (* Iop *) tr_code_simple_tac. + + (* Iload *) tr_code_simple_tac. + + (* Istore *) tr_code_simple_tac. + + (* Icall *) + inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. + inversion H. + + eapply tr_code_call; eauto; crush. + + 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. + 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. + 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. + monad_crush. + + (* Icond *) tr_code_simple_tac. + + (* Ireturn *) + inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. + inversion H. + eapply tr_code_return; crush; eexists; simplify; monad_crush. + - eapply IHl; eauto. + intuition crush. Qed. 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 -> - y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). +Lemma map_incr_some : forall {A} map (s s' : st) idx (x : A), + (map s) ! idx = Some x -> + map_incr map s s' -> + (map s') ! idx = Some x. +Proof. intros * ? Hincr. destruct Hincr with idx; crush. Qed. +Hint Resolve map_incr_some : htlspec. + +Lemma tr_code_trans : forall ge c pc instr fin rtrn stack s s', + tr_code ge c pc (st_datapath s) (st_controllogic s) (st_externctrl s) fin rtrn (st_st s) stack instr -> + st_prop s s' -> + tr_code ge c pc (st_datapath s') (st_controllogic s') (st_externctrl s') fin rtrn (st_st s') stack instr. Proof. - inversion 1; split; auto. + intros * Htr Htrans. + destruct Htr. + + eapply tr_code_single. + * trans_step s s'. + * inversion Htrans. + destruct H6 with pc. crush. + replace ((st_datapath s') ! pc). + eassumption. + * inversion Htrans. + destruct H7 with pc. crush. + replace ((st_controllogic s') ! pc). + eassumption. + * inversion Htrans. crush. + + eapply tr_code_call; eauto with htlspec. + simplify. + 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. + + eapply tr_code_return; eauto with htlspec. + inversion Htrans. + simplify. eexists. + replace (st_st s'). + repeat split; eauto with htlspec. + Unshelve. all: eauto. Qed. +Hint Resolve tr_code_trans : htlspec. -Lemma create_reg_inv : forall a b s r s' i, - create_reg a b s = OK r s' i -> - r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). +Lemma declare_params_freshreg_trans : forall params s s' x i, + declare_params params s = OK x s' i -> + st_freshreg s = st_freshreg s'. Proof. - inversion 1; auto. + induction params; unfold declare_params in *; intros * H. + - inv H. trivial. + - monadInv H. + transitivity (st_freshreg s0). + + monadInv EQ. auto. + + eauto. Qed. +Hint Resolve declare_params_freshreg_trans : htlspec. + +Lemma declare_params_externctrl_trans : forall params s s' x i, + declare_params params s = OK x s' i -> + st_externctrl s = st_externctrl s'. +Proof. + induction params; unfold declare_params in *; intros * H. + - inv H. trivial. + - monadInv H. + transitivity (st_externctrl s0). + + monadInv EQ. auto. + + eauto. +Qed. +Hint Resolve declare_params_freshreg_trans : htlspec. Theorem transl_module_correct : - forall f m, - transl_module f = Errors.OK m -> tr_module f m. + forall p f m, + transl_module p f = Errors.OK m -> tr_module (Globalenvs.Genv.globalenv p) f m. Proof. - intros until m. - unfold transl_module. - unfold run_mon. - destruct (transf_module f (max_state f)) eqn:?; try discriminate. - intros. inv H. + intros * H. + unfold transl_module in *. + unfold run_mon in *. + unfold_match H. + inv H. inversion s; subst. unfold transf_module in *. unfold stack_correct in *. - 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; - monadInv Heqr. - - repeat unfold_match EQ9. monadInv EQ9. - - (* TODO: We should be able to fold this into the automation. *) - pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. inv STK_LEN. inv H5. - pose proof (create_reg_inv _ _ _ _ _ _ EQ) as FIN_VAL. inv FIN_VAL. - pose proof (create_reg_inv _ _ _ _ _ _ EQ1) as RET_VAL. inv RET_VAL. - destruct x3. destruct x4. - pose proof (collect_trans_instr_freshreg_trans _ _ _ _ _ _ _ EQ2) as TR_INSTR. - pose proof (collect_declare_freshreg_trans _ _ _ _ _ _ EQ3) as TR_DEC. - pose proof (create_reg_inv _ _ _ _ _ _ EQ4) as START_VAL. inv START_VAL. - pose proof (create_reg_inv _ _ _ _ _ _ EQ5) as RESET_VAL. inv RESET_VAL. - pose proof (create_reg_inv _ _ _ _ _ _ EQ6) as CLK_VAL. inv CLK_VAL. - rewrite H9 in *. rewrite H8 in *. replace (st_freshreg s4) with (st_freshreg s2) in * by congruence. - rewrite H6 in *. rewrite H7 in *. rewrite H5 in *. simpl in *. - inv_incr. - econstructor; simpl; auto; try lia. - intros. - assert (EQ3D := EQ3). - apply collect_declare_datapath_trans in EQ3. - apply collect_declare_controllogic_trans in EQ3D. - replace (st_controllogic s10) with (st_controllogic s3) by congruence. - 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. + destruct_match; simplify; crush. + monadInv Heqr. + + repeat destruct_match; crush. + repeat match goal with + | [ EQ : ret _ _ = OK _ _ _ |- _ ] => monadInv EQ + | [ EQ : OK _ _ _ = OK _ _ _ |- _ ] => monadInv EQ + | [ EQ : get _ = OK _ _ _ |- _ ] => monadInv EQ + end. + + econstructor; + eauto with htlspec; + try solve [ repeat relevant_monad_inv; crush ]. + - auto_apply declare_params_freshreg_trans. + replace (st_st s'). + monadInv EQ1. + inversion INCR. + repeat match goal with + | [ H : context[st_freshreg (max_state _)] |- _ ] => unfold max_state in H; simpl in H + end. + crush. + - assert (forall n, (st_externctrl (max_state f)) ! n = None) by (simplify; eauto using AssocMap.gempty). + assert (forall n, (st_externctrl s0) ! n = None) by (erewrite <- (declare_params_externctrl_trans); eauto). + assert (forall n, (st_externctrl s1) ! n = None) by (any_monad_inv; simplify; auto). + assert (forall n, (st_externctrl s2) ! n = None) by (any_monad_inv; simplify; auto). + assert (forall n, (st_externctrl s3) ! n = None) by (any_monad_inv; simplify; auto). + assert (forall n, (st_externctrl s4) ! n = None) by (any_monad_inv; simplify; auto). + assert (forall n, (st_externctrl s5) ! n = None) by (any_monad_inv; simplify; auto). + + assert (forall n, (st_externctrl s6) ! n = None) by (any_monad_inv; simplify; auto). + assert ((st_freshreg s6) > x6)%positive by (relevant_monad_inv; simplify; crush). + + unfold externctrl_ordering. intros. + repeat match goal with + | [ H: forall (_ : positive), _ |- _ ] => specialize (H n) + end. + + enough (n >= st_freshreg s6)%positive by lia. + solve [ some_incr; auto ]. Qed. |