405 lines
14 KiB
Haskell
405 lines
14 KiB
Haskell
|
module Nuthatch.ModelEvidence
|
||
|
|
( ModelAction (..)
|
||
|
|
, ModelCheck (..)
|
||
|
|
, ScenarioEvidence (..)
|
||
|
|
, SnapshotFixture
|
||
|
|
, ProjectedFixture (..)
|
||
|
|
, allModelActions
|
||
|
|
, allModelChecks
|
||
|
|
, scenarioEvidence
|
||
|
|
, actionName
|
||
|
|
, checkName
|
||
|
|
, actionConstructor
|
||
|
|
, checkConstructor
|
||
|
|
, coveredAction
|
||
|
|
, checkedModel
|
||
|
|
, verifySnapshotFixtures
|
||
|
|
) where
|
||
|
|
|
||
|
|
import Data.Aeson
|
||
|
|
( FromJSON (parseJSON)
|
||
|
|
, (.:)
|
||
|
|
, withObject
|
||
|
|
)
|
||
|
|
import Data.Text (Text)
|
||
|
|
import qualified Data.Text as T
|
||
|
|
import qualified Data.Text.IO as T
|
||
|
|
import Nuthatch.Protocol
|
||
|
|
( MutationPhase (..)
|
||
|
|
, TerminalResult (..)
|
||
|
|
, decodeMutationPhase
|
||
|
|
, externalState
|
||
|
|
)
|
||
|
|
import Nuthatch.Types
|
||
|
|
|
||
|
|
data ModelAction
|
||
|
|
= ActionConflictRequest
|
||
|
|
| ActionDispatchEffect
|
||
|
|
| ActionExternalEffectApplied
|
||
|
|
| ActionExternalEffectNotApplied
|
||
|
|
| ActionFinalizeFailure
|
||
|
|
| ActionFinalizeSuccess
|
||
|
|
| ActionFirstRequest
|
||
|
|
| ActionLoseObjectStore
|
||
|
|
| ActionLosePostgres
|
||
|
|
| ActionLoseUploadBody
|
||
|
|
| ActionPrepareEffect
|
||
|
|
| ActionReplayRequest
|
||
|
|
| ActionRestoreObjectStore
|
||
|
|
| ActionRestorePostgres
|
||
|
|
| ActionSettleLostUpload
|
||
|
|
deriving stock (Bounded, Enum, Eq, Ord, Show)
|
||
|
|
|
||
|
|
data ModelCheck
|
||
|
|
= CheckAccountingAtQuiescence
|
||
|
|
| CheckActiveObjectConsistent
|
||
|
|
| CheckExternalStateConsistent
|
||
|
|
| CheckFingerprintBindsRequest
|
||
|
|
| CheckLocksConsistent
|
||
|
|
| CheckLostUploadEventuallyTerminal
|
||
|
|
| CheckObjectQuotaBound
|
||
|
|
| CheckObjectStateCovered
|
||
|
|
| CheckObjectStoreFailureFencesObjects
|
||
|
|
| CheckObservationConsistent
|
||
|
|
| CheckPersonalPoolsDisjoint
|
||
|
|
| CheckPersonalRequestsUseOwnPool
|
||
|
|
| CheckPostgresFailureFencesDurableState
|
||
|
|
| CheckQuotaReservationBound
|
||
|
|
| CheckRecordIdentityConsistent
|
||
|
|
| CheckRecordsNeverForgotten
|
||
|
|
| CheckRequestBindingsStable
|
||
|
|
| CheckReservationsConsistent
|
||
|
|
| CheckSettledEffectsDoNotMutate
|
||
|
|
| CheckTerminalRecordsStable
|
||
|
|
| CheckTypeOK
|
||
|
|
| CheckUnfinishedEventuallyTerminal
|
||
|
|
| CheckUploadBodyConsistent
|
||
|
|
deriving stock (Bounded, Enum, Eq, Ord, Show)
|
||
|
|
|
||
|
|
data ScenarioEvidence = ScenarioEvidence
|
||
|
|
{ scenarioAction :: ModelAction
|
||
|
|
, scenarioPrecondition :: Text
|
||
|
|
, scenarioObservation :: Text
|
||
|
|
, scenarioExpectedPost :: Text
|
||
|
|
}
|
||
|
|
deriving stock (Eq, Show)
|
||
|
|
|
||
|
|
data ConcreteSnapshot = ConcreteSnapshot
|
||
|
|
{ concreteIdentity :: Text
|
||
|
|
, concreteKind :: MutationKind
|
||
|
|
, concreteDeclaredSize :: Integer
|
||
|
|
, concreteContent :: Maybe ContentSha256
|
||
|
|
, concreteRecordState :: MutationState
|
||
|
|
, concreteExternalState :: ExternalState
|
||
|
|
, concreteUploadBodyAvailable :: Bool
|
||
|
|
, concreteKeyOwner :: Maybe Text
|
||
|
|
, concretePriorObject :: Maybe SnapshotObject
|
||
|
|
, concreteCurrentObject :: Maybe SnapshotObject
|
||
|
|
, concreteGrowthBytes :: Integer
|
||
|
|
, concreteReservedBytes :: Integer
|
||
|
|
, concreteUsedBytes :: Integer
|
||
|
|
, concreteLimitBytes :: Integer
|
||
|
|
, concreteMaxObjectBytes :: Integer
|
||
|
|
}
|
||
|
|
deriving stock (Eq, Show)
|
||
|
|
|
||
|
|
data SnapshotObject = SnapshotObject
|
||
|
|
{ snapshotObjectSize :: Integer
|
||
|
|
, snapshotObjectContent :: ContentSha256
|
||
|
|
}
|
||
|
|
deriving stock (Eq, Show)
|
||
|
|
|
||
|
|
data SnapshotFixture = SnapshotFixture
|
||
|
|
{ snapshotName :: Text
|
||
|
|
, snapshotConcrete :: ConcreteSnapshot
|
||
|
|
}
|
||
|
|
deriving stock (Eq, Show)
|
||
|
|
|
||
|
|
data AbstractSnapshot = AbstractSnapshot
|
||
|
|
{ abstractIdentity :: Text
|
||
|
|
, abstractKind :: MutationKind
|
||
|
|
, abstractDesiredObject :: Maybe SnapshotObject
|
||
|
|
, abstractPriorObject :: Maybe SnapshotObject
|
||
|
|
, abstractCurrentObject :: Maybe SnapshotObject
|
||
|
|
, abstractPhase :: MutationPhase
|
||
|
|
, abstractUploadBodyAvailable :: Bool
|
||
|
|
, abstractKeyOwner :: Maybe Text
|
||
|
|
, abstractGrowthBytes :: Integer
|
||
|
|
, abstractReservedBytes :: Integer
|
||
|
|
, abstractUsedBytes :: Integer
|
||
|
|
, abstractLimitBytes :: Integer
|
||
|
|
, abstractMaxObjectBytes :: Integer
|
||
|
|
}
|
||
|
|
deriving stock (Eq, Show)
|
||
|
|
|
||
|
|
data ProjectedFixture = ProjectedFixture
|
||
|
|
{ projectedName :: Text
|
||
|
|
, projectedPhase :: Text
|
||
|
|
}
|
||
|
|
deriving stock (Eq, Show)
|
||
|
|
|
||
|
|
instance FromJSON SnapshotFixture where
|
||
|
|
parseJSON = withObject "SnapshotFixture" $ \value ->
|
||
|
|
SnapshotFixture
|
||
|
|
<$> value .: "name"
|
||
|
|
<*> value .: "concrete"
|
||
|
|
|
||
|
|
instance FromJSON ConcreteSnapshot where
|
||
|
|
parseJSON = withObject "ConcreteSnapshot" $ \value -> do
|
||
|
|
kindText <- value .: "kind"
|
||
|
|
contentText <- value .: "content"
|
||
|
|
stateText <- value .: "record_state"
|
||
|
|
externalText <- value .: "external_state"
|
||
|
|
kind <- maybe (fail "invalid mutation kind") pure (parseKind kindText)
|
||
|
|
content <-
|
||
|
|
traverse
|
||
|
|
(either (fail . T.unpack) pure . validateContentSha256)
|
||
|
|
contentText
|
||
|
|
state <- maybe (fail "invalid mutation state") pure (parseState stateText)
|
||
|
|
external <-
|
||
|
|
maybe (fail "invalid external state") pure (parseExternal externalText)
|
||
|
|
ConcreteSnapshot
|
||
|
|
<$> value .: "identity"
|
||
|
|
<*> pure kind
|
||
|
|
<*> value .: "declared_size"
|
||
|
|
<*> pure content
|
||
|
|
<*> pure state
|
||
|
|
<*> pure external
|
||
|
|
<*> value .: "upload_body_available"
|
||
|
|
<*> value .: "key_owner"
|
||
|
|
<*> value .: "prior_object"
|
||
|
|
<*> value .: "current_object"
|
||
|
|
<*> value .: "growth_bytes"
|
||
|
|
<*> value .: "reserved_bytes"
|
||
|
|
<*> value .: "used_bytes"
|
||
|
|
<*> value .: "limit_bytes"
|
||
|
|
<*> value .: "max_object_bytes"
|
||
|
|
|
||
|
|
instance FromJSON SnapshotObject where
|
||
|
|
parseJSON = withObject "SnapshotObject" $ \value -> do
|
||
|
|
contentText <- value .: "content"
|
||
|
|
content <-
|
||
|
|
either (fail . T.unpack) pure (validateContentSha256 contentText)
|
||
|
|
SnapshotObject
|
||
|
|
<$> value .: "size"
|
||
|
|
<*> pure content
|
||
|
|
|
||
|
|
allModelActions :: [ModelAction]
|
||
|
|
allModelActions = [minBound .. maxBound]
|
||
|
|
|
||
|
|
allModelChecks :: [ModelCheck]
|
||
|
|
allModelChecks = [minBound .. maxBound]
|
||
|
|
|
||
|
|
actionName :: ModelAction -> Text
|
||
|
|
actionName = T.drop 6 . T.pack . show
|
||
|
|
|
||
|
|
checkName :: ModelCheck -> Text
|
||
|
|
checkName = T.drop 5 . T.pack . show
|
||
|
|
|
||
|
|
actionConstructor :: ModelAction -> Text
|
||
|
|
actionConstructor = T.pack . show
|
||
|
|
|
||
|
|
checkConstructor :: ModelCheck -> Text
|
||
|
|
checkConstructor = T.pack . show
|
||
|
|
|
||
|
|
coveredAction :: ModelAction -> IO ()
|
||
|
|
coveredAction action =
|
||
|
|
T.putStrLn ("protocol action covered: " <> actionName action)
|
||
|
|
|
||
|
|
checkedModel :: ModelCheck -> IO ()
|
||
|
|
checkedModel check =
|
||
|
|
T.putStrLn ("model check covered: " <> checkName check)
|
||
|
|
|
||
|
|
scenarioEvidence :: [ScenarioEvidence]
|
||
|
|
scenarioEvidence =
|
||
|
|
[ scenario ActionFirstRequest "postgresUp /\\ NoRecord" "first / pending or rejected" "prepared with lock and reservation iff CanAdmit; otherwise rejected"
|
||
|
|
, scenario ActionReplayRequest "postgresUp /\\ matching recorded request" "replay / StateResult" "protocol state unchanged"
|
||
|
|
, scenario ActionConflictRequest "postgresUp /\\ different request fingerprint" "conflict / conflict" "protocol state unchanged"
|
||
|
|
, scenario ActionPrepareEffect "postgresUp /\\ prepared" "NoObservation" "applying-idle"
|
||
|
|
, scenario ActionDispatchEffect "postgresUp /\\ objectStoreUp /\\ applying-idle" "NoObservation" "applying-pending without upload body"
|
||
|
|
, scenario ActionExternalEffectApplied "objectStoreUp /\\ applying-pending" "NoObservation" "applying-settled with desired object"
|
||
|
|
, scenario ActionExternalEffectNotApplied "objectStoreUp /\\ applying-pending" "NoObservation" "applying-settled with object unchanged"
|
||
|
|
, scenario ActionFinalizeSuccess "postgresUp /\\ objectStoreUp /\\ applying-settled /\\ object = desired" "NoObservation" "succeeded-idle without lock or reservation"
|
||
|
|
, scenario ActionFinalizeFailure "postgresUp /\\ objectStoreUp /\\ applying-settled /\\ object = prior" "NoObservation" "failed-idle without lock or reservation"
|
||
|
|
, scenario ActionLoseUploadBody "active put /\\ external idle /\\ upload body available" "NoObservation" "active-idle without upload body"
|
||
|
|
, scenario ActionSettleLostUpload "postgresUp /\\ objectStoreUp /\\ applying-idle /\\ upload body unavailable" "NoObservation" "applying-settled"
|
||
|
|
, scenario ActionLosePostgres "postgresUp /\\ losses below bound" "NoObservation" "postgres down; protocol state unchanged"
|
||
|
|
, scenario ActionRestorePostgres "~postgresUp" "NoObservation" "postgres up; protocol state unchanged"
|
||
|
|
, scenario ActionLoseObjectStore "objectStoreUp /\\ losses below bound" "NoObservation" "object store down; protocol state unchanged"
|
||
|
|
, scenario ActionRestoreObjectStore "~objectStoreUp" "NoObservation" "object store up; protocol state unchanged"
|
||
|
|
]
|
||
|
|
where
|
||
|
|
scenario = ScenarioEvidence
|
||
|
|
|
||
|
|
verifySnapshotFixtures
|
||
|
|
:: [SnapshotFixture]
|
||
|
|
-> Either Text [ProjectedFixture]
|
||
|
|
verifySnapshotFixtures fixtures = do
|
||
|
|
projected <- traverse projectFixture fixtures
|
||
|
|
let phases = map projectedPhase projected
|
||
|
|
concrete = map snapshotConcrete fixtures
|
||
|
|
requireCoverage "prepared" phases
|
||
|
|
requireCoverage "applying-idle" phases
|
||
|
|
requireCoverage "applying-pending" phases
|
||
|
|
requireCoverage "applying-settled" phases
|
||
|
|
requireCoverage "terminal" phases
|
||
|
|
requireCoverage "rejected" phases
|
||
|
|
requireAny "lock" ((/= Nothing) . concreteKeyOwner) concrete
|
||
|
|
requireAny "reservation" ((> 0) . concreteReservedBytes) concrete
|
||
|
|
requireAny "prior object" ((/= Nothing) . concretePriorObject) concrete
|
||
|
|
requireAny "desired object" ((== Put) . concreteKind) concrete
|
||
|
|
requireAny "object" ((/= Nothing) . concreteCurrentObject) concrete
|
||
|
|
requireAny "upload body" concreteUploadBodyAvailable concrete
|
||
|
|
pure projected
|
||
|
|
|
||
|
|
projectFixture :: SnapshotFixture -> Either Text ProjectedFixture
|
||
|
|
projectFixture SnapshotFixture{..} = do
|
||
|
|
projected <- projectSnapshot snapshotConcrete
|
||
|
|
validateSnapshot snapshotName projected
|
||
|
|
pure ProjectedFixture
|
||
|
|
{ projectedName = snapshotName
|
||
|
|
, projectedPhase = phaseName (abstractPhase projected)
|
||
|
|
}
|
||
|
|
|
||
|
|
projectSnapshot :: ConcreteSnapshot -> Either Text AbstractSnapshot
|
||
|
|
projectSnapshot ConcreteSnapshot{..} = do
|
||
|
|
phase <-
|
||
|
|
maybe
|
||
|
|
(Left "ExternalStateConsistent")
|
||
|
|
Right
|
||
|
|
(decodeMutationPhase concreteRecordState concreteExternalState)
|
||
|
|
desired <-
|
||
|
|
case (concreteKind, concreteDeclaredSize, concreteContent) of
|
||
|
|
(Put, size, Just content)
|
||
|
|
| size > 0 ->
|
||
|
|
Right (Just (SnapshotObject size content))
|
||
|
|
(Delete, 0, Nothing) -> Right Nothing
|
||
|
|
_ -> Left "ValidRequest"
|
||
|
|
pure AbstractSnapshot
|
||
|
|
{ abstractIdentity = concreteIdentity
|
||
|
|
, abstractKind = concreteKind
|
||
|
|
, abstractDesiredObject = desired
|
||
|
|
, abstractPriorObject = concretePriorObject
|
||
|
|
, abstractCurrentObject = concreteCurrentObject
|
||
|
|
, abstractPhase = phase
|
||
|
|
, abstractUploadBodyAvailable = concreteUploadBodyAvailable
|
||
|
|
, abstractKeyOwner = concreteKeyOwner
|
||
|
|
, abstractGrowthBytes = concreteGrowthBytes
|
||
|
|
, abstractReservedBytes = concreteReservedBytes
|
||
|
|
, abstractUsedBytes = concreteUsedBytes
|
||
|
|
, abstractLimitBytes = concreteLimitBytes
|
||
|
|
, abstractMaxObjectBytes = concreteMaxObjectBytes
|
||
|
|
}
|
||
|
|
|
||
|
|
validateSnapshot :: Text -> AbstractSnapshot -> Either Text ()
|
||
|
|
validateSnapshot label snapshot = do
|
||
|
|
let active =
|
||
|
|
case abstractPhase snapshot of
|
||
|
|
PhasePrepared -> True
|
||
|
|
PhaseApplying _ -> True
|
||
|
|
PhaseTerminal _ -> False
|
||
|
|
idle = externalState (abstractPhase snapshot) == ExtIdle
|
||
|
|
priorSize = objectSize (abstractPriorObject snapshot)
|
||
|
|
desiredSize = objectSize (abstractDesiredObject snapshot)
|
||
|
|
currentSize = objectSize (abstractCurrentObject snapshot)
|
||
|
|
expectedGrowth = max 0 (desiredSize - priorSize)
|
||
|
|
require
|
||
|
|
(validObject (abstractPriorObject snapshot))
|
||
|
|
"ObjectValues"
|
||
|
|
require
|
||
|
|
(validObject (abstractDesiredObject snapshot))
|
||
|
|
"ObjectValues"
|
||
|
|
require
|
||
|
|
(validObject (abstractCurrentObject snapshot))
|
||
|
|
"ObjectValues"
|
||
|
|
require
|
||
|
|
( all
|
||
|
|
((<= abstractMaxObjectBytes snapshot) . objectSize)
|
||
|
|
[ abstractPriorObject snapshot
|
||
|
|
, abstractDesiredObject snapshot
|
||
|
|
, abstractCurrentObject snapshot
|
||
|
|
]
|
||
|
|
)
|
||
|
|
"ObjectValues"
|
||
|
|
require
|
||
|
|
( not active
|
||
|
|
|| abstractCurrentObject snapshot
|
||
|
|
`elem` [abstractPriorObject snapshot, abstractDesiredObject snapshot]
|
||
|
|
)
|
||
|
|
"ActiveObjectConsistent"
|
||
|
|
require
|
||
|
|
( not (abstractUploadBodyAvailable snapshot)
|
||
|
|
|| (active && abstractKind snapshot == Put && idle)
|
||
|
|
)
|
||
|
|
"UploadBodyConsistent"
|
||
|
|
require
|
||
|
|
((abstractKeyOwner snapshot == Just (abstractIdentity snapshot)) == active)
|
||
|
|
"LocksConsistent"
|
||
|
|
require
|
||
|
|
( abstractReservedBytes snapshot
|
||
|
|
== if active then abstractGrowthBytes snapshot else 0
|
||
|
|
)
|
||
|
|
"ReservationsConsistent"
|
||
|
|
require
|
||
|
|
(abstractGrowthBytes snapshot == expectedGrowth)
|
||
|
|
"Reservation"
|
||
|
|
require
|
||
|
|
( abstractUsedBytes snapshot + abstractReservedBytes snapshot
|
||
|
|
<= abstractLimitBytes snapshot
|
||
|
|
)
|
||
|
|
"QuotaReservationBound"
|
||
|
|
require
|
||
|
|
(currentSize <= abstractUsedBytes snapshot + abstractReservedBytes snapshot)
|
||
|
|
"ObjectStateCovered"
|
||
|
|
require
|
||
|
|
(currentSize <= abstractLimitBytes snapshot)
|
||
|
|
"ObjectQuotaBound"
|
||
|
|
require
|
||
|
|
(active || abstractUsedBytes snapshot == currentSize)
|
||
|
|
"AccountingAtQuiescence"
|
||
|
|
case abstractPhase snapshot of
|
||
|
|
PhaseTerminal TerminalRejected ->
|
||
|
|
require
|
||
|
|
( abstractUsedBytes snapshot
|
||
|
|
+ abstractReservedBytes snapshot
|
||
|
|
+ abstractGrowthBytes snapshot
|
||
|
|
> abstractLimitBytes snapshot
|
||
|
|
)
|
||
|
|
"CanAdmit"
|
||
|
|
_ -> Right ()
|
||
|
|
require (abstractGrowthBytes snapshot >= 0) "growth must be natural"
|
||
|
|
require (abstractReservedBytes snapshot >= 0) "reservation must be natural"
|
||
|
|
require (abstractUsedBytes snapshot >= 0) "used bytes must be natural"
|
||
|
|
require (abstractLimitBytes snapshot >= 0) "limit must be natural"
|
||
|
|
require (abstractMaxObjectBytes snapshot > 0) "MaxObjectSize"
|
||
|
|
where
|
||
|
|
require condition invariant =
|
||
|
|
if condition then Right () else Left (label <> ": " <> invariant)
|
||
|
|
|
||
|
|
objectSize :: Maybe SnapshotObject -> Integer
|
||
|
|
objectSize = maybe 0 snapshotObjectSize
|
||
|
|
|
||
|
|
validObject :: Maybe SnapshotObject -> Bool
|
||
|
|
validObject Nothing = True
|
||
|
|
validObject (Just SnapshotObject{..}) = snapshotObjectSize > 0
|
||
|
|
|
||
|
|
phaseName :: MutationPhase -> Text
|
||
|
|
phaseName = \case
|
||
|
|
PhasePrepared -> "prepared"
|
||
|
|
PhaseApplying ExtIdle -> "applying-idle"
|
||
|
|
PhaseApplying ExtPending -> "applying-pending"
|
||
|
|
PhaseApplying ExtSettled -> "applying-settled"
|
||
|
|
PhaseTerminal TerminalRejected -> "rejected"
|
||
|
|
PhaseTerminal _ -> "terminal"
|
||
|
|
|
||
|
|
requireCoverage :: Text -> [Text] -> Either Text ()
|
||
|
|
requireCoverage expected actual =
|
||
|
|
if expected `elem` actual
|
||
|
|
then Right ()
|
||
|
|
else Left ("missing projection coverage: " <> expected)
|
||
|
|
|
||
|
|
requireAny :: Text -> (value -> Bool) -> [value] -> Either Text ()
|
||
|
|
requireAny label predicate values =
|
||
|
|
if any predicate values
|
||
|
|
then Right ()
|
||
|
|
else Left ("missing projection coverage: " <> label)
|