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

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

import qualified Cardano.Binary as CBOR
import Cardano.Crypto.DSIGN (
  DSIGNAlgorithm (deriveVerKeyDSIGN),
  encodeSigDSIGN,
  genKeyDSIGN,
  seedSizeDSIGN,
  signDSIGN,
 )
import Cardano.Crypto.Leios (
  AggregationError (..),
  LeiosCert (..),
  LeiosCommittee (..),
  LeiosDSIGN,
  LeiosSignature,
  LeiosSigningKey,
  LeiosVoter (..),
  LeiosVoterId (..),
  VerificationError (..),
  Weight,
  aggregateLeiosCert,
  decodeLeiosCert,
  decodeLeiosVoterId,
  encodeBitField,
  encodeLeiosCert,
  encodeLeiosVoterId,
  getLeiosVoterId,
  leiosSignContext,
  resolveLeiosVoter,
  verifyLeiosCert,
 )
import Cardano.Crypto.Seed (mkSeedFromBytes)
import Codec.CBOR.Encoding (Encoding, encodeBreak, encodeListLenIndef)
import qualified Data.ByteString as BS
import qualified Data.ByteString.Base16 as BS16
import qualified Data.ByteString.Char8 as BS8
import qualified Data.ByteString.Lazy as BSL
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.Cardano.Crypto.Leios.Gen (genLeiosCert)
import Test.Hspec (Spec, context, describe, it)
import Test.Hspec.Golden (Golden (..))
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 -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"round-trips through CBOR" Property
prop_roundtrip_LeiosCert
    String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"decodes indefinite-length encoding" Property
prop_decode_indefinite_LeiosCert
    String -> Golden ByteString -> SpecM (Arg (Golden ByteString)) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"matches golden encoding" (Golden ByteString -> SpecM (Arg (Golden ByteString)) ())
-> Golden ByteString -> SpecM (Arg (Golden ByteString)) ()
forall a b. (a -> b) -> a -> b
$
      String -> (LeiosCert -> Encoding) -> LeiosCert -> Golden ByteString
forall a. String -> (a -> Encoding) -> a -> Golden ByteString
goldenEncoding String
"test/golden/LeiosCert" LeiosCert -> Encoding
encodeLeiosCert LeiosCert
exampleCert

    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
"LeiosVoterId" (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
"round-trips through CBOR" Property
prop_roundtrip_VoterId
    String -> Golden ByteString -> SpecM (Arg (Golden ByteString)) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"matches golden encoding" (Golden ByteString -> SpecM (Arg (Golden ByteString)) ())
-> Golden ByteString -> SpecM (Arg (Golden ByteString)) ()
forall a b. (a -> b) -> a -> b
$
      String
-> (LeiosVoterId -> Encoding) -> LeiosVoterId -> Golden ByteString
forall a. String -> (a -> Encoding) -> a -> Golden ByteString
goldenEncoding String
"test/golden/LeiosVoterId" LeiosVoterId -> Encoding
encodeLeiosVoterId LeiosVoterId
exampleVoterId

  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

-- * CBOR roundtrip / golden

prop_roundtrip_LeiosCert :: Property
prop_roundtrip_LeiosCert :: Property
prop_roundtrip_LeiosCert = Gen LeiosCert -> (LeiosCert -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen LeiosCert
genLeiosCert ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
cert ->
  let bs :: ByteString
bs = Encoding -> ByteString
forall a. ToCBOR a => a -> ByteString
CBOR.serialize (LeiosCert -> Encoding
encodeLeiosCert LeiosCert
cert)
   in Text
-> (forall s. Decoder s LeiosCert)
-> ByteString
-> Either DecoderError LeiosCert
forall a.
Text
-> (forall s. Decoder s a) -> ByteString -> Either DecoderError a
CBOR.decodeFullDecoder Text
"LeiosCert" Decoder s LeiosCert
forall s. Decoder s LeiosCert
decodeLeiosCert ByteString
bs Either DecoderError LeiosCert
-> Either DecoderError LeiosCert -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LeiosCert -> Either DecoderError LeiosCert
forall a b. b -> Either a b
Right LeiosCert
cert

-- | The decoder must accept indefinite-length encodings of the outer
-- 2-element array, not just the canonical definite-length form.
prop_decode_indefinite_LeiosCert :: Property
prop_decode_indefinite_LeiosCert :: Property
prop_decode_indefinite_LeiosCert = Gen LeiosCert -> (LeiosCert -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen LeiosCert
genLeiosCert ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
cert ->
  let indef :: Encoding
indef =
        Encoding
encodeListLenIndef
          Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> BitField -> Encoding
encodeBitField (LeiosCert -> BitField
leiosCertSigners LeiosCert
cert)
          Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> SigDSIGN LeiosDSIGN -> Encoding
forall v. DSIGNAlgorithm v => SigDSIGN v -> Encoding
encodeSigDSIGN (LeiosCert -> SigDSIGN LeiosDSIGN
leiosCertSignature LeiosCert
cert)
          Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Encoding
encodeBreak
   in Text
-> (forall s. Decoder s LeiosCert)
-> ByteString
-> Either DecoderError LeiosCert
forall a.
Text
-> (forall s. Decoder s a) -> ByteString -> Either DecoderError a
CBOR.decodeFullDecoder Text
"LeiosCert" Decoder s LeiosCert
forall s. Decoder s LeiosCert
decodeLeiosCert (Encoding -> ByteString
forall a. ToCBOR a => a -> ByteString
CBOR.serialize Encoding
indef)
        Either DecoderError LeiosCert
-> Either DecoderError LeiosCert -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LeiosCert -> Either DecoderError LeiosCert
forall a b. b -> Either a b
Right LeiosCert
cert

-- | Pin the byte-for-byte CBOR encoding of a value to a golden file using
-- 'hspec-golden'. Failure diffs are rendered as base16 hex. Decode
-- round-trip of arbitrary values is covered by the matching @roundtrip_@
-- property; this only locks the encoding shape.
goldenEncoding :: FilePath -> (a -> Encoding) -> a -> Golden BSL.ByteString
goldenEncoding :: forall a. String -> (a -> Encoding) -> a -> Golden ByteString
goldenEncoding String
path a -> Encoding
enc a
value =
  Golden
    { output :: ByteString
output = Encoding -> ByteString
forall a. ToCBOR a => a -> ByteString
CBOR.serialize (a -> Encoding
enc a
value)
    , encodePretty :: ByteString -> String
encodePretty = ByteString -> String
BS8.unpack (ByteString -> String)
-> (ByteString -> ByteString) -> ByteString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
BS16.encode (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
BSL.toStrict
    , writeToFile :: String -> ByteString -> IO ()
writeToFile = String -> ByteString -> IO ()
BSL.writeFile
    , readFromFile :: String -> IO ByteString
readFromFile = String -> IO ByteString
BSL.readFile
    , goldenFile :: String
goldenFile = String
path
    , actualFile :: Maybe String
actualFile = Maybe String
forall a. Maybe a
Nothing
    , failFirstTime :: Bool
failFirstTime = Bool
False
    }

exampleCert :: LeiosCert
exampleCert :: LeiosCert
exampleCert = case LeiosCommittee
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
-> Either AggregationError LeiosCert
aggregateLeiosCert LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
contributions = ByteString
-> [(Int, LeiosSigningKey)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 CBOR / committee lookup

prop_roundtrip_VoterId :: Property
prop_roundtrip_VoterId :: Property
prop_roundtrip_VoterId = Gen LeiosVoterId -> (LeiosVoterId -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Word16 -> LeiosVoterId
LeiosVoterId (Word16 -> LeiosVoterId) -> Gen Word16 -> Gen LeiosVoterId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word16
forall a. Arbitrary a => Gen a
QC.arbitrary) ((LeiosVoterId -> Property) -> Property)
-> (LeiosVoterId -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosVoterId
vid ->
  let bs :: ByteString
bs = Encoding -> ByteString
forall a. ToCBOR a => a -> ByteString
CBOR.serialize (LeiosVoterId -> Encoding
encodeLeiosVoterId LeiosVoterId
vid)
   in Text
-> (forall s. Decoder s LeiosVoterId)
-> ByteString
-> Either DecoderError LeiosVoterId
forall a.
Text
-> (forall s. Decoder s a) -> ByteString -> Either DecoderError a
CBOR.decodeFullDecoder Text
"LeiosVoterId" Decoder s LeiosVoterId
forall s. Decoder s LeiosVoterId
decodeLeiosVoterId ByteString
bs Either DecoderError LeiosVoterId
-> Either DecoderError LeiosVoterId -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LeiosVoterId -> Either DecoderError LeiosVoterId
forall a b. b -> Either a b
Right LeiosVoterId
vid

exampleVoterId :: LeiosVoterId
exampleVoterId :: LeiosVoterId
exampleVoterId = Word16 -> LeiosVoterId
LeiosVoterId Word16
0xABCD

-- | '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 (SigDSIGN LeiosDSIGN)
signContribs ByteString
msg [(Int, LeiosSigningKey)]
pairs =
  [(LeiosVoterId, SigDSIGN LeiosDSIGN)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 -> SigDSIGN LeiosDSIGN
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 -> SigDSIGN LeiosDSIGN
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 (SigDSIGN LeiosDSIGN)
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
contributions LeiosCert -> Property
k = case LeiosCommittee
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
-> Either AggregationError LeiosCert
aggregateLeiosCert LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
contributions = ByteString
-> [(Int, LeiosSigningKey)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
contributions = ByteString
-> [(Int, LeiosSigningKey)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
contributions = ByteString
-> [(Int, LeiosSigningKey)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
contributions = ByteString
-> [(Int, LeiosSigningKey)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
signContribs ByteString
msg [(Int
0, LeiosSigningKey
sk0)]
   in LeiosCommittee
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
contributions = ByteString
-> [(Int, LeiosSigningKey)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committeeA Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
contribsAlone = ByteString
-> [(Int, LeiosSigningKey)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
signContribs ByteString
msg [(Int
0, LeiosSigningKey
sks0)]
      contribsPair :: Map LeiosVoterId (SigDSIGN LeiosDSIGN)
contribsPair = ByteString
-> [(Int, LeiosSigningKey)]
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
signContribs ByteString
msg [(Int
0, LeiosSigningKey
sks0), (Int
1, LeiosSigningKey
sks1)]
   in LeiosCommittee
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
contribsAlone ((LeiosCert -> Property) -> Property)
-> (LeiosCert -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \LeiosCert
certA ->
        LeiosCommittee
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
-> (LeiosCert -> Property)
-> Property
aggregateOrFail LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
contributions = LeiosVoterId
-> SigDSIGN LeiosDSIGN -> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
forall k a. k -> a -> Map k a
Map.singleton LeiosVoterId
bad (ContextDSIGN LeiosDSIGN
-> ByteString -> LeiosSigningKey -> SigDSIGN LeiosDSIGN
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 -> SigDSIGN LeiosDSIGN
signDSIGN ContextDSIGN LeiosDSIGN
BLS12381SignContext
leiosSignContext ByteString
msg LeiosSigningKey
sk0)
     in LeiosCommittee
-> Map LeiosVoterId (SigDSIGN LeiosDSIGN)
-> Either AggregationError LeiosCert
aggregateLeiosCert LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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 (SigDSIGN LeiosDSIGN)
-> Either AggregationError LeiosCert
aggregateLeiosCert LeiosCommittee
committee Map LeiosVoterId (SigDSIGN LeiosDSIGN)
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)