spec for scripts and multi-currency #3

JaredCorduan · 2018-10-08T19:33:49Z

This is the beginning of a spec for a UTxO Ledger that has scripts and mutli-currency. It is essentially putting the two papers An Abstract Model of UTxO-based Cryptocurrencies with Scripts and Multi-Currency Ledgers into a rule style spec.

So far it has the types, basic functions, needed ledger state, validation rules, and a few notes about disabling multi-currency and scripts, and adding extended UTxO.

mgudemann · 2018-10-09T12:00:41Z

specs/scripts/latex/scripts-multicurrency.tex

+\caption{Scripts}
+\label{fig:scripts}
+\end{figure}
+


although it's an arbitrary type, T should be mentioned and maybe renamed to R as in the utxo/scripts paper

yes, R would be better, thanks! I was going to explain that arbitrary type in a paragraph explaining the scripts in general. Do you think I should mention R in that figure as well?

I would prefer having something like R : arbitrary return type of redeemer script / input type of validator script, because I often quickly look at figures like this for reference.

mgudemann · 2018-10-09T14:31:54Z

specs/scripts/latex/scripts-multicurrency.tex

+  \type{Tx}
+& \powerset{\type{TxIn}} \times (\type{Ix} \mapsto
+    \type{TxOut}) \times \type{Forge} \times \type{Value}
+&


shouldn't the optional Create also be part of this?

yes, thanks!

mgudemann · 2018-10-09T14:37:25Z

specs/scripts/latex/scripts-multicurrency.tex

+\begin{equation*}
+tx.create.currency \notin currencies
+\end{equation*}
+


There are more validation rules in the paper, e.g., creator has enough money to cover fees, fee is non-negative. Are these implicitly present here?

please check that I am correct (though we'll cover this more when doing property testing), but I think negative fees and cover fees are not an issue since this spec is UTxO only (accounts make some things trickier).

thinking about this a bit more, I realize I'm making an assumption that I'm not stating, namely that Quantity is an alias for Nat. We don't need inverses/subtraction if we don't have accounts.

mgudemann · 2018-10-09T14:40:01Z

specs/scripts/latex/scripts-multicurrency.tex

+
+\todo[inline]{We need to think carefully about how to handle similar names,
+like ``ada", ``Ada", and ``ADA".}
+


in my opinion the policy should offer the lowest risk of surprises, i.e., only uppercase or only lowercase, no UTF-8 etc.

I agree completely!

mgudemann · 2018-10-10T05:59:19Z

@JaredCorduan one thing which I was thinking about, is it possible to create a new currency CUR and forge a quantity of CUR in the same transaction? One would have to consider the currencies of the ledger and of the current transaction in that case. Does this make sense?

dnadales · 2018-10-10T09:15:19Z

Why not putting figure 4 and 6 as a single inference rule?

JaredCorduan · 2018-10-10T11:20:21Z

Why not putting figure 4 and 6 as a single inference rule?

yea, I should probably do that to be consistent with our other specs. It's just that figure 4 has so much information in it. Maybe I could define a new predicate that is just the conjunction of fig 4, and place it in a judgment style rule?

JaredCorduan · 2018-10-10T11:38:09Z

@JaredCorduan one thing which I was thinking about, is it possible to create a new currency CUR and forge a quantity of CUR in the same transaction? One would have to consider the currencies of the ledger and of the current transaction in that case. Does this make sense?

that's an excellent point! As I have it written now it would fail, since in "forge obeys policy" the new currency is not yet inside currencies (the ledger state has not yet been updated), so "∃ policy" fails. I guess the question now is should we require a newly created currency to follow the policy in the transaction in which it is created? I seems reasonable to me to allow forging in the transaction that creates a currency to be independent of the policy. I can make a TODO in the document for this is we want to think more about it later...

mgudemann · 2018-10-10T13:45:56Z

@JaredCorduan right, so currently it isn't possible. But there does not seem to be any problem with allowing it, right? We do have the monetary policy from Create, so we could check it. Of course it would then be a question what to do if the script does not verify. Should only the forge be dropped or should the Create also be rejected.

JaredCorduan · 2018-10-10T14:43:58Z

@mgudemann you are totally right, there is no problem, and in fact I think we want to be able to forge and create at the same time. If the script fails, then I think that the entire transaction should fail. I've just pushed a change that separates the state transition rule into two rules. And then I made a note/todo about being careful about the order in which rules are processed (with the understanding that if any rule fails validation, the transaction will not be processed at all). the other solution is to just search for policies in currencies U {new_currency -> new_policy}.

# This is the 1st commit message: Alter the endorsement registration rule, so that the set of confirmed proposals remains the same. # This is the commit message #2: Perform cleanup of confirmed proposals in the epoch change rule. # This is the commit message #3: Remove the section that expressed that there were no voting deadlines. There are now. # This is the commit message #4: Define what "endorsement" means in this context. # This is the commit message #5: Explain the acronyms used in the labels of the update-proposal interface. # This is the commit message #6: Add a figure explaining the situation with a too small endorsement window. # This is the commit message #7: Model the software update proposal in the update proposal validity rule. # This is the commit message #8: Make it possible for an update proposal not to change the protocol version.

# This is the 1st commit message: Merge branch 'spec/incentives-kh' of https://github.com/input-output-hk/cardano-ledger-specs into spec/incentives-kh # This is the commit message #2: overcoming fake make error Signed-off-by: Kevin Hammond <12563287+kevinhammond@users.noreply.github.com> # This is the commit message #3: overcoming fake make error Signed-off-by: Kevin Hammond <12563287+kevinhammond@users.noreply.github.com> # This is the commit message #4: overcoming fake make error Signed-off-by: Kevin Hammond <12563287+kevinhammond@users.noreply.github.com> # This is the commit message #5: overcoming fake make error Signed-off-by: Kevin Hammond <12563287+kevinhammond@users.noreply.github.com> # This is the commit message #6: overcoming fake make error Signed-off-by: Kevin Hammond <12563287+kevinhammond@users.noreply.github.com> # This is the commit message #7: fix user.email Signed-off-by: Kevin Hammond <12563287+kevinhammond@users.noreply.github.com> # This is the commit message #8: overcoming fake make error Signed-off-by: Kevin Hammond <12563287+kevinhammond@users.noreply.github.com> # This is the commit message #9: overcoming fake make error Signed-off-by: Kevin Hammond <12563287+kevinhammond@users.noreply.github.com>

…udit-pt-3 small shelley ledger spec edits from isabelle review #3

[#2] Add Cardano.Prelude

# This is the 1st commit message: Alter the endorsement registration rule, so that the set of confirmed proposals remains the same. # This is the commit message #2: Perform cleanup of confirmed proposals in the epoch change rule. # This is the commit message #3: Remove the section that expressed that there were no voting deadlines. There are now. # This is the commit message #4: Define what "endorsement" means in this context. # This is the commit message #5: Explain the acronyms used in the labels of the update-proposal interface. # This is the commit message #6: Add a figure explaining the situation with a too small endorsement window. # This is the commit message #7: Model the software update proposal in the update proposal validity rule. # This is the commit message #8: Make it possible for an update proposal not to change the protocol version.

* Add a `goldenTestCBOR` function. This function is basically a re-implementation of 'goldenTestBi', but it can be used with values of types that don't have a `Bi` instance. * Implement `goldenTestBi` in terms of `goldenTestCBOR`.

initial draft for scripts and multicurrency

5c59c23

mgudemann reviewed Oct 9, 2018

View reviewed changes

JaredCorduan added 2 commits October 9, 2018 12:20

fixup! initial draft for scripts and multicurrency

fb33658

fixup! initial draft for scripts and multicurrency

28c18c1

JaredCorduan changed the title ~~WIP spec for scripts and multi-currency~~ spec for scripts and multi-currency Oct 9, 2018

Fix compilation errors . [skip ci]

9b923c9

fixup! initial draft for scripts and multicurrency

787a5c7

JaredCorduan merged commit a84fc62 into master Oct 11, 2018

JaredCorduan deleted the scripts_and_multicurrency branch October 11, 2018 11:41

mdimjasevic pushed a commit that referenced this pull request May 30, 2019

Issue #512: implements properties #3 and #4 of the UPIEC STS

8244c1d

JaredCorduan added a commit that referenced this pull request Jan 22, 2020

small edits from isabelle review #3

c7f41e1

JaredCorduan added a commit that referenced this pull request Jan 22, 2020

small edits from isabelle review #3

1fcf580

JaredCorduan pushed a commit that referenced this pull request Jan 22, 2020

Merge pull request #1163 from input-output-hk/spec/shelley/isabelle-a…

f44f0ec

…udit-pt-3 small shelley ledger spec edits from isabelle review #3

nc6 pushed a commit that referenced this pull request May 19, 2020

Merge pull request #3 from input-output-hk/ruhatch/#1

38812bb

[#2] Add Cardano.Prelude

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

spec for scripts and multi-currency #3

spec for scripts and multi-currency #3

JaredCorduan commented Oct 8, 2018

mgudemann Oct 9, 2018 •

edited

Loading

JaredCorduan Oct 9, 2018

mgudemann Oct 9, 2018

mgudemann Oct 9, 2018

JaredCorduan Oct 9, 2018

mgudemann Oct 9, 2018

JaredCorduan Oct 9, 2018

JaredCorduan Oct 9, 2018

mgudemann Oct 9, 2018

JaredCorduan Oct 9, 2018

mgudemann commented Oct 10, 2018

dnadales commented Oct 10, 2018

JaredCorduan commented Oct 10, 2018

JaredCorduan commented Oct 10, 2018

mgudemann commented Oct 10, 2018

JaredCorduan commented Oct 10, 2018


		\todo[inline]{We need to think carefully about how to handle similar names,
		like ``ada", ``Ada", and ``ADA".}

spec for scripts and multi-currency #3

spec for scripts and multi-currency #3

Conversation

JaredCorduan commented Oct 8, 2018

mgudemann Oct 9, 2018 • edited Loading

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

mgudemann commented Oct 10, 2018

dnadales commented Oct 10, 2018

JaredCorduan commented Oct 10, 2018

JaredCorduan commented Oct 10, 2018

mgudemann commented Oct 10, 2018

JaredCorduan commented Oct 10, 2018

mgudemann Oct 9, 2018 •

edited

Loading