Skip to content

Commit

Permalink
Fixed the certStateSpec, from issue #4775 (#4783)
Browse files Browse the repository at this point in the history
  • Loading branch information
TimSheard authored Dec 5, 2024
1 parent b14ba81 commit 172dca9
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 15 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ import Test.QuickCheck (generate)
-- and the EraSpecLedger class has methods that asbtract over those changes.
class
( EraSpecTxOut era fn
, Era era
, HasSpec fn (GovState era)
) =>
EraSpecLedger era fn
Expand Down Expand Up @@ -213,17 +214,29 @@ aggregateDRep m = Map.foldlWithKey accum Map.empty m
dstateSpec ::
forall era fn.
EraSpecLedger era fn =>
Term fn (Set (Credential 'DRepRole (EraCrypto era))) ->
Term fn AccountState ->
Term fn (Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))) ->
Specification fn (DState era)
dstateSpec acct poolreg = constrained $ \ [var| ds |] ->
dstateSpec drepRoleCredSet acct poolreg = constrained $ \ [var| ds |] ->
match ds $ \ [var|umap|] [var|futureGenDelegs|] [var|genDelegs|] [var|irewards|] ->
match umap $ \ [var|rdMap|] [var|ptrmap|] [var|sPoolMap|] [var|dRepMap|] ->
[ satisfies dRepMap TrueSpec
, -- This is passed to vstateSpec to enforce that the random set of DReps
-- delegated to actually exist and are registered, and that credentials appear as delegatees
-- TODO, see that more than one credential delegates to the same DRep
genHint 5 sPoolMap
[ -- This field, dRepMap, is passed to vstateSpec to enforce that the set of DReps
-- delegated to actually are registered and appear in the DState, and that every credential
-- delegated to a DRep, appears in the set of credentials for that DRep.
-- The dRepMap depends on the rdMap, so it is computed afterwards, forced by the reify
reify rdMap id $ \ [var|rdm|] ->
[ assert $ subset_ (dom_ dRepMap) (dom_ rdm)
, -- , assert $ sizeOf_ (dom_ dRepMap) >=. lit 1
forAll dRepMap $ \ [var|pair|] ->
match pair $ \_ [var|drep|] ->
(caseOn drep)
(branchW 3 $ \keyhash -> assert $ member_ (con @"KeyHashObj" keyhash) drepRoleCredSet)
(branchW 3 $ \scripthash -> assert $ member_ (con @"ScriptHashObj" scripthash) drepRoleCredSet)
(branchW 1 $ \_abstain -> True)
(branchW 1 $ \_noconfidence -> True)
]
, genHint 5 sPoolMap
, assertExplain (pure "The delegations delegate to actual pools") $
forAll (rng_ sPoolMap) (\ [var|keyhash|] -> member_ keyhash (dom_ poolreg))
, assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdMap
Expand Down Expand Up @@ -291,16 +304,15 @@ certStateSpec ::
Term fn AccountState ->
Term fn EpochNo ->
Specification fn (CertState era)
certStateSpec ctxDelegatees acct epoch = constrained $ \ [var|certState|] ->
certStateSpec drepRoleCredSet acct epoch = constrained $ \ [var|certState|] ->
match certState $ \ [var|vState|] [var|pState|] [var|dState|] ->
[ satisfies pState (pstateSpec epoch)
, reify pState psStakePoolParams $ \ [var|poolreg|] ->
[ dependsOn dState poolreg
, satisfies dState (dstateSpec acct poolreg)
, satisfies dState (dstateSpec drepRoleCredSet acct poolreg)
]
, reify dState getDelegatees $ \ [var|delegatees|] ->
[ satisfies vState (vstateSpec epoch delegatees)
, assert $ ctxDelegatees ==. dom_ delegatees
]
]

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -126,8 +126,9 @@ specSuite ::
Int -> Spec
specSuite n = do
soundSpecWith @(PState era) (5 * n) (pstateSpec !$! epochNoSpec)
soundSpecWith @(DState era) (5 * n) (dstateSpec @era !$! accountStateSpec !*! poolMapSpec)

soundSpecWith @(DState era)
(5 * n)
(dstateSpec @era !$! TrueSpec !*! accountStateSpec !*! poolMapSpec)
soundSpecWith @(VState era)
(10 * n)
( vstateSpec @_ @era
Expand All @@ -139,15 +140,15 @@ specSuite n = do
)
)
)

soundSpecWith @(CertState era)
(5 * n)
$ certStateSpec !$! TrueSpec !*! accountStateSpec !*! epochNoSpec
$ certStateSpec !$! (hasSize (rangeSize 6 10)) !*! accountStateSpec !*! epochNoSpec
soundSpecWith @(UTxOState era) (2 * n) (utxoStateGen @era)
soundSpecWith @(UTxO era) (5 * n) (utxoSpec !$! delegationsSpec)
soundSpecWith @(GovState era)
(2 * n)
(do x <- genFromSpec (pparamsSpec @ConwayFn); pure $ govStateSpec @era x)
soundSpecWith @(UTxOState era) (2 * n) (utxoStateGen @era)

soundSpecWith @(LedgerState era)
(2 * n)
(ledgerStateSpec <$> genConwayFn pparamsSpec !*! accountStateSpec !*! epochNoSpec)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -76,10 +76,11 @@ psX = do
dsX :: forall era. EraSpecLedger era ConwayFn => Gen (DState era)
dsX = do
acct <- genFromSpec @ConwayFn @AccountState accountStateSpec
drepRoleSet <- genFromSpec @ConwayFn TrueSpec
pools <-
genFromSpec @ConwayFn @(Map (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
(hasSize (rangeSize 8 8))
genFromSpec @ConwayFn @(DState era) (dstateSpec (lit acct) (lit pools))
genFromSpec @ConwayFn @(DState era) (dstateSpec @era (lit drepRoleSet) (lit acct) (lit pools))

vsX :: forall era. EraSpecPParams era => Gen (VState era)
vsX = do
Expand Down

0 comments on commit 172dca9

Please sign in to comment.