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)

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) : :=
  match op with
  | OpNegInterval.neg
  | OpNotInterval.not

Definition itv_binop (op: int_binary_operation) : :=
  match op with
  | OpAddInterval.add
  | OpSubInterval.sub
  | OpMulInterval.mult
  | OpDivsInterval.div
  | OpShlInterval.shl
  | OpShrInterval.shr
  | OpShruInterval.shru
  | OpModsInterval.rem
  | OpOrInterval.or
  | OpAndInterval.and
  | OpXorInterval.xor
  | OpCmp cfun _ _Interval.booleans
  | OpCmpu cfun _ _Interval.booleans

Function itv_concretize_aux (from: Z) (nb: N)
         (acc: IntSet.int_set) {measure N.to_nat nb} : IntSet.int_set :=
  match nb with
  | N0acc
  | Npos p
    let nb' := Pos.pred_N p in
    itv_concretize_aux from nb'
    (IntSet.union (IntSet.singleton (Int.repr (from + Zpos p))) acc)

Definition itv_concretize (i: : IntSet.fint_set :=
  let (m, M) := i in
  match z2n (M - m) with
  | inleft nJust (itv_concretize_aux m (proj1_sig n) (IntSet.singleton (Int.repr m)))
  | inright GTJust (IntSet.empty)

Instance itv_dom : ab_machine_int
  := Build_ab_machine_int
    (fun xJust (N_of_Z (x.(Interval.max) - x.(Interval.min))))
    (fun i sNotBot (match s with Signedi | UnsignedInterval.reduc2unsigned i end))
    (fun op ⇒ @NotBot _ itv_unop op)
    (fun op x ⇒ @NotBot _ itv_binop op x)
    (fun m M xInterval.is_in_interval (Int.signed m) (Int.signed M) x)
    (fun op
       match op with
         | OpNegInterval.backward_neg
         | OpNotInterval.backward_not
    (fun op
       match op with
         | OpAddInterval.backward_add
         | OpSubInterval.backward_sub
         | OpCmp cInterval.backward_cmp c
         | OpCmpu cInterval.backward_cmpu c
         | OpAnd | OpOr
         | OpShr | OpShru
         | OpXor | OpMul | OpDivs | OpMods | OpShlfun x y _(NotBot x, NotBot y)

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: :
    γ x γ (itv_concretize x).


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 then
          match c with
            | Ceqlet ab := ab1 ab2 in (ab,ab)
            | Cnebackward_ne ab1 ab2
            | Cltbackward_ltu ab1 ab2
            | Clebackward_leu ab1 ab2
            | Cgtswap (backward_ltu ab2 ab1)
            | Cgeswap (backward_leu ab2 ab1)
        else if Int.eq i then
               match c with
                 | Ceqbackward_ne ab1 ab2
                 | Cnelet ab := ab1 ab2 in (ab,ab)
                 | Cgebackward_ltu ab1 ab2
                 | Cgtbackward_leu ab1 ab2
                 | Cleswap (backward_ltu ab2 ab1)
                 | Cltswap (backward_leu ab2 ab1)
             else (NotBot ab1,NotBot ab2)

Definition itvu_unop (op: int_unary_operation) : itv itv :=
  match op with
  | OpNegneg
  | OpNotnot

Definition itvu_binop (op: int_binary_operation) : :=
  match op with
  | OpAddadd
  | OpSubsub
  | OpMulmult
  | OpDivstodo
  | OpShltodo
  | _todo

 Instance itvu_num : ab_machine_int itv := Build_ab_machine_int
   (fun xJust (N_of_Z (x.(max) - x.(min))))
   (fun _All)
   (fun i sNotBot (match s with Signedreduc2signed i | Unsignedi 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 cbackward_cmpu c
      | _back_id2

 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, _ | _, BotBot
       | NotBot a, NotBot bNotBot (a,b)

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.