Module Mach2Mach2

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Op.
Require Import Locations.
Require Import Conventions.
Require Stacklayout.
Require Import Mach.

Section WITHEXTCALLS.
  Context `{external_calls: ExternalCalls}.

Section WITHINITSP.
  Variables init_ra: val.
  Variable return_address_offset: function -> code -> ptrofs -> Prop.
  Variable prog: program.
  Let ge:= Genv.globalenv prog.

  Existing Instance inject_perm_all.

  Definition stack_equiv s1 s2 :=
    list_forall2 (fun tf1 tf2 => size_frames tf1 = size_frames tf2) s1 s2.
  
  Inductive match_states : state -> state -> Prop :=
  | match_states_regular s f sp c rs rs' m m'
                         (MLD: Mem.extends m m')
                         (RLD: forall r, Val.lessdef (rs r) (rs' r))
                         (SE: stack_equiv (Mem.stack m) (Mem.stack m')):
      match_states (State s f sp c rs m) (State s f sp c rs' m')
  | match_states_call s fb rs rs' m m'
                      (MLD: Mem.extends m m')
                      (RLD: forall r, Val.lessdef (rs r) (rs' r))
                      (SE: stack_equiv (Mem.stack m) (Mem.stack m')):
      match_states (Callstate s fb rs m) (Callstate s fb rs' m')
  | match_states_return s rs rs' m m'
                        (MLD: Mem.extends m m')
                        (RLD: forall r, Val.lessdef (rs r) (rs' r))
                        (SE: stack_equiv (Mem.stack m) (Mem.stack m')):
      match_states (Returnstate s rs m) (Returnstate s rs' m').

  Variable init_sg: signature.
  Variable init_stk: stack.

  Lemma parent_sp_same_tl:
    forall s1 s2 cs
           (LP1: Mach.list_prefix init_sg init_stk cs (tl s1)) (LP2: list_prefix init_sg init_stk cs (tl s2)) (LEN: length s1 = length s2),
      parent_sp s1 = parent_sp s2.

  Lemma list_prefix_length:
    forall cs s,
      Mach.list_prefix init_sg init_stk cs s ->
      length s = (length init_stk + length cs)%nat.

  Lemma parent_sp_same:
    forall s1 s2 cs
           (LP1: list_prefix init_sg init_stk cs s1) (LP2: list_prefix init_sg init_stk cs s2),
      parent_sp s1 = parent_sp s2.

  Lemma zle_zlt_false:
    forall lo hi o,
      zle lo o && zlt o hi = false <-> ~ (lo <= o < hi)%Z.

  Hypothesis frame_correct:
    forall (fb : block) (f : function),
      Genv.find_funct_ptr (Genv.globalenv prog) fb = Some (Internal f) ->
      0 < fn_stacksize f.

  Lemma lessdef_set_reg:
    forall rs rs'
      (RLD : forall r : RegEq.t, Val.lessdef (rs r) (rs' r))
      v v' (LD: Val.lessdef v v') dst r,
      Val.lessdef (rs # dst <- v r) (rs' # dst <- v' r).

  Lemma lessdef_set_res:
    forall res rs rs'
      (RLD : forall r : RegEq.t, Val.lessdef (rs r) (rs' r))
      v v' (LD: Val.lessdef v v') r,
      Val.lessdef (set_res res v rs r)
                  (set_res res v' rs' r).

  Lemma lessdef_set_pair:
    forall pair rs rs'
      (RLD : forall r : RegEq.t, Val.lessdef (rs r) (rs' r))
      v v' (LD: Val.lessdef v v') r,
      Val.lessdef (set_pair pair v rs r)
                  (set_pair pair v' rs' r).
  
  Lemma lessdef_undef_regs:
    forall rs rs'
      (RLD : forall r : RegEq.t, Val.lessdef (rs r) (rs' r))
      l r,
      Val.lessdef (undef_regs l rs r) (undef_regs l rs' r).

  Lemma lessdef_args:
    forall rs rs'
      (RLD : forall r : RegEq.t, Val.lessdef (rs r) (rs' r))
      l,
      Val.lessdef_list (rs ## l) (rs' ## l).

  Lemma find_function_ptr_lessdef:
    forall ge ros b rs rs'
      (RLD : forall r : RegEq.t, Val.lessdef (rs r) (rs' r))
      (FFP: find_function_ptr ge ros rs = Some b),
      find_function_ptr ge ros rs' = Some b.


Section EXTERNAL_ARGUMENTS.

  Variables rs rs': regset.
  Hypothesis RLD: forall r : RegEq.t, Val.lessdef (rs r) (rs' r).
  Variables m m' : mem.
  Hypothesis MLD: Mem.extends m m'.
  Variable sp: val.
  
  Lemma extcall_arg_ld:
    forall l v,
      extcall_arg rs m sp l v ->
      exists v',
        extcall_arg rs' m' sp l v' /\ Val.lessdef v v'.

  Lemma extcall_arg_pair_ld:
    forall l v,
      extcall_arg_pair rs m sp l v ->
      exists v',
        extcall_arg_pair rs' m' sp l v' /\ Val.lessdef v v'.

  Lemma extcall_arguments_ld:
    forall sg v,
      extcall_arguments rs m sp sg v ->
      exists v',
        extcall_arguments rs' m' sp sg v' /\ Val.lessdef_list v v'.

End EXTERNAL_ARGUMENTS.


Lemma max_l_pos:
  forall l, 0 <= max_l l.

Lemma stack_equiv_size_stack:
  forall s1 s2,
    stack_equiv s1 s2 ->
    size_stack s2 = size_stack s1.

Hypothesis init_ra_not_undef: init_ra <> Vundef.
Lemma parent_ra_not_undef:
  forall ge s,
    callstack_function_defined return_address_offset ge s ->
    parent_ra init_ra s <> Vundef.

Ltac same_hyps :=
  repeat match goal with
         | H1: ?a = _, H2: ?a = _ |- _ => rewrite H1 in H2; inv H2
         | H1: ?a, H2: ?a |- _ => clear H1
         end.

      Lemma step_correct:
    forall S1 t S2 (STEP: Mach.step init_ra return_address_offset invalidate_frame1 ge S1 t S2)
      S1' (MS: match_states S1 S1')
      (HC1: has_code return_address_offset ge S1)
      (CSC1: call_stack_consistency ge init_sg init_stk S1)
      (HC1': has_code return_address_offset ge S1')
      (CSC1': call_stack_consistency ge init_sg init_stk S1'),
    exists S2',
      Mach.step init_ra return_address_offset invalidate_frame2 ge S1' t S2' /\ match_states S2 S2'.

End WITHINITSP.
  Existing Instance inject_perm_all.

  Lemma initial_transf:
    forall p s, initial_state p s -> match_states s s.

  Lemma final_transf:
    forall s1 s2 i, match_states s1 s2 -> final_state s1 i -> final_state s2 i.

  Lemma mach2_simulation:
    forall rao p,
      (forall (fb : block) (f : function),
          Genv.find_funct_ptr (Genv.globalenv p) fb = Some (Internal f) ->
          0 < fn_stacksize f) ->
      forward_simulation (Mach.semantics1 rao p) (Mach.semantics2 rao p).

End WITHEXTCALLS.