Merge pull request #1969 from input-output-hk/andre/shelley-spec-fix

Add missing restriction to VKey in witsVKeyNeeded
IntersectMBO · Nov 5, 2020 · 0ecab80 · 0ecab80
2 parents 2f70be6 + 50a1a28
commit 0ecab80
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex
@@ -475,7 +475,7 @@ \subsection{Witnesses}
  \cup & ~~
  \{\fun{stakeCred_r}~a\mid a\mapsto \wcard \in \AddrRWDVKey
  \restrictdom \txwdrls{tx}\}\\
- \cup & ~~\fun{certWitsNeeded}~{tx} \\
+ \cup & ~~(\AddrVKey \cap \fun{certWitsNeeded}~{tx}) \\
  \cup & ~~\fun{propWits}~(\fun{txup}~\var{tx})~\var{genDelegs} \\
  \cup & ~~\bigcup_{\substack{c \in \txcerts{tx} \\ ~c \in\DCertRegPool}} \fun{poolOwners}~{c}
  \end{align*}