Implement getBIP32Path

cardano-foundation · May 6, 2024 · 217cc16 · 217cc16
1 parent fe0f5ce
commit 217cc16
Show file tree

Hide file tree

Showing 2 changed files with 93 additions and 4 deletions.
diff --git a/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/Address.agda b/lib/customer-deposit-wallet-pure/agda/Cardano/Wallet/Deposit/Pure/Address.agda
@@ -26,6 +26,12 @@ module Cardano.Wallet.Deposit.Pure.Address
 open import Haskell.Prelude
 open import Haskell.Reasoning
 
+open import Cardano.Wallet.Address.BIP32 using
+    ( BIP32Path
+    ; DerivationType
+      ; Hardened
+      ; Soft
+    )
 open import Cardano.Wallet.Address.BIP32_Ed25519 using
     ( XPub
     ; deriveXPubSoft
@@ -83,11 +89,41 @@ data DerivationPath : Set where
 
 {-# COMPILE AGDA2HS DerivationPath #-}
 
+toBIP32Path : DerivationPath → BIP32Path
+toBIP32Path = addSuffix prefix
+  where
+    prefix =
+      (BIP32Path.Segment
+      (BIP32Path.Segment
+      (BIP32Path.Segment
+        BIP32Path.Root
+        Hardened 1857) -- Address derivation standard
+        Hardened 1815) -- ADA
+        Hardened 0)    -- account
+
+    addSuffix : BIP32Path → DerivationPath → BIP32Path
+    addSuffix path DerivationChange =
+        (BIP32Path.Segment
+          path
+          Soft 1)
+    addSuffix path (DerivationCustomer c) =
+        (BIP32Path.Segment
+        (BIP32Path.Segment
+          path
+          Soft 0)
+          Soft c)
+
+{-# COMPILE AGDA2HS toBIP32Path #-}
+
 xpubFromDerivationPath : XPub → DerivationPath → XPub
 xpubFromDerivationPath xpub DerivationChange =
-  deriveXPubSoft xpub 0
+  (deriveXPubSoft xpub
+    1)
 xpubFromDerivationPath xpub (DerivationCustomer c) =
-  deriveXPubSoft (deriveXPubSoft xpub 1) c
+  (deriveXPubSoft
+  (deriveXPubSoft xpub
+    0)
+    c)
 
 {-# COMPILE AGDA2HS xpubFromDerivationPath #-}
 
@@ -243,6 +279,30 @@ lemma-contra-Bool True True impl1 = λ _ → impl1 refl
 lemma-isCustomer-not-isChange s addr =
     lemma-contra-Bool _ _ (lemma-isChange-not-isCustomer s addr)
 
+{-----------------------------------------------------------------------------
+    Observations, BIP32
+------------------------------------------------------------------------------}
+
+getDerivationPath'cases
+  : AddressState → Address → Maybe Customer → Maybe DerivationPath
+getDerivationPath'cases s addr (Just c) = Just (DerivationCustomer c)
+getDerivationPath'cases s addr Nothing =
+  if isChangeAddress s addr
+  then Just DerivationChange
+  else Nothing
+
+getDerivationPath : AddressState → Address → Maybe DerivationPath
+getDerivationPath s addr =
+    getDerivationPath'cases s addr (Map.lookup addr (addresses s))
+
+{-# COMPILE AGDA2HS getDerivationPath'cases #-}
+{-# COMPILE AGDA2HS getDerivationPath #-}
+
+getBIP32Path : AddressState → Address → Maybe BIP32Path
+getBIP32Path s = fmap toBIP32Path ∘ getDerivationPath s
+
+{-# COMPILE AGDA2HS getBIP32Path #-}
+
 {-----------------------------------------------------------------------------
     Observations, specification
 ------------------------------------------------------------------------------}

diff --git a/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/Address.hs b/lib/customer-deposit-wallet-pure/haskell/Cardano/Wallet/Deposit/Pure/Address.hs
@@ -1,5 +1,6 @@
 module Cardano.Wallet.Deposit.Pure.Address where
 
+import Cardano.Wallet.Address.BIP32 (BIP32Path(Root, Segment), DerivationType(Hardened, Soft))
 import Cardano.Wallet.Address.BIP32_Ed25519 (XPub, deriveXPubSoft)
 import Cardano.Wallet.Address.Encoding (mkEnterpriseAddress)
 import Cardano.Wallet.Deposit.Read (Address)
@@ -14,11 +15,24 @@ type Customer = Word31
 data DerivationPath = DerivationCustomer Customer
                     | DerivationChange
 
+toBIP32Path :: DerivationPath -> BIP32Path
+toBIP32Path = addSuffix prefix
+  where
+    prefix :: BIP32Path
+    prefix
+      = Segment (Segment (Segment Root Hardened 1857) Hardened 1815)
+          Hardened
+          0
+    addSuffix :: BIP32Path -> DerivationPath -> BIP32Path
+    addSuffix path DerivationChange = Segment path Soft 1
+    addSuffix path (DerivationCustomer c)
+      = Segment (Segment path Soft 0) Soft c
+
 xpubFromDerivationPath :: XPub -> DerivationPath -> XPub
 xpubFromDerivationPath xpub DerivationChange
-  = deriveXPubSoft xpub 0
+  = deriveXPubSoft xpub 1
 xpubFromDerivationPath xpub (DerivationCustomer c)
-  = deriveXPubSoft (deriveXPubSoft xpub 1) c
+  = deriveXPubSoft (deriveXPubSoft xpub 0) c
 
 deriveAddress :: XPub -> DerivationPath -> Address
 deriveAddress xpub
@@ -42,6 +56,21 @@ isOurs :: AddressState -> Address -> Bool
 isOurs
   = \ s addr -> isChangeAddress s addr || isCustomerAddress s addr
 
+getDerivationPath'cases ::
+                        AddressState -> Address -> Maybe Customer -> Maybe DerivationPath
+getDerivationPath'cases s addr (Just c)
+  = Just (DerivationCustomer c)
+getDerivationPath'cases s addr Nothing
+  = if isChangeAddress s addr then Just DerivationChange else Nothing
+
+getDerivationPath ::
+                  AddressState -> Address -> Maybe DerivationPath
+getDerivationPath s addr
+  = getDerivationPath'cases s addr (Map.lookup addr (addresses s))
+
+getBIP32Path :: AddressState -> Address -> Maybe BIP32Path
+getBIP32Path s = fmap toBIP32Path . getDerivationPath s
+
 swap :: (a, b) -> (b, a)
 swap (x, y) = (y, x)