Library IntSetDom

Require Import
  Coqlib Utf8
  TreeAl
  Integers
  LatticeSignatures
  IntervalDomain
  AdomLib
  AbMachineNonrel
  IntSet.

Definition fs_unop_sound (op: int → int) :
  ∀ x : fint_set, lift_unop op (γ x) ⊆ γ (fs_unop op x).

Definition fs_binop_sound (op: int → int → int) :
  ∀ x y : fint_set, lift_binop op (γ x) (γ y) ⊆ γ (fs_binop op x y).

Lemma fs_is_in_itv_sound (l r: int) (x: fint_set) :
  fs_is_in_itv l r x = true →
  ∀ i: int, γ x i → Int.lt r i = false ∧ Int.lt i l = false.

Notation todobw1 := (fun x _ ⇒ NotBot x).
Notation todobw2 := (fun x y _ ⇒ (NotBot x, NotBot y)).

Instance int_set_dom : ab_machine_int fint_set :=
{ as_int_adom := int_set_adom
; meet_int := fs_meet
; size := top_lift fs_size
; concretize x := x
; range_int := fs_range
; const_int := fs_const
; booleans := fs_booleans
; forward_int_unop := fs_unop ∘ eval_int_unop
; forward_int_binop := fs_binop ∘ eval_int_binop
; is_in_itv := fs_is_in_itv
; backward_int_unop op := todobw1
; backward_int_binop op := todobw2
}.

Instance int_set_dom_correct : ab_machine_int_correct int_set_dom.