-- | Off-chain differential (real-node binding): the Agda-extracted round-robin leader
-- 'Hydra.Agda.OffChainReference.leaderRef' (the §6 figure's @leader(s)@) checked against the REAL
-- 'Hydra.HeadLogic.isLeader'. This is the off-chain counterpart of the on-chain validator differentials:
-- the extracted decision is pinned not just to a Haskell transcription of the figure but to the function
-- the node actually runs, closing the figure↔Agda↔Haskell loop for leader selection.
--
-- Domain note: snapshot numbers in the protocol start at 1, but the property covers @sn = 0@ too.
-- @leaderRef@ works over Nat, whose truncated subtraction would make @0 - 1@ zero where @isLeader@'s
-- 'Int' arithmetic gives @-1 `mod` n = n-1@; the extracted checker adds @m@ instead of subtracting 1
-- (the same residue for every @sn >= 1@, and @n-1@ at zero) precisely so the oracle cannot disagree
-- with the node anywhere - including on an @sn = 0@ a peer could put in a @ReqSn@.
module Hydra.OffChainLeaderSpec (spec) where

import Hydra.Prelude
import Test.Hydra.Prelude

import Hydra.Agda.OffChainReference (leaderRef)
import Hydra.HeadLogic (isLeader)
import Hydra.Tx.HeadParameters (HeadParameters (..))
import Hydra.Tx.Snapshot (SnapshotNumber)
import Test.Hydra.Tx.Fixture (alice, bob, carol)
import Test.QuickCheck (NonNegative (..), choose, conjoin, counterexample, elements, forAll, (===))

spec :: Spec
spec :: Spec
spec =
  String -> Spec -> Spec
forall a. HasCallStack => String -> SpecWith a -> SpecWith a
describe String
"Off-chain round-robin leader: extracted leaderRef vs real Hydra.HeadLogic.isLeader" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    -- A 3-party head; @leaderRef@ takes @m@ where #parties = @suc m@, so @m = 2@ here.
    let parties :: [Party]
parties = [Party
alice, Party
bob, Party
carol]
        params :: HeadParameters
params = HeadParameters{$sel:contestationPeriod:HeadParameters :: ContestationPeriod
contestationPeriod = ContestationPeriod
60, $sel:depositPeriod:HeadParameters :: DepositPeriod
depositPeriod = DepositPeriod
60, [Party]
parties :: [Party]
$sel:parties:HeadParameters :: [Party]
parties}
    -- the fixture set is three parties, so head sizes 1..3: enough to cover the degenerate
    -- modulus (n = 1, every snapshot elects the only party) and two distinct wraparound points
    String -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"sn 1 elects party 0 (alice)" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$
      Integer -> Integer -> Integer -> Bool
leaderRef Integer
2 Integer
1 Integer
0 Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Bool
True
    String -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"sn 2 elects party 1 (bob)" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$
      Integer -> Integer -> Integer -> Bool
leaderRef Integer
2 Integer
2 Integer
1 Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Bool
True
    String -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"sn 3 elects party 2 (carol)" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$
      Integer -> Integer -> Integer -> Bool
leaderRef Integer
2 Integer
3 Integer
2 Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Bool
True
    String -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"sn 4 wraps back to party 0 (alice)" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$
      Integer -> Integer -> Integer -> Bool
leaderRef Integer
2 Integer
4 Integer
0 Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Bool
True
    String -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"a non-leader index is rejected" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$
      Integer -> Integer -> Integer -> Bool
leaderRef Integer
2 Integer
1 Integer
1 Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Bool
False
    -- The boundary the truncated-subtraction version got wrong: at sn 0 the node's signed
    -- arithmetic elects the LAST party, not the first.
    String -> Expectation -> SpecM (Arg Expectation) ()
forall a.
(HasCallStack, Example a) =>
String -> a -> SpecWith (Arg a)
it String
"sn 0 elects the last party (n-1), as the node's signed arithmetic does" (Expectation -> SpecM (Arg Expectation) ())
-> Expectation -> SpecM (Arg Expectation) ()
forall a b. (a -> b) -> a -> b
$ do
      Integer -> Integer -> Integer -> Bool
leaderRef Integer
2 Integer
0 Integer
2 Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Bool
True
      Integer -> Integer -> Integer -> Bool
leaderRef Integer
2 Integer
0 Integer
0 Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Bool
False
      HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
params Party
carol SnapshotNumber
0 Bool -> Bool -> Expectation
forall a. (HasCallStack, Show a, Eq a) => a -> a -> Expectation
`shouldBe` Bool
True
    String -> (NonNegative Integer -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"leaderRef agrees with the real isLeader for every party index, including sn = 0" ((NonNegative Integer -> Property) -> Spec)
-> (NonNegative Integer -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$
      \(NonNegative Integer
sn) -> Gen (Integer, Party) -> ((Integer, Party) -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ([(Integer, Party)] -> Gen (Integer, Party)
forall a. HasCallStack => [a] -> Gen a
elements ([Integer] -> [Party] -> [(Integer, Party)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0 :: Integer ..] [Party]
parties)) (((Integer, Party) -> Property) -> Property)
-> ((Integer, Party) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(Integer
i, Party
party) ->
        Integer -> Integer -> Integer -> Bool
leaderRef Integer
2 Integer
sn Integer
i Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
params Party
party (Integer -> SnapshotNumber
forall a. Num a => Integer -> a
fromInteger Integer
sn :: SnapshotNumber)

    -- ...and for every head SIZE, not just three parties. `leaderRef` is
    -- `(sn + m) mod (suc m)`, so the modulus itself varies with n: n = 1 is the degenerate case
    -- where every snapshot elects the only party, and the wraparound point moves with n.
    String -> (NonNegative Integer -> Property) -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
prop String
"leaderRef agrees with the real isLeader for every head size and party index" ((NonNegative Integer -> Property) -> Spec)
-> (NonNegative Integer -> Property) -> Spec
forall a b. (a -> b) -> a -> b
$
      \(NonNegative Integer
sn) ->
        Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, [Party] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Party]
parties)) ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
          let someParties :: [Party]
someParties = Int -> [Party] -> [Party]
forall a. Int -> [a] -> [a]
take Int
n [Party]
parties
              someParams :: HeadParameters
someParams = HeadParameters{$sel:contestationPeriod:HeadParameters :: ContestationPeriod
contestationPeriod = ContestationPeriod
60, $sel:depositPeriod:HeadParameters :: DepositPeriod
depositPeriod = DepositPeriod
60, $sel:parties:HeadParameters :: [Party]
parties = [Party]
someParties}
              m :: Integer
m = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) :: Integer
           in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
                [ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"n=" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall b a. (Show a, IsString b) => a -> b
show Int
n String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" i=" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall b a. (Show a, IsString b) => a -> b
show Integer
i) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
                  Integer -> Integer -> Integer -> Bool
leaderRef Integer
m Integer
sn Integer
i Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== HeadParameters -> Party -> SnapshotNumber -> Bool
isLeader HeadParameters
someParams Party
party (Integer -> SnapshotNumber
forall a. Num a => Integer -> a
fromInteger Integer
sn :: SnapshotNumber)
                | (Integer
i, Party
party) <- [Integer] -> [Party] -> [(Integer, Party)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
0 :: Integer ..] [Party]
someParties
                ]