Library IntervalDomain
Abstract domain of intervals of machine integers.
Require Import Coqlib Utf8 ToString.
Require Import Psatz.
Require Import Integers.
Require Import LatticeSignatures AdomLib.
Require Import DLib.
Require Import PrintPos.
Require Recdef.
Import String.
Section SIGNEDNESS.
LocalInductive signedness : Type :=
| Signed: signedness
| Unsigned: signedness.
End SIGNEDNESS.
Module Interval.
Record itv : Type := ITV { min: Z; max: Z }.
Definition t := itv.
Instance toString : ToString t :=
{ to_string i := ("[" ++ string_of_z i.(min) ++ "; " ++ string_of_z i.(max) ++ "]")%string }.
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).
Instance gamma : gamma_op itv int := fun i v ⇒
min i ≤ Int.signed v ≤ max i.
Lemma gamma_top : ∀ v,
gamma top v.
Lemma gamma_monotone : ∀ ab1 ab2,
order ab1 ab2 = true → ∀ v, gamma ab1 v → gamma ab2 v.
Lemma join_correct : ∀ (i1 i2:itv) i,
gamma i1 i ∨ gamma i2 i →
gamma (join i1 i2) i.
Instance signed_itv_wl : weak_lattice itv :=
{ leb := order;
top := top;
join := join;
widen := widen_heuristic
}.
Lemma signed_itv_adom : adom itv int _ gamma.
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:itv) : itvbot :=
match i1, i2 with
| (ITV min1 max1), (ITV min2 max2) ⇒
reduce (Zmax min1 min2) (Zmin max1 max2)
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 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 (Z.quot a i2) (Z.quot 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 rem (v1 v2:itv) : itv :=
match is_singleton v2 with
| Some i2 ⇒
let i2 := Int.signed i2 in
if zlt 0 i2 then
match is_singleton v1 with
| Some i1 ⇒
let i1 := Int.signed i1 in
let r := Z.rem i1 i2 in
ITV r r
| None ⇒
let 'ITV lo hi := v1 in
if zlt 0 lo then
ITV 0 (i2 - 1)
else top
end
else top
| None ⇒ top
end.
Definition backward_eq (i1 i2:itv) : itvbot × itvbot :=
(meet i1 i2, meet i1 i2).
Definition backward_lt (i1 i2:itv) : itvbot × itvbot :=
(botbind (meet i1) (reduce Int.min_signed ((max i2)-1)),
botbind (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 :=
(botbind (meet i1) (reduce Int.min_signed (max i2)),
botbind (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: ∀ (ab1:itv) (ab2:itv) v,
γ ab1 v → γ ab2 v → γ (meet ab1 ab2) v.
Definition meet' (ab1 ab2:itvbot) : itvbot :=
botbind2 meet ab1 ab2.
Lemma meet'_correct: ∀ (ab1 ab2:itvbot) v,
γ ab1 v → γ ab2 v → γ (meet' ab1 ab2) v.
Lemma neg_correct : ∀ ab i,
γ ab i →
γ (neg ab) (Int.neg i).
Lemma signed_correct: ∀ i, γ (signed i) i.
Lemma bool_correct_zero : γ booleans Int.zero.
Lemma bool_correct_one : γ booleans Int.one.
Lemma is_in_interval_correct : ∀ a b ab,
is_in_interval a b ab = true →
∀ i, γ ab i → a ≤ Int.signed i ≤ b.
Lemma add_correct : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (add ab1 ab2) (Int.add i1 i2).
Lemma not_correct : ∀ ab i,
γ ab i → γ (not ab) (Int.not i).
Lemma sub_correct : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (sub ab1 ab2) (Int.sub i1 i2).
Lemma mul_correct : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (mult ab1 ab2) (Int.mul i1 i2).
Lemma is_singleton_correct : ∀ 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 : ∀ 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: ∀ i n,
γ i n →
is_a_boolean i = true →
n = Int.zero ∨ n = Int.one.
Lemma is_a_boolean_correct_extra: ∀ i n,
γ i n →
is_a_boolean i = true →
0 ≤ min i ∧ max i ≤ 1.
Lemma is_a_boolean_correct_zero: ∀ i n,
γ i n →
is_a_boolean i = true →
(max i) = 0 →
n = Int.zero.
Lemma is_a_boolean_correct_one: ∀ 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: ∀ n,
IsBool n → γ booleans n.
Lemma bool_op_correct : ∀ f,
(∀ x y, IsBool x → IsBool y → IsBool (f x y)) →
∀ 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 : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (and ab1 ab2) (Int.and i1 i2).
Lemma or_correct : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (or ab1 ab2) (Int.or i1 i2).
Lemma xor_correct : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (xor ab1 ab2) (Int.xor i1 i2).
Lemma shl_correct : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (shl ab1 ab2) (Int.shl i1 i2).
Lemma divs_correct : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (div ab1 ab2) (Int.divs i1 i2).
Hint Resolve Z_div_le Int.modulus_pos.
Definition shr_l (x: itv) (y: Z) : itv :=
{| min := Z.shiftr x.(min) y
; max := Z.shiftr x.(max) y
|}.
Lemma shr_l_correct x y i :
0 ≤ y < Int.modulus →
γ x i →
γ (shr_l x y) (Int.shr i (Int.repr y)).
Definition shr (x y: itv) : itv :=
match is_singleton y with
| Some l ⇒ shr_l x (Int.unsigned l)
| None ⇒ top
end.
Lemma shr_correct x y i j :
gamma x i → gamma y j →
γ (shr x y) (Int.shr i j).
Definition shru_top (y: Z) : itv :=
{| min := 0
; max := Z.shiftr (2 ^ 32 - 1) y
|}.
Lemma shru_top_correct i j :
Int.unsigned j ≠ 0 →
γ (shru_top (Int.unsigned j)) (Int.shru i j).
Definition shru (x y: itv) : itv :=
match is_singleton y with
| Some l ⇒
let y' := Int.unsigned l in
if Z_zerop y'
then x
else if znegb x.(min)
then shru_top y'
else shr_l x y'
| None ⇒ top
end.
Lemma shru_correct x y i j :
gamma x i → gamma y j →
γ (shru x y) (Int.shru i j).
Lemma rem_correct : ∀ ab1 ab2 i1 i2,
γ ab1 i1 → γ ab2 i2 →
γ (rem ab1 ab2) (Int.mods i1 i2).
Lemma contains_correct : ∀ x ab,
if contains x ab then γ ab x else ¬ γ ab x.
Lemma gamma_backward_eq: ∀ 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.
Opaque meet.
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
botbind (meet it) (reduce (min+1) Int.max_signed)
else if zeq i max then
botbind (meet it) (reduce Int.min_signed (max-1))
else NotBot it.
Lemma remove_correct : ∀ ab i0 i,
γ ab i → Int.eq i i0 = false → γ (remove ab i0) i.
Definition backward_neg (iin:itv) (out:itv) : itvbot :=
meet iin (neg out).
Lemma backward_neg_correct : ∀ ab1 ab2 i,
γ ab1 i →
γ ab2 (Int.neg i) →
γ (backward_neg ab1 ab2) i.
Definition backward_not (iin:itv) (out:itv) : itvbot :=
meet iin (not out).
Lemma backward_not_correct : ∀ 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 (sub res ab2),
meet ab2 (sub res ab1)).
Lemma add_sub: ∀ i1 i2:int,
(Int.sub (Int.add i1 i2) i2) = i1.
Lemma backward_add_correct : ∀ 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 (add res ab2),
meet ab2 (sub ab1 res)).
Lemma add_sub2: ∀ i1 i2:int,
(Int.add (Int.sub i1 i2) i2) = i1.
Lemma add_sub3: ∀ i1 i2:int,
(Int.sub i1 (Int.sub i1 i2)) = i2.
Lemma backward_sub_correct : ∀ 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_list (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 (signed Int.one),
meet ab2 (signed Int.one)) ::nil
else if Int.eq i Int.zero then
(NotBot ab1,meet ab2 (signed Int.zero)) ::
(meet ab1 (signed Int.zero), NotBot ab2) :: nil
else (NotBot ab1,NotBot ab2) :: nil
end
else (NotBot ab1,NotBot ab2) :: nil.
Lemma backward_and_list_correct : ∀ ab1 ab2 res i1 i2,
γ ab1 i1 →
γ ab2 i2 →
γ res (Int.and i1 i2) →
∃ ab, In ab (backward_and_list ab1 ab2 res) ∧
γ (fst ab) i1 ∧
γ (snd ab) i2.
Definition backward_or_list (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 (signed Int.zero),
meet ab2 (signed Int.zero)) ::nil
else if Int.eq i Int.one then
(NotBot ab1, meet ab2 (signed Int.one)) ::
(meet ab1 (signed Int.one), NotBot ab2) :: nil
else (NotBot ab1,NotBot ab2) :: nil
end
else (NotBot ab1,NotBot ab2) :: nil.
Lemma backward_or_list_correct : ∀ ab1 ab2 res i1 i2,
γ ab1 i1 →
γ ab2 i2 →
γ res (Int.or i1 i2) →
∃ ab, In ab (backward_or_list ab1 ab2 res) ∧
γ (fst ab) i1 ∧
γ (snd ab) i2.
Lemma gamma_backward_lt: ∀ 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: ∀ 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: ∀ 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: ∀ ab i,
cast_int16u ab = true →
γ ab i →
Int.signed i = Int.unsigned i.
Lemma gamma_backward_leu: ∀ 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: ∀ 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 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 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 : ∀ 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 : ∀ 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 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 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 : ∀ 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: ∀ i v,
gamma i v →
ugamma (reduc2unsigned i) v.
Lemma reduc2signed_correct: ∀ 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_wl : weak_lattice itv :=
{ leb := order
; top := utop
; join := join
; widen := widen
}.
Lemma itvu_adom : adom itv int itvu_wl ugamma.
Definition unsigned_itv_adom := itvu_adom.
Local Notation Γ := ugamma.
Transparent meet.
Lemma meet_correctu : ∀ x y,
Γ x ∩ Γ y ⊆ match x ⊓ y with Bot ⇒ ∅ | NotBot z ⇒ Γ z end.
Hint Resolve Zmax_lub Zmin_glb.
Opaque meet.
End Interval.
Definition ints_in_range (r: signedness→ Interval.itv+⊥) : int → Prop :=
lift_gamma Interval.gamma (r Signed)
∩ lift_gamma Interval.ugamma (r Unsigned).