Require Import String.
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Smallstep.
Require Csyntax.
Require Csem.
Require Cstrategy.
Require Cexec.
Require Clight.
Require Csharpminor.
Require Cminor.
Require CminorSel.
Require RTL.
Require LTL.
Require Linear.
Require Mach.
Require Asm.
Require Initializers.
Require SimplExpr.
Require SimplLocals.
Require Cshmgen.
Require Cminorgen.
Require Selection.
Require RTLgen.
Require Renumber.
Require Constprop.
Require CSE.
Require Deadcode.
Require Allocation.
Require Tunneling.
Require Linearize.
Require CleanupLabels.
Require Stacking.
Require Asmgen.
Require SimplExprproof.
Require SimplLocalsproof.
Require Cshmgenproof.
Require Cminorgenproof.
Require Selectionproof.
Require RTLgenproof.
Require Renumberproof.
Require Constpropproof.
Require CSEproof.
Require Deadcodeproof.
Require Allocproof.
Require Tunnelingproof.
Require Linearizeproof.
Require CleanupLabelsproof.
Require Stackingproof.
Require Asmgenproof.

Parameter print_Clight: Clight.program -> unit.
Parameter print_Cminor: Cminor.program -> unit.
Parameter print_RTL: Z -> RTL.program -> unit.
Parameter print_LTL: LTL.program -> unit.
Parameter print_Linear: Linear.program -> unit.
Parameter print_Mach: Mach.program -> unit.

Open Local Scope string_scope.

Composing the translation passes

Definition apply_total (A B: Type) (x: res A) (f: A -> B) : res B :=
  match x with Error msg => Error msg | OK x1 => OK (f x1) end.

Definition apply_partial (A B: Type)
                         (x: res A) (f: A -> res B) : res B :=
  match x with Error msg => Error msg | OK x1 => f x1 end.

Notation "a @@@ b" :=
   (apply_partial _ _ a b) (at level 50, left associativity).
Notation "a @@ b" :=
   (apply_total _ _ a b) (at level 50, left associativity).

Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
  let unused := printer prog in prog.

Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.


Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
   OK f
   @@ print (print_RTL 0)
   @@ print (print_RTL 2)
   @@ time "Renumbering" Renumber.transf_program
   @@ print (print_RTL 3)
   @@ time "Constant propagation" Constprop.transf_program
   @@ print (print_RTL 4)
   @@ time "Renumbering" Renumber.transf_program
   @@ print (print_RTL 5)
  @@@ time "CSE" CSE.transf_program
   @@ print (print_RTL 6)
  @@@ time "Dead code" Deadcode.transf_program
   @@ print (print_RTL 7)
  @@@ time "Register allocation" Allocation.transf_program
   @@ print print_LTL
   @@ time "Branch tunneling" Tunneling.tunnel_program
  @@@ Linearize.transf_program
   @@ time "Label cleanup" CleanupLabels.transf_program
  @@@ time "Mach generation" Stacking.transf_program
   @@ print print_Mach
  @@@ time "Asm generation" Asmgen.transf_program.

Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
   OK p
   @@ print print_Cminor
  @@@ time "Instruction selection" Selection.sel_program
  @@@ time "RTL generation" RTLgen.transl_program
  @@@ transf_rtl_program.


Definition transf_clight_program (p: Clight.program) : res Asm.program :=
  OK p
   @@ print print_Clight
  @@@ time "Simplification of locals" SimplLocals.transf_program
  @@@ time "C#minor generation" Cshmgen.transl_program
  @@@ time "Cminor generation" Cminorgen.transl_program
  @@@ transf_cminor_program.
  
Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
  OK p
  @@@ time "Clight generation" SimplExpr.transl_program
  @@@ transf_clight_program.


Definition transl_init := Initializers.transl_init.
Definition cexec_do_step := Cexec.do_step.


Lemma print_identity:
  forall (A: Type) (printer: A -> unit) (prog: A),
  print printer prog = prog.

Lemma compose_print_identity:
  forall (A: Type) (x: res A) (f: A -> unit),
  x @@ print f = x.

Semantic preservation

Lemma Cminor_eval_expr_determ:
  forall ge sp e m a v1,
    Cminor.eval_expr ge sp e m a v1 ->
    forall v2,
      Cminor.eval_expr ge sp e m a v2 ->
      v1 = v2.

Lemma Cminor_eval_exprlist_determ:
  forall ge sp e m a v1,
    Cminor.eval_exprlist ge sp e m a v1 ->
    forall v2,
      Cminor.eval_exprlist ge sp e m a v2 ->
      v1 = v2.

Ltac detcm :=
  match goal with
      A : ?a = ?b, B : ?a = ?c |- _ => rewrite A in B; inv B
    | A: Cminor.eval_expr ?ge ?sp ?e ?m ?a ?v1,
         B: Cminor.eval_expr ?ge ?sp ?e ?m ?a ?v2 |- _ =>
      rewrite (Cminor_eval_expr_determ ge sp e m a _ A _ B) in *; clear A B
    | A: Cminor.eval_exprlist ?ge ?sp ?e ?m ?a ?v1,
         B: Cminor.eval_exprlist ?ge ?sp ?e ?m ?a ?v2 |- _ =>
      rewrite (Cminor_eval_exprlist_determ ge sp e m a _ A _ B) in *; clear A B
  end.




Ltac detlin :=
  match goal with
      A : ?a = ?b, B : ?a = ?c |- _ => rewrite A in B; inv B
    | H: Events.external_call' _ _ _ _ _ _ _ |- _ => inv H
    | H: Events.external_call _ _ _ _ _ _ _,
         H': Events.external_call _ _ _ _ _ _ _ |- _ =>
      exploit (Events.external_call_determ); [eexact H'|eexact H|];
      clear H H'
  end.

Definition needed_stackspace_exact ns tp :=
  forall p' (COMP: Asmgen.transf_program p' = OK tp)
    f tf
    (STACK: Stacking.transf_function f = OK tf)
    b
    (GFF: Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv (V:=unit) p') b =
          Some (Internal tf)),
    Linear.fn_stacksize f + 8* Z.of_nat (ns (Linear.fn_id f)) = Mach.fn_stacksize tf.


Definition oracle_ns (p: Asm.program) : (ident -> nat) :=
  fold_right (fun (elt: ident * globdef Asm.fundef unit)
                (acc: (ident -> nat)) =>
                let ns: ident -> nat := acc in
                match snd elt with
                  Gfun (Internal f) =>
                  (fun i => if peq i (Asm.fn_id f) then
                           NPeano.div (Asm.fn_nbextra f) 8
                         else ns i)
                | _ => ns
                end
             ) (fun _ => O) (prog_defs p).

Definition cond_globalenv (tp:Asm.program) :=
  list_norepet (prog_defs_names tp) /\
  forall b1 f1 b2 f2,
    Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv tp) b1 = Some (Internal f1) ->
    Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv tp) b2 = Some (Internal f2) ->
    Asm.fn_id f1 = Asm.fn_id f2 ->
    Asm.fn_nbextra f1 = Asm.fn_nbextra f2 /\
    list_length_z (Asm.fn_code f1) = list_length_z (Asm.fn_code f2).
    
    
Lemma in_find_funct:
  forall {F: Type} tp
         (lnr: list_norepet (prog_defs_names tp))
    i1 (f1: F)
    (IN : In (i1, Gfun (Internal f1)) (prog_defs (V:=unit) tp)),
  exists b, Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv tp) b =
       Some (Internal f1).

Lemma oracle_ns_correct:
  forall tp
    (Cond_Ge: cond_globalenv tp),
    needed_stackspace_exact (oracle_ns tp) tp.

Definition oracle_sg (p: Asm.program) : (ident -> Z) :=
  fold_right (fun (elt: ident * globdef Asm.fundef unit)
                (acc: (ident -> Z)) =>
                let sg: ident -> Z := acc in
                match snd elt with
                  Gfun (Internal f) =>
                  (fun i => if peq i (Asm.fn_id f) then
                            list_length_z (Asm.fn_code f) + 1
                         else sg i)
                | _ => sg
                end
             ) (fun _ => 1) (prog_defs p).

Lemma oracle_sg_correct_1:
  forall p' tp
    (Cond_Ge: cond_globalenv tp)
    (AG: Asmgen.transf_program p' = OK tp),
    Asmgenproof.sg_prop p' (oracle_sg tp).


Definition return_address_correct {V} (p8: program (fundef Mach.function) V) sg:=
  forall f tf c ofs sig ros,
    (forall (f : Mach.function) (i : Mach.instruction)
       (ep : bool) (k : Asm.code) (c : list Asm.instruction),
        Asmgen.transl_instr f i ep k = OK c -> is_tail k c) ->
    Stacking.transf_function f = OK tf ->
    is_tail
          (Mach.Mcall sig ros
           :: Stacking.transl_code (Stacklayout.make_env (Bounds.function_bounds f)) c)
          (Mach.fn_code tf) ->
    Asmgenproof0.return_address_offset tf (Stacking.transl_code (Stacklayout.make_env (Bounds.function_bounds f)) c) ofs ->
    forall fb : Values.block,
      Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv (V:=V) p8) fb =
      Some (Internal tf) ->
      forall im : Memory.Mem.mem,
        Globalenvs.Genv.init_mem Mach.fid sg p8 = Some im ->
        Memory.Mem.in_bound_m (Integers.Int.unsigned ofs) im fb.

Lemma oracle_sg_pos:
  forall tp i, oracle_sg tp i > 0.

Lemma oracle_sg_correct_2:
  forall p' tp
    (Cond_Ge: cond_globalenv tp)
    (AG: Asmgen.transf_program p' = OK tp),
    return_address_correct p' (oracle_sg tp).


Lemma box_span_mul_plus:
  forall z y, z >= 0 -> y >= 0 ->
    Memory.Mem.box_span (8 * z + y) = (Z.to_nat z + Memory.Mem.box_span y)%nat.


Theorem transf_rtl_program_correct:
  forall p tp
    (cond_ge: cond_globalenv tp)
    (TRTL: transf_rtl_program p = OK tp),
    let sg := oracle_sg tp in
    let ns := oracle_ns tp in
    forward_simulation (RTL.semantics p ns sg) (Asm.semantics tp sg)
    * backward_simulation (RTL.semantics p ns sg) (Asm.semantics tp sg).

Theorem transf_cminor_program_correct:
  forall p tp (cond_ge: cond_globalenv tp),
    transf_cminor_program p = OK tp ->
    let sg := oracle_sg tp in
    let ns := oracle_ns tp in
    forward_simulation (Cminor.semantics p ns sg) (Asm.semantics tp sg)
    * backward_simulation (Cminor.semantics p ns sg) (Asm.semantics tp sg).

Definition nssl (p: Clight.program) :=
    fold_right (fun (elt: ident * globdef Clight.fundef Ctypes.type)
                (acc: (ident -> nat)) =>
                let ns: ident -> nat := acc in
                match snd elt with
                  Gfun (Clight.Internal f) =>
                  (fun i => if peq i (Clight.fn_id f) then
                           Clight.fn_sl_save f
                         else ns i)
                | _ => ns
                end
             ) (fun _ => O) (prog_defs p).


Lemma varsort_app_comm:
  forall l1 l2,
    Permutation.Permutation (VarSort.varsort (l1 ++ l2)) (VarSort.varsort (l2 ++ l1)).

Definition cond_ge_clight (p: Clight.program) :=
  forall f1 f2 : Clight.function,
    In (Gfun (Clight.Internal f1)) (map snd (prog_defs p)) ->
    In (Gfun (Clight.Internal f2)) (map snd (prog_defs p)) ->
    Clight.fn_id f1 = Clight.fn_id f2 ->
    Clight.fn_params f1 = Clight.fn_params f2 /\
    Clight.fn_vars f1 = Clight.fn_vars f2 /\
    SimplLocals.addr_taken_stmt (Clight.fn_body f1) =
    SimplLocals.addr_taken_stmt (Clight.fn_body f2).


Lemma sl_correct:
  forall p p',
    SimplLocals.transf_program p = OK p' ->
    forall (NR: cond_ge_clight p)

    ,
    forall f : Clight.function,

      In (Gfun (Clight.Internal f)) (map snd (prog_defs p)) ->
      nssl p' (Clight.fn_id f) =
      Datatypes.length
        (filter
           (fun it : SimplLocals.VSet.elt * Ctypes.type =>
              SimplLocals.VSet.mem (fst it)
                                   (SimplLocalsproof.cenv_for_gen
                                      (SimplLocals.addr_taken_stmt (Clight.fn_body f))
                                      (VarSort.varsort (Clight.fn_params f ++ Clight.fn_vars f))))
           (VarSort.varsort (Clight.fn_params f ++ Clight.fn_vars f))).

Theorem transf_clight_program_correct:
  forall p tp (cond_ge: cond_globalenv tp) (cond_ge': cond_ge_clight p),
    transf_clight_program p = OK tp ->
    forall p',
      SimplLocals.transf_program p = OK p' ->
      let sg := oracle_sg tp in
      let ns := oracle_ns tp in
      let sl := nssl p' in
      let ns := fun i => (ns i - sl i)%nat in
    forward_simulation (Clight.semantics1 p ns sg) (Asm.semantics tp sg)
    * backward_simulation (Clight.semantics1 p ns sg) (Asm.semantics tp sg).

Fixpoint filter_map { A B : Type} (f: A -> option B) (l: list A): list B :=
  match l with
    nil => nil
  | a::r => match f a with
             Some a' => a':: filter_map f r
           | None => filter_map f r
           end
  end.

Definition cond_ge_c (p: Csyntax.program) :=
  list_norepet (prog_defs_names p) /\
  list_norepet (filter_map (fun x => match x with
                                    Gfun (Csyntax.Internal f) => Some (Csyntax.fn_id f)
                                  | _ => None
                                  end) (map snd (prog_defs p))).

Definition cond_ge_c' (p: Csyntax.program) :=
  list_norepet (prog_defs_names p) /\
  forall f1 f2 : Csyntax.function,
    In (Gfun (Csyntax.Internal f1)) (map snd (prog_defs p)) ->
    In (Gfun (Csyntax.Internal f2)) (map snd (prog_defs p)) ->
    Csyntax.fn_id f1 = Csyntax.fn_id f2 ->
    f1 = f2.

Lemma filter_map_in:
  forall {A B: Type} f l (a:A) (b:B),
  In a l -> f a = Some b ->
  In b (filter_map f l).

Lemma cond_ge_c_impl:
  forall p,
    cond_ge_c p -> cond_ge_c' p.


Lemma find_funct_ptr_impl_in_snd_prog_defs:
  forall {V W: Type} (p: program V W) b f,
    Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv p) b = Some f ->
    In (Gfun f) (map snd (prog_defs p)).


    Ltac des t :=
      destruct t eqn:?; try subst; simpl in *;
      try intuition congruence;
      repeat
        match goal with
        | H:_ = left _ |- _ => clear H
        | H:_ = right _ |- _ => clear H
        end.

    Ltac destr' := try destr_cond_match; simpl in *; try intuition congruence.

    Ltac destr :=
      destr';
      repeat
        match goal with
        | H:_ = left _ |- _ => clear H
        | H:_ = right _ |- _ => clear H
        end.

    Ltac destr_in H :=
      match type of H with
      | context [match ?f with
                 | _ => _
                 end] => des f
      end;
      repeat
        match goal with
        | H:_ = left _ |- _ => clear H
        | H:_ = right _ |- _ => clear H
        end.

Ltac inv H := inversion H; clear H; try subst.
Ltac ami := repeat match goal with
                     H: bind _ _ = OK _ |- _ => monadInv H
                   | H : OK _ = OK _ |- _ => inv H
                   | H : context [if ?a then _ else _ ] |- _ => destr_in H
                   | |- _ => destr
                   end.




Lemma tgdefs_fn_id:
  forall l g' x0 tf,
    SimplExpr.transl_globdefs l g' = OK x0 ->
    In (Gfun (Clight.Internal tf)) (map snd x0) ->
    In (Clight.fn_id tf) (filter_map (fun x : globdef Csyntax.fundef Ctypes.type =>
                                        match x with
                                        | Gfun (Csyntax.Internal f) => Some (Csyntax.fn_id f)
                                        | Gfun (Csyntax.External _ _ _ _) => None
                                        | Gvar _ => None
                                        end) (map snd l)).

Lemma se_function_ptr_translated_rev''
  : forall (prog : Csyntax.program) (tprog : Clight.program),
    cond_ge_c prog ->
    SimplExpr.transl_program prog = OK tprog ->
    forall (b : Values.block) tf b' tf',
      Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv tprog) b =
      Some (Clight.Internal tf) ->
      Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv tprog) b' =
      Some (Clight.Internal tf') ->
      Clight.fn_id tf = Clight.fn_id tf' ->
      tf = tf'.


Lemma se_transf_globdefs_doesnt_invent_names:
  forall l l' g,
    SimplExpr.transl_globdefs l g = OK l' ->
    forall i,
    In i (map fst l') ->
    In i (map fst l).


Lemma setp_lnr_pdn:
  forall p p',
    list_norepet (prog_defs_names p) ->
    SimplExpr.transl_program p = OK p' ->
    list_norepet (prog_defs_names p').


Lemma cond_ge_c_clight:
  forall p p',
    SimplExpr.transl_program p = OK p' ->
    cond_ge_c p ->
    cond_ge_clight p'.


  Ltac t H :=
    match type of H with
    | ?f _ = _ => unfold f in H; unfold bind in H; destr_in H; inv H
    | ?f _ _ = _ => unfold f in H; unfold bind in H; destr_in H; inv H
    | ?f _ _ _ = _ => unfold f in H; unfold bind in H; destr_in H; inv H
    | ?f _ _ _ _ = _ => unfold f in H; unfold bind in H; destr_in H; inv H
    end.






Definition eq_f {A B: Type} (f: A -> B) (a b: A) : Prop :=
  f a = f b.



Ltac nice_inv' H :=
  match type of H with
    OK _ = OK _ => inv H
  | Error _ = OK _ => inv H
  | _ :: _ = _ => inv H
  | _ => idtac
  end.
  
Ltac dinv' H :=
  unfold bind2, bind in H;
  repeat destr_in H; nice_inv' H.

Ltac autodinv' :=
  repeat match goal with
         | H: context [bind _ _] |- _ => dinv' H
         | H: context [bind2 _ _] |- _ => dinv' H
         | H: context [match _ with _ => _ end] |- _ => dinv' H
         | H: _ = OK _ |- _ => dinv' H
         end.

    

Lemma transf_globdefs_doesnt_invent_names:
  forall A B V W (ff: A -> res B) (fv: V -> res W) l l',
    transf_globdefs ff fv l = OK l' ->
    forall i,
    In i (map fst l') ->
    In i (map fst l).

Lemma transform_partial_program2_lnr_pdn:
  forall A B V W (ff: A -> res B) (fv: V -> res W) (p: program A V) p',
    list_norepet (prog_defs_names p) ->
    transform_partial_program2 ff fv p = OK p' ->
    list_norepet (prog_defs_names p').

Lemma transform_partial_program_lnr_pdn:
  forall A B V (f: A -> res B) (p: program A V) p',
    list_norepet (prog_defs_names p) ->
    transform_partial_program f p = OK p' ->
    list_norepet (prog_defs_names p').
Lemma transform_program_lnr_pdn:
  forall A B V (f: A -> B) (p: program A V),
    list_norepet (prog_defs_names p) ->
    list_norepet (prog_defs_names (transform_program f p)).


Require Import Globalenvs.

Lemma find_funct_add_globvars:
  forall {F V} l (ge: Genv.t (fundef F) V) id x b (f: fundef F),
    Genv.find_funct_ptr (Genv.add_globals (Genv.add_global ge (id, Gvar x)) l) b = Some f ->
    exists b',
      Genv.find_funct_ptr (Genv.add_globals ge l) b' = Some f.

Lemma find_funct_add_globs:
  forall {F V} l (ge: Genv.t (fundef F) V) id (x: external_function) b (f: F),
    Genv.find_funct_ptr (Genv.add_globals (Genv.add_global ge (id, Gfun (External x))) l) b = Some (Internal f) ->
    exists b',
      Genv.find_funct_ptr (Genv.add_globals ge l) b' = Some (Internal f).

Definition front_end (p: Csyntax.program) : res Cminor.program :=
  OK p
     @@@ time "Clight generation" SimplExpr.transl_program
     @@@ time "Simplification of locals" SimplLocals.transf_program
     @@@ time "C#minor generation" Cshmgen.transl_program
     @@@ time "Cminor generation" Cminorgen.transl_program.

Lemma front_end_lnr:
 forall p tp
         (TC: front_end p = OK tp)
         (CGE: cond_ge_c p),
    list_norepet (prog_defs_names tp).

Lemma cond_ge_c_front_end:
  forall p tp,
    front_end p = OK tp ->
    cond_ge_c p ->
    list_norepet (prog_defs_names tp) /\
    forall b1 f1 b2 f2,
      Genv.find_funct_ptr (Genv.globalenv tp) b1 = Some (Internal f1) ->
      Genv.find_funct_ptr (Genv.globalenv tp) b2 = Some (Internal f2) ->
      Cminor.fn_id f1 = Cminor.fn_id f2 -> f1 = f2.

Lemma back_end_lnr:
 forall p tp
         (TC: transf_cminor_program p = OK tp)
         (CGE: list_norepet (prog_defs_names p)),
    list_norepet (prog_defs_names tp).

Lemma cond_ge_cminor_asm:
  forall p tp
         (TC: transf_cminor_program p = OK tp)
         (LNR: list_norepet (prog_defs_names p))
         (EQ: forall b1 f1 b2 f2,
             Genv.find_funct_ptr (Genv.globalenv p) b1 = Some (Internal f1) ->
             Genv.find_funct_ptr (Genv.globalenv p) b2 = Some (Internal f2) ->
             Cminor.fn_id f1 = Cminor.fn_id f2 ->
             f1 = f2),
    cond_globalenv tp.

Definition inj_internal_id (ge : Cminor.genv) :=
  forall b1 f1 b2 f2,
    Genv.find_funct_ptr ge b1 = Some (Internal f1) ->
    Genv.find_funct_ptr ge b2 = Some (Internal f2) ->
    Cminor.fn_id f1 = Cminor.fn_id f2 ->
    f1 = f2.


Definition cminor_preserves_fn_id (p tp : Cminor.program) : Prop :=
  forall
         (LNR: list_norepet (prog_defs_names p))
         (EQ: inj_internal_id (Genv.globalenv p)),
    inj_internal_id (Genv.globalenv tp).

  
Lemma transf_c_program_decomp:
  forall p,
    transf_c_program p =
    front_end p @@@ (transf_cminor_program).

Definition list_norepet_preserves (F : Cminor.program -> res Cminor.program) : Prop :=
  forall p p'
         (NOREP : list_norepet (prog_defs_names p))
         (APP : F p = OK p'),
    list_norepet (prog_defs_names p').


Lemma list_norepet_apply_partial :
  forall (R : res Cminor.program) (tp : Cminor.program)
         (G: Cminor.program -> res Cminor.program)
         (APPG : list_norepet_preserves G)
         (ROK : forall p (ROK : R = OK p), list_norepet (prog_defs_names p))
         (APP : R @@@ G = OK tp),
    list_norepet (prog_defs_names tp).
  
Lemma list_norepet_time :
  forall str (F : Cminor.program -> res Cminor.program),
         list_norepet_preserves F ->
         list_norepet_preserves (time str F).

Hint Resolve list_norepet_time.


Lemma cminor_preserves_fn_id_trans :
  forall p q r
         (NOREP : list_norepet (prog_defs_names p) -> list_norepet (prog_defs_names q))
         (P_PQ : cminor_preserves_fn_id p q)
         (P_QR : cminor_preserves_fn_id q r),
    cminor_preserves_fn_id p r.

Lemma cminor_preserves_fn_id_apply_partial :
  forall (p tp: Cminor.program)
         (R: res Cminor.program)
         (G: Cminor.program -> res Cminor.program)
         (APP : R @@@ G = OK tp)
         (APPG : forall q r, G q = OK r -> cminor_preserves_fn_id q r)
  ,
    exists p, R = OK p /\ G p = OK tp /\ cminor_preserves_fn_id p tp.

Lemma cond_ge_c_asm:
  forall p tp
         (TC: transf_c_program p = OK tp)
         (CGE: cond_ge_c p),
    cond_globalenv tp.

Theorem transf_cstrategy_program_correct:
  forall p tp
    p' (SE: SimplExpr.transl_program p = OK p')
    (cond_ge: cond_ge_c p),
    transf_c_program p = OK tp ->
  forall p'',
      SimplLocals.transf_program p' = OK p'' ->
      let sg := oracle_sg tp in
      let ns := oracle_ns tp in
      let sl := nssl p'' in
      let ns := fun i => (ns i - sl i)%nat in
  forward_simulation (Cstrategy.semantics p ns sg) (Asm.semantics tp sg)
  * backward_simulation (atomic (Cstrategy.semantics p ns sg)) (Asm.semantics tp sg).

Definition oracles p tp (TC: transf_c_program p = OK tp) :
  (ident -> Z) * (ident -> nat) * (ident -> nat).

Definition do_oracles (p: Csyntax.program) : option ((ident -> Z) * (ident -> nat) * (ident -> nat)).

Theorem transf_c_program_correct:
  forall p tp
    (cond_ge: cond_ge_c p)
    (TC: transf_c_program p = OK tp),
    let (sgns,sl) := oracles p tp TC in
    let (sg,ns) := sgns in
  backward_simulation (Csem.semantics p ns sg) (Asm.semantics tp sg).