EverCDDL crashes on cddl specification

[facundominguez]

The following input causes CDDL.exe to crash, probably because it runs out of memory. The RSS grows beyond 150G at least.

Details

bootstrap_witness =
  [ public_key : vkey
  , signature  : signature
  , chain_code : bytes .size 32
  , attributes : bytes
  ]

block_number = uint .size 8

slot = uint .size 8

hash32 = bytes .size 32

vkey = bytes .size 32

vrf_vkey = bytes .size 32

vrf_cert = [bytes, bytes .size 80]


operational_cert = 
  ( hot_vkey        : kes_vkey       
  , sequence_number : sequence_number
  , kes_period      : kes_period     
  , sigma           : signature      
  )

kes_vkey = bytes .size 32

sequence_number = uint .size 8

kes_period = uint .size 8

protocol_version = (major_protocol_version, uint)

major_protocol_version = 0 .. 3

kes_signature = bytes .size 448

signature = bytes .size 64

bytes = bstr
bstr = #2
uint = #0

These are the reproduction steps:

nix-shell -p podman --run 'podman run --rm -v $PWD:/mnt/cddl_test ghcr.io/project-everest/everparse:v2025.10.06 "bin/cddl.exe /mnt/cddl_test/test.cddl"'

This is tested in Nixos 25.11.

Here's the output:

Details

Running: '/mnt/everparse/opt/FStar/out/bin/fstar.exe' '--locate_z3' '4.13.3' >'/dev/null' 2>&1
Success, output F* to: /tmp/evercddl_362_1765284662.tmp/CDDLTest.Test.fst
Running: '/mnt/everparse/opt/FStar/out/bin/fstar.exe' '/tmp/evercddl_362_1765284662.tmp/CDDLTest.Test.fst' '--cache_dir' '/tmp/evercddl_362_1765284662.tmp' '--already_cached' '*,-CDDLTest.Test' '--z3version' '4.13.3' '--cache_checked_modules' '--warn_error' '@241' '--cmi' '--ext' 'context_pruning' '--load_cmxs' 'evercddl_lib' '--load_cmxs' 'evercddl_plugin' '--include' '/mnt/everparse/src/cbor/spec' '--include' '/mnt/everparse/src/cbor/pulse' '--include' '/mnt/everparse/src/cddl/spec' '--include' '/mnt/everparse/src/cddl/pulse' '--include' '/mnt/everparse/src/cddl/tool' '--include' '/mnt/everparse/opt/karamel/krmllib' '--include' '/mnt/everparse/opt/karamel/krmllib/obj' '--include' '/mnt/everparse/opt/pulse/out/lib/pulse' '--include' '/mnt/everparse/lib/evercddl/lib' '--include' '/mnt/everparse/lib/evercddl/plugin'
* Warning 274:
  - Implicitly opening namespace 'cddl.pulse.ast.det.' shadows module 'c'
    in file "/mnt/everparse/opt/karamel/krmllib/C.fst".
  - Rename "/mnt/everparse/opt/karamel/krmllib/C.fst" to avoid conflicts.

TAC>> 20 defs remaining. Producing definitions for bool
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 19 defs remaining. Producing definitions for everparse-no-match
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 18 defs remaining. Producing definitions for uint
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 17 defs remaining. Producing definitions for bstr
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 16 defs remaining. Producing definitions for bytes
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 15 defs remaining. Producing definitions for signature
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 14 defs remaining. Producing definitions for kes_signature
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 13 defs remaining. Producing definitions for major_protocol_version
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 12 defs remaining. Producing definitions for protocol_version
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 11 defs remaining. Producing definitions for kes_period
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 10 defs remaining. Producing definitions for sequence_number
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 9 defs remaining. Producing definitions for kes_vkey
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 8 defs remaining. Producing definitions for operational_cert
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 7 defs remaining. Producing definitions for vrf_cert
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 6 defs remaining. Producing definitions for vrf_vkey
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 5 defs remaining. Producing definitions for vkey
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 4 defs remaining. Producing definitions for hash32
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 3 defs remaining. Producing definitions for slot
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 2 defs remaining. Producing definitions for block_number
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
TAC>> 1 defs remaining. Producing definitions for bootstrap_witness
TAC>> owf'
TAC>> owf
TAC>> wf'
TAC>> wf
TAC>> validator
TAC>> bundle
TAC>> type
TAC>> teq
TAC>> prettify impl
TAC>> spec type
TAC>> specteq
TAC>> prettify spec
TAC>> relteq
TAC>> rel
TAC>> releq
TAC>> grelteq
TAC>> greleq
TAC>> specteq
TAC>> gspecteq
TAC>> teq
TAC>> gteq
TAC>> parser
TAC>> bundle'
TAC>> env'
TAC>> ancillary envs
TAC>> source'
Verified module: CDDLTest.Test
All verification conditions discharged successfully
Running: '/mnt/everparse/opt/FStar/out/bin/fstar.exe' '/tmp/evercddl_362_1765284662.tmp/CDDLTest.Test.fst' '--cache_dir' '/tmp/evercddl_362_1765284662.tmp' '--odir' '/tmp/evercddl_362_1765284662.tmp' '--already_cached' '*,' '--codegen' 'krml' '--extract_module' 'CDDLTest.Test' '--z3version' '4.13.3' '--cache_checked_modules' '--warn_error' '@241' '--cmi' '--ext' 'context_pruning' '--load_cmxs' 'evercddl_lib' '--load_cmxs' 'evercddl_plugin' '--include' '/mnt/everparse/src/cbor/spec' '--include' '/mnt/everparse/src/cbor/pulse' '--include' '/mnt/everparse/src/cddl/spec' '--include' '/mnt/everparse/src/cddl/pulse' '--include' '/mnt/everparse/src/cddl/tool' '--include' '/mnt/everparse/opt/karamel/krmllib' '--include' '/mnt/everparse/opt/karamel/krmllib/obj' '--include' '/mnt/everparse/opt/pulse/out/lib/pulse' '--include' '/mnt/everparse/lib/evercddl/lib' '--include' '/mnt/everparse/lib/evercddl/plugin'
* Warning 274:
  - Implicitly opening namespace 'cddl.pulse.ast.det.' shadows module 'c'
    in file "/mnt/everparse/opt/karamel/krmllib/C.fst".
  - Rename "/mnt/everparse/opt/karamel/krmllib/C.fst" to avoid conflicts.

Killed
Extraction to krml failed

[tahina-pro]

Thanks for reporting! This seems to be caused by the F* normalizer when extracting EverCDDL-generated definitions to krml. We have a fix proposal in the works, we'll keep you posted.

[tahina-pro]

We are still working on a fix, but in the meantime, I am going to add just added a temporary option to cddl.exe (--__tmp_no_nbe) to control the F* normalizer during extraction. That option will make your example work.

[facundominguez]

Thanks for the update @tahina-pro. I'm leaving a larger crashing example for the testing here.

Details

block =
  [ header
  , transaction_bodies       : [* transaction_body]
  , transaction_witness_sets : [* transaction_witness_set]
  , transaction_metadata_set : {* transaction_index => metadata}
  ]

header = [header_body, body_signature : kes_signature]


header_body =
  [ block_number      : block_number
  , slot              : slot
  , prev_hash         : hash32/ nil
  , issuer_vkey       : vkey
  , vrf_vkey          : vrf_vkey
  , nonce_vrf         : vrf_cert
  , leader_vrf        : vrf_cert
  , block_body_size   : uint .size 4
  , block_body_hash   : hash32
  , operational_cert
  , protocol_version
  ]


block_number = uint .size 8

slot = uint .size 8

hash32 = bytes .size 32

vkey = bytes .size 32

vrf_vkey = bytes .size 32

vrf_cert = [bytes, bytes .size 80]


kes_vkey = bytes .size 32

sequence_number = uint .size 8

kes_period = uint .size 8

signature = bytes .size 64

protocol_version = (major_protocol_version, uint)

major_protocol_version = 0 .. 3

kes_signature = bytes .size 448

transaction_body =
; EverCDDL does not support generics
; {   0 : set<transaction_input>
  {   0 : [* transaction_input]
  ,   1 : [* transaction_output]
  ,   2 : coin
  ,   3 : slot
  , ? 4 : [* certificate]
  , ? 5 : withdrawals
  , ? 6 : update
  , ? 7 : auxiliary_data_hash
  }

; EverCDDL does not support generics
; set<a0> = [* a0]

transaction_input = [id : transaction_id, index : uint .size 2]

transaction_id = hash32

transaction_output = [address, amount : coin]

; 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
; EverCDDL cannot parse h'... syntax
; address =
;  h'001000000000000000000000000000000000000000000000000000000011000000000000000000000000000000000000000000000000000000'
;  / h'102000000000000000000000000000000000000000000000000000000022000000000000000000000000000000000000000000000000000000'
;  / h'203000000000000000000000000000000000000000000000000000000033000000000000000000000000000000000000000000000000000000'
;  / h'304000000000000000000000000000000000000000000000000000000044000000000000000000000000000000000000000000000000000000'
;  / h'405000000000000000000000000000000000000000000000000000000087680203'
;  / h'506000000000000000000000000000000000000000000000000000000087680203'
;  / h'6070000000000000000000000000000000000000000000000000000000'
;  / h'7080000000000000000000000000000000000000000000000000000000'
address = bytes

coin = uint

certificate =
  [  account_registration_cert
  // account_unregistration_cert
  // delegation_to_stake_pool_cert
  // pool_registration_cert
  // pool_retirement_cert
  // genesis_delegation_cert
  // move_instantaneous_rewards_cert
  ]

; This certificate will be deprecated in a future era
account_registration_cert = (0, stake_credential)

stake_credential = credential

credential = [0, addr_keyhash// 1, script_hash]

addr_keyhash = hash28

hash28 = bytes .size 28

; To compute a script hash, note that you must prepend
; a tag to the bytes of the script before hashing.
; The tag is determined by the language.
; The tags are:
;   "\x00" for multisig/native scripts
;   "\x01" for Plutus V1 scripts
;   "\x02" for Plutus V2 scripts
;   "\x03" for Plutus V3 scripts
;   "\x04" for Plutus V4 scripts
script_hash = hash28

; This certificate will be deprecated in a future era
account_unregistration_cert = (1, stake_credential)

delegation_to_stake_pool_cert = (2, stake_credential, pool_keyhash)

pool_keyhash = hash28

pool_registration_cert = (3, pool_params)

; Pool parameters for stake pool registration
pool_params =
  ( operator       : pool_keyhash
  , vrf_keyhash    : vrf_keyhash
  , pledge         : coin
  , cost           : coin
  , margin         : unit_interval
  , reward_account : reward_account
; EverCDDL does not support generics
; , pool_owners    : set<addr_keyhash>
  , pool_owners    : [* addr_keyhash]
  , relays         : [* relay]
  , pool_metadata  : pool_metadata/ nil
  )

vrf_keyhash = hash32

; 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
unit_interval = #6.30([1, 2])
;
reward_account = bytes
; EverCDDL cannot parse h'...
; reward_account =
;   h'E090000000000000000000000000000000000000000000000000000000'
;   / h'F0A0000000000000000000000000000000000000000000000000000000'

relay = [single_host_addr// single_host_name// multi_host_name]

single_host_addr = (0, port/ nil, ipv4/ nil, ipv6/ nil)
;
; EverCDDL does not support .le
; port = uint .le 65535
port = uint .size 2

ipv4 = bytes .size 4

ipv6 = bytes .size 16

; dns_name: An A or AAAA DNS record
single_host_name = (1, port/ nil, dns_name)

dns_name = text .size (0 .. 64)

; dns_name: An SRV DNS record
multi_host_name = (2, dns_name)

pool_metadata = [url, bytes]

url = text .size (0 .. 64)

pool_retirement_cert = (4, pool_keyhash, epoch)

epoch = uint .size 8

genesis_delegation_cert = (5, genesis_hash, genesis_delegate_hash, vrf_keyhash)

genesis_hash = hash28

genesis_delegate_hash = hash28

move_instantaneous_rewards_cert = (6, move_instantaneous_reward)

; The first field determines where the funds are drawn from.
;   0 denotes the reserves,
;   1 denotes the treasury.
; If the second field is a map, funds are moved to stake credentials.
; Otherwise, the funds are given to the other accounting pot.
; NOTE:
;   This has been safely backported to Shelley from Alonzo.
move_instantaneous_reward = [0/ 1, {* stake_credential => delta_coin}/ coin]
;
; This too has been introduced in Shelley as a backport from Alonzo.
delta_coin = int

withdrawals = {* reward_account => coin}

update = [proposed_protocol_parameter_updates, epoch]

proposed_protocol_parameter_updates = {* genesis_hash => protocol_param_update}

protocol_param_update =
  { ? 0  : uint                   ; minfee A
  , ? 1  : uint                   ; minfee B
  , ? 2  : uint                   ; max block body size
  , ? 3  : uint                   ; max transaction size
  , ? 4  : uint .size 2           ; max block header size
  , ? 5  : coin                   ; key deposit
  , ? 6  : coin                   ; pool deposit
  , ? 7  : epoch_interval         ; maximum epoch
  , ? 8  : uint .size 2           ; n_opt: desired number of stake pools
  , ? 9  : nonnegative_interval   ; pool pledge influence
  , ? 10 : unit_interval          ; expansion rate
  , ? 11 : unit_interval          ; treasury growth rate
  , ? 12 : unit_interval          ; decentralization constant
  , ? 13 : nonce                  ; extra entropy
  , ? 14 : [protocol_version]     ; protocol version
  , ? 15 : coin                   ; min utxo value
  , ? 16 : coin                   ; min pool cost
  }


epoch_interval = uint .size 4

nonnegative_interval = #6.30([uint, positive_int])

positive_int = 1 .. max_word64

max_word64 = 18446744073709551615

nonce = [0// 1, hash32]

auxiliary_data_hash = hash32

transaction_witness_set =
  {? 0 : [* vkeywitness], ? 1 : [* native_script], ? 2 : [* bootstrap_witness]}

vkeywitness = [vkey, signature]

; Native scripts support 4 operations:
;   - Signature verification (script_pubkey)
;   - Conjunctions (script_all)
;   - Disjunctions (script_any)
;   - M-of-N thresholds (script_n_of_k)
;
; Note: Shelley uses VUInt for the threshold in script_n_of_k.
;
; EverCDDL is rejecting recursive definitions like native_script at the moment
;
; script_pubkey = (0, addr_keyhash)
; script_all = (1, [* native_script])
; script_any = (2, [* native_script])
; script_n_of_k = (3, n : uint, [* native_script])
; native_script = [script_pubkey // script_all // script_any // script_n_of_k]

native_script = uint;


bootstrap_witness =
  [ public_key : vkey
  , signature  : signature
  , chain_code : bytes .size 32
  , attributes : bytes
  ]


operational_cert =
  ( hot_vkey        : kes_vkey
  , sequence_number : sequence_number
  , kes_period      : kes_period
  , sigma           : signature
  )

transaction_index = uint .size 2


metadata = {* metadatum_label => metadatum}

metadatum_label = uint .size 8

; EverCDDL is rejecting recursive definitions like metadatum at the moment
; metadatum =
;   {* metadatum => metadatum}
;   / [* metadatum]
;   / int
;   / bytes .size (0 .. 64)
;   / text .size (0 .. 64)

metadatum = int

transaction = [transaction_body, transaction_witness_set, metadata/ nil]

signkey_kes = bytes .size 64



bytes = bstr
bstr = #2
uint = #0
nint = #1
int = uint / nint

tstr = #3
text = tstr

false = #7.20
true = #7.21
null = nil
nil = #7.22
undefined = #7.23

any = #