Incomplete and in-progress proof of merge function for a unicit balanced Merkel Tree using join-semilattices

lattice_merkle_tree.thy

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