Module BTL_SEsimplifyMem


Rewriting theory involving symbolic memories in BTL symbolic execution. Main contents:

Require Import Coqlib AST Values Integers Memory Maps.
Require Import RelationClasses.
Require Import OptionMonad.
Require Import Op.
Require Import BTL BTL_SEtheory BTL_SEsimuref Memcpy.
Require Import ValueDomain.
Require Import Impure.ImpHCons.
Require Import Decidableplus Datatypes.

Import SvalNotations.
Import ListNotations.
Local Open Scope option_monad_scope.
Local Open Scope lazy_bool_scope.

Local Notation "a #* b" := (PXMap.get b a) (at level 1).

Local Opaque Z.add Z.sub.

Section IsIndexedAddr.

  Definition is_indexed_addr (addr : addressing) (ofs : ptrofs) : Prop :=
    forall F V (genv: Globalenvs.Genv.t F V) (sp: val) (args: list val) (rb : Values.block) (rofs : ptrofs),
    eval_addressing genv sp addr args = Some (Vptr rb rofs) <->
    exists bofs, args = Vptr rb bofs :: nil /\ rofs = Ptrofs.add bofs ofs.

  Local Obligation Tactic := simpl; intros.
  Local Transparent Archi.ptr64.
  Program Definition test_is_indexed (addr : addressing):
    {ofs : ptrofs | is_indexed_addr addr ofs} + {True} :=
    match addr with
    | Aindexed iofs => inleft (exist _ _ _)
    | _ => inright _
    end.
  Next Obligation.
    (* Depending on the architecture, we may need to convert [iofs].
       An alternative to this test would be to define [test_is_indexed] for each architecture. *)
    solve [exact iofs
          |exact (Ptrofs.of_int iofs)
          |exact (Ptrofs.of_int64 iofs)
          |exact (if Archi.ptr64
                  then Ptrofs.of_int64 (Int64.repr iofs)
                  else Ptrofs.of_int (Int.repr iofs))].
  Defined.
  Local Obligation Tactic := program_simpl.
  Solve All Obligations.
  Next Obligation.
    unfold test_is_indexed_obligation_1, is_indexed_addr, eval_addressing;
      try unfold Archi.ptr64;
      try unfold eval_addressing32, eval_addressing64;
      unfold Val.offset_ptr, Val.add, Val.addl;
      intros.
    split.
    + repeat autodestruct. repeat first [injection 1 as <- <- | intro]; eauto;
      try (injection H; clear H; intros H; feapply Val.addptr_ptrofs_inv; subst; eauto).
    + intros (? & -> & ->). try (rewrite Val.addptr_ptrofs); simpl; reflexivity.
  Qed.
  Local Opaque Archi.ptr64.
  Global Opaque test_is_indexed.

  Lemma is_indexed_addr_case [addr ofs] (ADDR : is_indexed_addr addr ofs)
    [F V] (genv: Globalenvs.Genv.t F V) sp args
    :
    (exists b bofs,
      eval_addressing genv sp addr args = Some (Vptr b (Ptrofs.add bofs ofs)) /\
      args = Vptr b bofs :: nil) \/
    (match eval_addressing genv sp addr args with
     | Some (Vptr b rofs) => False
     | _ => True
     end).
  Proof.
    specialize (ADDR F V genv sp args). revert ADDR.
    destruct (eval_addressing genv sp addr args) as [[]|]; simpl; eauto.
    intro EQV.
    destruct (EQV b i) as [[bofs EQ] _]. reflexivity.
    case EQ as [-> ->]; eauto.
  Qed.

  Lemma is_indexed_addr_eval [addr ofs] (ADDR : is_indexed_addr addr ofs)
    [F V] (genv: Globalenvs.Genv.t F V) sp b bofs:
    eval_addressing genv sp addr (Vptr b bofs :: nil) = Some (Vptr b (Ptrofs.add bofs ofs)).
  Proof.
    eapply proj2 in ADDR. rewrite ADDR; eauto.
  Qed.

End IsIndexedAddr.


Additionnal properties of Mem
Section LemmasMemory.


Preservation of memory operations success
  Lemma store_success_iff chk m b ofs v:
    Mem.store chk m b ofs v <> None <-> Mem.valid_access m chk b ofs Writable.
  Proof.
    split; intro H.
    - case Mem.store as [|] eqn:STORE. 2:congruence.
      eapply Mem.store_valid_access_3. eauto.
    - eapply Mem.valid_access_store in H as [? ->].
      congruence.
  Qed.

  Lemma store_fail_iff chk m b ofs v:
    Mem.store chk m b ofs v = None <-> ~Mem.valid_access m chk b ofs Writable.
  Proof.
    rewrite <- (not_iff_compat (store_success_iff chk m b ofs v)).
    destruct Mem.store; split; intro H1; try congruence.
    exfalso. apply H1. intro. congruence.
  Qed.

  Lemma load_success_iff chk m b ofs:
    Mem.load chk m b ofs <> None <-> Mem.valid_access m chk b ofs Readable.
  Proof.
    split; intro H.
    - case Mem.load as [|] eqn:LOAD. 2:congruence.
      eapply Mem.load_valid_access. eauto.
    - eapply Mem.valid_access_load in H as [? ->].
      congruence.
  Qed.

  Lemma loadbytes_success_iff len m b ofs:
    Mem.loadbytes m b ofs len <> None <-> Mem.range_perm m b ofs (ofs + len) Cur Readable.
  Proof.
    split; intro H.
    - case Mem.loadbytes as [|] eqn:X; try congruence.
      eapply Mem.loadbytes_range_perm. eauto.
    - feapply Mem.range_perm_loadbytes. congruence.
  Qed.

  Lemma storebytes_success_iff bytes m b ofs:
    Mem.storebytes m b ofs bytes <> None <-> Mem.range_perm m b ofs (ofs + Z.of_nat (Datatypes.length bytes)) Cur Writable.
  Proof.
    split; intro H.
    - case Mem.storebytes as [|] eqn:X; try congruence.
      eapply Mem.storebytes_range_perm. eauto.
    - case (Mem.range_perm_storebytes m b ofs bytes); auto. congruence.
  Qed.

  Lemma memmove_success_iff sz bdst odst bsrc osrc rm wm:
    memmove sz bdst odst bsrc osrc rm wm <> None <-> ( Mem.range_perm rm bsrc osrc (osrc + (Zpos sz)) Cur Readable
                                                       /\ Mem.range_perm wm bdst odst (odst + (Zpos sz)) Cur Writable ).
  Proof.
    split; intro H.
    - case memmove as [|] eqn:X; try congruence.
      eapply memmove_range_perm. eauto.
    - destruct H; feapply range_perm_memmove. congruence.
  Qed.

  Lemma memcpy_success_iff chk bmal bdst odst bsrc osrc rm wm:
    memcpy chk bmal bdst odst bsrc osrc rm wm <> None <-> (memcpy_args_ok chk bmal bdst odst bsrc osrc
                                                     /\ Mem.range_perm rm bsrc osrc (osrc + (Zpos (cpy_sz chk))) Cur Readable
                                                     /\ Mem.range_perm wm bdst odst (odst + (Zpos (cpy_sz chk))) Cur Writable ).
  Proof.
    split; intro H.
    - case memcpy as [|] eqn:X; try congruence.
      rewrite memcpy_Some_equiv in *. destruct X as (OK & MOVE).
      exploit memmove_range_perm; eauto.
    - intros X. rewrite memcpy_None_equiv in X. intuition.
      feapply range_perm_memmove. congruence.
  Qed.

  Lemma memcpy_fail_iff chk bmal bdst odst bsrc osrc rm wm:
    memcpy chk bmal bdst odst bsrc osrc rm wm = None <-> (memcpy_args_ok chk bmal bdst odst bsrc osrc ->
                                                     ~ (Mem.range_perm rm bsrc osrc (osrc + (Zpos (cpy_sz chk))) Cur Readable
                                                        /\ Mem.range_perm wm bdst odst (odst + (Zpos (cpy_sz chk))) Cur Writable)).
  Proof.
    rewrite memcpy_None_equiv in *.
    rewrite <- (not_iff_compat (memmove_success_iff (cpy_sz chk) bdst odst bsrc osrc rm wm)).
    destruct memmove; intuition congruence.
  Qed.

  Lemma perm_store_iff [chunk m1 b ofs v m2]:
    Mem.store chunk m1 b ofs v = Some m2 ->
    forall (b' : Values.block) (ofs' : Z) (k : perm_kind) (p : permission),
    Mem.perm m1 b' ofs' k p <-> Mem.perm m2 b' ofs' k p.
  Proof.
    split; [eapply Mem.perm_store_1|eapply Mem.perm_store_2]; eassumption.
  Qed.

  Lemma store_valid_access_iff [chunk m1 b ofs v m2]:
    Mem.store chunk m1 b ofs v = Some m2 ->
    forall (chunk' : memory_chunk) (b' : Values.block) (ofs' : Z) (p : permission),
    Mem.valid_access m1 chunk' b' ofs' p <-> Mem.valid_access m2 chunk' b' ofs' p.
  Proof.
    split; [eapply Mem.store_valid_access_1|eapply Mem.store_valid_access_2]; eassumption.
  Qed.

  Lemma range_perm_store_iff [chunk m1 b ofs v m2]:
    Mem.store chunk m1 b ofs v = Some m2 ->
    forall (b' : Values.block) (lo hi: Z) (k : perm_kind) (p : permission),
    Mem.range_perm m1 b' lo hi k p <-> Mem.range_perm m2 b' lo hi k p.
  Proof.
    intros; unfold Mem.range_perm; setoid_rewrite perm_store_iff at 1; eauto.
    reflexivity.
  Qed.

  Lemma memcpy_fail_store_iff [chunk bmal m1 b ofs v m2]:
    Mem.store chunk m1 b ofs v = Some m2 ->
    forall chk bdst odst bsrc osrc rm,
    (memcpy chk bmal bdst odst bsrc osrc rm m1 = None) <-> (memcpy chk bmal bdst odst bsrc osrc rm m2 = None).
  Proof.
    intros; rewrite !memcpy_fail_iff, !range_perm_store_iff with (m1:=m1) (m2:=m2); eauto.
    reflexivity.
  Qed.

  Lemma memcpy_valid_access_iff [chk bmal bdst odst bsrc osrc rm m1 m2]:
    memcpy chk bmal bdst odst bsrc osrc rm m1 = Some m2 ->
    forall (chunk' : memory_chunk) (b' : Values.block) (ofs' : Z) (p : permission),
    Mem.valid_access m1 chunk' b' ofs' p <-> Mem.valid_access m2 chunk' b' ofs' p.
  Proof.
    unfold Mem.valid_access. intros; erewrite range_perm_memcpy_iff; eauto.
    reflexivity.
  Qed.

  Lemma memcpy_fail_memcpy_iff [chk bmal bdst odst bsrc osrc rm m1 m2]:
    memcpy chk bmal bdst odst bsrc osrc rm m1 = Some m2 ->
    forall chk' bmal' bdst' odst' bsrc' osrc' rm',
    (memcpy chk' bmal' bdst' odst' bsrc' osrc' rm' m1 = None) <-> (memcpy chk' bmal' bdst' odst' bsrc' osrc' rm' m2 = None).
  Proof.
    intros; rewrite !memcpy_fail_iff, !range_perm_memcpy_iff with (m1:=m1) (m2:=m2); eauto.
    reflexivity.
  Qed.

Theory of mem_equiv_on: a stronger version of Mem.unchanged_on, not *preserved* by alloc and free. Thus typically for reasoning within BTL blocks.
  Section Equiv_on.

    Definition memct_t := PXMap.t (ZXMap.xmap_default Mem.memval_default).

    Definition memct_get (b : Values.block) (ofs : Z) (m : memct_t) : memval :=
      ZXMap.get ofs (PXMap.get b m).

    Definition memct_set (b : Values.block) (ofs : Z) (v : memval) (m : memct_t) : memct_t :=
      PXMap.set b (ZXMap.set ofs v (PXMap.get b m)) m.

    Definition eq_on_frame : Type := (Values.block -> Z -> Prop).
    Variable P : eq_on_frame.

    Definition memct_equiv_on (m0 m1 : memct_t) : Prop :=
      forall b ofs, P b ofs -> memct_get b ofs m0 = memct_get b ofs m1.

    Record mem_equiv_on (m0 m1 : mem) : Prop :=
      mk_mem_equiv_on {
        EQ_ACCESS : Mem.mem_access m0 = Mem.mem_access m1;
        EQ_ALIGN : Mem.mem_align m0 = Mem.mem_align m1;
        EQ_NEXTBLOCK : Mem.nextblock m0 = Mem.nextblock m1;
        EQ_CTNT : memct_equiv_on (Mem.mem_contents m0) (Mem.mem_contents m1);
    }.

    Lemma mem_equiv_on_perm [m0 m1] (E: mem_equiv_on m0 m1) b ofs k p:
      Mem.perm m0 b ofs k p <-> Mem.perm m1 b ofs k p.
    Proof.
      unfold Mem.perm; apply EQ_ACCESS in E as ->; reflexivity.
    Qed.

    Lemma mem_equiv_on_valid_access [m0 m1] (E : mem_equiv_on m0 m1) chk b ofs p:
      Mem.valid_access m0 chk b ofs p <-> Mem.valid_access m1 chk b ofs p.
    Proof.
      unfold Mem.valid_access, Mem.range_perm.
      setoid_rewrite (mem_equiv_on_perm E).
      reflexivity.
    Qed.

    Lemma mem_equiv_on_range_perm [m0 m1] (E : mem_equiv_on m0 m1) b lo hi k p:
       Mem.range_perm m0 b lo hi k p <-> Mem.range_perm m1 b lo hi k p.
    Proof.
      unfold Mem.range_perm. setoid_rewrite (mem_equiv_on_perm E).
      reflexivity.
    Qed.

    Lemma mem_equiv_on_memcpy_success [m0 m1] (E : mem_equiv_on m0 m1) chk bmal bdst odst bsrc osrc rm:
     (memcpy chk bmal bdst odst bsrc osrc rm m0 <> None) <-> (memcpy chk bmal bdst odst bsrc osrc rm m1 <> None).
    Proof.
      intros; rewrite !memcpy_success_iff, !(mem_equiv_on_range_perm E).
      reflexivity.
    Qed.

    Lemma mem_equiv_on_get [m0 m1] (E : mem_equiv_on m0 m1) b ofs
      (H : P b ofs):
      ZXMap.get ofs (PXMap.get b (Mem.mem_contents m0)) =
      ZXMap.get ofs (PXMap.get b (Mem.mem_contents m1)).
    Proof.
      apply E in H. apply H.
    Qed.

    Lemma mem_equiv_on_all m0 m1
      (ALL : forall b i, P b i)
      (EQ : mem_equiv_on m0 m1):
      m0 = m1.
    Proof.
      apply Mem.mem_same_proof_irr; try apply EQ.
      case EQ as [_ _ _ CT2].
      apply PXMap.extensionality. intros.
      apply ZXMap.extensionality; intros. apply CT2; auto.
    Qed.

    Lemma load_equiv_on m0 m1 chk b ofs:
      mem_equiv_on m0 m1 ->
      (forall i, ofs <= i < ofs + size_chunk chk -> P b i) ->
      Mem.load chk m0 b ofs = Mem.load chk m1 b ofs.
    Proof.
      intros EQ HP.
      specialize (load_success_iff chk m0 b ofs).
        rewrite (mem_equiv_on_valid_access EQ).
        rewrite <- load_success_iff.
      case (Mem.load chk m0 b ofs) as [v0|] eqn:L0, (Mem.load chk m1 b ofs) as [v1|] eqn:L1; cycle 1;
        try solve [reflexivity | intros [F0 F1]; exfalso; (apply F0 + apply F1); congruence].
      intros _; apply Mem.load_result in L0 as ->, L1 as ->; do 2 f_equal.
      apply Mem.getN_exten; rewrite <- size_chunk_conv.
      intros; apply mem_equiv_on_get; auto.
    Qed.

    Local Transparent Mem.loadbytes.
    Lemma loadbytes_equiv_on m0 m1 b ofs len:
      mem_equiv_on m0 m1 ->
      (forall i, ofs <= i < ofs + (Zpos len) -> P b i) ->
      Mem.loadbytes m0 b ofs (Zpos len) = Mem.loadbytes m1 b ofs (Zpos len).
    Proof.
      intros EQ HP.
      specialize (loadbytes_success_iff (Zpos len) m0 b ofs).
      rewrite (mem_equiv_on_range_perm EQ).
      rewrite <- loadbytes_success_iff.
      unfold Mem.loadbytes.
      case Mem.range_perm_dec; case Mem.range_perm_dec; try intuition congruence.
      intros _ _ _. f_equal. apply Mem.getN_exten.
      rewrite Z2Nat.id by auto with zarith. intros; apply mem_equiv_on_get; auto.
    Qed.
    Local Opaque Mem.loadbytes.

    Lemma memcpy_read_equiv_on rm0 rm1 chk bmal bdst odst bsrc osrc wm:
      mem_equiv_on rm0 rm1 ->
      (forall ofs, osrc <= ofs < osrc + Zpos (cpy_sz chk) -> P bsrc ofs) ->
      memcpy chk bmal bdst odst bsrc osrc rm0 wm = memcpy chk bmal bdst odst bsrc osrc rm1 wm.
    Proof.
      intros EQ HP.
      unfold memcpy, memmove. erewrite loadbytes_equiv_on; eauto.
    Qed.

  End Equiv_on.

  Local Instance memct_equiv_on_Equivalence {P}:
    Equivalence (memct_equiv_on P).
  Proof.
    unfold memct_equiv_on; constructor.
    - repeat constructor.
    - intros x y H. symmetry. apply H; auto.
    - intros x y z H H0; (etransitivity; [apply H|apply H0]); auto.
  Qed.

  Global Instance mem_equiv_on_Equivalence {P}:
    Equivalence (mem_equiv_on P).
  Proof.
    constructor.
    - constructor; reflexivity.
    - constructor; symmetry; apply H.
    - constructor; (etransitivity; [apply H|apply H0]).
  Qed.

  Lemma memct_equiv_on_weaken (P0 P1 : eq_on_frame) m0 m1
    (E : memct_equiv_on P0 m0 m1)
    (HP : forall b p, P1 b p -> P0 b p):
    memct_equiv_on P1 m0 m1.
  Proof.
    unfold memct_equiv_on; auto.
  Qed.

  Lemma mem_equiv_on_weaken (P0 P1 : eq_on_frame) m0 m1
    (E : mem_equiv_on P0 m0 m1)
    (HP : forall b p, P1 b p -> P0 b p):
    mem_equiv_on P1 m0 m1.
  Proof.
    case E; split; eauto using memct_equiv_on_weaken.
  Qed.

  Lemma memct_gsspec b ofs v m0 b' ofs':
    memct_get b' ofs' (memct_set b ofs v m0) =
    if peq b' b && zeq ofs' ofs then v else memct_get b' ofs' m0.
  Proof.
    unfold memct_get, memct_set.
    rewrite PXMap.gsspec; case peq as [->|]. 2:reflexivity.
    rewrite ZXMap.gsspec; unfold ZIndexed.eq; case zeq as [->|]; reflexivity.
  Qed.

  Lemma memct_set_eq1 b ofs v m0:
    memct_equiv_on (fun b' ofs' => ~(b' = b /\ ofs' = ofs)) m0 (memct_set b ofs v m0).
  Proof.
    intros b' ofs' NEQ; simpl in NEQ.
    rewrite memct_gsspec.
    unfold proj_sumbool; do 2 (autodestruct; simpl; auto).
    tauto.
  Qed.

  Lemma memct_set_eq2 P b ofs v m0 m1
    (E : memct_equiv_on P m0 m1):
    memct_equiv_on
      (fun b' ofs' => P b' ofs' \/ (b' = b /\ ofs' = ofs))
      (memct_set b ofs v m0) (memct_set b ofs v m1).
  Proof.
    intros b' ofs' H; simpl in H.
    rewrite !memct_gsspec.
    unfold proj_sumbool. do 2 try (autodestruct; simpl; intros _).
    auto.
    all:apply E; tauto.
  Qed.

  Fixpoint memct_setN (b : Values.block) (vl : list memval) (p : Z) (m : memct_t) : memct_t :=
    match vl with
    | nil => m
    | v :: vl => memct_setN b vl (p + 1) (memct_set b p v m)
    end.

  Lemma mem_setN_ctnt (m : memct_t) (mb : ZXMap.t Mem.memval_default) (b : Values.block) (vl : list memval) (p : Z):
    PXMap.set b (Mem.setN vl p mb) m = memct_setN b vl p (PXMap.set b mb m).
  Proof.
    revert mb p; induction vl; simpl; intros.
    - reflexivity.
    - rewrite IHvl; f_equal.
      unfold memct_set.
      rewrite PXMap.gss, PXMap.set2.
      reflexivity.
  Qed.

  Lemma memct_setN_equiv_on1 b bytes: forall ofs c,
    memct_equiv_on
     (fun b' ofs' => ~(b' = b /\ ofs <= ofs' < ofs + Z.of_nat (Datatypes.length bytes)))
     c (memct_setN b bytes ofs c).
  Proof.
    induction bytes; intros.
      + reflexivity.
      + simpl length; rewrite Nat2Z.inj_succ; simpl.
        etransitivity; cycle 1.
        * eapply memct_equiv_on_weaken. apply IHbytes.
          all:simpl; lia.
        * eapply memct_equiv_on_weaken. apply memct_set_eq1.
          all:simpl; lia.
  Qed.

  Lemma store_equiv_on1 chk m b p v m'
    (ST : Mem.store chk m b p v = Some m'):
    mem_equiv_on (fun b' p' => ~(b' = b /\ p <= p' < p + size_chunk chk)) m m'.
  Proof.
    constructor.
    - apply Mem.store_access in ST; congruence.
    - apply Mem.store_align in ST; congruence.
    - apply Mem.nextblock_store in ST; congruence.
    - apply Mem.store_mem_contents in ST as ->.
      rewrite mem_setN_ctnt; generalize (Mem.mem_contents m); intro c.
      set (c0 := PXMap.set b c #* b c <: memct_t).
      transitivity c0. {
        unfold memct_equiv_on, c0, memct_get; simpl; intros.
        rewrite PXMap.gsspec; case peq as [->|]; auto.
      }
      erewrite size_chunk_conv, <-(encode_val_length chk v).
      apply memct_setN_equiv_on1; auto.
  Qed.

  Lemma storebytes_equiv_on1 m b ofs bytes m'
    (ST : Mem.storebytes m b ofs bytes = Some m'):
    mem_equiv_on (fun b' ofs' => ~(b' = b /\ ofs <= ofs' < ofs + Z.of_nat (List.length bytes))) m m'.
  Proof.
    constructor.
    - apply Mem.storebytes_access in ST; congruence.
    - apply Mem.storebytes_align in ST; congruence.
    - apply Mem.nextblock_storebytes in ST; congruence.
    - apply Mem.storebytes_mem_contents in ST as ->.
      rewrite mem_setN_ctnt; generalize (Mem.mem_contents m); intro c.
      set (c0 := PXMap.set b c #* b c <: memct_t).
      transitivity c0. {
        unfold memct_equiv_on, c0, memct_get; simpl; intros.
        rewrite PXMap.gsspec; case peq as [->|]; auto.
      }
      apply memct_setN_equiv_on1; auto.
  Qed.

  Lemma memcpy_equiv_on1 chk bmal bdst odst bsrc osrc rm m m':
    memcpy chk bmal bdst odst bsrc osrc rm m = Some m' ->
    mem_equiv_on (fun b' ofs' => ~(b' = bdst /\ odst <= ofs' < odst + Zpos (cpy_sz chk))) m m'.
  Proof.
    rewrite memcpy_Some_equiv. intros (_ & MOVE); revert MOVE.
    unfold memmove. autodestruct.
    intros; feapply storebytes_equiv_on1.
    erewrite Mem.loadbytes_length, Z2Nat.id; eauto with zarith.
  Qed.

  Lemma memct_setN_equiv_on2 b bytes: forall P ofs c0 c1
    (EQ: memct_equiv_on P c0 c1),
    memct_equiv_on (fun b' ofs' => P b' ofs' \/ (b' = b /\ ofs <= ofs' < ofs + Z.of_nat (Datatypes.length bytes)))
        (memct_setN b bytes ofs c0) (memct_setN b bytes ofs c1).
  Proof.
    induction bytes; intros.
    + eapply memct_equiv_on_weaken. apply EQ.
      all:simpl; intuition lia.
    + simpl length; rewrite Nat2Z.inj_succ; simpl.
      eapply memct_equiv_on_weaken. {
         eapply IHbytes, memct_set_eq2, EQ.
      }
      all:simpl; intuition lia.
  Qed.

  Lemma store_equiv_on2 P chk m0 m1 b p v m0' m1'
    (E : mem_equiv_on P m0 m1)
    (ST0 : Mem.store chk m0 b p v = Some m0')
    (ST1 : Mem.store chk m1 b p v = Some m1'):
    mem_equiv_on
      (fun b' p' => P b' p' \/ (b' = b /\ p <= p' < p + size_chunk chk)) m0' m1'.
  Proof.
    destruct E; constructor.
    - apply Mem.store_access in ST0, ST1; congruence.
    - apply Mem.store_align in ST0, ST1; congruence.
    - apply Mem.nextblock_store in ST0, ST1; congruence.
    - apply Mem.store_mem_contents in ST0 as ->, ST1 as ->.
      rewrite !mem_setN_ctnt.
      set (c0 := PXMap.set b _ _).
      set (c1 := PXMap.set b _ _).
      assert (E : memct_equiv_on P c0 c1). {
        unfold memct_equiv_on, c0, c1, memct_get; simpl; intros.
        rewrite !PXMap.gsspec; autodestruct; intros; subst; apply EQ_CTNT0; auto.
      }
      erewrite size_chunk_conv, <-(encode_val_length chk v).
      eapply memct_setN_equiv_on2; eauto.
  Qed.

  Lemma store_morph_equiv_on P chk m0 m1 b ofs v m0' m1'
    (E : mem_equiv_on P m0 m1)
    (ST0 : Mem.store chk m0 b ofs v = Some m0')
    (ST1 : Mem.store chk m1 b ofs v = Some m1'):
    mem_equiv_on P m0' m1'.
  Proof.
    eapply mem_equiv_on_weaken. eapply store_equiv_on2; eauto.
    all:simpl; tauto.
  Qed.

  Lemma storebytes_equiv_on2 P m0 m1 b ofs bytes m0' m1'
    (E : mem_equiv_on P m0 m1)
    (ST0 : Mem.storebytes m0 b ofs bytes = Some m0')
    (ST1 : Mem.storebytes m1 b ofs bytes = Some m1'):
    mem_equiv_on
      (fun b' ofs' => P b' ofs' \/ (b' = b /\ ofs <= ofs' < ofs + Z.of_nat (List.length bytes))) m0' m1'.
  Proof.
    destruct E; constructor.
    - apply Mem.storebytes_access in ST0, ST1; congruence.
    - apply Mem.storebytes_align in ST0, ST1; congruence.
    - apply Mem.nextblock_storebytes in ST0, ST1; congruence.
    - apply Mem.storebytes_mem_contents in ST0 as ->, ST1 as ->.
      rewrite !mem_setN_ctnt.
      set (c0 := PXMap.set b _ _).
      set (c1 := PXMap.set b _ _).
      assert (E : memct_equiv_on P c0 c1). {
        unfold memct_equiv_on, c0, c1, memct_get; simpl; intros.
        rewrite !PXMap.gsspec; autodestruct; intros; subst; apply EQ_CTNT0; auto.
      }
      eapply memct_setN_equiv_on2; eauto.
  Qed.

  Lemma memcpy_equiv_on2 P m0 m1 chk bmal bdst odst bsrc osrc rm m0' m1'
    (EQ : mem_equiv_on P m0 m1):
    (memcpy chk bmal bdst odst bsrc osrc rm m0 = Some m0') ->
    (memcpy chk bmal bdst odst bsrc osrc rm m1 = Some m1') ->
    mem_equiv_on (fun b' ofs' => P b' ofs' \/ (b' = bdst /\ odst <= ofs' < odst + Zpos (cpy_sz chk))) m0' m1'.
  Proof.
    rewrite !memcpy_Some_equiv. intros (_ & MOVE1) (_ & MOVE2); revert MOVE1 MOVE2.
    unfold memmove. autodestruct.
    intros; feapply storebytes_equiv_on2.
    erewrite Mem.loadbytes_length, Z2Nat.id; eauto with zarith.
  Qed.

  Lemma memcpy_morph_equiv_on P m0 m1 chk bmal bdst odst bsrc osrc rm m0' m1'
    (EQ : mem_equiv_on P m0 m1)
    (CPY1: memcpy chk bmal bdst odst bsrc osrc rm m0 = Some m0')
    (CPY2: memcpy chk bmal bdst odst bsrc osrc rm m1 = Some m1'):
    mem_equiv_on P m0' m1'.
  Proof.
    eapply mem_equiv_on_weaken. eapply memcpy_equiv_on2; eauto.
    all:simpl; tauto.
  Qed.

End LemmasMemory.

Symbolic & abstract address in a memory/memcpy chunk of size a_size

Record address : Set := mk_addr {
  a_size: positive;
  a_addr: addressing;
  a_args: list_sval;
  a_aval: option aval
}.

Definition psize_chunk (chunk:memory_chunk) : positive := Z.to_pos (size_chunk chunk).

Lemma psize_chunk_Zpos chunk: Zpos (psize_chunk chunk) = size_chunk chunk.
Proof.
  unfold psize_chunk; generalize (size_chunk_pos chunk). intros; rewrite Z2Pos.id; auto with zarith.
Qed.

Definition eval_address (ctx : iblock_common_context) (a : address): option (Values.block * ptrofs) :=
  SOME args <- eval_list_sval ctx (a_args a) IN
  SOME v <- eval_addressing (cge ctx) (csp ctx) (a_addr a) args IN
  ASSERT (if_Some_dec (a_aval a) (fun av => vmatch_dec (cbc ctx) v av)) IN
  match v with
  | Vptr b o => Some (b, o)
  | _ => None
  end.

Section DisjointnessCriteria.


  Definition vaddr_disjoint (v0 : Values.block * ptrofs) (sz0 : positive)
                            (v1 : Values.block * ptrofs) (sz1 : positive): Prop :=
    let (b0, ofs0) := v0 in
    let (b1, ofs1) := v1 in
    b0 <> b1 \/
    Ptrofs.unsigned ofs0 + (Zpos sz0) <= Ptrofs.unsigned ofs1 \/
    Ptrofs.unsigned ofs1 + (Zpos sz1) <= Ptrofs.unsigned ofs0.

  Definition addr_disjoint (ctx : iblock_common_context) (a0 a1 : address) :=
    if_Some (eval_address ctx a0) (fun v0 =>
    if_Some (eval_address ctx a1) (fun v1 =>
    vaddr_disjoint v0 (a_size a0) v1 (a_size a1))).

  Lemma addr_disjoint_sym ctx a0 a1:
    addr_disjoint ctx a0 a1 -> addr_disjoint ctx a1 a0.
  Proof.
    unfold addr_disjoint, vaddr_disjoint, if_Some.
    repeat autodestruct. lia.
  Qed.

  Remark addr_disjoint_irrefl ctx a: addr_disjoint ctx a a -> eval_address ctx a = None.
  Proof.
   unfold addr_disjoint, vaddr_disjoint, if_Some.
   autodestruct. destruct p as (b & ofs). lia.
  Qed.


  Let u := Ptrofs.unsigned.

  Definition offset_chunk_lt (ofs0 : ptrofs) (sz0 : positive)
                             (ofs1 : ptrofs) (sz1 : positive)
    := (u ofs0 + Zpos sz0) <= u ofs1 /\
       (u ofs1 + Zpos sz1) <= u ofs0 + Ptrofs.modulus.

  Definition offset_disjoint (ofs0 : ptrofs) (sz0 : positive)
                                   (ofs1 : ptrofs) (sz1 : positive)
    := offset_chunk_lt ofs0 sz0 ofs1 sz1 \/ offset_chunk_lt ofs1 sz1 ofs0 sz0.

  Lemma disjoint_interval_modulo (m : Z) (a b : Z) (al bl : Z) (c : Z):
    0 < m ->
    0 <= al -> 0 <= bl ->
    a + al <= b ->
    b + bl <= a + m ->
    (c + a) mod m + al <= (c + b) mod m \/ (c + b) mod m + bl <= (c + a) mod m.
  Proof.
    intros Hmpos Le0 Le1 Le2 Le3.
    rewrite !Z.mod_eq by lia.
    case (Z_le_lt_eq_dec ((c + a) / m) ((c + b) / m)) as [Wrap|NoWrap].
      { apply Z.div_le_mono; lia. }
    - right.
      assert (Le: (c + a) / m + 1 <= (c + b) / m) by lia.
      apply Zmult_le_compat_l with (p:=m) in Le; lia.
    - left. lia.
  Qed.

  Lemma offset_disjoint_computed_addr (bo : Z) ofs0 sz0 ofs1 sz1:
    offset_disjoint ofs0 sz0 ofs1 sz1 ->
    (bo + u ofs0) mod Ptrofs.modulus + Zpos sz0 <= (bo + u ofs1) mod Ptrofs.modulus \/
    (bo + u ofs1) mod Ptrofs.modulus + Zpos sz1 <= (bo + u ofs0) mod Ptrofs.modulus.
  Proof.
    specialize Ptrofs.modulus_pos as ?.
    intros [Lt|Lt]; [|apply or_comm];
      apply disjoint_interval_modulo; solve [apply Lt|lia].
  Qed.

  Lemma offset_disjoint_sound ctx a0 ofs0 a1 ofs1
    (A0: is_indexed_addr (a_addr a0) ofs0)
    (A1: is_indexed_addr (a_addr a1) ofs1)
    (B: list_sval_equiv ctx (a_args a0) (a_args a1))
    (D: offset_disjoint ofs0 (a_size a0) ofs1 (a_size a1)):
    addr_disjoint ctx a0 a1.
  Proof.
    unfold is_indexed_addr in A0, A1.
    unfold addr_disjoint, eval_address; rewrite <- B.
    repeat (autodestruct; simpl; try trivial); intros; right.
    eapply proj1 in A0, A1.
    exploit A0. eassumption.
    exploit A1. eassumption.
    intros (cofs1 & B1 & ->) (cofs0 & B0 & ->).
    replace cofs1 with cofs0 by congruence.
    unfold Ptrofs.add. rewrite !Ptrofs.unsigned_repr_eq. fold u.
    apply offset_disjoint_computed_addr; assumption.
  Qed.

Static criteria using the result of the abstract analysis, for -fprepass-alias-abs, the LCT and the store-motion.

  Lemma abs_disjoint_sound ctx a0 a1 aa0 aa1
    (AA0 : a_aval a0 = Some aa0)
    (AA1 : a_aval a1 = Some aa1)
    (D: vdisjoint aa0 (Zpos (a_size a0)) aa1 (Zpos (a_size a1)) = true):
    addr_disjoint ctx a0 a1.
  Proof.
    unfold addr_disjoint, eval_address; rewrite AA0, AA1.
    repeat (autodestruct; simpl; trivial; intro).
    eapply vdisjoint_sound; eauto.
  Qed.

End DisjointnessCriteria.


Section MemcpyLib.

Handling of fake smem from memcpy sequences

Definition fmcpy (mc: memcpy_args list_sval) (sm: smem)
 := fSmemcpy sm (mcpy_chk mc) (mcpy_daddr mc) (mcpy_dargs mc) (mcpy_saddr mc) (mcpy_sargs mc) sm (mcpy_info mc).

Lemma fmcpy_alive_monotonic ctx mc: forall sm,
  eval_smem ctx sm = None -> eval_smem ctx (fmcpy mc sm) = None.
Proof.
  unfold fmcpy; simplify_option.
Qed.

Lemma fmcpy_morph_smem_equiv ctx mc: forall sm1 sm2,
  smem_equiv ctx sm1 sm2 -> smem_equiv ctx (fmcpy mc sm1) (fmcpy mc sm2).
Proof.
  unfold fmcpy; cbn. simplify_option.
Qed.

Fixpoint fmcpy_merge (seq: list (memcpy_args list_sval)) (sm: smem) : smem :=
  match seq with
  | nil => sm
  | mc::seq0 => fmcpy_merge seq0 (fmcpy mc sm)
  end.

Local Hint Resolve fmcpy_alive_monotonic fmcpy_morph_smem_equiv: core.

Lemma fmcpy_merge_alive_monotonic ctx seq: forall sm,
  eval_smem ctx sm = None -> eval_smem ctx (fmcpy_merge seq sm) = None.
Proof.
  induction seq; cbn; eauto.
Qed.

Lemma fmcpy_merge_alive_back ctx seq sm:
  alive (eval_smem ctx (fmcpy_merge seq sm)) -> alive (eval_smem ctx sm).
Proof.
  intros ALIVE H. apply ALIVE, fmcpy_merge_alive_monotonic, H.
Qed.

Lemma fmcpy_merge_morph_smem_equiv ctx seq: forall sm1 sm2,
  smem_equiv ctx sm1 sm2 -> smem_equiv ctx (fmcpy_merge seq sm1) (fmcpy_merge seq sm2).
Proof.
  induction seq; cbn; eauto.
Qed.

Definition mcpy_da (mc: memcpy_args list_sval): address :=
  mk_addr (cpy_sz (mcpy_chk mc)) (mcpy_daddr mc) (mcpy_dargs mc) (memcpy_daaddr (mcpy_info mc)).

Definition mcpy_sa (mc: memcpy_args list_sval): address :=
  mk_addr (cpy_sz (mcpy_chk mc)) (mcpy_saddr mc) (mcpy_sargs mc) (memcpy_saaddr (mcpy_info mc)).

Lemma fmcpy_alive_eval_address ctx mc sm:
   alive (eval_smem ctx (fmcpy mc sm)) ->
   exists dst src m,
          eval_address ctx (mcpy_da mc) = Some dst
       /\ eval_address ctx (mcpy_sa mc) = Some src
       /\ eval_smem ctx sm = Some m
       /\ eval_smem ctx (fmcpy mc sm) = memcpy (mcpy_chk mc) (bmal_of (Mem.block_align (cm1 ctx)) (fst dst) (fst src)) (fst dst) (Ptrofs.unsigned (snd dst)) (fst src) (Ptrofs.unsigned (snd src)) m m.
Proof.
  unfold fmcpy, eval_address; cbn; do 8 autodestruct.
  destruct a.
  intros; do 3 eexists; split; autodestruct. cbn.
  repeat (econstructor; eauto).
Qed.

Lemma eval_address_fmcpy ctx mc sm dst src m:
  eval_smem ctx sm = Some m ->
  eval_address ctx (mcpy_da mc) = Some dst ->
  eval_address ctx (mcpy_sa mc) = Some src ->
  eval_smem ctx (fmcpy mc sm) = memcpy (mcpy_chk mc) (bmal_of (Mem.block_align (cm1 ctx)) (fst dst) (fst src)) (fst dst) (Ptrofs.unsigned (snd dst)) (fst src) (Ptrofs.unsigned (snd src)) m m.
Proof.
  unfold fmcpy, eval_address; simplify_option.
Qed.

End MemcpyLib.


Section EqualityTests.

address oa is a shift of address ta by offset ofs
Definition shift_address (ctx : iblock_common_context) (oa ta: address) (ofs: ptrofs) :=
  if_Some (eval_address ctx oa) (fun ov =>
  if_Some (eval_address ctx ta) (fun tv =>
                 fst ov = fst tv
              /\ snd ov = Ptrofs.add (snd tv) ofs
  )).

Definition pure_fast_eq [A: Set] (h : A -> hashcode) (x0 x1 : A) : {x0 = x1}+{True}.
Proof.
  case (PureComparisons.fast_eq h x0 x1) eqn:T.
  - left; eapply PureComparisons.fast_eq_correct, T; auto with wlp.
  - right; constructor.
Qed.


Definition test_shift_rel (oa ta: address) (ofs: ptrofs): bool :=
  if pure_fast_eq list_sval_get_hid (a_args oa) (a_args ta)
  then
    match test_is_indexed (a_addr oa) with
    | inright _ => false
    | inleft oo =>
    match test_is_indexed (a_addr ta) with
    | inright _ => false
    | inleft to =>
      Ptrofs.eq_dec (` oo) (Ptrofs.add (` to) ofs) ||| false
    end end
  else false.

Lemma test_shift_rel_correct ctx oa ta ofs:
  test_shift_rel oa ta ofs = true ->
  shift_address ctx oa ta ofs.
Proof.
  unfold test_shift_rel. repeat autodestruct.
  intros _ _ _ _ _.
  destruct s as (oo & Hoo), s0 as (to & Hto). cbn in *.
  unfold shift_address, eval_address.
  unfold if_Some.
  do 4 autodestruct. cbn.
  intros EQ _ EVALo.
  eapply is_indexed_addr_case in Hoo.
  erewrite EVALo in Hoo.
  destruct Hoo as [(ob & oo0 & EQo & EQl)|]; contradiction || subst.
  rewrite e; clear e.
  try_simplify_someHyps.
  intros EVALoa EVALov.
  erewrite is_indexed_addr_eval; eauto.
  autodestruct. cbn.
  intros.
  repeat (split; auto with zarith).
  rewrite Ptrofs.add_assoc. auto.
Qed.
Global Opaque test_shift_rel.

Definition test_pshift (op tp: aptr) (ofs: ptrofs) : bool :=
  match op, tp with
  | Pbot, _ => true
  | _, Pbot => true
  | Gl oid oo, Gl tid to =>
      QualIdent.eq oid tid
      &&& (Ptrofs.eq_dec oo (Ptrofs.add to ofs) ||| false)
  | Stk oo, Stk to =>
      Ptrofs.eq_dec oo (Ptrofs.add to ofs) ||| false
  | _, _ => false
  end.

Lemma test_pshift_correct (bc: block_classification) op tp ofs ob oo tb to:
  pmatch bc ob oo op -> pmatch bc tb to tp ->
  test_pshift op tp ofs = true ->
  ob = tb /\ oo = Ptrofs.add to ofs.
Proof.
  unfold test_pshift. destruct bc. cbn.
  destruct 1; destruct 1; try congruence;
  repeat autodestruct; cbn in *; subst; intuition eauto.
Qed.

Definition test_ashift (oav tav: aval) (ofs: ptrofs): bool :=
  match oav with
  | Uns op _ | Sgn op _ | Ptr op | Ifptr op =>
    match tav with
    | Uns tp _ | Sgn tp _ | Ptr tp | Ifptr tp => test_pshift op tp ofs
    | _ => true
    end
  | _ => true
  end.

Lemma test_ashift_correct bc oav tav ofs ob oo tb to:
  vmatch bc (Vptr ob oo) oav ->
  vmatch bc (Vptr tb to) tav ->
  test_ashift oav tav ofs = true ->
  ob = tb /\ oo = Ptrofs.add to ofs.
Proof.
  unfold test_ashift. intros Mo Mt EQ.
  inv Mo; inv Mt; eapply test_pshift_correct; eauto.
Qed.
Global Opaque test_ashift.

Definition test_shift_addr (oa ta: address) (ofs: ptrofs): bool :=
  test_shift_rel oa ta ofs |||
    match a_aval oa, a_aval ta with
    | Some oav, Some tav => test_ashift oav tav ofs
    | _, _ => false
    end.

Lemma test_shift_addr_correct ctx oa ta ofs:
  test_shift_addr oa ta ofs = true -> shift_address ctx oa ta ofs.
Proof.
  unfold test_shift_addr.
  repeat autodestruct.
  + intros; apply test_shift_rel_correct; auto.
  + intros ? ? _ TEST.
    unfold shift_address, if_Some, eval_address.
    try_simplify_someHyps; cbn.
    repeat autodestruct; cbn.
    intros. eapply test_ashift_correct in TEST; eauto.
Qed.

Definition test_eq_live_abs (oa ta: address): bool :=
    match a_aval oa, a_aval ta with
    | Some oav, Some tav => test_ashift oav tav Ptrofs.zero
    | _, _ => false
    end.

Lemma test_eq_live_abs_correct ctx oa ta:
  alive (eval_address ctx oa) ->
  alive (eval_address ctx ta) ->
  test_eq_live_abs oa ta = true -> eval_address ctx oa = eval_address ctx ta.
Proof.
  unfold test_eq_live_abs.
  repeat autodestruct.
  intros ? ? ALIVEo ALIVEa TEST.
  unfold eval_address in *.
  repeat autodestruct.
  intros ? _ ? ? ? _ ?. subst. cbn in *. try_simplify_someHyps.
  intros; eapply test_ashift_correct in TEST; eauto.
  destruct TEST as (-> & ->).
  rewrite Ptrofs.add_zero. auto.
Qed.
Global Opaque test_eq_live_abs.


Definition test_eq_addr (oa ta : address): bool :=
 pure_fast_eq list_sval_get_hid (a_args oa) (a_args ta)
 &&& (eq_addressing (a_addr oa) (a_addr ta)
      &&& (option_eq eq_aval (a_aval oa) (a_aval ta) ||| false))
 .

Lemma test_eq_addr_correct ctx oa ta:
  test_eq_addr oa ta = true -> eval_address ctx oa = eval_address ctx ta.
Proof.
  unfold test_eq_addr; repeat autodestruct; intuition auto.
  unfold eval_address;
  replace (a_args oa) with (a_args ta);
  replace (a_addr oa) with (a_addr ta);
  replace (a_aval oa) with (a_aval ta).
  reflexivity.
Qed.
Global Opaque test_eq_addr.


Definition test_eq_live_addr (oa ta : address): bool :=
  test_eq_live_abs oa ta
  ||| test_eq_addr oa ta
  .

Lemma test_eq_live_addr_correct ctx oa ta:
  test_eq_live_addr oa ta = true ->
  alive (eval_address ctx oa) ->
  alive (eval_address ctx ta) ->
  eval_address ctx oa = eval_address ctx ta.
Proof.
  unfold test_eq_live_addr; repeat autodestruct.
  + intros; eapply test_eq_live_abs_correct; auto.
  + intros; eapply test_eq_addr_correct; auto.
Qed.
Global Opaque test_eq_live_addr.

Definition test_pcmp (p1 p2: aptr): option comparison :=
  match p1, p2 with
  | Gl id1 o1, Gl id2 o2 =>
      ASSERT QualIdent.eq id1 id2 IN
      Some (Ptrofs.unsigned o1 ?= Ptrofs.unsigned o2)
  | Stk o1, Stk o2 =>
      Some (Ptrofs.unsigned o1 ?= Ptrofs.unsigned o2)
  | _, _ => None
  end.

Lemma test_pcmp_correct (bc: block_classification) p1 p2 b1 o1 b2 o2 cmp:
  pmatch bc b1 o1 p1 -> pmatch bc b2 o2 p2 ->
  test_pcmp p1 p2 = Some cmp ->
  b1 = b2 /\ (Ptrofs.unsigned o1 ?= Ptrofs.unsigned o2) = cmp.
Proof.
  unfold test_pcmp. destruct bc. cbn.
  destruct 1; destruct 1; try congruence;
  simplify_option.
Qed.

Definition test_acmp (av1 av2: aval): option comparison :=
  match av1 with
  | Uns p1 _ | Sgn p1 _ | Ptr p1 | Ifptr p1 =>
    match av2 with
    | Uns p2 _ | Sgn p2 _ | Ptr p2 | Ifptr p2 => test_pcmp p1 p2
    | _ => None
    end
  | _ => None
  end.

Lemma test_acmp_correct bc av1 av2 b1 o1 b2 o2 cmp:
  vmatch bc (Vptr b1 o1) av1 ->
  vmatch bc (Vptr b2 o2) av2 ->
  test_acmp av1 av2 = Some cmp ->
  b1 = b2 /\ (Ptrofs.unsigned o1 ?= Ptrofs.unsigned o2) = cmp.
Proof.
  unfold test_acmp. intros Mo Mt EQ.
  inv Mo; inv Mt; eapply test_pcmp_correct; eauto.
Qed.
Global Opaque test_acmp.

Definition test_cmp_addr (oa1 oa2: address): option comparison :=
    SOME av1 <- a_aval oa1 IN
    SOME av2 <- a_aval oa2 IN
    test_acmp av1 av2.

Lemma test_cmp_addr_correct ctx oa1 oa2 r1 r2 cmp:
  test_cmp_addr oa1 oa2 = Some cmp ->
  eval_address ctx oa1 = Some r1 ->
  eval_address ctx oa2 = Some r2 ->
  fst r1 = fst r2 /\ (Ptrofs.unsigned (snd r1) ?= Ptrofs.unsigned (snd r2)) = cmp.
Proof.
  unfold test_cmp_addr; unfold eval_address; simplify_option.
  intros; eapply test_acmp_correct; eauto.
Qed.
Global Opaque test_cmp_addr.

End EqualityTests.



Section RewritingRules.

Definition aSload sm trap chk addr args aaddr :=
  fSmayUndef_opt
    (SOME aaddr <- aaddr IN Some (fOKaddrMatch addr args aaddr))
    (fSload sm trap chk addr args).

Definition eval_aSload_def_0 trap (v : option val) : option val :=
  match v with
  | Some v => Some v
  | None =>
      match trap with
      | TRAP => None
      | NOTRAP => Some Vundef
      end
  end.

Definition eval_aSload_def_1 ctx trap chk addr args m :=
  SOME args <- eval_list_sval ctx args IN
  match trap with
  | TRAP =>
      SOME v <- eval_addressing (cge ctx) (csp ctx) addr args IN
      match v with
      | Vptr b ofs =>
          match Mem.load chk m b (Ptrofs.unsigned ofs) with
          | Some v => Some Vundef
          | None => None
          end
      | _ => None
      end
  | NOTRAP => Some Vundef
  end.

Lemma eval_aSload_def_1_unchanged ctx trap chk addr args m0 m1
  (EQ_PERM : forall b ofs k p, Mem.perm m0 b ofs k p <-> Mem.perm m1 b ofs k p):
  eval_aSload_def_1 ctx trap chk addr args m0 = eval_aSload_def_1 ctx trap chk addr args m1.
Proof.
  unfold eval_aSload_def_1; repeat autodestruct; [intros LKO LOK|intros LOK LKO]; exfalso;
  (eapply load_success_iff; [|eapply LKO]);
  apply Mem.load_valid_access in LOK; revert LOK;
  unfold Mem.valid_access, Mem.range_perm; setoid_rewrite EQ_PERM; auto.
Qed.

Lemma eval_aSload_eq ctx sm m trap chk addr args aaddr
  (MEM : eval_smem ctx sm = Some m):
  eval_sval ctx (aSload sm trap chk addr args aaddr) =
  match eval_address ctx (mk_addr (psize_chunk chk) addr args aaddr) with
  | Some (b, ofs) => eval_aSload_def_0 trap (Mem.load chk m b (Ptrofs.unsigned ofs))
  | None => eval_aSload_def_1 ctx trap chk addr args m
  end.
Proof.
  unfold aSload, eval_address, eval_aSload_def_0, eval_aSload_def_1, if_Some_dec; simpl.
  destruct aaddr; simpl;
  unfold adp_addr_match_dec, adp_addr_match, if_Some_dec, Mem.loadv, proj_sumbool; simpl;
  rewrite MEM;
  repeat (autodestruct; simpl).
Qed.

Lemma eval_aSstore_eq ctx sm chk addr args sinfo sv hc:
  eval_smem ctx (Sstore sm chk addr args sinfo sv hc) =
  SOME a <- eval_address ctx (mk_addr (psize_chunk chk) addr args (store_aaddr sinfo)) IN
  let (b, ofs) := a in
  SOME v <- eval_sval ctx sv IN
  SOME m <- eval_smem ctx sm IN
  Mem.store chk m b (Ptrofs.unsigned ofs) v.
Proof.
  simpl. unfold eval_address, Mem.storev. simpl.
  do 2 autodestruct.
  case adp_store_dec, if_Some_dec; intuition try congruence.
  repeat (simpl; autodestruct).
Qed.

Lemma eval_aSmemcpy_eq ctx sm chk daddr dargs saddr sargs rom minfo hc:
  eval_smem ctx (Smemcpy sm chk daddr dargs saddr sargs rom minfo hc) =
  SOME da <- eval_address ctx (mk_addr (cpy_sz chk) daddr dargs (memcpy_daaddr minfo)) IN
  SOME sa <- eval_address ctx (mk_addr (cpy_sz chk) saddr sargs (memcpy_saaddr minfo)) IN
  let (bdst, odst) := da in
  let (bsrc, osrc) := sa in
  SOME rm <- eval_smem ctx rom IN
  SOME wm <- eval_smem ctx sm IN
  memcpy chk (bmal_of (Mem.block_align (cm1 ctx)) bdst bsrc) bdst (Ptrofs.unsigned odst) bsrc (Ptrofs.unsigned osrc) rm wm.
Proof.
  unfold eval_address. cbn. symmetry.
  repeat autodestruct.
Qed.

Rules to reorder stores


Definition smem_reorderable (a0: address) (rew0: smem -> hashcode -> smem) (a1: address) (rew1: smem -> hashcode -> smem) : Prop :=
  forall ctx sm hc0 hc1 hc0' hc1', addr_disjoint ctx a0 a1 ->
      smem_equiv ctx (rew0 (rew1 sm hc1) hc0) (rew1 (rew0 sm hc0') hc1').

Definition store_reorderable (a0: address) (rew0: smem -> smem): Prop
  := forall chk1 addr1 args1 sv1 sinfo1,
      smem_reorderable a0 (fun sm _ => rew0 sm) (mk_addr (psize_chunk chk1) addr1 args1 (store_aaddr sinfo1))
                                                (fun sm => Sstore sm chk1 addr1 args1 sinfo1 sv1).

Lemma store_store_reorderable chk0 addr0 args0 sv0 sinfo0:
  store_reorderable (mk_addr (psize_chunk chk0) addr0 args0 (store_aaddr sinfo0))
                    (fun sm => fSstore sm chk0 addr0 args0 sinfo0 sv0).
Proof.
  unfold store_reorderable, smem_reorderable, fSstore, addr_disjoint.
  intros until hc1'.
  rewrite !eval_aSstore_eq.
  do 2 (case eval_address as [[]|]; [|solve [repeat autodestruct]]); cbn.
  repeat autodestruct.
  2,3:
    repeat (let H := fresh "H" in intro H; try apply store_fail_iff in H);
    try ((idtac + symmetry); apply store_fail_iff);
    eauto using Mem.store_valid_access_2.
  intros. rewrite !psize_chunk_Zpos in *.
  eapply Mem.store_store_other; eauto.
Qed.

Lemma store_memcpy_reorderable_aux (sm : smem) (chk0: memory_chunk) chk1
  addr args sv sinfo daddr dargs saddr sargs rom minfo:
  smem_reorderable (mk_addr (psize_chunk chk0) addr args (store_aaddr sinfo))
                   (fun sm => Sstore sm chk0 addr args sinfo sv)
                   (mk_addr (cpy_sz chk1) daddr dargs (memcpy_daaddr minfo))
                   (fun sm => Smemcpy sm chk1 daddr dargs saddr sargs rom minfo).
Proof.
  unfold smem_reorderable, addr_disjoint.
  intros until hc1'.
  rewrite !eval_aSstore_eq, !eval_aSmemcpy_eq. cbn.
  unfold Mem.storev.
  destruct eval_address as [[]|] eqn: ADDR; cbn in *.
  2: { repeat autodestruct. unfold adp_store in *.
       intros.
       revert ADDR. unfold eval_address.
       try_simplify_someHyps.
       autodestruct.
  }
  destruct (eval_address _ (mk_addr _ daddr _ _)) as [[]|] eqn: DADDR; cbn in *. 2: { repeat autodestruct. }
  destruct (eval_address _ (mk_addr _ saddr _ _)) as [[]|] eqn: SADDR; cbn in *. 2: { repeat autodestruct. }
  autodestruct. 2: { repeat autodestruct. }
  do 2 autodestruct. 2: { repeat autodestruct. }
  autodestruct. 2: { repeat autodestruct. intros.
       rewrite memcpy_fail_store_iff in *; eauto.
  }
  intros. revert ADDR; unfold eval_address, adp_store_dec, Mem.storev. cbn.
  do 4 autodestruct. intros; inv ADDR. rewrite !psize_chunk_Zpos in *.
  autodestruct. 2: {
    rewrite !store_fail_iff, memcpy_valid_access_iff; eauto.
  }
  intros STORE1.
  exploit memcpy_store_diamond; eauto.
  - unfold disjoint. lia.
  - intros (? & ? & ?); congruence.
Qed.

Definition memcpy_reorderable (a0: address) (rew0: smem -> smem): Prop
  := forall chk1 daddr dargs saddr sargs rom minfo,
      smem_reorderable a0 (fun sm _ => rew0 sm)
                   (mk_addr (cpy_sz chk1) daddr dargs (memcpy_daaddr minfo))
                   (fun sm => Smemcpy sm chk1 daddr dargs saddr sargs rom minfo).

Lemma store_memcpy_reorderable chk0 addr0 args0 sv0 sinfo0:
  memcpy_reorderable (mk_addr (psize_chunk chk0) addr0 args0 (store_aaddr sinfo0))
                     (fun sm => fSstore sm chk0 addr0 args0 sinfo0 sv0).
Proof.
  unfold memcpy_reorderable, fSstore, smem_reorderable.
  intros; exploit (store_memcpy_reorderable_aux sm); eauto.
Qed.

Lemma memcpy_store_reorderable chk daddr dargs saddr sargs rom minfo:
   store_reorderable (mk_addr (cpy_sz chk) daddr dargs (memcpy_daaddr minfo))
                     (fun sm => fSmemcpy sm chk daddr dargs saddr sargs rom minfo).
Proof.
  unfold store_reorderable, fSmemcpy, smem_reorderable.
  intros; exploit (store_memcpy_reorderable_aux sm); eauto.
  apply addr_disjoint_sym; auto.
Qed.

Lemma memcpy_memcpy_reorderable chk daddr dargs saddr sargs rom minfo:
   memcpy_reorderable (mk_addr (cpy_sz chk) daddr dargs (memcpy_daaddr minfo))
                      (fun sm => fSmemcpy sm chk daddr dargs saddr sargs rom minfo).
Proof.
  unfold memcpy_reorderable, smem_reorderable, fSmemcpy, addr_disjoint.
  intros until hc1'.
  rewrite !eval_aSmemcpy_eq. cbn.
  destruct (eval_address _ (mk_addr _ daddr _ _)) as [[]|] eqn: DADDR; cbn in *. 2: { repeat autodestruct. }
  destruct (eval_address _ (mk_addr _ saddr _ _)) as [[]|] eqn: SADDR; cbn in *. 2: { repeat autodestruct. }
  destruct (eval_address _ (mk_addr _ daddr0 _ _)) as [[]|] eqn: DADDR0; cbn in *. 2: { repeat autodestruct. }
  destruct (eval_address _ (mk_addr _ saddr0 _ _)) as [[]|] eqn: SADDR0; cbn in *. 2: { repeat autodestruct. }
  autodestruct. 2: { repeat autodestruct. }
  do 3 autodestruct. 2: { repeat autodestruct. intros.
    erewrite memcpy_fail_memcpy_iff in EQ0. eauto.
    eapply EQ.
  }
  autodestruct. 2: { intros.
    rewrite memcpy_fail_memcpy_iff in EQ; eauto.
  }
  intros.
  exploit memcpy_diamond. eapply EQ. eapply EQ0.
  - unfold disjoint. lia.
  - intros (? & ? & ?); congruence.
Qed.


Definition sm_reorderable (a0: address) (rew0: smem -> smem) :=
     store_reorderable a0 rew0
  /\ memcpy_reorderable a0 rew0
  .

Lemma store_sm_reorderable chk0 addr0 args0 sv0 sinfo0:
  sm_reorderable (mk_addr (psize_chunk chk0) addr0 args0 (store_aaddr sinfo0))
                 (fun sm => fSstore sm chk0 addr0 args0 sinfo0 sv0).
Proof.
  split.
  - apply store_store_reorderable.
  - apply store_memcpy_reorderable.
Qed.

Lemma memcpy_sm_reorderable chk daddr dargs saddr sargs rom minfo:
   sm_reorderable (mk_addr (cpy_sz chk) daddr dargs (memcpy_daaddr minfo))
                  (fun sm => fSmemcpy sm chk daddr dargs saddr sargs rom minfo).
Proof.
  split.
  - apply memcpy_store_reorderable.
  - apply memcpy_memcpy_reorderable.
Qed.


Rules to rewrite under loads and stores


Inductive smem_equiv_on (P : eq_on_frame) (ctx : iblock_common_context) (sm0 sm1 : smem)
  : Prop
  := Smem_equiv_on m0 m1
      (EVAL_M0 : eval_smem ctx sm0 = Some m0)
      (EVAL_M1 : eval_smem ctx sm1 = Some m1)
      (EQ_ON : mem_equiv_on P m0 m1).

Lemma smem_equiv_on_refl P ctx sm:
  alive (eval_smem ctx sm) ->
  smem_equiv_on P ctx sm sm.
Proof.
  case eval_smem as [m|] eqn:M. 2:congruence.
  exists m m; auto. reflexivity.
Qed.

Global Instance smem_equiv_on_PER {P ctx}: PER (smem_equiv_on P ctx).
Proof.
  split.
  - intros ? ? []. econstructor; eauto. symmetry; assumption.
  - intros ? ? ? [m0 m1 E0 E1 EQ0] [m1' m2 E1' E2 EQ1].
    rewrite E1 in E1'. injection E1' as ?. subst m1'.
    exists m0 m2; eauto.
    etransitivity; eassumption.
Qed.

Lemma apply_store_smem_equiv_on P ctx sm0 sm1 chk addr sargs sinfo sv hc0 hc1:
  smem_equiv_on P ctx sm0 sm1 ->
  let sm0' := Sstore sm0 chk addr sargs sinfo sv hc0 in
  let sm1' := Sstore sm1 chk addr sargs sinfo sv hc1 in
  alive (eval_smem ctx sm0') ->
  smem_equiv_on P ctx sm0' sm1'.
Proof.
  intros [m0 m1 M0 M1 EM].
  cbn zeta; rewrite eval_aSstore_eq, M0.
  repeat autodestruct. intros EVAL _ EADDR.
  intros M0'. apply elim_alive in M0' as (m0' & M0').
  apply Mem.store_valid_access_3 in M0' as A0.
  apply (mem_equiv_on_valid_access _ EM) in A0.
  eapply Mem.valid_access_store in A0 as [m1' M1'].
  exists m0' m1'.
    1,2:rewrite eval_aSstore_eq, EADDR, EVAL, ?M0, ?M1; eassumption.
  eapply store_morph_equiv_on; eauto.
Qed.

Lemma apply_memcpy_smem_equiv_on P ctx sm0 sm1 chk daddr dargs saddr sargs rm minfo hc0 hc1:
  smem_equiv_on P ctx sm0 sm1 ->
  let sm0' := Smemcpy sm0 chk daddr dargs saddr sargs rm minfo hc0 in
  let sm1' := Smemcpy sm1 chk daddr dargs saddr sargs rm minfo hc1 in
  alive (eval_smem ctx sm0') ->
  smem_equiv_on P ctx sm0' sm1'.
Proof.
  intros [m0 m1 M0 M1 EM].
  cbn zeta; rewrite eval_aSmemcpy_eq, M0.
  repeat autodestruct. intros EVAL _ _ SADDR DADDR.
  intros M0'. apply elim_alive in M0' as (m0' & M0').
  cut (Some m0' <> None). 2: congruence.
  rewrite <- M0', mem_equiv_on_memcpy_success; eauto.
  destruct (memcpy _ _ _ _ _ _ _ m1) as [m1'|] eqn: M1'; try congruence.
  intros _.
  exists m0' m1'.
    1,2:rewrite eval_aSmemcpy_eq; try_simplify_someHyps.
  eapply memcpy_morph_equiv_on; eauto.
Qed.


Definition store_crange (ctx : iblock_common_context) (a : address) : eq_on_frame :=
  (fun b' p' => if_Some (eval_address ctx a) (fun av => let (b, ofs) := av in
                let p := Ptrofs.unsigned ofs in
                ~(b' = b /\ p <= p' < p + Zpos (a_size a)))).

Lemma rewrite_store_equiv_on ctx sm0 sm1 (chk: memory_chunk) addr sargs sinfo sv hc0 hc1 :
  let a := mk_addr (psize_chunk chk) addr sargs (store_aaddr sinfo) in
  let sm0' := Sstore sm0 chk addr sargs sinfo sv hc0 in
  let sm1' := Sstore sm1 chk addr sargs sinfo sv hc1 in
  smem_equiv_on (store_crange ctx a) ctx sm0 sm1 ->
  smem_equiv ctx sm0' sm1'.
Proof.
  cbn zeta; rewrite !eval_aSstore_eq.
  do 3 autodestruct; intros EVAL _ EADDR.
  intros [m0 m1 -> -> EM].
  do 2 destruct Mem.store eqn:? in |-*;
    (progress f_equal ||
    (exfalso;
     exploit Mem.store_valid_access_3; eauto;
     intro V; eapply (mem_equiv_on_valid_access _ EM) in V;
     eapply Mem.valid_access_store with (v := v) in V as [? ?]; congruence)).
  eapply mem_equiv_on_all; cycle -1.
  eapply store_equiv_on2; eauto.
  simpl. unfold store_crange. rewrite EADDR; simpl.
  intro b'; intros; rewrite !psize_chunk_Zpos; case (peq b' b); tauto.
Qed.

Lemma remove_store_smem_equiv_on ctx sm0 (chk: memory_chunk) addr sargs sinfo sv hc:
  let a := mk_addr (psize_chunk chk) addr sargs (store_aaddr sinfo) in
  let sm1 := Sstore sm0 chk addr sargs sinfo sv hc in
  forall (MALIVE: alive (eval_smem ctx sm1)),
  smem_equiv_on (store_crange ctx a) ctx sm0 sm1.
Proof.
  cbn zeta. rewrite eval_aSstore_eq.
  repeat autodestruct; intros EMEM EVAL _ EADDR.
  intros M1; apply elim_alive in M1 as (m1 & STORE).
  eexists _ m1; eauto.
  - rewrite eval_aSstore_eq, EADDR, EVAL, EMEM. exact STORE.
  - eapply mem_equiv_on_weaken. eapply store_equiv_on1, STORE.
    simpl; unfold store_crange. rewrite EADDR; simpl.
    intros ? ?; rewrite psize_chunk_Zpos; auto.
Qed.

Lemma remove_memcpy_smem_equiv_on ctx sm0 chk daddr dargs saddr sargs rom minfo hc:
  let a := mk_addr (cpy_sz chk) daddr dargs (memcpy_daaddr minfo) in
  let sm1 := Smemcpy sm0 chk daddr dargs saddr sargs rom minfo hc in
  forall (MALIVE: alive (eval_smem ctx sm1)),
  smem_equiv_on (store_crange ctx a) ctx sm0 sm1.
Proof.
  cbn zeta. rewrite eval_aSmemcpy_eq.
  repeat autodestruct. intros WMEM RMEM _ _ SADDR DADDR.
  intros M1; apply elim_alive in M1 as (m1 & CPY).
  eexists _ m1; eauto.
  - rewrite eval_aSmemcpy_eq; try_simplify_someHyps.
  - eapply mem_equiv_on_weaken. eapply memcpy_equiv_on1, CPY.
    simpl; unfold store_crange. rewrite DADDR; cbn.
    auto.
Qed.

Definition load_range (ctx : iblock_common_context) (a : address) : eq_on_frame :=
  (fun b i => exists ofs, eval_address ctx a = Some (b, ofs) /\
                          Ptrofs.unsigned ofs <= i < Ptrofs.unsigned ofs + Zpos (a_size a)).

Lemma rewrite_load_equiv_on ctx sm0 sm1 trap (chk: memory_chunk) addr sargs aaddr:
  let a := mk_addr (psize_chunk chk) addr sargs aaddr in
  smem_equiv_on (load_range ctx a) ctx sm0 sm1 ->
  sval_equiv ctx (aSload sm0 trap chk addr sargs aaddr)
                 (aSload sm1 trap chk addr sargs aaddr).
Proof.
  intros a [].
  erewrite !eval_aSload_eq by eassumption.
  case eval_address as [[]|] eqn:ADDR.
    2:{ apply eval_aSload_def_1_unchanged. eapply mem_equiv_on_perm, EQ_ON. }
  f_equal.
  eapply load_equiv_on. apply EQ_ON.
  intros; eexists; simpl. rewrite psize_chunk_Zpos; eauto.
Qed.

Lemma rewrite_memcpy_read_equiv_on ctx rm0 rm1 chk daddr dargs saddr sargs sm minfo:
  let sa := mk_addr (cpy_sz chk) saddr sargs (memcpy_saaddr minfo) in
  smem_equiv_on (load_range ctx sa) ctx rm0 rm1 ->
  smem_equiv ctx (fSmemcpy sm chk daddr dargs saddr sargs rm0 minfo)
                 (fSmemcpy sm chk daddr dargs saddr sargs rm1 minfo).
Proof.
  intros sa []; unfold fSmemcpy.
  erewrite !eval_aSmemcpy_eq by eassumption.
  simplify_option.
  intros; eapply memcpy_read_equiv_on; eauto.
  intros; eexists; cbn; split; eauto.
Qed.

Lemma disjoint_store_smem_equiv_on ctx a sm0 (chk: memory_chunk) addr sargs sinfo sv hc
  (DJ : addr_disjoint ctx a (mk_addr (psize_chunk chk) addr sargs (store_aaddr sinfo))):
  let range := load_range ctx a in
  let sm1 := Sstore sm0 chk addr sargs sinfo sv hc in
  forall (MALIVE: alive (eval_smem ctx sm1)),
  smem_equiv_on range ctx sm0 sm1.
Proof.
  cbn zeta; intro.
  apply remove_store_smem_equiv_on in MALIVE as [m0 m1 E0 E1 EQ].
  eexists m0 m1; auto.
  eapply mem_equiv_on_weaken. apply EQ.
  unfold load_range, store_crange; simpl; try tauto.
  setoid_rewrite if_Some_iff.
  intros b' i' (ofs & EADDR0 & RANGE0) (?, ?) EADDR1 [? RANGE1]; subst b'.
  unfold addr_disjoint in DJ; rewrite EADDR0, EADDR1 in DJ; simpl in DJ.
  case DJ as [|DJ]; [congruence|lia].
Qed.

Lemma disjoint_memcpy_smem_equiv_on ctx a sm0 chk daddr dargs saddr sargs rom minfo hc
  (DJ : addr_disjoint ctx a (mk_addr (cpy_sz chk) daddr dargs (memcpy_daaddr minfo))):
  let range := load_range ctx a in
  let sm1 := Smemcpy sm0 chk daddr dargs saddr sargs rom minfo hc in
  forall (MALIVE: alive (eval_smem ctx sm1)),
  smem_equiv_on range ctx sm0 sm1.
Proof.
  cbn zeta; intro.
  apply remove_memcpy_smem_equiv_on in MALIVE as [m0 m1 E0 E1 EQ].
  eexists m0 m1; auto.
  eapply mem_equiv_on_weaken. apply EQ.
  unfold load_range, store_crange; simpl; try tauto.
  setoid_rewrite if_Some_iff.
  intros b' i' (ofs & EADDR0 & RANGE0) (?, ?) EADDR1 [? RANGE1]; subst b'.
  unfold addr_disjoint in DJ; rewrite EADDR0, EADDR1 in DJ; simpl in DJ.
  case DJ as [|DJ]; [congruence|lia].
Qed.

End RewritingRules.


Section DisjointnessTest.


Program Definition test_offset_lt (ofs0 : ptrofs) (sz0 : positive)
                                  (ofs1 : ptrofs) (sz1 : positive)
  : {offset_chunk_lt ofs0 sz0 ofs1 sz1}+{True} :=
  if zle (Ptrofs.unsigned ofs0 + Zpos sz0) (Ptrofs.unsigned ofs1)
  then if zle (Ptrofs.unsigned ofs1 + Zpos sz1) (Ptrofs.unsigned ofs0 + Ptrofs.modulus)
  then left _ else right _ else right _.
Next Obligation.
unfold offset_chunk_lt. auto. Qed.

Program Definition test_offset_disjoint (ofs0 : ptrofs) (sz0 : positive)
                                        (ofs1 : ptrofs) (sz1 : positive)
  : {offset_disjoint ofs0 sz0 ofs1 sz1}+{True} :=
  if test_offset_lt ofs0 sz0 ofs1 sz1
  then left _
  else if test_offset_lt ofs1 sz1 ofs0 sz0
  then left _ else right _.
Solve All Obligations with (unfold offset_disjoint; auto).

Program Definition test_disjoint_rel (a0 a1 : address)
  : {forall ctx, addr_disjoint ctx a0 a1}+{True} :=
  if pure_fast_eq list_sval_get_hid (a_args a0) (a_args a1)
  then
    match test_is_indexed (a_addr a0) with
    | inright _ => right _
    | inleft ofs0 =>
    match test_is_indexed (a_addr a1) with
    | inright _ => right _
    | inleft ofs1 => if test_offset_disjoint ofs0 (a_size a0) ofs1 (a_size a1)
                     then left _ else right _
    end end
  else right _.
Next Obligation.
  eapply offset_disjoint_sound; eauto.
  congruence.
Qed.
Global Opaque test_disjoint_rel.


Definition test_disjoint_abs (a0 a1 : address)
  : {forall ctx, addr_disjoint ctx a0 a1}+{True}.
  case (a_aval a0) as [aa0|] eqn:AA0; [|right; trivial].
  case (a_aval a1) as [aa1|] eqn:AA1; [|right; trivial].
  case (vdisjoint aa0 (Zpos (a_size a0))
                  aa1 (Zpos (a_size a1))) eqn:D;
    [|right; trivial].
  left; intros.
  eapply abs_disjoint_sound; eauto.
Defined.
Global Opaque test_disjoint_abs.


Program Definition test_disjoint (rel abs : bool) (a0 a1 : address)
  : {forall ctx, addr_disjoint ctx a0 a1}+{True} :=
  if (if rel then test_disjoint_rel a0 a1 else right _)
  then left _
  else if abs
  then test_disjoint_abs a0 a1
  else right _.

End DisjointnessTest.



Section RRImplAlias.


  Variable p_test_disjoint : forall (a0 a1 : address),
    {forall ctx : iblock_common_context, addr_disjoint ctx a0 a1} + {True}.

  Local Obligation Tactic := try solve [program_simpl]; cbn beta; intros; subst.


Program Fixpoint rewrite_stores_under_load (sm: smem) (a0 : address) {struct sm}
  : {sm' : smem |
      forall ctx (MALIVE : alive (eval_smem ctx sm)), smem_equiv_on (load_range ctx a0) ctx sm' sm}
  := match sm with
  | Sstore sm1 chk1 addr1 sargs1 sinfo1 sv1 _ =>
      let sm1' := rewrite_stores_under_load sm1 a0 in
      let a1 := mk_addr (psize_chunk chk1) addr1 sargs1 (store_aaddr sinfo1) in
      if p_test_disjoint a0 a1
      then sm1'
      else fSstore sm1' chk1 addr1 sargs1 sinfo1 sv1
  | Smemcpy sm1 chk1 daddr1 dargs1 saddr1 sargs1 rom minfo _ =>
      let sm1' := rewrite_stores_under_load sm1 a0 in
      let a1 := mk_addr (cpy_sz chk1) daddr1 dargs1 (memcpy_daaddr minfo) in
      if p_test_disjoint a0 a1
      then sm1'
      else fSmemcpy sm1' chk1 daddr1 dargs1 saddr1 sargs1 rom minfo
  | Sinit _ => sm
  end.
Next Obligation.
  etransitivity.
  - apply (proj2_sig sm1'); auto. revert MALIVE. simpl; repeat autodestruct.
  - apply disjoint_store_smem_equiv_on; auto.
Defined.
Next Obligation.
  symmetry. apply apply_store_smem_equiv_on.
  - symmetry. apply (proj2_sig sm1'); auto.
    revert MALIVE; simpl; repeat autodestruct.
  - exact MALIVE.
Defined.
Next Obligation.
  etransitivity.
 - apply (proj2_sig sm1'); auto. revert MALIVE. simpl; repeat autodestruct.
 - apply disjoint_memcpy_smem_equiv_on; auto.
Defined.
Next Obligation.
  symmetry. apply apply_memcpy_smem_equiv_on.
  - symmetry. apply (proj2_sig sm1'); auto.
    revert MALIVE; simpl; repeat autodestruct.
  - exact MALIVE.
Defined.
Next Obligation.
  apply smem_equiv_on_refl. exact MALIVE.
Qed.
Global Opaque rewrite_stores_under_load.

Program Definition rewrite_load_impl (sm: smem)
  (trap : trapping_mode) (chk: memory_chunk) (addr: addressing) (sargs : list_sval) aaddr
  : {sv : sval |
      forall ctx (MALIVE : alive (eval_smem ctx sm)),
        sval_equiv ctx sv (aSload sm trap chk addr sargs aaddr)}
  := aSload (rewrite_stores_under_load sm (mk_addr (psize_chunk chk) addr sargs aaddr)) trap chk addr sargs aaddr.
Next Obligation.
  case rewrite_stores_under_load as [sm' SM].
  eapply rewrite_load_equiv_on; auto.
Qed.
Global Opaque rewrite_load_impl.


Program Definition rewrite_memcpy_read (sm: smem) chk (daddr: addressing) (dargs : list_sval) (saddr: addressing) (sargs : list_sval) (rom: smem) minfo:
  {sm' : smem |
      forall ctx (RMALIVE : alive (eval_smem ctx rom)),
        smem_equiv ctx sm' (fSmemcpy sm chk daddr dargs saddr sargs rom minfo) } :=
   let saaddr := mk_addr (cpy_sz chk) saddr sargs (memcpy_saaddr minfo) in
   fSmemcpy sm chk daddr dargs saddr sargs (rewrite_stores_under_load rom saaddr) minfo.
Next Obligation.
  case rewrite_stores_under_load as [sm' SM].
  eapply rewrite_memcpy_read_equiv_on; eauto.
Qed.
Global Opaque rewrite_memcpy_read.

Definition store_num_lt (i0 i1 : store_num_t) : bool :=
  match i0, i1 with
  | SNumNone, _ | _, SNumNone => false
  | SNumInv i0, SNumInv i1 | SNumSrc i0, SNumSrc i1 => Pos.ltb i0 i1
  | SNumInv _, SNumSrc _ => true
  | SNumSrc _, SNumInv _ => false
  end.

Definition try_apply {A B} (f: A -> option B) (x:A) (catch: A -> B) : B :=
  match f x with
  | Some y => y
  | None => catch x
  end.

Fixpoint reorder_stores_rec (num0: store_num_t) (a0: address) (rew: smem -> smem) (sm: smem) {struct sm} : option smem :=
  match sm with
  | Sstore sm1 chk1 addr1 sargs1 sinfo1 sv1 _ =>
      let a1 := mk_addr (psize_chunk chk1) addr1 sargs1 (store_aaddr sinfo1) in
      ASSERT p_test_disjoint a0 a1 IN
      ASSERT store_num_lt num0 (store_num sinfo1) IN
      let sm2 := try_apply (reorder_stores_rec num0 a0 rew) sm1 rew in
      Some (fSstore sm2 chk1 addr1 sargs1 sinfo1 sv1)
  | Smemcpy sm1 chk1 daddr dargs saddr sargs rom minfo _ =>
      let a1 := mk_addr (cpy_sz chk1) daddr dargs (memcpy_daaddr minfo) in
      ASSERT p_test_disjoint a0 a1 IN
      ASSERT store_num_lt num0 (memcpy_num minfo) IN
      let sm2 := try_apply (reorder_stores_rec num0 a0 rew) sm1 rew in
      Some (fSmemcpy sm2 chk1 daddr dargs saddr sargs rom minfo)
  | _ => None
  end.

Lemma reorder_stores_rec_correct sm num0 a0 rew ctx sm':
  reorder_stores_rec num0 a0 rew sm = Some sm' -> sm_reorderable a0 rew -> smem_equiv ctx sm' (rew sm).
Proof.
  intros EQ (RES & REM). revert sm' EQ; unfold reorder_stores_rec, try_apply.
  Local Opaque eval_smem.
  induction sm; cbn; simplify_option.
  Local Transparent eval_smem.
  - intros; rewrite RES; eauto.
    cbn; erewrite <- IHsm; eauto.
  - intros; rewrite RES; auto.
  - intros; rewrite REM; auto.
    cbn; erewrite <- IHsm1; eauto.
  - intros; rewrite REM; auto.
Unshelve.
  all: auto.
Defined.
Global Opaque reorder_stores_rec.

Definition reorder_stores_gen sm num0 a0 rew := try_apply (reorder_stores_rec num0 a0 rew) sm rew.

Lemma reorder_stores_gen_correct sm num0 a0 rew ctx:
  sm_reorderable a0 rew -> smem_equiv ctx (reorder_stores_gen sm num0 a0 rew) (rew sm).
Proof.
  unfold reorder_stores_gen, try_apply.
  autodestruct.
  intros; feapply reorder_stores_rec_correct.
Qed.

Definition reorder_stores sm (chk: memory_chunk) (addr: addressing) (sargs : list_sval) (sinfo : store_info) (sv : sval)
 := reorder_stores_rec (store_num sinfo) (mk_addr (psize_chunk chk) addr sargs (store_aaddr sinfo))
                                          (fun sm => fSstore sm chk addr sargs sinfo sv) sm.

Lemma reorder_stores_correct sm (chk: memory_chunk) (addr: addressing) (sargs : list_sval) (sinfo : store_info) (sv : sval) ctx sm':
  reorder_stores sm chk addr sargs sinfo sv = Some sm' -> smem_equiv ctx sm' (fSstore sm chk addr sargs sinfo sv).
Proof.
  unfold reorder_stores; intros; exploit reorder_stores_rec_correct; eauto.
  apply store_sm_reorderable.
Qed.

Definition reorder_memcpy (mc: memcpy_args list_sval) sm
 := reorder_stores_gen sm (memcpy_num (mcpy_info mc)) (mcpy_da mc)
                           (fun sm0 => ` (rewrite_memcpy_read sm0 (mcpy_chk mc) (mcpy_daddr mc) (mcpy_dargs mc)
                                                                  (mcpy_saddr mc) (mcpy_sargs mc) sm (mcpy_info mc))).

Lemma reorder_memcpy_correct sm mc ctx:
  alive (eval_smem ctx sm) -> smem_equiv ctx (reorder_memcpy mc sm) (fmcpy mc sm).
Proof.
  intros; unfold reorder_memcpy. rewrite reorder_stores_gen_correct; auto.
  - destruct rewrite_memcpy_read as (sm0 & Hsm0). auto.
  - apply memcpy_sm_reorderable.
Qed.

End RRImplAlias.

Section RRImplStoreMotion.

Local Obligation Tactic := try solve [program_simpl]; cbn beta; intros; subst; eauto.

Definition ands [A B C D : Prop] := Sumbool.sumbool_and A B C D.

Program Definition test_address_eq (a0 a1 : address): {a0=a1}+{True} :=
  if ands (peq (a_size a0) (a_size a1)) (
     ands (eq_addressing (a_addr a0) (a_addr a1)) (
     ands (pure_fast_eq list_sval_get_hid (a_args a0) (a_args a1))
          (option_eq eq_aval (a_aval a0) (a_aval a1))))
  then in_left else in_right.
Next Obligation.
  intuition.
  destruct a0, a1; simpl in *; subst; reflexivity.
Qed.

When applying a store on x <- v on m := x_i <- v_i we can remove all the stores x_i <- v_i such that x_i = x.

Program Fixpoint rewrite_stores_under_store (sm: smem) (a0 : address) {struct sm}
  : {sm' : smem |
     forall ctx (MALIVE : alive (eval_smem ctx sm)), smem_equiv_on (store_crange ctx a0) ctx sm' sm}
  := match sm with
  | Sstore sm1 chk1 addr1 sargs1 sinfo1 sv1 hc =>
      let a1 := mk_addr (psize_chunk chk1) addr1 sargs1 (store_aaddr sinfo1) in
      if test_address_eq a0 a1
      then sm1
      else
        let sm1' := rewrite_stores_under_store sm1 a0 in
        fSstore sm1' chk1 addr1 sargs1 sinfo1 sv1
  | _ => sm
  end.
Next Obligation.
  apply remove_store_smem_equiv_on; auto.
Qed.
Next Obligation.
  symmetry; apply apply_store_smem_equiv_on; auto.
  symmetry; apply (proj2_sig sm1').
  revert MALIVE; simpl; repeat autodestruct.
Defined.
Next Obligation.
  apply smem_equiv_on_refl; auto.
Qed.
Global Opaque rewrite_stores_under_store.

Program Definition remove_overriden_store
  (sm : smem) (chk : memory_chunk) (addr : addressing) (sargs : list_sval) (sinfo : store_info)
  : {sm1 : smem |
     forall ctx (MALIVE : alive (eval_smem ctx sm)) sv,
     smem_equiv ctx (fSstore sm1 chk addr sargs sinfo sv) (fSstore sm chk addr sargs sinfo sv)}
  :=
    let a0 := mk_addr (psize_chunk chk) addr sargs (store_aaddr sinfo) in
    let sm' := rewrite_stores_under_store sm a0 in
    sm'.
Next Obligation.
  apply rewrite_store_equiv_on, (proj2_sig sm'), MALIVE.
Qed.

Program Definition rewrite_store_motion (reorder : bool)
  (sm : smem) (chk : memory_chunk) (addr : addressing) (sargs : list_sval) (sinfo : store_info)
  (sv : sval)
  : {sm1 : smem |
     forall ctx (MALIVE : alive (eval_smem ctx sm)),
     smem_equiv ctx sm1 (fSstore sm chk addr sargs sinfo sv)}
  :=
    let sm' := remove_overriden_store sm chk addr sargs sinfo in
    if reorder
    then match reorder_stores test_disjoint_abs sm' chk addr sargs sinfo sv with
         | Some sm1 => sm1
         | None => fSstore sm' chk addr sargs sinfo sv
         end
    else
      fSstore sm' chk addr sargs (set_store_num SNumNone sinfo) sv.
Next Obligation.
  exploit reorder_stores_correct; eauto.
  intros ->.
  rewrite (proj2_sig sm'); auto.
Qed.
Next Obligation.
  rewrite (proj2_sig sm'); auto.
Qed.
Next Obligation.
  rewrite <- (proj2_sig sm'); auto.
Qed.
Global Opaque rewrite_store_motion.

End RRImplStoreMotion.


Definition rrules_filter (RRULES: rrules_set) :=
  match RRULES with
  | RRschedule rel abs => Some (rel, abs)
  | RRlct _ true => Some (false, true)
  | RRstoreMotion true _ => Some (false, true)
  | _ => None
  end.

Definition rewrite_load (RRULES: rrules_set) (sm: smem)
  (trap : trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (aaddr: option aval)
  : option sval
  := match rrules_filter RRULES with
  | Some (rel, abs) => Some (proj1_sig
        (rewrite_load_impl (test_disjoint rel abs) sm trap chunk addr lsv aaddr))
  | _ => None
  end.

Lemma rewrite_load_correct
   (ctx : iblock_common_context) (RRULES: rrules_set) sm trap chunk addr sargs aaddr rew
   (RW: rewrite_load RRULES sm trap chunk addr sargs aaddr = Some rew):
   alive (eval_smem ctx sm) ->
   sval_equiv ctx rew (root_apply (Rload trap chunk addr aaddr) sargs sm).
Proof.
  unfold rewrite_load in RW.
  destruct rrules_filter as [[]|] in RW; [injection RW as <-|discriminate RW].
  case rewrite_load_impl as [rew H]; apply H.
Qed.
Global Opaque rewrite_load.

Definition rewrite_store (RRULES: rrules_set) (sm: smem)
  (chk: memory_chunk) (addr: addressing) (sargs : list_sval) (sinfo : store_info) (sv : sval)
  : option smem
  := match RRULES with
  | RRschedule rel abs => reorder_stores (test_disjoint rel abs) sm chk addr sargs sinfo sv
  | RRstoreMotion _ alias_store =>
      Some (proj1_sig (rewrite_store_motion alias_store sm chk addr sargs sinfo sv))
  | _ => None
  end.

Lemma rewrite_store_correct
   (ctx : iblock_common_context) (RRULES: rrules_set) sm chunk addr sargs sinfo sv rew:
   let sm1 := fSstore sm chunk addr sargs sinfo sv in forall
   (MALIVE : alive (eval_smem ctx sm1))
   (RW: rewrite_store RRULES sm chunk addr sargs sinfo sv = Some rew),
   smem_equiv ctx rew sm1.
Proof.
  intros.
  destruct RRULES; simpl in RW; try congruence.
  - (*Case RRschedule*)
    feapply reorder_stores_correct.
  - (*Case RRstoreMotion*)
    injection RW as <-; case rewrite_store_motion as [rw H]; apply H.
    intro DEAD; apply MALIVE; simpl; rewrite DEAD; repeat autodestruct.
Qed.
Global Opaque rewrite_store.

Definition rewrite_memcpy (RRULES: rrules_set) (mc: memcpy_args list_sval) sm: option smem :=
  if test_eq_live_addr (mcpy_da mc) (mcpy_sa mc)
  then Some sm
  else
    match rrules_filter RRULES with
    | Some (rel, abs) => Some (reorder_memcpy (test_disjoint rel abs) mc sm)
    | _ => None
    end.

Local Opaque eval_smem.

Lemma rewrite_memcpy_correct (ctx : iblock_common_context) (RRULES: rrules_set) mc sm rew:
  let sm1 := fmcpy mc sm in forall
  (MALIVE : alive (eval_smem ctx sm1))
  (RW: rewrite_memcpy RRULES mc sm = Some rew),
  smem_equiv ctx rew sm1.
Proof.
  unfold rewrite_memcpy. autodestruct.
  + (* skip case *)
    intros EQ ALIVE H; inv H.
    exploit fmcpy_alive_eval_address; eauto.
    destruct (eval_smem ctx (fmcpy mc rew)) as [m'|]; try congruence. clear ALIVE.
    intros ((bdst & odst) & (bsrc & osrc) & m & ? & ? & ? & H); cbn in *.
    eapply test_eq_live_addr_correct in EQ; try_simplify_someHyps.
    exploit memcpy_skip; eauto. congruence.
  + (* standard case *)
    destruct (rrules_filter RRULES); try congruence.
    autodestruct. intros _ _ MALIVE X. inv X. apply reorder_memcpy_correct.
    intro DEAD; apply MALIVE. apply fmcpy_alive_monotonic; auto.
Qed.
Global Opaque rewrite_memcpy.


Definition almost_best_align (sz: positive) (al ofs bal: Z) : Prop :=
      0 <= ofs <= bal - al
   /\ ofs + bal <= Zpos sz
   .

Definition args_almost_ok (chk: cpychunk) (bdst: Values.block) (odst: Z) (bsrc: Values.block) (osrc: Z) : Prop :=
      is_align (cpy_al chk)
   /\ (cpy_al chk | Zpos (cpy_sz chk))
   /\ (cpy_al chk | osrc)
   /\ (cpy_al chk | odst)
   /\ (cpy_mode chk = None -> noover (cpy_sz chk) bdst odst bsrc osrc)
   /\ if_Some (cpy_mode chk) (fun b => bsrc = bdst /\ if b then odst < osrc else osrc < odst)
   /\ if_Some (cpy_bal chk) (fun p => almost_best_align (cpy_sz chk) (cpy_al chk) (fst p) (snd p))
   .

Definition check_balp (chk: cpychunk) (tmc: memcpy_args list_sval) (balp: nat) (ofs: ptrofs): option nat :=
  match balp with
  | O => Some O
  | S O =>
     match cpy_bal (mcpy_chk tmc) with
     | Some (ofs', bal) =>
       ASSERT zeq bal (cpy_al chk) &&& (zeq ofs' ((Ptrofs.unsigned ofs) mod bal) ||| false) IN
       Some O
     | _ => None
     end
  | S n => Some n
  end.

Fixpoint check_mempcy_merge_loop (oseq: list (memcpy_args list_sval)) tmc (balp: nat) (ofs: ptrofs): bool :=
 match oseq with
 | nil => zeq (Ptrofs.unsigned ofs) (Zpos (cpy_sz (mcpy_chk tmc))) &&& match balp with O => true | _ => false end
 | omc::oseq' =>
         zle (Zpos (cpy_sz (mcpy_chk omc))) (Zpos (cpy_sz (mcpy_chk tmc)) - Ptrofs.unsigned ofs)
     &&& test_shift_addr (mcpy_da omc) (mcpy_da tmc) ofs
     &&& test_shift_addr (mcpy_sa omc) (mcpy_sa tmc) ofs
     &&& match check_balp (mcpy_chk omc) tmc balp ofs with
         | Some balp' => check_mempcy_merge_loop oseq' tmc balp' (Ptrofs.add ofs (Ptrofs.repr (Zpos (cpy_sz (mcpy_chk omc)))))
         | None => false
         end
 end.

Section MERGE_FWD.

Variable tmc: memcpy_args list_sval.

Hypothesis ctx: iblock_common_context.
Variable bdst bsrc: Values.block.
Variable odst osrc: ptrofs.
Hypothesis ARGSOK: args_almost_ok (mcpy_chk tmc) bdst (Ptrofs.unsigned odst) bsrc (Ptrofs.unsigned osrc).

Let bmal := (bmal_of (Mem.block_align (cm1 ctx)) bdst bsrc).
Let tchk := (mcpy_chk tmc).

Lemma check_balp_correct (omc: memcpy_args list_sval) balp ofs osrc' odst' m0 m
  (VALID: check_balp (mcpy_chk omc) tmc balp ofs = Some O)
  (ARG1 : memcpy_args_ok (mcpy_chk omc) bmal bdst (Ptrofs.unsigned odst') bsrc (Ptrofs.unsigned osrc'))
  (EQS : osrc' = Ptrofs.add osrc ofs)
  (EQD : odst' = Ptrofs.add odst ofs)
  (SM: ofs = Ptrofs.zero
       \/ exists sz, Zpos sz = Ptrofs.unsigned ofs /\
          memmove sz bdst (Ptrofs.unsigned odst) bsrc (Ptrofs.unsigned osrc) m0 m0 = Some m)
  (BALP: balp = O -> if_Some (cpy_bal tchk) (fun p => best_align (cpy_sz tchk) bmal (cpy_al tchk) (Ptrofs.unsigned odst) (Ptrofs.unsigned osrc) (fst p) (snd p)))
  :if_Some (cpy_bal tchk) (fun p => best_align (cpy_sz tchk) bmal (cpy_al tchk) (Ptrofs.unsigned odst) (Ptrofs.unsigned osrc) (fst p) (snd p)).
Proof.
  unfold tchk in *.
  revert VALID. unfold check_balp. autodestruct; eauto.
  repeat autodestruct; cbn.
  rename e into EQal. rename e0 into EQofs.
  intros _ _ _ BAL _ _ _. clear BALP. cbn in *.
  destruct ARGSOK as (_ & _ & _ & _ & _ & _ & ABA).
  rewrite BAL in ABA.
  destruct ABA as (? & ?).
  destruct ARG1 as (ALIGN & _ & BMAL & SRC & DST & ?); subst.
  do 3 try (split; auto).
  assert (ALPOS: cpy_al (mcpy_chk omc) <> 0). {
    lapply (is_align_pos (cpy_al (mcpy_chk omc))); auto with zarith.
  }
  destruct SM as [OFS | (sz & SZ & MOVE0)].
  + subst. rewrite !Ptrofs.add_zero, !Ptrofs.unsigned_zero, Zmod_0_l, !Z.add_0_r in *.
    auto.
  + specialize (memmove_max_size _ _ _ _ _ _ _ MOVE0).
    intros REP.
    exploit (@size_offset_representable sz osrc). { lia. }
    intros REP1.
    exploit (@size_offset_representable sz odst). { lia. }
    intros REP2.
    rewrite !SZ, !Ptrofs.repr_unsigned in *.
    rewrite REP1, REP2 in *.
    rewrite <- !Z.mod_divide in SRC, DST, BMAL; auto.
    rewrite <- !Z.mod_divide, !Zplus_mod_idemp_r; auto.
Qed.

Hypothesis TDST: eval_address ctx (mcpy_da tmc) = Some (bdst, odst).
Hypothesis TSRC: eval_address ctx (mcpy_sa tmc) = Some (bsrc, osrc).
Hypothesis REPchunk: Zpos (cpy_sz (mcpy_chk tmc)) <= Ptrofs.max_unsigned.
Hypothesis MODE: cpy_mode (mcpy_chk tmc) <> Some false.
Hypothesis TBMAL: (cpy_al (mcpy_chk tmc) | bmal).

Variable sm0: smem.
Variable m0: mem.
Hypothesis EVALsm0: eval_smem ctx sm0 = Some m0.

Lemma check_memcpy_merge_fwd_correct (oseq: list (memcpy_args list_sval)): forall ofs balp
  (VALID: check_mempcy_merge_loop oseq tmc balp ofs = true)
  sm
  (ALIVE : alive (eval_smem ctx (fmcpy_merge oseq sm)))
  (BALP: balp = O -> if_Some (cpy_bal tchk) (fun p => best_align (cpy_sz tchk) bmal (cpy_al tchk) (Ptrofs.unsigned odst) (Ptrofs.unsigned osrc) (fst p) (snd p)))
  (SM: (ofs = Ptrofs.zero /\ smem_equiv ctx sm0 sm)
       \/ exists sz, Zpos sz = Ptrofs.unsigned ofs /\
             memmove sz bdst (Ptrofs.unsigned odst) bsrc (Ptrofs.unsigned osrc) m0 m0 = eval_smem ctx sm)
  , smem_equiv ctx (fmcpy tmc sm0) (fmcpy_merge oseq sm).
Proof.
  induction oseq as [|omc oseq]; cbn; intros.
  + revert VALID. repeat autodestruct. intros BALPEQ _ _. rename e into EQ.
    destruct SM as [(? & _) | (sz & SZ & MOVE)].
    * (* absurd case *)
      subst. rewrite Ptrofs.unsigned_zero in EQ. lia.
    * (* final case *)
      rewrite <- SZ in EQ. injection EQ. clear EQ. intros; subst.
      erewrite eval_address_fmcpy; eauto. cbn.
      erewrite memcpy_ok_move, <- MOVE; eauto.
      unfold args_almost_ok, memcpy_args_ok in *.
      intuition auto.
  + (* recursive case *)
    revert VALID; repeat autodestruct. rename l into BND.
    intros CHECKBALP SUBS SUBD _ CHECK.
    apply (test_shift_addr_correct ctx) in SUBS, SUBD.
    specialize (fmcpy_merge_alive_back _ _ _ ALIVE).
    intro ALIVE1.
    feapply fmcpy_alive_eval_address.
    rename H3 into MCPY. symmetry in MCPY.
    destruct (eval_smem ctx (fmcpy omc sm)) as [m1|] eqn: Hm1; try congruence. clear ALIVE1.
    revert SUBS SUBD.
    unfold shift_address. try_simplify_someHyps.
    intros; destruct SUBS as (EQ1 & EQS). destruct SUBD as (EQ2 & EQD).
    rewrite EQ1, EQ2 in *.
    rewrite memcpy_Some_equiv in MCPY.
    destruct MCPY as (ARG1 & MOVE1).
    (* recursive call *) intros; eapply IHoseq; eauto.
    { (* BALP *)
       intros; eapply check_balp_correct; eauto.
       + subst; eauto.
       + destruct SM as [(OFS & EQm0) | (sz & SZ & MOVE0)]; eauto.
    }
    clear ALIVE IHoseq. right.
    generalize (Ptrofs.unsigned_range_2 ofs).
    intros R.
    assert (BNDomc: 0 <= Z.pos (cpy_sz (mcpy_chk omc)) <= Ptrofs.max_unsigned). { lia. }
    destruct SM as [(OFS & EQm0) | (sz & SZ & MOVE0)]. {
      (* first call *)
      subst. symmetry in EQm0; injection EQm0; clear EQm0; intros; subst.
      rewrite Hm1, !Ptrofs.add_zero_l, !Ptrofs.add_zero, !Ptrofs.unsigned_repr in *;
      subst; eauto.
    }
    (* next calls *)
    exploit (@size_offset_representable (cpy_sz (mcpy_chk omc)) ofs). { lia. }
    intros NXT; rewrite NXT.
    assert (X: 0 < Ptrofs.unsigned ofs + Z.pos (cpy_sz (mcpy_chk omc))) by lia.
    destruct (Ptrofs.unsigned ofs + Z.pos (cpy_sz (mcpy_chk omc))) as [|sz0|] eqn: SZ0; try lia.
    clear X NXT.
    eexists; split; eauto.
    assert (NXT: (sz0 = sz + (cpy_sz (mcpy_chk omc)))%positive) by lia.
    rewrite NXT, memmove_split_forward. 2 : {
      destruct ARGSOK as (? & ? & ? & ? & NOOV & MAYOV & _).
      destruct (cpy_mode (mcpy_chk tmc)) as [[]|]; cbn in *; auto with zarith.
      feapply NOOV. unfold noover; lia.
    }
    rewrite MOVE0.
    specialize (memmove_max_size _ _ _ _ _ _ _ MOVE0).
    intros REP.
    exploit (@size_offset_representable sz osrc). { lia. }
    intros REP1.
    exploit (@size_offset_representable sz odst). { lia. }
    intros REP2.
    rewrite !SZ, !Ptrofs.repr_unsigned in *.
    congruence.
Qed.

End MERGE_FWD.

checking the args_ok

Lemma addr_disjoint_noover ctx (tmc: memcpy_args list_sval) dst src:
   eval_address ctx (mcpy_da tmc) = Some dst ->
   eval_address ctx (mcpy_sa tmc) = Some src ->
   addr_disjoint ctx (mcpy_da tmc) (mcpy_sa tmc) ->
   noover (cpy_sz (mcpy_chk tmc)) (fst dst) (Ptrofs.unsigned (snd dst)) (fst src) (Ptrofs.unsigned (snd src)).
Proof.
  unfold addr_disjoint, eval_address, noover. intros; simplify_option. lia.
Qed.

Definition check_almost_bal chk balp :=
  match cpy_bal chk with
  | None => true
  | Some (ofs, bal) =>
        decide (almost_best_align (cpy_sz chk) (cpy_al chk) ofs bal)
    &&& match balp with
        | O => false
        | _ => true
        end
  end.

Local Opaque Decidable_witness Decidable_and.

Lemma check_almost_bal_correct chk balp
  (VALID: check_almost_bal chk balp = true)
  : if_Some (cpy_bal chk) (fun p => almost_best_align (cpy_sz chk) (cpy_al chk) (fst p) (snd p))
   /\ (balp = O -> cpy_bal chk = None).
Proof.
  revert VALID; unfold check_almost_bal; simplify_option.
  intros DEC; apply Decidable_sound in DEC.
  intuition congruence.
Qed.

Definition check_args_ok (oseq: list (memcpy_args list_sval)) (tmc: memcpy_args list_sval) (balp: nat): bool :=
  match oseq with
  | omc::_ =>
    let td := mcpy_da tmc in
    let ts := mcpy_sa tmc in
    let chk := mcpy_chk tmc in
    let al := cpy_al chk in
        Zdivide_dec al (cpy_al (mcpy_chk omc))
    &&& (zle 1 al
    &&& (Zdivide_dec al (Zpos (cpy_sz chk))
    &&& test_eq_addr (mcpy_da omc) td
    &&& test_eq_addr (mcpy_sa omc) ts))
    &&& check_almost_bal chk balp
    &&& match cpy_mode chk with
        | None => test_disjoint true true td ts ||| false
        | Some b as mode =>
           match test_cmp_addr td ts with
           | Some Lt => b
           | Some Gt => negb b
           | _ => option_eq bool_dec (cpy_mode (mcpy_chk omc)) mode ||| false
           end
        end
  | _ => false
  end.


Lemma check_args_ok_correct ctx oseq tmc balp
  (VALID: check_args_ok oseq tmc balp = true) sm
  (ALIVE : alive (eval_smem ctx (fmcpy_merge oseq sm))):
  exists dst src m0, eval_address ctx (mcpy_da tmc) = Some dst
              /\ eval_address ctx (mcpy_sa tmc) = Some src
              /\ eval_smem ctx sm = Some m0
              /\ args_almost_ok (mcpy_chk tmc) (fst dst) (Ptrofs.unsigned (snd dst)) (fst src) (Ptrofs.unsigned (snd src))
              /\ (balp = O -> (cpy_bal (mcpy_chk tmc)) = None)
              /\ (cpy_al (mcpy_chk tmc) | bmal_of (Mem.block_align (cm1 ctx)) (fst dst) (fst src)).
Proof.
  revert VALID; unfold check_args_ok. destruct oseq as [|omc]; try congruence. do 6 autodestruct.
  rename d into AL. rename l into ALl. rename d0 into SZ.
  intros BAL EQs EQd _ _ _ MODE; eapply test_eq_addr_correct in EQd, EQs.
  cbn in ALIVE. specialize (fmcpy_merge_alive_back _ _ _ ALIVE). clear ALIVE.
  intros ALIVE; feapply fmcpy_alive_eval_address.
  rewrite EQs, EQd in *.
  exploit check_almost_bal_correct; eauto.
  clear BAL; intros (BAL & BALP).
  do 6 (econstructor; eauto).
  rename H3 into MEMCPY.
  symmetry in MEMCPY.
  revert MEMCPY; destruct (eval_smem ctx (fmcpy omc sm)) as [m|] eqn: SM; try congruence. clear ALIVE.
  rewrite memcpy_Some_equiv.
  unfold memcpy_args_ok.
  intros ((ALIGN & ? & BMAL & SRC & DST & NOV & MAOV & BOK) & _ ).
  do 7 try (split; auto).
  + eapply is_align_divides; eauto.
  + etransitivity. 2: apply SRC. auto.
  + etransitivity. 2: apply DST. auto.
  + revert MODE. do 2 autodestruct.
    exploit addr_disjoint_noover; eauto.
  + revert MODE. simplify_option;
    intros; exploit test_cmp_addr_correct; eauto;
    rewrite ?Zcompare_Gt_Lt_antisym; intuition auto with zarith.
  + etransitivity. eapply AL. eauto.
Qed.

Definition check_memcpy_init_merge (oseq: list (memcpy_args list_sval)) (tmc: memcpy_args list_sval) (balp: nat): bool :=
      zle (Zpos (cpy_sz (mcpy_chk tmc))) Ptrofs.max_unsigned
  &&& check_args_ok oseq tmc balp
  &&& check_mempcy_merge_loop oseq tmc balp Ptrofs.zero
  .

Lemma check_memcpy_init_merge_fwd_correct ctx oseq tmc balp
  (VALID: check_memcpy_init_merge oseq tmc balp = true) sm
  (ALIVE : alive (eval_smem ctx (fmcpy_merge oseq sm)))
  (MODE: cpy_mode (mcpy_chk tmc) <> Some false):
  smem_equiv ctx (fmcpy tmc sm) (fmcpy_merge oseq sm).
Proof.
  revert VALID. unfold check_memcpy_init_merge.
  do 2 autodestruct. intros. exploit check_args_ok_correct; eauto.
  intros ((bdst & odst) & (bsrc & osrc) & ? & ? & ? & ? & ? & BAL & BMAL). cbn in *.
  eapply check_memcpy_merge_fwd_correct; eauto.
  intros BALP. rewrite BAL; cbn; auto.
Qed.

Definition check_memcpy_merge (oseq: list (memcpy_args list_sval)) (tmc: memcpy_args list_sval) balp: bool :=
  match cpy_mode (mcpy_chk tmc) with
  | None | Some true => check_memcpy_init_merge oseq tmc balp
  | Some false => false
  end
  .

Lemma check_memcpy_merge_correct ctx oseq tmc balp
  (VALID: check_memcpy_merge oseq tmc balp = true) sm
  (ALIVE : alive (eval_smem ctx (fmcpy_merge oseq sm))):
  smem_equiv ctx (fmcpy tmc sm) (fmcpy_merge oseq sm).
Proof.
  unfold check_memcpy_merge in VALID.
  destruct (cpy_mode (mcpy_chk tmc)) as [[]|] eqn: MODE; congruence || (eapply check_memcpy_init_merge_fwd_correct; congruence || eauto).
Qed.
Global Opaque check_memcpy_merge.
Generated by coq2html