Use new type Nonce for nonces instead of Seed

IntersectMBO · May 7, 2024 · 7779c7e · 7779c7e
1 parent 70a46f3
commit 7779c7e
Show file tree

Hide file tree

Showing 4 changed files with 60 additions and 45 deletions.
diff --git a/docs/formal-spec/chain.tex b/docs/formal-spec/chain.tex
@@ -19,6 +19,8 @@ \subsection{Block Definitions}
       \var{h} & \HashHeader & \text{hash of a block header}\\
       \var{hb} & \HashBBody & \text{hash of a block body}\\
       \var{bn} & \BlockNo & \text{block number}\\
+      \eta & \Nonce & \text{nonce}\\
+      \var{vrfRes} & \VRFRes & \text{VRF result value}\\
     \end{array}
   \end{equation*}
   %
@@ -47,7 +49,7 @@ \subsection{Block Definitions}
         \var{vrfVk} & \VKey & \text{VRF verification key}\\
         \var{blockNo} & \BlockNo & \text{block number}\\
         \var{slot} & \Slot & \text{block slot}\\
-        \var{vrfRes} & \Seed & \text{VRF result value}\\
+        \var{vrfRes} & \VRFRes & \text{VRF result value}\\
         \var{vrfPrf} & \Proof & \text{VRF proof}\\
         \var{bodySize} & \N & \text{size of the block body}\\
         \var{bodyHash} & \HashBBody & \text{block body hash}\\
@@ -70,12 +72,16 @@ \subsection{Block Definitions}
   %
   \begin{equation*}
     \begin{array}{r@{~\in~}lr}
+      \nonceOp{} & \Nonce \to \Nonce \to \Nonce
+                 & \text{binary nonce operation} \\
       \headerHash{} & \BHeader \to \HashHeader
                    & \text{hash of a block header} \\
       \headerSize{} & \BHeader \to \N
                    & \text{size of a block header} \\
       \slotToSeed{} & \Slot \to \Seed
                     & \text{convert a slot to a seed} \\
+      \nonceToSeed{} & \Nonce \to \Seed
+                     & \text{convert a nonce to a seed} \\
       \prevHashToNonce{} & \HashHeader^? \to \Seed
                     & \text{convert an optional header hash to a seed} \\
     \end{array}
@@ -92,7 +98,7 @@ \subsection{Block Definitions}
       \fun{hBPrevHeader} & \BHBody \to \HashHeader^? \\
       \fun{hBSlot} & \BHBody \to \Slot &
       \fun{hBBlockNo} & \BHBody \to \BlockNo \\
-      \fun{hBVrfRes} & \BHBody \to \Seed &
+      \fun{hBVrfRes} & \BHBody \to \VRFRes &
       \fun{hBVrfPrf} & \BHBody \to \Proof \\
       \fun{hBBodySize} & \BHBody \to \N &
       \fun{hBBodyHash} & \BHBody \to \HashBBody \\
@@ -111,11 +117,11 @@ \subsection{Block Definitions}
 \begin{figure}[htb]
   \emph{Block Helper Functions}
   \begin{align*}
-      & \fun{bleader} \in \BHBody \to \Seed \\
-      & \fun{bleader}~\var{bhb} = \fun{hash}~(``L"~|~(\fun{hBVrfRes}~\var{bhb}))\\
+      & \fun{hBLeader} \in \BHBody \to \N \\
+      & \fun{hBLeader}~\var{bhb} = \fun{hash}~(``L"~|~(\fun{hBVrfRes}~\var{bhb}))\\
       \\
-      & \fun{bnonce} \in \BHBody \to \Seed \\
-      & \fun{bnonce}~\var{bhb} = \fun{hash}~(``N"~|~(\fun{hBVrfRes}~\var{bhb}))\\
+      & \fun{hBNonce} \in \BHBody \to \Nonce \\
+      & \fun{hBNonce}~\var{bhb} = \fun{hash}~(``N"~|~(\fun{hBVrfRes}~\var{bhb}))\\
   \end{align*}
   %
   \caption{Helper Functions used for Blocks}
@@ -141,8 +147,8 @@ \subsection{$\mathsf{TICKN}$ Transition}
     \left(
       \begin{array}{r@{~\in~}lr}
         \var{pp} & \PParams & \text{protocol parameters} \\
-        \eta_c & \Seed & \text{candidate nonce} \\
-        \eta_\var{ph} & \Seed & \text{previous header hash as nonce} \\
+        \eta_c & \Nonce & \text{candidate nonce} \\
+        \eta_\var{ph} & \Nonce & \text{previous header hash as nonce} \\
       \end{array}
     \right)
   \end{equation*}
@@ -152,8 +158,8 @@ \subsection{$\mathsf{TICKN}$ Transition}
     \TickNonceState =
     \left(
       \begin{array}{r@{~\in~}lr}
-        \eta_0 & \Seed & \text{epoch nonce} \\
-        \eta_h & \Seed & \text{seed from hash of previous epoch's last block header} \\
+        \eta_0 & \Nonce & \text{epoch nonce} \\
+        \eta_h & \Nonce & \text{nonce from hash of previous epoch's last block header} \\
       \end{array}
     \right)
   \end{equation*}
@@ -207,7 +213,7 @@ \subsection{$\mathsf{TICKN}$ Transition}
      \end{array}\right)}
      \trans{tickn}{\mathsf{True}}
      {\left(\begin{array}{c}
-           \varUpdate{\eta_c \seedOp \eta_h} \\
+           \varUpdate{\eta_c \nonceOp \eta_h} \\
            \varUpdate{\eta_\var{ph}} \\
      \end{array}\right)}
    }
@@ -232,7 +238,7 @@ \subsection{$\mathsf{UPDN}$ Transition}
     \UpdateNonceEnv =
     \left(
       \begin{array}{r@{~\in~}lr}
-        \eta & \Seed & \text{new nonce} \\
+        \eta & \Nonce & \text{new nonce} \\
       \end{array}
     \right)
   \end{equation*}
@@ -242,8 +248,8 @@ \subsection{$\mathsf{UPDN}$ Transition}
     \UpdateNonceState =
     \left(
       \begin{array}{r@{~\in~}lr}
-        \eta_v & \Seed & \text{evolving nonce} \\
-        \eta_c & \Seed & \text{candidate nonce} \\
+        \eta_v & \Nonce & \text{evolving nonce} \\
+        \eta_c & \Nonce & \text{candidate nonce} \\
       \end{array}
     \right)
   \end{equation*}
@@ -269,7 +275,7 @@ \subsection{$\mathsf{UPDN}$ Transition}
 slots until the start of the next epoch.
 
 Note that in \ref{eq:update-both}, the candidate nonce $\eta_c$ transitions to
-$\eta_v\seedOp\eta$, not $\eta_c\seedOp\eta$. The reason for this is that even
+$\eta_v\nonceOp\eta$, not $\eta_c\nonceOp\eta$. The reason for this is that even
 though the candidate nonce is frozen sometime during the epoch, we want the two
 nonces to again be equal at the start of a new epoch.
 
@@ -291,8 +297,8 @@ \subsection{$\mathsf{UPDN}$ Transition}
       \end{array}\right)}
       \trans{updn}{\var{s}}
       {\left(\begin{array}{c}
-            \varUpdate{\eta_v\seedOp\eta} \\
-            \varUpdate{\eta_v\seedOp\eta} \\
+            \varUpdate{\eta_v\nonceOp\eta} \\
+            \varUpdate{\eta_v\nonceOp\eta} \\
       \end{array}\right)}
     }
   \end{equation}
@@ -315,7 +321,7 @@ \subsection{$\mathsf{UPDN}$ Transition}
       \end{array}\right)}
       \trans{updn}{\var{s}}
       {\left(\begin{array}{c}
-            \varUpdate{\eta_v\seedOp\eta} \\
+            \varUpdate{\eta_v\nonceOp\eta} \\
             \eta_c \\
       \end{array}\right)}
     }
@@ -458,7 +464,7 @@ \subsection{Verifiable Random Function}
 \begin{itemize}
 \item The validity of the proofs for the leader value and the new nonce.
 \item The verification key is associated with relative stake $\sigma$ in the stake distribution.
-\item The $\fun{bleader}$ value of \var{bhb} indicates a possible leader for
+\item The $\fun{hBLeader}$ value of \var{bhb} indicates a possible leader for
   this slot. The function $\fun{checkLeaderVal}$ is defined in \ref{sec:leader-value-calc}.
 \end{itemize}
 
@@ -469,9 +475,9 @@ \subsection{Verifiable Random Function}
   \end{align*}
   %
   \begin{align*}
-      & \fun{vrfChecks} \in \Seed \to \BHBody \to \Bool \\
+      & \fun{vrfChecks} \in \Nonce \to \BHBody \to \Bool \\
       & \fun{vrfChecks}~\eta_0~\var{bhb} =
-          \verifyVrf{\Seed}{\var{vrfK}}{(\slotToSeed{slot}~\XOR~\eta_0)}{(\var{value},~\var{proof}}) \\
+          \verifyVrf{\VRFRes}{\var{vrfK}}{((\slotToSeed{slot})~\XOR~(\nonceToSeed{\eta_0}))}{(\var{value},~\var{proof}}) \\
       & ~~~~\where \\
       & ~~~~~~~~~~\var{slot} \leteq \hBSlot{bhb} \\
       & ~~~~~~~~~~\var{vrfK} \leteq \fun{hBVrfVk}~\var{bhb} \\
@@ -480,13 +486,13 @@ \subsection{Verifiable Random Function}
   \end{align*}
   %
   \begin{align*}
-      & \fun{praosVrfChecks} \in \Seed \to \PoolDistr \to \unitIntervalNonNull \to \BHBody \to \Bool \\
+      & \fun{praosVrfChecks} \in \Nonce \to \PoolDistr \to \unitIntervalNonNull \to \BHBody \to \Bool \\
       & \fun{praosVrfChecks}~\eta_0~\var{pd}~\var{f}~\var{bhb} = \\
       & \begin{array}{cl}
         ~~~~ & \var{hk}\mapsto (\sigma,~\var{vrfHK})\in\var{pd} \; (\ref{itm:vrf-failures-1}) \\
         ~~~~ \land & \var{vrfHK} = \hashKey{vrfK} \; (\ref{itm:vrf-failures-2}) \\
         ~~~~ \land & \fun{vrfChecks}~\eta_0~\var{bhb} \; (\ref{itm:vrf-failures-3}) \\
-        ~~~~ \land & \fun{checkLeaderVal}~(\fun{bleader}~\var{bhb})~\sigma~\var{f} \; (\ref{itm:vrf-failures-4}) \\
+        ~~~~ \land & \fun{checkLeaderVal}~(\fun{hBLeader}~\var{bhb})~\sigma~\var{f} \; (\ref{itm:vrf-failures-4}) \\
       \end{array} \\
       & ~~~~\where \\
       & ~~~~~~~~~~\var{hk} \leteq \fun{issuerIDfromBHBody}~\var{bhb} \\
@@ -510,7 +516,6 @@ \subsection{Verifiable Random Function}
   compared to the relative stake of the pool, there is a \emph{VRFLeaderValueTooBig} failure.
 \end{enumerate}
 
-
 \clearpage
 
 \subsection{$\mathsf{PRTCL}$ Transition}
@@ -526,7 +531,7 @@ \subsection{$\mathsf{PRTCL}$ Transition}
     \left(
       \begin{array}{r@{~\in~}lr}
         \var{pd} & \PoolDistr & \text{pool stake distribution} \\
-        \eta_0 & \Seed & \text{epoch nonce} \\
+        \eta_0 & \Nonce & \text{epoch nonce} \\
       \end{array}
     \right)
   \end{equation*}
@@ -537,8 +542,8 @@ \subsection{$\mathsf{PRTCL}$ Transition}
     \left(
       \begin{array}{r@{~\in~}lr}
         \var{cs} & \KeyHash_{pool} \mapsto \N & \text{operational certificate issues numbers} \\
-        \eta_v & \Seed & \text{evolving nonce} \\
-        \eta_c & \Seed & \text{candidate nonce} \\
+        \eta_v & \Nonce & \text{evolving nonce} \\
+        \eta_c & \Nonce & \text{candidate nonce} \\
       \end{array}
     \right)
   \end{equation*}
@@ -570,8 +575,8 @@ \subsection{$\mathsf{PRTCL}$ Transition}
     \inference[PRTCL]
     {
       \var{bhb}\leteq\headerBody{bh} &
-      \eta\leteq\fun{bnonce}~bhb &
-      slot\leteq\fun{bslot}~bhb
+      \eta\leteq\fun{hBNonce}~bhb &
+      slot\leteq\fun{hBSlot}~bhb
       \\~\\
       {
         \eta
@@ -797,10 +802,10 @@ \subsection{$\mathsf{CHAINHEAD}$ Transition}
     \left(
       \begin{array}{r@{~\in~}lr}
         \var{cs} & \KeyHash_{pool} \mapsto \N & \text{operational certificate issue numbers} \\
-        ~\eta_0 & \Seed & \text{epoch nonce} \\
-        ~\eta_v & \Seed & \text{evolving nonce} \\
-        ~\eta_c & \Seed & \text{candidate nonce} \\
-        ~\eta_h & \Seed & \text{seed from hash of last epoch's last header} \\
+        ~\eta_0 & \Nonce & \text{epoch nonce} \\
+        ~\eta_v & \Nonce & \text{evolving nonce} \\
+        ~\eta_c & \Nonce & \text{candidate nonce} \\
+        ~\eta_h & \Nonce & \text{nonce from hash of last epoch's last header} \\
         \var{lab} & \LastAppliedBlock^? & \text{latest applied block} \\
       \end{array}
     \right)

diff --git a/docs/formal-spec/consensus-spec.tex b/docs/formal-spec/consensus-spec.tex
@@ -92,7 +92,7 @@
 \newcommand{\Duration}{\type{Duration}}
 \newcommand{\StakePools}{\type{StakePools}}
 \newcommand{\Seed}{\type{Seed}}
-\newcommand{\seedOp}{\star}
+\newcommand{\nonceOp}{\star}
 \newcommand{\Ppm}{\type{Ppm}}
 \newcommand{\ProtVer}{\ensuremath{\type{ProtVer}}}
 \newcommand{\Metadatum}{\ensuremath{\type{Metadatum}}}
@@ -199,6 +199,7 @@
 \newcommand{\Seedl}{\mathsf{Seed}_\ell}
 \newcommand{\Seede}{\mathsf{Seed}_\eta}
 \newcommand{\slotToSeed}[1]{\fun{slotToSeed}~ \var{#1}}
+\newcommand{\nonceToSeed}[1]{\fun{nonceToSeed}~ #1}
 \newcommand{\prevHashToNonce}[1]{\fun{prevHashToNonce}~ \var{#1}}
 \newcommand{\isOverlaySlot}[3]{\fun{isOverlaySlot}~\var{#1}~\var{#2}~\var{#3}}
 \newcommand{\classifyOverlaySlot}[5]{\fun{classifyOverlaySlot}~\var{#1}~\var{#2}~\var{#3}~\var{#4}~\var{#5}}
@@ -216,6 +217,8 @@
 \newcommand{\OCert}{\type{OCert}}
 \newcommand{\BHeader}{\type{BHeader}}
 \newcommand{\BHBody}{\type{BHBody}}
+\newcommand{\Nonce}{\type{Nonce}}
+\newcommand{\VRFRes}{\type{VRFRes}}
 
 \newcommand{\bheader}[1]{\fun{bheader}~\var{#1}}
 \newcommand{\hsig}[1]{\fun{hsig}~\var{#1}}
@@ -375,15 +378,9 @@
 \bibliographystyle{habbrv}
 \bibliography{references}
 
-%\clearpage
-%\begin{appendix}
-%  \input{crypto-details}
-%  \input{address-binary}
-%  \input{bootstrap-witnesses}
-%  \input{cddl}
-%  \input{txsize}
-%  \input{proofs}
-%\end{appendix}
-
+\clearpage
+\begin{appendix}
+  \input{crypto-details}
+\end{appendix}
 
 \end{document}
diff --git a/docs/formal-spec/crypto-details.tex b/docs/formal-spec/crypto-details.tex
@@ -0,0 +1,13 @@
+\section{Cryptographic Details}
+\label{sec:crypto-details}
+
+\subsection{Abstract functions}
+\label{sec:abstract-funcs-implementation}
+
+\begin{itemize}
+  \item The nonce operation $x \nonceOp y$ from Figure~\ref{fig:defs:blocks} is implemented
+        as the BLAKE2b-256 hash of the concatenation of $x$ and $y$.
+  \item The functions \fun{slotToSeed} and \fun{nonceToSeed} from Figure~\ref{fig:defs:blocks} are implemented
+        as the big-endian encoding of the slot/nonce number in 8 bytes.
+\end{itemize}
+
diff --git a/docs/formal-spec/properties.tex b/docs/formal-spec/properties.tex
@@ -41,7 +41,7 @@ \subsection{Header-Only Validation}
   $$
   where $s=(\var{nes},~\tilde{s})$,
   $t_E$ is the maximum slot number appearing in the blocks contained in
-  $E$, and $H$ is obtained from $E$ by applying $\fun{bheader}$ to each block in $E$.
+  $E$, and $H$ is obtained from $E$ by applying $\fun{blockHeader}$ to each block in $E$.
 \end{property}
 
 \begin{property}[Body only validation]\label{prop:body-only-validation}