Fix some issues pointed out in the Babbage audit

In particular, I've removed the rounding from checking the balancing
of the collateral since if n is a natural number and x is a
rational (or real) number, n >= x is equivalent to n >= ceil x.
Without the rounding it's way more obvious that you can just multiply
the equation by 100 without changing the semantics.

Author: WhatisRT

eras/babbage/formal-spec/remove-overlay.tex

@@ -76,11 +76,11 @@ \section{Removal of the Overlay Schedule}
 'decentralized' case and drop all the unnecessary variables from its environment.
 It is invoked in $\mathsf{CHAIN}$, which needs to be adjusted accordingly.
 
-As there is now only a singe VRF check, slight modifications are needed for the
+As there is now only a single VRF check, slight modifications are needed for the
 definition of the block header body \text{BHBody} type and the function \text{vrfChecks}.
 The Shelley era accessor functions $\fun{bleader}$ and $\fun{bnonce}$ are replaced with new functions
 which make use of the VRF range extension as described in \cite{vrf-range-extension}[4.1],
-to re-use the singe VRF value.
+to re-use the single VRF value.
 
 \begin{figure*}[htb]
   %

eras/babbage/formal-spec/rewards.tex

@@ -21,7 +21,7 @@ \section{Forgo Reward Calculation Prefilter}
      & ~~~\where \\
           & ~~~~~~~\ldots \\
           & ~~~~~~~\hldiff{\var{rewards}} =
-               \var{mRewards} \cup
+               \var{mRewards} \unionoverridePlus
                \{(\fun{poolRAcnt}~\var{pool})\mapsto\var{lReward}\} \\
   \end{align*}
   \caption{Reward Calculation Helper Function}

eras/babbage/formal-spec/utxo.tex

@@ -33,9 +33,9 @@ \section{UTxO}
     & \fun{feesOK} : \PParams \to \Tx \to \UTxO \to \Bool  \\
     & \fun{feesOK}~\var{pp}~tx~utxo = \\
     &~~      \minfee{pp}{tx} \leq \txfee{tx} \wedge (\fun{txrdmrs}~tx \neq \Nothing \Rightarrow \\
-    &~~~~~~~~~~\forall (a, \wcard, \wcard) \in \fun{range}~(\fun{collInputs}~tx \restrictdom \var{utxo}), a \in \AddrVKey \\
+    &~~~~~~~~~~\forall (a, \wcard, \wcard, \wcard) \in \fun{range}~(\fun{collInputs}~tx \restrictdom \var{utxo}), a \in \AddrVKey \\
     &~~~~~~\wedge \fun{adaOnly}~\var{balance} \\
-    &~~~~~~\wedge \var{balance} \geq \hldiff{\lceil \txfee{txb} * \fun{collateralPercent}~pp / 100 \rceil} \\
+    &~~~~~~\wedge \var{balance} \geq \hldiff{\txfee{txb} * \fun{collateralPercent}~pp / 100} \\
     &~~~~~~\wedge \hldiff{(\fun{txcoll}~tx \neq \Nothing) \Rightarrow \var{balance} = \fun{txcoll}~tx} \\
     &~~~~~~\wedge \fun{collInputs}~{tx} \neq \emptyset) \\
     &~~      \where \\
@@ -196,8 +196,8 @@ \section{UTxO}
       \forall txout \in \hldiff{\fun{allOuts}~txb},\\
       \fun{serSize}~(\fun{getValue}~txout) \leq \fun{maxValSize}~pp \\~
       \\
-      \forall (\wcard\mapsto (a,~\wcard)) \in \hldiff{\fun{allOuts}~txb}, a \in \AddrBS \Rightarrow \fun{bootstrapAttrsSize}~a \leq 64 \\
-      \forall (\wcard\mapsto (a,~\wcard)) \in \hldiff{\fun{allOuts}~txb}, \fun{netId}~a = \NetworkId
+      \forall (\wcard\mapsto (a,~\wcard, \wcard, \wcard)) \in \hldiff{\fun{allOuts}~txb}, a \in \AddrBS \Rightarrow \fun{bootstrapAttrsSize}~a \leq 64 \\
+      \forall (\wcard\mapsto (a,~\wcard, \wcard, \wcard)) \in \hldiff{\fun{allOuts}~txb}, \fun{netId}~a = \NetworkId
       \\
       \forall (a\mapsto\wcard) \in \txwdrls{txb}, \fun{netId}~a = \NetworkId \\
       (\fun{txnetworkid}~\var{txb} = \NetworkId) \vee (\fun{txnetworkid}~\var{txb} = \Nothing)
@@ -290,7 +290,7 @@ \section{UTxO}
       \var{inputHashes}\leteq \left\{ h \,\middle|
         {
           \begin{array}{l}
-            (a, \_, h) \in \range(\var{utxo}|_{\fun{spendInputs}~tx}) \\
+            (a, \_, h, \_) \in \range(\var{utxo}|_{\fun{spendInputs}~tx}) \\
             \fun{isTwoPhaseScriptAddress}~tx~\hldiff{utxo}~a \\
           \end{array}
         }
@@ -299,7 +299,7 @@ \section{UTxO}
       \forall \var{s} \in (\fun{txscripts}~txw~\hldiff{utxo~\var{neededHashes}}) \cap \ScriptPhOne,
       \fun{validateScript}~\var{s}~\var{tx}\\~\\
       \var{neededHashes} - \hldiff{\dom (\fun{refScripts}~tx~utxo)} = \dom (\fun{txwitscripts}~txw) \\~\\
-      \var{inputHashes} \subseteq_{\{h \mid (\wcard, \wcard, h)\in\fun{allOuts}~tx \cup \hldiff{\var{utxo}~(\fun{refInputs}~{tx})}\}} \dom (\fun{txdats}~{txw})  \\~\\
+      \var{inputHashes} \subseteq_{\{h \mid (\wcard, \wcard, h, \wcard)\in\fun{allOuts}~tx \cup \hldiff{\var{utxo}~(\fun{refInputs}~{tx})}\}} \dom (\fun{txdats}~{txw})  \\~\\
       \\~\\
       \dom (\fun{txrdmrs}~tx) = \left\{ \fun{rdptr}~txb~sp \,\middle|
         {