Proof.v 40.2 KB
Newer Older
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1 2 3 4 5 6 7
From TLC Require Import LibTactics LibLogic LibSet LibRelation LibFun LibEqual
                        LibInt.
From iris_time.union_find.math Require Import TLCBuffer.

From stdpp Require Import gmap.

From iris.bi Require Import big_op.
8
From iris_time.heap_lang Require Import proofmode.
9
From iris_time Require Import Combined.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25

(* Load extra math libraries. *)
From iris_time.union_find.math Require Import LibNatExtra InverseAckermann.
(* Load the mathematical analysis of UnionFind. *)
From iris_time.union_find.math Require Import UnionFind01Data
     UnionFind02EmptyCreate UnionFind03Link UnionFind04Compress
     UnionFind05IteratedCompression UnionFind06Join UnionFind11Rank
     UnionFind12RankEmptyCreate UnionFind13RankLink UnionFind14RankCompress
     UnionFind15RankJoin UnionFind41Potential UnionFind43PotentialAnalysis
     UnionFind44PotentialJoin.

(* Load the heap_lang code *)
From iris_time.union_find Require Import Code.

Section UnionFind.

26
Context `{!tctrHeapG Σ} (nmax : nat).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
27 28 29 30 31 32 33 34 35 36

(* An object in the Union Find data structure is represented by an
   heap_lang location. *)
Notation elem := loc.

(* The logical type of the content of a vertex. *)
Inductive content :=
| Root : nat -> val -> content
| Link : elem -> content.

37
Definition val_of_content (c : content) : option val :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
38
  match c with
39 40
  | Root k v => (λ (k : mach_int), ROOTV(#k, v)) <$> to_mach_int k
  | Link e => Some $ LINKV #e
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
41 42
  end.

43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
Lemma val_of_content_Some :
  forall c v,
    val_of_content c = Some v 
    ( (k1 : mach_int) (k2 : nat) v', v = ROOTV(#k1, v') /\ c = Root k2 v' /\ `k1 = k2)
    \/ ( e : elem, v = LINKV #e /\ c = Link e).
Proof.
  introv Hv. destruct c as [k2 v'|e]; [left|right].
  - simpl in Hv. destruct (to_mach_int k2) as [k1|] eqn:Hk12; [|done].
    eexists k1, k2, v'. repeat split; try naive_solver.
    unfold to_mach_int in Hk12. case_decide; inversion Hk12. done.
  - inversion Hv. eauto.
Qed.

Lemma val_of_content_Some_Root :
  forall k2 v v',
    val_of_content (Root k2 v') = Some v 
    ( (k1 : mach_int), v = ROOTV(#k1, v') /\ `k1 = k2).
Proof.
  introv [(? & ? & ? & -> & [= -> ->] & ?)|(? & ? & [=])]%val_of_content_Some. eauto.
Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
(* Hints for the type-checker. *)

(* It seems important that [D], [R], and [V] which are the public parameters to
   [UF], mention [elem] in their types, as opposed to [loc]. Internally [elem]
   is equal to [loc]. Ultimately, however, the type [elem] is made opaque. *)

Implicit Types x y r : elem.
Implicit Types v : val.
Implicit Types D : LibSet.set elem.  (* domain *)
Implicit Types F : binary elem.      (* edges *)
Implicit Types K : elem -> nat.      (* rank *)
Implicit Types R : elem -> elem.     (* functional view of [is_repr F] *)
Implicit Types V : elem -> val.      (* data stored at the roots *)
Implicit Types M : gmap elem content. (* view of the memory *)

(* -------------------------------------------------------------------------- *)

(* Invariants and representation predicate. *)

(* The predicate [Mem ...] relates the mathematical graph encoded by [D/F/K/V]
   and the memory encoded by the finite map [M]. In short,
    1. elements of [D] have a mapping in M;
    2. the links in [M] coincide with the links in [F];
    3. the rank and data stored at a root in [M] agree with [K] and [V]. *)

Definition Mem D F K V M : Prop :=
  forall x, x \in D ->
    match M!!x with
    | Some (Link y)   => F x y
    | Some (Root k v) => is_root F x /\ k = K x /\ v = V x
    | None => False
    end.

(* The predicate [Inv ...] relates the mathematical graph encoded by [D/F/K/V]
   and the view that is exposed to the client, which is encoded by [D/R/V].
   In short,
   1. [D/F/K] form a ranked disjoint set forest, as per [is_rdsf];
   2. [R] is included in [is_repr F],
      which means that [R x = y] implies [is_repr F x y],
      or in other words, [R] agrees with [F];
   3. [V] agrees with [R]. *)

Record Inv D F K R V : Prop := {
  Inv_rdsf  : is_rdsf D F K;
  Inv_incl  : fun_in_rel R (is_repr F);
  Inv_data  : forall x, V x = V (R x)
}.

Hint Resolve is_rdsf_is_dsf.
Hint Resolve Inv_rdsf Inv_incl Inv_data.

(* Throughout, we instantiate the parameter [r] of Alstrup et al.'s proof
   with the value 1. Thus, we write just [Phi] for [Phi 1]. *)

Notation Phi := (Phi 1).

(* [UF D R V] is the representation predicate. It is an abstract predicate: the
   client uses this predicate, but does not know how it is defined. *)

(* The definition asserts the existence (and ownership) of a group of references,
   whose content is described by a finite map [M]. It asserts the two invariants
   above. Finally, it asserts the existence (and ownership) of [Phi] time credits,
   which have been set aside to help pay for future operations. The definition
   quantifies existentially over [F/K/M], which therefore are not exposed to the
   client. *)

Definition mapsto_M M : iProp Σ :=
131
  ([ map] l  c  M, from_option (mapsto l 1) False (val_of_content c))%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
132 133 134 135 136 137

Definition UF D R V : iProp Σ :=
  ( F K M,
   Inv D F K R V  
   Mem D F K V M  
  mapsto_M M 
138 139
  TC (11 * Phi D F K) 
  TR (card D))%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470

(* -------------------------------------------------------------------------- *)

(* The functions [V] and [R] are compatible with [R]. In other words, every
   member of an equivalence class must have the same image through [V] (see
   [Inv_data]) and through [R]. For this reason, when we wish to update one of
   these functions, we must update it not just at one point, but at a whole
   equivalence class. *)

(* The function [update1 R f x b] coincides with the function [f] everywhere,
   except on the equivalence class of [x], whose elements are mapped to [b]. *)

Definition update1 {B : Type} (f : elem -> B) R x (b : B) :=
  fcupdate f (fun z => R z = R x) b.

(* The function [update2 R f x y b] coincides with the function [f] everywhere,
   except on the equivalence classes of [x] and [y], whose elements are mapped
   to [b]. *)

Definition update2 {B : Type} (f : elem -> B) R x y b :=
  fcupdate f (fun z => R z = R x \/ R z = R y) b.

(* Updating [V] by mapping the equivalence classes of [x] and [x] to [V x]
   has no effect. *)

Lemma update2_V_self : forall D F K R V x,
  Inv D F K R V ->
  update2 V R x x (V x) = V.
Proof using.
  introv [ _ _ H ]. unfold update2.
  eapply fcupdate_self; intros.
  branches; rewrite H; congruence.
Qed.

(* If [x] is a root, then updating [R] by mapping the equivalence classes of [x]
   and [x] to [x] has no effect. *)

Lemma update2_R_self : forall R x,
  R x = x ->
  update2 R R x x x = R.
Proof using.
  intros. unfold update2.
  eapply fcupdate_self; intros.
  branches; congruence.
Qed.

(* Updating [f] at [R x] and [R y] is the same as updating [f] at [x] and [y]. *)

Lemma update2_root : forall (B : Type) (f : elem -> B) R x y b,
  idempotent R ->
  update2 f R (R x) (R y) b = update2 f R x y b.
Proof using.
  introv H. unfold update2. do 2 rewrite* H.
Qed.

(* Updating [V] at [x] and [y] is the same as updating [V] at [y] and [x]. *)

Lemma update2_sym : forall B (f : elem -> B) R x y b,
  update2 f R x y b = update2 f R y x b.
Proof using.
  intros. extens. intros z. unfold update2.
  f_equal. clear z. extens; intros z. tauto.
Qed.

(* -------------------------------------------------------------------------- *)

(* Exploitation and preservation lemmas for the invariant [Inv]. *)

(* If [x] is in the domain and [r] is its representative, then [r] is in the
   domain and [r] is its own representative. *)

Lemma Inv_root : forall D F K R V x r,
  Inv D F K R V ->
  x \in D ->
  r = R x ->
  r \in D /\ R r = r.
Proof using.
  intros; subst; split.
  applys* sticky_R.
  applys* idempotent_R.
Qed.

(* The invariant is preserved when a new element [r] is created and the
   function [V] is updated at [r] in an arbitrary manner. *)

Lemma Inv_make : forall D R F K V D' V' r v,
  Inv D F K R V ->
  r \notin D ->
  D' = D \u \{r} ->
  V' = update1 V R r v ->
  Inv D' F K R V'.
Proof using.
  introv HI Dr ED EV. subst D'. lets [Hrdsf Hroots Hdata]: HI.
  constructor.
  { eauto using is_rdsf_create. }
  { auto. }
  { subst V'. eapply fcupdate_absorbs; intros; eauto.
    rewrites* (>> idempotent_R R). }
Qed.

(* The invariant is preserved by updating [V] at one equivalence class. *)

Lemma Inv_update1 : forall D F K R V x v,
  Inv D F K R V ->
  Inv D F K R (update1 V R x v).
Proof using.
  introv [? ? ?]. constructors~; intros.
  eapply fcupdate_absorbs; intros; eauto.
  rewrites* (>> idempotent_R R).
Qed.

(* The invariant is preserved by a [link] operation. *)

(* The hypothesis is that the invariant holds and [x] and [y] are distinct roots
   in the domain. The conclusion is that the invariant holds again and the
   potential [Phi] grows by at most 2. The domain [D] is unchanged, while the
   other parameters [F'/K'/R'/V'/z] are described by five equations. *)

Lemma Inv_link: forall D R F K V F' K' V' x y z,
  (* Hypotheses: *)
  Inv D F K R V ->
  x  y ->
  x \in D ->
  y \in D ->
  R x = x ->
  R y = y ->
  (* Five equations, describing the situation after the link: *)
  z = new_repr_by_rank K x y ->
  F' = link_by_rank_F F K x y ->
  K' = link_by_rank_K K x y ->
  V' = update2 V R x y (V z) ->
  let R' := link_by_rank_R R x y z in
  (* Conclusions: *)
  Inv D F' K' R' V' /\
  (Phi D F' K' <= Phi D F K + 2)%nat.
Proof.
  introv HI. intros. subst R' F' K' V' z. split. constructor.
  (* Preservation of [is_rdsf]. *)
  { eauto 8 using is_rdsf_link, R_self_is_root. }
  (* Preservation of the agreement between [R] and [F]. *)
  { eauto 8 using link_by_rank_R_link_by_rank_F_agree, R_self_is_root. }
  (* Preservation of the agreement between [V] and [R]. *)
  { intros w.
    unfold update2, fcupdate, link_by_rank_R. repeat case_if~.
    { false. forwards* HR: idempotent_R R. rewrite ->HR in *. tauto. }
    { rewrites~ <- (>> Inv_data HI). }
  }
  (* Change in potential. *)
  { eapply potential_increase_during_link; eauto using R_self_is_root. }
Qed.

(* This tactic helps apply the above lemma. The user is supposed to supply
   expressions for [F'/K'/V'/z], which we prove equal to what we expect.
   This allows some flexibility. *)

Ltac Inv_link F' K' V' x y z :=
  match goal with HInv: Inv ?D ?F ?K ?R ?V |- _ =>
    let Hpotential := fresh in
    (* Apply [Inv_link] to appropriate parameters. *)
    forwards* (?&Hpotential):
      (Inv_link _ _ _ _ _ F' K' V' x y z HInv);
    (* We expect to see some equations as sub-goals. We prove them by
       unfolding definitions and performing a simple case analysis. *)
    try solve [
       unfold new_repr_by_rank, link_by_rank_F, link_by_rank_K;
       case_if; solve [ eauto | math ]
     | congruence
    ]
  end.

(* -------------------------------------------------------------------------- *)

(* Exploitation and preservation lemmas for the invariant [Mem]. *)

(* If [x] is in the domain and is a root, then [M] maps [x] to [Root]
   with rank [K x] and data [V x]. *)

Lemma Mem_root : forall D R F K M V x,
  Inv D F K R V ->
  Mem D F K V M ->
  x \in D ->
  R x = x ->
  M!!x = Some (Root (K x) (V x)).
Proof using.
  introv HI HM Dx Rxx.
  forwards~ HV: HM x. destruct (M!!x) as [[]|]; [| |done].
    destruct HV as (?&?&?). congruence.
    false* (>> R_self_is_root HI HV).
Qed.

(* Conversely, if [M] maps [x] to [Root], then [x] is a root whose
   rank and data are as predicted by [M]. *)

Lemma Mem_root_inv : forall D F K M V x rx vx,
  Mem D F K V M ->
  x \in D ->
  M!!x = Some(Root rx vx) ->
  is_root F x /\ rx = K x /\ vx = V x.
Proof using.
  introv HM Dx HE. forwards~ HVx: HM x.
  destruct (M!!x) as [[]|]; [|false|done]. inverts* HE.
Qed.

(* [Mem] is preserved when a new element [r] is created with rank 0 and the
   function [V] is updated at [r] in an arbitrary manner. *)

Lemma Mem_make : forall D R F K D' r M V v,
  Inv D F K R V ->
  Mem D F K V M ->
  is_rdsf D F K ->
  r \notin D ->
  D' = D \u \{r} ->
  Mem D' F K (update1 V R r v) (<[r:=Root 0 v]>M).
Proof using.
  introv HI HV HG Dr -> Dx.
  rewrite in_union_eq in_single_eq in Dx. destruct Dx as [Dx| ->].
  { rewrite lookup_insert_ne; [|naive_solver].
    rewrite /update1 fcupdate_miss; [by apply HV|].
    intro. forwards* : R_is_identity_outside_D R r.
    forwards*: Inv_root x (R x). intuition congruence. }
  { rewrite lookup_insert /update1 fcupdate_hit //. splits.
    { eauto using only_roots_outside_D with is_dsf. }
    { (* We use the fact that [K] is zero outside the domain. *)
      erewrite is_rdsf_zero_rank_outside_domain; eauto. }
    { done. } }
Qed.

(* [Mem] is preserved by installing a link from a root [x] to a root [y]
   without updating any rank. *)

Lemma Mem_link : forall D F R K F' M V V' x y,
  Inv D F K R V ->
  Mem D F K V M ->
  x \in D ->
  x = R x ->
  y = R y ->
  F' = UnionFind03Link.link F x y ->
  V' = update2 V R x y (V y) ->
  Mem D F' K V' (<[x:=Link y]>M).
Proof using.
  introv HI HR Dx Rx Ry EG' HV. subst F'.
  intros a Da. specializes HR Da.
  destruct (decide (x = a)) as [->|].
  { rewrite lookup_insert. eauto using link_appears. }
  rewrite lookup_insert_ne //. destruct (M!!a) as [[]|]; [| |done]; first last.
  { eauto using link_previous. }
  rewrite~ HV. destruct HR as (?&?&E). splits*.
  { applys* is_root_link. }
  rewrites (rm E).
  unfold update2, fcupdate. rewrites <- (rm Rx). rewrites <- (rm Ry).
  forwards* Ra: is_root_R_self a. rewrite Ra. case_if~.
  branches. false. congruence.
Qed.

(* [Mem] is preserved by installing a link from a root [x] to a root [y]
   and incrementing the rank of [y]. *)

Lemma Mem_link_incr : forall D F R K F' K' M V V' x y (rx : nat) v,
  Inv D F K R V ->
  Mem D F K V M ->
  x \in D ->
  y \in D ->
  x = R x ->
  y = R y ->
  x  y ->
  rx = K x ->
  F' = UnionFind03Link.link F x y ->
  K' = fupdate K y (1 + K x)%nat ->
  v = V y ->
  V' = update2 V R x y (V y) ->
  Mem D F' K' V' (<[y:=Root (rx + 1) v]>(<[x:=Link y]>M)).
Proof using.
  introv HI HM Dx Dy Rx Ry HN Hy Kx HK. introv Hv HV'.
  forwards* HV: (>> Mem_link V V' x y HM).
  sets M': (<[x := Link y]>M). clearbody M'.
  intros a Da. specializes HV Da. destruct (decide (y = a)) as [->|].
  { rewrite lookup_insert. splits.
    { subst F'. applys* is_root_link. applys* R_self_is_root. }
    { subst K'. subst rx. rewrite fupdate_same. math. }
    { subst v. subst V'. rewrite /update2 fcupdate_hit; by auto. } }
  rewrite lookup_insert_ne //. destruct (M'!!a) as [[]|]; [| |done].
  { subst F' K'. destruct HV. split~. unfolds fupdate. case_if~. }
  { subst F'. auto. }
Qed.

(* [Mem] is preserved by installing a direct link from [x] to [y] during
   path compression. *)

Lemma Mem_compress : forall D F K F' M V x y,
  Mem D F K V M ->
  x \in D ->
  F' = compress F x y ->
  Mem D F' K V (<[x:=Link y]>M).
Proof using.
  introv HR Dx EG'. subst.
  intros a Da. specializes HR Da. destruct (decide (x = a)) as [->|].
  { rewrite lookup_insert. eauto using compress_x_z. }
  { rewrite lookup_insert_ne //. destruct (M!!a) as [[]|];
      [|by eauto using compress_preserves_other_edges|done].
    destruct HR. split*.
    eauto using compress_preserves_roots_other_than_x. }
Qed.

(* [Mem] is preserved when [V] is updated at one equivalence class and [M]
   is updated at the representative element. *)

Lemma Mem_update1 : forall D R F K M V r x v,
  Inv D F K R V ->
  Mem D F K V M ->
  x \in D ->
  r = R x ->
  Mem D F K (update1 V R x v) (<[r := Root (K r) v]>M).
Proof using.
  introv HI HM E Rx. forwards* (Dr&Rr): Inv_root x r.
  intros y Dy. specializes HM Dy. destruct (decide (r = y)) as [->|].
  { rewrite lookup_insert. splits.
    { applys* R_self_is_root. }
    { done. }
    { rewrite /update1 fcupdate_hit; congruence. } }
  { rewrite lookup_insert_ne // /update1 /fcupdate. case_if~.
    destruct~ (M!!y) as [[]|]; [|done..]. destruct HM as (H1&H2&H3).
    forwards*: is_root_R_self H1. congruence. }
Qed.

(* -------------------------------------------------------------------------- *)

(* Private lemmas about the representation predicate and about [mapsto_M]. *)


Lemma mapsto_M_acc : forall M x c,
  M !! x = Some c ->
471 472 473 474
  mapsto_M M -
     v, val_of_content c = Some v  x  v 
     ( c' v', val_of_content c' = Some v' -
               x  v' - mapsto_M (<[x:=c']>M)).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
475 476 477
Proof.
  introv HM. iIntros "HM".
  rewrite -[in mapsto_M _](insert_id _ _ _ HM) -insert_delete /mapsto_M.
478 479 480 481
  rewrite big_sepM_insert ?lookup_delete //. iDestruct "HM" as "[Hc HM]".
  destruct (val_of_content c); [|done]. iExists _. iFrame. iSplit; [done|].
  iIntros (c' v' Hv') "?".
  rewrite -insert_delete big_sepM_insert ?lookup_delete // Hv'. iFrame.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
482 483 484 485
Qed.

Lemma mapsto_M_acc_same : forall M x c,
  M !! x = Some c ->
486 487
  mapsto_M M -
     v, val_of_content c = Some v  x  v  (x  v - mapsto_M M).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
488
Proof.
489 490 491 492
  introv HM. iIntros "HM".
  iDestruct (mapsto_M_acc with "HM") as (v Hv) "[Hv HM]"; [done|].
  iExists _. iFrame. iSplit; [done|].
  iSpecialize ("HM" $! _ _ Hv). by rewrite insert_id.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508
Qed.

(* TODO : that should go into Iris libraries for big ops *)
Lemma mapsto_M_union : forall M1 M2,
  M1 ## M2 ->
  mapsto_M M1  mapsto_M M2  mapsto_M (M1  M2).
Proof.
  introv HM12. unfold mapsto_M.
  induction M1 as [|l x M1 ? IH] using map_ind.
  { by rewrite big_opM_empty !left_id. }
  rewrite -insert_union_l !big_sepM_insert //; last first.
  { apply lookup_union_None; split; [done|]. specialize (HM12 l).
    rewrite lookup_insert in HM12. revert HM12. case: (M2 !! l)=>//=. }
  rewrite -assoc. f_equiv. apply IH. by eapply map_disjoint_insert_l.
Qed.

509 510 511 512
Lemma mapsto_M_insert : forall M x c v,
  M !! x = None ->
  val_of_content c = Some v ->
  x  v  mapsto_M M  mapsto_M (<[x:=c]>M).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
513
Proof.
514
  introv Mxc Hcv. by rewrite /mapsto_M big_sepM_insert // Hcv.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
515 516 517 518 519 520 521 522 523
Qed.

Lemma mapsto_M_disjoint : forall M1 M2,
  mapsto_M M1 - mapsto_M M2 -  M1 ## M2 .
Proof.
  iIntros "* HM1 HM2" (x). unfold mapsto_M.
  destruct (M1!!x) eqn:HM1, (M2!!x) eqn:HM2=>//.
  iDestruct (big_sepM_lookup with "HM1") as "H1"=>//.
  iDestruct (big_sepM_lookup with "HM2") as "H2"=>//.
524
  do 2 destruct val_of_content; try done.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567
  by iDestruct (mapsto_valid_2 with "H1 H2") as %[].
Qed.

(* -------------------------------------------------------------------------- *)

(* Public lemmas about the representation predicate. *)

(* If [UF D R V] holds, then [R] is idempotent. *)

Theorem UF_idempotent : forall D R V,
  UF D R V -  idempotent R .
Proof using.
  iDestruct 1 as (?????) "?". eauto 10 using idempotent_R.
Qed.

(* If [UF D R V] holds, then [R] preserves [D]. *)

Theorem UF_image : forall D R V x, x \in D 
  UF D R V -  R x \in D .
Proof using.
  iDestruct 1 as (?????) "?". eauto 10 using sticky_R.
Qed.

(* If [UF D R V] holds, then [R] is the identity outside of [D]. *)

Theorem UF_identity : forall D R V x, x \notin D ->
  UF D R V -  R x = x .
Proof using.
  iDestruct 1 as (?????) "?". eauto 10 using R_is_identity_outside_D.
Qed.

(* If [UF D R V] holds, then [V] is compatible with [R]. *)

Theorem UF_compatible : forall D R V x, x \in D ->
  UF D R V -  V x = V (R x) .
Proof using.
  iDestruct 1 as (?????) "?". eauto.
Qed.

(* An empty instance of the Union-Find data structure can be created out of
   thin air. This is how the data structure is initialized. *)

Theorem UF_create : forall V,
568
  TCTR_invariant nmax ={}= UF \{} id V.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
569 570 571 572 573 574 575 576 577 578 579
Proof using.
  unfold UF. iIntros (V) "#?".
  iExists (@LibRelation.empty elem), (λ _, 0%nat), .
  repeat iSplitL.
  { iPureIntro. constructors.
    { apply is_rdsf_empty. }
    { intro x. eapply is_repr_empty. }
    { eauto. } }
  { iIntros "!%" (??). false. }
  { rewrite /mapsto_M. by auto. }
  { rewrite Phi_empty. by iApply zero_TC. }
580
  { rewrite card_empty. by iApply zero_TR. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599
Qed.

(* Two separate instances of the UnionFind data structure can be merged, without
   actually doing anything at runtime. *)

(* In principle, we could also prove the converse property, [UF_split]. A UnionFind
   data structure can be split in two independent parts, provided the split respects
   the equivalence relation. Considering the amount of dreary work that went into
   establishing [UF_join], I leave this to future work. *)

Theorem UF_join : forall D1 R1 V1 D2 R2 V2,
  UF D1 R1 V1 - UF D2 R2 V2 -
  UF
    (D1 \u D2)
    (fun x => If x \in D1 then R1 x else R2 x)
    (fun x => If x \in D1 then V1 x else V2 x)
    D1 \# D2 .
Proof using.
  intros.
600 601
  iDestruct 1 as (F1 K1 M1 HI1 HM1) "(HM1 & HTC1 & TR1)".
  iDestruct 1 as (F2 K2 M2 HI2 HM2) "(HM2 & HTC2 & TR2)".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664
  sets D: (D1 \u D2).
  sets R: (fun x => If x \in D1 then R1 x else R2 x).
  sets V: (fun x => If x \in D1 then V1 x else V2 x).
  set (F := LibRelation.union F1 F2).
  set (K := fun x => If x \in D1 then K1 x else K2 x).
  set (M := M1  M2).

  (* Disjointness lemmas. Trivial and painful. *)

  iDestruct (mapsto_M_disjoint with "HM1 HM2") as %HM12.

  assert (forall x, x \in D1 -> x \in D2 -> False).
  { intros l Hl1%HM1 Hl2%HM2. specialize (HM12 l).
    destruct (M1!!l) eqn:HM1l=>//. destruct (M2!!l) eqn:HM2l=>//. }

  assert (D1 \# D2) by by rew_set.

  assert (forall x, x \in D2 -> x \notin D1).
  { intros. intro. eauto. }

  assert (forall x y, F1 x y -> x \in D1).
  { eauto with confined is_dsf. }

  assert (forall x y, F2 x y -> x \in D2).
  { eauto with confined is_dsf. }

  assert (forall x, x \in D1 -> F1 x = F x).
  { intros. subst F. extens; intros y.
    unfold LibRelation.union; split; intros; try branches; eauto; false; eauto. }

  assert (forall x, x \in D2 -> F2 x = F x).
  { intros. subst F. extens; intros y.
    unfold LibRelation.union; split; intros; try branches; eauto; false; eauto. }

  assert (forall x, x \in D1 -> K1 x = K x).
  { intros. subst K. simpl. cases_if~. }

  assert (forall x, x \in D2 -> K2 x = K x).
  { intros. subst K. simpl. cases_if~. false; eauto. }

  assert (forall x, x \in D1 -> R1 x = R x).
  { intros. subst R. simpl. cases_if~. }

  assert (forall x, x \in D2 -> R2 x = R x).
  { intros. subst R. simpl. cases_if~. false; eauto. }

  assert (forall x, x \in D1 -> V1 x = V x).
  { intros. subst V. simpl. cases_if~. }

  assert (forall x, x \in D2 -> V2 x = V x).
  { intros. subst V. simpl. cases_if~. false; eauto. }

  assert (forall x, x \in D1 -> M1!!x = M!!x).
  { intros x Hx%HM1. subst M. destruct (M1!!x) eqn:? =>//.
    symmetry. by apply lookup_union_Some_l. }

  assert (forall x, x \in D2 -> M2!!x = M!!x).
  { intros x Hx%HM2. subst M. destruct (M2!!x) eqn:? =>//.
    symmetry. by apply lookup_union_Some_r. }

  iSplit; last done. iExists F, K, M.

  iCombine "HTC1 HTC2" as "HTC".
665
  iCombine "TR1 TR2" as "HTR".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
666
  rewrite -mapsto_M_union // -Nat.mul_add_distr_l (@Phi_join 1 _ D F K); eauto.
667
  rewrite -card_disjoint_union; eauto using is_rdsf_finite; [].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721
  iFrame. iPureIntro. split.

  (* Preservation of [Inv]. *)
  { destruct HI1, HI2. constructor.
    (* Preservation of [is_rdsf]. *)
    { subst D F K. eapply is_rdsf_join; eauto. }
    (* Preservation of the agreement between [R] and [F]. *)
    { intros x. subst F R. simpl. cases_if.
      (* Case: [x \in D1]. *)
      { eapply is_repr_join_direct_1; eauto. }
      (* Case: [x \notin D1]. *)
      { eapply is_repr_join_direct_2; eauto. }
    }
    (* Preservation of the compatibility of [V]. *)
    { intros x. subst V R. simpl. cases_if; [ | destruct (classic (x \in D2)) ].
      (* Case: [x \in D1]. *)
      { assert (R1 x \in D1). { eauto using sticky_R. }
        cases_if. intuition eauto. }
      (* Case: [x \in D2]. *)
      { assert (R2 x \in D2). { eauto using sticky_R. }
        cases_if. false; eauto. eauto. }
      (* Case: [x \notin D1 \u D2]. *)
      { assert (h: R2 x = x). { eapply R_is_identity_outside_D; eauto with is_dsf. }
        rewrite h. cases_if. reflexivity. }
    }
  }

  (* Preservation of [Mem]. *)
  { intros x Dx. subst D. rewrite in_union_eq in Dx.
    destruct Dx as [ Dx | Dx ].
    { forwards : HM1 Dx. destruct (M1!!x) as [c|] eqn:EQM1=>//.
      unfold is_root in *. rewrite (lookup_union_Some_l _ _ _ _ EQM1) //.
      repeat match goal with h: forall_ x \in D1, _ |- _ =>
        specializes h Dx; try rewrite <- h
      end. done. }
    { forwards : HM2 Dx. destruct (M2!!x) as [c|] eqn:EQM2=>//.
      unfold is_root in *. rewrite (lookup_union_Some_r _ _ _ _ HM12 EQM2) //.
      repeat match goal with h: forall_ x \in D2, _ |- _ =>
        specializes h Dx; try rewrite <- h
      end. done. } }
Qed.

(* -------------------------------------------------------------------------- *)

(* Verification of [make]. *)

(* The function call [make v] requires [UF D R V] as well as O(1) time credits.
   It returns a new element [x], that is, [x] is not in [D]. It updates the
   data structure to [UF D' R' V'], where:
   1. [D'] is [D] extended with [x];
   2. [R'] is [R];
   3. [V'] is [V] extended with a mapping of [x] to [v]. *)

Theorem make_spec : forall D R V v,
722
  TCTR_invariant nmax -
723
  {{{ UF D R V  TC 26 }}}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
724 725 726 727 728 729 730 731
    «make v»
  {{{ (x : elem), RET #x;
      let D' := D \u \{x} in
      let V' := update1 V R x «v»%V in
      UF D' R V' 
      x \notin D /\
       R x = x }}}.
Proof using.
732
  iIntros "* #?" (Φ) "!# [HF TC] HΦ".
733 734 735 736
  wp_tick_rec. wp_tick_pair. wp_tick_inj.
  iMod (zero_TR with "[//]") as "TR"=>//.
  wp_tick. wp_alloc x as "Hx". iApply "HΦ".
  iDestruct "HF" as (F K M HI HM) "(HM & TC' & TR')".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
737 738 739 740

  iAssert M !! x = None%I as %Mx.
  { case HMx: (M!!x)=>//.
    iDestruct (big_sepM_lookup with "HM") as "Hx'"=>//.
741
    destruct val_of_content; try done.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
742 743 744 745 746 747
    by iDestruct (mapsto_valid_2 with "Hx Hx'") as %[]. }
  assert (x \notin D) as Dx.
  { intros Dx%HM. by rewrite Mx in Dx. }

  iSplit; [|by eauto 10 using R_is_identity_outside_D].
  iExists _, _, (<[x:=Root 0 _]>M).
748 749 750 751 752 753 754
  rewrite -Phi_extend 1?Nat.mul_add_distr_l; eauto; [].
  iCombine "TC' TC" as "$".

  rewrite card_disjoint_union; eauto using is_rdsf_finite, finite_single; last first.
  { by rewrite disjoint_single_r_eq. }
  rewrite card_single. iCombine "TR' TR" as "$".

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
755 756
  repeat iSplit; try iPureIntro.
  { applys* Inv_make. } { applys* Mem_make. }
757 758 759
  iApply mapsto_M_insert; [done| |by iFrame].
  rewrite /= /to_mach_int decide_left /=; [by apply (proj2_sig mach_int_0)|].
  intros ?. by rewrite (exists_proj1_pi _ mach_int_0).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778
Qed.

(* -------------------------------------------------------------------------- *)

(* Verification of [find]. *)

(* Because [find] is a recursive function, we must begin with a specification
   that is amenable to an inductive proof. It states that [find] essentially
   implements the mathematical predicate [bw_ipc]. If [bw_ipc F x d F'] holds,
   which means that path compression at [x] requires [d] steps and changes the
   graph from [F] to [F'], then [find] requires [d+1] time credits and changes
   the memory from [M] to some [M'] that agrees with [F']. Furthermore, the
   value [r] returned by [find] is the representative of [x]. *)

Lemma find_spec_inductive: forall d D R F K F' M V x,
  Inv D F K R V ->
  Mem D F K V M ->
  x \in D ->
  bw_ipc F x d F' ->
779
  TCTR_invariant nmax -
780
  {{{ mapsto_M M  TC (11*d+11) }}}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
781 782 783
    «find #x»
  {{{ M', RET #(R x); mapsto_M M'   Mem D F' K V M'  }}}.
Proof using.
784
  intros d. induction_wf IH: Wf_nat.lt_wf d.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
785 786 787
  introv HI HM Dx HC. iIntros "#?" (Φ) "!# [HM TC] HΦ /=".
  iDestruct "TC" as "[TCd TC]". wp_tick_rec.
  assert (HV := HM _ Dx). destruct (M !! x) as [c|] eqn:? =>//.
788 789 790
  iDestruct (mapsto_M_acc_same with "HM") as (v Hv) "[Hx HM]"=>//. wp_tick_load.
  iDestruct ("HM" with "Hx") as "HM".
  destruct (val_of_content_Some _ _ Hv) as [(k1 & k2 & v' & -> & -> & ?)|(y & -> & ->)].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
791 792 793 794 795 796 797 798 799 800 801 802 803 804 805
  (* Case: Root. *)
  { wp_tick_match. wp_tick_proj. wp_tick_seq. wp_tick_proj. wp_tick_seq.
    destruct HV as [HR HP]. forwards* EQ : is_root_R_self HR. rewrite EQ.
    iApply "HΦ". iFrame. iPureIntro.
    invert HC; intros. by subst. by false* a_root_has_no_parent HR.
  }
  (* Case: Link. *)
  { wp_tick_match. rename HV into HF. invert HC.
    { intros. subst F. subst. false* a_root_has_no_parent. }
    intros F'0 F'' x0 y0 z' d' HF' HR' HB' EF' Ex Ed EF''. subst F'' x0 d.
    lets* E: is_dsf_functional D HF HF'. subst y0. clear HF'.
    assert (y \in D). { eauto with confined is_dsf. }
    assert (z' = R y). { symmetry. eapply is_repr_incl_R; eauto. } subst z'.
    forwards IH' : IH HI HM HB'; [math|done|].
    iCombine "TCd TC" as "TC".
806
    math_rewrite (11 * S d' + 6 = 11 * d' + 11 + 6)%nat.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
807
    iDestruct "TC" as "[TCd TC]".
808 809
    wp_apply (IH' with "[//] [$HM $TCd]").
    iIntros (M') "[HM' hM']". iDestruct "hM'" as %HM'. wp_tick_let.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
810
    assert (HV := HM' _ Dx). destruct (M' !! x) as [c|] eqn:? =>//.
811 812 813
    iDestruct (mapsto_M_acc with "HM'") as (v' Hv') "[Hx HM']"=>//.
    wp_tick_inj. wp_tick_store. wp_tick_seq.
    iDestruct ("HM'" $! (Link (R y)) _ eq_refl with "Hx") as "HM'".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
814 815 816 817 818 819 820 821 822 823
    assert (is_equiv F x y). { eauto using path_is_equiv with rtclosure. }
    assert (R x = R y) as ->. { eauto using is_equiv_incl_same_R. }
    iApply ("HΦ" with "[$HM']").
    iPureIntro. applys~ Mem_compress HM'. }
Qed.

(* The function call [find x] requires [UF D R V] as well as O(alpha(D)) time
   credits. It preserves [UF D R V] and returns the representative of [x]. *)

Theorem find_spec : forall D R V x, x \in D ->
824
  TCTR_invariant nmax -
825
  {{{ UF D R V  TC (22 * alpha (card D) + 44) }}}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
826 827 828 829
    «find #x»
  {{{ RET #(R x); UF D R V }}}.
Proof using.
  introv Dx. iIntros "#?" (Φ) "!# [UF TC1] HΦ".
830
  iDestruct "UF" as (F K M HI HM) "(HM & TC2 & TR)".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
831 832
  forwards* (d&F'&HC&HP): amortized_cost_of_iterated_path_compression_simplified x.
  iCombine "TC1 TC2" as "TC".
833
  rewrite [TC (_ + _)](TC_weaken _ (11*Phi D F' K + (11 * d + 11))%nat); [|math].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
834 835 836 837 838 839 840 841 842 843 844 845 846 847 848
  iDestruct "TC" as "[TC1 TC2]".
  iApply (find_spec_inductive with "[//] [$TC2 $HM]")=>//.
  iIntros "!>" (M') "[HM' %]". iApply "HΦ".
  iExists _, _, _. iFrame. iPureIntro. split; [|done].
  split; eauto 10 using is_rdsf_bw_ipc, bw_ipc_preserves_RF_agreement.
Qed.

(* -------------------------------------------------------------------------- *)

(* Verification of [get]. *)

(* The function call [get x] requires [UF D R V] as well as O(alpha(D)) time
   credits. It preserves [UF D R V] and returns the data stored at [x]. *)

Theorem get_spec : forall D R V x, x \in D ->
849
  TCTR_invariant nmax -
850
  {{{ UF D R V  TC (22 * alpha (card D) + 57) }}}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
851 852 853 854
    «get #x»
  {{{ RET V x; UF D R V }}}.
Proof using.
  introv Dx. iIntros "#?" (Φ) "!# [UF TC] HΦ".
855
  math_rewrite (22 * alpha (card D) + 57 = 22 * alpha (card D) + 44 + 13)%nat.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
856
  iDestruct "TC" as "[TC1 TC2]".
857 858
  wp_tick_rec.
  wp_apply (find_spec with "[//] [$TC1 $UF]")=>//.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
859 860 861
  iIntros "UF". wp_tick_let. iDestruct "UF" as (F K M HI HM) "[HM TC]".
  forwards* (Drx&Rrx): Inv_root x (R x).
  forwards* EM: Mem_root (R x).
862
  iDestruct (mapsto_M_acc_same with "HM") as (v Hv) "[Hx HM]"=>//. wp_tick_load.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
863
  iDestruct ("HM" with "Hx") as "HM".
864
  destruct (val_of_content_Some_Root _ _ _ Hv) as (k1 & -> & _).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880
  wp_tick_match. wp_tick_proj. wp_tick_seq. wp_tick_proj. wp_tick_let.
  rewrite -(Inv_data _ _ _ _ _ HI). iApply "HΦ".
  iExists _, _, _. eauto with iFrame.
Qed.


(* -------------------------------------------------------------------------- *)

(* Verification of [set]. *)

(* The function call [set x v] requires [UF D R V] as well as O(alpha(D)) time
   credits. It produces [UF D R V'], where [V'] is obtained from [V] by mapping
   the equivalence class of [x] to [v]. *)

Theorem set_spec : forall D R V x v,
  x \in D ->
881
  TCTR_invariant nmax -
882
  {{{ UF D R V  TC (22 * alpha (card D) + 62) }}}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
883 884 885 886
    «set #x v»
  {{{ RET #(); UF D R (update1 V R x «v»%V) }}}.
Proof using.
  introv Dx. iIntros "#?" (Φ) "!# [UF TC] HΦ".
887
  math_rewrite (22 * alpha (card D) + 62 = 22 * alpha (card D) + 44 + 18)%nat.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
888
  iDestruct "TC" as "[TC1 TC2]".
889
  wp_tick_rec. wp_tick_let. wp_apply (find_spec with "[//] [$TC1 $UF]")=>//.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
890 891 892
  iIntros "UF". wp_tick_let. iDestruct "UF" as (F K M HI HM) "[HM TC]".
  forwards* (Drx&Rrx): Inv_root x (R x).
  forwards* EM: Mem_root (R x).
893 894 895 896
  iDestruct (mapsto_M_acc with "HM") as (v' Hv') "[Hx HM]"=>//. wp_tick_load.
  destruct (val_of_content_Some_Root _ _ _ Hv') as (k1 & -> & _).
  wp_tick_match. wp_tick_proj. wp_tick_seq. wp_tick_proj. wp_tick_seq.
  wp_tick_pair. wp_tick_inj. wp_tick_store.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
897 898
  iApply "HΦ". iExists _, _, _. iFrame.
  iSplit; [auto using Inv_update1|]. iSplit; [eauto using Mem_update1|].
899 900
  rewrite Rrx. iApply ("HM" with "[%] Hx").
  simpl in *. by destruct (to_mach_int (K (R x))); inversion Hv'.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
901 902 903 904 905 906 907 908 909 910 911 912
Qed.

(* -------------------------------------------------------------------------- *)

(* Verification of [eq]. *)

(* The function call [eq x y] requires [UF D R V] as well as O(alpha(D)) time
   credits. It preserves [UF D R V] and returns a Boolean outcome which
   indicates whether [x] and [y] are members of a common equivalence class. *)

Theorem eq_spec : forall D R V x y,
  x \in D -> y \in D ->
913
  TCTR_invariant nmax -
914
  {{{ UF D R V  TC (44 * alpha (card D) + 92) }}}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
915 916 917 918
    «eq #x #y»
  {{{ RET #(bool_decide (R x = R y)); UF D R V }}}.
Proof using.
  introv Dx Dy. iIntros "#?" (Φ) "!# [UF TC] HΦ".
919 920
  math_rewrite (44 * alpha (card D) + 92 =
                (22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 4)%nat.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
921
  iDestruct "TC" as "[[TC1 TC2] TC3]".
922
  wp_tick_rec. wp_tick_let.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942
  wp_apply (find_spec with "[//] [$TC1 $UF]")=>//. iIntros "UF".
  wp_apply (find_spec with "[//] [$TC2 $UF]")=>//. iIntros "UF".
  wp_tick_op.
  rewrite (bool_decide_iff (#(R x) = #(R y)) (R x = R y)); last (split; congruence).
  by iApply "HΦ".
Qed.

(* -------------------------------------------------------------------------- *)

(* Verification of [link]. (This is an internal function.) *)

(* The function call [link x y] requires [UF D R V] as well as O(1) time credits.
   It requires [x] and [y] to be roots. It chooses the new representative [z] to
   be one of [x] or [y], and returns [z], together with [UF D' R' V'], where:
   1. [D'] is [D], i.e., the domain is unchanged;
   2. [R'] is [R], where the equivalence classes of [x] and [y] are mapped to [z];
   3. [V'] is [V], where the equivalence classes of [x] and [y] are mapped to [V z].
*)

Lemma link_spec : forall D R V x y,
943
  (log2 (log2 nmax) < word_size - 1)%nat ->
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
944 945 946 947
  x \in D ->
  y \in D ->
  R x = x ->
  R y = y ->
948
  TCTR_invariant nmax -
949
  {{{ UF D R V  TC 61 }}}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
950 951 952 953
    «link #x #y»
  {{{ z, RET #z; UF D (update2 R R x y z) (update2 V R x y (V z)) 
                   z = x \/ z = y}}}.
Proof using.
954
  introv Hnmax Dx Dy Rx Ry. iIntros "#?" (Φ) "!# [UF TC] HΦ".
955
  wp_tick_rec. wp_tick_let.
956
  iDestruct "UF" as (F K M HI HM) "(HM & TC'TR)".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
957 958 959 960 961 962 963 964 965
  wp_tick_op. case_bool_decide as Hxy.
  (* Case: [x == y]. *)
  { inversion Hxy. subst. wp_tick_if. iApply "HΦ".
    rewrite update2_R_self; [|by eauto]. erewrite update2_V_self; [|by eauto..].
    iSplit; [|by auto]. iExists _, _, _. auto with iFrame. }
  (* Case: [x != y]. *)
  wp_tick_if.
  forwards Hx: HM Dx. forwards Hy: HM Dy.
  destruct (M !! x) as [cx|] eqn:EQx, (M !! y) as [cy|] eqn:EQy=>//.
966
  iDestruct (mapsto_M_acc_same _ x with "HM") as (v Hv) "[Hx HM]"=>//.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
967
  wp_tick_load. iDestruct ("HM" with "Hx") as "HM".
968 969 970 971
  destruct cx; last by false; eauto using a_root_has_no_parent, R_self_is_root.
  destruct (val_of_content_Some_Root _ _ _ Hv) as (k1 & -> & ?).
  wp_tick_match. wp_tick_proj. wp_tick_let. wp_tick_proj. wp_tick_let.
  iDestruct (mapsto_M_acc_same _ y with "HM") as (v' Hv') "[Hy HM]"=>//.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
972
  wp_tick_load. iDestruct ("HM" with "Hy") as "HM".
973 974 975
  destruct cy; last by false; eauto using a_root_has_no_parent, R_self_is_root.
  destruct (val_of_content_Some_Root _ _ _ Hv') as (k1' & -> & ?).
  wp_tick_match. wp_tick_proj. wp_tick_let. wp_tick_proj. wp_tick_seq.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
976 977 978 979
  destruct Hx as (HRx&Kx&Vx). substs. destruct Hy as (HRy&Ky&Vy). substs.
  wp_tick_op; case_bool_decide; wp_tick_if;
    [|wp_tick_op; case_bool_decide; wp_tick_if].
  (* Sub-case: [K x < K y]. *)
980 981
  { iDestruct (mapsto_M_acc _ _ _ EQx with "HM") as (? _) "[Hx HM]".
    wp_tick_inj. wp_tick_store. wp_tick_seq. iApply "HΦ". iSplit; [|by auto].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
982 983 984 985 986 987
    Inv_link
    (* F' := *) (UnionFind03Link.link F x y)
    (* K' := *) K
    (* V' := *) (update2 V R x y (V y))
                x y
    (* z  := *) y.
988 989
    iDestruct "TC'TR" as "[TC' TR]". iCombine "TC' TC" as "TC".
    iExists _, _, (<[x:=Link y]>M). iFrame "% TR".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
990 991 992
    rewrite TC_weaken; [iFrame "TC"|lia]. iSplit; [by eauto using Mem_link|].
    by iApply "HM". }
  (* Sub-case: [K x > K y]. *)
993 994
  { iDestruct (mapsto_M_acc _ _ _ EQy with "HM") as (? _) "[Hy HM]".
    wp_tick_inj. wp_tick_store. wp_tick_seq. iApply "HΦ".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
995 996 997 998 999 1000 1001 1002
    rewrite [update2 _ _ _ _ x]update2_sym. rewrite [update2 _ _ _ _ (V x)]update2_sym.
    iSplit; [|by auto].
    Inv_link
    (* F' := *) (UnionFind03Link.link F y x)
    (* K' := *) K
    (* V' := *) (update2 V R y x (V x))
                y x
    (* z  := *) x.
1003 1004
    iDestruct "TC'TR" as "[TC' TR]". iCombine "TC' TC" as "TC".
    iExists _, _, (<[y:=Link x]>M). iFrame "% TR".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1005 1006 1007
    rewrite TC_weaken; [iFrame "TC"|lia]. iSplit; [by eauto using Mem_link|].
    by iApply "HM". }
  (* Sub-case: [K x = K y]. *)
1008 1009 1010
  { iDestruct (mapsto_M_acc _ _ _ EQy with "HM") as (? _) "[Hy HM]"=>//.
    wp_tick_inj. wp_tick_store.
    iDestruct ("HM" $! (Link _) _ eq_refl with "Hy") as "HM".
1011 1012 1013 1014 1015 1016
    Inv_link
    (* F' := *) (UnionFind03Link.link F y x)
    (* K' := *) (fupdate K x (1 + K y)%nat)
    (* V' := *) (update2 V R x y (V x))
                x y
    (* z  := *) x.
Glen Mével's avatar
Glen Mével committed
1017 1018 1019 1020 1021
    iDestruct "TC'TR" as "[TC' TR]".
    iMod (TR_lt_nmax with "[//] TR") as "[TR %]" ; first done.
    iCombine "TC' TR" as "TC'TR".
    iAssert (card D  nmax)%I%nat as %HDnmax%Nat.log2_le_mono.
    { auto with lia. }
1022
    assert (bool_decide (mach_int_bounded (`k1 + 1))).
1023
    { assert (log2 nmax < 2 ^ (word_size - 1))%nat.
1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034
      { destruct (decide (0 < log2 nmax)%nat); [by eapply Nat.log2_lt_pow2|].
        assert (log2 nmax = 0%nat) as -> by lia. apply power_positive. lia. }
      forwards* Hklog: rank_is_logarithmic (fupdate K x (S (K y))) x.
      rewrite fupdate_same in Hklog.
      assert (S (K y) < 2 ^ (word_size - 1))%nat as HK%inj_lt by lia.
      rewrite Z2Nat_inj_pow -Z.shiftl_1_l Nat2Z.inj_sub in HK;
        [|pose proof word_size_gt_1; lia].
      apply bool_decide_pack. split.
      { destruct (bool_decide_unpack _ (proj2_sig k1)) as [? _]. lia. }
      assert (`k1 = `k1') as -> by lia. rewrite (_:`k1' = K y) //.
      rewrite Z.add_comm -(Nat2Z.inj_add 1). done. }
1035 1036 1037
    wp_tick_seq. wp_tick_op.
    { by rewrite /bin_op_eval /= /to_mach_int decide_left. }
    iDestruct (mapsto_M_acc _ x with "HM") as (v'' Hv'') "[Hx HM]".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1038
    { rewrite lookup_insert_ne //. congruence. }
1039
    wp_tick_pair. wp_tick_inj. wp_tick_store. wp_tick_seq.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1040
    iApply "HΦ". iSplit; [|by auto].
1041 1042
    iDestruct "TC'TR" as "[TC' TR]".
    iExists _, _, _. iFrame "% TR".
1043 1044 1045 1046 1047
    iCombine "TC' TC" as "TC". rewrite TC_weaken; [iFrame "TC"|lia].
    iSplit; last iApply ("HM" with "[%] Hx").
    { iPureIntro. applys* Mem_link_incr HM. congruence. applys update2_sym. }
    rewrite /= -(_:(`k1 + 1) = (K y + 1)%nat) //.
    { by rewrite /to_mach_int decide_left /=. }
1048 1049
    assert (`k1 + 1 = K y + 1)%Z as -> by lia. by rewrite ->Nat2Z.inj_add. }
Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063

(* -------------------------------------------------------------------------- *)

(* Verification of [union]. *)

(* The function call [union x y] requires [UF D R V] as well as O(alpha(D)) time
   credits. It chooses the new representative [z] to be one of [x] or [y], and
   returns [z], together with [UF D' R' V'], where:
   1. [D'] is [D], i.e., the domain is unchanged;
   2. [R'] is [R], where the equivalence classes of [x] and [y] are mapped to [z];
   3. [V'] is [V], where the equivalence classes of [x] and [y] are mapped to [V z].
*)

Theorem union_spec : forall D R V x y,
1064
  (log2 (log2 nmax) < word_size - 1)%nat ->
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1065 1066
  x \in D ->
  y \in D ->
1067
  TCTR_invariant nmax -
1068
  {{{ UF D R V  TC (44 * alpha (card D) + 152) }}}
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1069 1070 1071 1072
    «union #x #y»
  {{{ z, RET #z; UF D (update2 R R x y z) (update2 V R x y (V z)) 
                 z = R x \/ z = R y }}}.
Proof using.
1073
  introv Hnmax Dx Dy.
1074 1075
  math_rewrite (44 * alpha (card D) + 152 =
                (22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 61 + 3)%nat.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1076
  iIntros "#?" (Φ) "!# [UF [[[TC1 TC2] TC3] TC4]] HΦ".
1077
  wp_tick_rec. wp_tick_let.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1078 1079 1080 1081 1082
  wp_apply (find_spec with "[//] [$TC1 $UF]")=>//. iIntros "UF".
  wp_apply (find_spec with "[//] [$TC2 $UF]")=>//. iIntros "UF".
  iDestruct (UF_image _ _ _ x with "UF") as %? =>//.
  iDestruct (UF_image _ _ _ y with "UF") as %? =>//.
  iDestruct (UF_idempotent with "UF") as %Idem =>//.
1083
  wp_apply (link_spec _ _ _ _ _ Hnmax with "[//] [$TC3 $UF]")=>//.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1084 1085 1086 1087 1088
  iIntros (z). by rewrite !update2_root.
Qed.

End UnionFind.

1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102
Definition final_theorems :=
  (@UF_idempotent,
   @UF_image,
   @UF_identity,
   @UF_compatible,
   @UF_create,
   @UF_join,
   @make_spec,
   @find_spec,
   @get_spec,
   @set_spec,
   @eq_spec,
   @union_spec).
Print Assumptions final_theorems.