Merge pull request #2024 from input-output-hk/andre/shelley-ma

Fix missing check for bootstrap addresses and missing `getValue`
IntersectMBO · Dec 2, 2020 · ef7a385 · ef7a385
2 parents 3456837 + 70de608
commit ef7a385
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/shelley-ma/formal-spec/utxo.tex b/shelley-ma/formal-spec/utxo.tex
@@ -158,7 +158,9 @@ \subsection*{The UTXO Transition Rule}
       \hldiff{\mathsf{adaPolicy}~\notin \supp{\fun{mint}~txb}} \\
       ~\\
       \hldiff{\forall txout \in \txouts{txb},} \\
-      \hldiff{txout \geq \fun{coinToValue}(\fun{outputSize}~{txout} * \fun{adaPerUTxOByte}~pp)} \\~
+      \hldiff{\fun{getValue}~txout \geq \fun{coinToValue}(\fun{outputSize}~{txout} * \fun{adaPerUTxOByte}~pp)} \\~
+      \\
+      \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, a \in \AddrBS \to \fun{bootstrapAttrsSize}~a \leq 64
       \\
       \forall (\wcard\mapsto (a,~\wcard)) \in \txouts{txb}, \fun{netId}~a =\NetworkId
       \\