Module Intervals

Require Import
  Coqlib Integers
  Utf8 DLib
  LatticeSignatures AbEnvironment
  AbNumDomain
  IntervalDomain.

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).

Instance itv_num : num_dom Interval.itv := Build_num_dom
  Interval.signed_itv_adom
  Interval.meet
  Interval.signed
  Interval.booleans
  (fun i s => NotBot (match s with Signed => i | Unsigned => Interval.reduc2unsigned i end))
  (@NotBot _ ∘ Interval.neg) (@NotBot _ ∘ Interval.not)
  (@NotBot _ ∘ Interval.notbool)
  (@NotBot _ ∘ Interval.boolval)
  (bb Interval.add) (bb Interval.sub)
  (bb Interval.mult) (bb Interval.div) (bb Interval.shl)
  (bb Interval.and) (bb Interval.or)
  (bb Interval.xor)
  (fun m M x => Interval.is_in_interval (Int.signed m) (Int.signed M) x)
  Interval.backward_boolval
  Interval.backward_notbool
  Interval.backward_neg
  Interval.backward_not
  Interval.backward_add
  Interval.backward_sub
  Interval.backward_cmp
  Interval.backward_cmpu
  Interval.backward_and
  Interval.backward_or
.

Instance itv_num_correct : num_dom_correct itv_num.

Module UInterval.

  Import Interval.

  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 notbool (i:itv) : itv :=
    if zlt 0 (min i) || zlt (max i) 0
    then ITV 0 0
    else if zeq 0 (min i) && zeq 0 (max i)
         then ITV 1 1
         else ITV 0 1.

  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 back_id_list (x y z: itv) : list (itv+⊥ * itv+⊥) := (NotBot x, NotBot y)::nil.

  Definition backward_ltu (i1 i2:itv) : itv+⊥ * itv+⊥ :=
    (i1 ⊓ (reduce 0 ((max i2)-1)),
     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+⊥ :=
    (i1 ⊓ (reduce 0 (max i2)),
     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 ⊓ (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 := 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.

Instance itvu_num : num_dom itv := Build_num_dom
  unsigned_itv_adom
  meet
  const
  booleans
  (fun i s => NotBot (match s with Signed => reduc2signed i | Unsigned => i end))
  (@NotBot _ ∘ neg) (@NotBot _ ∘ not)
  (@NotBot _ ∘ notbool)
  (@NotBot _ ∘ boolval)
  (bb add) (bb sub)
  (bb todo) (bb todo)
  (bb todo) (bb todo)
  (bb todo) (bb todo)
  (fun _ _ _ => false)
  back_id1 back_id1
  back_id1 back_id1
  back_id2 back_id2
  (fun _ => back_id2)
  (backward_cmpu)
  back_id_list back_id_list
.

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 →
  γ (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 :
    γ x i →
    γ y j →
    Int.unsigned i < Int.unsigned j →
    let '(u,v) := backward_ltu x y in
    γ u i ∧ γ v j.

  Lemma backward_ne_correct x y i j :
    γ x i →
    γ y j →
    Int.unsigned i ≠ Int.unsigned j →
    let '(u,v) := backward_ne x y in
    γ u i ∧ γ v j.

  Lemma backward_leu_correct x y i j :
    γ x i →
    γ y j →
    Int.unsigned i <= Int.unsigned j →
    let '(u,v) := backward_leu x y in
    γ u i ∧ γ v j.

Instance itvu_num_correct : num_dom_correct itvu_num.

End UInterval.

Import Interval.
Instance itv_red : reduction itv itv :=
{| ρ := botbind2 (fun s u =>
     let s' := reduc2signed u in
     let u' := reduc2unsigned s in
     match s ⊓ NotBot s', u ⊓ NotBot u' with
       | Bot, _ | _, Bot => Bot
       | NotBot a, NotBot b => NotBot (a,b)
     end)
|}.

Instance itv_red_correct : reduction_correct signed_itv_adom unsigned_itv_adom.

Instance intervals : num_dom _ := @reduced_product_num_dom _ _ itv_num UInterval.itvu_num itv_red.
Instance intervals_correct : num_dom_correct intervals :=
  reduced_product_num_dom_correct _ _ itv_num_correct UInterval.itvu_num_correct _ _.