Use Cuddle to define CDDL in Shelley #4552

nc6 · 2024-08-15T11:11:48Z

Description

This addresses issue #4462

Moves some core type CDDL definitions to cardano-ledger-core
Defines Shelley CDDL types through Huddle
Adds huddle-based testing in Shelley
Moves the Shelley CDDL to being auto-generated via the Huddle def
Updates Conway to use some definitions from Shelley where they were unchanged
Updates the gen-cddl.sh script to check Shelley definitions

One unexpected change: the huddle definition for protocol_param_updates has a size limit on the max block header size. This is consistent with the Haskell serialisers and data structure.

Checklist

Commit sequence broadly makes sense and commits have useful messages
New tests are added if needed and existing tests are updated
All visible changes are prepended to the latest section of a CHANGELOG.md for the affected packages.
New section is never added with the code changes. (See RELEASING.md)
When applicable, versions are updated in .cabal and CHANGELOG.md files according to the
versioning process.
The version bounds in .cabal files for all affected packages are updated.
If you change the bounds in a cabal file, that package itself must have a version increase. (See RELEASING.md)
Code is formatted with fourmolu (use scripts/fourmolize.sh)
Cabal files are formatted (use scripts/cabal-format.sh)
hie.yaml has been updated (use scripts/gen-hie.sh)
Self-reviewed the diff

Now that the CDDL is defined with Cuddle, we can begin to properly modularise it. As a first step, we move the common crypto and utility types into the core package.

- Switch existing tests to using the generated CDDL - Add additional Huddle based tests for Shelley types - Add a tool to regenerate the Shelley CDDL from Huddle - Move additional core types to the core CDDL - Make a few fixes in the Shelley Huddle spec There is one unusual thing here: the size bound on the max block header size in the protocol param update. This does not reflect the original CDDL, but it is consistent with the FromCBOR instance and the underlying data type in PParams. I can only assume that the CDDL generator wasn't exploring the whole range and thus never found this error.

Now that Shelley is defined using Huddle, we can rely on the relevant parts from Conway.

lehins

This looks awesome. I am loving seeing CDDL specified in Haskell 😄

lehins · 2024-08-21T00:24:03Z

eras/shelley/impl/cddl-files/shelley.cddl

+protocol_param_update = {? 0 : uint
+                         , ? 1 : uint
+                         , ? 2 : uint
+                         , ? 3 : uint
+                         , ? 4 : uint .size 2
+                         , ? 5 : coin
+                         , ? 6 : coin
+                         , ? 7 : epoch
+                         , ? 8 : uint
+                         , ? 9 : nonnegative_interval
+                         , ? 10 : unit_interval
+                         , ? 11 : unit_interval
+                         , ? 12 : unit_interval
+                         , ? 13 : nonce
+                         , ? 14 : [protocol_version]


All of the comments have disappeared, which were very useful

Most of the comments will come back with #4553. But yes, at the moment, comments are only supported on rules, not on arbitrary CDDL sections. I will have a think about how best to bring this back - input-output-hk/cuddle#36

lehins · 2024-08-23T22:43:56Z

libs/cardano-ledger-core/testlib/Test/Cardano/Ledger/Core/Binary/CDDL.hs

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


Convert this into CDDL comment

Done in #4553

lehins · 2024-08-23T22:45:55Z

libs/cardano-ledger-core/testlib/Test/Cardano/Ledger/Core/Binary/CDDL.hs

+unit_interval :: Rule
+unit_interval = "unit_interval" =:= tag 30 (arr [1, 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


Convert it to CDDL comment

Done in #4553

lehins · 2024-08-23T22:47:16Z

libs/cardano-ledger-core/testlib/Test/Cardano/Ledger/Core/Binary/CDDL.hs

+set :: IsType0 t0 => t0 -> GRuleCall
+set = binding $ \x -> "set" =:= tag 258 (arr [0 <+ a x]) / sarr [0 <+ a x]


This definition should live in cardano-ledger-conway, since it is not valid for all previous eras.

More over it will also change in the next era, because tag 258 will become mandatory

lehins · 2024-08-23T22:47:26Z

libs/cardano-ledger-core/testlib/Test/Cardano/Ledger/Core/Binary/CDDL.hs

+-- Conway era introduces an optional 258 tag for sets, which will become mandatory in the
+-- second era after Conway. We recommend all the tooling to account for this future breaking
+-- change sooner rather than later, in order to provide a smooth transition for their users.


Convert to CDDL comment

lehins · 2024-08-24T00:06:19Z

eras/shelley/impl/cddl-files/shelley.cddl

+
+pool_metadata = [url, metadata_hash]
+
+pool_params = (pool_keyhash


Am I right in assuming that key+value syntax is not supported by huddle?

Suggested change

pool_params = (pool_keyhash

pool_params = (operator: pool_keyhash

It is supported, but not for named groups (only for maps). input-output-hk/cuddle#32

lehins · 2024-08-24T00:08:46Z

eras/shelley/impl/cddl-files/shelley.cddl

+                         , ? 10 : unit_interval
+                         , ? 11 : unit_interval
+                         , ? 12 : unit_interval
+                         , ? 13 : nonce


I don't remember the distinction between the two, but this has changed from previous spec. Was this desired?

Suggested change

, ? 13 : nonce

, ? 13 : $nonce

lehins · 2024-08-24T00:10:11Z

eras/shelley/impl/cddl-files/shelley.cddl


-vkeywitness = [ $vkey, $signature ]
+multi_host_name = (2, dns_name)


Lost comment

lehins · 2024-08-24T00:12:26Z

eras/shelley/impl/cddl-files/shelley.cddl


-transaction_index = uint .size 2
+$hash32 = bytes .size 32


What is the difference in syntax between = and /=?

Suggested change

$hash32 = bytes .size 32

$hash32 /= bytes .size 32

For both type choices and group choices, additional alternatives can be added to a rule later in separate rules by using "/=" and "//=", respectively, instead of "=": attire /= "swimwear" delivery //= ( lat: float, long: float, drone-type: tstr ) It is not an error if a name is first used with a "/=" or "//=" (there is no need to "create it" with "=").

So basically CDDL supports ad-hoc extending choices. Huddle does not support this. In any case, these definitions are the only definitions, so the use of /= is meaningless.

lehins · 2024-08-26T14:48:51Z

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/CDDL.hs

 import Data.Word (Word64)
 import GHC.Num (Integer)
-import GHC.Show (Show (show))
+import Test.Cardano.Ledger.Core.Binary.CDDL


We've just made a release, so addition of a new module will require a minor version bump for:

cardano-ledger-shelley-1.13.1.0

cardano-ledger-conway-1.16.2.0

cardano-ledger-core-1.14.1.0

Also, the lower bounds will need to be adjusted accordingly

nc6 · 2024-08-28T11:50:11Z

Closing this in favour of #4553

nc6 requested a review from lehins August 15, 2024 11:11

nc6 force-pushed the nc/4462 branch 2 times, most recently from b890871 to c788d10 Compare August 16, 2024 08:11

nc6 mentioned this pull request Aug 16, 2024

Address issues in auto-generated CDDL specification #4553

Merged

9 tasks

nc6 force-pushed the nc/4462 branch from c788d10 to e165d4e Compare August 16, 2024 12:10

nc6 and others added 7 commits August 19, 2024 10:11

Move extras and crypto types to core CDDL

2a9488c

Now that the CDDL is defined with Cuddle, we can begin to properly modularise it. As a first step, we move the common crypto and utility types into the core package.

Define Shelley CDDL via Huddle

ed05a18

Use common CDDL definitions from Shelley.

529bdd3

Now that Shelley is defined using Huddle, we can rely on the relevant parts from Conway.

Fourmolu

16106f4

Update gen-cddl script to handle multiple eras

9c7954d

Update hie file.

f87081c

nc6 force-pushed the nc/4462 branch from e165d4e to f87081c Compare August 19, 2024 09:38

nc6 mentioned this pull request Aug 21, 2024

Define CDDL via Huddle in shelley-ma #4557

Merged

9 tasks

lehins requested changes Aug 26, 2024

View reviewed changes

lehins mentioned this pull request Aug 27, 2024

Why remove documentation of script_data_hash in conway CDDL? #4556

Closed

nc6 closed this Aug 28, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use Cuddle to define CDDL in Shelley #4552

Use Cuddle to define CDDL in Shelley #4552

nc6 commented Aug 15, 2024

lehins left a comment

lehins Aug 21, 2024

nc6 Aug 26, 2024

lehins Aug 23, 2024

nc6 Aug 26, 2024

lehins Aug 23, 2024

nc6 Aug 26, 2024

lehins Aug 23, 2024

lehins Aug 23, 2024

lehins Aug 24, 2024

nc6 Aug 26, 2024

lehins Aug 24, 2024

lehins Aug 24, 2024

lehins Aug 24, 2024

nc6 Aug 26, 2024

lehins Aug 26, 2024

nc6 commented Aug 28, 2024

		set :: IsType0 t0 => t0 -> GRuleCall
		set = binding $ \x -> "set" =:= tag 258 (arr [0 <+ a x]) / sarr [0 <+ a x]


		pool_metadata = [url, metadata_hash]

		pool_params = (pool_keyhash

	pool_params = (pool_keyhash
	pool_params = (operator: pool_keyhash


		vkeywitness = [ $vkey, $signature ]
		multi_host_name = (2, dns_name)

Use Cuddle to define CDDL in Shelley #4552

Use Cuddle to define CDDL in Shelley #4552

Conversation

nc6 commented Aug 15, 2024

Description

Checklist

lehins left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nc6 commented Aug 28, 2024