Implementation of abstract ledger spec using Backpack. (#6)

* Implementation of abstract ledger spec using Backpack.

How does this work?

We parametrise over a signature `UTxO`, which currenly encompasses the types
`Hash`, `Coin` and `Addr`. We can specify explicitly our constraints on these
types. We then define an abstract ledger in `Ledger.Abstract` which depends on
these types, but knows nothing of their concrete representation.

In `simple/UTxO` we instantiate these parameters as in Jared's original spec.

There's a bit of a wart at the moment in that I don't think I can have the
`HasHash` class being part of the signature. So this is defined in
`Ledger.Abstract` and we then need to define the `simple/Ledger` module to
contain these.

* Define transitions for a simple ledger system.

* Change copyright, maintainer etc.

.gitignore

@@ -18,4 +18,8 @@
 **/latex/*.blg
 **/latex/*-blx.aux
 **/latex/*-blx.bib
-**/latex/*.run.xml
+**/latex/*.run.xml
+/specs/ledger/hs/.ghc.environment.x86_64-linux-8.4.3
+/specs/ledger/hs/.ghc.environment.x86_64-linux-8.6.0.20180810
+**/*~
+**/dist-newstyle

specs/ledger/hs/CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for cs-ledger
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

specs/ledger/hs/LICENSE

@@ -0,0 +1,20 @@
+Copyright (c) 2018 IOHK
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

specs/ledger/hs/Makefile

@@ -0,0 +1,13 @@
+help: ## Print documentation
+	@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | sort | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}'
+
+ghcid: ## Run ghcid
+	ghcid \
+					--command "cabal new-repl ledger-simple"
+
+ghcid-test: ## Have ghcid run the test suite
+	ghcid \
+          --command "stack ghci utxo:lib utxo:test:utxo-test --ghci-options=-fobject-code" \
+          --test "main"
+
+.PHONY: ghcid ghcid-test help

specs/ledger/hs/Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

specs/ledger/hs/cabal.project.local

@@ -0,0 +1 @@
+with-compiler: ghc-8.6.0.20180810

specs/ledger/hs/cs-ledger.cabal

@@ -0,0 +1,69 @@
+-- Initial cs-ledger.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                cs-ledger
+version:             0.1.0.0
+synopsis:            Executable specification of Cardano ledger
+-- description:
+homepage:            https://github.com/input-output-hk/cardano-chain
+license:             MIT
+license-file:        LICENSE
+author:              IOHK Formal Methods Team
+maintainer:          formal.methods@iohk.io
+-- copyright:
+category:            Testing
+build-type:          Simple
+extra-source-files:  CHANGELOG.md, README.md
+cabal-version:       >= 2.0
+
+library utxo-sig
+  signatures:          UTxO
+  exposed-modules:     Ledger.Abstract
+  build-depends:       base >=4.11 && <5
+                     , bytestring
+                     , containers
+                     , cryptonite
+                     , memory
+                     , text
+  hs-source-dirs:      src/sig/utxo
+  default-language:    Haskell2010
+
+library extension-sig
+  signatures:          Extension
+  exposed-modules:     Ledger.Transition
+  build-depends:       base >=4.11 && <5
+                     , bytestring
+                     , text
+  hs-source-dirs:      src/sig/extension
+  default-language:    Haskell2010
+
+library utxo-impl-simple
+  hs-source-dirs:      src/simple/utxo
+  exposed-modules:     UTxO
+  default-language:    Haskell2010
+  build-depends:       base >=4.12 && <5
+                     , cryptonite
+                     , memory
+
+library extension-impl-simple
+  hs-source-dirs:      src/simple/extension
+  exposed-modules:     Extension
+  default-language:    Haskell2010
+  build-depends:       base >=4.12 && <5
+                     , cryptonite
+                     , memory
+                     , utxo-sig
+
+library ledger-simple
+  hs-source-dirs:      src/simple/ledger
+  exposed-modules:     Ledger
+  default-language:    Haskell2010
+  build-depends:       base >=4.11 && <5
+                     , bytestring
+                     , containers
+                     , cryptonite
+                     , memory
+                     , utxo-sig
+                     , utxo-impl-simple
+                     , extension-sig
+                     , extension-impl-simple

specs/ledger/hs/src/sig/extension/Extension.hsig

@@ -0,0 +1,31 @@
+signature Extension where
+
+---------------------------------------------------------------------------------
+-- UTxO transitions
+---------------------------------------------------------------------------------
+-- | Core state which can be extended.
+data State
+
+instance Eq State
+
+-- | Signal which may extend a leger.
+data Signal
+
+-- | Base states, which may be considered valid without any transitions.
+baseStates :: [State]
+
+-- | All states must be reachable from a finite set of _base states_ through a
+-- chain of valid transitions. In order to allow us to validate from the "top
+-- down", we additionally require that we be able to deconstruct the state layer
+-- by layer.
+--
+-- TODO This is basically requiring that `State` be `Foldable` if we made it
+-- polymorphic. Would this be easier to understand?
+peelState :: State -> (State, Signal)
+
+-- | Type encapsulating the set of possible failures at the predicate level when
+-- extending a ledger.
+data PredicateFailure
+
+instance Eq PredicateFailure
+instance Show PredicateFailure

specs/ledger/hs/src/sig/extension/Ledger/Transition.hs

@@ -0,0 +1,67 @@
+{-# LANGUAGE LambdaCase #-}
+{- | Ledger transitions.
+
+This module describes ledger transitions; that is, the rules which allow one to
+define a valid ledger.
+
+These serve the dual purpose of _generation_ and _validation_ of ledgers.
+
+-}
+
+module Ledger.Transition where
+
+import qualified Data.Text as T
+import Data.Maybe (mapMaybe)
+import Data.Either (rights)
+import Extension
+
+-- | A 'Transition' specifies the conditions under which some signal might
+-- effect a state transition over some state.
+--
+-- Given a state st and a signal s, we have two options:
+--
+-- - The signal is _invalid_ for this given state, and no transition is
+--   effected.
+--
+-- - The signal is valid for the state, and some function is applied to the
+--   state to generate a new state.
+--
+-- The question of validity is determined by a set of preconditions which apply
+-- over the state and signal.
+data Transition = Transition
+  { _tPredicates :: [Predicate]
+  , _tUncheckedApply :: State -> Signal -> State
+  }
+
+-- | Apply a transition, checking the preconditions.
+applyTransition :: Transition -> State -> Signal -> Either [PredicateFailure] State
+applyTransition (Transition preds app) st sig =
+    case gatherFailures $ checkPredicate <$> preds of
+      [] -> Right $ app st sig
+      xs -> Left xs
+  where
+    checkPredicate (Predicate _ validate) = validate st sig
+    gatherFailures :: [PredicateResult] -> [PredicateFailure]
+    gatherFailures = mapMaybe (\case Passed -> Nothing; Failed pr -> Just pr)
+
+-- | The result of a predicate
+data PredicateResult
+  = Passed
+  | Failed PredicateFailure
+
+-- | A precondition on the application of a signal to a state.
+data Predicate = Predicate
+  { _pName :: T.Text
+  , _pValidate :: State -> Signal -> PredicateResult
+  }
+
+validateAll
+  :: [Transition] -- ^ Transition rules for the system
+  -> State -- ^ State to validate
+  -> Bool -- TODO This should be something more like `Validity`
+validateAll _ st | st `elem` baseStates = True
+validateAll transitions st =
+  let
+    (oldSt, signal) = peelState st
+    canTransition = st `elem` (rights $ (\t -> applyTransition t oldSt signal) <$> transitions)
+  in canTransition && validateAll transitions st

specs/ledger/hs/src/sig/utxo/Ledger/Abstract.hs

@@ -0,0 +1,120 @@
+{-# LANGUAGE FlexibleContexts #-}
+{- |
+Core implementation of the ledger logic.
+-}
+module Ledger.Abstract where
+
+import qualified Data.ByteString.Char8 as BS
+import           Data.Map              (Map)
+import qualified Data.Map              as Map
+import           Data.Set              (Set)
+import qualified Data.Set              as Set
+import           UTxO
+import           Numeric.Natural       (Natural)
+
+-- | Hash part of the ledger paylod
+class HasHash a where
+  hash :: a -> Hash
+
+-- |A unique ID of a transaction, which is computable from the transaction.
+newtype TxId = TxId { getTxId :: Hash }
+  deriving (Show, Eq, Ord)
+
+-- |The input of a UTxO.
+--
+--     * __TODO__ - is it okay to use list indices instead of implementing the Ix Type?
+data TxIn = TxIn TxId Natural deriving (Show, Eq, Ord)
+
+-- |The output of a UTxO.
+data TxOut = TxOut Addr Coin deriving (Show, Eq)
+
+-- |The unspent transaction outputs.
+newtype UTxO = UTxO (Map TxIn TxOut) deriving (Show, Eq)
+
+-- |A raw transaction
+data Tx = Tx { inputs  :: Set TxIn
+             , outputs :: [TxOut]
+             } deriving (Show, Eq)
+
+-- |Compute the id of a transaction.
+txid :: HasHash Tx => Tx -> TxId
+txid = TxId . hash
+
+-- |Compute the UTxO inputs of a transaction.
+txins :: Tx -> Set TxIn
+txins = inputs
+
+-- |Compute the UTxO outputs of a transaction.
+txouts :: HasHash Tx => Tx -> UTxO
+txouts tx = UTxO $
+  Map.fromList [(TxIn transId idx, out) | (out, idx) <- zip (outputs tx) [0..]]
+  where
+    transId = txid tx
+
+-- |Representation of the owner of key pair.
+newtype Owner = Owner Natural deriving (Show, Eq, Ord)
+
+-- |Signing Key.
+newtype SKey = SKey Owner deriving (Show, Eq, Ord)
+
+-- |Verification Key.
+newtype VKey = VKey Owner deriving (Show, Eq, Ord)
+
+-- |Key Pair.
+data KeyPair = KeyPair
+  {sKey :: SKey, vKey :: VKey} deriving (Show, Eq, Ord)
+
+-- |Return a key pair for a given owner.
+keyPair :: Owner -> KeyPair
+keyPair owner = KeyPair (SKey owner) (VKey owner)
+
+-- |A digital signature.
+data Sig a = Sig a Owner deriving (Show, Eq, Ord)
+
+-- |Proof/Witness that a transaction is authorized by the given key holder.
+data Wit = Wit VKey (Sig Tx) deriving (Show, Eq)
+
+-- |A fully formed transaction.
+--
+--     * __TODO__ - Would it be better to name this type Tx, and rename Tx to TxBody?
+data TxWits = TxWits
+              { body     :: Tx
+              , witneses :: Set Wit
+              } deriving (Show, Eq)
+
+-- |Produce a digital signature
+sign :: SKey -> a -> Sig a
+sign (SKey k) d = Sig d k
+
+-- |Create a witness for transaction
+makeWitness :: KeyPair -> Tx -> Wit
+makeWitness keys tx = Wit (vKey keys) (sign (sKey keys) tx)
+
+-- |Verify a digital signature
+verify :: Eq a => VKey -> a -> Sig a -> Bool
+verify (VKey vk) vd (Sig sd sk) = vk == sk && vd == sd
+
+-- |Domain restriction
+--
+--     * __TODO__ - better symbol?
+(◁) :: Set TxIn -> UTxO -> UTxO
+ins ◁ (UTxO utxo) =
+  UTxO $ Map.filterWithKey (\k _ -> k `Set.member` ins) utxo
+
+-- |Domain exclusion
+--
+(/◁) :: Set TxIn -> UTxO -> UTxO
+ins /◁ (UTxO utxo) =
+  UTxO $ Map.filterWithKey (\k _ -> k `Set.notMember` ins) utxo
+
+-- |Combine two collections of UTxO.
+--
+--     * TODO - Should we return 'Maybe UTxO' so that we can return
+-- Nothing when the collections are not disjoint?
+union :: UTxO -> UTxO -> UTxO
+union (UTxO a) (UTxO b) = UTxO $ Map.union a b
+
+-- |Determine the total balance contained in the UTxO.
+balance :: UTxO -> Coin
+balance (UTxO utxo) = foldr addCoins mempty utxo
+  where addCoins (TxOut _ a) b = a <> b

specs/ledger/hs/src/sig/utxo/UTxO.hsig

@@ -0,0 +1,35 @@
+{- |
+Module : Ledger
+Description : General Ledger
+
+This module defines the types and functions for a simple UTxO Ledger
+as specified in /A Simplified Formal Specification of a UTxO Ledger/.
+-}
+
+signature UTxO where
+
+---------------------------------------------------------------------------------
+-- Core UTxO primitives
+---------------------------------------------------------------------------------
+
+-- | An encoded hash of part of the system.
+data Hash
+
+instance Eq Hash
+instance Ord Hash
+instance Show Hash
+
+-- | A unit of value held by a UTxO.
+data Coin
+
+instance Eq Coin
+instance Show Coin
+instance Semigroup Coin
+instance Monoid Coin
+
+-- | Address of a UTxO, used to identify the owner.
+data Addr
+
+instance Eq Addr
+instance Ord Addr
+instance Show Addr