Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.common.AST.
Require Import compcert.common.Globalenvs.
Require Import compcert.common.Memory.
Require Import compcert.common.Memdata.
Require Import compcert.common.Values.

Require Import VST.msl.Coqlib2.
Require Import VST.msl.eq_dec.
Require Import VST.msl.seplog.
Require Import VST.veric.Memory.
Require Import VST.veric.juicy_mem. 
Require Import VST.veric.juicy_extspec.

Require Import VST.veric.res_predicates.

(*Lenb: Should Imports from sepcomp really be here?*)
Require Import VST.sepcomp.extspec.

(*Require Import VST.sepcomp.event_semantics.
Require Import VST.sepcomp.extspec.*)
(*Lenb: Should stuff that requires Imports from sepcomp really be here?*)

Notation val_inject := Val.inject. (*as in sepcomp.mem_lemmas*)

Definition mem_lessdef m1 m2 :=
  (forall b ofs len v,
      Mem.loadbytes m1 b ofs len = Some v ->
      exists v',
        Mem.loadbytes m2 b ofs len = Some v' /\
        list_forall2 memval_lessdef v v'
  ) /\
  (forall b ofs k p,
      Mem.perm m1 b ofs k p ->
      Mem.perm m2 b ofs k p) /\
  (Mem.nextblock m1 <=
   Mem.nextblock m2)%positive.

Definition mem_lessalloc m1 m2 :=
  Mem.loadbytes m1 = Mem.loadbytes m2 /\
  Mem.perm m1 = Mem.perm m2 /\
  (Mem.nextblock m1 <= Mem.nextblock m2)%positive.

Definition mem_equiv m1 m2 :=
  Mem.loadbytes m1 = Mem.loadbytes m2 /\
  Mem.perm m1 = Mem.perm m2 /\
  Mem.nextblock m1 = Mem.nextblock m2.

Lemma perm_order_pp_refl p: Mem.perm_order'' p p.
(* Goal: Mem.perm_order'' p p *)
Proof. unfold Mem.perm_order''. destruct p; trivial. apply perm_refl. Qed.

Lemma same_perm_spec m1 m2 :
  Mem.perm m1 = Mem.perm m2 <->
  (forall k x, access_at m1 x k = access_at m2 x k).
Proof.
  split; intros E.
  - intros k (b, ofs).
    match type of E with ?f = ?g => assert (S : forall b z k p, f b z k p <-> g b z k p) end.
    { rewrite E; tauto. } clear E.
    specialize (S b ofs k). revert S.
    unfold access_at, Mem.perm. simpl.
    set (o1 := (Mem.mem_access _) !! b ofs k).
    set (o2 := (Mem.mem_access _) !! b ofs k). clearbody o1 o2. intros S.
    assert (S' : forall o, Mem.perm_order'' o1 o <-> Mem.perm_order'' o2 o).
    { intros [ o | ]. apply S. destruct o1 as [o1 | ], o2 as [o2 | ]; split; intro; constructor. }
    clear S.
    destruct (S' o1) as [A _]. spec A. apply perm_order_pp_refl.
    destruct (S' o2) as [_ B]. spec B. apply perm_order_pp_refl.
    destruct o1 as [[]|], o2 as [[]|]; auto; simpl in *.
    all: try solve [inv A; inv B; auto].
  - extensionality b ofs k. specialize (E k (b, ofs)).
    unfold access_at in *.
    simpl in E.
    unfold Mem.perm in *.
    rewrite E.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    auto.
Qed.

Lemma same_loadbytes_spec m1 m2 :
  Mem.perm m1 = Mem.perm m2 ->  (* TODO change this to only need same Cur *)
  Mem.loadbytes m1 = Mem.loadbytes m2 <->
  (forall x, Mem.perm_order' (access_at m1 x Cur) Readable -> contents_at m1 x = contents_at m2 x).
Proof.
  intros P; split; intros E.
  - intros (b, ofs) R.
    Transparent Mem.loadbytes.
    unfold Mem.loadbytes in *.
    apply equal_f with (x := b) in E.
    apply equal_f with (x := ofs) in E.
    apply equal_f with (x := 1) in E.
    unfold access_at in *.
    if_tac [p1|np1] in E; if_tac in E; try discriminate.
    + simpl in E.
      unfold contents_at in *.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval (Byte i) bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
      simpl.
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
      congruence.
    + destruct np1.
      intros ofs1 r1.
      cut (ofs1 = ofs). intros <-. apply R.
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
      omega.
  - extensionality b ofs k.
    unfold Mem.loadbytes in *.
    if_tac [p1|np1]; if_tac [p2|np2].
    + destruct (zle 0 k).
      * clear p2.
        f_equal.
        rewrite <-(Coqlib.nat_of_Z_eq k) in p1. 2:omega.
        revert p1. generalize (nat_of_Z k); clear k l; intros n.
        revert ofs.
        induction n; auto; intros ofs p.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval (Byte i) bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
        simpl. f_equal.
        -- specialize (E (b, ofs)).
           unfold contents_at in *.
           simpl in E.
           apply E.
           apply p.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval (Byte i) bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
           simpl.
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
           zify; omega.
        -- apply IHn.
           intros ofs' r'.
           apply p.
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
           zify. omega.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
      * rewrite nat_of_Z_neg. auto. omega.
    + destruct np2.
      unfold Mem.range_perm in *.
      rewrite <-P.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
      auto.
    + destruct np1.
      unfold Mem.range_perm in *.
      rewrite P.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
      auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    + auto.
Qed.

Definition mem_equiv' m1 m2 :=
  (forall x, Mem.perm_order' (access_at m1 x Cur) Readable -> contents_at m1 x = contents_at m2 x) /\
  Mem.perm m1 = Mem.perm m2 /\
  Mem.nextblock m1 = Mem.nextblock m2.

Definition mem_lessalloc' m1 m2 :=
  (forall x, Mem.perm_order' (access_at m1 x Cur) Readable -> contents_at m1 x = contents_at m2 x) /\
  Mem.perm m1 = Mem.perm m2 /\
  (Mem.nextblock m1 <= Mem.nextblock m2)%positive.

Lemma mem_equiv'_spec m1 m2 : mem_equiv m1 m2 <-> mem_equiv' m1 m2.
Proof.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  split; intros (? & ? & ?); repeat split; auto.
  rewrite <-same_loadbytes_spec; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  rewrite same_loadbytes_spec; auto.
Qed.

Lemma mem_lessalloc'_spec m1 m2 : mem_lessalloc m1 m2 <-> mem_lessalloc' m1 m2.
Proof.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  split; intros (? & ? & ?); repeat split; auto.
  rewrite <-same_loadbytes_spec; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  rewrite same_loadbytes_spec; auto.
Qed.

Lemma val_inject_antisym v1 v2 :
  val_inject inject_id v1 v2 ->
  val_inject inject_id v2 v1 ->
  v1 = v2.
Proof.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  destruct v1, v2; intros A B; auto.
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
  all: inversion A; subst; inversion B; try subst; try congruence.
  unfold inject_id in *.
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
  f_equal. congruence.
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
  replace delta with 0%Z by congruence.
  symmetry; apply Ptrofs.add_zero.
Qed.

Lemma memval_lessdef_antisym v1 v2 : memval_lessdef v1 v2 -> memval_lessdef v2 v1 -> v1 = v2.
Proof.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  destruct v1, v2; intros A B; auto.
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
  all: inversion A; subst; inversion B; subst; try congruence.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  f_equal. apply val_inject_antisym; auto.
Qed.

Lemma mem_lessdef_equiv m1 m2 : mem_lessdef m1 m2 -> mem_lessdef m2 m1 ->  mem_equiv m1 m2.
Proof.
(* Goal: forall (_ : mem_lessdef m1 m2) (_ : mem_lessdef m2 m1), mem_equiv m1 m2 *)
  intros (L1 & P1 & N1) (L2 & P2 & N2); repeat split.
  - clear -L1 L2.
(* Goal: @eq (forall (_ : block) (_ : Z) (_ : Z), option (list memval)) (Mem.loadbytes m1) (Mem.loadbytes m2) *)
    extensionality b ofs z.
    match goal with |- ?a = ?b => destruct a as [v1|] eqn:E1; destruct b as [v2|] eqn:E2 end;
      try destruct (L1 _ _ _ _ E1) as (v2' & E1' & l1);
      try destruct (L2 _ _ _ _ E2) as (v1' & E2' & l2);
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
      try congruence.
    assert (v1' = v1) by congruence; assert (v2' = v2) by congruence; subst; f_equal.
    clear -l1 l2.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    revert v2 l1 l2; induction v1; intros v2 l1 l2; inversion l1; subst; auto.
(* Goal: @eq (list memval) (@cons memval a v1) (@cons memval b1 bl) *)
    inversion l2; subst.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    f_equal; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    apply memval_lessdef_antisym; auto.
  - repeat extensionality.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    apply prop_ext; split; auto.
  - zify.
(* Goal: @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
    cut (Z.pos (Mem.nextblock m2) = Z.pos (Mem.nextblock m1)).
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
    congruence. omega.
Qed.

Lemma mem_equiv_refl m : mem_equiv m m.
Proof.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  split3; hnf; auto.
Qed.

Lemma mem_lessalloc_refl m : mem_lessalloc m m.
Proof.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  split3; auto. apply Ple_refl.
Qed.

Lemma mem_equiv_refl' m m' : m = m' -> mem_equiv m m'.
Proof.
  intros <-; apply mem_equiv_refl.
Qed.

Lemma mem_lessalloc_refl' m m' : m = m' -> mem_lessalloc m m'.
Proof.
  intros <-; apply mem_lessalloc_refl.
Qed.

Lemma mem_equiv_sym m1 m2 : mem_equiv m1 m2 -> mem_equiv m2 m1.
Proof.
(* Goal: forall _ : mem_equiv m1 m2, mem_equiv m2 m1 *)
  intros []; split; intuition.
Qed.

Lemma mem_equiv_trans m1 m2 m3 :
  mem_equiv m1 m2 ->
  mem_equiv m2 m3 ->
  mem_equiv m1 m3.
Proof.
  unfold mem_equiv in *.
  intros (-> & -> & ->) (-> & -> & ->); auto.
Qed.

Lemma mem_lessalloc_trans m1 m2 m3 :
  mem_lessalloc m1 m2 ->
  mem_lessalloc m2 m3 ->
  mem_lessalloc m1 m3.
Proof.
  unfold mem_lessalloc in *.
  intros (-> & -> & l) (-> & -> & l'); split; auto. split; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  eapply Ple_trans; eauto.
Qed.

Lemma mem_equiv_lessalloc m1 m2 : mem_equiv m1 m2 -> mem_lessalloc m1 m2.
Proof.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  intros (L1 & P1 & N1); repeat split; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
  rewrite N1; auto. apply Ple_refl.
Qed.

Lemma mem_lessalloc_lessdef m1 m2 : mem_lessalloc m1 m2 -> mem_lessdef m1 m2.
Proof.
(* Goal: forall _ : mem_lessalloc m1 m2, mem_lessdef m1 m2 *)
  intros (L1 & P1 & N1); repeat split.
  - rewrite L1; auto.
(* Goal: forall (b : block) (ofs len : Z) (v : list memval) (_ : @eq (option (list memval)) (Mem.loadbytes m2 b ofs len) (@Some (list memval) v)), @ex (list memval) (fun v' : list memval => and (@eq (option (list memval)) (Mem.loadbytes m2 b ofs len) (@Some (list memval) v')) (@list_forall2 memval memval memval_lessdef v v')) *)
    intros b ofs len v H.
(* Goal: @ex (list memval) (fun v' : list memval => and (@eq (option (list memval)) (Mem.loadbytes m2 b ofs len) (@Some (list memval) v')) (@list_forall2 memval memval memval_lessdef v v')) *)
    exists v; intuition.
(* Goal: @list_forall2 memval memval memval_lessdef v v *)
    clear.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    induction v; constructor; auto.
(* Goal: memval_lessdef a a *)
    apply memval_lessdef_refl.
  - rewrite P1; auto.
  - auto.
Qed.

Lemma mem_equiv_lessdef m1 m2 : mem_equiv m1 m2 -> mem_lessdef m1 m2.
Proof.
(* Goal: forall _ : mem_equiv m1 m2, mem_lessdef m1 m2 *)
  intro H.
(* Goal: mem_lessdef m1 m2 *)
  apply mem_lessalloc_lessdef, mem_equiv_lessalloc, H.
Qed.

Lemma mem_lessdef_valid_pointer:
  forall m1 m2 b z, 
       mem_lessdef m1 m2 ->
       Mem.valid_pointer m1 b z = true ->
       Mem.valid_pointer m2 b z = true.
Proof.
(* Goal: forall (m1 m2 : Mem.mem) (_ : mem_lessdef m1 m2) (b : block) (z n : Z) (v1 : list memval) (_ : @eq (option (list memval)) (Mem.loadbytes m1 b z n) (@Some (list memval) v1)), @ex (list memval) (fun v2 : list memval => and (@list_forall2 memval memval memval_lessdef v1 v2) (@eq (option (list memval)) (Mem.loadbytes m2 b z n) (@Some (list memval) v2))) *)
intros.
(* Goal: @ex (list memval) (fun v2 : list memval => and (@list_forall2 memval memval memval_lessdef v1 v2) (@eq (option (list memval)) (Mem.loadbytes m2 b z n) (@Some (list memval) v2))) *)
destruct H as [? [? ?]].
unfold Mem.valid_pointer in *.
(* Goal: @eq bool (@proj_sumbool (Mem.perm m2 b z Cur Nonempty) (not (Mem.perm m2 b z Cur Nonempty)) (Mem.perm_dec m2 b z Cur Nonempty)) true *)
destruct (Mem.perm_dec m1 b z Cur Nonempty); inv H0.
(* Goal: @eq bool (@proj_sumbool (Mem.perm m2 b z Cur Nonempty) (not (Mem.perm m2 b z Cur Nonempty)) (Mem.perm_dec m2 b z Cur Nonempty)) true *)
destruct (Mem.perm_dec m2 b z Cur Nonempty); try reflexivity.
(* Goal: @eq bool (@proj_sumbool (Mem.perm m2 b z Cur Nonempty) (not (Mem.perm m2 b z Cur Nonempty)) (@right (Mem.perm m2 b z Cur Nonempty) (not (Mem.perm m2 b z Cur Nonempty)) n)) true *)
contradiction n. clear n.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
apply H1; auto.
Qed.

Lemma mem_lessdef_weak_valid_pointer:
  forall m1 m2 b z, 
       mem_lessdef m1 m2 ->
       Mem.weak_valid_pointer m1 b z = true ->
       Mem.weak_valid_pointer m2 b z = true.
Proof.
(* Goal: forall (m1 m2 : Mem.mem) (_ : mem_lessdef m1 m2) (b : block) (z n : Z) (v1 : list memval) (_ : @eq (option (list memval)) (Mem.loadbytes m1 b z n) (@Some (list memval) v1)), @ex (list memval) (fun v2 : list memval => and (@list_forall2 memval memval memval_lessdef v1 v2) (@eq (option (list memval)) (Mem.loadbytes m2 b z n) (@Some (list memval) v2))) *)
intros.
unfold Mem.weak_valid_pointer in *.
rewrite orb_true_iff in *.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
destruct H0; [left|right]; eapply mem_lessdef_valid_pointer; eauto.
Qed.

Ltac memval_lessdef_tac :=
match goal with
 | H: memval_lessdef ?a ?b |- _ => destruct a,b; inv H
 | H: list_forall2 _ ?a ?b |- _ => destruct a,b; inv H
 | H: proj_bytes ?a = Some _ |- _ => match a with context [nil] => inv H end
end;
 try discriminate;
 try solve [unfold decode_val; simpl; auto] .

Lemma mem_lessdef_proj_bytes:
  forall vl vl',
  list_forall2 memval_lessdef vl vl' ->
  forall bl, proj_bytes vl = Some bl -> proj_bytes vl' = Some bl.
Proof.
(* Goal: forall (m1 m2 : Mem.mem) (_ : mem_lessdef m1 m2) (b : block) (z n : Z) (v1 : list memval) (_ : @eq (option (list memval)) (Mem.loadbytes m1 b z n) (@Some (list memval) v1)), @ex (list memval) (fun v2 : list memval => and (@list_forall2 memval memval memval_lessdef v1 v2) (@eq (option (list memval)) (Mem.loadbytes m2 b z n) (@Some (list memval) v2))) *)
intros.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
revert bl H0; induction H; intros; auto.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@Some (list Byte.int) bl0) *)
destruct bl0; inv H1.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
destruct a1; auto.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@None (list Byte.int)) *)
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) match a1 with | Undef => @None (list Byte.int) | Byte b => match proj_bytes al with | Some bl => @Some (list Byte.int) (@cons Byte.int b bl) | None => @None (list Byte.int) end | Fragment v q n => @None (list Byte.int) end *)
inv H3.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@None (list Byte.int)) *)
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) match a1 with | Undef => @None (list Byte.int) | Byte b => match proj_bytes al with | Some bl => @Some (list Byte.int) (@cons Byte.int b bl) | None => @None (list Byte.int) end | Fragment v q n => @None (list Byte.int) end *)
destruct (proj_bytes al) eqn:?H; inv H3. inv H3.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) match a1 with | Undef => @None (list Byte.int) | Byte b => match proj_bytes al with | Some bl => @Some (list Byte.int) (@cons Byte.int b bl) | None => @None (list Byte.int) end | Fragment v q n => @None (list Byte.int) end *)
destruct a1; try discriminate.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@None (list Byte.int)) *)
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) match a1 with | Undef => @None (list Byte.int) | Byte b => match proj_bytes al with | Some bl => @Some (list Byte.int) (@cons Byte.int b bl) | None => @None (list Byte.int) end | Fragment v q n => @None (list Byte.int) end *)
destruct (proj_bytes al) eqn:?H; inv H3.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
specialize (IHlist_forall2 _ (eq_refl _)).
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
inv H.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval (Byte i) bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
simpl.
(* Goal: @eq (option (list Byte.int)) match proj_bytes bl with | Some bl => @Some (list Byte.int) (@cons Byte.int i bl) | None => @None (list Byte.int) end (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
rewrite IHlist_forall2.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
auto.
Qed.

Lemma mem_lessdef_decode_val:
  forall ch vl vl', list_forall2 memval_lessdef vl vl' ->
    Val.lessdef (decode_val ch vl) (decode_val ch vl').
Proof.
(* Goal: forall (m1 m2 : Mem.mem) (_ : mem_lessdef m1 m2) (b : block) (z n : Z) (v1 : list memval) (_ : @eq (option (list memval)) (Mem.loadbytes m1 b z n) (@Some (list memval) v1)), @ex (list memval) (fun v2 : list memval => and (@list_forall2 memval memval memval_lessdef v1 v2) (@eq (option (list memval)) (Mem.loadbytes m2 b z n) (@Some (list memval) v2))) *)
intros.
unfold decode_val.
destruct (proj_bytes vl) eqn:?H.
2: {
     unfold proj_value.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
     destruct ch eqn:Hch; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
     + destruct Archi.ptr64; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct vl; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct m; auto.
       match type of Hch with
       | ch = Mint64 =>
           destruct (check_value (size_quantity_nat Q64) v Q64 (Fragment v q n :: vl)) eqn:?; auto
       | ch = Mint32 =>
           destruct (check_value (size_quantity_nat Q32) v Q32 (Fragment v q n :: vl)) eqn:?; auto
       end.
       revert Hch.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct vl'; inv H.
       inv H4.
       intro.
       unfold proj_bytes.
       destruct (Val.eq v Vundef).
       subst v.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval (Byte i) bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       simpl. auto.
       match type of Hch with
       | ch = Mint64 =>
           assert (H9: check_value (size_quantity_nat Q64) v2 Q64 (Fragment v2 q n :: vl') = true)
       | ch = Mint32 =>
           assert (H9: check_value (size_quantity_nat Q32) v2 Q32 (Fragment v2 q n :: vl') = true)
       end.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       2: rewrite H9; apply Val.load_result_lessdef; apply val_inject_id; auto.
       assert (v2=v).
       apply val_inject_id in H5.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct v; try solve [contradiction n0; auto]; inv H5; auto.
       subst v2.
       clear H5.
       eapply (check_value_inject inject_id); try eassumption.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       constructor; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       constructor; auto.
       apply val_inject_id; apply Val.lessdef_refl.
       apply val_inject_id; apply Val.lessdef_refl.
     +
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct vl; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct m; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct (check_value (size_quantity_nat Q32) v Q32 (Fragment v q n :: vl)) eqn:?; auto.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct vl'; inv H.
       unfold proj_bytes.
       inv H4.
       destruct (Val.eq v Vundef).
       subst.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval (Byte i) bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       simpl. auto.
       assert (H9: check_value (size_quantity_nat Q32) v2 Q32 (Fragment v2 q n :: vl') = true).
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       2: rewrite H9; apply Val.load_result_lessdef; apply val_inject_id; auto.
       assert (v2=v).
       apply val_inject_id in H5.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct v; try solve [contradiction n0; auto]; inv H5; auto.
       subst v2.
       clear H5.
       eapply (check_value_inject inject_id); try eassumption.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       constructor; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       constructor; auto.
       apply val_inject_id; apply Val.lessdef_refl.
       apply val_inject_id; apply Val.lessdef_refl.
     +
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct vl; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct m; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct (check_value (size_quantity_nat Q64) v Q64 (Fragment v q n :: vl)) eqn:?; auto.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval b1 bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct vl'; inv H.
       unfold proj_bytes.
       inv H4.
       destruct (Val.eq v Vundef).
       subst.
(* Goal: @eq (option (list Byte.int)) (proj_bytes (@cons memval (Byte i) bl)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       simpl. auto.
       assert (H9: check_value (size_quantity_nat Q64) v2 Q64 (Fragment v2 q n :: vl') = true).
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       2: rewrite H9; apply Val.load_result_lessdef; apply val_inject_id; auto.
       assert (v2=v).
       apply val_inject_id in H5.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       destruct v; try solve [contradiction n0; auto]; inv H5; auto.
       subst v2.
       clear H5.
       eapply (check_value_inject inject_id); try eassumption.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       constructor; auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
       constructor; auto.
       apply val_inject_id; apply Val.lessdef_refl.
       apply val_inject_id; apply Val.lessdef_refl.
     } 
rewrite (mem_lessdef_proj_bytes _ _ H _ H0).
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
auto.
Qed.

Lemma mem_lessdef_loadbytes:
  forall m1 m2, mem_lessdef m1 m2 ->
  forall b z n v1, Mem.loadbytes m1 b z n = Some v1 ->
  exists v2, list_forall2 memval_lessdef v1 v2 /\ Mem.loadbytes m2 b z n = Some v2.
Proof.
(* Goal: forall (m1 m2 : Mem.mem) (_ : mem_lessdef m1 m2) (b : block) (z n : Z) (v1 : list memval) (_ : @eq (option (list memval)) (Mem.loadbytes m1 b z n) (@Some (list memval) v1)), @ex (list memval) (fun v2 : list memval => and (@list_forall2 memval memval memval_lessdef v1 v2) (@eq (option (list memval)) (Mem.loadbytes m2 b z n) (@Some (list memval) v2))) *)
intros.
(* Goal: @ex (list memval) (fun v2 : list memval => and (@list_forall2 memval memval memval_lessdef v1 v2) (@eq (option (list memval)) (Mem.loadbytes m2 b z n) (@Some (list memval) v2))) *)
destruct H as [? [? ?]].
(* Goal: @ex (list memval) (fun v2 : list memval => and (@list_forall2 memval memval memval_lessdef v1 v2) (@eq (option (list memval)) (Mem.loadbytes m2 b z n) (@Some (list memval) v2))) *)
apply H in H0.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
destruct H0 as [v2 [? ?]]; exists v2; split; auto.
Qed.

Lemma valid_pointer_lessalloc {m m2} (M:mem_lessalloc m m2):
      Mem.valid_pointer m = Mem.valid_pointer m2.
(* Goal: @eq (forall (_ : block) (_ : Z), bool) (Mem.valid_pointer m) (Mem.valid_pointer m2) *)
Proof. unfold Mem.valid_pointer. destruct M as [M1 [M2 M3]].
(* Goal: @eq (forall (_ : block) (_ : Z), bool) (fun (b : block) (ofs : Z) => orb (Mem.valid_pointer m b ofs) (Mem.valid_pointer m b (Z.sub ofs (Zpos xH)))) (fun (b : block) (ofs : Z) => orb (Mem.valid_pointer m2 b ofs) (Mem.valid_pointer m2 b (Z.sub ofs (Zpos xH)))) *)
  extensionality b. extensionality i.
  destruct (Mem.perm_dec m b i Cur Nonempty);
  destruct (Mem.perm_dec m2 b i Cur Nonempty); trivial.
(* Goal: @eq bool (@proj_sumbool (Mem.perm m b i Cur Nonempty) (not (Mem.perm m b i Cur Nonempty)) (@right (Mem.perm m b i Cur Nonempty) (not (Mem.perm m b i Cur Nonempty)) n)) (@proj_sumbool (Mem.perm m2 b i Cur Nonempty) (not (Mem.perm m2 b i Cur Nonempty)) (@left (Mem.perm m2 b i Cur Nonempty) (not (Mem.perm m2 b i Cur Nonempty)) p)) *)
  exfalso. rewrite M2 in p. contradiction.
(* Goal: @eq bool (@proj_sumbool (Mem.perm m b i Cur Nonempty) (not (Mem.perm m b i Cur Nonempty)) (@right (Mem.perm m b i Cur Nonempty) (not (Mem.perm m b i Cur Nonempty)) n)) (@proj_sumbool (Mem.perm m2 b i Cur Nonempty) (not (Mem.perm m2 b i Cur Nonempty)) (@left (Mem.perm m2 b i Cur Nonempty) (not (Mem.perm m2 b i Cur Nonempty)) p)) *)
  exfalso. rewrite M2 in n. contradiction.
Qed.

Lemma weak_valid_pointer_lessalloc {m m2} (M:mem_lessalloc m m2):
      Mem.weak_valid_pointer m = Mem.weak_valid_pointer m2.
Proof.
(* Goal: @eq (forall (_ : block) (_ : Z), bool) (Mem.weak_valid_pointer m) (Mem.weak_valid_pointer m2) *)
  unfold Mem.weak_valid_pointer.
(* Goal: @eq (forall (_ : block) (_ : Z), bool) (fun (b : block) (ofs : Z) => orb (Mem.valid_pointer m b ofs) (Mem.valid_pointer m b (Z.sub ofs (Zpos xH)))) (fun (b : block) (ofs : Z) => orb (Mem.valid_pointer m2 b ofs) (Mem.valid_pointer m2 b (Z.sub ofs (Zpos xH)))) *)
  extensionality b. extensionality i.
(* Goal: @eq bool (orb (Mem.valid_pointer m b i) (Mem.valid_pointer m b (Z.sub i (Zpos xH)))) (orb (Mem.valid_pointer m2 b i) (Mem.valid_pointer m2 b (Z.sub i (Zpos xH)))) *)
  rewrite (valid_pointer_lessalloc M); trivial.
Qed.


Definition juicy_mem_equiv jm1 jm2 := mem_equiv (m_dry jm1) (m_dry jm2) /\ m_phi jm1 = m_phi jm2.

Definition juicy_mem_lessdef jm1 jm2 := mem_lessdef (m_dry jm1) (m_dry jm2) /\ m_phi jm1 = m_phi jm2.

Definition juicy_mem_lessalloc jm1 jm2 := mem_lessdef (m_dry jm1) (m_dry jm2) /\ m_phi jm1 = m_phi jm2.

Ltac sync D :=
  first
    [ split; [destruct D as [D _] | destruct D as [_ D]]
    | destruct D as [|D]; [left|right]
    | let x := fresh in destruct D as (x, D); exists x
    | let x := fresh in intro x; specialize (D x)
    ].

Definition ext_spec_stable {M E Z} (R : M -> M -> Prop)
           (spec : external_specification M E Z) :=
  (forall e x b tl vl z m1 m2,
    R m1 m2 ->
    ext_spec_pre spec e x b tl vl z m1 ->
    ext_spec_pre spec e x b tl vl z m2) /\
  (forall e v m1 m2,
    R m1 m2 ->
    ext_spec_exit spec e v m1 ->
    ext_spec_exit spec e v m2).

(* Currently fails because jsafeN__ind is too weak. 
Lemma jsafeN__mem_equiv {G C Z HH Sem Jspec ge n z c jm1 jm2} :
  juicy_mem_equiv jm1 jm2 ->
  ext_spec_stable juicy_mem_equiv (JE_spec _ Jspec) ->
  @jsafeN_ G Z C HH Sem Jspec ge n z c jm1 ->
  @jsafeN_ G Z C HH Sem Jspec ge n z c jm2.
Proof.  intros E [Spre Sexit] S1.
  revert jm2 E. 
  induction S1 as
      [ z c jm1
      | n z c jm1 c' jm1' step safe IH
      | n z c jm1 ef args x atex Pre Post
      | n z c jm1 v Halt Exit ]; intros jm2 E.

  - constructor 1.

  - destruct (juicy_step_mem_equiv_sim E step) as (jm2' & E' & step').
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    econstructor 2; eauto.
    apply IH, E'.

  - econstructor 3 with (x := x); eauto.
    intros ret jm2' z' n' Hargsty Hretty Hn [-> [lev pure]] post.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    destruct (Post ret jm2' z' _ Hargsty Hretty Hn) as (c' & atex' & safe'); auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    + split; auto.
      destruct E as [Ed Ew].
      unfold juicy_safety.pures_eq in *.
      unfold juicy_safety.pures_sub in *.
      split.
      * repeat rewrite level_juice_level_phi in *.
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
        congruence.
      * revert pure.
        rewrite Ew.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
        auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    + exists c'; split; auto.

  - econstructor 4; eauto.
Qed.

Lemma jsafeN__mem_equiv {G C Z HH Sem Jspec ge n z c jm1 jm2} :
  juicy_mem_equiv jm1 jm2 ->
  ext_spec_stable juicy_mem_equiv (JE_spec _ Jspec) ->
  @jsafeN_ G Z C HH Sem Jspec ge n z c jm1 ->
  @jsafeN_ G Z C HH Sem Jspec ge n z c jm2.
Proof.
  intros E [Spre Sexit] S1.
  revert jm2 E.
  induction S1 as
      [ z c jm1
      | n z c jm1 c' jm1' step safe IH
      | n z c jm1 ef args x atex Pre Post
      | n z c jm1 v Halt Exit ]; intros jm2 E.

  - constructor 1.

  - destruct (juicy_step_mem_equiv_sim E step) as (jm2' & E' & step').
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    econstructor 2; eauto.
    apply IH, E'.

  - econstructor 3 with (x := x); eauto.
    intros ret jm2' z' n' Hargsty Hretty Hn [-> [lev pure]] post.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    destruct (Post ret jm2' z' _ Hargsty Hretty Hn) as (c' & atex' & safe'); auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    + split; auto.
      destruct E as [Ed Ew].
      unfold juicy_safety.pures_eq in *.
      unfold juicy_safety.pures_sub in *.
      split.
      * repeat rewrite level_juice_level_phi in *.
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
        congruence.
      * revert pure.
        rewrite Ew.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
        auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    + exists c'; split; auto.

  - econstructor 4; eauto.
Qed.

Lemma jsafeN_mem_lessdef {Z Jspec ge n z c jm1 jm2} :
  juicy_mem_lessdef jm1 jm2 ->
  ext_spec_stable juicy_mem_lessdef (JE_spec _ Jspec) ->
  @jsafeN Z Jspec ge n z c jm1 ->
  @jsafeN Z Jspec ge n z c jm2.
Proof.
  intros L [Spre Sexit] S1.
  revert jm2 L.
  induction S1 as
      [ z c jm1
      | n z c jm1 c' jm1' step safe IH
      | n z c jm1 ef args x atex Pre Post
      | n z c jm1 v Halt Exit ]; intros jm2 L.

  - constructor 1.

  - destruct (juicy_step_mem_lessdef_sim L step) as (jm2' & E' & step').
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    econstructor 2; eauto.
    apply IH, E'.

  - econstructor 3 with (x := x); eauto.
    intros ret jm2' z' n' Hargsty Hretty Hn [-> [lev pure]] post.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    destruct (Post ret jm2' z' _ Hargsty Hretty Hn) as (c' & atex' & safe'); auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    + split; auto.
      destruct L as [Ed Ew].
      unfold juicy_safety.pures_eq in *.
      unfold juicy_safety.pures_sub in *.
      split.
      * repeat rewrite level_juice_level_phi in *.
(* Goal: forall _ : @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)), @eq block (Mem.nextblock m1) (Mem.nextblock m2) *)
(* Goal: @eq Z (Zpos (Mem.nextblock m2)) (Zpos (Mem.nextblock m1)) *)
        congruence.
      * revert pure.
        rewrite Ew.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
        auto.
(* Goal: @eq (option (list Byte.int)) (@Some (list Byte.int) (@cons Byte.int i bl0)) (@Some (list Byte.int) (@cons Byte.int i bl0)) *)
    + exists c'; split; auto.

  - econstructor 4; eauto.
Qed.*)

Lemma mem_ext m1 m2 :
  Mem.mem_contents m1 = Mem.mem_contents m2 ->
  Mem.mem_access m1 = Mem.mem_access m2 ->
  Mem.nextblock m1 = Mem.nextblock m2 ->
  m1 = m2.
Proof.
  destruct m1, m2; simpl in *.
  intros <- <- <- .
(* Goal: @eq Mem.mem' (Mem.mkmem mem_contents mem_access nextblock access_max nextblock_noaccess contents_default) (Mem.mkmem mem_contents mem_access nextblock access_max0 nextblock_noaccess0 contents_default0) *)
  f_equal; apply proof_irr.
Qed.
