{- | Reach Active and retire it permanently; compare unknown-key and excluded
encoding refusals beside accepting controls. No Absent or deletion success is
claimed, and the broader retirement requirement remains separately uncovered.
-}
module Conformance.Edge.Retire (story) where

import Conformance.Lean.Registration
    ( insertActiveRow
    , modelComparison
    )
import Conformance.Lean.Retirement (updateTerminalRow)
import Conformance.Lean.Retirement qualified as Retirement
import Conformance.Story.Live
    ( Context (Context)
    , Edge (..)
    , EdgeRequest (..)
    , Story
    , compareWithModel
    , observe
    , submit
    )
import Conformance.Story.Specification (clause, theorem)

story
    :: Context reg wal -> Context reg wal -> Story reg wal step obs cmp ()
story :: forall reg wal step obs cmp.
Context reg wal -> Context reg wal -> Story reg wal step obs cmp ()
story (Context reg
registry wal
holder) (Context reg
otherRegistry wal
_) = 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
"The holder receives the token that will be retired"
                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
holder)
    _ <-
        theorem updateTerminalRow
            $ clause
                "Retirement burns the holder's token and leaves the key Terminal"
                Retirement.modelComparison
            $ submit registry (EdgeRequest UpdateTerminal "alice" holder)
    checked registry (EdgeRequest InsertAbsent "never-active" holder)
    checked registry (EdgeRequest UpdateTerminal "never-active" holder)

    -- A refused request remains pending. The unknown control uses a fresh
    -- registry so the first refusal cannot account for the second one.
    checked otherRegistry (EdgeRequest InsertActive "control" holder)
    checked otherRegistry (EdgeRequest UpdateTerminal "control" holder)
    checked
        otherRegistry
        (EdgeRequest UpdateTerminal "never-registered" holder)

    -- Excluded deletion leaves the registration live. Its termination then
    -- succeeds, and that Terminal key cannot be registered again.
    let deletion = Edge -> String -> wal -> EdgeRequest wal
forall wal. Edge -> String -> wal -> EdgeRequest wal
EdgeRequest Edge
DeleteActive String
"deleted" wal
holder
    checked registry (EdgeRequest InsertActive "deleted" holder)
    checked registry deletion
    checked registry (EdgeRequest UpdateTerminal "deleted" holder)
    checked registry (EdgeRequest InsertActive "deleted" holder)
  where
    checked :: reg
-> EdgeRequest wal
-> ProgramT (Step (LiveI reg wal a obs cmp)) Identity ()
checked reg
registry' 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 ()