{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Use camelCase" #-}
{-# HLINT ignore "Evaluate" #-}

module Test.Cardano.Ledger.Core.Binary.CDDL where

import Codec.CBOR.Cuddle.Huddle
import Data.Function (($))
import Data.Semigroup ((<>))
import qualified Data.Text as T
import Data.Word (Word64)
import GHC.Show (Show (show))
import Text.Heredoc
import Prelude (Integer)

--------------------------------------------------------------------------------
-- Base Types
--------------------------------------------------------------------------------
coin :: Rule
coin :: Rule
coin = Text
"coin" forall a. IsType0 a => Text -> a -> Rule
=:= Value Int
VUInt

positive_coin :: Rule
positive_coin :: Rule
positive_coin = Text
"positive_coin" forall a. IsType0 a => Text -> a -> Rule
=:= Integer
1 Integer -> Integer -> Ranged
... Integer
maxWord64

address :: Rule
address :: Rule
address =
  forall a. Text -> Named a -> Named a
comment
    [str|address = bytes
        |
        |address format:
        |  [ 8 bit header | payload ];
        |
        |shelley payment addresses:
        |     bit 7: 0
        |     bit 6: base/other
        |     bit 5: pointer/enterprise [for base: stake cred is keyhash/scripthash]
        |     bit 4: payment cred is keyhash/scripthash
        |  bits 3-0: network id
        |
        |reward addresses:
        |  bits 7-5: 111
        |     bit 4: credential is keyhash/scripthash
        |  bits 3-0: network id
        |
        |byron addresses:
        |  bits 7-4: 1000
        |
        |     0000: base address: keyhash28,keyhash28
        |     0001: base address: scripthash28,keyhash28
        |     0010: base address: keyhash28,scripthash28
        |     0011: base address: scripthash28,scripthash28
        |     0100: pointer address: keyhash28, 3 variable length uint
        |     0101: pointer address: scripthash28, 3 variable length uint
        |     0110: enterprise address: keyhash28
        |     0111: enterprise address: scripthash28
        |     1000: byron address
        |     1110: reward account: keyhash28
        |     1111: reward account: scripthash28
        |1001-1101: future formats
        |]
    forall a b. (a -> b) -> a -> b
$ Text
"address"
      forall a. IsType0 a => Text -> a -> Rule
=:= ByteString -> Literal
bstr
        ByteString
"001000000000000000000000000000000000000000000000000000000011000000000000000000000000000000000000000000000000000000"
      forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ ByteString -> Literal
bstr
        ByteString
"102000000000000000000000000000000000000000000000000000000022000000000000000000000000000000000000000000000000000000"
      forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ ByteString -> Literal
bstr
        ByteString
"203000000000000000000000000000000000000000000000000000000033000000000000000000000000000000000000000000000000000000"
      forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ ByteString -> Literal
bstr
        ByteString
"304000000000000000000000000000000000000000000000000000000044000000000000000000000000000000000000000000000000000000"
      forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ ByteString -> Literal
bstr ByteString
"405000000000000000000000000000000000000000000000000000000087680203"
      forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ ByteString -> Literal
bstr ByteString
"506000000000000000000000000000000000000000000000000000000087680203"
      forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ ByteString -> Literal
bstr ByteString
"6070000000000000000000000000000000000000000000000000000000"
      forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ ByteString -> Literal
bstr ByteString
"7080000000000000000000000000000000000000000000000000000000"

reward_account :: Rule
reward_account :: Rule
reward_account =
  forall a. Text -> Named a -> Named a
comment
    [str|reward_account = bytes
        |]
    forall a b. (a -> b) -> a -> b
$ Text
"reward_account"
      forall a. IsType0 a => Text -> a -> Rule
=:= ByteString -> Literal
bstr ByteString
"E090000000000000000000000000000000000000000000000000000000"
      forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ ByteString -> Literal
bstr ByteString
"F0A0000000000000000000000000000000000000000000000000000000"

addr_keyhash :: Rule
addr_keyhash :: Rule
addr_keyhash = Text
"addr_keyhash" forall a. IsType0 a => Text -> a -> Rule
=:= Rule
hash28

pool_keyhash :: Rule
pool_keyhash :: Rule
pool_keyhash = Text
"pool_keyhash" forall a. IsType0 a => Text -> a -> Rule
=:= Rule
hash28

vrf_keyhash :: Rule
vrf_keyhash :: Rule
vrf_keyhash = Text
"vrf_keyhash" forall a. IsType0 a => Text -> a -> Rule
=:= Rule
hash32

--------------------------------------------------------------------------------
-- Crypto
--------------------------------------------------------------------------------

hash28 :: Rule
hash28 :: Rule
hash28 = Text
"$hash28" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
28 :: Word64)

hash32 :: Rule
hash32 :: Rule
hash32 = Text
"$hash32" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
32 :: Word64)

vkey :: Rule
vkey :: Rule
vkey = Text
"$vkey" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
32 :: Word64)

vrf_vkey :: Rule
vrf_vkey :: Rule
vrf_vkey = Text
"$vrf_vkey" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
32 :: Word64)

vrf_cert :: Rule
vrf_cert :: Rule
vrf_cert = Text
"$vrf_cert" forall a. IsType0 a => Text -> a -> Rule
=:= ArrayChoice -> ArrayChoice
arr [forall a e. (IsType0 a, IsGroupOrArrayEntry e) => a -> e
a Value ByteString
VBytes, forall a e. (IsType0 a, IsGroupOrArrayEntry e) => a -> e
a (Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
80 :: Word64))]

kes_vkey :: Rule
kes_vkey :: Rule
kes_vkey = Text
"$kes_vkey" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
32 :: Word64)

kes_signature :: Rule
kes_signature :: Rule
kes_signature = Text
"$kes_signature" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
448 :: Word64)

signkeyKES :: Rule
signkeyKES :: Rule
signkeyKES = Text
"signkeyKES" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
64 :: Word64)

signature :: Rule
signature :: Rule
signature = Text
"$signature" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
64 :: Word64)

--------------------------------------------------------------------------------
-- Utility
--------------------------------------------------------------------------------

big_int :: Rule
big_int :: Rule
big_int = Text
"big_int" forall a. IsType0 a => Text -> a -> Rule
=:= Value Int
VInt forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ Rule
big_uint forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ Rule
big_nint

big_uint :: Rule
big_uint :: Rule
big_uint = Text
"big_uint" forall a. IsType0 a => Text -> a -> Rule
=:= forall a. Word64 -> a -> Tagged a
tag Word64
2 Rule
bounded_bytes

big_nint :: Rule
big_nint :: Rule
big_nint = Text
"big_nint" forall a. IsType0 a => Text -> a -> Rule
=:= forall a. Word64 -> a -> Tagged a
tag Word64
3 Rule
bounded_bytes

-- Once https://github.com/input-output-hk/cuddle/issues/29 is in place, replace
-- with:
--
-- minInt64 :: Rule
-- minInt64 = "minInt64" =:= -9223372036854775808
minInt64 :: Integer
minInt64 :: Integer
minInt64 = -Integer
9223372036854775808

-- Once https://github.com/input-output-hk/cuddle/issues/29 is in place, replace
-- with:
--
-- maxInt64 :: Rule
-- maxInt64 = "maxInt64" =:= 9223372036854775807
maxInt64 :: Integer
maxInt64 :: Integer
maxInt64 = Integer
9223372036854775807

-- Once https://github.com/input-output-hk/cuddle/issues/29 is in place, replace
-- with:
--
-- maxWord64 :: Rule
-- maxWord64 = "maxWord64" =:= 18446744073709551615
maxWord64 :: Integer
maxWord64 :: Integer
maxWord64 = Integer
18446744073709551615

negInt64 :: Rule
negInt64 :: Rule
negInt64 = Text
"negInt64" forall a. IsType0 a => Text -> a -> Rule
=:= Integer
minInt64 Integer -> Integer -> Ranged
... (-Integer
1)

posInt64 :: Rule
posInt64 :: Rule
posInt64 = Text
"posInt64" forall a. IsType0 a => Text -> a -> Rule
=:= Integer
1 Integer -> Integer -> Ranged
... Integer
maxInt64

-- | this is the same as the current int64 definition but without zero
nonZeroInt64 :: Rule
nonZeroInt64 :: Rule
nonZeroInt64 = Text
"nonZeroInt64" forall a. IsType0 a => Text -> a -> Rule
=:= Rule
negInt64 forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ Rule
posInt64

int64 :: Rule
int64 :: Rule
int64 = Text
"int64" forall a. IsType0 a => Text -> a -> Rule
=:= Integer
minInt64 Integer -> Integer -> Ranged
... Integer
maxInt64

positive_int :: Rule
positive_int :: Rule
positive_int = Text
"positive_int" forall a. IsType0 a => Text -> a -> Rule
=:= Integer
1 Integer -> Integer -> Ranged
... Integer
18446744073709551615

unit_interval :: Rule
unit_interval :: Rule
unit_interval =
  forall a. Text -> Named a -> Named a
comment
    [str|The real unit_interval is: #6.30([uint, uint])
        |
        |A unit interval is a number in the range between 0 and 1, which
        |means there are two extra constraints:
        |  1. numerator <= denominator
        |  2. denominator > 0
        |
        |The relation between numerator and denominator can be
        |expressed in CDDL, but we have a limitation currently
        |(see: https://github.com/input-output-hk/cuddle/issues/30)
        |which poses a problem for testing. We need to be able to
        |generate random valid data for testing implementation of
        |our encoders/decoders. Which means we cannot use the actual
        |definition here and we hard code the value to 1/2
        |]
    forall a b. (a -> b) -> a -> b
$ Text
"unit_interval" forall a. IsType0 a => Text -> a -> Rule
=:= forall a. Word64 -> a -> Tagged a
tag Word64
30 (ArrayChoice -> ArrayChoice
arr [ArrayEntry
1, ArrayEntry
2])

-- | nonnegative_interval = tag 0 [uint, positive_int]
nonnegative_interval :: Rule
nonnegative_interval :: Rule
nonnegative_interval = Text
"nonnegative_interval" forall a. IsType0 a => Text -> a -> Rule
=:= forall a. Word64 -> a -> Tagged a
tag Word64
30 (ArrayChoice -> ArrayChoice
arr [forall a e. (IsType0 a, IsGroupOrArrayEntry e) => a -> e
a Value Int
VUInt, forall a e. (IsType0 a, IsGroupOrArrayEntry e) => a -> e
a Rule
positive_int])

bounded_bytes :: Rule
bounded_bytes :: Rule
bounded_bytes =
  forall a. Text -> Named a -> Named a
comment
    [str|The real bounded_bytes does not have this limit. it instead has
        |a different limit which cannot be expressed in CDDL.
        |
        |The limit is as follows:
        | - bytes with a definite-length encoding are limited to size 0..64
        | - for bytes with an indefinite-length CBOR encoding, each chunk is
        |   limited to size 0..64
        | ( reminder: in CBOR, the indefinite-length encoding of
        | bytestrings consists of a token #2.31 followed by a sequence
        | of definite-length encoded bytestrings and a stop code )
        |]
    forall a b. (a -> b) -> a -> b
$ Text
"bounded_bytes" forall a. IsType0 a => Text -> a -> Rule
=:= Value ByteString
VBytes forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
0 :: Word64, Word64
64 :: Word64)

distinct :: IsSizeable s => Value s -> Rule
distinct :: forall s. IsSizeable s => Value s -> Rule
distinct Value s
x =
  forall a. Text -> Named a -> Named a
comment
    [str|A type for distinct values.
        |The type parameter must support .size, for example: bytes or uint
        |]
    forall a b. (a -> b) -> a -> b
$ Text
"distinct_"
      forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (forall a. Show a => a -> String
show Value s
x)
        forall a. IsType0 a => Text -> a -> Rule
=:= (Value s
x forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
8 :: Word64))
        forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ (Value s
x forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
16 :: Word64))
        forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ (Value s
x forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
20 :: Word64))
        forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ (Value s
x forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
24 :: Word64))
        forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ (Value s
x forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
30 :: Word64))
        forall a c b.
(IsChoosable a c, IsChoosable b c) =>
a -> b -> Choice c
/ (Value s
x forall a s. (IsSizeable a, IsSize s) => Value a -> s -> Constrained
`sized` (Word64
32 :: Word64))