-
Notifications
You must be signed in to change notification settings - Fork 158
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
TxInfo chapter #2494
TxInfo chapter #2494
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This does not actually define the txInfo
function though. Also, since txInfo
needs to invoke transVITime
, it needs to have EpochInfo
and SystemStart
as parameters
alonzo/formal-spec/txinfo.tex
Outdated
\nextdef | ||
& \fun{transValue} \in \Value \to \type{P.Value} \\ | ||
& \fun{transValue}~ (c,~ mp) = \{~ pid_P\mapsto (aid_P \mapsto q_P) ~\mid~ pid \mapsto (aid \mapsto q) ~\in ~mp ~\} \\ | ||
& ~~~~\cup \{~\type{P.adaSymbol}\mapsto (\type{P.adaToken} \mapsto c) ~\} \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So Plutus has a pid and asset name for Ada? We should mention that in the MA spec!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
maybe we should do that in the other (Value) PR?
9f9db83
to
bdf74e2
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this section should go into an appendix. It's not really required to understand the ledger and its properties. In fact, none of the properties we've proven depends on how txinfo
is defined.
I've also made some small formatting changes & fixes, I hope you like them!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've done a commit on top of yours that streamlines everything a bit and restores the _P
notation (I liked it, it just needed to be formally justified). If you like it the way it is now, we can merge it!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually, I realized that the threading through of the EpochInfo
and SystemStart
isn't finished. collectTwoPhaseScriptInputs
needs to pass these to txinfo
, which it needs to get from UTXOS
, which means that we need to adjust the context of the entire family of UTXO*
rules...
I don't even know where these parameters come from in the first place, I just hope they don't have to be threaded through all the way to CHAIN
...
b813111
to
3c35cd2
Compare
eras/alonzo/formal-spec/utxo.tex
Outdated
@@ -480,6 +480,9 @@ \subsection{The UTXOS transition system} | |||
|
|||
There are two rules, corresponding to the two possible state changes of the | |||
UTxO state in the UTXOS transition system (Figure~\ref{fig:rules:utxo-state-upd}). | |||
Note here that the constants $\mathsf{ei}$ and $\mathsf{sysSt}$ are available | |||
inside the definition of all ledger rules. They are supplied by the consensus |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, this is not true. The ledger rules are simply relations, so to make this true we'd have to break our entire theory. Those need to be provided by the contexts, even if the code does it differently.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
we act as if it's hard-coded, like other constants. But this is obscuring where it comes from. It is not part of the context
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
i can re-word this and point out it's an implementation detail (ie it's actually hard-coded)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm, if they're constants then maybe we can just stick them into the global constants?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also, I'm confused. Why is slotToPOSIXTime
a constant?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The use of EpochInfo is similar to the use of NetworkID
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And the NetworkID is a global constant, see Fig 8 of the Shelley spec
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM!
The commits need to be signed before we can merge. Perhaps we can also clean up the commit history? Thanks! |
rebase comments Small changes to formatting comments Streamlining & cleanup ei sysSt global constants time translate
0b5e6e3
to
b58d8b7
Compare
No description provided.