{-# 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 Data.String.Here (here)
import qualified Data.Text as T
import Data.Word (Word64)
import GHC.Show (Show (show))
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
    [here|
    address = bytes
    reward_account = 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 =
  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

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 -- this is the same as the current int64 definition but without zero

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 = 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])

-- unit_interval = tag 0 [uint, uint]
--
-- Comment above depicts the actual definition for `unit_interval`.
--
-- Unit interval is a number in the range between 0 and 1, which
-- means there are two extra constraints:
-- \* numerator <= denominator
-- \* denominator > 0
--
-- Relation between numerator and denominator cannot be expressed in CDDL, 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

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

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

-- a type for distinct values.
-- The type parameter must support .size, for example: bytes or uint
distinct :: IsSizeable s => Value s -> Rule
distinct :: forall s. IsSizeable s => Value s -> Rule
distinct Value s
x =
  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))