-- 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