{- |
Module      : Singular.Registry.FoldSelection
Description : Pure fold selection over pending requests (#518)
License     : Apache-2.0

Pull request 1 of #518 judges every pending request alone and settles one
per fold. This module is the pure selection: it takes the pending requests,
the live facts, the clock and a capacity bound as arguments and returns, for
every pending request, exactly one of settled or excluded-with-reason. It
reads no file, no clock and no provider, and imports no command-line module
and no application module, so both the command line and the conformance suite
can use it.

The seven checks run in the spec's order; the first one a request fails
names its reason:

1. it decodes as a request, otherwise @undecodable@
2. its edge is one the model admits, otherwise @edge-inadmissible@
3. its processing window is open beyond the fold margin, otherwise
   @window-closed@
4. the model's approval check accepts it, otherwise @no-approval@ or
   @approval-mismatch@
5. the model's leaf check accepts it from the live state, otherwise
   @key-exists@, @token-missing@, @key-unknown@, @not-booked@ or
   @terminal-immutable@
6. the application step's verdict carried on the request is ready, otherwise
   @application-datum-unreadable@ or @application-required@
7. no earlier included request names the same key, otherwise @key-in-batch@

Requests that pass all seven keep ledger input order; the first ones up to
the capacity bound are settled and each remaining one is named @capacity@.
The window rule mirrors the command line's processing-window rule: open
only while the time left is beyond the margin. The approval and leaf checks
follow the model's refusal order: excluded edges first, then approval, then
the leaf from the live state.
-}
module Singular.Registry.FoldSelection
    ( EdgeKind (..)
    , Leaf (..)
    , ApprovalCheck (..)
    , AppVerdict (..)
    , PendingRequest (..)
    , SelectedRequest (..)
    , Reason (..)
    , Exclusion (..)
    , Selection (..)
    , LiveFacts
    , selectFold
    , judgeAlone
    , foldCapacity
    , foldCapacityProvenance
    , exclusionName
    , exclusionSource
    ) where

import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Text (Text)

{- | The edge a pending request names. Only the two edges the model admits
settle; any other edge is refused @edge-inadmissible@.
-}
data EdgeKind
    = EdgeInsertActive
    | EdgeUpdateTerminal
    | EdgeOther Text
    deriving stock (EdgeKind -> EdgeKind -> Bool
(EdgeKind -> EdgeKind -> Bool)
-> (EdgeKind -> EdgeKind -> Bool) -> Eq EdgeKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EdgeKind -> EdgeKind -> Bool
== :: EdgeKind -> EdgeKind -> Bool
$c/= :: EdgeKind -> EdgeKind -> Bool
/= :: EdgeKind -> EdgeKind -> Bool
Eq, Int -> EdgeKind -> ShowS
[EdgeKind] -> ShowS
EdgeKind -> String
(Int -> EdgeKind -> ShowS)
-> (EdgeKind -> String) -> ([EdgeKind] -> ShowS) -> Show EdgeKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EdgeKind -> ShowS
showsPrec :: Int -> EdgeKind -> ShowS
$cshow :: EdgeKind -> String
show :: EdgeKind -> String
$cshowList :: [EdgeKind] -> ShowS
showList :: [EdgeKind] -> ShowS
Show)

-- | The live leaf for a key, read from the registry state before the decision.
data Leaf
    = LeafUnknown
    | LeafAbsent
    | LeafActive
    | LeafTerminal
    deriving stock (Leaf -> Leaf -> Bool
(Leaf -> Leaf -> Bool) -> (Leaf -> Leaf -> Bool) -> Eq Leaf
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Leaf -> Leaf -> Bool
== :: Leaf -> Leaf -> Bool
$c/= :: Leaf -> Leaf -> Bool
/= :: Leaf -> Leaf -> Bool
Eq, Int -> Leaf -> ShowS
[Leaf] -> ShowS
Leaf -> String
(Int -> Leaf -> ShowS)
-> (Leaf -> String) -> ([Leaf] -> ShowS) -> Show Leaf
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Leaf -> ShowS
showsPrec :: Int -> Leaf -> ShowS
$cshow :: Leaf -> String
show :: Leaf -> String
$cshowList :: [Leaf] -> ShowS
showList :: [Leaf] -> ShowS
Show)

{- | The model's approval check, decided by the caller from the live state:
a missing approval, an approval under another policy (both @no-approval@),
an approval whose tuple does not match (@approval-mismatch@), or a match.
-}
data ApprovalCheck
    = ApprovalMissing
    | ApprovalPolicyMismatch
    | ApprovalTupleMismatch
    | ApprovalOk
    deriving stock (ApprovalCheck -> ApprovalCheck -> Bool
(ApprovalCheck -> ApprovalCheck -> Bool)
-> (ApprovalCheck -> ApprovalCheck -> Bool) -> Eq ApprovalCheck
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ApprovalCheck -> ApprovalCheck -> Bool
== :: ApprovalCheck -> ApprovalCheck -> Bool
$c/= :: ApprovalCheck -> ApprovalCheck -> Bool
/= :: ApprovalCheck -> ApprovalCheck -> Bool
Eq, Int -> ApprovalCheck -> ShowS
[ApprovalCheck] -> ShowS
ApprovalCheck -> String
(Int -> ApprovalCheck -> ShowS)
-> (ApprovalCheck -> String)
-> ([ApprovalCheck] -> ShowS)
-> Show ApprovalCheck
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ApprovalCheck -> ShowS
showsPrec :: Int -> ApprovalCheck -> ShowS
$cshow :: ApprovalCheck -> String
show :: ApprovalCheck -> String
$cshowList :: [ApprovalCheck] -> ShowS
showList :: [ApprovalCheck] -> ShowS
Show)

{- | The application step's verdict, asked through the application value and
carried on the pending request: the settlement inputs are ready, the
carried datum does not read, or the value carries no holding rules for a
termination, naming the application's executable.
-}
data AppVerdict
    = AppReady
    | AppDatumUnreadable
    | AppRequired Text
    deriving stock (AppVerdict -> AppVerdict -> Bool
(AppVerdict -> AppVerdict -> Bool)
-> (AppVerdict -> AppVerdict -> Bool) -> Eq AppVerdict
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AppVerdict -> AppVerdict -> Bool
== :: AppVerdict -> AppVerdict -> Bool
$c/= :: AppVerdict -> AppVerdict -> Bool
/= :: AppVerdict -> AppVerdict -> Bool
Eq, Int -> AppVerdict -> ShowS
[AppVerdict] -> ShowS
AppVerdict -> String
(Int -> AppVerdict -> ShowS)
-> (AppVerdict -> String)
-> ([AppVerdict] -> ShowS)
-> Show AppVerdict
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AppVerdict -> ShowS
showsPrec :: Int -> AppVerdict -> ShowS
$cshow :: AppVerdict -> String
show :: AppVerdict -> String
$cshowList :: [AppVerdict] -> ShowS
showList :: [AppVerdict] -> ShowS
Show)

{- | One pending request with everything the seven checks need. The
application verdict arrives as a field, like the decode verdict does: the
selection never calls the application value.
-}
data PendingRequest = PendingRequest
    { PendingRequest -> Int
prRef :: Int
    , PendingRequest -> Int
prKey :: Int
    , PendingRequest -> Text
prOwner :: Text
    , PendingRequest -> EdgeKind
prEdge :: EdgeKind
    , PendingRequest -> Integer
prDeadline :: Integer
    , PendingRequest -> Bool
prDecodeOk :: Bool
    , PendingRequest -> ApprovalCheck
prApproval :: ApprovalCheck
    , PendingRequest -> AppVerdict
prApp :: AppVerdict
    }
    deriving stock (PendingRequest -> PendingRequest -> Bool
(PendingRequest -> PendingRequest -> Bool)
-> (PendingRequest -> PendingRequest -> Bool) -> Eq PendingRequest
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PendingRequest -> PendingRequest -> Bool
== :: PendingRequest -> PendingRequest -> Bool
$c/= :: PendingRequest -> PendingRequest -> Bool
/= :: PendingRequest -> PendingRequest -> Bool
Eq, Int -> PendingRequest -> ShowS
[PendingRequest] -> ShowS
PendingRequest -> String
(Int -> PendingRequest -> ShowS)
-> (PendingRequest -> String)
-> ([PendingRequest] -> ShowS)
-> Show PendingRequest
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PendingRequest -> ShowS
showsPrec :: Int -> PendingRequest -> ShowS
$cshow :: PendingRequest -> String
show :: PendingRequest -> String
$cshowList :: [PendingRequest] -> ShowS
showList :: [PendingRequest] -> ShowS
Show)

-- | A request that passed all seven checks.
data SelectedRequest = SelectedRequest
    { SelectedRequest -> Int
selRef :: Int
    , SelectedRequest -> Int
selKey :: Int
    , SelectedRequest -> Text
selOwner :: Text
    , SelectedRequest -> EdgeKind
selEdge :: EdgeKind
    , SelectedRequest -> Integer
selDeadline :: Integer
    }
    deriving stock (SelectedRequest -> SelectedRequest -> Bool
(SelectedRequest -> SelectedRequest -> Bool)
-> (SelectedRequest -> SelectedRequest -> Bool)
-> Eq SelectedRequest
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SelectedRequest -> SelectedRequest -> Bool
== :: SelectedRequest -> SelectedRequest -> Bool
$c/= :: SelectedRequest -> SelectedRequest -> Bool
/= :: SelectedRequest -> SelectedRequest -> Bool
Eq, Int -> SelectedRequest -> ShowS
[SelectedRequest] -> ShowS
SelectedRequest -> String
(Int -> SelectedRequest -> ShowS)
-> (SelectedRequest -> String)
-> ([SelectedRequest] -> ShowS)
-> Show SelectedRequest
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SelectedRequest -> ShowS
showsPrec :: Int -> SelectedRequest -> ShowS
$cshow :: SelectedRequest -> String
show :: SelectedRequest -> String
$cshowList :: [SelectedRequest] -> ShowS
showList :: [SelectedRequest] -> ShowS
Show)

{- | Every exclusion reason: eight model refusals in the model's own words,
six selection-policy reasons of the processor.
-}
data Reason
    = ReasonEdgeInadmissible
    | ReasonNoApproval
    | ReasonApprovalMismatch
    | ReasonKeyExists
    | ReasonTokenMissing
    | ReasonKeyUnknown
    | ReasonNotBooked
    | ReasonTerminalImmutable
    | ReasonUndecodable
    | ReasonWindowClosed
    | ReasonAppDatumUnreadable
    | ReasonAppRequired
    | ReasonKeyInBatch
    | ReasonCapacity
    deriving stock (Reason -> Reason -> Bool
(Reason -> Reason -> Bool)
-> (Reason -> Reason -> Bool) -> Eq Reason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Reason -> Reason -> Bool
== :: Reason -> Reason -> Bool
$c/= :: Reason -> Reason -> Bool
/= :: Reason -> Reason -> Bool
Eq, Int -> Reason -> ShowS
[Reason] -> ShowS
Reason -> String
(Int -> Reason -> ShowS)
-> (Reason -> String) -> ([Reason] -> ShowS) -> Show Reason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Reason -> ShowS
showsPrec :: Int -> Reason -> ShowS
$cshow :: Reason -> String
show :: Reason -> String
$cshowList :: [Reason] -> ShowS
showList :: [Reason] -> ShowS
Show, Int -> Reason
Reason -> Int
Reason -> [Reason]
Reason -> Reason
Reason -> Reason -> [Reason]
Reason -> Reason -> Reason -> [Reason]
(Reason -> Reason)
-> (Reason -> Reason)
-> (Int -> Reason)
-> (Reason -> Int)
-> (Reason -> [Reason])
-> (Reason -> Reason -> [Reason])
-> (Reason -> Reason -> [Reason])
-> (Reason -> Reason -> Reason -> [Reason])
-> Enum Reason
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Reason -> Reason
succ :: Reason -> Reason
$cpred :: Reason -> Reason
pred :: Reason -> Reason
$ctoEnum :: Int -> Reason
toEnum :: Int -> Reason
$cfromEnum :: Reason -> Int
fromEnum :: Reason -> Int
$cenumFrom :: Reason -> [Reason]
enumFrom :: Reason -> [Reason]
$cenumFromThen :: Reason -> Reason -> [Reason]
enumFromThen :: Reason -> Reason -> [Reason]
$cenumFromTo :: Reason -> Reason -> [Reason]
enumFromTo :: Reason -> Reason -> [Reason]
$cenumFromThenTo :: Reason -> Reason -> Reason -> [Reason]
enumFromThenTo :: Reason -> Reason -> Reason -> [Reason]
Enum, Reason
Reason -> Reason -> Bounded Reason
forall a. a -> a -> Bounded a
$cminBound :: Reason
minBound :: Reason
$cmaxBound :: Reason
maxBound :: Reason
Bounded)

{- | Why a pending request is left out: its reason and a detail text. The
detail of @application-required@ names the application's executable.
-}
data Exclusion = Exclusion
    { Exclusion -> Reason
excReason :: Reason
    , Exclusion -> Text
excDetail :: Text
    }
    deriving stock (Exclusion -> Exclusion -> Bool
(Exclusion -> Exclusion -> Bool)
-> (Exclusion -> Exclusion -> Bool) -> Eq Exclusion
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Exclusion -> Exclusion -> Bool
== :: Exclusion -> Exclusion -> Bool
$c/= :: Exclusion -> Exclusion -> Bool
/= :: Exclusion -> Exclusion -> Bool
Eq, Int -> Exclusion -> ShowS
[Exclusion] -> ShowS
Exclusion -> String
(Int -> Exclusion -> ShowS)
-> (Exclusion -> String)
-> ([Exclusion] -> ShowS)
-> Show Exclusion
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Exclusion -> ShowS
showsPrec :: Int -> Exclusion -> ShowS
$cshow :: Exclusion -> String
show :: Exclusion -> String
$cshowList :: [Exclusion] -> ShowS
showList :: [Exclusion] -> ShowS
Show)

{- | The selection: the settled requests and the excluded requests, each in
ledger input order, with the capacity bound used and its provenance.
-}
data Selection = Selection
    { Selection -> [SelectedRequest]
selectionSettled :: [SelectedRequest]
    , Selection -> [(PendingRequest, Exclusion)]
selectionExcluded :: [(PendingRequest, Exclusion)]
    , Selection -> Int
selectionBound :: Int
    , Selection -> Text
selectionProvenance :: Text
    }
    deriving stock (Selection -> Selection -> Bool
(Selection -> Selection -> Bool)
-> (Selection -> Selection -> Bool) -> Eq Selection
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Selection -> Selection -> Bool
== :: Selection -> Selection -> Bool
$c/= :: Selection -> Selection -> Bool
/= :: Selection -> Selection -> Bool
Eq, Int -> Selection -> ShowS
[Selection] -> ShowS
Selection -> String
(Int -> Selection -> ShowS)
-> (Selection -> String)
-> ([Selection] -> ShowS)
-> Show Selection
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Selection -> ShowS
showsPrec :: Int -> Selection -> ShowS
$cshow :: Selection -> String
show :: Selection -> String
$cshowList :: [Selection] -> ShowS
showList :: [Selection] -> ShowS
Show)

{- | The live facts: per key, the leaf and whether a live output holds the
key's one active token.
-}
type LiveFacts = Map Int (Leaf, Bool)

{- | The capacity bound of a fold: nine requests per fold, an estimate
under preprod's execution budget of 14 million memory units, bound by
trie-proof verification. The number is not measured under preprod parameters.
-}
foldCapacity :: Int
foldCapacity :: Int
foldCapacity = Int
9

-- | an estimate, not a measurement: about nine requests fit in a fold under preprod's execution budget of 14 million memory units, bound by trie-proof verification
foldCapacityProvenance :: Text
foldCapacityProvenance :: Text
foldCapacityProvenance =
    Text
"an estimate, not a measurement: about nine requests fit in a fold under preprod's execution budget of 14 million memory units, bound by trie-proof verification"

-- | The reason's name in the receipt's vocabulary.
exclusionName :: Exclusion -> Text
exclusionName :: Exclusion -> Text
exclusionName Exclusion
exc = case Exclusion -> Reason
excReason Exclusion
exc of
    Reason
ReasonEdgeInadmissible -> Text
"edge-inadmissible"
    Reason
ReasonNoApproval -> Text
"no-approval"
    Reason
ReasonApprovalMismatch -> Text
"approval-mismatch"
    Reason
ReasonKeyExists -> Text
"key-exists"
    Reason
ReasonTokenMissing -> Text
"token-missing"
    Reason
ReasonKeyUnknown -> Text
"key-unknown"
    Reason
ReasonNotBooked -> Text
"not-booked"
    Reason
ReasonTerminalImmutable -> Text
"terminal-immutable"
    Reason
ReasonUndecodable -> Text
"undecodable"
    Reason
ReasonWindowClosed -> Text
"window-closed"
    Reason
ReasonAppDatumUnreadable -> Text
"application-datum-unreadable"
    Reason
ReasonAppRequired -> Text
"application-required"
    Reason
ReasonKeyInBatch -> Text
"key-in-batch"
    Reason
ReasonCapacity -> Text
"capacity"

{- | Which vocabulary the reason belongs to: a refusal of the model or the
processor's own selection policy.
-}
exclusionSource :: Exclusion -> Text
exclusionSource :: Exclusion -> Text
exclusionSource Exclusion
exc = case Exclusion -> Reason
excReason Exclusion
exc of
    Reason
ReasonEdgeInadmissible -> Text
"model-refusal"
    Reason
ReasonNoApproval -> Text
"model-refusal"
    Reason
ReasonApprovalMismatch -> Text
"model-refusal"
    Reason
ReasonKeyExists -> Text
"model-refusal"
    Reason
ReasonTokenMissing -> Text
"model-refusal"
    Reason
ReasonKeyUnknown -> Text
"model-refusal"
    Reason
ReasonNotBooked -> Text
"model-refusal"
    Reason
ReasonTerminalImmutable -> Text
"model-refusal"
    Reason
ReasonUndecodable -> Text
"selection-policy"
    Reason
ReasonWindowClosed -> Text
"selection-policy"
    Reason
ReasonAppDatumUnreadable -> Text
"selection-policy"
    Reason
ReasonAppRequired -> Text
"selection-policy"
    Reason
ReasonKeyInBatch -> Text
"selection-policy"
    Reason
ReasonCapacity -> Text
"selection-policy"

-- | Whether the edge is one the model admits.
isAdmittedEdge :: EdgeKind -> Bool
isAdmittedEdge :: EdgeKind -> Bool
isAdmittedEdge EdgeKind
EdgeInsertActive = Bool
True
isAdmittedEdge EdgeKind
EdgeUpdateTerminal = Bool
True
isAdmittedEdge (EdgeOther Text
_) = Bool
False

{- | Judge one request alone against the live facts: the six per-request
checks in the spec's order. No argument names any other pending request, so
a request's verdict never depends on requests on other keys. The seventh
check, 'ReasonKeyInBatch', needs the earlier verdicts and runs in
'selectFold'.
-}
judgeAlone
    :: Integer
    -> Integer
    -> LiveFacts
    -> PendingRequest
    -> Either Exclusion SelectedRequest
judgeAlone :: Integer
-> Integer
-> LiveFacts
-> PendingRequest
-> Either Exclusion SelectedRequest
judgeAlone Integer
now Integer
margin LiveFacts
facts PendingRequest
req
    | Bool -> Bool
not (PendingRequest -> Bool
prDecodeOk PendingRequest
req) =
        Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
            (Reason -> Text -> Exclusion
Exclusion Reason
ReasonUndecodable Text
"the output does not decode as a request")
    | Bool -> Bool
not (EdgeKind -> Bool
isAdmittedEdge (PendingRequest -> EdgeKind
prEdge PendingRequest
req)) =
        Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
            ( Reason -> Text -> Exclusion
Exclusion
                Reason
ReasonEdgeInadmissible
                Text
"the edge is not one the model admits"
            )
    | PendingRequest -> Integer
prDeadline PendingRequest
req Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
now Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
margin =
        Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
            ( Reason -> Text -> Exclusion
Exclusion
                Reason
ReasonWindowClosed
                Text
"the processing window is not open beyond the fold margin"
            )
    | Bool
otherwise = case PendingRequest -> ApprovalCheck
prApproval PendingRequest
req of
        ApprovalCheck
ApprovalMissing ->
            Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left (Reason -> Text -> Exclusion
Exclusion Reason
ReasonNoApproval Text
"the request carries no approval")
        ApprovalCheck
ApprovalPolicyMismatch ->
            Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
                (Reason -> Text -> Exclusion
Exclusion Reason
ReasonNoApproval Text
"the approval is under another policy")
        ApprovalCheck
ApprovalTupleMismatch ->
            Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
                ( Reason -> Text -> Exclusion
Exclusion
                    Reason
ReasonApprovalMismatch
                    Text
"the approval does not match the request"
                )
        ApprovalCheck
ApprovalOk ->
            (Leaf, Bool) -> PendingRequest -> Either Exclusion SelectedRequest
judgeLeaf
                ((Leaf, Bool) -> Int -> LiveFacts -> (Leaf, Bool)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Leaf
LeafUnknown, Bool
False) (PendingRequest -> Int
prKey PendingRequest
req) LiveFacts
facts)
                PendingRequest
req

{- | The model's leaf check from the live facts. A key the facts never
mention reads unknown, like a fresh key. The admitted edge is already
established, so the remaining 'EdgeOther' arm cannot fire.
-}
judgeLeaf
    :: (Leaf, Bool) -> PendingRequest -> Either Exclusion SelectedRequest
judgeLeaf :: (Leaf, Bool) -> PendingRequest -> Either Exclusion SelectedRequest
judgeLeaf (Leaf
leaf, Bool
tokenPresent) PendingRequest
req = case PendingRequest -> EdgeKind
prEdge PendingRequest
req of
    EdgeKind
EdgeInsertActive
        | Leaf
leaf Leaf -> Leaf -> Bool
forall a. Eq a => a -> a -> Bool
== Leaf
LeafUnknown -> PendingRequest -> Either Exclusion SelectedRequest
judgeApp PendingRequest
req
        | Bool
otherwise ->
            Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left (Reason -> Text -> Exclusion
Exclusion Reason
ReasonKeyExists Text
"the key is already booked")
    EdgeKind
EdgeUpdateTerminal -> case Leaf
leaf of
        Leaf
LeafUnknown -> Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left (Reason -> Text -> Exclusion
Exclusion Reason
ReasonKeyUnknown Text
"the key is unknown")
        Leaf
LeafAbsent -> Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left (Reason -> Text -> Exclusion
Exclusion Reason
ReasonNotBooked Text
"the key is not booked")
        Leaf
LeafTerminal -> Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left (Reason -> Text -> Exclusion
Exclusion Reason
ReasonTerminalImmutable Text
"the key is terminal")
        Leaf
LeafActive
            | Bool
tokenPresent -> PendingRequest -> Either Exclusion SelectedRequest
judgeApp PendingRequest
req
            | Bool
otherwise ->
                Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
                    ( Reason -> Text -> Exclusion
Exclusion
                        Reason
ReasonTokenMissing
                        Text
"no live output holds the key's active token"
                    )
    EdgeOther Text
_ ->
        Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
            ( Reason -> Text -> Exclusion
Exclusion
                Reason
ReasonEdgeInadmissible
                Text
"the edge is not one the model admits"
            )

{- | The sixth check: place the application step's verdict, which arrives as
a field of the pending request, after the model's leaf check.
-}
judgeApp :: PendingRequest -> Either Exclusion SelectedRequest
judgeApp :: PendingRequest -> Either Exclusion SelectedRequest
judgeApp PendingRequest
req = case PendingRequest -> AppVerdict
prApp PendingRequest
req of
    AppVerdict
AppDatumUnreadable ->
        Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
            (Reason -> Text -> Exclusion
Exclusion Reason
ReasonAppDatumUnreadable Text
"the carried datum does not read")
    AppRequired Text
exe ->
        Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
            ( Reason -> Text -> Exclusion
Exclusion
                Reason
ReasonAppRequired
                (Text
"the value carries no holding rules; settle with " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
exe)
            )
    AppVerdict
AppReady ->
        SelectedRequest -> Either Exclusion SelectedRequest
forall a b. b -> Either a b
Right
            ( Int -> Int -> Text -> EdgeKind -> Integer -> SelectedRequest
SelectedRequest
                (PendingRequest -> Int
prRef PendingRequest
req)
                (PendingRequest -> Int
prKey PendingRequest
req)
                (PendingRequest -> Text
prOwner PendingRequest
req)
                (PendingRequest -> EdgeKind
prEdge PendingRequest
req)
                (PendingRequest -> Integer
prDeadline PendingRequest
req)
            )

{- | Judge every pending request alone, keep ledger input order, and settle
the first included requests up to the capacity bound. The only cross-request
rule is the seventh check, which reads earlier included requests of the same
key; the capacity cut runs after every request has its own verdict. Both
lists keep ledger input order.
-}
selectFold
    :: Int
    -> Integer
    -> Integer
    -> LiveFacts
    -> [PendingRequest]
    -> Selection
selectFold :: Int
-> Integer -> Integer -> LiveFacts -> [PendingRequest] -> Selection
selectFold Int
bound Integer
now Integer
margin LiveFacts
facts [PendingRequest]
reqs =
    [SelectedRequest]
-> [(PendingRequest, Exclusion)] -> Int -> Text -> Selection
Selection [SelectedRequest]
settled [(PendingRequest, Exclusion)]
excluded Int
bound Text
foldCapacityProvenance
  where
    judged :: [(PendingRequest, Either Exclusion SelectedRequest)]
    judged :: [(PendingRequest, Either Exclusion SelectedRequest)]
judged = [(PendingRequest
req, Integer
-> Integer
-> LiveFacts
-> PendingRequest
-> Either Exclusion SelectedRequest
judgeAlone Integer
now Integer
margin LiveFacts
facts PendingRequest
req) | PendingRequest
req <- [PendingRequest]
reqs]

    deduped :: [(PendingRequest, Either Exclusion SelectedRequest)]
    deduped :: [(PendingRequest, Either Exclusion SelectedRequest)]
deduped = Set Int
-> [(PendingRequest, Either Exclusion SelectedRequest)]
-> [(PendingRequest, Either Exclusion SelectedRequest)]
forall {a}.
Set Int
-> [(a, Either Exclusion SelectedRequest)]
-> [(a, Either Exclusion SelectedRequest)]
go Set Int
forall a. Set a
Set.empty [(PendingRequest, Either Exclusion SelectedRequest)]
judged
      where
        go :: Set Int
-> [(a, Either Exclusion SelectedRequest)]
-> [(a, Either Exclusion SelectedRequest)]
go Set Int
_ [] = []
        go Set Int
seen ((a
req, Either Exclusion SelectedRequest
verdict) : [(a, Either Exclusion SelectedRequest)]
rest) = case Either Exclusion SelectedRequest
verdict of
            Left Exclusion
exc -> (a
req, Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left Exclusion
exc) (a, Either Exclusion SelectedRequest)
-> [(a, Either Exclusion SelectedRequest)]
-> [(a, Either Exclusion SelectedRequest)]
forall a. a -> [a] -> [a]
: Set Int
-> [(a, Either Exclusion SelectedRequest)]
-> [(a, Either Exclusion SelectedRequest)]
go Set Int
seen [(a, Either Exclusion SelectedRequest)]
rest
            Right SelectedRequest
sel
                | SelectedRequest -> Int
selKey SelectedRequest
sel Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Int
seen ->
                    ( a
req
                    , Exclusion -> Either Exclusion SelectedRequest
forall a b. a -> Either a b
Left
                        ( Reason -> Text -> Exclusion
Exclusion
                            Reason
ReasonKeyInBatch
                            Text
"an earlier included request names the same key"
                        )
                    )
                        (a, Either Exclusion SelectedRequest)
-> [(a, Either Exclusion SelectedRequest)]
-> [(a, Either Exclusion SelectedRequest)]
forall a. a -> [a] -> [a]
: Set Int
-> [(a, Either Exclusion SelectedRequest)]
-> [(a, Either Exclusion SelectedRequest)]
go Set Int
seen [(a, Either Exclusion SelectedRequest)]
rest
                | Bool
otherwise ->
                    (a
req, SelectedRequest -> Either Exclusion SelectedRequest
forall a b. b -> Either a b
Right SelectedRequest
sel) (a, Either Exclusion SelectedRequest)
-> [(a, Either Exclusion SelectedRequest)]
-> [(a, Either Exclusion SelectedRequest)]
forall a. a -> [a] -> [a]
: Set Int
-> [(a, Either Exclusion SelectedRequest)]
-> [(a, Either Exclusion SelectedRequest)]
go (Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert (SelectedRequest -> Int
selKey SelectedRequest
sel) Set Int
seen) [(a, Either Exclusion SelectedRequest)]
rest

    settledRefs :: Set.Set Int
    settledRefs :: Set Int
settledRefs =
        [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList
            (Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 Int
bound) [SelectedRequest -> Int
selRef SelectedRequest
sel | (PendingRequest
_, Right SelectedRequest
sel) <- [(PendingRequest, Either Exclusion SelectedRequest)]
deduped])

    settled :: [SelectedRequest]
    settled :: [SelectedRequest]
settled =
        [SelectedRequest
sel | (PendingRequest
_, Right SelectedRequest
sel) <- [(PendingRequest, Either Exclusion SelectedRequest)]
deduped, SelectedRequest -> Int
selRef SelectedRequest
sel Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Int
settledRefs]

    excluded :: [(PendingRequest, Exclusion)]
    excluded :: [(PendingRequest, Exclusion)]
excluded =
        [ (PendingRequest
req, Exclusion
exc)
        | (PendingRequest
req, Either Exclusion SelectedRequest
verdict) <- [(PendingRequest, Either Exclusion SelectedRequest)]
deduped
        , Just Exclusion
exc <- [Either Exclusion SelectedRequest -> Maybe Exclusion
toExclusion Either Exclusion SelectedRequest
verdict]
        ]
      where
        toExclusion :: Either Exclusion SelectedRequest -> Maybe Exclusion
toExclusion (Left Exclusion
exc) = Exclusion -> Maybe Exclusion
forall a. a -> Maybe a
Just Exclusion
exc
        toExclusion (Right SelectedRequest
sel)
            | SelectedRequest -> Int
selRef SelectedRequest
sel Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Int
settledRefs = Maybe Exclusion
forall a. Maybe a
Nothing
            | Bool
otherwise =
                Exclusion -> Maybe Exclusion
forall a. a -> Maybe a
Just
                    ( Reason -> Text -> Exclusion
Exclusion
                        Reason
ReasonCapacity
                        Text
"the fold is at its capacity bound; the next fold takes this request"
                    )