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

Generalize Contract #135

Open
wants to merge 5 commits into
base: master
Choose a base branch
from

Conversation

edsko
Copy link

@edsko edsko commented Sep 9, 2022

This PR makes three changes:

  1. As a preliminary step, it enables -Wall and gives a few modules some export lists. This helped me understand what exactly was the expected interface of these modules. It's possible I should have exported a few more things. (If it's preferred, I can also remove the export lists again now that they served their purpose).
  2. The main event: generalize Contract and everything related over the type of identity i (here, that was ByteString; in marlowe-cardano, that would be PubKeyHash), and the token of tokens t (by default Token). See commit message for further detail.
  3. Split off the definition of the language into a library, which is then used by the executable.

This PR comes after an older one against marlowe-cardano (input-output-hk/marlowe-cardano#182), along with a comment there from @hrajchert that that work would have been better done against this repo. At the time I thought that would not be an option for us, as we needed the generalization also in the Plutus interpreter, but we have since realized that we can avoid that. Moreover, the marlowe repo now seems to be in line with the marlowe-cardano in terms of the language (concretely, merkleization is supported and it uses POSXTIme instead of slots). These two things together mean that it might indeed be feasible for us to use this repo instead.

This helps understand the public surface of the `Semantics` module.
This introduces two type parameters `i` and `t` that generalize over the
type of identity (`ByteString` in `marlowe`, `PubKeyHash` in
`marlowe-cardano`) and token (`Token` by default). Nothing in the
language definition actually cares what these two types are.

For the main definitions in each module, I've introduced a new
"generalized" function (e.g., `computeTransaction'`), and then defined
the "old" function (e.g., `computeTransaction`) in terms of that more
general one.

I have also generalized all the examples; the examples don't care what
`i` and `t` are either, _except_ that they often hardcode a choice of
`ada` as the token; but this doesn't change the examples at all. So for
the examples I've added a separate token type as an additional argument.
(The examples always use roles, so they really are polymorphic in `i`.)
@edsko edsko marked this pull request as draft September 9, 2022 16:55
@edsko
Copy link
Author

edsko commented Sep 9, 2022

Marked this as a draft because we haven't tried to use this yet. Will report back, but can invite feedback in the meanwhile.

@edsko
Copy link
Author

edsko commented Sep 13, 2022

Ok, confirmed that this works for us. Marked as ready for review. Let me know if there is anything you'd like me to change! :)

@edsko edsko marked this pull request as ready for review September 13, 2022 06:02
@hrajchert
Copy link
Collaborator

Hi Edsko, Thanks for your contribution! We will soon analyze the PR in more detail, but I wanted to share some quick notes:

  • We have the initiative to replace PK in favour of Address in the making. Currently, there is PR 132 in this repo which will be merged together with PR 134. Other repos will have corresponding PRs soon.
  • As this note suggest, in the context of the specification we treat the Token and Address as opaque ByteStream. In the marlowe-cardano repository we use the Plutus types instead. Knowing that making the type polymorphic increases the size of the validator, I wonder if there is a special gain in abstracting them here.
  • The main entity of this repository are the Isabelle proofs that conform the specification. At the moment, the proofs and the Haskell reference are not 100% aligned as the reference has Merkelization support while the specification doesn't. I have ticket SCP-4449 to export a Haskell implementation from the Isabelle proofs, so we can later decide if
    1. We can remove the Haskell reference altogether and use the exported code instead
    2. Or add some property-based testing to increase our confidence that both implementations are aligned.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants