Module Cells


Require Import
  Coqlib AST Values Maps ShareTree Globalenvs Csharpminorannot Memory Hash Integers.

Require Import
  Utf8 String ToString DebugLib DebugCminor FastArith
  AdomLib Util TreeAl AssocList MemChunkTree Sets.

Require Import AbMemSignatureCsharpminor.

Notation fname := ident (only parsing).

Set Implicit Arguments.
Unset Elimination Schemes.

Type of abstract blocks.
Inductive ablock :=
| ABlocal (f: fname) (l: ident)
| ABglobal (b: block)
.

Instance AblockToString {F V} (ge: Genv.t F V) : ToString ablock :=
  (λ b, match b with
       | ABlocal f l => "Local(" ++ PrintPos.print_pos f ++ ", " ++ string_of_ident l ++ ")"
       | ABglobal b => "Global(" ++ match Genv.invert_symbol ge b with Some s => string_of_ident s | None => "?" end ++ ")"
       end)%string.

Definition ablock_beq (x y: ablock) : bool :=
  match x, y with
  | ABlocal a b, ABlocal c d => match Pos.eqb a c with true => Pos.eqb b d | f => f end
  | ABglobal a, ABglobal b => Pos.eqb a b
  | _, _ => false
  end.

Lemma ablock_beq_correct :
  ∀ x y, ablock_beq x y = true <-> x = y.
Proof.
  intros [a b|a] [c d|c]; simpl;
  (try intuition discriminate);
  repeat
    (match goal with
     | |- appcontext[Pos.eqb ?a ?b] => generalize (Pos.eqb_spec a b); destruct (Pos.eqb a b)
     | |- appcontext[Z.eqb ?a ?b] => generalize (Z.eqb_spec a b); destruct (Z.eqb a b)
     end; simpl;
     let H := fresh in
     intros H; inversion H; clear H; subst);
  intuition congruence.
Qed.

Definition ablock_dec (x y: ablock) : { x = y } + { xy } :=
  eq_dec_of_beq ablock_beq ablock_beq_correct x y.
Instance AblockDec : EqDec ablock := ablock_dec.

Module Ablock : TYPE_EQ
with Definition s := ablock
with Definition t := (fname * ident + block)%type.

  Definition s := ablock.
  Definition t := (fname * ident + block)%type.
  Definition t_of_s (b: s) : t :=
    match b with
    | ABlocal f l => inl (f, l)
    | ABglobal b => inr b
    end.
  Definition s_of_t (x: t) : s :=
    match x with
    | inl (f, l) => ABlocal f l
    | inr b => ABglobal b
    end.
  Lemma s_of_t_of_s : forall x : s, s_of_t (t_of_s x) = x.
Proof.
intros [f l|b]; reflexivity. Qed.
  Lemma t_of_s_of_t: forall x : t, t_of_s (s_of_t x) = x.
Proof.
intros [(f,l)|b]; reflexivity. Qed.
  Definition eq: forall (x y: s), {x = y} + {x <> y} := ablock_dec.
End Ablock.

Module _MTFI : SHARETREE with Definition elt := (fname * ident)%type
  := ProdShareTree(PShareTree)(PShareTree).
Module _MTFIB : SHARETREE with Definition elt := (fname * ident + block)%type
  := SumShareTree(_MTFI)(PShareTree).
Module ABTree : SHARETREE with Definition elt := ablock := BijShareTree(Ablock)(_MTFIB).
Module ABTreeDom := WPFun ABTree.
Existing Instance ABTreeDom.toString.
Module BlockSet := Tree2Set ABTree.
Module BSO := SetOp BlockSet.

Definition get_stk (f: fname) (stk: list (temp_env * env)) : option (temp_env * env) :=
  nth (rev stk) f.

Lemma get_stk_in {f stk r} : get_stk f stk = Some rIn r stk.
Proof.
rewrite in_rev. apply nth_in. Qed.

Lemma get_stk_length' pre a stk :
  get_stk (plength stk) (pre ++ a :: stk) = Some a.
Proof.
  induction stk as [ | b stk ] using rev_ind;
  unfold get_stk in *; simpl in *; rewrite ! rev_app_distr, ? app_length.
  reflexivity.
  simpl. rewrite rev_app_distr in *.
  rewrite plength_snoc.
  now rewrite nth_succ.
Qed.

Lemma get_stk_length a stk :
  get_stk (plength stk) (a :: stk) = Some a.
Proof.
exact (get_stk_length' nil a stk). Qed.

Lemma get_stk_cons n a b :
  get_stk n (a :: b) = if Pos.eqb n (plength b) then Some a else get_stk n b.
Proof.
  case (Pos.eqb_spec _ _). intros ->. apply get_stk_length.
  revert n.
  induction b as [ | x b IH ] using rev_ind;
    unfold get_stk; try rewrite plength_nil; simpl; intros n H.
  destruct n; congruence.
  rewrite rev_app_distr.
  rewrite plength_snoc in H.
  simpl rev. simpl app.
  destruct n as [ n | n | ]; simpl; auto;
  apply IH. zify; Psatz.lia.
  rewrite (Pos.pred_double_spec).
  intros K; apply H. rewrite <- K. symmetry. apply Pos.succ_pred.
  discriminate.
Qed.

Lemma get_stk_lt n m a :
  get_stk n m = Some a
  (n < plength m)%positive.
Proof.
  revert n.
  induction m as [ | b m IH ] using rev_ind; unfold get_stk; simpl; intros n.
  intros; eq_some_inv.
  rewrite rev_app_distr, plength_snoc.
  destruct n as [ n | n | ]; [ | | Psatz.lia ];
  intros H; specialize (IH _ H).
  Psatz.lia.
  rewrite Pos.pred_double_spec in IH.
  clear -IH.
  zify. cut (2 * Zpos n - 1 < Zpos (plength m)). Psatz.lia.
  simpl. rewrite Pos.pred_double_spec, Pos.pred_sub. exact IH.
Qed.

Definition get_stk_dep n m :
  { r |
    get_stk n m = Some (snd (fst r)) ∧
    (rev m = rev (fst (fst r) ++ snd (fst r) :: snd r) ∧
     Pos.eqb n (plength (snd r)))%list
  } +
  { (plength m <=? nget_stk n m = None )%positive }.
Proof.
  unfold get_stk.
  rewrite <- (rev_plength m).
  generalize (rev m). clear m. intros m. revert n.
  induction m as [ | x m IH ]; intros n.
  right. split. apply Pos.leb_le, Pos.le_1_l. reflexivity.
  destruct n as [ n | n | ];
    [ specialize (IH (xO n)) | specialize (IH (Pos.pred_double n)) | ].
  destruct IH as [ (((pre & a) & post) & Ha & -> & Hk) | (H & K) ].
  left. simpl. exists ((pre, a), (post ++ x :: nil))%list. split.
  easy. split. simpl. rewrite ! rev_app_distr. simpl. now rewrite rev_app_distr.
  simpl. rewrite plength_snoc. simpl in *.
  apply Pos.eqb_eq in Hk. rewrite <- Hk. apply Pos.eqb_refl.
  right. split. apply Pos.leb_le in H. apply Pos.leb_le. rewrite plength_cons. Psatz.lia. exact K.
  destruct IH as [ (((pre & a) & post) & Ha & -> & Hk) | (H & K) ].
  left. simpl. exists ((pre, a), (post ++ x :: nil))%list. split.
  easy. split. simpl. rewrite ! rev_app_distr. simpl. now rewrite rev_app_distr.
  simpl. rewrite plength_snoc. simpl in *.
  apply Pos.eqb_eq in Hk. rewrite <- Hk, Pos.pred_double_spec, Pos.succ_pred.
  apply Pos.eqb_refl. discriminate.
  right. apply Pos.leb_le in H. rewrite Pos.pred_double_spec in *.
  split. apply Pos.leb_le. simpl. rewrite <- (Pos.succ_pred (xO n)). 2: discriminate.
  rewrite plength_cons. Psatz.lia. exact K.
  left. exists ((rev m, x), nil). split. reflexivity. simpl. now rewrite rev_app_distr, rev_involutive.
Qed.

Lemma get_stk_app {x n y} :
  get_stk n (y ++ x) = if (n <? plength x)%positive then get_stk n x else get_stk (Pos.succ n - plength x)%positive y.
Proof.
  revert n. induction x as [ | a x IH ] using rev_ind;
    intros n; simpl.
  rewrite (app_nil_r). rewrite (proj2 (Pos.ltb_nlt _ _)).
  now rewrite <- Ppred_minus, Pos.pred_succ. rewrite plength_nil. Psatz.lia.
  rewrite plength_snoc.
  unfold get_stk. rewrite ! rev_app_distr.
  destruct n as [ n | n | ];
    [ specialize (IH (xO n)) | specialize (IH (Pos.pred_double n)) | ].
  simpl. rewrite <- rev_app_distr.
  fold (get_stk (xO n) (y ++ x)). rewrite IH. clear IH.
  case (Pos.ltb_spec); case (Pos.ltb_spec);
  auto.
  Psatz.lia.
  Psatz.lia.
  intros H H0.
  unfold get_stk. f_equal.
  simpl. rewrite ! Pplus_one_succ_l.
  zify. rewrite ! Pos2Z.inj_sub; Psatz.lia.
  simpl. rewrite <- rev_app_distr.
  fold (get_stk (Pos.pred_double n) (y ++ x)). rewrite IH. clear IH.
  rewrite Pos.pred_double_spec, Ppred_minus, ! Pplus_one_succ_l.
  case (Pos.ltb_spec); case (Pos.ltb_spec);
  auto.
  zify. rewrite Pos2Z.inj_sub; Psatz.lia.
  zify. rewrite Pos2Z.inj_sub; Psatz.lia.
  intros H H0.
  unfold get_stk. f_equal.
  zify. repeat (rewrite ? Pos2Z.inj_sub, ? Pos2Z.inj_add; try Psatz.lia).
  case (Pos.ltb_spec). reflexivity.
  destruct x; Psatz.lia.
Qed.

Lemma get_stk_tail e n m a :
  get_stk n m = Some a
  get_stk n (e :: m) = Some a.
Proof.
  intros H.
  generalize (get_stk_lt _ _ H).
  rewrite get_stk_cons.
  case (Pos.eqb_spec). Psatz.lia.
  easy.
Qed.

Lemma get_stk_nil n : get_stk n nil = None.
Proof.
unfold get_stk. reflexivity. Qed.

Lemma in_get_stk x y :
  In x y → ∃ n, get_stk n y = Some x.
Proof.
  rewrite in_rev. unfold get_stk. generalize (rev y). clear y.
  intros y.
  induction y as [ | a y IH ]. intros ().
  intros [ -> | IN ].
  exists (xH). reflexivity.
  destruct (IH IN) as (n & Hn).
  exists (Pos.succ n). now rewrite nth_succ.
Qed.

Definition block_of_ablock (ge: genv) (stk: list (temp_env * env))
           (ab: ablock) : option block :=
  match ab with
  | ABlocal f l =>
    do (_, e) <- get_stk f stk;
    do (b, _) <- PTree.get l e;
    ret b
  | ABglobal b =>
    do s <- Genv.invert_symbol ge b;
    ret b
  end.

Definition size_ty_chunk (κ:typed_memory_chunk) := size_chunk (proj1_sig κ).

Inductive cell : Type :=
| AClocal (f: fname) (l: ident) (ofs: Z) (κ: typed_memory_chunk)
| ACtemp (f: fname) (r: ident)
| ACglobal (b: block) (ofs: Z) (κ: typed_memory_chunk)
.

Definition ablock_of_cell (c: cell) : ablock :=
  match c with
  | AClocal f l _ _ => ABlocal f l
  | ACglobal b _ _ => ABglobal b
  | ACtemp f r => ABglobal xH
  end.

Definition range : Type := (Z * typed_memory_chunk)%type.

Definition range_of_cell (c: cell) : range :=
  match c with
  | AClocal _ _ o κ
  | ACglobal _ o κ => (o, κ)
  | ACtemp _ _ => (0, exist _ Mint32 I)
  end.

Definition cell_from (b: ablock) (r: range) : cell :=
  match b with
  | ABlocal f l => AClocal f l (fst r) (snd r)
  | ABglobal b => ACglobal b (fst r) (snd r)
  end.

Lemma ablock_of_cell_from b r :
  ablock_of_cell (cell_from b r) = b.
Proof.
destruct b; reflexivity. Qed.

Definition cell_beq (x y: cell) : bool :=
  match x, y return _ with
  | AClocal f l o κ, AClocal f' l' o' κ' =>
    Pos.eqb f f' && Pos.eqb l l' &&
    Z.eqb o o' && chunk_beq κ κ'
  | ACtemp f r, ACtemp f' r' =>
    Pos.eqb f f' && Pos.eqb r r'
  | ACglobal b o κ, ACglobal b' o' κ' =>
    Pos.eqb b b' && Z.eqb o o' && chunk_beq κ κ'
  | _, _ => false
  end.

Lemma cell_beq_correct x y :
  cell_beq x yx = y.
Proof.
  unfold is_true.
  split.
- destruct x; simpl; destruct y; intros; eq_some_inv;
  try destruct κ as [[] []], κ0 as [[] []];
  InvBooleans; try discriminate;
  repeat rewrite Pos.eqb_eq in *;
  repeat rewrite Z.eqb_eq in *;
  repeat rewrite chunk_beq_correct in *;
  f_equal;
  try congruence.
- intros <-. destruct x; simpl;
  repeat rewrite (proj2 (Pos.eqb_eq _ _) eq_refl);
  repeat rewrite (proj2 (Z.eqb_eq _ _) eq_refl);
  repeat rewrite (proj2 (chunk_beq_correct _ _) eq_refl);
  reflexivity.
Qed.

Instance CellToString (ge: genv): ToString cell :=
  λ c,
  match c with
  | ACtemp f r => ("Temp(" ++ to_string f ++ ", " ++ string_of_ident r ++")")%string
  | AClocal _ _ o κ
  | ACglobal _ o κ =>
    ("[" ++ to_string (ToString := AblockToString ge) (ablock_of_cell c) ++
               (if Z_zerop o then "" else ", " ++ to_string o) ++
               "]%" ++ to_string (proj1_sig κ))%string
  end.

Definition read_cell (ge: genv) (m: concrete_state) (c: cell) : option val :=
  match c with
  | AClocal f l ofs κ =>
    do (_, e) <- get_stk f (fst m);
    do (b, sz) <- PTree.get l e;
    Mem.load (proj1_sig κ) (snd m) b ofs
  | ACtemp f r =>
    do (t, _) <- get_stk f (fst m);
    PTree.get r t
  | ACglobal b ofs κ =>
    do s <- Genv.invert_symbol ge b;
    Mem.load (proj1_sig κ) (snd m) b ofs
  end.

Definition extend {A} (f: Aoption val) : Aval :=
  λ a, match f a with Some v => v | None => Vundef end.
Arguments extend [A] f _ /.

Definition mem_as_fun ge (m: concrete_state) : cellval :=
  extend (read_cell ge m).
Arguments mem_as_fun ge m _ /.

Lemma block_of_ablock_None ge m ab :
  block_of_ablock ge (fst m) ab = None
  ∀ r, read_cell ge m (cell_from ab r) = None.
Proof.
  destruct ab as [ f x | b ]; simpl.
  - case (get_stk); simpl; auto. intros (tmp, e).
    case (e ! x); simpl; auto. intros (b, sz).
    intros; eq_some_inv.
  - case Genv.invert_symbol; simpl; auto.
    intros; eq_some_inv.
Qed.

Lemma block_of_ablock_Some ge m ab b :
  block_of_ablock ge (fst m) ab = Some b
  ∀ r, read_cell ge m (cell_from ab r) = Mem.load (proj1_sig (snd r)) (snd m) b (fst r).
Proof.
  destruct ab as [ f x | b' ]; simpl.
  - case (get_stk); simpl. intros (tmp, e).
    case (e ! x); simpl. intros (b', sz).
    intros; eq_some_inv; congruence.
    intros; eq_some_inv. intros; eq_some_inv.
  - case Genv.invert_symbol; simpl;
    intros; eq_some_inv.
    congruence.
Qed.

Section OVERLAP.

Definition ranges_disjoint (a b: range) : Prop :=
  let '(i,c) := a in
  let '(j,d) := b in
  i + size_ty_chunk c <= jj + size_ty_chunk d <= i.

Definition ranges_overlap (a b: range) : Prop :=
  let '(i,c) := a in
  let '(j,d) := b in
  j < i + size_ty_chunk ci < j + size_ty_chunk d.

Remark ranges_disjoint_overlap a b :
  ranges_disjoint a b
  ranges_overlap a b
  ∀ P : Prop, P.
Proof.
  unfold ranges_disjoint, ranges_overlap. destruct a, b. intuition.
Qed.

Lemma ranges_disjoint_dec a b :
  { ranges_disjoint a b } + { ranges_overlap a b }.
Proof.
  unfold ranges_overlap, ranges_disjoint.
  destruct a; destruct b.
  match goal with |- context[ ?a <= ?b \/ _ ] => destruct (Z_le_dec a b) end. intuition.
  match goal with |- context[ _ \/ ?a <= ?b ] => destruct (Z_le_dec a b) end; intuition.
Defined.
Global Opaque ranges_disjoint_dec.

Lemma ranges_disjoint_not_eq r r' :
  ranges_disjoint r r' → rr'.
Proof.
  destruct r as (i,κ), r' as (i', κ').
  simpl. intros H K. eq_some_inv. subst.
  destruct κ' as [[] []]; unfold size_ty_chunk in *; simpl in *; Psatz.lia.
Qed.

Definition is_temp (c: cell) : bool :=
  match c with
  | ACtemp _ _ => true
  | _ => false
  end.

Definition cells_disjoint (a b: cell) : Prop :=
  is_temp a || is_temp bab
  ablock_of_cell aablock_of_cell b
  ranges_disjoint (range_of_cell a) (range_of_cell b).

Definition cells_overlap (a b: cell) : Prop :=
  (is_temp a || is_temp b = falsea = b) ∧
  ablock_of_cell a = ablock_of_cell b
  ranges_overlap (range_of_cell a) (range_of_cell b).

Remark cells_disjoint_overlap a b :
  cells_disjoint a b
  cells_overlap a b
  ∀ P : Prop, P.
Proof.
  unfold cells_disjoint, cells_overlap.
  unfold is_true. rewrite orb_true_iff, orb_false_iff.
  intuition. congruence. congruence.
  eapply ranges_disjoint_overlap; eauto.
  eapply ranges_disjoint_overlap; eauto.
Qed.

Lemma cells_disjoint_not_eq c c' :
  cells_disjoint c c' → cc'.
Proof.
  unfold cells_disjoint, is_true. rewrite orb_true_iff.
  intros H <-. destruct H as [(_, H) | [ H | H ] ]; try exact (H eq_refl).
  exact (ranges_disjoint_not_eq H eq_refl).
Qed.

Definition cells_disjoint_dec a b :
  { cells_disjoint a b } + { cells_overlap a b }.
  refine (
      (if (is_temp a || is_temp b) && negb (cell_beq a b) as q return _ = q_
      then λ K, left (or_introl _)
      else
        λ K,
        match ablock_dec (ablock_of_cell a) (ablock_of_cell b) with
        | left EQ =>
          match ranges_disjoint_dec (range_of_cell a) (range_of_cell b) with
          | left D => left (or_intror (or_intror D))
          | right H => right (conj _ (conj EQ H))
          end
        | right NE => left (or_intror (or_introl NE))
        end) eq_refl).
Proof.
    rewrite andb_true_iff, negb_true_iff in K.
    destruct K as [Htmp NE]. split. exact Htmp. intros EQ.
    generalize (proj2 (cell_beq_correct a b) EQ). rewrite NE.
    unfold is_true; intros X; eq_some_inv.
    rewrite andb_false_iff in K.
    destruct K as [K|K]. left. exact K.
    right. rewrite negb_false_iff in K. exact (proj1 (cell_beq_correct _ _) K).
  Defined.

Program Definition memory_chunk_fold {A} (f: Atyped_memory_chunkA) (a: A) : A :=
  (f (f (f (f (f (f (f (f a Mint8signed) Mint8unsigned) Mint16signed) Mint16unsigned) Mint32) Mint64) Mfloat32) Mfloat64).

Definition overlap_aux (b: ablock) (ofs: Z) (κ': typed_memory_chunk) (n: N) (acc: list cell): list cell :=
  let base := ofs - size_ty_chunk κ' + 1 in
  N.peano_rect_, list cell)
               acc
               (λ n,
                let ofs' := base + Z.of_N n in
                cons (cell_from b (ofs', κ'))
                )
               n.

Lemma overlap_aux_correct b ofs κ' c:
  ∀ n acc,
    In c (overlap_aux b ofs κ' n acc)
       ↔
    In c acc
    ∃ ofs', c = cell_from b (ofs', κ') ∧ ofs' < ofs - size_ty_chunk κ' + Z.of_N n + 1 ∧ ofs < ofs' + size_ty_chunk κ'.
Proof.
  unfold overlap_aux.
  induction n as [|n IH] using N.peano_ind; intros acc.
  split. exact (@or_introl _ _).
  intros [H|H]. exact H. hsplit. subst. simpl. Psatz.lia.
  rewrite N.peano_rect_succ. split.
  intros [ <- | IN ].
  right. eexists. split. reflexivity. split. rewrite N2Z.inj_succ. Psatz.lia. Psatz.lia.
  destruct (proj1 (IH _) IN). left; easy. right. hsplit. subst. eexists. split. reflexivity. split.
  rewrite N2Z.inj_succ. Psatz.lia. Psatz.lia.
  intros [H|H]. right. exact (proj2 (IH _) (or_introl H)).
  hsplit. subst.
  rewrite N2Z.inj_succ in *.
  assert (ofs' < ofs - size_ty_chunk κ' + Z.of_N n + 1 ∨ ofs' = ofs - size_ty_chunk κ' + 1 + Z.of_N n) as K by Psatz.lia.
  destruct K.
  right. apply (proj2 (IH _)). vauto.
  left. repeat f_equal. easy.
Qed.

Definition overlap (c: cell) : list cell :=
  match c with
  | ACtemp _ _ => nil
  | AClocal _ _ ofs κ
  | ACglobal _ ofs κ =>
    let b := ablock_of_cell c in
    memory_chunk_fold
      (λ l κ',
       if eq_dec (proj1_sig κ) (proj1_sig κ')
       then
         overlap_aux b ofs κ (Z.to_N (size_ty_chunk κ - 1))
        (overlap_aux b (ofs + size_ty_chunk κ) κ (Z.to_N (size_ty_chunk κ - 1)) l)
       else overlap_aux b ofs κ' (Z.to_N (size_ty_chunk κ + size_ty_chunk κ' - 1)) l)
      nil
  end.

Lemma memory_chunk_fold_rec {A} (f: A -> typed_memory_chunk -> A) :
  ∀ (P:A -> Prop), (∀ x c, P x -> P (f x c)) ->
  ∀ x, P x -> P (memory_chunk_fold f x).
Proof.
  unfold memory_chunk_fold. intros.
  repeat apply H. auto.
Qed.

Lemma in_memory_chunk_fold {A} (f: list Atyped_memory_chunklist A) :
  (∀ x c l, In x lIn x (f l c)) →
  ∀ x c, (∀ l, In x (f l c)) →
         ∀ l, In x (memory_chunk_fold f l).
Proof.
  unfold memory_chunk_fold; intros H x c Hx l.
  destruct c as [[] []]; repeat first [apply Hx|apply H]; congruence.
Qed.

Lemma overlap_correct' : ∀ c c', cells_overlap c c' → cc' → In c' (overlap c).
Proof.
  unfold overlap, ablock_of_cell.
  intros [f l ofs κ|f r|b ofs κ] [f' l' ofs' κ'|f' r'|b' ofs' κ'];
  intros (Htmp & EQ & H);
  simpl in Htmp; unfold is_true in Htmp; eq_some_inv;
  simpl in EQ; inv EQ; intros NE;
  try (destruct Htmp as [ K | K ]; eq_some_inv; easy).
+ apply (in_memory_chunk_fold) with κ'.
  intros x q l H0. destruct (eq_dec (proj1_sig κ) (proj1_sig q)); repeat (apply overlap_aux_correct; left); easy.
  simpl in H.
  intros l. destruct (eq_dec (proj1_sig κ) (proj1_sig κ')).
  - assert (κ = κ') by (destruct κ as [[] []], κ' as [[] []]; simpl in *; congruence).
    subst κ'. apply overlap_aux_correct.
    assert (ofs' = ofsofs' < ofsofs' > ofs) as K by Psatz.lia.
    destruct K as [K | [K | K] ]. congruence.
    right. eexists. split. reflexivity. rewrite Z2N.id; Psatz.lia.
    left. apply overlap_aux_correct. right. eexists. split. reflexivity.
    rewrite Z2N.id; Psatz.lia.
  - apply overlap_aux_correct. right. eexists. split. reflexivity.
    simpl in H. rewrite Z2N.id; Psatz.lia.
+ (* exactly same script as above *)
  apply (in_memory_chunk_fold) with κ'.
  intros x q l H0. destruct (eq_dec (proj1_sig κ) (proj1_sig q)); repeat (apply overlap_aux_correct; left); easy.
  simpl in H.
  intros l. destruct (eq_dec (proj1_sig κ) (proj1_sig κ')).
  - assert (κ = κ') by (destruct κ as [[] []], κ' as [[] []]; simpl in *; congruence).
    subst κ'. apply overlap_aux_correct.
    assert (ofs' = ofsofs' < ofsofs' > ofs) as K by Psatz.lia.
    destruct K as [K | [K | K] ]. congruence.
    right. eexists. split. reflexivity. rewrite Z2N.id; Psatz.lia.
    left. apply overlap_aux_correct. right. eexists. split. reflexivity.
    rewrite Z2N.id; Psatz.lia.
  - apply overlap_aux_correct. right. eexists. split. reflexivity.
    simpl in H. rewrite Z2N.id; Psatz.lia.
Qed.

Lemma overlap_correct r r' : ¬ In r' (overlap r) → cells_disjoint r r' ∨ r = r'.
Proof.
  Hint Resolve overlap_correct'.
  intros H. destruct (cells_disjoint_dec r r'); auto.
  right. destruct (eq_dec_of_beq cell_beq cell_beq_correct r r'); auto.
  elim H. auto.
Qed.

Global Opaque overlap.

End OVERLAP.

Module Cell : TYPE_EQ
with Definition s := cell
with Definition t := (fname * ident * Z * typed_memory_chunk + fname * ident + block * Z * typed_memory_chunk)%type.

  Definition s := cell.
  Definition t := (fname * ident * Z * typed_memory_chunk + fname * ident + block * Z * typed_memory_chunk)%type.
  Definition t_of_s (b: s) : t :=
    match b with
    | AClocal f l o κ => inl (inl (f, l, o, κ))
    | ACtemp f r => inl (inr (f, r))
    | ACglobal b o κ => inr (b, o, κ)
    end.
  Definition s_of_t (x: t) : s :=
    match x with
    | inl (inl (f, l, o, κ)) => AClocal f l o κ
    | inl (inr (f, r)) => ACtemp f r
    | inr (b, o, κ) => ACglobal b o κ
    end.
  Lemma s_of_t_of_s : forall x : s, s_of_t (t_of_s x) = x.
Proof.
intros [f l|f r|b]; reflexivity. Qed.
  Lemma t_of_s_of_t: forall x : t, t_of_s (s_of_t x) = x.
Proof.
intros [[(((f,l),o), κ)|(f,r)]|((b,o),κ)]; reflexivity. Qed.
  Definition eq: forall (x y: s), {x = y} + {x <> y} :=
    eq_dec_of_beq cell_beq cell_beq_correct.
End Cell.

Module _MTFIZ : SHARETREE with Definition elt := (fname * ident * Z)%type
  := ProdShareTree(_MTFI)(ZShareTree).
Module _MTFIZC : SHARETREE with Definition elt := (fname * ident * Z * typed_memory_chunk)%type
  := ProdShareTree(_MTFIZ)(MemChunkTree).
Module _MTFIZCFI : SHARETREE with Definition elt := (fname * ident * Z * typed_memory_chunk + fname * ident)%type
  := SumShareTree(_MTFIZC)(_MTFI).
Module _MTBZ : SHARETREE with Definition elt := (block * Z)%type
  := ProdShareTree(PShareTree)(ZShareTree).
Module _MTBZC : SHARETREE with Definition elt := (block * Z * typed_memory_chunk)%type
  := ProdShareTree(_MTBZ)(MemChunkTree).
Module _MTFIZCFIBZC : SHARETREE with Definition elt := (fname * ident * Z * typed_memory_chunk + fname * ident + block * Z * typed_memory_chunk)%type
  := SumShareTree(_MTFIZCFI)(_MTBZC).

Module ACTree : SHARETREE with Definition elt := cell := BijShareTree(Cell)(_MTFIZCFIBZC).
Module CellSet : SET with Definition elt := cell := Tree2Set ACTree.
Module CSO := SetOp CellSet.

Instance ACellDec : EqDec cell := ACTree.elt_eq.

Definition set_product (bs: BlockSet.t) κ (offs: ZSet.t+⊤+⊥) : CellSet.t +⊤ :=
  match offs with
  | Bot => Just CellSet.empty
  | NotBot offs =>
    do offs <- offs;
    Just (BlockSet.fold
            (λ b cs, ZSet.foldofs cs, CellSet.add (cell_from b (ofs, κ)) cs) offs cs)
            bs
            CellSet.empty)
  end.

Lemma ztree_fold_union_In f acc x (is: ZSet.t) :
  ((∃i, In i (ZSet.elements is) ∧ x = f i) ∨ CellSet.mem x acc)
  ↔
  CellSet.mem x (ZSet.foldi cs, CellSet.add (f i) cs) is acc).
Proof.
  rewrite ZSet.fold_spec.
  generalize (ZSet.elements is). clear is.
  induction l.
  simpl. split. now intros [(i & ()&_)|H]. intuition.
  simpl.
  destruct IHl as [A B]. split.
  - intros [(? & [->|H] & ->)|H];
    apply CellSet.mem_add; eauto 6.
  - intros H; apply CellSet.mem_add in H; destruct H as [H|H].
    destruct (B H) as [(i & K & ->)|K]; eauto. eauto.
Qed.

Lemma set_product_correct :
  forall bs κ offs b i,
    BlockSet.mem b bs ->
    i ∈ γ offs ->
    match set_product bs κ offs with
    | All => True
    | Just res => CellSet.mem (cell_from b (Int.unsigned i, κ)) res
    end.
Proof.
  unfold set_product.
  intros bs κ [|[|offs]]. intuition. intros; exact I.
  simpl. intros b i.
  rewrite BlockSet.fold_spec.
  rewrite BlockSet.elements_spec.
  generalize (BlockSet.elements bs). clear bs.

  intros l H IN. apply ZSet.elements_spec in IN.
  induction l. inversion H.
  destruct H as [->|H].
  simpl. apply ztree_fold_union_In. left. exists (Int.unsigned i). intuition.
  simpl. apply ztree_fold_union_In. right. now apply IHl.
Qed.

Instance hash_cell : hashable cell := fun (h:Nfast) (c:cell) =>
  match c with
  | AClocal x y z t =>
    hash (hash (hash (hash (MIX h F0) x) y) (z:Zfast)) t
  | ACtemp x y =>
    hash (hash (MIX h F1) x) y
  | ACglobal x y z =>
    hash (hash (hash (MIX h F2) (Npos x:Nfast)) (y:Zfast)) z
  end.


Inductive cmp_blockset_t := Equal (b: ablock) | Disjoint | DontKnow | Contradiction.

Definition cmp_blockset (x y: BlockSet.t) : cmp_blockset_t :=
  match BSO.classify x, BSO.classify y with
  | BSO.Empty, _ | _, BSO.Empty => Contradiction
  | BSO.Singleton v, BSO.Singleton w => if eq_dec v w then Equal v else Disjoint
  | _, _ => if BlockSet.le (BlockSet.inter x y) BlockSet.empty then Disjoint else DontKnow
  end.

Lemma cmp_blockset_correct x y v w :
  BlockSet.mem v xBlockSet.mem w y
  match cmp_blockset x y with
  | Equal b => v = bw = b
  | Disjoint => vw
  | DontKnow => True
  | Contradiction => False
  end.
Proof.
  intros V W.
  unfold cmp_blockset.
  pose proof (BSO.classify_correct x) as X.
  pose proof (BSO.classify_correct y) as Y.
  destruct (BSO.classify x) as [|v'|]; try (now intuition eauto);
  destruct (BSO.classify y) as [|w'|]; try (now intuition eauto);
  repeat
  match goal with |- appcontext[ BlockSet.le ?a ?b ] =>
    generalize (proj2 (BlockSet.le_spec a b));
    destruct BlockSet.le; auto;
    intros HLE ->;
    refine (BlockSet.mem_empty _ (HLE eq_refl _ _));
    rewrite BlockSet.mem_inter; split; eauto
  end.
  assert (v = v'). intuition eauto.
  assert (w = w'). intuition eauto.
  subst v' w'. destruct (eq_dec v w); easy.
Qed.

Inductive min_size_t := MinSize | Size (z: Z) | MaxSize.
Definition size_of_option {A} (a: option (Z * A)) := match a with Some (a, _) => Size a | None => MinSize end.

Definition omin {A} (x: option (Z * A)) (y: min_size_t) : min_size_t :=
  match x, y with
  | None, _ => MinSize
  | _, MinSize => y
  | Some (x, _), Size y => Size (Z.min x y)
  | Some (x, _), MaxSize => Size x
  end.

Definition ozle (x y: min_size_t) : Prop :=
  match x, y with
  | MinSize, _ | _, MaxSize => True
  | MaxSize, _ | _, MinSize => False
  | Size x, Size y => Z.le x y
  end.

Remark ozle_refl : ∀ a, ozle a a.
Proof.
intros [|a|]; simpl; Psatz.lia. Qed.

Remark ozle_min_2 : ∀ A (a: option (Z * A)) b c,
  ozle (size_of_option a) cozle b c
  ozle (omin a b) c.
Proof.
intros A [(a, ?)|] [|b|] [|c|]; simpl; Psatz.lia. Qed.

Definition min_size A (sz: ABTree.t (Z * A)) := BlockSet.foldb, omin (ABTree.get b sz)).

Lemma min_size_min A (sz: ABTree.t (Z * A)) bs z:
  let m := min_size sz bs z in
  (∀ b, BlockSet.mem b bsozle m (size_of_option (ABTree.get b sz))) ∧ ozle m z.
Proof.
  unfold min_size.
  apply BSO.foldspec.
  2: refine_ H, conj_ K, False_ind _ (H _ K)) (ozle_refl _)).
  intros s s' z' acc x H [H0 H1] [IH Hacc].
  split. 2: apply ozle_min_2; auto.
  intros c Hc. apply ozle_min_2.
  destruct (H0 _ Hc); [ left | right ].
  subst; apply ozle_refl. eauto.
Qed.