Add BIP32_Ed25519 module importing from cardano-crypto

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

@@ -0,0 +1,135 @@
+{-# OPTIONS --erasure #-}
+
+module Cardano.Wallet.Address.BIP32_Ed25519 where
+
+open import Haskell.Prelude
+
+open import Haskell.Data.ByteString using
+  ( ByteString
+  )
+open import Haskell.Data.Word.Odd using
+  ( Word31
+  )
+
+{-# FOREIGN AGDA2HS
+{-# LANGUAGE UnicodeSyntax #-}
+import Cardano.Crypto.Wallet
+  ( XPrv
+  , XPub
+  , XSignature
+  , toXPub
+  )
+import Data.ByteString
+  ( ByteString
+  )
+import Data.Maybe
+  ( fromJust
+  )
+import Data.Word
+  ( Word32
+  )
+import Data.Word.Odd
+  ( Word31
+  )
+import qualified Cardano.Crypto.Wallet as CC
+import qualified Data.ByteString as BS
+#-}
+
+dummy : Int
+dummy = 12 -- needed for Agda2hs to add sufficient imports
+
+{-----------------------------------------------------------------------------
+    Extended private and public keys
+------------------------------------------------------------------------------}
+
+-- TODO: Extend to encrypted keys
+postulate
+  XPub : Set  -- plaintext public key
+  XPrv : Set  -- plaintext private key
+
+  toXPub : XPrv → XPub
+
+  XSignature : Set
+  sign   : XPrv → ByteString → XSignature
+  verify : XPub → ByteString → XSignature → Bool
+
+  prop-verify-sign
+    : ∀ (xprv : XPrv)
+        (msg  : ByteString)
+    → let xpub = toXPub xprv
+      in  verify xpub msg (sign xprv msg) ≡ True
+
+{-# FOREIGN AGDA2HS
+sign :: XPrv → ByteString → XSignature
+sign = CC.sign BS.empty
+
+verify :: XPub → ByteString → XSignature → Bool
+verify = CC.verify
+#-}
+
+{-----------------------------------------------------------------------------
+    Key derivation
+------------------------------------------------------------------------------}
+
+postulate
+  deriveXPubSoft : XPub → Word31 → XPub
+  deriveXPrvSoft : XPrv → Word31 → XPrv
+  deriveXPrvHard : XPrv → Word31 → XPrv
+
+  prop-derive-soft
+    : ∀ (xprv : XPrv)
+        (ix   : Word31)
+    → deriveXPubSoft (toXPub xprv) ix
+      ≡ toXPub (deriveXPrvSoft xprv ix)
+
+  -- The following properties about injectivity
+  -- are not true in the strict sense,
+  -- only cryptographically hard.
+  prop-deriveXPubSoft-injective
+    : ∀ (xpub    : XPub)
+        (ix1 ix2 : Word31)
+    → deriveXPubSoft xpub ix1 ≡ deriveXPubSoft xpub ix2
+    → ix1 ≡ ix2
+
+  prop-deriveXPrvSoft-injective
+    : ∀ (xprv    : XPrv)
+        (ix1 ix2 : Word31)
+    → deriveXPrvSoft xprv ix1 ≡ deriveXPrvSoft xprv ix2
+    → ix1 ≡ ix2
+
+  prop-deriveXPrvHard-injective
+    : ∀ (xprv    : XPrv)
+        (ix1 ix2 : Word31)
+    → deriveXPrvHard xprv ix1 ≡ deriveXPrvHard xprv ix2
+    → ix1 ≡ ix2
+
+{-# FOREIGN AGDA2HS
+word32fromWord31 :: Word31 → Word32
+word32fromWord31 = fromInteger . toInteger
+
+deriveXPubSoft :: XPub → Word31 → XPub
+deriveXPubSoft xpub ix =
+  fromJust 
+    (CC.deriveXPub
+      CC.DerivationScheme2
+      xpub
+      (word32fromWord31 ix)
+    )
+  -- deriveXPub always returns Just on Word31
+
+deriveXPrvSoft :: XPrv → Word31 → XPrv
+deriveXPrvSoft xprv ix = 
+  CC.deriveXPrv
+    CC.DerivationScheme2
+    BS.empty
+    xprv
+    (word32fromWord31 ix)
+
+deriveXPrvHard :: XPrv → Word31 → XPrv
+deriveXPrvHard xprv ix =
+  CC.deriveXPrv
+    CC.DerivationScheme2
+    BS.empty
+    xprv
+    (0x80000000 + word32fromWord31 ix)
+#-}

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

@@ -1,5 +1,7 @@
 module Cardano.Wallet.Deposit.Everything where
 
+import Cardano.Wallet.Address.BIP32_Ed25519
+
 import Cardano.Wallet.Deposit.Pure
 import Cardano.Wallet.Deposit.Pure.Timeline
 import Cardano.Wallet.Deposit.Pure.TxSummary

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

@@ -33,6 +33,7 @@ common opts-lib
     -Wincomplete-record-updates
     -Wno-redundant-constraints
     -Wno-unused-matches
+    -Wno-unused-imports
 
   if flag(release)
     ghc-options: -O2 -Werror
@@ -53,11 +54,13 @@ library
   build-depends:
     , base >= 4.14.3.0 && < 4.20
     , bytestring >= 0.10.12.0 && < 0.13
+    , cardano-crypto >= 1.1.2 && < 1.2
     , containers >= 0.6.6 && < 0.8
     , deepseq >= 1.4.4 && < 1.6
     , text >= 1.2.4.1 && < 2.2
     , OddWord >= 1.0.1.1 && < 1.1
   exposed-modules:
+    Cardano.Wallet.Address.BIP32_Ed25519
     Cardano.Wallet.Deposit.Pure
     Cardano.Wallet.Deposit.Pure.Address
     Cardano.Wallet.Deposit.Pure.UTxO.DeltaUTxO

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

@@ -0,0 +1,58 @@
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Cardano.Wallet.Address.BIP32_Ed25519 where
+
+
+import Cardano.Crypto.Wallet
+  ( XPrv
+  , XPub
+  , XSignature
+  , toXPub
+  )
+import Data.ByteString
+  ( ByteString
+  )
+import Data.Maybe
+  ( fromJust
+  )
+import Data.Word.Odd
+  ( Word31
+  )
+import qualified Cardano.Crypto.Wallet as CC
+import qualified Data.ByteString as BS
+
+sign :: XPrv ->ByteString ->XSignature
+sign = CC.sign mempty
+
+verify :: XPub ->ByteString ->XSignature ->Bool
+verify = CC.verify
+
+word32fromWord31 :: Word31 ->Word32
+word32fromWord31 = fromInteger . toInteger
+
+deriveXPubSoft :: XPub ->Word31 ->XPub
+deriveXPubSoft xpub ix =
+  fromJust
+    (CC.deriveXPub
+      CC.DerivationScheme2
+      xpub
+      (word32fromWord31 ix)
+    )
+  -- deriveXPub always returns Just on Word31
+
+deriveXPrvSoft :: XPrv ->Word31 ->XPrv
+deriveXPrvSoft xprv ix =
+  CC.deriveXPrv
+    CC.DerivationScheme2
+    mempty
+    xprv
+    (word32fromWord31 ix)
+
+deriveXPrvHard :: XPrv ->Word31 ->XPrv
+deriveXPrvHard xprv ix =
+  CC.deriveXPrv
+    CC.DerivationScheme2
+    mempty
+    xprv
+    (0x80000000 + word32fromWord31 ix)
+