		Search-engine friendly clone of the ACL2 documentation.

Addresses

Private-key-to-address

Calculate the address for a private key.

Signature
(private-key-to-address priv-key) → address
Arguments: priv-key — Guard (secp256k1-priv-key-p priv-key).
Returns: address — Type (byte-list20p address).

We calculate the public key from the private key, and then use public-key-to-address to calculate the addres.

Definitions and Theorems

Function: private-key-to-address

(defun private-key-to-address (priv-key)
  (declare (xargs :guard (secp256k1-priv-key-p priv-key)))
  (let ((__function__ 'private-key-to-address))
    (declare (ignorable __function__))
    (public-key-to-address (secp256k1-priv-to-pub priv-key))))

Theorem: byte-list20p-of-private-key-to-address

(defthm byte-list20p-of-private-key-to-address
  (b* ((address (private-key-to-address priv-key)))
    (byte-list20p address))
  :rule-classes :rewrite)

Theorem: private-key-to-address-of-secp256k1-priv-key-fix-priv-key

(defthm private-key-to-address-of-secp256k1-priv-key-fix-priv-key
 (equal
  (private-key-to-address (ecurve::secp256k1-priv-key-fix priv-key))
  (private-key-to-address priv-key)))

Theorem: private-key-to-address-secp256k1-priv-key-equiv-congruence-on-priv-key

(defthm
 private-key-to-address-secp256k1-priv-key-equiv-congruence-on-priv-key
 (implies (ecurve::secp256k1-priv-key-equiv priv-key priv-key-equiv)
          (equal (private-key-to-address priv-key)
                 (private-key-to-address priv-key-equiv)))
 :rule-classes :congruence)