Module ForgetNorm

Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import NormaliseSpec.
Require Import ExprEval.
Require Import Memory.
Require Import Psatz.
Require Import MemRel Align Tactics.
Require Import Permutation MemReserve BlockAppears ListUtils.

Opaque two_power_nat.
Opaque minus Z.mul.
Local Opaque Pos.of_nat.

Hint Resolve two_power_nat_pos.

Lemma npow_inj : forall x y,
   Z.of_nat (NPeano.pow x y) = (Z.of_nat x ^ Z.of_nat y)%Z.
Proof.
  induction y.
  * reflexivity.
  *
    rewrite NPeano.pow_succ_r.
    rewrite Nat2Z.inj_mul.
    rewrite IHy.
    rewrite Nat2Z.inj_succ.
    rewrite Z.pow_succ_r.
    reflexivity.
    apply Zle_0_nat.
    auto with zarith.
Qed.


Section NAT_RANGE'.

Nat ranges

We define ranges lo,lo+n.

  Fixpoint nat_range' lo n : list nat :=
    match n with
      O => lo :: nil
    | S m => lo :: nat_range' (S lo) m
    end.

  Lemma nat_range'_range:
    forall n lo b,
      (In b (nat_range' lo n) ->
       (lo <= b <= lo + n)%nat).
Proof.
    induction n; simpl; intros.
    des H. lia.
    des (eq_nat_dec lo b). lia.
    des H.
    apply IHn in i. lia.
  Qed.

  Lemma range_nat_range':
    forall n lo b,
      (lo <= b <= lo + n)%nat ->
      In b (nat_range' lo n).
Proof.
    induction n; simpl; intros.
    des H. lia.
    des (eq_nat_dec lo b). clear Heqs.
    right. apply IHn. lia.
  Qed.

  Lemma lnr_nat_range':
    forall n lo,
      list_norepet (nat_range' lo n).
Proof.
    induction n; simpl; intros.
    repeat constructor. destr.
    constructor. intro IN. apply nat_range'_range in IN. lia.
    eauto.
  Qed.

End NAT_RANGE'.



Section NAT_RANGE.

Nat ranges

We define ranges lo,hi.

  Definition nat_range lo hi : list nat :=
    if le_dec lo hi then nat_range' lo (hi-lo)%nat else nil.

  Lemma nat_range_rew: forall lo hi,
      nat_range lo hi =
      if le_dec lo hi
      then lo :: nat_range (S lo) hi
      else nil.
Proof.
    intros.
    unfold nat_range. destr. destr.
    des hi. lia.
    rewrite <- minus_Sn_m. simpl. f_equal. lia.
    replace hi with lo by lia. rewrite minus_diag. reflexivity.
  Qed.

Special case for n,n = n
  Lemma nat_range_same:
    forall n,
      nat_range n n = n :: nil.
Proof.
    intros.
    unfold nat_range. destr; try lia. rewrite minus_diag; simpl. auto.
  Qed.

  Lemma length_nat_range:
    forall m n,
      (n <= m)%nat ->
      length (nat_range n m)%nat = S (m - n)%nat.
Proof.
    unfold nat_range.
    intros m n.
    intros. destr.
    generalize (m - n)%nat.
    intro n0; clear. revert n; induction n0; simpl; intros; eauto.
  Qed.

  Lemma nat_range_range:
    forall lo hi b,
      (In b (nat_range lo hi) ->
       (lo <= b <= hi)%nat).
Proof.
    unfold nat_range. intros. destr_in H.
    apply nat_range'_range in H. lia.
  Qed.

  Lemma range_nat_range_range:
    forall lo hi b,
      (lo <= b <= hi)%nat ->
      In b (nat_range lo hi).
Proof.
    unfold nat_range. intros. destr.
    apply range_nat_range'. lia. lia.
  Qed.

  Lemma lnr_nat_range:
    forall lo hi,
      list_norepet (nat_range lo hi).
Proof.
    unfold nat_range. intros. destr.
    apply lnr_nat_range'. constructor.
  Qed.

End NAT_RANGE.


Section BOX_RANGE.

Box ranges

The "box range" of a block b of size z in a concrete memory cm is given by box_range cm (b,z) is the list of boxes that b spans over in cm.
  Definition box_range cm (bz : block * Z) :=
    let (b,sz) := bz in
    if zlt 0 sz
    then nat_range (Z.to_nat (Int.unsigned (cm b) / 8))
                   (Z.to_nat ((Int.unsigned (cm b) + sz - 1) / 8))
    else nil.

  Lemma lnr_box_range:
    forall cm a,
      list_norepet (box_range cm a).
Proof.
    unfold box_range. intros. des a.
    destr.
    apply lnr_nat_range.
    constructor.
  Qed.

This alternate version of box range uses the memory m to get the block size instead of having the size given directly as argument.
  Definition box_range' m cm b :=
    let sz := (Mem.size_block m b) in
    box_range cm (b,sz).

  Lemma box_range'_eq:
    forall cm m,
      map (box_range cm) (Mem.mk_block_list m) =
      map (box_range' m cm) (map fst (Mem.mk_block_list m)).
Proof.
    unfold box_range'.
    intros.
    unfold Mem.mk_block_list.
    generalize (mbla_in (Mem.size_block m) (pred (Pos.to_nat (Mem.nextblock m)))).
    generalize (mk_block_list_aux (Mem.size_block m) (pred (Pos.to_nat (Mem.nextblock m)))).
    induction l; simpl; intros; eauto.
    f_equal. des a. rewrite (H _ _ (or_introl eq_refl)). auto. auto.
  Qed.
  
End BOX_RANGE.



Definition nb_boxes_used_cm m (cm : block -> int) : nat :=
  length
    (remove_dbl eq_nat_dec (concat (map (box_range cm) (Mem.mk_block_list m)))).


Section MK_BLOCK_LIST.

  Lemma in_bl:
    forall m b1 z1
      (i: In (b1, z1) (Mem.mk_block_list m)),
      (Pos.to_nat b1 <= pred (Pos.to_nat (Mem.nextblock m)))%nat.
Proof.
    intro m.
    unfold Mem.mk_block_list.
    generalize (pred (Pos.to_nat (Mem.nextblock m))).
    intros.
    destruct (le_dec (Pos.to_nat b1) n); auto.
    apply (in_map fst) in i.
    contradict i.
    eapply Alloc.mbla_not_above. simpl. lia.
  Qed.

  Lemma lnr_mbl:
    forall m,
      list_norepet (map fst (Mem.mk_block_list m)).
Proof.
    unfold Mem.mk_block_list.
    intros.
    generalize (pred (Pos.to_nat (Mem.nextblock m))).
    Local Opaque Pos.of_nat.
    induction n; simpl; intros; eauto.
    constructor.
    constructor; auto.
    rewrite map_map. simpl.
    apply nin_list_ints. lia.
  Qed.

  Lemma in_bound_in_mk_block_list:
    forall m b z,
      In (b,z) (Mem.mk_block_list m) ->
      0 < z ->
      in_bound (Int.unsigned Int.zero) (Mem.bounds_of_block m b).
Proof.
    intros m b z INMBL POS.
    unfold Mem.mk_block_list in INMBL. eapply mbla_in in INMBL.
    subst. rewrite bounds_eq.
    red; simpl. rewrite Int.unsigned_zero; lia.
  Qed.

End MK_BLOCK_LIST.


Lemma box_span_mu:
  (Mem.box_span Int.max_unsigned - 2)%nat = Z.to_nat Mem.nb_boxes_max.
Proof.
  unfold Mem.box_span, Mem.nb_boxes_max.
  apply Nat2Z.inj. rewrite ! Z2Nat.id.
  rewrite Nat2Z.inj_sub.
  rewrite ! Z2Nat.id.
  simpl. f_equal.
  replace (Int.max_unsigned - 1) with (two_power_nat MA * two_power_nat (32 - MA) + (- 2)).
  rewrite two_p_div_rew.
  rewrite Z.mul_comm, Z_div_mult_full.
  replace (-2 / two_power_nat MA) with (-1). lia.
  -
    assert (Forall (fun x => -1 = -2 / two_power_nat x) (list_ints 13)).
    repeat constructor.
    eapply Forall_forall in H. eauto.
    apply list_ints_In. generalize MA_bound; lia.
  - generalize Mem.tpMA_pos. lia.
  - lia.
  - rewrite <- two_power_nat_split. reflexivity.
    generalize MA_bound. lia.
  - apply Z.add_nonneg_nonneg.
    apply Z.div_pos. vm_compute. destr.
    apply Z.gt_lt, Mem.tpMA_pos. lia.
  - change 2%nat with (1+1)%nat.
    rewrite Z2Nat.inj_add.
    apply NPeano.Nat.add_le_mono_r.
    transitivity (Z.to_nat ((Int.max_unsigned - 1) / two_power_nat 12)).
    rewrite two_power_nat_two_p.
    apply Nat2Z.inj_le. rewrite Z2Nat.id. vm_compute. destr.
    apply Z.div_pos. vm_compute; destr. apply Z.gt_lt, two_p_gt_ZERO. lia.
    apply Nat2Z.inj_le. rewrite ! Z2Nat.id. apply Z.div_le_compat_l.
    vm_compute; destr. generalize MA_bound.
    split. apply Z.gt_lt, Mem.tpMA_pos. rewrite ! two_power_nat_two_p. apply two_p_monotone; auto. lia.
    apply Z.div_pos. vm_compute; destr. apply Z.gt_lt, Mem.tpMA_pos.
    apply Z.div_pos. vm_compute; destr. apply Z.gt_lt, two_power_nat_pos.
    apply Z.div_pos. vm_compute; destr. apply Z.gt_lt, Mem.tpMA_pos. lia.
  - transitivity (two_power_nat 20 - 2). vm_compute; destr.
    generalize (two_p_monotone 20 (Z.of_nat (32 - MA))).
    rewrite ! two_power_nat_two_p. generalize MA_bound. lia.
Qed.

Section CANON_CM.

Lemma alloc_compat' : forall m l,
    Mem.is_block_list (Mem.mem_blocksize m) (pred (Pos.to_nat (Mem.nextblock m))) l ->
    { al : block -> nat |
      Mem.mk_cm l (Mem.nb_extra m) = Some al /\ Mem.compat_m m Mem.M31 (Mem.box_alloc_to_cm al) }.
Proof.
  intros.
  generalize (Mem.wfm_alloc m).
  intros. unfold Mem.mk_cm.
  des (Mem.make_box_allocation l).
  destr.
  - eexists; split; eauto.
    eapply Mem.box_alloc_to_cm_compat. 3: eauto.
    apply Z2Nat.inj_lt in l0. rewrite Nat2Z.id in l0. lia. lia. lia. auto.
  - eapply Mem.nb_boxes_used_thr in Heqp.
    subst.
    unfold Mem.nb_boxes_used_m in H0.
    erewrite Mem.nb_used_permut in H0. apply g in H0. easy.
    apply Permutation_sym, Mem.is_block_list_permut_mk_block_list; auto.
Qed.

Definition canon_cm (m:mem) : block -> int.
Proof.
  destruct (alloc_compat' m (Mem.mk_block_list m)).
  apply Mem.is_block_list_mk_block_list.
  destruct a.
  apply Mem.box_alloc_to_cm. apply x.
Defined.

Lemma canon_cm_mulMA:
  forall m b,
    exists k,
      Int.unsigned (canon_cm m b) = two_power_nat MA * k.
Proof.
  intros.
  unfold canon_cm. destr. des a.
  unfold Mem.box_alloc_to_cm.
  rewrite Int.unsigned_repr_eq.
  unfold Int.modulus.
  rewrite ! (two_power_nat_two_p).
  replace (Z.of_nat Int.wordsize) with (Z.of_nat MA + (Z.of_nat Int.wordsize - Z.of_nat MA)).
  rewrite two_p_is_exp.
  rewrite Zmult_mod_distr_l.
  generalize ((Z.of_nat (x b) + 1) mod two_p (Z.of_nat Int.wordsize - Z.of_nat MA)).
  intros. eauto. lia.
  change Int.wordsize with 32%nat. generalize (MA_bound); lia.
  change Int.wordsize with 32%nat. generalize (MA_bound); lia.
Qed.

Lemma canon_cm_mul8:
  forall m b,
    exists k,
      Int.unsigned (canon_cm m b) = 8 * k.
Proof.
  intros.
  change 8 with (two_power_nat 3).
  eapply div_large_div_small_two_p.
  apply canon_cm_mulMA.
  apply MA_bound.
Qed.

Lemma canon_cm_mul_mask:
  forall m b,
    exists k,
      Int.unsigned (canon_cm m b) = two_power_nat (Mem.mask m b) * k.
Proof.
  intros.
  eapply div_large_div_small_two_p.
  apply canon_cm_mulMA.
  unfold Mem.mask. destr.
  eapply Mem.alignment_ok in Heqo.
  destruct Heqo as (LEMA & AOS). lia. lia.
Qed.

The meaning of the following lemma is the following: given an address x aligned on m bits, and a size s compatible with the m-alignment and no larger than 8 bytes, all the range x,x+s-1 fits inside the same 8-byte box.

Lemma add_small_div_Z:
  forall k s m,
    0 <= k ->
    (m <= MA)%nat ->
    (alignment_of_size s <= m)%nat ->
    0 < s <= 8 ->
    two_power_nat m * k / 8 = (two_power_nat m * k + s - 1) / 8.
Proof.
  intros k s m POS LEMA AOS SMALL.
  destruct (le_dec 3 m).
  -
    rewrite ! two_power_nat_two_p.
    rewrite (two_p_split (Z.of_nat m) 3) by lia.
    rewrite <- Z.mul_assoc.
    generalize (two_p (Z.of_nat m - 3) * k). clear k POS. intro k.
    change (two_p 3) with 8.
    rewrite (Z.mul_comm 8). rewrite Z_div_mult_full by lia.
    replace (k * 8 + s - 1) with (k * 8 + (s - 1)) by lia.
    rewrite Z_div_plus_full_l by lia.
    rewrite Z.div_small; lia.
  -
    apply NPeano.Nat.nle_gt in n.
    destruct (div_spec k (two_p (Z.of_nat (3 - m)))) as (q & r & EQD & LT).
    rewrite <- two_power_nat_two_p; apply two_power_nat_pos.
    assert (REW: two_power_nat m * k = 8 * q + two_power_nat m * r).
    {
      rewrite EQD.
      rewrite (Z.mul_comm q).
      rewrite Z.mul_add_distr_l.
      rewrite (Z.mul_assoc).
      rewrite two_power_nat_two_p, <- two_p_is_exp by lia.
      replace (Z.of_nat m + Z.of_nat (3 - m)) with 3 by lia.
      change (two_p 3) with 8. reflexivity.
    }
    rewrite REW. clear REW.
    rewrite (Z.mul_comm 8).
    replace (q * 8 + two_power_nat m * r + s - 1)
      with (q * 8 + ((two_power_nat m * r + s) - 1)) by lia.
    rewrite ! Z_div_plus_full_l by lia.
    f_equal.
    generalize (aos_spec _ _ (proj2 SMALL) AOS). intro LE.
    generalize (two_power_nat_pos m); intro TPPOS.
    rewrite two_power_nat_two_p in *.
    change 8 with (two_p 3).
    rewrite (two_p_split 3 (Z.of_nat m)) by lia.
    rewrite Nat2Z.inj_sub in LT by lia.
    symmetry; rewrite ! Z.div_small; nia.
Qed.


Lemma int_and_two_p_m1_mul:
  forall i n,
    (n <= MA)%nat ->
    Int.and i (Int.not (Int.repr (two_power_nat n - 1))) = i ->
    exists k,
      i = Int.mul (Int.repr (two_power_nat n)) k.
Proof.
  intros; eapply int_and_two_p_m1_mul'; eauto.
  transitivity 12.
  generalize (MA_bound). lia. vm_compute; congruence.
Qed.

Lemma int_and_two_p_m1_mul_Z:
  forall i n,
    (n <= MA)%nat ->
    Int.and i (Int.not (Int.repr (two_power_nat n - 1))) = i ->
    exists k,
      Int.unsigned i = (two_power_nat n) * k.
Proof.
  intros.
  eapply int_and_two_p_m1_mul_Z'; eauto.
  generalize (MA_bound); lia.
Qed.

Lemma int_and_two_p_m1_mul_Z_inv:
  forall i n k,
    (n <= MA)%nat ->
    Int.unsigned i = (two_power_nat n) * k ->
    Int.and i (Int.not (Int.repr (two_power_nat n - 1))) = i.
Proof.
  intros i n k LEMA EQ.
  unfold Int.and.
  rewrite EQ.
  apply Int.same_bits_eq.
  intros.
  rewrite Int.testbit_repr; auto.
  rewrite Z.land_spec.
  rewrite <- (Int.testbit_repr (Int.unsigned _)); auto.
  rewrite Int.repr_unsigned.
  rewrite Int.bits_not; auto.
  rewrite Int.testbit_repr; auto.
  rewrite <- (Int.repr_unsigned i).
  rewrite Int.testbit_repr; auto. rewrite EQ.
  destruct (Z.testbit (two_power_nat n * k) i0) eqn:TB. 2: reflexivity.
  rewrite two_power_nat_two_p. rewrite Int.Ztestbit_two_p_m1 by lia.
  simpl. destr.
  rewrite Z.mul_comm in TB.
  replace (two_power_nat n) with (2 ^ Z.of_nat n) in TB.
  rewrite Z.mul_pow2_bits_low in TB; auto.
  rewrite two_power_nat_two_p.
  rewrite two_p_correct. auto.
Qed.


Lemma add_small_div:
  forall x s m,
    Int.and x (Int.not (Int.repr (two_power_nat m - 1))) = x ->
    (m <= MA)%nat ->
    (alignment_of_size s <= m)%nat ->
    0 < s <= 8 ->
    Int.unsigned x / 8 = (Int.unsigned x + s - 1) / 8.
Proof.
  intros x s m ALIGN LEMA AOS SMALL.
  destruct (int_and_two_p_m1_mul_Z _ _ LEMA ALIGN) as (k & EQ).
  rewrite EQ.
  eapply add_small_div_Z; eauto.
  eapply Z.mul_nonneg_cancel_l. 2: setoid_rewrite <- EQ.
  apply Zgt_lt, two_power_nat_pos.
  apply Int.unsigned_range.
Qed.

Lemma canon_cm_box_range:
  forall cm m b z,
    Mem.compat_m m Mem.M32 cm ->
    0 < z -> z = Mem.size_block m b ->
    length (box_range cm (b,z)) = length (box_range (canon_cm m) (b,z)).
Proof.
  intros.
  unfold box_range.
  destr. subst.
  generalize (alignment _ _ _ _ H b).
  intros ALIGN.
  assert (LEMA: (Mem.mask m b <= MA /\ alignment_of_size (Mem.size_block m b) <= Mem.mask m b)%nat).
  {
    unfold Mem.mask.
    destr.
    - apply Mem.alignment_ok in Heqo.
      unfold Mem.size_block. auto.
    - split. lia.
      apply Mem.bounds_mask_consistency in Heqo.
      unfold Mem.size_block, get_size in H0. rewrite Heqo in H0. lia.
  }
  destruct LEMA as (LEMA & AOS).
  assert (MULCM: exists k, Int.unsigned (cm b) = two_power_nat (Mem.mask m b) * k).
  {
    edestruct int_and_two_p_m1_mul_Z as (o & EQo); eauto.
  }
  destruct (canon_cm_mul_mask m b) as [k EQ].
  destruct (zle (Mem.size_block m b) 8).
  - pose proof (fun x pf => add_small_div x (Mem.size_block m b) (Mem.mask m b) pf LEMA AOS
                                       (conj H0 l0)
               ) as ASD.
    rewrite (ASD (cm b)).
    rewrite nat_range_same. simpl.
    rewrite (ASD (canon_cm m b)).
    rewrite nat_range_same. simpl. auto.
    +
      eapply int_and_two_p_m1_mul_Z_inv; eauto.
    +
      apply ALIGN.
  - assert (LE: (3 <= Mem.mask m b)%nat).
    {
      unfold alignment_of_size in AOS.
      repeat destr_in AOS; lia.
    }
    rewrite <- ! Z.add_sub_assoc.
    destruct MULCM.
    eapply two_p_div in H1; eauto.
    eapply two_p_div in EQ; eauto.
    erewrite ! div_mul_add; eauto.
    rewrite ! Z2Nat.inj_add; try apply Z.div_pos; try lia; try apply Int.unsigned_range.
    rewrite ! length_nat_range by lia. lia.
Qed.

Lemma canon_cm_box_range':
  forall cm m b z,
    Mem.compat_m m Mem.M32 cm ->
    z = Mem.size_block m b ->
    length (box_range cm (b,z)) = length (box_range (canon_cm m) (b,z)).
Proof.
  intros.
  destruct (zlt 0 z).
  eapply canon_cm_box_range; eauto.
  unfold box_range. destr.
Qed.

Lemma box_over_approx:
  forall z (l0 : 0 < z),
    (z - 1) / two_power_nat 3 < two_power_nat (MA - 3) * Z.of_nat (Mem.box_span z).
Proof.
  intros.
  unfold Mem.box_span. rewrite Z2Nat.id.
  2: apply Z.add_nonneg_nonneg; try lia. 2: generalize (two_power_nat_pos MA); intros; apply Z.div_pos; lia.
  rewrite (two_power_nat_split MA 3) by apply MA_bound.
  rewrite <- Zdiv_Zdiv; auto.
  rewrite Z.mul_add_distr_l.
  rewrite Z.mul_1_r.
  rewrite Z.mul_comm.
  assert (MOD: forall a b, b > 0 -> a - a mod b = (a / b) * b).
  {
    intros. rewrite Zmod_eq_full. lia. lia.
  }
  rewrite <- MOD; auto.
  assert (LTadd: forall a b c, b < c -> a < a - b + c) by (intros; lia).
  apply LTadd.
  apply Z_mod_lt; auto.
Qed.

Lemma rng_contrad:
  forall z b b0 y
    (l : 0 < z)
    (LEY1 : (Z.to_nat (two_power_nat (MA - 3) * (Z.of_nat b + 1)) <= y)%nat)
    (YLE2 : (y <= Z.to_nat (two_power_nat (MA - 3) * (Z.of_nat b0 + 1) + (z - 1) / two_power_nat 3))%nat)
    (l2 : (b0 + Mem.box_span z <= b)%nat),
    False.
Proof.
  intros.
  generalize (two_power_nat_pos (MA-3)). intro POS.
  contradict l2. apply lt_not_le. apply Nat2Z.inj_lt.
  apply Z.add_lt_mono_r with (p:=1).
  rewrite Z.mul_lt_mono_pos_l with (p:= (two_power_nat (MA-3))) by lia.
  eapply Z.le_lt_trans.
  apply Nat2Z.inj_le in LEY1.
  rewrite Z2Nat.id in LEY1 by nia. apply LEY1.
  eapply Z.le_lt_trans.
  apply Nat2Z.inj_le in YLE2.
  rewrite Z2Nat.id in YLE2. apply YLE2.
  generalize (Z.div_pos (z - 1) (two_power_nat 3)) (two_power_nat_pos 3). nia.
  generalize (box_over_approx _ l); lia.
Qed.

Lemma box_alloc_rew:
  forall (thr : nat) (m : Mem.mem') (ba : block -> nat),
    (thr < Z.to_nat Mem.nb_boxes_max)%nat ->
    Mem.make_box_allocation (Mem.mk_block_list m) = (thr, ba) ->
    forall (b : block) (o : int),
      in_bound (Int.unsigned o) (Mem.bounds_of_block m b) ->
      Int.unsigned (Mem.box_alloc_to_cm ba b) = two_power_nat MA * (Z.of_nat (ba b) + 1).
Proof.
  intros; unfold Mem.box_alloc_to_cm. rewrite Int.unsigned_repr.
  2: eapply Mem.box_alloc_unsigned_range; eauto.
  auto.
  apply Mem.is_block_list_mk_block_list.
Qed.

Lemma lnr_box_alloc_to_cm:
  forall m n x
    (LT : Z.of_nat (n + Mem.nb_extra m) < Mem.nb_boxes_max)
    (MBO : Mem.make_box_allocation (Mem.mk_block_list m) = (n, x)),
   forall l : list (block * Z),
   (forall x0 : block * Z, In x0 l -> In x0 (Mem.mk_block_list m)) ->
   list_norepet (map fst l) -> list_norepet (concat (map (box_range (Mem.box_alloc_to_cm x)) l)).
Proof.
  induction l; simpl; intros INIMPL LNR; eauto. constructor. inv LNR.
  trim IHl; auto.
  trim IHl; auto.
  apply list_norepet_append; auto.
  - unfold box_range. destr. destr. apply lnr_nat_range. constructor.
  - rename H1 into NIN. rename H2 into LNR.
    red. intros x0 y INBR INCONCAT.
    rewrite in_concat in INCONCAT. destruct INCONCAT as (l' & INMAP & INB).
    generalize (proj1 (in_map_iff _ _ _) INMAP).
    intros ((b,z)&BR & IN). subst.
    assert (LTa: 0 < snd a) by (revert INBR; unfold box_range; repeat destr).
    assert (LTz: 0 < z) by (revert INB; unfold box_range; repeat destr).
    clear INMAP.
    revert INBR; unfold box_range. des a. destr.
    intros INB0; apply nat_range_range in INB0.
    destr_in INB.
    apply nat_range_range in INB.
    exploit Mem.make_box_allocation_disjoint. 2: eauto. eapply mbla_norepet.
    apply INIMPL. left. apply surjective_pairing.
    apply INIMPL. right; eauto.
    intro; subst. rewrite in_map_iff in NIN. apply NIN. exists (b0, z). simpl; auto.
    simpl; lia.
    lia.
    intros OR.
    revert INB0 INB.
    eapply N2Z_add_lt_lt_Z2N in LT; eauto.
    erewrite ! box_alloc_rew; eauto.
    rewrite <- ! Z.add_sub_assoc.
    change 8 with (two_power_nat 3).
    generalize (MA_bound). intros MB.
    rewrite ! two_p_div_rew by lia.
    rewrite ! two_p_div_rew' by lia.
    intros. intro; subst.
    simpl in *.
    destruct OR as [OR|OR]; revert OR; eapply rng_contrad; eauto; lia.
    eapply in_bound_in_mk_block_list; eauto.
    eapply in_bound_in_mk_block_list; eauto.
Qed.

Lemma lnr_canon:
  forall m,
    list_norepet (concat (map (box_range (canon_cm m)) (Mem.mk_block_list m))).
Proof.
  intros.
  unfold canon_cm.
  destr. des a. clear Heqs.
  revert e. unfold Mem.mk_cm.
  destr. destr. intro A; inv A.
  eapply lnr_box_alloc_to_cm; eauto.
  eapply mbla_norepet.
Qed.

Lemma canon_cm_more_boxes:
  forall cm m,
    Mem.compat_m m Mem.M32 cm ->
    (nb_boxes_used_cm m cm <= nb_boxes_used_cm m (canon_cm m))%nat.
Proof.
  unfold nb_boxes_used_cm.
  intros.
  rewrite (lnr_remove _ (lnr_canon _)).
  etransitivity. eapply length_remove.
  rewrite ! length_concat.
  apply eq_le.
  f_equal.
  rewrite ! map_map. simpl.
  apply list_map_exten.
  intros.
  des x.
  symmetry; eapply canon_cm_box_range'; eauto.
  unfold Mem.mk_block_list in H0. eapply mbla_in in H0. auto.
Qed.

End CANON_CM.

Lemma length_box_range_canon_cm:
  forall m b z, 0 < z ->
    length (box_range (canon_cm m) (b,z)) = (S (Z.to_nat ((z - 1)/ 8))).
Proof.
  intros m b z LT.
  unfold box_range.
  destr.
  destruct (canon_cm_mul8 m b). rewrite H.
  rewrite (Z.mul_comm 8). rewrite Z_div_mult_full by lia.
  replace (x * 8 + z - 1) with (x * 8 + (z - 1)) by lia.
  rewrite Z_div_plus_full_l by lia. rewrite Z2Nat.inj_add.
  2: eapply Z.mul_le_mono_pos_l with 8. 2: lia. 2: rewrite <- H. 2: change (8*0) with 0.
  2: apply Int.unsigned_range.
  2: apply Z_div_pos; lia.
  rewrite ! length_nat_range by lia.
  lia.
Qed.

Definition boxes cm l :=
  map (box_range cm) l.

Definition num_boxes {A} (bl: list (list A)) := length (concat bl).

Definition box_span m cm x :=
  length (box_range' m cm x).

Lemma nb_boxes_used_cm_nb_boxes_used_m:
  forall m,
    (nb_boxes_used_cm m (canon_cm m) <= Mem.nb_boxes_used_m m * NPeano.pow 2 (MA-3))%nat.
Proof.
  intros.
  unfold Mem.nb_boxes_used_m, nb_boxes_used_cm.
  intros. rewrite ! (lnr_remove _ (lnr_canon _)).
  rewrite length_concat.
  transitivity (Mem.nb_boxes_used (Mem.mk_block_list m) * NPeano.pow 2 (MA - 3))%nat.
  - generalize (Mem.mk_block_list m).
    induction l; simpl; intros. lia. destruct a as [b z].
    destruct (zlt 0 z).
    + rewrite Mem.nb_boxes_used_cons.
      rewrite length_box_range_canon_cm; auto.
      cut (S (Z.to_nat ((z-1)/8)) <= Mem.box_span z * NPeano.pow 2 (MA - 3))%nat. lia.
      unfold Mem.box_span.
      rewrite Z2Nat.inj_add; try apply Z.div_pos; auto; try lia.
      rewrite (two_power_nat_split MA 3). 2: apply MA_bound.
      2: apply Z.gt_lt, two_power_nat_pos.
      rewrite <- Zdiv_Zdiv; auto.
      change (two_power_nat 3) with 8.
      cut (0 <= (z-1)/8).
      generalize ((z-1)/8). simpl; intros.
      apply Nat2Z.inj_le.
      rewrite Nat2Z.inj_mul.
      replace (Z.of_nat (Z.to_nat (z0 / two_power_nat (MA - 3)) + Pos.to_nat 1))
        with ((z0 / two_power_nat (MA - 3)) + 1).
      transitivity ((z0 /two_power_nat (MA - 3) * two_power_nat (MA - 3)) + two_power_nat (MA - 3)).
      assert (MOD: forall a b, b > 0 -> a - a mod b = (a / b) * b).
      {
        intros. rewrite Zmod_eq_full. lia. lia.
      }
      rewrite <- (MOD z0 (two_power_nat (MA - 3)) (two_power_nat_pos _)).
      rewrite Nat2Z.inj_succ by lia. rewrite Z2Nat.id by lia.
      cut (z0 mod two_power_nat (MA - 3) < two_power_nat (MA - 3) ). lia.
      apply Z_mod_lt.
      apply two_power_nat_pos.
      rewrite Z.mul_add_distr_r.
      rewrite (npow_inj 2 (MA-3)).
      simpl. rewrite <- two_p_correct.
      rewrite <- two_power_nat_two_p.
      lia.
      rewrite Nat2Z.inj_add. simpl. rewrite Z2Nat.id. lia.
      apply Z.div_pos. lia.
      apply Z.gt_lt, two_power_nat_pos.
      apply Z.div_pos. lia. lia.
    + unfold box_range at 1. destr.
      rewrite Mem.nb_boxes_used_cons.
      replace (Mem.box_span z) with O. lia.
      unfold Mem.box_span.
      cut ((z - 1)/ two_power_nat MA + 1 <= 0). unfold Z.to_nat. destr. lia.
      cut ((z - 1)/ two_power_nat MA < 0). lia.
      apply BigNumPrelude.Zdiv_neg. lia. apply Z.gt_lt, two_power_nat_pos.
  - apply NPeano.Nat.mul_le_mono_nonneg_r. lia.
    apply NPeano.Nat.le_add_r.
Qed.


Definition has_free_boxes m cm N :=
  (nb_boxes_used_cm m cm + N < Z.to_nat Mem.nb_boxes_max * NPeano.pow 2 (MA-3))%nat.

Definition nb_boxes8_max := (Z.to_nat Mem.nb_boxes_max * NPeano.pow 2 (MA - 3))%nat.

Section GET_FREE_BOXES.

  Definition get_free_boxes m cm :=
    fold_left
      (fun (acc: list nat) b =>
         filter (fun x => negb (in_dec eq_nat_dec x (box_range' m cm b))) acc)
      (map fst (Mem.mk_block_list m))
      (list_ints nb_boxes8_max).

  
  Lemma in_gfb:
    forall x m cm ,
      In x (get_free_boxes m cm) ->
      In x (list_ints nb_boxes8_max) /\
      Forall (fun y => negb (in_dec eq_nat_dec x (box_range' m cm y)) = true) (map fst (Mem.mk_block_list m)).
Proof.
    intros. unfold get_free_boxes in H. apply in_fold_left_filter in H. auto.
  Qed.


  Lemma align_two_power_nat:
    forall m n,
      (1 <= m)%nat ->
      (m <= n)%nat ->
      align (two_power_nat n - 1) (two_power_nat m) = two_power_nat n.
Proof.
    unfold align.
    intros.
    replace (two_power_nat n - 1 + two_power_nat m - 1)
    with (two_power_nat n * 1 + (two_power_nat m - 2)) by lia.
    rewrite two_p_div_rew; auto.
    rewrite Z.mul_add_distr_r.
    rewrite two_p_div_rew'; auto.
    rewrite Z.mul_1_r.
    rewrite Z.mul_comm.
    rewrite <- two_power_nat_split; auto.
    rewrite Z.div_small. lia.
    split; [|lia].
    change 2 with (two_p 1).
    rewrite two_power_nat_two_p.
    cut (two_p 1 <= two_p (Z.of_nat m)).
    lia.
    apply two_p_monotone. lia.
  Qed.

  Lemma align_max_unsigned:
    align (Int.max_unsigned) (two_power_nat MA) = Int.max_unsigned + 1.
Proof.
    change Int.max_unsigned with (two_p Int.zwordsize - 1).
    unfold Int.zwordsize.
    generalize MA_bound. intro.
    rewrite <- two_power_nat_two_p.
    rewrite align_two_power_nat. lia.
    lia. change Int.wordsize with 32%nat. lia.
  Qed.
  

  Lemma valid_box_repr:
    forall x (i: (0 < x <= nb_boxes8_max)%nat)
      o (RNGO: 0 <= o < 8),
      0 < 8 * Z.of_nat x + o < Int.max_unsigned.
Proof.
    split. lia. eapply Z.le_lt_trans with (m := 8 * Z.of_nat nb_boxes8_max + o). lia.
    clear - RNGO. unfold nb_boxes8_max.
    rewrite <- box_span_mu.
    rewrite Nat2Z.inj_mul.
    rewrite Z.mul_comm.
    rewrite <- Z.mul_assoc.
    rewrite npow_inj.
    rewrite <- two_p_correct.
    change 8 with (two_p 3).
    rewrite <- two_p_is_exp by lia.
    replace (Z.of_nat (MA - 3) + 3) with (Z.of_nat MA) by (generalize MA_bound; lia).
    rewrite Z.mul_comm. rewrite <- two_power_nat_two_p.
    rewrite Nat2Z.inj_sub.
    rewrite Zmult_minus_distr_l.
    rewrite Mem.box_span_align.
    rewrite align_max_unsigned.
    cut (1 + o < 2 * two_power_nat MA). lia.
    eapply Z.lt_le_trans with (m := 2 * two_power_nat 3).
    change (1 + o < 16); lia.
    generalize (two_power_nat_monotone _ _ (proj1 MA_bound)). lia.
    vm_compute; congruence.
    unfold Mem.box_span.
    apply Nat2Z.inj_le. rewrite Z2Nat.id.
    etransitivity. 2: apply Z.add_le_mono_r.
    2: apply Zdiv_le_compat_l.
    3: split. 3: apply Z.gt_lt, two_power_nat_pos. 3: rewrite two_power_nat_two_p; apply two_p_monotone_strict.
    3: split. 3: lia. 3: instantiate (1:= 13). 3: generalize MA_bound; lia.
    vm_compute. destr.
    vm_compute; destr.
    apply Z.add_nonneg_nonneg. apply Z.div_pos. vm_compute; destr.
    apply Z.gt_lt, two_power_nat_pos. lia.
  Qed.

  Lemma valid_box_repr_le:
    forall x (i: (0 < x <= nb_boxes8_max)%nat)
      o (RNGO: 0 <= o < 8),
      0 <= 8 * Z.of_nat x + o <= Int.max_unsigned.
Proof.
    intros.
    generalize (valid_box_repr _ i _ RNGO). lia.
  Qed.
  
  Lemma in_gfb':
    forall x m cm ,
      Mem.compat_m m Mem.M32 cm ->
      In x (get_free_boxes m cm) ->
      (0 < x <= nb_boxes8_max)%nat /\
      forall b o o',
        Mem.in_bound_m (Int.unsigned o) m b ->
        0 <= Int.unsigned o' < 8 ->
        Int.unsigned (Int.add (cm b) o) <> Int.unsigned (Int.add (Int.repr (8 * Z.of_nat x)) o').
Proof.
    intros x m cm COMP IN.
    apply in_gfb in IN. des IN.
    rewrite list_ints_In in i.
    split; auto.
    intros b o o' IB IB'.
    rewrite Forall_forall in f. trim (f b).
    eapply mbla_below_in.
    eapply Mem.in_bound_valid in IB. red in IB. apply Pos2Nat.inj_lt in IB. lia.
    generalize IB; intro MIB.
    des (in_dec eq_nat_dec x (box_range' m cm b)).
    clear Heqs f.
    unfold box_range', box_range in n.
    red in IB. rewrite bounds_eq in IB.
    red in IB. simpl in IB.
    destr_in n; [| lia].
    assert (~ (Z.to_nat (Int.unsigned (cm b) / 8) <= x <= Z.to_nat ((Int.unsigned (cm b) + Mem.size_block m b - 1)/8)))%nat as RNG.
    {
      intro RNG. apply n. apply range_nat_range_range. auto.
    }
    clear n.
    intro EQ.
    destruct RNG.
    unfold Int.add in EQ.
    rewrite (Int.unsigned_repr ( 8 * _ )) in EQ.
    2: replace (8 * Z.of_nat x) with (8 * Z.of_nat x + 0) by lia; apply valid_box_repr_le; auto; lia.
    rewrite ! Int.unsigned_repr in EQ.
    2: apply valid_box_repr_le; auto; lia.
    - replace (Int.unsigned (cm b)) with ((Int.unsigned o' - Int.unsigned o) + Z.of_nat x * 8) by lia.
      clear EQ.
      replace ((Int.unsigned o' - Int.unsigned o) + Z.of_nat x * 8 + Mem.size_block m b - 1)
      with ((Int.unsigned o' - Int.unsigned o + (Mem.size_block m b - 1)) + Z.of_nat x * 8) by lia.
      rewrite ! Z_div_plus_full by lia.
      split.
      + apply Nat2Z.inj_le.
        rewrite nat_of_Z_max.
        rewrite Zmax_spec. destr. 2: lia.
        cut ((Int.unsigned o' - Int.unsigned o) / 8 <= 0). lia.
        destruct (zlt (Int.unsigned o' - Int.unsigned o) 0).
        eapply BigNumPrelude.Zdiv_neg in l1.
        apply Z.lt_le_incl; eauto. lia.
        rewrite Z.div_small. lia. lia.
      + apply Nat2Z.inj_le.
        rewrite Z2Nat.id.
        cut (0 <= (Int.unsigned o' - Int.unsigned o + (Mem.size_block m b - 1)) / 8). lia.
        apply Z.div_pos. 2: lia.
        transitivity ((Mem.size_block m b - Int.unsigned o - 1) + Int.unsigned o'); lia.
        apply Z.add_nonneg_nonneg; try lia.
        apply Z.div_pos; lia.
    - erewrite <- compat_add_unsigned. 3: apply COMP. 3: apply MIB.
      exploit addr_space. apply COMP. apply MIB. simpl. lia.
      intros; rewrite bounds_eq; reflexivity.
  Qed.

  Lemma lnr_gfb:
    forall m cm,
      list_norepet (get_free_boxes m cm).
Proof.
    unfold get_free_boxes.
    intros.
    match goal with
      |- context [ fold_left ?g ?a ?b ] => set (f := g)
    end.
    cut (list_norepet (list_ints nb_boxes8_max)).
    generalize (list_ints nb_boxes8_max) as ints.
    generalize (lnr_mbl m).
    generalize (map fst (Mem.mk_block_list m)).
    induction l; simpl; intros; auto.
    - trim IHl. inv H; auto.
      apply IHl. unfold f.
      apply filter_norepet. auto.
    - apply lnr_list_ints.
  Qed.

  Lemma in_gfb_addrspace:
    forall x m cm ,
      In x (get_free_boxes m cm) ->
      forall o, 0 <= Int.unsigned o < 8 -> 0 < (8 * Z.of_nat x) + Int.unsigned o < Int.max_unsigned.
Proof.
    intros x m cm IN.
    apply in_gfb in IN. des IN.
    rewrite list_ints_In in i.
    intros o SMALL.
    split. lia.
    apply valid_box_repr; auto.
  Qed.

  Lemma get_free_boxes_filter:
    forall m cm,
      Permutation
        (get_free_boxes m cm)
        (filter
           (fun box => negb
                      (existsb
                         (fun b => in_dec eq_nat_dec box (box_range' m cm b))
                         (map fst (Mem.mk_block_list m))))
           (list_ints nb_boxes8_max)).
Proof.
    unfold get_free_boxes.
    intros.
    generalize (list_ints nb_boxes8_max).
    generalize (map fst (Mem.mk_block_list m)).
    induction l; simpl; intros.
    - rewrite filter_true; reflexivity.
    - rewrite IHl.
      rewrite filter_filter.
      erewrite filter_ext. reflexivity.
      simpl; intros.
      rewrite negb_orb. ring.
  Qed.

  Lemma get_used_boxes_filter:
    forall m cm (COMP: Mem.compat_m m Mem.M32 cm),
      Permutation (remove_dbl eq_nat_dec (concat (map (box_range cm) (Mem.mk_block_list m))))
                  (filter (fun x : nat => existsb (fun b : block => in_dec eq_nat_dec x (box_range' m cm b)) (map fst (Mem.mk_block_list m)))
                          (list_ints nb_boxes8_max ++ O :: nat_range (S nb_boxes8_max) (Z.to_nat (Int.max_unsigned / 8)))).
Proof.
    intros m cm COMP.
    eapply Permutation_intro. apply eq_nat_dec.
    apply remove_dbl_lnr.
    apply filter_norepet.
    {
      apply list_norepet_append; auto.
      apply lnr_list_ints. constructor.
      intro IN; apply nat_range_range in IN. destruct IN. clear - H. lia.
      apply lnr_nat_range.
      red; intros. rewrite list_ints_In in H.
      simpl in H0. des H0. lia. apply nat_range_range in i. des i. clear l0. lia.
    }
    intros.
    rewrite <- remove_dbl_In.
    rewrite filter_In.
    rewrite in_concat.
    rewrite existsb_exists.
    split.
    - intros (l' & INboxes & INl').
      rewrite in_map_iff in INboxes. destruct INboxes as ((b & sz) & BOXRANGE & INM). subst.
      split.
      + simpl in INl'. destr_in INl'.
        rewrite in_app, list_ints_In.
        apply nat_range_range in INl'.
        cut (x <= Z.to_nat (Int.max_unsigned / 8))%nat. intros LE. simpl.
        destruct (lt_dec O x). destruct (le_dec x nb_boxes8_max); auto.
        right. right. apply range_nat_range_range. lia. right; left; lia.
        
        exploit mbla_in. apply INM. intro; subst.
        assert (Mem.size_block m b <= Int.max_unsigned) by eauto using size_block_mu.

        etransitivity. apply INl'.
        apply Nat2Z.inj_le. rewrite Z2Nat.id.
        exploit compat_add_unsigned. 2: apply COMP.
        intros; rewrite bounds_eq; simpl; auto.
        rewrite bounds_eq. red; simpl. instantiate (2:= Int.repr (Mem.size_block m b - 1)).
        split. apply Int.unsigned_range.
        rewrite Int.unsigned_repr.
        instantiate (1:=b). lia. split. lia.
        lia.
        rewrite Int.unsigned_repr by lia. intro A.
        replace (Int.unsigned (cm b) + Mem.size_block m b - 1) with
        (Int.unsigned (cm b) + (Mem.size_block m b - 1)) by lia.
        rewrite <- A.
        etransitivity.
        apply Z.div_le_mono. lia. apply Int.unsigned_range_2.
        rewrite Z2Nat.id. lia. vm_compute; destr.
        apply Z.div_pos. generalize (Int.unsigned_range (cm b)). lia.
        lia.

      + exists b; split.
        rewrite in_map_iff. exists (b,sz). split; auto.
        destruct (in_dec eq_nat_dec x (box_range' m cm b)); auto.
        unfold box_range' in n. Opaque box_range. simpl in n.
        unfold Mem.mk_block_list in INM.
        eapply mbla_in in INM. subst. congruence.
    - intros (IN & (b & INM & INBOX)).
      rewrite in_map_iff in INM. destruct INM as ((bb & z) & EQ & INM). subst. simpl in *.
      eexists; split.
      rewrite in_map_iff. eexists; split; eauto.
      des (in_dec eq_nat_dec x (box_range' m cm bb)).
      unfold box_range' in i.
      unfold Mem.mk_block_list in INM.
      eapply mbla_in in INM. subst. congruence.
  Qed.

  Lemma length_get_free_boxes:
    forall m cm,
      Mem.compat_m m Mem.M32 cm ->
      (Z.to_nat Mem.nb_boxes_max * NPeano.pow 2 (MA - 3) <= length (get_free_boxes m cm) + nb_boxes_used_cm m cm)%nat.
Proof.
    unfold nb_boxes_used_cm.
    intros m cm COMP.
    transitivity (length (list_ints nb_boxes8_max)).
    unfold nb_boxes8_max. rewrite list_ints_length. lia.
    rewrite (Permutation_length (get_free_boxes_filter m cm)).
    rewrite (Permutation_length (get_used_boxes_filter m cm COMP)).
    rewrite filter_app.
    rewrite app_length.
    rewrite plus_assoc.
    apply le_plus_trans.
    rewrite plus_comm.
    rewrite <- app_length.
    rewrite <- length_filters. lia.
  Qed.

  Lemma has_free_boxes_correct:
    forall m cm n,
      Mem.compat_m m Mem.M32 cm ->
      has_free_boxes m cm n ->
      exists l,
        (length l >= n)%nat /\
        list_norepet l /\
        Forall (fun z : Z => forall b o o',
                    Mem.in_bound_m (Int.unsigned o) m b ->
                    0 <= Int.unsigned o' < 8 ->
                    Int.unsigned (Int.add (cm b) o) <> Int.unsigned (Int.add (Int.repr z) o')) l /\
        Forall (fun z => forall o, 0 <= Int.unsigned o < 8 -> 0 < z + Int.unsigned o < Int.max_unsigned) l /\
        Forall (fun z => exists k, z = 8 * k) l.
Proof.
    intros m cm n COMP HFB.
    set (l := get_free_boxes m cm).
    exists (map (fun n => 8 * Z.of_nat n) l).
    repSplit.
    - rewrite map_length. red in HFB.
      cut (Z.to_nat Mem.nb_boxes_max * NPeano.pow 2 (MA - 3) <= length l + nb_boxes_used_cm m cm)%nat. lia.
      unfold l. apply length_get_free_boxes. auto.
    - apply list_map_norepet. apply lnr_gfb.
      intros. lia.
    - rewrite Forall_forall. intros x.
      rewrite in_map_iff. intros (x0 & EQ & IN). subst.
      intros b o o' IB IB'.
      exploit in_gfb'; eauto. intros (RNG & NOOV).
      apply NOOV; auto.
    - rewrite Forall_forall. intros x.
      rewrite in_map_iff. intros (x0 & EQ & IN). subst.
      unfold l in *. intros.
      exploit in_gfb_addrspace; eauto.
    - rewrite Forall_forall. intros x.
      rewrite in_map_iff. intros (x0 & EQ & IN). eauto.
  Qed.



End GET_FREE_BOXES.
Generated by coq2html