-- | One registration program, expressed only as edge requests and comparisons.
module Conformance.Edge.Register (story, insertActiveRow) where

import Conformance.Lean.Registration
    ( insertActiveRow
    , modelComparison
    )
import Conformance.Story.Live
    ( BatchTamper (..)
    , Context (Context)
    , Edge (..)
    , EdgeRequest (..)
    , Story
    , Tamper (..)
    , compareWithModel
    , observe
    , submit
    , tamper
    , tamperFoldBatch
    )
import Conformance.Story.Specification (clause, theorem)

story :: Context reg wal -> Story reg wal step obs cmp ()
story :: forall reg wal step obs cmp.
Context reg wal -> Story reg wal step obs cmp ()
story (Context reg
registry wal
recipient) = do
    _ <-
        Theorem InsertActive
-> TheoremStory InsertActive (LiveI reg wal step obs cmp) step
-> Story (LiveI reg wal step obs cmp) step
forall {k} (thm :: k) (act :: * -> *) res.
Theorem thm -> TheoremStory thm act res -> Story act res
theorem Theorem InsertActive
insertActiveRow
            (TheoremStory InsertActive (LiveI reg wal step obs cmp) step
 -> Story (LiveI reg wal step obs cmp) step)
-> TheoremStory InsertActive (LiveI reg wal step obs cmp) step
-> Story (LiveI reg wal step obs cmp) step
forall a b. (a -> b) -> a -> b
$ String
-> LeanCheck (LiveI reg wal step obs cmp) InsertActive step
-> Story (LiveI reg wal step obs cmp) step
-> TheoremStory InsertActive (LiveI reg wal step obs cmp) step
forall {k} (act :: * -> *) (thm :: k) obs.
String
-> LeanCheck act thm obs
-> Story act obs
-> TheoremStory thm act obs
clause
                String
"Registration delivers one active token to the requested recipient"
                LeanCheck (LiveI reg wal step obs cmp) InsertActive step
forall reg wal step obs cmp.
LeanCheck (LiveI reg wal step obs cmp) InsertActive step
modelComparison
            (Story (LiveI reg wal step obs cmp) step
 -> TheoremStory InsertActive (LiveI reg wal step obs cmp) step)
-> Story (LiveI reg wal step obs cmp) step
-> TheoremStory InsertActive (LiveI reg wal step obs cmp) step
forall a b. (a -> b) -> a -> b
$ reg -> EdgeRequest wal -> Story (LiveI 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 (Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
InsertActive String
"alice" wal
recipient)
    checked (EdgeRequest InsertActive "bob" recipient)
    checked (EdgeRequest InsertActive "alice" recipient)
    let redirected = Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
InsertActive String
"redirect" wal
recipient
    tamper OtherAddress registry redirected >>= compared
    tamper ShortByOne registry redirected >>= compared
    checked redirected
    tamper
        ExtraSigner
        registry
        (EdgeRequest InsertActive "cosigned" recipient)
        >>= compared
    -- Two registrations folded in one transaction that mints both tokens at the
    -- first key: the same quantity of the kind, at the wrong keys.
    _ <-
        tamperFoldBatch
            MintOnFirstKey
            registry
            [ EdgeRequest InsertActive "minted-a" recipient
            , EdgeRequest InsertActive "minted-b" recipient
            ]
    pure ()
  where
    checked :: EdgeRequest wal
-> ProgramT (Step (LiveI reg wal a obs cmp)) Identity ()
checked EdgeRequest wal
request = reg -> EdgeRequest wal -> Story reg wal a obs cmp a
forall reg wal step obs cmp.
reg -> EdgeRequest wal -> Story reg wal step obs cmp step
submit reg
registry EdgeRequest wal
request Story reg wal a obs cmp a
-> (a -> ProgramT (Step (LiveI reg wal a obs cmp)) Identity ())
-> ProgramT (Step (LiveI reg wal a obs cmp)) Identity ()
forall a b.
ProgramT (Step (LiveI reg wal a obs cmp)) Identity a
-> (a -> ProgramT (Step (LiveI reg wal a obs cmp)) Identity b)
-> ProgramT (Step (LiveI reg wal a obs cmp)) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> ProgramT (Step (LiveI reg wal a obs cmp)) Identity ()
forall {step} {reg} {wal} {a} {cmp}.
step -> ProgramT (Step (LiveI reg wal step a cmp)) Identity ()
compared
    compared :: step -> ProgramT (Step (LiveI reg wal step a cmp)) Identity ()
compared step
step = do
        observation <- step -> Story reg wal step a cmp a
forall step reg wal obs cmp. step -> Story reg wal step obs cmp obs
observe step
step
        _ <- compareWithModel step observation
        pure ()