diff options
| -rw-r--r-- | src/hls/HTLgenproof.v | 114 | ||||
| -rw-r--r-- | src/hls/HTLgenspec.v | 50 |
2 files changed, 94 insertions, 70 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index db564af..b4f2a05 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -120,14 +120,14 @@ Definition has_externctrl (caller : HTL.module) (current_id : HTL.ident) (ret rs (HTL.mod_externctrl caller)!rst = Some (current_id, HTL.ctrl_reset) /\ (HTL.mod_externctrl caller)!fin = Some (current_id, HTL.ctrl_finish). -Inductive match_frames (current_id : HTL.ident) (mem : Memory.mem) +Inductive match_frames (ge : RTL.genv) (current_id : HTL.ident) (mem : Memory.mem) : (list RTL.stackframe) -> (list HTL.stackframe) -> Prop := | match_frames_nil : - match_frames current_id mem nil nil + match_frames ge current_id mem nil nil | match_frames_cons : forall dst f sp sp' rs mid m pc st asr asa rtl_tl htl_tl ret rst fin (MASSOC : match_assocmaps f rs asr) - (TF : tr_module f m) + (TF : tr_module ge f m) (MARR : match_arrs m f sp mem asa) (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) (RSBP : reg_stack_based_pointers sp' rs) @@ -137,40 +137,43 @@ Inductive match_frames (current_id : HTL.ident) (mem : Memory.mem) (EXTERN_CALLER : has_externctrl m current_id ret rst fin) (JOIN_CTRL : (HTL.mod_controllogic m)!st = Some (state_wait (HTL.mod_st m) fin pc)) (JOIN_DATA : (HTL.mod_datapath m)!st = Some (join ret rst dst)) - (TAILS : match_frames mid mem rtl_tl htl_tl) + (TAILS : match_frames ge mid mem rtl_tl htl_tl) (DST : Ple dst (RTL.max_reg_function f)) (PC : (Z.pos pc <= Int.max_unsigned)), - match_frames current_id mem + match_frames ge current_id mem ((RTL.Stackframe dst f sp pc rs) :: rtl_tl) ((HTL.Stackframe mid m st asr asa) :: htl_tl). -Inductive match_states : RTL.state -> HTL.state -> Prop := +Inductive match_states (ge : RTL.genv) : RTL.state -> HTL.state -> Prop := | match_state : forall asa asr sf f sp sp' rs mem mid m st res (MASSOC : match_assocmaps f rs asr) - (TF : tr_module f m) + (TF : tr_module ge f m) (WF : state_st_wf m (HTL.State res mid m st asr asa)) - (MF : match_frames mid mem sf res) + (MF : match_frames ge mid mem sf res) (MARR : match_arrs m f sp mem asa) (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) (RSBP : reg_stack_based_pointers sp' rs) (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem) (CONST : match_constants m asr), - match_states (RTL.State sf f sp st rs mem) + match_states ge + (RTL.State sf f sp st rs mem) (HTL.State res mid m st asr asa) | match_returnstate : forall v v' rtl_stk htl_stk mem mid - (MF : match_frames mid mem rtl_stk htl_stk) + (MF : match_frames ge mid mem rtl_stk htl_stk) (MV : val_value_lessdef v v') (NP : not_pointer v), - match_states (RTL.Returnstate rtl_stk v mem) + match_states ge + (RTL.Returnstate rtl_stk v mem) (HTL.Returnstate htl_stk mid v') | match_call : forall f m rtl_args htl_args mid mem rtl_stk htl_stk - (TF : tr_module f m) - (MF : match_frames mid mem rtl_stk htl_stk) + (TF : tr_module ge f m) + (MF : match_frames ge mid mem rtl_stk htl_stk) (MARGS : list_forall2 val_value_lessdef rtl_args htl_args), - match_states (RTL.Callstate rtl_stk (AST.Internal f) rtl_args mem) + match_states ge + (RTL.Callstate rtl_stk (AST.Internal f) rtl_args mem) (HTL.Callstate htl_stk mid m htl_args). Hint Constructors match_states : htlproof. @@ -351,14 +354,14 @@ Proof. intros. inversion H. trivial. Qed. Ltac inv_state := match goal with - MSTATE : match_states _ _ |- _ => + MSTATE : match_states _ _ _ |- _ => inversion MSTATE; - try match goal with - TF : tr_module _ _ |- _ => + match goal with + TF : tr_module _ _ _ |- _ => inversion TF; match goal with TC : forall _ _, - Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _ _, + Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _ _ _, H : Maps.PTree.get _ _ = Some _ |- _ => apply TC in H; inversion H; try match goal with @@ -420,6 +423,9 @@ Section CORRECTNESS. Variable prog : RTL.program. Variable tprog : HTL.program. + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. + Hypothesis TRANSL : match_prog prog tprog. (** This is assumed to be guaranteed by a check before this stage which @@ -428,17 +434,17 @@ Section CORRECTNESS. *) Axiom no_pointer_return : forall (rs : RTL.regset) r s (f : RTL.function) sp pc rs mem f S, (RTL.fn_code f) ! pc = Some (RTL.Ireturn (Some r)) -> - match_states (RTL.State s f sp pc rs mem) S -> + match_states ge (RTL.State s f sp pc rs mem) S -> (not_pointer rs !! r). (** The following admitted lemmas should be provable *) Axiom no_stack_functions : forall f sp rs mem st rtl_stk S, - match_states (RTL.State rtl_stk f sp st rs mem) S -> + match_states ge (RTL.State rtl_stk f sp st rs mem) S -> (RTL.fn_stacksize f) = 0 \/ rtl_stk = nil. (** The following admitted lemmas should be provable *) Axiom no_stack_calls : forall f mem args rtl_stk S, - match_states (RTL.Callstate rtl_stk (AST.Internal f) args mem) S -> + match_states ge (RTL.Callstate rtl_stk (AST.Internal f) args mem) S -> (RTL.fn_stacksize f) = 0 \/ rtl_stk = nil. Lemma mem_free_zero : forall mem blk, Mem.free mem blk 0 0 = Some mem. @@ -456,9 +462,6 @@ Section CORRECTNESS. Linking.match_program (fun cu f tf => transl_fundef (AST.prog_main prog) f = Errors.OK tf) eq prog tprog. Proof. intros; apply match_prog_matches; assumption. Qed. - Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. - Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. - Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. @@ -688,7 +691,7 @@ Section CORRECTNESS. Lemma eval_cond_correct : forall stk f sp pc rs mid m res ml st asr asa e b f' s s' args i cond, - match_states (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> + match_states ge (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> (forall v, In v args -> Ple v (RTL.max_reg_function f)) -> Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> translate_condition cond args s = OK e s' i -> @@ -819,7 +822,7 @@ Section CORRECTNESS. Lemma eval_cond_correct' : forall e stk f sp pc rs m res mid ml st asr asa v f' s s' args i cond, - match_states (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> + match_states ge (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> (forall v, In v args -> Ple v (RTL.max_reg_function f)) -> Values.Val.of_optbool None = v -> translate_condition cond args s = OK e s' i -> @@ -832,7 +835,7 @@ Section CORRECTNESS. Lemma eval_correct_Oshrximm : forall s sp rs m v e asr asa f f' stk s' i pc res0 pc' args res mid ml st n, - match_states (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> + match_states ge (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> (RTL.fn_code f) ! pc = Some (RTL.Iop (Op.Oshrximm n) args res0 pc') -> Op.eval_operation ge sp (Op.Oshrximm n) (List.map (fun r : BinNums.positive => @@ -894,7 +897,7 @@ Section CORRECTNESS. Lemma eval_correct : forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res mid ml st , - match_states (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> + match_states ge (RTL.State stk f sp pc rs m) (HTL.State res mid ml st asr asa) -> (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> Op.eval_operation ge sp op (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> @@ -1166,9 +1169,9 @@ Section CORRECTNESS. (rs : RTL.regset) (m : mem) (pc' : RTL.node), (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states ge (RTL.State s f sp pc' rs m) R2. Proof. intros * H R1 MSTATE. inv_state. @@ -1196,10 +1199,10 @@ Section CORRECTNESS. (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. + match_states ge (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. Proof. intros * H H0 R1 MSTATE. inv_state. inv MARR. @@ -1251,10 +1254,10 @@ Section CORRECTNESS. (m : mem) (m' : Mem.mem') (stk : Values.block), Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> forall R1 : HTL.state, - match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> + match_states ge (RTL.Callstate s (AST.Internal f) args m) R1 -> exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states + match_states ge (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) (RTL.init_regs args (RTL.fn_params f)) m') R2. Proof. @@ -1293,6 +1296,17 @@ Section CORRECTNESS. Admitted. Hint Resolve transl_callstate_correct : htlproof. + Lemma only_internal_calls : forall fd fn rs, + RTL.find_function ge (inr fn) rs = Some fd -> + (exists f : RTL.function, rtl_find_func ge fn = Some (AST.Internal f)) -> + (exists f, fd = AST.Internal f). + Proof. + intros * ? [? ?]. + unfold rtl_find_func in *. + unfold RTL.find_function in *. + destruct (Genv.find_symbol ge fn); try discriminate. + exists x. crush. + Qed. Lemma return_val_exec_spec : forall f or asr asa, Verilog.expr_runp f asr asa (return_val or) (match or with @@ -1308,10 +1322,10 @@ Section CORRECTNESS. (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> forall R1 : HTL.state, - match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> + match_states ge (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. + match_states ge (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. Proof. intros * H H0 * MSTATE. inv_state. @@ -1371,10 +1385,10 @@ Section CORRECTNESS. forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) (R1 : HTL.state), - match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> + match_states ge (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. + match_states ge (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. Proof. intros * MSTATE. inv MSTATE. @@ -1527,10 +1541,10 @@ Section CORRECTNESS. Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> Mem.loadv chunk m a = Some v -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ - match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. + match_states ge (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. Proof. intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. inv_state. @@ -1934,9 +1948,9 @@ Section CORRECTNESS. Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states ge (RTL.State s f sp pc' rs m') R2. Proof. intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. inv_state. inv_arr_access. @@ -2744,9 +2758,9 @@ Section CORRECTNESS. Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> pc' = (if b then ifso else ifnot) -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states ge (RTL.State s f sp pc' rs m) R2. Proof. intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. inv_state. @@ -2807,9 +2821,9 @@ Section CORRECTNESS. Registers.Regmap.get arg rs = Values.Vint n -> list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> forall R1 : HTL.state, - match_states (RTL.State s f sp pc rs m) R1 -> + match_states ge (RTL.State s f sp pc rs m) R1 -> exists R2 : HTL.state, - Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states ge (RTL.State s f sp pc' rs m) R2. Proof. intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. @@ -2851,7 +2865,7 @@ Section CORRECTNESS. forall s1 : Smallstep.state (RTL.semantics prog), Smallstep.initial_state (RTL.semantics prog) s1 -> exists s2 : Smallstep.state (HTL.semantics tprog), - Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. + Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states ge s1 s2. Proof. induction 1. destruct TRANSL. unfold main_is_internal in H4. @@ -2889,7 +2903,7 @@ Section CORRECTNESS. forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog)) (r : Integers.Int.int), - match_states s1 s2 -> + match_states ge s1 s2 -> Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r. Proof. @@ -2902,8 +2916,8 @@ Section CORRECTNESS. forall (S1 : RTL.state) t S2, RTL.step ge S1 t S2 -> forall (R1 : HTL.state), - match_states S1 R1 -> - exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. + match_states ge S1 R1 -> + exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states ge S2 R2. Proof. induction 1; try (eauto with htlproof; intros; inv_state). Admitted. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index d02aff6..0c15f53 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -21,6 +21,7 @@ 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. @@ -74,7 +75,13 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt - 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) (stmnts : datapath) (trans : controllogic) +Definition rtl_find_func (ge : RTL.genv) (symb : AST.ident) := + match Globalenvs.Genv.find_symbol ge symb with + | None => None + | Some b => Globalenvs.Genv.find_funct_ptr ge b + end. + +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, @@ -82,10 +89,11 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : c stmnts!pc = Some s -> trans!pc = Some t -> tr_instr fin rtrn st stk i s t -> - tr_code c pc stmnts trans externctrl fin rtrn st stk i + 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, rtl_find_func ge fn = Some (AST.Internal fd)) -> Z.pos n <= Int.max_unsigned -> (exists pc2 fn_rst fn_return fn_finish fn_params, @@ -101,7 +109,7 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : c stmnts!pc2 = Some (join fn_return fn_rst dst) /\ trans!pc2 = Some (state_wait st fn_finish n)) -> - tr_code c pc stmnts trans externctrl fin rtrn st stk (RTL.Icall sig (inr fn) args dst 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) -> @@ -112,10 +120,10 @@ Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts : datapath) (trans : c stmnts!pc2 = Some (idle fin) /\ trans!pc2 = Some Vskip) -> - tr_code c pc stmnts trans externctrl fin rtrn st stk (RTL.Ireturn r). + tr_code ge c pc stmnts trans externctrl fin rtrn st stk (RTL.Ireturn r). Hint Constructors tr_code : htlspec. -Inductive tr_module (f : RTL.function) : module -> Prop := +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 wf, m = (mkmodule f.(RTL.fn_params) @@ -124,7 +132,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := 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 data control externctrl fin rtrn st stk 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 -> @@ -136,7 +144,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := (start > stk)%positive -> (rst > start)%positive -> (clk > rst)%positive -> - tr_module f m. + tr_module ge f m. Hint Constructors tr_module : htlspec. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. @@ -339,12 +347,12 @@ 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, + forall l ge 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 s'.(st_datapath) s'.(st_controllogic) s'.(st_externctrl) fin rtrn s'.(st_st) stack instr). + tr_code ge c pc s'.(st_datapath) s'.(st_controllogic) s'.(st_externctrl) fin rtrn s'.(st_st) stack instr). Proof. (** Used to solve the simpler cases of tr_code: those involving tr_instr *) Ltac tr_code_simple_tac := @@ -375,7 +383,9 @@ Proof. inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. inversion H. - eapply tr_code_call; crush. + assert (exists fd, rtl_find_func ge i0 = Some (AST.Internal fd)) by admit. + + eapply tr_code_call; eauto; crush. destruct (map_externctrl_params_combine _ _ _ _ _ _ EQ1) as [? [? ?]]; subst. repeat (eapply ex_intro). @@ -388,9 +398,9 @@ Proof. inversion H2; try solve [eapply in_map with (f:=fst) in H; contradiction]. inversion H. eapply tr_code_return; crush; eexists; monad_crush. - - clear EQ. (* EQ is very big and sauto gets lost *) - sauto q: on. -Qed. + - eapply IHl; eauto. + intuition crush. +Admitted. Hint Resolve iter_expand_instr_spec : htlspec. Lemma map_incr_some : forall {A} map (s s' : st) idx (x : A), @@ -400,10 +410,10 @@ Lemma map_incr_some : forall {A} map (s s' : st) idx (x : A), Proof. intros * ? Hincr. destruct Hincr with idx; crush. Qed. Hint Resolve map_incr_some : htlspec. -Lemma tr_code_trans : forall c pc instr fin rtrn stack s s', - tr_code c pc (st_datapath s) (st_controllogic s) (st_externctrl s) fin rtrn (st_st s) stack instr -> +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 c pc (st_datapath s') (st_controllogic s') (st_externctrl s') fin rtrn (st_st s') stack instr. + tr_code ge c pc (st_datapath s') (st_controllogic s') (st_externctrl s') fin rtrn (st_st s') stack instr. Proof. intros * Htr Htrans. destruct Htr. @@ -423,8 +433,8 @@ Proof. repeat (eapply ex_intro). repeat split; try (eapply map_incr_some; inversion Htrans; eauto with htlspec); try eauto with htlspec. intros. - insterU H4. - destruct H4 as [r [? ?]]. + insterU H5. + destruct H5 as [r [? ?]]. eexists. split; eauto with htlspec. + eapply tr_code_return; eauto with htlspec. inversion Htrans. @@ -437,8 +447,8 @@ Qed. Hint Resolve tr_code_trans : htlspec. Theorem transl_module_correct : - forall i f m, - transl_module i f = Errors.OK m -> tr_module f m. + forall i f m ge, + transl_module i f = Errors.OK m -> tr_module ge f m. Proof. intros * H. unfold transl_module in *. |