Commit fca38e9f authored by Gerwin Klein's avatar Gerwin Klein
Browse files

new entry BTree

parent a175903c09b5
......@@ -10283,3 +10283,29 @@ abstract =
used for the proof of the strong law is a particularly quick and slick
one based on ergodic theory, which was formalised by Gouëzel in
another AFP entry.</p>
[BTree]
title = A Verified Imperative Implementation of B-Trees
author = Niels Mündler <mailto:n.muendler@tum.de>
topic = Computer science/Data structures
date = 2021-02-24
notify = n.muendler@tum.de
abstract =
In this work, we use the interactive theorem prover Isabelle/HOL to
verify an imperative implementation of the classical B-tree data
structure invented by Bauer and McCreight [ACM 1970]. The
implementation supports set membership and insertion queries with
efficient binary search for intra-node navigation. This is
accomplished by first specifying the structure abstractly in the
functional modeling language HOL and proving functional correctness.
Using manual refinement, we derive an imperative implementation in
Imperative/HOL. We show the validity of this refinement using the
separation logic utilities from the <a
href="https://www.isa-afp.org/entries/Refine_Imperative_HOL.html">
Isabelle Refinement Framework </a> . The code can be exported to
the programming languages SML and Scala. We examine the runtime of all
operations indirectly by reproducing results of the logarithmic
relationship between height and the number of nodes. The results are
discussed in greater detail in the corresponding <a
href="https://mediatum.ub.tum.de/1596550">Bachelor's
Thesis</a>.
theory Array_SBlit
imports "Separation_Logic_Imperative_HOL.Array_Blit"
begin
section "Same array Blit"
text "The standard framework already provides a function to copy array
elements."
term blit
thm blit_rule
thm blit.simps
(* Same array BLIT *)
definition "sblit a s d l \<equiv> blit a s a d l"
text "When copying values within arrays,
blit only works for moving elements to the left."
lemma sblit_rule[sep_heap_rules]:
assumes LEN:
"si+len \<le> length lsrc"
and DST_SM: "di \<le> si"
shows
"< src \<mapsto>\<^sub>a lsrc >
sblit src si di len
<\<lambda>_. src \<mapsto>\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding sblit_def
using LEN DST_SM
proof (induction len arbitrary: lsrc si di)
case 0 thus ?case by sep_auto
next
case (Suc len)
note [sep_heap_rules] = Suc.IH
have [simp]: "\<And>x. lsrc ! si # take len (drop (Suc si) lsrc) @ x
= take (Suc len) (drop si lsrc) @ x"
apply simp
by (metis Suc.prems(1) add_Suc_right Cons_nth_drop_Suc
less_Suc_eq_le add.commute not_less_eq take_Suc_Cons
Nat.trans_le_add2)
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
subsection "A reverse blit"
text "The function rblit may be used to copy elements a defined offset to the right"
(* Right BLIT or Reverse BLIT *)
primrec rblit :: "_ array \<Rightarrow> nat \<Rightarrow> _ array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
"rblit _ _ _ _ 0 = return ()"
| "rblit src si dst di (Suc l) = do {
x \<leftarrow> Array.nth src (si+l);
Array.upd (di+l) x dst;
rblit src si dst di l
}"
text "For separated arrays it is equivalent to normal blit.
The proof follows similarly to the corresponding proof for blit."
lemma rblit_rule[sep_heap_rules]:
assumes LEN: "si+len \<le> length lsrc" "di+len \<le> length ldst"
shows
"< src \<mapsto>\<^sub>a lsrc
* dst \<mapsto>\<^sub>a ldst >
rblit src si dst di len
<\<lambda>_. src \<mapsto>\<^sub>a lsrc
* dst \<mapsto>\<^sub>a (take di ldst @ take len (drop si lsrc) @ drop (di+len) ldst)
>"
using LEN
proof (induction len arbitrary: ldst)
case 0 thus ?case by sep_auto
next
case (Suc len)
note [sep_heap_rules] = Suc.IH
have [simp]: "drop (di + len) (ldst[di + len := lsrc ! (si + len)])
= lsrc ! (si + len) # drop (Suc (di + len)) ldst"
by (metis Cons_nth_drop_Suc Suc.prems(2) Suc_le_eq add_Suc_right drop_upd_irrelevant length_list_update lessI nth_list_update_eq)
have "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
proof -
have "len < length (drop si lsrc)"
using Suc.prems(1) by force
then show "take len (drop si lsrc) @ [lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
by (metis (no_types) Suc.prems(1) add_leD1 nth_drop take_Suc_conv_app_nth)
qed
then have [simp]: "\<And>x. take len (drop si lsrc) @
lsrc ! (si + len) # x = take (Suc len) (drop si lsrc) @ x"
by simp
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
definition "srblit a s d l \<equiv> rblit a s a d l"
text "However, within arrays we can now copy to the right."
lemma srblit_rule[sep_heap_rules]:
assumes LEN:
"di+len \<le> length lsrc"
and DST_GR: "di \<ge> si"
shows
"< src \<mapsto>\<^sub>a lsrc >
srblit src si di len
<\<lambda>_. src \<mapsto>\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding srblit_def
using LEN DST_GR
proof (induction len arbitrary: lsrc si di)
case 0 thus ?case by sep_auto
next
case (Suc len)
note [sep_heap_rules] = Suc.IH
have[simp]: "take len (drop si (lsrc[di + len := lsrc ! (si + len)]))
= take len (drop si lsrc)"
sledgehammer
by (metis Suc.prems(2) ab_semigroup_add_class.add.commute add_le_cancel_right take_drop take_update_cancel)
have [simp]: "drop (di + len) (lsrc[di + len := lsrc ! (si + len)])
= lsrc ! (si+len) # drop (Suc di + len) lsrc"
by (metis Suc.prems(1) add_Suc_right add_Suc_shift add_less_cancel_left append_take_drop_id le_imp_less_Suc le_refl plus_1_eq_Suc same_append_eq take_update_cancel upd_conv_take_nth_drop)
have "take len (drop si lsrc) @
[lsrc ! (si + len)] = take (Suc len) (drop si lsrc)"
proof -
have "len < length lsrc - si"
using Suc.prems(1) Suc.prems(2) by linarith
then show ?thesis
by (metis (no_types) Suc.prems(1) Suc.prems(2) add_leD1 le_add_diff_inverse length_drop nth_drop take_Suc_conv_app_nth)
qed
then have [simp]: "\<And>x. take len (drop si lsrc) @
lsrc ! (si + len) # x = take (Suc len) (drop si lsrc) @ x"
by simp
from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed
subsection "Modeling target language blit"
text "For convenience, a function that is oblivious to the direction of the shift
is defined."
definition "safe_sblit a s d l \<equiv>
if s > d then
sblit a s d l
else
srblit a s d l
"
text "We obtain a heap rule similar to the one of blit,
but for copying within one array."
lemma safe_sblit_rule[sep_heap_rules]:
assumes LEN:
"len > 0 \<longrightarrow> di+len \<le> length lsrc \<and> si+len \<le> length lsrc"
shows
"< src \<mapsto>\<^sub>a lsrc >
safe_sblit src si di len
<\<lambda>_. src \<mapsto>\<^sub>a (take di lsrc @ take len (drop si lsrc) @ drop (di+len) lsrc)
>"
unfolding safe_sblit_def
using LEN
apply(cases len)
apply(sep_auto simp add: sblit_def srblit_def)[]
apply sep_auto
done
(* Compare this to blit_rule *)
thm blit_rule
thm safe_sblit_rule
subsection "Code Generator Setup"
text "Note that the requirement for correctness
is even weaker here than in SML.
We therefore manually handle the case where length is 0 (in which case nothing happens at all)."
code_printing code_module "array_sblit" \<rightharpoonup> (SML)
\<open>
fun array_sblit src si di len = (
if len > 0 then
ArraySlice.copy {
di = IntInf.toInt di,
src = ArraySlice.slice (src,IntInf.toInt si,SOME (IntInf.toInt len)),
dst = src}
else ()
)
\<close>
definition safe_sblit' where
[code del]: "safe_sblit' src si di len
= safe_sblit src (nat_of_integer si) (nat_of_integer di)
(nat_of_integer len)"
lemma [code]:
"safe_sblit src si di len
= safe_sblit' src (integer_of_nat si) (integer_of_nat di)
(integer_of_nat len)" by (simp add: safe_sblit'_def)
(* TODO: Export to other languages: OCaml, Haskell *)
code_printing constant safe_sblit' \<rightharpoonup>
(SML) "(fn/ ()/ => /array'_sblit _ _ _ _)"
and (Scala) "{ ('_: Unit)/=>/
def safescopy(src: Array['_], srci: Int, dsti: Int, len: Int) = {
if (len > 0)
System.arraycopy(src, srci, src, dsti, len)
else
()
}
safescopy(_.array,_.toInt,_.toInt,_.toInt)
}"
export_code safe_sblit checking SML Scala
subsection "Derived operations"
definition array_shr where
"array_shr a i k \<equiv> do {
l \<leftarrow> Array.len a;
safe_sblit a i (i+k) (l-(i+k))
}"
find_theorems "Array.len"
lemma array_shr_rule[sep_heap_rules]:
"< src \<mapsto>\<^sub>a lsrc >
array_shr src i k
<\<lambda>_. src \<mapsto>\<^sub>a (take (i+k) lsrc @ take (length lsrc - (i+k)) (drop i lsrc))
>"
unfolding array_shr_def
by sep_auto
lemma array_shr_rule_alt:
"< src \<mapsto>\<^sub>a lsrc >
array_shr src i k
<\<lambda>_. src \<mapsto>\<^sub>a (take (length lsrc) (take (i+k) lsrc @ (drop i lsrc)))
>"
by (sep_auto simp add: min_def)
definition array_shl where
"array_shl a i k \<equiv> do {
l \<leftarrow> Array.len a;
safe_sblit a i (i-k) (l-i)
}
"
lemma array_shl_rule[sep_heap_rules]:
"
< src \<mapsto>\<^sub>a lsrc >
array_shl src i k
<\<lambda>_. src \<mapsto>\<^sub>a (take (i-k) lsrc @ (drop i lsrc) @ drop (i - k + (length lsrc - i)) lsrc)
>"
unfolding array_shl_def
by sep_auto
lemma array_shl_rule_alt:
"
\<lbrakk>i \<le> length lsrc; k \<le> i\<rbrakk> \<Longrightarrow>
< src \<mapsto>\<^sub>a lsrc >
array_shl src i k
<\<lambda>_. src \<mapsto>\<^sub>a (take (i-k) lsrc @ (drop i lsrc) @ drop (length lsrc - k) lsrc)
>"
by sep_auto
end
\ No newline at end of file
theory BTree
imports Main "HOL-Data_Structures.Sorted_Less" "HOL-Data_Structures.Cmp"
begin
(* some setup to cover up the redefinition of sorted in Sorted_Less
but keep the lemmas *)
hide_const (open) Sorted_Less.sorted
abbreviation "sorted_less \<equiv> Sorted_Less.sorted"
section "Definition of the B-Tree"
subsection "Datatype definition"
text "B-trees can be considered to have all data stored interleaved
as child nodes and separating elements (also keys or indices).
We define them to either be a Node that holds a list of pairs of children
and indices or be a completely empty Leaf."
datatype 'a btree = Leaf | Node "('a btree * 'a) list" "'a btree"
type_synonym 'a btree_list = "('a btree * 'a) list"
type_synonym 'a btree_pair = "('a btree * 'a)"
abbreviation subtrees where "subtrees xs \<equiv> (map fst xs)"
abbreviation separators where "separators xs \<equiv> (map snd xs)"
subsection "Inorder and Set"
text "The set of B-tree elements is defined automatically."
thm btree.set
value "set_btree (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"
text "The inorder view is defined with the help of the concat function."
fun inorder :: "'a btree \<Rightarrow> 'a list" where
"inorder Leaf = []" |
"inorder (Node ts t) = concat (map (\<lambda> (sub, sep). inorder sub @ [sep]) ts) @ inorder t"
abbreviation "inorder_pair \<equiv> \<lambda>(sub,sep). inorder sub @ [sep]"
abbreviation "inorder_list ts \<equiv> concat (map inorder_pair ts)"
(* this abbreviation makes handling the list much nicer *)
thm inorder.simps
value "inorder (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"
subsection "Height and Balancedness"
class height =
fixes height :: "'a \<Rightarrow> nat"
instantiation btree :: (type) height
begin
fun height_btree :: "'a btree \<Rightarrow> nat" where
"height Leaf = 0" |
"height (Node ts t) = Suc (Max (height ` (set (subtrees ts@[t]))))"
instance ..
end
text "Balancedness is defined is close accordance to the definition by Ernst"
fun bal:: "'a btree \<Rightarrow> bool" where
"bal Leaf = True" |
"bal (Node ts t) = (
(\<forall>sub \<in> set (subtrees ts). height sub = height t) \<and>
(\<forall>sub \<in> set (subtrees ts). bal sub) \<and> bal t
)"
value "height (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"
subsection "Order"
text "The order of a B-tree is defined just as in the original paper by Bayer."
(* alt1: following knuths definition to allow for any
natural number as order and resolve ambiguity *)
(* alt2: use range [k,2*k] allowing for valid btrees
from k=1 onwards NOTE this is what I ended up implementing *)
fun order:: "nat \<Rightarrow> 'a btree \<Rightarrow> bool" where
"order k Leaf = True" |
"order k (Node ts t) = (
(length ts \<ge> k) \<and>
(length ts \<le> 2*k) \<and>
(\<forall>sub \<in> set (subtrees ts). order k sub) \<and> order k t
)"
text \<open>The special condition for the root is called \textit{root\_order}\<close>
(* the invariant for the root of the btree *)
fun root_order:: "nat \<Rightarrow> 'a btree \<Rightarrow> bool" where
"root_order k Leaf = True" |
"root_order k (Node ts t) = (
(length ts > 0) \<and>
(length ts \<le> 2*k) \<and>
(\<forall>s \<in> set (subtrees ts). order k s) \<and> order k t
)"
subsection "Auxiliary Lemmas"
(* auxiliary lemmas when handling sets *)
lemma separators_split:
"set (separators (l@(a,b)#r)) = set (separators l) \<union> set (separators r) \<union> {b}"
by simp
lemma subtrees_split:
"set (subtrees (l@(a,b)#r)) = set (subtrees l) \<union> set (subtrees r) \<union> {a}"
by simp
(* height and set lemmas *)
lemma finite_set_ins_swap:
assumes "finite A"
shows "max a (Max (Set.insert b A)) = max b (Max (Set.insert a A))"
using Max_insert assms max.commute max.left_commute by fastforce
lemma finite_set_in_idem:
assumes "finite A"
shows "max a (Max (Set.insert a A)) = Max (Set.insert a A)"
using Max_insert assms max.commute max.left_commute by fastforce
lemma height_Leaf: "height t = 0 \<longleftrightarrow> t = Leaf"
by (induction t) (auto)
lemma height_btree_order:
"height (Node (ls@[a]) t) = height (Node (a#ls) t)"
by simp
lemma height_btree_sub:
"height (Node ((sub,x)#ls) t) = max (height (Node ls t)) (Suc (height sub))"
by simp
lemma height_btree_last:
"height (Node ((sub,x)#ts) t) = max (height (Node ts sub)) (Suc (height t))"
by (induction ts) auto
lemma set_btree_inorder: "set (inorder t) = set_btree t"
apply(induction t)
apply(auto)
done
lemma child_subset: "p \<in> set t \<Longrightarrow> set_btree (fst p) \<subseteq> set_btree (Node t n)"
apply(induction p arbitrary: t n)
apply(auto)
done
lemma some_child_sub:
assumes "(sub,sep) \<in> set t"
shows "sub \<in> set (subtrees t)"
and "sep \<in> set (separators t)"
using assms by force+
(* balancedness lemmas *)
lemma bal_all_subtrees_equal: "bal (Node ts t) \<Longrightarrow> (\<forall>s1 \<in> set (subtrees ts). \<forall>s2 \<in> set (subtrees ts). height s1 = height s2)"
by (metis BTree.bal.simps(2))
lemma fold_max_set: "\<forall>x \<in> set t. x = f \<Longrightarrow> fold max t f = f"
apply(induction t)
apply(auto simp add: max_def_raw)
done
lemma height_bal_tree: "bal (Node ts t) \<Longrightarrow> height (Node ts t) = Suc (height t)"
by (induction ts) auto
lemma bal_split_last:
assumes "bal (Node (ls@(sub,sep)#rs) t)"
shows "bal (Node (ls@rs) t)"
and "height (Node (ls@(sub,sep)#rs) t) = height (Node (ls@rs) t)"
using assms by auto
lemma bal_split_right:
assumes "bal (Node (ls@rs) t)"
shows "bal (Node rs t)"
and "height (Node rs t) = height (Node (ls@rs) t)"
using assms by (auto simp add: image_constant_conv)
lemma bal_split_left:
assumes "bal (Node (ls@(a,b)#rs) t)"
shows "bal (Node ls a)"
and "height (Node ls a) = height (Node (ls@(a,b)#rs) t)"
using assms by (auto simp add: image_constant_conv)
lemma bal_substitute: "\<lbrakk>bal (Node (ls@(a,b)#rs) t); height t = height c; bal c\<rbrakk> \<Longrightarrow> bal (Node (ls@(c,b)#rs) t)"
unfolding bal.simps
by auto
lemma bal_substitute_subtree: "\<lbrakk>bal (Node (ls@(a,b)#rs) t); height a = height c; bal c\<rbrakk> \<Longrightarrow> bal (Node (ls@(c,b)#rs) t)"
using bal_substitute
by auto
lemma bal_substitute_separator: "bal (Node (ls@(a,b)#rs) t) \<Longrightarrow> bal (Node (ls@(a,c)#rs) t)"
unfolding bal.simps
by auto
(* order lemmas *)
lemma order_impl_root_order: "\<lbrakk>k > 0; order k t\<rbrakk> \<Longrightarrow> root_order k t"
apply(cases t)
apply(auto)
done
(* sorted inorder implies that some sublists are sorted. This can be followed directly *)
lemma sorted_inorder_list_separators: "sorted_less (inorder_list ts) \<Longrightarrow> sorted_less (separators ts)"
apply(induction ts)
apply (auto simp add: sorted_lems)
done
corollary sorted_inorder_separators: "sorted_less (inorder (Node ts t)) \<Longrightarrow> sorted_less (separators ts)"
using sorted_inorder_list_separators sorted_wrt_append
by auto
lemma sorted_inorder_list_subtrees:
"sorted_less (inorder_list ts) \<Longrightarrow> \<forall> sub \<in> set (subtrees ts). sorted_less (inorder sub)"
apply(induction ts)
apply (auto simp add: sorted_lems)+
done
corollary sorted_inorder_subtrees: "sorted_less (inorder (Node ts t)) \<Longrightarrow> \<forall> sub \<in> set (subtrees ts). sorted_less (inorder sub)"
using sorted_inorder_list_subtrees sorted_wrt_append by auto
lemma sorted_inorder_list_induct_subtree:
"sorted_less (inorder_list (ls@(sub,sep)#rs)) \<Longrightarrow> sorted_less (inorder sub)"
by (simp add: sorted_wrt_append)
corollary sorted_inorder_induct_subtree:
"sorted_less (inorder (Node (ls@(sub,sep)#rs) t)) \<Longrightarrow> sorted_less (inorder sub)"
by (simp add: sorted_wrt_append)
lemma sorted_inorder_induct_last: "sorted_less (inorder (Node ts t)) \<Longrightarrow> sorted_less (inorder t)"
by (simp add: sorted_wrt_append)
end
\ No newline at end of file
theory BTree_Height
imports BTree
begin
section "Maximum and minimum height"
text "Textbooks usually provide some proofs relating the maxmimum and minimum height of the BTree
for a given number of nodes. We therefore introduce this counting and show the respective proofs."
subsection "Definition of node/size"
thm BTree.btree.size
(* the automatically derived size is a bit weird for our purposes *)
value "size (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"
text "The default size function does not suit our needs as it regards the length of the list in each node.
We would like to count the number of nodes in the tree only, not regarding the number of keys."
(* we want a different counting method,
namely only the number of nodes in a tree *)
(* TODO what if we count Leafs as nodes? *)
fun nodes::"'a btree \<Rightarrow> nat" where
"nodes Leaf = 0" |
"nodes (Node ts t) = 1 + (\<Sum>t\<leftarrow>subtrees ts. nodes t) + (nodes t)"
value "nodes (Node [(Leaf, (0::nat)), (Node [(Leaf, 1), (Leaf, 10)] Leaf, 12), (Leaf, 30), (Leaf, 100)] Leaf)"
(* maximum number of nodes for given height *)
subsection "Maximum number of nodes for a given height"
lemma sum_list_replicate: "sum_list (replicate n c) = n*c"
apply(induction n)
apply(auto simp add: ring_class.ring_distribs(2))
done
abbreviation "bound k h \<equiv> ((k+1)^h - 1)"
lemma nodes_height_upper_bound:
"\<lbrakk>order k t; bal t\<rbrakk> \<Longrightarrow> nodes t * (2*k) \<le> bound (2*k) (height t)"
proof(induction t rule: nodes.induct)
case (2 ts t)
let ?sub_height = "((2 * k + 1) ^ height t - 1)"
have "sum_list (map nodes (subtrees ts)) * (2*k) =
sum_list (map (\<lambda>t. nodes t * (2 * k)) (subtrees ts))"
using sum_list_mult_const by metis
also have "\<dots> \<le> sum_list (map (\<lambda>x.?sub_height) (subtrees ts))"
using 2
using sum_list_mono[of "subtrees ts" "\<lambda>t. nodes t * (2 * k)" "\<lambda>x. bound (2 * k) (height t)"]
by (metis bal.simps(2) order.simps(2))
also have "\<dots> = sum_list (replicate (length ts) ?sub_height)"
using map_replicate_const[of ?sub_height "subtrees ts"] length_map
by simp
also have "\<dots> = (length ts)*(?sub_height)"
using sum_list_replicate by simp
also have "\<dots> \<le> (2*k)*(?sub_height)"
using "2.prems"(1)
by simp
finally have "sum_list (map nodes (subtrees ts))*(2*k) \<le> ?sub_height*(2*k)"
by simp
moreover have "(nodes t)*(2*k) \<le> ?sub_height"
using 2 by simp
ultimately have "(nodes (Node ts t))*(2*k) \<le>
2*k
+ ?sub_height * (2*k)
+ ?sub_height"
unfolding nodes.simps add_mult_distrib
by linarith
also have "\<dots> = 2*k + (2*k)*((2 * k + 1) ^ height t) - 2*k + (2 * k + 1) ^ height t - 1"
by (simp add: diff_mult_distrib2 mult.assoc mult.commute)
also have "\<dots> = (2*k)*((2 * k + 1) ^ height t) + (2 * k + 1) ^ height t - 1"
by simp
also have "\<dots> = (2*k+1)^(Suc(height t)) - 1"
by simp
finally show ?case
by (metis "2.prems"(2) height_bal_tree)
qed simp
text "To verify our lower bound is sharp, we compare it to the height of artificially constructed
full trees."
fun full_node::"nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a btree" where
"full_node k c 0 = Leaf"|
"full_node k c (Suc n) = (Node (replicate (2*k) ((full_node k c n),c)) (full_node k c n))"
value "let k = (2::nat) in map (\<lambda>x. nodes x * 2*k) (map (full_node k (1::nat)) [0,1,2,3,4])"