-- | The retirement effect computed by the model after a real registration.
module Conformance.Lean.Retirement
    ( UpdateTerminal
    , modelComparison
    , updateTerminalRow
    ) where

import Conformance.Story.Binding (mkBoundObligation)
import Conformance.Story.Live (LiveI (Compare, Observe))
import Conformance.Story.Specification
    ( LeanCheck
    , Theorem
    , action
    , bindCheck
    , bindTheorem
    )

-- | The accepted retirement declaration.
data UpdateTerminal

-- | Check burn, witness consumption, remaining holdings and the committed leaf.
modelComparison
    :: LeanCheck (LiveI reg wal step obs cmp) UpdateTerminal step
modelComparison :: forall reg wal step obs cmp.
LeanCheck (LiveI reg wal step obs cmp) UpdateTerminal step
modelComparison = Theorem UpdateTerminal
-> (step -> Story (LiveI reg wal step obs cmp) ())
-> LeanCheck (LiveI reg wal step obs cmp) UpdateTerminal step
forall {k} (thm :: k) obs (act :: * -> *).
Theorem thm -> (obs -> Story act ()) -> LeanCheck act thm obs
bindCheck Theorem UpdateTerminal
updateTerminalRow ((step -> Story (LiveI reg wal step obs cmp) ())
 -> LeanCheck (LiveI reg wal step obs cmp) UpdateTerminal step)
-> (step -> Story (LiveI reg wal step obs cmp) ())
-> LeanCheck (LiveI reg wal step obs cmp) UpdateTerminal step
forall a b. (a -> b) -> a -> b
$ \step
step -> do
    observation <- LiveI reg wal step obs cmp obs
-> Story (LiveI reg wal step obs cmp) obs
forall (act :: * -> *) res. act res -> Story act res
action (step -> LiveI reg wal step obs cmp obs
forall step reg wal obs cmp. step -> LiveI reg wal step obs cmp obs
Observe step
step)
    _ <- action (Compare step observation)
    pure ()

-- | The revision and statement digest resolved before the live clause runs.
updateTerminalRow :: Theorem UpdateTerminal
updateTerminalRow :: Theorem UpdateTerminal
updateTerminalRow =
    Binding -> Theorem UpdateTerminal
forall {k} (thm :: k). Binding -> Theorem thm
bindTheorem (Binding -> Theorem UpdateTerminal)
-> Binding -> Theorem UpdateTerminal
forall a b. (a -> b) -> a -> b
$
        String -> String -> String -> Binding
mkBoundObligation
            String
"Singular.Statements.update_terminal_transaction_row"
            String
"4806b33d0b74c975981c8905ceb8aab758efbe5d780eca50f59e68202ea2a4bf"
            String
"88957e41876911a993c5d9a338f8ab006c9f6843"