{-# LANGUAGE GADTs #-}

{- | Programs over the nine exits of the model: seven folds, a reject and a
retract, and over the model's two batch questions: several requests folded in one
transaction, and several rejected in one. Handles remain opaque to stories.
-}
module Conformance.Story.Live
    ( Edge (..)
    , edgeName
    , Exit (..)
    , exitName
    , EdgeRequest (..)
    , Tamper (..)
    , tamperName
    , BatchTamper (..)
    , batchTamperName
    , RefundTamper (..)
    , refundTamperName
    , refundShortfall
    , Booking (..)
    , Placement (..)
    , placementName
    , placementReading
    , placementWindow
    , LiveI (..)
    , Story
    , Context (..)
    , submit
    , tamper
    , rejectWithin
    , tamperRejectWithin
    , retract
    , tamperExit
    , foldBatch
    , tamperFoldBatch
    , rejectBatchWithin
    , rejectBookedBatchWithin
    , tamperRejectBookedBatchWithin
    , observe
    , compareWithModel
    , renderLive
    , validateLive
    , Instruction (..)
    , InstructionKind (..)
    , liveInstructions
    ) where

import Conformance.Story.Binding (Binding, BoundObligation (..))
import Conformance.Story.Specification
    ( Clause (..)
    , Step (..)
    , TheoremStory
    , action
    , checkAction
    , clauses
    , theoremBinding
    )
import Conformance.Story.Specification qualified as Specification
import Control.Monad.Operational
    ( Program
    , ProgramViewT (Return, (:>>=))
    , view
    )
import Data.List (intercalate)

data Edge
    = InsertAbsent
    | InsertActive
    | UpdateActive
    | UpdateTerminal
    | DeleteAbsent
    | DeleteActive
    | WitnessTerminal
    deriving stock (Edge -> Edge -> Bool
(Edge -> Edge -> Bool) -> (Edge -> Edge -> Bool) -> Eq Edge
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Edge -> Edge -> Bool
== :: Edge -> Edge -> Bool
$c/= :: Edge -> Edge -> Bool
/= :: Edge -> Edge -> Bool
Eq, Eq Edge
Eq Edge =>
(Edge -> Edge -> Ordering)
-> (Edge -> Edge -> Bool)
-> (Edge -> Edge -> Bool)
-> (Edge -> Edge -> Bool)
-> (Edge -> Edge -> Bool)
-> (Edge -> Edge -> Edge)
-> (Edge -> Edge -> Edge)
-> Ord Edge
Edge -> Edge -> Bool
Edge -> Edge -> Ordering
Edge -> Edge -> Edge
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Edge -> Edge -> Ordering
compare :: Edge -> Edge -> Ordering
$c< :: Edge -> Edge -> Bool
< :: Edge -> Edge -> Bool
$c<= :: Edge -> Edge -> Bool
<= :: Edge -> Edge -> Bool
$c> :: Edge -> Edge -> Bool
> :: Edge -> Edge -> Bool
$c>= :: Edge -> Edge -> Bool
>= :: Edge -> Edge -> Bool
$cmax :: Edge -> Edge -> Edge
max :: Edge -> Edge -> Edge
$cmin :: Edge -> Edge -> Edge
min :: Edge -> Edge -> Edge
Ord, Int -> Edge -> ShowS
[Edge] -> ShowS
Edge -> String
(Int -> Edge -> ShowS)
-> (Edge -> String) -> ([Edge] -> ShowS) -> Show Edge
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Edge -> ShowS
showsPrec :: Int -> Edge -> ShowS
$cshow :: Edge -> String
show :: Edge -> String
$cshowList :: [Edge] -> ShowS
showList :: [Edge] -> ShowS
Show, Int -> Edge
Edge -> Int
Edge -> [Edge]
Edge -> Edge
Edge -> Edge -> [Edge]
Edge -> Edge -> Edge -> [Edge]
(Edge -> Edge)
-> (Edge -> Edge)
-> (Int -> Edge)
-> (Edge -> Int)
-> (Edge -> [Edge])
-> (Edge -> Edge -> [Edge])
-> (Edge -> Edge -> [Edge])
-> (Edge -> Edge -> Edge -> [Edge])
-> Enum Edge
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 :: Edge -> Edge
succ :: Edge -> Edge
$cpred :: Edge -> Edge
pred :: Edge -> Edge
$ctoEnum :: Int -> Edge
toEnum :: Int -> Edge
$cfromEnum :: Edge -> Int
fromEnum :: Edge -> Int
$cenumFrom :: Edge -> [Edge]
enumFrom :: Edge -> [Edge]
$cenumFromThen :: Edge -> Edge -> [Edge]
enumFromThen :: Edge -> Edge -> [Edge]
$cenumFromTo :: Edge -> Edge -> [Edge]
enumFromTo :: Edge -> Edge -> [Edge]
$cenumFromThenTo :: Edge -> Edge -> Edge -> [Edge]
enumFromThenTo :: Edge -> Edge -> Edge -> [Edge]
Enum, Edge
Edge -> Edge -> Bounded Edge
forall a. a -> a -> Bounded a
$cminBound :: Edge
minBound :: Edge
$cmaxBound :: Edge
maxBound :: Edge
Bounded)

edgeName :: Edge -> String
edgeName :: Edge -> String
edgeName Edge
edge = case Edge
edge of
    Edge
InsertAbsent -> String
"insertAbsent"
    Edge
InsertActive -> String
"insertActive"
    Edge
UpdateActive -> String
"updateActive"
    Edge
UpdateTerminal -> String
"updateTerminal"
    Edge
DeleteAbsent -> String
"deleteAbsent"
    Edge
DeleteActive -> String
"deleteActive"
    Edge
WitnessTerminal -> String
"witnessTerminal"

{- | How a request leaves the queue: folded by its own edge, rejected by a folder
in a window its story names, or retracted by its owner.
-}
data Exit = Fold | Reject | Retract
    deriving stock (Exit -> Exit -> Bool
(Exit -> Exit -> Bool) -> (Exit -> Exit -> Bool) -> Eq Exit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Exit -> Exit -> Bool
== :: Exit -> Exit -> Bool
$c/= :: Exit -> Exit -> Bool
/= :: Exit -> Exit -> Bool
Eq, Int -> Exit -> ShowS
[Exit] -> ShowS
Exit -> String
(Int -> Exit -> ShowS)
-> (Exit -> String) -> ([Exit] -> ShowS) -> Show Exit
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Exit -> ShowS
showsPrec :: Int -> Exit -> ShowS
$cshow :: Exit -> String
show :: Exit -> String
$cshowList :: [Exit] -> ShowS
showList :: [Exit] -> ShowS
Show, Int -> Exit
Exit -> Int
Exit -> [Exit]
Exit -> Exit
Exit -> Exit -> [Exit]
Exit -> Exit -> Exit -> [Exit]
(Exit -> Exit)
-> (Exit -> Exit)
-> (Int -> Exit)
-> (Exit -> Int)
-> (Exit -> [Exit])
-> (Exit -> Exit -> [Exit])
-> (Exit -> Exit -> [Exit])
-> (Exit -> Exit -> Exit -> [Exit])
-> Enum Exit
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 :: Exit -> Exit
succ :: Exit -> Exit
$cpred :: Exit -> Exit
pred :: Exit -> Exit
$ctoEnum :: Int -> Exit
toEnum :: Int -> Exit
$cfromEnum :: Exit -> Int
fromEnum :: Exit -> Int
$cenumFrom :: Exit -> [Exit]
enumFrom :: Exit -> [Exit]
$cenumFromThen :: Exit -> Exit -> [Exit]
enumFromThen :: Exit -> Exit -> [Exit]
$cenumFromTo :: Exit -> Exit -> [Exit]
enumFromTo :: Exit -> Exit -> [Exit]
$cenumFromThenTo :: Exit -> Exit -> Exit -> [Exit]
enumFromThenTo :: Exit -> Exit -> Exit -> [Exit]
Enum, Exit
Exit -> Exit -> Bounded Exit
forall a. a -> a -> Bounded a
$cminBound :: Exit
minBound :: Exit
$cmaxBound :: Exit
maxBound :: Exit
Bounded)

-- | An exit's operation name: a fold is named by the edge it folds.
exitName :: Exit -> Edge -> String
exitName :: Exit -> Edge -> String
exitName Exit
Fold Edge
edge = Edge -> String
edgeName Edge
edge
exitName Exit
Reject Edge
_ = String
"reject"
exitName Exit
Retract Edge
_ = String
"retract"

data EdgeRequest wal = EdgeRequest
    { forall wal. EdgeRequest wal -> Edge
requestEdge :: Edge
    , forall wal. EdgeRequest wal -> String
requestKey :: String
    , forall wal. EdgeRequest wal -> wal
requestWallet :: wal
    }
    deriving stock (EdgeRequest wal -> EdgeRequest wal -> Bool
(EdgeRequest wal -> EdgeRequest wal -> Bool)
-> (EdgeRequest wal -> EdgeRequest wal -> Bool)
-> Eq (EdgeRequest wal)
forall wal. Eq wal => EdgeRequest wal -> EdgeRequest wal -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall wal. Eq wal => EdgeRequest wal -> EdgeRequest wal -> Bool
== :: EdgeRequest wal -> EdgeRequest wal -> Bool
$c/= :: forall wal. Eq wal => EdgeRequest wal -> EdgeRequest wal -> Bool
/= :: EdgeRequest wal -> EdgeRequest wal -> Bool
Eq, Int -> EdgeRequest wal -> ShowS
[EdgeRequest wal] -> ShowS
EdgeRequest wal -> String
(Int -> EdgeRequest wal -> ShowS)
-> (EdgeRequest wal -> String)
-> ([EdgeRequest wal] -> ShowS)
-> Show (EdgeRequest wal)
forall wal. Show wal => Int -> EdgeRequest wal -> ShowS
forall wal. Show wal => [EdgeRequest wal] -> ShowS
forall wal. Show wal => EdgeRequest wal -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall wal. Show wal => Int -> EdgeRequest wal -> ShowS
showsPrec :: Int -> EdgeRequest wal -> ShowS
$cshow :: forall wal. Show wal => EdgeRequest wal -> String
show :: EdgeRequest wal -> String
$cshowList :: forall wal. Show wal => [EdgeRequest wal] -> ShowS
showList :: [EdgeRequest wal] -> ShowS
Show)

{- | A change to the submitted transaction the model's request does not make.
'OtherAddress' sends the payment the exit owes to another address, and
'ShortByOne' pays it one lovelace short; the ledger must refuse both, and the
model must refuse them for the reason it gives. 'ExtraSigner' adds one
required signer the model does not require; the ledger accepts it, and the
comparison must report the transaction's signers.
'Unsigned' removes the owner's required signature from a retraction; its
admission witness tells the model which signatures that transaction requires.
-}
data Tamper
    = OtherAddress
    | ShortByOne
    | ExtraSigner
    | OtherReference
    | StateSpent
    | Unsigned
    | BeforePhase2
    | AfterPhase2
    deriving stock (Tamper -> Tamper -> Bool
(Tamper -> Tamper -> Bool)
-> (Tamper -> Tamper -> Bool) -> Eq Tamper
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Tamper -> Tamper -> Bool
== :: Tamper -> Tamper -> Bool
$c/= :: Tamper -> Tamper -> Bool
/= :: Tamper -> Tamper -> Bool
Eq, Int -> Tamper -> ShowS
[Tamper] -> ShowS
Tamper -> String
(Int -> Tamper -> ShowS)
-> (Tamper -> String) -> ([Tamper] -> ShowS) -> Show Tamper
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Tamper -> ShowS
showsPrec :: Int -> Tamper -> ShowS
$cshow :: Tamper -> String
show :: Tamper -> String
$cshowList :: [Tamper] -> ShowS
showList :: [Tamper] -> ShowS
Show, Int -> Tamper
Tamper -> Int
Tamper -> [Tamper]
Tamper -> Tamper
Tamper -> Tamper -> [Tamper]
Tamper -> Tamper -> Tamper -> [Tamper]
(Tamper -> Tamper)
-> (Tamper -> Tamper)
-> (Int -> Tamper)
-> (Tamper -> Int)
-> (Tamper -> [Tamper])
-> (Tamper -> Tamper -> [Tamper])
-> (Tamper -> Tamper -> [Tamper])
-> (Tamper -> Tamper -> Tamper -> [Tamper])
-> Enum Tamper
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 :: Tamper -> Tamper
succ :: Tamper -> Tamper
$cpred :: Tamper -> Tamper
pred :: Tamper -> Tamper
$ctoEnum :: Int -> Tamper
toEnum :: Int -> Tamper
$cfromEnum :: Tamper -> Int
fromEnum :: Tamper -> Int
$cenumFrom :: Tamper -> [Tamper]
enumFrom :: Tamper -> [Tamper]
$cenumFromThen :: Tamper -> Tamper -> [Tamper]
enumFromThen :: Tamper -> Tamper -> [Tamper]
$cenumFromTo :: Tamper -> Tamper -> [Tamper]
enumFromTo :: Tamper -> Tamper -> [Tamper]
$cenumFromThenTo :: Tamper -> Tamper -> Tamper -> [Tamper]
enumFromThenTo :: Tamper -> Tamper -> Tamper -> [Tamper]
Enum, Tamper
Tamper -> Tamper -> Bounded Tamper
forall a. a -> a -> Bounded a
$cminBound :: Tamper
minBound :: Tamper
$cmaxBound :: Tamper
maxBound :: Tamper
Bounded)

tamperName :: Tamper -> String
tamperName :: Tamper -> String
tamperName Tamper
OtherAddress = String
"other-address"
tamperName Tamper
ShortByOne = String
"short-by-one"
tamperName Tamper
ExtraSigner = String
"extra-signer"
tamperName Tamper
OtherReference = String
"other-reference"
tamperName Tamper
StateSpent = String
"state-spent"
tamperName Tamper
Unsigned = String
"unsigned"
tamperName Tamper
BeforePhase2 = String
"before-phase-2"
tamperName Tamper
AfterPhase2 = String
"after-phase-2"

{- | A change to the transaction of a fold batch. 'MintOnFirstKey' mints every
token the batch delivers at the key of its first request, the deliveries
carrying it: the same quantity of each kind, at the wrong keys.
-}
data BatchTamper = MintOnFirstKey
    deriving stock (BatchTamper -> BatchTamper -> Bool
(BatchTamper -> BatchTamper -> Bool)
-> (BatchTamper -> BatchTamper -> Bool) -> Eq BatchTamper
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BatchTamper -> BatchTamper -> Bool
== :: BatchTamper -> BatchTamper -> Bool
$c/= :: BatchTamper -> BatchTamper -> Bool
/= :: BatchTamper -> BatchTamper -> Bool
Eq, Int -> BatchTamper -> ShowS
[BatchTamper] -> ShowS
BatchTamper -> String
(Int -> BatchTamper -> ShowS)
-> (BatchTamper -> String)
-> ([BatchTamper] -> ShowS)
-> Show BatchTamper
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BatchTamper -> ShowS
showsPrec :: Int -> BatchTamper -> ShowS
$cshow :: BatchTamper -> String
show :: BatchTamper -> String
$cshowList :: [BatchTamper] -> ShowS
showList :: [BatchTamper] -> ShowS
Show, Int -> BatchTamper
BatchTamper -> Int
BatchTamper -> [BatchTamper]
BatchTamper -> BatchTamper
BatchTamper -> BatchTamper -> [BatchTamper]
BatchTamper -> BatchTamper -> BatchTamper -> [BatchTamper]
(BatchTamper -> BatchTamper)
-> (BatchTamper -> BatchTamper)
-> (Int -> BatchTamper)
-> (BatchTamper -> Int)
-> (BatchTamper -> [BatchTamper])
-> (BatchTamper -> BatchTamper -> [BatchTamper])
-> (BatchTamper -> BatchTamper -> [BatchTamper])
-> (BatchTamper -> BatchTamper -> BatchTamper -> [BatchTamper])
-> Enum BatchTamper
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 :: BatchTamper -> BatchTamper
succ :: BatchTamper -> BatchTamper
$cpred :: BatchTamper -> BatchTamper
pred :: BatchTamper -> BatchTamper
$ctoEnum :: Int -> BatchTamper
toEnum :: Int -> BatchTamper
$cfromEnum :: BatchTamper -> Int
fromEnum :: BatchTamper -> Int
$cenumFrom :: BatchTamper -> [BatchTamper]
enumFrom :: BatchTamper -> [BatchTamper]
$cenumFromThen :: BatchTamper -> BatchTamper -> [BatchTamper]
enumFromThen :: BatchTamper -> BatchTamper -> [BatchTamper]
$cenumFromTo :: BatchTamper -> BatchTamper -> [BatchTamper]
enumFromTo :: BatchTamper -> BatchTamper -> [BatchTamper]
$cenumFromThenTo :: BatchTamper -> BatchTamper -> BatchTamper -> [BatchTamper]
enumFromThenTo :: BatchTamper -> BatchTamper -> BatchTamper -> [BatchTamper]
Enum, BatchTamper
BatchTamper -> BatchTamper -> Bounded BatchTamper
forall a. a -> a -> Bounded a
$cminBound :: BatchTamper
minBound :: BatchTamper
$cmaxBound :: BatchTamper
maxBound :: BatchTamper
Bounded)

batchTamperName :: BatchTamper -> String
batchTamperName :: BatchTamper -> String
batchTamperName BatchTamper
MintOnFirstKey = String
"mint-on-first-key"

-- | The batch tamper as the book reads it.
batchTamperReading :: BatchTamper -> String
batchTamperReading :: BatchTamper -> String
batchTamperReading BatchTamper
MintOnFirstKey =
    String
"every token the transaction mints moved onto the first request's key"

{- | A change to the refunds of a reject batch, in the transaction's input
order. 'CrossedRefunds' pays each request's owner, at its refund's position,
what the next request's owner is owed. 'ShortFirstRefund' pays the first
request's owner the given lovelace short, the rest going to the transaction's
change. 'SplitFirstRefund' pays it short at its refund's position too, with two
ada more in another output at the same owner's key.
-}
data RefundTamper
    = CrossedRefunds
    | ShortFirstRefund Integer
    | SplitFirstRefund Integer
    deriving stock (RefundTamper -> RefundTamper -> Bool
(RefundTamper -> RefundTamper -> Bool)
-> (RefundTamper -> RefundTamper -> Bool) -> Eq RefundTamper
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RefundTamper -> RefundTamper -> Bool
== :: RefundTamper -> RefundTamper -> Bool
$c/= :: RefundTamper -> RefundTamper -> Bool
/= :: RefundTamper -> RefundTamper -> Bool
Eq, Int -> RefundTamper -> ShowS
[RefundTamper] -> ShowS
RefundTamper -> String
(Int -> RefundTamper -> ShowS)
-> (RefundTamper -> String)
-> ([RefundTamper] -> ShowS)
-> Show RefundTamper
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RefundTamper -> ShowS
showsPrec :: Int -> RefundTamper -> ShowS
$cshow :: RefundTamper -> String
show :: RefundTamper -> String
$cshowList :: [RefundTamper] -> ShowS
showList :: [RefundTamper] -> ShowS
Show)

refundTamperName :: RefundTamper -> String
refundTamperName :: RefundTamper -> String
refundTamperName RefundTamper
CrossedRefunds = String
"crossed-refunds"
refundTamperName (ShortFirstRefund Integer
_) = String
"short-first-refund"
refundTamperName (SplitFirstRefund Integer
_) = String
"split-first-refund"

-- | The lovelace a refund tamper takes from the first refund, if any.
refundShortfall :: RefundTamper -> Maybe Integer
refundShortfall :: RefundTamper -> Maybe Integer
refundShortfall RefundTamper
CrossedRefunds = Maybe Integer
forall a. Maybe a
Nothing
refundShortfall (ShortFirstRefund Integer
lovelace) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
lovelace
refundShortfall (SplitFirstRefund Integer
lovelace) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
lovelace

-- | The refund tamper as the book reads it.
refundTamperReading :: RefundTamper -> String
refundTamperReading :: RefundTamper -> String
refundTamperReading RefundTamper
CrossedRefunds =
    String
"each owner refunded, in its refund's position, what the next request's owner is owed"
refundTamperReading (ShortFirstRefund Integer
lovelace) =
    String
"the first request's refund " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
lovelace String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" lovelace short"
refundTamperReading (SplitFirstRefund Integer
lovelace) =
    String
"the first request's refund "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
lovelace
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" lovelace short in its own position and two ada more in another output at the same owner's key"

{- | Who books a request and what it holds beyond the processing tip. A request
without a booking is booked by the runner's own wallet with the default
deposit.
-}
data Booking wal = Booking
    { forall wal. Booking wal -> wal
bookingOwner :: wal
    , forall wal. Booking wal -> Integer
bookingDeposit :: Integer
    }
    deriving stock (Booking wal -> Booking wal -> Bool
(Booking wal -> Booking wal -> Bool)
-> (Booking wal -> Booking wal -> Bool) -> Eq (Booking wal)
forall wal. Eq wal => Booking wal -> Booking wal -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall wal. Eq wal => Booking wal -> Booking wal -> Bool
== :: Booking wal -> Booking wal -> Bool
$c/= :: forall wal. Eq wal => Booking wal -> Booking wal -> Bool
/= :: Booking wal -> Booking wal -> Bool
Eq, Int -> Booking wal -> ShowS
[Booking wal] -> ShowS
Booking wal -> String
(Int -> Booking wal -> ShowS)
-> (Booking wal -> String)
-> ([Booking wal] -> ShowS)
-> Show (Booking wal)
forall wal. Show wal => Int -> Booking wal -> ShowS
forall wal. Show wal => [Booking wal] -> ShowS
forall wal. Show wal => Booking wal -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall wal. Show wal => Int -> Booking wal -> ShowS
showsPrec :: Int -> Booking wal -> ShowS
$cshow :: forall wal. Show wal => Booking wal -> String
show :: Booking wal -> String
$cshowList :: forall wal. Show wal => [Booking wal] -> ShowS
showList :: [Booking wal] -> ShowS
Show)

{- | Where a reject is placed: a fact about the submitted transaction, not a
tamper. The model gives a reject no admission, so its answer does not depend
on it; the chain is asked in the window the story names.
-}
data Placement = InProcessingWindow | InRetractionWindow | AfterTheWindows
    deriving stock (Placement -> Placement -> Bool
(Placement -> Placement -> Bool)
-> (Placement -> Placement -> Bool) -> Eq Placement
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Placement -> Placement -> Bool
== :: Placement -> Placement -> Bool
$c/= :: Placement -> Placement -> Bool
/= :: Placement -> Placement -> Bool
Eq, Int -> Placement -> ShowS
[Placement] -> ShowS
Placement -> String
(Int -> Placement -> ShowS)
-> (Placement -> String)
-> ([Placement] -> ShowS)
-> Show Placement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Placement -> ShowS
showsPrec :: Int -> Placement -> ShowS
$cshow :: Placement -> String
show :: Placement -> String
$cshowList :: [Placement] -> ShowS
showList :: [Placement] -> ShowS
Show, Int -> Placement
Placement -> Int
Placement -> [Placement]
Placement -> Placement
Placement -> Placement -> [Placement]
Placement -> Placement -> Placement -> [Placement]
(Placement -> Placement)
-> (Placement -> Placement)
-> (Int -> Placement)
-> (Placement -> Int)
-> (Placement -> [Placement])
-> (Placement -> Placement -> [Placement])
-> (Placement -> Placement -> [Placement])
-> (Placement -> Placement -> Placement -> [Placement])
-> Enum Placement
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 :: Placement -> Placement
succ :: Placement -> Placement
$cpred :: Placement -> Placement
pred :: Placement -> Placement
$ctoEnum :: Int -> Placement
toEnum :: Int -> Placement
$cfromEnum :: Placement -> Int
fromEnum :: Placement -> Int
$cenumFrom :: Placement -> [Placement]
enumFrom :: Placement -> [Placement]
$cenumFromThen :: Placement -> Placement -> [Placement]
enumFromThen :: Placement -> Placement -> [Placement]
$cenumFromTo :: Placement -> Placement -> [Placement]
enumFromTo :: Placement -> Placement -> [Placement]
$cenumFromThenTo :: Placement -> Placement -> Placement -> [Placement]
enumFromThenTo :: Placement -> Placement -> Placement -> [Placement]
Enum, Placement
Placement -> Placement -> Bounded Placement
forall a. a -> a -> Bounded a
$cminBound :: Placement
minBound :: Placement
$cmaxBound :: Placement
maxBound :: Placement
Bounded)

-- | The placement as the run log names it.
placementName :: Placement -> String
placementName :: Placement -> String
placementName Placement
InProcessingWindow = String
"in the processing window"
placementName Placement
InRetractionWindow = String
"in the owner's retraction window"
placementName Placement
AfterTheWindows = String
"after the windows"

-- | The placement as the book reads it.
placementReading :: Placement -> String
placementReading :: Placement -> String
placementReading Placement
InProcessingWindow = String
"while the request can still be folded"
placementReading Placement
InRetractionWindow = String
"while its owner can still retract it"
placementReading Placement
AfterTheWindows = String
"after its owner's retraction window has closed"

{- | The window a placement names, in POSIX milliseconds, for a request
submitted at @submittedAt@ under a registry's processing and retraction
times: from its start to its excluded end, open-ended after the windows.
-}
placementWindow
    :: Placement -> Integer -> Integer -> Integer -> (Integer, Maybe Integer)
placementWindow :: Placement
-> Integer -> Integer -> Integer -> (Integer, Maybe Integer)
placementWindow Placement
placement Integer
submittedAt Integer
processTime Integer
retractTime =
    case Placement
placement of
        Placement
InProcessingWindow -> (Integer
submittedAt, Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
processDeadline)
        Placement
InRetractionWindow -> (Integer
processDeadline, Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
retractDeadline)
        Placement
AfterTheWindows -> (Integer
retractDeadline, Maybe Integer
forall a. Maybe a
Nothing)
  where
    processDeadline :: Integer
processDeadline = Integer
submittedAt Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
processTime
    retractDeadline :: Integer
retractDeadline = Integer
processDeadline Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
retractTime

type Story reg wal step obs cmp =
    Specification.Story (LiveI reg wal step obs cmp)

data Context reg wal = Context reg wal

data LiveI reg wal step obs cmp result where
    Submit
        :: Exit -> reg -> EdgeRequest wal -> LiveI reg wal step obs cmp step
    Tamper
        :: Tamper
        -> Exit
        -> reg
        -> EdgeRequest wal
        -> LiveI reg wal step obs cmp step
    RejectWithin
        :: Placement
        -> Maybe Tamper
        -> reg
        -> EdgeRequest wal
        -> LiveI reg wal step obs cmp step
    Observe :: step -> LiveI reg wal step obs cmp obs
    Compare :: step -> obs -> LiveI reg wal step obs cmp cmp
    FoldBatch
        :: Maybe BatchTamper
        -> reg
        -> [EdgeRequest wal]
        -> LiveI reg wal step obs cmp cmp
    RejectBatchWithin
        :: Placement
        -> Maybe RefundTamper
        -> reg
        -> [(EdgeRequest wal, Maybe (Booking wal))]
        -> LiveI reg wal step obs cmp cmp

submit :: reg -> EdgeRequest wal -> Story reg wal step obs cmp step
submit :: forall reg wal step obs cmp.
reg -> EdgeRequest wal -> Story reg wal step obs cmp step
submit reg
registry EdgeRequest wal
request = LiveI reg wal step obs cmp step
-> Story (LiveI reg wal step obs cmp) step
forall (act :: * -> *) res. act res -> Story act res
action (Exit -> reg -> EdgeRequest wal -> LiveI reg wal step obs cmp step
forall reg wal step obs cmp.
Exit -> reg -> EdgeRequest wal -> LiveI reg wal step obs cmp step
Submit Exit
Fold reg
registry EdgeRequest wal
request)

tamper
    :: Tamper -> reg -> EdgeRequest wal -> Story reg wal step obs cmp step
tamper :: forall reg wal step obs cmp.
Tamper -> reg -> EdgeRequest wal -> Story reg wal step obs cmp step
tamper Tamper
alteration = Tamper
-> Exit
-> reg
-> EdgeRequest wal
-> Story reg wal step obs cmp step
forall reg wal step obs cmp.
Tamper
-> Exit
-> reg
-> EdgeRequest wal
-> Story reg wal step obs cmp step
tamperExit Tamper
alteration Exit
Fold

-- | A folder rejects the request in the window the placement names.
rejectWithin
    :: Placement -> reg -> EdgeRequest wal -> Story reg wal step obs cmp step
rejectWithin :: forall reg wal step obs cmp.
Placement
-> reg -> EdgeRequest wal -> Story reg wal step obs cmp step
rejectWithin Placement
placement reg
registry EdgeRequest wal
request =
    LiveI reg wal step obs cmp step
-> Story (LiveI reg wal step obs cmp) step
forall (act :: * -> *) res. act res -> Story act res
action (Placement
-> Maybe Tamper
-> reg
-> EdgeRequest wal
-> LiveI reg wal step obs cmp step
forall reg wal step obs cmp.
Placement
-> Maybe Tamper
-> reg
-> EdgeRequest wal
-> LiveI reg wal step obs cmp step
RejectWithin Placement
placement Maybe Tamper
forall a. Maybe a
Nothing reg
registry EdgeRequest wal
request)

-- | A folder rejects the request in that window, through a tampered transaction.
tamperRejectWithin
    :: Tamper
    -> Placement
    -> reg
    -> EdgeRequest wal
    -> Story reg wal step obs cmp step
tamperRejectWithin :: forall reg wal step obs cmp.
Tamper
-> Placement
-> reg
-> EdgeRequest wal
-> Story reg wal step obs cmp step
tamperRejectWithin Tamper
alteration Placement
placement reg
registry EdgeRequest wal
request =
    LiveI reg wal step obs cmp step
-> Story (LiveI reg wal step obs cmp) step
forall (act :: * -> *) res. act res -> Story act res
action (Placement
-> Maybe Tamper
-> reg
-> EdgeRequest wal
-> LiveI reg wal step obs cmp step
forall reg wal step obs cmp.
Placement
-> Maybe Tamper
-> reg
-> EdgeRequest wal
-> LiveI reg wal step obs cmp step
RejectWithin Placement
placement (Tamper -> Maybe Tamper
forall a. a -> Maybe a
Just Tamper
alteration) reg
registry EdgeRequest wal
request)

-- | The request's owner retracts it.
retract :: reg -> EdgeRequest wal -> Story reg wal step obs cmp step
retract :: forall reg wal step obs cmp.
reg -> EdgeRequest wal -> Story reg wal step obs cmp step
retract reg
registry EdgeRequest wal
request = LiveI reg wal step obs cmp step
-> Story (LiveI reg wal step obs cmp) step
forall (act :: * -> *) res. act res -> Story act res
action (Exit -> reg -> EdgeRequest wal -> LiveI reg wal step obs cmp step
forall reg wal step obs cmp.
Exit -> reg -> EdgeRequest wal -> LiveI reg wal step obs cmp step
Submit Exit
Retract reg
registry EdgeRequest wal
request)

-- | The request leaves by this exit through a transaction changed by the tamper.
tamperExit
    :: Tamper
    -> Exit
    -> reg
    -> EdgeRequest wal
    -> Story reg wal step obs cmp step
tamperExit :: forall reg wal step obs cmp.
Tamper
-> Exit
-> reg
-> EdgeRequest wal
-> Story reg wal step obs cmp step
tamperExit Tamper
alteration Exit
exit reg
registry EdgeRequest wal
request = LiveI reg wal step obs cmp step
-> Story (LiveI reg wal step obs cmp) step
forall (act :: * -> *) res. act res -> Story act res
action (Tamper
-> Exit
-> reg
-> EdgeRequest wal
-> LiveI reg wal step obs cmp step
forall reg wal step obs cmp.
Tamper
-> Exit
-> reg
-> EdgeRequest wal
-> LiveI reg wal step obs cmp step
Tamper Tamper
alteration Exit
exit reg
registry EdgeRequest wal
request)

{- | Fold these requests in one transaction, each on its own edge, and ask the
model the same batch: its @foldBatch@ question. The batch is submitted and asked
as one instruction; its answer is what the model and the chain each said.
-}
foldBatch
    :: reg -> [EdgeRequest wal] -> Story reg wal step obs cmp cmp
foldBatch :: forall reg wal step obs cmp.
reg -> [EdgeRequest wal] -> Story reg wal step obs cmp cmp
foldBatch reg
registry [EdgeRequest wal]
requests = LiveI reg wal step obs cmp cmp
-> Story (LiveI reg wal step obs cmp) cmp
forall (act :: * -> *) res. act res -> Story act res
action (Maybe BatchTamper
-> reg -> [EdgeRequest wal] -> LiveI reg wal step obs cmp cmp
forall reg wal step obs cmp.
Maybe BatchTamper
-> reg -> [EdgeRequest wal] -> LiveI reg wal step obs cmp cmp
FoldBatch Maybe BatchTamper
forall a. Maybe a
Nothing reg
registry [EdgeRequest wal]
requests)

{- | Fold these requests in one transaction changed by the batch tamper, and ask
the model the same batch, each request claiming what that transaction mints at
its key.
-}
tamperFoldBatch
    :: BatchTamper
    -> reg
    -> [EdgeRequest wal]
    -> Story reg wal step obs cmp cmp
tamperFoldBatch :: forall reg wal step obs cmp.
BatchTamper
-> reg -> [EdgeRequest wal] -> Story reg wal step obs cmp cmp
tamperFoldBatch BatchTamper
alteration reg
registry [EdgeRequest wal]
requests =
    LiveI reg wal step obs cmp cmp
-> Story (LiveI reg wal step obs cmp) cmp
forall (act :: * -> *) res. act res -> Story act res
action (Maybe BatchTamper
-> reg -> [EdgeRequest wal] -> LiveI reg wal step obs cmp cmp
forall reg wal step obs cmp.
Maybe BatchTamper
-> reg -> [EdgeRequest wal] -> LiveI reg wal step obs cmp cmp
FoldBatch (BatchTamper -> Maybe BatchTamper
forall a. a -> Maybe a
Just BatchTamper
alteration) reg
registry [EdgeRequest wal]
requests)

{- | A folder rejects these requests in one transaction, in the window the
placement names, and the model is asked the same batch: its @rejectBatch@
question.
-}
rejectBatchWithin
    :: Placement
    -> reg
    -> [EdgeRequest wal]
    -> Story reg wal step obs cmp cmp
rejectBatchWithin :: forall reg wal step obs cmp.
Placement
-> reg -> [EdgeRequest wal] -> Story reg wal step obs cmp cmp
rejectBatchWithin Placement
placement reg
registry [EdgeRequest wal]
requests =
    LiveI reg wal step obs cmp cmp
-> Story (LiveI reg wal step obs cmp) cmp
forall (act :: * -> *) res. act res -> Story act res
action
        ( Placement
-> Maybe RefundTamper
-> reg
-> [(EdgeRequest wal, Maybe (Booking wal))]
-> LiveI reg wal step obs cmp cmp
forall reg wal step obs cmp.
Placement
-> Maybe RefundTamper
-> reg
-> [(EdgeRequest wal, Maybe (Booking wal))]
-> LiveI reg wal step obs cmp cmp
RejectBatchWithin
            Placement
placement
            Maybe RefundTamper
forall a. Maybe a
Nothing
            reg
registry
            [(EdgeRequest wal
r, Maybe (Booking wal)
forall a. Maybe a
Nothing) | EdgeRequest wal
r <- [EdgeRequest wal]
requests]
        )

{- | A folder rejects these requests in one transaction, in the window the
placement names, each booked by the owner and with the deposit its booking
names, and the model is asked the same batch.
-}
rejectBookedBatchWithin
    :: Placement
    -> reg
    -> [(EdgeRequest wal, Booking wal)]
    -> Story reg wal step obs cmp cmp
rejectBookedBatchWithin :: forall reg wal step obs cmp.
Placement
-> reg
-> [(EdgeRequest wal, Booking wal)]
-> Story reg wal step obs cmp cmp
rejectBookedBatchWithin Placement
placement reg
registry [(EdgeRequest wal, Booking wal)]
requests =
    LiveI reg wal step obs cmp cmp
-> Story (LiveI reg wal step obs cmp) cmp
forall (act :: * -> *) res. act res -> Story act res
action
        ( Placement
-> Maybe RefundTamper
-> reg
-> [(EdgeRequest wal, Maybe (Booking wal))]
-> LiveI reg wal step obs cmp cmp
forall reg wal step obs cmp.
Placement
-> Maybe RefundTamper
-> reg
-> [(EdgeRequest wal, Maybe (Booking wal))]
-> LiveI reg wal step obs cmp cmp
RejectBatchWithin
            Placement
placement
            Maybe RefundTamper
forall a. Maybe a
Nothing
            reg
registry
            [(EdgeRequest wal
r, Booking wal -> Maybe (Booking wal)
forall a. a -> Maybe a
Just Booking wal
booking) | (EdgeRequest wal
r, Booking wal
booking) <- [(EdgeRequest wal, Booking wal)]
requests]
        )

{- | A folder rejects these booked requests in one transaction changed by the
refund tamper, and the model is asked the same batch, judged on the refunds
that transaction pays.
-}
tamperRejectBookedBatchWithin
    :: RefundTamper
    -> Placement
    -> reg
    -> [(EdgeRequest wal, Booking wal)]
    -> Story reg wal step obs cmp cmp
tamperRejectBookedBatchWithin :: forall reg wal step obs cmp.
RefundTamper
-> Placement
-> reg
-> [(EdgeRequest wal, Booking wal)]
-> Story reg wal step obs cmp cmp
tamperRejectBookedBatchWithin RefundTamper
alteration Placement
placement reg
registry [(EdgeRequest wal, Booking wal)]
requests =
    LiveI reg wal step obs cmp cmp
-> Story (LiveI reg wal step obs cmp) cmp
forall (act :: * -> *) res. act res -> Story act res
action
        ( Placement
-> Maybe RefundTamper
-> reg
-> [(EdgeRequest wal, Maybe (Booking wal))]
-> LiveI reg wal step obs cmp cmp
forall reg wal step obs cmp.
Placement
-> Maybe RefundTamper
-> reg
-> [(EdgeRequest wal, Maybe (Booking wal))]
-> LiveI reg wal step obs cmp cmp
RejectBatchWithin
            Placement
placement
            (RefundTamper -> Maybe RefundTamper
forall a. a -> Maybe a
Just RefundTamper
alteration)
            reg
registry
            [(EdgeRequest wal
r, Booking wal -> Maybe (Booking wal)
forall a. a -> Maybe a
Just Booking wal
booking) | (EdgeRequest wal
r, Booking wal
booking) <- [(EdgeRequest wal, Booking wal)]
requests]
        )

observe :: step -> Story reg wal step obs cmp obs
observe :: forall step reg wal obs cmp. step -> Story reg wal step obs cmp obs
observe = LiveI reg wal step obs cmp obs
-> Story (LiveI reg wal step obs cmp) obs
forall (act :: * -> *) res. act res -> Story act res
action (LiveI reg wal step obs cmp obs
 -> Story (LiveI reg wal step obs cmp) obs)
-> (step -> LiveI reg wal step obs cmp obs)
-> step
-> Story (LiveI reg wal step obs cmp) obs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. step -> LiveI reg wal step obs cmp obs
forall step reg wal obs cmp. step -> LiveI reg wal step obs cmp obs
Observe

compareWithModel :: step -> obs -> Story reg wal step obs cmp cmp
compareWithModel :: forall step obs reg wal cmp.
step -> obs -> Story reg wal step obs cmp cmp
compareWithModel step
step obs
observation = LiveI reg wal step obs cmp cmp
-> Story (LiveI reg wal step obs cmp) cmp
forall (act :: * -> *) res. act res -> Story act res
action (step -> obs -> LiveI reg wal step obs cmp cmp
forall step obs reg wal cmp.
step -> obs -> LiveI reg wal step obs cmp cmp
Compare step
step obs
observation)

{- | Check instruction order over the same program with display-only handles,
before a runner can submit a transaction.
-}
validateLive
    :: Story String String String String String res -> Either String ()
validateLive :: forall res.
Story String String String String String res -> Either String ()
validateLive Story String String String String String res
program = do
    (end, _) <- PreflightPhase
-> Story String String String String String res
-> Either String (PreflightPhase, res)
forall a.
PreflightPhase
-> Story String String String String String a
-> Either String (PreflightPhase, a)
walk PreflightPhase
Ready Story String String String String String res
program
    if end == Ready
        then Right ()
        else Left "live story ended before Observe and Compare"
  where
    walk
        :: PreflightPhase
        -> Story String String String String String a
        -> Either String (PreflightPhase, a)
    walk :: forall a.
PreflightPhase
-> Story String String String String String a
-> Either String (PreflightPhase, a)
walk PreflightPhase
phase Story String String String String String a
body = case Story String String String String String a
-> ProgramView (Step (LiveI String String String String String)) a
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view Story String String String String String a
body of
        Return a
result -> (PreflightPhase, a) -> Either String (PreflightPhase, a)
forall a b. b -> Either a b
Right (PreflightPhase
phase, a
result)
        Action LiveI String String String String String b
instruction :>>= b -> Story String String String String String a
rest -> case LiveI String String String String String b
instruction of
            Submit Exit
Reject String
_ EdgeRequest String
_ -> String -> Either String (PreflightPhase, a)
forall a b. a -> Either a b
Left String
unplaced
            Submit{} -> PreflightPhase
-> PreflightPhase -> b -> Either String (PreflightPhase, a)
advance PreflightPhase
Ready PreflightPhase
NeedObserve b
"preflight step"
            Tamper Tamper
_ Exit
Reject String
_ EdgeRequest String
_ -> String -> Either String (PreflightPhase, a)
forall a b. a -> Either a b
Left String
unplaced
            Tamper{} -> PreflightPhase
-> PreflightPhase -> b -> Either String (PreflightPhase, a)
advance PreflightPhase
Ready PreflightPhase
NeedObserve b
"preflight step"
            RejectWithin{} -> PreflightPhase
-> PreflightPhase -> b -> Either String (PreflightPhase, a)
advance PreflightPhase
Ready PreflightPhase
NeedObserve b
"preflight step"
            Observe String
_ -> PreflightPhase
-> PreflightPhase -> b -> Either String (PreflightPhase, a)
advance PreflightPhase
NeedObserve PreflightPhase
NeedCompare b
"preflight observation"
            Compare String
_ String
_ -> PreflightPhase
-> PreflightPhase -> b -> Either String (PreflightPhase, a)
advance PreflightPhase
NeedCompare PreflightPhase
Ready b
"preflight comparison"
            FoldBatch{} -> b -> Either String (PreflightPhase, a)
batch b
"preflight batch"
            RejectBatchWithin Placement
_ Maybe RefundTamper
alteration String
_ [(EdgeRequest String, Maybe (Booking String))]
requests ->
                case Maybe RefundTamper
-> [(EdgeRequest String, Maybe (Booking String))] -> Maybe String
forall wal.
Maybe RefundTamper
-> [(EdgeRequest wal, Maybe (Booking wal))] -> Maybe String
refundProblem Maybe RefundTamper
alteration [(EdgeRequest String, Maybe (Booking String))]
requests of
                    Just String
problem -> String -> Either String (PreflightPhase, a)
forall a b. a -> Either a b
Left String
problem
                    Maybe String
Nothing -> b -> Either String (PreflightPhase, a)
batch b
"preflight batch"
          where
            advance :: PreflightPhase
-> PreflightPhase -> b -> Either String (PreflightPhase, a)
advance PreflightPhase
expected PreflightPhase
nextPhase b
value
                | PreflightPhase
phase PreflightPhase -> PreflightPhase -> Bool
forall a. Eq a => a -> a -> Bool
== PreflightPhase
expected = PreflightPhase
-> Story String String String String String a
-> Either String (PreflightPhase, a)
forall a.
PreflightPhase
-> Story String String String String String a
-> Either String (PreflightPhase, a)
walk PreflightPhase
nextPhase (b -> Story String String String String String a
rest b
value)
                | Bool
otherwise =
                    String -> Either String (PreflightPhase, a)
forall a b. a -> Either a b
Left String
"live story must Submit or Tamper, Observe, then Compare"
            unplaced :: String
unplaced =
                String
"a live story's reject must name the window it is placed in"
            -- A batch is submitted and asked as one instruction, so it stands
            -- between complete steps, never inside one.
            batch :: b -> Either String (PreflightPhase, a)
batch b
value
                | PreflightPhase
phase PreflightPhase -> PreflightPhase -> Bool
forall a. Eq a => a -> a -> Bool
== PreflightPhase
Ready = PreflightPhase
-> Story String String String String String a
-> Either String (PreflightPhase, a)
forall a.
PreflightPhase
-> Story String String String String String a
-> Either String (PreflightPhase, a)
walk PreflightPhase
Ready (b -> Story String String String String String a
rest b
value)
                | Bool
otherwise =
                    String -> Either String (PreflightPhase, a)
forall a b. a -> Either a b
Left
                        String
"a live story's batch stands between complete steps, not inside one"
        Theorem Theorem thm
_ TheoremStory thm (LiveI String String String String String) b
body' :>>= b -> Story String String String String String a
rest -> do
            (afterClauses, result) <-
                PreflightPhase
-> Program
     (Clause thm (LiveI String String String String String)) b
-> Either String (PreflightPhase, b)
forall {k} (thm :: k) a.
PreflightPhase
-> Program
     (Clause thm (LiveI String String String String String)) a
-> Either String (PreflightPhase, a)
walkClauses PreflightPhase
phase (TheoremStory thm (LiveI String String String String String) b
-> Program
     (Clause thm (LiveI String String String String String)) b
forall {k} (thm :: k) (act :: * -> *) res.
TheoremStory thm act res -> Program (Clause thm act) res
Specification.clauses TheoremStory thm (LiveI String String String String String) b
body')
            walk afterClauses (rest result)
    walkClauses
        :: PreflightPhase
        -> Program (Clause thm (LiveI String String String String String)) a
        -> Either String (PreflightPhase, a)
    walkClauses :: forall {k} (thm :: k) a.
PreflightPhase
-> Program
     (Clause thm (LiveI String String String String String)) a
-> Either String (PreflightPhase, a)
walkClauses PreflightPhase
phase Program (Clause thm (LiveI String String String String String)) a
body = case Program (Clause thm (LiveI String String String String String)) a
-> ProgramView
     (Clause thm (LiveI String String String String String)) a
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view Program (Clause thm (LiveI String String String String String)) a
body of
        Return a
result -> (PreflightPhase, a) -> Either String (PreflightPhase, a)
forall a b. b -> Either a b
Right (PreflightPhase
phase, a
result)
        Clause String
_ LeanCheck (LiveI String String String String String) thm b
check Story (LiveI String String String String String) b
actions :>>= b
-> Program
     (Clause thm (LiveI String String String String String)) a
rest -> do
            (afterActions, observation) <- PreflightPhase
-> Story (LiveI String String String String String) b
-> Either String (PreflightPhase, b)
forall a.
PreflightPhase
-> Story String String String String String a
-> Either String (PreflightPhase, a)
walk PreflightPhase
phase Story (LiveI String String String String String) b
actions
            (afterCheck, ()) <-
                walk afterActions (Specification.checkAction check observation)
            walkClauses afterCheck (rest observation)

data PreflightPhase = Ready | NeedObserve | NeedCompare
    deriving stock (PreflightPhase -> PreflightPhase -> Bool
(PreflightPhase -> PreflightPhase -> Bool)
-> (PreflightPhase -> PreflightPhase -> Bool) -> Eq PreflightPhase
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PreflightPhase -> PreflightPhase -> Bool
== :: PreflightPhase -> PreflightPhase -> Bool
$c/= :: PreflightPhase -> PreflightPhase -> Bool
/= :: PreflightPhase -> PreflightPhase -> Bool
Eq)

{- | Why a reject batch's bookings or refund tamper cannot be built, if they
cannot: a deposit must be positive, a shortfall positive, a crossed allocation
needs two requests to cross, and a tampered first refund needs a first request.
-}
refundProblem
    :: Maybe RefundTamper
    -> [(EdgeRequest wal, Maybe (Booking wal))]
    -> Maybe String
refundProblem :: forall wal.
Maybe RefundTamper
-> [(EdgeRequest wal, Maybe (Booking wal))] -> Maybe String
refundProblem Maybe RefundTamper
alteration [(EdgeRequest wal, Maybe (Booking wal))]
requests
    | (Booking wal -> Bool) -> [Booking wal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0) (Integer -> Bool)
-> (Booking wal -> Integer) -> Booking wal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Booking wal -> Integer
forall wal. Booking wal -> Integer
bookingDeposit) [Booking wal
b | (EdgeRequest wal
_, Just Booking wal
b) <- [(EdgeRequest wal, Maybe (Booking wal))]
requests] =
        String -> Maybe String
forall a. a -> Maybe a
Just String
"a booked request's deposit must be positive"
    | Bool
otherwise = case Maybe RefundTamper
alteration of
        Maybe RefundTamper
Nothing -> Maybe String
forall a. Maybe a
Nothing
        Just RefundTamper
CrossedRefunds
            | [(EdgeRequest wal, Maybe (Booking wal))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(EdgeRequest wal, Maybe (Booking wal))]
requests Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 ->
                String -> Maybe String
forall a. a -> Maybe a
Just String
"crossed refunds need two requests to cross"
        Just RefundTamper
changed
            | Just Integer
lovelace <- RefundTamper -> Maybe Integer
refundShortfall RefundTamper
changed
            , Integer
lovelace Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 ->
                String -> Maybe String
forall a. a -> Maybe a
Just String
"a refund's shortfall must be positive"
            | [(EdgeRequest wal, Maybe (Booking wal))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(EdgeRequest wal, Maybe (Booking wal))]
requests -> String -> Maybe String
forall a. a -> Maybe a
Just String
"a tampered refund needs a request to refund"
        Maybe RefundTamper
_ -> Maybe String
forall a. Maybe a
Nothing

renderLive :: Story String String String String String res -> String
renderLive :: forall res. Story String String String String String res -> String
renderLive = (String, res) -> String
forall a b. (a, b) -> a
fst ((String, res) -> String)
-> (Story String String String String String res -> (String, res))
-> Story String String String String String res
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Story String String String String String res -> (String, res)
forall res.
Story String String String String String res -> (String, res)
renderWithResult

renderWithResult
    :: Story String String String String String res -> (String, res)
renderWithResult :: forall res.
Story String String String String String res -> (String, res)
renderWithResult Story String String String String String res
program = case Story String String String String String res
-> ProgramView
     (Step (LiveI String String String String String)) res
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view Story String String String String String res
program of
    Return res
result -> (String
"", res
result)
    Action LiveI String String String String String b
instruction :>>= b -> Story String String String String String res
rest -> LiveI String String String String String b
-> (b -> Story String String String String String res)
-> (String, res)
forall obs res.
LiveI String String String String String obs
-> (obs -> Story String String String String String res)
-> (String, res)
renderAction LiveI String String String String String b
instruction b -> Story String String String String String res
rest
    Theorem Theorem thm
binding TheoremStory thm (LiveI String String String String String) b
body :>>= b -> Story String String String String String res
rest ->
        let (String
text, b
result) = TheoremStory thm (LiveI String String String String String) b
-> (String, b)
forall {k} (thm :: k) res.
TheoremStory thm (LiveI String String String String String) res
-> (String, res)
renderClauses TheoremStory thm (LiveI String String String String String) b
body
        in  String -> (String, res) -> (String, res)
forall res. String -> (String, res) -> (String, res)
prepend
                (Binding -> String
formal (Theorem thm -> Binding
forall {k} (thm :: k). Theorem thm -> Binding
theoremBinding Theorem thm
binding) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
text)
                (Story String String String String String res -> (String, res)
forall res.
Story String String String String String res -> (String, res)
renderWithResult (b -> Story String String String String String res
rest b
result))

renderClauses
    :: TheoremStory thm (LiveI String String String String String) res
    -> (String, res)
renderClauses :: forall {k} (thm :: k) res.
TheoremStory thm (LiveI String String String String String) res
-> (String, res)
renderClauses = Program (Clause thm (LiveI String String String String String)) res
-> (String, res)
forall {k} (thm :: k) res.
Program (Clause thm (LiveI String String String String String)) res
-> (String, res)
renderClauseProgram (Program
   (Clause thm (LiveI String String String String String)) res
 -> (String, res))
-> (TheoremStory thm (LiveI String String String String String) res
    -> Program
         (Clause thm (LiveI String String String String String)) res)
-> TheoremStory thm (LiveI String String String String String) res
-> (String, res)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheoremStory thm (LiveI String String String String String) res
-> Program
     (Clause thm (LiveI String String String String String)) res
forall {k} (thm :: k) (act :: * -> *) res.
TheoremStory thm act res -> Program (Clause thm act) res
clauses

renderClauseProgram
    :: Program (Clause thm (LiveI String String String String String)) res
    -> (String, res)
renderClauseProgram :: forall {k} (thm :: k) res.
Program (Clause thm (LiveI String String String String String)) res
-> (String, res)
renderClauseProgram Program (Clause thm (LiveI String String String String String)) res
program = case Program (Clause thm (LiveI String String String String String)) res
-> ProgramView
     (Clause thm (LiveI String String String String String)) res
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view Program (Clause thm (LiveI String String String String String)) res
program of
    Return res
result -> (String
"", res
result)
    Clause String
title LeanCheck (LiveI String String String String String) thm b
check Story (LiveI String String String String String) b
body :>>= b
-> Program
     (Clause thm (LiveI String String String String String)) res
rest ->
        let (String
text, b
result) = Story (LiveI String String String String String) b -> (String, b)
forall res.
Story String String String String String res -> (String, res)
renderWithResult Story (LiveI String String String String String) b
body
            (String
checked, ()) = Story String String String String String () -> (String, ())
forall res.
Story String String String String String res -> (String, res)
renderWithResult (LeanCheck (LiveI String String String String String) thm b
-> b -> Story String String String String String ()
forall {k} (act :: * -> *) (thm :: k) obs.
LeanCheck act thm obs -> obs -> Story act ()
checkAction LeanCheck (LiveI String String String String String) thm b
check b
result)
        in  String -> (String, res) -> (String, res)
forall res. String -> (String, res) -> (String, res)
prepend
                (String
"### " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
title String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n\n" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
text String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
checked)
                (Program (Clause thm (LiveI String String String String String)) res
-> (String, res)
forall {k} (thm :: k) res.
Program (Clause thm (LiveI String String String String String)) res
-> (String, res)
renderClauseProgram (b
-> Program
     (Clause thm (LiveI String String String String String)) res
rest b
result))

renderAction
    :: LiveI String String String String String obs
    -> (obs -> Story String String String String String res)
    -> (String, res)
renderAction :: forall obs res.
LiveI String String String String String obs
-> (obs -> Story String String String String String res)
-> (String, res)
renderAction LiveI String String String String String obs
instruction obs -> Story String String String String String res
rest = case LiveI String String String String String obs
instruction of
    Submit Exit
exit String
registry EdgeRequest String
request ->
        String
-> Story String String String String String res -> (String, res)
forall {res}.
String
-> Story String String String String String res -> (String, res)
step
            ( Exit -> String -> EdgeRequest String -> String
forall {wal}. Exit -> String -> EdgeRequest wal -> String
subject Exit
exit String
registry EdgeRequest String
request
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", using the "
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest String -> String
forall wal. EdgeRequest wal -> wal
requestWallet EdgeRequest String
request
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"."
            )
            (obs -> Story String String String String String res
rest (EdgeRequest String -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest String
request))
    Tamper Tamper
alteration Exit
exit String
registry EdgeRequest String
request ->
        String
-> Story String String String String String res -> (String, res)
forall {res}.
String
-> Story String String String String String res -> (String, res)
step
            (Exit -> String -> EdgeRequest String -> String
forall {wal}. Exit -> String -> EdgeRequest wal -> String
subject Exit
exit String
registry EdgeRequest String
request String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Tamper -> String
altered Tamper
alteration)
            (obs -> Story String String String String String res
rest (EdgeRequest String -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest String
request))
    RejectWithin Placement
placement Maybe Tamper
alteration String
registry EdgeRequest String
request ->
        String
-> Story String String String String String res -> (String, res)
forall {res}.
String
-> Story String String String String String res -> (String, res)
step
            ( String
"Reject the "
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest String -> ShowS
forall {wal}. EdgeRequest wal -> ShowS
named EdgeRequest String
request String
registry
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" "
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Placement -> String
placementReading Placement
placement
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> (Tamper -> String) -> Maybe Tamper -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
                    (String
", using the " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest String -> String
forall wal. EdgeRequest wal -> wal
requestWallet EdgeRequest String
request String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
".")
                    Tamper -> String
altered
                    Maybe Tamper
alteration
            )
            (obs -> Story String String String String String res
rest (EdgeRequest String -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest String
request))
    Observe String
handle ->
        String
-> Story String String String String String res -> (String, res)
forall {res}.
String
-> Story String String String String String res -> (String, res)
step
            ( String
"Observe the complete registry, token, leaf and transaction boundary after **"
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
handle
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"**."
            )
            (obs -> Story String String String String String res
rest (obs
"observations for " obs -> obs -> obs
forall a. Semigroup a => a -> a -> a
<> obs
String
handle))
    Compare String
handle String
_ ->
        String
-> Story String String String String String res -> (String, res)
forall {res}.
String
-> Story String String String String String res -> (String, res)
step
            ( String
"Compare **"
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
handle
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"** and its observation with the executable registry model."
            )
            (obs -> Story String String String String String res
rest (obs
"comparison for " obs -> obs -> obs
forall a. Semigroup a => a -> a -> a
<> obs
String
handle))
    FoldBatch Maybe BatchTamper
alteration String
registry [EdgeRequest String]
requests ->
        String
-> Story String String String String String res -> (String, res)
forall {res}.
String
-> Story String String String String String res -> (String, res)
step
            ( String
"Fold, in one transaction"
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> (BatchTamper -> String) -> Maybe BatchTamper -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
                    String
""
                    (\BatchTamper
changed -> String
" with " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> BatchTamper -> String
batchTamperReading BatchTamper
changed)
                    Maybe BatchTamper
alteration
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", "
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [EdgeRequest String] -> ShowS
batched [EdgeRequest String]
requests String
registry
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", and ask the executable registry model the same batch."
            )
            (obs -> Story String String String String String res
rest (obs
"batch in " obs -> obs -> obs
forall a. Semigroup a => a -> a -> a
<> obs
String
registry))
    RejectBatchWithin Placement
placement Maybe RefundTamper
alteration String
registry [(EdgeRequest String, Maybe (Booking String))]
requests ->
        String
-> Story String String String String String res -> (String, res)
forall {res}.
String
-> Story String String String String String res -> (String, res)
step
            ( String
"Reject, in one transaction "
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Placement -> String
placementReading Placement
placement
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> (RefundTamper -> String) -> Maybe RefundTamper -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
                    String
""
                    (\RefundTamper
changed -> String
" with " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> RefundTamper -> String
refundTamperReading RefundTamper
changed)
                    Maybe RefundTamper
alteration
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", "
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [EdgeRequest String] -> ShowS
batched (((EdgeRequest String, Maybe (Booking String))
 -> EdgeRequest String)
-> [(EdgeRequest String, Maybe (Booking String))]
-> [EdgeRequest String]
forall a b. (a -> b) -> [a] -> [b]
map (EdgeRequest String, Maybe (Booking String)) -> EdgeRequest String
forall a b. (a, b) -> a
fst [(EdgeRequest String, Maybe (Booking String))]
requests) String
registry
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(EdgeRequest String, Maybe (Booking String))] -> String
forall {wal}. [(EdgeRequest wal, Maybe (Booking String))] -> String
booked [(EdgeRequest String, Maybe (Booking String))]
requests
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
", and ask the executable registry model the same batch."
            )
            (obs -> Story String String String String String res
rest (obs
"batch in " obs -> obs -> obs
forall a. Semigroup a => a -> a -> a
<> obs
String
registry))
  where
    step :: String
-> Story String String String String String res -> (String, res)
step String
sentence Story String String String String String res
next = String -> (String, res) -> (String, res)
forall res. String -> (String, res) -> (String, res)
prepend (String
"- " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
sentence String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\n\n") (Story String String String String String res -> (String, res)
forall res.
Story String String String String String res -> (String, res)
renderWithResult Story String String String String String res
next)
    named :: EdgeRequest wal -> ShowS
named EdgeRequest wal
request String
registry =
        String
"**"
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Edge -> String
edgeName (EdgeRequest wal -> Edge
forall wal. EdgeRequest wal -> Edge
requestEdge EdgeRequest wal
request)
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"** for **"
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest wal -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest wal
request
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"** in **"
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
registry
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"**"
    -- Every request of a batch is named, in order; an empty batch says so.
    batched :: [EdgeRequest String] -> ShowS
batched [] String
registry = String
"no request in **" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
registry String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"**"
    batched [EdgeRequest String]
requests String
registry =
        String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate
            String
", "
            [ String
"**"
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Edge -> String
edgeName (EdgeRequest String -> Edge
forall wal. EdgeRequest wal -> Edge
requestEdge EdgeRequest String
request)
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"** for **"
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest String -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest String
request
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"**"
            | EdgeRequest String
request <- [EdgeRequest String]
requests
            ]
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" in **"
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
registry
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"**, using "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((EdgeRequest String -> String) -> [EdgeRequest String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"the " String -> ShowS
forall a. Semigroup a => a -> a -> a
<>) ShowS
-> (EdgeRequest String -> String) -> EdgeRequest String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EdgeRequest String -> String
forall wal. EdgeRequest wal -> wal
requestWallet) [EdgeRequest String]
requests)
    -- Who booked each request and what it holds, when the story names it.
    booked :: [(EdgeRequest wal, Maybe (Booking String))] -> String
booked [(EdgeRequest wal, Maybe (Booking String))]
requests = case [ String
"**"
                                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest wal -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest wal
request
                                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"** by the "
                                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Booking String -> String
forall wal. Booking wal -> wal
bookingOwner Booking String
booking
                                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" with a deposit of "
                                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show (Booking String -> Integer
forall wal. Booking wal -> Integer
bookingDeposit Booking String
booking)
                                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" lovelace"
                           | (EdgeRequest wal
request, Just Booking String
booking) <- [(EdgeRequest wal, Maybe (Booking String))]
requests
                           ] of
        [] -> String
""
        [String]
bookings -> String
", booked " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
bookings
    subject :: Exit -> String -> EdgeRequest wal -> String
subject Exit
Fold String
registry EdgeRequest wal
request = String
"Submit " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest wal -> ShowS
forall {wal}. EdgeRequest wal -> ShowS
named EdgeRequest wal
request String
registry
    subject Exit
Reject String
registry EdgeRequest wal
request =
        String
"Reject the "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest wal -> ShowS
forall {wal}. EdgeRequest wal -> ShowS
named EdgeRequest wal
request String
registry
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" with no placement, which story validation refuses"
    subject Exit
Retract String
registry EdgeRequest wal
request = String
"Retract the " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> EdgeRequest wal -> ShowS
forall {wal}. EdgeRequest wal -> ShowS
named EdgeRequest wal
request String
registry String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" as its owner"
    refused :: String
refused =
        String
" The ledger and the model must both refuse it; the same request untampered is its control."
    altered :: Tamper -> String
altered Tamper
OtherAddress = String
" with the payment it owes sent to another address." String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
refused
    altered Tamper
ShortByOne = String
" with the payment it owes one lovelace short." String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
refused
    altered Tamper
OtherReference =
        String
" with its return bound to another request's output reference."
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
refused
    altered Tamper
StateSpent = String
" spending the registry's state beside it." String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
refused
    altered Tamper
Unsigned =
        String
" without requiring its owner's signature; the ledger and the model must refuse it, with the owner-signed retraction of that request as its control."
    altered Tamper
BeforePhase2 =
        String
" with a finite validity interval before phase 2; the ledger and the model must refuse it, with the same request retracted inside phase 2 as its control."
    altered Tamper
AfterPhase2 =
        String
" with a finite validity interval after phase 2; the ledger and the model must refuse it, with the earlier in-window retraction of its owner's other request as its control."
    altered Tamper
ExtraSigner =
        String
" with one required signer the model does not require. The ledger accepts it; the comparison must report the difference in the transaction's signers."

-- | What one instruction of a program is.
data InstructionKind
    = StepInstruction
    | ObserveInstruction
    | CompareInstruction
    | BatchInstruction
    deriving stock (InstructionKind -> InstructionKind -> Bool
(InstructionKind -> InstructionKind -> Bool)
-> (InstructionKind -> InstructionKind -> Bool)
-> Eq InstructionKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InstructionKind -> InstructionKind -> Bool
== :: InstructionKind -> InstructionKind -> Bool
$c/= :: InstructionKind -> InstructionKind -> Bool
/= :: InstructionKind -> InstructionKind -> Bool
Eq, Int -> InstructionKind -> ShowS
[InstructionKind] -> ShowS
InstructionKind -> String
(Int -> InstructionKind -> ShowS)
-> (InstructionKind -> String)
-> ([InstructionKind] -> ShowS)
-> Show InstructionKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InstructionKind -> ShowS
showsPrec :: Int -> InstructionKind -> ShowS
$cshow :: InstructionKind -> String
show :: InstructionKind -> String
$cshowList :: [InstructionKind] -> ShowS
showList :: [InstructionKind] -> ShowS
Show)

-- | One instruction of a program, with the tamper it carries, if any.
data Instruction = Instruction
    { Instruction -> InstructionKind
instructionKind :: InstructionKind
    , Instruction -> Maybe String
instructionTamper :: Maybe String
    -- ^ the name of the tamper, batch tamper or refund tamper
    }
    deriving stock (Instruction -> Instruction -> Bool
(Instruction -> Instruction -> Bool)
-> (Instruction -> Instruction -> Bool) -> Eq Instruction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Instruction -> Instruction -> Bool
== :: Instruction -> Instruction -> Bool
$c/= :: Instruction -> Instruction -> Bool
/= :: Instruction -> Instruction -> Bool
Eq, Int -> Instruction -> ShowS
[Instruction] -> ShowS
Instruction -> String
(Int -> Instruction -> ShowS)
-> (Instruction -> String)
-> ([Instruction] -> ShowS)
-> Show Instruction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Instruction -> ShowS
showsPrec :: Int -> Instruction -> ShowS
$cshow :: Instruction -> String
show :: Instruction -> String
$cshowList :: [Instruction] -> ShowS
showList :: [Instruction] -> ShowS
Show)

{- | Every instruction of a program over display handles, in order, theorem
clauses included. The walk feeds each instruction the result the book's
renderer feeds it, so it meets the instructions the book prints.
-}
liveInstructions
    :: Story String String String String String res -> [Instruction]
liveInstructions :: forall res.
Story String String String String String res -> [Instruction]
liveInstructions = ([Instruction], res) -> [Instruction]
forall a b. (a, b) -> a
fst (([Instruction], res) -> [Instruction])
-> (Story String String String String String res
    -> ([Instruction], res))
-> Story String String String String String res
-> [Instruction]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Story String String String String String res
-> ([Instruction], res)
forall res.
Story String String String String String res
-> ([Instruction], res)
instructionsWithResult

instructionsWithResult
    :: Story String String String String String res -> ([Instruction], res)
instructionsWithResult :: forall res.
Story String String String String String res
-> ([Instruction], res)
instructionsWithResult Story String String String String String res
program = case Story String String String String String res
-> ProgramView
     (Step (LiveI String String String String String)) res
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view Story String String String String String res
program of
    Return res
result -> ([], res
result)
    Action LiveI String String String String String b
instruction :>>= b -> Story String String String String String res
rest -> case LiveI String String String String String b
instruction of
        Submit Exit
_ String
_ EdgeRequest String
request ->
            InstructionKind
-> Maybe String
-> Story String String String String String res
-> ([Instruction], res)
forall {b}.
InstructionKind
-> Maybe String
-> Story String String String String String b
-> ([Instruction], b)
one InstructionKind
StepInstruction Maybe String
forall a. Maybe a
Nothing (b -> Story String String String String String res
rest (EdgeRequest String -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest String
request))
        Tamper Tamper
alteration Exit
_ String
_ EdgeRequest String
request ->
            InstructionKind
-> Maybe String
-> Story String String String String String res
-> ([Instruction], res)
forall {b}.
InstructionKind
-> Maybe String
-> Story String String String String String b
-> ([Instruction], b)
one
                InstructionKind
StepInstruction
                (String -> Maybe String
forall a. a -> Maybe a
Just (Tamper -> String
tamperName Tamper
alteration))
                (b -> Story String String String String String res
rest (EdgeRequest String -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest String
request))
        RejectWithin Placement
_ Maybe Tamper
alteration String
_ EdgeRequest String
request ->
            InstructionKind
-> Maybe String
-> Story String String String String String res
-> ([Instruction], res)
forall {b}.
InstructionKind
-> Maybe String
-> Story String String String String String b
-> ([Instruction], b)
one
                InstructionKind
StepInstruction
                (Tamper -> String
tamperName (Tamper -> String) -> Maybe Tamper -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Tamper
alteration)
                (b -> Story String String String String String res
rest (EdgeRequest String -> String
forall wal. EdgeRequest wal -> String
requestKey EdgeRequest String
request))
        Observe String
handle ->
            InstructionKind
-> Maybe String
-> Story String String String String String res
-> ([Instruction], res)
forall {b}.
InstructionKind
-> Maybe String
-> Story String String String String String b
-> ([Instruction], b)
one InstructionKind
ObserveInstruction Maybe String
forall a. Maybe a
Nothing (b -> Story String String String String String res
rest (b
"observations for " b -> b -> b
forall a. Semigroup a => a -> a -> a
<> b
String
handle))
        Compare String
handle String
_ ->
            InstructionKind
-> Maybe String
-> Story String String String String String res
-> ([Instruction], res)
forall {b}.
InstructionKind
-> Maybe String
-> Story String String String String String b
-> ([Instruction], b)
one InstructionKind
CompareInstruction Maybe String
forall a. Maybe a
Nothing (b -> Story String String String String String res
rest (b
"comparison for " b -> b -> b
forall a. Semigroup a => a -> a -> a
<> b
String
handle))
        FoldBatch Maybe BatchTamper
alteration String
registry [EdgeRequest String]
_ ->
            InstructionKind
-> Maybe String
-> Story String String String String String res
-> ([Instruction], res)
forall {b}.
InstructionKind
-> Maybe String
-> Story String String String String String b
-> ([Instruction], b)
one
                InstructionKind
BatchInstruction
                (BatchTamper -> String
batchTamperName (BatchTamper -> String) -> Maybe BatchTamper -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe BatchTamper
alteration)
                (b -> Story String String String String String res
rest (b
"batch in " b -> b -> b
forall a. Semigroup a => a -> a -> a
<> b
String
registry))
        RejectBatchWithin Placement
_ Maybe RefundTamper
alteration String
registry [(EdgeRequest String, Maybe (Booking String))]
_ ->
            InstructionKind
-> Maybe String
-> Story String String String String String res
-> ([Instruction], res)
forall {b}.
InstructionKind
-> Maybe String
-> Story String String String String String b
-> ([Instruction], b)
one
                InstructionKind
BatchInstruction
                (RefundTamper -> String
refundTamperName (RefundTamper -> String) -> Maybe RefundTamper -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe RefundTamper
alteration)
                (b -> Story String String String String String res
rest (b
"batch in " b -> b -> b
forall a. Semigroup a => a -> a -> a
<> b
String
registry))
    Theorem Theorem thm
_ TheoremStory thm (LiveI String String String String String) b
body :>>= b -> Story String String String String String res
rest ->
        let ([Instruction]
inner, b
result) = Program (Clause thm (LiveI String String String String String)) b
-> ([Instruction], b)
forall {k} (thm :: k) res.
Program (Clause thm (LiveI String String String String String)) res
-> ([Instruction], res)
clauseInstructions (TheoremStory thm (LiveI String String String String String) b
-> Program
     (Clause thm (LiveI String String String String String)) b
forall {k} (thm :: k) (act :: * -> *) res.
TheoremStory thm act res -> Program (Clause thm act) res
clauses TheoremStory thm (LiveI String String String String String) b
body)
            ([Instruction]
after, res
final) = Story String String String String String res
-> ([Instruction], res)
forall res.
Story String String String String String res
-> ([Instruction], res)
instructionsWithResult (b -> Story String String String String String res
rest b
result)
        in  ([Instruction]
inner [Instruction] -> [Instruction] -> [Instruction]
forall a. Semigroup a => a -> a -> a
<> [Instruction]
after, res
final)
  where
    one :: InstructionKind
-> Maybe String
-> Story String String String String String b
-> ([Instruction], b)
one InstructionKind
kind Maybe String
alteration Story String String String String String b
next =
        let ([Instruction]
after, b
result) = Story String String String String String b -> ([Instruction], b)
forall res.
Story String String String String String res
-> ([Instruction], res)
instructionsWithResult Story String String String String String b
next
        in  (InstructionKind -> Maybe String -> Instruction
Instruction InstructionKind
kind Maybe String
alteration Instruction -> [Instruction] -> [Instruction]
forall a. a -> [a] -> [a]
: [Instruction]
after, b
result)

clauseInstructions
    :: Program (Clause thm (LiveI String String String String String)) res
    -> ([Instruction], res)
clauseInstructions :: forall {k} (thm :: k) res.
Program (Clause thm (LiveI String String String String String)) res
-> ([Instruction], res)
clauseInstructions Program (Clause thm (LiveI String String String String String)) res
program = case Program (Clause thm (LiveI String String String String String)) res
-> ProgramView
     (Clause thm (LiveI String String String String String)) res
forall (instr :: * -> *) a. Program instr a -> ProgramView instr a
view Program (Clause thm (LiveI String String String String String)) res
program of
    Return res
result -> ([], res
result)
    Clause String
_ LeanCheck (LiveI String String String String String) thm b
check Story (LiveI String String String String String) b
body :>>= b
-> Program
     (Clause thm (LiveI String String String String String)) res
rest ->
        let ([Instruction]
inBody, b
result) = Story (LiveI String String String String String) b
-> ([Instruction], b)
forall res.
Story String String String String String res
-> ([Instruction], res)
instructionsWithResult Story (LiveI String String String String String) b
body
            ([Instruction]
inCheck, ()) = Story String String String String String () -> ([Instruction], ())
forall res.
Story String String String String String res
-> ([Instruction], res)
instructionsWithResult (LeanCheck (LiveI String String String String String) thm b
-> b -> Story String String String String String ()
forall {k} (act :: * -> *) (thm :: k) obs.
LeanCheck act thm obs -> obs -> Story act ()
checkAction LeanCheck (LiveI String String String String String) thm b
check b
result)
            ([Instruction]
after, res
final) = Program (Clause thm (LiveI String String String String String)) res
-> ([Instruction], res)
forall {k} (thm :: k) res.
Program (Clause thm (LiveI String String String String String)) res
-> ([Instruction], res)
clauseInstructions (b
-> Program
     (Clause thm (LiveI String String String String String)) res
rest b
result)
        in  ([Instruction]
inBody [Instruction] -> [Instruction] -> [Instruction]
forall a. Semigroup a => a -> a -> a
<> [Instruction]
inCheck [Instruction] -> [Instruction] -> [Instruction]
forall a. Semigroup a => a -> a -> a
<> [Instruction]
after, res
final)

prepend :: String -> (String, res) -> (String, res)
prepend :: forall res. String -> (String, res) -> (String, res)
prepend String
prefix (String
text, res
result) = (String
prefix String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
text, res
result)

formal :: Binding -> String
formal :: Binding -> String
formal Binding
binding =
    String
"Formal specification: `"
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Binding -> String
boName Binding
binding
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"` @ `"
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Binding -> String
boRevision Binding
binding
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"`. Statement digest: `"
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Binding -> String
boDigest Binding
binding
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"`.\n\n"