Skip to content

Instantly share code, notes, and snippets.

@iamwilhelm
Created January 22, 2024 02:29
Show Gist options
  • Save iamwilhelm/e984efe79b031b8eaac8673b0c1a0618 to your computer and use it in GitHub Desktop.
Save iamwilhelm/e984efe79b031b8eaac8673b0c1a0618 to your computer and use it in GitHub Desktop.
Incomplete and in-progress proof of merge function for a unicit balanced Merkel Tree using join-semilattices
theory lattice_merkle_tree
imports Main
begin
fun opt_last :: "'a list ⇒ 'a option" where
"opt_last [] = None" |
"opt_last xs = Some (last xs)"
(****** Lattice Merke Tree ******)
(* Define a key/value pair datatype *)
datatype ('k::linorder, 'v) key_value = KeyValue "'k::linorder" "'v" int
fun key_of :: "('k::linorder, 'v) key_value ⇒ 'k::linorder" where
"key_of (KeyValue k _ _) = k"
fun value_of :: "('k::linorder, 'v) key_value ⇒ 'v" where
"value_of (KeyValue _ v _) = v"
fun parity_of :: "('k::linorder, 'v) key_value ⇒ int" where
"parity_of (KeyValue _ _ p) = p"
(* Define a tree structure with Branch and Leaf *)
datatype ('k::linorder, 'v) tree =
Leaf "('k::linorder, 'v) key_value set" (* Leaf with a list of key-value pairs *)
| Branch "('k::linorder, 'v) tree list" (* Branch with a list of children *)
fun is_leaf :: "('k::linorder, 'v) tree ⇒ bool" where
"is_leaf (Leaf _) = True" |
"is_leaf (Branch _) = False"
fun is_branch :: "('k::linorder, 'v) tree ⇒ bool" where
"is_branch (Leaf _) = False" |
"is_branch (Branch _) = True"
fun min_key_of :: "('k::linorder, 'v) tree ⇒ 'k::linorder" where
"min_key_of (Leaf kv) = (
if {kv' ∈ kv. odd (parity_of kv')} = {}
then undefined
else Min (key_of ` {kv' ∈ kv. odd (parity_of kv')}))" |
"min_key_of (Branch []) = undefined" |
"min_key_of (Branch (child # _)) = min_key_of child"
definition min_of_leaf_kvs :: "('k::linorder, 'v) key_value set ⇒ ('k::linorder, 'v) key_value option" where
"min_of_leaf_kvs kv_set =
(let odd_kv_set = {kv. kv ∈ kv_set ∧ odd (parity_of kv)};
odd_keys = {key_of kv | kv. kv ∈ odd_kv_set}
in if odd_keys = {} then None
else Some (THE kv. kv ∈ odd_kv_set ∧ key_of kv = Min odd_keys))"
definition max_of_leaf_kvs :: "('k::linorder, 'v) key_value set ⇒ ('k::linorder, 'v) key_value option" where
"max_of_leaf_kvs kv_set =
(let odd_kv_set = {kv. kv ∈ kv_set ∧ odd (parity_of kv)};
odd_keys = {key_of kv | kv. kv ∈ odd_kv_set}
in if odd_keys = {} then None
else Some (THE kv. kv ∈ odd_kv_set ∧ key_of kv = Max odd_keys))"
definition add_to_leaf_kvs :: "('k::linorder, 'v) key_value set ⇒ ('k::linorder, 'v) key_value ⇒ ('k::linorder, 'v) key_value set" where
"add_to_leaf_kvs leaf kv =
(if (∃kv'. kv' ∈ leaf ∧ key_of kv' = key_of kv) then
(let kv' = THE kv'. kv' ∈ leaf ∧ key_of kv' = key_of kv in
if even (parity_of kv') then
leaf - {kv'} ∪ {KeyValue (key_of kv') (value_of kv) (parity_of kv' + 1)}
else
leaf - {kv'} ∪ {KeyValue (key_of kv') (value_of kv) (parity_of kv')})
else
leaf ∪ {KeyValue (key_of kv) (value_of kv) 1})"
(****** Tree Split Description ******)
(* get the height of a tree *)
fun height :: "('k::linorder, 'v) tree ⇒ nat" where
"height (Leaf _) = 0" |
"height (Branch []) = undefined" |
"height (Branch children) = Suc (Max (set (map height children)))"
thm height.induct
lemma height_of_parent_of_leaf_node:
assumes "children ≠ []"
shows "height (Branch children) > 0"
using assms gr0_conv_Suc height.elims by blast
lemma node_height_higher_than_children:
shows "∀child ∈ set children. height child < height (Branch children)"
proof
fix child
assume "child ∈ set children"
then have "height child ≤ Max (set (map height children))"
by simp
moreover have "height (Branch children) = Suc (Max (set (map height children)))"
by (metis ‹child ∈ set children› height.simps(3) list.set_cases)
ultimately show "height child < height (Branch children)"
by simp
qed
(* Count the children or key-value pairs in a single node *)
fun node_size :: "('k::linorder, 'v) tree ⇒ nat" where
"node_size (Leaf pairs) = card pairs" |
"node_size (Branch children) = length children"
(* Count number of children/key-value pairs at each layer *)
fun node_sizes_of_tree :: "('k::linorder, 'v) tree list ⇒ nat ⇒ nat list list" where
"node_sizes_of_tree [] _ = []" |
"node_sizes_of_tree trees 0 = [map node_size trees]" |
"node_sizes_of_tree trees (Suc depth) =
(map node_size trees) # node_sizes_of_tree (concat (map (λtree.
case tree of
Leaf _ ⇒ []
| Branch children ⇒ children) trees)) depth"
(*
fun my_all :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"my_all P [] = True" |
"my_all P (x # xs) = (P x ∧ my_all P xs)"
fun is_balanced :: "('a, 'b) tree ⇒ bool" where
"is_balanced (Leaf _) = True" |
"is_balanced (Branch []) = True" |
"is_balanced (Branch (t # ts)) =
(let h = height t in
my_all (λx. height x = h) ts ∧ is_balanced t ∧ my_all is_balanced ts)"
*)
(* This is a representation of how the tree is split at all layers *)
definition tree_splits :: "('k::linorder, 'v) tree ⇒ nat list list" where
"tree_splits t = node_sizes_of_tree [t] (height t)"
(* The target node size for the tree *)
definition "N ≡ 10"
(* Define the balance metric for a single layer *)
fun balance_metric_by_layer :: "nat list ⇒ nat" where
"balance_metric_by_layer [] = 0" |
"balance_metric_by_layer (x # xs) = (x - N) ^ 2 + balance_metric_by_layer xs"
(* Sum the metric across all layers of the tree *)
definition balance_metric :: "('k::linorder, 'v) tree ⇒ nat" where
"balance_metric t = sum_list (map (λlayer. balance_metric_by_layer layer) (tree_splits t))"
(********* Partial Order of Tree Splits **********)
(* Binary relation based on balance_metric *)
definition leq :: "('k::linorder, 'v) tree ⇒ ('k::linorder, 'v) tree ⇒ bool" where
"leq t1 t2 = (balance_metric t1 ≥ balance_metric t2)"
(* Lemma stating that leq is reflexive *)
lemma leq_reflexive: "leq t t"
unfolding leq_def
by simp
(* Lemma stating that leq is antisymmetric *)
lemma leq_antisymmetric: "leq t1 t2 ⟹ leq t2 t1 ⟹ balance_metric t1 = balance_metric t2"
unfolding leq_def
by auto
(* Lemma stating that leq is transitive *)
lemma leq_transitive: "leq t1 t2 ⟹ leq t2 t3 ⟹ leq t1 t3"
unfolding leq_def
by auto
(********* Query functions ********)
fun is_key_exists_in_leaf :: "('k::linorder, 'v) tree ⇒ 'k::linorder ⇒ bool" where
"is_key_exists_in_leaf (Leaf leaf) k = (∃kv. kv ∈ leaf ∧ key_of kv = k ∧ odd (parity_of kv))" |
"is_key_exists_in_leaf _ _ = False"
fun find_leaf :: "('k::linorder, 'v) tree ⇒ 'k::linorder ⇒ ('k::linorder, 'v) tree option" where
"find_leaf (Leaf leaf) k =
(if ∃kv. kv ∈ leaf ∧ key_of kv = k ∧ odd (parity_of kv) then Some (Leaf leaf) else None)" |
"find_leaf (Branch []) k = None" |
"find_leaf (Branch (t # ts)) k =
(if ts = [] ∨ k < min_key_of (hd ts)
then find_leaf t k
else find_leaf (Branch ts) k)"
(********* Balancing Operations ********)
type_synonym ('k, 'v) balance_op_fn =
"('k, 'v) tree list ⇒
('k, 'v) tree ⇒
('k, 'v) tree list ⇒
('k, 'v) tree"
definition lend_left_operation :: "('k::linorder, 'v) balance_op_fn"
where
"lend_left_operation prev tgt rest =
(case tgt of
Leaf tgt_kvs ⇒
(case opt_last prev of
Some (Leaf left_kvs) ⇒
(case min_of_leaf_kvs tgt_kvs of
Some min_kv ⇒
(let updated_left_kvs = add_to_leaf_kvs left_kvs min_kv;
updated_tgt_kvs = tgt_kvs - {min_kv}
in Branch (prev @ [Leaf updated_left_kvs, Leaf updated_tgt_kvs] @ rest))
| None ⇒ Branch (prev @ [tgt] @ rest))
| _ ⇒ Branch (prev @ [tgt] @ rest))
| _ ⇒ Branch (prev @ [tgt] @ rest))"
definition borrow_left_operation :: "('k::linorder, 'v) balance_op_fn" where
"borrow_left_operation prev tgt rest =
(case tgt of
Leaf tgt_kvs ⇒
(case opt_last prev of
Some (Leaf left_kvs) ⇒
(case max_of_leaf_kvs left_kvs of
Some max_kv ⇒
(let updated_left_kvs = left_kvs - {max_kv};
updated_tgt_kvs = add_to_leaf_kvs tgt_kvs max_kv
in Branch (prev @ [Leaf updated_left_kvs, Leaf updated_tgt_kvs] @ rest))
| None ⇒ Branch (prev @ [tgt] @ rest))
| _ ⇒ Branch (prev @ [tgt] @ rest))
| _ ⇒ Branch (prev @ [tgt] @ rest))"
definition lend_right_operation :: "('k::linorder, 'v) balance_op_fn" where
"lend_right_operation prev tgt rest =
(case tgt of
Leaf tgt_kvs ⇒
(case rest of
Leaf right_kvs # rest' ⇒
(case max_of_leaf_kvs tgt_kvs of
Some max_kv ⇒
(let updated_tgt_kvs = tgt_kvs - {max_kv};
updated_right_kvs = add_to_leaf_kvs right_kvs max_kv
in Branch (prev @ [Leaf updated_tgt_kvs, Leaf updated_right_kvs] @ rest'))
| None ⇒ Branch (prev @ [tgt] @ rest))
| _ ⇒ Branch (prev @ [tgt] @ rest))
| _ ⇒ Branch (prev @ [tgt] @ rest))"
definition borrow_right_operation :: "('k::linorder, 'v) balance_op_fn" where
"borrow_right_operation prev tgt rest =
(case tgt of
Leaf tgt_kvs ⇒
(case rest of
Leaf right_kvs # rest' ⇒
(case min_of_leaf_kvs right_kvs of
Some min_kv ⇒
(let updated_tgt_kvs = add_to_leaf_kvs tgt_kvs min_kv;
updated_right_kvs = right_kvs - {min_kv}
in Branch (prev @ [Leaf updated_tgt_kvs, Leaf updated_right_kvs] @ rest'))
| None ⇒ Branch (prev @ [tgt] @ rest))
| _ ⇒ Branch (prev @ [tgt] @ rest))
| _ ⇒ Branch (prev @ [tgt] @ rest))"
fun balance_with_op_helper ::
"('k::linorder, 'v) tree list ⇒
('k::linorder, 'v) tree ⇒
('k::linorder, 'v) balance_op_fn ⇒
'k::linorder ⇒
('k::linorder, 'v) tree option"
where
"balance_with_op_helper _ (Leaf _) _ _ = None" |
"balance_with_op_helper _ (Branch []) _ _ = None" |
"balance_with_op_helper prevs (Branch (tgt # nexts)) op k =
(if nexts = [] ∨ k < min_key_of (hd nexts) then
(if is_leaf tgt ∧ is_key_exists_in_leaf tgt k then
(case opt_last prevs of
Some left ⇒ Some (op prevs tgt nexts)
| None ⇒ None)
else
(case balance_with_op_helper [] tgt op k of
Some rebal_subtree ⇒ Some (Branch ((prevs @ [rebal_subtree]) @ nexts))
| None ⇒ None)
)
else
(case opt_last prevs of
None ⇒ balance_with_op_helper [tgt] (Branch nexts) op k
| Some left ⇒ balance_with_op_helper (prevs @ [tgt]) (Branch nexts) op k)
)"
definition balance_with_op ::
"('k::linorder, 'v) balance_op_fn ⇒
('k::linorder, 'v) tree ⇒
'k::linorder ⇒
('k::linorder, 'v) tree option"
where
"balance_with_op op tree k = balance_with_op_helper [] tree op k"
(* TODO implement fun split *)
(********* Insertion Operation *********)
fun insert_without_balancing :: "('k::linorder, 'v) tree ⇒ ('k::linorder, 'v) key_value ⇒ ('k::linorder, 'v) tree" where
"insert_without_balancing (Leaf leaf) kv = Leaf (add_to_leaf_kvs leaf kv)" |
"insert_without_balancing (Branch []) kv = Branch [Leaf {kv}]" |
"insert_without_balancing (Branch (t # ts)) kv =
(if key_of kv < min_key_of t then
Branch (insert_without_balancing t kv # ts)
else
Branch (t # [insert_without_balancing (Branch ts) kv]))"
definition insert_with_balancing :: "('k::linorder, 'v) tree ⇒ ('k::linorder, 'v) key_value ⇒ ('k::linorder, 'v) tree" where
"insert_with_balancing t kv =
(let
old_metric = balance_metric t;
new_tree = insert_without_balancing t kv;
new_metric = balance_metric new_tree
in
if should_balance old_metric new_metric then balance_tree new_tree else new_tree)"
(********* Algebraic Merge Function *********)
(* Merge function for leaf nodes using ordered set union *)
(*fun merge_leaves :: "('a key * 'b data_val) set ⇒ ('a key * 'b data_val) set ⇒ ('a key * 'b data_val) set" where
"merge_leaves xs ys = union xs ys"
*)
(* fun merge :: "('a, 'b) tree ⇒ ('a, 'b) tree ⇒ ('a, 'b) tree" where
"merge (Leaf xs) (Leaf ys) = Leaf (merge_leaves xs ys)" |
"merge (Branch xs) (Branch ys) = ..." (* Define how to merge two branches *) |
"merge (Leaf xs) (Branch ys) = ..." (* Define how to merge a leaf and a branch *) |
"merge (Branch xs) (Leaf ys) = merge (Leaf ys) (Branch xs)" (* Symmetric case *) *)
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment