Bitcoin Improvement Proposal (BIP) 32.

This is described at
this page in the

As stated in the 'Conventions' section of [BIP32],
the elliptic curve cryptography is based on the secp256k1 curve.
In our model, the types for private and public keys are
`secp256k1-priv-key-p` and `secp256k1-pub-key-p`.

The conversion functions described in the 'Conventions' section of [BIP32] are formalized as follows in our model of Bitcoin:

\mathsf{point} is`secp256k1-mul`with point`secp256k1-point-generator`; when the argument is a private key, we use`secp256k1-priv-to-pub`.\mathsf{ser}_{32} is`nat=>bebytes`with width 4.\mathsf{ser}_{256} is`nat=>bebytes`with width 32.\mathsf{ser}_\mathsf{P} is`secp256k1-point-to-bytes`with the compression flag set.\mathsf{parse}_{256} is`bebytes=>nat`.

The operations defined below should suffice to cover the use cases that BIP 32 should cater to:

- Given a seed,
`bip32-master-tree`is used to generate a singleton tree with the master private key at the root. - This master tree is extended as needed,
via
`bip32-extend-tree`. - For signing, private keys can be retrieved from the tree
via
`bip32-get-priv-key-at-path`. For calculating addresses, auditing, etc., public keys can be retrieved from the tree via`bip32-get-pub-key-at-path`. - For sharing (subtrees of) the master tree,
`bip32-export-key`is used to serialize a (private or public) key. Then`bip32-import-key`is used to construct a separate (sub)tree rooted at that key. - (Sub)trees shared as just explained can be then operated upon via
`bip32-extend-tree`for deriving more keys,`bip32-get-priv-key-at-path`for signing (unless the tree consists of public keys),`bip32-get-pub-key-at-path`for calculating addresses, auditing, etc., and`bip32-export-key`for further sharing.

- Bip32-wallet-structure
- Wallet structure.
- Bip32-key-trees
- Key trees.
- Bip32-key-serialization
- Key serialization.
- Bip32-key-derivation
- Key derivation functions.
- Bip32-executable-attachments
- Executable attachments for the BIP 32 formalization.
- Bip32-extended-keys
- Extended keys.
- Bip32-master-key-generation
- Master key generation.