Formal Spec with Plutus Integration - Review 3.rtf

{\rtf1\ansi\ansicpg1252\cocoartf1671\cocoasubrtf600
{\fonttbl\f0\fswiss\fcharset0 Helvetica;}
{\colortbl;\red255\green255\blue255;\red251\green2\blue7;\red251\green2\blue7;}
{\*\expandedcolortbl;;\cssrgb\c100000\c14913\c0;\cssrgb\c100000\c14913\c0;}
\margl1440\margr1440\vieww10800\viewh11560\viewkind0
\deftab720
\pard\pardeftab720\partightenfactor0

\f0\fs24 \cf0 A Formal Specification of the Cardano Ledger with Plutus Integration\
Review 3\
\
- p16 \'93\'85based on current resource use pricing.\'94 is a bit more clear if replaced by \'93based on pricing for current resource use\'94\
\cf2 Changed to: .. based on the amount of $\\ExUnits$ it has budgeted for running the \
  scripts it carries, and the prices (as indicated in the current protocol parameters) \
  for each of the components of $\\ExUnits$. Recall that a transaction pays a flat \
  fee for running a Plutus script, plus some amount per unit of memory \
  and per reduction step.\cf0 \
\
Figure 8\
- \'93tx VK inputs used for fees\'94 -> \'93tx VK and multisignature script inputs used for fees\'94?\
\cf2 Yes\cf0 \
\
- Very minor, but there are extra parentheses in definition of txinputs_vf, ie ((txid, ix), isfee) should be (txid, ix, isfee).\
\cf3 Yes\cf0 \
\
- Does \'93range\'94 output empty set if the input to range is empty? For example, in feesOK, does range(txinputs_vf\'85) output empty set if none of the fee-marked inputs are in UTXO or no input is marked for fees?\
\cf3 Yes\cf0 \
\
- In feesOK, the line \'93^ ubalance (txinputs_vf txb) \\in Coin\'94 should be  \'93^ ubalance (txinputs_vf txb \\lefttriangle utxo) \\in Coin\'94 \
\cf3 Yes\cf0 \
\
- ubalance outputs the type Value, which is different from Coin. How is it checked that the output of ubalance is in the set Coin? This should be done by checking that the Value part of the fee-marked inputs all have domain that is equal to adaID, right?\
\cf2 I added a note about notation abuse, and put it in the section where I explain adaID:\
\'93However, we will abuse notation and\
write shorthand that $v ~\\in~ \\Coin$ is $\\type\{True\}$ when\
$v~ =~ \\fun\{coinToValue\}~ c$ for some $c~\\in~\\Coin$.\'94\cf0 \
\
- The definition of outs: According to the definition of UTxOOut, the output part of UTXO has \'93slot\'94 only when it has a DataHash (ie. when UTxOOut is type TxOutP x Slot). However in the definition of outs, slot is always included in the output. This would result in the wrong type if the output of getOut is of type TxOutND.\
\cf2 Thank you! There is a mistake here - the brackets are wrong for the UTxOOut definition, the slot should be included regardless \
of whether the output type is TxOutP or TxOutND. \
getOut throws away the HasDV value in the case that a TxOut is of type TxOutP, and keeps \
the whole output if it is of type TxOutND (because it does not have a HasDV tag). The outs \
function adds the slot number to whatever getOut returned.  \cf0 \
\
- Very minor, but we could replace \'93TxId x Ix\'94 in definition of txins with UTxOIn.\
\cf2 This is intentional. Even though they are the same, we do not want to conflate them,\
As they may be different in the future.\cf0 \
\
Figure 9\
- \'93UTxO with only the Ada coins\'94 -> \'93UtxO with only Ada coins\'94\
\cf2 Changed to:\
\'93returns the addresses in the UTxO paired with the amount of Ada in them\'94\cf0 \
\
- The definition of ubalance: The function getValue takes input UTxOOut or TxOut, so the definition should be \'93\\sum_\{_-> out \\in utxo\} getValue out\'94. \
\cf2 Yup!\cf0 \
\
- The argument \'93rewards\'94 is not used in the definition of \'93consumed\'94.\
\cf2 Removed\cf0 \
\
- The description of \'93consumed\'94 is in slightly different order than the definition. According to the definition, the description should be \'93sum of the value UTXO entries consumed, reward address value consumed, value consumed from the deposit pot, and the value forged by a transaction.\'94\
\cf3 Yup!\cf0 \
\
- I\'92m not sure which part of the definition of \'93produced\'94 is the fee for processing scripts? According to definition txfee, it is the non-script fee, right?\
\cf3 The fee now covers the script fees as well (I made a note saying that).\cf0 \
\
- The description of \'93produced\'94 is also in a slightly different order than the definition. According to the definition, the description should be \'93contains the output it adds to UTxO, the fee\'85, and the deposits\'85\'94\
\cf3 Yup!}