Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow 'sized' to operate on references in huddle #31

Closed
nc6 opened this issue Jul 4, 2024 · 0 comments
Closed

Allow 'sized' to operate on references in huddle #31

nc6 opened this issue Jul 4, 2024 · 0 comments
Labels
Huddle Issues relating to the Huddle language

Comments

@nc6
Copy link
Collaborator

nc6 commented Jul 4, 2024

Currently sized is specialised to operate on values:

-- | Declare a size constraint on an int-style type.
sized :: (IsSizeable a, IsSize s) => Value a -> s -> Constrained

This is nice in terms of preventing invalid use, but it prevents the use of sized on references, including on generic args where we might not know the suitability of the operator. So alas we need to liberalise it.

@nc6 nc6 added the Huddle Issues relating to the Huddle language label Jul 4, 2024
nc6 added a commit to IntersectMBO/cardano-ledger that referenced this issue Jul 5, 2024
This is the final set of changes to the Conway
CDDL spec made via comparison with the original
cddl files for Conway.

As of this commit, the remaining changes with the
original cddl are as follows:

- Various fields in crypto were defined with /=
  and are now defined with =. This does not affect
  the semantics, being instead a convention as per
  https://datatracker.ietf.org/doc/html/rfc8610#section-3.9
- The index keys in auxiliary_data are written as
  if they were value and not type keys:
  ```
    39,43c30,34
      <                   / #6.259({? 0 : metadata
      <                             , ? 1 : [* native_script]
      <                             , ? 2 : [* plutus_v1_script]
      <                             , ? 3 : [* plutus_v2_script]
      <                             , ? 4 : [* plutus_v3_script]})
      ---
      >                   / #6.259({? 0 => metadata
      >                             , ? 1 => [* native_script]
      >                             , ? 2 => [* plutus_v1_script]
      >                             , ? 3 => [* plutus_v2_script]
      >                             , ? 4 => [* plutus_v3_script]})
  ```
  This is a simpler formulation with identical semantics.
- The alternatives in 'certificate', 'relay',
  'native_script' and 'gov_action' are encoded
  using type1 choice semantics ('/') rather than
  group choice semantics ('//'). In the context,
  this is an equivalent formulation.
- nonempty_oset has been removed, pending
  explanation of what it means. nonempty_set is
  used instead.
- In various places, null is replaced with nil.
  They are synonyms.
- The names of type parameters are changed;
  typically a is replaced with a0.
- A few rules using references as the bounds in
  ranges are now inlined. This will be fixed once
  input-output-hk/cuddle#29
  is addressed.
- `distinct` is not currently possible to
  implement as a generic function, since `sized`
  is currently specialised to work on values.
  input-output-hk/cuddle#31
  addresses. Until this is fixed, distinct<bytes>
  is instead distinct_bytes.
- tstr is replaced with text. They are synonyms.
- The keys in the 'pool_params' and
  'script_n_of_k' groups are lost. This is due to
  input-output-hk/cuddle#32.
  However, since pool_params is included into an
  array, this does not alter the semantics, only
  the documentation.
- datum_hash is of type datum_hash, not hash32.
  This seems an overlooked item in the original
  cddl.
nc6 added a commit to IntersectMBO/cardano-ledger that referenced this issue Jul 25, 2024
This is the final set of changes to the Conway
CDDL spec made via comparison with the original
cddl files for Conway.

As of this commit, the remaining changes with the
original cddl are as follows:

- Various fields in crypto were defined with /=
  and are now defined with =. This does not affect
  the semantics, being instead a convention as per
  https://datatracker.ietf.org/doc/html/rfc8610#section-3.9
- The index keys in auxiliary_data are written as
  if they were value and not type keys:
  ```
    39,43c30,34
      <                   / #6.259({? 0 : metadata
      <                             , ? 1 : [* native_script]
      <                             , ? 2 : [* plutus_v1_script]
      <                             , ? 3 : [* plutus_v2_script]
      <                             , ? 4 : [* plutus_v3_script]})
      ---
      >                   / #6.259({? 0 => metadata
      >                             , ? 1 => [* native_script]
      >                             , ? 2 => [* plutus_v1_script]
      >                             , ? 3 => [* plutus_v2_script]
      >                             , ? 4 => [* plutus_v3_script]})
  ```
  This is a simpler formulation with identical semantics.
- The alternatives in 'certificate', 'relay',
  'native_script' and 'gov_action' are encoded
  using type1 choice semantics ('/') rather than
  group choice semantics ('//'). In the context,
  this is an equivalent formulation.
- nonempty_oset has been removed, pending
  explanation of what it means. nonempty_set is
  used instead.
- In various places, null is replaced with nil.
  They are synonyms.
- The names of type parameters are changed;
  typically a is replaced with a0.
- A few rules using references as the bounds in
  ranges are now inlined. This will be fixed once
  input-output-hk/cuddle#29
  is addressed.
- `distinct` is not currently possible to
  implement as a generic function, since `sized`
  is currently specialised to work on values.
  input-output-hk/cuddle#31
  addresses. Until this is fixed, distinct<bytes>
  is instead distinct_bytes.
- tstr is replaced with text. They are synonyms.
- The keys in the 'pool_params' and
  'script_n_of_k' groups are lost. This is due to
  input-output-hk/cuddle#32.
  However, since pool_params is included into an
  array, this does not alter the semantics, only
  the documentation.
- datum_hash is of type datum_hash, not hash32.
  This seems an overlooked item in the original
  cddl.
Soupstraw pushed a commit to IntersectMBO/cardano-ledger that referenced this issue Aug 1, 2024
This is the final set of changes to the Conway
CDDL spec made via comparison with the original
cddl files for Conway.

As of this commit, the remaining changes with the
original cddl are as follows:

- Various fields in crypto were defined with /=
  and are now defined with =. This does not affect
  the semantics, being instead a convention as per
  https://datatracker.ietf.org/doc/html/rfc8610#section-3.9
- The index keys in auxiliary_data are written as
  if they were value and not type keys:
  ```
    39,43c30,34
      <                   / #6.259({? 0 : metadata
      <                             , ? 1 : [* native_script]
      <                             , ? 2 : [* plutus_v1_script]
      <                             , ? 3 : [* plutus_v2_script]
      <                             , ? 4 : [* plutus_v3_script]})
      ---
      >                   / #6.259({? 0 => metadata
      >                             , ? 1 => [* native_script]
      >                             , ? 2 => [* plutus_v1_script]
      >                             , ? 3 => [* plutus_v2_script]
      >                             , ? 4 => [* plutus_v3_script]})
  ```
  This is a simpler formulation with identical semantics.
- The alternatives in 'certificate', 'relay',
  'native_script' and 'gov_action' are encoded
  using type1 choice semantics ('/') rather than
  group choice semantics ('//'). In the context,
  this is an equivalent formulation.
- nonempty_oset has been removed, pending
  explanation of what it means. nonempty_set is
  used instead.
- In various places, null is replaced with nil.
  They are synonyms.
- The names of type parameters are changed;
  typically a is replaced with a0.
- A few rules using references as the bounds in
  ranges are now inlined. This will be fixed once
  input-output-hk/cuddle#29
  is addressed.
- `distinct` is not currently possible to
  implement as a generic function, since `sized`
  is currently specialised to work on values.
  input-output-hk/cuddle#31
  addresses. Until this is fixed, distinct<bytes>
  is instead distinct_bytes.
- tstr is replaced with text. They are synonyms.
- The keys in the 'pool_params' and
  'script_n_of_k' groups are lost. This is due to
  input-output-hk/cuddle#32.
  However, since pool_params is included into an
  array, this does not alter the semantics, only
  the documentation.
- datum_hash is of type datum_hash, not hash32.
  This seems an overlooked item in the original
  cddl.
nc6 added a commit that referenced this issue Nov 22, 2024
Before this commit, it wasn't possible to apply constraints (e.g.
'.size') to references, only directly to Value types. This gives us some
nice type safety (you can't apply '.cbor' to an integer, for example),
it also doesn't allow us to constrain types which are passed as generic
parameters, or where we genuinely want to constrain another rule.

This commit changes that by allowing references (both direct and
generic) to be constrained. Obviously we don't have any guarantees here
that what we are constraining makes sense, but we never had that in CDDL
anyway. And we retain the type safety for anything that _isn't_ a
reference.

This resolves issue #31
@nc6 nc6 closed this as completed Nov 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Huddle Issues relating to the Huddle language
Projects
None yet
Development

No branches or pull requests

1 participant