{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Conway.Governance.ProceduresSpec (spec) where

import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance (
  GovActionId,
  Voter,
  VotingProcedure,
  VotingProcedures (..),
  foldlVotingProcedures,
 )
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Test.Cardano.Base.QuickCheck (testLawsGroup)
import Test.Cardano.Ledger.Common
import Test.Cardano.Ledger.Conway.Arbitrary ()
import Test.QuickCheck.Classes (
  exponentialSemigroupLaws,
  monoidLaws,
  semigroupLaws,
  semigroupMonoidLaws,
 )

spec :: Spec
spec :: Spec
spec = String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"VotingProcedures" (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
"Semigroup and Monoid" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$
    -- `<>` for `VotingProcedures` is not commutative, so
    -- `commutativeSemigroupLaws` and `commutativeMonoidLaws` must not be applied
    -- here.
    forall a. [Proxy a -> Laws] -> Spec
testLawsGroup @(VotingProcedures ConwayEra)
      [ Proxy (VotingProcedures ConwayEra) -> Laws
forall a.
(Semigroup a, Eq a, Arbitrary a, Show a) =>
Proxy a -> Laws
semigroupLaws
      , Proxy (VotingProcedures ConwayEra) -> Laws
forall a.
(Semigroup a, Eq a, Arbitrary a, Show a) =>
Proxy a -> Laws
exponentialSemigroupLaws
      , Proxy (VotingProcedures ConwayEra) -> Laws
forall a. (Monoid a, Eq a, Arbitrary a, Show a) => Proxy a -> Laws
monoidLaws
      , Proxy (VotingProcedures ConwayEra) -> Laws
forall a.
(Semigroup a, Monoid a, Eq a, Arbitrary a, Show a) =>
Proxy a -> Laws
semigroupMonoidLaws
      ]
  -- Needs the overlapping 'VotingProcedures' generator, or else we won't be able to assert that <> is not commutative (disjoint operands *do* commute)
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"<> is not commutative" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
    Property -> Property
forall prop. Testable prop => prop -> Property
expectFailure (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
      -- Use `forAllBlind` and `==` instead of `forAll` and `===` because an
      -- expected failure would print the whole counterexample on every run.
      Gen (VotingProcedures ConwayEra, VotingProcedures ConwayEra)
-> ((VotingProcedures ConwayEra, VotingProcedures ConwayEra)
    -> Bool)
-> Property
forall prop a. Testable prop => Gen a -> (a -> prop) -> Property
forAllBlind Gen (VotingProcedures ConwayEra, VotingProcedures ConwayEra)
genOverlappingVotingProcedures (((VotingProcedures ConwayEra, VotingProcedures ConwayEra) -> Bool)
 -> Property)
-> ((VotingProcedures ConwayEra, VotingProcedures ConwayEra)
    -> Bool)
-> Property
forall a b. (a -> b) -> a -> b
$ \(VotingProcedures ConwayEra
vps1, VotingProcedures ConwayEra
vps2) ->
        VotingProcedures ConwayEra
vps1 VotingProcedures ConwayEra
-> VotingProcedures ConwayEra -> VotingProcedures ConwayEra
forall a. Semigroup a => a -> a -> a
<> VotingProcedures ConwayEra
vps2 VotingProcedures ConwayEra -> VotingProcedures ConwayEra -> Bool
forall a. Eq a => a -> a -> Bool
== VotingProcedures ConwayEra
vps2 VotingProcedures ConwayEra
-> VotingProcedures ConwayEra -> VotingProcedures ConwayEra
forall a. Semigroup a => a -> a -> a
<> VotingProcedures ConwayEra
vps1
  String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"<> is a right-biased union per (Voter, GovActionId)" (Property -> Spec) -> Property -> Spec
forall a b. (a -> b) -> a -> b
$
    Gen (VotingProcedures ConwayEra, VotingProcedures ConwayEra)
-> ((VotingProcedures ConwayEra, VotingProcedures ConwayEra)
    -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen (VotingProcedures ConwayEra, VotingProcedures ConwayEra)
genOverlappingVotingProcedures (((VotingProcedures ConwayEra, VotingProcedures ConwayEra)
  -> Property)
 -> Property)
-> ((VotingProcedures ConwayEra, VotingProcedures ConwayEra)
    -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \(VotingProcedures ConwayEra
vps1, VotingProcedures ConwayEra
vps2) ->
      -- Map.union is right-biased
      VotingProcedures ConwayEra
-> Map (Voter, GovActionId) (VotingProcedure ConwayEra)
forall era.
VotingProcedures era
-> Map (Voter, GovActionId) (VotingProcedure era)
flattenVotes (VotingProcedures ConwayEra
vps1 VotingProcedures ConwayEra
-> VotingProcedures ConwayEra -> VotingProcedures ConwayEra
forall a. Semigroup a => a -> a -> a
<> VotingProcedures ConwayEra
vps2) Map (Voter, GovActionId) (VotingProcedure ConwayEra)
-> Map (Voter, GovActionId) (VotingProcedure ConwayEra) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Map (Voter, GovActionId) (VotingProcedure ConwayEra)
-> Map (Voter, GovActionId) (VotingProcedure ConwayEra)
-> Map (Voter, GovActionId) (VotingProcedure ConwayEra)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (VotingProcedures ConwayEra
-> Map (Voter, GovActionId) (VotingProcedure ConwayEra)
forall era.
VotingProcedures era
-> Map (Voter, GovActionId) (VotingProcedure era)
flattenVotes VotingProcedures ConwayEra
vps2) (VotingProcedures ConwayEra
-> Map (Voter, GovActionId) (VotingProcedure ConwayEra)
forall era.
VotingProcedures era
-> Map (Voter, GovActionId) (VotingProcedure era)
flattenVotes VotingProcedures ConwayEra
vps1)

-- | This function flattens the nested 'Map' from 'VotingProcedures' to a single
-- 'Map'. With a single 'Map', 'VotingProcedures' represents a partial function
-- @(Voter, GovActionId) -> VotingProcedure@.
--
-- Asserting against this model rather than against the nested 'Map's is what
-- makes the property above reject an outer-level union that drops a shared
-- voter's other votes. For example, a wrong @(\<>)@ that implements
-- @vps1 \<> vps2@ as @Map.union@ only unions the outer, 'Voter'-keyed 'Map'.
-- For a voter @v@ who voted on @gaid1 :: GovActionId@ in @vps1@ and on
-- @gaid2 :: GovActionId@ in @vps2@, 'Map.union' keeps @vps1@'s whole inner map
-- @Map GovActionId (VotingProcedure era)@ for @v@ and discards @vps2@'s inner
-- map for @v@, so @v@'s vote on @gaid2@ vanishes from the result even though
-- it never collided with anything. Comparing against 'flattenVotes' models
-- instead catches this immediately, because @(v, gaid2)@ is simply a missing
-- key in the flattened union.
flattenVotes :: VotingProcedures era -> Map (Voter, GovActionId) (VotingProcedure era)
flattenVotes :: forall era.
VotingProcedures era
-> Map (Voter, GovActionId) (VotingProcedure era)
flattenVotes = (Map (Voter, GovActionId) (VotingProcedure era)
 -> Voter
 -> GovActionId
 -> VotingProcedure era
 -> Map (Voter, GovActionId) (VotingProcedure era))
-> Map (Voter, GovActionId) (VotingProcedure era)
-> VotingProcedures era
-> Map (Voter, GovActionId) (VotingProcedure era)
forall c era.
(c -> Voter -> GovActionId -> VotingProcedure era -> c)
-> c -> VotingProcedures era -> c
foldlVotingProcedures (\Map (Voter, GovActionId) (VotingProcedure era)
acc Voter
voter GovActionId
gaid VotingProcedure era
vp -> (Voter, GovActionId)
-> VotingProcedure era
-> Map (Voter, GovActionId) (VotingProcedure era)
-> Map (Voter, GovActionId) (VotingProcedure era)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Voter
voter, GovActionId
gaid) VotingProcedure era
vp Map (Voter, GovActionId) (VotingProcedure era)
acc) Map (Voter, GovActionId) (VotingProcedure era)
forall k a. Map k a
Map.empty

-- | A pair of 'VotingProcedures' that overlaps in terms of 'Voter' and
-- 'GovActionId'. Two independent 'arbitrary' values of 'VotingProcedures' don't
-- have 'Voter' or 'GovActionId' that overlap, since both keys are random
-- hashes, so a property over them would only ever exercise the disjoint case.
--
-- A generated pair covers all three interesting shapes at once, each ruling out a different wrong
-- implementation of `<>`:
--
--   * a 'Voter' only one side of `<>` has;
--   * a 'Voter' both sides of `<>` have, with a 'GovActionId' only one side has;
--   * a 'Voter' and 'GovActionId' both sides of `<>` have;
genOverlappingVotingProcedures :: Gen (VotingProcedures ConwayEra, VotingProcedures ConwayEra)
genOverlappingVotingProcedures :: Gen (VotingProcedures ConwayEra, VotingProcedures ConwayEra)
genOverlappingVotingProcedures = do
  -- Voters both sides have
  sharedVoters <- [(Voter,
  (Map GovActionId (VotingProcedure ConwayEra),
   Map GovActionId (VotingProcedure ConwayEra)))]
-> Map
     Voter
     (Map GovActionId (VotingProcedure ConwayEra),
      Map GovActionId (VotingProcedure ConwayEra))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Voter,
   (Map GovActionId (VotingProcedure ConwayEra),
    Map GovActionId (VotingProcedure ConwayEra)))]
 -> Map
      Voter
      (Map GovActionId (VotingProcedure ConwayEra),
       Map GovActionId (VotingProcedure ConwayEra)))
-> Gen
     [(Voter,
       (Map GovActionId (VotingProcedure ConwayEra),
        Map GovActionId (VotingProcedure ConwayEra)))]
-> Gen
     (Map
        Voter
        (Map GovActionId (VotingProcedure ConwayEra),
         Map GovActionId (VotingProcedure ConwayEra)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Int)
-> Gen
     [(Voter,
       (Map GovActionId (VotingProcedure ConwayEra),
        Map GovActionId (VotingProcedure ConwayEra)))]
-> Gen
     [(Voter,
       (Map GovActionId (VotingProcedure ConwayEra),
        Map GovActionId (VotingProcedure ConwayEra)))]
forall a. (Int -> Int) -> Gen a -> Gen a
scale (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
6) (Gen
  (Voter,
   (Map GovActionId (VotingProcedure ConwayEra),
    Map GovActionId (VotingProcedure ConwayEra)))
-> Gen
     [(Voter,
       (Map GovActionId (VotingProcedure ConwayEra),
        Map GovActionId (VotingProcedure ConwayEra)))]
forall a. Gen a -> Gen [a]
listOf ((,) (Voter
 -> (Map GovActionId (VotingProcedure ConwayEra),
     Map GovActionId (VotingProcedure ConwayEra))
 -> (Voter,
     (Map GovActionId (VotingProcedure ConwayEra),
      Map GovActionId (VotingProcedure ConwayEra))))
-> Gen Voter
-> Gen
     ((Map GovActionId (VotingProcedure ConwayEra),
       Map GovActionId (VotingProcedure ConwayEra))
      -> (Voter,
          (Map GovActionId (VotingProcedure ConwayEra),
           Map GovActionId (VotingProcedure ConwayEra))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Voter
forall a. Arbitrary a => Gen a
arbitrary Gen
  ((Map GovActionId (VotingProcedure ConwayEra),
    Map GovActionId (VotingProcedure ConwayEra))
   -> (Voter,
       (Map GovActionId (VotingProcedure ConwayEra),
        Map GovActionId (VotingProcedure ConwayEra))))
-> Gen
     (Map GovActionId (VotingProcedure ConwayEra),
      Map GovActionId (VotingProcedure ConwayEra))
-> Gen
     (Voter,
      (Map GovActionId (VotingProcedure ConwayEra),
       Map GovActionId (VotingProcedure ConwayEra)))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen
  (Map GovActionId (VotingProcedure ConwayEra),
   Map GovActionId (VotingProcedure ConwayEra))
genOverlappingVotes))
  -- Voters only one side has. Their 'Voter' keys are random hashes, so they don't collide with
  -- `sharedVoters`.
  leftOnlyVoters <- unVotingProcedures <$> arbitrary
  rightOnlyVoters <- unVotingProcedures <$> arbitrary
  pure
    ( VotingProcedures $ Map.union (fmap fst sharedVoters) leftOnlyVoters
    , VotingProcedures $ Map.union (fmap snd sharedVoters) rightOnlyVoters
    )

-- | The two sets of votes that a shared 'Voter' could cast, one for each side
-- of the generated pair.
--
-- Both sides of the pair vote on the same generated `sharedGovActionIds`, but
-- with independently generated 'VotingProcedure's, so the two sides disagree
-- and it becomes observable which of them the `<>` implementation keeps. Each
-- side also votes on 'GovActionId' the other side doesn't have.
genOverlappingVotes ::
  Gen (Map GovActionId (VotingProcedure ConwayEra), Map GovActionId (VotingProcedure ConwayEra))
genOverlappingVotes :: Gen
  (Map GovActionId (VotingProcedure ConwayEra),
   Map GovActionId (VotingProcedure ConwayEra))
genOverlappingVotes = do
  -- Non-empty, so that a shared voter always does share a gov action, and so
  -- that neither side can come out with no votes at all.
  sharedGovActionIds <- (Int -> Int) -> Gen [GovActionId] -> Gen [GovActionId]
forall a. (Int -> Int) -> Gen a -> Gen a
scale (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
6) (Gen GovActionId -> Gen [GovActionId]
forall a. Gen a -> Gen [a]
listOf1 Gen GovActionId
forall a. Arbitrary a => Gen a
arbitrary)
  let genVotes = do
        sharedVotes <- (GovActionId -> Gen (GovActionId, VotingProcedure ConwayEra))
-> [GovActionId] -> Gen [(GovActionId, VotingProcedure ConwayEra)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\GovActionId
gaid -> (,) GovActionId
gaid (VotingProcedure ConwayEra
 -> (GovActionId, VotingProcedure ConwayEra))
-> Gen (VotingProcedure ConwayEra)
-> Gen (GovActionId, VotingProcedure ConwayEra)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (VotingProcedure ConwayEra)
forall a. Arbitrary a => Gen a
arbitrary) [GovActionId]
sharedGovActionIds
        uniqueVotes <- Map.fromList <$> scale (min 6) (listOf ((,) <$> arbitrary <*> arbitrary))
        pure $ Map.fromList sharedVotes `Map.union` uniqueVotes
  (,) <$> genVotes <*> genVotes