{-# 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.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Core (Era)
import Cardano.Ledger.Keys (GenDelegPair)
import Cardano.Ledger.State (EraCertState (..), FutureGenDeleg (..))
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 Typed (DependGraph era) -> Either [[Char]] (DependGraph era)
forall x. Typed x -> Either [[Char]] x
runTyped (OrderInfo -> [Pred era] -> Typed (DependGraph era)
forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
standardOrderInfo [Pred era]
cs) of
  Right DependGraph era
x -> DependGraph era -> IO ()
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 = [Pred era] -> [Pred era] -> [Pred era]
forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeEqual [Pred era]
cs []
  let cs4 :: [Pred era]
cs4 = [Pred era] -> [Pred era] -> [Pred era]
forall era. Era era => [Pred era] -> [Pred era] -> [Pred era]
removeSameVar [Pred era]
cs3 []
  graph :: DependGraph era
graph@(DependGraph [([Name era], [Pred era])]
_) <- Typed (DependGraph era) -> Gen (DependGraph era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (DependGraph era) -> Gen (DependGraph era))
-> Typed (DependGraph era) -> Gen (DependGraph era)
forall a b. (a -> b) -> a -> b
$ OrderInfo -> [Pred era] -> Typed (DependGraph era)
forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
order [Pred era]
cs
  let messages1 :: [[Char]]
messages1 =
        if (Pred era -> Pred era -> Bool) -> [Pred era] -> [Pred era] -> Bool
forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
listEq Pred era -> Pred era -> Bool
forall era. Era era => Pred era -> Pred era -> Bool
cpeq [Pred era]
cs4 [Pred era]
cs
          then [[Char]
"Constraints", [Pred era] -> [Char]
forall a. Show a => a -> [Char]
show [Pred era]
cs, [Char]
"Rewriting is idempotent"]
          else
            [ [Char]
"Constraints"
            , [Pred era] -> [Char]
forall a. Show a => a -> [Char]
show [Pred era]
cs
            , [Char]
"Substitute for Equality"
            , [Pred era] -> [Char]
forall a. Show a => a -> [Char]
show [Pred era]
cs3
            , [Char]
"Remove syntactic tautologies"
            , [Pred era] -> [Char]
forall a. Show a => a -> [Char]
show [Pred era]
cs4
            , [Char]
"Pick a variable ordering\n"
            , DependGraph era -> [Char]
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 [Char]
-> Gen (Either [[Char]] (Subst era))
-> Gen (Either [[Char]] (Subst era))
forall a. [Char] -> a -> a
Debug.trace ([[Char]] -> [Char]
unlines [[Char]]
messages1) (Bool
-> Proof era
-> DependGraph era
-> Gen (Either [[Char]] (Subst era))
forall era.
Bool
-> Proof era
-> DependGraph era
-> Gen (Either [[Char]] (Subst era))
genDependGraph Bool
loud Proof era
proof DependGraph era
graph)
      else Bool
-> Proof era
-> DependGraph era
-> Gen (Either [[Char]] (Subst era))
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 -> [Char] -> Gen (Subst era)
forall a. HasCallStack => [Char] -> a
error ([[Char]] -> [Char]
unlines [[Char]]
msgs)
    Right Subst era
x -> Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
x
  !Env era
env <- Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv
  [([Char], Bool, Pred era)]
testTriples <- Typed [([Char], Bool, Pred era)] -> Gen [([Char], Bool, Pred era)]
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped ((Pred era -> Typed ([Char], Bool, Pred era))
-> [Pred era] -> Typed [([Char], Bool, Pred era)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env era -> Pred era -> Typed ([Char], Bool, Pred era)
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" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Subst era -> [Char]
forall a. Show a => a -> [Char]
show Subst era
subst
  ![[Char]]
messages3 <- case Assembler era
target of
    Assembler era
Skip -> [[Char]] -> Gen [[Char]]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    Assemble RootTarget era x t
t -> do
      !t
tval <- Typed t -> Gen t
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Env era -> RootTarget era x t -> Typed t
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era x t
t)
      [[Char]] -> Gen [[Char]]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [[Char]
"\nAssemble the pieces\n", PDoc -> [Char]
forall a. Show a => a -> [Char]
show (t -> PDoc
forall t. PrettyA t => t -> PDoc
prettyA t
tval)]
  let bad :: [([Char], Bool, Pred era)]
bad = (([Char], Bool, Pred era) -> Bool)
-> [([Char], Bool, Pred era)] -> [([Char], Bool, Pred era)]
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 [([Char], Bool, Pred era)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], Bool, Pred era)]
bad
          then Maybe [Char]
forall a. Maybe a
Nothing -- Indicates success, nothing bad happened
          else [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char]
"Some conditions fail\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [([Char], Bool, Pred era)] -> Subst era -> [Char]
forall era.
Era era =>
[([Char], Bool, Pred era)] -> Subst era -> [Char]
explainBad [([Char], Bool, Pred era)]
bad Subst era
subst)
  if Bool
loud
    then [Char] -> Gen (Maybe [Char]) -> Gen (Maybe [Char])
forall a. [Char] -> a -> a
Debug.trace ([[Char]] -> [Char]
unlines ([Char]
messages2 [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]]
messages3)) (Maybe [Char] -> Gen (Maybe [Char])
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Char]
ans)
    else Maybe [Char] -> Gen (Maybe [Char])
forall a. a -> Gen a
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 <- Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen (Maybe [Char])
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 -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample [Char]
"" Bool
True
    Just [Char]
xs -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> Property
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
  IO () -> Selector ErrorCall -> IO ()
forall e a.
(HasCallStack, Exception e) =>
IO a -> Selector e -> IO ()
shouldThrow
    ( do
        Maybe [Char]
result <- Gen (Maybe [Char]) -> IO (Maybe [Char])
forall a. Gen a -> IO a
generate (Proof era
-> [Char]
-> Bool
-> OrderInfo
-> [Pred era]
-> Assembler era
-> Gen (Maybe [Char])
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 [Char] -> [Char] -> [Char]
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 () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    )
    ( \(ErrorCall [Char]
msg) ->
        [Char] -> Bool -> Bool
forall a. [Char] -> a -> a
Debug.trace
          ( if Bool
loud
              then ([Char]
"Fails as expected\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
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: '" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
name [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'")
  Gen Property -> IO ()
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 Term era (Set Int) -> Term era (Set Int) -> Pred era
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 Term era (Set Int) -> Term era (Set Int) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
c, Term era (Set Int) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Set Int)
c]
  where
    a :: Term era (Set Int)
a = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Set Int) -> Access era Any (Set Int) -> V era (Set Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"a" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
forall era s t. Access era s t
No)
    b :: Term era (Set Int)
b = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Set Int) -> Access era Any (Set Int) -> V era (Set Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"b" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
forall era s t. Access era s t
No)
    c :: Term era (Set Int)
c = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Set Int) -> Access era Any (Set Int) -> V era (Set Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"c" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
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 Term era (Set Int) -> Term era (Set Int) -> Pred era
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 Term era (Set Int) -> Term era (Set Int) -> Pred era
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 Term era (Set Int) -> Term era (Set Int) -> Pred era
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 Term era (Set Int) -> Term era (Set Int) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
a, Term era (Set Int) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Set Int)
d]
  where
    a :: Term era (Set Int)
a = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Set Int) -> Access era Any (Set Int) -> V era (Set Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"a" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
forall era s t. Access era s t
No)
    b :: Term era (Set Int)
b = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Set Int) -> Access era Any (Set Int) -> V era (Set Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"b" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
forall era s t. Access era s t
No)
    c :: Term era (Set Int)
c = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Set Int) -> Access era Any (Set Int) -> V era (Set Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"c" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
forall era s t. Access era s t
No)
    d :: Term era (Set Int)
d = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Set Int) -> Access era Any (Set Int) -> V era (Set Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"d" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
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 [Pred BabbageEra]
forall era. Era era => [Pred era]
aCyclicPred
  [Char] -> IO ()
putStrLn [Char]
"+++ OK, passed 1 test."

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

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

test4 :: IO ()
test4 :: IO ()
test4 = Proof MaryEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred MaryEra]
-> Assembler MaryEra
-> IO ()
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 Assembler MaryEra
forall era. Assembler era
Skip
  where
    cs :: [Pred MaryEra]
cs =
      [ Term MaryEra Size
-> Term MaryEra (Map (Credential 'Staking) Coin) -> Pred MaryEra
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term MaryEra Size
forall era. Era era => Int -> Term era Size
ExactSize Int
5) Term MaryEra (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
      , Direct Coin
-> Term MaryEra Coin
-> OrdCond
-> [Sum MaryEra Coin]
-> Pred MaryEra
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) (Rep MaryEra Coin -> Coin -> Term MaryEra Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep MaryEra Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
5)) OrdCond
GTH [Term MaryEra (Map (Credential 'Staking) Coin) -> Sum MaryEra Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term MaryEra (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards]
      ]

test5 :: IO ()
test5 :: IO ()
test5 = Proof MaryEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred MaryEra]
-> Assembler MaryEra
-> IO ()
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 Assembler MaryEra
forall era. Assembler era
Skip
  where
    cs :: [Pred MaryEra]
cs =
      [ Term MaryEra Size
-> Term MaryEra (Map (Credential 'Staking) Coin) -> Pred MaryEra
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term MaryEra Size
forall era. Era era => Int -> Term era Size
ExactSize Int
5) Term MaryEra (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
      , Direct Coin
-> Term MaryEra Coin
-> OrdCond
-> [Sum MaryEra Coin]
-> Pred MaryEra
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) (Rep MaryEra Coin -> Coin -> Term MaryEra Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep MaryEra Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
4)) OrdCond
EQL [Term MaryEra (Map (Credential 'Staking) Coin) -> Sum MaryEra Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term MaryEra (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards]
      ]

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

constraints :: (EraGov era, EraCertState era) => Proof era -> [Pred era]
constraints :: forall era.
(EraGov era, EraCertState era) =>
Proof era -> [Pred era]
constraints Proof era
proof =
  [ Term era Size -> Term era (Set (Credential 'Staking)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
10) Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
10) Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era Size
-> Term era (Map (KeyHash 'StakePool) (Ratio Integer)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) Term era (Map (KeyHash 'StakePool) (Ratio Integer))
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr -- This is summed so it can't be empty.
  , Term era Size
-> Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools -- This has the same domain, so it can't be empty either
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era (Map (KeyHash 'StakePool) Coin)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
  , Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (KeyHash 'StakePool) (Ratio Integer))
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) (Ratio Integer))
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr
  , Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (KeyHash 'StakePool) Coin)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits
  , Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era (Map (KeyHash 'StakePool) EpochNo)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) EpochNo)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) EpochNo)
retiring Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
deposits OrdCond
EQL [Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits, Term era (Map (KeyHash 'StakePool) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits]
  , Direct (Ratio Integer)
-> Term era (Ratio Integer)
-> OrdCond
-> [Sum era (Ratio Integer)]
-> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Ratio Integer -> Direct (Ratio Integer)
forall a b. b -> Either a b
Right (Integer
1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (Rep era (Ratio Integer)
-> Ratio Integer -> Term era (Ratio Integer)
forall era t. Rep era t -> t -> Term era t
Lit Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [Term era (Map (KeyHash 'StakePool) (Ratio Integer))
-> Sum era (Ratio Integer)
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (KeyHash 'StakePool) (Ratio Integer))
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) (Ratio Integer))
mockPoolDistr]
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
      Term era Coin
forall era. Era era => Term era Coin
totalAda
      OrdCond
EQL
      [ Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
utxoCoin
      , Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
treasury
      , Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
reserves
      , Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
fees
      , Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits
      , Term era (Map (KeyHash 'StakePool) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits
      , Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
      ]
  , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
treasury
  , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
reserves
  , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
fees
  , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
utxoCoin
  , Term era (PParamsF era) -> Pred era
forall era t. Term era t -> Pred era
Random (Term era (PParamsF era) -> Pred era)
-> Term era (PParamsF era) -> Pred era
forall a b. (a -> b) -> a -> b
$ Proof era -> Term era (PParamsF era)
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"
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn [Char]
"======================================================="
  case Typed (DependGraph ShelleyEra)
-> Either [[Char]] (DependGraph ShelleyEra)
forall x. Typed x -> Either [[Char]] x
runTyped (OrderInfo -> [Pred ShelleyEra] -> Typed (DependGraph ShelleyEra)
forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
standardOrderInfo ([Pred ShelleyEra] -> Typed (DependGraph ShelleyEra))
-> [Pred ShelleyEra] -> Typed (DependGraph ShelleyEra)
forall a b. (a -> b) -> a -> b
$ Proof ShelleyEra -> [Pred ShelleyEra]
forall era.
(EraGov era, EraCertState era) =>
Proof era -> [Pred era]
constraints Proof ShelleyEra
Shelley) of
    Right DependGraph ShelleyEra
x ->
      if Bool
loud
        then DependGraph ShelleyEra -> IO ()
forall a. Show a => a -> IO ()
print DependGraph ShelleyEra
x
        else [Char] -> IO ()
putStrLn [Char]
"+++ OK, passed 1 test."
    Left [[Char]]
xs -> [Char] -> IO ()
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"
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn [Char]
"======================================================="
  let proof :: Proof ShelleyEra
proof = Proof ShelleyEra
Shelley
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn ([Pred ShelleyEra] -> [Char]
forall a. Show a => a -> [Char]
show ([Pred ShelleyEra] -> [Char]) -> [Pred ShelleyEra] -> [Char]
forall a b. (a -> b) -> a -> b
$ Proof ShelleyEra -> [Pred ShelleyEra]
forall era.
(EraGov era, EraCertState era) =>
Proof era -> [Pred era]
constraints Proof ShelleyEra
proof)
  DependGraph ShelleyEra
graph <- Typed (DependGraph ShelleyEra) -> IO (DependGraph ShelleyEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (DependGraph ShelleyEra) -> IO (DependGraph ShelleyEra))
-> Typed (DependGraph ShelleyEra) -> IO (DependGraph ShelleyEra)
forall a b. (a -> b) -> a -> b
$ OrderInfo -> [Pred ShelleyEra] -> Typed (DependGraph ShelleyEra)
forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile OrderInfo
standardOrderInfo ([Pred ShelleyEra] -> Typed (DependGraph ShelleyEra))
-> [Pred ShelleyEra] -> Typed (DependGraph ShelleyEra)
forall a b. (a -> b) -> a -> b
$ Proof ShelleyEra -> [Pred ShelleyEra]
forall era.
(EraGov era, EraCertState era) =>
Proof era -> [Pred era]
constraints Proof ShelleyEra
proof
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn (DependGraph ShelleyEra -> [Char]
forall a. Show a => a -> [Char]
show DependGraph ShelleyEra
graph)
  Either [[Char]] (Subst ShelleyEra)
result <- Gen (Either [[Char]] (Subst ShelleyEra))
-> IO (Either [[Char]] (Subst ShelleyEra))
forall a. Gen a -> IO a
generate (Bool
-> Proof ShelleyEra
-> DependGraph ShelleyEra
-> Gen (Either [[Char]] (Subst ShelleyEra))
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 -> [Char] -> IO (Subst ShelleyEra)
forall a. HasCallStack => [Char] -> a
error ([[Char]] -> [Char]
unlines [[Char]]
msgs)
    Right Subst ShelleyEra
x -> Subst ShelleyEra -> IO (Subst ShelleyEra)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst ShelleyEra
x
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
loud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn (Subst ShelleyEra -> [Char]
forall a. Show a => a -> [Char]
show Subst ShelleyEra
subst)
  Env ShelleyEra
env <- Typed (Env ShelleyEra) -> IO (Env ShelleyEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env ShelleyEra) -> IO (Env ShelleyEra))
-> Typed (Env ShelleyEra) -> IO (Env ShelleyEra)
forall a b. (a -> b) -> a -> b
$ Subst ShelleyEra -> Env ShelleyEra -> Typed (Env ShelleyEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ShelleyEra
subst Env ShelleyEra
forall era. Env era
emptyEnv
  [([Char], Bool, Pred ShelleyEra)]
ss <- Typed [([Char], Bool, Pred ShelleyEra)]
-> IO [([Char], Bool, Pred ShelleyEra)]
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped ((Pred ShelleyEra -> Typed ([Char], Bool, Pred ShelleyEra))
-> [Pred ShelleyEra] -> Typed [([Char], Bool, Pred ShelleyEra)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env ShelleyEra
-> Pred ShelleyEra -> Typed ([Char], Bool, Pred ShelleyEra)
forall era. Env era -> Pred era -> Typed ([Char], Bool, Pred era)
makeTest Env ShelleyEra
env) ([Pred ShelleyEra] -> Typed [([Char], Bool, Pred ShelleyEra)])
-> [Pred ShelleyEra] -> Typed [([Char], Bool, Pred ShelleyEra)]
forall a b. (a -> b) -> a -> b
$ Proof ShelleyEra -> [Pred ShelleyEra]
forall era.
(EraGov era, EraCertState era) =>
Proof era -> [Pred era]
constraints Proof ShelleyEra
proof)
  let bad :: [([Char], Bool, Pred ShelleyEra)]
bad = (([Char], Bool, Pred ShelleyEra) -> Bool)
-> [([Char], Bool, Pred ShelleyEra)]
-> [([Char], Bool, Pred ShelleyEra)]
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 ([([Char], Bool, Pred ShelleyEra)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], Bool, Pred ShelleyEra)]
bad)
    then [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char]
"Some conditions fail\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unlines ((([Char], Bool, Pred ShelleyEra) -> [Char])
-> [([Char], Bool, Pred ShelleyEra)] -> [[Char]]
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 :: EraCertState era => [Pred era]
pstateConstraints :: forall era. EraCertState era => [Pred era]
pstateConstraints =
  [ Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
20) Term era (Set (KeyHash 'StakePool))
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
    Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtMost Int
3) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) -- Small enough that its leaves some slack with poolHashUniv
  , Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
5 Int
6) (Term era (Map (KeyHash 'StakePool) EpochNo)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) EpochNo)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) EpochNo)
retiring) -- Small enough that its leaves some slack with poolHashUniv
  , Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
9) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState 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
  , (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , (Term era (Map (KeyHash 'StakePool) Coin)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits) Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (Term era (Map (KeyHash 'StakePool) Coin)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits)
  , (Term era (Map (KeyHash 'StakePool) EpochNo)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) EpochNo)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) EpochNo)
retiring) Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools)
  , (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) (Term era (Map (KeyHash 'StakePool) EpochNo)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) EpochNo)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) EpochNo)
retiring)
  ]

test8 :: Gen Property
test8 :: Gen Property
test8 =
  Proof AlonzoEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AlonzoEra]
-> Assembler AlonzoEra
-> Gen Property
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 = True}) -- But neither works without the Sized constraints
    [Pred AlonzoEra]
forall era. EraCertState era => [Pred era]
pstateConstraints
    (RootTarget AlonzoEra (PState AlonzoEra) (PState AlonzoEra)
-> Assembler AlonzoEra
forall t era x. PrettyA t => RootTarget era x t -> Assembler era
Assemble RootTarget AlonzoEra (PState AlonzoEra) (PState AlonzoEra)
forall era.
EraCertState 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 =
  [ Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
totalAda
  , Term era Coin
forall era. Era era => Term era Coin
fees Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
400))
  , Term era Coin
forall era. Era era => Term era Coin
deposits Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
200))
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
totalAda OrdCond
LTE [Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
fees, Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
deposits, Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
utxoAmt]
  , Direct (Ratio Integer)
-> Term era (Ratio Integer)
-> OrdCond
-> [Sum era (Ratio Integer)]
-> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Ratio Integer -> Direct (Ratio Integer)
forall a b. b -> Either a b
Right (Integer
1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (Rep era (Ratio Integer)
-> Ratio Integer -> Term era (Ratio Integer)
forall era t. Rep era t -> t -> Term era t
Lit Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [Rep era (Ratio Integer)
-> Lens' IndividualPoolStake (Ratio Integer)
-> Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
-> Sum era (Ratio Integer)
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR (Ratio Integer -> f (Ratio Integer))
-> IndividualPoolStake -> f IndividualPoolStake
Lens' IndividualPoolStake (Ratio Integer)
individualPoolStakeL Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr]
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
utxoAmt OrdCond
GTH [Rep era Coin
-> Lens' (TxOutF era) Coin
-> Term era (Map TxIn (TxOutF era))
-> Sum era Coin
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era Coin
forall era. Rep era Coin
CoinR (Coin -> f Coin) -> TxOutF era -> f (TxOutF era)
forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
Lens' (TxOutF era) Coin
outputCoinL (Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
proof)]
  , Term era Size -> Term era (Map TxIn (TxOutF era)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) (Proof era -> Term era (Map TxIn (TxOutF era))
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.
  , Term era Size
-> Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
-> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr
  ]
  where
    utxoAmt :: Term era Coin
utxoAmt = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var ([Char] -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"utxoAmt" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No)

test9 :: Gen Property
test9 :: Gen Property
test9 = Proof AlonzoEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AlonzoEra]
-> Assembler AlonzoEra
-> Gen Property
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 (Proof AlonzoEra -> [Pred AlonzoEra]
forall era. Reflect era => Proof era -> [Pred era]
sumPreds Proof AlonzoEra
Alonzo) Assembler AlonzoEra
forall era. Assembler era
Skip

test10 :: Gen Property
test10 :: Gen Property
test10 =
  Proof MaryEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred MaryEra]
-> Assembler MaryEra
-> Gen Property
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
    [ Term MaryEra Coin -> Pred MaryEra
forall era t. Term era t -> Pred era
Random Term MaryEra Coin
x
    , Term MaryEra Size -> Term MaryEra Coin -> Pred MaryEra
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term MaryEra Size
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
    , Direct Coin
-> Term MaryEra Coin
-> OrdCond
-> [Sum MaryEra Coin]
-> Pred MaryEra
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumLTH OrdCond
LTH [Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    , Direct Coin
-> Term MaryEra Coin
-> OrdCond
-> [Sum MaryEra Coin]
-> Pred MaryEra
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumLTE OrdCond
LTE [Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    , Direct Coin
-> Term MaryEra Coin
-> OrdCond
-> [Sum MaryEra Coin]
-> Pred MaryEra
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumGTH OrdCond
GTH [Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    , Direct Coin
-> Term MaryEra Coin
-> OrdCond
-> [Sum MaryEra Coin]
-> Pred MaryEra
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumGTE OrdCond
GTE [Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    , Direct Coin
-> Term MaryEra Coin
-> OrdCond
-> [Sum MaryEra Coin]
-> Pred MaryEra
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term MaryEra Coin
tsumEQL OrdCond
EQL [Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
x, Term MaryEra Coin -> Sum MaryEra Coin
forall era c. Term era c -> Sum era c
One Term MaryEra Coin
y]
    ]
    Assembler MaryEra
forall era. Assembler era
Skip
  where
    x :: Term MaryEra Coin
x = V MaryEra Coin -> Term MaryEra Coin
forall era t. V era t -> Term era t
Var ([Char]
-> Rep MaryEra Coin -> Access MaryEra Any Coin -> V MaryEra Coin
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"x" Rep MaryEra Coin
forall era. Rep era Coin
rep Access MaryEra Any Coin
forall era s t. Access era s t
No)
    y :: Term MaryEra Coin
y = V MaryEra Coin -> Term MaryEra Coin
forall era t. V era t -> Term era t
Var ([Char]
-> Rep MaryEra Coin -> Access MaryEra Any Coin -> V MaryEra Coin
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"y" Rep MaryEra Coin
forall era. Rep era Coin
rep Access MaryEra Any Coin
forall era s t. Access era s t
No)
    tsumLTH :: Term MaryEra Coin
tsumLTH = V MaryEra Coin -> Term MaryEra Coin
forall era t. V era t -> Term era t
Var ([Char]
-> Rep MaryEra Coin -> Access MaryEra Any Coin -> V MaryEra Coin
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumLTH" Rep MaryEra Coin
forall era. Rep era Coin
rep Access MaryEra Any Coin
forall era s t. Access era s t
No)
    tsumLTE :: Term MaryEra Coin
tsumLTE = V MaryEra Coin -> Term MaryEra Coin
forall era t. V era t -> Term era t
Var ([Char]
-> Rep MaryEra Coin -> Access MaryEra Any Coin -> V MaryEra Coin
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumLTE" Rep MaryEra Coin
forall era. Rep era Coin
rep Access MaryEra Any Coin
forall era s t. Access era s t
No)
    tsumGTH :: Term MaryEra Coin
tsumGTH = V MaryEra Coin -> Term MaryEra Coin
forall era t. V era t -> Term era t
Var ([Char]
-> Rep MaryEra Coin -> Access MaryEra Any Coin -> V MaryEra Coin
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumGTH" Rep MaryEra Coin
forall era. Rep era Coin
rep Access MaryEra Any Coin
forall era s t. Access era s t
No)
    tsumGTE :: Term MaryEra Coin
tsumGTE = V MaryEra Coin -> Term MaryEra Coin
forall era t. V era t -> Term era t
Var ([Char]
-> Rep MaryEra Coin -> Access MaryEra Any Coin -> V MaryEra Coin
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumGTE" Rep MaryEra Coin
forall era. Rep era Coin
rep Access MaryEra Any Coin
forall era s t. Access era s t
No)
    tsumEQL :: Term MaryEra Coin
tsumEQL = V MaryEra Coin -> Term MaryEra Coin
forall era t. V era t -> Term era t
Var ([Char]
-> Rep MaryEra Coin -> Access MaryEra Any Coin -> V MaryEra Coin
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"tsumEQL" Rep MaryEra Coin
forall era. Rep era Coin
rep Access MaryEra Any Coin
forall era s t. Access era s t
No)
    rep :: Rep era Coin
rep = Rep era Coin
forall era. Rep era Coin
CoinR
    proof :: Proof MaryEra
proof = Proof MaryEra
Mary

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

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

test12 :: Gen Property
test12 :: Gen Property
test12 =
  Proof ShelleyEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred ShelleyEra]
-> Assembler ShelleyEra
-> Gen Property
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
    [ Term ShelleyEra (PParamsF ShelleyEra) -> Pred ShelleyEra
forall era t. Term era t -> Pred era
Random (Proof ShelleyEra -> Term ShelleyEra (PParamsF ShelleyEra)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof ShelleyEra
p)
    , Term ShelleyEra ProtVer -> Pred ShelleyEra
forall era t. Term era t -> Pred era
Random (Proof ShelleyEra -> Term ShelleyEra ProtVer
forall era. Era era => Proof era -> Term era ProtVer
prevProtVer Proof ShelleyEra
p)
    , (Proof ShelleyEra -> Term ShelleyEra ProtVer
forall era. Era era => Proof era -> Term era ProtVer
protVer Proof ShelleyEra
p) Term ShelleyEra ProtVer
-> Term ShelleyEra ProtVer -> Pred ShelleyEra
forall n era. Count n => Term era n -> Term era n -> Pred era
`CanFollow` (Proof ShelleyEra -> Term ShelleyEra ProtVer
forall era. Era era => Proof era -> Term era ProtVer
prevProtVer Proof ShelleyEra
p)
    , Direct (Term ShelleyEra (PParamsF ShelleyEra))
-> [AnyF ShelleyEra (PParamsF ShelleyEra)] -> Pred ShelleyEra
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (Term ShelleyEra (PParamsF ShelleyEra)
-> Direct (Term ShelleyEra (PParamsF ShelleyEra))
forall a b. b -> Either a b
Right (Proof ShelleyEra -> Term ShelleyEra (PParamsF ShelleyEra)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof ShelleyEra
p)) [Rep ShelleyEra (PParamsF ShelleyEra)
-> Term ShelleyEra ProtVer -> AnyF ShelleyEra (PParamsF ShelleyEra)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep ShelleyEra (PParamsF ShelleyEra)
pp (Proof ShelleyEra -> Term ShelleyEra ProtVer
forall era. Era era => Proof era -> Term era ProtVer
protVer Proof ShelleyEra
p)]
    , Direct (Term ShelleyEra (PParamsF ShelleyEra))
-> [AnyF ShelleyEra (PParamsF ShelleyEra)] -> Pred ShelleyEra
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (Term ShelleyEra (PParamsF ShelleyEra)
-> Direct (Term ShelleyEra (PParamsF ShelleyEra))
forall a b. b -> Either a b
Right (Proof ShelleyEra -> Term ShelleyEra (PParamsF ShelleyEra)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
prevPParams Proof ShelleyEra
p)) [Rep ShelleyEra (PParamsF ShelleyEra)
-> Term ShelleyEra ProtVer -> AnyF ShelleyEra (PParamsF ShelleyEra)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep ShelleyEra (PParamsF ShelleyEra)
pp (Proof ShelleyEra -> Term ShelleyEra ProtVer
forall era. Era era => Proof era -> Term era ProtVer
prevProtVer Proof ShelleyEra
p)]
    ]
    Assembler ShelleyEra
forall era. Assembler era
Skip
  where
    pp :: Rep ShelleyEra (PParamsF ShelleyEra)
pp = Proof ShelleyEra -> Rep ShelleyEra (PParamsF ShelleyEra)
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 =
  [ Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
minFeeA Proof era
proof)
  , Term era Size -> Pred era
forall era t. Term era t -> Pred era
Random Term era Size
size
  , Term era Size -> Term era (Set Int) -> Pred era
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
  , Term era Size -> Term era (Map Int Int) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
size Term era (Map Int Int)
mm
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
      (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
100))
      OrdCond
EQL
      [ Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
minFeeA Proof era
proof)
      , Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
minFeeB Proof era
proof)
      ]
  , Direct (Term era (PParamsF era))
-> [AnyF era (PParamsF era)] -> Pred era
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component (Term era (PParamsF era) -> Direct (Term era (PParamsF era))
forall a b. b -> Either a b
Right (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
proof)) [Rep era (PParamsF era) -> Term era Coin -> AnyF era (PParamsF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
minFeeA Proof era
proof), Rep era (PParamsF era) -> Term era Coin -> AnyF era (PParamsF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (Proof era -> Term era Coin
forall era. Era era => Proof era -> Term era Coin
minFeeB Proof era
proof)]
  ]
  where
    pp :: Rep era (PParamsF era)
pp = Proof era -> Rep era (PParamsF era)
forall era. Era era => Proof era -> Rep era (PParamsF era)
PParamsR Proof era
proof
    llx :: Term era (Set Int)
llx = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Set Int) -> Access era Any (Set Int) -> V era (Set Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"llx" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
forall era s t. Access era s t
No)
    size :: Term era Size
size = V era Size -> Term era Size
forall era t. V era t -> Term era t
Var ([Char] -> Rep era Size -> Access era Any Size -> V era Size
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"size" Rep era Size
forall era. Rep era Size
SizeR Access era Any Size
forall era s t. Access era s t
No)
    mm :: Term era (Map Int Int)
mm = V era (Map Int Int) -> Term era (Map Int Int)
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Map Int Int)
-> Access era Any (Map Int Int)
-> V era (Map Int Int)
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"mm" (Rep era Int -> Rep era Int -> Rep era (Map Int Int)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era Int
forall era. Rep era Int
IntR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Map Int Int)
forall era s t. Access era s t
No)

test13 :: Gen Property
test13 :: Gen Property
test13 =
  Proof ShelleyEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred ShelleyEra]
-> Assembler ShelleyEra
-> Gen Property
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
    (Proof ShelleyEra -> [Pred ShelleyEra]
forall era. EraGov era => Proof era -> [Pred era]
componentPreds Proof ShelleyEra
proof)
    Assembler ShelleyEra
forall era. Assembler era
Skip
  where
    proof :: Proof ShelleyEra
proof = Proof ShelleyEra
Shelley

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

test14 :: IO ()
test14 :: IO ()
test14 =
  Proof AllegraEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AllegraEra]
-> Assembler AllegraEra
-> IO ()
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
    [ Term AllegraEra Size
-> Term AllegraEra (Set (Credential 'Staking)) -> Pred AllegraEra
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term AllegraEra Size
forall era. Era era => Int -> Term era Size
ExactSize Int
6) Term AllegraEra (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
    , Term AllegraEra Size
-> Term AllegraEra (Map (Credential 'Staking) Coin)
-> Pred AllegraEra
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term AllegraEra Size
forall era. Era era => Int -> Term era Size
ExactSize Int
10) Term AllegraEra (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
    , Term AllegraEra (Map (Credential 'Staking) Coin)
-> Term AllegraEra (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term AllegraEra (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term AllegraEra (Set (Credential 'Staking))
-> Term AllegraEra (Set (Credential 'Staking)) -> Pred AllegraEra
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term AllegraEra (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
    ]
    Assembler AllegraEra
forall era. Assembler era
Skip

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

test15 :: Gen Property
test15 :: Gen Property
test15 =
  Proof AlonzoEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AlonzoEra]
-> Assembler AlonzoEra
-> Gen Property
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
    [ Term AlonzoEra Size -> Term AlonzoEra Natural -> Pred AlonzoEra
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term AlonzoEra Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) (Proof AlonzoEra -> Term AlonzoEra Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof AlonzoEra
proof)
    , Term AlonzoEra Size -> Term AlonzoEra Natural -> Pred AlonzoEra
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term AlonzoEra Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) (Proof AlonzoEra -> Term AlonzoEra Natural
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.
      Direct Natural
-> Term AlonzoEra Natural
-> OrdCond
-> [Sum AlonzoEra Natural]
-> Pred AlonzoEra
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Natural -> Direct Natural
forall a b. b -> Either a b
Right Natural
1) (Proof AlonzoEra -> Term AlonzoEra Natural
forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof AlonzoEra
proof) OrdCond
LTE [Term AlonzoEra Natural -> Sum AlonzoEra Natural
forall era c. Term era c -> Sum era c
One (Proof AlonzoEra -> Term AlonzoEra Natural
forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof AlonzoEra
proof), Term AlonzoEra Natural -> Sum AlonzoEra Natural
forall era c. Term era c -> Sum era c
One (Proof AlonzoEra -> Term AlonzoEra Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof AlonzoEra
proof)]
    , Direct (Term AlonzoEra (PParamsF AlonzoEra))
-> [AnyF AlonzoEra (PParamsF AlonzoEra)] -> Pred AlonzoEra
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component
        (Term AlonzoEra (PParamsF AlonzoEra)
-> Direct (Term AlonzoEra (PParamsF AlonzoEra))
forall a b. b -> Either a b
Right (Proof AlonzoEra -> Term AlonzoEra (PParamsF AlonzoEra)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof AlonzoEra
proof))
        [Rep AlonzoEra (PParamsF AlonzoEra)
-> Term AlonzoEra Natural -> AnyF AlonzoEra (PParamsF AlonzoEra)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep AlonzoEra (PParamsF AlonzoEra)
pp (Proof AlonzoEra -> Term AlonzoEra Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof AlonzoEra
proof), Rep AlonzoEra (PParamsF AlonzoEra)
-> Term AlonzoEra Natural -> AnyF AlonzoEra (PParamsF AlonzoEra)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep AlonzoEra (PParamsF AlonzoEra)
pp (Proof AlonzoEra -> Term AlonzoEra Natural
forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof AlonzoEra
proof), Rep AlonzoEra (PParamsF AlonzoEra)
-> Term AlonzoEra Natural -> AnyF AlonzoEra (PParamsF AlonzoEra)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep AlonzoEra (PParamsF AlonzoEra)
pp (Proof AlonzoEra -> Term AlonzoEra Natural
forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof AlonzoEra
proof)]
    ]
    Assembler AlonzoEra
forall era. Assembler era
Skip
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo
    pp :: Rep AlonzoEra (PParamsF AlonzoEra)
pp = Proof AlonzoEra -> Rep AlonzoEra (PParamsF AlonzoEra)
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 =
  [ Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
6) Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
3) (Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr) -- At least 1 but smaller than the poolHashUniv
  , Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Direct (Ratio Integer)
-> Term era (Ratio Integer)
-> OrdCond
-> [Sum era (Ratio Integer)]
-> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Ratio Integer -> Direct (Ratio Integer)
forall a b. b -> Either a b
Right (Integer
1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (Rep era (Ratio Integer)
-> Ratio Integer -> Term era (Ratio Integer)
forall era t. Rep era t -> t -> Term era t
Lit Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [Rep era (Ratio Integer)
-> Lens' IndividualPoolStake (Ratio Integer)
-> Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
-> Sum era (Ratio Integer)
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR (Ratio Integer -> f (Ratio Integer))
-> IndividualPoolStake -> f IndividualPoolStake
Lens' IndividualPoolStake (Ratio Integer)
individualPoolStakeL Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
poolDistr]
  , Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
4) (Term era (Map (KeyHash 'StakePool) (Ratio Integer))
-> Term era (Set (KeyHash 'StakePool))
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
  , Term era (Map (KeyHash 'StakePool) (Ratio Integer))
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) (Ratio Integer))
foox Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Direct (Ratio Integer)
-> Term era (Ratio Integer)
-> OrdCond
-> [Sum era (Ratio Integer)]
-> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Ratio Integer -> Direct (Ratio Integer)
forall a b. b -> Either a b
Right (Integer
1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (Rep era (Ratio Integer)
-> Ratio Integer -> Term era (Ratio Integer)
forall era t. Rep era t -> t -> Term era t
Lit Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [Term era (Map (KeyHash 'StakePool) (Ratio Integer))
-> Sum era (Ratio Integer)
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 = V era (Map (KeyHash 'StakePool) (Ratio Integer))
-> Term era (Map (KeyHash 'StakePool) (Ratio Integer))
forall era t. V era t -> Term era t
Var ([Char]
-> Rep era (Map (KeyHash 'StakePool) (Ratio Integer))
-> Access era Any (Map (KeyHash 'StakePool) (Ratio Integer))
-> V era (Map (KeyHash 'StakePool) (Ratio Integer))
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"foo" (Rep era (KeyHash 'StakePool)
-> Rep era (Ratio Integer)
-> Rep era (Map (KeyHash 'StakePool) (Ratio Integer))
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era (KeyHash 'StakePool)
forall era. Era era => Rep era (KeyHash 'StakePool)
PoolHashR Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR) Access era Any (Map (KeyHash 'StakePool) (Ratio Integer))
forall era s t. Access era s t
No)

test16 :: Gen Property
test16 :: Gen Property
test16 =
  Proof AlonzoEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AlonzoEra]
-> Assembler AlonzoEra
-> Gen Property
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
    (Proof AlonzoEra -> [Pred AlonzoEra]
forall era. Era era => Proof era -> [Pred era]
preds16 Proof AlonzoEra
proof)
    Assembler AlonzoEra
forall era. Assembler era
Skip
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo

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

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

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

dstatePreds :: EraCertState era => Proof era -> [Pred era]
dstatePreds :: forall era. EraCertState era => Proof era -> [Pred era]
dstatePreds Proof era
_p =
  [ Term era Size
-> Term era (Map (Credential 'Staking) Coin) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtMost Int
8) Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards -- Small enough that its leaves some slack with credUniv
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
  , Term era (Map (Credential 'Staking) DRep) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'Staking) DRep)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) DRep)
drepDelegation
  , -- TODO: these are Conway related
    -- , Random currentDRepState
    -- , Random committeeState
    -- , Random numDormantEpochs
    Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map Ptr (Credential 'Staking))
-> Term era (Set (Credential 'Staking))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map Ptr (Credential 'Staking))
forall era.
EraCertState 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)

    Term era Size -> Term era Coin -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) Term era Coin
forall era. Era era => Term era Coin
treasury
  , Term era (Map (Credential 'Staking) Coin) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanTreasury
  , Term era Size
-> Term era (Map (Credential 'Staking) Coin) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanReserves
  , Term era DeltaCoin -> Term era DeltaCoin
forall era. Term era DeltaCoin -> Term era DeltaCoin
Negate (Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaReserves) Term era DeltaCoin -> Term era DeltaCoin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaTreasury
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
instanReservesSum OrdCond
EQL [Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanReserves]
  , Direct DeltaCoin
-> Term era DeltaCoin -> OrdCond -> [Sum era DeltaCoin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (DeltaCoin -> Direct DeltaCoin
forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
forall era. Era era => Term era Coin
instanReservesSum) OrdCond
LTH [Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
forall era. Era era => Term era Coin
reserves), Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaReserves]
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
instanTreasurySum OrdCond
EQL [Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanTreasury]
  , Direct DeltaCoin
-> Term era DeltaCoin -> OrdCond -> [Sum era DeltaCoin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (DeltaCoin -> Direct DeltaCoin
forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
forall era. Era era => Term era Coin
instanTreasurySum) OrdCond
LTH [Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
forall era. Era era => Term era Coin
treasury), Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaTreasury]
  , -- , Before reserves deltaReserves -- XXX
    -- , Before treasury deltaTreasury -- XXX
    Lens' FutureGenDeleg (KeyHash 'Genesis)
-> Rep era (KeyHash 'Genesis)
-> Term era (Set FutureGenDeleg)
-> Term era (Set (KeyHash 'Genesis))
forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS (KeyHash 'Genesis -> f (KeyHash 'Genesis))
-> FutureGenDeleg -> f FutureGenDeleg
Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL Rep era (KeyHash 'Genesis)
forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR (Term era (Map FutureGenDeleg GenDelegPair)
-> Term era (Set FutureGenDeleg)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map FutureGenDeleg GenDelegPair)
forall era.
EraCertState era =>
Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs) Term era (Set (KeyHash 'Genesis))
-> Term era (Set (KeyHash 'Genesis)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> Term era (Set (KeyHash 'Genesis))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState 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 =
  [ Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
utxoCoin OrdCond
EQL [Rep era Coin
-> Lens' (TxOutF era) Coin
-> Term era (Map TxIn (TxOutF era))
-> Sum era Coin
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era Coin
forall era. Rep era Coin
CoinR (Coin -> f Coin) -> TxOutF era -> f (TxOutF era)
forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
Lens' (TxOutF era) Coin
outputCoinL (Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
proof)]
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
deposits OrdCond
EQL [Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits, Term era (Map (KeyHash 'StakePool) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits]
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
      Term era Coin
forall era. Era era => Term era Coin
totalAda
      OrdCond
EQL
      [Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
utxoCoin, Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
treasury, Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
reserves, Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
fees, Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
forall era. Era era => Term era Coin
deposits, Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards]
  , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
fees
  , Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era)) -> Pred era
forall era t. Term era t -> Pred era
Random (Proof era -> Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era))
forall era.
Era era =>
Proof era -> Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era))
pparamProposals Proof era
proof)
  , Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era)) -> Pred era
forall era t. Term era t -> Pred era
Random (Proof era -> Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era))
forall era.
Era era =>
Proof era -> Term era (Map (KeyHash 'Genesis) (PParamsUpdateF era))
futurePParamProposals Proof era
proof)
  , Term era (FuturePParams era) -> Pred era
forall era t. Term era t -> Pred era
Random (Proof era -> Term era (FuturePParams era)
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 =
  [ Term era (Map (Credential 'Staking) Coin) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
markStake
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
markDelegs
  , Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
markPools
  , Term era (Map (Credential 'Staking) Coin) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
setStake
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
setDelegs
  , Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
setPools
  , Term era (Map (Credential 'Staking) Coin) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
goStake
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
goDelegs
  , Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
goPools
  , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
snapShotFee
  , Term era (PParamsF era) -> Pred era
forall era t. Term era t -> Pred era
Random (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
prevPParams Proof era
proof)
  , Term era (PParamsF era) -> Pred era
forall era t. Term era t -> Pred era
Random (Proof era -> Term era (PParamsF era)
forall era. Era era => Proof era -> Term era (PParamsF era)
currPParams Proof era
proof)
  , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
donation
  , Term era Size -> Term era Natural -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
proof)
  , Term era Size -> Term era Natural -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
proof)
  , -- , Random (maxBBSize proof) -- This will cause underflow on Natural
    Direct (Ratio Integer)
-> Term era (Ratio Integer)
-> OrdCond
-> [Sum era (Ratio Integer)]
-> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (Ratio Integer -> Direct (Ratio Integer)
forall a b. b -> Either a b
Right (Integer
1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
1000))
      (Rep era (Ratio Integer)
-> Ratio Integer -> Term era (Ratio Integer)
forall era t. Rep era t -> t -> Term era t
Lit Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1)
      OrdCond
EQL
      [Rep era (Ratio Integer)
-> Lens' IndividualPoolStake (Ratio Integer)
-> Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
-> Sum era (Ratio Integer)
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR (Ratio Integer -> f (Ratio Integer))
-> IndividualPoolStake -> f IndividualPoolStake
Lens' IndividualPoolStake (Ratio Integer)
individualPoolStakeL Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
markPoolDistr]
  , Direct Natural
-> Term era Natural -> OrdCond -> [Sum era Natural] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Natural -> Direct Natural
forall a b. b -> Either a b
Right Natural
1) (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof era
proof) OrdCond
LTE [Term era Natural -> Sum era Natural
forall era c. Term era c -> Sum era c
One (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
proof), Term era Natural -> Sum era Natural
forall era c. Term era c -> Sum era c
One (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
proof)]
  , Direct (Term era (PParamsF era))
-> [AnyF era (PParamsF era)] -> Pred era
forall era t. Direct (Term era t) -> [AnyF era t] -> Pred era
Component
      (Term era (PParamsF era) -> Direct (Term era (PParamsF era))
forall a b. b -> Either a b
Right (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
proof))
      [Rep era (PParamsF era)
-> Term era Natural -> AnyF era (PParamsF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxTxSize Proof era
proof), Rep era (PParamsF era)
-> Term era Natural -> AnyF era (PParamsF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBHSize Proof era
proof), Rep era (PParamsF era)
-> Term era Natural -> AnyF era (PParamsF era)
forall era s t. Era era => Rep era s -> Term era t -> AnyF era s
field Rep era (PParamsF era)
pp (Proof era -> Term era Natural
forall era. Era era => Proof era -> Term era Natural
maxBBSize Proof era
proof)]
  ]
  where
    pp :: Rep era (PParamsF era)
pp = Proof era -> Rep era (PParamsF era)
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 =
  [ Term era EpochNo -> Pred era
forall era t. Term era t -> Pred era
Random Term era EpochNo
forall era. Era era => Term era EpochNo
currentEpoch
  , Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
8) (Term era (Map (KeyHash 'StakePool) Natural)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Natural)
forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
prevBlocksMade) -- Both prevBlocksMade and prevBlocksMadeDom will have size 8
  , Term era Size -> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
8) (Term era (Map (KeyHash 'StakePool) Natural)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Natural)
forall era. Era era => Term era (Map (KeyHash 'StakePool) Natural)
currBlocksMade)
  , Direct (Ratio Integer)
-> Term era (Ratio Integer)
-> OrdCond
-> [Sum era (Ratio Integer)]
-> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Ratio Integer -> Direct (Ratio Integer)
forall a b. b -> Either a b
Right (Integer
1 Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
1000)) (Rep era (Ratio Integer)
-> Ratio Integer -> Term era (Ratio Integer)
forall era t. Rep era t -> t -> Term era t
Lit Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR Ratio Integer
1) OrdCond
EQL [Rep era (Ratio Integer)
-> Lens' IndividualPoolStake (Ratio Integer)
-> Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
-> Sum era (Ratio Integer)
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era (Ratio Integer)
forall era. Rep era (Ratio Integer)
RationalR (Ratio Integer -> f (Ratio Integer))
-> IndividualPoolStake -> f IndividualPoolStake
Lens' IndividualPoolStake (Ratio Integer)
individualPoolStakeL Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
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 =
  Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
univPreds Proof era
pr
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
pstatePreds Proof era
pr
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
dstatePreds Proof era
pr
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. Reflect era => Proof era -> [Pred era]
utxostatePreds Proof era
pr
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. Proof era -> [Pred era]
accountstatePreds Proof era
pr
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. EraGov era => Proof era -> [Pred era]
epochstatePreds Proof era
pr
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. Era era => Proof era -> [Pred era]
newepochstatePreds Proof era
pr

test17 :: Gen Property
test17 :: Gen Property
test17 =
  Proof AlonzoEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AlonzoEra]
-> Assembler AlonzoEra
-> Gen Property
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 = False})
    (Proof AlonzoEra -> [Pred AlonzoEra]
forall era. Reflect era => Proof era -> [Pred era]
newepochConstraints Proof AlonzoEra
proof)
    (RootTarget
  AlonzoEra (NewEpochState AlonzoEra) (NewEpochState AlonzoEra)
-> Assembler AlonzoEra
forall t era x. PrettyA t => RootTarget era x t -> Assembler era
Assemble (Proof AlonzoEra
-> RootTarget
     AlonzoEra (NewEpochState AlonzoEra) (NewEpochState AlonzoEra)
forall era.
Reflect 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 :: EraCertState era => Proof era -> [Pred era]
projPreds1 :: forall era. EraCertState era => Proof era -> [Pred era]
projPreds1 Proof era
_proof =
  [ Term era Size
-> Term era (Map FutureGenDeleg GenDelegPair) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
4) Term era (Map FutureGenDeleg GenDelegPair)
forall era.
EraCertState era =>
Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs
  , Lens' FutureGenDeleg (KeyHash 'Genesis)
-> Rep era (KeyHash 'Genesis)
-> Term era (Set FutureGenDeleg)
-> Term era (Set (KeyHash 'Genesis))
forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS (KeyHash 'Genesis -> f (KeyHash 'Genesis))
-> FutureGenDeleg -> f FutureGenDeleg
Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL Rep era (KeyHash 'Genesis)
forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR (Term era (Map FutureGenDeleg GenDelegPair)
-> Term era (Set FutureGenDeleg)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map FutureGenDeleg GenDelegPair)
forall era.
EraCertState era =>
Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs) Term era (Set (KeyHash 'Genesis))
-> Term era (Set (KeyHash 'Genesis)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> Term era (Set (KeyHash 'Genesis))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  ]

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

test18a :: Gen Property
test18a :: Gen Property
test18a = Proof AlonzoEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AlonzoEra]
-> Assembler AlonzoEra
-> Gen Property
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 (Proof AlonzoEra -> [Pred AlonzoEra]
forall era. EraCertState era => Proof era -> [Pred era]
projPreds1 Proof AlonzoEra
proof) Assembler AlonzoEra
forall era. Assembler era
Skip
  where
    proof :: Proof AlonzoEra
proof = Proof AlonzoEra
Alonzo

test18b :: Gen Property
test18b :: Gen Property
test18b =
  Proof AlonzoEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AlonzoEra]
-> Assembler AlonzoEra
-> Gen Property
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
    (Proof AlonzoEra -> [Pred AlonzoEra]
forall era. EraCertState era => Proof era -> [Pred era]
projPreds2 Proof AlonzoEra
proof)
    (RootTarget
  AlonzoEra
  Void
  (Map FutureGenDeleg GenDelegPair,
   Map (KeyHash 'Genesis) GenDelegPair)
-> Assembler AlonzoEra
forall t era x. PrettyA t => RootTarget era x t -> Assembler era
Assemble ([Char]
-> (Map FutureGenDeleg GenDelegPair
    -> Map (KeyHash 'Genesis) GenDelegPair
    -> (Map FutureGenDeleg GenDelegPair,
        Map (KeyHash 'Genesis) GenDelegPair))
-> RootTarget
     AlonzoEra
     Void
     (Map FutureGenDeleg GenDelegPair
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> (Map FutureGenDeleg GenDelegPair,
          Map (KeyHash 'Genesis) GenDelegPair))
forall a b era. [Char] -> (a -> b) -> RootTarget era Void (a -> b)
Constr [Char]
"Pair" (,) RootTarget
  AlonzoEra
  Void
  (Map FutureGenDeleg GenDelegPair
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> (Map FutureGenDeleg GenDelegPair,
       Map (KeyHash 'Genesis) GenDelegPair))
-> Term AlonzoEra (Map FutureGenDeleg GenDelegPair)
-> Target
     AlonzoEra
     (Map (KeyHash 'Genesis) GenDelegPair
      -> (Map FutureGenDeleg GenDelegPair,
          Map (KeyHash 'Genesis) GenDelegPair))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term AlonzoEra (Map FutureGenDeleg GenDelegPair)
forall era.
EraCertState era =>
Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs Target
  AlonzoEra
  (Map (KeyHash 'Genesis) GenDelegPair
   -> (Map FutureGenDeleg GenDelegPair,
       Map (KeyHash 'Genesis) GenDelegPair))
-> Term AlonzoEra (Map (KeyHash 'Genesis) GenDelegPair)
-> RootTarget
     AlonzoEra
     Void
     (Map FutureGenDeleg GenDelegPair,
      Map (KeyHash 'Genesis) GenDelegPair)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term AlonzoEra (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState 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 (Rep era (KeyHash 'Genesis) -> Rep era (Set (KeyHash 'Genesis))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era (KeyHash 'Genesis)
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 ((KeyHash 'Genesis -> f (KeyHash 'Genesis))
-> FutureGenDeleg -> f FutureGenDeleg
Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL) Rep era FutureGenDeleg
forall era. Era era => Rep era FutureGenDeleg
FutureGenDelegR Rep era GenDelegPair
forall era. Era era => Rep era GenDelegPair
GenDelegPairR
  Map FutureGenDeleg GenDelegPair
-> Gen (Map FutureGenDeleg GenDelegPair)
forall a. a -> Gen a
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 <- Gen (Map FutureGenDeleg GenDelegPair)
-> IO (Map FutureGenDeleg GenDelegPair)
forall a. Gen a -> IO a
generate (Proof MaryEra -> Gen (Map FutureGenDeleg GenDelegPair)
forall era.
Era era =>
Proof era -> Gen (Map FutureGenDeleg GenDelegPair)
help19 Proof MaryEra
Mary)
  [Char] -> IO ()
putStrLn (Rep BabbageEra (Map FutureGenDeleg GenDelegPair)
-> Map FutureGenDeleg GenDelegPair -> [Char]
forall e t. Rep e t -> t -> [Char]
synopsis (Rep BabbageEra FutureGenDeleg
-> Rep BabbageEra GenDelegPair
-> Rep BabbageEra (Map FutureGenDeleg GenDelegPair)
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) Rep BabbageEra GenDelegPair
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 =
  [ Term era Size -> Term era (Set Int) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
10) Term era (Set Int)
intUniv
  , Term era Size -> Term era (Map Int Word64) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtMost Int
6) Term era (Map Int Word64)
rewardsx
  , Term era (Map Int Word64) -> Term era (Set Int)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map Int Word64)
rewardsx Term era (Set Int) -> Term era (Set Int) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set Int)
intUniv
  , Term era (Map Int Word64) -> Term era (Set Int)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map Int Word64)
rewardsx Term era (Set Int) -> Term era (Set Int) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map Ptr Int) -> Term era (Set Int)
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 = V era (Map Int Word64) -> Term era (Map Int Word64)
forall era t. V era t -> Term era t
Var (Proof era
-> [Char]
-> Rep era (Map Int Word64)
-> Access era Any (Map Int Word64)
-> V era (Map Int Word64)
forall era t s.
Proof era -> [Char] -> Rep era t -> Access era s t -> V era t
pV Proof era
proof [Char]
"rewards" (Rep era Int -> Rep era Word64 -> Rep era (Map Int Word64)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era Int
forall era. Rep era Int
IntR Rep era Word64
forall era. Rep era Word64
Word64R) Access era Any (Map Int Word64)
forall era s t. Access era s t
No)
    ptrsx :: Term era (Map Ptr Int)
ptrsx = V era (Map Ptr Int) -> Term era (Map Ptr Int)
forall era t. V era t -> Term era t
Var (Proof era
-> [Char]
-> Rep era (Map Ptr Int)
-> Access era Any (Map Ptr Int)
-> V era (Map Ptr Int)
forall era t s.
Proof era -> [Char] -> Rep era t -> Access era s t -> V era t
pV Proof era
proof [Char]
"ptrs" (Rep era Ptr -> Rep era Int -> Rep era (Map Ptr Int)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era Ptr
forall era. Rep era Ptr
PtrR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Map Ptr Int)
forall era s t. Access era s t
No)
    intUniv :: Term era (Set Int)
intUniv = V era (Set Int) -> Term era (Set Int)
forall era t. V era t -> Term era t
Var (Proof era
-> [Char]
-> Rep era (Set Int)
-> Access era Any (Set Int)
-> V era (Set Int)
forall era t s.
Proof era -> [Char] -> Rep era t -> Access era s t -> V era t
pV Proof era
proof [Char]
"intUniv" (Rep era Int -> Rep era (Set Int)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Int
forall era. Rep era Int
IntR) Access era Any (Set Int)
forall era s t. Access era s t
No)

test20 :: Gen Property
test20 :: Gen Property
test20 =
  Proof AlonzoEra
-> [Char]
-> Bool
-> OrderInfo
-> [Pred AlonzoEra]
-> Assembler AlonzoEra
-> Gen Property
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
    (Proof AlonzoEra -> [Pred AlonzoEra]
forall era. Era era => Proof era -> [Pred era]
preds20 Proof AlonzoEra
proof)
    Assembler AlonzoEra
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 = V BabbageEra [Int] -> Term BabbageEra [Int]
forall era t. V era t -> Term era t
Var ([Char]
-> Rep BabbageEra [Int]
-> Access BabbageEra Any [Int]
-> V BabbageEra [Int]
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"w" (Rep BabbageEra Int -> Rep BabbageEra [Int]
forall era a. Rep era a -> Rep era [a]
ListR Rep BabbageEra Int
forall era. Rep era Int
IntR) Access BabbageEra Any [Int]
forall era s t. Access era s t
No)
      a :: Term BabbageEra Int
a = V BabbageEra Int -> Term BabbageEra Int
forall era t. V era t -> Term era t
Var ([Char]
-> Rep BabbageEra Int
-> Access BabbageEra Any Int
-> V BabbageEra Int
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"a" Rep BabbageEra Int
forall era. Rep era Int
IntR Access BabbageEra Any Int
forall era s t. Access era s t
No)
      b :: Term BabbageEra Int
b = V BabbageEra Int -> Term BabbageEra Int
forall era t. V era t -> Term era t
Var ([Char]
-> Rep BabbageEra Int
-> Access BabbageEra Any Int
-> V BabbageEra Int
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"b" Rep BabbageEra Int
forall era. Rep era Int
IntR Access BabbageEra Any Int
forall era s t. Access era s t
No)
      c :: Term BabbageEra Int
c = V BabbageEra Int -> Term BabbageEra Int
forall era t. V era t -> Term era t
Var ([Char]
-> Rep BabbageEra Int
-> Access BabbageEra Any Int
-> V BabbageEra Int
forall era t s.
Era era =>
[Char] -> Rep era t -> Access era s t -> V era t
V [Char]
"c" Rep BabbageEra Int
forall era. Rep era Int
IntR Access BabbageEra Any Int
forall era s t. Access era s t
No)
      pred21 :: Pred BabbageEra
pred21 =
        Term BabbageEra [Int]
-> [(Int, RootTarget BabbageEra [Int] [Int], [Pred BabbageEra])]
-> Pred BabbageEra
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
            , [Char]
-> TypeRep [Int]
-> (Int -> Int -> Int -> [Int])
-> RootTarget BabbageEra [Int] (Int -> Int -> Int -> [Int])
forall root a b era.
[Char] -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert [Char]
"three" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[Int]) (\Int
x Int
y Int
z -> [Int
x, Int
y, Int
z])
                RootTarget BabbageEra [Int] (Int -> Int -> Int -> [Int])
-> RootTarget BabbageEra [Int] Int
-> RootTarget BabbageEra [Int] (Int -> Int -> [Int])
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term BabbageEra Int
-> ([Int] -> Maybe Int) -> RootTarget BabbageEra [Int] Int
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
a (\case [Int
x, Int
_, Int
_] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
x; [Int]
_ -> Maybe Int
forall a. Maybe a
Nothing)
                RootTarget BabbageEra [Int] (Int -> Int -> [Int])
-> RootTarget BabbageEra [Int] Int
-> RootTarget BabbageEra [Int] (Int -> [Int])
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term BabbageEra Int
-> ([Int] -> Maybe Int) -> RootTarget BabbageEra [Int] Int
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
b (\case [Int
_, Int
y, Int
_] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
y; [Int]
_ -> Maybe Int
forall a. Maybe a
Nothing)
                RootTarget BabbageEra [Int] (Int -> [Int])
-> RootTarget BabbageEra [Int] Int
-> RootTarget BabbageEra [Int] [Int]
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term BabbageEra Int
-> ([Int] -> Maybe Int) -> RootTarget BabbageEra [Int] Int
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
c (\case [Int
_, Int
_, Int
z] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
z; [Int]
_ -> Maybe Int
forall a. Maybe a
Nothing)
            , [Term BabbageEra Int -> Pred BabbageEra
forall era t. Term era t -> Pred era
Random Term BabbageEra Int
a, Term BabbageEra Int -> Pred BabbageEra
forall era t. Term era t -> Pred era
Random Term BabbageEra Int
b, Term BabbageEra Int -> Pred BabbageEra
forall era t. Term era t -> Pred era
Random Term BabbageEra Int
c]
            )
          ,
            ( Int
1
            , [Char]
-> TypeRep [Int]
-> (Int -> Int -> [Int])
-> RootTarget BabbageEra [Int] (Int -> Int -> [Int])
forall root a b era.
[Char] -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert [Char]
"two" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[Int]) (\Int
x Int
y -> [Int
x, Int
y])
                RootTarget BabbageEra [Int] (Int -> Int -> [Int])
-> RootTarget BabbageEra [Int] Int
-> RootTarget BabbageEra [Int] (Int -> [Int])
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term BabbageEra Int
-> ([Int] -> Maybe Int) -> RootTarget BabbageEra [Int] Int
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
a (\case [Int
x, Int
_] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
x; [Int]
_ -> Maybe Int
forall a. Maybe a
Nothing)
                RootTarget BabbageEra [Int] (Int -> [Int])
-> RootTarget BabbageEra [Int] Int
-> RootTarget BabbageEra [Int] [Int]
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term BabbageEra Int
-> ([Int] -> Maybe Int) -> RootTarget BabbageEra [Int] Int
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
b (\case [Int
_, Int
y] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
y; [Int]
_ -> Maybe Int
forall a. Maybe a
Nothing)
            , [Term BabbageEra Int -> Pred BabbageEra
forall era t. Term era t -> Pred era
Random Term BabbageEra Int
a, Term BabbageEra Int -> Pred BabbageEra
forall era t. Term era t -> Pred era
Random Term BabbageEra Int
b]
            )
          ,
            ( Int
1
            , [Char]
-> TypeRep [Int]
-> (Int -> [Int])
-> RootTarget BabbageEra [Int] (Int -> [Int])
forall root a b era.
[Char] -> TypeRep root -> (a -> b) -> RootTarget era root (a -> b)
Invert [Char]
"one" (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @[Int]) (\Int
x -> [Int
x])
                RootTarget BabbageEra [Int] (Int -> [Int])
-> RootTarget BabbageEra [Int] Int
-> RootTarget BabbageEra [Int] [Int]
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ Term BabbageEra Int
-> ([Int] -> Maybe Int) -> RootTarget BabbageEra [Int] Int
forall era t root.
Term era t -> (root -> Maybe t) -> RootTarget era root t
Partial Term BabbageEra Int
a (\case [Int
x] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
x; [Int]
_ -> Maybe Int
forall a. Maybe a
Nothing)
            , [Term BabbageEra Int -> Pred BabbageEra
forall era t. Term era t -> Pred era
Random Term BabbageEra Int
a]
            )
          ]
  Env BabbageEra
env <-
    Int -> Gen (Env BabbageEra) -> IO (Env BabbageEra)
forall a. Int -> Gen a -> IO a
generateWithSeed
      Int
seed
      ( Subst BabbageEra -> Gen (Subst BabbageEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst BabbageEra
forall era. Subst era
emptySubst
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof BabbageEra
-> OrderInfo
-> [Pred BabbageEra]
-> Subst BabbageEra
-> Gen (Subst BabbageEra)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof BabbageEra
proof OrderInfo
standardOrderInfo [Pred BabbageEra
pred21]
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Env BabbageEra))
-> Gen (Env BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst BabbageEra
subst -> Typed (Env BabbageEra) -> Gen (Env BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Subst BabbageEra -> Env BabbageEra -> Typed (Env BabbageEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst BabbageEra
subst Env BabbageEra
forall era. Env era
emptyEnv))
      )
  Env BabbageEra -> IO ()
forall a. Show a => a -> IO ()
print Env BabbageEra
env
  Typed Bool -> IO Bool
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed Bool -> IO Bool) -> Typed Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ Env BabbageEra -> Pred BabbageEra -> Typed Bool
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" (IO () -> TestTree) -> IO () -> TestTree
forall a b. (a -> b) -> a -> b
$
        case Typed (DependGraph BabbageEra)
-> Either [[Char]] (DependGraph BabbageEra)
forall x. Typed x -> Either [[Char]] x
runTyped (forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile @BabbageEra OrderInfo
standardOrderInfo [Pred BabbageEra]
forall era. Era era => [Pred era]
cyclicPred) of
          Right DependGraph BabbageEra
_ -> [Char] -> IO ()
forall a. HasCallStack => [Char] -> IO a
assertFailure ([Char]
"Cyclic preds Not detected.")
          Left [[Char]]
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    , [Char] -> IO () -> TestTree
testCase [Char]
"test 1B. ACyclic preds solved" (IO () -> TestTree) -> IO () -> TestTree
forall a b. (a -> b) -> a -> b
$
        case Typed (DependGraph BabbageEra)
-> Either [[Char]] (DependGraph BabbageEra)
forall x. Typed x -> Either [[Char]] x
runTyped (forall era.
Era era =>
OrderInfo -> [Pred era] -> Typed (DependGraph era)
compile @BabbageEra OrderInfo
standardOrderInfo [Pred BabbageEra]
forall era. Era era => [Pred era]
aCyclicPred) of
          Right DependGraph BabbageEra
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Left [[Char]]
xs -> [Char] -> IO ()
forall a. HasCallStack => [Char] -> IO a
assertFailure ([[Char]] -> [Char]
unlines [[Char]]
xs)
    , [Char] -> IO (Map FutureGenDeleg GenDelegPair) -> TestTree
forall a. [Char] -> IO a -> TestTree
testIO
        [Char]
"test 19 Test of projOnDom function"
        (Gen (Map FutureGenDeleg GenDelegPair)
-> IO (Map FutureGenDeleg GenDelegPair)
forall a. Gen a -> IO a
generate (Proof MaryEra -> Gen (Map FutureGenDeleg GenDelegPair)
forall era.
Era era =>
Proof era -> Gen (Map FutureGenDeleg GenDelegPair)
help19 Proof MaryEra
Mary))
    , [Char] -> IO () -> TestTree
forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test 4. Inconsistent Size" IO ()
test4
    , [Char] -> IO () -> TestTree
forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test 5. Bad Sum, impossible partition." IO ()
test5
    , [Char] -> IO () -> TestTree
forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test6. Find a viable order of variables" (Bool -> IO ()
test6 Bool
False)
    , [Char] -> IO () -> TestTree
forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test7. Compute a solution" (Bool -> IO ()
test7 Bool
False)
    , [Char] -> IO () -> TestTree
forall a. [Char] -> IO a -> TestTree
testIO [Char]
"Test 14 Catch unsolveable use of Sized" IO ()
test14
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 3. PState example" Gen Property
test3
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 8. Pstate constraints" Gen Property
test8
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 9. Test of summing" Gen Property
test9
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 10. Test conditions EQL LTH LTE GTH GTE" Gen Property
test10
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
100 [Char]
"Test 11. Instanaeous Sum Tests" Gen Property
test11
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 12. CanFollow tests" Gen Property
test12
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 13. Component tests" Gen Property
test13
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 15. Summation on Natural" Gen Property
test15
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 16. Test NonEmpty subset" Gen Property
test16
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 17. Full NewEpochState" ((Property -> Property) -> Gen Property -> Gen Property
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30) Gen Property
test17)
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 18a. Projection test" Gen Property
test18a
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 18b. Projection test" Gen Property
test18b
    , Int -> [Char] -> Gen Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Test 20. ptr & rewards are inverses" Gen Property
test20
    , Int -> [Char] -> Property -> TestTree
forall prop. Testable prop => Int -> [Char] -> prop -> TestTree
testPropMax Int
30 [Char]
"Constraint soundness" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> (OrderInfo -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
within Int
1000000 ((OrderInfo -> Property) -> Property)
-> (OrderInfo -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ OrderInfo -> Property
prop_soundness
    , [Char] -> Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"Shrinking soundness" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> (OrderInfo -> Property) -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 ((OrderInfo -> Property) -> Property)
-> (OrderInfo -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ OrderInfo -> Property
prop_shrinking
    , [Char] -> Gen Bool -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
"NewEpochState and Tx generation" (Gen Bool -> TestTree) -> Gen Bool -> TestTree
forall a b. (a -> b) -> a -> b
$ do
        (NewEpochState ConwayEra
st, AlonzoTx ConwayEra
tx, Env ConwayEra
_) <- UnivSize
-> Proof ConwayEra
-> Gen (NewEpochState ConwayEra, Tx ConwayEra, Env ConwayEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (NewEpochState era, Tx era, Env era)
genTxAndNewEpoch UnivSize
forall a. Default a => a
def (Proof ConwayEra
 -> Gen (NewEpochState ConwayEra, Tx ConwayEra, Env ConwayEra))
-> Proof ConwayEra
-> Gen (NewEpochState ConwayEra, Tx ConwayEra, Env ConwayEra)
forall a b. (a -> b) -> a -> b
$ Proof ConwayEra
Conway
        (NewEpochState ConwayEra
st, AlonzoTx ConwayEra
tx) (NewEpochState ConwayEra, AlonzoTx ConwayEra)
-> Gen Bool -> Gen Bool
forall a b. NFData a => a -> b -> b
`deepseq` Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    , [Char] -> Proof ConwayEra -> [Pred ConwayEra] -> TestTree
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, Typed Bool -> Bool
forall t. HasCallStack => Typed t -> t
errorTyped (Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
p))
  Env era
env <-
    Gen (Env era) -> IO (Env era)
forall a. Gen a -> IO a
generate
      ( Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo [Pred era]
preds
          Gen (Subst era) -> (Subst era -> Gen (Env era)) -> Gen (Env era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv)
      )
  let pairs :: [(Pred era, Bool)]
pairs = (Pred era -> (Pred era, Bool)) -> [Pred era] -> [(Pred era, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (Env era -> Pred era -> (Pred era, Bool)
forall {era}. Env era -> Pred era -> (Pred era, Bool)
tryPred Env era
env) [Pred era]
preds
  ((Pred era, Bool) -> IO ()) -> [(Pred era, Bool)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Pred era
p, Bool
b) -> [Char] -> IO ()
putStrLn (Pred era -> [Char]
forall a. Show a => a -> [Char]
show Pred era
p [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. Show a => a -> [Char]
show Bool
b)) [(Pred era, Bool)]
pairs
  ReplMode -> Proof era -> Env era -> [Char] -> IO ()
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, Typed Bool -> Bool
forall t. HasCallStack => Typed t -> t
errorTyped (Env era -> Pred era -> Typed Bool
forall era. Env era -> Pred era -> Typed Bool
runPred Env era
env Pred era
p))
  [Char] -> Gen Property -> TestTree
forall a. Testable a => [Char] -> a -> TestTree
testProperty [Char]
name (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
    Env era
env <-
      ( Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
          Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo [Pred era]
preds
          Gen (Subst era) -> (Subst era -> Gen (Env era)) -> Gen (Env era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
subst -> Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv)
      )
    let pairs :: [(Pred era, Bool)]
pairs = (Pred era -> (Pred era, Bool)) -> [Pred era] -> [(Pred era, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (Env era -> Pred era -> (Pred era, Bool)
forall {era}. Env era -> Pred era -> (Pred era, Bool)
tryPred Env era
env) [Pred era]
preds
    Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Property
forall prop. Testable prop => prop -> Property
property ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (((Pred era, Bool) -> Bool) -> [(Pred era, Bool)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Pred era, Bool) -> Bool
forall a b. (a, b) -> b
snd [(Pred era, Bool)]
pairs)))

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

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

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

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