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.