Library AbMachineNonrel

Require Import
  Coqlib Utf8
  Integers DLib
  IntervalDomain AdomLib.

Set Implicit Arguments.

Numerical operations available on numerical domains.
Inductive int_unary_operation :=
| OpNeg | OpNot.

Inductive int_binary_operation :=
| OpAdd | OpSub | OpMul | OpDivs | OpMods | OpShl | OpShr | OpShru
| OpAnd | OpOr | OpXor
| OpCmp (c: comparison) | OpCmpu (c: comparison).

Definition eval_int_unop op : int int :=
  match op with
  | OpNegInt.neg
  | OpNotInt.not

Definition eval_int_binop op : int int int :=
  match op with
  | OpAddInt.add
  | OpSubInt.sub
  | OpMulInt.mul
  | OpDivsInt.divs
  | OpModsInt.mods
  | OpShlInt.shl
  | OpShrInt.shr
  | OpShruInt.shru
  | OpAndInt.and
  | OpOrInt.or
  | OpXorInt.xor
  | OpCmp cfun x yInterval.of_bool (Int.cmp c x y)
  | OpCmpu cfun x yInterval.of_bool (Int.cmpu c x y)

Specifications of the numerical operations on sets of concrete values.
Definition lift_unop {T U:Type} (op: T U) (A: 𝒫 T) : 𝒫 U :=
  fun i j, A j i = (op j).

Definition Eval_int_unop (op: int_unary_operation) : 𝒫 int 𝒫 int :=
  lift_unop (eval_int_unop op).

Definition lift_binop {T U:Type} (op: T T U) (A B: 𝒫 T) : 𝒫 U :=
  fun i a, b, A a B b i = (op a b).

Definition Eval_int_binop (op: int_binary_operation) : 𝒫 int 𝒫 int 𝒫 int :=
  lift_binop (eval_int_binop op).

Signature of an abstract non relationnal numerical domain on machine numbers.
Specification of an abstract numerical domain.
Reduced product of two abstract numerical domains.
Definition red_prod_unop {A B C D} ρ (opa: A B+⊥) (opb: C D+⊥) : A×C (B×D)+⊥ :=
  fun xmatch x with (a,b)ρ (opa a) (opb b) end.

Definition red_prod_binop {A B C D} ρ (opa: A A B+⊥) (opb: C C D+⊥)
  : (A×C) (A×C) (B×D)+⊥ :=
  fun x ymatch x,y with (a,b), (c,d)
                            ρ (opa a c) (opb b d)

Definition red_prod_backop_un {A B C D} ρ (opa: A B A+⊥) (opb: C D C+⊥)
  : (A×C) (B×D) (A×C)+⊥ :=
  fun x ymatch x,y with
               | (a,b), (c,d)
                 let a' := opa a c in
                 let b' := opb b d in
                 (ρ a' b')

Definition red_prod_backop_bin {A B C D} ρ (opa: A A B A+⊥ × A+⊥) (opb: C C D C+⊥ × C+⊥)
  : (A×C) (A×C) (B×D) (A×C)+⊥ × (A×C)+⊥ :=
  fun x y zmatch x,y,z with
               | (a,b), (c,d), (e,f)
                 let '(a',c') := opa a c e in
                 let '(b',d') := opb b d f in
                 (ρ a' b', ρ c' d')

Instance reduced_product_int A_int B_int {Da:ab_machine_int A_int} {Db:ab_machine_int B_int}
         (Ρ_int: reduction A_int B_int)
  : ab_machine_int (A_int×B_int) :=
{| as_int_wl := WProd.make_wl as_int_wl as_int_wl
 ; as_int_gamma := WProd.gamma as_int_gamma as_int_gamma
 ; as_int_adom := WProd.make as_int_adom as_int_adom
 ; size x := match size (fst x), size (snd x) with All, a | a, Alla | Just a, Just bJust (N.min a b) end
 ; concretize x := match fs_meet (concretize (fst x)) (concretize (snd x)) with NotBot mm | Botfempty end
 ; meet_int x y := ρ (meet_int (fst x) (fst y)) (meet_int (snd x) (snd y))
 ; const_int n := (const_int n, const_int n)
 ; booleans := (booleans, booleans)
 ; range_int x s :=' (range_int (fst x) s) (range_int (snd x) s)
 ; forward_int_unop op := red_prod_unop ρ (forward_int_unop op) (forward_int_unop op)
 ; forward_int_binop op := red_prod_binop ρ (forward_int_binop op) (forward_int_binop op)

 ; is_in_itv m M x := let '(a,b) := x in is_in_itv m M a || is_in_itv m M b

 ; backward_int_unop op := red_prod_backop_un ρ (backward_int_unop op) (backward_int_unop op)
 ; backward_int_binop op := red_prod_backop_bin ρ (backward_int_binop op) (backward_int_binop op)

This reducted product yields a correct abstract numerical domain.
Lemma reduced_product_int_correct A_int B_int
         `{Da:ab_machine_int A_int} `{Db:ab_machine_int B_int}
         (Das: ab_machine_int_correct Da) (Dbs: ab_machine_int_correct Db)
         (Ρ_int: reduction A_int B_int) (Ρs_int: reduction_correct (@as_int_adom _ Da) (@as_int_adom _ Db))
  : ab_machine_int_correct (reduced_product_int A_int B_int Ρ_int).