{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Crypto.Leios (spec, exampleCert) where

import Cardano.Crypto.DSIGN (
  DSIGNAlgorithm (deriveVerKeyDSIGN),
  genKeyDSIGN,
  seedSizeDSIGN,
  signDSIGN,
 )
import Cardano.Crypto.Leios (
  AggregationError (..),
  LeiosCert (..),
  LeiosCommittee (..),
  LeiosDSIGN,
  LeiosSignature,
  LeiosSigningKey,
  LeiosVoter (..),
  LeiosVoterId (..),
  VerificationError (..),
  Weight,
  aggregateLeiosCert,
  getLeiosVoterId,
  leiosSignContext,
  resolveLeiosVoter,
  verifyLeiosCert,
 )
import Cardano.Crypto.Seed (mkSeedFromBytes)
import qualified Data.ByteString as BS
import Data.Foldable (toList)
import Data.List.NonEmpty (NonEmpty (..), fromList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Proxy (Proxy (Proxy))
import qualified Data.Vector.Strict as V
import Data.Word (Word16, Word8)
import Test.Cardano.Base.Bytes (genByteString)
import Test.Hspec (Spec, context, describe)
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck (
  Property,
  chooseInt,
  counterexample,
  forAll,
  (===),
 )
import qualified Test.QuickCheck as QC

spec :: Spec
spec :: Spec
spec = do
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"LeiosCert" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"aggregateLeiosCert" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"rejects an out-of-range LeiosVoterId" Property
prop_aggregateLeiosCert_rejects_out_of_range
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"rejects empty contributions" Property
prop_aggregateLeiosCert_rejects_empty

    String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"verifyLeiosCert" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"with a valid certificate" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"accepts a full-committee aggregation" Property
prop_verifyLeiosCert_accepts_aggregated
        String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"accepts a subset of signers above threshold" Property
prop_verifyLeiosCert_accepts_subset
      String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
context String
"with an invalid certificate" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
        String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"rejects a wrong message" Property
prop_verifyLeiosCert_rejects_wrong_message
        String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"rejects when total weight is below threshold" Property
prop_verifyLeiosCert_rejects_below_threshold
        String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"rejects a bitfield wider than the committee" Property
prop_verifyLeiosCert_rejects_oversized_signers
        String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"rejects a tampered bitfield" Property
prop_verifyLeiosCert_rejects_tampered_bitfield

  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"LeiosCommittee" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop
      String
"getLeiosVoterId and resolveLeiosVoter agree on verification keys"
      Property
prop_resolveVoter_getVoterId_inverse
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"getLeiosVoterId returns the first matching index" Property
prop_getVoterId_returns_first_index

exampleCert :: LeiosCert
exampleCert :: LeiosCert
exampleCert = case LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> Either AggregationError LeiosCert
aggregateLeiosCert LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contributions of
  Right LeiosCert
c -> LeiosCert
c
  Left AggregationError
e -> String -> LeiosCert
forall a. HasCallStack => String -> a
error (String
"exampleCert: aggregation failed: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> AggregationError -> String
forall a. Show a => a -> String
show AggregationError
e)
  where
    (NonEmpty LeiosSigningKey
sks, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
1000
    msg :: ByteString
msg = ByteString
"leios-golden-message" :: BS.ByteString
    contributions :: Map LeiosVoterId LeiosSignature
contributions = ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
msg ([Int] -> [LeiosSigningKey] -> [(Int, LeiosSigningKey)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] (NonEmpty LeiosSigningKey -> [LeiosSigningKey]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty LeiosSigningKey
sks))

-- * LeiosVoterId committee lookup

-- | 'getLeiosVoterId' and 'resolveLeiosVoter' are mutual inverses on the verification
-- key projection: for any voter in the committee, looking up its 'LeiosVoterId'
-- via its key and resolving back to a 'LeiosVoter' yields the same key.
prop_resolveVoter_getVoterId_inverse :: Property
prop_resolveVoter_getVoterId_inverse :: Property
prop_resolveVoter_getVoterId_inverse =
  Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Int
genN ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let (NonEmpty LeiosSigningKey
_, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
        voters :: [LeiosVoter]
voters = Vector LeiosVoter -> [LeiosVoter]
forall a. Vector a -> [a]
V.toList LeiosCommittee
committee.leiosCommitteeVoters
     in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
QC.conjoin
          [ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"voter index " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              case HasCallStack =>
LeiosVerificationKey -> LeiosCommittee -> Maybe LeiosVoterId
LeiosVerificationKey -> LeiosCommittee -> Maybe LeiosVoterId
getLeiosVoterId (LeiosVoter -> LeiosVerificationKey
voterVKey LeiosVoter
voter) LeiosCommittee
committee of
                Maybe LeiosVoterId
Nothing -> Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
False
                Just LeiosVoterId
vid ->
                  case LeiosCommittee -> LeiosVoterId -> Maybe LeiosVoter
resolveLeiosVoter LeiosCommittee
committee LeiosVoterId
vid of
                    Maybe LeiosVoter
Nothing -> Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
False
                    Just LeiosVoter
voter' -> LeiosVoter -> LeiosVerificationKey
voterVKey LeiosVoter
voter' LeiosVerificationKey -> LeiosVerificationKey -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LeiosVoter -> LeiosVerificationKey
voterVKey LeiosVoter
voter
          | (Int
i :: Int, LeiosVoter
voter) <- [Int] -> [LeiosVoter] -> [(Int, LeiosVoter)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [LeiosVoter]
voters
          ]

-- | When the committee carries duplicate verification keys, 'getLeiosVoterId'
-- returns the smallest matching index. We don't deduplicate committees
-- internally; downstream selection is expected to.
prop_getVoterId_returns_first_index :: Property
prop_getVoterId_returns_first_index :: Property
prop_getVoterId_returns_first_index =
  Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Int
genN ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
    let (NonEmpty LeiosSigningKey
_, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
        voters :: [LeiosVoter]
voters = Vector LeiosVoter -> [LeiosVoter]
forall a. Vector a -> [a]
V.toList LeiosCommittee
committee.leiosCommitteeVoters
     in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
QC.conjoin
          [ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"first occurrence at " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              HasCallStack =>
LeiosVerificationKey -> LeiosCommittee -> Maybe LeiosVoterId
LeiosVerificationKey -> LeiosCommittee -> Maybe LeiosVoterId
getLeiosVoterId (LeiosVoter -> LeiosVerificationKey
voterVKey LeiosVoter
voter) LeiosCommittee
duped
                Maybe LeiosVoterId -> Maybe LeiosVoterId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LeiosVoterId -> Maybe LeiosVoterId
forall a. a -> Maybe a
Just (Word16 -> LeiosVoterId
LeiosVoterId (Int -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i))
          | let duped :: LeiosCommittee
duped =
                  Vector LeiosVoter -> LeiosCommittee
LeiosCommittee
                    (LeiosCommittee
committee.leiosCommitteeVoters Vector LeiosVoter -> Vector LeiosVoter -> Vector LeiosVoter
forall a. Semigroup a => a -> a -> a
<> LeiosCommittee
committee.leiosCommitteeVoters)
          , (Int
i :: Int, LeiosVoter
voter) <- [Int] -> [LeiosVoter] -> [(Int, LeiosVoter)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [LeiosVoter]
voters
          ]

-- * aggregate / verify

-- | Equal-weighted committee of @n@ voters derived from a fixed seed pattern.
-- Returns the signing keys alongside the committee so tests can produce
-- contributions. The 'NonEmpty' return reflects the @n ≥ 1@ precondition and
-- gives tests a total 'head' for "any-one-signer" cases.
fixedCommittee :: Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee :: Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n =
  ( NonEmpty LeiosSigningKey
sks
  , Vector LeiosVoter -> LeiosCommittee
LeiosCommittee
      ( [LeiosVoter] -> Vector LeiosVoter
forall a. [a] -> Vector a
V.fromList
          [Weight -> LeiosVerificationKey -> LeiosVoter
LeiosVoter (Weight
1 Weight -> Weight -> Weight
forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Weight Int
n) (LeiosSigningKey -> LeiosVerificationKey
forall v. DSIGNAlgorithm v => SignKeyDSIGN v -> VerKeyDSIGN v
deriveVerKeyDSIGN LeiosSigningKey
sk) | LeiosSigningKey
sk <- NonEmpty LeiosSigningKey -> [LeiosSigningKey]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty LeiosSigningKey
sks]
      )
  )
  where
    seedLen :: Int
seedLen = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Word @Int (Proxy LeiosDSIGN -> Word
forall v (proxy :: * -> *). DSIGNAlgorithm v => proxy v -> Word
seedSizeDSIGN (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @LeiosDSIGN))
    sks :: NonEmpty LeiosSigningKey
sks =
      [LeiosSigningKey] -> NonEmpty LeiosSigningKey
forall a. HasCallStack => [a] -> NonEmpty a
fromList
        [ forall v. DSIGNAlgorithm v => Seed -> SignKeyDSIGN v
genKeyDSIGN @LeiosDSIGN (ByteString -> Seed
mkSeedFromBytes (Int -> Word8 -> ByteString
BS.replicate Int
seedLen (forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Word8 Int
i)))
        | Int
i <- [Int
1 .. Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1 Int
n]
        ]

-- | Default committee size range exercised by the verify/aggregate properties.
-- 1 ≤ n ≤ 16 covers single-voter (n=1), single-byte bitfield (n ≤ 8) and the
-- two-byte boundary (n=9..16).
genN :: QC.Gen Int
genN :: Gen Int
genN = (Int, Int) -> Gen Int
chooseInt (Int
1, Int
16)

genMsg :: QC.Gen BS.ByteString
genMsg :: Gen ByteString
genMsg = (Int, Int) -> Gen Int
chooseInt (Int
0, Int
64) Gen Int -> (Int -> Gen ByteString) -> Gen ByteString
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> Gen ByteString
genByteString

-- | Sign @msg@ with each of the given keys and pack them into a 'Map' keyed
-- by 'LeiosVoterId', matching the input shape of 'aggregateLeiosCert'.
signContribs :: BS.ByteString -> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs :: ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
msg [(Int, LeiosSigningKey)]
pairs =
  [(LeiosVoterId, LeiosSignature)] -> Map LeiosVoterId LeiosSignature
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [(Word16 -> LeiosVoterId
LeiosVoterId (forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Word16 Int
i), ContextDSIGN LeiosDSIGN
-> ByteString -> LeiosSigningKey -> LeiosSignature
forall v a.
(DSIGNAlgorithm v, Signable v a, HasCallStack) =>
ContextDSIGN v -> a -> SignKeyDSIGN v -> SigDSIGN v
forall a.
(Signable LeiosDSIGN a, HasCallStack) =>
ContextDSIGN LeiosDSIGN -> a -> LeiosSigningKey -> LeiosSignature
signDSIGN ContextDSIGN LeiosDSIGN
BLS12381SignContext
leiosSignContext ByteString
msg LeiosSigningKey
sk) | (Int
i, LeiosSigningKey
sk) <- [(Int, LeiosSigningKey)]
pairs]

-- | Aggregate or fail the property with the error.
aggregateOrFail ::
  LeiosCommittee ->
  Map LeiosVoterId LeiosSignature ->
  (LeiosCert -> Property) ->
  Property
aggregateOrFail :: LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contributions LeiosCert -> Property
k = case LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> Either AggregationError LeiosCert
aggregateLeiosCert LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contributions of
  Right LeiosCert
c -> LeiosCert -> Property
k LeiosCert
c
  Left AggregationError
e -> String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (AggregationError -> String
forall a. Show a => a -> String
show AggregationError
e) (Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
False)

-- | All committee members sign the same message; the resulting cert verifies
-- against that committee, threshold and message, and reports full weight.
prop_verifyLeiosCert_accepts_aggregated :: Property
prop_verifyLeiosCert_accepts_aggregated :: Property
prop_verifyLeiosCert_accepts_aggregated = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Int
genN ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n -> Gen ByteString -> (ByteString -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen ByteString
genMsg ((ByteString -> Property) -> Property)
-> (ByteString -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ByteString
msg ->
  let (NonEmpty LeiosSigningKey
sks, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
      contributions :: Map LeiosVoterId LeiosSignature
contributions = ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
msg ([Int] -> [LeiosSigningKey] -> [(Int, LeiosSigningKey)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (NonEmpty LeiosSigningKey -> [LeiosSigningKey]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty LeiosSigningKey
sks))
   in LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contributions ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
cert ->
        LeiosCommittee
-> Weight
-> ByteString
-> LeiosCert
-> Either VerificationError Weight
forall msg.
SignableRepresentation msg =>
LeiosCommittee
-> Weight -> msg -> LeiosCert -> Either VerificationError Weight
verifyLeiosCert LeiosCommittee
committee Weight
1 ByteString
msg LeiosCert
cert Either VerificationError Weight
-> Either VerificationError Weight -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Weight -> Either VerificationError Weight
forall a b. b -> Either a b
Right Weight
1

-- | An arbitrary subset of @k@ committee members signs the same message.
-- The cert must verify against any threshold @≤ k/n@ and report weight
-- @k/n@. Catches bugs where the verifier doesn't actually sum the correct
-- subset of weights.
prop_verifyLeiosCert_accepts_subset :: Property
prop_verifyLeiosCert_accepts_subset :: Property
prop_verifyLeiosCert_accepts_subset = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Int
genN ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
  Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int, Int) -> Gen Int
chooseInt (Int
1, Int
n)) ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
k ->
    Gen ByteString -> (ByteString -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen ByteString
genMsg ((ByteString -> Property) -> Property)
-> (ByteString -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ByteString
msg ->
      let (NonEmpty LeiosSigningKey
sks, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
          contributions :: Map LeiosVoterId LeiosSignature
contributions = ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
msg (Int -> [(Int, LeiosSigningKey)] -> [(Int, LeiosSigningKey)]
forall a. Int -> [a] -> [a]
take Int
k ([Int] -> [LeiosSigningKey] -> [(Int, LeiosSigningKey)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (NonEmpty LeiosSigningKey -> [LeiosSigningKey]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty LeiosSigningKey
sks)))
          expectedWeight :: Weight
expectedWeight = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Weight Int
k Weight -> Weight -> Weight
forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Weight Int
n
       in LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contributions ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
cert ->
            LeiosCommittee
-> Weight
-> ByteString
-> LeiosCert
-> Either VerificationError Weight
forall msg.
SignableRepresentation msg =>
LeiosCommittee
-> Weight -> msg -> LeiosCert -> Either VerificationError Weight
verifyLeiosCert LeiosCommittee
committee Weight
expectedWeight ByteString
msg LeiosCert
cert Either VerificationError Weight
-> Either VerificationError Weight -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Weight -> Either VerificationError Weight
forall a b. b -> Either a b
Right Weight
expectedWeight

-- | A cert built over message @m1@ must not verify against message @m2@.
prop_verifyLeiosCert_rejects_wrong_message :: Property
prop_verifyLeiosCert_rejects_wrong_message :: Property
prop_verifyLeiosCert_rejects_wrong_message = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Int
genN ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
  let (NonEmpty LeiosSigningKey
sks, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
      m1 :: ByteString
m1 = ByteString
"leios-message-one" :: BS.ByteString
      m2 :: ByteString
m2 = ByteString
"leios-message-two" :: BS.ByteString
      contributions :: Map LeiosVoterId LeiosSignature
contributions = ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
m1 ([Int] -> [LeiosSigningKey] -> [(Int, LeiosSigningKey)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (NonEmpty LeiosSigningKey -> [LeiosSigningKey]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty LeiosSigningKey
sks))
   in LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contributions ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
cert ->
        LeiosCommittee
-> Weight
-> ByteString
-> LeiosCert
-> Either VerificationError Weight
forall msg.
SignableRepresentation msg =>
LeiosCommittee
-> Weight -> msg -> LeiosCert -> Either VerificationError Weight
verifyLeiosCert LeiosCommittee
committee Weight
1 ByteString
m2 LeiosCert
cert Either VerificationError Weight
-> Either VerificationError Weight -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== VerificationError -> Either VerificationError Weight
forall a b. a -> Either a b
Left VerificationError
InvalidSignature

-- | A cert whose signers' summed weight is below the threshold must be
-- rejected with 'InsufficientWeight', without ever performing the BLS
-- pairing. Uses n ≥ 2 so a single signer's weight @1/n@ is strictly less
-- than the full-weight threshold.
prop_verifyLeiosCert_rejects_below_threshold :: Property
prop_verifyLeiosCert_rejects_below_threshold :: Property
prop_verifyLeiosCert_rejects_below_threshold = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int, Int) -> Gen Int
chooseInt (Int
2, Int
16)) ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
  let (LeiosSigningKey
sk0 :| [LeiosSigningKey]
_, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
      msg :: ByteString
msg = ByteString
"leios-quorum-test" :: BS.ByteString
      contributions :: Map LeiosVoterId LeiosSignature
contributions = ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
msg [(Int
0, LeiosSigningKey
sk0)]
   in LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contributions ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
cert ->
        LeiosCommittee
-> Weight
-> ByteString
-> LeiosCert
-> Either VerificationError Weight
forall msg.
SignableRepresentation msg =>
LeiosCommittee
-> Weight -> msg -> LeiosCert -> Either VerificationError Weight
verifyLeiosCert LeiosCommittee
committee Weight
1 ByteString
msg LeiosCert
cert
          Either VerificationError Weight
-> Either VerificationError Weight -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== VerificationError -> Either VerificationError Weight
forall a b. a -> Either a b
Left (Weight -> VerificationError
InsufficientWeight (Weight
1 Weight -> Weight -> Weight
forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Weight Int
n))

-- | A 'signers' bitfield whose byte length differs from @⌈n/8⌉@ must be
-- rejected as 'MalformedSigners' before any signature work is done. We
-- build a cert against committee A and verify against committee B whose
-- size sits in the next byte bucket (A's bitfield is one byte short of
-- what B expects).
prop_verifyLeiosCert_rejects_oversized_signers :: Property
prop_verifyLeiosCert_rejects_oversized_signers :: Property
prop_verifyLeiosCert_rejects_oversized_signers = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Int
genN ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
  let (NonEmpty LeiosSigningKey
sks, LeiosCommittee
committeeA) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
      (NonEmpty LeiosSigningKey
_, LeiosCommittee
committeeB) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
8)
      msg :: ByteString
msg = ByteString
"leios-malformed-test" :: BS.ByteString
      contributions :: Map LeiosVoterId LeiosSignature
contributions = ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
msg ([Int] -> [LeiosSigningKey] -> [(Int, LeiosSigningKey)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (NonEmpty LeiosSigningKey -> [LeiosSigningKey]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty LeiosSigningKey
sks))
   in LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committeeA Map LeiosVoterId LeiosSignature
contributions ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
cert ->
        LeiosCommittee
-> Weight
-> ByteString
-> LeiosCert
-> Either VerificationError Weight
forall msg.
SignableRepresentation msg =>
LeiosCommittee
-> Weight -> msg -> LeiosCert -> Either VerificationError Weight
verifyLeiosCert LeiosCommittee
committeeB Weight
1 ByteString
msg LeiosCert
cert Either VerificationError Weight
-> Either VerificationError Weight -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== VerificationError -> Either VerificationError Weight
forall a b. a -> Either a b
Left VerificationError
MalformedSigners

-- | A cert whose 'leiosCertSigners' bitfield disagrees with its 'leiosCertSignature'
-- must be rejected with 'InvalidSignature'. We construct two real certs
-- against the same committee (voter 0 alone, then voters 0+1), then splice
-- certA's signature with certB's bitfield. The bitfield claims voter 1 also
-- signed but the aggregate doesn't include voter 1's signature, so the BLS
-- pairing fails. Uses n ≥ 2 so there are at least two voters to splice.
prop_verifyLeiosCert_rejects_tampered_bitfield :: Property
prop_verifyLeiosCert_rejects_tampered_bitfield :: Property
prop_verifyLeiosCert_rejects_tampered_bitfield = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int, Int) -> Gen Int
chooseInt (Int
2, Int
16)) ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
  let (NonEmpty LeiosSigningKey
sks, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
      (LeiosSigningKey
sks0, LeiosSigningKey
sks1) = case NonEmpty LeiosSigningKey
sks of
        LeiosSigningKey
s0 :| (LeiosSigningKey
s1 : [LeiosSigningKey]
_) -> (LeiosSigningKey
s0, LeiosSigningKey
s1)
        NonEmpty LeiosSigningKey
_ -> String -> (LeiosSigningKey, LeiosSigningKey)
forall a. HasCallStack => String -> a
error String
"prop_verifyLeiosCert_rejects_tampered_bitfield: n >= 2 invariant violated"
      msg :: ByteString
msg = ByteString
"leios-tamper-test" :: BS.ByteString
      contribsAlone :: Map LeiosVoterId LeiosSignature
contribsAlone = ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
msg [(Int
0, LeiosSigningKey
sks0)]
      contribsPair :: Map LeiosVoterId LeiosSignature
contribsPair = ByteString
-> [(Int, LeiosSigningKey)] -> Map LeiosVoterId LeiosSignature
signContribs ByteString
msg [(Int
0, LeiosSigningKey
sks0), (Int
1, LeiosSigningKey
sks1)]
   in LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contribsAlone ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
certA ->
        LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contribsPair ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
certB ->
          let tampered :: LeiosCert
tampered = LeiosCert
certA {leiosCertSigners = certB.leiosCertSigners}
           in -- Threshold is below the tampered weight 2/n so we exercise the BLS
              -- pairing failure, not the short-circuit.
              LeiosCommittee
-> Weight
-> ByteString
-> LeiosCert
-> Either VerificationError Weight
forall msg.
SignableRepresentation msg =>
LeiosCommittee
-> Weight -> msg -> LeiosCert -> Either VerificationError Weight
verifyLeiosCert LeiosCommittee
committee (Weight
1 Weight -> Weight -> Weight
forall a. Fractional a => a -> a -> a
/ forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Weight Int
n) ByteString
msg LeiosCert
tampered
                Either VerificationError Weight
-> Either VerificationError Weight -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== VerificationError -> Either VerificationError Weight
forall a b. a -> Either a b
Left VerificationError
InvalidSignature

-- | A 'LeiosVoterId' past the committee bound is rejected at aggregation time.
prop_aggregateLeiosCert_rejects_out_of_range :: Property
prop_aggregateLeiosCert_rejects_out_of_range :: Property
prop_aggregateLeiosCert_rejects_out_of_range = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Int
genN ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
  Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int, Int) -> Gen Int
chooseInt (Int
n, Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
100)) ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
badIdx ->
    let (LeiosSigningKey
sk0 :| [LeiosSigningKey]
_, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
        msg :: ByteString
msg = ByteString
"x" :: BS.ByteString
        bad :: LeiosVoterId
bad = Word16 -> LeiosVoterId
LeiosVoterId (forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Word16 Int
badIdx)
        contributions :: Map LeiosVoterId LeiosSignature
contributions = LeiosVoterId -> LeiosSignature -> Map LeiosVoterId LeiosSignature
forall k a. k -> a -> Map k a
Map.singleton LeiosVoterId
bad (ContextDSIGN LeiosDSIGN
-> ByteString -> LeiosSigningKey -> LeiosSignature
forall v a.
(DSIGNAlgorithm v, Signable v a, HasCallStack) =>
ContextDSIGN v -> a -> SignKeyDSIGN v -> SigDSIGN v
forall a.
(Signable LeiosDSIGN a, HasCallStack) =>
ContextDSIGN LeiosDSIGN -> a -> LeiosSigningKey -> LeiosSignature
signDSIGN ContextDSIGN LeiosDSIGN
BLS12381SignContext
leiosSignContext ByteString
msg LeiosSigningKey
sk0)
     in LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> Either AggregationError LeiosCert
aggregateLeiosCert LeiosCommittee
committee Map LeiosVoterId LeiosSignature
contributions Either AggregationError LeiosCert
-> Either AggregationError LeiosCert -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== AggregationError -> Either AggregationError LeiosCert
forall a b. a -> Either a b
Left (NonEmpty LeiosVoterId -> AggregationError
VoterIdsOutOfBounds (LeiosVoterId
bad LeiosVoterId -> [LeiosVoterId] -> NonEmpty LeiosVoterId
forall a. a -> [a] -> NonEmpty a
:| []))

-- | Aggregating an empty contribution set must fail: the underlying BLS
-- 'aggregateSigsDSIGN' rejects the empty input, which surfaces as
-- 'BLSAggregationFailed'. We don't pin the exact message string.
prop_aggregateLeiosCert_rejects_empty :: Property
prop_aggregateLeiosCert_rejects_empty :: Property
prop_aggregateLeiosCert_rejects_empty = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen Int
genN ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
  let (NonEmpty LeiosSigningKey
_, LeiosCommittee
committee) = Int -> (NonEmpty LeiosSigningKey, LeiosCommittee)
fixedCommittee Int
n
   in case LeiosCommittee
-> Map LeiosVoterId LeiosSignature
-> Either AggregationError LeiosCert
aggregateLeiosCert LeiosCommittee
committee Map LeiosVoterId LeiosSignature
forall k a. Map k a
Map.empty of
        Left BLSAggregationFailed {} -> Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
True
        Either AggregationError LeiosCert
other -> String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (Either AggregationError LeiosCert -> String
forall a. Show a => a -> String
show Either AggregationError LeiosCert
other) (Bool -> Property
forall prop. Testable prop => prop -> Property
QC.property Bool
False)