{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Constrained.Examples where

import Cardano.Ledger.Babbage (BabbageEra)
import Cardano.Ledger.BaseTypes (EpochNo (..))
import Cardano.Ledger.CertState (FutureGenDeleg (..))
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Core (Era)
import Cardano.Ledger.Keys (GenDelegPair)
import Control.DeepSeq (deepseq)
import Control.Exception (ErrorCall (..))
import Control.Monad (when)
import Data.Default (Default (..))
import Data.Map (Map)
import Data.Ratio ((%))
import qualified Debug.Trace as Debug
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes (OrdCond (..))
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Lenses (fGenDelegGenKeyHashL)
import Test.Cardano.Ledger.Constrained.Monad
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.Tx (genTxAndNewEpoch)
import Test.Cardano.Ledger.Constrained.Rewrite
import Test.Cardano.Ledger.Constrained.Solver
import Test.Cardano.Ledger.Constrained.Tests (prop_shrinking, prop_soundness)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (explainBad, testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (..))
import Test.Cardano.Ledger.Generic.Proof (ConwayEra, Reflect (..))
import Test.Cardano.Ledger.Generic.Trace (testPropMax)
import Test.Hspec (shouldThrow)
import Test.QuickCheck hiding (Fixed, total)
import Test.Tasty (TestTree, defaultMain, testGroup)
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck
import Type.Reflection (typeRep)

-- =======================================================

-- ===========================================

runCompile :: Era era => [Pred era] -> IO ()
runCompile :: forall era. Era era => [Pred era] -> IO ()
runCompile [Pred era]
cs = case forall x. Typed x -> Either [[Char]] x
runTyped (forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
standardOrderInfo [Pred era]
cs) of
  Right DependGraph era
x -> forall a. Show a => a -> IO ()
print DependGraph era
x
  Left [[Char]]
xs -> [Char] -> IO ()
putStrLn ([[Char]] -> [Char]
unlines [[Char]]
xs)

data Assembler era where
  Assemble :: PrettyA t => RootTarget era x t -> Assembler era
  Skip :: Assembler era

stoi :: OrderInfo
stoi :: OrderInfo
stoi = OrderInfo
standardOrderInfo

genMaybeCounterExample ::
  Reflect era =>
  Proof era ->
  String ->
  Bool ->
  OrderInfo ->
  [Pred era] ->
  Assembler era ->
  Gen (Maybe String)
genMaybeCounterExample :: forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen (Maybe [Char])
genMaybeCounterExample Proof era
proof [Char]
_testname Bool
loud OrderInfo
order [Pred era]
cs Assembler era
target = do
  let cs3 :: [Pred era]
cs3 = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual [Pred era]
cs []
  let cs4 :: [Pred era]
cs4 = forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar [Pred era]
cs3 []
  graph :: DependGraph era
graph@(DependGraph [([Name era], [Pred era])]
_) <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
order [Pred era]
cs
  let messages1 :: [[Char]]
messages1 =
        if forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq forall era. Era era => Pred era -> Pred era -> Bool
cpeq [Pred era]
cs4 [Pred era]
cs
          then [[Char]
"Constraints", forall a. Show a => a -> [Char]
show [Pred era]
cs, [Char]
"Rewriting is idempotent"]
          else
            [ [Char]
"Constraints"
            , forall a. Show a => a -> [Char]
show [Pred era]
cs
            , [Char]
"Substitute for Equality"
            , forall a. Show a => a -> [Char]
show [Pred era]
cs3
            , [Char]
"Remove syntactic tautologies"
            , forall a. Show a => a -> [Char]
show [Pred era]
cs4
            , [Char]
"Pick a variable ordering\n"
            , forall a. Show a => a -> [Char]
show DependGraph era
graph
            , [Char]
"Solve for each variable in the order computed. Note by the time we get"
            , [Char]
"to each variable, it is the only variable left in the constraint."
            ]
  Either [[Char]] (Subst era)
result <-
    if Bool
loud
      then forall a. [Char] -> a -> a
Debug.trace ([[Char]] -> [Char]
unlines [[Char]]
messages1) (forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [[Char]] (Subst era))
genDependGraph Bool
loud Proof era
proof DependGraph era
graph)
      else forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [[Char]] (Subst era))
genDependGraph Bool
loud Proof era
proof DependGraph era
graph
  Subst era
subst <- case Either [[Char]] (Subst era)
result of
    Left [[Char]]
msgs -> forall a. HasCallStack => [Char] -> a
error ([[Char]] -> [Char]
unlines [[Char]]
msgs)
    Right Subst era
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
x
  !Env era
env <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv
  [([Char], Bool, Pred era)]
testTriples <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era. Env era -> Pred era -> Typed ([Char], Bool, Pred era)
makeTest Env era
env) [Pred era]
cs)
  let messages2 :: [Char]
messages2 = [Char]
"\nSubstitution produced after solving\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Subst era
subst
  ![[Char]]
messages3 <- case Assembler era
target of
    Assembler era
Skip -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    Assemble RootTarget era x t
t -> do
      !t
tval <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era x t
t)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [[Char]
"\nAssemble the pieces\n", forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA t
tval)]
  let bad :: [([Char], Bool, Pred era)]
bad = forall a. (a -> Bool) -> [a] -> [a]
filter (\([Char]
_, Bool
b, Pred era
_) -> Bool -> Bool
not Bool
b) [([Char], Bool, Pred era)]
testTriples
      ans :: Maybe [Char]
ans =
        if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], Bool, Pred era)]
bad
          then forall a. Maybe a
Nothing -- Indicates success, nothing bad happened
          else forall a. a -> Maybe a
Just ([Char]
"Some conditions fail\n" forall a. [a] -> [a] -> [a]
++ forall era.
Era era =>
[([Char], Bool, Pred era)] -> Subst era -> [Char]
explainBad [([Char], Bool, Pred era)]
bad Subst era
subst)
  if Bool
loud
    then forall a. [Char] -> a -> a
Debug.trace ([[Char]] -> [Char]
unlines ([Char]
messages2 forall a. a -> [a] -> [a]
: [[Char]]
messages3)) (forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Char]
ans)
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Char]
ans

-- | Test that 'cs' :: [Pred] has a solution
testn ::
  Reflect era =>
  Proof era ->
  String ->
  Bool ->
  OrderInfo ->
  [Pred era] ->
  Assembler era ->
  Gen Property
testn :: forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn Proof era
proof [Char]
testname Bool
loud OrderInfo
order [Pred era]
cs Assembler era
target = do
  Maybe [Char]
result <- forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen (Maybe [Char])
genMaybeCounterExample Proof era
proof [Char]
testname Bool
loud OrderInfo
order [Pred era]
cs Assembler era
target
  case Maybe [Char]
result of
    Maybe [Char]
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => [Char] -> prop -> Property
counterexample [Char]
"" Bool
True
    Just [Char]
xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => [Char] -> prop -> Property
counterexample [Char]
xs Bool
False

-- | Test that 'cs' :: [Pred] does NOT have a solution. We expect a failure
failn ::
  Reflect era => Proof era -> String -> Bool -> OrderInfo -> [Pred era] -> Assembler era -> IO ()
failn :: forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> IO ()
failn Proof era
proof [Char]
message Bool
loud OrderInfo
order [Pred era]
cs Assembler era
target = do
  forall e a.
(HasCallStack, Exception e) =>
IO a -> Selector e -> IO ()
shouldThrow
    ( do
        Maybe [Char]
result <- forall a. Gen a -> IO a
generate (forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen (Maybe [Char])
genMaybeCounterExample Proof era
proof [Char]
message Bool
loud OrderInfo
order [Pred era]
cs Assembler era
target)
        case Maybe [Char]
result of
          Maybe [Char]
Nothing -> [Char] -> IO ()
putStrLn ([Char]
message forall a. [a] -> [a] -> [a]
++ [Char]
" should have failed but it did not.")
          Just [Char]
counter ->
            if Bool
loud
              then [Char] -> IO ()
putStrLn [Char]
counter
              else forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    )
    ( \(ErrorCall [Char]
msg) ->
        forall a. [Char] -> a -> a
Debug.trace
          ( if Bool
loud
              then ([Char]
"Fails as expected\n" forall a. [a] -> [a] -> [a]
++ [Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
"\nOK")
              else ([Char]
"Fails as expected OK")
          )
          Bool
True
    )

testSpec :: String -> Gen Property -> IO ()
testSpec :: [Char] -> Gen Property -> IO ()
testSpec [Char]
name Gen Property
p = do
  [Char] -> IO ()
putStrLn ([Char]
"testing: '" forall a. [a] -> [a] -> [a]
++ [Char]
name forall a. [a] -> [a] -> [a]
++ [Char]
"'")
  forall prop. Testable prop => prop -> IO ()
quickCheck Gen Property
p

-- ======================================================
-- Now some tests
-- ======================================================

-- | Used to test cyclic dependencies
aCyclicPred :: Era era => [Pred era]
aCyclicPred :: forall era. Era era => [Pred era]
aCyclicPred = [Term era (Set Int)
a forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
b, Term era (Set Int)
b forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
c, forall era t. Term era t -> Pred era
Random Term era (Set Int)
c]
  where
    a :: Term era (Set Int)
a = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"a" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)
    b :: Term era (Set Int)
b = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"b" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)
    c :: Term era (Set Int)
c = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"c" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)

cyclicPred :: Era era => [Pred era]
cyclicPred :: forall era. Era era => [Pred era]
cyclicPred = [Term era (Set Int)
a forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
b, Term era (Set Int)
b forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
c, Term era (Set Int)
c forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
d, Term era (Set Int)
d forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
a, forall era t. Term era t -> Pred era
Random Term era (Set Int)
d]
  where
    a :: Term era (Set Int)
a = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"a" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)
    b :: Term era (Set Int)
b = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"b" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)
    c :: Term era (Set Int)
c = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"c" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)
    d :: Term era (Set Int)
d = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"d" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)

test1 :: IO ()
test1 :: IO ()
test1 = do
  [Char] -> IO ()
putStrLn [Char]
"testing: Detect cycles"
  forall era. Era era => [Pred era] -> IO ()
runCompile @BabbageEra forall era. Era era => [Pred era]
aCyclicPred
  [Char] -> IO ()
putStrLn [Char]
"+++ OK, passed 1 test."

-- ===================================
test3 :: Gen Property
test3 :: Gen Property
test3 = forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn Proof MaryEra
Mary [Char]
"Test 3. PState example" Bool
False OrderInfo
stoi [Pred MaryEra]
cs (forall t era x. PrettyA t => RootTarget era x t -> Assembler era
Assemble forall era. Era era => RootTarget era (PState era) (PState era)
pstateT)
  where
    cs :: [Pred MaryEra]
cs =
      [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
10) forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
      , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
7) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr) -- At least 1, but smaller than the poolHashUniv
      , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools -- or mockPoolDistr can't sum to (1%1) if its empty
      , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits
      , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
      , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
      , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
      , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr]
      ]

-- ==============================

test4 :: IO ()
test4 :: IO ()
test4 = forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> IO ()
failn Proof MaryEra
Mary [Char]
"Test 4. Inconsistent Size" Bool
False OrderInfo
stoi [Pred MaryEra]
cs forall era. Assembler era
Skip
  where
    cs :: [Pred MaryEra]
cs =
      [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
5) forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
      , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
5)) OrdCond
GTH [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards]
      ]

test5 :: IO ()
test5 :: IO ()
test5 = forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> IO ()
failn Proof MaryEra
Mary [Char]
"Test 5. Bad Sum, impossible partition." Bool
False OrderInfo
stoi [Pred MaryEra]
cs forall era. Assembler era
Skip
  where
    cs :: [Pred MaryEra]
cs =
      [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
5) forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
      , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
4)) OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards]
      ]

-- ===========================================================
-- Example list of Constraints for test4 and test5

constraints :: EraGov era => Proof era -> [Pred era]
constraints :: forall era. EraGov era => Proof era -> [Pred era]
constraints Proof era
proof =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
10) forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
10) forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr -- This is summed so it can't be empty.
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools -- This has the same domain, so it can't be empty either
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
deposits OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits, forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
      forall era. Era era => Term era Coin
totalAda
      OrdCond
EQL
      [ forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
utxoCoin
      , forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
treasury
      , forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
reserves
      , forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
fees
      , forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits
      , forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits
      , forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
      ]
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
treasury
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
reserves
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
fees
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
utxoCoin
  , forall era t. Term era t -> Pred era
Random forall a b. (a -> b) -> a -> b
$ forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
proof
  ]

-- | Test that we can find a viable variable ordering
test6 :: Bool -> IO ()
test6 :: Bool -> IO ()
test6 Bool
loud = do
  [Char] -> IO ()
putStrLn [Char]
"testing: find a viable order of variables"
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn [Char]
"======================================================="
  case forall x. Typed x -> Either [[Char]] x
runTyped (forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
standardOrderInfo forall a b. (a -> b) -> a -> b
$ forall era. EraGov era => Proof era -> [Pred era]
constraints Proof ShelleyEra
Shelley) of
    Right DependGraph ShelleyEra
x ->
      if Bool
loud
        then forall a. Show a => a -> IO ()
print DependGraph ShelleyEra
x
        else [Char] -> IO ()
putStrLn [Char]
"+++ OK, passed 1 test."
    Left [[Char]]
xs -> forall a. HasCallStack => [Char] -> a
error ([[Char]] -> [Char]
unlines [[Char]]
xs)

-- | Test that we can compute a solution
test7 :: Bool -> IO ()
test7 :: Bool -> IO ()
test7 Bool
loud = do
  [Char] -> IO ()
putStrLn [Char]
"testing: compute a solution"
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn [Char]
"======================================================="
  let proof :: Proof ShelleyEra
proof = Proof ShelleyEra
Shelley
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn (forall a. Show a => a -> [Char]
show forall a b. (a -> b) -> a -> b
$ forall era. EraGov era => Proof era -> [Pred era]
constraints Proof ShelleyEra
proof)
  DependGraph ShelleyEra
graph <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
standardOrderInfo forall a b. (a -> b) -> a -> b
$ forall era. EraGov era => Proof era -> [Pred era]
constraints Proof ShelleyEra
proof
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn (forall a. Show a => a -> [Char]
show DependGraph ShelleyEra
graph)
  Either [[Char]] (Subst ShelleyEra)
result <- forall a. Gen a -> IO a
generate (forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [[Char]] (Subst era))
genDependGraph Bool
loud Proof ShelleyEra
proof DependGraph ShelleyEra
graph)
  Subst ShelleyEra
subst <- case Either [[Char]] (Subst ShelleyEra)
result of
    Left [[Char]]
msgs -> forall a. HasCallStack => [Char] -> a
error ([[Char]] -> [Char]
unlines [[Char]]
msgs)
    Right Subst ShelleyEra
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst ShelleyEra
x
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn (forall a. Show a => a -> [Char]
show Subst ShelleyEra
subst)
  Env ShelleyEra
env <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ShelleyEra
subst forall era. Env era
emptyEnv
  [([Char], Bool, Pred ShelleyEra)]
ss <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall era. Env era -> Pred era -> Typed ([Char], Bool, Pred era)
makeTest Env ShelleyEra
env) forall a b. (a -> b) -> a -> b
$ forall era. EraGov era => Proof era -> [Pred era]
constraints Proof ShelleyEra
proof)
  let bad :: [([Char], Bool, Pred ShelleyEra)]
bad = forall a. (a -> Bool) -> [a] -> [a]
filter (\([Char]
_, Bool
b, Pred ShelleyEra
_) -> Bool -> Bool
not Bool
b) [([Char], Bool, Pred ShelleyEra)]
ss
  if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], Bool, Pred ShelleyEra)]
bad)
    then forall a. HasCallStack => [Char] -> a
error ([Char]
"Some conditions fail\n" forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unlines (forall a b. (a -> b) -> [a] -> [b]
map (\([Char]
s, Bool
_, Pred ShelleyEra
_) -> [Char]
s) [([Char], Bool, Pred ShelleyEra)]
bad))
    else [Char] -> IO ()
putStrLn [Char]
"+++ OK, passed 1 test."

-- ================================================

pstateConstraints :: Era era => [Pred era]
pstateConstraints :: forall era. Era era => [Pred era]
pstateConstraints =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
20) forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , -- we have , retiring :⊆: regPools        :⊆: poolsUinv AND
    --                         futureRegPools) :⊆: poolHashUniv
    -- We need to adjust the sizes so that these constraints are possible
    forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtMost Int
3) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) -- Small enough that its leaves some slack with poolHashUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
5 Int
6) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring) -- Small enough that its leaves some slack with poolHashUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
9) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) -- Large enough that retiring is a strict subset
  -- the disjoint set futureRegPools can be as big as three
  -- the must set can be as big as 6
  -- so the may set can't be bigger than 6
  -- or we get an error like:   Size inconsistency. We need 7. The most we can get from (sub-disj) is 6
  , (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits) forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits)
  , (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring) forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
  , (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring)
  ]

test8 :: Gen Property
test8 :: Gen Property
test8 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof AlonzoEra
Alonzo
    [Char]
"Test 8. Pstate constraints"
    Bool
False
    -- (stoi{setBeforeSubset = False})  -- Both of these choices work
    (OrderInfo
stoi {setBeforeSubset :: Bool
setBeforeSubset = Bool
True}) -- But neither works without the Sized constraints
    forall era. Era era => [Pred era]
pstateConstraints
    (forall t era x. PrettyA t => RootTarget era x t -> Assembler era
Assemble forall era. Era era => RootTarget era (PState era) (PState era)
pstateT)

-- ==============================================================
-- Test the summation predicates

sumPreds :: Reflect era => Proof era -> [Pred era]
sumPreds :: forall era. Reflect era => Proof era -> [Pred era]
sumPreds Proof era
proof =
  [ forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
totalAda
  , forall era. Era era => Term era Coin
fees forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
400))
  , forall era. Era era => Term era Coin
deposits forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
200))
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
totalAda OrdCond
LTE [forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
fees, forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
deposits, forall era c. Term era c -> Sum era c
One Term era Coin
utxoAmt]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era (Ratio Integer)
RationalR Lens' IndividualPoolStake (Ratio Integer)
individualPoolStakeL forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
utxoAmt OrdCond
GTH [forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL (forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
proof)]
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) (forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
proof) -- Any map that is summed, to a nonzero amount, can't be empty.
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr
  ]
  where
    utxoAmt :: Term era Coin
utxoAmt = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"utxoAmt" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No)

test9 :: Gen Property
test9 :: Gen Property
test9 = forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn Proof AlonzoEra
Alonzo [Char]
"Test 9. Test of summing" Bool
False OrderInfo
stoi (forall era. Reflect era => Proof era -> [Pred era]
sumPreds Proof AlonzoEra
Alonzo) forall era. Assembler era
Skip

test10 :: Gen Property
test10 :: Gen Property
test10 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof MaryEra
proof
    [Char]
"Test 10. Test conditions EQL LTH LTE GTH GTE"
    Bool
False
    OrderInfo
stoi
    [ forall era t. Term era t -> Pred era
Random Term MaryEra Coin
x
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
2) Term MaryEra Coin
y -- We Shouldn't need this, but without it breaks the LTH case  ? < 2 can't be solved
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumLTH OrdCond
LTH [forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumLTE OrdCond
LTE [forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumGTH OrdCond
GTH [forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumGTE OrdCond
GTE [forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumEQL OrdCond
EQL [forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    ]
    forall era. Assembler era
Skip
  where
    x :: Term MaryEra Coin
x = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"x" forall era. Rep era Coin
rep forall era s t. Access era s t
No)
    y :: Term MaryEra Coin
y = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"y" forall era. Rep era Coin
rep forall era s t. Access era s t
No)
    tsumLTH :: Term MaryEra Coin
tsumLTH = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumLTH" forall era. Rep era Coin
rep forall era s t. Access era s t
No)
    tsumLTE :: Term MaryEra Coin
tsumLTE = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumLTE" forall era. Rep era Coin
rep forall era s t. Access era s t
No)
    tsumGTH :: Term MaryEra Coin
tsumGTH = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumGTH" forall era. Rep era Coin
rep forall era s t. Access era s t
No)
    tsumGTE :: Term MaryEra Coin
tsumGTE = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumGTE" forall era. Rep era Coin
rep forall era s t. Access era s t
No)
    tsumEQL :: Term MaryEra Coin
tsumEQL = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumEQL" forall era. Rep era Coin
rep forall era s t. Access era s t
No)
    rep :: Rep era Coin
rep = forall era. Rep era Coin
CoinR
    proof :: Proof MaryEra
proof = Proof MaryEra
Mary

test11 :: Gen Property
test11 :: Gen Property
test11 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof AlonzoEra
proof
    [Char]
"Test 11. Instanaeous Sum Tests"
    Bool
False
    OrderInfo
stoi
    [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era. Era era => Term era Coin
treasury
    , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanReserves
    , forall era. Term era DeltaCoin -> Term era DeltaCoin
Negate (forall era. Era era => Term era DeltaCoin
deltaReserves) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era DeltaCoin
deltaTreasury
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
instanReservesSum OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanReserves]
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
instanReservesSum) OrdCond
LTH [forall era c. Term era c -> Sum era c
One (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
reserves), forall era c. Term era c -> Sum era c
One forall era. Era era => Term era DeltaCoin
deltaReserves]
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
instanTreasurySum OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury]
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
instanTreasurySum) OrdCond
LTH [forall era c. Term era c -> Sum era c
One (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
treasury), forall era c. Term era c -> Sum era c
One forall era. Era era => Term era DeltaCoin
deltaTreasury]
    , forall era a b. Term era a -> Term era b -> Pred era
Before forall era. Era era => Term era Coin
reserves forall era. Era era => Term era DeltaCoin
deltaReserves
    ]
    forall era. Assembler era
Skip
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo

-- =====================================================

test12 :: Gen Property
test12 :: Gen Property
test12 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof ShelleyEra
p
    [Char]
"Test 12. CanFollow tests"
    Bool
False
    OrderInfo
stoi
    [ forall era t. Term era t -> Pred era
Random (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof ShelleyEra
p)
    , forall era t. Term era t -> Pred era
Random (forall era. Era era => Proof era -> Term era ProtVer
prevProtVer Proof ShelleyEra
p)
    , (forall era. Era era => Proof era -> Term era ProtVer
protVer Proof ShelleyEra
p) forall n era. Count n => Term era n -> Term era n -> Pred era
`CanFollow` (forall era. Era era => Proof era -> Term era ProtVer
prevProtVer Proof ShelleyEra
p)
    , forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (forall a b. b -> Either a b
Right (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof ShelleyEra
p)) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep ShelleyEra (PParamsF ShelleyEra)
pp (forall era. Era era => Proof era -> Term era ProtVer
protVer Proof ShelleyEra
p)]
    , forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (forall a b. b -> Either a b
Right (forall era. EraGov era => Proof era -> Term era (PParamsF era)
prevPParams Proof ShelleyEra
p)) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep ShelleyEra (PParamsF ShelleyEra)
pp (forall era. Era era => Proof era -> Term era ProtVer
prevProtVer Proof ShelleyEra
p)]
    ]
    forall era. Assembler era
Skip
  where
    pp :: Rep ShelleyEra (PParamsF ShelleyEra)
pp = forall era. Era era => Proof era -> Rep era (PParamsF era)
PParamsR Proof ShelleyEra
p
    p :: Proof ShelleyEra
p = Proof ShelleyEra
Shelley

-- ==============================================================
-- Test the Component Predicate

componentPreds :: EraGov era => Proof era -> [Pred era]
componentPreds :: forall era. EraGov era => Proof era -> [Pred era]
componentPreds Proof era
proof =
  [ forall era t. Term era t -> Pred era
Random (forall era. Era era => Proof era -> Term era Coin
minFeeA Proof era
proof)
  , forall era t. Term era t -> Pred era
Random Term era Size
size
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
size Term era (Set Int)
llx -- Note since size denotes a range, llx and mm could have different sizes
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
size Term era (Map Int Int)
mm
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
      (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
100))
      OrdCond
EQL
      [ forall era c. Term era c -> Sum era c
One (forall era. Era era => Proof era -> Term era Coin
minFeeA Proof era
proof)
      , forall era c. Term era c -> Sum era c
One (forall era. Era era => Proof era -> Term era Coin
minFeeB Proof era
proof)
      ]
  , forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (forall a b. b -> Either a b
Right (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
proof)) [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (forall era. Era era => Proof era -> Term era Coin
minFeeA Proof era
proof), forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (forall era. Era era => Proof era -> Term era Coin
minFeeB Proof era
proof)]
  ]
  where
    pp :: Rep era (PParamsF era)
pp = forall era. Era era => Proof era -> Rep era (PParamsF era)
PParamsR Proof era
proof
    llx :: Term era (Set Int)
llx = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"llx" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)
    size :: Term era Size
size = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"size" forall era. Rep era Size
SizeR forall era s t. Access era s t
No)
    mm :: Term era (Map Int Int)
mm = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"mm" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Rep era Int
IntR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)

test13 :: Gen Property
test13 :: Gen Property
test13 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof ShelleyEra
proof
    [Char]
"Test 13. Component tests"
    Bool
False
    OrderInfo
stoi
    (forall era. EraGov era => Proof era -> [Pred era]
componentPreds Proof ShelleyEra
proof)
    forall era. Assembler era
Skip
  where
    proof :: Proof ShelleyEra
proof = Proof ShelleyEra
Shelley

-- ==============================================

test14 :: IO ()
test14 :: IO ()
test14 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> IO ()
failn
    Proof AllegraEra
Allegra
    [Char]
"Test 14. Catch unsolveable use of Sized"
    Bool
False
    OrderInfo
stoi
    [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
6) forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
10) forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
    , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
    ]
    forall era. Assembler era
Skip

-- ==============================================

test15 :: Gen Property
test15 :: Gen Property
test15 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof AlonzoEra
proof
    [Char]
"Test 15. Summation on Natural"
    Bool
False
    OrderInfo
stoi
    [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof AlonzoEra
proof)
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof AlonzoEra
proof)
    , -- if both maxTxSize and maxBHSize are Random it may be impossible to solve
      -- because  both might be 0, and maxBBSize <= 0, is inconsistent.
      forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right Natural
1) (forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof AlonzoEra
proof) OrdCond
LTE [forall era c. Term era c -> Sum era c
One (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof AlonzoEra
proof), forall era c. Term era c -> Sum era c
One (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof AlonzoEra
proof)]
    , forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component
        (forall a b. b -> Either a b
Right (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof AlonzoEra
proof))
        [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep AlonzoEra (PParamsF AlonzoEra)
pp (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof AlonzoEra
proof), forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep AlonzoEra (PParamsF AlonzoEra)
pp (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof AlonzoEra
proof), forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep AlonzoEra (PParamsF AlonzoEra)
pp (forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof AlonzoEra
proof)]
    ]
    forall era. Assembler era
Skip
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo
    pp :: Rep AlonzoEra (PParamsF AlonzoEra)
pp = forall era. Era era => Proof era -> Rep era (PParamsF era)
PParamsR Proof AlonzoEra
proof

-- ============================================================

preds16 :: Era era => Proof era -> [Pred era]
preds16 :: forall era. Era era => Proof era -> [Pred era]
preds16 Proof era
_proof =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
6) forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
3) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr) -- At least 1 but smaller than the poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era (Ratio Integer)
RationalR Lens' IndividualPoolStake (Ratio Integer)
individualPoolStakeL forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr]
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
4) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) (Ratio Integer))
foox) -- At least 1 but smaller than the poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) (Ratio Integer))
foox forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (KeyHash 'StakePool) (Ratio Integer))
foox]
  ]
  where
    foox :: Term era (Map (KeyHash 'StakePool) (Ratio Integer))
foox = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"foo" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era (KeyHash 'StakePool)
PoolHashR forall era. Rep era (Ratio Integer)
RationalR) forall era s t. Access era s t
No)

test16 :: Gen Property
test16 :: Gen Property
test16 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof AlonzoEra
proof
    [Char]
"Test 11C. Test NonEmpty subset"
    Bool
False
    OrderInfo
stoi
    (forall era. Era era => Proof era -> [Pred era]
preds16 Proof AlonzoEra
proof)
    forall era. Assembler era
Skip
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo

-- ==============================================

univPreds :: Era era => Proof era -> [Pred era]
univPreds :: forall era. Era era => Proof era -> [Pred era]
univPreds Proof era
p =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
15) forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
20) forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
12) forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
12) forall era. Era era => Term era (Set TxIn)
txinUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
prevBlocksMade forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
currBlocksMade forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
markPools forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
markPoolDistr forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
setPools forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
goPools forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
markStake forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
markDelegs forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
setStake forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
setDelegs forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
goStake forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
goDelegs forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanReserves forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era -> Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era))
pparamProposals Proof era
p) forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era -> Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era))
futurePParamProposals Proof era
p) forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p) forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set TxIn)
txinUniv
  ]

pstatePreds :: Era era => Proof era -> [Pred era]
pstatePreds :: forall era. Era era => Proof era -> [Pred era]
pstatePreds Proof era
_p =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtMost Int
3) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) -- See comments in test8 why we need these Fixed predicates
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
5 Int
6) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring) -- we need       retiring :⊆: regPools        :⊆: poolsUinv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
9) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) -- AND we need                 futureRegPools  :⊆: poolHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
  , -- , Dom futureRegPools :⊆: Dom poolDistr  -- Don't think we want this
    forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring)
  ]

dstatePreds :: Era era => Proof era -> [Pred era]
dstatePreds :: forall era. Era era => Proof era -> [Pred era]
dstatePreds Proof era
_p =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtMost Int
8) forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards -- Small enough that its leaves some slack with credUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (Map (Credential 'Staking) DRep)
drepDelegation
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeeState
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era EpochNo
numDormantEpochs
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era era => Term era (Map Ptr (Credential 'Staking))
ptrs
  , -- This implies (Fixed (ExactSize 3) instanReserves)
    -- But it also implies that the new introduced variable instanReservesDom also has size 3
    -- ,  Sized (ExactSize 3) (Dom instanReserves)
    -- , Sized (ExactSize 2) (Dom instanTreasury)

    forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era. Era era => Term era Coin
treasury
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanReserves
  , forall era. Term era DeltaCoin -> Term era DeltaCoin
Negate (forall era. Era era => Term era DeltaCoin
deltaReserves) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era DeltaCoin
deltaTreasury
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
instanReservesSum OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanReserves]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
instanReservesSum) OrdCond
LTH [forall era c. Term era c -> Sum era c
One (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
reserves), forall era c. Term era c -> Sum era c
One forall era. Era era => Term era DeltaCoin
deltaReserves]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
instanTreasurySum OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
instanTreasurySum) OrdCond
LTH [forall era c. Term era c -> Sum era c
One (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
treasury), forall era c. Term era c -> Sum era c
One forall era. Era era => Term era DeltaCoin
deltaTreasury]
  , -- , Before reserves deltaReserves -- XXX
    -- , Before treasury deltaTreasury -- XXX
    forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  ]

accountstatePreds :: Proof era -> [Pred era]
accountstatePreds :: forall era. Proof era -> [Pred era]
accountstatePreds Proof era
_p = [] -- Constraints on reserves and treasury appear in dstatePreds

utxostatePreds :: Reflect era => Proof era -> [Pred era]
utxostatePreds :: forall era. Reflect era => Proof era -> [Pred era]
utxostatePreds Proof era
proof =
  [ forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
utxoCoin OrdCond
EQL [forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL (forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
proof)]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
deposits OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits, forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
      forall era. Era era => Term era Coin
totalAda
      OrdCond
EQL
      [forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
utxoCoin, forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
treasury, forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
reserves, forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
fees, forall era c. Term era c -> Sum era c
One forall era. Era era => Term era Coin
deposits, forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards]
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
fees
  , forall era t. Term era t -> Pred era
Random (forall era.
Era era =>
Proof era -> Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era))
pparamProposals Proof era
proof)
  , forall era t. Term era t -> Pred era
Random (forall era.
Era era =>
Proof era -> Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era))
futurePParamProposals Proof era
proof)
  , forall era t. Term era t -> Pred era
Random (forall era. Era era => Proof era -> Term era (FuturePParams era)
futurePParams Proof era
proof)
  ]

epochstatePreds :: EraGov era => Proof era -> [Pred era]
epochstatePreds :: forall era. EraGov era => Proof era -> [Pred era]
epochstatePreds Proof era
proof =
  [ forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (Map (Credential 'Staking) Coin)
markStake
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
markDelegs
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
markPools
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (Map (Credential 'Staking) Coin)
setStake
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
setDelegs
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
setPools
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (Map (Credential 'Staking) Coin)
goStake
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
goDelegs
  , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
goPools
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
snapShotFee
  , forall era t. Term era t -> Pred era
Random (forall era. EraGov era => Proof era -> Term era (PParamsF era)
prevPParams Proof era
proof)
  , forall era t. Term era t -> Pred era
Random (forall era. Era era => Proof era -> Term era (PParamsF era)
currPParams Proof era
proof)
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
donation
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
proof)
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
proof)
  , -- , Random (maxBBSize proof) -- This will cause underflow on Natural
    forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (forall a b. b -> Either a b
Right (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1000))
      (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1)
      OrdCond
EQL
      [forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era (Ratio Integer)
RationalR Lens' IndividualPoolStake (Ratio Integer)
individualPoolStakeL forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
markPoolDistr]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right Natural
1) (forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof era
proof) OrdCond
LTE [forall era c. Term era c -> Sum era c
One (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
proof), forall era c. Term era c -> Sum era c
One (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
proof)]
  , forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component
      (forall a b. b -> Either a b
Right (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
proof))
      [forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
proof), forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
proof), forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof era
proof)]
  ]
  where
    pp :: Rep era (PParamsF era)
pp = forall era. Era era => Proof era -> Rep era (PParamsF era)
PParamsR Proof era
proof

newepochstatePreds :: Era era => Proof era -> [Pred era]
newepochstatePreds :: forall era. Era era => Proof era -> [Pred era]
newepochstatePreds Proof era
_proof =
  [ forall era t. Term era t -> Pred era
Random forall era. Era era => Term era EpochNo
currentEpoch
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
8) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
prevBlocksMade) -- Both prevBlocksMade and prevBlocksMadeDom will have size 8
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
8) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
currBlocksMade)
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer
1 forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era (Ratio Integer)
RationalR Lens' IndividualPoolStake (Ratio Integer)
individualPoolStakeL forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr]
  ]

newepochConstraints :: Reflect era => Proof era -> [Pred era]
newepochConstraints :: forall era. Reflect era => Proof era -> [Pred era]
newepochConstraints Proof era
pr =
  forall era. Era era => Proof era -> [Pred era]
univPreds Proof era
pr
    forall a. [a] -> [a] -> [a]
++ forall era. Era era => Proof era -> [Pred era]
pstatePreds Proof era
pr
    forall a. [a] -> [a] -> [a]
++ forall era. Era era => Proof era -> [Pred era]
dstatePreds Proof era
pr
    forall a. [a] -> [a] -> [a]
++ forall era. Reflect era => Proof era -> [Pred era]
utxostatePreds Proof era
pr
    forall a. [a] -> [a] -> [a]
++ forall era. Proof era -> [Pred era]
accountstatePreds Proof era
pr
    forall a. [a] -> [a] -> [a]
++ forall era. EraGov era => Proof era -> [Pred era]
epochstatePreds Proof era
pr
    forall a. [a] -> [a] -> [a]
++ forall era. Era era => Proof era -> [Pred era]
newepochstatePreds Proof era
pr

test17 :: Gen Property
test17 :: Gen Property
test17 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof AlonzoEra
proof
    [Char]
"Test 17. Full NewEpochState"
    Bool
False
    (OrderInfo
stoi {sumBeforeParts :: Bool
sumBeforeParts = Bool
False})
    (forall era. Reflect era => Proof era -> [Pred era]
newepochConstraints Proof AlonzoEra
proof)
    (forall t era x. PrettyA t => RootTarget era x t -> Assembler era
Assemble (forall era.
EraGov era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof AlonzoEra
proof))
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo

-- ==========================================================
-- Tests of the Term projection function ProjS

projPreds1 :: Era era => Proof era -> [Pred era]
projPreds1 :: forall era. Era era => Proof era -> [Pred era]
projPreds1 Proof era
_proof =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
4) forall era. Era era => Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs
  , forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  ]

projPreds2 :: Era era => Proof era -> [Pred era]
projPreds2 :: forall era. Era era => Proof era -> [Pred era]
projPreds2 Proof era
_proof =
  [ forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
12) Term era (Set FutureGenDeleg)
futGDUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
6) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv)
  , forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  ]
  where
    futGDUniv :: Term era (Set FutureGenDeleg)
futGDUniv = (forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"futGDUniv" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era FutureGenDeleg
FutureGenDelegR) forall era s t. Access era s t
No))

test18a :: Gen Property
test18a :: Gen Property
test18a = forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn Proof AlonzoEra
proof [Char]
"Test 18a. Projection test" Bool
False OrderInfo
stoi (forall era. Era era => Proof era -> [Pred era]
projPreds1 Proof AlonzoEra
proof) forall era. Assembler era
Skip
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo

test18b :: Gen Property
test18b :: Gen Property
test18b =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof AlonzoEra
proof
    [Char]
"Test 18b. Projection test with subset"
    Bool
False
    OrderInfo
stoi
    (forall era. Era era => Proof era -> [Pred era]
projPreds2 Proof AlonzoEra
proof)
    (forall t era x. PrettyA t => RootTarget era x t -> Assembler era
Assemble (forall a b era. [Char] -> (a -> b) -> RootTarget era Void (a -> b)
Constr [Char]
"Pair" (,) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs))
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo

-- ===============================================
-- test of projOnDom

help19 ::
  forall era.
  Era era =>
  Proof era ->
  Gen (Map FutureGenDeleg GenDelegPair)
help19 :: forall era.
Era era =>
Proof era -> Gen (Map FutureGenDeleg GenDelegPair)
help19 Proof era
_proof = do
  Set (KeyHash 'Genesis)
setA <- forall era b. Rep era b -> Gen b
genRep @era (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR)
  Map FutureGenDeleg GenDelegPair
ans <- forall era a dom rng.
Ord dom =>
Set a
-> Lens' dom a -> Rep era dom -> Rep era rng -> Gen (Map dom rng)
projOnDom @era Set (KeyHash 'Genesis)
setA (Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL) forall era. Era era => Rep era FutureGenDeleg
FutureGenDelegR forall era. Era era => Rep era GenDelegPair
GenDelegPairR
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Map FutureGenDeleg GenDelegPair
ans

test19 :: IO ()
test19 :: IO ()
test19 = do
  [Char] -> IO ()
putStrLn [Char]
"testing: Test 19. test of projOnDom function"
  Map FutureGenDeleg GenDelegPair
ans <- forall a. Gen a -> IO a
generate (forall era.
Era era =>
Proof era -> Gen (Map FutureGenDeleg GenDelegPair)
help19 Proof MaryEra
Mary)
  [Char] -> IO ()
putStrLn (forall e t. Rep e t -> t -> [Char]
synopsis (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR (forall era. Era era => Rep era FutureGenDeleg
FutureGenDelegR @BabbageEra) forall era. Era era => Rep era GenDelegPair
GenDelegPairR) Map FutureGenDeleg GenDelegPair
ans) -- (ppMap pcFutureGenDeleg pcGenDelegPair ans))
  [Char] -> IO ()
putStrLn [Char]
"+++ OK, passed 1 test"

-- ===================================================

preds20 :: Era era => Proof era -> [Pred era]
preds20 :: forall era. Era era => Proof era -> [Pred era]
preds20 Proof era
proof =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
10) Term era (Set Int)
intUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtMost Int
6) Term era (Map Int Word64)
rewardsx
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map Int Word64)
rewardsx forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
intUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map Int Word64)
rewardsx forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map Ptr Int)
ptrsx
  ]
  where
    rewardsx :: Term era (Map Int Word64)
rewardsx = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> [Char] -> Rep era t -> Access era s t -> V era t
pV Proof era
proof [Char]
"rewards" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Rep era Int
IntR forall era. Rep era Word64
Word64R) forall era s t. Access era s t
No)
    ptrsx :: Term era (Map Ptr Int)
ptrsx = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> [Char] -> Rep era t -> Access era s t -> V era t
pV Proof era
proof [Char]
"ptrs" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Rep era Ptr
PtrR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)
    intUniv :: Term era (Set Int)
intUniv = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> [Char] -> Rep era t -> Access era s t -> V era t
pV Proof era
proof [Char]
"intUniv" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)

test20 :: Gen Property
test20 :: Gen Property
test20 =
  forall era.
Reflect era =>
Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen Property
testn
    Proof AlonzoEra
proof
    [Char]
"Test 20. Test ptr rewards iso"
    Bool
False
    OrderInfo
stoi
    (forall era. Era era => Proof era -> [Pred era]
preds20 Proof AlonzoEra
proof)
    forall era. Assembler era
Skip
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo

test21 :: Int -> IO Bool
test21 :: Int -> IO Bool
test21 Int
seed = do
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
      w :: Term BabbageEra [Int]
w = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"w" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Rep era Int
IntR) forall era s t. Access era s t
No)
      a :: Term BabbageEra Int
a = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"a" forall era. Rep era Int
IntR forall era s t. Access era s t
No)
      b :: Term BabbageEra Int
b = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"b" forall era. Rep era Int
IntR forall era s t. Access era s t
No)
      c :: Term BabbageEra Int
c = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"c" forall era. Rep era Int
IntR forall era s t. Access era s t
No)
      pred21 :: Pred BabbageEra
pred21 =
        forall t era.
(Eq t, Era era) =>
Term era t -> [(Int, RootTarget era t t, [Pred era])] -> Pred era
Oneof
          Term BabbageEra [Int]
w
          [
            ( Int
1
            , forall root a b era.
[Char] -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert [Char]
"three" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[Int]) (\Int
x Int
y Int
z -> [Int
x, Int
y, Int
z])
                forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
a (\case [Int
x, Int
_, Int
_] -> forall a. a -> Maybe a
Just Int
x; [Int]
_ -> forall a. Maybe a
Nothing)
                forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
b (\case [Int
_, Int
y, Int
_] -> forall a. a -> Maybe a
Just Int
y; [Int]
_ -> forall a. Maybe a
Nothing)
                forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
c (\case [Int
_, Int
_, Int
z] -> forall a. a -> Maybe a
Just Int
z; [Int]
_ -> forall a. Maybe a
Nothing)
            , [forall era t. Term era t -> Pred era
Random Term BabbageEra Int
a, forall era t. Term era t -> Pred era
Random Term BabbageEra Int
b, forall era t. Term era t -> Pred era
Random Term BabbageEra Int
c]
            )
          ,
            ( Int
1
            , forall root a b era.
[Char] -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert [Char]
"two" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[Int]) (\Int
x Int
y -> [Int
x, Int
y])
                forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
a (\case [Int
x, Int
_] -> forall a. a -> Maybe a
Just Int
x; [Int]
_ -> forall a. Maybe a
Nothing)
                forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
b (\case [Int
_, Int
y] -> forall a. a -> Maybe a
Just Int
y; [Int]
_ -> forall a. Maybe a
Nothing)
            , [forall era t. Term era t -> Pred era
Random Term BabbageEra Int
a, forall era t. Term era t -> Pred era
Random Term BabbageEra Int
b]
            )
          ,
            ( Int
1
            , forall root a b era.
[Char] -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert [Char]
"one" (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[Int]) (\Int
x -> [Int
x])
                forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
a (\case [Int
x] -> forall a. a -> Maybe a
Just Int
x; [Int]
_ -> forall a. Maybe a
Nothing)
            , [forall era t. Term era t -> Pred era
Random Term BabbageEra Int
a]
            )
          ]
  Env BabbageEra
env <-
    forall a. Int -> Gen a -> IO a
generateWithSeed
      Int
seed
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof BabbageEra
proof OrderInfo
standardOrderInfo [Pred BabbageEra
pred21]
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst BabbageEra
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst BabbageEra
subst forall era. Env era
emptyEnv))
      )
  forall a. Show a => a -> IO ()
print Env BabbageEra
env
  forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Env era -> Pred era -> Typed Bool
runPred Env BabbageEra
env Pred BabbageEra
pred21

-- ===================================================
-- run all the tests

testAll :: IO ()
testAll :: IO ()
testAll = TestTree -> IO ()
defaultMain TestTree
allExampleTests

allExampleTests :: TestTree
allExampleTests :: TestTree
allExampleTests =
  [Char] -> [TestTree] -> TestTree
testGroup
    [Char]
"Example tests"
    [ [Char] -> IO () -> TestTree
testCase [Char]
"test 1A. Cyclic preds detected" forall a b. (a -> b) -> a -> b
$
        case forall x. Typed x -> Either [[Char]] x
runTyped (forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile @BabbageEra OrderInfo
standardOrderInfo forall era. Era era => [Pred era]
cyclicPred) of
          Right DependGraph BabbageEra
_ -> forall a. HasCallStack => [Char] -> IO a
assertFailure ([Char]
"Cyclic preds Not detected.")
          Left [[Char]]
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    , [Char] -> IO () -> TestTree
testCase [Char]
"test 1B. ACyclic preds solved" forall a b. (a -> b) -> a -> b
$
        case forall x. Typed x -> Either [[Char]] x
runTyped (forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile @BabbageEra OrderInfo
standardOrderInfo forall era. Era era => [Pred era]
aCyclicPred) of
          Right DependGraph BabbageEra
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left [[Char]]
xs -> forall a. HasCallStack => [Char] -> IO a
assertFailure ([[Char]] -> [Char]
unlines [[Char]]
xs)
    , forall a. [Char] -> IO a -> TestTree
testIO
        [Char]
"test 19 Test of projOnDom function"
        (forall a. Gen a -> IO a
generate (forall era.
Era era =>
Proof era -> Gen (Map FutureGenDeleg GenDelegPair)
help19 Proof MaryEra
Mary))
    , forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test 4. Inconsistent Size" IO ()
test4
    , forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test 5. Bad Sum, impossible partition." IO ()
test5
    , forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test6. Find a viable order of variables" (Bool -> IO ()
test6 Bool
False)
    , forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test7. Compute a solution" (Bool -> IO ()
test7 Bool
False)
    , forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test 14 Catch unsolveable use of Sized" IO ()
test14
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 3. PState example" Gen Property
test3
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 8. Pstate constraints" Gen Property
test8
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 9. Test of summing" Gen Property
test9
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 10. Test conditions EQL LTH LTE GTH GTE" Gen Property
test10
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
100 [Char]
"Test 11. Instanaeous Sum Tests" Gen Property
test11
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 12. CanFollow tests" Gen Property
test12
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 13. Component tests" Gen Property
test13
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 15. Summation on Natural" Gen Property
test15
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 16. Test NonEmpty subset" Gen Property
test16
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 17. Full NewEpochState" (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30) Gen Property
test17)
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 18a. Projection test" Gen Property
test18a
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 18b. Projection test" Gen Property
test18b
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 20. ptr & rewards are inverses" Gen Property
test20
    , forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Constraint soundness" forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => Int -> prop -> Property
within Int
1000000 forall a b. (a -> b) -> a -> b
$ OrderInfo -> Property
prop_soundness
    , forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"Shrinking soundness" forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 forall a b. (a -> b) -> a -> b
$ OrderInfo -> Property
prop_shrinking
    , forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"NewEpochState and Tx generation" forall a b. (a -> b) -> a -> b
$ do
        (NewEpochState ConwayEra
st, AlonzoTx ConwayEra
tx, Env ConwayEra
_) <- forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (NewEpochState era, Tx era, Env era)
genTxAndNewEpoch forall a. Default a => a
def forall a b. (a -> b) -> a -> b
$ Proof ConwayEra
Conway
        (NewEpochState ConwayEra
st, AlonzoTx ConwayEra
tx) forall a b. NFData a => a -> b -> b
`deepseq` forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    , forall era.
Reflect era =>
[Char] -> Proof era -> [Pred era] -> TestTree
testPreds [Char]
"ListWhereTest" Proof ConwayEra
Conway [Pred ConwayEra]
listWherePreds
    ]

-- ==============================

-- | Use to generate a solution to 'preds', test that the
--   solution meets the 'preds', and puts you in the Repl to
--   inspect the value of each variable solved for.
--   Companion function to 'testPreds'
demoPreds :: Reflect era => Proof era -> [Pred era] -> IO ()
demoPreds :: forall era. Reflect era => Proof era -> [Pred era] -> IO ()
demoPreds Proof era
proof [Pred era]
preds = do
  let tryPred :: Env era -> Pred era -> (Pred era, Bool)
tryPred Env era
env Pred era
p = (Pred era
p, forall t. HasCallStack => Typed t -> t
errorTyped (forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
p))
  Env era
env <-
    forall a. Gen a -> IO a
generate
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo [Pred era]
preds
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv)
      )
  let pairs :: [(Pred era, Bool)]
pairs = forall a b. (a -> b) -> [a] -> [b]
map (forall {era}. Env era -> Pred era -> (Pred era, Bool)
tryPred Env era
env) [Pred era]
preds
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Pred era
p, Bool
b) -> [Char] -> IO ()
putStrLn (forall a. Show a => a -> [Char]
show Pred era
p forall a. [a] -> [a] -> [a]
++ [Char]
" = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Bool
b)) [(Pred era, Bool)]
pairs
  forall era. ReplMode -> Proof era -> Env era -> [Char] -> IO ()
modeRepl ReplMode
Interactive Proof era
proof Env era
env [Char]
""

-- | Use this to generate a solution to 'preds', and make a TestTree
--   that tests the solution meets the 'preds'.
--   Companion function to 'demoPreds'
testPreds :: Reflect era => String -> Proof era -> [Pred era] -> TestTree
testPreds :: forall era.
Reflect era =>
[Char] -> Proof era -> [Pred era] -> TestTree
testPreds [Char]
name Proof era
proof [Pred era]
preds = do
  let tryPred :: Env era -> Pred era -> (Pred era, Bool)
tryPred Env era
env Pred era
p = (Pred era
p, forall t. HasCallStack => Typed t -> t
errorTyped (forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
p))
  forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
name forall a b. (a -> b) -> a -> b
$ do
    Env era
env <-
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo [Pred era]
preds
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv)
      )
    let pairs :: [(Pred era, Bool)]
pairs = forall a b. (a -> b) -> [a] -> [b]
map (forall {era}. Env era -> Pred era -> (Pred era, Bool)
tryPred Env era
env) [Pred era]
preds
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall prop. Testable prop => prop -> Property
property (forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Pred era, Bool)]
pairs)))

listWherePreds :: [Pred ConwayEra]
listWherePreds :: [Pred ConwayEra]
listWherePreds =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
10) forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
10) forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
  , forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> RootTarget era t t -> [Pred era] -> Pred era
ListWhere
      (forall era. Era era => Int -> Int -> Term era Size
Range Int
2 Int
4)
      Term ConwayEra [(Credential 'Staking, Credential 'DRepRole)]
ans
      (forall era a b.
(Typeable a, Typeable b, Era era) =>
Rep era a -> Rep era b -> RootTarget era (a, b) (a, b)
pairT forall era. Era era => Rep era (Credential 'Staking)
CredR forall era. Era era => Rep era (Credential 'DRepRole)
VCredR)
      [forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. b -> Either a b
Right (forall era a. Era era => Rep era a -> Term era a
pair1 forall era. Era era => Rep era (Credential 'Staking)
CredR)) forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv, forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. b -> Either a b
Right (forall era a. Era era => Rep era a -> Term era a
pair2 forall era. Era era => Rep era (Credential 'DRepRole)
VCredR)) forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv]
  ]
  where
    ans :: Term ConwayEra [(Credential 'Staking, Credential 'DRepRole)]
ans = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"ans" (forall era a. Rep era a -> Rep era [a]
ListR (forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR forall era. Era era => Rep era (Credential 'Staking)
CredR forall era. Era era => Rep era (Credential 'DRepRole)
VCredR)) forall era s t. Access era s t
No)

mainListWhere :: IO ()
mainListWhere :: IO ()
mainListWhere = forall era. Reflect era => Proof era -> [Pred era] -> IO ()
demoPreds Proof ConwayEra
Conway [Pred ConwayEra]
listWherePreds

govPreds :: [Pred ConwayEra]
govPreds :: [Pred ConwayEra]
govPreds =
  [ forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> RootTarget era t t -> [Pred era] -> Pred era
ListWhere
      (forall era. Era era => Int -> Int -> Term era Size
Range Int
2 Int
4)
      forall era. Era era => Term era [GovActionState era]
currGovStates
      forall era.
Era era =>
RootTarget era (GovActionState era) (GovActionState era)
govActionStateTarget
      [ forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Set (Credential 'HotCommitteeRole))
hotCommitteeCredsUniv
      , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
      , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
      , forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
13) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era Coin
depositV
      , forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era EpochNo
EpochR (Word64 -> EpochNo
EpochNo Word64
3) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era EpochNo
currentEpoch
      , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era GovActionId
idV
      , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'HotCommitteeRole) Vote)
committeeVotesV) forall era.
Era era =>
Term era (Set (Credential 'HotCommitteeRole))
hotCommitteeCredsUniv
      , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'DRepRole) Vote)
drepVotesV) forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
      , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Vote)
stakePoolVotesV) forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
      , forall era. Era era => Term era Coin
proposalDeposits forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era Coin
depositV
      , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era RewardAccount
returnAddrV
      , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era (GovAction era)
actionV
      , forall era. Era era => Term era EpochNo
currentEpoch forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era EpochNo
proposedInV
      , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era EpochNo
expiresAfterV
      , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
3) forall era. Era era => Term era (Set GovActionId)
childrenV
      ]
  ]

mainGov :: IO ()
mainGov :: IO ()
mainGov = forall era. Reflect era => Proof era -> [Pred era] -> IO ()
demoPreds Proof ConwayEra
Conway [Pred ConwayEra]
govPreds