# Module AdomLib

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 "xy" := (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, a1a2 = true -> γ a1 ⊆ γ a2.

Class join_op (A B:Type) : Type := join : A -> A -> B.
Notation "xy" := (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 ⊆ γ (xy).

Class meet_op (A B:Type) : Type := meet : A -> A -> B.
Notation "xy" := (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 ⊆ γ (xy).

# 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).
Proof.
unfold union_list.
destruct l as [|a q]. intuition.
revert q.
refine (rev_ind _ _ _).
intros ab m [->|()]. easy.
intros b q HI.
intros ab m.
rewrite app_comm_cons, in_app, fold_left_app. simpl.
intros [[->|?]|[->|()]] AB.
apply join_correct. left. eapply HI; eauto. now left.
apply join_correct. left. eapply HI; eauto. now right.
apply join_correct. now right.
Qed.

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

Lemma union_list_map_correct l :
union_list_map l = union_list (map f l).
Proof.
unfold union_list_map, union_list.
destruct l as [|a q]. reflexivity.
induction q as [|b l IH] using rev_ind.
reflexivity.
simpl. rewrite fold_left_app, map_app, fold_left_app. simpl in *.
now rewrite IH.
Qed.

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.
Proof.
eauto. Qed.

Instance leb_bot (A:Type) (L:leb_op A) : leb_op (A+⊥) :=
(fun x y =>
match x, y with
| NotBot x, NotBot y => xy
| 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.
Proof.
destruct a1, a2; try easy. apply H. Qed.

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.
Proof.
auto. Qed.

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 => xy
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.
Proof.
destruct x, y; try now intuition. eauto. Qed.

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 => xy
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.
Proof.
repeat intro. destruct x, y, H0; auto. unfold meet. simpl. eapply meet_correct. auto. Qed.

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:AB+⊥) (x:A') (y:B'),
(∀ a:A, x ∈ γ a -> y ∈ γ (f a)) ->
(∀ a:A+⊥, x ∈ γ a -> y ∈ γ (bind a f)).
Prooff 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.
Proof.
destruct x_ab. destruct 1. auto. Qed.

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 : Atoplift 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.
Proof.
constructor. Qed.

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.
Proof.
destruct a1, a2; try easy. apply H. Qed.

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.
Proof.
auto. Qed.

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.
Proof.
destruct x, y; try now intuition. eauto. Qed.

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 <- xy; 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.
Proof.
repeat intro. destruct x, y, H0; auto. eapply botbind_spec; eauto. Qed.

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:AB+⊤, ∀ x y, (∀ a, x ∈ γ a -> y ∈ γ (f a)) ->
(∀ a, x ∈ γ a -> y ∈ γ (bind a f)).
Proof.
destruct a; simpl; eauto. intros; apply H, H0. Qed.

Definition flat_top_leb {A} (beq: AAbool) (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:TTbool).

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 = truex = y).

Instance flat_leb_op_correct : leb_op_correct T U.
Proof.
repeat intro. apply BEQ in H. congruence. Qed.

Instance flat_join_op_correct : join_op_correct T (T+⊤) U.
Proof.
repeat intro. simpl. unfold join, flat_join_op.
specialize (@BEQ x y). destruct (beq x y).
destruct H. auto. rewrite BEQ; auto.
constructor.
Qed.

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).
Proof.
split; auto. Qed.

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).
Proof.
destruct a1, a2. unfold leb; simpl. rewrite Bool.andb_true_iff. intros [? ?] ? [? ?].
red. eauto.
Qed.

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).
Proof.
destruct x, y. split; destruct H1 as [[]|[]]; unfold join, join_prod; eauto.
Qed.

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).
Proof.
repeat intro. eapply botbind_spec, (@top_correct _ _ _ _ H _).
intros. eapply botbind_spec, (@top_correct _ _ _ _ H0 _).
split; eauto.
Qed.

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).
Proof.
destruct x, y.
intros. eapply botbind_spec, (@join_correct _ _ _ _ _ _ H).
intros. eapply botbind_spec, (@join_correct _ _ _ _ _ _ H0).
split; eauto.
destruct H1 as [[]|[]]; eauto.
destruct H1 as [[]|[]]; eauto.
Qed.

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).
Proof.
destruct x, y.
intros. eapply toplift_bind_spec, (@join_correct _ _ _ _ _ _ H).
intros. eapply toplift_bind_spec, (@join_correct _ _ _ _ _ _ H0).
split; eauto.
destruct H1 as [[]|[]]; eauto.
destruct H1 as [[]|[]]; eauto.
Qed.

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)).
Proof.
split; auto. Qed.

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)).
Proof.
destruct a1, a2. unfold leb, WProd.leb_prod. rewrite Bool.andb_true_iff. intros [? ?] ? [? ?].
red. red. eauto.
Qed.

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)).
Proof.
destruct x, y. split; destruct H1 as [[]|[]]; unfold join, WProd.join_prod; eauto. Qed.

End WTensor.

Class widen_op (A B:Type) : Type :=
{ init_iter : B -> A;
widen : A -> B -> A * B }.
Notation "xy" := (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 ⊆ γ (xy) }.
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.
Proof.
unfold get.
destruct v as [|v]; simpl.
now rewrite T.grspec; destruct T.elt_eq.
now rewrite T.gsspec; destruct T.elt_eq.
Qed.

Lemma gss x p v :
get p (set x p v) = v.
Proof.
rewrite gsspec. destruct T.elt_eq; congruence. Qed.

Lemma gso x p v p' :
pp' →
get p' (set x p v) = get p' x.
Proof.
rewrite gsspec. destruct T.elt_eq; congruence. Qed.

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.
Next Obligation.
destruct v; auto. Qed.

Lemma leb_le (x y: t) :
leb x y = true <->
∀ p : T.elt, flat_top_leb leb (get p x) (get p y) = true.
Proof.
unfold leb, get, flat_top_leb, leb_tree.
rewrite T.shforall2_correct.
split; intros HH p; specialize (HH p);
destruct (T.get p x);
destruct (T.get p y); eauto;
congruence.
Qed.

Program Definition joinwiden f (Hf:∀ x, f x x = Just x): ttt :=
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)
_.
Next Obligation.
destruct v. rewrite Hf. auto. auto. Qed.

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.
Proof.
unfold get, joinwiden.
rewrite T.gshcombine.
destruct (T.get x a) as [u|].
destruct (T.get x b) as [v|].
simpl. destruct (f u v); reflexivity.
reflexivity.
reflexivity.
Qed.

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.
Proof.
unfold get. rewrite T.gempty. reflexivity. Qed.

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

Lemma gamma_set x a b p v :
γ x a
γ v (b p) →
(∀ q, qpa q = b q) →
γ (set x p v) b.
Proof.
intros A V HH c.
rewrite gsspec. destruct T.elt_eq.
subst; auto.
rewrite <- HH; auto.
Qed.

Lemma gamma_forget x a b p :
γ x a
(∀ q, qpa q = b q) →
γ (set x p All) b.
Proof.
intros A HH c. specialize (HH c).
rewrite gsspec. destruct T.elt_eq as [EQ|NE].
easy.
rewrite <- (HH NE). exact (A c).
Qed.

Instance top_tree_correct : top_op_correct t (T.elt -> B).
Proof.
repeat intro. rewrite get_top. constructor. Qed.

Instance leb_tree_correct : leb_op_correct elt B -> leb_op_correct t (T.elt -> B).
Proof.
intros HL a1 a2 LEB ρ Hρ.
unfold leb, leb_tree in LEB.
rewrite T.shforall2_correct in LEB.
intro x. specialize (LEB x). specialize (Hρ x).
unfold get in *. destruct T.get, T.get; try constructor.
eapply HL; eauto. discriminate.
Qed.

Instance join_tree_correct : join_op_correct elt (elt+⊤) B -> join_op_correct t t (T.elt -> B).
Proof.
intros HJ x y a HH c. simpl. unfold get, join, join_tree, joinwiden.
rewrite T.gshcombine.
destruct HH as [HH|HH]; specialize (HH c); unfold get in HH.
- destruct (T.get c x) as [u|].
* destruct (T.get c y) as [v|].
specialize (HJ u v _ (or_introl HH)).
destruct (uv); eauto. easy.
* easy.
- destruct (T.get c x) as [u|].
* destruct (T.get c y) as [v|].
specialize (HJ u v _ (or_intror HH)).
destruct (uv); eauto. easy.
* easy.
Qed.

Lemma widen_tree_incr :
(∀ x y, γ x ⊆ γ (widen x y)) ->
∀ x y, γ x ⊆ γ (widen_tree x y).
Proof.
intros HW x y a HH c. simpl. unfold get, widen_tree, joinwiden.
rewrite T.gshcombine.
specialize (HH c); unfold get in HH.
destruct (T.get c x) as [u|].
- destruct (T.get c y) as [v|].
specialize (HW u v _ HH).
destruct (widen u v); eauto. easy.
- easy.
Qed.

Instance toString {TS:ToString T.elt} {TS':ToString elt} : ToString (T.t elt) :=
(λ x, T.folds 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.