		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-trees

Bip32-path

Paths in key trees.

As explained in [BIP32], the derivation of child keys from parent keys give rise to key trees. Each key in a tree is designated by a list of zero or more unsigned 32-bit bytes, each of which is a key index i as used in the child key derivation functions; the empty path designates the root of the tree.

This kind of path corresponds to the notation \mathsf{a/b/c} used in [BIP32]. However, we do not use any explicit \mathsf{H} subscripts to denote indices of hardened keys; we simply use indices whose most significant bit is set, e.g. 3_\mathsf{H} is index 2^{31}+3.

Below we lift the key derivation functions from single indices to paths. These key derivation functions on paths designate keys in a tree, starting with a root. All the derivations in the path must be valid (i.e. return no error) in order for a path to designate a valid key; otherwise, as stated in [BIP32], the corresponding key is skipped.

In our formalization of BIP 32, we use the library type ubyte32-list for paths.