Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Require the caller of checkLeaderValue to provide bounds. #2776

Merged
merged 1 commit into from
May 11, 2022
Merged

Require the caller of checkLeaderValue to provide bounds. #2776

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 32 additions & 10 deletions libs/cardano-protocol-tpraos/src/Cardano/Protocol/TPraos/BHeader.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
Expand All @@ -11,14 +10,15 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}

module Cardano.Protocol.TPraos.BHeader
( HashHeader (..),
PrevHash (..),
BHeader (BHeader),
BHBody (..),
LastAppliedBlock (..),
BoundedNatural (bvValue, bvMaxValue),
assertBoundedNatural,
lastAppliedHash,
issuerIDfromBHBody,
checkLeaderValue,
Expand Down Expand Up @@ -367,6 +367,26 @@ bhbody (BHeader b _) = b
hBbsize :: BHBody crypto -> Natural
hBbsize = bsize

-- | Natural value with some additional bound. It must always be the base that
-- 'bvValue <= bvMaxValue'. The creator is responsible for checking this value.
data BoundedNatural = UnsafeBoundedNatural
{ bvMaxValue :: Natural,
bvValue :: Natural
}

-- | Assert that a natural is bounded by a certain value. Throws an error when
-- this is not the case.
assertBoundedNatural ::
-- | Maximum bound
Natural ->
-- | Value
Natural ->
BoundedNatural
assertBoundedNatural maxVal val =
if val <= maxVal
then UnsafeBoundedNatural maxVal val
else error $ show val <> " is greater than max value " <> show maxVal

-- | Check that the certified VRF output, when used as a natural, is valid for
-- being slot leader.
checkLeaderValue ::
Expand All @@ -377,7 +397,10 @@ checkLeaderValue ::
ActiveSlotCoeff ->
Bool
checkLeaderValue certVRF σ f =
checkLeaderNatValue certVRF (VRF.getOutputVRFNatural certVRF) σ f
checkLeaderNatValue (assertBoundedNatural certNatMax (VRF.getOutputVRFNatural certVRF)) σ f
where
certNatMax :: Natural
certNatMax = (2 :: Natural) ^ (8 * VRF.sizeOutputVRF certVRF)

-- | Check that the certified input natural is valid for being slot leader. This
-- means we check that
Expand All @@ -403,14 +426,13 @@ checkLeaderValue certVRF σ f =
-- --- = ----- = ---------------------------- = ----------------------
-- q 1 - p 1 - (certNat / certNatMax) (certNatMax - certNat)
checkLeaderNatValue ::
forall proxy v.
(VRF.VRFAlgorithm v) =>
proxy v ->
Natural ->
-- | Certified nat value
BoundedNatural ->
-- | Stake proportion
Rational ->
ActiveSlotCoeff ->
Bool
checkLeaderNatValue prox certNat σ f =
checkLeaderNatValue bn σ f =
if activeSlotVal f == maxBound
then -- If the active slot coefficient is equal to one,
-- then nearly every stake pool can produce a block every slot.
Expand All @@ -424,12 +446,12 @@ checkLeaderNatValue prox certNat σ f =
BELOW _ _ -> True
MaxReached _ -> False
where
certNatMax :: Natural
certNatMax = (2 :: Natural) ^ (8 * VRF.sizeOutputVRF prox)
c, recip_q, x :: FixedPoint
c = activeSlotLog f
recip_q = fromRational (toInteger certNatMax % toInteger (certNatMax - certNat))
x = -fromRational σ * c
certNatMax = bvMaxValue bn
certNat = bvValue bn

seedEta :: Nonce
seedEta = mkNonceFromNumber 0
Expand Down