Proof.v 40.2 KB
Newer Older
 Jacques-Henri Jourdan committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 07, 2018 8 From iris_time.heap_lang Require Import proofmode.  Jacques-Henri Jourdan committed Nov 09, 2018 9 From iris_time Require Import Combined.  Jacques-Henri Jourdan committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 09, 2018 26 Context {!tctrHeapG Σ} (nmax : nat).  Jacques-Henri Jourdan committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 07, 2018 37 Definition val_of_content (c : content) : option val :=  Jacques-Henri Jourdan committed Oct 29, 2018 38  match c with  Jacques-Henri Jourdan committed Nov 07, 2018 39 40  | Root k v => (λ (k : mach_int), ROOTV(#k, v)) <$> to_mach_int k | Link e => Some$ LINKV #e  Jacques-Henri Jourdan committed Oct 29, 2018 41 42  end.  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 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 Σ :=  Jacques-Henri Jourdan committed Nov 07, 2018 131  ([∗ map] l ↦ c ∈ M, from_option (mapsto l 1) False (val_of_content c))%I.  Jacques-Henri Jourdan committed Oct 29, 2018 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 ∗  Jacques-Henri Jourdan committed Nov 09, 2018 138 139  TC (11 * Phi D F K) ∗ TR (card D))%I.  Jacques-Henri Jourdan committed Oct 29, 2018 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 ->  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 475 476 477 Proof. introv HM. iIntros "HM". rewrite -[in mapsto_M _](insert_id _ _ _ HM) -insert_delete /mapsto_M.  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 482 483 484 485 Qed. Lemma mapsto_M_acc_same : forall M x c, M !! x = Some c ->  Jacques-Henri Jourdan committed Nov 07, 2018 486 487  mapsto_M M -∗ ∃ v, ⌜val_of_content c = Some v⌝ ∗ x ↦ v ∗ (x ↦ v -∗ mapsto_M M).  Jacques-Henri Jourdan committed Oct 29, 2018 488 Proof.  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 513 Proof.  Jacques-Henri Jourdan committed Nov 07, 2018 514  introv Mxc Hcv. by rewrite /mapsto_M big_sepM_insert // Hcv.  Jacques-Henri Jourdan committed Oct 29, 2018 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"=>//.  Jacques-Henri Jourdan committed Nov 07, 2018 524  do 2 destruct val_of_content; try done.  Jacques-Henri Jourdan committed Oct 29, 2018 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,  Jacques-Henri Jourdan committed Nov 09, 2018 568  TCTR_invariant nmax ={⊤}=∗ UF \{} id V.  Jacques-Henri Jourdan committed Oct 29, 2018 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. }  Jacques-Henri Jourdan committed Nov 09, 2018 580  { rewrite card_empty. by iApply zero_TR. }  Jacques-Henri Jourdan committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 09, 2018 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 committed Oct 29, 2018 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".  Jacques-Henri Jourdan committed Nov 09, 2018 665  iCombine "TR1 TR2" as "HTR".  Jacques-Henri Jourdan committed Oct 29, 2018 666  rewrite -mapsto_M_union // -Nat.mul_add_distr_l (@Phi_join 1 _ D F K); eauto.  Jacques-Henri Jourdan committed Nov 09, 2018 667  rewrite -card_disjoint_union; eauto using is_rdsf_finite; [].  Jacques-Henri Jourdan committed Oct 29, 2018 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,  Jacques-Henri Jourdan committed Nov 09, 2018 722  TCTR_invariant nmax -∗  Jacques-Henri Jourdan committed Nov 07, 2018 723  {{{ UF D R V ∗ TC 26 }}}  Jacques-Henri Jourdan committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 07, 2018 732  iIntros "* #?" (Φ) "!# [HF TC] HΦ".  Jacques-Henri Jourdan committed Nov 09, 2018 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 committed Oct 29, 2018 737 738 739 740  iAssert ⌜M !! x = None⌝%I as %Mx. { case HMx: (M!!x)=>//. iDestruct (big_sepM_lookup with "HM") as "Hx'"=>//.  Jacques-Henri Jourdan committed Nov 07, 2018 741  destruct val_of_content; try done.  Jacques-Henri Jourdan committed Oct 29, 2018 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).  Jacques-Henri Jourdan committed Nov 09, 2018 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 committed Oct 29, 2018 755 756  repeat iSplit; try iPureIntro. { applys* Inv_make. } { applys* Mem_make. }  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 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' ->  Jacques-Henri Jourdan committed Nov 09, 2018 779  TCTR_invariant nmax -∗  Jacques-Henri Jourdan committed Nov 07, 2018 780  {{{ mapsto_M M ∗ TC (11*d+11) }}}  Jacques-Henri Jourdan committed Oct 29, 2018 781 782 783  «find #x» {{{ M', RET #(R x); mapsto_M M' ∗ ⌜ Mem D F' K V M' ⌝ }}}. Proof using.  Jacques-Henri Jourdan committed Nov 07, 2018 784  intros d. induction_wf IH: Wf_nat.lt_wf d.  Jacques-Henri Jourdan committed Oct 29, 2018 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:? =>//.  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 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".  Jacques-Henri Jourdan committed Nov 07, 2018 806  math_rewrite (11 * S d' + 6 = 11 * d' + 11 + 6)%nat.  Jacques-Henri Jourdan committed Oct 29, 2018 807  iDestruct "TC" as "[TCd TC]".  Jacques-Henri Jourdan committed Nov 07, 2018 808 809  wp_apply (IH' with "[//] [$HM $TCd]"). iIntros (M') "[HM' hM']". iDestruct "hM'" as %HM'. wp_tick_let.  Jacques-Henri Jourdan committed Oct 29, 2018 810  assert (HV := HM' _ Dx). destruct (M' !! x) as [c|] eqn:? =>//.  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 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 ->  Jacques-Henri Jourdan committed Nov 09, 2018 824  TCTR_invariant nmax -∗  Jacques-Henri Jourdan committed Nov 07, 2018 825  {{{ UF D R V ∗ TC (22 * alpha (card D) + 44) }}}  Jacques-Henri Jourdan committed Oct 29, 2018 826 827 828 829  «find #x» {{{ RET #(R x); UF D R V }}}. Proof using. introv Dx. iIntros "#?" (Φ) "!# [UF TC1] HΦ".  Jacques-Henri Jourdan committed Nov 09, 2018 830  iDestruct "UF" as (F K M HI HM) "(HM & TC2 & TR)".  Jacques-Henri Jourdan committed Oct 29, 2018 831 832  forwards* (d&F'&HC&HP): amortized_cost_of_iterated_path_compression_simplified x. iCombine "TC1 TC2" as "TC".  Jacques-Henri Jourdan committed Nov 07, 2018 833  rewrite [TC (_ + _)](TC_weaken _ (11*Phi D F' K + (11 * d + 11))%nat); [|math].  Jacques-Henri Jourdan committed Oct 29, 2018 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 ->  Jacques-Henri Jourdan committed Nov 09, 2018 849  TCTR_invariant nmax -∗  Jacques-Henri Jourdan committed Nov 07, 2018 850  {{{ UF D R V ∗ TC (22 * alpha (card D) + 57) }}}  Jacques-Henri Jourdan committed Oct 29, 2018 851 852 853 854  «get #x» {{{ RET V x; UF D R V }}}. Proof using. introv Dx. iIntros "#?" (Φ) "!# [UF TC] HΦ".  Jacques-Henri Jourdan committed Nov 07, 2018 855  math_rewrite (22 * alpha (card D) + 57 = 22 * alpha (card D) + 44 + 13)%nat.  Jacques-Henri Jourdan committed Oct 29, 2018 856  iDestruct "TC" as "[TC1 TC2]".  Jacques-Henri Jourdan committed Nov 07, 2018 857 858  wp_tick_rec. wp_apply (find_spec with "[//] [$TC1 $UF]")=>//.  Jacques-Henri Jourdan committed Oct 29, 2018 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).  Jacques-Henri Jourdan committed Nov 07, 2018 862  iDestruct (mapsto_M_acc_same with "HM") as (v Hv) "[Hx HM]"=>//. wp_tick_load.  Jacques-Henri Jourdan committed Oct 29, 2018 863  iDestruct ("HM" with "Hx") as "HM".  Jacques-Henri Jourdan committed Nov 07, 2018 864  destruct (val_of_content_Some_Root _ _ _ Hv) as (k1 & -> & _).  Jacques-Henri Jourdan committed Oct 29, 2018 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 ->  Jacques-Henri Jourdan committed Nov 09, 2018 881  TCTR_invariant nmax -∗  Jacques-Henri Jourdan committed Nov 07, 2018 882  {{{ UF D R V ∗ TC (22 * alpha (card D) + 62) }}}  Jacques-Henri Jourdan committed Oct 29, 2018 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Φ".  Jacques-Henri Jourdan committed Nov 07, 2018 887  math_rewrite (22 * alpha (card D) + 62 = 22 * alpha (card D) + 44 + 18)%nat.  Jacques-Henri Jourdan committed Oct 29, 2018 888  iDestruct "TC" as "[TC1 TC2]".  Jacques-Henri Jourdan committed Nov 07, 2018 889  wp_tick_rec. wp_tick_let. wp_apply (find_spec with "[//] [$TC1 $UF]")=>//.  Jacques-Henri Jourdan committed Oct 29, 2018 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).  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 897 898  iApply "HΦ". iExists _, _, _. iFrame. iSplit; [auto using Inv_update1|]. iSplit; [eauto using Mem_update1|].  Jacques-Henri Jourdan committed Nov 07, 2018 899 900  rewrite Rrx. iApply ("HM" with "[%] Hx"). simpl in *. by destruct (to_mach_int (K (R x))); inversion Hv'.  Jacques-Henri Jourdan committed Oct 29, 2018 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 ->  Jacques-Henri Jourdan committed Nov 09, 2018 913  TCTR_invariant nmax -∗  Jacques-Henri Jourdan committed Nov 07, 2018 914  {{{ UF D R V ∗ TC (44 * alpha (card D) + 92) }}}  Jacques-Henri Jourdan committed Oct 29, 2018 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Φ".  Jacques-Henri Jourdan committed Nov 07, 2018 919 920  math_rewrite (44 * alpha (card D) + 92 = (22 * alpha (card D) + 44) + (22 * alpha (card D) + 44) + 4)%nat.  Jacques-Henri Jourdan committed Oct 29, 2018 921  iDestruct "TC" as "[[TC1 TC2] TC3]".  Jacques-Henri Jourdan committed Nov 07, 2018 922  wp_tick_rec. wp_tick_let.  Jacques-Henri Jourdan committed Oct 29, 2018 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,  Jacques-Henri Jourdan committed Nov 07, 2018 943  (log2 (log2 nmax) < word_size - 1)%nat ->  Jacques-Henri Jourdan committed Oct 29, 2018 944 945 946 947  x \in D -> y \in D -> R x = x -> R y = y ->  Jacques-Henri Jourdan committed Nov 09, 2018 948  TCTR_invariant nmax -∗  Jacques-Henri Jourdan committed Nov 07, 2018 949  {{{ UF D R V ∗ TC 61 }}}  Jacques-Henri Jourdan committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 07, 2018 954  introv Hnmax Dx Dy Rx Ry. iIntros "#?" (Φ) "!# [UF TC] HΦ".  Jacques-Henri Jourdan committed Nov 07, 2018 955  wp_tick_rec. wp_tick_let.  Jacques-Henri Jourdan committed Nov 09, 2018 956  iDestruct "UF" as (F K M HI HM) "(HM & TC'TR)".  Jacques-Henri Jourdan committed Oct 29, 2018 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=>//.  Jacques-Henri Jourdan committed Nov 07, 2018 966  iDestruct (mapsto_M_acc_same _ x with "HM") as (v Hv) "[Hx HM]"=>//.  Jacques-Henri Jourdan committed Oct 29, 2018 967  wp_tick_load. iDestruct ("HM" with "Hx") as "HM".  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 972  wp_tick_load. iDestruct ("HM" with "Hy") as "HM".  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 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]. *)  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 09, 2018 988 989  iDestruct "TC'TR" as "[TC' TR]". iCombine "TC' TC" as "TC". iExists _, _, (<[x:=Link y]>M). iFrame "% TR".  Jacques-Henri Jourdan committed Oct 29, 2018 990 991 992  rewrite TC_weaken; [iFrame "TC"|lia]. iSplit; [by eauto using Mem_link|]. by iApply "HM". } (* Sub-case: [K x > K y]. *)  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 09, 2018 1003 1004  iDestruct "TC'TR" as "[TC' TR]". iCombine "TC' TC" as "TC". iExists _, _, (<[y:=Link x]>M). iFrame "% TR".  Jacques-Henri Jourdan committed Oct 29, 2018 1005 1006 1007  rewrite TC_weaken; [iFrame "TC"|lia]. iSplit; [by eauto using Mem_link|]. by iApply "HM". } (* Sub-case: [K x = K y]. *)  Jacques-Henri Jourdan committed Nov 07, 2018 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".  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Nov 15, 2018 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. }  Jacques-Henri Jourdan committed Nov 07, 2018 1022  assert (bool_decide (mach_int_bounded (k1 + 1))).  Jacques-Henri Jourdan committed Nov 09, 2018 1023  { assert (log2 nmax < 2 ^ (word_size - 1))%nat.  Jacques-Henri Jourdan committed Nov 07, 2018 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. }  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 1038  { rewrite lookup_insert_ne //. congruence. }  Jacques-Henri Jourdan committed Nov 07, 2018 1039  wp_tick_pair. wp_tick_inj. wp_tick_store. wp_tick_seq.  Jacques-Henri Jourdan committed Oct 29, 2018 1040  iApply "HΦ". iSplit; [|by auto].  Jacques-Henri Jourdan committed Nov 09, 2018 1041 1042  iDestruct "TC'TR" as "[TC' TR]". iExists _, _, _. iFrame "% TR".  Jacques-Henri Jourdan committed Nov 07, 2018 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 /=. }  Jacques-Henri Jourdan committed Nov 07, 2018 1048 1049  assert (k1 + 1 = K y + 1)%Z as -> by lia. by rewrite ->Nat2Z.inj_add. } Qed.  Jacques-Henri Jourdan committed Oct 29, 2018 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,  Jacques-Henri Jourdan committed Nov 07, 2018 1064  (log2 (log2 nmax) < word_size - 1)%nat ->  Jacques-Henri Jourdan committed Oct 29, 2018 1065 1066  x \in D -> y \in D ->  Jacques-Henri Jourdan committed Nov 09, 2018 1067  TCTR_invariant nmax -∗  Jacques-Henri Jourdan committed Nov 07, 2018 1068  {{{ UF D R V ∗ TC (44 * alpha (card D) + 152) }}}  Jacques-Henri Jourdan committed Oct 29, 2018 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.  Jacques-Henri Jourdan committed Nov 07, 2018 1073  introv Hnmax Dx Dy.  Jacques-Henri Jourdan committed Nov 07, 2018 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 committed Oct 29, 2018 1076  iIntros "#?" (Φ) "!# [UF [[[TC1 TC2] TC3] TC4]] HΦ".  Jacques-Henri Jourdan committed Nov 07, 2018 1077  wp_tick_rec. wp_tick_let.  Jacques-Henri Jourdan committed Oct 29, 2018 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 =>//.  Jacques-Henri Jourdan committed Nov 07, 2018 1083  wp_apply (link_spec _ _ _ _ _ Hnmax with "[//] [$TC3$UF]")=>//.  Jacques-Henri Jourdan committed Oct 29, 2018 1084 1085 1086 1087 1088  iIntros (z). by rewrite !update2_root. Qed. End UnionFind.  Jacques-Henri Jourdan committed Nov 07, 2018 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.`