Add and use mkEnterpriseAddress (#29)

This pull request

* adds a function `mkEnterpriseAddress` that maps a payment `XPub` to an
enterprise address
* uses this function in `deriveAddress`.

### Comments

* With this pull request, the `AddressState` type can be used to
generate addresses which are (should be) spendable on mainnet.

lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Address/Encoding.agda

@@ -0,0 +1,62 @@
+{-# OPTIONS --erasure #-}
+
+module Cardano.Wallet.Address.Encoding
+    {-
+    ; mkEnterpriseAddress
+    ; prop-mkEnterpriseAddress-injective
+    -}
+    where
+
+open import Haskell.Prelude
+
+open import Cardano.Wallet.Address.BIP32_Ed25519 using
+  ( XPub
+  ; rawSerialiseXPub
+  ; prop-rawSerialiseXPub-injective
+  )
+open import Cardano.Wallet.Address.Hash using
+  ( blake2b'224
+  ; prop-blake2b'224-injective
+  )
+open import Cardano.Wallet.Deposit.Read using
+  ( Addr
+  )
+open import Haskell.Data.ByteString using
+  ( ByteString
+  ; singleton
+  ; prop-<>-cancel-left
+  )
+open import Haskell.Data.Word using
+  ( Word8
+  )
+
+{-----------------------------------------------------------------------------
+    Create addresses from public keys
+
+    For magic numbers, see
+    https://github.com/cardano-foundation/CIPs/tree/master/CIP-0019
+------------------------------------------------------------------------------}
+
+tagEnterprise : Word8 
+tagEnterprise = 0b01100001
+
+{-# COMPILE AGDA2HS tagEnterprise #-}
+
+mkEnterpriseAddress : XPub → Addr
+mkEnterpriseAddress xpub =
+    singleton tagEnterprise <> blake2b'224 (rawSerialiseXPub xpub)
+
+{-# COMPILE AGDA2HS mkEnterpriseAddress #-}
+
+{-----------------------------------------------------------------------------
+    Properties
+------------------------------------------------------------------------------}
+
+prop-mkEnterpriseAddress-injective
+  : ∀ (x y : XPub)
+  → mkEnterpriseAddress x ≡ mkEnterpriseAddress y
+  → x ≡ y
+prop-mkEnterpriseAddress-injective x y =
+  prop-rawSerialiseXPub-injective _ _
+    ∘ prop-blake2b'224-injective _ _
+    ∘ prop-<>-cancel-left (singleton tagEnterprise) _ _

lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/Address.agda

@@ -34,9 +34,9 @@ open import Cardano.Wallet.Address.BIP32_Ed25519 using
     ; prop-deriveXPubSoft-not-identity
     ; prop-rawSerialiseXPub-injective
     )
-open import Cardano.Wallet.Address.Hash using
-    ( blake2b'256
-    ; prop-blake2b'256-injective
+open import Cardano.Wallet.Address.Encoding using
+    ( mkEnterpriseAddress
+    ; prop-mkEnterpriseAddress-injective
     )
 open import Cardano.Wallet.Deposit.Read using
     ( Address
@@ -77,11 +77,6 @@ Customer = Word31
 
 {-# COMPILE AGDA2HS Customer #-}
 
-hashFromXPub : XPub → BS.ByteString
-hashFromXPub = blake2b'256 ∘ rawSerialiseXPub
-
-{-# COMPILE AGDA2HS hashFromXPub #-}
-
 data DerivationPath : Set where
   DerivationCustomer : Customer → DerivationPath
   DerivationChange   : DerivationPath
@@ -96,9 +91,8 @@ xpubFromDerivationPath xpub (DerivationCustomer c) =
 
 {-# COMPILE AGDA2HS xpubFromDerivationPath #-}
 
--- FIXME: Proper enterprise address.
 deriveAddress : XPub → DerivationPath → Address
-deriveAddress xpub = hashFromXPub ∘ xpubFromDerivationPath xpub
+deriveAddress xpub = mkEnterpriseAddress ∘ xpubFromDerivationPath xpub
 
 {-# COMPILE AGDA2HS deriveAddress #-}
 
@@ -130,8 +124,7 @@ lemma-xpubFromDerivationPath-injective {_} {DerivationChange} {DerivationChange}
 --
 lemma-derive-injective =
   lemma-xpubFromDerivationPath-injective
-  ∘ prop-rawSerialiseXPub-injective _ _
-  ∘ prop-blake2b'256-injective _ _
+  ∘ prop-mkEnterpriseAddress-injective _ _
 
 --
 @0 lemma-derive-notCustomer

lib/customer-deposit-wallet-pure/agda/Haskell/Data/ByteString.agda

@@ -26,17 +26,29 @@ postulate
     iEqByteString  : Eq ByteString
 
   iOrdByteString₀ : Ord ByteString
-  
+
 instance
   iOrdByteString : Ord ByteString
   iOrdByteString = record iOrdByteString₀ { super = iEqByteString }
 
 empty : ByteString
 empty = pack []
 
+append : ByteString → ByteString → ByteString
+append x y = pack (unpack x ++ unpack y)
+
 singleton : Word8 → ByteString
 singleton x = pack (x ∷ [])
 
+instance
+  iSemigroupDeltaUTxO : Semigroup ByteString
+  iSemigroupDeltaUTxO = record { _<>_ = append }
+
+instance
+  iMonoidDeltaUTxO : Monoid ByteString
+  iMonoidDeltaUTxO =
+    record {DefaultMonoid (λ where .DefaultMonoid.mempty → empty)}
+
 {-----------------------------------------------------------------------------
     Properties
 ------------------------------------------------------------------------------}
@@ -68,3 +80,52 @@ prop-pack-injective x y eq =
     y
   ∎
 
+prop-unpack-injective
+  : ∀ (x y : ByteString)
+  → unpack x ≡ unpack y
+  → x ≡ y
+prop-unpack-injective x y eq =
+  begin
+    x
+  ≡⟨ sym (prop-pack-∘-unpack x) ⟩
+    pack (unpack x)
+  ≡⟨ cong pack eq ⟩
+    pack (unpack y)
+  ≡⟨ prop-pack-∘-unpack y ⟩
+    y
+  ∎
+
+prop-pack-morphism
+  : ∀ (x y : List Word8)
+  → pack x <> pack y ≡ pack (x ++ y)
+prop-pack-morphism x y =
+  begin
+    pack x <> pack y
+  ≡⟨⟩
+    pack (unpack (pack x) ++ unpack (pack y))
+  ≡⟨ cong (λ X → pack (X ++ unpack (pack y))) (prop-unpack-∘-pack x) ⟩
+    pack (x ++ unpack (pack y))
+  ≡⟨ cong (λ Y → pack (x ++ Y)) (prop-unpack-∘-pack y) ⟩
+    pack (x ++ y)
+  ∎
+
+prop-unpack-morphism
+  : ∀ (x y : ByteString)
+  → unpack (x <> y) ≡ unpack x ++ unpack y
+prop-unpack-morphism x y =
+  begin
+    unpack (x <> y)
+  ≡⟨ cong unpack refl ⟩
+    unpack (pack (unpack x ++ unpack y))
+  ≡⟨ prop-unpack-∘-pack _ ⟩
+    unpack x ++ unpack y
+  ∎
+
+prop-<>-cancel-left
+  : ∀ (x y z : ByteString)
+  → x <> y ≡ x <> z
+  → y ≡ z
+prop-<>-cancel-left x y z =
+  prop-unpack-injective _ _
+  ∘ ++-cancel-left (unpack x) (unpack y)
+  ∘ prop-pack-injective _ _

lib/customer-deposit-wallet-pure/customer-deposit-wallet-pure.cabal

@@ -62,6 +62,7 @@ library
     , OddWord >= 1.0.1.1 && < 1.1
   exposed-modules:
     Cardano.Wallet.Address.BIP32_Ed25519
+    Cardano.Wallet.Address.Encoding
     Cardano.Wallet.Address.Hash
     Cardano.Wallet.Deposit.Pure
     Cardano.Wallet.Deposit.Pure.Address

lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Address/Encoding.hs

@@ -0,0 +1,15 @@
+module Cardano.Wallet.Address.Encoding where
+
+import Cardano.Wallet.Address.BIP32_Ed25519 (XPub, rawSerialiseXPub)
+import Cardano.Wallet.Address.Hash (blake2b'224)
+import Cardano.Wallet.Deposit.Read (Addr)
+import Data.Word (Word8)
+import Haskell.Data.ByteString (singleton)
+
+tagEnterprise :: Word8
+tagEnterprise = 97
+
+mkEnterpriseAddress :: XPub -> Addr
+mkEnterpriseAddress xpub
+  = singleton tagEnterprise <> blake2b'224 (rawSerialiseXPub xpub)
+

lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/Address.hs

@@ -1,7 +1,7 @@
 module Cardano.Wallet.Deposit.Pure.Address where
 
-import Cardano.Wallet.Address.BIP32_Ed25519 (XPub, deriveXPubSoft, rawSerialiseXPub)
-import Cardano.Wallet.Address.Hash (blake2b'256)
+import Cardano.Wallet.Address.BIP32_Ed25519 (XPub, deriveXPubSoft)
+import Cardano.Wallet.Address.Encoding (mkEnterpriseAddress)
 import Cardano.Wallet.Deposit.Read (Address)
 import Cardano.Write.Tx.Balance (ChangeAddressGen)
 import Data.Word.Odd (Word31)
@@ -11,9 +11,6 @@ import Haskell.Data.Maybe (isJust)
 
 type Customer = Word31
 
-hashFromXPub :: XPub -> BS.ByteString
-hashFromXPub = blake2b'256 . rawSerialiseXPub
-
 data DerivationPath = DerivationCustomer Customer
                     | DerivationChange
 
@@ -24,7 +21,8 @@ xpubFromDerivationPath xpub (DerivationCustomer c)
   = deriveXPubSoft (deriveXPubSoft xpub 1) c
 
 deriveAddress :: XPub -> DerivationPath -> Address
-deriveAddress xpub = hashFromXPub . xpubFromDerivationPath xpub
+deriveAddress xpub
+  = mkEnterpriseAddress . xpubFromDerivationPath xpub
 
 deriveCustomerAddress :: XPub -> Customer -> Address
 deriveCustomerAddress xpub c