Commit 1fe68c70 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Add code for union find.

parent 597a25e0
......@@ -3,6 +3,7 @@
theories/Auth_mnat.v
theories/Auth_nat.v
theories/MachineIntegers.v
theories/ClockIntegers.v
theories/Examples.v
theories/Misc.v
......@@ -48,3 +49,4 @@ theories/union_find/math/UnionFind41Potential.v
theories/union_find/math/UnionFind42PotentialCompress.v
theories/union_find/math/UnionFind43PotentialAnalysis.v
theories/union_find/math/UnionFind44PotentialJoin.v
theories/union_find/Code.v
From iris.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeReceipts.
From iris_time Require Import TimeReceipts MachineIntegers.
From stdpp Require Import numbers.
Open Scope Z_scope.
Definition w : nat := 64.
Definition max_int : Z := 1 (w-1).
Definition min_int : Z := - max_int.
Definition max_uint : Z := 2 * max_int.
(*
* Bare machine integers can overflow.
*)
Section machine_int.
Context `{heapG Σ}.
Definition is_machine_int (n : Z) : iProp Σ :=
min_int n < max_int%I.
Definition machine_int_add : val :=
λ: "x" "y",
("x" + "y" + #max_int) `rem` #max_uint - #max_int.
(* Machine addition does not overflow when some inequality is met: *)
Lemma machine_int_add_spec n1 n2 :
{{{ is_machine_int n1 is_machine_int n2 min_int n1+n2 < max_int }}}
machine_int_add #n1 #n2
{{{ RET #(n1+n2) ; is_machine_int (n1+n2) }}}.
Proof.
iIntros (Φ) "(_ & _ & %) Post". repeat (wp_pure _).
(* boring arithmetic proof: *)
assert ((n1 + n2 + max_int) `rem` max_uint - max_int = n1 + n2) as ->. {
assert ((n1 + n2 + max_int) `rem` max_uint = n1 + n2 + max_int). {
apply Z.rem_small. unfold min_int, max_uint in *. lia.
}
lia.
}
by iApply "Post".
Qed.
End machine_int.
(*
* A clock integer (onetime integer in Clochards thesis) is a non-duplicable
* integer which supports addition.
......
From iris.heap_lang Require Import proofmode notation.
Open Scope Z_scope.
Definition w : nat := 64.
Definition max_int : Z := 1 (w-1).
Definition min_int : Z := - max_int.
Definition max_uint : Z := 2 * max_int.
(*
* Bare machine integers can overflow.
*)
Section machine_int.
Context `{heapG Σ}.
Definition is_machine_int (n : Z) : iProp Σ :=
min_int n < max_int%I.
Definition machine_int_add : val :=
λ: "x" "y",
("x" + "y" + #max_int) `rem` #max_uint - #max_int.
(* Machine addition does not overflow when some inequality is met: *)
Lemma machine_int_add_spec n1 n2 :
{{{ is_machine_int n1 is_machine_int n2 min_int n1+n2 < max_int }}}
machine_int_add #n1 #n2
{{{ RET #(n1+n2) ; is_machine_int (n1+n2) }}}.
Proof.
iIntros (Φ) "(_ & _ & %) Post". repeat (wp_pure _).
(* boring arithmetic proof: *)
assert ((n1 + n2 + max_int) `rem` max_uint - max_int = n1 + n2) as ->. {
assert ((n1 + n2 + max_int) `rem` max_uint = n1 + n2 + max_int). {
apply Z.rem_small. unfold min_int, max_uint in *. lia.
}
lia.
}
by iApply "Post".
Qed.
End machine_int.
From iris.heap_lang Require Import notation lib.assert.
From iris_time Require Import MachineIntegers.
Notation ROOT x := (InjL x).
Notation ROOTV x := (InjLV x).
Notation LINK x := (InjR x).
Notation LINKV x := (InjRV x).
Notation "'match:' e0 'with' 'ROOT' ( r , v ) => e1 | 'LINK' x => e2 'end'" :=
(Match e0
"__x" (let: r%bind := Fst "__x" in let: v%bind := Snd "__x" in e1)
x%bind e2)
(e0, r, v, e1, x, e2 at level 200, only parsing) : expr_scope.
Definition make : val := λ: "v",
ref (ROOT (#0, "v")).
Definition find : val := rec: "find" "x" :=
match: !"x" with
ROOT (<>, <>) => "x"
| LINK "y" =>
let: "z" := "find" "y" in
"x" <- LINK "z";;
"z"
end.
Definition eq : val := λ: "x" "y",
find "x" = find "y".
Definition get : val := λ: "x",
let: "x" := find "x" in
match: !"x" with
ROOT (<>, "v") => "v"
| LINK <> => assert: #false
end.
Definition set : val := λ: "x" "v",
let: "x" := find "x" in
match: !"x" with
ROOT ("r", <>) => "x" <- ROOT ("r", "v")
| LINK <> => assert: #false
end.
Definition link : val := λ: "x" "y",
if: "x" = "y" then "x"
else
match: !"x" with
ROOT ("rx", "vx") =>
match: !"y" with
ROOT ("ry", <>) =>
if: "rx" < "ry" then
"x" <- LINK "y";;
"y"
else if: "ry" < "rx" then
"y" <- LINK "x";;
"x"
else
"y" <- LINK "x";;
"x" <- ROOT ("rx"+#1, "vx");;
"x"
| LINK <> =>
assert: #false
end
| LINK <> =>
assert: #false
end.
Definition union : val := λ: "x" "y",
link (find "x") (find "y").
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment