-- editorconfig-checker-disable-file
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

{-| Tests for [CIP-0122](https://cips.cardano.org/cip/CIP-0122) (the first
batch of bitwise builtins) -}
module Evaluation.Builtins.Bitwise.CIP0122
  ( abelianSemigroupLaws
  , abelianMonoidLaws
  , idempotenceLaw
  , absorbtionLaw
  , leftDistributiveLaw
  , distributiveLaws
  , xorInvoluteLaw
  , complementSelfInverse
  , deMorgan
  , getSet
  , setGet
  , setSet
  , writeBitsHomomorphismLaws
  , replicateHomomorphismLaws
  , replicateIndex
  ) where

import PlutusCore qualified as PLC
import PlutusCore.MkPlc (builtin, mkConstant, mkIterAppNoAnn)
import PlutusCore.Test (mapTestLimitAtLeast)
import UntypedPlutusCore qualified as UPLC

import Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Evaluation.Helpers
  ( evaluateTheSame
  , evaluateToHaskell
  , evaluatesToConstant
  , forAllByteString
  )
import GHC.Exts (fromString)
import Hedgehog (Gen, Property, PropertyT, forAll, forAllWith, property)
import Hedgehog.Gen qualified as Gen
import Hedgehog.Range qualified as Range
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Hedgehog (testPropertyNamed)

{-| Any call to 'replicateByteString' must produce the same byte at
every valid index, namely the byte specified. -}
replicateIndex :: TestTree
replicateIndex :: TestTree
replicateIndex = TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"every byte is the same" PropertyName
"replicate_all_match" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
  TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
99 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    Integer
n <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> (Integer -> Gen Integer) -> Integer -> PropertyT IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Integer -> Range Integer) -> Integer -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> Range a
Range.linear Integer
1 (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
512
    Integer
b <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> (Integer -> Gen Integer) -> Integer -> PropertyT IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Integer -> Range Integer) -> Integer -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
0 (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
255
    Integer
i <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> (Integer -> Gen Integer) -> Integer -> PropertyT IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Integer -> Range Integer) -> Integer -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> Range a
Range.linear Integer
0 (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
    let lhsInner :: Term TyName Name DefaultUni DefaultFun ()
lhsInner =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ReplicateByte)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
n
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
b
            ]
    let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IndexByteString)
            [ Term TyName Name DefaultUni DefaultFun ()
lhsInner
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
i
            ]
    forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant @Integer Integer
b Term TyName Name DefaultUni DefaultFun ()
lhs

{-| If you retrieve a bit value at an index, then write that same value to
the same index, nothing should happen. -}
getSet :: TestTree
getSet :: TestTree
getSet =
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"get-set" PropertyName
"get_set" (Property -> TestTree)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> TestTree) -> PropertyT IO () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
    ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
1 Int
512
    Integer
i <- ByteString -> PropertyT IO Integer
forAllIndexOf ByteString
bs
    let lookupExp :: Term TyName Name DefaultUni DefaultFun ()
lookupExp =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ReadBit)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
i
            ]
    Bool
b <- Term TyName Name DefaultUni DefaultFun () -> PropertyT IO Bool
forall a.
ReadKnownIn DefaultUni (Term Name DefaultUni DefaultFun ()) a =>
Term TyName Name DefaultUni DefaultFun () -> PropertyT IO a
evaluateToHaskell Term TyName Name DefaultUni DefaultFun ()
lookupExp
    let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () [Integer
i]
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b
            ]
    ByteString
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant ByteString
bs Term TyName Name DefaultUni DefaultFun ()
lhs

{-| If you write a bit value to an index, then retrieve the bit value at the
same index, you should get back what you wrote. -}
setGet :: TestTree
setGet :: TestTree
setGet =
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"set-get" PropertyName
"set_get" (Property -> TestTree)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
99 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> TestTree) -> PropertyT IO () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
    ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
1 Int
512
    Integer
i <- ByteString -> PropertyT IO Integer
forAllIndexOf ByteString
bs
    Bool
b <- Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
    let lhsInner :: Term TyName Name DefaultUni DefaultFun ()
lhsInner =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () [Integer
i]
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b
            ]
    let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ReadBit)
            [ Term TyName Name DefaultUni DefaultFun ()
lhsInner
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
i
            ]
    Bool
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant Bool
b Term TyName Name DefaultUni DefaultFun ()
lhs

-- | If you write twice to the same bit index, the second write should win.
setSet :: TestTree
setSet :: TestTree
setSet =
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"set-set" PropertyName
"set_set" (Property -> TestTree)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> TestTree) -> PropertyT IO () -> TestTree
forall a b. (a -> b) -> a -> b
$ do
    ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
1 Int
512
    Integer
i <- ByteString -> PropertyT IO Integer
forAllIndexOf ByteString
bs
    Bool
b1 <- Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
    Bool
b2 <- Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
    let lhsInner :: Term TyName Name DefaultUni DefaultFun ()
lhsInner =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () [Integer
i, Integer
i]
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b1
            ]
    let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
            [ Term TyName Name DefaultUni DefaultFun ()
lhsInner
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () [Integer
i, Integer
i]
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b2
            ]
    let rhs :: Term TyName Name DefaultUni DefaultFun ()
rhs =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () [Integer
i]
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b2
            ]
    HasCallStack =>
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateTheSame Term TyName Name DefaultUni DefaultFun ()
lhs Term TyName Name DefaultUni DefaultFun ()
rhs

{-| Checks that:

* Writing with an empty list of positions does nothing; and if you write a
* boolean b with one list of positions, then a second, it is the same as
* writing b with their concatenation. -}
writeBitsHomomorphismLaws :: TestTree
writeBitsHomomorphismLaws :: TestTree
writeBitsHomomorphismLaws =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"homomorphism to lists"
    [ TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"identity -> []" PropertyName
"write_bits_h_1_false" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
99 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Bool -> Property
identityProp Bool
False)
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"identity -> []" PropertyName
"write_bits_h_1_true" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
99 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Bool -> Property
identityProp Bool
True)
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"composition -> concatenation" PropertyName
"write_bits_h_2_false" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Bool -> Property
compositionProp Bool
False)
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"composition -> concatenation" PropertyName
"write_bits_h_2_true" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Bool -> Property
compositionProp Bool
True)
    ]
  where
    identityProp :: Bool -> Property
    identityProp :: Bool -> Property
identityProp Bool
b = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
1 Int
512
      let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () []
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b
              ]
      ByteString
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant ByteString
bs Term TyName Name DefaultUni DefaultFun ()
lhs
    compositionProp :: Bool -> Property
    compositionProp :: Bool -> Property
compositionProp Bool
b = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
1 Int
512
      [Integer]
ixes1 <- ByteString -> PropertyT IO [Integer]
forAllListsOfIndices ByteString
bs
      [Integer]
ixes2 <- ByteString -> PropertyT IO [Integer]
forAllListsOfIndices ByteString
bs
      let lhsInner :: Term TyName Name DefaultUni DefaultFun ()
lhsInner =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () [Integer]
ixes1
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b
              ]
      let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
              [ Term TyName Name DefaultUni DefaultFun ()
lhsInner
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () [Integer]
ixes2
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b
              ]
      let rhs :: Term TyName Name DefaultUni DefaultFun ()
rhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.WriteBits)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @[Integer] () ([Integer]
ixes1 [Integer] -> [Integer] -> [Integer]
forall a. Semigroup a => a -> a -> a
<> [Integer]
ixes2)
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b
              ]
      HasCallStack =>
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateTheSame Term TyName Name DefaultUni DefaultFun ()
lhs Term TyName Name DefaultUni DefaultFun ()
rhs

{-| Checks that:

* Replicating any byte 0 times produces the empty 'ByteString'; and
* Replicating a byte @n@ times, then replicating a byte @m@ times and
  concatenating the results, is the same as replicating that byte @n + m@
  times. -}
replicateHomomorphismLaws :: TestTree
replicateHomomorphismLaws :: TestTree
replicateHomomorphismLaws =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"homomorphism"
    [ TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"0 -> empty" PropertyName
"replicate_h_1" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
99 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) Property
identityProp
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"+ -> concat" PropertyName
"replicate_h_2" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) Property
compositionProp
    ]
  where
    identityProp :: Property
    identityProp :: Property
identityProp = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      Integer
b <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> (Integer -> Gen Integer) -> Integer -> PropertyT IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Integer -> Range Integer) -> Integer -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
0 (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
255
      let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ReplicateByte)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
b
              ]
      forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant @ByteString ByteString
"" Term TyName Name DefaultUni DefaultFun ()
lhs
    compositionProp :: Property
    compositionProp :: Property
compositionProp = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      Integer
b <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> (Integer -> Gen Integer) -> Integer -> PropertyT IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Integer -> Range Integer) -> Integer -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
0 (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
255
      Integer
n1 <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> (Integer -> Gen Integer) -> Integer -> PropertyT IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Integer -> Range Integer) -> Integer -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> Range a
Range.linear Integer
0 (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
512
      Integer
n2 <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> (Integer -> Gen Integer) -> Integer -> PropertyT IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Integer -> Range Integer) -> Integer -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> Range a
Range.linear Integer
0 (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
512
      let lhsInner1 :: Term TyName Name DefaultUni DefaultFun ()
lhsInner1 =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ReplicateByte)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
n1
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
b
              ]
      let lhsInner2 :: Term TyName Name DefaultUni DefaultFun ()
lhsInner2 =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ReplicateByte)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
n2
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
b
              ]
      let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.AppendByteString)
              [ Term TyName Name DefaultUni DefaultFun ()
lhsInner1
              , Term TyName Name DefaultUni DefaultFun ()
lhsInner2
              ]
      let rhs :: Term TyName Name DefaultUni DefaultFun ()
rhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ReplicateByte)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () (Integer
n1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n2)
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
b
              ]
      HasCallStack =>
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateTheSame Term TyName Name DefaultUni DefaultFun ()
lhs Term TyName Name DefaultUni DefaultFun ()
rhs

-- | If you complement a 'ByteString' twice, nothing should change.
complementSelfInverse :: TestTree
complementSelfInverse :: TestTree
complementSelfInverse =
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"self-inverse" PropertyName
"self_inverse" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
    TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
99 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
      let lhsInner :: Term TyName Name DefaultUni DefaultFun ()
lhsInner =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ComplementByteString)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
              ]
      let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ComplementByteString)
              [ Term TyName Name DefaultUni DefaultFun ()
lhsInner
              ]
      ByteString
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant ByteString
bs Term TyName Name DefaultUni DefaultFun ()
lhs

{-| Checks that:

* The complement of an AND is an OR of complements; and
* The complement of an OR is an AND of complements. -}
deMorgan :: TestTree
deMorgan :: TestTree
deMorgan =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"De Morgan's laws"
    [ TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"NOT AND -> OR" PropertyName
"demorgan_and" (Property -> TestTree)
-> (DefaultFun -> Property) -> DefaultFun -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultFun -> DefaultFun -> Property
go DefaultFun
PLC.AndByteString (DefaultFun -> TestTree) -> DefaultFun -> TestTree
forall a b. (a -> b) -> a -> b
$ DefaultFun
PLC.OrByteString
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"NOT OR -> AND" PropertyName
"demorgan_or" (Property -> TestTree)
-> (DefaultFun -> Property) -> DefaultFun -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultFun -> DefaultFun -> Property
go DefaultFun
PLC.OrByteString (DefaultFun -> TestTree) -> DefaultFun -> TestTree
forall a b. (a -> b) -> a -> b
$ DefaultFun
PLC.AndByteString
    ]
  where
    go :: UPLC.DefaultFun -> UPLC.DefaultFun -> Property
    go :: DefaultFun -> DefaultFun -> Property
go DefaultFun
f DefaultFun
g = TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      Bool
semantics <- (Bool -> TestName) -> Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> TestName) -> Gen a -> PropertyT m a
forAllWith Bool -> TestName
showSemantics Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
      ByteString
bs1 <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
      ByteString
bs2 <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
      let lhsInner :: Term TyName Name DefaultUni DefaultFun ()
lhsInner =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
semantics
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs1
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs2
              ]
      let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ComplementByteString)
              [ Term TyName Name DefaultUni DefaultFun ()
lhsInner
              ]
      let rhsInner1 :: Term TyName Name DefaultUni DefaultFun ()
rhsInner1 =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ComplementByteString)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs1
              ]
      let rhsInner2 :: Term TyName Name DefaultUni DefaultFun ()
rhsInner2 =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ComplementByteString)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs2
              ]
      let rhs :: Term TyName Name DefaultUni DefaultFun ()
rhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
g)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
semantics
              , Term TyName Name DefaultUni DefaultFun ()
rhsInner1
              , Term TyName Name DefaultUni DefaultFun ()
rhsInner2
              ]
      HasCallStack =>
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateTheSame Term TyName Name DefaultUni DefaultFun ()
lhs Term TyName Name DefaultUni DefaultFun ()
rhs

-- | If you XOR any 'ByteString' with itself twice, nothing should change.
xorInvoluteLaw :: TestTree
xorInvoluteLaw :: TestTree
xorInvoluteLaw = TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"involute (both)" PropertyName
"involute_both" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
  TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
99 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
20) (Property -> Property)
-> (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
    Bool
semantics <- (Bool -> TestName) -> Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> TestName) -> Gen a -> PropertyT m a
forAllWith Bool -> TestName
showSemantics Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
    let lhsInner :: Term TyName Name DefaultUni DefaultFun ()
lhsInner =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.XorByteString)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
semantics
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
            ]
    let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
          Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
            (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.XorByteString)
            [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
semantics
            , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
            , Term TyName Name DefaultUni DefaultFun ()
lhsInner
            ]
    ByteString
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant ByteString
bs Term TyName Name DefaultUni DefaultFun ()
lhs

{-| Checks that the first 'DefaultFun' distributes over the second from the
left, given the specified semantics (as a 'Bool'). More precisely, for
'DefaultFun's @f@ and @g@, checks that @f x (g y z) = g (f x y) (f x z)@. -}
leftDistributiveLaw :: String -> String -> UPLC.DefaultFun -> UPLC.DefaultFun -> Bool -> TestTree
leftDistributiveLaw :: TestName
-> TestName -> DefaultFun -> DefaultFun -> Bool -> TestTree
leftDistributiveLaw TestName
name TestName
distOpName DefaultFun
f DefaultFun
distOp Bool
isPadding =
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed
    (TestName
"left distribution (" TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
name TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
") over " TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
distOpName)
    (PropertyName
"left_distribution_" PropertyName -> PropertyName -> PropertyName
forall a. Semigroup a => a -> a -> a
<> TestName -> PropertyName
forall a. IsString a => TestName -> a
fromString TestName
name PropertyName -> PropertyName -> PropertyName
forall a. Semigroup a => a -> a -> a
<> PropertyName
"_" PropertyName -> PropertyName -> PropertyName
forall a. Semigroup a => a -> a -> a
<> TestName -> PropertyName
forall a. IsString a => TestName -> a
fromString TestName
distOpName)
    (TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ DefaultFun -> DefaultFun -> Bool -> Property
leftDistProp DefaultFun
f DefaultFun
distOp Bool
isPadding)

-- | Checks that the given function self-distributes both left and right.
distributiveLaws :: String -> UPLC.DefaultFun -> Bool -> TestTree
distributiveLaws :: TestName -> DefaultFun -> Bool -> TestTree
distributiveLaws TestName
name DefaultFun
f Bool
isPadding =
  TestName -> [TestTree] -> TestTree
testGroup
    (TestName
"distributivity over itself (" TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
name TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
")")
    [ TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"left distribution" PropertyName
"left_distribution" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          DefaultFun -> DefaultFun -> Bool -> Property
leftDistProp DefaultFun
f DefaultFun
f Bool
isPadding
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"right distribution" PropertyName
"right_distribution" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          DefaultFun -> Bool -> Property
rightDistProp DefaultFun
f Bool
isPadding
    ]

{-| Checks that the given 'DefaultFun', under the given semantics, forms an
abelian semigroup: that is, the operation both commutes and associates. -}
abelianSemigroupLaws :: String -> UPLC.DefaultFun -> Bool -> TestTree
abelianSemigroupLaws :: TestName -> DefaultFun -> Bool -> TestTree
abelianSemigroupLaws TestName
name DefaultFun
f Bool
isPadding =
  TestName -> [TestTree] -> TestTree
testGroup
    (TestName
"abelian semigroup (" TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
name TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
")")
    [ TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"commutativity" PropertyName
"commutativity" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          DefaultFun -> Bool -> Property
commProp DefaultFun
f Bool
isPadding
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"associativity" PropertyName
"associativity" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          DefaultFun -> Bool -> Property
assocProp DefaultFun
f Bool
isPadding
    ]

{-| As 'abelianSemigroupLaws', but also checks that the provided 'ByteString'
is both a left and right identity. -}
abelianMonoidLaws :: String -> UPLC.DefaultFun -> Bool -> ByteString -> TestTree
abelianMonoidLaws :: TestName -> DefaultFun -> Bool -> ByteString -> TestTree
abelianMonoidLaws TestName
name DefaultFun
f Bool
isPadding ByteString
unit =
  TestName -> [TestTree] -> TestTree
testGroup
    (TestName
"abelian monoid (" TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
name TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
")")
    [ TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"commutativity" PropertyName
"commutativity" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          DefaultFun -> Bool -> Property
commProp DefaultFun
f Bool
isPadding
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"associativity" PropertyName
"associativity" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
50 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
10) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          DefaultFun -> Bool -> Property
assocProp DefaultFun
f Bool
isPadding
    , TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"unit" PropertyName
"unit" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
75 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
15) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          DefaultFun -> Bool -> ByteString -> Property
unitProp DefaultFun
f Bool
isPadding ByteString
unit
    ]

{-| Checks that the provided 'DefaultFun', under the given semantics, is
idempotent; namely, that @f x x = x@ for any @x@. -}
idempotenceLaw :: String -> UPLC.DefaultFun -> Bool -> TestTree
idempotenceLaw :: TestName -> DefaultFun -> Bool -> TestTree
idempotenceLaw TestName
name DefaultFun
f Bool
isPadding =
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed
    (TestName
"idempotence (" TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
name TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
")")
    (PropertyName
"idempotence_" PropertyName -> PropertyName -> PropertyName
forall a. Semigroup a => a -> a -> a
<> TestName -> PropertyName
forall a. IsString a => TestName -> a
fromString TestName
name)
    (TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
75 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
15) Property
idempProp)
  where
    idempProp :: Property
    idempProp :: Property
idempProp = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
      let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
              ]
      ByteString
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant ByteString
bs Term TyName Name DefaultUni DefaultFun ()
lhs

{-| Checks that the provided 'ByteString' is an absorbing element for the
given 'DefaultFun', under the given semantics. Specifically, given @f@
as the operation and @0@ as the absorbing element, for any @x@,
@f x 0 = f 0 x = 0@. -}
absorbtionLaw :: String -> UPLC.DefaultFun -> Bool -> ByteString -> TestTree
absorbtionLaw :: TestName -> DefaultFun -> Bool -> ByteString -> TestTree
absorbtionLaw TestName
name DefaultFun
f Bool
isPadding ByteString
absorber =
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed
    (TestName
"absorbing element (" TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
name TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
")")
    (PropertyName
"absorbing_element_" PropertyName -> PropertyName -> PropertyName
forall a. Semigroup a => a -> a -> a
<> TestName -> PropertyName
forall a. IsString a => TestName -> a
fromString TestName
name)
    (TestLimit -> (TestLimit -> TestLimit) -> Property -> Property
mapTestLimitAtLeast TestLimit
75 (TestLimit -> TestLimit -> TestLimit
forall a. Integral a => a -> a -> a
`div` TestLimit
15) Property
absorbProp)
  where
    absorbProp :: Property
    absorbProp :: Property
absorbProp = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
      let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
            Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
              (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
              [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
              , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
absorber
              ]
      ByteString
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant ByteString
absorber Term TyName Name DefaultUni DefaultFun ()
lhs

-- Helpers

showSemantics :: Bool -> String
showSemantics :: Bool -> TestName
showSemantics Bool
b =
  if Bool
b
    then TestName
"padding semantics"
    else TestName
"truncation semantics"

leftDistProp :: UPLC.DefaultFun -> UPLC.DefaultFun -> Bool -> Property
leftDistProp :: DefaultFun -> DefaultFun -> Bool -> Property
leftDistProp DefaultFun
f DefaultFun
distOp Bool
isPadding = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  ByteString
x <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  ByteString
y <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  ByteString
z <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  let distLhs :: Term TyName Name DefaultUni DefaultFun ()
distLhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
distOp)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
y
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
z
          ]
  let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
x
          , Term TyName Name DefaultUni DefaultFun ()
distLhs
          ]
  let distRhs1 :: Term TyName Name DefaultUni DefaultFun ()
distRhs1 =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
x
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
y
          ]
  let distRhs2 :: Term TyName Name DefaultUni DefaultFun ()
distRhs2 =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
x
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
z
          ]
  let rhs :: Term TyName Name DefaultUni DefaultFun ()
rhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
distOp)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , Term TyName Name DefaultUni DefaultFun ()
distRhs1
          , Term TyName Name DefaultUni DefaultFun ()
distRhs2
          ]
  HasCallStack =>
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateTheSame Term TyName Name DefaultUni DefaultFun ()
lhs Term TyName Name DefaultUni DefaultFun ()
rhs

rightDistProp :: UPLC.DefaultFun -> Bool -> Property
rightDistProp :: DefaultFun -> Bool -> Property
rightDistProp DefaultFun
f Bool
isPadding = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  ByteString
x <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  ByteString
y <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  ByteString
z <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  let lhsInner :: Term TyName Name DefaultUni DefaultFun ()
lhsInner =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
x
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
y
          ]
  let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , Term TyName Name DefaultUni DefaultFun ()
lhsInner
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
z
          ]
  let rhsInner1 :: Term TyName Name DefaultUni DefaultFun ()
rhsInner1 =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
x
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
z
          ]
  let rhsInner2 :: Term TyName Name DefaultUni DefaultFun ()
rhsInner2 =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
y
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
z
          ]
  let rhs :: Term TyName Name DefaultUni DefaultFun ()
rhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , Term TyName Name DefaultUni DefaultFun ()
rhsInner1
          , Term TyName Name DefaultUni DefaultFun ()
rhsInner2
          ]
  HasCallStack =>
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateTheSame Term TyName Name DefaultUni DefaultFun ()
lhs Term TyName Name DefaultUni DefaultFun ()
rhs

commProp :: UPLC.DefaultFun -> Bool -> Property
commProp :: DefaultFun -> Bool -> Property
commProp DefaultFun
f Bool
isPadding = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  ByteString
data1 <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  ByteString
data2 <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data1
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data2
          ]
  let rhs :: Term TyName Name DefaultUni DefaultFun ()
rhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data2
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data1
          ]
  HasCallStack =>
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateTheSame Term TyName Name DefaultUni DefaultFun ()
lhs Term TyName Name DefaultUni DefaultFun ()
rhs

assocProp :: UPLC.DefaultFun -> Bool -> Property
assocProp :: DefaultFun -> Bool -> Property
assocProp DefaultFun
f Bool
isPadding = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  ByteString
data1 <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  ByteString
data2 <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  ByteString
data3 <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  let data12 :: Term TyName Name DefaultUni DefaultFun ()
data12 =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data1
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data2
          ]
  let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , Term TyName Name DefaultUni DefaultFun ()
data12
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data3
          ]
  let data23 :: Term TyName Name DefaultUni DefaultFun ()
data23 =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data2
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data3
          ]
  let rhs :: Term TyName Name DefaultUni DefaultFun ()
rhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
data1
          , Term TyName Name DefaultUni DefaultFun ()
data23
          ]
  HasCallStack =>
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateTheSame Term TyName Name DefaultUni DefaultFun ()
lhs Term TyName Name DefaultUni DefaultFun ()
rhs

unitProp :: UPLC.DefaultFun -> Bool -> ByteString -> Property
unitProp :: DefaultFun -> Bool -> ByteString -> Property
unitProp DefaultFun
f Bool
isPadding ByteString
unit = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  ByteString
bs <- Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
Int -> Int -> PropertyT m ByteString
forAllByteString Int
0 Int
512
  let lhs :: Term TyName Name DefaultUni DefaultFun ()
lhs =
        Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
          (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
f)
          [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
isPadding
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
          , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
unit
          ]
  ByteString
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant ByteString
bs Term TyName Name DefaultUni DefaultFun ()
lhs

forAllIndexOf :: ByteString -> PropertyT IO Integer
forAllIndexOf :: ByteString -> PropertyT IO Integer
forAllIndexOf ByteString
bs = Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> (Int -> Gen Integer) -> Int -> PropertyT IO Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Int -> Range Integer) -> Int -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> Range a
Range.linear Integer
0 (Integer -> Range Integer)
-> (Int -> Integer) -> Int -> Range Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> PropertyT IO Integer) -> Int -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ ByteString -> Int
BS.length ByteString
bs Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

forAllListsOfIndices :: ByteString -> PropertyT IO [Integer]
forAllListsOfIndices :: ByteString -> PropertyT IO [Integer]
forAllListsOfIndices ByteString
bs = do
  Int
ourLen :: Int <- Gen Int -> PropertyT IO Int
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Int -> PropertyT IO Int)
-> (Int -> Gen Int) -> Int -> PropertyT IO Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Int -> Gen Int
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Int -> Gen Int) -> (Int -> Range Int) -> Int -> Gen Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
0 (Int -> PropertyT IO Int) -> Int -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
  [Integer]
ixes <- Gen [Integer] -> PropertyT IO [Integer]
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen [Integer] -> PropertyT IO [Integer])
-> (Gen Integer -> Gen [Integer])
-> Gen Integer
-> PropertyT IO [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Int -> Gen Integer -> Gen [Integer]
forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Gen.list (Int -> Range Int
forall a. a -> Range a
Range.singleton Int
ourLen) (Gen Integer -> PropertyT IO [Integer])
-> Gen Integer -> PropertyT IO [Integer]
forall a b. (a -> b) -> a -> b
$ Gen Integer
genIndex
  [Integer] -> PropertyT IO [Integer]
forall a. a -> PropertyT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Integer]
ixes
  where
    len :: Int
    len :: Int
len = ByteString -> Int
BS.length ByteString
bs
    genIndex :: Gen Integer
    genIndex :: Gen Integer
genIndex = Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> Gen Integer)
-> (Int -> Range Integer) -> Int -> Gen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> Range a
Range.linear Integer
0 (Integer -> Range Integer)
-> (Int -> Integer) -> Int -> Range Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Gen Integer) -> Int -> Gen Integer
forall a b. (a -> b) -> a -> b
$ Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1