		Search-engine friendly clone of the ACL2 documentation.

Bip32-ext-pub-key

Make-bip32-ext-pub-key

Basic constructor macro for bip32-ext-pub-key structures.

Syntax

(make-bip32-ext-pub-key [:key <key>] 
                        [:chain-code <chain-code>])

This is the usual way to construct bip32-ext-pub-key structures. It simply conses together a structure with the specified fields.

This macro generates a new bip32-ext-pub-key structure from scratch. See also change-bip32-ext-pub-key, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-bip32-ext-pub-key

(defmacro make-bip32-ext-pub-key (&rest args)
  (std::make-aggregate 'bip32-ext-pub-key
                       args '((:key) (:chain-code))
                       'make-bip32-ext-pub-key
                       nil))

Function: bip32-ext-pub-key

(defun bip32-ext-pub-key (key chain-code)
  (declare (xargs :guard (and (secp256k1-pub-key-p key)
                              (bip32-chain-code-p chain-code))))
  (declare (xargs :guard t))
  (let ((__function__ 'bip32-ext-pub-key))
    (declare (ignorable __function__))
    (b* ((key (mbe :logic (ecurve::secp256k1-pub-key-fix key)
                   :exec key))
         (chain-code (mbe :logic (bip32-chain-code-fix chain-code)
                          :exec chain-code)))
      (list key chain-code))))