|
|
|---|
|
|
|
|---|
Key trees.
This is a product type introduced by fty::defprod.
The following invariant is enforced on the fields:
(and (bip32-valid-keys-p root-key index-tree)
(bip32-valid-depths-p root-depth index-tree)
(implies (equal root-depth 0)
(equal root-index 0))
(equal (len root-parent) 4)
(implies (equal root-depth 0)
(equal root-parent (list 0 0 0 0))))
In a key tree, each node is labeled by a key derived from the root key. Thus, at the specification level, it suffices to have the root key and the underlying index tree, since all the non-root keys can be derived. We require each non-root key to be valid, as defined by bip32-valid-keys-p.
In addition to a root key and an index tree, our formalization of root keys includes a few other components. These are needed in order for the keys in the tree to be serializable in the manner specified in [BIP32].
One of these components is the depth of the root key with respect to the (super)tree rooted at the master key. This is 0 if this tree is rooted at the master key. We require each key in this (sub)tree to have a depth below 256, taking into account the depth of the root. We pass the root depth to bip32-valid-depths-p to check this condition.
Another component is the index of the root of this tree within the (super)tree rooted at the master key. This must be 0 if this tree's root is master key. Otherwise, the root of this subtree is some child within the supertree, and this component is the index of that child. Without this component, we would be unable to serialize the root of this subtree. Note that the non-root nodes in the tree have known indices.
Yet another component is the fingerprint (consisting of 4 bytes [BIP32]) of the parent of the key at the root of this tree. This must consist of four zeros if this root key is the master key. Without this component, we would be unable to serialize the root of this subtree. Note that the non-root nodes in the tree have parent fingerprints that can be calculated from their parent key.