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

module Test.Cardano.Ledger.Constrained.Examples where

import Cardano.Ledger.Babbage (Babbage)
import Cardano.Ledger.BaseTypes (EpochNo (..))
import Cardano.Ledger.CertState (FutureGenDeleg (..))
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Core (Era (EraCrypto))
import Cardano.Ledger.Keys (GenDelegPair)
import Control.DeepSeq (deepseq)
import Control.Exception (ErrorCall (..))
import Control.Monad (when)
import Data.Default (Default (..))
import Data.Map (Map)
import Data.Ratio ((%))
import qualified Debug.Trace as Debug
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes (OrdCond (..))
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Lenses (fGenDelegGenKeyHashL)
import Test.Cardano.Ledger.Constrained.Monad
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.Tx (genTxAndNewEpoch)
import Test.Cardano.Ledger.Constrained.Rewrite
import Test.Cardano.Ledger.Constrained.Solver
import Test.Cardano.Ledger.Constrained.Spec (TT)
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 (..), StandardCrypto)
import Test.Cardano.Ledger.Generic.Trace (testPropMax)
import Test.Hspec (shouldThrow)
import Test.QuickCheck hiding (Fixed, total)
import Test.Tasty (TestTree, defaultMain, testGroup)
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck
import Type.Reflection (typeRep)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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