Add Cardano.Wallet.Deposit.Read.Value (#34)

This pull request adds an implementation of the `Value` type which
includes both `Coin` and native assets.

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

@@ -78,7 +78,6 @@ open import Cardano.Wallet.Deposit.Read using
     ; TxIn
     ; TxOut
     ; Value
-    ; exceeds
     )
 open import Cardano.Write.Tx.Balance using
     ( ChangeAddressGen

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

@@ -3,6 +3,15 @@ module Cardano.Wallet.Deposit.Read where
 
 open import Haskell.Prelude
 
+open import Cardano.Wallet.Deposit.Read.Value public
+
+{-# FOREIGN AGDA2HS
+-- Working around a limitation in agda2hs.
+import Cardano.Wallet.Deposit.Read.Value 
+    ( Value
+    )
+#-}
+
 import Haskell.Data.ByteString as BS
 import Haskell.Data.Map as Map
 
@@ -26,32 +35,6 @@ instance
 {-# COMPILE AGDA2HS Addr #-}
 {-# COMPILE AGDA2HS Address #-}
 
-{-----------------------------------------------------------------------------
-    Value
-------------------------------------------------------------------------------}
-data Value : Set where
-    MkValue : Integer → Value
-
-instance
-  iSemigroupValue : Semigroup Value
-  _<>_ {{iSemigroupValue}} (MkValue a) (MkValue b) = MkValue (a + b)
-
-  iMonoidValue : Monoid Value
-  iMonoidValue =
-    record {DefaultMonoid (λ where .DefaultMonoid.mempty → MkValue 0)}
-
-exceeds : Value → Value → Bool
-exceeds (MkValue a) (MkValue b) = a >= b
-
-minus : Value → Value → Value
-minus (MkValue a) (MkValue b) = MkValue (a - b)
-
-{-# COMPILE AGDA2HS Value #-}
-{-# COMPILE AGDA2HS iSemigroupValue #-}
-{-# COMPILE AGDA2HS iMonoidValue #-}
-{-# COMPILE AGDA2HS exceeds #-}
-{-# COMPILE AGDA2HS minus #-}
-
 {-----------------------------------------------------------------------------
     Transactions
 ------------------------------------------------------------------------------}

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

@@ -0,0 +1,140 @@
+{-# OPTIONS --erasure #-}
+module Cardano.Wallet.Deposit.Read.Value where
+
+open import Haskell.Prelude
+
+open import Haskell.Data.Maybe using
+    ( fromMaybe
+    )
+
+import Haskell.Data.ByteString as BS
+import Haskell.Data.Map as Map
+
+{-----------------------------------------------------------------------------
+    Coin
+------------------------------------------------------------------------------}
+Coin = Nat
+
+-- general helper, remove when updating adga2hs dependency
+subst : ∀ {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x → P y
+subst P refl z = z
+
+monusCoin : Coin → Coin → Coin
+monusCoin a b = case a < b of λ
+  { False {{eq}} →
+    _-_ a b {{subst IsFalse (sym eq) IsFalse.itsFalse}}
+  ; True → 0
+  }
+
+{-# COMPILE AGDA2HS Coin #-}
+{-# COMPILE AGDA2HS monusCoin #-}
+
+{-----------------------------------------------------------------------------
+    Assets
+------------------------------------------------------------------------------}
+AssetName  = BS.ByteString   -- max 32 bytes
+ScriptHash = BS.ByteString   -- blake2b-224
+PolicyID   = ScriptHash
+
+{-# COMPILE AGDA2HS AssetName #-}
+{-# COMPILE AGDA2HS ScriptHash #-}
+{-# COMPILE AGDA2HS PolicyID #-}
+
+Quantity = Integer
+
+{-# COMPILE AGDA2HS Quantity #-}
+
+data AssetID : Set where
+    AdaID : AssetID
+    Asset : PolicyID → AssetName → AssetID
+
+{-# COMPILE AGDA2HS AssetID #-}
+
+instance
+  iEqAssetID : Eq AssetID
+  iEqAssetID ._==_ AdaID AdaID = True
+  iEqAssetID ._==_ (Asset a1 b1) (Asset a2 b2) = a1 == a2 && b1 == b2
+  iEqAssetID ._==_ _ _ = False
+
+postulate instance
+  iOrdAssetID : Ord AssetID
+
+{-# COMPILE AGDA2HS iEqAssetID derive #-}
+{-# COMPILE AGDA2HS iOrdAssetID derive #-}
+
+{-----------------------------------------------------------------------------
+    Value
+------------------------------------------------------------------------------}
+record Value : Set where
+  field
+    ada    : Coin
+    assets : Map.Map (PolicyID × AssetName) Quantity
+
+open Value public
+
+{-# COMPILE AGDA2HS Value #-}
+
+valueFromList : Coin → List (PolicyID × AssetName × Quantity) → Value
+valueFromList coin xs = record
+    { ada = coin
+    ; assets = Map.fromList (map (λ { (p , n , q) → ((p , n) , q) }) xs)
+    }
+
+{-# COMPILE AGDA2HS valueFromList #-}
+
+injectCoin : Coin → Value
+injectCoin coin = record { ada = coin; assets = Map.empty }
+
+{-# COMPILE AGDA2HS injectCoin #-}
+
+getCoin : Value → Coin
+getCoin v = ada v
+
+{-# COMPILE AGDA2HS getCoin #-}
+
+largerOrEqual : Value → Value → Bool
+largerOrEqual a b =
+    ada a >= ada b
+    && Map.null (Map.filterWithKey isSmallerThanB (assets a))
+  where
+    isSmallerThanB : PolicyID × AssetName → Quantity → Bool
+    isSmallerThanB key qa = qa < fromMaybe 0 (Map.lookup key (assets b))
+
+{-# COMPILE AGDA2HS largerOrEqual #-}
+
+instance
+  iSemigroupValue : Semigroup Value
+  _<>_ {{iSemigroupValue}} a b =
+    record
+      { ada = ada a + ada b
+      ; assets = Map.unionWith (_+_) (assets a) (assets b)
+      }
+
+  iMonoidValue : Monoid Value
+  iMonoidValue =
+    record {DefaultMonoid (λ where
+      .DefaultMonoid.mempty → record { ada = 0; assets = Map.empty }
+    )}
+
+{-# COMPILE AGDA2HS iSemigroupValue #-}
+{-# COMPILE AGDA2HS iMonoidValue #-}
+
+monus : Value → Value → Value
+monus a b = record
+  { ada = monusCoin (ada a) (ada b)
+  ; assets = Map.unionWith minus (assets a) (assets b)
+  }
+  where
+    minus : Quantity → Quantity → Quantity
+    minus a b = a - b
+
+{-# COMPILE AGDA2HS monus #-}
+
+{-----------------------------------------------------------------------------
+    Value properties
+------------------------------------------------------------------------------}
+
+prop-coin-inject
+    : ∀ (c : Coin)
+    → getCoin (injectCoin c) ≡ c
+prop-coin-inject coin = refl

lib/customer-deposit-wallet-pure/agda/Cardano/Write/Tx/Balance.agda

@@ -24,8 +24,8 @@ open import Cardano.Wallet.Deposit.Read using
     ; TxIn
     ; TxOut
     ; Value
-    ; exceeds
-    ; minus
+    ; largerOrEqual
+    ; monus
     )
 open import Haskell.Data.List.Prop using ( _∈_ )
 open import Haskell.Data.Maybe using ( isJust )
@@ -76,9 +76,9 @@ coinSelectionGreedy
 coinSelectionGreedy v [] = (mempty , [])
 coinSelectionGreedy v ((txin , txout) ∷ xs) =
     let dv = (TxOut.value txout)
-    in  if exceeds v dv
-            then secondCons txin $ coinSelectionGreedy (minus v dv) xs
-            else (minus dv v , [])
+    in  if largerOrEqual v dv
+            then secondCons txin $ coinSelectionGreedy (monus v dv) xs
+            else (monus dv v , [])
 
 {-# COMPILE AGDA2HS secondCons #-}
 {-# COMPILE AGDA2HS coinSelectionGreedy #-}
@@ -102,7 +102,7 @@ balanceTransaction utxo newAddress c0 partialTx =
             ; value = changeValue
             }
     in
-    if exceeds target (UTxO.balance utxo)
+    if largerOrEqual target (UTxO.balance utxo)
         then Nothing
         else Just $ record
           { outputs = changeOutput ∷ PartialTx.outputs partialTx
@@ -134,7 +134,7 @@ lemma-balanceTransaction-addresses
   → map TxOut.address (TxBody.outputs tx)
     ≡ fst (new c0) ∷ map TxOut.address (PartialTx.outputs partialTx)
 lemma-balanceTransaction-addresses u partialTx new c0 tx balance
-  with exceeds (totalOut partialTx) (UTxO.balance u)
+  with largerOrEqual (totalOut partialTx) (UTxO.balance u)
 ...  | True = magic (unequal tx balance)
 ...  | False = begin
           map TxOut.address (TxBody.outputs tx)

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

@@ -28,18 +28,18 @@ unionWithMaybe f Nothing my = my
 unionWithMaybe f (Just x) Nothing = Just x
 unionWithMaybe f (Just x) (Just y) = Just (f x y)
 
+intersectionWithMaybe : (f : a → b → c) → Maybe a → Maybe b → Maybe c
+intersectionWithMaybe f (Just x) (Just y) = Just (f x y)
+intersectionWithMaybe _ _ _ = Nothing
+
 {-----------------------------------------------------------------------------
     Data.Map
 ------------------------------------------------------------------------------}
 
 postulate
   Map : ∀ (k : Set) {{iOrd : Ord k}} → Set → Set
 
-module
-    OperationsAndProperties
-      {k a : Set}
-      {{_ : Ord k}}
-  where
+module _ {k a : Set} {{_ : Ord k}} where
   postulate
     lookup    : k → Map k a → Maybe a
     null      : Map k a → Bool
@@ -59,6 +59,8 @@ module
     instance
       iMapFunctor : Functor (Map k)
 
+    mapWithKey : (k → a → b) → Map k a → Map k b
+
     prop-member-null
       : ∀ (m : Map k a)
           (_ : ∀ (key : k) → lookup key m ≡ Nothing)
@@ -161,13 +163,38 @@ module
   foldMap' : ∀ {{_ : Monoid b}} → (a → b) → Map k a → b
   foldMap' f = foldMap f ∘ L.map snd ∘ toAscList
 
-open OperationsAndProperties public
+postulate
+  prop-lookup-fmap
+    : ∀ {a b k : Set} {{_ : Ord k}}
+        (key : k)
+        (m : Map k a)
+        (f : a → b)
+    → lookup key (fmap {{iMapFunctor {k} {a}}} f m)
+      ≡ fmap f (lookup key m)
+
+  prop-lookup-mapWithKey
+    : ∀ {a b k : Set} {{_ : Ord k}}
+        (key : k)
+        (m : Map k a)
+        (f : k → a → b)
+    → lookup key (mapWithKey f m)
+      ≡ fmap (f key) (lookup key m)
 
 instance
   iMapFoldable : ∀ {k : Set} {{_ : Ord k}} → Foldable (Map k)
   iMapFoldable =
     record {DefaultFoldable (record {foldMap = foldMap'})}
 
+module _ {k a b c : Set} {{_ : Ord k}} where
+  postulate
+    intersectionWith : (a → b → c) → Map k a → Map k b → Map k c
+
+    prop-lookup-intersectionWith
+      : ∀ (key : k) (ma : Map k a) (mb : Map k b)
+          (f : a → b → c)
+      → lookup key (intersectionWith f ma mb)
+        ≡ intersectionWithMaybe f (lookup key ma) (lookup key mb)
+
 {-----------------------------------------------------------------------------
     Test proofs
 ------------------------------------------------------------------------------}

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

@@ -17,6 +17,11 @@ catMaybes [] = []
 catMaybes (Nothing ∷ xs) = catMaybes xs
 catMaybes (Just x ∷ xs) = x ∷ catMaybes xs
 
+fromMaybe : ∀ {a : Set} → a → Maybe a → a
+fromMaybe _ (Just a) = a
+fromMaybe a Nothing = a
+
 {-# COMPILE AGDA2HS isNothing #-}
 {-# COMPILE AGDA2HS isJust #-}
 {-# COMPILE AGDA2HS catMaybes #-}
+{-# COMPILE AGDA2HS fromMaybe #-}

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

@@ -74,6 +74,7 @@ library
     Cardano.Wallet.Deposit.Pure.Timeline
     Cardano.Wallet.Deposit.Pure.TxSummary
     Cardano.Wallet.Deposit.Read
+    Cardano.Wallet.Deposit.Read.Value
     Cardano.Write.Tx.Balance
   other-modules:
     Haskell.Data.ByteString

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

@@ -1,7 +1,8 @@
 module Cardano.Wallet.Deposit.Pure where
 
 import Cardano.Wallet.Address.BIP32_Ed25519 (XPub)
-import Cardano.Wallet.Deposit.Read (Address, Block(transactions), ChainPoint, Tx, TxBody, TxOut(TxOutC), Value, chainPointFromBlock)
+import Cardano.Wallet.Deposit.Read (Address, Block(transactions), ChainPoint, Tx, TxBody, TxOut(TxOutC), chainPointFromBlock)
+import Cardano.Wallet.Deposit.Read.Value (Value)
 import Cardano.Write.Tx.Balance (ChangeAddressGen, PartialTx(PartialTxC), balanceTransaction)
 import qualified Haskell.Data.Map as Map (Map, lookup)
 

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

@@ -6,7 +6,8 @@ import Cardano.Wallet.Deposit.Pure.UTxO.UTxO (UTxO)
 import qualified Cardano.Wallet.Deposit.Pure.UTxO.UTxO as UTxO (filterByAddress, null, restrictedBy)
 import Cardano.Wallet.Deposit.Pure.UTxO.ValueTransfer (ValueTransfer, fromReceived, fromSpent)
 import Cardano.Wallet.Deposit.Read (Tx(txbody, txid), TxBody(inputs, outputs))
-import qualified Cardano.Wallet.Deposit.Read as Read (Addr, Address, TxIn, TxOut(address, value), Value)
+import qualified Cardano.Wallet.Deposit.Read as Read (Addr, Address, TxIn, TxOut(address, value))
+import qualified Cardano.Wallet.Deposit.Read.Value as Read (Value)
 import Data.Set (Set)
 import qualified Haskell.Data.ByteString (ByteString)
 import qualified Haskell.Data.Map as Map (Map, elems, fromList, fromListWith, map, unionWith)

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

@@ -1,6 +1,7 @@
 module Cardano.Wallet.Deposit.Pure.UTxO.UTxO where
 
-import Cardano.Wallet.Deposit.Read (Address, TxIn, TxOut(address, value), Value)
+import Cardano.Wallet.Deposit.Read (Address, TxIn, TxOut(address, value))
+import Cardano.Wallet.Deposit.Read.Value (Value)
 import Data.Set (Set)
 import qualified Haskell.Data.Map as Map (Map, empty, filter, keysSet, member, null, restrictKeys, unionWith, withoutKeys)
 import qualified Haskell.Data.Set as Set (filter)

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

@@ -1,6 +1,6 @@
 module Cardano.Wallet.Deposit.Pure.UTxO.ValueTransfer where
 
-import Cardano.Wallet.Deposit.Read (Value)
+import Cardano.Wallet.Deposit.Read.Value (Value)
 
 data ValueTransfer = ValueTransfer{spent :: Value,
                                    received :: Value}

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

@@ -3,24 +3,15 @@ module Cardano.Wallet.Deposit.Read where
 import qualified Haskell.Data.ByteString as BS (ByteString)
 import Numeric.Natural (Natural)
 
+-- Working around a limitation in agda2hs.
+import Cardano.Wallet.Deposit.Read.Value
+    ( Value
+    )
+
 type Addr = BS.ByteString
 
 type Address = Addr
 
-data Value = MkValue Integer
-
-instance Semigroup Value where
-    MkValue a <> MkValue b = MkValue (a + b)
-
-instance Monoid Value where
-    mempty = MkValue 0
-
-exceeds :: Value -> Value -> Bool
-exceeds (MkValue a) (MkValue b) = a >= b
-
-minus :: Value -> Value -> Value
-minus (MkValue a) (MkValue b) = MkValue (a - b)
-
 type TxId = BS.ByteString
 
 type Ix = Int