{- |
Module      : Conformance.Edge.Programs
Description : Every registry row as a program over the registry's operations
License     : Apache-2.0

The registry rows of the inventory, each either a program over the story
language's instructions — an edge composition, or a tamper of an edge's
transaction — or named outside the model's vocabulary with its reason. A
program says which registries it boots and which wallets it names, the requests
it books before its first instruction, what each compared record must show and
how its outcome stands against the consuming project's requirement. The live
runner executes it through the generic interpreter and the book renders the
same program; neither holds a second description of a row.
-}
module Conformance.Edge.Programs
    ( Program (..)
    , Registry (..)
    , Wallet (..)
    , WalletRole (..)
    , Expected (..)
    , Standing (..)
    , Chapter (..)
    , Kind (..)
    , Classification (..)
    , programs
    , programFor
    , outsideVocabulary
    , classify
    , classifyGroup
    , kindOf
    , recordsOf
    , displayStory
    , displayCohort
    ) where

import Conformance.Edge.EarlyReject qualified as EarlyReject
import Conformance.Edge.Exit qualified as Exit
import Conformance.Edge.Occupied qualified as Occupied
import Conformance.Edge.Register qualified as Register
import Conformance.Edge.Retire qualified as Retire
import Conformance.Edge.RetractionWindow qualified as RetractionWindow
import Conformance.Edge.Sequence qualified as Sequence
import Conformance.Story.Live
    ( Booking (..)
    , Context (..)
    , Edge (..)
    , EdgeRequest (..)
    , Instruction (..)
    , InstructionKind (..)
    , Placement (..)
    , RefundTamper (..)
    , Story
    , compareWithModel
    , foldBatch
    , liveInstructions
    , observe
    , rejectBookedBatchWithin
    , rejectWithin
    , retract
    , submit
    , tamperRejectBookedBatchWithin
    )
import Control.Monad ((>=>))
import Data.List (nub)
import Data.Maybe (isJust)
import Data.Text (Text)
import Data.Text qualified as T

-- | A registry a program acts on, booted fresh for its row.
data Registry = Registry
    { Registry -> String
registryName :: String
    -- ^ the name the run boots it under
    , Registry -> String
registryReading :: String
    -- ^ the name the book reads
    , Registry -> Integer
registryProcessingMs :: Integer
    , Registry -> Integer
registryRetractionMs :: Integer
    }
    deriving stock (Registry -> Registry -> Bool
(Registry -> Registry -> Bool)
-> (Registry -> Registry -> Bool) -> Eq Registry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Registry -> Registry -> Bool
== :: Registry -> Registry -> Bool
$c/= :: Registry -> Registry -> Bool
/= :: Registry -> Registry -> Bool
Eq, Int -> Registry -> ShowS
[Registry] -> ShowS
Registry -> String
(Int -> Registry -> ShowS)
-> (Registry -> String) -> ([Registry] -> ShowS) -> Show Registry
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Registry -> ShowS
showsPrec :: Int -> Registry -> ShowS
$cshow :: Registry -> String
show :: Registry -> String
$cshowList :: [Registry] -> ShowS
showList :: [Registry] -> ShowS
Show)

-- | Which wallet of the run a program's wallet is.
data WalletRole
    = -- | the wallet the run signs and funds every fold with
      RunnerWallet
    | -- | a second wallet the run funds once
      SecondWallet
    | {- | a wallet that books requests and receives no fold's change, funded
      with this lovelace when the row starts
      -}
      OwnerWallet Integer
    deriving stock (WalletRole -> WalletRole -> Bool
(WalletRole -> WalletRole -> Bool)
-> (WalletRole -> WalletRole -> Bool) -> Eq WalletRole
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WalletRole -> WalletRole -> Bool
== :: WalletRole -> WalletRole -> Bool
$c/= :: WalletRole -> WalletRole -> Bool
/= :: WalletRole -> WalletRole -> Bool
Eq, Int -> WalletRole -> ShowS
[WalletRole] -> ShowS
WalletRole -> String
(Int -> WalletRole -> ShowS)
-> (WalletRole -> String)
-> ([WalletRole] -> ShowS)
-> Show WalletRole
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WalletRole -> ShowS
showsPrec :: Int -> WalletRole -> ShowS
$cshow :: WalletRole -> String
show :: WalletRole -> String
$cshowList :: [WalletRole] -> ShowS
showList :: [WalletRole] -> ShowS
Show)

-- | A wallet a program names, beside the name the book reads.
data Wallet = Wallet
    { Wallet -> WalletRole
walletRole :: WalletRole
    , Wallet -> String
walletReading :: String
    }
    deriving stock (Wallet -> Wallet -> Bool
(Wallet -> Wallet -> Bool)
-> (Wallet -> Wallet -> Bool) -> Eq Wallet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Wallet -> Wallet -> Bool
== :: Wallet -> Wallet -> Bool
$c/= :: Wallet -> Wallet -> Bool
/= :: Wallet -> Wallet -> Bool
Eq, Int -> Wallet -> ShowS
[Wallet] -> ShowS
Wallet -> String
(Int -> Wallet -> ShowS)
-> (Wallet -> String) -> ([Wallet] -> ShowS) -> Show Wallet
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Wallet -> ShowS
showsPrec :: Int -> Wallet -> ShowS
$cshow :: Wallet -> String
show :: Wallet -> String
$cshowList :: [Wallet] -> ShowS
showList :: [Wallet] -> ShowS
Show)

-- | What one compared record of a program must show.
data Expected
    = -- | the chain and the model reach the same outcome, for the same reason
      Agrees
    | {- | a recorded disagreement, never a pass: the chain's and the model's
      outcomes, the reason the traced replay admits for the chain, and the
      issue that tracks it
      -}
      Diverges
        { Expected -> Text
divergenceChain :: Text
        , Expected -> Text
divergenceModel :: Text
        , Expected -> Text
divergenceTrace :: Text
        , Expected -> Text
divergenceIssue :: Text
        }
    deriving stock (Expected -> Expected -> Bool
(Expected -> Expected -> Bool)
-> (Expected -> Expected -> Bool) -> Eq Expected
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Expected -> Expected -> Bool
== :: Expected -> Expected -> Bool
$c/= :: Expected -> Expected -> Bool
/= :: Expected -> Expected -> Bool
Eq, Int -> Expected -> ShowS
[Expected] -> ShowS
Expected -> String
(Int -> Expected -> ShowS)
-> (Expected -> String) -> ([Expected] -> ShowS) -> Show Expected
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Expected -> ShowS
showsPrec :: Int -> Expected -> ShowS
$cshow :: Expected -> String
show :: Expected -> String
$cshowList :: [Expected] -> ShowS
showList :: [Expected] -> ShowS
Show)

-- | How a program row stands against the consuming project's requirement.
data Standing
    = -- | the row's outcome is what the requirement asks
      Agreement
    | -- | the consuming project's theorem and the model disagree; held
      Held
        { Standing -> String
heldFor :: String
        , Standing -> String
heldLean :: String
        , Standing -> String
heldConsumer :: String
        }
    | -- | the requirement is kept unmet by a ruling
      Unmet
        { Standing -> String
unmetRuling :: String
        , Standing -> String
unmetRegistry :: String
        , Standing -> String
unmetConsumer :: String
        }
    deriving stock (Standing -> Standing -> Bool
(Standing -> Standing -> Bool)
-> (Standing -> Standing -> Bool) -> Eq Standing
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Standing -> Standing -> Bool
== :: Standing -> Standing -> Bool
$c/= :: Standing -> Standing -> Bool
/= :: Standing -> Standing -> Bool
Eq, Int -> Standing -> ShowS
[Standing] -> ShowS
Standing -> String
(Int -> Standing -> ShowS)
-> (Standing -> String) -> ([Standing] -> ShowS) -> Show Standing
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Standing -> ShowS
showsPrec :: Int -> Standing -> ShowS
$cshow :: Standing -> String
show :: Standing -> String
$cshowList :: [Standing] -> ShowS
showList :: [Standing] -> ShowS
Show)

-- | A program the book renders as a chapter of its own.
data Chapter = Chapter
    { Chapter -> String
chapterTitle :: String
    , Chapter -> String
chapterIntroduction :: String
    , Chapter -> String
chapterSummary :: String
    -- ^ how the run's results open, before the counts
    }
    deriving stock (Chapter -> Chapter -> Bool
(Chapter -> Chapter -> Bool)
-> (Chapter -> Chapter -> Bool) -> Eq Chapter
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Chapter -> Chapter -> Bool
== :: Chapter -> Chapter -> Bool
$c/= :: Chapter -> Chapter -> Bool
/= :: Chapter -> Chapter -> Bool
Eq, Int -> Chapter -> ShowS
[Chapter] -> ShowS
Chapter -> String
(Int -> Chapter -> ShowS)
-> (Chapter -> String) -> ([Chapter] -> ShowS) -> Show Chapter
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Chapter -> ShowS
showsPrec :: Int -> Chapter -> ShowS
$cshow :: Chapter -> String
show :: Chapter -> String
$cshowList :: [Chapter] -> ShowS
showList :: [Chapter] -> ShowS
Show)

-- | One row's program.
data Program = Program
    { Program -> String
programRow :: String
    , Program -> [Registry]
programRegistries :: [Registry]
    , Program -> [Wallet]
programWallets :: [Wallet]
    , Program
-> forall reg wal.
   [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort
        :: forall reg wal
         . [reg]
        -> [wal]
        -> Either String [(reg, EdgeRequest wal)]
    {- ^ requests booked before the first instruction, each in its registry;
    a story that needs no request pending before it starts books none
    -}
    , Program
-> forall reg wal step obs cmp.
   [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory
        :: forall reg wal step obs cmp
         . [reg]
        -> [wal]
        -> Either String (Story reg wal step obs cmp ())
    , Program -> [Expected]
programExpected :: [Expected]
    -- ^ one per compared record, in order
    , Program -> Standing
programStanding :: Standing
    , Program -> [String]
programControls :: [String]
    -- ^ the story controls the row admits
    , Program -> Maybe Chapter
programChapter :: Maybe Chapter
    }

-- | Whether a program composes edges or tampers with an edge's transaction.
data Kind = EdgeComposition | Tamper
    deriving stock (Kind -> Kind -> Bool
(Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
/= :: Kind -> Kind -> Bool
Eq, Int -> Kind -> ShowS
[Kind] -> ShowS
Kind -> String
(Int -> Kind -> ShowS)
-> (Kind -> String) -> ([Kind] -> ShowS) -> Show Kind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Kind -> ShowS
showsPrec :: Int -> Kind -> ShowS
$cshow :: Kind -> String
show :: Kind -> String
$cshowList :: [Kind] -> ShowS
showList :: [Kind] -> ShowS
Show)

-- | How a registry row is run.
data Classification
    = -- | a program of this kind
      Composed Kind
    | -- | outside the model's vocabulary, for this reason
      Outside Text
    deriving stock (Classification -> Classification -> Bool
(Classification -> Classification -> Bool)
-> (Classification -> Classification -> Bool) -> Eq Classification
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Classification -> Classification -> Bool
== :: Classification -> Classification -> Bool
$c/= :: Classification -> Classification -> Bool
/= :: Classification -> Classification -> Bool
Eq, Int -> Classification -> ShowS
[Classification] -> ShowS
Classification -> String
(Int -> Classification -> ShowS)
-> (Classification -> String)
-> ([Classification] -> ShowS)
-> Show Classification
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Classification -> ShowS
showsPrec :: Int -> Classification -> ShowS
$cshow :: Classification -> String
show :: Classification -> String
$cshowList :: [Classification] -> ShowS
showList :: [Classification] -> ShowS
Show)

-- | Every program, the book's chapters first, in book order.
programs :: [Program]
programs :: [Program]
programs =
    [ Program
registration
    , Program
occupied
    , Program
retirement
    , Program
exits
    , Program
earlyRejection
    , Program
retractionWindow
    , Program
sequenceProgram
    , Program
insertion
    , Program
phase2Retraction
    , Program
lateRejection
    , Program
processingRejection
    , Program
emptyFold
    , Program
refundRouting
    ]

-- | The program of a row, if it has one.
programFor :: String -> Maybe Program
programFor :: String -> Maybe Program
programFor String
row = case [Program
p | Program
p <- [Program]
programs, Program -> String
programRow Program
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
row] of
    [Program
p] -> Program -> Maybe Program
forall a. a -> Maybe a
Just Program
p
    [Program]
_ -> Maybe Program
forall a. Maybe a
Nothing

{- | The registry rows the model cannot express, each with its reason. A row
here has no program; the ones a run still executes for their chain evidence
do so through their own runner.
-}
outsideVocabulary :: [(Text, Text)]
outsideVocabulary :: [(Text, Text)]
outsideVocabulary =
    [
        ( Text
"update-existing-key"
        , Text
"The original broader update requirement remains uncovered. Its insertAbsent/updateActive success setup is excluded by the current two-edge law. No excluded-edge refusal certifies that requirement."
        )
    ,
        ( Text
"delete-existing-key"
        , Text
"The original deletion requirement remains uncovered: the current two-edge law refuses deletion and cannot return a key to absence."
        )
    ,
        ( Text
"reinsert-deleted-key"
        , Text
"The original reincarnation requirement remains uncovered: the current two-edge law cannot reach its successful deletion prefix."
        )
    ,
        ( Text
"retire-active-key"
        , Text
"The original retirement requirement remains uncovered because it also requires an Absent starting key. A separate current retirement story certifies Active to Terminal and excluded encodings, without claiming that unreachable prefix or the former deletion-refund chapter."
        )
    ,
        ( Text
"fold-against-superseded-root"
        , Text
"a fold whose proof was built against a root the registry has since superseded. The model takes no proof and no authenticated root, so it has no reason to compare with the chain's refusal (lambdasistemi/singular#346). The conformance session runs the refusal and its accepting control on the devnet; the model comparison stays unmet by ruling."
        )
    ,
        ( Text
"surplus-fold-actions"
        , Text
"a fold carrying an action beyond its requests, and one missing an action. The model takes requests, not an action list, so it has no reason to compare with the chain's refusals (lambdasistemi/singular#345). The conformance session runs both refusals and an accepting control on the devnet; the model comparison stays unmet by ruling."
        )
    ,
        ( Text
"historical-owner-change"
        , Text
"a fold that changes the registry's owner. The registry has no owner role (the ownerless-registry ruling of 2026-09-12, commit f3a68b1b) and the model has none either; the earlier observation is history and the claim is withdrawn."
        )
    ,
        ( Text
"retired-stake-hook-with-withdrawal"
        , Text
"a fold carrying a withdrawal under a stake_script hook. The registry interface has no stake_script hook (registry mode, no hook) and the model has no withdrawal; the row is retired and nothing runs it."
        )
    ,
        ( Text
"retired-stake-hook-without-withdrawal"
        , Text
"the same fold with its withdrawal absent. The registry interface has no stake_script hook (registry mode, no hook) and the model has no withdrawal; the row is retired and nothing runs it."
        )
    ,
        ( Text
"historical-owner-signed-sweep"
        , Text
"an owner-signed sweep of an output that is not a request. The registry has no owner role and no sweep: its scripts refuse a sweep for every party (the ownerless-registry ruling of 2026-09-12, commit f3a68b1b), and the model has no sweep. The earlier observation is history and the claim is withdrawn; no run sweeps a registry."
        )
    ,
        ( Text
"historical-non-owner-sweep"
        , Text
"a sweep by someone other than the owner. The registry has no owner role and no sweep (the ownerless-registry ruling of 2026-09-12, commit f3a68b1b), and the model has no sweep; the earlier observation is history and the claim is withdrawn."
        )
    ,
        ( Text
"historical-registry-termination"
        , Text
"ending the registry by burning its state token. The registry has no termination: its state script refuses End for every party (the ownerless-registry ruling of 2026-09-12, commit f3a68b1b), and the model has no termination exit. The claim that End is accepted is withdrawn; no run ends a registry."
        )
    ,
        ( Text
"historical-permissionless-fold"
        , Text
"a fold whose owner's required signer is removed. The registry has no owner role, so there is no owner signer to remove; that no fold requires a signer is compared on every fold the programs run, through the transaction's required signers."
        )
    ]

-- | A program's kind, read off its instructions.
kindOf :: Program -> Either String Kind
kindOf :: Program -> Either String Kind
kindOf Program
p = do
    story <- Program
-> Either String (Story String String String String String ())
displayStory Program
p
    pure $
        if any (isJust . instructionTamper) (liveInstructions story)
            then Tamper
            else EdgeComposition

-- | How many records a program compares: one per compared request, one per batch.
recordsOf :: Program -> Either String Int
recordsOf :: Program -> Either String Int
recordsOf Program
p = do
    story <- Program
-> Either String (Story String String String String String ())
displayStory Program
p
    pure
        ( length
            [ ()
            | Instruction kind _ <- liveInstructions story
            , kind `elem` [CompareInstruction, BatchInstruction]
            ]
        )

-- | How one registry row is run.
classify :: Text -> Either String Classification
classify :: Text -> Either String Classification
classify Text
row = case (String -> Maybe Program
programFor (Text -> String
T.unpack Text
row), Text -> [(Text, Text)] -> Maybe Text
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
row [(Text, Text)]
outsideVocabulary) of
    (Just Program
p, Maybe Text
Nothing) -> Kind -> Classification
Composed (Kind -> Classification)
-> Either String Kind -> Either String Classification
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Program -> Either String Kind
kindOf Program
p
    (Maybe Program
Nothing, Just Text
reason) -> Classification -> Either String Classification
forall a b. b -> Either a b
Right (Text -> Classification
Outside Text
reason)
    (Just Program
_, Just Text
_) ->
        String -> Either String Classification
forall a b. a -> Either a b
Left (Text -> String
T.unpack Text
row String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" is both a program and outside the vocabulary")
    (Maybe Program
Nothing, Maybe Text
Nothing) -> String -> Either String Classification
forall a b. a -> Either a b
Left (Text -> String
T.unpack Text
row String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" is not classified")

{- | Every row of the registry group classified exactly once. An empty group,
or a program or reason for a row the group does not hold, is refused.
-}
classifyGroup :: [Text] -> Either String [(Text, Classification)]
classifyGroup :: [Text] -> Either String [(Text, Classification)]
classifyGroup [Text]
group
    | [Text] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
group = String -> Either String [(Text, Classification)]
forall a b. a -> Either a b
Left String
"there is no registry row to classify"
    | [Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Text] -> [Text]
forall a. Eq a => [a] -> [a]
nub [Text]
group) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Text] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Text]
group =
        String -> Either String [(Text, Classification)]
forall a b. a -> Either a b
Left String
"a registry row is listed twice"
    | Bool -> Bool
not ([Text] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
strays) =
        String -> Either String [(Text, Classification)]
forall a b. a -> Either a b
Left
            ( String
"classified rows the inventory does not hold: "
                String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [String] -> String
unwords ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
strays)
            )
    | Bool
otherwise = (Text -> Either String (Text, Classification))
-> [Text] -> Either String [(Text, Classification)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\Text
row -> (,) Text
row (Classification -> (Text, Classification))
-> Either String Classification
-> Either String (Text, Classification)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Either String Classification
classify Text
row) [Text]
group
  where
    strays :: [Text]
strays =
        [ Text
row
        | Text
row <-
            [String -> Text
T.pack (Program -> String
programRow Program
p) | Program
p <- [Program]
programs, Program -> String
programRow Program
p String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"sequence"]
                [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((Text, Text) -> Text) -> [(Text, Text)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Text) -> Text
forall a b. (a, b) -> a
fst [(Text, Text)]
outsideVocabulary
        , Text
row Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
group
        ]

-- | A program's story over the display names the book reads.
displayStory
    :: Program -> Either String (Story String String String String String ())
displayStory :: Program
-> Either String (Story String String String String String ())
displayStory Program
p =
    Program
-> forall reg wal step obs cmp.
   [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory
        Program
p
        ((Registry -> String) -> [Registry] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Registry -> String
registryReading (Program -> [Registry]
programRegistries Program
p))
        ((Wallet -> String) -> [Wallet] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Wallet -> String
walletReading (Program -> [Wallet]
programWallets Program
p))

-- | A program's cohort over the display names the book reads.
displayCohort
    :: Program -> Either String [(String, EdgeRequest String)]
displayCohort :: Program -> Either String [(String, EdgeRequest String)]
displayCohort Program
p =
    Program
-> forall reg wal.
   [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort
        Program
p
        ((Registry -> String) -> [Registry] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Registry -> String
registryReading (Program -> [Registry]
programRegistries Program
p))
        ((Wallet -> String) -> [Wallet] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Wallet -> String
walletReading (Program -> [Wallet]
programWallets Program
p))

-- ---------------------------------------------------------
-- The programs
-- ---------------------------------------------------------

{- | The story controls every program admits: the model's answer altered, or an
observation the chain gives perturbed, each of which must fail the row.
-}
generalControls :: [String]
generalControls :: [String]
generalControls = [String
"wrong-fee", String
"wrong-timing", String
"wrong-delivery", String
"unknown-identity"]

-- | Every story control the interpreter knows.
allControls :: [String]
allControls :: [String]
allControls = [String]
generalControls [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String
"inside-phase-2", String
"signed-owner"]

-- | A registry with thirty seconds for processing and thirty for retraction.
standard :: String -> String -> Registry
standard :: String -> String -> Registry
standard String
name String
reading = String -> String -> Integer -> Integer -> Registry
Registry String
name String
reading Integer
30_000 Integer
30_000

runner :: String -> Wallet
runner :: String -> Wallet
runner = WalletRole -> String -> Wallet
Wallet WalletRole
RunnerWallet

noCohort :: [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort [reg]
_ [wal]
_ = [(reg, EdgeRequest wal)] -> Either String [(reg, EdgeRequest wal)]
forall a b. b -> Either a b
Right []

-- | A story over one registry and one wallet.
single
    :: (Context reg wal -> Story reg wal step obs cmp ())
    -> [reg]
    -> [wal]
    -> Either String (Story reg wal step obs cmp ())
single :: forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single Context reg wal -> Story reg wal step obs cmp ()
story [reg]
registries [wal]
wallets = case ([reg]
registries, [wal]
wallets) of
    ([reg
registry], [wal
wallet]) -> Story reg wal step obs cmp ()
-> Either String (Story reg wal step obs cmp ())
forall a b. b -> Either a b
Right (Context reg wal -> Story reg wal step obs cmp ()
story (reg -> wal -> Context reg wal
forall reg wal. reg -> wal -> Context reg wal
Context reg
registry wal
wallet))
    ([reg], [wal])
_ -> String -> Either String (Story reg wal step obs cmp ())
forall a b. a -> Either a b
Left String
"the story names one registry and one wallet"

-- | A story over two registries and one wallet.
double
    :: (Context reg wal -> Context reg wal -> Story reg wal step obs cmp ())
    -> [reg]
    -> [wal]
    -> Either String (Story reg wal step obs cmp ())
double :: forall reg wal step obs cmp.
(Context reg wal
 -> Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
double Context reg wal -> Context reg wal -> Story reg wal step obs cmp ()
story [reg]
registries [wal]
wallets = case ([reg]
registries, [wal]
wallets) of
    ([reg
first, reg
second], [wal
wallet]) ->
        Story reg wal step obs cmp ()
-> Either String (Story reg wal step obs cmp ())
forall a b. b -> Either a b
Right (Context reg wal -> Context reg wal -> Story reg wal step obs cmp ()
story (reg -> wal -> Context reg wal
forall reg wal. reg -> wal -> Context reg wal
Context reg
first wal
wallet) (reg -> wal -> Context reg wal
forall reg wal. reg -> wal -> Context reg wal
Context reg
second wal
wallet))
    ([reg], [wal])
_ -> String -> Either String (Story reg wal step obs cmp ())
forall a b. a -> Either a b
Left String
"the story names two registries and one wallet"

-- | Submit, observe and compare each request in turn.
compared :: reg -> [EdgeRequest wal] -> Story reg wal step obs cmp ()
compared :: forall reg wal step obs cmp.
reg -> [EdgeRequest wal] -> Story reg wal step obs cmp ()
compared reg
registry = (EdgeRequest wal
 -> ProgramT (Step (LiveI reg wal step obs cmp)) Identity ())
-> [EdgeRequest wal]
-> ProgramT (Step (LiveI reg wal step obs cmp)) Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (reg -> EdgeRequest wal -> Story reg wal step obs cmp step
forall reg wal step obs cmp.
reg -> EdgeRequest wal -> Story reg wal step obs cmp step
submit reg
registry (EdgeRequest wal -> Story reg wal step obs cmp step)
-> (step
    -> ProgramT (Step (LiveI reg wal step obs cmp)) Identity ())
-> EdgeRequest wal
-> ProgramT (Step (LiveI reg wal step obs cmp)) Identity ()
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> step -> ProgramT (Step (LiveI reg wal step obs cmp)) Identity ()
forall step reg wal obs cmp. step -> Story reg wal step obs cmp ()
checked)

-- | Observe and compare a step already taken.
checked :: step -> Story reg wal step obs cmp ()
checked :: forall step reg wal obs cmp. step -> Story reg wal step obs cmp ()
checked step
step = do
    observation <- step -> Story reg wal step obs cmp obs
forall step reg wal obs cmp. step -> Story reg wal step obs cmp obs
observe step
step
    _ <- compareWithModel step observation
    pure ()

chapter :: String -> String -> String -> Maybe Chapter
chapter :: String -> String -> String -> Maybe Chapter
chapter String
title String
introduction String
summary = Chapter -> Maybe Chapter
forall a. a -> Maybe a
Just (String -> String -> String -> Chapter
Chapter String
title String
introduction String
summary)

registration :: Program
registration :: Program
registration =
    Program
        { programRow :: String
programRow = String
"register-active-key"
        , programRegistries :: [Registry]
programRegistries = [String -> String -> Registry
standard String
"story-registration" String
"registration"]
        , programWallets :: [Wallet]
programWallets = [WalletRole -> String -> Wallet
Wallet WalletRole
SecondWallet String
"recipient wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single Context reg wal -> Story reg wal step obs cmp ()
forall reg wal step obs cmp.
Context reg wal -> Story reg wal step obs cmp ()
Register.story
        , programExpected :: [Expected]
programExpected = Int -> Expected -> [Expected]
forall a. Int -> a -> [a]
replicate Int
8 Expected
Agrees
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
generalControls
        , programChapter :: Maybe Chapter
programChapter =
            String -> String -> String -> Maybe Chapter
chapter
                String
"Register a key and receive its active token"
                String
"A requester submits two distinct active registrations and then repeats one key. The delivery is then sent to another address, and paid one lovelace short, beside the same untampered request. Every step is compared with the executable registry model."
                String
"Registration compared"
        }

occupied :: Program
occupied :: Program
occupied =
    Program
        { programRow :: String
programRow = String
"insert-occupied-key"
        , programRegistries :: [Registry]
programRegistries = [String -> String -> Registry
standard String
"occupied-insert" String
"occupied insert"]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"holder wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single Context reg wal -> Story reg wal step obs cmp ()
forall reg wal step obs cmp.
Context reg wal -> Story reg wal step obs cmp ()
Occupied.story
        , programExpected :: [Expected]
programExpected = Int -> Expected -> [Expected]
forall a. Int -> a -> [a]
replicate Int
3 Expected
Agrees
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
allControls
        , programChapter :: Maybe Chapter
programChapter =
            String -> String -> String -> Maybe Chapter
chapter
                String
"Insert on a key the registry already holds"
                String
"A key is registered Active in this run. Registering that key again is refused beside its accepting control. The excluded updateActive encoding is also refused without changing the registration. Each result is compared with the executable registry model."
                String
"Occupied-key insertion compared"
        }

retirement :: Program
retirement :: Program
retirement =
    Program
        { programRow :: String
programRow = String
"permanent-retire-active-key"
        , programRegistries :: [Registry]
programRegistries =
            [ String -> String -> Registry
standard String
"story-retirement" String
"retirement"
            , String -> String -> Registry
standard String
"story-unknown-key comparison" String
"comparison"
            ]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"holder wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal
 -> Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal
 -> Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
double Context reg wal -> Context reg wal -> Story reg wal step obs cmp ()
forall reg wal step obs cmp.
Context reg wal -> Context reg wal -> Story reg wal step obs cmp ()
Retire.story
        , programExpected :: [Expected]
programExpected = Int -> Expected -> [Expected]
forall a. Int -> a -> [a]
replicate Int
11 Expected
Agrees
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
generalControls
        , programChapter :: Maybe Chapter
programChapter =
            String -> String -> String -> Maybe Chapter
chapter
                String
"Retire a registration and burn its active token"
                String
"The holder registers a key in this run, then termination consumes and burns that very token and changes the key to Terminal. Unknown-key termination is refused beside a reached accepting control. Excluded insertion and deletion encodings are refused. After a refused deletion the same Active key can still terminate; its Terminal key cannot register again. The original broader Absent and deletion-refund requirements stay published as uncovered."
                String
"Retirement compared"
        }

exits :: Program
exits :: Program
exits =
    Program
        { programRow :: String
programRow = String
"reject-and-retract-refund-controls"
        , programRegistries :: [Registry]
programRegistries =
            [ String -> String -> Integer -> Integer -> Registry
Registry String
"story-rejection" String
"rejection" Integer
1_000 Integer
1_000
            , String -> String -> Integer -> Integer -> Registry
Registry String
"story-retraction" String
"retraction" Integer
1_000 Integer
30_000
            ]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"holder wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal
 -> Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal
 -> Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
double Context reg wal -> Context reg wal -> Story reg wal step obs cmp ()
forall reg wal step obs cmp.
Context reg wal -> Context reg wal -> Story reg wal step obs cmp ()
Exit.story
        , programExpected :: [Expected]
programExpected = Int -> Expected -> [Expected]
forall a. Int -> a -> [a]
replicate Int
10 Expected
Agrees
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
generalControls [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String
"signed-owner"]
        , programChapter :: Maybe Chapter
programChapter =
            String -> String -> String -> Maybe Chapter
chapter
                String
"A request that is never folded"
                String
"A request can leave the queue without a fold. After its owner's retraction window has closed, a folder rejects it and must refund its owner the deposit, keeping the tip; while it is still retractable, its owner retracts it and must get back everything it held, deposit and tip, through an output whose inline datum is the retracted request's own output reference. Each refund paid one lovelace short or to another address, a return bound to another request, and a retraction spending the registry's state beside it must be refused, each beside the untampered exit of the same request."
                String
"Rejection and retraction compared"
        }

earlyRejection :: Program
earlyRejection :: Program
earlyRejection =
    Program
        { programRow :: String
programRow = String
"reject-inside-processing-and-retraction-windows"
        , programRegistries :: [Registry]
programRegistries =
            [String -> String -> Integer -> Integer -> Registry
Registry String
"story-early-rejection" String
"early rejection" Integer
120_000 Integer
120_000]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"holder wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = \[reg]
registries [wal]
wallets -> case ([reg]
registries, [wal]
wallets) of
            ([reg
registry], [wal
holder]) ->
                let (EdgeRequest wal
first, EdgeRequest wal
second) = wal -> (EdgeRequest wal, EdgeRequest wal)
forall wal. wal -> (EdgeRequest wal, EdgeRequest wal)
EarlyReject.requests wal
holder
                in  [(reg, EdgeRequest wal)] -> Either String [(reg, EdgeRequest wal)]
forall a b. b -> Either a b
Right [(reg
registry, EdgeRequest wal
first), (reg
registry, EdgeRequest wal
second)]
            ([reg], [wal])
_ -> String -> Either String [(reg, EdgeRequest wal)]
forall a b. a -> Either a b
Left String
"the early rejection names one registry and one wallet"
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single Context reg wal -> Story reg wal step obs cmp ()
forall reg wal step obs cmp.
Context reg wal -> Story reg wal step obs cmp ()
EarlyReject.story
        , programExpected :: [Expected]
programExpected = Int -> Expected -> [Expected]
forall a. Int -> a -> [a]
replicate Int
6 Expected
Agrees
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
allControls
        , programChapter :: Maybe Chapter
programChapter =
            String -> String -> String -> Maybe Chapter
chapter
                String
"A folder rejects a request before its retraction deadline"
                String
"A reject carries no admission: the model accepts it in every window, and the chain does too. Two insertion requests from the same owner are booked together in a registry of their own. The first is rejected while it can still be folded, the second while its owner can still retract it. In each window a reject refunding the owner one lovelace short, and one refunding another key, must be refused by both, leaving the request pending; the untampered reject of the same request must be accepted by both, refund the owner the deposit and leave the registry state as it was. Each reject's validity interval is checked to lie inside the window its step names before it is submitted."
                String
"Early rejection compared"
        }

retractionWindow :: Program
retractionWindow :: Program
retractionWindow =
    Program
        { programRow :: String
programRow = String
"retract-outside-window"
        , programRegistries :: [Registry]
programRegistries =
            [String -> String -> Registry
standard String
"story-retraction-window" String
"retraction window"]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"owner wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = \[reg]
registries [wal]
wallets -> case ([reg]
registries, [wal]
wallets) of
            ([reg
registry], [wal
owner]) ->
                let (EdgeRequest wal
first, EdgeRequest wal
second) = wal -> (EdgeRequest wal, EdgeRequest wal)
forall wal. wal -> (EdgeRequest wal, EdgeRequest wal)
RetractionWindow.requests wal
owner
                in  [(reg, EdgeRequest wal)] -> Either String [(reg, EdgeRequest wal)]
forall a b. b -> Either a b
Right [(reg
registry, EdgeRequest wal
first), (reg
registry, EdgeRequest wal
second)]
            ([reg], [wal])
_ -> String -> Either String [(reg, EdgeRequest wal)]
forall a b. a -> Either a b
Left String
"the retraction window names one registry and one wallet"
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single Context reg wal -> Story reg wal step obs cmp ()
forall reg wal step obs cmp.
Context reg wal -> Story reg wal step obs cmp ()
RetractionWindow.story
        , programExpected :: [Expected]
programExpected = Int -> Expected -> [Expected]
forall a. Int -> a -> [a]
replicate Int
3 Expected
Agrees
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String
"inside-phase-2"]
        , programChapter :: Maybe Chapter
programChapter =
            String -> String -> String -> Maybe Chapter
chapter
                String
"Retract only inside phase 2"
                String
"Two insertion requests from the same owner are booked in one registry before either exits. The first is retracted before phase 2, then inside it; the second is retracted after its window closes. Both outside-window retractions must be refused, and the in-window retraction must be accepted. The second request shares the first's accepting control: once its own window is over it cannot have an in-window retry. The registry allows thirty seconds for processing and thirty more for retraction; waits follow each request's recorded submission time."
                String
"Retraction window compared"
        }

sequenceProgram :: Program
sequenceProgram :: Program
sequenceProgram =
    Program
        { programRow :: String
programRow = String
"sequence"
        , programRegistries :: [Registry]
programRegistries = [String -> String -> Registry
standard String
"unnamed-sequence" String
"sequence"]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"holder wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single Context reg wal -> Story reg wal step obs cmp ()
forall reg wal step obs cmp.
Context reg wal -> Story reg wal step obs cmp ()
Sequence.story
        , programExpected :: [Expected]
programExpected = Int -> Expected -> [Expected]
forall a. Int -> a -> [a]
replicate Int
8 Expected
Agrees
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
allControls
        , programChapter :: Maybe Chapter
programChapter =
            String -> String -> String -> Maybe Chapter
chapter
                String
"A sequence no chapter names"
                String
"This program uses the same live interpreter for each listed request. Each step records its own model and chain outcome; any unsupported result carries the reason observed at the booking or fold boundary."
                String
"Unnamed sequence compared"
        }

-- | A program over one fresh registry, comparing each request it submits.
foldsOf :: String -> String -> String -> [(Edge, String)] -> Program
foldsOf :: String -> String -> String -> [(Edge, String)] -> Program
foldsOf String
row String
name String
reading [(Edge, String)]
requests =
    Program
        { programRow :: String
programRow = String
row
        , programRegistries :: [Registry]
programRegistries = [String -> String -> Registry
standard String
name String
reading]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"holder wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single ((Context reg wal -> Story reg wal step obs cmp ())
 -> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ()))
-> (Context reg wal -> Story reg wal step obs cmp ())
-> [reg]
-> [wal]
-> Either String (Story reg wal step obs cmp ())
forall a b. (a -> b) -> a -> b
$ \(Context reg
registry wal
holder) ->
            reg -> [EdgeRequest wal] -> Story reg wal step obs cmp ()
forall reg wal step obs cmp.
reg -> [EdgeRequest wal] -> Story reg wal step obs cmp ()
compared
                reg
registry
                [Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
edge String
key wal
holder | (Edge
edge, String
key) <- [(Edge, String)]
requests]
        , programExpected :: [Expected]
programExpected = ((Edge, String) -> Expected) -> [(Edge, String)] -> [Expected]
forall a b. (a -> b) -> [a] -> [b]
map (Expected -> (Edge, String) -> Expected
forall a b. a -> b -> a
const Expected
Agrees) [(Edge, String)]
requests
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
generalControls
        , programChapter :: Maybe Chapter
programChapter = Maybe Chapter
forall a. Maybe a
Nothing
        }

insertion :: Program
insertion :: Program
insertion =
    String -> String -> String -> [(Edge, String)] -> Program
foldsOf String
"insert-key" String
"cg01" String
"insertion" [(Edge
InsertActive, String
"cg01-key")]

-- | The owner retracts an insertion request inside phase 2.
phase2Retraction :: Program
phase2Retraction :: Program
phase2Retraction =
    Program
        { programRow :: String
programRow = String
"retract-inside-window"
        , programRegistries :: [Registry]
programRegistries =
            [String -> String -> Integer -> Integer -> Registry
Registry String
"cg06" String
"retraction in phase 2" Integer
1_000 Integer
30_000]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"owner wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single ((Context reg wal -> Story reg wal step obs cmp ())
 -> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ()))
-> (Context reg wal -> Story reg wal step obs cmp ())
-> [reg]
-> [wal]
-> Either String (Story reg wal step obs cmp ())
forall a b. (a -> b) -> a -> b
$ \(Context reg
registry wal
owner) ->
            reg -> EdgeRequest wal -> Story reg wal step obs cmp step
forall reg wal step obs cmp.
reg -> EdgeRequest wal -> Story reg wal step obs cmp step
retract reg
registry (Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
InsertActive String
"cg06-key" wal
owner)
                Story reg wal step obs cmp step
-> (step -> Story reg wal step obs cmp ())
-> Story reg wal step obs cmp ()
forall a b.
ProgramT (Step (LiveI reg wal step obs cmp)) Identity a
-> (a -> ProgramT (Step (LiveI reg wal step obs cmp)) Identity b)
-> ProgramT (Step (LiveI reg wal step obs cmp)) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= step -> Story reg wal step obs cmp ()
forall step reg wal obs cmp. step -> Story reg wal step obs cmp ()
checked
        , programExpected :: [Expected]
programExpected = [Expected
Agrees]
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
generalControls
        , programChapter :: Maybe Chapter
programChapter = Maybe Chapter
forall a. Maybe a
Nothing
        }

-- | A folder rejects an insertion request after its owner's retraction window.
lateRejection :: Program
lateRejection :: Program
lateRejection =
    Program
        { programRow :: String
programRow = String
"reject-after-window"
        , programRegistries :: [Registry]
programRegistries =
            [String -> String -> Integer -> Integer -> Registry
Registry String
"cg08" String
"rejection after the windows" Integer
1_000 Integer
1_000]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"holder wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single ((Context reg wal -> Story reg wal step obs cmp ())
 -> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ()))
-> (Context reg wal -> Story reg wal step obs cmp ())
-> [reg]
-> [wal]
-> Either String (Story reg wal step obs cmp ())
forall a b. (a -> b) -> a -> b
$ \(Context reg
registry wal
holder) ->
            Placement
-> reg -> EdgeRequest wal -> Story reg wal step obs cmp step
forall reg wal step obs cmp.
Placement
-> reg -> EdgeRequest wal -> Story reg wal step obs cmp step
rejectWithin
                Placement
AfterTheWindows
                reg
registry
                (Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
InsertActive String
"cg08-key" wal
holder)
                Story reg wal step obs cmp step
-> (step -> Story reg wal step obs cmp ())
-> Story reg wal step obs cmp ()
forall a b.
ProgramT (Step (LiveI reg wal step obs cmp)) Identity a
-> (a -> ProgramT (Step (LiveI reg wal step obs cmp)) Identity b)
-> ProgramT (Step (LiveI reg wal step obs cmp)) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= step -> Story reg wal step obs cmp ()
forall step reg wal obs cmp. step -> Story reg wal step obs cmp ()
checked
        , programExpected :: [Expected]
programExpected = [Expected
Agrees]
        , programStanding :: Standing
programStanding = Standing
Agreement
        , programControls :: [String]
programControls = [String]
generalControls
        , programChapter :: Maybe Chapter
programChapter = Maybe Chapter
forall a. Maybe a
Nothing
        }

{- | A folder rejects a request while it can still be folded. Its control comes
first, on the same request: the reject refunding the owner one lovelace short,
refused by both. Then the known divergence: one lovelace short at the refund's
position and two ada more in another output at the owner's key, which the
chain refuses and the model accepts (lambdasistemi/singular#361). Last the
reject itself, accepted by both, while the consuming project requires it
refused: its requirement is kept unmet by ruling.
-}
processingRejection :: Program
processingRejection :: Program
processingRejection =
    Program
        { programRow :: String
programRow = String
"reject-before-deadline-consumer-requirement"
        , programRegistries :: [Registry]
programRegistries =
            [String -> String -> Integer -> Integer -> Registry
Registry String
"cg09" String
"processing-window rejection" Integer
30_000 Integer
5_000]
        , programWallets :: [Wallet]
programWallets = [WalletRole -> String -> Wallet
Wallet (Integer -> WalletRole
OwnerWallet Integer
10_000_000) String
"owner wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single ((Context reg wal -> Story reg wal step obs cmp ())
 -> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ()))
-> (Context reg wal -> Story reg wal step obs cmp ())
-> [reg]
-> [wal]
-> Either String (Story reg wal step obs cmp ())
forall a b. (a -> b) -> a -> b
$ \(Context reg
registry wal
owner) -> do
            let booked :: [(EdgeRequest wal, Booking wal)]
booked =
                    [
                        ( Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
InsertAbsent String
"cg09-key" wal
owner
                        , wal -> Integer -> Booking wal
forall wal. wal -> Integer -> Booking wal
Booking wal
owner Integer
3_000_000
                        )
                    ]
            _ <-
                RefundTamper
-> Placement
-> reg
-> [(EdgeRequest wal, Booking wal)]
-> Story reg wal step obs cmp cmp
forall reg wal step obs cmp.
RefundTamper
-> Placement
-> reg
-> [(EdgeRequest wal, Booking wal)]
-> Story reg wal step obs cmp cmp
tamperRejectBookedBatchWithin
                    (Integer -> RefundTamper
ShortFirstRefund Integer
1)
                    Placement
InProcessingWindow
                    reg
registry
                    [(EdgeRequest wal, Booking wal)]
booked
            _ <-
                tamperRejectBookedBatchWithin
                    (SplitFirstRefund 1)
                    InProcessingWindow
                    registry
                    booked
            _ <- rejectBookedBatchWithin InProcessingWindow registry booked
            pure ()
        , programExpected :: [Expected]
programExpected =
            [ Expected
Agrees
            , Diverges
                { divergenceChain :: Text
divergenceChain = Text
"refused"
                , divergenceModel :: Text
divergenceModel = Text
"accepted"
                , divergenceTrace :: Text
divergenceTrace = Text
"deposit-returned"
                , divergenceIssue :: Text
divergenceIssue = Text
"lambdasistemi/singular#361"
                }
            , Expected
Agrees
            ]
        , programStanding :: Standing
programStanding =
            Unmet
                { unmetRuling :: String
unmetRuling =
                    String
"kept unmet by operator ruling 2026-10-01 (singular#320; alignment: cardano-keri#468)"
                , unmetRegistry :: String
unmetRegistry =
                    String
"Singular's Lean gives a reject no admission (Model.lean exitAdmission .reject = none): a folder may reject a request inside its process window"
                , unmetConsumer :: String
unmetConsumer =
                    String
"R9_reject_needs_rejectable — a reject is refused until the request's retract window has passed"
                }
        , programControls :: [String]
programControls = [String]
generalControls
        , programChapter :: Maybe Chapter
programChapter = Maybe Chapter
forall a. Maybe a
Nothing
        }

{- | A fold of no request, refused by both for the empty batch, beside its
accepting control: one insertion folded on the same registry.
-}
emptyFold :: Program
emptyFold :: Program
emptyFold =
    Program
        { programRow :: String
programRow = String
"empty-fold"
        , programRegistries :: [Registry]
programRegistries = [String -> String -> Registry
standard String
"cg11" String
"empty fold"]
        , programWallets :: [Wallet]
programWallets = [String -> Wallet
runner String
"holder wallet"]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = (Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
forall reg wal step obs cmp.
(Context reg wal -> Story reg wal step obs cmp ())
-> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
single ((Context reg wal -> Story reg wal step obs cmp ())
 -> [reg] -> [wal] -> Either String (Story reg wal step obs cmp ()))
-> (Context reg wal -> Story reg wal step obs cmp ())
-> [reg]
-> [wal]
-> Either String (Story reg wal step obs cmp ())
forall a b. (a -> b) -> a -> b
$ \(Context reg
registry wal
holder) -> do
            _ <- reg -> [EdgeRequest wal] -> Story reg wal step obs cmp cmp
forall reg wal step obs cmp.
reg -> [EdgeRequest wal] -> Story reg wal step obs cmp cmp
foldBatch reg
registry []
            compared registry [EdgeRequest InsertActive "cg11-key" holder]
        , programExpected :: [Expected]
programExpected = [Expected
Agrees, Expected
Agrees]
        , programStanding :: Standing
programStanding =
            Held
                { heldFor :: String
heldFor = String
"Q-002 (story 2)"
                , heldLean :: String
heldLean =
                    String
"Singular's Lean refuses the empty fold for empty-fold (foldBatch over no request), the reason the traced replay admits for the state script"
                , heldConsumer :: String
heldConsumer =
                    String
"R8_empty_fold_refused — the empty batch must be refused (consumer-side; upstream cardano-mpfs-onchain#100 is the partition fix)"
                }
        , programControls :: [String]
programControls = [String]
generalControls
        , programChapter :: Maybe Chapter
programChapter = Maybe Chapter
forall a. Maybe a
Nothing
        }

{- | Two requests owned by two wallets, holding unequal deposits, rejected
together after the windows with each owner refunded what the other is owed:
refused by both, beside the same two requests refunded as owed. Then two more,
the first refunded a thousand lovelace short of its floor, refused by both,
beside the same two refunded as owed.
-}
refundRouting :: Program
refundRouting :: Program
refundRouting =
    Program
        { programRow :: String
programRow = String
"request-value-and-refund-routing"
        , programRegistries :: [Registry]
programRegistries = [String -> String -> Registry
standard String
"cg19" String
"refund routing"]
        , programWallets :: [Wallet]
programWallets =
            [ WalletRole -> String -> Wallet
Wallet (Integer -> WalletRole
OwnerWallet Integer
25_000_000) String
"first owner wallet"
            , WalletRole -> String -> Wallet
Wallet WalletRole
SecondWallet String
"second owner wallet"
            ]
        , programCohort :: forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
programCohort = [reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
forall reg wal.
[reg] -> [wal] -> Either String [(reg, EdgeRequest wal)]
noCohort
        , programStory :: forall reg wal step obs cmp.
[reg] -> [wal] -> Either String (Story reg wal step obs cmp ())
programStory = \[reg]
registries [wal]
wallets -> case ([reg]
registries, [wal]
wallets) of
            ([reg
registry], [wal
first, wal
second]) -> Story reg wal step obs cmp ()
-> Either String (Story reg wal step obs cmp ())
forall a b. b -> Either a b
Right (Story reg wal step obs cmp ()
 -> Either String (Story reg wal step obs cmp ()))
-> Story reg wal step obs cmp ()
-> Either String (Story reg wal step obs cmp ())
forall a b. (a -> b) -> a -> b
$ do
                let pair :: String -> String -> [(EdgeRequest wal, Booking wal)]
pair String
a String
b =
                        [ (Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
InsertAbsent String
a wal
first, wal -> Integer -> Booking wal
forall wal. wal -> Integer -> Booking wal
Booking wal
first Integer
4_000_000)
                        , (Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
InsertAbsent String
b wal
second, wal -> Integer -> Booking wal
forall wal. wal -> Integer -> Booking wal
Booking wal
second Integer
2_000_000)
                        ]
                    crossed :: [(EdgeRequest wal, Booking wal)]
crossed = String -> String -> [(EdgeRequest wal, Booking wal)]
pair String
"cg19-key-a" String
"cg19-key-b"
                    floored :: [(EdgeRequest wal, Booking wal)]
floored = String -> String -> [(EdgeRequest wal, Booking wal)]
pair String
"cg19-rej-a" String
"cg19-rej-b"
                _ <-
                    RefundTamper
-> Placement
-> reg
-> [(EdgeRequest wal, Booking wal)]
-> Story reg wal step obs cmp cmp
forall reg wal step obs cmp.
RefundTamper
-> Placement
-> reg
-> [(EdgeRequest wal, Booking wal)]
-> Story reg wal step obs cmp cmp
tamperRejectBookedBatchWithin
                        RefundTamper
CrossedRefunds
                        Placement
AfterTheWindows
                        reg
registry
                        [(EdgeRequest wal, Booking wal)]
crossed
                _ <- rejectBookedBatchWithin AfterTheWindows registry crossed
                _ <-
                    tamperRejectBookedBatchWithin
                        (ShortFirstRefund 1_000)
                        AfterTheWindows
                        registry
                        floored
                _ <- rejectBookedBatchWithin AfterTheWindows registry floored
                pure ()
            ([reg], [wal])
_ -> String -> Either String (Story reg wal step obs cmp ())
forall a b. a -> Either a b
Left String
"refund routing names one registry and two wallets"
        , programExpected :: [Expected]
programExpected = Int -> Expected -> [Expected]
forall a. Int -> a -> [a]
replicate Int
4 Expected
Agrees
        , programStanding :: Standing
programStanding =
            Held
                { heldFor :: String
heldFor = String
"Q-002 (story 2)"
                , heldLean :: String
heldLean =
                    String
"Singular's Lean refuses the crossed refunds: its reject batch owes each owner its deposit back and the first is paid short, deposit-returned, the reason the traced replay admits for the state script"
                , heldConsumer :: String
heldConsumer =
                    String
"R11 — action-dependent routing (E18 disposition): processed Update value routes to the checkpoint/consumer hook (Update contributes no Rejected-owner obligations); Rejected owes input-tip per owner under a no-underpayment floor (upstream cardano-mpfs-onchain#101 is the partition fix)"
                }
        , programControls :: [String]
programControls = [String]
generalControls
        , programChapter :: Maybe Chapter
programChapter = Maybe Chapter
forall a. Maybe a
Nothing
        }