From ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 30 Aug 2020 14:03:40 +0100 Subject: Add RTLBlock intermediate language --- src/hls/HTLgenspec.v | 641 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 641 insertions(+) create mode 100644 src/hls/HTLgenspec.v (limited to 'src/hls/HTLgenspec.v') diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v new file mode 100644 index 0000000..541f9fa --- /dev/null +++ b/src/hls/HTLgenspec.v @@ -0,0 +1,641 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert Require RTL Op Maps Errors. +From compcert Require Import Maps Integers. +From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap. +Require Import Lia. + +Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. +Hint Resolve Maps.PTree.elements_correct : htlspec. + +Remark bind_inversion: + forall (A B: Type) (f: mon A) (g: A -> mon B) + (y: B) (s1 s3: st) (i: st_incr s1 s3), + 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. + +Remark bind2_inversion: + forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) + (z: C) (s1 s3: st) (i: st_incr s1 s3), + 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. + +Ltac monadInv1 H := + match type of H with + | (OK _ _ _ = OK _ _ _) => + inversion H; clear H; try subst + | (Error _ _ = OK _ _ _) => + discriminate + | (ret _ _ = OK _ _ _) => + inversion H; clear H; try subst + | (error _ _ = OK _ _ _) => + discriminate + | (bind ?F ?G ?S = OK ?X ?S' ?I) => + let x := fresh "x" in ( + let s := fresh "s" in ( + let i1 := fresh "INCR" in ( + let i2 := fresh "INCR" in ( + let EQ1 := fresh "EQ" in ( + let EQ2 := fresh "EQ" in ( + destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]]; + clear H; + try (monadInv1 EQ2))))))) + | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => + let x1 := fresh "x" in ( + let x2 := fresh "x" in ( + let s := fresh "s" in ( + let i1 := fresh "INCR" in ( + let i2 := fresh "INCR" in ( + let EQ1 := fresh "EQ" in ( + let EQ2 := fresh "EQ" in ( + destruct (bind2_inversion _ _ _ F G X S S' I H) as [x1 [x2 [s [i1 [i2 [EQ1 EQ2]]]]]]; + clear H; + try (monadInv1 EQ2)))))))) + end. + +Ltac monadInv H := + match type of H with + | (ret _ _ = 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 + | (?F _ _ _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ = OK _ _ _) => + ((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 wf, + m = (mkmodule f.(RTL.fn_params) + data + control + f.(RTL.fn_entrypoint) + st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> + (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 + 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 unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + 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. + +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. + +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. + +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. + +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. + +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). +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. + +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 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). +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. + +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 -> + 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). +Proof. + induction l; simpl; intros; try contradiction. + destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. + 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. +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)). +Proof. + inversion 1; split; auto. +Qed. + +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)). +Proof. + inversion 1; auto. +Qed. + +Theorem transl_module_correct : + forall f m, + transl_module f = Errors.OK m -> tr_module 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. + 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