TxInfo chapter #2494
TxInfo chapter #2494
Conversation
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.
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.
maybe we should do that in the other (Value) PR?
polinavino
force-pushed
the
polina/txinfo
branch
from
9f9db83
to
bdf74e2
Compare
There was a problem hiding this comment.
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.
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...
WhatisRT
force-pushed
the
polina/txinfo
branch
from
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.
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.
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.
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.
Hmm, if they're constants then maybe we can just stick them into the global constants?
There was a problem hiding this comment.
Also, I'm confused. Why is slotToPOSIXTime a constant?
There was a problem hiding this comment.
The use of EpochInfo is similar to the use of NetworkID
There was a problem hiding this comment.
And the NetworkID is a global constant, see Fig 8 of the Shelley spec
|
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
WhatisRT
force-pushed
the
polina/txinfo
branch
from
0b5e6e3
to
b58d8b7
Compare
No description provided.