Require Import String.
Require Import Coqlib.
Require Intv.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.

Inductive eventval: Type :=
  | EVint: int → eventval
  | EVlong: int64 → eventval
  | EVfloat: float → eventval
  | EVsingle: float32 → eventval
  | EVptr_global: ident → ptrofs → eventval.

Inductive event: Type :=
  | Event_syscall: string → list eventval → eventval → event
  | Event_vload: memory_chunk → ident → ptrofs → eventval → event
  | Event_vstore: memory_chunk → ident → ptrofs → eventval → event
  | Event_annot: string → list eventval → event.

Definition trace := list event.

Definition E0 : trace := nil.

Definition Eapp (t1 t2: trace) : trace := t1 ++ t2.

CoInductive traceinf : Type :=
  | Econsinf: event → traceinf → traceinf.

Fixpoint Eappinf (t: trace) (T: traceinf) {struct t} : traceinf :=
  match t with
  | nil ⇒ T
  | ev :: t' ⇒ Econsinf ev (Eappinf t' T)
  end.

Infix "**" := Eapp (at level 60, right associativity).
Infix "***" := Eappinf (at level 60, right associativity).

Lemma E0_left: ∀ t, E0 ** t = t.
Proof. auto. Qed.

Lemma E0_right: ∀ t, t ** E0 = t.
Proof. intros. unfold E0, Eapp. rewrite <- app_nil_end. auto. Qed.

Lemma Eapp_assoc: ∀ t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3).
Proof. intros. unfold Eapp, trace. apply app_ass. Qed.

Lemma Eapp_E0_inv: ∀ t1 t2, t1 ** t2 = E0 → t1 = E0 ∧ t2 = E0.
Proof (@app_eq_nil event).

Lemma E0_left_inf: ∀ T, E0 *** T = T.
Proof. auto. Qed.

Lemma Eappinf_assoc: ∀ t1 t2 T, (t1 ** t2) *** T = t1 *** (t2 *** T).
Proof.
  induction t1; intros; simpl. auto. decEq; auto.
Qed.

Hint Rewrite E0_left E0_right Eapp_assoc
             E0_left_inf Eappinf_assoc: trace_rewrite.

Opaque trace E0 Eapp Eappinf.

Ltac substTraceHyp :=
  match goal with
  | [ H: (@eq trace ?x ?y) |- _ ] ⇒
       subst x || clear H
  end.

Ltac decomposeTraceEq :=
  match goal with
  | [ |- (_ ** _) = (_ ** _) ] ⇒
      apply (f_equal2 Eapp); auto; decomposeTraceEq
  | _ ⇒
      auto
  end.

Ltac traceEq :=
  repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq.

CoInductive traceinf_sim: traceinf → traceinf → Prop :=
  | traceinf_sim_cons: ∀ e T1 T2,
      traceinf_sim T1 T2 →
      traceinf_sim (Econsinf e T1) (Econsinf e T2).

Lemma traceinf_sim_refl:
  ∀ T, traceinf_sim T T.
Proof.
  cofix COINDHYP; intros.
  destruct T. constructor. apply COINDHYP.
Qed.

Lemma traceinf_sim_sym:
  ∀ T1 T2, traceinf_sim T1 T2 → traceinf_sim T2 T1.
Proof.
  cofix COINDHYP; intros. inv H; constructor; auto.
Qed.

Lemma traceinf_sim_trans:
  ∀ T1 T2 T3,
  traceinf_sim T1 T2 → traceinf_sim T2 T3 → traceinf_sim T1 T3.
Proof.
  cofix COINDHYP;intros. inv H; inv H0; constructor; eauto.
Qed.

CoInductive traceinf_sim': traceinf → traceinf → Prop :=
  | traceinf_sim'_cons: ∀ t T1 T2,
      t ≠ E0 → traceinf_sim' T1 T2 → traceinf_sim' (t *** T1) (t *** T2).

Lemma traceinf_sim'_sim:
  ∀ T1 T2, traceinf_sim' T1 T2 → traceinf_sim T1 T2.
Proof.
  cofix COINDHYP; intros. inv H.
  destruct t. elim H0; auto.
Transparent Eappinf.
Transparent E0.
  simpl.
  destruct t. simpl. constructor. apply COINDHYP; auto.
  constructor. apply COINDHYP.
  constructor. unfold E0; congruence. auto.
Qed.

CoInductive traceinf': Type :=
  | Econsinf': ∀ (t: trace) (T: traceinf'), t ≠ E0 → traceinf'.

Program Definition split_traceinf' (t: trace) (T: traceinf') (NE: t ≠ E0): event × traceinf' :=
  match t with
  | nil ⇒ _
  | e :: nil ⇒ (e, T)
  | e :: t' ⇒ (e, Econsinf' t' T _)
  end.
Next Obligation.
  elimtype False. elim NE. auto.
Qed.
Next Obligation.
  red; intro. elim (H e). rewrite H0. auto.
Qed.

CoFixpoint traceinf_of_traceinf' (T': traceinf') : traceinf :=
  match T' with
  | Econsinf' t T'' NOTEMPTY ⇒
      let (e, tl) := split_traceinf' t T'' NOTEMPTY in
      Econsinf e (traceinf_of_traceinf' tl)
  end.

Remark unroll_traceinf':
  ∀ T, T = match T with Econsinf' t T' NE ⇒ Econsinf' t T' NE end.
Proof.
  intros. destruct T; auto.
Qed.

Remark unroll_traceinf:
  ∀ T, T = match T with Econsinf t T' ⇒ Econsinf t T' end.
Proof.
  intros. destruct T; auto.
Qed.

Lemma traceinf_traceinf'_app:
  ∀ t T NE,
  traceinf_of_traceinf' (Econsinf' t T NE) = t *** traceinf_of_traceinf' T.
Proof.
  induction t.
  intros. elim NE. auto.
  intros. simpl.
  rewrite (unroll_traceinf (traceinf_of_traceinf' (Econsinf' (a :: t) T NE))).
  simpl. destruct t. auto.
Transparent Eappinf.
  simpl. f_equal. apply IHt.
Qed.

Definition trace_prefix (t1 t2: trace) :=
  ∃ t3, t2 = t1 ** t3.

Definition traceinf_prefix (t1: trace) (T2: traceinf) :=
  ∃ T3, T2 = t1 *** T3.

Lemma trace_prefix_app:
  ∀ t1 t2 t,
  trace_prefix t1 t2 →
  trace_prefix (t ** t1) (t ** t2).
Proof.
  intros. destruct H as [t3 EQ]. ∃ t3. traceEq.
Qed.

Lemma traceinf_prefix_app:
  ∀ t1 T2 t,
  traceinf_prefix t1 T2 →
  traceinf_prefix (t ** t1) (t *** T2).
Proof.
  intros. destruct H as [T3 EQ]. ∃ T3. subst T2. traceEq.
Qed.

Set Implicit Arguments.

Section EVENTVAL.

Variable ge: Senv.t.

Inductive eventval_match: eventval → typ → val → Prop :=
  | ev_match_int: ∀ i,
      eventval_match (EVint i) Tint (Vint i)
  | ev_match_long: ∀ i,
      eventval_match (EVlong i) Tlong (Vlong i)
  | ev_match_float: ∀ f,
      eventval_match (EVfloat f) Tfloat (Vfloat f)
  | ev_match_single: ∀ f,
      eventval_match (EVsingle f) Tsingle (Vsingle f)
  | ev_match_ptr: ∀ id b ofs,
      Senv.public_symbol ge id = true →
      Senv.find_symbol ge id = Some b →
      eventval_match (EVptr_global id ofs) Tptr (Vptr b ofs).

Inductive eventval_list_match: list eventval → list typ → list val → Prop :=
  | evl_match_nil:
      eventval_list_match nil nil nil
  | evl_match_cons:
      ∀ ev1 evl ty1 tyl v1 vl,
      eventval_match ev1 ty1 v1 →
      eventval_list_match evl tyl vl →
      eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl).

Lemma eventval_match_type:
  ∀ ev ty v,
  eventval_match ev ty v → Val.has_type v ty.
Proof.
  intros. inv H; simpl; auto. unfold Tptr; destruct Archi.ptr64; auto.
Qed.

Lemma eventval_list_match_length:
  ∀ evl tyl vl, eventval_list_match evl tyl vl → List.length vl = List.length tyl.
Proof.
  induction 1; simpl; eauto.
Qed.

Lemma eventval_match_lessdef:
  ∀ ev ty v1 v2,
  eventval_match ev ty v1 → Val.lessdef v1 v2 → eventval_match ev ty v2.
Proof.
  intros. inv H; inv H0; constructor; auto.
Qed.

Lemma eventval_list_match_lessdef:
  ∀ evl tyl vl1, eventval_list_match evl tyl vl1 →
  ∀ vl2, Val.lessdef_list vl1 vl2 → eventval_list_match evl tyl vl2.
Proof.
  induction 1; intros. inv H; constructor.
  inv H1. constructor. eapply eventval_match_lessdef; eauto. eauto.
Qed.

Lemma eventval_match_determ_1:
  ∀ ev ty v1 v2, eventval_match ev ty v1 → eventval_match ev ty v2 → v1 = v2.
Proof.
  intros. inv H; inv H0; auto. congruence.
Qed.

Lemma eventval_match_determ_2:
  ∀ ev1 ev2 ty v, eventval_match ev1 ty v → eventval_match ev2 ty v → ev1 = ev2.
Proof.
  intros. inv H; inv H0; auto.
  decEq. eapply Senv.find_symbol_injective; eauto.
Qed.

Lemma eventval_list_match_determ_2:
  ∀ evl1 tyl vl, eventval_list_match evl1 tyl vl →
  ∀ evl2, eventval_list_match evl2 tyl vl → evl1 = evl2.
Proof.
  induction 1; intros. inv H. auto. inv H1. f_equal; eauto.
  eapply eventval_match_determ_2; eauto.
Qed.

Definition eventval_valid (ev: eventval) : Prop :=
  match ev with
  | EVint _ ⇒ True
  | EVlong _ ⇒ True
  | EVfloat _ ⇒ True
  | EVsingle _ ⇒ True
  | EVptr_global id ofs ⇒ Senv.public_symbol ge id = true
  end.

Definition eventval_type (ev: eventval) : typ :=
  match ev with
  | EVint _ ⇒ Tint
  | EVlong _ ⇒ Tlong
  | EVfloat _ ⇒ Tfloat
  | EVsingle _ ⇒ Tsingle
  | EVptr_global id ofs ⇒ Tptr
  end.

Lemma eventval_match_receptive:
  ∀ ev1 ty v1 ev2,
  eventval_match ev1 ty v1 →
  eventval_valid ev1 → eventval_valid ev2 → eventval_type ev1 = eventval_type ev2 →
  ∃ v2, eventval_match ev2 ty v2.
Proof.
  intros. unfold eventval_type, Tptr in H2. remember Archi.ptr64 as ptr64.
  inversion H; subst ev1 ty v1; clear H; destruct ev2; simpl in H2; inv H2.
- ∃ (Vint i0); constructor.
- simpl in H1; exploit Senv.public_symbol_exists; eauto. intros [b FS].
  ∃ (Vptr b i1); rewrite H3. constructor; auto.
- ∃ (Vlong i0); constructor.
- simpl in H1; exploit Senv.public_symbol_exists; eauto. intros [b FS].
  ∃ (Vptr b i1); rewrite H3; constructor; auto.
- ∃ (Vfloat f0); constructor.
- destruct Archi.ptr64; discriminate.
- ∃ (Vsingle f0); constructor; auto.
- destruct Archi.ptr64; discriminate.
- ∃ (Vint i); unfold Tptr; rewrite H5; constructor.
- ∃ (Vlong i); unfold Tptr; rewrite H5; constructor.
- destruct Archi.ptr64; discriminate.
- destruct Archi.ptr64; discriminate.
- exploit Senv.public_symbol_exists. eexact H1. intros [b' FS].
  ∃ (Vptr b' i0); constructor; auto.
Qed.

Lemma eventval_match_valid:
  ∀ ev ty v, eventval_match ev ty v → eventval_valid ev.
Proof.
  destruct 1; simpl; auto.
Qed.

Lemma eventval_match_same_type:
  ∀ ev1 ty v1 ev2 v2,
  eventval_match ev1 ty v1 → eventval_match ev2 ty v2 → eventval_type ev1 = eventval_type ev2.
Proof.
  destruct 1; intros EV; inv EV; auto.
Qed.

End EVENTVAL.

Section EVENTVAL_INV.

Variables ge1 ge2: Senv.t.

Hypothesis public_preserved:
  ∀ id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id.

Lemma eventval_valid_preserved:
  ∀ ev, eventval_valid ge1 ev → eventval_valid ge2 ev.
Proof.
  intros. destruct ev; simpl in *; auto. rewrite <- H; auto.
Qed.

Hypothesis symbols_preserved:
  ∀ id, Senv.find_symbol ge2 id = Senv.find_symbol ge1 id.

Lemma eventval_match_preserved:
  ∀ ev ty v,
  eventval_match ge1 ev ty v → eventval_match ge2 ev ty v.
Proof.
  induction 1; constructor; auto.
  rewrite public_preserved; auto.
  rewrite symbols_preserved; auto.
Qed.

Lemma eventval_list_match_preserved:
  ∀ evl tyl vl,
  eventval_list_match ge1 evl tyl vl → eventval_list_match ge2 evl tyl vl.
Proof.
  induction 1; constructor; auto. eapply eventval_match_preserved; eauto.
Qed.

End EVENTVAL_INV.

Section EVENTVAL_INJECT.

Variable f: block → option (block × Z).
Variable ge1 ge2: Senv.t.

Definition symbols_inject : Prop :=
   (∀ id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id)
∧ (∀ id b1 b2 delta,
     f b1 = Some(b2, delta) → Senv.find_symbol ge1 id = Some b1 →
     delta = 0 ∧ Senv.find_symbol ge2 id = Some b2)
∧ (∀ id b1,
     Senv.public_symbol ge1 id = true → Senv.find_symbol ge1 id = Some b1 →
     ∃ b2, f b1 = Some(b2, 0) ∧ Senv.find_symbol ge2 id = Some b2)
∧ (∀ b1 b2 delta,
     f b1 = Some(b2, delta) →
     Senv.block_is_volatile ge2 b2 = Senv.block_is_volatile ge1 b1).

Hypothesis symb_inj: symbols_inject.

Lemma eventval_match_inject:
  ∀ ev ty v1 v2,
  eventval_match ge1 ev ty v1 → Val.inject f v1 v2 → eventval_match ge2 ev ty v2.
Proof.
  intros. inv H; inv H0; try constructor; auto.
  destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ.
  rewrite Ptrofs.add_zero. constructor; auto. rewrite A; auto.
Qed.

Lemma eventval_match_inject_2:
  ∀ ev ty v1,
  eventval_match ge1 ev ty v1 →
  ∃ v2, eventval_match ge2 ev ty v2 ∧ Val.inject f v1 v2.
Proof.
  intros. inv H; try (econstructor; split; eauto; constructor; fail).
  destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]].
  ∃ (Vptr b2 ofs); split. econstructor; eauto.
  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
Qed.

Lemma eventval_list_match_inject:
  ∀ evl tyl vl1, eventval_list_match ge1 evl tyl vl1 →
  ∀ vl2, Val.inject_list f vl1 vl2 → eventval_list_match ge2 evl tyl vl2.
Proof.
  induction 1; intros. inv H; constructor.
  inv H1. constructor. eapply eventval_match_inject; eauto. eauto.
Qed.

End EVENTVAL_INJECT.

Section MATCH_TRACES.

Variable ge: Senv.t.

Inductive match_traces: trace → trace → Prop :=
  | match_traces_E0:
      match_traces nil nil
  | match_traces_syscall: ∀ id args res1 res2,
      eventval_valid ge res1 → eventval_valid ge res2 → eventval_type res1 = eventval_type res2 →
      match_traces (Event_syscall id args res1 :: nil) (Event_syscall id args res2 :: nil)
  | match_traces_vload: ∀ chunk id ofs res1 res2,
      eventval_valid ge res1 → eventval_valid ge res2 → eventval_type res1 = eventval_type res2 →
      match_traces (Event_vload chunk id ofs res1 :: nil) (Event_vload chunk id ofs res2 :: nil)
  | match_traces_vstore: ∀ chunk id ofs arg,
      match_traces (Event_vstore chunk id ofs arg :: nil) (Event_vstore chunk id ofs arg :: nil)
  | match_traces_annot: ∀ id args,
      match_traces (Event_annot id args :: nil) (Event_annot id args :: nil).

End MATCH_TRACES.

Section MATCH_TRACES_INV.

Variables ge1 ge2: Senv.t.

Hypothesis public_preserved:
  ∀ id, Senv.public_symbol ge2 id = Senv.public_symbol ge1 id.

Lemma match_traces_preserved:
  ∀ t1 t2, match_traces ge1 t1 t2 → match_traces ge2 t1 t2.
Proof.
  induction 1; constructor; auto; eapply eventval_valid_preserved; eauto.
Qed.

End MATCH_TRACES_INV.

Definition output_event (ev: event) : Prop :=
  match ev with
  | Event_syscall _ _ _ ⇒ False
  | Event_vload _ _ _ _ ⇒ False
  | Event_vstore _ _ _ _ ⇒ True
  | Event_annot _ _ ⇒ True
  end.

Fixpoint output_trace (t: trace) : Prop :=
  match t with
  | nil ⇒ True
  | ev :: t' ⇒ output_event ev ∧ output_trace t'
  end.

Section WITHMEMORYMODELOPS.
Context `{memory_model_ops: Mem.MemoryModelOps}.

Inductive volatile_load (ge: Senv.t):
                   memory_chunk → mem → block → ptrofs → trace → val → Prop :=
  | volatile_load_vol: ∀ chunk m b ofs id ev v,
      Senv.block_is_volatile ge b = Some true →
      Senv.find_symbol ge id = Some b →
      eventval_match ge ev (type_of_chunk chunk) v →
      volatile_load ge chunk m b ofs
                      (Event_vload chunk id ofs ev :: nil)
                      (Val.load_result chunk v)
  | volatile_load_nonvol: ∀ chunk m b ofs v,
      Senv.block_is_volatile ge b = Some false →
      Mem.load chunk m b (Ptrofs.unsigned ofs) = Some v →
      volatile_load ge chunk m b ofs E0 v.

Inductive volatile_store (ge: Senv.t):
                  memory_chunk → mem → block → ptrofs → val → trace → mem → Prop :=
  | volatile_store_vol: ∀ chunk m b ofs id ev v,
      Senv.block_is_volatile ge b = Some true →
      Senv.find_symbol ge id = Some b →
      eventval_match ge ev (type_of_chunk chunk) (Val.load_result chunk v) →
      volatile_store ge chunk m b ofs v
                      (Event_vstore chunk id ofs ev :: nil)
                      m
  | volatile_store_nonvol: ∀ chunk m b ofs v m',
      Senv.block_is_volatile ge b = Some false →
      Mem.store chunk m b (Ptrofs.unsigned ofs) v = Some m' →
      volatile_store ge chunk m b ofs v E0 m'.

End WITHMEMORYMODELOPS.

Definition extcall_sem `{memory_model_ops: Mem.MemoryModelOps} : Type :=
  Senv.t → list val → mem → trace → val → mem → Prop.

Section WITHMEMORYMODEL.
Context `{memory_model_prf: Mem.MemoryModel}.

Definition loc_out_of_bounds (m: mem) (b: block) (ofs: Z) : Prop :=
  ¬Mem.perm m b ofs Max Nonempty.

Definition loc_not_writable (m: mem) (b: block) (ofs: Z) : Prop :=
  ¬Mem.perm m b ofs Max Writable.

Definition loc_unmapped (f: meminj) (b: block) (ofs: Z): Prop :=
  f b = None.

Definition loc_out_of_reach (f: meminj) (m: mem) (b: block) (ofs: Z): Prop :=
  ∀ b0 delta,
  f b0 = Some(b, delta) → ¬Mem.perm m b0 (ofs - delta) Max Nonempty.

Definition inject_separated (f f': meminj) (m1 m2: mem): Prop :=
  ∀ b1 b2 delta,
  f b1 = None → f' b1 = Some(b2, delta) →
  ¬Mem.valid_block m1 b1 ∧ ¬Mem.valid_block m2 b2.

Definition meminj_preserves_globals' (ge: Senv.t) (f: block → option (block × Z)) : Prop :=
     (∀ id b, Senv.find_symbol ge id = Some b → f b = Some(b, 0)) ∧
     (∀ b1 b2 delta, f b1 = Some (b2, delta) → Senv.block_is_volatile ge b2 = Senv.block_is_volatile ge b1).

Lemma meminj_preserves_globals'_symbols_inject (ge: Senv.t) (f: block → option (block × Z)):
  meminj_preserves_globals' ge f →
  symbols_inject f ge ge.
Proof.
  unfold meminj_preserves_globals'.
  intros (A & B).
  repeat split; intros.
  + simpl in H0. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto.
  + simpl in H0. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto.
  + simpl in H0. ∃ b1; split; eauto.
  + eauto.
Qed.

Class SymbolsInject: Type :=
  {
    symbols_inject' (f: block → option (block × Z)) (ge1 ge2: Senv.t):
      Prop;
    meminj_preserves_globals'_symbols_inject' ge f:
      meminj_preserves_globals' ge f →
      symbols_inject' f ge ge;
    symbols_inject'_symbols_inject f ge1 ge2:
      symbols_inject' f ge1 ge2 →
      symbols_inject f ge1 ge2
  }.

Program Definition meminj_preserves_globals'_instance:
  SymbolsInject :=
  {|
    symbols_inject' f ge1 ge2 :=
      meminj_preserves_globals' ge1 f ∧ ge1 = ge2
  |}.
Next Obligation.
  apply meminj_preserves_globals'_symbols_inject.
  assumption.
Qed.

Program Definition symbols_inject_instance:
  SymbolsInject :=
  {|
    symbols_inject' := symbols_inject
  |}.
Next Obligation.
  apply meminj_preserves_globals'_symbols_inject.
  assumption.
Qed.

Context `{symbols_inject'_instance: SymbolsInject}.

Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop :=
  mk_extcall_properties {

  ec_well_typed:
    ∀ ge vargs m1 t vres m2,
    sem ge vargs m1 t vres m2 →
    Val.has_type vres (proj_sig_res sg);

  ec_symbols_preserved:
    ∀ ge1 ge2 vargs m1 t vres m2,
    Senv.equiv ge1 ge2 →
    sem ge1 vargs m1 t vres m2 →
    sem ge2 vargs m1 t vres m2;

  ec_valid_block:
    ∀ ge vargs m1 t vres m2 b,
    sem ge vargs m1 t vres m2 →
    Mem.valid_block m1 b → Mem.valid_block m2 b;

  ec_max_perm:
    ∀ ge vargs m1 t vres m2 b ofs p,
    sem ge vargs m1 t vres m2 →
    Mem.valid_block m1 b → Mem.perm m2 b ofs Max p → Mem.perm m1 b ofs Max p;

  ec_readonly:
    ∀ ge vargs m1 t vres m2,
    sem ge vargs m1 t vres m2 →
    Mem.unchanged_on (loc_not_writable m1) m1 m2;

  ec_mem_extends:
    ∀ ge vargs m1 t vres m2 m1' vargs',
    sem ge vargs m1 t vres m2 →
    Mem.extends m1 m1' →
    Val.lessdef_list vargs vargs' →
    ∃ vres', ∃ m2',
       sem ge vargs' m1' t vres' m2'
    ∧ Val.lessdef vres vres'
    ∧ Mem.extends m2 m2'
    ∧ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2';

  ec_mem_inject:
    ∀ ge1 ge2 vargs m1 t vres m2 f m1' vargs',
    symbols_inject' f ge1 ge2 →
    sem ge1 vargs m1 t vres m2 →
    Mem.inject f m1 m1' →
    Val.inject_list f vargs vargs' →
    ∃ f', ∃ vres', ∃ m2',
       sem ge2 vargs' m1' t vres' m2'
    ∧ Val.inject f' vres vres'
    ∧ Mem.inject f' m2 m2'
    ∧ Mem.unchanged_on (loc_unmapped f) m1 m2
    ∧ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'
    ∧ inject_incr f f'
    ∧ inject_separated f f' m1 m1';

  ec_trace_length:
    ∀ ge vargs m t vres m',
    sem ge vargs m t vres m' → (length t ≤ 1)%nat;

  ec_receptive:
    ∀ ge vargs m t1 vres1 m1 t2,
    sem ge vargs m t1 vres1 m1 → match_traces ge t1 t2 →
    ∃ vres2, ∃ m2, sem ge vargs m t2 vres2 m2;

  ec_determ:
    ∀ ge vargs m t1 vres1 m1 t2 vres2 m2,
    sem ge vargs m t1 vres1 m1 → sem ge vargs m t2 vres2 m2 →
    match_traces ge t1 t2 ∧ (t1 = t2 → vres1 = vres2 ∧ m1 = m2)
}.

Inductive volatile_load_sem (chunk: memory_chunk) (ge: Senv.t):
              list val → mem → trace → val → mem → Prop :=
  | volatile_load_sem_intro: ∀ b ofs m t v,
      volatile_load ge chunk m b ofs t v →
      volatile_load_sem chunk ge (Vptr b ofs :: nil) m t v m.

Lemma volatile_load_preserved:
  ∀ ge1 ge2 chunk m b ofs t v,
  Senv.equiv ge1 ge2 →
  volatile_load ge1 chunk m b ofs t v →
  volatile_load ge2 chunk m b ofs t v.
Proof.
  intros. destruct H as (_ & A & B & C). inv H0; constructor; auto.
  rewrite C; auto.
  rewrite A; auto.
  eapply eventval_match_preserved; eauto.
  rewrite C; auto.
Qed.

Lemma volatile_load_extends:
  ∀ ge chunk m b ofs t v m',
  volatile_load ge chunk m b ofs t v →
  Mem.extends m m' →
  ∃ v', volatile_load ge chunk m' b ofs t v' ∧ Val.lessdef v v'.
Proof.
  intros. inv H.
  econstructor; split; eauto. econstructor; eauto.
  exploit Mem.load_extends; eauto. intros [v' [A B]]. ∃ v'; split; auto. constructor; auto.
Qed.

Lemma volatile_load_inject:
  ∀ ge1 ge2 f chunk m b ofs t v b' ofs' m',
  symbols_inject f ge1 ge2 →
  volatile_load ge1 chunk m b ofs t v →
  Val.inject f (Vptr b ofs) (Vptr b' ofs') →
  Mem.inject f m m' →
  ∃ v', volatile_load ge2 chunk m' b' ofs' t v' ∧ Val.inject f v v'.
Proof.
  intros until m'; intros SI VL VI MI. generalize SI; intros (A & B & C & D).
  inv VL.
-
  inv VI. exploit B; eauto. intros [U V]. subst delta.
  exploit eventval_match_inject_2; eauto. intros (v2 & X & Y).
  rewrite Ptrofs.add_zero. ∃ (Val.load_result chunk v2); split.
  constructor; auto.
  erewrite D; eauto.
  apply Val.load_result_inject. auto.
-
  exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros (v2 & X & Y).
  ∃ v2; split; auto.
  constructor; auto.
  inv VI. erewrite D; eauto.
Qed.

Lemma volatile_load_receptive:
  ∀ ge chunk m b ofs t1 t2 v1,
  volatile_load ge chunk m b ofs t1 v1 → match_traces ge t1 t2 →
  ∃ v2, volatile_load ge chunk m b ofs t2 v2.
Proof.
  intros. inv H; inv H0.
  exploit eventval_match_receptive; eauto. intros [v' EM].
  ∃ (Val.load_result chunk v'). constructor; auto.
  ∃ v1; constructor; auto.
Qed.

Lemma volatile_load_ok:
  ∀ chunk,
  extcall_properties (volatile_load_sem chunk)
                     (mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default).
Proof.
  intros; constructor; intros.
- unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type.
  eapply Mem.load_type; eauto.
- inv H0. constructor. eapply volatile_load_preserved; eauto.
- inv H; auto.
- inv H; auto.
- inv H. apply Mem.unchanged_on_refl.
- inv H. inv H1. inv H6. inv H4.
  exploit volatile_load_extends; eauto. intros [v' [A B]].
  ∃ v'; ∃ m1'; intuition. constructor; auto.
- apply symbols_inject'_symbols_inject in H.
  inv H0. inv H2. inv H7. inversion H5; subst.
  exploit volatile_load_inject; eauto. intros [v' [A B]].
  ∃ f; ∃ v'; ∃ m1'; intuition. constructor; auto.
  red; intros. congruence.
- inv H; inv H0; simpl; omega.
- inv H. exploit volatile_load_receptive; eauto. intros [v2 A].
  ∃ v2; ∃ m1; constructor; auto.
- inv H; inv H0. inv H1; inv H7; try congruence.
  assert (id = id0) by (eapply Senv.find_symbol_injective; eauto). subst id0.
  split. constructor.
  eapply eventval_match_valid; eauto.
  eapply eventval_match_valid; eauto.
  eapply eventval_match_same_type; eauto.
  intros EQ; inv EQ.
  assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0.
  auto.
  split. constructor. intuition congruence.
Qed.

Inductive volatile_store_sem (chunk: memory_chunk) (ge: Senv.t):
              list val → mem → trace → val → mem → Prop :=
  | volatile_store_sem_intro: ∀ b ofs m1 v t m2,
      volatile_store ge chunk m1 b ofs v t m2 →
      volatile_store_sem chunk ge (Vptr b ofs :: v :: nil) m1 t Vundef m2.

Lemma volatile_store_preserved:
  ∀ ge1 ge2 chunk m1 b ofs v t m2,
  Senv.equiv ge1 ge2 →
  volatile_store ge1 chunk m1 b ofs v t m2 →
  volatile_store ge2 chunk m1 b ofs v t m2.
Proof.
  intros. destruct H as (_ & A & B & C). inv H0; constructor; auto.
  rewrite C; auto.
  rewrite A; auto.
  eapply eventval_match_preserved; eauto.
  rewrite C; auto.
Qed.

Lemma volatile_store_readonly:
  ∀ ge chunk1 m1 b1 ofs1 v t m2,
  volatile_store ge chunk1 m1 b1 ofs1 v t m2 →
  Mem.unchanged_on (loc_not_writable m1) m1 m2.
Proof.
  intros. inv H.
  apply Mem.unchanged_on_refl.
  eapply Mem.store_unchanged_on; eauto.
  exploit Mem.store_valid_access_3; eauto. intros [P Q].
  intros. unfold loc_not_writable. red; intros. elim H2.
  apply Mem.perm_cur_max. apply P. auto.
Qed.

Lemma volatile_store_extends:
  ∀ ge chunk m1 b ofs v t m2 m1' v',
  volatile_store ge chunk m1 b ofs v t m2 →
  Mem.extends m1 m1' →
  Val.lessdef v v' →
  ∃ m2',
     volatile_store ge chunk m1' b ofs v' t m2'
  ∧ Mem.extends m2 m2'
  ∧ Mem.unchanged_on (loc_out_of_bounds m1) m1' m2'.
Proof.
  intros. inv H.
- econstructor; split. econstructor; eauto.
  eapply eventval_match_lessdef; eauto. apply Val.load_result_lessdef; auto.
  auto with mem.
- exploit Mem.store_within_extends; eauto. intros [m2' [A B]].
  ∃ m2'; repeat (split; auto).
+ econstructor; eauto.
+ eapply Mem.store_unchanged_on; eauto.
  unfold loc_out_of_bounds; intros.
  assert (Mem.perm m1 b i Max Nonempty).
  { apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
    exploit Mem.store_valid_access_3. eexact H3. intros [P Q]. eauto. }
  tauto.
Qed.

Lemma volatile_store_inject:
  ∀ ge1 ge2 f chunk m1 b ofs v t m2 m1' b' ofs' v',
  symbols_inject f ge1 ge2 →
  volatile_store ge1 chunk m1 b ofs v t m2 →
  Val.inject f (Vptr b ofs) (Vptr b' ofs') →
  Val.inject f v v' →
  Mem.inject f m1 m1' →
  ∃ m2',
       volatile_store ge2 chunk m1' b' ofs' v' t m2'
    ∧ Mem.inject f m2 m2'
    ∧ Mem.unchanged_on (loc_unmapped f) m1 m2
    ∧ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'.
Proof.
  intros until v'; intros SI VS AI VI MI.
  generalize SI; intros (P & Q & R & S).
  inv VS.
-
  inv AI. exploit Q; eauto. intros [A B]. subst delta.
  rewrite Ptrofs.add_zero. ∃ m1'; split.
  constructor; auto. erewrite S; eauto.
  eapply eventval_match_inject; eauto. apply Val.load_result_inject. auto.
  intuition auto with mem.
-
  inversion AI; subst.
  assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto.
  exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]].
  ∃ m2'; repeat (split; auto).
+ constructor; auto. erewrite S; eauto.
+ eapply Mem.store_unchanged_on; eauto.
  unfold loc_unmapped; intros. inv AI; congruence.
+ eapply Mem.store_unchanged_on; eauto.
  unfold loc_out_of_reach; intros. red; intros. simpl in A.
  assert (EQ: Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta)) = Ptrofs.unsigned ofs + delta)
  by (eapply Mem.address_inject; eauto with mem).
  rewrite EQ in ×.
  eelim H3; eauto.
  exploit Mem.store_valid_access_3. eexact H0. intros [X Y].
  apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
  apply X. omega.
Qed.

Lemma volatile_store_receptive:
  ∀ ge chunk m b ofs v t1 m1 t2,
  volatile_store ge chunk m b ofs v t1 m1 → match_traces ge t1 t2 → t1 = t2.
Proof.
  intros. inv H; inv H0; auto.
Qed.

Lemma volatile_store_ok:
  ∀ chunk,
  extcall_properties (volatile_store_sem chunk)
                     (mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default).
Proof.
  intros; constructor; intros.
- unfold proj_sig_res; simpl. inv H; constructor.
- inv H0. constructor. eapply volatile_store_preserved; eauto.
- inv H. inv H1. auto. eauto with mem.
- inv H. inv H2. auto. eauto with mem.
- inv H. eapply volatile_store_readonly; eauto.
- inv H. inv H1. inv H6. inv H7. inv H4.
  exploit volatile_store_extends; eauto. intros [m2' [A [B C]]].
  ∃ Vundef; ∃ m2'; intuition. constructor; auto.
- apply symbols_inject'_symbols_inject in H.
  inv H0. inv H2. inv H7. inv H8. inversion H5; subst.
  exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]].
  ∃ f; ∃ Vundef; ∃ m2'; intuition. constructor; auto. red; intros; congruence.
- inv H; inv H0; simpl; omega.
- assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto.
  subst t2; ∃ vres1; ∃ m1; auto.
- inv H; inv H0. inv H1; inv H8; try congruence.
  assert (id = id0) by (eapply Senv.find_symbol_injective; eauto). subst id0.
  assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0.
  split. constructor. auto.
  split. constructor. intuition congruence.
Qed.

Inductive extcall_malloc_sem (ge: Senv.t):
              list val → mem → trace → val → mem → Prop :=
  | extcall_malloc_sem_intro: ∀ sz m m' b m'',
      Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned sz) = (m', b) →
      Mem.store Mptr m' b (- size_chunk Mptr) (Vptrofs sz) = Some m'' →
      extcall_malloc_sem ge (Vptrofs sz :: nil) m E0 (Vptr b Ptrofs.zero) m''.

Lemma extcall_malloc_ok:
  extcall_properties extcall_malloc_sem
                     (mksignature (Tptr :: nil) (Some Tptr) cc_default).
Proof.
  assert (UNCHANGED:
    ∀ (P: block → Z → Prop) m lo hi v m' b m'',
    Mem.alloc m lo hi = (m', b) →
    Mem.store Mptr m' b lo v = Some m'' →
    Mem.unchanged_on P m m'').
  {
    intros.
    apply Mem.unchanged_on_implies with (fun b1 ofs1 ⇒ b1 ≠ b).
    apply Mem.unchanged_on_trans with m'.
    eapply Mem.alloc_unchanged_on; eauto.
    eapply Mem.store_unchanged_on; eauto.
    intros. eapply Mem.valid_not_valid_diff; eauto with mem.
  }
  constructor; intros.
- inv H. unfold proj_sig_res, Tptr; simpl. destruct Archi.ptr64; auto.
- inv H0; econstructor; eauto.
- inv H. eauto with mem.
- inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto.
  rewrite dec_eq_false. auto.
  apply Mem.valid_not_valid_diff with m1; eauto with mem.
- inv H. eapply UNCHANGED; eauto.
- inv H. inv H1. inv H7.
  assert (SZ: v2 = Vptrofs sz).
  { unfold Vptrofs in ×. destruct Archi.ptr64; inv H5; auto. }
  subst v2.
  exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
  intros [m3' [A B]].
  exploit Mem.store_within_extends. eexact B. eauto. eauto.
  intros [m2' [C D]].
  ∃ (Vptr b Ptrofs.zero); ∃ m2'; intuition.
  econstructor; eauto.
  eapply UNCHANGED; eauto.
- inv H0. inv H2. inv H8.
  assert (SZ: v' = Vptrofs sz).
  { unfold Vptrofs in ×. destruct Archi.ptr64; inv H6; auto. }
  subst v'.
  exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl.
  intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]].
  exploit Mem.store_mapped_inject. eexact A. eauto. eauto.
  instantiate (1 := Vptrofs sz). unfold Vptrofs; destruct Archi.ptr64; constructor.
  rewrite Zplus_0_r. intros [m2' [E G]].
  ∃ f'; ∃ (Vptr b' Ptrofs.zero); ∃ m2'; intuition auto.
  econstructor; eauto.
  econstructor. eauto. auto.
  eapply UNCHANGED; eauto.
  eapply UNCHANGED; eauto.
  red; intros. destruct (eq_block b1 b).
  subst b1. rewrite C in H2. inv H2. eauto with mem.
  rewrite D in H2 by auto. congruence.
- inv H; simpl; omega.
- assert (t1 = t2). inv H; inv H0; auto. subst t2.
  ∃ vres1; ∃ m1; auto.
- inv H. simple inversion H0.
  assert (EQ2: sz0 = sz).
  { unfold Vptrofs in H4; destruct Archi.ptr64 eqn:SF.
    rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
    rewrite <- (Ptrofs.of_int_to_int SF sz0), <- (Ptrofs.of_int_to_int SF sz). congruence.
  }
  subst.
  split. constructor. intuition congruence.
Qed.

Inductive extcall_free_sem (ge: Senv.t):
              list val → mem → trace → val → mem → Prop :=
  | extcall_free_sem_intro: ∀ b lo sz m m',
      Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) →
      Ptrofs.unsigned sz > 0 →
      Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' →
      extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'.

Lemma extcall_free_ok:
  extcall_properties extcall_free_sem
                     (mksignature (Tptr :: nil) None cc_default).
Proof.
  constructor; intros.
- inv H. unfold proj_sig_res. simpl. auto.
- inv H0; econstructor; eauto.
- inv H. eauto with mem.
- inv H. eapply Mem.perm_free_3; eauto.
- inv H. eapply Mem.free_unchanged_on; eauto.
  intros. red; intros. elim H3.
  apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
  eapply Mem.free_range_perm; eauto.
- inv H. inv H1. inv H8. inv H6.
  exploit Mem.load_extends; eauto. intros [v' [A B]].
  assert (v' = Vptrofs sz).
  { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
  subst v'.
  exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]].
  ∃ Vundef; ∃ m2'.
  repeat
    match goal with
        |- _ ∧ _ ⇒
        split; try now auto
    end.
  econstructor; eauto.
  eapply Mem.free_unchanged_on; eauto.
  unfold loc_out_of_bounds; intros.
  assert (Mem.perm m1 b i Max Nonempty).
  { apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
    eapply Mem.free_range_perm. eexact H4. eauto. }
  tauto.
- inv H0. inv H2. inv H7. inv H9.
  exploit Mem.load_inject; eauto. intros [v' [A B]].
  assert (v' = Vptrofs sz).
  { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. }
  subst v'.
  assert (P: Mem.range_perm m1 b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) Cur Freeable).
    eapply Mem.free_range_perm; eauto.
  exploit Mem.address_inject; eauto.
    apply Mem.perm_implies with Freeable; auto with mem.
    apply P. instantiate (1 := lo).
    generalize (size_chunk_pos Mptr); omega.
  intro EQ.
  exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
  ∃ f, Vundef, m2'; split.
  apply extcall_free_sem_intro with (sz := sz) (m' := m2').
    rewrite EQ. rewrite <- A. f_equal. omega.
    auto. auto.
    rewrite ! EQ. rewrite <- C. f_equal; omega.
  eauto.
  split. auto.
  split. auto.
  split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence.
  split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach.
    intros. red; intros. eelim H2; eauto.
    apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
    apply P. omega.
  split. auto.
  red; intros. congruence.
- inv H; simpl; omega.
- assert (t1 = t2). inv H; inv H0; auto. subst t2.
  ∃ vres1; ∃ m1; auto.
- inv H; inv H0.
  assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence.
  assert (EQ2: sz0 = sz).
  { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF.
    rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence.
    rewrite <- (Ptrofs.of_int_to_int SF sz0), <- (Ptrofs.of_int_to_int SF sz). congruence.
  }
  subst sz0.
  split. constructor. intuition congruence.
Qed.