{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE RankNTypes #-}

{- |
Module      : Singular.Registry.Evidence
Description : Acquisition identity and abstract evidence policy
License     : Apache-2.0

A session identity records one acquisition; it does not assert a snapshot.
Facts may carry an abstract witness. Demo 1 has no inhabitant of NoWitness or
Endorsement and configures only the honest unverified verdict.
-}
module Singular.Registry.Evidence
    ( SessionId (..)
    , SessionBinding (..)
    , Evidenced (..)
    , NoWitness
    , Endorsement
    , Reason (..)
    , Verdict (..)
    , Verifier (..)
    , unverifiedVerifier
    ) where

import Data.ByteString (ByteString)
import Data.Text (Text)

-- | Identifies one acquisition, including all facts consumed within it.
newtype SessionId = SessionId Text deriving stock (SessionId -> SessionId -> Bool
(SessionId -> SessionId -> Bool)
-> (SessionId -> SessionId -> Bool) -> Eq SessionId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SessionId -> SessionId -> Bool
== :: SessionId -> SessionId -> Bool
$c/= :: SessionId -> SessionId -> Bool
/= :: SessionId -> SessionId -> Bool
Eq, Eq SessionId
Eq SessionId =>
(SessionId -> SessionId -> Ordering)
-> (SessionId -> SessionId -> Bool)
-> (SessionId -> SessionId -> Bool)
-> (SessionId -> SessionId -> Bool)
-> (SessionId -> SessionId -> Bool)
-> (SessionId -> SessionId -> SessionId)
-> (SessionId -> SessionId -> SessionId)
-> Ord SessionId
SessionId -> SessionId -> Bool
SessionId -> SessionId -> Ordering
SessionId -> SessionId -> SessionId
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 :: SessionId -> SessionId -> Ordering
compare :: SessionId -> SessionId -> Ordering
$c< :: SessionId -> SessionId -> Bool
< :: SessionId -> SessionId -> Bool
$c<= :: SessionId -> SessionId -> Bool
<= :: SessionId -> SessionId -> Bool
$c> :: SessionId -> SessionId -> Bool
> :: SessionId -> SessionId -> Bool
$c>= :: SessionId -> SessionId -> Bool
>= :: SessionId -> SessionId -> Bool
$cmax :: SessionId -> SessionId -> SessionId
max :: SessionId -> SessionId -> SessionId
$cmin :: SessionId -> SessionId -> SessionId
min :: SessionId -> SessionId -> SessionId
Ord, Int -> SessionId -> ShowS
[SessionId] -> ShowS
SessionId -> String
(Int -> SessionId -> ShowS)
-> (SessionId -> String)
-> ([SessionId] -> ShowS)
-> Show SessionId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SessionId -> ShowS
showsPrec :: Int -> SessionId -> ShowS
$cshow :: SessionId -> String
show :: SessionId -> String
$cshowList :: [SessionId] -> ShowS
showList :: [SessionId] -> ShowS
Show)

-- | Snapshot binding, independent of the latest observed tip.
data SessionBinding = Unbound | Bound Integer ByteString
    deriving stock (SessionBinding -> SessionBinding -> Bool
(SessionBinding -> SessionBinding -> Bool)
-> (SessionBinding -> SessionBinding -> Bool) -> Eq SessionBinding
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SessionBinding -> SessionBinding -> Bool
== :: SessionBinding -> SessionBinding -> Bool
$c/= :: SessionBinding -> SessionBinding -> Bool
/= :: SessionBinding -> SessionBinding -> Bool
Eq, Int -> SessionBinding -> ShowS
[SessionBinding] -> ShowS
SessionBinding -> String
(Int -> SessionBinding -> ShowS)
-> (SessionBinding -> String)
-> ([SessionBinding] -> ShowS)
-> Show SessionBinding
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SessionBinding -> ShowS
showsPrec :: Int -> SessionBinding -> ShowS
$cshow :: SessionBinding -> String
show :: SessionBinding -> String
$cshowList :: [SessionBinding] -> ShowS
showList :: [SessionBinding] -> ShowS
Show)

-- | A raw fact and its optional abstract witness.
data Evidenced w a = Evidenced
    { forall w a. Evidenced w a -> a
value :: a
    , forall w a. Evidenced w a -> Maybe w
witness :: Maybe w
    }

-- | Demo 1 has no concrete witness representation.
data NoWitness

-- | No endorsement implementation or concrete decoder ships in Demo 1.
data Endorsement

-- | Why a fact remains unverified.
data Reason = NoVerifierConfigured deriving stock (Reason -> Reason -> Bool
(Reason -> Reason -> Bool)
-> (Reason -> Reason -> Bool) -> Eq Reason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Reason -> Reason -> Bool
== :: Reason -> Reason -> Bool
$c/= :: Reason -> Reason -> Bool
/= :: Reason -> Reason -> Bool
Eq, Int -> Reason -> ShowS
[Reason] -> ShowS
Reason -> String
(Int -> Reason -> ShowS)
-> (Reason -> String) -> ([Reason] -> ShowS) -> Show Reason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Reason -> ShowS
showsPrec :: Int -> Reason -> ShowS
$cshow :: Reason -> String
show :: Reason -> String
$cshowList :: [Reason] -> ShowS
showList :: [Reason] -> ShowS
Show)

-- | A verdict retains the exact fact it describes.
data Verdict a = Verified a Endorsement | Unverified a Reason

-- | An abstract, effect-polymorphic fact verifier.
newtype Verifier w m = Verifier
    { forall w (m :: * -> *).
Verifier w m -> forall a. Evidenced w a -> m (Verdict a)
verifyFact :: forall a. Evidenced w a -> m (Verdict a)
    }

-- | The sole configured Demo 1 policy; never upgrades a raw fact.
unverifiedVerifier :: (Applicative m) => Verifier NoWitness m
unverifiedVerifier :: forall (m :: * -> *). Applicative m => Verifier NoWitness m
unverifiedVerifier =
    (forall a. Evidenced NoWitness a -> m (Verdict a))
-> Verifier NoWitness m
forall w (m :: * -> *).
(forall a. Evidenced w a -> m (Verdict a)) -> Verifier w m
Verifier
        (\Evidenced NoWitness a
fact -> Verdict a -> m (Verdict a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Reason -> Verdict a
forall a. a -> Reason -> Verdict a
Unverified (Evidenced NoWitness a -> a
forall w a. Evidenced w a -> a
value Evidenced NoWitness a
fact) Reason
NoVerifierConfigured))