Calculate the address for a public key.
The address consists of the rightmost 160 bits of the 256-bit Keccak-256 hash of the serialized public key [YP:(284)]. This is equivalent to the rightmost 20 bytes of the 32-byte hash.
This function corresponds to ``part of'' the function
The function private-key-to-address calculates an address from a private key instead.
(defun public-key-to-address (pub-key) (declare (xargs :guard (secp256k1-pub-key-p pub-key))) (let ((__function__ 'public-key-to-address)) (declare (ignorable __function__)) (b* ((pub-key (mbe :logic (secp256k1-pub-key-fix pub-key) :exec pub-key)) (uncompressed-form (secp256k1-point-to-bytes pub-key nil)) (hash (keccak-256-bytes uncompressed-form)) (address (nthcdr 12 hash))) address)))
(defthm byte-list20p-of-public-key-to-address (b* ((address (public-key-to-address pub-key))) (byte-list20p address)) :rule-classes :rewrite)
(defthm public-key-to-address-of-secp256k1-pub-key-fix-pub-key (equal (public-key-to-address (secp256k1-pub-key-fix pub-key)) (public-key-to-address pub-key)))
(defthm public-key-to-address-secp256k1-pub-key-equiv-congruence-on-pub-key (implies (ecurve::secp256k1-pub-key-equiv pub-key pub-key-equiv) (equal (public-key-to-address pub-key) (public-key-to-address pub-key-equiv))) :rule-classes :congruence)