Formal Spec with Plutus Integration - Review 4.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\viewh14920\viewkind0
\deftab720
\pard\pardeftab720\partightenfactor0

\f0\fs24 \cf0 A Formal Specification of the Cardano Ledger with Plutus Integration\
Review 4\
\
- p22 - \'93signle\'94 -> \'93single\'94\
\cf2 Yup!\cf0 \
\
- p23 - \'93alloted\'94 -> \'93allotted\'94\
\cf2 Yup!\cf0 \
\
Figure 10\
- In the first definition of indexof, there is an extra right arrow \'93->\'94\
\cf2 Yup!\cf0 \
\
- In the definition of getmdl, what happens if \'93(language s) <| (costmdls pp)\'94 is empty, eg. a multisig script which does not have a cost model? Will all scripts called with this function have a cost model?\
\cf3 Since all the scripts that go into the sLst are Plutus scripts, they are supposed to have have a cost model. Do you have a suggestion for a better way to to express things so that there is no need for implicitly assuming that the list of cost models will be non empty? \cf0 \
\
- In the definition of findRdmr, when indexof is given arguments of wrong type (eg. if the first argument is type Wdrl but second argument is DCert*) will it just cause the predicate the return false? Or might it output an error?\
\cf3 The intention was that it cannot be applied at all to a predicate of the wrong type, so there is no way the predicate in the subset definition should not be satisfied in case of wrong type. I am not sure if this is a problem?\cf0 \
\
Figure 11\
- In the definition of allCertScrts, does it output (script_v, r; \'85) such that \'93r\'94 is all the items in \'93findRdmr tx cert\'94 appended together? Or is there a different (script_v, r; \'85) for each \'93r\'94 in \'93findRdmr tx cert\'94?\
\cf3 the r would be any redeemer that is associated with the CurItem, and there would be an element (script_v, r; \'85) in the set for each associated r found. However, the idea is that there is a unique r associated with each item, so it should be just one element. Does this make sense?\cf0 \
\
- In the definition of allWDRLSScrts: The input of validatorHash should be type Addr^script but the definition of Wdrl in Shelley spec is Addr_rwd. Has Addr_rwd been replaced by Addr^script?\
\cf3 Mistake. The reward address contains exactly one thing - the hash of either a key or a script which can collect rewards. This is what should be used to look up the script in indexedScripts. By default it will only return anything if the reward address was a script hash.\cf0 \
\
Figure 12\
- In the definition of allInsScrts: The output of txinputs is TxIn which has the IsFee field, so \'93(txid, ix) \\in txinputs (txbody tx),\'94 should be  \'93(txid, ix, _) \\in txinputs (txbody tx),\'94\
\cf2 Yup!\cf0 \
\
- The function findRdmr takes second argument of type TxIn (type in CurItem) which has the IsFee field so \'93r \\in findRdmr tx (txid, ix),\'94 should be  \'93r \\in findRdmr tx (txid, ix, _),\'94 \
\cf3 I am changing the types of CurItem slightly to get rid of data not needed for uniquely identifying \
the current item, including removing IsFee , changing Wdrl to just the address, and only the certificate entity being registered/deregistered. \cf0 \
\
- \'93(txid, ix) -> ((a, v), h_d) \\in utxo,\'94 should be \'93(txid, ix) -> ((a, v), h_d, _) \\in utxo,\'94 (is missing the \'93Slot\'94 part of UTxOOut)\
\cf2 Yup!}