(** Simulation between the two semantics for the Mach language. *)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Machabstr.
Require Import Mach.
Require Import Machtyping.
Require Import Stackingproof.

(** Two semantics were defined for the Mach intermediate language:
- The concrete semantics (file [Mach]), where the whole activation
  record resides in memory and the [Mgetstack], [Msetstack] and
  [Mgetparent] are interpreted as [sp]-relative memory accesses.
- The abstract semantics (file [Machabstr]), where the activation
  record is split in two parts: the Cminor stack data, resident in
  memory, and the frame information, residing not in memory but
  in additional evaluation environments.

  In this file, we show a simulation result between these
  semantics: if a program executes to some result [r] in the
  abstract semantics, it also executes to the same result in
  the concrete semantics.  This result bridges the correctness proof
  in file [Stackingproof] (which uses the abstract Mach semantics
  as output) and that in file [PPCgenproof] (which uses the concrete
  Mach semantics as input).
*)

Remark align_16_top_ge:
  forall lo hi,
  hi <= align_16_top lo hi.
Proof.
  intros. unfold align_16_top. apply Zmax_bound_r. 
  assert (forall x, x <= (x + 15) / 16 * 16).
  intro. assert (16 > 0). omega.
  generalize (Z_div_mod_eq (x + 15) 16 H). intro.
  replace ((x + 15) / 16 * 16) with ((x + 15) - (x + 15) mod 16).
  generalize (Z_mod_lt (x + 15) 16 H). omega. 
  rewrite Zmult_comm. omega.
  generalize (H (hi - lo)). omega. 
Qed.

Remark align_16_top_pos:
  forall lo hi,
  0 <= align_16_top lo hi.
Proof.
  intros. unfold align_16_top. apply Zmax_bound_l. omega.
Qed.

Remark size_mem_pos:
  forall sz, size_mem sz > 0.
Proof.
  destruct sz; simpl; compute; auto.
Qed.

Remark size_type_chunk:
  forall ty, size_chunk (chunk_of_type ty) = 4 * typesize ty.
Proof.
  destruct ty; reflexivity.
Qed.

Remark mem_chunk_type:
  forall ty, mem_chunk (chunk_of_type ty) = mem_type ty.
Proof.
  destruct ty; reflexivity.
Qed.

Remark size_mem_type:
  forall ty, size_mem (mem_type ty) = 4 * typesize ty.
Proof.
  destruct ty; reflexivity.
Qed.

(** * Agreement between frames and memory-resident activation records *)

(** ** Agreement for one frame *)

(** The core idea of the simulation proof is that for all active
  functions, the memory-allocated activation record, in the concrete 
  semantics, contains the same data as the Cminor stack block
  (at positive offsets) and the frame of the function (at negative
  offsets) in the abstract semantics.

  This intuition (activation record = Cminor stack data + frame)
  is formalized by the following predicate [frame_match fr sp base mm ms].
  [fr] is a frame and [mm] the current memory state in the abstract
  semantics. [ms] is the current memory state in the concrete semantics.
  The stack pointer is [Vptr sp base] in both semantics. *)

Inductive frame_match: frame -> block -> int -> mem -> mem -> Prop :=
  frame_match_intro:
    forall fr sp base mm ms,
    valid_block ms sp ->
    low_bound mm sp = 0 ->
    low_bound ms sp = fr.(low) ->
    high_bound ms sp = align_16_top fr.(low) (high_bound mm sp) ->
    fr.(low) <= 0 ->
    Int.min_signed <= fr.(low) ->
    base = Int.repr fr.(low) ->
    block_contents_agree fr.(low) 0 fr (ms.(blocks) sp) ->
    block_contents_agree 0 (high_bound ms sp)
                         (mm.(blocks) sp) (ms.(blocks) sp) ->
    frame_match fr sp base mm ms.

(** [frame_match], while presented as a relation for convenience,
  is actually a function: it fully determines the contents of the
  activation record [ms.(blocks) sp]. *)

Lemma frame_match_exten:
  forall fr sp base mm ms1 ms2,
  frame_match fr sp base mm ms1 ->
  frame_match fr sp base mm ms2 ->
  ms1.(blocks) sp = ms2.(blocks) sp. 
Proof.
  intros. inversion H. inversion H0.
  unfold low_bound, high_bound in *.
  apply block_contents_exten.
  congruence.
  congruence.
  hnf; intros.
  elim H29. rewrite H3; rewrite H4; intros.
  case (zlt ofs 0); intro.
  assert (low fr <= ofs < 0). tauto.
  transitivity (contents fr ofs).
  symmetry. apply H8; auto.
  apply H22; auto.
  transitivity (contents (blocks mm sp) ofs).
  symmetry. apply H9. rewrite H4. omega.
  apply H23. rewrite H18. omega.
Qed.

(** The following two innocuous-looking lemmas are the key results
  showing that [sp]-relative memory accesses in the concrete
  semantics behave like the direct frame accesses in the abstract
  semantics.  First, a value [v] that has type [ty] is preserved
  when stored in memory with chunk [chunk_of_type ty], then read
  back with the same chunk.  The typing hypothesis is crucial here:
  for instance, a float value reads back as [Vundef] when stored
  and load with chunk [Mint32]. *)

Lemma load_result_ty:
  forall v ty,
  Val.has_type v ty -> Val.load_result (chunk_of_type ty) v = v.
Proof.
  destruct v; destruct ty; simpl; contradiction || reflexivity.
Qed.

(** Second, computations of [sp]-relative offsets using machine
  arithmetic (as done in the concrete semantics) never overflows
  and behaves identically to the offset computations using exact
  arithmetic (as done in the abstract semantics). *)

Lemma int_add_no_overflow:
  forall x y,
  Int.min_signed <= Int.signed x + Int.signed y <= Int.max_signed ->
  Int.signed (Int.add x y) = Int.signed x + Int.signed y.
Proof.
  intros. rewrite Int.add_signed. rewrite Int.signed_repr. auto. auto.
Qed.

(** Given matching frames and activation records, loading from the
  activation record (in the concrete semantics) behaves identically
  to reading the corresponding slot from the frame
  (in the abstract semantics).  *)

Lemma frame_match_get_slot:
  forall fr sp base mm ms ty ofs v,
  frame_match fr sp base mm ms ->
  get_slot fr ty (Int.signed ofs) v ->
  Val.has_type v ty ->
  load_stack ms (Vptr sp base) ty ofs = Some v.
Proof.
  intros. inversion H. inversion H0. subst v.
  unfold load_stack, Val.add, loadv. 
  assert (Int.signed base = low fr).
    rewrite H8. apply Int.signed_repr.
    split. auto. apply Zle_trans with 0. auto. compute; congruence.
  assert (Int.signed (Int.add base ofs) = low fr + Int.signed ofs).
    rewrite int_add_no_overflow. rewrite H18. auto.
    rewrite H18. split. omega. apply Zle_trans with 0.
    generalize (typesize_pos ty). omega. compute. congruence.
  rewrite H23. 
  assert (BND1: low_bound ms sp <= low fr + Int.signed ofs). 
    omega. 
  assert (BND2: (low fr + Int.signed ofs) + size_chunk (chunk_of_type ty) <= high_bound ms sp).
    rewrite size_type_chunk. apply Zle_trans with 0.
    assumption. rewrite H5. apply align_16_top_pos.
  generalize (load_in_bounds (chunk_of_type ty) ms sp (low fr + Int.signed ofs) H2 BND1 BND2).
  intros [v' LOAD].
  generalize (load_inv _ _ _ _ _ LOAD).
  intros [A [B [C D]]].
  rewrite LOAD. rewrite <- D. 
  decEq. rewrite mem_chunk_type. 
  rewrite <- size_mem_type in H17.
  assert (low fr <= low fr + Int.signed ofs). omega.
  generalize (load_contentmap_agree _ _ _ _ _ _ H9 H24 H17).
  intro. rewrite H25.
  apply load_result_ty.
  assumption.
Qed.

(** Loads from [sp], corresponding to accesses to Cminor stack data
  in the abstract semantics, give the same results in the concrete
  semantics.  This is because the offset from [sp] must be positive or
  null for the original load to succeed, and because the part
  of the activation record at positive offsets matches the Cminor
  stack data block. *)

Lemma frame_match_load:
  forall fr sp base mm ms chunk ofs v,
  frame_match fr sp base mm ms ->
  load chunk mm sp ofs = Some v ->
  load chunk ms sp ofs = Some v.
Proof.
  intros. inversion H. 
  generalize (load_inv _ _ _ _ _ H0). intros [A [B [C D]]].
  change (low (blocks mm sp)) with (low_bound mm sp) in B.
  change (high (blocks mm sp)) with (high_bound mm sp) in C.
  unfold load. rewrite zlt_true; auto.
  rewrite in_bounds_holds. 
  rewrite <- D. decEq. decEq. eapply load_contentmap_agree.
  red in H9. eexact H9. 
  omega.
  unfold size_chunk in C. rewrite H4. 
  apply Zle_trans with (high_bound mm sp). auto. 
  apply align_16_top_ge. 
  change (low (blocks ms sp)) with (low_bound ms sp).
  rewrite H3. omega.
  change (high (blocks ms sp)) with (high_bound ms sp).
  rewrite H4. apply Zle_trans with (high_bound mm sp). auto.
  apply align_16_top_ge.
Qed.

(** Assigning a value to a frame slot (in the abstract semantics)
  corresponds to storing this value in the activation record
  (in the concrete semantics).  Moreover, agreement between frames
  and activation records is preserved. *)

Lemma frame_match_set_slot:
  forall fr sp base mm ms ty ofs v fr',
  frame_match fr sp base mm ms ->
  set_slot fr ty (Int.signed ofs) v fr' ->
  exists ms',
    store_stack ms (Vptr sp base) ty ofs v = Some ms' /\
    frame_match fr' sp base mm ms'.
Proof.
  intros. inversion H. inversion H0. subst ty0.
  unfold store_stack, Val.add, storev. 
  assert (Int.signed base = low fr).
    rewrite H7. apply Int.signed_repr.
    split. auto. apply Zle_trans with 0. auto. compute; congruence.
  assert (Int.signed (Int.add base ofs) = low fr + Int.signed ofs).
    rewrite int_add_no_overflow. rewrite H16. auto.
    rewrite H16. split. omega. apply Zle_trans with 0.
    generalize (typesize_pos ty). omega. compute. congruence.
  rewrite H20.
  assert (BND1: low_bound ms sp <= low fr + Int.signed ofs). 
    omega. 
  assert (BND2: (low fr + Int.signed ofs) + size_chunk (chunk_of_type ty) <= high_bound ms sp).
    rewrite size_type_chunk. rewrite H4.
    apply Zle_trans with 0. subst ofs0. auto. apply align_16_top_pos. 
  generalize (store_in_bounds _ _ _ _ v H1 BND1 BND2).
  intros [ms' STORE].
  generalize (store_inv _ _ _ _ _ _ STORE). intros [P [Q [R [S [x T]]]]].
  generalize (low_bound_store _ _ _ _ sp _ _ STORE). intro LB.
  generalize (high_bound_store _ _ _ _ sp _ _ STORE). intro HB.
  exists ms'. 
  split. exact STORE.
  apply frame_match_intro; auto.
  eapply valid_block_store; eauto.
  rewrite LB. auto.
  rewrite HB. auto.
  red. rewrite T; rewrite update_s; simpl. 
  rewrite mem_chunk_type. 
  subst ofs0. eapply store_contentmap_agree; eauto.
  rewrite HB; rewrite T; rewrite update_s.
  red. simpl. apply store_contentmap_outside_agree.
  assumption. left. rewrite mem_chunk_type. 
  rewrite size_mem_type. subst ofs0. auto.
Qed.

(** Agreement is preserved by stores within blocks other than the
  one pointed to by [sp]. *)

Lemma frame_match_store_stack_other:
  forall fr sp base mm ms sp' base' ty ofs v ms',
  frame_match fr sp base mm ms ->
  store_stack ms (Vptr sp' base') ty ofs v = Some ms' ->
  sp <> sp' ->
  frame_match fr sp base mm ms'.
Proof.
  unfold store_stack, Val.add, storev. intros. inversion H.
  generalize (store_inv _ _ _ _ _ _ H0). intros [P [Q [R [S [x T]]]]].
  generalize (low_bound_store _ _ _ _ sp _ _ H0). intro LB.
  generalize (high_bound_store _ _ _ _ sp _ _ H0). intro HB.
  apply frame_match_intro; auto.
  eapply valid_block_store; eauto.
  rewrite LB; auto.
  rewrite HB; auto.
  rewrite T; rewrite update_o; auto.
  rewrite HB; rewrite T; rewrite update_o; auto.
Qed.

(** Stores relative to [sp], corresponding to accesses to Cminor stack data
  in the abstract semantics, give the same results in the concrete
  semantics.  Moreover, agreement between frames and activation
  records is preserved. *)

Lemma frame_match_store_ok:
  forall fr sp base mm ms chunk ofs v mm',
  frame_match fr sp base mm ms ->
  store chunk mm sp ofs v = Some mm' ->
  exists ms', store chunk ms sp ofs v = Some ms'.
Proof.
  intros. inversion H. 
  generalize (store_inv _ _ _ _ _ _ H0). intros [P [Q [R [S [x T]]]]].
  change (low (blocks mm sp)) with (low_bound mm sp) in Q.
  change (high (blocks mm sp)) with (high_bound mm sp) in R.
  apply store_in_bounds.
  auto.
  omega. 
  apply Zle_trans with (high_bound mm sp).
    auto. rewrite H4. apply align_16_top_ge. 
Qed.

Lemma frame_match_store:
  forall fr sp base mm ms chunk b ofs v mm' ms',
  frame_match fr sp base mm ms ->
  store chunk mm b ofs v = Some mm' ->
  store chunk ms b ofs v = Some ms' ->
  frame_match fr sp base mm' ms'.
Proof.
  intros. inversion H. 
  generalize (store_inv _ _ _ _ _ _ H1). intros [A [B [C [D [x1 E]]]]].
  generalize (store_inv _ _ _ _ _ _ H0). intros [I [J [K [L [x2 M]]]]].
  generalize (low_bound_store _ _ _ _ sp _ _ H0). intro LBm.
  generalize (low_bound_store _ _ _ _ sp _ _ H1). intro LBs.
  generalize (high_bound_store _ _ _ _ sp _ _ H0). intro HBm.
  generalize (high_bound_store _ _ _ _ sp _ _ H1). intro HBs.
  apply frame_match_intro; auto.
  eapply valid_block_store; eauto.
  congruence. congruence. congruence. 
  rewrite E. unfold update. case (zeq sp b); intro.
  subst b. red; simpl.
  apply store_contentmap_outside_agree; auto.
  right. unfold low_bound in H3. omega.
  assumption.
  rewrite HBs; rewrite E; rewrite M; unfold update.
  case (zeq sp b); intro.
  subst b. red; simpl.
  apply store_contentmap_agree; auto.
  assumption.
Qed.

(** Memory allocation of the Cminor stack data block (in the abstract
  semantics) and of the whole activation record (in the concrete
  semantics) return memory states that agree according to [frame_match].
  Moreover, [frame_match] relations over already allocated blocks
  remain true. *)

Lemma frame_match_new:
  forall mm ms mm' ms' sp sp' f,
  mm.(nextblock) = ms.(nextblock) ->
  alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
  alloc ms (- f.(fn_framesize)) (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) = (ms', sp') ->
  f.(fn_framesize) >= 0 ->
  f.(fn_framesize) <= -Int.min_signed ->
  frame_match (init_frame f) sp (Int.repr (-f.(fn_framesize))) mm' ms'.
Proof.
  intros. 
  injection H0; intros. injection H1; intros.
  assert (sp = sp'). congruence. rewrite <- H8 in H6. subst sp'.
  generalize (low_bound_alloc _ _ sp _ _ _ H0). rewrite zeq_true. intro LBm.
  generalize (low_bound_alloc _ _ sp _ _ _ H1). rewrite zeq_true. intro LBs.
  generalize (high_bound_alloc _ _ sp _ _ _ H0). rewrite zeq_true. intro HBm.
  generalize (high_bound_alloc _ _ sp _ _ _ H1). rewrite zeq_true. intro HBs.
  apply frame_match_intro; auto.
  eapply valid_new_block; eauto.
  simpl. congruence.
  simpl. omega.
  simpl. omega.
  rewrite <- H7. simpl. rewrite H6; simpl. rewrite update_s.
  hnf; simpl; auto.
  rewrite HBs; rewrite <- H5; simpl; rewrite H4; rewrite <- H7; simpl; rewrite H6; simpl;
  repeat (rewrite update_s).
  hnf; simpl; auto.
Qed.

Lemma frame_match_alloc:
  forall mm ms fr sp base lom him los his mm' ms' bm bs,
  mm.(nextblock) = ms.(nextblock) ->
  frame_match fr sp base mm ms ->
  alloc mm lom him = (mm', bm) ->
  alloc ms los his = (ms', bs) ->
  frame_match fr sp base mm' ms'.
Proof.
  intros. inversion H0.
  assert (sp <> bm). 
    apply valid_not_valid_diff with mm. 
    red. rewrite H. exact H3.
    eapply fresh_block_alloc; eauto.
  assert (sp <> bs).
    apply valid_not_valid_diff with ms. auto. 
    eapply fresh_block_alloc; eauto.
  generalize (low_bound_alloc _ _ sp _ _ _  H1). 
    rewrite zeq_false; auto; intro LBm.
  generalize (low_bound_alloc _ _ sp _ _ _  H2). 
    rewrite zeq_false; auto; intro LBs.
  generalize (high_bound_alloc _ _ sp _ _ _  H1). 
    rewrite zeq_false; auto; intro HBm.
  generalize (high_bound_alloc _ _ sp _ _ _  H2). 
    rewrite zeq_false; auto; intro HBs.
  apply frame_match_intro.
  eapply valid_block_alloc; eauto.
  congruence. congruence. congruence. auto. auto. auto. 
  injection H2; intros. rewrite <- H20; simpl; rewrite H19; simpl.
    rewrite update_o; auto. 
  rewrite HBs;
  injection H2; intros. rewrite <- H20; simpl; rewrite H19; simpl.
  injection H1; intros. rewrite <- H22; simpl; rewrite H21; simpl.
  repeat (rewrite update_o; auto).
Qed.

(** [frame_match] relations are preserved by freeing a block
  other than the one pointed to by [sp]. *)

Lemma frame_match_free:
  forall fr sp base mm ms b,
  frame_match fr sp base mm ms ->
  sp <> b ->
  frame_match fr sp base (free mm b) (free ms b).
Proof.
  intros. inversion H.
  generalize (low_bound_free mm _ _ H0); intro LBm.
  generalize (low_bound_free ms _ _ H0); intro LBs.
  generalize (high_bound_free mm _ _ H0); intro HBm.
  generalize (high_bound_free ms _ _ H0); intro HBs.
  apply frame_match_intro; auto.
  congruence. congruence. congruence. 
  unfold free; simpl. rewrite update_o; auto. 
  rewrite HBs. 
  unfold free; simpl. repeat (rewrite update_o; auto).
Qed.

(** ** Agreement for all the frames in a call stack *)

(** We need to reason about all the frames and activation records
    active at any given time during the executions: not just
    about those for the currently executing function, but also
    those for the callers.  These collections of 
    active frames are called ``call stacks''.  They are lists
    of triples representing a frame and a stack pointer
    (reference and offset) in the abstract semantics. *)

Definition callstack : Set := list (frame * block * int).

(** The correct linking of frames (each frame contains a pointer
  to the frame of its caller at the lowest offset) is captured
  by the following predicate. *)

Inductive callstack_linked: callstack -> Prop :=
  | callstack_linked_nil:
      callstack_linked nil
  | callstack_linked_one:
      forall fr1 sp1 base1,
      callstack_linked ((fr1, sp1, base1) :: nil)
  | callstack_linked_cons:
      forall fr1 sp1 base1 fr2 base2 sp2 cs,
      get_slot fr1 Tint 0 (Vptr sp2 base2) ->
      callstack_linked ((fr2, sp2, base2) :: cs) ->
      callstack_linked ((fr1, sp1, base1) :: (fr2, sp2, base2) :: cs).

(** [callstack_dom cs b] (read: call stack [cs] is ``dominated''
  by block reference [b]) means that the stack pointers in [cs]
  strictly decrease and are all below [b].  This ensures that
  the stack block for a function was allocated after that for its
  callers.  A consequence is that no two active functions share
  the same stack block. *)

Inductive callstack_dom: callstack -> block -> Prop :=
  | callstack_dom_nil:
      forall b, callstack_dom nil b
  | callstack_dom_cons:
      forall fr sp base cs b,
      sp < b ->
      callstack_dom cs sp ->
      callstack_dom ((fr, sp, base) :: cs) b.

Lemma callstack_dom_less:
  forall cs b, callstack_dom cs b ->
  forall fr sp base, In (fr, sp, base) cs -> sp < b.
Proof.
  induction 1. simpl. tauto. 
  simpl. intros fr0 sp0 base0 [A|B].
  injection A; intros; subst fr0; subst sp0; subst base0. auto.
  apply Zlt_trans with sp. eapply IHcallstack_dom; eauto. auto.
Qed.

Lemma callstack_dom_diff:
  forall cs b, callstack_dom cs b ->
  forall fr sp base, In (fr, sp, base) cs -> sp <> b.
Proof.
  intros. apply Zlt_not_eq. eapply callstack_dom_less; eauto.
Qed.

Lemma callstack_dom_incr:
  forall cs b, callstack_dom cs b ->
  forall b', b < b' -> callstack_dom cs b'.
Proof.
  induction 1; intros.
  apply callstack_dom_nil.
  apply callstack_dom_cons. omega. auto.
Qed.

(** Every block reference is either ``in'' a call stack (that is,
  refers to the stack block of one of the calls) or  ``not in''
  a call stack (that is, differs from all the stack blocks). *)

Inductive notin_callstack: block -> callstack -> Prop :=
  | notin_callstack_nil:
      forall b, notin_callstack b nil
  | notin_callstack_cons:
      forall b fr sp base cs,
      b <> sp ->
      notin_callstack b cs ->
      notin_callstack b ((fr, sp, base) :: cs).

Lemma in_or_notin_callstack:
  forall b cs,
  (exists fr, exists base, In (fr, b, base) cs) \/ notin_callstack b cs.
Proof.
  induction cs.
  right; constructor.
  elim IHcs. 
  intros [fr [base IN]]. left. exists fr; exists base; auto with coqlib.
  intro NOTIN. destruct a. destruct p. case (eq_block b b0); intro.
  left. exists f; exists i. subst b0. auto with coqlib.
  right. apply notin_callstack_cons; auto.
Qed. 

(** [callstack_invariant cs mm ms] relates the memory state [mm]
  from the abstract semantics with the memory state [ms] from the
  concrete semantics, relative to the current call stack [cs].
  Five conditions are enforced:
- All frames in [cs] agree with the corresponding activation records
  (in the sense of [frame_match]).
- The frames in the call stack are properly linked.
- Memory blocks that are not activation records for active function
  calls are exactly identical in [mm] and [ms].
- The allocation pointers are the same in [mm] and [ms].
- The call stack [cs] is ``dominated'' by this allocation pointer,
  implying that all activation records are valid, allocated blocks,
  pairwise disjoint, and they were allocated in the order implied
  by [cs]. *)

Record callstack_invariant (cs: callstack) (mm ms: mem) : Prop :=
  mk_callstack_invariant {
    cs_frame:
      forall fr sp base,
      In (fr, sp, base) cs -> frame_match fr sp base mm ms;
    cs_linked:
      callstack_linked cs;
    cs_others:
      forall b, notin_callstack b cs ->
            mm.(blocks) b = ms.(blocks) b;
    cs_next:
      mm.(nextblock) = ms.(nextblock);
    cs_dom:
      callstack_dom cs ms.(nextblock)
  }.

(** Again, while [callstack_invariant] is presented as a relation,
  it actually fully determines the concrete memory state [ms]
  from the abstract memory state [mm] and the call stack [cs]. *)

Lemma callstack_exten:
  forall cs mm ms1 ms2,
  callstack_invariant cs mm ms1 ->
  callstack_invariant cs mm ms2 ->
  ms1 = ms2.
Proof.
  intros. inversion H; inversion H0. 
  apply mem_exten.
  congruence. 
  intros. elim (in_or_notin_callstack b cs).
  intros [fr [base FM]]. apply frame_match_exten with fr base mm; auto.
  intro. transitivity (blocks mm b).
  symmetry. auto. auto.
Qed.

(** The following properties of [callstack_invariant] are the
  building blocks for the proof of simulation.  First, a [get_slot]
  operation in the abstract semantics corresponds to a [sp]-relative
  memory load in the concrete semantics. *)

Lemma callstack_get_slot:
  forall fr sp base cs mm ms ty ofs v,
  callstack_invariant ((fr, sp, base) :: cs) mm ms ->
  get_slot fr ty (Int.signed ofs) v ->
  Val.has_type v ty ->
  load_stack ms (Vptr sp base) ty ofs = Some v.
Proof.
  intros. inversion H. 
  apply frame_match_get_slot with fr mm. 
  apply cs_frame0. apply in_eq.
  auto. auto.
Qed.

(** Similarly, a [get_parent] operation corresponds to loading
  the back-link from the current activation record, then loading
  from this back-link. *)

Lemma callstack_get_parent:
  forall fr1 sp1 base1 fr2 sp2 base2 cs mm ms ty ofs v,
  callstack_invariant ((fr1, sp1, base1) :: (fr2, sp2, base2) :: cs) mm ms ->
  get_slot fr2 ty (Int.signed ofs) v ->
  Val.has_type v ty ->
  load_stack ms (Vptr sp1 base1) Tint (Int.repr 0) = Some (Vptr sp2 base2) /\
  load_stack ms (Vptr sp2 base2) ty ofs = Some v.
Proof.
  intros. inversion H. split.
  inversion cs_linked0. 
  apply frame_match_get_slot with fr1 mm.
  apply cs_frame0. auto with coqlib.
  rewrite Int.signed_repr. auto. compute. intuition congruence.
  exact I.
  apply frame_match_get_slot with fr2 mm. 
  apply cs_frame0. auto with coqlib.
  auto. auto.
Qed.

(** A memory load valid in the abstract semantics can also be performed
  in the concrete semantics. *)

Lemma callstack_load:
  forall cs chunk mm ms a v,
  callstack_invariant cs mm ms ->
  loadv chunk mm a = Some v ->
  loadv chunk ms a = Some v.
Proof.
  unfold loadv. intros. destruct a; try discriminate.
  inversion H.
  elim (in_or_notin_callstack b cs).
  intros [fr [base IN]]. apply frame_match_load with fr base mm; auto.
  intro. rewrite <- H0. unfold load. 
  rewrite (cs_others0 b H1). rewrite cs_next0. reflexivity.
Qed.

(** A [set_slot] operation in the abstract semantics corresponds
  to a [sp]-relative memory store in the concrete semantics.
  Moreover, the property [callstack_invariant] still holds for
  the final call stacks and memory states. *)

Lemma callstack_set_slot:
  forall fr sp base cs mm ms ty ofs v fr',
  callstack_invariant ((fr, sp, base) :: cs) mm ms ->
  set_slot fr ty (Int.signed ofs) v fr' ->
  4 <= Int.signed ofs ->
  exists ms',
    store_stack ms (Vptr sp base) ty ofs v = Some ms' /\
    callstack_invariant ((fr', sp, base) :: cs) mm ms'.
Proof.
  intros. inversion H.
  assert (frame_match fr sp base mm ms). apply cs_frame0. apply in_eq.
  generalize (frame_match_set_slot _ _ _ _ _ _ _ _ _ H2 H0).
  intros [ms' [SS FM]].
  generalize (store_inv _ _ _ _ _ _ SS). intros [A [B [C [D [x E]]]]].
  exists ms'.
  split. auto.
  constructor.
  (* cs_frame *)
  intros. elim H3; intros. 
  injection H4; intros; clear H4. 
  subst fr0; subst sp0; subst base0. auto.
  apply frame_match_store_stack_other with ms sp base ty ofs v.
  apply cs_frame0. auto with coqlib. auto. 
  apply callstack_dom_diff with cs fr0 base0. inversion cs_dom0; auto. auto.
  (* cs_linked *)
  inversion cs_linked0. apply callstack_linked_one.
  apply callstack_linked_cons. 
  eapply slot_gso; eauto.
  auto.
  (* cs_others *)
  intros. inversion H3. 
  rewrite E; simpl. rewrite update_o; auto. apply cs_others0.
  constructor; auto.
  (* cs_next *)
  congruence.
  (* cs_dom *)
  inversion cs_dom0. constructor. rewrite D; auto. auto.
Qed.

(** A memory store in the abstract semantics can also be performed
  in the concrete semantics.  Moreover, the property
  [callstack_invariant] is preserved. *)

Lemma callstack_store_aux:
  forall cs mm ms chunk b ofs v mm' ms',
  callstack_invariant cs mm ms ->
  store chunk mm b ofs v = Some mm' ->
  store chunk ms b ofs v = Some ms' ->
  callstack_invariant cs mm' ms'.
Proof.
  intros. inversion H.
  generalize (store_inv _ _ _ _ _ _ H0). intros [A [B [C [D [x E]]]]].
  generalize (store_inv _ _ _ _ _ _ H1). intros [P [Q [R [S [y T]]]]].
  constructor; auto.
  (* cs_frame *)
  intros. eapply frame_match_store; eauto.
  (* cs_others *)
  intros. generalize (cs_others0 b0 H2); intro.
  rewrite E; rewrite T; unfold update.
  case (zeq b0 b); intro.
  subst b0. 
  generalize x; generalize y. rewrite H3. 
  intros. replace y0 with x0. reflexivity. apply proof_irrelevance.
  auto.
  (* cs_nextblock *)
  congruence.
  (* cs_dom *)
  rewrite S. auto.
Qed.

Lemma callstack_store_ok:
  forall cs mm ms chunk b ofs v mm',
  callstack_invariant cs mm ms ->
  store chunk mm b ofs v = Some mm' ->
  exists ms', store chunk ms b ofs v = Some ms'.
Proof.
  intros. inversion H.
  elim (in_or_notin_callstack b cs).
  intros [fr [base IN]].
  apply frame_match_store_ok with fr base mm mm'; auto.
  intro. generalize (cs_others0 b H1). intro.
  generalize (store_inv _ _ _ _ _ _ H0). 
  rewrite cs_next0; rewrite H2. intros [A [B [C [D [x E]]]]].
  apply store_in_bounds; auto.
Qed.

Lemma callstack_store:
  forall cs mm ms chunk a v mm',
  callstack_invariant cs mm ms ->
  storev chunk mm a v = Some mm' ->
  exists ms',
    storev chunk ms a v = Some ms' /\
    callstack_invariant cs mm' ms'.
Proof.
  unfold storev; intros. destruct a; try discriminate.
  generalize (callstack_store_ok _ _ _ _ _ _ _ _ H H0).
  intros [ms' STORE].
  exists ms'. split. auto. eapply callstack_store_aux; eauto.
Qed.

(** Allocations of heap blocks can be performed in parallel in
    both semantics, preserving [callstack_invariant]. *)

Lemma callstack_alloc:
  forall cs mm ms lo hi mm' blk,
  callstack_invariant cs mm ms ->
  Mem.alloc mm lo hi = (mm', blk) ->
  exists ms',
    Mem.alloc ms lo hi = (ms', blk) /\
    callstack_invariant cs mm' ms'.
Proof.
  intros. inversion H. 
  caseEq (alloc ms lo hi). intros ms' blk' ALLOC'.
  injection H0; intros. injection ALLOC'; intros.
  assert (blk' = blk). congruence. rewrite H5 in H3. rewrite H5. 
  exists ms'; split. auto.
  constructor. 
  (* frame *)
  intros; eapply frame_match_alloc; eauto.
  (* linked *)
  auto.
  (* others *)
  intros. rewrite <- H2; rewrite <- H4; simpl.
  rewrite H1; rewrite H3. unfold update. case (zeq b blk); auto.
  (* next *)
  rewrite <- H2; rewrite <- H4; simpl; congruence.
  (* dom *)
  eapply callstack_dom_incr; eauto. rewrite <- H4; simpl. omega.
Qed.

(** At function entry, a new frame is pushed on the call stack,
  and memory blocks are allocated in both semantics.  Moreover,
  the back link to the caller's activation record is set up
  in the concrete semantics.  All this preserves [callstack_invariant]. *)

Lemma callstack_function_entry:
  forall fr0 sp0 base0 cs mm ms f fr mm' sp ms' sp',
  callstack_invariant ((fr0, sp0, base0) :: cs) mm ms ->
  alloc mm 0 f.(fn_stacksize) = (mm', sp) ->
  alloc ms (- f.(fn_framesize)) (align_16_top (- f.(fn_framesize)) f.(fn_stacksize)) = (ms', sp') ->
  f.(fn_framesize) >= 0 ->
  f.(fn_framesize) <= -Int.min_signed ->
  set_slot (init_frame f) Tint 0 (Vptr sp0 base0) fr ->
  let base := Int.repr (-f.(fn_framesize)) in
  exists ms'',
     store_stack ms' (Vptr sp base) Tint (Int.repr 0) (Vptr sp0 base0) = Some ms''
  /\ callstack_invariant ((fr, sp, base) :: (fr0, sp0, base0) :: cs) mm' ms''
  /\ sp' = sp.
Proof.
  assert (ZERO: 0 = Int.signed (Int.repr 0)).
    rewrite Int.signed_repr. auto. compute; intuition congruence.
  intros. inversion H.
  injection H0; intros. injection H1; intros.
  assert (sp' = sp). congruence. rewrite H9 in H7. subst sp'.
  assert (frame_match (init_frame f) sp base mm' ms').
    unfold base. eapply frame_match_new; eauto.
  rewrite ZERO in H4.
  generalize (frame_match_set_slot _ _ _ _ _ _ _ _ _ H9 H4).
  intros [ms'' [SS FM]].
  generalize (store_inv _ _ _ _ _ _ SS).  
  intros [A [B [C [D [x E]]]]].
  exists ms''. split; auto. split.
  constructor.
  (* cs_frame *)
  intros. elim H10; intro.
  injection H11; intros; clear H11.
  subst fr1; subst sp1; subst base1. auto.
  eapply frame_match_store_stack_other; eauto.
  eapply frame_match_alloc; [idtac|idtac|eexact H0|eexact H1].
  congruence. eapply cs_frame; eauto with coqlib. 
  rewrite <- H7. eapply callstack_dom_diff; eauto with coqlib.
  (* cs_linked *)
  constructor. rewrite ZERO. eapply slot_gss; eauto. auto.
  (* cs_others *)
  intros. inversion H10. 
  rewrite E; rewrite update_o; auto. 
  rewrite <- H6; rewrite <- H8; simpl; rewrite H5; rewrite H7; simpl. 
  repeat (rewrite update_o; auto). 
  (* cs_next *)
  rewrite D. rewrite <- H6; rewrite <- H8; simpl. congruence.
  (* cs_dom *)
  constructor. rewrite D; auto. rewrite <- H7. auto.
  auto.
Qed.

(** At function return, the memory blocks corresponding to Cminor
  stack data and activation record for the function are freed.
  This preserves [callstack_invariant]. *)

Lemma callstack_function_return:
  forall fr sp base cs mm ms,
  callstack_invariant ((fr, sp, base) :: cs) mm ms ->
  callstack_invariant cs (free mm sp) (free ms sp).
Proof.
  intros. inversion H. inversion cs_dom0.
  constructor.
  (* cs_frame *)
  intros. apply frame_match_free. apply cs_frame0; auto with coqlib.
  apply callstack_dom_diff with cs fr1 base1. auto. auto.
  (* cs_linked *)
  inversion cs_linked0. apply callstack_linked_nil. auto.
  (* cs_others *)
  intros. 
  unfold free; simpl; unfold update.
  case (zeq b0 sp); intro.
  auto.
  apply cs_others0. apply notin_callstack_cons; auto.
  (* cs_nextblock *)
  simpl. auto.
  (* cs_dom *)
  simpl. apply callstack_dom_incr with sp; auto.
Qed.

(** Finally, [callstack_invariant] holds for the initial memory states
  in the two semantics. *)

Lemma callstack_init:
  forall (p: program),
  callstack_invariant ((empty_frame, nullptr, Int.zero) :: nil) 
                      (Genv.init_mem p) (Genv.init_mem p).
Proof.
  intros.
  generalize (Genv.initmem_nullptr p). intros [A B].
  constructor.
  (* cs_frame *)
  intros. elim H; intro.
  injection H0; intros; subst fr; subst sp; subst base.
  constructor.
  assumption.
  unfold low_bound. rewrite B. reflexivity.
  unfold low_bound, empty_frame. rewrite B. reflexivity.
  unfold high_bound. rewrite B. reflexivity.
  simpl. omega.
  simpl. compute. intuition congruence.
  reflexivity.
  rewrite B. unfold empty_frame. simpl. hnf. auto.
  rewrite B. hnf. auto.
  elim H0.
  (* cs_linked *)
  apply callstack_linked_one.
  (* cs_others *)
  auto.
  (* cs_nextblock *)
  reflexivity.
  (* cs_dom *)
  constructor. exact A. constructor.
Qed.

(** * The proof of simulation *)

Section SIMULATION.

Variable p: program.
Hypothesis wt_p: wt_program p.
Let ge := Genv.globalenv p.

(** The proof of simulation relies on diagrams of the following form:
<<
     sp, parent, c, rs, fr, mm ----------- sp, c, rs, ms
                 |                              |
                 |                              |
                 v                              v
   sp, parent, c', rs', fr', mm' --------  sp, c', rs', ms'
>>
  The left vertical arrow is a transition in the abstract semantics.
  The right vertical arrow is a transition in the concrete semantics.
  The precondition (top horizontal line) is the appropriate
  [callstack_invariant] property between the initial memory states
  [mm] and [ms] and any call stack with [fr] as top frame and
  [parent] as second frame.  In addition, well-typedness conditions
  over the code [c], the register [rs] and the frame [fr] are demanded.
  The postcondition (bottom horizontal line) is [callstack_invariant]
  between the final memory states [mm'] and [ms'] and the final
  call stack.
*)

Definition exec_instr_prop
    (f: function) (sp: val) (parent: frame)
    (c: code) (rs: regset) (fr: frame) (mm: mem) (t: trace)
    (c': code) (rs': regset) (fr': frame) (mm': mem) : Prop :=
  forall ms stk base pstk pbase cs
         (WTF: wt_function f)
         (INCL: incl c f.(fn_code))
         (WTRS: wt_regset rs)
         (WTFR: wt_frame fr)
         (WTPA: wt_frame parent)
         (CSI: callstack_invariant ((fr, stk, base) :: (parent, pstk, pbase) :: cs) mm ms)
         (SP: sp = Vptr stk base),
  exists ms',
    exec_instr ge f sp c rs ms t c' rs' ms' /\
    callstack_invariant ((fr', stk, base) :: (parent, pstk, pbase) :: cs) mm' ms'.

Definition exec_instrs_prop
    (f: function) (sp: val) (parent: frame)
    (c: code) (rs: regset) (fr: frame) (mm: mem) (t: trace)
    (c': code) (rs': regset) (fr': frame) (mm': mem) : Prop :=
  forall ms stk base pstk pbase cs
         (WTF: wt_function f)
         (INCL: incl c f.(fn_code))
         (WTRS: wt_regset rs)
         (WTFR: wt_frame fr)
         (WTPA: wt_frame parent)
         (CSI: callstack_invariant ((fr, stk, base) :: (parent, pstk, pbase) :: cs) mm ms)
         (SP: sp = Vptr stk base),
  exists ms',
    exec_instrs ge f sp c rs ms t c' rs' ms' /\
    callstack_invariant ((fr', stk, base) :: (parent, pstk, pbase) :: cs) mm' ms'.

Definition exec_function_body_prop
    (f: function) (parent: frame) (link ra: val)
    (rs: regset) (mm: mem) (t: trace)
    (rs': regset) (mm': mem) : Prop :=
  forall ms pstk pbase cs
         (WTF: wt_function f)
         (WTRS: wt_regset rs)
         (WTPA: wt_frame parent)
         (WTRA: Val.has_type ra Tint)
         (LINK: link = Vptr pstk pbase)
         (CSI: callstack_invariant ((parent, pstk, pbase) :: cs) mm ms),
  exists ms',
    exec_function_body ge f (Vptr pstk pbase) ra rs ms t rs' ms' /\
    callstack_invariant ((parent, pstk, pbase) :: cs) mm' ms'.

Definition exec_function_prop
    (f: fundef) (parent: frame)
    (rs: regset) (mm: mem) (t: trace)
    (rs': regset) (mm': mem) : Prop :=
  forall ms pstk pbase cs
         (WTF: wt_fundef f)
         (WTRS: wt_regset rs)
         (WTPA: wt_frame parent)
         (CSI: callstack_invariant ((parent, pstk, pbase) :: cs) mm ms),
  exists ms',
    exec_function ge f (Vptr pstk pbase) rs ms t rs' ms' /\
    callstack_invariant ((parent, pstk, pbase) :: cs) mm' ms'.

Lemma exec_function_equiv:
  forall f parent rs mm t rs' mm',
  Machabstr.exec_function ge f parent rs mm t rs' mm' ->
  exec_function_prop f parent rs mm t rs' mm'.
Proof.
  apply (Machabstr.exec_function_ind4 ge
           exec_instr_prop
           exec_instrs_prop
           exec_function_body_prop
           exec_function_prop);
  intros; red; intros.

  (* Mlabel *)
  exists ms. split. constructor. auto.
  (* Mgetstack *)
  exists ms. split. 
  constructor. rewrite SP. eapply callstack_get_slot; eauto. 
  apply wt_get_slot with fr (Int.signed ofs); auto.
  auto.
  (* Msetstack *)
  generalize (wt_function_instrs f WTF _ (INCL _ (in_eq _ _))).
  intro WTI. inversion WTI.
  assert (4 <= Int.signed ofs). omega. 
  generalize (callstack_set_slot _ _ _ _ _ _ _ _ _ _ CSI H H5).
  intros [ms' [STO CSI']].
  exists ms'. split. constructor. rewrite SP. auto. auto.
  (* Mgetparam *)
  exists ms. split. 
  assert (WTV: Val.has_type v ty). eapply wt_get_slot; eauto.
  generalize (callstack_get_parent _ _ _ _ _ _ _ _ _ _ _ _
                CSI H WTV).
  intros [L1 L2].
  eapply exec_Mgetparam. rewrite SP; eexact L1. eexact L2.
  auto.
  (* Mop *)
  exists ms. split. constructor. auto. auto.
  (* Mload *)
  exists ms. split. econstructor. eauto. eapply callstack_load; eauto.
  auto.
  (* Mstore *)
  generalize (callstack_store _ _ _ _ _ _ _ CSI H0).
  intros [ms' [STO CSI']].
  exists ms'. split. econstructor. eauto. auto.
  auto. 
  (* Mcall *)
  red in H1. 
  assert (WTF': wt_fundef f').
    destruct ros; simpl in H.
    apply (Genv.find_funct_prop wt_fundef wt_p H).
    destruct (Genv.find_symbol ge i); try discriminate.
    apply (Genv.find_funct_ptr_prop wt_fundef wt_p H).
  generalize (H1 _ _ _ _ WTF' WTRS WTFR CSI). 
  intros [ms' [EXF CSI']].
  exists ms'. split. apply exec_Mcall with f'; auto. 
  rewrite SP. auto.
  auto.
  (* Malloc *)
  generalize (callstack_alloc _ _ _ _ _ _ _ CSI H0). 
  intros [ms' [ALLOC' CSI']].
  exists ms'; split.
  eapply exec_Malloc; eauto.
  auto.
  (* Mgoto *)
  exists ms. split. constructor; auto. auto.
  (* Mcond *)
  exists ms. split. apply exec_Mcond_true; auto. auto.
  exists ms. split. apply exec_Mcond_false; auto. auto.

  (* refl *)
  exists ms. split. apply exec_refl. auto.
  (* one *)
  generalize (H0 _ _ _ _ _ _ WTF INCL WTRS WTFR WTPA CSI SP).
  intros [ms' [EX CSI']].
  exists ms'. split. apply exec_one; auto. auto.
  (* trans *)
  generalize (subject_reduction_instrs p wt_p 
               _ _ _ _ _ _ _ _ _ _ _ _ H WTF INCL WTRS WTFR WTPA).
  intros [INCL2 [WTRS2 WTFR2]].
  generalize (H0 _ _ _ _ _ _ WTF INCL WTRS WTFR WTPA CSI SP).
  intros [ms1 [EX1 CSI1]].
  generalize (H2 _ _ _ _ _ _ WTF INCL2 WTRS2 WTFR2 WTPA CSI1 SP).
  intros [ms2 [EX2 CSI2]].
  exists ms2. split. eapply exec_trans; eauto. auto.

  (* function body *)
  caseEq (alloc ms (- f.(fn_framesize))
                   (align_16_top (- f.(fn_framesize)) f.(fn_stacksize))).
  intros ms1 stk1 ALL.
  subst link.
  assert (FS: f.(fn_framesize) >= 0).
    generalize (wt_function_framesize f WTF). omega.
  generalize (callstack_function_entry _ _ _ _ _ _ _ _ _ _ _ _
               CSI H ALL FS
               (wt_function_no_overflow f WTF) H0).
  intros [ms2 [STORELINK [CSI2 EQ]]].
  subst stk1.
  assert (ZERO: Int.signed (Int.repr 0) = 0). reflexivity.
  assert (FOUR: Int.signed (Int.repr 4) = 4). reflexivity.
  assert (BND: 4 <= Int.signed (Int.repr 4)).
    rewrite FOUR; omega.
  rewrite <- FOUR in H1.
  generalize (callstack_set_slot _ _ _ _ _ _ _ _ _ _
               CSI2 H1 BND).
  intros [ms3 [STORERA CSI3]].
  assert (WTFR2: wt_frame fr2).
    eapply wt_set_slot; eauto. eapply wt_set_slot; eauto.
    red. intros. simpl. auto. 
    exact I. 
  red in H3.
  generalize (H3 _ _ _ _ _ _ WTF (incl_refl _) WTRS WTFR2 WTPA
                CSI3 (refl_equal _)).
  intros [ms4 [EXEC CSI4]].
  generalize (exec_instrs_link_invariant _ _ _ _ _ _ _ _ _ _ _ _ _
                H2 WTF (incl_refl _)).
  intros [INCL LINKINV].
  exists (free ms4 stk). split.
  eapply exec_funct_body; eauto.
  eapply callstack_get_slot. eexact CSI4.
  apply LINKINV. rewrite ZERO. omega. 
  eapply slot_gso; eauto. rewrite ZERO. eapply slot_gss; eauto. 
  exact I. 
  eapply callstack_get_slot. eexact CSI4.
  apply LINKINV. rewrite FOUR. omega. eapply slot_gss; eauto. auto.
  eapply callstack_function_return; eauto.

  (* internal function *)
  inversion WTF. subst f0. 
  generalize (H0 (Vptr pstk pbase) Vzero I I
                 ms pstk pbase cs H2 WTRS WTPA I (refl_equal _) CSI).
  intros [ms' [EXEC CSI']].
  exists ms'. split. constructor. intros.
  generalize (H0 (Vptr pstk pbase) ra I H1 
                ms pstk pbase cs H2 WTRS WTPA H1 (refl_equal _) CSI).
  intros [ms1 [EXEC1 CSI1]].
  rewrite (callstack_exten _ _ _ _ CSI' CSI1). auto.
  auto.

  (* external function *)
  exists ms; split. econstructor; eauto. auto.
Qed.  

End SIMULATION.

Theorem exec_program_equiv:
  forall p t r, 
  wt_program p ->
  Machabstr.exec_program p t r -> 
  Mach.exec_program p t r.
Proof.
  intros p t r WTP [fptr [f [rs [mm [FINDPTR [FINDF [EXEC RES]]]]]]].
  assert (WTF: wt_fundef f).
    apply (Genv.find_funct_ptr_prop wt_fundef WTP FINDF).
  assert (WTRS: wt_regset (Regmap.init Vundef)).
    red; intros. rewrite Regmap.gi; simpl; auto.
  assert (WTFR: wt_frame empty_frame).
    red; intros. simpl. auto.
  generalize (exec_function_equiv p WTP
                f empty_frame
                (Regmap.init Vundef) (Genv.init_mem p) t rs mm
                EXEC (Genv.init_mem p) nullptr Int.zero nil
                WTF WTRS WTFR (callstack_init p)).
  intros [ms' [EXEC' CSI]].
  red. exists fptr; exists f; exists rs; exists ms'. tauto.
Qed.