Module ZIntervalDomain


Require Import Coqlib Values Zbits Integers Lattice.
Require Import RTL Registers Maps.
Require Eqdep_dec.
Require Import Program.
Require AST.

Inductive ibool :=
  | Bnone
  | Just (b : bool)
  | Any_bool
  | Btop.

Inductive cmatch : option bool -> ibool -> Prop :=
  | cmatch_none : cmatch None Bnone
  | cmatch_just : forall b, cmatch (Some b) (Just b)
  | cmatch_any: forall b, cmatch (Some b) Any_bool
  | cmatch_top: forall ob, cmatch ob Btop.

Unset Transparent Obligations.

Section Decidable.

  Variable T: Type.
  Variable beq : T -> T -> bool.
  Variable beq_correct: forall x y, beq x y = true -> x = y.
  Variable beq_correct2: forall x y, beq x y = false -> x <> y.

  Definition eq_dec: forall (x y : T), {x=y} + {x<>y}.
  Proof.
    intros.
    pose proof (beq_correct x y).
    pose proof (beq_correct2 x y).
    destruct (beq x y).
    - left. auto.
    - right. auto.
  Qed.
End Decidable.

Module Interval <: SEMILATTICE_WITHOUT_BOTTOM.

Record interval :=
  mkinterval { itv_lo : Z.t;
               itv_hi : Z.t;
               itv_ok : itv_lo <=? itv_hi = true }.

Lemma itv_eq_bounds :
  forall a b,
    a.(itv_lo) = b.(itv_lo) ->
    a.(itv_hi) = b.(itv_hi) ->
    a = b.
Proof.
  intros.
  destruct a as [aulo auhi auok].
  destruct b as [bulo buhi buok].
  cbn in *.
  subst. f_equal.
  apply Eqdep_dec.UIP_dec.
  decide equality.
Qed.

Definition t := interval.

Definition eq := @eq t.

Lemma eq_refl: forall x, eq x x.
Proof.
  apply (@eq_refl t).
Qed.

Lemma eq_sym: forall x y, eq x y -> eq y x.
Proof.
  apply (@eq_sym t).
Qed.

Definition eq2 a b := a.(itv_lo) = b.(itv_lo) /\ a.(itv_hi) = b.(itv_hi).

Lemma eq2_eqv: forall a b, eq a b <-> eq2 a b.
Proof.
  unfold eq, eq2. intros. split.
  intuition congruence.
  intros (LO & HI).
  apply itv_eq_bounds; assumption.
Qed.

Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
Proof.
  exact (@eq_trans t).
Qed.

Definition beq (a b : t) :=
  (a.(itv_lo) =? b.(itv_lo)) && (a.(itv_hi) =? b.(itv_hi)).

Lemma beq_correct: forall x y, beq x y = true -> eq x y.
Proof.
  intros. rewrite eq2_eqv.
  unfold beq, eq2 in *.
  intuition lia.
Qed.

Lemma beq_correct2: forall x y, beq x y = false -> x <> y.
Proof.
  intros.
  destruct x. destruct y.
  unfold beq in *. cbn in *.
  intro Z. inv Z.
  lia.
Qed.

Lemma eq_dec: forall (a b : t), {a=b} + {a<>b}.
Proof.
  exact (eq_dec t beq beq_correct beq_correct2).
Qed.

Definition ge (a b : t) :=
  a.(itv_lo) <= b.(itv_lo) /\
  a.(itv_hi) >= b.(itv_hi).

Lemma ge_refl: forall x y, eq x y -> ge x y.
Proof.
  unfold eq, ge. intros. subst.
  intuition lia.
Qed.

Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
Proof.
  unfold ge. intuition lia.
Qed.

Lemma ge_antisym : forall x y, ge x y -> ge y x -> eq x y.
Proof.
  intros. rewrite eq2_eqv. unfold ge, eq2 in *.
  intuition lia.
Qed.

Program Definition lub (a b : t) :=
  {| itv_lo := Z.min a.(itv_lo) b.(itv_lo);
     itv_hi := Z.max a.(itv_hi) b.(itv_hi);
    itv_ok := _ |}.
Obligation 1.
Proof.
  destruct a. destruct b. cbn. lia.
Qed.

Lemma ge_lub_left: forall x y, ge (lub x y) x.
Proof.
  unfold ge, lub. cbn.
  intuition lia.
Qed.

Lemma ge_lub_right: forall x y, ge (lub x y) y.
Proof.
  unfold ge, lub. cbn.
  intuition lia.
Qed.

Lemma lub_least:
  forall r p q, ge r p -> ge r q -> ge r (lub p q).
Proof.
  unfold ge. intros.
  destruct r. destruct p. destruct q.
  cbn in *. intuition lia.
Qed.

Definition zmatch z itv :=
  itv.(itv_lo) <= z <= itv.(itv_hi).

Lemma zmatch_lub_left :
  forall z a b (MATCH : zmatch z a), (zmatch z (lub a b)).
Proof.
  destruct a, b.
  unfold zmatch, lub; cbn. lia.
Qed.

Lemma zmatch_lub_right :
  forall z a b (MATCH : zmatch z b), (zmatch z (lub a b)).
Proof.
  destruct a, b.
  unfold zmatch, lub; cbn. lia.
Qed.

Definition ge_sem a b :=
  forall z, (zmatch z b) -> (zmatch z a).

Lemma ge_sem_eqv : forall a b,
    ge a b <-> ge_sem a b.
Proof.
  unfold ge, ge_sem, zmatch.
  intros. destruct a. destruct b. cbn.
  split.
  - intuition lia.
  - intro ZZ.
    split.
    + apply ZZ. lia.
    + apply Z.le_ge. apply ZZ. lia.
Qed.

Lemma zmatch_ge:
  forall a b z, ge a b -> zmatch z b -> zmatch z a.
Proof.
  intros. rewrite ge_sem_eqv in H.
  unfold ge_sem in H.
  auto.
Qed.

Definition eq_sem a b :=
  forall z, (zmatch z a) <-> (zmatch z b).

Lemma eq_sem_eqv : forall a b,
    eq a b <-> eq_sem a b.
Proof.
  intros.
  destruct a as [la ha LEa].
  destruct b as [lb hb LEb].
  split.
  - unfold eq_sem, eq, zmatch. cbn.
    intro EQ. inv EQ. lia.
  - intro SEM. apply ge_antisym.
    + apply ge_sem_eqv. unfold eq_sem, ge_sem in *.
      intros. apply SEM. assumption.
    + apply ge_sem_eqv. unfold eq_sem, ge_sem in *.
      intros. apply SEM. assumption.
Qed.

Program Definition add (a b : t) : t :=
  {| itv_lo := Z.add a.(itv_lo) b.(itv_lo) ;
     itv_hi := Z.add a.(itv_hi) b.(itv_hi) ;
     itv_ok := _ |}.
Next Obligation.
  destruct a. destruct b. cbn. lia.
Qed.

Lemma zmatch_add :
  forall (x y : Z.t) (a b : t) (AMATCH : zmatch x a) (BMATCH : zmatch y b),
    zmatch (Z.add x y) (add a b).
Proof.
  destruct a. destruct b. unfold add, zmatch. cbn. lia.
Qed.

Lemma minimal_add :
  forall itv a b
         (OK :
           forall (x y : Z.t)
                  (AMATCH : zmatch x a) (BMATCH : zmatch y b),
             zmatch (Z.add x y) itv),
    ge itv (add a b).
Proof.
  destruct a. destruct b. destruct itv.
  unfold zmatch, ge. cbn.
  intros.
  pose proof (OK itv_hi0 itv_hi1).
  pose proof (OK itv_lo0 itv_lo1).
  lia.
Qed.

Program Definition sub (a b : t) : t :=
  {| itv_lo := Z.sub a.(itv_lo) b.(itv_hi) ;
     itv_hi := Z.sub a.(itv_hi) b.(itv_lo) ;
     itv_ok := _ |}.
Next Obligation.
  destruct a. destruct b. cbn. lia.
Qed.

Lemma zmatch_sub :
  forall (x y : Z.t) (a b : t) (AMATCH : zmatch x a) (BMATCH : zmatch y b),
    zmatch (Z.sub x y) (sub a b).
Proof.
  destruct a. destruct b. unfold sub, zmatch. cbn. lia.
Qed.

Lemma minimal_sub :
  forall itv a b
         (OK :
           forall (x y : Z.t)
                  (AMATCH : zmatch x a) (BMATCH : zmatch y b),
             zmatch (Z.sub x y) itv),
    ge itv (sub a b).
Proof.
  destruct a. destruct b. destruct itv.
  unfold zmatch, ge. cbn.
  intros.
  pose proof (OK itv_hi0 itv_lo1).
  pose proof (OK itv_lo0 itv_hi1).
  lia.
Qed.

Program Definition mul (a b : t) : t :=
  let c1 := Z.mul a.(itv_lo) b.(itv_lo) in
  let c2 := Z.mul a.(itv_lo) b.(itv_hi) in
  let c3 := Z.mul a.(itv_hi) b.(itv_lo) in
  let c4 := Z.mul a.(itv_hi) b.(itv_hi) in
  {| itv_lo := Z.min (Z.min c1 c2) (Z.min c3 c4) ;
     itv_hi := Z.max (Z.max c1 c2) (Z.max c3 c4) ;
    itv_ok := _ |}.
Next Obligation.
  destruct a. destruct b. unfold zmatch. cbn. nia.
Qed.

Lemma zmatch_mul :
  forall (x y : Z.t) (a b : t) (AMATCH : zmatch x a) (BMATCH : zmatch y b),
    zmatch (Z.mul x y) (mul a b).
Proof.
  destruct a. destruct b. unfold mul, zmatch. cbn. intros.
  pose proof (Z.compare_spec itv_lo0 0) as CMP; inv CMP;
    pose proof (Z.compare_spec itv_hi0 0) as CMP; inv CMP.
  all: try lia.
  all: pose proof (Z.compare_spec itv_lo1 0) as CMP; inv CMP;
    pose proof (Z.compare_spec itv_hi1 0) as CMP; inv CMP.
  all: try lia.
  all: try nia.
  pose proof (Z.compare_spec x 0) as CMP; inv CMP;
    pose proof (Z.compare_spec y 0) as CMP; inv CMP.
  all: nia.
Qed.

Lemma minimal_mul :
  forall itv a b
         (OK :
           forall (x y : Z.t)
                  (AMATCH : zmatch x a) (BMATCH : zmatch y b),
             zmatch (Z.mul x y) itv),
    ge itv (mul a b).
Proof.
  destruct a. destruct b. destruct itv.
  unfold zmatch, ge. cbn.
  intros.
  pose proof (OK itv_hi0 itv_lo1).
  pose proof (OK itv_lo0 itv_hi1).
  pose proof (OK itv_lo0 itv_lo1).
  pose proof (OK itv_hi0 itv_hi1).
  lia.
Qed.

Program Definition shl (lhs rhs : t)
  (POS_lhs: 0 <=? itv_lo lhs = true)
  (POS_rhs: 0 <=? itv_lo rhs = true) : t :=
  mkinterval (Z.shiftl lhs.(itv_lo) rhs.(itv_lo))
             (Z.shiftl lhs.(itv_hi) rhs.(itv_hi)) _.
Next Obligation.
  destruct lhs, rhs; cbn in *.
  apply Zle_imp_le_bool.
  rewrite Z.shiftl_mul_pow2 by lia.
  rewrite Z.shiftl_mul_pow2 by lia.
  apply Z.mul_le_mono_nonneg. lia. lia. nia.
  apply Zpow_facts.Zpower_le_monotone. lia. lia.
Qed.

Lemma zmatch_shl (x y : Z.t) (a b : t) POS_a POS_b:
  zmatch x a -> zmatch y b ->
  zmatch (Z.shiftl x y) (shl a b POS_a POS_b).
Proof.
  intros [] [].
  constructor; cbn;
  rewrite !Z.shiftl_mul_pow2 by lia.
  - apply Z.mul_le_mono_nonneg. lia. lia. nia.
    apply Zpow_facts.Zpower_le_monotone. lia. lia.
  - apply Z.mul_le_mono_nonneg. lia. lia. nia.
    apply Zpow_facts.Zpower_le_monotone. lia. lia.
Qed.

Program Definition intconst i := mkinterval i i _.
Next Obligation.
  lia.
Qed.

Lemma zmatch_intconst: forall i, zmatch i (intconst i).
Proof.
  unfold zmatch, intconst. cbn. lia.
Qed.

Program Definition glb_nb (a b : t) : option t :=
  let lo := Z.max a.(itv_lo) b.(itv_lo) in
  let hi := Z.min a.(itv_hi) b.(itv_hi) in
  if zle lo hi
  then Some (mkinterval lo hi _)
  else None.
Next Obligation.
  lia.
Qed.

Lemma zmatch_glb_nb:
  forall x a b
         (MATCHx : zmatch x a) (MATCHy : zmatch x b),
  exists c,
    glb_nb a b = Some c /\ zmatch x c.
Proof.
  unfold zmatch, glb_nb; destruct a; destruct b; cbn; intros.
  destruct zle.
  - eexists. split. reflexivity. cbn. lia.
  - exfalso. lia.
Qed.

Program Definition filter_less_equal (i0 i1 : t) : option (t*t) :=
  if zle i0.(itv_lo) i1.(itv_hi)
  then Some((mkinterval i0.(itv_lo) (Z.min i0.(itv_hi) i1.(itv_hi)) _),
             (mkinterval (Z.max i0.(itv_lo) i1.(itv_lo)) i1.(itv_hi) _))
  else None.
Solve Obligations with destruct i0, i1; cbn in *; lia.

Lemma zmatch_filter_less_equal :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x <= y),
    exists a', exists b',
      filter_less_equal a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  unfold zmatch, filter_less_equal.
  destruct a, b. cbn. intros.
  destruct zle; cbn; cycle 1.
  { exfalso. lia. }
  eexists. eexists. split. reflexivity. cbn.
  split; lia.
Qed.

Program Definition filter_less (i0 i1 : t) : option (t*t) :=
  if zlt i0.(itv_lo) i1.(itv_hi)
  then Some((mkinterval i0.(itv_lo) (Z.min i0.(itv_hi) (i1.(itv_hi)-1)) _),
             (mkinterval (Z.max (i0.(itv_lo)+1) i1.(itv_lo)) i1.(itv_hi) _))
  else None.
Solve Obligations with destruct i0, i1; cbn in *; lia.

Lemma zmatch_filter_less :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x < y),
    exists a', exists b',
      filter_less a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  unfold zmatch, filter_less.
  destruct a, b. cbn. intros.
  destruct zlt; cbn; cycle 1.
  { exfalso. lia. }
  eexists. eexists. split. reflexivity. cbn.
  split; lia.
Qed.

Definition pair_lub ip0 ip1 :=
  match ip0, ip1 with
  | Some(i0', i1'), None => Some(i0', i1')
  | None, Some(i0', i1') => Some(i0', i1')
  | Some(i0', i1'), Some(i0'', i1'') => Some ((lub i0' i0''), (lub i1' i1''))
  | None, None => None
  end.

Lemma zmatch_pair_lub_left :
  forall (x y : Z.t) (a b : t) (other : option(t*t))
         (AMATCH : zmatch x a) (BMATCH : zmatch y b),
    exists a', exists b',
      pair_lub (Some (a, b)) other = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  intros.
  unfold pair_lub.
  destruct other as [[a' b'] | ]; cbn.
  - eexists. eexists. split. reflexivity. split.
    + apply zmatch_lub_left. assumption.
    + apply zmatch_lub_left. assumption.
  - eexists. eexists. split. reflexivity. split; assumption.
Qed.

Lemma zmatch_pair_lub_right :
  forall (other : option(t*t)) (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b),
    exists a', exists b',
      pair_lub other (Some (a, b)) = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  intros.
  unfold pair_lub.
  destruct other as [[a' b'] | ]; cbn.
  - eexists. eexists. split. reflexivity. split.
    + apply zmatch_lub_right. assumption.
    + apply zmatch_lub_right. assumption.
  - eexists. eexists. split. reflexivity. split; assumption.
Qed.

Definition filter_not_equal i0 i1 :=
  match (filter_less i0 i1),
        (filter_less i1 i0) with
  | Some(i0', i1'), None => Some(i0', i1')
  | None, Some(i1', i0') => Some(i0', i1')
  | Some(i0', i1'), Some(i1'', i0'') => Some ((lub i0' i0''), (lub i1' i1''))
  | None, None => None
  end.

Lemma zmatch_filter_not_equal :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x <> y),
    exists a', exists b',
      filter_not_equal a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  intros. unfold filter_not_equal.
  assert (x < y \/ y < x) as INEQ by lia.
  destruct INEQ as [LT | GT].
  { destruct (zmatch_filter_less x y a b AMATCH BMATCH LT) as (a' & b' & RE & AMATCH' & BMATCH').
    rewrite RE.
    destruct (filter_less b a) as [[b'' a'']| ].
    { eexists. eexists. eauto using zmatch_lub_left. }
    eexists. eexists. eauto.
  }
  destruct (zmatch_filter_less y x b a BMATCH AMATCH GT) as (b' & a' & RE & BMATCH' & AMATCH').
  rewrite RE.
  destruct (filter_less a b) as [[a'' b'']| ].
  { eexists. eexists. eauto using zmatch_lub_right. }
  eexists. eexists. eauto.
Qed.
End Interval.

Module Interval_Bot <: SEMILATTICE.
  Include ADD_BOTTOM(Interval).

  Lemma ge_glb_nb_left: forall (a b : Interval.t),
      ge (Some a) (Interval.glb_nb a b).
  Proof.
    unfold Interval.glb_nb, ge.
    intros.
    destruct zle. 2: constructor.
    constructor; cbn; lia.
  Qed.
  
  Lemma ge_glb_nb_right: forall (a b : Interval.t),
      ge (Some b) (Interval.glb_nb a b).
  Proof.
    unfold Interval.glb_nb, ge.
    intros.
    destruct zle. 2: constructor.
    constructor; cbn; lia.
  Qed.

  Definition glb (a b : t) : t :=
    match a, b with
    | None, _ | _, None => None
    | (Some x), (Some y) => Interval.glb_nb x y
    end.
  
  Lemma glb_greatest:
    forall r p q, ge p r -> ge q r -> ge (glb p q) r.
  Proof.
    unfold ge. intros until q. intros GE0 GE1.
    destruct p; destruct q; destruct r; cbn; trivial.
    { unfold Interval.glb_nb.
      destruct t0 as [lo0 hi0 LE0].
      destruct t1 as [lo1 hi1 LE1].
      destruct t2 as [lo2 hi2 LE2].
      inv GE0. inv GE1. cbn in *.
      destruct zle ; cbn in *.
      - constructor; cbn; lia.
      - lia.
    }
    destruct Interval.glb_nb; trivial.
  Qed.

  Definition eq_dec:
    forall (x y : t), {x = y} + {x <> y}.
  Proof.
    generalize Interval.eq_dec.
    decide equality.
  Qed.
End Interval_Bot.

Module Type MODULUS_TYPE.
  Axiom modulus : Z.t.
  Axiom modulus_pos : modulus > 0.
End MODULUS_TYPE.

Module Modulus_Interval(Int_Type : MODULUS_TYPE).
  Notation modulus := Int_Type.modulus.
  Notation modulus_positive := Int_Type.modulus_pos.
  
  Record mod_interval :=
    mkmod_interval { mod_itv : Interval.t ;
                     mod_lo : (0 <=? mod_itv.(Interval.itv_lo) = true);
                     mod_hi : (mod_itv.(Interval.itv_hi) <? modulus) = true }.
  Definition t := mod_interval.

  Definition eq := @eq t.

  Lemma eq_refl : forall x, eq x x.
  Proof.
    apply @eq_refl.
  Qed.

  Lemma eq_sym: forall x y, eq x y -> eq y x.
  Proof.
    apply @eq_sym.
  Qed.

  Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
  Proof.
    apply @eq_trans.
  Qed.

  Definition eq2 a b := a.(mod_itv) = b.(mod_itv).

  Lemma itv_eq_bounds :
    forall a b,
      a.(mod_itv) = b.(mod_itv) ->
      a = b.
  Proof.
    destruct a. destruct b. cbn in *.
    intro. subst. f_equal.
    all: apply Eqdep_dec.UIP_dec; decide equality.
  Qed.
  
  Lemma eq2_eqv: forall a b, eq a b <-> eq2 a b.
  Proof.
    unfold eq, eq2. intros. split.
    intuition congruence.
    intro.
    apply itv_eq_bounds; assumption.
  Qed.
  
  Definition beq (a b : t) := Interval.beq a.(mod_itv) b.(mod_itv).

  Lemma beq_correct: forall x y, beq x y = true -> eq x y.
  Proof.
    intros. rewrite eq2_eqv.
    unfold beq, eq2 in *.
    apply Interval.beq_correct. assumption.
  Qed.

  Lemma beq_correct2: forall x y, beq x y = false -> x <> y.
  Proof.
    intros.
    destruct x. destruct y.
    unfold beq in *. cbn in *.
    apply Interval.beq_correct2 in H.
    congruence.
  Qed.

  Lemma eq_dec: forall (a b : t), {a=b} + {a<>b}.
  Proof.
    exact (eq_dec t beq beq_correct beq_correct2).
  Qed.

  Definition ge (a b : t) := Interval.ge a.(mod_itv) b.(mod_itv).

  Lemma ge_refl: forall x y, eq x y -> ge x y.
  Proof.
    unfold eq, ge. intros. subst.
    apply Interval.ge_refl. constructor.
  Qed.

  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
  Proof.
    unfold ge. intros.
    eapply Interval.ge_trans; eassumption.
  Qed.

  Lemma ge_antisym : forall x y, ge x y -> ge y x -> eq x y.
  Proof.
    unfold ge, eq. intros.
    rewrite eq2_eqv.
    apply Interval.ge_antisym; assumption.
  Qed.

  Program Definition lub (a b : t) :=
    mkmod_interval (Interval.lub a.(mod_itv) b.(mod_itv)) _ _.
  Solve Obligations with (destruct a; destruct b; cbn; lia).

  Lemma ge_lub_left: forall x y, ge (lub x y) x.
  Proof.
    unfold ge, lub. cbn. intros.
    apply Interval.ge_lub_left.
  Qed.
  
  Lemma ge_lub_right: forall x y, ge (lub x y) y.
  Proof.
    unfold ge, lub. cbn. intros.
    apply Interval.ge_lub_right.
  Qed.

  Lemma lub_least:
    forall r p q, ge r p -> ge r q -> ge r (lub p q).
  Proof.
    unfold ge, lub. cbn. intros.
    apply Interval.lub_least; assumption.
  Qed.

  Program Definition full_range : t :=
    mkmod_interval (Interval.mkinterval 0 (modulus - 1) _) _ _.
  Next Obligation.
    pose proof modulus_positive.
    lia.
  Qed.
  Next Obligation.
    pose proof modulus_positive.
    lia.
  Qed.

  Definition zmatch z a := Interval.zmatch z a.(mod_itv).
  
  Lemma zmatch_lub_left :
    forall z a b (MATCH : zmatch z a), (zmatch z (lub a b)).
  Proof.
    destruct a, b. unfold zmatch, lub. cbn. intros.
    apply Interval.zmatch_lub_left; assumption.
  Qed.
  
  Lemma zmatch_lub_right :
    forall z a b (MATCH : zmatch z b), (zmatch z (lub a b)).
  Proof.
    destruct a, b. unfold zmatch, lub. cbn. intros.
    apply Interval.zmatch_lub_right; assumption.
  Qed.

  Lemma zmatch_full_range :
    forall z (RANGE : 0 <= z < modulus), zmatch z full_range.
  Proof.
    pose proof modulus_positive.
    unfold full_range, zmatch, Interval.zmatch. cbn.
    intros. lia.
  Qed.

  Program Definition force (a : Interval.t) : t :=
    if Z_ge_lt_dec a.(Interval.itv_lo) 0
    then if Z_ge_lt_dec a.(Interval.itv_hi) modulus
         then full_range
         else mkmod_interval a _ _
    else full_range.
  Solve Obligations with lia.
     
  Definition add (a b : t) :=
    force (Interval.add a.(mod_itv) b.(mod_itv)).

  Definition sub (a b : t) :=
    force (Interval.sub a.(mod_itv) b.(mod_itv)).

  Definition mul (a b : t) :=
    force (Interval.mul a.(mod_itv) b.(mod_itv)).

  Lemma zmatch_force : forall z a,
      (Interval.zmatch z a) ->
      (zmatch (z mod modulus) (force a)).
  Proof.
    pose proof modulus_positive.
    unfold force. intros.
    destruct Z_ge_lt_dec; cycle 1.
    { apply zmatch_full_range.
      apply Z_mod_lt. assumption. }
    destruct Z_ge_lt_dec.
    { apply zmatch_full_range.
      apply Z_mod_lt. assumption. }
    unfold zmatch, Interval.zmatch in *. cbn.
    rewrite Zmod_small. assumption.
    lia.
  Qed.

  Lemma zmatch_add:
        forall (x y : Z.t) (a b : t)
               (AMATCH : zmatch x a) (BMATCH : zmatch y b),
          zmatch ((x + y) mod modulus) (add a b).
  Proof.
    destruct a. destruct b. unfold add. cbn. intros.
    apply zmatch_force.
    unfold zmatch in *. cbn in *.
    apply Interval.zmatch_add; assumption.
  Qed.

  Lemma zmatch_sub:
        forall (x y : Z.t) (a b : t)
               (AMATCH : zmatch x a) (BMATCH : zmatch y b),
          zmatch ((x - y) mod modulus) (sub a b).
  Proof.
    destruct a. destruct b. unfold sub. cbn. intros.
    apply zmatch_force.
    unfold zmatch in *. cbn in *.
    apply Interval.zmatch_sub; assumption.
  Qed.

  Lemma zmatch_mul:
        forall (x y : Z.t) (a b : t)
               (AMATCH : zmatch x a) (BMATCH : zmatch y b),
          zmatch ((x * y) mod modulus) (mul a b).
  Proof.
    destruct a. destruct b. unfold mul. cbn. intros.
    apply zmatch_force.
    unfold zmatch in *. cbn in *.
    apply Interval.zmatch_mul; assumption.
  Qed.

  Program Definition intconst i :=
    mkmod_interval (Interval.intconst (i mod modulus)) _ _.
  Next Obligation.
    pose proof (Z_mod_lt i modulus modulus_positive). lia.
  Qed.
  Next Obligation.
    pose proof (Z_mod_lt i modulus modulus_positive). lia.
  Qed.

  Lemma zmatch_intconst :
    forall i, zmatch (i mod modulus) (intconst i).
  Proof.
    intros. unfold zmatch, intconst. cbn.
    apply Interval.zmatch_intconst.
  Qed.
  
  Lemma zmatch_ge:
    forall a b z, ge a b -> zmatch z b -> zmatch z a.
  Proof.
    unfold ge. intros.
    eapply Interval.zmatch_ge; eassumption.
  Qed.


  Program Definition glb_nb (a b : t) : option t :=
    let lo := Z.max a.(mod_itv).(Interval.itv_lo) b.(mod_itv).(Interval.itv_lo) in
    let hi := Z.min a.(mod_itv).(Interval.itv_hi) b.(mod_itv).(Interval.itv_hi) in
    if zle lo hi
    then Some (mkmod_interval (Interval.mkinterval lo hi _) _ _)
    else None.
  Next Obligation.
    lia.
  Qed.
  Next Obligation.
    destruct a. destruct b. cbn in *. lia.
  Qed.
  Next Obligation.
    destruct a. destruct b. cbn in *. lia.
  Qed.

  Lemma zmatch_glb_nb:
    forall x a b
           (MATCHx : zmatch x a) (MATCHy : zmatch x b),
    exists c,
      glb_nb a b = Some c /\ zmatch x c.
  Proof.
    unfold zmatch, glb_nb, Interval.zmatch, Interval.glb_nb.
    destruct a; destruct b.
    destruct mod_itv0; destruct mod_itv1; cbn in *.
    destruct zle.
    - eexists. split. reflexivity. cbn. lia.
    - intros. exfalso. lia.
  Qed.

Program Definition filter_less_equal (i0 i1 : t) : option (t*t) :=
  if zle i0.(mod_itv).(Interval.itv_lo) i1.(mod_itv).(Interval.itv_hi)
  then Some((mkmod_interval
            (Interval.mkinterval i0.(mod_itv).(Interval.itv_lo)
                       (Z.min i0.(mod_itv).(Interval.itv_hi)
                              i1.(mod_itv).(Interval.itv_hi)) _) _ _),
            (mkmod_interval
            (Interval.mkinterval (Z.max i0.(mod_itv).(Interval.itv_lo)
                                i1.(mod_itv).(Interval.itv_lo))
                         i1.(mod_itv).(Interval.itv_hi) _) _ _))
  else None.
Solve Obligations with (destruct i0, i1, mod_itv0, mod_itv1; cbn in *; lia).
  
Lemma zmatch_filter_less_equal :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x <= y),
    exists a', exists b',
      filter_less_equal a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  unfold zmatch, Interval.zmatch, filter_less_equal.
  destruct a, b, mod_itv0, mod_itv1. cbn. intros.
  destruct zle; cbn; cycle 1.
  { exfalso. lia. }
  eexists. eexists. split. reflexivity. cbn.
  split; lia.
Qed.

Program Definition filter_less (i0 i1 : t) : option (t*t) :=
  if zlt i0.(mod_itv).(Interval.itv_lo) i1.(mod_itv).(Interval.itv_hi)
  then Some((mkmod_interval
               (Interval.mkinterval i0.(mod_itv).(Interval.itv_lo)
                    (Z.min i0.(mod_itv).(Interval.itv_hi)
                          (i1.(mod_itv).(Interval.itv_hi)-1)) _) _ _),
            (mkmod_interval
            (Interval.mkinterval (Z.max (i0.(mod_itv).(Interval.itv_lo)+1)
                                i1.(mod_itv).(Interval.itv_lo))
                         i1.(mod_itv).(Interval.itv_hi) _) _ _))
  else None.
Solve Obligations with (destruct i0, i1, mod_itv0, mod_itv1; cbn in *; lia).

Definition filter_greater (i0 i1 : t) :=
  match filter_less i1 i0 with
  | Some(i1', i0') => (Some(i0', i1'))
  | None => None
  end.

Definition filter_greater_equal (i0 i1 : t) :=
  match filter_less_equal i1 i0 with
  | Some(i1', i0') => (Some(i0', i1'))
  | None => None
  end.
  
Lemma zmatch_filter_less :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x < y),
    exists a', exists b',
      filter_less a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  unfold zmatch, Interval.zmatch, filter_less.
  destruct a, b, mod_itv0, mod_itv1. cbn. intros.
  destruct zlt; cbn; cycle 1.
  { exfalso. lia. }
  eexists. eexists. split. reflexivity. cbn.
  split; lia.
Qed.
  
Lemma zmatch_filter_greater :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x > y),
    exists a', exists b',
      filter_greater a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  unfold filter_greater. intros.
  assert (y < x) as ORDER by lia.
  destruct (zmatch_filter_less y x b a BMATCH AMATCH ORDER) as (b' & a' & RE & MATCHB' & MATCHA' ).
  exists a'. exists b'. rewrite RE. auto.
Qed.
  
Lemma zmatch_filter_greater_equal :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x >= y),
    exists a', exists b',
      filter_greater_equal a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  unfold filter_greater_equal. intros.
  assert (y <= x) as ORDER by lia.
  destruct (zmatch_filter_less_equal y x b a BMATCH AMATCH ORDER) as (b' & a' & RE & MATCHB' & MATCHA' ).
  exists a'. exists b'. rewrite RE. auto.
Qed.
      
Definition filter_not_equal i0 i1 :=
  match (filter_less i0 i1),
        (filter_less i1 i0) with
  | Some(i0', i1'), None => Some(i0', i1')
  | None, Some(i1', i0') => Some(i0', i1')
  | Some(i0', i1'), Some(i1'', i0'') => Some ((lub i0' i0''), (lub i1' i1''))
  | None, None => None
  end.

Lemma zmatch_filter_not_equal :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x <> y),
    exists a', exists b',
      filter_not_equal a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  intros. unfold filter_not_equal.
  assert (x < y \/ y < x) as INEQ by lia.
  destruct INEQ as [LT | GT].
  { destruct (zmatch_filter_less x y a b AMATCH BMATCH LT) as (a' & b' & RE & AMATCH' & BMATCH').
    rewrite RE.
    destruct (filter_less b a) as [[b'' a'']| ].
    { eexists. eexists. eauto using zmatch_lub_left. }
    eexists. eexists. eauto.
  }
  destruct (zmatch_filter_less y x b a BMATCH AMATCH GT) as (b' & a' & RE & BMATCH' & AMATCH').
  rewrite RE.
  destruct (filter_less a b) as [[a'' b'']| ].
  { eexists. eexists. eauto using zmatch_lub_right. }
  eexists. eexists. eauto.
Qed.

Definition filter_equal i0 i1 :=
  match glb_nb i0 i1 with
  | Some x => Some(x, x)
  | None => None
  end.

Lemma zmatch_filter_equal :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : x = y),
    exists a', exists b',
      filter_equal a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  intros. unfold filter_equal. subst y.
  destruct (zmatch_glb_nb x a b AMATCH BMATCH) as (c & RE & MATCH).
  exists c. exists c. rewrite RE. auto.
Qed.

Section FILTER_TO_ABOOL.
Variable pred: Z.t -> Z.t -> bool.
Variable filter : t -> t -> option (t*t).
Hypothesis zmatch_filter :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : pred x y = true),
    exists a', exists b',
      filter a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Variable filter_not : t -> t -> option (t*t).
Hypothesis zmatch_filter_not :
  forall (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b)
         (CMP : pred x y = false),
    exists a', exists b',
      filter_not a b = Some(a', b') /\ zmatch x a' /\ zmatch y b'.

Definition filter_to_eval (a b : t) : ibool :=
  match (filter a b), (filter_not a b) with
  | (Some _), (Some _) => Any_bool
  | (Some _), None => Just true
  | None, (Some _) => Just false
  | None, None => Bnone
  end.

Lemma filter_to_eval_sound:
  forall (x y : Z.t) (a b : t) (AMATCH: zmatch x a) (BMATCH: zmatch y b),
    cmatch (Some (pred x y)) (filter_to_eval a b).
Proof.
  intros. unfold filter_to_eval.
  destruct (pred x y) eqn:PRED.
  - pose proof (zmatch_filter x y a b AMATCH BMATCH PRED) as (a' & b' & RE & MATCHA' & MATCHB').
    rewrite RE.
    destruct filter_not; constructor.
  - pose proof (zmatch_filter_not x y a b AMATCH BMATCH PRED) as (a' & b' & RE & MATCHA' & MATCHB').
    rewrite RE.
    destruct filter; constructor.
Qed.
End FILTER_TO_ABOOL.

Definition pair_lub ip0 ip1 :=
  match ip0, ip1 with
  | Some(i0', i1'), None => Some(i0', i1')
  | None, Some(i0', i1') => Some(i0', i1')
  | Some(i0', i1'), Some(i0'', i1'') => Some ((lub i0' i0''), (lub i1' i1''))
  | None, None => None
  end.

Lemma zmatch_pair_lub_left :
  forall (x y : Z.t) (a b : t) (other : option(t*t))
         (AMATCH : zmatch x a) (BMATCH : zmatch y b),
    exists a', exists b',
      pair_lub (Some (a, b)) other = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  intros.
  unfold pair_lub.
  destruct other as [[a' b'] | ]; cbn.
  - eexists. eexists. split. reflexivity. split.
    + apply zmatch_lub_left. assumption.
    + apply zmatch_lub_left. assumption.
  - eexists. eexists. split. reflexivity. split; assumption.
Qed.

Lemma zmatch_pair_lub_right :
  forall (other : option(t*t)) (x y : Z.t) (a b : t)
         (AMATCH : zmatch x a) (BMATCH : zmatch y b),
    exists a', exists b',
      pair_lub other (Some (a, b)) = Some(a', b') /\ zmatch x a' /\ zmatch y b'.
Proof.
  intros.
  unfold pair_lub.
  destruct other as [[a' b'] | ]; cbn.
  - eexists. eexists. split. reflexivity. split.
    + apply zmatch_lub_right. assumption.
    + apply zmatch_lub_right. assumption.
  - eexists. eexists. split. reflexivity. split; assumption.
Qed.
End Modulus_Interval.

Module Modulus_Interval_Bot(Int_Type : MODULUS_TYPE) <: SEMILATTICE.
  Module ModInt := Modulus_Interval(Int_Type).
  Include ADD_BOTTOM(ModInt).

  Lemma ge_glb_nb_left: forall (a b : ModInt.t),
      ge (Some a) (ModInt.glb_nb a b).
  Proof.
    unfold ModInt.glb_nb, ge.
    intros.
    destruct zle. 2: constructor.
    constructor; cbn; lia.
  Qed.
  
  Lemma ge_glb_nb_right: forall (a b : ModInt.t),
      ge (Some b) (ModInt.glb_nb a b).
  Proof.
    unfold ModInt.glb_nb, ge.
    intros.
    destruct zle. 2: constructor.
    constructor; cbn; lia.
  Qed.

  Definition glb (a b : t) : t :=
    match a, b with
    | None, _ | _, None => None
    | (Some x), (Some y) => ModInt.glb_nb x y
    end.
  
  Lemma glb_greatest:
    forall r p q, ge p r -> ge q r -> ge (glb p q) r.
  Proof.
    unfold ge. intros until q. intros GE0 GE1.
    destruct p, q, r; cbn; trivial.
    { unfold ModInt.glb_nb.
      destruct t0 as [lo0 hi0 LE0].
      destruct t1 as [lo1 hi1 LE1].
      destruct t2 as [lo2 hi2 LE2].
      inv GE0. inv GE1. cbn in *.
      destruct zle ; cbn in *.
      - constructor; cbn; lia.
      - destruct lo0, lo1, lo2; cbn in *.
        lia.
    }
    destruct ModInt.glb_nb; trivial.
  Qed.

  Definition eq_dec:
    forall (x y : t), {x = y} + {x <> y}.
  Proof.
    generalize ModInt.eq_dec.
    decide equality.
  Qed.
End Modulus_Interval_Bot.

Module Int_Modulus_Interval_Bot := Modulus_Interval_Bot(Int).
Module Int_Modulus_Interval := Int_Modulus_Interval_Bot.ModInt.
Module Int64_Modulus_Interval_Bot := Modulus_Interval_Bot(Int64).
Module Int64_Modulus_Interval := Int64_Modulus_Interval_Bot.ModInt.

Inductive ival :=
  | Itop : ival
  | Iint : bool -> Int_Modulus_Interval.t -> ival
  | Ilong : bool -> Int64_Modulus_Interval.t -> ival
  | Iundef : ival
  | Ibot : ival.
 
Inductive vmatch : val -> ival -> Prop :=
| vmatch_iitv : forall i b itv,
    Int_Modulus_Interval.zmatch (Int.unsigned i) itv ->
    vmatch (Vint i) (Iint b itv)
| vmatch_undef_iitv : forall itv,
    vmatch Vundef (Iint true itv)
| vmatch_litv : forall l b itv,
    Int64_Modulus_Interval.zmatch (Int64.unsigned l) itv ->
    vmatch (Vlong l) (Ilong b itv)
| vmatch_undef_litv : forall itv,
    vmatch Vundef (Ilong true itv)
| vmatch_undef: vmatch Vundef Iundef
| vmatch_top : forall v, vmatch v Itop.

Global Hint Constructors vmatch : ival.

Definition intconst i : ival :=
  Iint false ( Int_Modulus_Interval.intconst (Int.unsigned i)).

Lemma intconst_sound : forall i,
    vmatch (Vint i) (intconst i).
Proof.
  unfold intconst. constructor.
  replace (Int.unsigned i) with ((Int.unsigned i) mod Int.modulus) at 1.
  { apply Int_Modulus_Interval.zmatch_intconst. }
  apply Z.mod_small.
  apply Int.unsigned_range.
Qed.

Definition longconst i : ival :=
  Ilong false ( Int64_Modulus_Interval.intconst (Int64.unsigned i)).

Lemma longconst_sound : forall i,
    vmatch (Vlong i) (longconst i).
Proof.
  unfold intconst. constructor.
  replace (Int64.unsigned i) with ((Int64.unsigned i) mod Int64.modulus) at 1.
  { apply Int64_Modulus_Interval.zmatch_intconst. }
  apply Z.mod_small.
  apply Int64.unsigned_range.
Qed.
  
Definition add a1 a2 :=
  match a1, a2 with
  | Iint b1 i1, Iint b2 i2 => Iint (orb b1 b2) (Int_Modulus_Interval.add i1 i2)
  | _, _ => Itop
  end.

Lemma add_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.add v w) (add x y).
Proof.
  intros.
  inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  {
    unfold Int.add. rewrite Int.unsigned_repr_eq.
    apply Int_Modulus_Interval.zmatch_add; assumption.
  }
  { rewrite orb_true_r. constructor. }
  destruct y; constructor.
Qed.
  
Definition sub a1 a2 :=
  match a1, a2 with
  | Iint b1 i1, Iint b2 i2 => Iint (orb b1 b2) (Int_Modulus_Interval.sub i1 i2)
  | _, _ => Itop
  end.

Lemma sub_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.sub v w) (sub x y).
Proof.
  intros.
  inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  {
    unfold Int.sub. rewrite Int.unsigned_repr_eq.
    apply Int_Modulus_Interval.zmatch_sub; assumption.
  }
  { rewrite orb_true_r. constructor. }
  destruct y; constructor.
Qed.
  
Definition mul a1 a2 :=
  match a1, a2 with
  | Iint b1 i1, Iint b2 i2 => Iint (orb b1 b2) (Int_Modulus_Interval.mul i1 i2)
  | _, _ => Itop
  end.

Lemma mul_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.mul v w) (mul x y).
Proof.
  intros.
  inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  {
    unfold Int.mul. rewrite Int.unsigned_repr_eq.
    apply Int_Modulus_Interval.zmatch_mul; assumption.
  }
  { rewrite orb_true_r. constructor. }
  destruct y; constructor.
Qed.
  
Definition addl a1 a2 :=
  match a1, a2 with
  | Ilong b1 i1, Ilong b2 i2 => Ilong (orb b1 b2) (Int64_Modulus_Interval.add i1 i2)
  | _, _ => Itop
  end.

Lemma addl_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.addl v w) (addl x y).
Proof.
  intros.
  inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  {
    unfold Int64.add. rewrite Int64.unsigned_repr_eq.
    apply Int64_Modulus_Interval.zmatch_add; assumption.
  }
  { rewrite orb_true_r. constructor. }
  destruct y; constructor.
Qed.
  
Definition subl a1 a2 :=
  match a1, a2 with
  | Ilong b1 i1, Ilong b2 i2 => Ilong (orb b1 b2) (Int64_Modulus_Interval.sub i1 i2)
  | _, _ => Itop
  end.

Lemma subl_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.subl v w) (subl x y).
Proof.
  intros.
  inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  {
    unfold Int64.sub. rewrite Int64.unsigned_repr_eq.
    apply Int64_Modulus_Interval.zmatch_sub; assumption.
  }
  { rewrite orb_true_r. constructor. }
  destruct y; constructor.
Qed.
  
Definition mull a1 a2 :=
  match a1, a2 with
  | Ilong b1 i1, Ilong b2 i2 => Ilong (orb b1 b2) (Int64_Modulus_Interval.mul i1 i2)
  | _, _ => Itop
  end.

Lemma mull_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.mull v w) (mull x y).
Proof.
  intros.
  inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  {
    unfold Int64.mul. rewrite Int64.unsigned_repr_eq.
    apply Int64_Modulus_Interval.zmatch_mul; assumption.
  }
  { rewrite orb_true_r. constructor. }
  destruct y; constructor.
Qed.

Inductive ige : ival -> ival -> Prop :=
| Ige_int : forall b1 i1 b2 i2,
    Bool.le b2 b1 -> Int_Modulus_Interval.ge i1 i2 ->
    ige (Iint b1 i1) (Iint b2 i2)
| Ige_long : forall b1 i1 b2 i2,
    Bool.le b2 b1 -> Int64_Modulus_Interval.ge i1 i2 ->
    ige (Ilong b1 i1) (Ilong b2 i2)
| Ige_top : forall x, ige Itop x
| Ige_undef_int : forall i1, ige (Iint true i1) Iundef
| Ige_undef_long : forall i1, ige (Ilong true i1) Iundef
| Ige_undef : ige Iundef Iundef
| Ige_bot : forall x, ige x Ibot.

Lemma bool_le_refl: forall b, Bool.le b b.
Proof.
  destruct b; constructor.
Qed.

Lemma ige_refl: forall x, ige x x.
Proof.
  destruct x; constructor.
  - apply bool_le_refl.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - apply bool_le_refl.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
Qed.

Lemma bool_le_trans: forall b1 b2 b3,
    Bool.le b1 b2 -> Bool.le b2 b3 -> Bool.le b1 b3.
Proof.
  unfold Bool.le.
  intros.
  destruct b1, b2, b3; trivial.
Qed.

Lemma ige_trans: forall x y z, ige x y -> ige y z -> ige x z.
Proof.
  intros. inv H; inv H0; try constructor.
  - eapply bool_le_trans; eassumption.
  - eapply Int_Modulus_Interval.ge_trans; eassumption.
  - destruct b1. constructor. discriminate.
  - eapply bool_le_trans; eassumption.
  - eapply Int64_Modulus_Interval.ge_trans; eassumption.
  - destruct b1. constructor. discriminate.
Qed.

Definition ilub x y :=
  match x, y with
  | Ibot, x | x, Ibot => x
  | Iundef, (Iint b1 i1) | (Iint b1 i1), Iundef => Iint true i1
  | Iundef, Iundef => Iundef
  | Iundef, (Ilong b1 i1) => Ilong true i1
  | (Ilong b1 i1), Iundef => Ilong true i1
  | (Iint b1 i1), (Iint b2 i2) =>
      Iint (orb b1 b2) (Int_Modulus_Interval.lub i1 i2)
  | (Ilong b1 i1), (Ilong b2 i2) =>
      Ilong (orb b1 b2) (Int64_Modulus_Interval.lub i1 i2)
  | _, _ => Itop
  end.

Lemma orb_le1: forall b b0, Bool.le b (b || b0).
Proof.
  destruct b, b0; cbn; trivial.
Qed.

Lemma orb_le2: forall b b0, Bool.le b (b0 || b).
Proof.
  destruct b, b0; cbn; trivial.
Qed.

Lemma bool_le_true: forall b, Bool.le b true.
Proof.
  destruct b; cbn; trivial.
Qed.

Lemma ige_lub_left : forall x y,
    ige (ilub x y) x.
Proof.
  destruct x; destruct y; cbn; constructor.
  - apply orb_le1.
  - apply Int_Modulus_Interval.ge_lub_left.
  - apply bool_le_true.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - apply bool_le_refl.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - apply orb_le1.
  - apply Int64_Modulus_Interval.ge_lub_left.
  - apply bool_le_true.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
  - apply bool_le_refl.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
Qed.

Lemma ige_lub_right : forall x y,
    ige (ilub x y) y.
Proof.
  destruct x; destruct y; cbn; constructor.
  - apply orb_le2.
  - apply Int_Modulus_Interval.ge_lub_right.
  - apply orb_le2.
  - apply Int64_Modulus_Interval.ge_lub_right.
  - apply bool_le_true.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - apply bool_le_true.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
  - apply bool_le_refl.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - apply bool_le_refl.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
Qed.

Lemma bool_le_least:
  forall b1 b2 b3,
    Bool.le b2 b1 -> Bool.le b3 b1 -> Bool.le (b2 || b3) b1.
Proof.
  unfold Bool.le.
  destruct b1, b2, b3; cbn; trivial.
Qed.

Lemma ilub_least:
  forall r p q, ige r p -> ige r q -> ige r (ilub p q).
Proof.
  intros. inv H; inv H0; try constructor; cbn;
            auto using Int_Modulus_Interval.lub_least,
            Int64_Modulus_Interval.lub_least, bool_le_least.
Qed.

Definition ieq_dec (x y : ival) : {x=y} + {x<>y}.
Proof.
  generalize Int_Modulus_Interval.eq_dec.
  generalize Int64_Modulus_Interval.eq_dec.
  generalize bool_dec.
  decide equality.
Qed.

Definition widen_down' z1 z2 :=
  if Z.eq_dec z1 z2 then z1 else 0.

Definition widen_down z1 z2 :=
  widen_down' z1 (Z.min z1 z2).

Fixpoint find_first {T: Type} (P : T->bool) l last_resort :=
  match l with
  | h::t => if P h then h else find_first P t last_resort
  | nil => last_resort
  end.

Lemma find_first_P: forall {T: Type} (P P': T->bool) l last_resort
  (ALL: List.forallb P l = true) (Plast: P last_resort = true),
    P(find_first P' l last_resort) = true.
Proof.
  induction l; cbn. { auto. }
  intros. rewrite andb_true_iff in ALL. destruct ALL.
  destruct (P' a); auto.
Qed.

Lemma find_first_P2: forall {T: Type} (P : T->bool) l last_resort
    (Plast: P last_resort = true),
    P(find_first P l last_resort) = true.
Proof.
  induction l; cbn. { auto. } intros.
  destruct (P a) eqn:DEC; auto.
Qed.

Definition find_in_ramp ramp z last_resort :=
  find_first (fun x => z <=? x) ramp last_resort.

Definition widen_up' z1 z2 (ramp : list Z.t) last_resort :=
  if Z.eq_dec z1 z2 then z1 else find_in_ramp ramp z2 last_resort.

Definition widen_up z1 z2 ramp last_resort :=
  widen_up' z1 (Z.max z1 z2) ramp last_resort.

Definition int_ramp := 0 :: 1 :: 2147483646 :: 2147483647 ::
                         4294967294 :: nil.

Program Definition int_widen i i0 :=
  Int_Modulus_Interval.mkmod_interval
    (Interval.mkinterval
       (widen_down i.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo)
                   i0.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo))
       (widen_up i.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi)
                   i0.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi)
                   int_ramp
                   Int.max_unsigned) _)
    _ _.
Next Obligation.
  destruct i, i0, mod_itv, mod_itv0; cbn in *.
  assert (widen_down itv_lo itv_lo0 <= Z.min itv_lo itv_lo0).
  { unfold widen_down, widen_down'.
    destruct Z.eq_dec; lia.
  }
  assert (Z.max itv_hi itv_hi0 <= widen_up itv_hi itv_hi0 int_ramp 4294967295).
  { unfold widen_up, widen_up'.
    destruct Z.eq_dec. lia.
    apply Z.leb_le.
    apply find_first_P2 with (P := fun x => Z.max itv_hi itv_hi0 <=? x).
    change Int.modulus with 4294967296 in *.
    lia.
  }
  lia.
Qed.

Next Obligation.
  destruct i, i0, mod_itv, mod_itv0; cbn in *.
  unfold widen_down, widen_down'.
  destruct Z.eq_dec; lia.
Qed.
Next Obligation.
  destruct i, i0, mod_itv, mod_itv0; cbn in *.
  unfold widen_up, widen_up'.
  destruct Z.eq_dec. lia.
  unfold find_in_ramp.
  apply find_first_P with (P := fun z => z <? Int.modulus); reflexivity.
Qed.

Lemma ge_int_widen_left: forall i i0,
    Int_Modulus_Interval.ge (int_widen i i0) i.
Proof.
  unfold int_widen.
  destruct i, i0, mod_itv, mod_itv0.
  constructor; cbn in *.
  - unfold widen_down, widen_down'.
    destruct Z.eq_dec; lia.
  - unfold widen_up, widen_up'.
    destruct Z.eq_dec. lia.
    unfold find_in_ramp.
    assert ((fun x : Z => Z.max itv_hi itv_hi0 <=? x)
              (find_first (fun x : Z => Z.max itv_hi itv_hi0 <=? x) int_ramp 4294967295) = true) as LEQ.
    { apply find_first_P2.
      change Int.modulus with 4294967296 in *. lia. }
    cbn beta in LEQ.
    lia.
Qed.

Lemma ge_int_widen_right: forall i i0,
    Int_Modulus_Interval.ge (int_widen i i0) i0.
Proof.
  unfold int_widen.
  destruct i, i0, mod_itv, mod_itv0.
  constructor; cbn in *.
  - unfold widen_down, widen_down'.
    destruct Z.eq_dec; lia.
  - unfold widen_up, widen_up'.
    destruct Z.eq_dec. lia.
    unfold find_in_ramp.
    assert ((fun x : Z => Z.max itv_hi itv_hi0 <=? x)
              (find_first (fun x : Z => Z.max itv_hi itv_hi0 <=? x) int_ramp 4294967295) = true) as LEQ.
    { apply find_first_P2.
      change Int.modulus with 4294967296 in *. lia. }
    cbn beta in LEQ.
    lia.
Qed.

Definition long_ramp := 0 :: 1 :: 2147483646 :: 2147483647 ::
                          4294967294 :: 4294967295 ::
                          9223372036854775806 :: 9223372036854775807 ::
   18446744073709551614 :: nil.

Program Definition long_widen i i0 :=
  Int64_Modulus_Interval.mkmod_interval
    (Interval.mkinterval
       (widen_down i.(Int64_Modulus_Interval.mod_itv).(Interval.itv_lo)
                   i0.(Int64_Modulus_Interval.mod_itv).(Interval.itv_lo))
       (widen_up i.(Int64_Modulus_Interval.mod_itv).(Interval.itv_hi)
                   i0.(Int64_Modulus_Interval.mod_itv).(Interval.itv_hi)
                   long_ramp
                   Int64.max_unsigned) _)
    _ _.
Next Obligation.
  destruct i, i0, mod_itv, mod_itv0; cbn in *.
  assert (widen_down itv_lo itv_lo0 <= Z.min itv_lo itv_lo0).
  { unfold widen_down, widen_down'.
    destruct Z.eq_dec; lia.
  }
  assert (Z.max itv_hi itv_hi0 <= widen_up itv_hi itv_hi0 long_ramp 18446744073709551615).
  { unfold widen_up, widen_up'.
    destruct Z.eq_dec. lia.
    apply Z.leb_le.
    apply find_first_P2 with (P := fun x => Z.max itv_hi itv_hi0 <=? x).
    change Int64.modulus with 18446744073709551616 in *.
    lia.
  }
  lia.
Qed.

Next Obligation.
  destruct i, i0, mod_itv, mod_itv0; cbn in *.
  unfold widen_down, widen_down'.
  destruct Z.eq_dec; lia.
Qed.
Next Obligation.
  destruct i, i0, mod_itv, mod_itv0; cbn in *.
  unfold widen_up, widen_up'.
  destruct Z.eq_dec. lia.
  unfold find_in_ramp.
  apply find_first_P with (P := fun z => z <? Int64.modulus); reflexivity.
Qed.

Lemma ge_long_widen_left: forall i i0,
    Int64_Modulus_Interval.ge (long_widen i i0) i.
Proof.
  unfold int_widen.
  destruct i, i0, mod_itv, mod_itv0.
  constructor; cbn in *.
  - unfold widen_down, widen_down'.
    destruct Z.eq_dec; lia.
  - unfold widen_up, widen_up'.
    destruct Z.eq_dec. lia.
    unfold find_in_ramp.
    assert ((fun x : Z => Z.max itv_hi itv_hi0 <=? x)
              (find_first (fun x : Z => Z.max itv_hi itv_hi0 <=? x) long_ramp 18446744073709551615) = true) as LEQ.
    { apply find_first_P2.
      change Int64.modulus with 18446744073709551616 in *. lia. }
    cbn beta in LEQ.
    lia.
Qed.

Lemma ge_long_widen_right: forall i i0,
    Int64_Modulus_Interval.ge (long_widen i i0) i0.
  unfold int_widen.
  destruct i, i0, mod_itv, mod_itv0.
  constructor; cbn in *.
  - unfold widen_down, widen_down'.
    destruct Z.eq_dec; lia.
  - unfold widen_up, widen_up'.
    destruct Z.eq_dec. lia.
    unfold find_in_ramp.
    assert ((fun x : Z => Z.max itv_hi itv_hi0 <=? x)
              (find_first (fun x : Z => Z.max itv_hi itv_hi0 <=? x) long_ramp 18446744073709551615) = true) as LEQ.
    { apply find_first_P2.
      change Int64.modulus with 18446744073709551616 in *. lia. }
    cbn beta in LEQ.
    lia.
Qed.

Definition iwiden x y :=
  match x, y with
  | Ibot, x | x, Ibot => x
  | (Iint b1 i1), (Iint b2 i2) => Iint (orb b1 b2) (int_widen i1 i2)
  | (Ilong b1 i1), (Ilong b2 i2) => Ilong (orb b1 b2) (long_widen i1 i2)
  | _, _ => Itop
  end.
       
Lemma ige_widen_left :
  forall x y, ige (iwiden x y) x.
Proof.
  destruct x, y; try constructor.
  - apply orb_le1.
  - apply ge_int_widen_left.
  - apply bool_le_refl.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - apply orb_le1.
  - apply ge_long_widen_left.
  - apply bool_le_refl.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
Qed.
  
Lemma ige_widen_right :
  forall x y, ige (iwiden x y) y.
Proof.
  destruct x, y; try constructor.
  - apply orb_le2.
  - apply ge_int_widen_right.
  - apply orb_le2.
  - apply ge_long_widen_right.
  - apply bool_le_refl.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - apply bool_le_refl.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
Qed.

Definition iglb x y :=
  match x, y with
  | Itop, x | x, Itop => x
  | (Iint b1 i1), (Iint b2 i2) =>
      match Int_Modulus_Interval.glb_nb i1 i2 with
      | Some z => Iint (andb b1 b2) z
      | None => if andb b1 b2 then Iundef else Ibot
      end
  | (Ilong b1 i1), (Ilong b2 i2) =>
      match Int64_Modulus_Interval.glb_nb i1 i2 with
      | Some z => Ilong (andb b1 b2) z
      | None => if andb b1 b2 then Iundef else Ibot
      end
  | ((Iint true _) | (Ilong true _)), Iundef
  | Iundef, ((Iint true _) | (Ilong true _))
  | (Iint true _), (Ilong true _)
  | (Ilong true _), (Iint true _)
  | Iundef, Iundef => Iundef
  | _, _ => Ibot
  end.

Lemma ige_glb_left : forall x y,
    ige x (iglb x y).
Proof.
  destruct x, y; cbn; try rewrite if_same; try constructor.
  - apply bool_le_refl.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - pose proof (Int_Modulus_Interval_Bot.ge_glb_nb_left t t0).
    change Int_Modulus_Interval_Bot.ModInt.glb_nb with
      Int_Modulus_Interval.glb_nb in *.
    destruct Int_Modulus_Interval.glb_nb; try constructor; try
                                                             assumption; destruct b, b0; try constructor.
  - destruct b, b0; constructor.
  - destruct b; constructor.
  - apply bool_le_refl.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
  - destruct b, b0; constructor.
  - pose proof (Int64_Modulus_Interval_Bot.ge_glb_nb_left t t0).
    change Int64_Modulus_Interval_Bot.ModInt.glb_nb with
      Int64_Modulus_Interval.glb_nb in *.
    destruct Int64_Modulus_Interval.glb_nb; try constructor; try
                                                               assumption; destruct b, b0; constructor.
  - destruct b; constructor.
  - destruct b; constructor.
  - destruct b; constructor.
Qed.

Lemma ige_glb_right : forall x y,
    ige y (iglb x y).
Proof.
  destruct x, y; cbn; try rewrite if_same; try constructor.
  - apply bool_le_refl.
  - apply Int_Modulus_Interval.ge_refl. constructor.
  - apply bool_le_refl.
  - apply Int64_Modulus_Interval.ge_refl. constructor.
  - pose proof (Int_Modulus_Interval_Bot.ge_glb_nb_right t t0).
    change Int_Modulus_Interval_Bot.ModInt.glb_nb with
      Int_Modulus_Interval.glb_nb in *.
    destruct Int_Modulus_Interval.glb_nb; try constructor; try
                                                             assumption; destruct b, b0; constructor.
  - destruct b, b0; constructor.
  - destruct b; constructor.
  - destruct b, b0; constructor.
  - pose proof (Int64_Modulus_Interval_Bot.ge_glb_nb_right t t0).
    change Int64_Modulus_Interval_Bot.ModInt.glb_nb with
      Int64_Modulus_Interval.glb_nb in *.
    destruct Int64_Modulus_Interval.glb_nb; try constructor; try
                                                               assumption; destruct b, b0; constructor.
  - destruct b; constructor.
  - destruct b; constructor.
  - destruct b; constructor.
Qed.

Lemma andb_le1:
  forall b0 b1 b2,
    Bool.le b2 b1 -> Bool.le b2 b0 -> Bool.le b2 (b1 && b0).
Proof.
  destruct b0, b1, b2; cbn; trivial.
Qed.

Lemma andb_le2:
  forall b0 b1 b2,
    Bool.le b2 b1 -> Bool.le b2 b0 -> Bool.le b2 (b0 && b1).
Proof.
  destruct b0, b1, b2; cbn; trivial.
Qed.

Lemma iglb_greatest:
  forall r p q, ige p r -> ige q r -> ige (iglb p q) r.
Proof.
  intros. inv H; inv H0; cbn; try rewrite if_same; try constructor; trivial.
  - pose proof (Int_Modulus_Interval_Bot.glb_greatest (Some i2) (Some i1) (Some i0) H2 H6).
    unfold Int_Modulus_Interval_Bot.glb in *.
    change Int_Modulus_Interval_Bot.ModInt.glb_nb
      with Int_Modulus_Interval.glb_nb in H.
    destruct Int_Modulus_Interval.glb_nb.
    + constructor. apply andb_le1; assumption. assumption.
    + inv H.
 - pose proof (Int64_Modulus_Interval_Bot.glb_greatest (Some i2) (Some i1) (Some i0) H2 H6).
    unfold Int64_Modulus_Interval_Bot.glb in *.
    change Int64_Modulus_Interval_Bot.ModInt.glb_nb
      with Int64_Modulus_Interval.glb_nb in H.
    destruct Int64_Modulus_Interval.glb_nb.
    + constructor. apply andb_le2; assumption. assumption.
    + inv H.
 - destruct Int_Modulus_Interval.glb_nb; constructor.
 - destruct Int64_Modulus_Interval.glb_nb; constructor.
Qed.
  
Lemma vmatch_ge:
  forall v x y, ige x y -> vmatch v y -> vmatch v x.
Proof.
  intros. inv H; inv H0; try constructor.
  - eapply Int_Modulus_Interval.zmatch_ge; eassumption.
  - destruct b1. constructor. discriminate.
  - eapply Int64_Modulus_Interval.zmatch_ge; eassumption.
  - destruct b1. constructor. discriminate.
Qed.

Lemma vmatch_glb:
  forall v a1 a2
    (MATCH1 : vmatch v a1)
    (MATCH2 : vmatch v a2),
    vmatch v (iglb a1 a2).
Proof.
  intros. inv MATCH1; inv MATCH2; cbn; try rewrite if_same; try constructor; trivial.
  - destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned i) itv itv0 H H1) as [c [RE MATCH]].
    rewrite RE. constructor. assumption.
  - destruct Int_Modulus_Interval.glb_nb ; constructor.
  - destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned l) itv itv0 H H1) as [c [RE MATCH]].
    rewrite RE. constructor. assumption.
  - destruct Int64_Modulus_Interval.glb_nb ; constructor.
Qed.

Module AVal <: SEMILATTICE_WITH_TOP.

  Definition t := ival.
  Definition eq (x y: t) := (x = y).
  Definition eq_refl: forall x, eq x x := (@eq_refl t).
  Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t).
  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t).
  Definition eq_dec := ieq_dec.
    
  Definition beq (x y: t) : bool := if eq_dec x y then true else false.
  Lemma beq_correct: forall x y, beq x y = true -> eq x y.
  Proof.
    unfold beq, eq.
    intros.
    destruct eq_dec; congruence.
  Qed.

  Definition ge := ige.
  Lemma ge_refl : forall x y : t, eq x y -> ge x y.
  Proof.
    unfold eq, ge.
    intros. subst. apply ige_refl.
  Qed.
  
  Definition ge_trans := ige_trans.

  Definition lub := ilub.
  Definition ge_lub_left := ige_lub_left.
  Definition ge_lub_right := ige_lub_right.

  Definition widen := iwiden.
  Definition ge_widen_left := ige_widen_left.
  Definition ge_widen_right := ige_widen_right.

  Definition bot := Ibot.

  Lemma ge_bot: forall x, ge x bot.
  Proof.
    intro. constructor.
  Qed.

  Definition top := Itop.

  Lemma ge_top: forall x, ge top x.
  Proof.
    intro. constructor.
  Qed.
End AVal.

Lemma zmatch_intconst:
 forall n,
   Int_Modulus_Interval.zmatch (Int.unsigned n)
     (Int_Modulus_Interval.intconst (Int.unsigned n)).
Proof.
  intro.
  pose proof (Int_Modulus_Interval.zmatch_intconst (Int.unsigned n)).
  rewrite Zmod_small in H. assumption.
  apply Int.unsigned_range.
Qed.

Lemma zmatch_longconst:
 forall n,
   Int64_Modulus_Interval.zmatch (Int64.unsigned n)
     (Int64_Modulus_Interval.intconst (Int64.unsigned n)).
Proof.
  intro.
  pose proof (Int64_Modulus_Interval.zmatch_intconst (Int64.unsigned n)).
  rewrite Zmod_small in H. assumption.
  apply Int64.unsigned_range.
Qed.


Definition filter_Vint (a : ival) : option Int_Modulus_Interval.t :=
  match a with
  | Ibot => None
  | Iint false i => Some i
  | _ => Some Int_Modulus_Interval.full_range
  end.

Lemma zmatch_int_full_range i:
  Int_Modulus_Interval.zmatch (Int.unsigned i) Int_Modulus_Interval.full_range.
Proof.
  apply Int_Modulus_Interval.zmatch_full_range. apply Int.unsigned_range.
Qed.

Lemma zmatch_int64_full_range i:
  Int64_Modulus_Interval.zmatch (Int64.unsigned i) Int64_Modulus_Interval.full_range.
Proof.
  apply Int64_Modulus_Interval.zmatch_full_range. apply Int64.unsigned_range.
Qed.

Lemma if_both_Some:
  forall {A : Type} (b : bool) (x y : A),
    (if b then Some x else Some y) = Some (if b then x else y).
Proof.
  destruct b; reflexivity.
Qed.

Lemma filter_Vint_sound (i : int) (a : ival):
  vmatch (Vint i) a ->
  exists ai,
    filter_Vint a = Some ai /\ vmatch (Vint i) (Iint false ai).
Proof.
  inversion 1; simpl; subst.
  { rewrite if_both_Some.
    eexists; split. reflexivity.
    constructor. destruct b. { apply zmatch_int_full_range. }
    assumption.
  }
  eexists; split. reflexivity. constructor. apply zmatch_int_full_range.
Qed.

Definition filter_cmpu_Iint (cmp : comparison) (i0 i1 : Int_Modulus_Interval.t) : ival * ival :=
  match cmp with
  | Cle =>
      match Int_Modulus_Interval.filter_less_equal i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  | Cge =>
      match Int_Modulus_Interval.filter_greater_equal i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  | Clt =>
      match Int_Modulus_Interval.filter_less i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  | Cgt =>
      match Int_Modulus_Interval.filter_greater i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  | Ceq =>
      match Int_Modulus_Interval.glb_nb i0 i1 with
      | Some i' => ((Iint false i'), (Iint false i'))
      | None => (Ibot, Ibot)
      end
  | Cne =>
      match Int_Modulus_Interval.filter_not_equal i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  end.

Lemma filter_cmpu_Iint_sound cmp i0 i1 (x0 x1 : int)
  (Z0 : Int_Modulus_Interval.zmatch (Int.unsigned x0) i0)
  (Z1 : Int_Modulus_Interval.zmatch (Int.unsigned x1) i1)
  (CMP : Int.cmpu cmp x0 x1 = true):
  let (a0', a1') := filter_cmpu_Iint cmp i0 i1 in
  vmatch (Vint x0) a0' /\ vmatch (Vint x1) a1'.
Proof.
  Local Ltac slv := split; constructor; assumption.
  destruct cmp; simpl in *;
    first [ apply proj_sumbool_true in CMP as CMP'
          | apply negb_true_iff in CMP as CMP'; apply proj_sumbool_false in CMP' ].
  - rewrite (Int.same_if_eq _ _ CMP) in *.
    destruct (Int_Modulus_Interval.zmatch_glb_nb _ _ _ Z0 Z1)
      as (c & -> & MATCH).
    slv.
  - destruct (Int_Modulus_Interval.zmatch_filter_not_equal _ _ _ _ Z0 Z1 CMP')
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (Int_Modulus_Interval.zmatch_filter_less _ _ _ _ Z0 Z1 CMP')
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - apply Z.ge_le in CMP'.
    destruct (Int_Modulus_Interval.zmatch_filter_less_equal _ _ _ _ Z0 Z1 CMP')
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - apply Z.lt_gt in CMP'.
    destruct (Int_Modulus_Interval.zmatch_filter_greater _ _ _ _ Z0 Z1 CMP')
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (Int_Modulus_Interval.zmatch_filter_greater_equal _ _ _ _ Z0 Z1 CMP')
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
Qed.


Definition filter_cmpu (cmp : comparison) (a0 a1 : ival) : ival*ival :=
  if Archi.ptr64
  then
    match filter_Vint a0, filter_Vint a1 with
    | Some i0, Some i1 => filter_cmpu_Iint cmp i0 i1
    | _, _ => (Ibot, Ibot)
    end
  else
  match a0, a1 with
  | (Iint b0 i0), (Iint b1 i1) => filter_cmpu_Iint cmp i0 i1
  | (Iint b0 i0), _ =>
      match cmp with
      | Cle =>
          match Int_Modulus_Interval.filter_less_equal i0 Int_Modulus_Interval.full_range with
          | Some(i0', _) => ((Iint false i0'), a1)
          | None => (Ibot, Ibot)
          end
      | Cge =>
          match Int_Modulus_Interval.filter_greater_equal i0 Int_Modulus_Interval.full_range with
          | Some(i0', _) => ((Iint false i0'), a1)
          | None => (Ibot, Ibot)
          end
      | Clt =>
          match Int_Modulus_Interval.filter_less i0 Int_Modulus_Interval.full_range with
          | Some(i0', _) => ((Iint false i0'), a1)
          | None => (Ibot, Ibot)
          end
      | Cgt =>
          match Int_Modulus_Interval.filter_greater i0 Int_Modulus_Interval.full_range with
          | Some(i0', _) => ((Iint false i0'), a1)
          | None => (Ibot, Ibot)
          end
      | Ceq => (a0, a0)
      | Cne => (a0, a1)
      end
  | _, (Iint b1 i1) =>
      match cmp with
      | Cle =>
          match Int_Modulus_Interval.filter_less_equal Int_Modulus_Interval.full_range i1 with
          | Some(_, i1') => (a0, (Iint false i1'))
          | None => (Ibot, Ibot)
          end
      | Cge =>
          match Int_Modulus_Interval.filter_greater_equal Int_Modulus_Interval.full_range i1 with
          | Some(_, i1') => (a0, (Iint false i1'))
          | None => (Ibot, Ibot)
          end
      | Clt =>
          match Int_Modulus_Interval.filter_less Int_Modulus_Interval.full_range i1 with
          | Some(_, i1') => (a0, (Iint false i1'))
          | None => (Ibot, Ibot)
          end
      | Cgt =>
          match Int_Modulus_Interval.filter_greater Int_Modulus_Interval.full_range i1 with
          | Some(_, i1') => (a0, (Iint false i1'))
          | None => (Ibot, Ibot)
          end
      | Ceq => (a1, a1)
      | Cne => (a0, a1)
      end
  | _, _ => (a0, a1)
  end.

Lemma bad_test: forall (x : bool) (P: Prop),
    (if negb Archi.ptr64 then None else if x then Some false else None) = Some true -> P.
Proof.
  destruct Archi.ptr64, x; discriminate.
Qed.

Lemma bad_test2: forall (x : bool) (P: Prop),
    (if negb Archi.ptr64 then None else if x then None else None) = Some true -> P.
Proof.
  destruct Archi.ptr64, x; discriminate.
Qed.

Lemma bad_test3: forall (x : bool) (P: Prop),
    (if Archi.ptr64 then None else if x then Some false else None) = Some true -> P.
Proof.
  intros.
  destruct Archi.ptr64, x; discriminate.
Qed.

Lemma bad_test4: forall (x : bool) (P: Prop),
    (if Archi.ptr64 then None else if x then None else None) = Some true -> P.
Proof.
  intros.
  destruct Archi.ptr64, x; discriminate.
Qed.

Lemma filter_cmpu_sound mb (cmp : comparison)
  (a0 a1 : ival) (x0 x1 : val)
  (MATCH0 : vmatch x0 a0) (MATCH1 : vmatch x1 a1)
  (CMP : (Val.cmpu_bool mb cmp x0 x1) = Some true):
  let (a0', a1') := filter_cmpu cmp a0 a1 in
  vmatch x0 a0' /\ vmatch x1 a1'.
Proof.
  unfold filter_cmpu.
  case Archi.ptr64 eqn:A64. {
    assert (exists xi0 xi1, x0 = Vint xi0 /\ x1 = Vint xi1) as (xi0 & xi1 & ? & ?). {
      revert CMP; unfold Val.cmpu_bool; rewrite A64.
      destruct x0; try discriminate 1;
      destruct x1; try discriminate 1.
      repeat econstructor.
    }
    subst.
    apply filter_Vint_sound in MATCH0 as (i0 & -> & MATCH0),
                               MATCH1 as (i1 & -> & MATCH1).
    inv MATCH0; inv MATCH1; injection CMP as ?.
    eapply filter_cmpu_Iint_sound; eauto.
  }
  clear A64.
  inv MATCH0; inv MATCH1; cbn in *; try discriminate.
  all: try solve [split; constructor; auto].
  { injection CMP as ?; eapply filter_cmpu_Iint_sound; eauto. }
  {
    destruct cmp; destruct x1; inv CMP.
    all:try solve [ split; constructor; eassumption
                  | eapply bad_test3; eassumption
                  | eapply bad_test4; eassumption ].
    2-5:pose proof (H0 := zmatch_int_full_range i0).

    - pose proof (Int.same_if_eq _ _ H1). subst.
      split ; constructor; assumption.
  - unfold Int.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int_Modulus_Interval.zmatch_filter_less _ _ _ _ H H0 CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int.unsigned i <= Int.unsigned i0) as CMP' by lia.
    destruct (Int_Modulus_Interval.zmatch_filter_less_equal _ _ _ _ H H0 CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  - unfold Int.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int.unsigned i > Int.unsigned i0) as CMP' by lia.
    destruct (Int_Modulus_Interval.zmatch_filter_greater _ _ _ _ H H0 CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int_Modulus_Interval.zmatch_filter_greater_equal _ _ _ _ H H0 CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  }
  {
    destruct cmp; destruct x0; inv CMP.
    all: try solve [ split; constructor; eassumption
                   | eapply bad_test3; eassumption
                   | eapply bad_test4; eassumption ].
    2-5:pose proof (H0 := zmatch_int_full_range i0).

  - pose proof (Int.same_if_eq _ _ H1). subst.
      split ; constructor; assumption.
  - unfold Int.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int_Modulus_Interval.zmatch_filter_less _ _ _ _ H0 H CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int.unsigned i0 <= Int.unsigned i) as CMP' by lia.
    destruct (Int_Modulus_Interval.zmatch_filter_less_equal _ _ _ _ H0 H CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  - unfold Int.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int.unsigned i0 > Int.unsigned i) as CMP' by lia.
    destruct (Int_Modulus_Interval.zmatch_filter_greater _ _ _ _ H0 H CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int_Modulus_Interval.zmatch_filter_greater_equal _ _ _ _ H0 H CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  }
  { unfold Val.cmpu_bool in CMP. destruct x0; discriminate. }
Qed.

Definition cmpu_bool (cmp : comparison)
           (a0 a1 : ival) : ibool :=
  match a0, a1 with
  | (Iint false i0), (Iint false i1) =>
      match cmp with
      | Cle =>
          Int_Modulus_Interval.filter_to_eval
            Int_Modulus_Interval.filter_less_equal
            Int_Modulus_Interval.filter_greater i0 i1
      | Cge =>
          Int_Modulus_Interval.filter_to_eval
            Int_Modulus_Interval.filter_greater_equal
            Int_Modulus_Interval.filter_less i0 i1
      | Clt =>
          Int_Modulus_Interval.filter_to_eval
            Int_Modulus_Interval.filter_less
            Int_Modulus_Interval.filter_greater_equal i0 i1
      | Cgt =>
          Int_Modulus_Interval.filter_to_eval
            Int_Modulus_Interval.filter_greater
            Int_Modulus_Interval.filter_less_equal i0 i1
      | Ceq =>
          Int_Modulus_Interval.filter_to_eval
            Int_Modulus_Interval.filter_equal
            Int_Modulus_Interval.filter_not_equal i0 i1
      | Cne =>
          Int_Modulus_Interval.filter_to_eval
            Int_Modulus_Interval.filter_not_equal
            Int_Modulus_Interval.filter_equal
            i0 i1
      end
  | _, _ => Btop
  end.

Lemma cmpu_bool_sound:
  forall valid c v w x y, vmatch v x -> vmatch w y ->
    cmatch (Val.cmpu_bool valid c v w) (cmpu_bool c x y).
Proof.
  intros. unfold Val.cmpu_bool, cmpu_bool.
  inv H; try constructor; inv H0; try rewrite if_same; try constructor.
  destruct c; cbn; destruct b; try constructor; destruct b0; try constructor.
  - change (Int.eq i i0) with ((fun x y => if zeq x y then true else false) (Int.unsigned i) (Int.unsigned i0)).
    apply Int_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int_Modulus_Interval.zmatch_filter_equal; auto.
      destruct zeq; congruence.
    + intros. apply Int_Modulus_Interval.zmatch_filter_not_equal; auto.
      destruct zeq; congruence.
 - change (negb (Int.eq i i0)) with ((fun x y => negb (if zeq x y then true else false)) (Int.unsigned i) (Int.unsigned i0)).
   apply Int_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int_Modulus_Interval.zmatch_filter_not_equal; auto.
      destruct zeq; cbn in CMP; congruence.
    + intros. apply Int_Modulus_Interval.zmatch_filter_equal; auto.
      destruct zeq; cbn in CMP; congruence.
 - change (Int.ltu i i0) with ((fun x y => if zlt x y then true else false) (Int.unsigned i) (Int.unsigned i0)).
    apply Int_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int_Modulus_Interval.zmatch_filter_less; auto.
      destruct zlt; congruence.
    + intros. apply Int_Modulus_Interval.zmatch_filter_greater_equal; auto.
      destruct zlt; lia.
 - change (negb (Int.ltu i0 i)) with ((fun x y => negb (if zlt y x then true else false)) (Int.unsigned i) (Int.unsigned i0)).
    apply Int_Modulus_Interval.filter_to_eval_sound; trivial.
   + intros. apply Int_Modulus_Interval.zmatch_filter_less_equal; auto.
     destruct zlt; lia.
   + intros. apply Int_Modulus_Interval.zmatch_filter_greater; auto.
     destruct zlt; lia.
 - change (Int.ltu i0 i) with ((fun x y => (if zlt y x then true else false)) (Int.unsigned i) (Int.unsigned i0)).
    apply Int_Modulus_Interval.filter_to_eval_sound; trivial.
   + intros. apply Int_Modulus_Interval.zmatch_filter_greater; auto.
     destruct zlt; lia.
   + intros. apply Int_Modulus_Interval.zmatch_filter_less_equal; auto.
     destruct zlt; lia.
 - change (negb (Int.ltu i i0)) with ((fun x y => negb (if zlt x y then true else false)) (Int.unsigned i) (Int.unsigned i0)).
    apply Int_Modulus_Interval.filter_to_eval_sound; trivial.
   + intros. apply Int_Modulus_Interval.zmatch_filter_greater_equal; auto.
     destruct zlt; lia.
   + intros. apply Int_Modulus_Interval.zmatch_filter_less; auto.
     destruct zlt; lia.
Qed.

Definition filter_cmplu (cmp : comparison)
           (a0 a1 : ival) : ival*ival :=
  match a0, a1 with
  | (Ilong b0 i0), (Ilong b1 i1) =>
      match cmp with
      | Cle =>
          match Int64_Modulus_Interval.filter_less_equal i0 i1 with
          | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      | Cge =>
          match Int64_Modulus_Interval.filter_greater_equal i0 i1 with
          | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      | Clt =>
          match Int64_Modulus_Interval.filter_less i0 i1 with
          | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      | Cgt =>
          match Int64_Modulus_Interval.filter_greater i0 i1 with
          | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      | Ceq =>
          match Int64_Modulus_Interval.glb_nb i0 i1 with
          | Some i' => ((Ilong false i'), (Ilong false i'))
          | None => (Ibot, Ibot)
          end
      | Cne =>
          match Int64_Modulus_Interval.filter_not_equal i0 i1 with
          | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      end
  | (Ilong b0 i0), _ =>
      match cmp with
      | Cle =>
          match Int64_Modulus_Interval.filter_less_equal i0 Int64_Modulus_Interval.full_range with
          | Some(i0', _) => ((Ilong false i0'), a1)
          | None => (Ibot, Ibot)
          end
      | Cge =>
          match Int64_Modulus_Interval.filter_greater_equal i0 Int64_Modulus_Interval.full_range with
          | Some(i0', _) => ((Ilong false i0'), a1)
          | None => (Ibot, Ibot)
          end
      | Clt =>
          match Int64_Modulus_Interval.filter_less i0 Int64_Modulus_Interval.full_range with
          | Some(i0', _) => ((Ilong false i0'), a1)
          | None => (Ibot, Ibot)
          end
      | Cgt =>
          match Int64_Modulus_Interval.filter_greater i0 Int64_Modulus_Interval.full_range with
          | Some(i0', _) => ((Ilong false i0'), a1)
          | None => (Ibot, Ibot)
          end
      | Ceq => (a0, a0)
      | Cne => (a0, a1)
      end
  | _, (Ilong b1 i1) =>
      match cmp with
      | Cle =>
          match Int64_Modulus_Interval.filter_less_equal Int64_Modulus_Interval.full_range i1 with
          | Some(_, i1') => (a0, (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      | Cge =>
          match Int64_Modulus_Interval.filter_greater_equal Int64_Modulus_Interval.full_range i1 with
          | Some(_, i1') => (a0, (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      | Clt =>
          match Int64_Modulus_Interval.filter_less Int64_Modulus_Interval.full_range i1 with
          | Some(_, i1') => (a0, (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      | Cgt =>
          match Int64_Modulus_Interval.filter_greater Int64_Modulus_Interval.full_range i1 with
          | Some(_, i1') => (a0, (Ilong false i1'))
          | None => (Ibot, Ibot)
          end
      | Ceq => (a1, a1)
      | Cne => (a0, a1)
      end
  | _, _ => (a0, a1)
  end.

Lemma filter_cmplu_sound:
  forall mb (cmp : comparison)
         (a0 a1 : ival) (x0 x1 : val)
         (MATCH0 : vmatch x0 a0) (MATCH1 : vmatch x1 a1)
         (CMP : (Val.cmplu_bool mb cmp x0 x1) = Some true),
    let (a0', a1') := filter_cmplu cmp a0 a1 in
    vmatch x0 a0' /\ vmatch x1 a1'.
Proof.
  intros. inv MATCH0; inv MATCH1; cbn in *; try discriminate.
  all: try solve [split; constructor; auto].
  {
  destruct cmp; inv CMP.
  - rewrite (Int64.same_if_eq _ _ H2) in *.
    destruct (Int64_Modulus_Interval.zmatch_glb_nb _ _ _ H H0)
      as (c & RE & MATCH).
    rewrite RE. split; constructor; assumption.
  - unfold Int64.eq in H2. destruct zeq as [EQ | NEQ]. discriminate.
    assert (Int64.unsigned l <> Int64.unsigned l0) as NEQ' by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_not_equal _ _ _ _ H H0 NEQ')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int64_Modulus_Interval.zmatch_filter_less _ _ _ _ H H0 CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int64.unsigned l <= Int64.unsigned l0) as CMP' by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_less_equal _ _ _ _ H H0 CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int64.unsigned l > Int64.unsigned l0) as CMP' by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_greater _ _ _ _ H H0 CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int64_Modulus_Interval.zmatch_filter_greater_equal _ _ _ _ H H0 CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  }
  {
  destruct cmp; destruct x1; inv CMP.
    all: try solve [ split; constructor; eassumption
                   | eapply bad_test; eassumption
                   | eapply bad_test2; eassumption].
    2-5: pose proof (H0 := zmatch_int64_full_range i).
  - pose proof (Int64.same_if_eq _ _ H1). subst.
    split ; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int64_Modulus_Interval.zmatch_filter_less _ _ _ _ H H0 CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
      split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int64.unsigned l <= Int64.unsigned i) as CMP' by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_less_equal _ _ _ _ H H0 CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int64.unsigned l > Int64.unsigned i) as CMP' by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_greater _ _ _ _ H H0 CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int64_Modulus_Interval.zmatch_filter_greater_equal _ _ _ _ H H0 CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  }
  {
  destruct cmp; destruct x0; inv CMP.
    all: try solve [ split; constructor; eassumption
                   | eapply bad_test; eassumption
                   | eapply bad_test2; eassumption].
    2-5: pose proof (H0 := zmatch_int64_full_range i).
  - pose proof (Int64.same_if_eq _ _ H1). subst.
      split ; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int64_Modulus_Interval.zmatch_filter_less _ _ _ _ H0 H CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int64.unsigned i <= Int64.unsigned l) as CMP' by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_less_equal _ _ _ _ H0 H CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    assert (Int64.unsigned i > Int64.unsigned l) as CMP' by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_greater _ _ _ _ H0 H CMP')
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE.
    split; constructor; assumption.
  - unfold Int64.ltu in *. destruct zlt as [CMP | CMP]; try discriminate.
    destruct (Int64_Modulus_Interval.zmatch_filter_greater_equal _ _ _ _ H0 H CMP)
      as (i0' & i1' & RE & MATCH0' & MATCH1').
    rewrite RE. split; constructor; assumption.
  }
  unfold Val.cmplu_bool in CMP. destruct x0; discriminate.
Qed.

Definition cmplu_bool (cmp : comparison)
           (a0 a1 : ival) : ibool :=
  match a0, a1 with
  | (Ilong false i0), (Ilong false i1) =>
      match cmp with
      | Cle =>
          Int64_Modulus_Interval.filter_to_eval
            Int64_Modulus_Interval.filter_less_equal
            Int64_Modulus_Interval.filter_greater i0 i1
      | Cge =>
          Int64_Modulus_Interval.filter_to_eval
            Int64_Modulus_Interval.filter_greater_equal
            Int64_Modulus_Interval.filter_less i0 i1
      | Clt =>
          Int64_Modulus_Interval.filter_to_eval
            Int64_Modulus_Interval.filter_less
            Int64_Modulus_Interval.filter_greater_equal i0 i1
      | Cgt =>
          Int64_Modulus_Interval.filter_to_eval
            Int64_Modulus_Interval.filter_greater
            Int64_Modulus_Interval.filter_less_equal i0 i1
      | Ceq =>
          Int64_Modulus_Interval.filter_to_eval
            Int64_Modulus_Interval.filter_equal
            Int64_Modulus_Interval.filter_not_equal i0 i1
      | Cne =>
          Int64_Modulus_Interval.filter_to_eval
            Int64_Modulus_Interval.filter_not_equal
            Int64_Modulus_Interval.filter_equal
            i0 i1
      end
  | _, _ => Btop
  end.

Lemma cmplu_bool_sound:
  forall valid c v w x y, vmatch v x -> vmatch w y ->
    cmatch (Val.cmplu_bool valid c v w) (cmplu_bool c x y).
Proof.
  intros. unfold Val.cmplu_bool, cmplu_bool.
  inv H; try constructor; inv H0; try rewrite if_same; try constructor.
  destruct c; cbn; destruct b, b0; try constructor.
  - change (Int64.eq l l0) with ((fun x y => if zeq x y then true else false) (Int64.unsigned l) (Int64.unsigned l0)).
    apply Int64_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_equal; auto.
      destruct zeq; congruence.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_not_equal; auto.
      destruct zeq; congruence.
 - change (negb (Int64.eq l l0)) with ((fun x y => negb (if zeq x y then true else false)) (Int64.unsigned l) (Int64.unsigned l0)).
   apply Int64_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_not_equal; auto.
      destruct zeq; cbn in CMP; congruence.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_equal; auto.
      destruct zeq; cbn in CMP; congruence.
 - change (Int64.ltu l l0) with ((fun x y => if zlt x y then true else false) (Int64.unsigned l) (Int64.unsigned l0)).
    apply Int64_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_less; auto.
      destruct zlt; congruence.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_greater_equal; auto.
      destruct zlt; lia.
 - change (negb (Int64.ltu l0 l)) with ((fun x y => negb (if zlt y x then true else false)) (Int64.unsigned l) (Int64.unsigned l0)).
    apply Int64_Modulus_Interval.filter_to_eval_sound; trivial.
   + intros. apply Int64_Modulus_Interval.zmatch_filter_less_equal; auto.
     destruct zlt; lia.
   + intros. apply Int64_Modulus_Interval.zmatch_filter_greater; auto.
     destruct zlt; lia.
 - change (Int64.ltu l0 l) with ((fun x y => (if zlt y x then true else false)) (Int64.unsigned l) (Int64.unsigned l0)).
    apply Int64_Modulus_Interval.filter_to_eval_sound; trivial.
   + intros. apply Int64_Modulus_Interval.zmatch_filter_greater; auto.
     destruct zlt; lia.
   + intros. apply Int64_Modulus_Interval.zmatch_filter_less_equal; auto.
     destruct zlt; lia.
 - change (negb (Int64.ltu l l0)) with ((fun x y => negb (if zlt x y then true else false)) (Int64.unsigned l) (Int64.unsigned l0)).
    apply Int64_Modulus_Interval.filter_to_eval_sound; trivial.
   + intros. apply Int64_Modulus_Interval.zmatch_filter_greater_equal; auto.
     destruct zlt; lia.
   + intros. apply Int64_Modulus_Interval.zmatch_filter_less; auto.
     destruct zlt; lia.
Qed.

Definition pair_bot {A B: Type} (a : option A) (b : option B) : option(A*B) :=
  match a, b with
  | (Some a'), (Some b') => Some(a', b')
  | None, _ | _, None => None
  end.

Program Definition int_positive := (Int_Modulus_Interval.mkmod_interval (Interval.mkinterval 0 (Int.half_modulus-1) _) _ _)%Z.

Program Definition int_negative := (Int_Modulus_Interval.mkmod_interval (Interval.mkinterval Int.half_modulus (Int.modulus-1) _) _ _)%Z.

Definition signed_int_filter_less i0 i1 :=
  let p0 := Int_Modulus_Interval.glb_nb i0 int_positive in
  let n0 := Int_Modulus_Interval.glb_nb i0 int_negative in
  let p1 := Int_Modulus_Interval.glb_nb i1 int_positive in
  let n1 := Int_Modulus_Interval.glb_nb i1 int_negative in
  let pos_pos :=
    match p0, p1 with
    | (Some a), (Some b) =>
        Int_Modulus_Interval.filter_less a b
    | _, _ => None
    end in
  let neg_neg :=
    match n0, n1 with
    | (Some a), (Some b) =>
        Int_Modulus_Interval.filter_less a b
    | _, _ => None
    end in
  let neg_pos := pair_bot n0 p1 in
  Int_Modulus_Interval.pair_lub neg_pos
    (Int_Modulus_Interval.pair_lub pos_pos neg_neg).

Lemma zmatch_signed_int_filter_less :
  forall (x y : int) (a b : Int_Modulus_Interval.t)
         (AMATCH : Int_Modulus_Interval.zmatch (Int.unsigned x) a)
         (BMATCH : Int_Modulus_Interval.zmatch (Int.unsigned y) b)
         (CMP : Int.lt x y = true),
    exists a', exists b',
      signed_int_filter_less a b = Some(a', b') /\
        Int_Modulus_Interval.zmatch (Int.unsigned x) a' /\
        Int_Modulus_Interval.zmatch (Int.unsigned y) b'.
Proof.
  unfold Int.lt, Int.signed. intros.
  pose proof (Int.unsigned_range x) as xRANGE.
  pose proof (Int.unsigned_range y) as yRANGE.
  destruct (zlt (Int.unsigned x) Int.half_modulus) as [xPOS | xNEG];
    destruct (zlt (Int.unsigned y) Int.half_modulus) as [yPOS | yNEG];
    change Int.half_modulus with (2^31)%Z in *;
    change Int.modulus with (2^32)%Z in *.
  all: destruct zlt as [ LESS | GT ]; try discriminate; try lia; clear CMP.
  all: unfold signed_int_filter_less.
  - assert (Int_Modulus_Interval.zmatch (Int.unsigned x) int_positive) as xMPOS.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned x) a int_positive AMATCH xMPOS) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int_Modulus_Interval.zmatch (Int.unsigned y) int_positive) as yMPOS.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned y) b int_positive BMATCH yMPOS) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.

    destruct (Int_Modulus_Interval.zmatch_filter_less (Int.unsigned x) (Int.unsigned y) xGLB yGLB xGLB_MA yGLB_MA LESS) as (a1 & b1 & RE1 & MA1 & MB1).
    rewrite RE1.
    
    destruct (Int_Modulus_Interval.zmatch_pair_lub_left _ _ _ _
      (match Int_Modulus_Interval.glb_nb a int_negative with
       | Some a0 =>
           match Int_Modulus_Interval.glb_nb b int_negative with
           | Some b0 => Int_Modulus_Interval.filter_less a0 b0
           | None => None
           end
       | None => None
       end) MA1 MB1) as (a2 & b2 & RE2 & MA2 & MB2).
    rewrite RE2.

    apply Int_Modulus_Interval.zmatch_pair_lub_right; assumption.

 - assert (Int_Modulus_Interval.zmatch (Int.unsigned x) int_negative) as xMNEG.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned x) a int_negative AMATCH xMNEG) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int_Modulus_Interval.zmatch (Int.unsigned y) int_positive) as yMPOS.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned y) b int_positive BMATCH yMPOS) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.
    simpl pair_bot.

    apply Int_Modulus_Interval.zmatch_pair_lub_left; assumption.
    
 - assert (Int_Modulus_Interval.zmatch (Int.unsigned x) int_negative) as xMNEG.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned x) a int_negative AMATCH xMNEG) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int_Modulus_Interval.zmatch (Int.unsigned y) int_negative) as yMNEG.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned y) b int_negative BMATCH yMNEG) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.

    assert (LESS' : Int.unsigned x < Int.unsigned y) by lia.
    destruct (Int_Modulus_Interval.zmatch_filter_less (Int.unsigned x) (Int.unsigned y) xGLB yGLB xGLB_MA yGLB_MA LESS') as (a1 & b1 & RE1 & MA1 & MB1).
    rewrite RE1.
    
    destruct (Int_Modulus_Interval.zmatch_pair_lub_right
         (match Int_Modulus_Interval.glb_nb a int_positive with
         | Some a0 =>
             match Int_Modulus_Interval.glb_nb b int_positive with
             | Some b0 => Int_Modulus_Interval.filter_less a0 b0
             | None => None
             end
         | None => None
         end) _ _ _ _ MA1 MB1) as (a2 & b2 & RE2 & MA2 & MB2).
    rewrite RE2.

    apply Int_Modulus_Interval.zmatch_pair_lub_right; assumption.
Qed.

Definition signed_int_filter_less_equal i0 i1 :=
  let p0 := Int_Modulus_Interval.glb_nb i0 int_positive in
  let n0 := Int_Modulus_Interval.glb_nb i0 int_negative in
  let p1 := Int_Modulus_Interval.glb_nb i1 int_positive in
  let n1 := Int_Modulus_Interval.glb_nb i1 int_negative in
  let pos_pos :=
    match p0, p1 with
    | (Some a), (Some b) =>
        Int_Modulus_Interval.filter_less_equal a b
    | _, _ => None
    end in
  let neg_neg :=
    match n0, n1 with
    | (Some a), (Some b) =>
        Int_Modulus_Interval.filter_less_equal a b
    | _, _ => None
    end in
  let neg_pos := pair_bot n0 p1 in
  Int_Modulus_Interval.pair_lub neg_pos
    (Int_Modulus_Interval.pair_lub pos_pos neg_neg).

Lemma zmatch_signed_int_filter_less_equal :
  forall (x y : int) (a b : Int_Modulus_Interval.t)
         (AMATCH : Int_Modulus_Interval.zmatch (Int.unsigned x) a)
         (BMATCH : Int_Modulus_Interval.zmatch (Int.unsigned y) b)
         (CMP : Int.lt y x = false),
    exists a', exists b',
      signed_int_filter_less_equal a b = Some(a', b') /\
        Int_Modulus_Interval.zmatch (Int.unsigned x) a' /\
        Int_Modulus_Interval.zmatch (Int.unsigned y) b'.
Proof.
  unfold Int.lt, Int.signed. intros.
  pose proof (Int.unsigned_range x) as xRANGE.
  pose proof (Int.unsigned_range y) as yRANGE.
  destruct (zlt (Int.unsigned x) Int.half_modulus) as [xPOS | xNEG];
    destruct (zlt (Int.unsigned y) Int.half_modulus) as [yPOS | yNEG];
    change Int.half_modulus with (2^31)%Z in *;
    change Int.modulus with (2^32)%Z in *.
  all: destruct zlt as [ LT | GEQ ]; try discriminate; try lia; clear CMP.
  all: unfold signed_int_filter_less_equal.
  - assert (Int_Modulus_Interval.zmatch (Int.unsigned x) int_positive) as xMPOS.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned x) a int_positive AMATCH xMPOS) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int_Modulus_Interval.zmatch (Int.unsigned y) int_positive) as yMPOS.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned y) b int_positive BMATCH yMPOS) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.

    assert (LEQ : Int.unsigned x <= Int.unsigned y) by lia.
    destruct (Int_Modulus_Interval.zmatch_filter_less_equal (Int.unsigned x) (Int.unsigned y) xGLB yGLB xGLB_MA yGLB_MA LEQ) as (a1 & b1 & RE1 & MA1 & MB1).
    rewrite RE1.
    
    destruct (Int_Modulus_Interval.zmatch_pair_lub_left _ _ _ _
      (match Int_Modulus_Interval.glb_nb a int_negative with
       | Some a0 =>
           match Int_Modulus_Interval.glb_nb b int_negative with
           | Some b0 => Int_Modulus_Interval.filter_less_equal a0 b0
           | None => None
           end
       | None => None
       end) MA1 MB1) as (a2 & b2 & RE2 & MA2 & MB2).
    rewrite RE2.

    apply Int_Modulus_Interval.zmatch_pair_lub_right; assumption.

 - assert (Int_Modulus_Interval.zmatch (Int.unsigned x) int_negative) as xMNEG.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned x) a int_negative AMATCH xMNEG) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int_Modulus_Interval.zmatch (Int.unsigned y) int_positive) as yMPOS.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned y) b int_positive BMATCH yMPOS) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.
    simpl pair_bot.

    apply Int_Modulus_Interval.zmatch_pair_lub_left; assumption.
    
 - assert (Int_Modulus_Interval.zmatch (Int.unsigned x) int_negative) as xMNEG.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned x) a int_negative AMATCH xMNEG) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int_Modulus_Interval.zmatch (Int.unsigned y) int_negative) as yMNEG.
    { constructor; cbn; lia. }
    destruct (Int_Modulus_Interval.zmatch_glb_nb (Int.unsigned y) b int_negative BMATCH yMNEG) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.

    assert (LEQ' : Int.unsigned x <= Int.unsigned y) by lia.
    destruct (Int_Modulus_Interval.zmatch_filter_less_equal (Int.unsigned x) (Int.unsigned y) xGLB yGLB xGLB_MA yGLB_MA LEQ') as (a1 & b1 & RE1 & MA1 & MB1).
    rewrite RE1.
    
    destruct (Int_Modulus_Interval.zmatch_pair_lub_right
         (match Int_Modulus_Interval.glb_nb a int_positive with
         | Some a0 =>
             match Int_Modulus_Interval.glb_nb b int_positive with
             | Some b0 => Int_Modulus_Interval.filter_less_equal a0 b0
             | None => None
             end
         | None => None
         end) _ _ _ _ MA1 MB1) as (a2 & b2 & RE2 & MA2 & MB2).
    rewrite RE2.

    apply Int_Modulus_Interval.zmatch_pair_lub_right; assumption.
Qed.

Definition signed_int_filter_greater i0 i1 :=
  match signed_int_filter_less i1 i0 with
  | Some(i1', i0') => (Some(i0', i1'))
  | None => None
  end.

Definition signed_int_filter_greater_equal i0 i1 :=
  match signed_int_filter_less_equal i1 i0 with
  | Some(i1', i0') => (Some(i0', i1'))
  | None => None
  end.
  
Lemma zmatch_signed_int_filter_greater :
  forall (x y : int) a b
         (AMATCH : Int_Modulus_Interval.zmatch (Int.unsigned x) a)
         (BMATCH : Int_Modulus_Interval.zmatch (Int.unsigned y) b)
         (CMP : Int.lt y x = true),
    exists a', exists b',
      signed_int_filter_greater a b = Some(a', b') /\
        Int_Modulus_Interval.zmatch (Int.unsigned x) a' /\
        Int_Modulus_Interval.zmatch (Int.unsigned y) b'.
Proof.
  unfold signed_int_filter_greater. intros.
  destruct (zmatch_signed_int_filter_less y x b a BMATCH AMATCH CMP) as (b' & a' & RE & MATCHB' & MATCHA' ).
  exists a'. exists b'. rewrite RE. auto.
Qed.
  
Lemma zmatch_signed_int_filter_greater_equal :
  forall (x y : int) a b
         (AMATCH : Int_Modulus_Interval.zmatch (Int.unsigned x) a)
         (BMATCH : Int_Modulus_Interval.zmatch (Int.unsigned y) b)
         (CMP : Int.lt x y = false),
    exists a', exists b',
      signed_int_filter_greater_equal a b = Some(a', b') /\
        Int_Modulus_Interval.zmatch (Int.unsigned x) a' /\
        Int_Modulus_Interval.zmatch (Int.unsigned y) b'.
Proof.
  unfold signed_int_filter_greater_equal. intros.
  destruct (zmatch_signed_int_filter_less_equal y x b a BMATCH AMATCH CMP) as (b' & a' & RE & MATCHB' & MATCHA' ).
  exists a'. exists b'. rewrite RE. auto.
Qed.


Lemma negb_true_then_false:
  forall b, negb b = true -> b = false.
Proof.
  destruct b; cbn; congruence.
Qed.

Lemma negb_false_then_true:
  forall b, negb b = false -> b = true.
Proof.
  destruct b; cbn; congruence.
Qed.

Definition any_int := Iint false Int_Modulus_Interval.full_range.

Lemma any_int_sound : forall z, vmatch (Vint z) any_int.
Proof.
  intro. constructor. apply zmatch_int_full_range.
Qed.

Definition any_long := Ilong false Int64_Modulus_Interval.full_range.

Lemma any_long_sound : forall z, vmatch (Vlong z) any_long.
Proof.
  intro. constructor. apply zmatch_int64_full_range.
Qed.

Definition filter_cmp_Iint (cmp : comparison) (i0 i1 : Int_Modulus_Interval.t) : ival * ival :=
  match cmp with
  | Cle =>
      match signed_int_filter_less_equal i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  | Cge =>
      match signed_int_filter_greater_equal i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  | Clt =>
      match signed_int_filter_less i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  | Cgt =>
      match signed_int_filter_greater i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  | Ceq =>
      match Int_Modulus_Interval.glb_nb i0 i1 with
      | Some i' => ((Iint false i'), (Iint false i'))
      | None => (Ibot, Ibot)
      end
  | Cne =>
      match Int_Modulus_Interval.filter_not_equal i0 i1 with
      | Some(i0', i1') => ((Iint false i0'), (Iint false i1'))
      | None => (Ibot, Ibot)
      end
  end.

Lemma filter_cmp_Iint_sound cmp i0 i1 (x0 x1 : int)
  (Z0 : Int_Modulus_Interval.zmatch (Int.unsigned x0) i0)
  (Z1 : Int_Modulus_Interval.zmatch (Int.unsigned x1) i1)
  (CMP : Int.cmp cmp x0 x1 = true):
  let (a0', a1') := filter_cmp_Iint cmp i0 i1 in
  vmatch (Vint x0) a0' /\ vmatch (Vint x1) a1'.
Proof.
  Local Ltac slv ::= split; constructor; assumption.
  destruct cmp; simpl in *;
    try apply negb_true_iff in CMP.
  - rewrite (Int.same_if_eq _ _ CMP) in *.
    destruct (Int_Modulus_Interval.zmatch_glb_nb _ _ _ Z0 Z1)
      as (c & -> & MATCH).
    slv.
  - apply proj_sumbool_false in CMP.
    destruct (Int_Modulus_Interval.zmatch_filter_not_equal _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (zmatch_signed_int_filter_less _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (zmatch_signed_int_filter_less_equal _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (zmatch_signed_int_filter_greater _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (zmatch_signed_int_filter_greater_equal _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
Qed.

Definition filter_cmp (cmp : comparison) (a0 a1 : ival) : ival*ival :=
  match filter_Vint a0, filter_Vint a1 with
  | Some i0, Some i1 => filter_cmp_Iint cmp i0 i1
  | _, _ => (Ibot, Ibot)
  end.

Lemma filter_cmp_sound (cmp : comparison)
  (a0 a1 : ival) (x0 x1 : val)
  (MATCH0 : vmatch x0 a0) (MATCH1 : vmatch x1 a1)
  (CMP : (Val.cmp_bool cmp x0 x1) = Some true):
  let (a0', a1') := filter_cmp cmp a0 a1 in
  vmatch x0 a0' /\ vmatch x1 a1'.
Proof.
  assert (exists xi0 xi1, x0 = Vint xi0 /\ x1 = Vint xi1) as (xi0 & xi1 & ? & ?). {
    revert CMP; unfold Val.cmp_bool.
    destruct x0; try discriminate 1;
    destruct x1; try discriminate 1.
    repeat econstructor.
  }
  subst; unfold filter_cmp.
  apply filter_Vint_sound in MATCH0 as (i0 & -> & MATCH0),
                             MATCH1 as (i1 & -> & MATCH1).
  inv MATCH0; inv MATCH1; injection CMP as ?.
  eapply filter_cmp_Iint_sound; eauto.
Qed.

Definition cmp_bool (cmp : comparison)
           (a0 a1 : ival) : ibool :=
  match a0, a1 with
  | (Iint false i0), (Iint false i1) =>
      match cmp with
      | Cle =>
          Int_Modulus_Interval.filter_to_eval
            signed_int_filter_less_equal
            signed_int_filter_greater i0 i1
      | Cge =>
          Int_Modulus_Interval.filter_to_eval
            signed_int_filter_greater_equal
            signed_int_filter_less i0 i1
      | Clt =>
          Int_Modulus_Interval.filter_to_eval
            signed_int_filter_less
            signed_int_filter_greater_equal i0 i1
      | Cgt =>
          Int_Modulus_Interval.filter_to_eval
            signed_int_filter_greater
            signed_int_filter_less_equal i0 i1
      | Ceq =>
          Int_Modulus_Interval.filter_to_eval
            Int_Modulus_Interval.filter_equal
            Int_Modulus_Interval.filter_not_equal i0 i1
      | Cne =>
          Int_Modulus_Interval.filter_to_eval
            Int_Modulus_Interval.filter_not_equal
            Int_Modulus_Interval.filter_equal
            i0 i1
      end
  | _, _ => Btop
  end.

Lemma int_filter_to_eval_sound :
 forall (pred : Z.t -> Z.t -> bool)
         (filter : Int_Modulus_Interval.t ->
                   Int_Modulus_Interval.t ->
                   option (Int_Modulus_Interval.t * Int_Modulus_Interval.t))
       (zmatch_filter : forall (x y : int) (a b : Int_Modulus_Interval.t),
        Int_Modulus_Interval.zmatch (Int.unsigned x) a ->
        Int_Modulus_Interval.zmatch (Int.unsigned y) b ->
        pred (Int.unsigned x) (Int.unsigned y) = true ->
        exists a' b' : Int_Modulus_Interval.t,
          filter a b = Some (a', b') /\
            Int_Modulus_Interval.zmatch (Int.unsigned x) a' /\
            Int_Modulus_Interval.zmatch (Int.unsigned y) b')
       (filter_not : Int_Modulus_Interval.t ->
                      Int_Modulus_Interval.t ->
                      option (Int_Modulus_Interval.t * Int_Modulus_Interval.t))
       (zmatch_filter_not : forall (x y : int) (a b : Int_Modulus_Interval.t),
        Int_Modulus_Interval.zmatch (Int.unsigned x) a ->
        Int_Modulus_Interval.zmatch (Int.unsigned y) b ->
        pred (Int.unsigned x) (Int.unsigned y) = false ->
        exists a' b' : Int_Modulus_Interval.t,
          filter_not a b = Some (a', b') /\
            Int_Modulus_Interval.zmatch (Int.unsigned x) a' /\
            Int_Modulus_Interval.zmatch (Int.unsigned y) b')
       (x y : int) (a b : Int_Modulus_Interval.t)
       (AMATCH : Int_Modulus_Interval.zmatch (Int.unsigned x) a)
       (BMATCH : Int_Modulus_Interval.zmatch (Int.unsigned y) b),
       cmatch (Some (pred (Int.unsigned x) (Int.unsigned y)))
              (Int_Modulus_Interval.filter_to_eval filter filter_not a b).
Proof.
  intros.
  unfold Int_Modulus_Interval.filter_to_eval.
  destruct pred eqn:PRED.
  - pose proof (zmatch_filter _ _ _ _ AMATCH BMATCH PRED) as (a' & b' & RE & MATCHA' & MATCHB').
    rewrite RE.
    destruct filter_not; constructor.
  - pose proof (zmatch_filter_not _ _ _ _ AMATCH BMATCH PRED) as (a' & b' & RE & MATCHA' & MATCHB').
    rewrite RE.
    destruct filter; constructor.
Qed.

Lemma cmp_bool_sound:
  forall c v w x y, vmatch v x -> vmatch w y ->
    cmatch (Val.cmp_bool c v w) (cmp_bool c x y).
Proof.
  intros. unfold Val.cmp_bool, cmp_bool.
  inv H; try constructor; inv H0; try rewrite if_same; try constructor.
  destruct c; cbn; destruct b, b0; try constructor.
  - change (Int.eq i i0) with ((fun x y => if zeq x y then true else false) (Int.unsigned i) (Int.unsigned i0)).
    apply Int_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int_Modulus_Interval.zmatch_filter_equal; auto.
      destruct zeq; congruence.
    + intros. apply Int_Modulus_Interval.zmatch_filter_not_equal; auto.
      destruct zeq; congruence.
 - change (negb (Int.eq i i0)) with ((fun x y => negb (if zeq x y then true else false)) (Int.unsigned i) (Int.unsigned i0)).
   apply Int_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int_Modulus_Interval.zmatch_filter_not_equal; auto.
      destruct zeq; cbn in CMP; congruence.
    + intros. apply Int_Modulus_Interval.zmatch_filter_equal; auto.
      destruct zeq; cbn in CMP; congruence.
 - apply (int_filter_to_eval_sound
     (fun x y => zlt
           (if zlt x Int.half_modulus
            then x
            else x - Int.modulus)
           (if zlt y Int.half_modulus
            then y
            else y - Int.modulus))); trivial.
    + intros. apply zmatch_signed_int_filter_less; auto.
    + intros. apply zmatch_signed_int_filter_greater_equal; auto.
      
 - apply (int_filter_to_eval_sound
     (fun y x => negb (zlt
           (if zlt x Int.half_modulus
            then x
            else x - Int.modulus)
           (if zlt y Int.half_modulus
            then y
            else y - Int.modulus)))); trivial.
   + intros. apply zmatch_signed_int_filter_less_equal; auto.
     apply negb_true_then_false. exact H3.
     
   + intros. apply zmatch_signed_int_filter_greater; auto.
     apply negb_false_then_true. exact H3.
     
 - apply (int_filter_to_eval_sound
     (fun y x => zlt
           (if zlt x Int.half_modulus
            then x
            else x - Int.modulus)
           (if zlt y Int.half_modulus
            then y
            else y - Int.modulus))); trivial.
   + intros. apply zmatch_signed_int_filter_greater; auto.
   + intros. apply zmatch_signed_int_filter_less_equal; auto.
     
 - apply (int_filter_to_eval_sound
     (fun x y => negb (zlt
           (if zlt x Int.half_modulus
            then x
            else x - Int.modulus)
           (if zlt y Int.half_modulus
            then y
            else y - Int.modulus)))); trivial.
   + intros. apply zmatch_signed_int_filter_greater_equal; auto.
     apply negb_true_then_false. exact H3.
   + intros. apply zmatch_signed_int_filter_less; auto.
     apply negb_false_then_true. exact H3.
Qed.

Program Definition int64_positive := (Int64_Modulus_Interval.mkmod_interval (Interval.mkinterval 0 (Int64.half_modulus-1) _) _ _)%Z.

Program Definition int64_negative := (Int64_Modulus_Interval.mkmod_interval (Interval.mkinterval Int64.half_modulus (Int64.modulus-1) _) _ _)%Z.

Definition signed_int64_filter_less i0 i1 :=
  let p0 := Int64_Modulus_Interval.glb_nb i0 int64_positive in
  let n0 := Int64_Modulus_Interval.glb_nb i0 int64_negative in
  let p1 := Int64_Modulus_Interval.glb_nb i1 int64_positive in
  let n1 := Int64_Modulus_Interval.glb_nb i1 int64_negative in
  let pos_pos :=
    match p0, p1 with
    | (Some a), (Some b) =>
        Int64_Modulus_Interval.filter_less a b
    | _, _ => None
    end in
  let neg_neg :=
    match n0, n1 with
    | (Some a), (Some b) =>
        Int64_Modulus_Interval.filter_less a b
    | _, _ => None
    end in
  let neg_pos := pair_bot n0 p1 in
  Int64_Modulus_Interval.pair_lub neg_pos
    (Int64_Modulus_Interval.pair_lub pos_pos neg_neg).

Lemma zmatch_signed_int64_filter_less :
  forall (x y : int64) (a b : Int64_Modulus_Interval.t)
         (AMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned x) a)
         (BMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned y) b)
         (CMP : Int64.lt x y = true),
    exists a', exists b',
      signed_int64_filter_less a b = Some(a', b') /\
        Int64_Modulus_Interval.zmatch (Int64.unsigned x) a' /\
        Int64_Modulus_Interval.zmatch (Int64.unsigned y) b'.
Proof.
  unfold Int64.lt, Int64.signed. intros.
  pose proof (Int64.unsigned_range x) as xRANGE.
  pose proof (Int64.unsigned_range y) as yRANGE.
  destruct (zlt (Int64.unsigned x) Int64.half_modulus) as [xPOS | xNEG];
    destruct (zlt (Int64.unsigned y) Int64.half_modulus) as [yPOS | yNEG];
    change Int64.half_modulus with (2^63)%Z in *;
    change Int64.modulus with (2^64)%Z in *.
  all: destruct zlt as [ LESS | GT ]; try discriminate; try lia; clear CMP.
  all: unfold signed_int64_filter_less.
  - assert (Int64_Modulus_Interval.zmatch (Int64.unsigned x) int64_positive) as xMPOS.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned x) a int64_positive AMATCH xMPOS) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int64_Modulus_Interval.zmatch (Int64.unsigned y) int64_positive) as yMPOS.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned y) b int64_positive BMATCH yMPOS) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.

    destruct (Int64_Modulus_Interval.zmatch_filter_less (Int64.unsigned x) (Int64.unsigned y) xGLB yGLB xGLB_MA yGLB_MA LESS) as (a1 & b1 & RE1 & MA1 & MB1).
    rewrite RE1.
    
    destruct (Int64_Modulus_Interval.zmatch_pair_lub_left _ _ _ _
      (match Int64_Modulus_Interval.glb_nb a int64_negative with
       | Some a0 =>
           match Int64_Modulus_Interval.glb_nb b int64_negative with
           | Some b0 => Int64_Modulus_Interval.filter_less a0 b0
           | None => None
           end
       | None => None
       end) MA1 MB1) as (a2 & b2 & RE2 & MA2 & MB2).
    rewrite RE2.

    apply Int64_Modulus_Interval.zmatch_pair_lub_right; assumption.

 - assert (Int64_Modulus_Interval.zmatch (Int64.unsigned x) int64_negative) as xMNEG.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned x) a int64_negative AMATCH xMNEG) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int64_Modulus_Interval.zmatch (Int64.unsigned y) int64_positive) as yMPOS.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned y) b int64_positive BMATCH yMPOS) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.
    simpl pair_bot.

    apply Int64_Modulus_Interval.zmatch_pair_lub_left; assumption.
    
 - assert (Int64_Modulus_Interval.zmatch (Int64.unsigned x) int64_negative) as xMNEG.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned x) a int64_negative AMATCH xMNEG) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int64_Modulus_Interval.zmatch (Int64.unsigned y) int64_negative) as yMNEG.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned y) b int64_negative BMATCH yMNEG) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.

    assert (LESS' : Int64.unsigned x < Int64.unsigned y) by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_less (Int64.unsigned x) (Int64.unsigned y) xGLB yGLB xGLB_MA yGLB_MA LESS') as (a1 & b1 & RE1 & MA1 & MB1).
    rewrite RE1.
    
    destruct (Int64_Modulus_Interval.zmatch_pair_lub_right
         (match Int64_Modulus_Interval.glb_nb a int64_positive with
         | Some a0 =>
             match Int64_Modulus_Interval.glb_nb b int64_positive with
             | Some b0 => Int64_Modulus_Interval.filter_less a0 b0
             | None => None
             end
         | None => None
         end) _ _ _ _ MA1 MB1) as (a2 & b2 & RE2 & MA2 & MB2).
    rewrite RE2.

    apply Int64_Modulus_Interval.zmatch_pair_lub_right; assumption.
Qed.

Definition signed_int64_filter_less_equal i0 i1 :=
  let p0 := Int64_Modulus_Interval.glb_nb i0 int64_positive in
  let n0 := Int64_Modulus_Interval.glb_nb i0 int64_negative in
  let p1 := Int64_Modulus_Interval.glb_nb i1 int64_positive in
  let n1 := Int64_Modulus_Interval.glb_nb i1 int64_negative in
  let pos_pos :=
    match p0, p1 with
    | (Some a), (Some b) =>
        Int64_Modulus_Interval.filter_less_equal a b
    | _, _ => None
    end in
  let neg_neg :=
    match n0, n1 with
    | (Some a), (Some b) =>
        Int64_Modulus_Interval.filter_less_equal a b
    | _, _ => None
    end in
  let neg_pos := pair_bot n0 p1 in
  Int64_Modulus_Interval.pair_lub neg_pos
    (Int64_Modulus_Interval.pair_lub pos_pos neg_neg).

Lemma zmatch_signed_int64_filter_less_equal :
  forall (x y : int64) (a b : Int64_Modulus_Interval.t)
         (AMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned x) a)
         (BMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned y) b)
         (CMP : Int64.lt y x = false),
    exists a', exists b',
      signed_int64_filter_less_equal a b = Some(a', b') /\
        Int64_Modulus_Interval.zmatch (Int64.unsigned x) a' /\
        Int64_Modulus_Interval.zmatch (Int64.unsigned y) b'.
Proof.
  unfold Int64.lt, Int64.signed. intros.
  pose proof (Int64.unsigned_range x) as xRANGE.
  pose proof (Int64.unsigned_range y) as yRANGE.
  destruct (zlt (Int64.unsigned x) Int64.half_modulus) as [xPOS | xNEG];
    destruct (zlt (Int64.unsigned y) Int64.half_modulus) as [yPOS | yNEG];
    change Int64.half_modulus with (2^63)%Z in *;
    change Int64.modulus with (2^64)%Z in *.
  all: destruct zlt as [ LT | GEQ ]; try discriminate; try lia; clear CMP.
  all: unfold signed_int64_filter_less_equal.
  - assert (Int64_Modulus_Interval.zmatch (Int64.unsigned x) int64_positive) as xMPOS.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned x) a int64_positive AMATCH xMPOS) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int64_Modulus_Interval.zmatch (Int64.unsigned y) int64_positive) as yMPOS.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned y) b int64_positive BMATCH yMPOS) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.

    assert (LEQ : Int64.unsigned x <= Int64.unsigned y) by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_less_equal (Int64.unsigned x) (Int64.unsigned y) xGLB yGLB xGLB_MA yGLB_MA LEQ) as (a1 & b1 & RE1 & MA1 & MB1).
    rewrite RE1.
    
    destruct (Int64_Modulus_Interval.zmatch_pair_lub_left _ _ _ _
      (match Int64_Modulus_Interval.glb_nb a int64_negative with
       | Some a0 =>
           match Int64_Modulus_Interval.glb_nb b int64_negative with
           | Some b0 => Int64_Modulus_Interval.filter_less_equal a0 b0
           | None => None
           end
       | None => None
       end) MA1 MB1) as (a2 & b2 & RE2 & MA2 & MB2).
    rewrite RE2.

    apply Int64_Modulus_Interval.zmatch_pair_lub_right; assumption.

 - assert (Int64_Modulus_Interval.zmatch (Int64.unsigned x) int64_negative) as xMNEG.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned x) a int64_negative AMATCH xMNEG) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int64_Modulus_Interval.zmatch (Int64.unsigned y) int64_positive) as yMPOS.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned y) b int64_positive BMATCH yMPOS) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.
    simpl pair_bot.

    apply Int64_Modulus_Interval.zmatch_pair_lub_left; assumption.
    
 - assert (Int64_Modulus_Interval.zmatch (Int64.unsigned x) int64_negative) as xMNEG.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned x) a int64_negative AMATCH xMNEG) as (xGLB & xGLB_RE & xGLB_MA).
    rewrite xGLB_RE.
    
    assert (Int64_Modulus_Interval.zmatch (Int64.unsigned y) int64_negative) as yMNEG.
    { constructor; cbn; lia. }
    destruct (Int64_Modulus_Interval.zmatch_glb_nb (Int64.unsigned y) b int64_negative BMATCH yMNEG) as (yGLB & yGLB_RE & yGLB_MA).
    rewrite yGLB_RE.

    assert (LEQ' : Int64.unsigned x <= Int64.unsigned y) by lia.
    destruct (Int64_Modulus_Interval.zmatch_filter_less_equal (Int64.unsigned x) (Int64.unsigned y) xGLB yGLB xGLB_MA yGLB_MA LEQ') as (a1 & b1 & RE1 & MA1 & MB1).
    rewrite RE1.
    
    destruct (Int64_Modulus_Interval.zmatch_pair_lub_right
         (match Int64_Modulus_Interval.glb_nb a int64_positive with
         | Some a0 =>
             match Int64_Modulus_Interval.glb_nb b int64_positive with
             | Some b0 => Int64_Modulus_Interval.filter_less_equal a0 b0
             | None => None
             end
         | None => None
         end) _ _ _ _ MA1 MB1) as (a2 & b2 & RE2 & MA2 & MB2).
    rewrite RE2.

    apply Int64_Modulus_Interval.zmatch_pair_lub_right; assumption.
Qed.

Definition signed_int64_filter_greater i0 i1 :=
  match signed_int64_filter_less i1 i0 with
  | Some(i1', i0') => (Some(i0', i1'))
  | None => None
  end.

Definition signed_int64_filter_greater_equal i0 i1 :=
  match signed_int64_filter_less_equal i1 i0 with
  | Some(i1', i0') => (Some(i0', i1'))
  | None => None
  end.
  
Lemma zmatch_signed_int64_filter_greater :
  forall (x y : int64) a b
         (AMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned x) a)
         (BMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned y) b)
         (CMP : Int64.lt y x = true),
    exists a', exists b',
      signed_int64_filter_greater a b = Some(a', b') /\
        Int64_Modulus_Interval.zmatch (Int64.unsigned x) a' /\
        Int64_Modulus_Interval.zmatch (Int64.unsigned y) b'.
Proof.
  unfold signed_int64_filter_greater. intros.
  destruct (zmatch_signed_int64_filter_less y x b a BMATCH AMATCH CMP) as (b' & a' & RE & MATCHB' & MATCHA' ).
  exists a'. exists b'. rewrite RE. auto.
Qed.
  
Lemma zmatch_signed_int64_filter_greater_equal :
  forall (x y : int64) a b
         (AMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned x) a)
         (BMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned y) b)
         (CMP : Int64.lt x y = false),
    exists a', exists b',
      signed_int64_filter_greater_equal a b = Some(a', b') /\
        Int64_Modulus_Interval.zmatch (Int64.unsigned x) a' /\
        Int64_Modulus_Interval.zmatch (Int64.unsigned y) b'.
Proof.
  unfold signed_int64_filter_greater_equal. intros.
  destruct (zmatch_signed_int64_filter_less_equal y x b a BMATCH AMATCH CMP) as (b' & a' & RE & MATCHB' & MATCHA' ).
  exists a'. exists b'. rewrite RE. auto.
Qed.

Definition filter_Vlong (a : ival) : option Int64_Modulus_Interval.t :=
  match a with
  | Ibot => None
  | Ilong false i => Some i
  | _ => Some Int64_Modulus_Interval.full_range
  end.

Lemma filter_Vlong_sound (i : int64) (a : ival):
  vmatch (Vlong i) a ->
  exists ai,
    filter_Vlong a = Some ai /\ vmatch (Vlong i) (Ilong false ai).
Proof.
  inversion 1; simpl; subst.
  { rewrite if_both_Some.
    eexists; split. reflexivity.
    constructor. destruct b. { apply zmatch_int64_full_range. }
    assumption.
  }
  eexists; split. reflexivity. constructor. apply zmatch_int64_full_range.
Qed.

Definition filter_cmp_Ilong (cmp : comparison) (i0 i1 : Int64_Modulus_Interval.t) : ival * ival :=
  match cmp with
  | Cle =>
      match signed_int64_filter_less_equal i0 i1 with
      | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
      | None => (Ibot, Ibot)
      end
  | Cge =>
      match signed_int64_filter_greater_equal i0 i1 with
      | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
      | None => (Ibot, Ibot)
      end
  | Clt =>
      match signed_int64_filter_less i0 i1 with
      | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
      | None => (Ibot, Ibot)
      end
  | Cgt =>
      match signed_int64_filter_greater i0 i1 with
      | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
      | None => (Ibot, Ibot)
      end
  | Ceq =>
      match Int64_Modulus_Interval.glb_nb i0 i1 with
      | Some i' => ((Ilong false i'), (Ilong false i'))
      | None => (Ibot, Ibot)
      end
  | Cne =>
      match Int64_Modulus_Interval.filter_not_equal i0 i1 with
      | Some(i0', i1') => ((Ilong false i0'), (Ilong false i1'))
      | None => (Ibot, Ibot)
      end
  end.

Lemma filter_cmp_Ilong_sound cmp i0 i1 (x0 x1 : int64)
  (Z0 : Int64_Modulus_Interval.zmatch (Int64.unsigned x0) i0)
  (Z1 : Int64_Modulus_Interval.zmatch (Int64.unsigned x1) i1)
  (CMP : Int64.cmp cmp x0 x1 = true):
  let (a0', a1') := filter_cmp_Ilong cmp i0 i1 in
  vmatch (Vlong x0) a0' /\ vmatch (Vlong x1) a1'.
Proof.
  Local Ltac slv ::= split; constructor; assumption.
  destruct cmp; simpl in *;
    try apply negb_true_iff in CMP.
  - rewrite (Int64.same_if_eq _ _ CMP) in *.
    destruct (Int64_Modulus_Interval.zmatch_glb_nb _ _ _ Z0 Z1)
      as (c & -> & MATCH).
    slv.
  - apply proj_sumbool_false in CMP.
    destruct (Int64_Modulus_Interval.zmatch_filter_not_equal _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (zmatch_signed_int64_filter_less _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (zmatch_signed_int64_filter_less_equal _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (zmatch_signed_int64_filter_greater _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
  - destruct (zmatch_signed_int64_filter_greater_equal _ _ _ _ Z0 Z1 CMP)
      as (i0' & i1' & -> & MATCH0' & MATCH1').
    slv.
Qed.

Definition filter_cmpl (cmp : comparison) (a0 a1 : ival) : ival*ival :=
  match filter_Vlong a0, filter_Vlong a1 with
  | Some i0, Some i1 => filter_cmp_Ilong cmp i0 i1
  | _, _ => (Ibot, Ibot)
  end.

Lemma filter_cmpl_sound (cmp : comparison)
  (a0 a1 : ival) (x0 x1 : val)
  (MATCH0 : vmatch x0 a0) (MATCH1 : vmatch x1 a1)
  (CMP : (Val.cmpl_bool cmp x0 x1) = Some true):
  let (a0', a1') := filter_cmpl cmp a0 a1 in
  vmatch x0 a0' /\ vmatch x1 a1'.
Proof.
  assert (exists xi0 xi1, x0 = Vlong xi0 /\ x1 = Vlong xi1) as (xi0 & xi1 & ? & ?). {
    revert CMP; unfold Val.cmpl_bool.
    destruct x0; try discriminate 1;
    destruct x1; try discriminate 1.
    repeat econstructor.
  }
  subst; unfold filter_cmpl.
  apply filter_Vlong_sound in MATCH0 as (i0 & -> & MATCH0),
                              MATCH1 as (i1 & -> & MATCH1).
  inv MATCH0; inv MATCH1; injection CMP as ?.
  eapply filter_cmp_Ilong_sound; eauto.
Qed.

Definition cmpl_bool (cmp : comparison)
           (a0 a1 : ival) : ibool :=
  match a0, a1 with
  | (Ilong false i0), (Ilong false i1) =>
      match cmp with
      | Cle =>
          Int64_Modulus_Interval.filter_to_eval
            signed_int64_filter_less_equal
            signed_int64_filter_greater i0 i1
      | Cge =>
          Int64_Modulus_Interval.filter_to_eval
            signed_int64_filter_greater_equal
            signed_int64_filter_less i0 i1
      | Clt =>
          Int64_Modulus_Interval.filter_to_eval
            signed_int64_filter_less
            signed_int64_filter_greater_equal i0 i1
      | Cgt =>
          Int64_Modulus_Interval.filter_to_eval
            signed_int64_filter_greater
            signed_int64_filter_less_equal i0 i1
      | Ceq =>
          Int64_Modulus_Interval.filter_to_eval
            Int64_Modulus_Interval.filter_equal
            Int64_Modulus_Interval.filter_not_equal i0 i1
      | Cne =>
          Int64_Modulus_Interval.filter_to_eval
            Int64_Modulus_Interval.filter_not_equal
            Int64_Modulus_Interval.filter_equal
            i0 i1
      end
  | _, _ => Btop
  end.

Lemma int64_filter_to_eval_sound :
 forall (pred : Z.t -> Z.t -> bool)
         (filter : Int64_Modulus_Interval.t ->
                   Int64_Modulus_Interval.t ->
                   option (Int64_Modulus_Interval.t * Int64_Modulus_Interval.t))
       (zmatch_filter : forall (x y : int64) (a b : Int64_Modulus_Interval.t),
        Int64_Modulus_Interval.zmatch (Int64.unsigned x) a ->
        Int64_Modulus_Interval.zmatch (Int64.unsigned y) b ->
        pred (Int64.unsigned x) (Int64.unsigned y) = true ->
        exists a' b' : Int64_Modulus_Interval.t,
          filter a b = Some (a', b') /\
            Int64_Modulus_Interval.zmatch (Int64.unsigned x) a' /\
            Int64_Modulus_Interval.zmatch (Int64.unsigned y) b')
       (filter_not : Int64_Modulus_Interval.t ->
                      Int64_Modulus_Interval.t ->
                      option (Int64_Modulus_Interval.t * Int64_Modulus_Interval.t))
       (zmatch_filter_not : forall (x y : int64) (a b : Int64_Modulus_Interval.t),
        Int64_Modulus_Interval.zmatch (Int64.unsigned x) a ->
        Int64_Modulus_Interval.zmatch (Int64.unsigned y) b ->
        pred (Int64.unsigned x) (Int64.unsigned y) = false ->
        exists a' b' : Int64_Modulus_Interval.t,
          filter_not a b = Some (a', b') /\
            Int64_Modulus_Interval.zmatch (Int64.unsigned x) a' /\
            Int64_Modulus_Interval.zmatch (Int64.unsigned y) b')
       (x y : int64) (a b : Int64_Modulus_Interval.t)
       (AMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned x) a)
       (BMATCH : Int64_Modulus_Interval.zmatch (Int64.unsigned y) b),
       cmatch (Some (pred (Int64.unsigned x) (Int64.unsigned y)))
              (Int64_Modulus_Interval.filter_to_eval filter filter_not a b).
Proof.
  intros.
  unfold Int64_Modulus_Interval.filter_to_eval.
  destruct pred eqn:PRED.
  - pose proof (zmatch_filter _ _ _ _ AMATCH BMATCH PRED) as (a' & b' & RE & MATCHA' & MATCHB').
    rewrite RE.
    destruct filter_not; constructor.
  - pose proof (zmatch_filter_not _ _ _ _ AMATCH BMATCH PRED) as (a' & b' & RE & MATCHA' & MATCHB').
    rewrite RE.
    destruct filter; constructor.
Qed.

Lemma cmpl_bool_sound:
  forall c v w x y, vmatch v x -> vmatch w y ->
    cmatch (Val.cmpl_bool c v w) (cmpl_bool c x y).
Proof.
  intros. unfold Val.cmpl_bool, cmpl_bool.
  inv H; try constructor; inv H0; try rewrite if_same; try constructor.
  destruct c; cbn; destruct b, b0; try constructor.
  - change (Int64.eq l l0) with ((fun x y => if zeq x y then true else false) (Int64.unsigned l) (Int64.unsigned l0)).
    apply Int64_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_equal; auto.
      destruct zeq; congruence.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_not_equal; auto.
      destruct zeq; congruence.
 - change (negb (Int64.eq l l0)) with ((fun x y => negb (if zeq x y then true else false)) (Int64.unsigned l) (Int64.unsigned l0)).
   apply Int64_Modulus_Interval.filter_to_eval_sound; trivial.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_not_equal; auto.
      destruct zeq; cbn in CMP; congruence.
    + intros. apply Int64_Modulus_Interval.zmatch_filter_equal; auto.
      destruct zeq; cbn in CMP; congruence.
 - apply (int64_filter_to_eval_sound
     (fun x y => zlt
           (if zlt x Int64.half_modulus
            then x
            else x - Int64.modulus)
           (if zlt y Int64.half_modulus
            then y
            else y - Int64.modulus))); trivial.
    + intros. apply zmatch_signed_int64_filter_less; auto.
    + intros. apply zmatch_signed_int64_filter_greater_equal; auto.
      
 - apply (int64_filter_to_eval_sound
     (fun y x => negb (zlt
           (if zlt x Int64.half_modulus
            then x
            else x - Int64.modulus)
           (if zlt y Int64.half_modulus
            then y
            else y - Int64.modulus)))); trivial.
   + intros. apply zmatch_signed_int64_filter_less_equal; auto.
     apply negb_true_then_false. exact H3.
     
   + intros. apply zmatch_signed_int64_filter_greater; auto.
     apply negb_false_then_true. exact H3.
     
 - apply (int64_filter_to_eval_sound
     (fun y x => zlt
           (if zlt x Int64.half_modulus
            then x
            else x - Int64.modulus)
           (if zlt y Int64.half_modulus
            then y
            else y - Int64.modulus))); trivial.
   + intros. apply zmatch_signed_int64_filter_greater; auto.
   + intros. apply zmatch_signed_int64_filter_less_equal; auto.
     
 - apply (int64_filter_to_eval_sound
     (fun x y => negb (zlt
           (if zlt x Int64.half_modulus
            then x
            else x - Int64.modulus)
           (if zlt y Int64.half_modulus
            then y
            else y - Int64.modulus)))); trivial.
   + intros. apply zmatch_signed_int64_filter_greater_equal; auto.
     apply negb_true_then_false. exact H3.
   + intros. apply zmatch_signed_int64_filter_less; auto.
     apply negb_false_then_true. exact H3.
Qed.

Definition neg v := sub (intconst (Int.zero)) v.
Lemma neg_sound: forall v x (MATCH : vmatch x v), vmatch (Val.neg x) (neg v).
Proof.
  intros. inv MATCH; cbn in *; try constructor.
  change (Int.unsigned Int.zero) with 0.
  replace (Int.unsigned (Int.neg i)) with ((0 - Int.unsigned i) mod Int.modulus).
  { apply Int_Modulus_Interval.zmatch_sub.
    - apply Int_Modulus_Interval.zmatch_intconst.
    - assumption.
  }
  unfold Int.neg.
  rewrite Int.unsigned_repr_eq.
  reflexivity.
Qed.

Definition negl v := subl (longconst (Int64.zero)) v.
Lemma negl_sound: forall v x (MATCH : vmatch x v), vmatch (Val.negl x) (negl v).
Proof.
  intros. inv MATCH; cbn in *; try constructor.
  change (Int64.unsigned Int64.zero) with 0.
  replace (Int64.unsigned (Int64.neg l)) with ((0 - Int64.unsigned l) mod Int64.modulus).
  { apply Int64_Modulus_Interval.zmatch_sub.
    - apply Int64_Modulus_Interval.zmatch_intconst.
    - assumption.
  }
  unfold Int64.neg.
  rewrite Int64.unsigned_repr_eq.
  reflexivity.
Qed.

Definition int0 := intconst Int.zero.
Definition int1 := intconst Int.one.
Definition int01 := AVal.lub int0 int1.

Definition of_optbool (x : ibool) :=
  match x with
  | Just b => if b then int1 else int0
  | Any_bool => int01
  | _ => Itop
  end.

Lemma of_optbool_sound:
  forall ob ab, cmatch ob ab -> vmatch (Val.of_optbool ob) (of_optbool ab).
Proof.
  intros. inv H; cbn; try constructor.
  - destruct b; constructor; apply Int_Modulus_Interval.zmatch_intconst.
  - destruct b; constructor.
    + apply Int_Modulus_Interval.zmatch_lub_right. apply Int_Modulus_Interval.zmatch_intconst.
    + apply Int_Modulus_Interval.zmatch_lub_left. apply Int_Modulus_Interval.zmatch_intconst.
Qed.

Program Definition longofintu (v: ival) :=
  match v with
  | Iint b i => Ilong b (Int64_Modulus_Interval.mkmod_interval i.(Int_Modulus_Interval.mod_itv) _ _)
  | _ => Itop
  end.
Next Obligation.
  destruct i. cbn. assumption.
Qed.
Next Obligation.
  destruct i. cbn.
  change Int.modulus with (2^32)%Z in *.
  change Int64.modulus with (2^64)%Z in *.
  cbn in *. lia.
Qed.

Lemma longofintu_sound:
  forall v x, vmatch v x -> vmatch (Val.longofintu v) (longofintu x).
Proof.
  unfold Val.longofintu, longofintu; intros; inv H; constructor.
  rewrite Int64.unsigned_repr; cycle 1.
  { pose proof (Int.unsigned_range i).
    change Int.modulus with (2^32)%Z in *.
    change Int64.max_unsigned with (2^64-1)%Z in *.
    cbn in *. lia.
  }
  inv H0.
  constructor; cbn; assumption.
Qed.

Definition loword (x: ival) :=
  match x with
  | Ilong b i => Iint b (Int_Modulus_Interval.force i.(Int64_Modulus_Interval.mod_itv))
  | _ => Itop
  end.

Lemma loword_sound: forall v x (MATCH : vmatch v x),
    vmatch (Val.loword v) (loword x).
Proof.
  intros. inv MATCH; constructor.
  unfold Int64.loword.
  rewrite Int.unsigned_repr_eq.
  apply Int_Modulus_Interval.zmatch_force.
  exact H.
Qed.

Definition longofwords (hi lo : ival) :=
  match hi, lo with
  | (Iint b1 ihi), (Iint b2 ilo) => Ilong (orb b1 b2) Int64_Modulus_Interval.full_range
  | _, _ => Itop
  end.

  
Lemma longofwords_sound:
  forall v w x y (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.longofwords v w) (longofwords x y).
Proof.
  unfold longofwords. intros.
  inv MATCHx; inv MATCHy; try constructor.
  { apply Int64_Modulus_Interval.zmatch_full_range.
    unfold Int64.ofwords.
    apply Int64.unsigned_range. }
  rewrite orb_true_r. constructor.
Qed.
 
Definition shl v1 v2 :=
  match v1, v2 with
  | (Iint false i1), (Iint false i2) =>
      if zlt i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi) Int.zwordsize
      then Iint false (Int_Modulus_Interval.force
             (Interval.shl i1.(Int_Modulus_Interval.mod_itv) i2.(Int_Modulus_Interval.mod_itv)
                           i1.(Int_Modulus_Interval.mod_lo) i2.(Int_Modulus_Interval.mod_lo)))
      else Itop
  | _, _ => Itop
  end.

Lemma shl_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.shl v w) (shl x y).
Proof.
  intros. inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  all: try (rewrite if_same; constructor).
  destruct b; destruct b0; try constructor.
  destruct itv, itv0, mod_itv, mod_itv0; cbn in *.
  inv H; inv H0; cbn in *; unfold Int.ltu.
  change (Int.unsigned Int.iwordsize) with 32.
  destruct zlt; cycle 1.
  { destruct zlt. lia. constructor. }
  destruct zlt. constructor.
  unfold Int.shl. rewrite Int.unsigned_repr_eq.
  apply Int_Modulus_Interval.zmatch_force.
  apply Interval.zmatch_shl; constructor; simpl; assumption.
  constructor.
Qed.

Program Definition shru v1 v2 :=
  match v1, v2 with
  | (Iint false i1), (Iint false i2) =>
      if zlt i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi) Int.zwordsize
      then Iint false (Int_Modulus_Interval.force (Interval.mkinterval
             (Z.shiftr i1.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo)
                       i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi))
             (Z.shiftr i1.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi)
                       i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo)) _))
      else Itop
  | _, _ => Itop
  end.
Next Obligation.
  destruct i1, i2, mod_itv, mod_itv0. cbn in *.
  apply Zle_imp_le_bool.
  repeat (rewrite Z.shiftr_div_pow2 by lia).
  apply Z.le_trans with (m := itv_hi / 2 ^ itv_hi0).
  { apply Z.div_le_mono. nia. lia. }
  apply Z.div_le_compat_l. lia.
  split. nia.
  apply Zpow_facts.Zpower_le_monotone; lia.
Qed.

Lemma shru_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.shru v w) (shru x y).
Proof.
  intros. inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  all: try (destruct b; constructor).
  destruct b, b0; try constructor.
  destruct itv, itv0, mod_itv, mod_itv0; cbn in *.
  inv H; inv H0; cbn in *. unfold Int.ltu.
  change (Int.unsigned Int.iwordsize) with 32.
  destruct zlt; cycle 1.
  { destruct zlt. lia. constructor. }
  destruct zlt; constructor.
  unfold Int.shru. rewrite Int.unsigned_repr_eq.
  apply Int_Modulus_Interval.zmatch_force.
  constructor; cbn; repeat (rewrite Z.shiftr_div_pow2 by lia).
  - apply Z.le_trans with (m := Int.unsigned i / 2 ^ itv_hi0).
    + apply Z.div_le_mono. nia. lia.
    + apply Z.div_le_compat_l. lia.
      split. nia.
      apply Zpow_facts.Zpower_le_monotone; lia.
  - apply Z.le_trans with (m := itv_hi / 2 ^ Int.unsigned i0).
    + apply Z.div_le_mono. nia. lia.
    + apply Z.div_le_compat_l. lia.
      split. nia.
      apply Zpow_facts.Zpower_le_monotone; lia.
Qed.

Program Definition shll v1 v2 :=
  match v1, v2 with
  | (Ilong false i1), (Iint false i2) =>
      if zlt i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi) Int.zwordsize
      then Ilong false (Int64_Modulus_Interval.force (Interval.mkinterval
             (i1.(Int64_Modulus_Interval.mod_itv).(Interval.itv_lo)
                * 2^(i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo)))
             (i1.(Int64_Modulus_Interval.mod_itv).(Interval.itv_hi)
                * 2^(i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi))) _))
      else Itop
  | _, _ => Itop
  end.
Next Obligation.
  destruct i1, i2, mod_itv, mod_itv0. cbn in *.
  apply Zle_imp_le_bool.
  apply Z.mul_le_mono_nonneg. lia. lia. nia.
  apply Zpow_facts.Zpower_le_monotone. lia. lia.
Qed.

Lemma shll_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.shll v w) (shll x y).
Proof.
  intros. inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  all: try (destruct b; constructor).
  destruct b, b0; try constructor.
  destruct itv, itv0, mod_itv, mod_itv0; cbn in *.
  inv H; inv H0; cbn in *. unfold Int.ltu.
  change (Int.unsigned Int64.iwordsize') with 64.
  destruct zlt; cycle 1.
  { destruct zlt. lia. constructor. }
  destruct zlt; constructor.
  unfold Int64.shl'. rewrite Int64.unsigned_repr_eq.
  apply Int64_Modulus_Interval.zmatch_force.
  constructor; cbn; rewrite Z.shiftl_mul_pow2; try lia.
  - apply Z.mul_le_mono_nonneg. lia. lia. nia.
    apply Zpow_facts.Zpower_le_monotone. lia. lia.
  - apply Z.mul_le_mono_nonneg. lia. lia. nia.
    apply Zpow_facts.Zpower_le_monotone. lia. lia.
Qed.

Program Definition shrlu v1 v2 :=
  match v1, v2 with
  | (Ilong false i1), (Iint false i2) =>
      if zlt i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi) Int.zwordsize
      then Ilong false (Int64_Modulus_Interval.force (Interval.mkinterval
             (Z.shiftr i1.(Int64_Modulus_Interval.mod_itv).(Interval.itv_lo)
                       i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi))
             (Z.shiftr i1.(Int64_Modulus_Interval.mod_itv).(Interval.itv_hi)
                       i2.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo)) _))
      else Itop
  | _, _ => Itop
  end.
Next Obligation.
  destruct i1, i2, mod_itv, mod_itv0. cbn in *.
  apply Zle_imp_le_bool.
  repeat (rewrite Z.shiftr_div_pow2 by lia).
  apply Z.le_trans with (m := itv_hi / 2 ^ itv_hi0).
  { apply Z.div_le_mono. nia. lia. }
  apply Z.div_le_compat_l. lia.
  split. nia.
  apply Zpow_facts.Zpower_le_monotone; lia.
Qed.

Lemma shrlu_sound:
  forall v w x y
         (MATCHx : vmatch v x) (MATCHy : vmatch w y),
    vmatch (Val.shrlu v w) (shrlu x y).
Proof.
  intros. inv MATCHx; cbn; try constructor.
  inv MATCHy; cbn; try constructor.
  all: try (destruct b; constructor).
  destruct b, b0; try constructor.
  destruct itv, itv0, mod_itv, mod_itv0; cbn in *.
  inv H; inv H0; cbn in *. unfold Int.ltu.
  change (Int.unsigned Int64.iwordsize') with 64.
  destruct zlt; cycle 1.
  { destruct zlt. lia. constructor. }
  destruct zlt; constructor.
  unfold Int64.shru, Int64.shru'. rewrite Int64.unsigned_repr_eq.
  apply Int64_Modulus_Interval.zmatch_force.
  constructor; cbn; repeat (rewrite Z.shiftr_div_pow2 by lia).
  - apply Z.le_trans with (m := Int64.unsigned l / 2 ^ itv_hi0).
    + apply Z.div_le_mono. nia. lia.
    + apply Z.div_le_compat_l. lia.
      split. nia.
      apply Zpow_facts.Zpower_le_monotone; lia.
  - apply Z.le_trans with (m := itv_hi / 2 ^ Int.unsigned i).
    + apply Z.div_le_mono. nia. lia.
    + apply Z.div_le_compat_l. lia.
      split. nia.
      apply Zpow_facts.Zpower_le_monotone; lia.
Qed.

Definition val_of_ival (a: ival) : val :=
  match a with
  | Iint false itv =>
      if Z.eq_dec itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo)
                  itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi)
      then Vint (Int.repr itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo))
      else Vundef
  | Ilong false itv =>
      if Z.eq_dec itv.(Int64_Modulus_Interval.mod_itv).(Interval.itv_lo)
                  itv.(Int64_Modulus_Interval.mod_itv).(Interval.itv_hi)
      then Vlong (Int64.repr itv.(Int64_Modulus_Interval.mod_itv).(Interval.itv_lo))
      else Vundef
  | _ => Vundef
  end.

Definition ival_of_val (v: val) : option ival :=
  match v with
  | Vint n => Some (intconst n)
  | Vlong n => Some (longconst n)
  | Vfloat f => Some Itop
  | Vsingle f => Some Itop
  | _ => None
  end.

Lemma val_of_ival_sound:
  forall v a (MATCH : vmatch v a), Val.lessdef (val_of_ival a) v.
Proof.
  intros. unfold val_of_ival. inv MATCH; try constructor.
  - destruct b. constructor.
    destruct Z.eq_dec.
    + inv H. destruct itv ; destruct mod_itv; cbn in *.
      replace itv_lo with (Int.unsigned i) by lia.
      rewrite Int.repr_unsigned. constructor.
    + constructor.
  - destruct b. constructor.
    destruct Z.eq_dec.
    + inv H. destruct itv ; destruct mod_itv; cbn in *.
      replace itv_lo with (Int64.unsigned l) by lia.
      rewrite Int64.repr_unsigned. constructor.
    + constructor.
Qed.

Corollary list_val_of_ival_sound:
  forall vl al (MATCHL : list_forall2 vmatch vl al),
    Val.lessdef_list (map val_of_ival al) vl.
Proof.
  induction 1; simpl; constructor; auto using val_of_ival_sound.
Qed.

Lemma ival_of_val_sound:
  forall v a (CONV: ival_of_val v = Some a), vmatch v a.
Proof.
  intros v a E; destruct v; simpl in E; inv E; auto with ival.
  apply intconst_sound. apply longconst_sound.
Qed.

Definition option_val_of_ival (a: ival) : option val :=
  match a with
  | Iint false itv =>
      if Z.eq_dec itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo)
                  itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi)
      then Some (Vint (Int.repr itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_lo)))
      else None
  | Ilong false itv =>
      if Z.eq_dec itv.(Int64_Modulus_Interval.mod_itv).(Interval.itv_lo)
                  itv.(Int64_Modulus_Interval.mod_itv).(Interval.itv_hi)
      then Some (Vlong (Int64.repr itv.(Int64_Modulus_Interval.mod_itv).(Interval.itv_lo)))
      else None
  | _ => None
  end.

Lemma option_val_of_ival_sound:
  forall v a (MATCH : vmatch v a) w (FOUND: option_val_of_ival a = Some w),
    v = w.
Proof.
  unfold option_val_of_ival. intros.
  inv MATCH; try discriminate.
  - destruct b. discriminate.
    destruct Z.eq_dec. 2: discriminate.
    inv FOUND. f_equal.
    destruct H.
    replace (Interval.itv_lo _) with (Int.unsigned i) by lia.
    symmetry. apply Int.repr_unsigned.
  - destruct b. discriminate.
    destruct Z.eq_dec. 2: discriminate.
    inv FOUND. f_equal.
    destruct H.
    replace (Interval.itv_lo _) with (Int64.unsigned l) by lia.
    symmetry. apply Int64.repr_unsigned.
Qed.

Definition normalize (v: ival) (ty: AST.typ) : ival :=
  match v, ty with
  | (Iint _ _), AST.Tint
  | (Ilong _ _), AST.Tlong
  | Ibot, _ => v
  | _, _ => Itop
  end.

Lemma normalize_sound : forall x v (MATCH : vmatch x v) (ty: AST.typ),
    vmatch (Val.normalize x ty) (normalize v ty).
Proof.
  intros. inv MATCH; cbn.
  all: destruct ty; constructor; trivial.
Qed.

Definition select (ab: ibool) (x y: ival) (ty : AST.typ) :=
  match ab with
  | Bnone | Btop => Itop
  | Just b => normalize (if b then x else y) ty
  | Any_bool => normalize (ilub x y) ty
  end.

Lemma select_sound:
  forall ob v w ab x y ty
  (CMATCH : cmatch ob ab) (VMATCHx : vmatch v x) (VMATCHy : vmatch w y),
  vmatch (Val.select ob v w ty) (select ab x y ty).
Proof.
  intros. unfold Val.select.
  inv CMATCH; cbn; try constructor.
  - destruct b; apply normalize_sound; assumption.
  - destruct b; apply normalize_sound.
    + eapply vmatch_ge. apply ige_lub_left. assumption.
    + eapply vmatch_ge. apply ige_lub_right. assumption.
Qed.

Definition int_is_nonnegative (iv : ival) : bool :=
  match iv with
  | Iint _ itv => zlt itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi) Int.half_modulus
  | Itop => false
  | _ => true
  end.

Lemma int_is_nonnegative_sound:
  forall x iv (MATCH : vmatch (Vint x) iv)
         (COND : int_is_nonnegative iv = true),
    Int.signed x >= 0.
Proof.
  unfold int_is_nonnegative, Int.signed.
  intros.
  pose proof (Int.unsigned_range x) as RANGE.
  inv MATCH.
  - destruct H0. destruct zlt; destruct zlt; cbn in *; lia.
  - discriminate.
Qed.

Definition long_is_nonnegative (iv : ival) : bool :=
  match iv with
  | Ilong _ itv => zlt itv.(Int64_Modulus_Interval.mod_itv).(Interval.itv_hi) Int64.half_modulus
  | Itop => false
  | _ => true
  end.

Lemma long_is_nonnegative_sound:
  forall x iv (MATCH : vmatch (Vlong x) iv)
         (COND : long_is_nonnegative iv = true),
    Int64.signed x >= 0.
Proof.
  unfold long_is_nonnegative, Int64.signed.
  intros.
  pose proof (Int64.unsigned_range x) as RANGE.
  inv MATCH.
  - destruct H0. destruct zlt; destruct zlt; cbn in *; lia.
  - discriminate.
Qed.

Definition int_is_zero (iv : ival) : bool :=
  match iv with
  | Iint _ itv => zeq itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi) 0
  | Itop => false
  | _ => true
  end.

Lemma int_is_zero_sound:
  forall x iv (MATCH : vmatch (Vint x) iv)
         (COND : int_is_zero iv = true),
    Int.unsigned x = 0.
Proof.
  unfold int_is_zero. intros.
  inv MATCH. 2: discriminate. inv H0.
  pose proof (Int.unsigned_range x).
  destruct zeq. lia. discriminate.
Qed.

Definition is_int_zero (iv : ival) : bool :=
  match iv with
  | Iint false itv => zeq itv.(Int_Modulus_Interval.mod_itv).(Interval.itv_hi) 0
  | _ => false
  end.

Lemma is_int_zero_sound:
  forall v iv (MATCH : vmatch v iv)
         (COND : is_int_zero iv = true),
    v = (Vint Int.zero).
Proof.
  unfold is_int_zero. intros.
  inv MATCH. all: try discriminate.
  destruct b. discriminate.
  destruct zeq. 2: discriminate. inv H.
  pose proof (Int.unsigned_range i).
  assert (Int.unsigned i = 0) as ZERO by lia.
  rewrite <- (Int.repr_unsigned i).
  rewrite ZERO.
  reflexivity.
Qed.

Definition is_long_zero (iv : ival) : bool :=
  match iv with
  | Ilong false itv => zeq itv.(Int64_Modulus_Interval.mod_itv).(Interval.itv_hi) 0
  | _ => false
  end.

Lemma is_long_zero_sound:
  forall v iv (MATCH : vmatch v iv)
         (COND : is_long_zero iv = true),
    v = (Vlong Int64.zero).
Proof.
  unfold is_long_zero. intros.
  inv MATCH. all: try discriminate.
  destruct b. discriminate.
  destruct zeq. 2: discriminate. inv H.
  pose proof (Int64.unsigned_range l).
  assert (Int64.unsigned l = 0) as ZERO by lia.
  rewrite <- (Int64.repr_unsigned l).
  rewrite ZERO.
  reflexivity.
Qed.
  
Module AE := LPWMap(AVal).

Definition aenv := AE.t.

Definition ematch (e: regset) (ae: aenv) : Prop :=
  forall r, vmatch e#r (AE.get r ae).

Lemma ematch_ge:
  forall e ae1 ae2,
  ematch e ae1 -> AE.ge ae2 ae1 -> ematch e ae2.
Proof.
  intros; red; intros. apply vmatch_ge with (AE.get r ae1); auto. apply H0.
Qed.

Lemma ematch_update:
  forall e ae v av r,
  ematch e ae -> vmatch v av -> ematch (e#r <- v) (AE.set r av ae).
Proof.
  intros; red; intros. rewrite AE.gsspec. rewrite PMap.gsspec.
  destruct (peq r0 r); auto.
  red; intros. specialize (H xH). subst ae. simpl in H. inv H.
  unfold AVal.eq; red; intros. subst av. inv H0.
Qed.

Fixpoint einit_regs (rl: list reg) : aenv :=
  match rl with
  | r1 :: rs => AE.set r1 Itop (einit_regs rs)
  | nil => AE.top
  end.

Lemma ematch_init:
  forall rl vl,
  (forall v, In v vl -> vmatch v Itop) ->
  ematch (init_regs vl rl) (einit_regs rl).
Proof.
  induction rl; simpl; intros.
- red; intros. rewrite Regmap.gi. simpl.
  constructor.
- destruct vl as [ | v1 vs ].
  + assert (ematch (init_regs nil rl) (einit_regs rl)).
    { apply IHrl. simpl; tauto. }
    replace (init_regs nil rl) with (Regmap.init Vundef) in H0 by (destruct rl; auto).
    red; intros. rewrite AE.gsspec. destruct (peq r a).
    rewrite Regmap.gi. constructor.
    apply H0.
    red; intros EQ; rewrite EQ in H0. specialize (H0 xH). simpl in H0. inv H0.
    unfold AVal.eq, AVal.bot. congruence.
  + assert (ematch (init_regs vs rl) (einit_regs rl)).
    { apply IHrl. eauto with coqlib. }
    red; intros. rewrite Regmap.gsspec. rewrite AE.gsspec. destruct (peq r a).
    auto with coqlib.
    apply H0.
    red; intros EQ; rewrite EQ in H0. specialize (H0 xH). simpl in H0. inv H0.
    unfold AVal.eq, AVal.bot. congruence.
Qed.

Fixpoint eforget (rl: list reg) (ae: aenv) {struct rl} : aenv :=
  match rl with
  | nil => ae
  | r1 :: rs => eforget rs (AE.set r1 Itop ae)
  end.

Lemma eforget_ge:
  forall rl ae, AE.ge (eforget rl ae) ae.
Proof.
  unfold AE.ge; intros. revert rl ae; induction rl; intros; simpl.
  apply AVal.ge_refl. apply AVal.eq_refl.
  destruct ae. unfold AE.get at 2. apply AVal.ge_bot.
  eapply AVal.ge_trans. apply IHrl. rewrite AE.gsspec.
  destruct (peq p a). apply AVal.ge_top. apply AVal.ge_refl. apply AVal.eq_refl.
  congruence.
  unfold AVal.eq, AVal.bot. congruence.
Qed.

Lemma ematch_forget:
  forall e rl ae, ematch e ae -> ematch e (eforget rl ae).
Proof.
  intros. eapply ematch_ge; eauto. apply eforget_ge.
Qed.

Lattice for dataflow analysis


Module Interval_Analysis := ADD_BOTTOM_WITH_WIDENING(AE).

Global Hint Resolve vmatch_glb zmatch_intconst zmatch_longconst intconst_sound longconst_sound any_int_sound any_long_sound add_sound sub_sound mul_sound addl_sound subl_sound mull_sound neg_sound negl_sound cmpu_bool_sound cmplu_bool_sound of_optbool_sound shl_sound shll_sound shru_sound shrlu_sound loword_sound longofintu_sound longofwords_sound normalize_sound select_sound ematch_update: ival.
Global Hint Constructors cmatch : ival.
Generated by coq2html