Library Intervals
Instance: (signed) interval domain.
Definition botlift_backop {A} op (x y: A+⊥) :=
match x, y with
| NotBot x', NotBot y' ⇒ op x' y'
| _, _ ⇒ (@Bot A, @Bot A)
end.
Definition bb {A B C} (f: A → B → C) (a: A) (b: B) : C+⊥ := NotBot (f a b).
Definition itv_unop (op: int_unary_operation) : Interval.itv → Interval.itv :=
match op with
| OpNeg ⇒ Interval.neg
| OpNot ⇒ Interval.not
end.
Definition itv_binop (op: int_binary_operation) : Interval.itv → Interval.itv → Interval.itv :=
match op with
| OpAdd ⇒ Interval.add
| OpSub ⇒ Interval.sub
| OpMul ⇒ Interval.mult
| OpDivs ⇒ Interval.div
| OpShl ⇒ Interval.shl
| OpShr ⇒ Interval.shr
| OpShru ⇒ Interval.shru
| OpMods ⇒ Interval.rem
| OpOr ⇒ Interval.or
| OpAnd ⇒ Interval.and
| OpXor ⇒ Interval.xor
| OpCmp c ⇒ fun _ _ ⇒ Interval.booleans
| OpCmpu c ⇒ fun _ _ ⇒ Interval.booleans
end.
Function itv_concretize_aux (from: Z) (nb: N)
(acc: IntSet.int_set) {measure N.to_nat nb} : IntSet.int_set :=
match nb with
| N0 ⇒ acc
| Npos p ⇒
let nb' := Pos.pred_N p in
itv_concretize_aux from nb'
(IntSet.union (IntSet.singleton (Int.repr (from + Zpos p))) acc)
end.
Definition itv_concretize (i: Interval.itv) : IntSet.fint_set :=
let (m, M) := i in
match z2n (M - m) with
| inleft n ⇒ Just (itv_concretize_aux m (proj1_sig n) (IntSet.singleton (Int.repr m)))
| inright GT ⇒ Just (IntSet.empty)
end.
Instance itv_dom : ab_machine_int Interval.itv
:= Build_ab_machine_int
Interval.signed_itv_adom
(fun x ⇒ Just (N_of_Z (x.(Interval.max) - x.(Interval.min))))
itv_concretize
Interval.meet
Interval.signed
Interval.booleans
(fun i s ⇒ NotBot (match s with Signed ⇒ i | Unsigned ⇒ Interval.reduc2unsigned i end))
(fun op ⇒ @NotBot _ ∘ itv_unop op)
(fun op x ⇒ @NotBot _ ∘ itv_binop op x)
(fun m M x ⇒ Interval.is_in_interval (Int.signed m) (Int.signed M) x)
(fun op ⇒
match op with
| OpNeg ⇒ Interval.backward_neg
| OpNot ⇒ Interval.backward_not
end)
(fun op ⇒
match op with
| OpAdd ⇒ Interval.backward_add
| OpSub ⇒ Interval.backward_sub
| OpCmp c ⇒ Interval.backward_cmp c
| OpCmpu c ⇒ Interval.backward_cmpu c
| OpAnd | OpOr
| OpShr | OpShru
| OpXor | OpMul | OpDivs | OpMods | OpShl ⇒ fun x y _ ⇒ (NotBot x, NotBot y)
end).
Section CONCR.
Import IntSet.
Local Open Scope int_set_scope.
Lemma itv_concretize_aux_correct z :
let round x := proj (Int.repr x) in
∀ nb acc,
round z ∈ acc →
∀ q, round q ∈ acc ∨ z < q ≤ z + Z.of_N nb →
round q ∈ itv_concretize_aux z nb acc.
Corollary itv_concretize_correct (x: Interval.itv) :
γ x ⊆ γ (itv_concretize x).
End CONCR.
Instance itv_dom_correct : ab_machine_int_correct itv_dom.
match x, y with
| NotBot x', NotBot y' ⇒ op x' y'
| _, _ ⇒ (@Bot A, @Bot A)
end.
Definition bb {A B C} (f: A → B → C) (a: A) (b: B) : C+⊥ := NotBot (f a b).
Definition itv_unop (op: int_unary_operation) : Interval.itv → Interval.itv :=
match op with
| OpNeg ⇒ Interval.neg
| OpNot ⇒ Interval.not
end.
Definition itv_binop (op: int_binary_operation) : Interval.itv → Interval.itv → Interval.itv :=
match op with
| OpAdd ⇒ Interval.add
| OpSub ⇒ Interval.sub
| OpMul ⇒ Interval.mult
| OpDivs ⇒ Interval.div
| OpShl ⇒ Interval.shl
| OpShr ⇒ Interval.shr
| OpShru ⇒ Interval.shru
| OpMods ⇒ Interval.rem
| OpOr ⇒ Interval.or
| OpAnd ⇒ Interval.and
| OpXor ⇒ Interval.xor
| OpCmp c ⇒ fun _ _ ⇒ Interval.booleans
| OpCmpu c ⇒ fun _ _ ⇒ Interval.booleans
end.
Function itv_concretize_aux (from: Z) (nb: N)
(acc: IntSet.int_set) {measure N.to_nat nb} : IntSet.int_set :=
match nb with
| N0 ⇒ acc
| Npos p ⇒
let nb' := Pos.pred_N p in
itv_concretize_aux from nb'
(IntSet.union (IntSet.singleton (Int.repr (from + Zpos p))) acc)
end.
Definition itv_concretize (i: Interval.itv) : IntSet.fint_set :=
let (m, M) := i in
match z2n (M - m) with
| inleft n ⇒ Just (itv_concretize_aux m (proj1_sig n) (IntSet.singleton (Int.repr m)))
| inright GT ⇒ Just (IntSet.empty)
end.
Instance itv_dom : ab_machine_int Interval.itv
:= Build_ab_machine_int
Interval.signed_itv_adom
(fun x ⇒ Just (N_of_Z (x.(Interval.max) - x.(Interval.min))))
itv_concretize
Interval.meet
Interval.signed
Interval.booleans
(fun i s ⇒ NotBot (match s with Signed ⇒ i | Unsigned ⇒ Interval.reduc2unsigned i end))
(fun op ⇒ @NotBot _ ∘ itv_unop op)
(fun op x ⇒ @NotBot _ ∘ itv_binop op x)
(fun m M x ⇒ Interval.is_in_interval (Int.signed m) (Int.signed M) x)
(fun op ⇒
match op with
| OpNeg ⇒ Interval.backward_neg
| OpNot ⇒ Interval.backward_not
end)
(fun op ⇒
match op with
| OpAdd ⇒ Interval.backward_add
| OpSub ⇒ Interval.backward_sub
| OpCmp c ⇒ Interval.backward_cmp c
| OpCmpu c ⇒ Interval.backward_cmpu c
| OpAnd | OpOr
| OpShr | OpShru
| OpXor | OpMul | OpDivs | OpMods | OpShl ⇒ fun x y _ ⇒ (NotBot x, NotBot y)
end).
Section CONCR.
Import IntSet.
Local Open Scope int_set_scope.
Lemma itv_concretize_aux_correct z :
let round x := proj (Int.repr x) in
∀ nb acc,
round z ∈ acc →
∀ q, round q ∈ acc ∨ z < q ≤ z + Z.of_N nb →
round q ∈ itv_concretize_aux z nb acc.
Corollary itv_concretize_correct (x: Interval.itv) :
γ x ⊆ γ (itv_concretize x).
End CONCR.
Instance itv_dom_correct : ab_machine_int_correct itv_dom.
Instance: (unsigned) interval domain.
Module UInterval.
Import Interval.
Instance ugamma_op : gamma_op itv int := ugamma.
Definition const (i: int) : itv :=
ITV (Int.unsigned i) (Int.unsigned i).
Definition neg (x: itv) : itv :=
if zeq 0 (max x)
then x
else if zle (min x) 0
then utop
else ITV (Int.modulus - max x) (Int.modulus - min x).
Definition repr (x: itv) : itv :=
if x ⊑ utop then x else utop.
Definition add (x y: itv) : itv :=
let m := min x + min y in
let M := max x + max y in
if zle m Int.max_unsigned
then if zle M Int.max_unsigned
then ITV m M
else utop
else ITV (m - Int.modulus) (M - Int.modulus).
Definition not (x: itv) : itv :=
add (neg x) (ITV Int.max_unsigned Int.max_unsigned).
Definition sub (x y: itv) : itv :=
repr (ITV (min x - max y) (max x - min y)).
Definition mult (x y:itv) : itv :=
let b1 := x.(min) × y.(min) in
let b2 := x.(min) × y.(max) in
let b3 := x.(max) × y.(min) in
let b4 := x.(max) × y.(max) in
repr (ITV
(Zmin (Zmin b1 b4) (Zmin b3 b2))
(Zmax (Zmax b1 b4) (Zmax b3 b2))).
Definition todo (x y: itv) : itv := utop.
Definition back_id1 (x y: itv) : itv+⊥ := NotBot x.
Definition back_id2 (x y z: itv) : itv+⊥ × itv+⊥ := (NotBot x, NotBot y).
Definition backward_ltu (i1 i2:itv) : itv+⊥ × itv+⊥ :=
(botbind (meet i1) (reduce 0 ((max i2)-1)),
botbind (meet i2) (reduce ((min i1)+1) Int.max_unsigned)).
Definition backward_ne (x y:itv) : itv+⊥ × itv+⊥ :=
let '(x', y') := backward_ltu x y in
let '(y'', x'') := backward_ltu y x in
(x' ⊔ x'', y' ⊔ y'').
Definition backward_leu (i1 i2:itv) : itv+⊥ × itv+⊥ :=
(botbind (meet i1) (reduce 0 (max i2)),
botbind (meet i2) (reduce (min i1) Int.max_unsigned)).
Definition backward_cmpu (c:comparison) (ab1 ab2 res:itv) : itv+⊥ × itv+⊥ :=
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 := 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 := 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.
Definition itvu_unop (op: int_unary_operation) : itv → itv :=
match op with
| OpNeg ⇒ neg
| OpNot ⇒ not
end.
Definition itvu_binop (op: int_binary_operation) : Interval.itv → Interval.itv → Interval.itv :=
match op with
| OpAdd ⇒ add
| OpSub ⇒ sub
| OpMul ⇒ mult
| OpDivs ⇒ todo
| OpShl ⇒ todo
| _ ⇒ todo
end.
Instance itvu_num : ab_machine_int itv := Build_ab_machine_int
unsigned_itv_adom
(fun x ⇒ Just (N_of_Z (x.(max) - x.(min))))
(fun _ ⇒ All)
meet
const
booleans
(fun i s ⇒ NotBot (match s with Signed ⇒ reduc2signed i | Unsigned ⇒ i end))
(fun op ⇒ @NotBot _ ∘ itvu_unop op)
(fun op x ⇒ @NotBot _ ∘ itvu_binop op x)
(fun _ _ _ ⇒ false)
(fun _ ⇒ back_id1)
(fun op ⇒
match op with
| OpCmpu c ⇒ backward_cmpu c
| _ ⇒ back_id2
end).
Lemma neg_correct: ∀ x i,
ugamma x i →
ugamma (neg x) (Int.neg i).
Lemma reduce_correct (m M: Z) (i:int) :
m ≤ Int.unsigned i ≤ M →
lift_gamma Interval.ugamma (reduce m M) i.
Lemma add_correct x y i j:
ugamma x i →
ugamma y j →
ugamma (add x y) (Int.add i j).
Lemma backward_ltu_correct x y i j :
ugamma x i →
ugamma y j →
Int.unsigned i < Int.unsigned j →
let '(u,v) := backward_ltu x y in
lift_gamma ugamma u i ∧ lift_gamma ugamma v j.
Lemma backward_ne_correct x y i j :
ugamma x i →
ugamma y j →
Int.unsigned i ≠ Int.unsigned j →
let '(u,v) := backward_ne x y in
lift_gamma ugamma u i ∧ lift_gamma ugamma v j.
Hint Resolve (lift_bot itvu_adom).
Lemma backward_leu_correct x y i j :
ugamma x i →
ugamma y j →
Int.unsigned i ≤ Int.unsigned j →
let '(u,v) := backward_leu x y in
lift_gamma ugamma u i ∧ lift_gamma ugamma v j.
Instance itvu_num_correct : ab_machine_int_correct itvu_num.
Opaque meet.
End UInterval.
Import Interval.
Instance ugamma_op : gamma_op itv int := ugamma.
Definition const (i: int) : itv :=
ITV (Int.unsigned i) (Int.unsigned i).
Definition neg (x: itv) : itv :=
if zeq 0 (max x)
then x
else if zle (min x) 0
then utop
else ITV (Int.modulus - max x) (Int.modulus - min x).
Definition repr (x: itv) : itv :=
if x ⊑ utop then x else utop.
Definition add (x y: itv) : itv :=
let m := min x + min y in
let M := max x + max y in
if zle m Int.max_unsigned
then if zle M Int.max_unsigned
then ITV m M
else utop
else ITV (m - Int.modulus) (M - Int.modulus).
Definition not (x: itv) : itv :=
add (neg x) (ITV Int.max_unsigned Int.max_unsigned).
Definition sub (x y: itv) : itv :=
repr (ITV (min x - max y) (max x - min y)).
Definition mult (x y:itv) : itv :=
let b1 := x.(min) × y.(min) in
let b2 := x.(min) × y.(max) in
let b3 := x.(max) × y.(min) in
let b4 := x.(max) × y.(max) in
repr (ITV
(Zmin (Zmin b1 b4) (Zmin b3 b2))
(Zmax (Zmax b1 b4) (Zmax b3 b2))).
Definition todo (x y: itv) : itv := utop.
Definition back_id1 (x y: itv) : itv+⊥ := NotBot x.
Definition back_id2 (x y z: itv) : itv+⊥ × itv+⊥ := (NotBot x, NotBot y).
Definition backward_ltu (i1 i2:itv) : itv+⊥ × itv+⊥ :=
(botbind (meet i1) (reduce 0 ((max i2)-1)),
botbind (meet i2) (reduce ((min i1)+1) Int.max_unsigned)).
Definition backward_ne (x y:itv) : itv+⊥ × itv+⊥ :=
let '(x', y') := backward_ltu x y in
let '(y'', x'') := backward_ltu y x in
(x' ⊔ x'', y' ⊔ y'').
Definition backward_leu (i1 i2:itv) : itv+⊥ × itv+⊥ :=
(botbind (meet i1) (reduce 0 (max i2)),
botbind (meet i2) (reduce (min i1) Int.max_unsigned)).
Definition backward_cmpu (c:comparison) (ab1 ab2 res:itv) : itv+⊥ × itv+⊥ :=
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 := 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 := 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.
Definition itvu_unop (op: int_unary_operation) : itv → itv :=
match op with
| OpNeg ⇒ neg
| OpNot ⇒ not
end.
Definition itvu_binop (op: int_binary_operation) : Interval.itv → Interval.itv → Interval.itv :=
match op with
| OpAdd ⇒ add
| OpSub ⇒ sub
| OpMul ⇒ mult
| OpDivs ⇒ todo
| OpShl ⇒ todo
| _ ⇒ todo
end.
Instance itvu_num : ab_machine_int itv := Build_ab_machine_int
unsigned_itv_adom
(fun x ⇒ Just (N_of_Z (x.(max) - x.(min))))
(fun _ ⇒ All)
meet
const
booleans
(fun i s ⇒ NotBot (match s with Signed ⇒ reduc2signed i | Unsigned ⇒ i end))
(fun op ⇒ @NotBot _ ∘ itvu_unop op)
(fun op x ⇒ @NotBot _ ∘ itvu_binop op x)
(fun _ _ _ ⇒ false)
(fun _ ⇒ back_id1)
(fun op ⇒
match op with
| OpCmpu c ⇒ backward_cmpu c
| _ ⇒ back_id2
end).
Lemma neg_correct: ∀ x i,
ugamma x i →
ugamma (neg x) (Int.neg i).
Lemma reduce_correct (m M: Z) (i:int) :
m ≤ Int.unsigned i ≤ M →
lift_gamma Interval.ugamma (reduce m M) i.
Lemma add_correct x y i j:
ugamma x i →
ugamma y j →
ugamma (add x y) (Int.add i j).
Lemma backward_ltu_correct x y i j :
ugamma x i →
ugamma y j →
Int.unsigned i < Int.unsigned j →
let '(u,v) := backward_ltu x y in
lift_gamma ugamma u i ∧ lift_gamma ugamma v j.
Lemma backward_ne_correct x y i j :
ugamma x i →
ugamma y j →
Int.unsigned i ≠ Int.unsigned j →
let '(u,v) := backward_ne x y in
lift_gamma ugamma u i ∧ lift_gamma ugamma v j.
Hint Resolve (lift_bot itvu_adom).
Lemma backward_leu_correct x y i j :
ugamma x i →
ugamma y j →
Int.unsigned i ≤ Int.unsigned j →
let '(u,v) := backward_leu x y in
lift_gamma ugamma u i ∧ lift_gamma ugamma v j.
Instance itvu_num_correct : ab_machine_int_correct itvu_num.
Opaque meet.
End UInterval.
Instance: reduction for signed/unsigned intervals.
Import Interval.
Instance itv_red : reduction itv itv :=
{| ρ := botbind2 (fun s u ⇒
let s' := reduc2signed u in
let u' := reduc2unsigned s in
match s ⊓ s', u ⊓ u' with
| Bot, _ | _, Bot ⇒ Bot
| NotBot a, NotBot b ⇒ NotBot (a,b)
end)
|}.
Lemma itv_red_correct : reduction_correct signed_itv_adom unsigned_itv_adom.
Hint Resolve reduc2unsigned_correct reduc2signed_correct.
Instance intervals : ab_machine_int _ :=
@reduced_product_int _ _ itv_dom UInterval.itvu_num itv_red.
Instance intervals_correct : ab_machine_int_correct intervals :=
reduced_product_int_correct itv_dom_correct UInterval.itvu_num_correct itv_red_correct.
Instance itv_red : reduction itv itv :=
{| ρ := botbind2 (fun s u ⇒
let s' := reduc2signed u in
let u' := reduc2unsigned s in
match s ⊓ s', u ⊓ u' with
| Bot, _ | _, Bot ⇒ Bot
| NotBot a, NotBot b ⇒ NotBot (a,b)
end)
|}.
Lemma itv_red_correct : reduction_correct signed_itv_adom unsigned_itv_adom.
Hint Resolve reduc2unsigned_correct reduc2signed_correct.
Instance intervals : ab_machine_int _ :=
@reduced_product_int _ _ itv_dom UInterval.itvu_num itv_red.
Instance intervals_correct : ab_machine_int_correct intervals :=
reduced_product_int_correct itv_dom_correct UInterval.itvu_num_correct itv_red_correct.