address two more items in issue 457

src/Ledger/Transaction.lagda

@@ -37,17 +37,29 @@ record TransactionStructure : Type₁ where
 
 Transactions are defined in Figure~\ref{fig:defs:transactions}. A
 transaction is made up of a transaction body, a collection of
-witnesses and some optional auxiliary data. Some key ingredients in
-the transaction body are:
-
+witnesses and some optional auxiliary data.
+\begin{NoConway}
+Some key ingredients in the transaction body are:
 \begin{itemize}
   \item A set \AgdaField{txins} of transaction inputs, each of which identifies an output from a previous transaction.
     A transaction input consists of a transaction id and an index to uniquely identify the output.
   \item An indexed collection \AgdaField{txouts} of transaction outputs.
     The \TxOut type is an address paired with a coin value.
   \item A transaction fee. This value will be added to the fee pot.
-  \item The size and the hash of the serialized form of the transaction that was included in the block.
+  \item The size \AgdaField{txsize} and the hash \AgdaField{txId} of the serialized form of the transaction that was included in the block.
 \end{itemize}
+\end{NoConway}
+\begin{Conway}
+Ingredients of the transaction body introduced in the Conway era are the following:
+\AgdaField{txvote}, \AgdaField{txprop}, \AgdaField{txdonation} and \AgdaField{curTreasury}.
+%% TODO: remove previous line; uncomment list below; add descriptions to each item
+%% \begin{itemize}
+%%   \item \AgdaField{txvote};
+%%   \item \AgdaField{txprop};
+%%   \item \AgdaField{txdonation};
+%%   \item \AgdaField{curTreasury}.
+%% \end{itemize}
+\end{Conway}
 
 \begin{figure*}[h]
 \emph{Abstract types}

src/Ledger/Utxow.lagda

@@ -15,10 +15,12 @@ open import Ledger.Utxo txs abs
 open import Ledger.ScriptValidation txs abs
 \end{code}
 
-Figure~\ref{fig:functions:utxow} defines functions used for
-witnessing. \witsVKeyNeeded and \scriptsNeeded are now defined by
-projecting the same information out of \credsNeeded. Note that the
-last component of \credsNeeded adds the script in the proposal policy
+The purpose of witnessing is make sure the intended action is
+authorized by the holder of the signing key.  (For details see
+the Formal Ledger Specification for the Shelley Era~\cite[Sec.~8.3]{cardano_shelley_ledger}.)
+Figure~\ref{fig:functions:utxow} defines functions used for witnessing.
+\witsVKeyNeeded and \scriptsNeeded are now defined by projecting the same information out of
+\credsNeeded. Note that the last component of \credsNeeded adds the script in the proposal policy
 only if it is present.
 
 \allowedLanguages has additional conditions for new features in
@@ -88,8 +90,7 @@ allowedLanguages tx utxo =
   else
     fromList (PlutusV1 ∷ PlutusV2 ∷ PlutusV3 ∷ [])
   where
-    txb = tx .Tx.body
-    open TxBody txb
+    txb = tx .Tx.body; open TxBody txb
     os = range (outs txb) ∪ range (utxo ∣ (txins ∪ refInputs))
 
 getScripts : ℙ Credential → ℙ ScriptHash

src/latex/references.bib

@@ -1,3 +1,11 @@
+@misc{cardano_shelley_ledger,
+  title        = {A Formal Specification of the Cardano Ledger},
+  author       = {Jared Corduan and Polina Vinogradova and Matthias G\"{u}demann},
+  year         = {2019},
+  url          = {https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf},
+  note         = {Accessed: 2024-07-15},
+  howpublished = {\url{https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf}}
+}
 @misc{cip1694,
   title={A First Step Towards On-Chain Decentralized Governance},
   author={Jared Corduan and Matthias Benkort and Kevin Hammond and Charles Hoskinson and Andre Knispel and Samuel Leathers},