{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}

-- | Tests for [CIP-0123](https://cips.cardano.org/cip/CIP-0123)(the second
-- batch of bitwise builtins).
module Evaluation.Builtins.Bitwise.CIP0123 (
  shiftHomomorphism,
  rotateHomomorphism,
  csbHomomorphism,
  shiftClear,
  rotateRollover,
  csbRotate,
  shiftPosClearLow,
  shiftNegClearHigh,
  rotateMoveBits,
  csbComplement,
  csbInclusionExclusion,
  csbXor,
  ffsReplicate,
  ffsXor,
  ffsIndex,
  ffsZero,
  shiftMinBound,
  rotateMinBound,
  ffs6453
  ) where

import Evaluation.Helpers (assertEvaluatesToConstant, evaluateTheSame, evaluateToHaskell,
                           evaluatesToConstant, forAllByteString, forAllByteStringThat)

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

import Control.Monad (unless)
import Data.Bits qualified as Bits
import Data.ByteString (ByteString)
import Data.ByteString qualified as BS
import Hedgehog (Property, forAll, property)
import Hedgehog.Gen qualified as Gen
import Hedgehog.Range qualified as Range
import Test.Tasty (TestTree)
import Test.Tasty.Hedgehog (testPropertyNamed)
import Test.Tasty.HUnit (testCase)

-- | Test for a regression found [here](https://github.com/IntersectMBO/plutus/pull/6453).
ffs6453 :: Property
ffs6453 :: Property
ffs6453 = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  -- Generate a suffix that is an exact multiple of 8 bytes, all zero
  Int
suffixLenMult <- 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
1 (Int -> PropertyT IO Int) -> Int -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ Int
10
  let suffix :: ByteString
suffix = Int -> Word8 -> ByteString
BS.replicate (Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
suffixLenMult) Word8
0x00
  -- Generate a prefix nonzero byte
  Word8
prefix <- Gen Word8 -> PropertyT IO Word8
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Word8 -> PropertyT IO Word8)
-> (Word8 -> Gen Word8) -> Word8 -> PropertyT IO Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range Word8 -> Gen Word8
forall (m :: * -> *). MonadGen m => Range Word8 -> m Word8
Gen.word8 (Range Word8 -> Gen Word8)
-> (Word8 -> Range Word8) -> Word8 -> Gen Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> Word8 -> Range Word8
forall a. a -> a -> Range a
Range.constant Word8
0x01 (Word8 -> PropertyT IO Word8) -> Word8 -> PropertyT IO Word8
forall a b. (a -> b) -> a -> b
$ Word8
0xFF
  let expected :: Int
expected = Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
* ByteString -> Int
BS.length ByteString
suffix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Word8 -> Int
forall b. FiniteBits b => b -> Int
Bits.countTrailingZeros Word8
prefix
  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.FindFirstSetBit) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () (ByteString -> Term TyName Name DefaultUni DefaultFun ())
-> (ByteString -> ByteString)
-> ByteString
-> Term TyName Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word8 -> ByteString -> ByteString
BS.cons Word8
prefix (ByteString -> Term TyName Name DefaultUni DefaultFun ())
-> ByteString -> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ByteString
suffix
        ]
  forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant @Integer (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
expected) Term TyName Name DefaultUni DefaultFun ()
lhs

-- | If given 'Int' 'minBound' as an argument, rotations behave sensibly.
rotateMinBound :: Property
rotateMinBound :: Property
rotateMinBound = 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 bitLen :: Integer
bitLen = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> 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
  -- By the laws of rotations, we know that we can perform a modular reduction on
  -- the argument and not change the result we get. Thus, we (via Integer) do
  -- this exact reduction on minBound, then compare the result of running a
  -- rotation using this reduced argument versus the actual argument.
  let minBoundInt :: Integer
minBoundInt = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
minBound :: Int)
  let minBoundIntReduced :: Integer
minBoundIntReduced = Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer
forall a. Num a => a -> a
abs Integer
minBoundInt Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
bitLen)
  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.RotateByteString) [
        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
minBoundInt
        ]
  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.RotateByteString) [
        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
minBoundIntReduced
        ]
  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 given 'Int' 'minBound' as an argument, shifts behave sensibly.
shiftMinBound :: Property
shiftMinBound :: Property
shiftMinBound = 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 len :: Int
len = ByteString -> Int
BS.length ByteString
bs
  let shiftExp :: Term TyName Name DefaultUni DefaultFun ()
shiftExp = 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.ShiftByteString) [
        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 -> Term TyName Name DefaultUni DefaultFun ())
-> (Int -> Integer)
-> Int
-> Term TyName Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Term TyName Name DefaultUni DefaultFun ())
-> Int -> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ (Int
forall a. Bounded a => a
minBound :: Int)
        ]
  forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant @ByteString (Int -> Word8 -> ByteString
BS.replicate Int
len Word8
0x00) Term TyName Name DefaultUni DefaultFun ()
shiftExp

-- | Finding the first set bit in a bytestring with only zero bytes should always give -1.
ffsZero :: Property
ffsZero :: Property
ffsZero = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  Int
len <- 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
512
  let bs :: ByteString
bs = Int -> Word8 -> ByteString
BS.replicate Int
len Word8
0x00
  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.FindFirstSetBit) [
        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.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant @Integer (Integer -> Integer
forall a. Num a => a -> a
negate Integer
1) Term TyName Name DefaultUni DefaultFun ()
rhs

-- | If we find a valid index for the first set bit, then:
--
-- 1. The specified index should have a set bit; and
-- 2. Any valid smaller index should have a clear bit.
--
-- We 'hack' the generator slightly here to ensure we don't end up with all-zeroes (or the empty
-- bytestring), as otherwise, the test wouldn't be meaningful.
ffsIndex :: Property
ffsIndex :: Property
ffsIndex = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  ByteString
bs <- (ByteString -> Bool) -> Int -> Int -> PropertyT IO ByteString
forall (m :: * -> *).
(Monad m, HasCallStack) =>
(ByteString -> Bool) -> Int -> Int -> PropertyT m ByteString
forAllByteStringThat ((Word8 -> Bool) -> ByteString -> Bool
BS.any (Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word8
0x00)) Int
0 Int
512
  let ffsExp :: Term TyName Name DefaultUni DefaultFun ()
ffsExp = 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.FindFirstSetBit) [
        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
        ]
  Integer
ix <- Term TyName Name DefaultUni DefaultFun () -> PropertyT IO Integer
forall a.
ReadKnownIn DefaultUni (Term Name DefaultUni DefaultFun ()) a =>
Term TyName Name DefaultUni DefaultFun () -> PropertyT IO a
evaluateToHaskell Term TyName Name DefaultUni DefaultFun ()
ffsExp
  let hitIxExp :: Term TyName Name DefaultUni DefaultFun ()
hitIxExp = 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
ix
        ]
  Bool
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant Bool
True Term TyName Name DefaultUni DefaultFun ()
hitIxExp
  Bool -> PropertyT IO () -> PropertyT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
ix Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0) (PropertyT IO () -> PropertyT IO ())
-> PropertyT IO () -> PropertyT IO ()
forall a b. (a -> b) -> a -> b
$ do
    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
ix Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
    let missIxExp :: Term TyName Name DefaultUni DefaultFun ()
missIxExp = 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
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant Bool
False Term TyName Name DefaultUni DefaultFun ()
missIxExp

-- | For any choice of bytestring, if we XOR it with itself, there should be no set bits; that is,
-- finding the first set bit should give @-1@.
ffsXor :: Property
ffsXor :: Property
ffsXor = 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 <- 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 rhsInner :: Term TyName Name DefaultUni DefaultFun ()
rhsInner = 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 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.FindFirstSetBit) [
        Term TyName Name DefaultUni DefaultFun ()
rhsInner
        ]
  forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant @Integer (Integer -> Integer
forall a. Num a => a -> a
negate Integer
1) Term TyName Name DefaultUni DefaultFun ()
rhs

-- | If we replicate any byte any (positive) number of times, the first set bit
-- should be the same as in the case where we replicated it exactly once.
ffsReplicate :: Property
ffsReplicate :: Property
ffsReplicate = 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
w8 <- 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
255
  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
w8
        ]
  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.FindFirstSetBit) [
        Term TyName Name DefaultUni DefaultFun ()
lhsInner
        ]
  let rhsInner :: Term TyName Name DefaultUni DefaultFun ()
rhsInner = 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
1,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
w8
        ]
  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.FindFirstSetBit) [
        Term TyName Name DefaultUni DefaultFun ()
rhsInner
        ]
  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

-- | For any bytestring whose bit length is @n@ and has @k@ set bits, its complement should have
-- @n - k@ set bits.
csbComplement :: Property
csbComplement :: Property
csbComplement = 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 bitLen :: Int
bitLen = ByteString -> Int
BS.length ByteString
bs Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8
  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.CountSetBits) [
        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 rhsComplement :: Term TyName Name DefaultUni DefaultFun ()
rhsComplement = 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 rhsCount :: Term TyName Name DefaultUni DefaultFun ()
rhsCount = 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.CountSetBits) [
        Term TyName Name DefaultUni DefaultFun ()
rhsComplement
        ]
  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.SubtractInteger) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
bitLen),
        Term TyName Name DefaultUni DefaultFun ()
rhsCount
        ]
  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

-- | The inclusion-exclusion principle: specifically, for any @x@ and @y@, the number of set bits in
-- @x XOR y@ should be the number of set bits in @x OR y@ minus the number of set bits in @x AND y@.
csbInclusionExclusion :: Property
csbInclusionExclusion :: Property
csbInclusionExclusion = 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
  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
False,
        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
PLC.CountSetBits) [
        Term TyName Name DefaultUni DefaultFun ()
lhsInner
        ]
  let rhsOr :: Term TyName Name DefaultUni DefaultFun ()
rhsOr = 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.OrByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
        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 rhsAnd :: Term TyName Name DefaultUni DefaultFun ()
rhsAnd = 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.AndByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
        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 rhsCountOr :: Term TyName Name DefaultUni DefaultFun ()
rhsCountOr = 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.CountSetBits) [
        Term TyName Name DefaultUni DefaultFun ()
rhsOr
        ]
  let rhsCountAnd :: Term TyName Name DefaultUni DefaultFun ()
rhsCountAnd = 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.CountSetBits) [
        Term TyName Name DefaultUni DefaultFun ()
rhsAnd
        ]
  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.SubtractInteger) [
        Term TyName Name DefaultUni DefaultFun ()
rhsCountOr,
        Term TyName Name DefaultUni DefaultFun ()
rhsCountAnd
        ]
  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

-- | For any bytestring @x@, the number of set bits in @x XOR x@ should be 0.
csbXor :: Property
csbXor :: Property
csbXor = 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 <- 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 rhsInner :: Term TyName Name DefaultUni DefaultFun ()
rhsInner = 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 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.CountSetBits) [
        Term TyName Name DefaultUni DefaultFun ()
rhsInner
        ]
  forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant @Integer Integer
0 Term TyName Name DefaultUni DefaultFun ()
rhs

-- | There should exist a monoid homomorphism between natural number addition
-- and function composition for shifts over a fixed bytestring argument.
shiftHomomorphism :: [TestTree]
shiftHomomorphism :: [TestTree]
shiftHomomorphism = [
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"zero shift is identity" PropertyName
"zero_shift_id" (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
10) Property
idProp,
  -- Because the homomorphism on shifts is more restrictive than on rotations (namely, it is for
  -- naturals and their negative equivalents, not integers), we separate the composition property
  -- into two: one dealing with non-negative, the other with non-positive. This helps a bit with
  -- coverage, as otherwise, we wouldn't necessarily cover both paths equally well, as we'd have to
  -- either discard mismatched signs (which are likely) or 'hack them in-place', which would skew
  -- distributions.
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"non-negative addition of shifts is composition" PropertyName
"plus_shift_pos_comp" (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
plusCompProp,
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"non-positive addition of shifts is composition" PropertyName
"plus_shift_neg_comp" (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
minusCompProp
  ]
  where
    idProp :: Property
    idProp :: Property
idProp = 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
PLC.ShiftByteString) [
            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
0
            ]
      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
    plusCompProp :: Property
    plusCompProp :: Property
plusCompProp = 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
      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
512
      Integer
j <- 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 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.AddInteger) [
            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 @Integer () Integer
j
            ]
      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.ShiftByteString) [
            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
            ]
      let rhsInner :: Term TyName Name DefaultUni DefaultFun ()
rhsInner = 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.ShiftByteString) [
            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
            ]
      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.ShiftByteString) [
            Term TyName Name DefaultUni DefaultFun ()
rhsInner,
            forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
j
            ]
      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
    minusCompProp :: Property
    minusCompProp :: Property
minusCompProp = 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
      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 -> Integer
forall a. Num a => a -> a
negate Integer
512
      Integer
j <- 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 -> Integer
forall a. Num a => a -> a
negate Integer
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.AddInteger) [
            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 @Integer () Integer
j
            ]
      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.ShiftByteString) [
            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
            ]
      let rhsInner :: Term TyName Name DefaultUni DefaultFun ()
rhsInner = 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.ShiftByteString) [
            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
            ]
      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.ShiftByteString) [
            Term TyName Name DefaultUni DefaultFun ()
rhsInner,
            forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
j
            ]
      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

-- | There should exist a monoid homomorphism between integer addition and function composition for
-- rotations over a fixed bytestring argument.
rotateHomomorphism :: [TestTree]
rotateHomomorphism :: [TestTree]
rotateHomomorphism = [
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"zero rotation is identity" PropertyName
"zero_rotate_id" (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
10) Property
idProp,
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"addition of rotations is composition" PropertyName
"plus_rotate_comp" (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
compProp
  ]
  where
    idProp :: Property
    idProp :: Property
idProp = 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
PLC.RotateByteString) [
            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
0
            ]
      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
    compProp :: Property
    compProp :: Property
compProp = 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
      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 -> Integer
forall a. Num a => a -> a
negate Integer
512) (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
512
      Integer
j <- 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 -> Integer
forall a. Num a => a -> a
negate Integer
512) (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
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.AddInteger) [
            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 @Integer () Integer
j
            ]
      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.RotateByteString) [
            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
            ]
      let rhsInner :: Term TyName Name DefaultUni DefaultFun ()
rhsInner = 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.RotateByteString) [
            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
            ]
      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.RotateByteString) [
            Term TyName Name DefaultUni DefaultFun ()
rhsInner,
            forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
j
            ]
      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

-- | There should exist a monoid homomorphism between bytestring concatenation and natural number
-- addition.
csbHomomorphism :: [TestTree]
csbHomomorphism :: [TestTree]
csbHomomorphism = [
  TestName -> Assertion -> TestTree
testCase TestName
"count of empty is zero" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ do
    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.CountSetBits) [
          forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
""
          ]
    forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> Assertion
assertEvaluatesToConstant @Integer Integer
0 Term TyName Name DefaultUni DefaultFun ()
lhs,
  TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
"count of concat is addition" PropertyName
"concat_count_plus" (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
compProp
  ]
  where
    compProp :: Property
    compProp :: Property
compProp = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      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
PLC.AppendByteString) [
            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.CountSetBits) [
            Term TyName Name DefaultUni DefaultFun ()
lhsInner
            ]
      let rhsLeft :: Term TyName Name DefaultUni DefaultFun ()
rhsLeft = 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.CountSetBits) [
            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 rhsRight :: Term TyName Name DefaultUni DefaultFun ()
rhsRight = 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.CountSetBits) [
            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
PLC.AddInteger) [
            Term TyName Name DefaultUni DefaultFun ()
rhsLeft,
            Term TyName Name DefaultUni DefaultFun ()
rhsRight
            ]
      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

-- | Shifting by more than the bit length (either positive or negative) clears the result.
shiftClear :: Property
shiftClear :: Property
shiftClear = 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 bitLen :: Int
bitLen = Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
* ByteString -> Int
BS.length ByteString
bs
  Int
i <- 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 -> Int
forall a. Num a => a -> a
negate Int
256) (Int -> PropertyT IO Int) -> Int -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ Int
256
  Int
adjustment <- case Int -> Int
forall a. Num a => a -> a
signum Int
i of
    (-1) -> Int -> PropertyT IO Int
forall a. a -> PropertyT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> PropertyT IO Int) -> Int -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
negate Int
bitLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
    -- Here, we shift by the length exactly, so we randomly pick negative or positive
    Int
0    -> 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
. [Int] -> Gen Int
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element ([Int] -> PropertyT IO Int) -> [Int] -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ [Int
bitLen, Int -> Int
forall a. Num a => a -> a
negate Int
bitLen]
    Int
_    -> Int -> PropertyT IO Int
forall a. a -> PropertyT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> PropertyT IO Int) -> Int -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ Int
bitLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i
  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.ShiftByteString) [
        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 () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
adjustment)
        ]
  let rhsInner :: Term TyName Name DefaultUni DefaultFun ()
rhsInner = 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.LengthOfByteString) [
        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 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) [
        Term TyName Name DefaultUni DefaultFun ()
rhsInner,
        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
        ]
  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

-- | Positive shifts clear low-index bits.
shiftPosClearLow :: Property
shiftPosClearLow :: Property
shiftPosClearLow = 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 bitLen :: Int
bitLen = Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
* ByteString -> Int
BS.length ByteString
bs
  Int
n <- 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
1 (Int -> PropertyT IO Int) -> Int -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ Int
bitLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
  Int
i <- 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
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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.ShiftByteString) [
        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 () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)
        ]
  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 () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
        ]
  Bool
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant Bool
False Term TyName Name DefaultUni DefaultFun ()
lhs

-- | Negative shifts clear high-index bits.
shiftNegClearHigh :: Property
shiftNegClearHigh :: Property
shiftNegClearHigh = 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 bitLen :: Int
bitLen = Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
* ByteString -> Int
BS.length ByteString
bs
  Int
n <- 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
1 (Int -> PropertyT IO Int) -> Int -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ Int
bitLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
  Int
i <- 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
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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.ShiftByteString) [
        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 () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> (Int -> Int) -> Int -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Num a => a -> a
negate (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Int
n)
        ]
  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 () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Int
bitLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        ]
  Bool
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
forall a.
Contains DefaultUni a =>
a -> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluatesToConstant Bool
False Term TyName Name DefaultUni DefaultFun ()
lhs

-- | Rotations by more than the bit length 'roll over' bits.
rotateRollover :: Property
rotateRollover :: Property
rotateRollover = 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 bitLen :: Int
bitLen = Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
* ByteString -> Int
BS.length ByteString
bs
  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 -> Integer
forall a. Num a => a -> a
negate Integer
512) (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
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.RotateByteString) [
        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 () (case Integer -> Integer
forall a. Num a => a -> a
signum Integer
i of
                                  (-1) -> (Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> (Int -> Integer) -> Int -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Int
bitLen) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i
                                  Integer
_    -> Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
bitLen Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i)
        ]
  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.RotateByteString) [
        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
        ]
  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

-- | Rotations move bits, but don't change them.
rotateMoveBits :: Property
rotateMoveBits :: Property
rotateMoveBits = 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 bitLen :: Int
bitLen = Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
* ByteString -> Int
BS.length ByteString
bs
  Int
i <- 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
bitLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
  Int
j <- 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 -> Int
forall a. Num a => a -> a
negate Int
256) (Int -> PropertyT IO Int) -> Int -> PropertyT IO Int
forall a b. (a -> b) -> a -> b
$ Int
256
  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) [
        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 () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
        ]
  let rhsRotation :: Term TyName Name DefaultUni DefaultFun ()
rhsRotation = 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.RotateByteString) [
        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 () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
j)
        ]
  let rhsIndex :: Term TyName Name DefaultUni DefaultFun ()
rhsIndex = 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.ModInteger) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j),
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
bitLen)
        ]
  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.ReadBit) [
        Term TyName Name DefaultUni DefaultFun ()
rhsRotation,
        Term TyName Name DefaultUni DefaultFun ()
rhsIndex
        ]
  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

-- | Rotations do not change how many set (and clear) bits there are.
csbRotate :: Property
csbRotate :: Property
csbRotate = 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
  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 -> Integer
forall a. Num a => a -> a
negate Integer
512) (Integer -> PropertyT IO Integer)
-> Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Integer
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.CountSetBits) [
        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 rhsInner :: Term TyName Name DefaultUni DefaultFun ()
rhsInner = 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.RotateByteString) [
        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
        ]
  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.CountSetBits) [
        Term TyName Name DefaultUni DefaultFun ()
rhsInner
        ]
  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