Formal Spec with Plutus Integration - Review 6.rtf

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

\f0\fs24 \cf0 A Formal Specification of the Cardano Ledger with Plutus Integration\
Review 6\
\
p31\
- \'93To do this, we have two separate rules in for\'85\'94 -> the \'93in\'94 is extra\
\cf2 Yup\cf0 \
\
p32\
- \'93\'85we have tx \\in ShelleyTx, see Figure 19\'94 -> should be Figure 20\
\
Figure 19\
- \'93\\forall txin \\in txinputs txb, \'85 \\in dom(indexedDats txw)\'94 -> \'93\\in dom(indexedDats tx)\'94 (txw should be tx)\
\cf2 Yup\cf0 \
\
- \'93cert \\in txcerts txb, regCred cert\'85\'94 - regCred takes type DCert_regpool; however this line also checks that cert \\in DCert_deregkey. Are these the same type?\
\cf2 The registration credential of a deregestration certificate can be a script hash, but for no other kinds of certs \cf0 \
\
- \'93hashMD\'94 is not defined in this document. Is this the same as the \'93hash\'94 function?\
\cf2 MD is a Shelley feature\
\cf0 \
Figure 20\
- \'93mdh := txMDhash txb  md := txMD tx\'94 and \'93(mdh = <> ^ md = <>)\'85\'94 - If tx is a ShelleyTx it shouldn\'92t have the MetaData field right? So perhaps these couple lines should be omitted?\
\cf2 MD is a Shelley feature\
\cf0 \
Figure 21, Figure 22\
- \'93(stkCreds, _, _, _, _, genDelegs) := dstate\'94 (in two places in Figure 21, and also in Fig 22)  - should be \'93(stkCreds, _, _, _, _, genDelegs, _) := dstate\'94 (since in the DState definition in Shelley spec Fig 27, after genDelegs there is i_rwd).\
\cf2 Yup\cf0 \
\
- \'93(stpools, _, _, _) := pstate\'94 (in two places in Figure 21, and also in Fig 22) - should be \'93(stpools, _, _) := pstate\'94 since in the Shelley spec Fig 27 there are only 3 components in PState.\
\cf2 Yup\cf0 \
\
Figure 24\
\cf2 I changed the format of this figure\
\cf0 - In the Shelley ChainState, the field corresponding to \'93utxo\'94 in toGoguen is type UTxOState which contains UTxO as its first (of 4) components (Shelley spec Fig 19). So in toGoguen, instead of utxo, should be \'93(utxo, _, _, _)\'94\
\
- The component v_10 in toGoguen seems to be extra, since in Shelley spec, NewEpochState (Fig 60), the first component of Shelley ChainState, has only 7 components.\
\
Figure 25\
- Should toGoguenTx also include \'93rdmrsHash txb\'92 = <>\'94, \'93txMDhash txb\'92 = <>\'94, \'93IsValidating = No\'94, \'93MetaData = <>\'94?\
\cf2 Yes\cf0 \
\
- \'93txwits tx\'92 = (\\epsilon, \'85\'94 - Shelley transactions also have the field accessed by txwitsVKey, so this field should be included in Goguen transaction right?}