Playground for formal blockchain model

readme.md

Simplistic blockchain spec (playground)

stack ghci --package free --package containers --package mtl --package transformers Dlg.hs

Block.hs

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types            #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE ViewPatterns          #-}

module Block
  ( Block (..)
  , BlockStorage
  , BlkFunc (..)
  , BlkFuncState (..)
  , HasBlock (..)
  , BlockIntegrityVerifier (..)
  , tryApplyFork
  , getUniqueTx
  ) where

import           Control.Exception (assert)
import           Control.Monad     (foldM)
import           Data.Bifunctor    (first, second)
import           Data.Foldable     (find, foldr')
import           Data.Map.Strict   ((\\))
import qualified Data.Map.Strict   as M
import           Data.Maybe        (catMaybes, fromJust, fromMaybe, isJust, isNothing)
import           Data.Monoid       ((<>))
import           Data.Set          (Set)
import qualified Data.Set          as S

import           Util

-------------------------------
-- Block storage
-------------------------------


data Block blockRef tx = Block
  { blkPrev :: Maybe blockRef
  , blkTxs  :: OldestFirst [] tx
  }

getUniqueTx :: forall alt blockRef tx . HasEx tx alt => Block blockRef tx -> Maybe alt
getUniqueTx (unOldestFirst . blkTxs -> txs) = toSingleVal $ catMaybes $ map getEx txs
  where
    toSingleVal (a:[]) = Just a
    toSingleVal _      = Nothing

class HasBlock blockRef tx b where
    getBlock :: b tx -> Block blockRef tx

instance HasBlock blockRef tx (Block blockRef) where
    getBlock = id

newtype BlockWithUndo blockRef undo tx = BWU { unBWU :: (Block blockRef tx, undo) }

instance HasBlock blockRef tx (BlockWithUndo blockRef undo) where
    getBlock = getBlock . fst . unBWU

type BlockContainerD blockRef bdata tx = (blockRef ~> (bdata tx), blockRef)
type BlockContainerM blockRef bdata tx = Maybe (BlockContainerD blockRef bdata tx)

type BlockContainer blockRef tx = BlockContainerM blockRef (Block blockRef) tx
type BlockStorage blockRef undo tx = BlockContainerM blockRef (BlockWithUndo blockRef undo) tx

newtype BlockIntegrityVerifier blockRef tx = BIV { unBIV :: Block blockRef tx -> Bool }

instance Monoid (BlockIntegrityVerifier blockRef tx) where
    mempty = BIV $ const True
    BIV f `mappend` BIV g = BIV $ \blk -> f blk && g blk


data BlkFunc blockRef tx = BF
      { bfBlockRef     :: Block blockRef tx -> blockRef
      , bfBlkVerify    :: BlockIntegrityVerifier blockRef tx -- ^ Block integrity verifier
      , bfIsBetterThan :: forall bdata1 bdata2 . (HasBlock blockRef tx bdata2, HasBlock blockRef tx bdata1)
                            => BlockContainerD blockRef bdata1 tx
                            -> BlockContainerM blockRef bdata2 tx
                            -> Bool -- ^ Compare two chains with common ancestor
      , bfMaxForkDepth :: Int
      }

data BlkFuncState blockRef tx state undo = BFS
      { bfApplyTxs  :: state -> OldestFirst [] tx -> Maybe (state, undo)
      , bfApplyUndo :: state -> undo -> Maybe state
      , bf          :: BlkFunc blockRef tx
      }


-- FIXME TODO actually it's valid to have `bfMaxForkDepth` forks, we might be terribly out of sync with network

-- | Validate block container integrity:
--      a. integrity of each block
--      b. sequencing by prevBlock
validateBlkContainer :: (HasBlock blockRef tx bdata, Ord blockRef) => BlkFunc blockRef tx -> BlockContainerD blockRef bdata tx-> Bool
validateBlkContainer (BF {..}) initContainer = doValidate initContainer
  where
    doValidate (blks, tip) =
        case tip `M.lookup` blks of
          Just (getBlock -> blk) ->
              and [ unBIV bfBlkVerify blk
                  , bfBlockRef blk == tip
                  , maybe True (doValidate . (,) (tip `M.delete` blks)) (blkPrev blk)
                  ]
          _ -> False

blkTipData :: Ord blockRef => BlockContainerD blockRef bdata tx -> bdata tx
blkTipData (blks, tip) = fromMaybe (error "Broken blk container") $ tip `M.lookup` blks

blkOrigin :: (HasBlock blockRef tx bdata, Ord blockRef) => BlockContainerD blockRef bdata tx -> Maybe blockRef
blkOrigin = blkPrev . getBlock . blkTipData . last . unNewestFirst . blkTails . Just

toBdataList :: (HasBlock blockRef tx bdata, Ord blockRef) => BlockContainerM blockRef bdata tx -> NewestFirst [] (bdata tx)
toBdataList = fmap blkTipData . blkTails

blkTails :: (HasBlock blockRef tx bdata, Ord blockRef) => BlockContainerM blockRef bdata tx -> NewestFirst [] (BlockContainerD blockRef bdata tx)
blkTails Nothing = NewestFirst []
blkTails (Just blkC@(blks, tip)) =
        let NewestFirst rest = blkTails nextContainer
            Block {..} = getBlock $ blkTipData blkC
            nextContainer = maybe Nothing ( Just . (,) (tip `M.delete` blks) ) blkPrev
         in NewestFirst $ blkC : rest

blkHeads :: (HasBlock blockRef tx bdata, Ord blockRef) => BlockContainerM blockRef bdata tx -> NewestFirst [] (blockRef, BlockContainerD blockRef bdata tx)
blkHeads initC@(Just (_, topTip)) = NewestFirst $ second (,topTip) <$> loopH mempty tails
  where
    loopH m (tipBC@(_, tip) : tailsRest) = (tip, m') : loopH m' tailsRest
      where
        m' = M.insert tip (blkTipData tipBC) m
    loopH _ []                           = []
    NewestFirst tails = blkTails initC
blkHeads _ = NewestFirst []


-- | Finds LCA of two containers `cont1`, `cont2`
--   Returns `(lca, cont1', cont2')` such that:
--    * `blkOrigin cont1' == blkOrigin cont2' == lca`
--    * `cont1'` and `cont2'` are heads of `cont1`, `cont2` respectively.
findLCA
    :: (HasBlock blockRef tx bdata1, HasBlock blockRef tx bdata2, Ord blockRef)
    => Int
    -> BlockContainerD blockRef bdata1 tx
    -> BlockContainerD blockRef bdata2 tx
    -> Maybe (blockRef, BlockContainerM blockRef bdata1 tx, BlockContainerM blockRef bdata2 tx)
findLCA maxDepth cont1 cont2 = do
    (lca, dropTail lca -> cont2) <- lcaM
    (_, dropTail lca -> cont1) <- find ((==) lca . fst) refs1
    assertOrigin lca cont1 $
      assertOrigin lca cont2 $
      return (lca, cont1, cont2)
  where
    assertOrigin origin = assert . maybe True ((== Just origin) . blkOrigin)

    dropTail tailKey (m, tip)
        | tip == tailKey = Nothing
        | otherwise = Just (M.delete tailKey m, tip)

    lcaM = find (flip S.member refs1Set . fst) refs2
    NewestFirst (take maxDepth -> refs1) = blkHeads (Just cont1)
    refs1Set = S.fromList (fst <$> refs1)
    NewestFirst (take maxDepth -> refs2) = blkHeads (Just cont2)

data ForkVerResult blockRef bdata1 bdata2 tx
  = ApplyFork
      { fvrToApply    :: BlockContainerD blockRef bdata1 tx
      , fvrToRollback :: BlockContainerM blockRef bdata2 tx
      }
  | RejectFork

--  | Competition between block sequences
--     Rules might be arbitrary:
--      - By Chain length
--      - By Difficulty
--     So we encode this check via `bfIsBetterThan`
--      Assumption is each block contains O(1) data assisting in fork comparison
--      Validation of this O(1) information is to be done via `bfBlkVerify`, `bfTxValidator`
verifyFork
    :: (HasBlock blockRef tx bdata1, HasBlock blockRef tx bdata2, Ord blockRef)
    => BlkFunc blockRef tx
    -> BlockContainerM blockRef bdata1 tx
    -> BlockContainerM blockRef bdata2 tx
    -> ForkVerResult blockRef bdata1 bdata2 tx
verifyFork _ Nothing _ = RejectFork
verifyFork bf@(BF {..}) (Just fork) cont
  | not (validateBlkContainer bf fork) = RejectFork
  | isNothing cont
      && isNothing (blkOrigin fork)
      && fork `bfIsBetterThan` cont
      = ApplyFork fork Nothing
  | Just cont_ <- cont
  , Just lcaR@(lca, Just fork', cont') <- findLCA bfMaxForkDepth fork cont_
  , fork' `bfIsBetterThan` cont'
        = ApplyFork fork' cont'
  | otherwise = RejectFork

forkToChangeSet
    :: (Monoid undo, Ord blockRef)
    => BlkFunc blockRef tx
    -> BlockContainer blockRef tx
    -> BlockStorage blockRef undo tx
    -> Maybe (undo, OldestFirst [] (Block blockRef tx))
forkToChangeSet bf@(BF {..}) fork blkStorage =
    case verifyFork bf fork blkStorage of
      RejectFork     -> Nothing
      ApplyFork {..} ->
        let (NewestFirst toRollback) = toBdataList fvrToRollback
            (NewestFirst toApply) = toBdataList (Just fvrToApply)
            undo = mconcat $ map (snd . unBWU) toRollback
         in Just $ (undo,) $ OldestFirst (reverse toApply)

applyBlock
    :: (Monoid undo, Ord blockRef)
    => BlkFuncState blockRef tx state undo
    -> state
    -> BlockStorage blockRef undo tx
    -> Block blockRef tx
    -> Maybe (state, BlockStorage blockRef undo tx)
applyBlock (BFS {..}) state blkStorage blk
    | blkPrev blk == (snd <$> blkStorage) = do
        (state', undo) <- bfApplyTxs state (blkTxs blk)
        let storage = maybe mempty fst blkStorage
            storage' = M.insert (bfBlockRef bf blk) (BWU (blk, undo)) storage
        return (state', Just (storage', bfBlockRef bf blk))

    | otherwise = Nothing

tryApplyFork
    :: (Monoid undo, Ord blockRef)
    => BlkFuncState blockRef tx state undo
    -> BlockContainer blockRef tx
    -> BlockStorage blockRef undo tx
    -> state
    -> Maybe (state, BlockStorage blockRef undo tx)
tryApplyFork bfs@(BFS {..}) fork blkStorage state = do
    (undo, OldestFirst blocks) <- forkToChangeSet bf fork blkStorage
    state' <- bfApplyUndo state undo
    foldM (uncurry $ applyBlock bfs) (state', blkStorage) blocks


-- How to express functionality which shall decide upon inclusion of fork into blockchain?
--

-- For block application we need diff of change a.k.a. undo

-- Can Storage be used to represent whole state?
-- Can Transaction with validator considering only inputs/outputs uniquely represent state change?
--    No.
--    1) We need periodically do some recomputation w/o any actual transactions
--        ^ Block boundary is a transaction? Which inputs to use?
--    2) Validator sometimes would require whole state traversal:
--         * leader computation
--         * update system stake snapshots
-- So we need to think how to restrict access of validator, while allowing it to read needed data.
-- Validator to state ids it needs after considering transaction in O(|tx size|)?
-- And via proofs express this set of ids to be bounded?


--
-- -------------------------
--
-- Also, what's the model of accounting? If Id ~> Value is utxo, we need to maintain accounts somehow. How?
--   ^ This is precisely doing some (Id ~> Value) transition in addition to what's state in transaction.
--     Perhaps it can be expressed via appropriate transaction type? I.e. do a straightforward transition in-memory
-- This is easy, only thing we need to ensure is that each transaction shall be a O(|tx size|) change of state
--
-- But Block boundary tx can not always be processed in O(|tx size|)!
-- We may do more elaborate analysis per tx type and explicitly distinguish transactions for block boundaries for blocks `8k`, `10k` (or few other interesting blocks)

Dlg.hs

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}

module Dlg where

import           Control.Monad.Except (ExceptT, catchError, throwError)
import           Data.Bool            (bool)
import           Data.Foldable        (null, toList)
import qualified Data.Map.Strict      as M
import           Data.Maybe           (fromMaybe)
import           Data.Monoid          ((<>))
import           Data.Proxy           (Proxy (..))
import           Data.Ratio           (Ratio)
import           Data.Set             (Set)
import qualified Data.Set             as S

import           Pos                  (StakeConfiguration (..))
import           State                (StatePComputation, Tx (..), Validator (..),
                                       invalidate, queryP, queryPOne, stateCompOneOfManyE,
                                       validate)
import           Util

data LightDlgCert stId signature =
  LightDlgCert
    { ldcIssuer    :: stId
    , ldcSignature :: signature -- ^ Signature of delegate id by issuer
    -- , ldcCounter :: Int
    }

-- TODO define modifier for chain selection function (after counter)

newtype LightDlgToSign stId = LightDlgToSign stId

lightDelegationStakeConf
  :: forall stId time signature id proof value .
   ( Eq stId
   , Signable stId signature (LightDlgToSign stId)
   , HasEx proof (LightDlgCert stId signature)
   )
  => Proxy (stId, signature)
  -> StakeConfiguration id proof value stId time
  -> StakeConfiguration id proof value stId time
lightDelegationStakeConf _ (StakeConfiguration {..}) = StakeConfiguration scGetStake eligible'
  where
    getData = getEx @proof @(LightDlgCert stId signature)

    eligible' time delegate proof =
        case getData proof of
          Just (LightDlgCert issuer sig) ->
            bool invalidate (eligibleCheckDo issuer) $
                issuer /= delegate && verify issuer (LightDlgToSign delegate) sig
          _ -> eligibleCheckDo delegate
      where
        eligibleCheckDo st = scEligibleToForge time st proof

data HeavyDlgCert stId signature =
    HeavyDlgCert
      { hdcIssuer   :: stId
      , hdcDelegate :: Maybe stId
      -- , hdcCounter  :: time
      -- , hdcSignature :: signature -- ^ Signature of delegate id by issuer
      }

newtype HeavyDlgToSign stId = HeavyDlgToSign (Maybe stId)

data HeavyDlgCertId = HeavyDlgIssuersId | HeavyDlgDelegateId
  deriving Enum

data HeavyDlgTxId = HeavyDlgTxId

newtype HeavyDlgCertProof signature = HeavyDlgCertProof signature

-- Virtual state of delegation:
-- data DelegationState stId = DelegationState
--     { dsIssuers  :: stId ~> Set stId
--     , dsDelegate :: stId ~> stId
--     }

heavyDelegationStakeConf
  :: forall ids stId time signature id proof value .
   ( Ord stId
   , IdStorage ids HeavyDlgCertId
   , Ord id
   , HasAlt id stId
   , HasEx value (Set stId)
   )
  => Proxy (stId, signature, ids)
  -> StakeConfiguration id proof value stId time
  -> StakeConfiguration id proof value stId time
heavyDelegationStakeConf _ (StakeConfiguration {..}) = StakeConfiguration scGetStake eligible'
  where
    issuersId = getId (Proxy @ids) HeavyDlgIssuersId
    eligible' time delegate proof =
        queryPOne issuersId delegate >>= maybe (eligibleCheckDo delegate) (stateCompOneOfManyE . map eligibleCheckDo . S.toList)
      where
        eligibleCheckDo st = scEligibleToForge time st proof

heavyDlgValidator
  :: forall ids txIds stId signature id proof value .
   ( HasEx proof (HeavyDlgCertProof signature)
   , HasAlt id stId
   , HasEx value (Set stId)
   , HasEx value stId
   , Ord id
   , Ord stId
   -- ^ Constraint is `Has` and not `HasEx`, proposing that there shall be other validator for same tx to actually process it
   , IdStorage txIds HeavyDlgTxId
   , IdStorage ids HeavyDlgCertId
   , Signable stId signature (HeavyDlgToSign stId)
   )
  => Proxy (stId, signature, ids, txIds)
  -> Int
  -> Validator id proof value
heavyDlgValidator _ maxDlgDepth =
    Validator (S.singleton heavyDlgTxId) $ \Tx{..} ->
        case getData txProof of
          Just (HeavyDlgCertProof sig) ->
              validateDo sig txBody
          _ -> invalidate
  where
    getData = getEx @proof @(HeavyDlgCertProof signature)
    heavyDlgTxId = getId (Proxy @txIds) HeavyDlgTxId

    validateDo :: signature -> ChangeSet id value -> ExceptT () (StatePComputation id value) ()
    validateDo sig body
        | Just issuerCS <- issuerCS'
        , Just delegateCS <- delegateCS'
        , M.null $ M.delete issuersId $ M.delete delegateId $ byId
        , Right (issuer, newDelegateM) <- checkDelegates sig delegateCS
        , Right (oldDelegateM, stateCheckIds, stateCheckVals) <- checkIssuers issuer newDelegateM issuerCS
        , maybe True (\oldDlg -> dpRemove delegateCS == S.singleton oldDlg) oldDelegateM
            = validateStateDelegates issuer oldDelegateM <> validateStateIssuers stateCheckIds stateCheckVals
              <> maybe mempty (validateNewTree maxDlgDepth issuer) newDelegateM
        | otherwise
            = invalidate
      where
        byId :: Int ~> ChangeSet' id value
        byId = splitByPrefix body

        issuerCS' = getEx $ fromMaybe mempty $ issuersId `M.lookup` byId
        delegateCS' = getEx $ fromMaybe mempty $ delegateId `M.lookup` byId

    issuersId = getId (Proxy @ids) HeavyDlgIssuersId
    delegateId = getId (Proxy @ids) HeavyDlgDelegateId

    guard e = bool (throwError ()) (pure ())

    validateStateDelegates issuer oldDelegateM =
        queryPOne delegateId issuer
            >>= guard () . (==oldDelegateM) -- TODO throw meaningful error

    validateStateIssuers ids vals =
        queryP issuersId ids >>= guard () . ((==vals) . (∩ toDummyMap ids)) -- TODO throw meaningful error

    validateNewTree 0 _ _                           = invalidate
    validateNewTree depthCounter issuer newDelegate =
        queryPOne delegateId newDelegate >>= \case
          Just prev -> if prev == issuer
                           then invalidate
                           else validateNewTree (depthCounter - 1) issuer prev
          _ -> validate


    checkDelegates :: signature -> ChangeSet' stId stId -> Either () (stId, Maybe stId)
    checkDelegates sig (ChangeSet {..})
      | M.null dpAdd
      , [ issuer ] <- S.toList dpRemove
      , verify issuer (HeavyDlgToSign (Nothing :: Maybe stId)) sig
        = Right (issuer, Nothing)

      | [(issuer, newDelegate)] <- M.toList dpAdd
      , newDelegate /= issuer
      , S.null dpRemove || S.singleton issuer == dpRemove
      , verify issuer (HeavyDlgToSign $ Just newDelegate) sig
        = Right (issuer, Just newDelegate)

      | otherwise = Left ()

    -- Issuer validation cases:
    --  Ia. Delegation certificate, no previous delegation existed, new delegate had no issuers
    --  Ib. Delegation certificate, no previous delegation existed, new delegate had issuers
    --  Ic. Delegation certificate, previous delegation existed, previous delegate had single issuer, new delegate had no issuers
    --  Ie. Delegation certificate, previous delegation existed, previous delegate had single issuer, new delegate had issuers
    --  Id. Delegation certificate, previous delegation existed, previous delegate had > 1 issuers, new delegate had no issuers
    --  If. Delegation certificate, previous delegation existed, previous delegate had > 1 issuers, new delegate had issuers
    --  IIa. Revoke certificate, delegate had > 1 issuers on his behalf
    --  IIb. Revoke certificate, delegate had single issuer on his behalf

    checkIssuers :: stId -> Maybe stId -> ChangeSet' stId (Set stId) -> Either () (Maybe stId, Set stId, stId ~> Set stId)
    checkIssuers issuer (Just newDelegate) (ChangeSet issuersAdd issuersRemove)
        --  Ia. Delegation certificate, no previous delegation existed, new delegate had no issuers
        --    dpRemove = [], dpAdd = [ (newDelegate, [ issuer ] ) ]
        --    Check in state: [ newDelegate ] -> []
        | S.null issuersRemove
        , M.singleton newDelegate (S.singleton issuer) == issuersAdd
            = Right (Nothing, S.singleton newDelegate, mempty)

        --  Ib. Delegation certificate, no previous delegation existed, new delegate had issuers
        --    dpRemove = [ newDelegate ], dpAdd = [ (newDelegate, newDelegateV ) ]
        --      (issuer ∈ newDelegateV, (newDelegateV \ { issuer }) non-empty)
        --    Check in state: [ newDelegate ] -> [ (newDelegate, newDelegateV \ { issuer }) ]
        | checkSize1 issuersRemove
        , newDelegate `S.member` issuersRemove
        , Just newDelegateV <- newDelegate `M.lookup` issuersAdd
        , checkSize1 issuersAdd
        , issuer `S.member` newDelegateV
        , checkSizeMore1 newDelegateV
            = Right (Nothing, S.singleton newDelegate, M.singleton newDelegate $ S.delete issuer newDelegateV)

        --  Ic. Delegation certificate, previous delegation existed, previous delegate had single issuer, new delegate had no issuers
        --    dpRemove = [ oldDelegate ], dpAdd = [ (newDelegate, [ issuer ] ) ]
        --    Check in state: [ newDelegate, oldDelegate ] -> [ (oldDelegate, { issuer } ) ]
        | [ oldDelegate ] <- S.toList issuersRemove
        , oldDelegate /= newDelegate
        , M.singleton newDelegate (S.singleton issuer) == issuersAdd
            = Right (Just oldDelegate, S.fromList [ newDelegate, oldDelegate ], M.singleton oldDelegate $ S.singleton issuer)

        --  Ie. Delegation certificate, previous delegation existed, previous delegate had single issuer, new delegate had issuers
        --    dpRemove = [ oldDelegate, newDelegate ], dpAdd = [ (newDelegate, newDelegateV ) ]
        --      (issuer ∈ newDelegateV, (newDelegateV \ { issuer }) non-empty)
        --    Check in state: [ newDelegate, oldDelegate ] -> [ (newDelegate, newDelegateV \ { issuer }), (oldDelegate, { issuer } ) ]
        | newDelegate `S.member` issuersRemove
        , [ oldDelegate ] <- S.toList (newDelegate `S.delete` issuersRemove)
        , oldDelegate /= newDelegate
        , Just newDelegateV <- newDelegate `M.lookup` issuersAdd
        , checkSize1 issuersAdd
        , issuer `S.member` newDelegateV
        , checkSizeMore1 newDelegateV
            = Right (Just oldDelegate, S.fromList [ newDelegate, oldDelegate ], M.fromList [ (oldDelegate, S.singleton issuer), (newDelegate, S.delete issuer newDelegateV) ] )

        --  Id. Delegation certificate, previous delegation existed, previous delegate had > 1 issuers, new delegate had no issuers
        --    dpRemove = [ oldDelegate ], dpAdd = [ (newDelegate, [ issuer ] ), (oldDelegate, oldDelegateV) ]
        --      (issuer ∉ oldDelegateV, oldDelegateV non-empty)
        --    Check in state: [ newDelegate, oldDelegate ] -> [ (oldDelegate, oldDelegateV ∪ { issuer } ) ]
        | [ oldDelegate ] <- S.toList issuersRemove
        , oldDelegate /= newDelegate
        , M.singleton newDelegate (S.singleton issuer) == oldDelegate `M.delete` issuersAdd
        , Just oldDelegateV <- oldDelegate `M.lookup` issuersAdd
        , not (issuer `S.member` oldDelegateV)
        , not (S.null oldDelegateV)
            = Right (Just oldDelegate, S.fromList [ newDelegate, oldDelegate ], M.singleton oldDelegate (S.insert issuer oldDelegateV))

        --  If. Delegation certificate, previous delegation existed, previous delegate had > 1 issuers, new delegate had issuers
        --    dpRemove = [ oldDelegate, newDelegate ], dpAdd = [ (newDelegate, newDelegateV ), (oldDelegate, oldDelegateV) ]
        --      (issuer ∈ newDelegateV, (newDelegateV \ { issuer }) non-empty, issuer ∉ oldDelegateV, oldDelegateV non-empty)
        --    Check in state: [ newDelegate, oldDelegate ] -> [ (newDelegate, newDelegateV \ { issuer }), (oldDelegate, oldDelegateV ∪ { issuer } ) ]
        | newDelegate `S.member` issuersRemove
        , [ oldDelegate ] <- S.toList (newDelegate `S.delete` issuersRemove)
        , oldDelegate /= newDelegate
        , Just newDelegateV <- newDelegate `M.lookup` issuersAdd
        , Just oldDelegateV <- oldDelegate `M.lookup` issuersAdd
        , checkSize2 issuersAdd
        , issuer `S.member` newDelegateV
        , checkSizeMore1 newDelegateV
        , not (issuer `S.member` oldDelegateV)
        , not (S.null oldDelegateV)
            = Right (Just oldDelegate, S.fromList [ newDelegate, oldDelegate ], M.fromList [ (oldDelegate, S.insert issuer oldDelegateV), (newDelegate, S.delete issuer newDelegateV) ] )

        | otherwise = Left ()
      where
        checkSize1 s
            | _:[] <- toList s = True
            | otherwise = False
        checkSize2 s
            | _:_:[] <- toList s = True
            | otherwise = False
        checkSizeMore1 s
            | _:_:_ <- toList s = True
            | otherwise = False

    -- II. Revoke certificate check
    checkIssuers issuer _ (ChangeSet issuersAdd issuersRemove)
      | [ oldDelegate ] <- S.toList issuersRemove
      , [ (oldDelegate, oldDelegateV) ] <- M.toList issuersAdd
      , not (S.null oldDelegateV)
      , not (S.member issuer oldDelegateV)
        --  IIa. Revoke certificate, delegate had > 1 issuers on his behalf
        --    dpRemove = [ oldDelegate ], dpAdd = [ (oldDelegate, oldDelegateV' ) ]
        --      (issuer ∉ oldDelegateV', oldDelegateV' non-empty)
        --    Check in state: [ oldDelegate ] -> [ (oldDelegate, oldDelegateV' ∪ { issuer } ) ]
        = Right (Just oldDelegate, S.singleton oldDelegate, M.singleton oldDelegate $ S.insert issuer oldDelegateV)

      | [ oldDelegate ] <- S.toList issuersRemove
      , M.null issuersAdd
        --  IIb. Revoke certificate, delegate had single issuer on his behalf
        --    dpRemove = [ oldDelegate ], dpAdd = []
        --    Check in state: [ oldDelegate ] -> [ (oldDelegate, { issuer } ) ]
        = Right (Just oldDelegate, S.singleton oldDelegate, M.singleton oldDelegate $ S.singleton issuer)

      | otherwise = Left ()

Pos.hs

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE ViewPatterns          #-}

module Pos where

import           Control.Monad.Except (ExceptT)
import qualified Data.Map             as M
import           Data.Proxy           (Proxy (..))
import           Data.Ratio           (Ratio)
import qualified Data.Set             as S

import           Block                (Block, BlockIntegrityVerifier (..), getUniqueTx)
import           State                (StatePComputation, Tx (..), Validator (..),
                                       invalidate, validate)
import           Util

data StakeConfiguration id proof value stId time = StakeConfiguration
    { scGetStake        :: stId -> StatePComputation id value (Ratio Int)
    , scEligibleToForge :: time -> stId -> proof -> ExceptT () (StatePComputation id value) ()
    }

newtype BlkSignature stId signature = BlkSignature (stId, signature)

stakeBlkVerifier
  :: forall stId time signature blockRef tx .
   ( HasEx tx (BlkSignature stId signature)
   , Signable stId signature (Block blockRef tx)
   )
  => Proxy (stId, signature)
  -> BlockIntegrityVerifier blockRef tx
stakeBlkVerifier _ = BIV $ \blk ->
    case getUniqueTx @(BlkSignature stId signature) blk of
      Just (BlkSignature (stId, signature)) -> verify stId blk signature
      _                                     -> False

stakeValidator
  :: forall stId time signature id proof value .
   ( Has proof (Maybe (BlkSignature stId signature))
   -- ^ Constraint is `Has` and not `HasEx`, proposing that there shall be other validator for same tx to actually process it
   -- , IdStorage txIds BlkSigTxId
   )
  => Proxy (stId, signature)
  -> StakeConfiguration id proof value stId time
  -> time
  -> Validator id proof value
stakeValidator _ (scEligibleToForge -> eligible) time =
    Validator mempty $ \Tx {..} -> -- TODO extend validator to filter by txId without marking txId as checked (instead of `mempty`)
        case getData txProof of
          Just (BlkSignature (stId, _)) ->
            eligible time stId txProof
          _ -> validate
  where
    getData = get @proof @(Maybe (BlkSignature stId signature))
    -- blkSigTxId = getId (Proxy @txIds) BlkSigTxId

State.hs

{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE ViewPatterns               #-}

module State
  ( ReqIter (..)
  , StateComputation
  , StatePComputation
  , Validator (..)
  , StateP
  , Tx (..)
  , Undo
  , validate
  , validateIff
  , invalidate
  , query
  , queryP
  , queryPOne
  , stateCompOneOf
  , stateCompOneOfMany
  , stateCompOneOfManyE

  , inputsExist
  , propsPass

  , applyTx
  , applyTxs
  , applyUndo
  )
  where

import           Control.Applicative       (liftA2)
import           Control.Exception         (assert)
import           Control.Monad             (foldM)
import           Control.Monad.Except      (ExceptT (..), runExceptT, throwError)
import           Control.Monad.Free        (Free (..))
import qualified Control.Monad.Free        as F
import           Control.Monad.Trans.Class (lift)
import           Data.Bifunctor            (bimap, first, second)
import           Data.Bool                 (bool)
import           Data.Foldable             (find)
import           Data.Map.Strict           ((\\))
import qualified Data.Map.Strict           as M
import           Data.Maybe                (catMaybes, fromJust, fromMaybe, isJust,
                                            isNothing)
import           Data.Monoid               ((<>))
import           Data.Set                  (Set)
import qualified Data.Set                  as S

import           Util

------------------------------------------
-- Basic storage: model
------------------------------------------

type StateP id value = Prefixed id ~> value -- Portion of state

type Undo id value = ChangeSet id value

data Tx id proof value = Tx
    { txType  :: Int
    , txProof :: proof
    , txBody  :: ChangeSet id value
    }


-- Emulation of dependent type
-- Assumption: `txType` allows one to identify concrete types for `id`, `proof`, `value`
-- Validators try to do conversion from abstract type to particular types
-- Validator is associated with set of `txType`s
-- There shall be at least one validator for each `txType`

instance (Ord id1, HasEx id id1, HasEx value value1, HasEx proof proof1)
         => HasEx (Tx id proof value) (Tx id1 proof1 value1) where
  getEx (Tx {..}) = Tx txType <$> getEx txProof <*> getEx txBody

newtype ReqIter req resp res = ReqIter (req, resp -> res)
  deriving (Functor, Monoid)

-- | State computation which allows you to query for part of bigger state
-- and build computation considering returned result.
--
-- Note, response might contain more records than were requested in `req`
-- (because of monoidal gluing of many computations)
type StateComputation req resp = Free (ReqIter req resp)

query :: req -> StateComputation req resp resp
query req = Free $ ReqIter (req, pure)

hoistStateComp
  :: (req1 -> req2)
  -> (resp2 -> resp1)
  -> StateComputation req1 resp1 a
  -> StateComputation req2 resp2 a
hoistStateComp f g =
    F.hoistFree $ \(ReqIter (req1, f1)) ->
      let req2 = f req1
          f2 = \resp2 -> f1 (g resp2)
       in ReqIter (req2, f2)

-- hoistStateCompWithIds
--   :: Int ~>

type StatePComputation id value = StateComputation (PFilter id) (StateP id value)

-- TODO Not Exist shall be different error from getEx Left ()
queryPOne
  :: forall id id' value value' .
     (Ord id, Ord id', HasAlt id id', HasEx value value')
  => Int -> id' -> ExceptT () (StatePComputation id value) (Maybe value')
queryPOne prefix id' = M.lookup id' <$> queryP prefix (S.singleton id')

queryP
  :: forall id id' value value' .
     (Ord id, Ord id', HasAlt id id', HasEx value value')
  => Int -> Set id' -> ExceptT () (StatePComputation id value) (id' ~> value')
queryP prefix ids' = ExceptT $
    maybe (Left ()) (Right . fKeys) . getEx <$> query idFilter
  where
    idConv :: id' -> Prefixed id
    idConv = (,) prefix . mkAlt

    fKeys :: (Int, id') ~> value' -> id' ~> value'
    fKeys m = M.fromList $ first snd <$> M.toList m

    idFilter :: PFilter id
    idFilter = PFilter (S.fromList $ map idConv $ S.toList ids') mempty

-- | Tx validator: set of txTypes and validation function
-- Validator with empty set of txTypes is assumed to be tx type agnostic
data Validator id proof value = Validator (Set Int) (Tx id proof value -> ExceptT () (StatePComputation id value) ())

-- TODO use these types instead:
-- data TxValidationType res = ValidatesTx res | ConsidersTx res | IgnoresTx
-- newtype Validator id proof value = Validator (Tx id proof value -> TxValidationType (ExceptT () (StateComputation id value) ()))

instance Ord id => Monoid (Validator id proof value) where
    mempty = Validator mempty mempty
    mappend (Validator ids1 f1) (Validator ids2 f2) =
        Validator (ids1 <> ids2) $ \tx -> f (txType tx `S.member` ids1) (txType tx `S.member` ids2) tx
      where
        f False False = mempty
        f True False  = f1
        f False True  = f2
        f _ _         = \tx -> f1 tx <> f2 tx

stateCompOneOfManyE :: Monoid req => [ExceptT e (StateComputation req resp) a] -> ExceptT e (StateComputation req resp) a
stateCompOneOfManyE = ExceptT . stateCompOneOfMany . map runExceptT

stateCompOneOfMany :: Monoid req => [StateComputation req resp (Either e a)] -> StateComputation req resp (Either e a)
stateCompOneOfMany = foldr1 stateCompOneOf

stateCompOneOf :: Monoid req => StateComputation req resp (Either e a) -> StateComputation req resp (Either e a) -> StateComputation req resp (Either e a)
stateCompOneOf (Pure l@(Left _)) r = r
stateCompOneOf r (Pure l@(Left _)) = r
stateCompOneOf (Pure x) _                = Pure x
stateCompOneOf _ (Pure y)                = Pure y

stateCompOneOf (Free (ReqIter (req1, cont1))) (Free (ReqIter (req2, cont2)))       = Free $ ReqIter (req1 <> req2, \resp -> cont1 resp `stateCompOneOf` cont2 resp)

-- | Short-circuit Monoid instance for validator base
instance (Monoid a, Monoid req) => Monoid (ExceptT e (StateComputation req resp) a) where
    mempty = pure mempty
    mappend (ExceptT a) (ExceptT b) = ExceptT $ a <> b

-- | Short-circuit Monoid instance for validator base
instance (Monoid a, Monoid req) => Monoid (StateComputation req resp (Either e a)) where
    mempty = Pure $ Right mempty

    mappend l@(Pure (Left _)) _    = l
    mappend _ l@(Pure (Left _))    = l
    mappend (Pure (Right x)) (Pure (Right y)) = Pure $ Right $ x <> y

    mappend (Pure (Right x)) (Free (ReqIter (yReq, yF))) =
        Free $ ReqIter $ (yReq, \resp -> fmap (x <>) <$> yF resp)

    mappend (Free (ReqIter (xReq, xF))) (Pure (Right y)) =
        Free $ ReqIter $ (xReq, \resp -> fmap (<> y) <$> xF resp)

    mappend (Free xR) (Free yR) = Free $ xR <> yR

validate :: Monoid a => ExceptT () (Free f) a
validate = ExceptT $ Pure $ Right mempty

validateIff :: Monoid a => Bool -> ExceptT () (Free f) a
validateIff = bool invalidate validate

invalidate :: ExceptT () (Free f) a
invalidate = ExceptT $ Pure $ Left ()

---------------------------
-- Example validators
--------------------------

inputsExist :: Ord id => Validator id proof value
inputsExist = Validator mempty $ \(dpRemove . txBody -> inRefs) -> do
    ins <- lift $ query $ idsPFilter inRefs
    validateIff $ all (flip M.member ins) inRefs

propsPass :: Ord id => Validator id proof (proof -> Bool, value)
propsPass = Validator mempty $ \tx -> do
    let inRefs = dpRemove $ txBody tx
        proof = txProof tx
    ins <- lift $ query $ idsPFilter inRefs
    validateIff $ all (($ proof) . fst) ins

combinedValidator :: Ord id => Validator id proof (proof -> Bool, value)
combinedValidator = inputsExist <> propsPass

------------------------------------------------------
-- Basic storage: implementation with in-memory state
------------------------------------------------------

simpleStateAccessor :: (Monoid id, Ord id) => StateP id value -> ReqIter (PFilter id) (StateP id value) res -> res
simpleStateAccessor state (ReqIter (query, cont)) = cont $ query `applyFilterToMap` state

-- | Applies txs to state
applyUndo :: (Monoid id, Ord id)
         => StateP id value
         -> Undo id value
         -> Maybe (StateP id value)
applyUndo state undo = fst <$> undo `applyDiff` state

-- | Applies txs to state
applyTx :: (Monoid id, Ord id)
         => Validator id proof value
         -> StateP id value
         -> Tx id proof value
         -> Maybe (StateP id value, Undo id value)
applyTx (Validator txTypes txValidator) state tx
  | txType tx `S.member` txTypes
    = case F.iter (simpleStateAccessor state) $ runExceptT $ txValidator tx of
        Right () -> txBody tx `applyDiff` state
        _        -> Nothing
  | otherwise = Nothing

-- TODO rewrite applyTxs as StateComputation with (Maybe (StateP id value, Undo id value)) return value
-- This will allow to implement applyTxs :: [[Tx]] -> [Undo]
-- Which would be a badass

-- | Applies txs to state
applyTxs :: (Monoid id, Ord id)
         => Validator id proof value
         -> StateP id value
         -> OldestFirst [] (Tx id proof value)
         -> Maybe (StateP id value, Undo id value)
applyTxs txValidator initState = flip foldM (initState, mempty) $
  \(state, undoAccum) tx -> do
      (state', undo) <- applyTx txValidator state tx
      return (state', undoAccum <> undo)
  -- TODO Implementation with real db is planned to be much more effective
  -- Idea is that validation may be fused (thus be executed for whole bunch of
  -- operations in just few steps, depending on max depth of Free).
  -- And then whole pack of txs applied as single atomic change.
  -- Note, to correctly fuse validation you need to modify response of subsequent
  -- query with transactions preceeding current tx in pack.

Util.hs

{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeOperators              #-}

module Util where

import           Data.Bifunctor  (bimap)
import           Data.Bool       (bool)
import           Data.Foldable   (find, foldr')
import           Data.Map.Strict ((\\))
import qualified Data.Map.Strict as M
import           Data.Maybe      (catMaybes, isJust, isNothing)
import           Data.Monoid     ((<>))
import           Data.Proxy      (Proxy)
import           Data.Set        (Set)
import qualified Data.Set        as S

type (~>) a b = M.Map a b
infixr 8 ~>

(∩) :: Ord k => k ~> a -> k ~> b -> k ~> a
(∩) = M.intersection
infixr 8 ∩

(∪) :: Ord k => k ~> a -> k ~> a -> k ~> a
(∪) = M.union

type Prefixed id = (Int, id)
data PFilter id = PFilter
    { includeIds      :: Set (Prefixed id)
    , includePrefixes :: Set Int
    }

idsPFilter :: Set (Prefixed id) -> PFilter id
idsPFilter = flip PFilter mempty

-- TODO PFilter AND/OR algebra

instance Ord id => Monoid (PFilter id) where
    mempty = PFilter mempty mempty
    (PFilter ids1 prefixes1)
      `mappend` (PFilter ids2 prefixes2)
         = PFilter (ids1 <> ids2) (prefixes1 <> prefixes2)

newtype OldestFirst b a = OldestFirst { unOldestFirst :: b a }
deriving instance Foldable b => Foldable (OldestFirst b)
deriving instance Functor b => Functor (OldestFirst b)

newtype NewestFirst b a = NewestFirst { unNewestFirst :: b a }
deriving instance Foldable b => Foldable (NewestFirst b)
deriving instance Functor b => Functor (NewestFirst b)

toDummyMap :: Set a -> (a ~> ())
toDummyMap = M.fromSet (const ())

filterWithPrefix :: (Ord id, Monoid id) => Int -> Prefixed id ~> v -> Prefixed id ~> v
filterWithPrefix prefix m = maybe gtPl (\v -> M.insert (prefix, mempty) v gtPl) eqP
  where
    (_, eqP, gtP) = (prefix, mempty) `M.splitLookup` m
    (gtPl, _, _) = (succ prefix, mempty) `M.splitLookup` gtP

applyFilterToMap :: (Ord id, Monoid id) => PFilter id -> Prefixed id ~> v -> Prefixed id ~> v
applyFilterToMap (PFilter ids prefixes) m = foldr' M.union mempty maps
  where
    maps = (m ∩ toDummyMap ids)
              : map (flip filterWithPrefix m) (S.toList prefixes)

data ChangeSetBase id v = ChangeSet
    { dpAdd    :: id ~> v
    , dpRemove :: Set id
    }

type ChangeSet id = ChangeSetBase (Prefixed id)
type ChangeSet' id = ChangeSetBase id

splitByPrefix :: forall id v . Ord id => ChangeSet id v -> Int ~> ChangeSet' id v
splitByPrefix initCS = flip (M.foldrWithKey g) (dpAdd initCS) $ foldr' f mempty (dpRemove initCS)
  where
    f :: Prefixed id -> Int ~> ChangeSet' id v -> Int ~> ChangeSet' id v
    f (p, i) m = modifyPrefix p m $ \cs -> cs { dpRemove = S.insert i $ dpRemove cs }

    g :: Prefixed id -> v -> Int ~> ChangeSet' id v -> Int ~> ChangeSet' id v
    g (p, i) v m = modifyPrefix p m $ \cs -> cs { dpAdd = M.insert i v $ dpAdd cs }

    modifyPrefix :: Int -> Int ~> ChangeSet' id v -> (ChangeSet' id v -> ChangeSet' id v) -> Int ~> ChangeSet' id v
    modifyPrefix p m f = if M.member p m
                            then M.adjust f p m
                            else M.insert p (f mempty) m

dpIsEmpty :: ChangeSet id v -> Bool
dpIsEmpty (ChangeSet {..}) = M.null dpAdd && S.null dpRemove

-- TODO in future ChangeSet necessarily will need to be refined to allow for no-context
-- construction of txs modifying some value (not deleting and adding)
-- ChangeSet = { dpAdd , dpModify :: Prefixed id ~> (Maybe v -> Maybe v), dpRemove },
--  dpAdd ∩ dpRemove = mempty, dpRemove ∩ dpModify = mempty, dpAdd ∩ dpModify = mempty

instance Ord id => Monoid (ChangeSetBase id v) where
    mempty = ChangeSet mempty mempty
    (ChangeSet { dpAdd = a1, dpRemove = r1 })
      `mappend` (ChangeSet { dpAdd = a2, dpRemove = r2 })
        = ChangeSet { .. }
      where
        dpAdd = (a1 \\ toDummyMap r2) <> a2
        dpRemove = (r1 S.\\ M.keysSet a2) <> r2

applyDiff :: (Monoid id, Ord id) => ChangeSet id v -> Prefixed id ~> v -> Maybe (Prefixed id ~> v, ChangeSet id v)
applyDiff (ChangeSet {..}) m
    | M.keysSet forRemove == dpRemove
    , M.null (m' ∩ dpAdd)
      = Just (m' ∪ dpAdd, undo)

    | otherwise = Nothing

  where
    forRemove = m ∩ toDummyMap dpRemove
    m' = m \\ forRemove
    undo = ChangeSet { dpAdd = forRemove, dpRemove = M.keysSet m }

data VerificationRes
    = VerSuccess
    | VerFailure ()
  deriving (Eq)

isVerSuccess :: VerificationRes -> Bool
isVerSuccess VerSuccess = True
isVerSuccess _          = False

isVerFailure :: VerificationRes -> Bool
isVerFailure (VerFailure _) = True
isVerFailure _              = False

boolToVer :: Bool -> VerificationRes
boolToVer = bool (VerFailure ()) VerSuccess

instance Monoid VerificationRes where
    mempty = VerSuccess
    VerSuccess `mappend` a = a
    a `mappend` VerSuccess = a
    VerFailure xs `mappend` VerFailure ys = VerFailure $ xs `mappend` ys

-- | HasAlt laws:
--  * getEx . mkAlt = Just
--  * fmap mkAlt . getEx = Just
class HasEx b a => HasAlt b a where
    mkAlt :: a -> b

instance (HasEx a a', HasEx b b') => HasEx (a, b) (a', b') where
    getEx (a, b) = (,) <$> getEx a <*> getEx b

instance (HasAlt a a', HasAlt b b') => HasAlt (a, b) (a', b') where
    mkAlt (a', b') = (mkAlt a', mkAlt b')

class Signable stId signature a | signature -> stId where
    sign :: stId -> a -> signature
    verify :: stId -> a -> signature -> Bool

-- | HasEx class
-- Extracts `a` from `b` only if `a` contains no more data but extracted
-- (i.e. original `b` can be recreated with only `a`)
class HasEx b a where
    getEx :: b -> Maybe a

instance HasEx Int Int where
    getEx = Just

instance (Ord id1, HasEx id id1) => HasEx (Set id) (Set id1) where
  getEx vals
      | isJust (find isNothing valsM)
          = Nothing -- TODO after we have more sensitive errors,
                    -- have one error for "unexpected entry {..} in set"
      | otherwise
          = Just $ S.fromList $ catMaybes valsM
    where
      valsM = getEx <$> S.toList vals

instance (Ord id1, HasEx id id1, HasEx value value1) => HasEx (id ~> value) (id1 ~> value1) where
  getEx vals
      | isJust (find isNothing valsM)
          = Nothing -- TODO after we have more sensitive errors,
                    -- have one error for "id returned unexpected value" and one for "unexpected id"
      | otherwise
          = Just $ M.fromList $ catMaybes valsM
    where
      fPair :: Applicative f => (f a, f b) -> f (a, b)
      fPair (fa, fb) = (,) <$> fa <*> fb

      valsM = fPair . bimap getEx getEx <$> M.toList vals

instance forall id value id1 value1 . (Ord id1, HasEx id id1, HasEx value value1) => HasEx (ChangeSetBase id value) (ChangeSetBase id1 value1) where
    getEx (ChangeSet {..}) = ChangeSet <$> getEx dpAdd <*> getEx dpRemove

class (HasAlt b a, Enum b) => IdStorage b a

getId :: forall ids i . IdStorage ids i => Proxy ids -> i -> Int
getId _ i = fromEnum (mkAlt i :: ids)

class Has b a where
    get :: b -> a