Require Import
  Utf8 String Bool ToString
  List Maps ShareTree Coqlib Integers AST Util.

Class gamma_op (A B: Type) : Type := γ : A -> ℘ B.

Arguments γ {A} {B} {gamma_op} a b /.

Class top_op (A:Type) : Type := top : A.
Notation "⊤" := top (at level 40).
Class top_op_correct A B {T:top_op A} {G:gamma_op A B} : Prop :=
  top_correct : ∀ x, x ∈ γ (⊤).

Class leb_op (A:Type) : Type := leb : A -> A -> bool.
Notation "x ⊑ y" := (leb x y) (at level 39).
Class leb_op_correct A B {L:leb_op A} {G:gamma_op A B} : Prop :=
  leb_correct : ∀ a1 a2, a1 ⊑ a2 = true -> γ a1 ⊆ γ a2.

Class join_op (A B:Type) : Type := join : A -> A -> B.
Notation "x ⊔ y" := (join x y) (at level 40).
Class join_op_correct A B C {J:join_op A B} {GA:gamma_op A C} {GB:gamma_op B C} : Prop :=
  join_correct : ∀ x y, γ x ∪ γ y ⊆ γ (x ⊔ y).

Class meet_op (A B:Type) : Type := meet : A -> A -> B.
Notation "x ⊓ y" := (meet x y) (at level 40).
Class meet_op_correct A B C {J:meet_op A B} {G:gamma_op A C} {GB:gamma_op B C} : Prop :=
  meet_correct : ∀ x y, γ x ∩ γ y ⊆ γ (x ⊓ y).

Union of a list of abstract values

Section union_list.
Context {A B C:Type} (f : C -> A) (bot : A)
        {G:gamma_op A B} {J:join_op A A} {HJG:join_op_correct A A B}.

Definition union_list (l: list A) : A :=
  match l with
  | nil => bot
  | a::q =>
    List.fold_left join q a
  end.

Lemma union_list_correct : forall l ab m,
  In ab l ->
  m ∈ γ ab ->
  m ∈ γ (union_list l).

Definition union_list_map (l: list C) : A :=
  match l with
  | nil => bot
  | a :: q => List.fold_left (λ u x, join u (f x)) q (f a)
  end.

Lemma union_list_map_correct l :
  union_list_map l = union_list (map f l).

End union_list.

Set Implicit Arguments.

Adding a bottom element to an abstract domain

Inductive botlift (A:Type) : Type := Bot | NotBot (x:A).
Arguments Bot [A].
Notation "t +⊥" := (botlift t) (at level 39).

Instance gamma_bot (A B: Type) (G: gamma_op A B) : gamma_op (A+⊥) B :=
  (fun x =>
     match x with
       | Bot => fun _ => False
       | NotBot x => γ x
     end).

Instance top_bot (A:Type) (T:top_op A) : top_op (A+⊥) := NotBot (⊤).
Instance top_bot_correct A B (G:gamma_op A B) (T:top_op A) :
  top_op_correct A B -> top_op_correct (A+⊥) B.

Instance leb_bot (A:Type) (L:leb_op A) : leb_op (A+⊥) :=
  (fun x y =>
     match x, y with
       | NotBot x, NotBot y => x ⊑ y
       | Bot, _ => true
       | _, Bot => false
     end).
Instance leb_bot_correct A B (G:gamma_op A B) (L:leb_op A) :
  leb_op_correct A B -> leb_op_correct (A+⊥) B.

Instance join_bot_res A (J:join_op A A) : join_op A (A+⊥) :=
  (fun x y => NotBot (join x y)).
Instance join_bot_res_correct A C (GA:gamma_op A C) (GB:gamma_op A C) (J:join_op A A) :
  join_op_correct A A C -> join_op_correct A (A+⊥) C.

Instance join_bot_args A (J:join_op A (A+⊥)) : join_op (A+⊥) (A+⊥) :=
  (fun x y =>
     match x, y with
       | Bot, _ => y
       |_ , Bot => x
       | NotBot x, NotBot y => x ⊔ y
     end).
Instance join_bot_args_correct A B (G:gamma_op A B) (J:join_op A (A+⊥)) :
    join_op_correct A (A+⊥) B -> join_op_correct (A+⊥) (A+⊥) B.

Instance meet_bot_args (A:Type) (M:meet_op A (A+⊥)) : meet_op (A+⊥) (A+⊥) :=
  (fun x y =>
     match x, y with
       | Bot, _ | _, Bot => Bot
       | NotBot x, NotBot y => x ⊓ y
     end).
Instance meet_bot_args_correct A B (GA:gamma_op A B) (M:meet_op A (A+⊥)) :
  meet_op_correct A (A+⊥) B -> meet_op_correct (A+⊥) (A+⊥) B.

Instance monad_botlift : monad botlift :=
  { ret := NotBot;
    bind A B a f :=
      match a with
      | Bot => Bot
      | NotBot x => f x
      end }.

Lemma botbind_spec {A A' B B'} {GA:gamma_op A A'} {GB:gamma_op B B'} :
  ∀ (f:A→B+⊥) (x:A') (y:B'),
    (∀ a:A, x ∈ γ a -> y ∈ γ (f a)) ->
    (∀ a:A+⊥, x ∈ γ a -> y ∈ γ (bind a f)).
Proof (λ f x y H a,
       match a with
       | Bot => λ K, K
       | NotBot a' => λ K, H _ K
       end).

Definition is_bot {A:Type} (v:A+⊥) : bool :=
  match v with
    | Bot => true
    | NotBot _ => false
  end.

Lemma is_bot_spec {A A':Type} {AD:gamma_op A A'} :
  forall x x_ab, x ∈ γ x_ab -> is_bot x_ab = false.

Instance bot_lift_toString A {TS:ToString A} : ToString (A+⊥) :=
  { to_string x := match x with
                   | Bot => "⊥"%string
                   | NotBot x' => to_string x'
                   end
  }.

Adding a top element to a domain.

Inductive toplift (A: Type) := All : top_op (toplift A) | Just : A → toplift A.
Existing Instance All.
Notation "x +⊤" := (toplift x) (at level 39).
Arguments All [A].
Arguments Just [A] v.

Instance toplift_gamma t B (GAMMA: gamma_op t B) : gamma_op (t+⊤) B :=
  λ x, match x with All => λ _, True | Just y => γ y end.

Instance All_correct A B (G:gamma_op A B) : top_op_correct (A+⊤) B.

Instance leb_top (A:Type) (L:leb_op A) : leb_op (A+⊤) :=
  (fun x y =>
     match x, y with
       | Just x, Just y => leb x y
       | _, All => true
       | All, _ => false
     end).
Instance leb_top_correct A B (G:gamma_op A B) (L:leb_op A) :
  leb_op_correct A B -> leb_op_correct (A+⊤) B.

Instance join_top_res (A B:Type) (J:join_op A B) : join_op A (B+⊤) :=
  (fun x y => Just (join x y)).
Instance join_top_res_correct A B C (GA:gamma_op A C) (GB:gamma_op B C) (J:join_op A B) :
  join_op_correct A B C -> join_op_correct A (B+⊤) C.

Instance join_top_args (A B:Type) (J:join_op A (B+⊤)) : join_op (A+⊤) (B+⊤) :=
  (fun x y =>
     match x, y with
       | All, _ | _, All => All
       | Just x, Just y => join x y
     end).
Instance join_top_args_correct A B C (GA:gamma_op A C) (GB:gamma_op B C) (J:join_op A (B+⊤)) :
  join_op_correct A (B+⊤) C -> join_op_correct (A+⊤) (B+⊤) C.

Instance meet_top (A:Type) (J:meet_op A (A+⊥)) : meet_op (A+⊤) (A+⊤+⊥) :=
  (fun x y =>
     match x, y with
       | All, res | res, All => NotBot res
       | Just x, Just y => do r <- x ⊓ y; NotBot (Just r)
     end).
Instance meet_top_correct A B (GA:gamma_op A B) (J:meet_op A (A+⊥)) :
  meet_op_correct A (A+⊥) B -> meet_op_correct (A+⊤) (A+⊤+⊥) B.

Instance monad_toplift : monad toplift :=
  { ret := Just;
    bind A B a f :=
      match a with
      | All => All
      | Just x => f x
      end }.

Lemma toplift_bind_spec {A A' B B':Type} {GA: gamma_op A A'} {GB: gamma_op B B'} :
  ∀ f:A→B+⊤, ∀ x y, (∀ a, x ∈ γ a -> y ∈ γ (f a)) ->
                    (∀ a, x ∈ γ a -> y ∈ γ (bind a f)).

Definition flat_top_leb {A} (beq: A → A → bool) (x y: A+⊤) : bool :=
  match x, y with
  | _, All => true
  | All, _ => false
  | Just x', Just y' => beq x' y'
  end.

Instance toplift_toString A {TS:ToString A} : ToString (A+⊤) :=
  { to_string x := match x with
                   | All => "⊤"%string
                   | Just y => to_string y
                   end
  }.

Section beq.

Context {T} (beq:T → T → bool).

Instance flat_leb_op : leb_op T := beq.
Instance flat_join_op : join_op T (T+⊤) :=
  fun x y => if beq x y then Just x else All.

Context U {G:gamma_op T U} (BEQ: ∀ x y, beq x y = true → x = y).

Instance flat_leb_op_correct : leb_op_correct T U.

Instance flat_join_op_correct : join_op_correct T (T+⊤) U.

End beq.

Existing Instances flat_leb_op_correct flat_join_op_correct.

Direct product of two abstract domains

Module WProd.

  Instance gamma {A B C} (GA:gamma_op A C) (GB:gamma_op B C) : gamma_op (A*B) C :=
    fun x => γ (fst x) ∩ γ (snd x).

  Instance top_prod {A B} (T:top_op A) (T:top_op B) : top_op (A*B) := (top, top)%bool.

  Instance top_prod_correct A B T
        (GA:gamma_op A T) (GB:gamma_op B T) (TA:top_op A) (TB:top_op B) :
    (top_op_correct A T) -> (top_op_correct B T) -> (top_op_correct (A*B) T).

  Instance leb_prod {A B} (LA:leb_op A) (LB:leb_op B) : leb_op (A*B) :=
    fun x y =>
      let (x1,x2) := x in
      let (y1,y2) := y in
      (leb x1 y1 && leb x2 y2)%bool.

  Instance leb_prod_correct A B T
        (GA:gamma_op A T) (GB:gamma_op B T) (LA:leb_op A) (LB:leb_op B) :
    (leb_op_correct A T) -> (leb_op_correct B T) -> (leb_op_correct (A*B) T).

  Instance join_prod {A B C D} (JAC:join_op A C) (JBD:join_op B D) : join_op (A*B) (C*D) :=
    fun x y =>
      let (x1,x2) := x in
      let (y1,y2) := y in
      (join x1 y1, join x2 y2).

  Instance join_prod_correct A B C D T
        (GA:gamma_op A T) (GB:gamma_op B T) (GC:gamma_op C T) (GD:gamma_op D T)
        (JAC:join_op A C) (JBD:join_op B D) :
    (join_op_correct A C T) -> (join_op_correct B D T) -> (join_op_correct (A*B) (C*D) T).

  Instance top_prod_bot {A B} (T:top_op (A+⊥)) (T:top_op (B+⊥)) : top_op ((A*B)+⊥) :=
    do t1 <- top;
    do t2 <- top;
    ret (t1, t2)%bool.

  Instance top_prod_bot_correct A B T
        (GA:gamma_op A T) (GB:gamma_op B T) (TA:top_op (A+⊥)) (TB:top_op (B+⊥)) :
    (top_op_correct (A+⊥) T) -> (top_op_correct (B+⊥) T) -> (top_op_correct ((A*B)+⊥) T).

  Instance join_prod_bot {A B C D} (JAC:join_op A (C+⊥)) (JBD:join_op B (D+⊥)) :
    join_op (A*B) ((C*D)+⊥) :=
    fun x y =>
      let (x1,x2) := x in
      let (y1,y2) := y in
      do j1 <- join x1 y1;
      do j2 <- join x2 y2;
      ret (j1, j2).

  Instance join_prod_bot_correct A B C D T
        (GA:gamma_op A T) (GB:gamma_op B T) (GC:gamma_op C T) (GD:gamma_op D T)
        (JAC:join_op A (C+⊥)) (JBD:join_op B (D+⊥)) :
    (join_op_correct A (C+⊥) T) -> (join_op_correct B (D+⊥) T) ->
    (join_op_correct (A*B) ((C*D)+⊥) T).

  Instance join_prod_top {A B C D} (JAC:join_op A (C+⊤)) (JBD:join_op B (D+⊤)) :
    join_op (A*B) ((C*D)+⊤) :=
    fun x y =>
      let (x1,x2) := x in
      let (y1,y2) := y in
      do j1 <- join x1 y1;
      do j2 <- join x2 y2;
      ret (j1, j2).

  Instance join_prod_top_correct A B C D T
        (GA:gamma_op A T) (GB:gamma_op B T) (GC:gamma_op C T) (GD:gamma_op D T)
        (JAC:join_op A (C+⊤)) (JBD:join_op B (D+⊤)) :
    (join_op_correct A (C+⊤) T) -> (join_op_correct B (D+⊤) T) ->
    (join_op_correct (A*B) ((C*D)+⊤) T).

End WProd.

Existing Instances WProd.gamma WProd.top_prod WProd.leb_prod WProd.join_prod.
Existing Instances WProd.top_prod_correct WProd.leb_prod_correct WProd.join_prod_correct.
Existing Instances WProd.top_prod_bot WProd.join_prod_bot.
Existing Instances WProd.top_prod_bot_correct WProd.join_prod_bot_correct.

Abstract domain of pairs of concrete elements.

Module WTensor.

  Instance gamma {A B C D} (GAC:gamma_op A C) (GBD:gamma_op B D) : gamma_op (A*B) (C*D) :=
    fun x y => γ (fst x) (fst y) /\ γ (snd x) (snd y).

  Instance top_prod_correct A B T U
        (GAT:gamma_op A T) (GBU:gamma_op B U) (TA:top_op A) (TB:top_op B) :
    (top_op_correct A T) -> (top_op_correct B U) -> (top_op_correct (A*B) (T*U)).

  Instance leb_op_correct A B T U
        (GAT:gamma_op A T) (GBU:gamma_op B U) (LAC:leb_op A) (LBD:leb_op B) :
    (leb_op_correct A T) -> (leb_op_correct B U) -> (leb_op_correct (A*B) (T*U)).

  Instance join_op_correct A B C D T U
        (GAT:gamma_op A T) (GBU:gamma_op B U) (GCT:gamma_op C T) (GDU:gamma_op D U)
        (JAC:join_op A C) (JBD:join_op B D) :
    (join_op_correct A C T) -> (join_op_correct B D U) -> (join_op_correct (A*B) (C*D) (T*U)).

End WTensor.

Class widen_op (A B:Type) : Type :=
  { init_iter : B -> A;
    widen : A -> B -> A * B }.
Notation "x ▽ y" := (widen x y) (at level 40).
Class widen_op_correct A B C {W:widen_op A B} {GA:gamma_op A C} {GB:gamma_op B C} : Prop :=
  { init_iter_correct : ∀ x, γ x ⊆ γ (init_iter x);
    widen_incr : ∀ (x:A) y, γ x ⊆ γ (x ▽ y) }.
Arguments widen_op_correct A B C {W} {GA} {GB}.

Existing Instance WTensor.gamma.
Existing Instances WTensor.top_prod_correct WTensor.leb_op_correct WTensor.join_op_correct.

Exponentiation of an abstract domain to an abstract domain of total environments

Module WPFun (T:SHARETREE).
Module P := Tree_Properties T.
Module SP := ShareTree_Properties T.
Section elt.

  Context (elt B: Type)
          (G:gamma_op elt B)
          (J:join_op elt (elt+⊤)) (H_join_eq: ∀ (x:elt), join x x = Just x)
          (widen:elt -> elt -> (elt+⊤)) (H_widen_eq: ∀ (x:elt), widen x x = Just x)
          (L:leb_op elt) (H_leb_eq: ∀ (x:elt), leb x x = true).

  Definition t : Type := T.t elt.

  Definition get (p: T.elt) (x: t) : elt+⊤ :=
    match T.get p x with
    | Some r => Just r
    | None => All
    end.

  Definition set (x:t) (p: T.elt) (v: elt+⊤) : t :=
    match v with
    | All => T.remove p x
    | Just v' => T.set p v' x
    end.

  Lemma gsspec x p v p' :
    get p' (set x p v) = if T.elt_eq p' p then v else get p' x.

  Lemma gss x p v :
    get p (set x p v) = v.

  Lemma gso x p v p' :
    p ≠ p' →
    get p' (set x p v) = get p' x.

  Program Instance leb_tree : leb_op t :=
    λ x y,
    T.shforall2 (λ _ a b, match a, b return _ with
                            | _, None => true
                            | None, Some _ => false
                            | Some a', Some b' => leb a' b'
                          end)
                _ x y.

  Lemma leb_le (x y: t) :
    leb x y = true <->
    ∀ p : T.elt, flat_top_leb leb (get p x) (get p y) = true.

  Program Definition joinwiden f (Hf:∀ x, f x x = Just x): t → t → t :=
    T.shcombine
      (λ _ u v, match u, v return _ with
                  | None, _
                  | _, None => None
                  | Some u', Some v' =>
                    match f u' v' return _ with
                      | Just r => Some r
                      | All => None
                    end
                end)
      _.

  Lemma get_joinwiden f Hf a b x :
    get x (joinwiden f Hf a b) = do xa <- get x a; do xb <- get x b; f xa xb.

  Instance top_tree : top_op t := T.empty _.
  Instance join_tree : join_op t t := joinwiden join H_join_eq.
  Definition widen_tree : t -> t -> t := joinwiden widen H_widen_eq.

  Lemma get_top x : get x (T.empty _) = All.

  Instance gamma_tree : gamma_op t (T.elt → B) :=
    λ x y, ∀ e, y e ∈ γ (get e x).

  Lemma gamma_set x a b p v :
    γ x a →
    γ v (b p) →
    (∀ q, q ≠ p → a q = b q) →
    γ (set x p v) b.

  Lemma gamma_forget x a b p :
    γ x a →
    (∀ q, q ≠ p → a q = b q) →
    γ (set x p All) b.

  Instance top_tree_correct : top_op_correct t (T.elt -> B).

  Instance leb_tree_correct : leb_op_correct elt B -> leb_op_correct t (T.elt -> B).

  Instance join_tree_correct : join_op_correct elt (elt+⊤) B -> join_op_correct t t (T.elt -> B).

  Lemma widen_tree_incr :
    (∀ x y, γ x ⊆ γ (widen x y)) ->
    ∀ x y, γ x ⊆ γ (widen_tree x y).

  Instance toString {TS:ToString T.elt} {TS':ToString elt} : ToString (T.t elt) :=
    (λ x, T.fold (λ s k v, s ++ "["++ to_string k ++ "↦" ++ to_string v ++"]" ) x "{" ++ "}")%string.

End elt.

Opaque get.
Opaque set.

Existing Instances gamma_tree top_tree join_tree leb_tree toString.
Existing Instances top_tree_correct join_tree_correct leb_tree_correct.

End WPFun.