Require SeparateCompiler.
Require AsmgenproofX.
Require MachX2Mach2X.
Require StackingproofX.
Require CleanupLabelsproofX.
Require LinearizeproofX.
Require TunnelingproofX.
Require AllocproofX.
Require DeadcodeproofX.
Require ConstpropproofX.
Require CSEproofX.
Require RenumberproofX.
Require InliningproofX.
Require TailcallproofX.
Require RTLgenproofX.
Require SelectionproofX.
Require CminorgenproofX.
Require CshmgenproofX.
Require RTLtypingX.

Import Coqlib.
Import String.
Import Errors.
Import AST.
Import Values.
Import MemoryX.
Import Globalenvs.
Import ComposePasses.
Import Events.
Import SmallstepX.
Import Conventions1.
Import Asm.
Import SeparateCompiler.

Local Open Scope string_scope.

Semantic preservation

Section WITHCONFIG.
Context mem `{external_calls_prf : ExternalCalls mem}
        `{memory_model_x: !Mem.MemoryModelX mem}.

Context {i64_helpers: SplitLongproof.I64HelpersCorrect mem}.

Variables
  (p: Clight.program) (p2: RTL.program)
  (TRANSL_TO_RTL: transf_clight_program_to_rtl p = OK p2)

.

Let fenv := Inlining.funenv_program p2.


Ltac rew_genv_next :=
  lazymatch goal with
  | |- context [Genv.genv_next (Genv.globalenv ?p)] =>
    match goal with
    | H: Cminorgen.transl_program ?p = OK _ |- _ =>
      rewrite <- (Cminorgenproof.genv_next_preserved _ _ (Cminorgenproof.transf_program_match _ _ H))
    | H: Selection.sel_program ?p = OK _ |- _ =>
      rewrite <- (Selectionproof.genv_next_preserved _ _ (Selectionproof.transf_program_match _ _ H))
    | H: RTLgen.transl_program ?p = OK _ |- _ =>
      rewrite <- (RTLgenproof.genv_next_preserved _ _ (RTLgenproof.transf_program_match _ _ H))
    | H := Tailcall.transf_program ?p |- _ =>
           rewrite <- (Tailcallproof.genv_next_preserved _ _ (Tailcallproof.transf_program_match p)); fold H
         | H: InliningX.transf_program _ ?p = OK _ |- _ =>
           rewrite <- (Inliningproof.genv_next_preserved _ _ (Inliningproof.transf_program_match _ _ H))
         | H := Renumber.transf_program ?p |- _ =>
                rewrite <- (Renumberproof.genv_next_preserved _ _ (Renumberproof.transf_program_match p)); fold H
              | H := ConstpropX.transf_program ?p |- _ =>
                     rewrite <- (ConstpropproofX.genv_next_preserved p); fold H
                   | H: CSEX.transf_program ?p = OK _ |- _ =>
                     rewrite <- (CSEproofX.genv_next_preserved _ _ H)
                   | H: DeadcodeX.transf_program ?p = OK _ |- _ =>
                     rewrite <- (DeadcodeproofX.genv_next_preserved _ _ H)
                   | H: Allocation.transf_program ?p = OK _ |- _ =>
                     rewrite <- (Allocproof.genv_next_preserved _ _ (Allocproof.transf_program_match _ _ H))
                   | H := Tunneling.tunnel_program ?p |- _ =>
                          rewrite <- (Tunnelingproof.genv_next_preserved _ _ (Tunnelingproof.transf_program_match p)); fold H
                        | H: Linearize.transf_program ?p = OK _ |- _ =>
                          rewrite <- (Linearizeproof.genv_next_preserved _ _ (Linearizeproof.transf_program_match _ _ H))
                        | H := CleanupLabels.transf_program ?p |- _ =>
                               rewrite <- (CleanupLabelsproof.genv_next_preserved _ _ (CleanupLabelsproof.transf_program_match p)); fold H
    end
  end.

Lemma transf_clight_to_linear_correct:
    forall fn_stack_requirements
      (tp: Linear.program)
      (TRANSL_TO_LINEAR: transf_rtl_program_to_linear fenv p2 = OK tp)
      m
      (INJECT_NEUTRAL: Mem.inject_neutral (Mem.nextblock m) m)
      (GENV_NEXT: Ple (Genv.genv_next (Genv.globalenv tp)) (Mem.nextblock m))
      args
      (args_inj: Val.inject_list (Mem.flat_inj (Mem.nextblock m)) args args)
      sg
      init_linear_rs
      (Hargs_val: args = map (fun r : rpair Locations.loc => Locations.Locmap.getpair r init_linear_rs) (loc_arguments sg))
 
      (Hargs_type:
         Val.has_type_list
           (map (fun r : rpair Locations.loc => Locations.Locmap.getpair r init_linear_rs) (loc_arguments sg))
           (sig_args sg))
      i
    ,
      forward_simulation
        (ClightX.semantics (fn_stack_requirements) p i m sg args)
        (semantics_with_inject (LinearX.semantics fn_stack_requirements init_linear_rs tp i sg args m) m).

  Lemma plt_eq_eq:
    forall a b, (forall c, Plt c a <-> Plt c b) -> a = b.

  Definition fn_stack_requirements (tp: Asm.program) (id: ident) : Z :=
    match Globalenvs.Genv.find_symbol (Globalenvs.Genv.globalenv tp) id with
    | Some b =>
      match Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv tp) b with
      | Some (Internal f) => Asm.fn_stacksize f
      | _ => 0
      end
    | None => 0
    end.

  Lemma match_program_no_more_functions:
    forall {F1 V1 F2 V2}
      `{Linking.Linker F1} `{Linking.Linker V1}
      Mf Mv
      (p1: AST.program F1 V1) (p2: AST.program F2 V2),
      Linking.match_program Mf Mv p1 p2 ->
      forall b,
        Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv p1) b = None ->
        Globalenvs.Genv.find_funct_ptr (Globalenvs.Genv.globalenv p2) b = None.

  Definition funsig (f: Asm.fundef) : signature :=
    match f with
      External ef => ef_sig ef
    | Internal f => fn_sig f
    end.

  Theorem transf_clight_program_correct:
    forall
      tp
      (TRANSL_TO_ASM: transf_rtl_program fenv p2 = OK tp)
      m init_asm_rs
      (ASM_INVARIANT: AsmX.asm_invariant (Genv.globalenv tp) init_asm_rs m)
      args sg
      (EXTCALL_ARGS: Asm.extcall_arguments init_asm_rs m sg args)
      i b
      (Hsymb: Genv.find_symbol (Genv.globalenv tp) i = Some b)
      (SIGNATURE: forall f, Genv.find_funct_ptr (Genv.globalenv tp) b = Some f -> sg = funsig f)
      (INITSP: StackingproofX.init_sp m = init_asm_rs RSP)
      (PC_VAL: init_asm_rs PC = Values.Vptr b Integers.Ptrofs.zero)
      (RA_NOT_VUNDEF: init_asm_rs RA <> Vundef)
      (ARGSSIZE: 4 * size_arguments sg <= Integers.Ptrofs.max_unsigned)
      (ARGSTYPE: Val.has_type_list
                    (map
                       (fun r =>
                          Locations.Locmap.getpair
                            r
                            (StackingproofX.init_linear_rs
                               (AsmgenproofX.init_mach_rs init_asm_rs)
                               m))
                       (loc_arguments sg))
                    (sig_args sg))
      (StackInfo: Mach.init_sp_stackinfo sg (Mem.stack m))
      (RaCorrect: forall (b0 : block) (o : Integers.Ptrofs.int),
          init_asm_rs RA = Vptr b0 o ->
          forall f : fundef,
            Genv.find_funct_ptr (Genv.globalenv tp) b0 = Some f ->
            is_after_call f (Integers.Ptrofs.unsigned o)
      ),
      forward_simulation
        (ClightX.semantics (fn_stack_requirements tp) p i m sg args)
        (semantics_with_inject (AsmX.semantics init_asm_rs tp i sg args m) m).

End WITHCONFIG.