Module IntervalDomain

Require Import Coqlib Utf8.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Op.
Require Import z_extra_props.
Require Import LatticeSignatures.
Require Import DLib.

Module Interval.

  Record itv : Type := ITV { min: Z; max: Z }.
  Definition t := itv.

  Definition order (i1 i2: itv) : bool :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        zle min2 min1 && zle max1 max2
    end.

  Definition join (i1 i2: itv) : itv :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        (ITV (Zmin min1 min2) (Zmax max1 max2))
    end.

  Definition widen_classic (i1 i2: itv) : itv :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        ITV
        (if zle min1 min2 then min1 else Int.min_signed)
 (if zle max2 max1 then max1 else Int.max_signed)
    end.

  Fixpoint next_pow2_pos (p:positive) :=
    match p with
    | xH => xH
    | xI p
    | xO p => xI (next_pow2_pos p)
    end.

  Definition previous_pow2_pos p :=
    let p' := next_pow2_pos p in
     match p' with
       | xI p => p
       | _ => p'
     end.

  Definition next_threshold (z:Z) :=
    match z with
      | Z0 => Z0
      | Zpos xH => Zpos xH
      | Zneg xH => Zneg xH
      | Zpos p => Zpos (next_pow2_pos p)
      | Zneg p => Zneg (previous_pow2_pos p)
    end.

  Definition previous_threshold (z:Z) :=
    match z with
      | Z0 => Z0
      | Zpos xH => Zpos xH
      | Zneg xH => Zneg xH
      | Zpos p => Zpos (previous_pow2_pos p)
      | Zneg p => Zneg (next_pow2_pos p)
    end.

  Definition widen (i1 i2: itv) : itv :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        ITV
        (if zle min1 min2 then min1
          else previous_threshold min2)
 (if zle max2 max1 then max1
          else next_threshold max2)
    end.

  Parameter next_smaller : Z -> Z.
  Parameter next_larger : Z -> Z.
  
  Definition widen_heuristic (i1 i2: itv) : itv :=
    match i1, i2 with
      | (ITV min1 max1), (ITV min2 max2) =>
        ITV
        (if zle min1 min2 then min1
          else next_smaller min2)
 (if zle max2 max1 then max1
          else next_larger max2)
    end.


  Definition top : itv := (ITV Int.min_signed Int.max_signed).
  Definition utop : itv := (ITV 0 Int.max_unsigned).

  Definition gamma (i:itv) (v:int) : Prop :=
    min i <= Int.signed v <= max i.

  Lemma gamma_top : forall v,
    gamma top v.

  Lemma gamma_monotone : forall ab1 ab2,
    order ab1 ab2 = true -> forall v, gamma ab1 v -> gamma ab2 v.

  Lemma join_correct : forall (i1 i2:itv) i,
    gamma i1 i \/ gamma i2 i ->
    gamma (join i1 i2) i.

  Instance signed_itv_adom : adom itv int :=
  { leb := order;
    top := top;
    join := join;
    widen := widen_heuristic;
    gamma := gamma;
    gamma_monotone := gamma_monotone;
    gamma_top := gamma_top
   ;join_sound := join_correct
   }.

  Definition itvbot := itv+⊥.

  Definition reduce (min max : Z) : itvbot :=
    if zle min max then NotBot (ITV min max) else Bot.

  Definition meet (i1: itv) (i2:itvbot) : itvbot :=
    match i2 with
      | Bot => Bot
      | NotBot i2 =>
        match i1, i2 with
          | (ITV min1 max1), (ITV min2 max2) =>
            reduce (Zmax min1 min2) (Zmin max1 max2)
        end
    end.
  Notation "x ⊓ y" := (meet x y) (at level 40).

  Definition repr (i:itv) : itv :=
    if leb i top then i else top.

  Definition signed (n:int) : itv :=
    let z := Int.signed n in
      (ITV z z).

  Definition neg (i:itv) : itv :=
    match i with
      | (ITV min max) =>
        repr (ITV (-max) (-min))
    end.

  Definition mult (i1 i2:itv) : itv :=
    let min1 := min i1 in
    let min2 := min i2 in
    let max1 := max i1 in
    let max2 := max i2 in
    let b1 := min1 * min2 in
    let b2 := min1 * max2 in
    let b3 := max1 * min2 in
    let b4 := max1 * max2 in
      repr (ITV
               (Zmin (Zmin b1 b4) (Zmin b3 b2))
               (Zmax (Zmax b1 b4) (Zmax b3 b2))).

  Definition add (i1 i2:itv) : itv :=
    repr (ITV ((min i1)+(min i2)) ((max i1)+(max i2))).

  Definition sub (i1 i2:itv) : itv :=
    repr (ITV ((min i1)-(max i2)) ((max i1)-(min i2))).

  Definition not (i:itv) : itv :=
    add (neg i) (signed Int.mone).

  Definition contains (x:int) (i:itv) : bool :=
    let (min,max) := i in
      let x := Int.signed x in
      zle min x && zle x max.

  Definition is_singleton (v:itv) : option int :=
    let (min,max) := v in
      if zeq min max then Some (Int.repr min) else None.

  Definition is_bool (v:itv) : option bool :=
    let (min,max) := v in
      if zeq min max then
        let x := Int.repr min in
          if Int.eq x Int.zero then Some false
          else if Int.eq x Int.one then Some true
            else None
        else None.

  Definition booleans :=
    join (signed Int.zero) (signed Int.one).

  Definition notbool (i:itv) : itv :=
    match is_singleton i with
      | Some i =>
        if zeq Z0 (Int.unsigned i) then signed Int.one else signed Int.zero
      | None =>
        if contains Int.zero i then booleans else signed Int.zero
    end.

  Definition boolval (i:itv) : itv :=
    match is_singleton i with
      | Some i =>
        if zeq Z0 (Int.unsigned i) then signed Int.zero else signed Int.one
      | None =>
        if contains Int.zero i then booleans else signed Int.one
    end.

  Definition div (v1 v2:itv) : itv :=
    match is_singleton v2 with
      | Some i2 =>
        let (a,b) := v1 in
        let i2 := Int.signed i2 in
          if zlt 0 i2 then
            ITV (Int.Zdiv_round a i2) (Int.Zdiv_round b i2)
            else top
      | None => top
    end.

  Definition shl (v1 v2:itv) : itv :=
    match is_singleton v2 with
      | Some i2 => mult v1 (signed (Int.shl Int.one i2))
      | None => top
    end.

  Definition backward_eq (i1 i2:itv) : itvbot * itvbot :=
    (meet i1 (NotBot i2), meet i1 (NotBot i2)).

  Definition backward_lt (i1 i2:itv) : itvbot * itvbot :=
        (meet i1 (reduce Int.min_signed ((max i2)-1)),
          meet i2 (reduce ((min i1)+1) Int.max_signed))
    .

  Definition backward_ne (i1 i2:itv) : itvbot * itvbot :=
    let (i1',i2') := backward_lt i1 i2 in
      let (i2'',i1'') := backward_lt i2 i1 in
        (i1' ⊔ i1'',i2' ⊔ i2'').

  Definition backward_le (i1 i2:itv) : itvbot * itvbot :=
    (meet i1 (reduce Int.min_signed (max i2)),
      meet i2 (reduce (min i1) Int.max_signed))
    .

  Definition is_in_interval (a b : Z) (ab:itv) : bool :=
    ab ⊑ (ITV a b).

  Definition cast_int16u : Interval.t-> bool := is_in_interval 0 65535.

  Definition backward_leu (i1 i2:itv) : itvbot * itvbot :=
    if cast_int16u i1 && cast_int16u i2
      then backward_le i1 i2
      else (NotBot i1, NotBot i2).

  Definition backward_ltu (i1 i2:itv) : itvbot * itvbot :=
    if cast_int16u i1 && cast_int16u i2
      then backward_lt i1 i2
      else (NotBot i1, NotBot i2).

  Lemma meet_correct: forall (ab1:itv) (ab2:itvbot) v,
    γ ab1 v -> γ ab2 v -> γ (meet ab1 ab2) v.

  Definition meet' (ab1 ab2:itvbot) : itvbot :=
    match ab1 with
      | Bot => Bot
      | NotBot ab1 => meet ab1 ab2
    end.

  Lemma meet'_correct: forall (ab1 ab2:itvbot) v,
    γ ab1 v -> γ ab2 v -> γ (meet' ab1 ab2) v.

  Lemma neg_correct : forall ab i,
    γ ab i ->
    γ (neg ab) (Int.neg i).

  Lemma signed_correct: forall i, γ (signed i) i.


  Lemma bool_correct_zero : γ booleans Int.zero.

  Lemma bool_correct_one : γ booleans Int.one.

  Lemma is_in_interval_correct : forall a b ab,
    is_in_interval a b ab = true ->
    forall i, γ ab i -> a <= Int.signed i <= b.

  Lemma add_correct : forall ab1 ab2 i1 i2,
    γ ab1 i1 -> γ ab2 i2 ->
    γ (add ab1 ab2) (Int.add i1 i2).

  Lemma not_correct : forall ab i,
    γ ab i -> γ (not ab) (Int.not i).

  Lemma sub_correct : forall ab1 ab2 i1 i2,
    γ ab1 i1 -> γ ab2 i2 ->
    γ (sub ab1 ab2) (Int.sub i1 i2).

  Lemma mul_correct : forall ab1 ab2 i1 i2,
    γ ab1 i1 -> γ ab2 i2 ->
    γ (mult ab1 ab2) (Int.mul i1 i2).

  Lemma is_singleton_correct : forall i n n',
    γ i n -> is_singleton i = Some n' -> n'=n.

  Definition of_bool (b: bool): int :=
    if b then Int.one else Int.zero.

  Lemma is_bool_correct : forall i n b,
    γ i n -> is_bool i = Some b -> n = of_bool b.

  Definition is_a_boolean (i:itv) : bool :=
    is_in_interval 0 1 i.

  Lemma is_a_boolean_correct: forall i n,
    γ i n ->
    is_a_boolean i = true ->
    n = Int.zero \/ n = Int.one.

  Lemma is_a_boolean_correct_extra: forall i n,
    γ i n ->
    is_a_boolean i = true ->
    0 <= min i /\ max i <= 1.

  Lemma is_a_boolean_correct_zero: forall i n,
    γ i n ->
    is_a_boolean i = true ->
    (max i) = 0 ->
    n = Int.zero.

  Lemma is_a_boolean_correct_one: forall i n,
    γ i n ->
    is_a_boolean i = true ->
    (min i) = 1 ->
    n = Int.one.

  Definition bool_op (f:int->int->int) (i1 i2:itv) : itv :=
    match is_singleton i1, is_singleton i2 with
      | Some i1, Some i2 => signed (f i1 i2)
      | _ , _ =>
        if is_a_boolean i1 && is_a_boolean i2 then booleans else top
    end.

  Definition IsBool (n:int) : Prop :=
    n = Int.zero \/ n = Int.one.

  Lemma IsBool_booleans: forall n,
    IsBool n -> γ booleans n.

  Lemma bool_op_correct : forall f,
    (forall x y, IsBool x -> IsBool y -> IsBool (f x y)) ->
    forall ab1 ab2 i1 i2,
      γ ab1 i1 -> γ ab2 i2 ->
      γ (bool_op f ab1 ab2) (f i1 i2).

  Definition and : itv -> itv -> itv := bool_op Int.and.
  Definition or : itv -> itv -> itv := bool_op Int.or.
  Definition xor : itv -> itv -> itv := bool_op Int.xor.

  Lemma and_correct : forall ab1 ab2 i1 i2,
    γ ab1 i1 -> γ ab2 i2 ->
    γ (and ab1 ab2) (Int.and i1 i2).

  Lemma or_correct : forall ab1 ab2 i1 i2,
    γ ab1 i1 -> γ ab2 i2 ->
    γ (or ab1 ab2) (Int.or i1 i2).

  Lemma xor_correct : forall ab1 ab2 i1 i2,
    γ ab1 i1 -> γ ab2 i2 ->
    γ (xor ab1 ab2) (Int.xor i1 i2).

  Lemma shl_correct : forall ab1 ab2 i1 i2,
    γ ab1 i1 -> γ ab2 i2 ->
    γ (shl ab1 ab2) (Int.shl i1 i2).

  Lemma divs_correct : forall ab1 ab2 i1 i2,
    γ ab1 i1 -> γ ab2 i2 ->
    γ (div ab1 ab2) (Int.divs i1 i2).

  Lemma contains_correct : forall x ab,
    if contains x ab then γ ab x else ~ γ ab x.

  Lemma notbool_correct : forall ab i,
    γ ab i -> γ (notbool ab) (of_bool (Int.eq i Int.zero)).

  Lemma boolval_correct : forall ab i,
    γ ab i -> γ (boolval ab) (of_bool (negb (Int.eq i Int.zero))).

  Lemma gamma_backward_eq: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_eq ab1 ab2 = (ab1',ab2') ->
    γ ab1 i1 ->
    γ ab2 i2 ->
    Int.eq i1 i2 = true ->
    γ ab1' i1 /\ γ ab2' i2.
  Transparent meet.

  Definition remove (it:itv) (i:int) : itvbot :=
    let (min,max) := it in
      let i := Int.signed i in
      if zeq i min then
        meet it (reduce (min+1) Int.max_signed)
        else if zeq i max then
          meet it (reduce Int.min_signed (max-1))
          else NotBot it.

  Lemma remove_correct : forall ab i0 i,
    γ ab i -> Int.eq i i0 = false -> γ (remove ab i0) i.

 Definition backward_boolval (iin:itv) (out:itv) : itvbot :=
   match is_singleton out with
     | None => NotBot iin
     | Some i =>
       if Int.eq i Int.zero then NotBot (signed Int.zero)
         else if Int.eq i Int.one then
           remove iin Int.zero
         else NotBot iin
   end.

  Lemma backward_boolval_correct : forall ab1 ab2 i,
    γ ab1 i ->
    γ ab2 (of_bool (negb (Int.eq i Int.zero))) ->
    γ (backward_boolval ab1 ab2) i.

 Definition backward_notbool (iin:itv) (out:itv) : itvbot :=
   match is_singleton out with
     | None => NotBot iin
     | Some i =>
       if Int.eq i Int.one then NotBot (signed Int.zero)
         else if Int.eq i Int.zero then
           remove iin Int.zero
         else NotBot iin
   end.

  Lemma backward_notbool_correct : forall ab1 ab2 i,
    γ ab1 i ->
    γ ab2 (of_bool (Int.eq i Int.zero)) ->
    γ (backward_notbool ab1 ab2) i.

 Definition backward_neg (iin:itv) (out:itv) : itvbot :=
   meet iin (NotBot (neg out)).

  Lemma backward_neg_correct : forall ab1 ab2 i,
    γ ab1 i ->
    γ ab2 (Int.neg i) ->
    γ (backward_neg ab1 ab2) i.

 Definition backward_not (iin:itv) (out:itv) : itvbot :=
   meet iin (NotBot (not out)).

  Lemma backward_not_correct : forall ab1 ab2 i,
    γ ab1 i ->
    γ ab2 (Int.not i) ->
    γ (backward_not ab1 ab2) i.


Lemma max_signed_unsigned: Int.max_unsigned = 2*Int.max_signed + 1.

Definition backward_add (ab1 ab2 res:itv) : itvbot * itvbot :=
  (meet ab1 (NotBot (sub res ab2)),
    meet ab2 (NotBot (sub res ab1))).

Lemma add_sub: forall i1 i2:int,
  (Int.sub (Int.add i1 i2) i2) = i1.

Lemma backward_add_correct : forall ab1 ab2 res i1 i2,
  γ ab1 i1 ->
  γ ab2 i2 ->
  γ res (Int.add i1 i2) ->
  γ (fst (backward_add ab1 ab2 res)) i1 /\
  γ (snd (backward_add ab1 ab2 res)) i2.

Definition backward_sub (ab1 ab2 res:itv) : itvbot * itvbot :=
  (meet ab1 (NotBot (add res ab2)),
    meet ab2 (NotBot (sub ab1 res))).

Lemma add_sub2: forall i1 i2:int,
  (Int.add (Int.sub i1 i2) i2) = i1.

Lemma add_sub3: forall i1 i2:int,
  (Int.sub i1 (Int.sub i1 i2)) = i2.

Lemma backward_sub_correct : forall ab1 ab2 res i1 i2,
  γ ab1 i1 ->
  γ ab2 i2 ->
  γ res (Int.sub i1 i2) ->
  γ (fst (backward_sub ab1 ab2 res)) i1 /\
  γ (snd (backward_sub ab1 ab2 res)) i2.

Definition backward_and (ab1 ab2 res:itv) : list (itvbot * itvbot) :=
  if is_a_boolean ab1 && is_a_boolean ab2 then
    match is_singleton res with
      | None => (NotBot ab1,NotBot ab2) :: nil
      | Some i =>
        if Int.eq i Int.one then
          (meet ab1 (NotBot (signed Int.one)),
            meet ab2 (NotBot (signed Int.one))) ::nil
          else if Int.eq i Int.zero then
            (NotBot ab1,meet ab2 (NotBot (signed Int.zero))) ::
            (meet ab1 (NotBot (signed Int.zero)), NotBot ab2) :: nil
            else (NotBot ab1,NotBot ab2) :: nil
    end
    else (NotBot ab1,NotBot ab2) :: nil.


Lemma backward_and_correct : forall ab1 ab2 res i1 i2,
  γ ab1 i1 ->
  γ ab2 i2 ->
  γ res (Int.and i1 i2) ->
  exists ab, In ab (backward_and ab1 ab2 res) /\
    γ (fst ab) i1 /\
    γ (snd ab) i2.

Definition backward_or (ab1 ab2 res:itv) : list (itvbot * itvbot) :=
  if is_a_boolean ab1 && is_a_boolean ab2 then
    match is_singleton res with
      | None => (NotBot ab1,NotBot ab2) :: nil
      | Some i =>
        if Int.eq i Int.zero then
          (meet ab1 (NotBot (signed Int.zero)),
            meet ab2 (NotBot (signed Int.zero))) ::nil
          else if Int.eq i Int.one then
            (NotBot ab1,meet ab2 (NotBot (signed Int.one))) ::
            (meet ab1 (NotBot (signed Int.one)), NotBot ab2) :: nil
            else (NotBot ab1,NotBot ab2) :: nil
    end
    else (NotBot ab1,NotBot ab2) :: nil.

Lemma backward_or_correct : forall ab1 ab2 res i1 i2,
  γ ab1 i1 ->
  γ ab2 i2 ->
  γ res (Int.or i1 i2) ->
  exists ab, In ab (backward_or ab1 ab2 res) /\
    γ (fst ab) i1 /\
    γ (snd ab) i2.

  Lemma gamma_backward_lt: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_lt ab1 ab2 = (ab1',ab2') ->
    γ ab1 i1 ->
    γ ab2 i2 ->
    Int.lt i1 i2 = true ->
    γ ab1' i1 /\ γ ab2' i2.

  Lemma gamma_backward_ne: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_ne ab1 ab2 = (ab1',ab2') ->
    γ ab1 i1 ->
    γ ab2 i2 ->
    negb (Int.eq i1 i2) = true ->
    γ ab1' i1 /\ γ ab2' i2.

  Lemma gamma_backward_le: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_le ab1 ab2 = (ab1',ab2') ->
    γ ab1 i1 ->
    γ ab2 i2 ->
    negb (Int.lt i2 i1) = true ->
    γ ab1' i1 /\ γ ab2' i2.


  Lemma cast_int16u_correct: forall ab i,
    cast_int16u ab = true ->
    γ ab i ->
    Int.signed i = Int.unsigned i.


  Lemma gamma_backward_leu: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_leu ab1 ab2 = (ab1',ab2') ->
    γ ab1 i1 ->
    γ ab2 i2 ->
    negb (Int.ltu i2 i1) = true ->
    γ ab1' i1 /\ γ ab2' i2.

  Lemma gamma_backward_ltu: forall ab1 ab2 ab1' ab2' i1 i2,
    backward_ltu ab1 ab2 = (ab1',ab2') ->
    γ ab1 i1 ->
    γ ab2 i2 ->
    Int.ltu i1 i2 = true ->
    γ ab1' i1 /\ γ ab2' i2.


Definition swap {A} (xy:A*A) : A*A :=
  let (x,y) := xy in (y,x).

Definition backward_cmp (c:comparison) (ab1 ab2 res:itv) : itvbot * itvbot :=
  match is_singleton res with
    | None => (NotBot ab1,NotBot ab2)
    | Some i =>
      if Int.eq i Int.one then
        match c with
          | Ceq => let ab := meet ab1 (NotBot ab2) in (ab,ab)
          | Cne => backward_ne ab1 ab2
          | Clt => backward_lt ab1 ab2
          | Cle => backward_le ab1 ab2
          | Cgt => swap (backward_lt ab2 ab1)
          | Cge => swap (backward_le ab2 ab1)
        end
        else if Int.eq i Int.zero then
        match c with
          | Ceq => backward_ne ab1 ab2
          | Cne => let ab := meet ab1 (NotBot ab2) in (ab,ab)
          | Cge => backward_lt ab1 ab2
          | Cgt => backward_le ab1 ab2
          | Cle => swap (backward_lt ab2 ab1)
          | Clt => swap (backward_le ab2 ab1)
        end
        else (NotBot ab1,NotBot ab2)
    end.

Lemma pair_eq : forall A B (x:A*B), x = (fst x, snd x).
Hint Resolve pair_eq.

Lemma swap_inv {A} (x:A*A) (u v: A) : swap x = (u,v) -> x = (v,u).

Opaque meet.
Lemma backward_cmp_correct : forall c ab1 ab2 res i1 i2,
  γ ab1 i1 ->
  γ ab2 i2 ->
  γ res (of_bool (Int.cmp c i1 i2)) ->
  let '(u,v) := backward_cmp c ab1 ab2 res in
  γ u i1 /\ γ v i2.

Definition backward_cmpu (c:comparison) (ab1 ab2 res:itv) : itvbot * itvbot :=
  match is_singleton res with
    | None => (NotBot ab1,NotBot ab2)
    | Some i =>
      if Int.eq i Int.one then
        match c with
          | Ceq => let ab := meet ab1 (NotBot ab2) in (ab,ab)
          | Cne => backward_ne ab1 ab2
          | Clt => backward_ltu ab1 ab2
          | Cle => backward_leu ab1 ab2
          | Cgt => swap (backward_ltu ab2 ab1)
          | Cge => swap (backward_leu ab2 ab1)
        end
        else if Int.eq i Int.zero then
        match c with
          | Ceq => backward_ne ab1 ab2
          | Cne => let ab := meet ab1 (NotBot ab2) in (ab,ab)
          | Cge => backward_ltu ab1 ab2
          | Cgt => backward_leu ab1 ab2
          | Cle => swap (backward_ltu ab2 ab1)
          | Clt => swap (backward_leu ab2 ab1)
        end
        else (NotBot ab1,NotBot ab2)
    end.

Lemma backward_cmpu_correct : forall c ab1 ab2 res i1 i2,
  γ ab1 i1 ->
  γ ab2 i2 ->
  γ res (of_bool (Int.cmpu c i1 i2)) ->
  let '(u,v) := backward_cmpu c ab1 ab2 res in
  γ u i1 /\ γ v i2.

  Hint Resolve gamma_top signed_correct.

  Definition ugamma (i:itv) (v:int) : Prop :=
    min i <= Int.unsigned v <= max i.

  Definition reduc2signed (i:itv) : itv :=
    match i with
      | ITV m M =>
        if zlt M Int.half_modulus
        then i
        else if zle Int.half_modulus m
             then ITV (m - Int.modulus) (M - Int.modulus)
             else ⊤
    end.
  Definition reduc2unsigned (i: itv) : itv :=
    match i with
      | ITV m M =>
        if zle 0 m
        then i
        else if zlt M 0
             then ITV (m + Int.modulus) (M + Int.modulus)
             else utop
    end.
  Lemma reduc2unsigned_correct: forall i v,
    gamma i v ->
    ugamma (reduc2unsigned i) v.
  Lemma reduc2signed_correct: forall i v,
    ugamma i v ->
    gamma (reduc2signed i) v.

Lemma ugamma_top: ∀ x, ugamma utop x.

Lemma join_correctu : ∀ a b, ugamma a ∪ ugamma b ⊆ ugamma (a ⊔ b).

Instance itvu_adom : adom itv int := Build_adom _ _
  order utop join widen
  ugamma _ ugamma_top join_correctu.
Definition unsigned_itv_adom := itvu_adom.

Local Notation Γ := ugamma.

Transparent meet.
Lemma meet_correctu : forall x y,
  γ x ∩ γ y ⊆ match x ⊓ y with Bot => ∅ | NotBot z => Γ z end.
Opaque meet.


End Interval.

Inductive sign_flag : Type := Signed | Unsigned.

Definition ints_in_range (r: sign_flag -> Interval.itv+⊥) : int -> Prop :=
    botlift_prop Interval.gamma (r Signed)
  ∩ botlift_prop Interval.ugamma (r Unsigned).