Prerequisite is a set, ensure all dependencies are known/valid when r…

…eported (#122)

* Prerequisite is a set, ensure all  dependencies are known when reported

* Keep the two types of deps disjoint

* Tidy

* Check SR lookups directly in reporting

* Avoid blocking accumulation on SR lookup checks

* Avoid need for disjointness

* Avoid the possibility of too little accumulation gas for the immediates

* Avoid dupe term.

* Nits

text/accumulation.tex

@@ -39,9 +39,9 @@ \subsection{Preimage Integration}
 
 \subsection{History and Queuing}
 
-Accumulation of a work-package/work-report is deferred in the case that it has a not-yet-fulfilled dependency and is cancelled entirely in the case of an invalid dependency. Dependencies are specified as work-package hashes and in order to know which work-packages have been accumulated already, we maintain a history of what has been accumulated. This history, $\accumulated$, is sufficiently large for an epoch worth of work-reports. For all such reports, we also retain their segment-root in order that we may validate any guarantor-proscribed segment-roots in work-reports prior to accumulation. Formally:
+Accumulation of a work-package/work-report is deferred in the case that it has a not-yet-fulfilled dependency and is cancelled entirely in the case of an invalid dependency. Dependencies are specified as work-package hashes and in order to know which work-packages have been accumulated already, we maintain a history of what has been accumulated. This history, $\accumulated$, is sufficiently large for an epoch worth of work-reports. Formally:
 \begin{align}
-  \accumulated &\in \seq{\dict{\H}{\H}}_\mathsf{E} \\
+  \accumulated &\in \seq{\{\H\}}_\mathsf{E} \\
   \accumulatedcup &\equiv \bigcup_{x \in \accumulated}(x)
 \end{align}
 
@@ -52,26 +52,25 @@ \subsection{History and Queuing}
 
 The newly available work-reports, $\mathbf{W}$, are partitioned into two sequences based on the condition of having zero prerequisite work-reports. Those meeting the condition, $\mathbf{W}^!$, are accumulated immediately. Those not, $\mathbf{W}^Q$, are for queued execution. Formally:
 \begin{align}
-  \mathbf{W}^! &\equiv [ w \mid w \orderedin \mathbf{W}, (w_x)_p = \none \wedge w_\wr¬srlookup = \{\} ] \\
+  \mathbf{W}^! &\equiv [ w \mid w \orderedin \mathbf{W}, (w_x)_\mathbf{p} = \none \wedge w_\wr¬srlookup = \{\} ] \\
   \mathbf{W}^Q &\equiv E(\sq{
     D(w) \mid
     w \orderedin \mathbf{W},
-    (w_x)_p \ne \none \vee w_\wr¬srlookup \ne \{\}
+    (w_x)_\mathbf{p} \ne \none \vee w_\wr¬srlookup \ne \{\}
   }, \accumulatedcup)\!\!\!\!\\
-  D(w) &\equiv (w, \{(w_x)_p\} \cup \keys{w_\wr¬srlookup})
+  D(w) &\equiv (w, \{(w_x)_\mathbf{p}\} \cup \keys{w_\wr¬srlookup})
 \end{align}
 
-We define the queue-editing function $E$, which is essentially a mutator function for items such as those of $\ready$, parameterized by a dictionary such as the items in $\accumulated$. It is used to update queues of work-reports when some of them are accumulated. Functionally, it removes all entries whose work-report's hash is in the parameter's keys, removes any dependencies which appear in said set and, crucially, removes any entries whose segment-root correspondences diverge from those in the dictionary. Formally:
+We define the queue-editing function $E$, which is essentially a mutator function for items such as those of $\ready$, parameterized by sets of now-accumulated work-package hashes (those in $\accumulated$). It is used to update queues of work-reports when some of them are accumulated. Functionally, it removes all entries whose work-report's hash is in the parameter's keys, removes any dependencies which appear in said set and, crucially, removes any entries whose segment-root correspondences diverge from those in the dictionary. Formally:
 \begin{equation}
   E\colon\left\{\begin{aligned}
-      &(\seq{(\mathbb{W}, \{\H\})}, \dict{\H}{\H}) \to \seq{(\mathbb{W}, \{\H\})} \\
+      &(\seq{(\mathbb{W}, \{\H\})}, \{\H\}) \to \seq{(\mathbb{W}, \{\H\})} \\
     &(\mathbf{r}, \mathbf{x}) \mapsto \left[
-      (w, \mathbf{d} \setminus \keys{\mathbf{x}})
+      (w, \mathbf{d} \setminus \mathbf{x})
       \,\middle\vert\,
       \left\{\,\begin{aligned}
         &(w, \mathbf{d}) \orderedin \mathbf{r} ,\\
-        &(w_s)_h \not\in \keys{\mathbf{x}},\\
-        &\mathbf{x} \cup w_\wr¬srlookup = w_\wr¬srlookup \cup \mathbf{x}
+        &(w_s)_h \not\in \mathbf{x}
       \end{aligned}\right.
       \right]
   \end{aligned}\right.
@@ -89,11 +88,11 @@ \subsection{History and Queuing}
   \end{aligned}\right.
 \end{equation}
 
-Finally, we define the mapping function $\srmap$ which builds a dictionary of work-package hashes to segment-roots from a set of work-reports:
+Finally, we define the mapping function $\srmap$ which extracts the corresponding work-package hashes from a set of work-reports:
 \begin{equation}
   \srmap\colon\left\{\begin{aligned}
-    \{\mathbb{W}\} &\to \dict{\H}{\H}\\
-    \mathbf{w} &\mapsto \{ ((w_s)_h \mapsto (w_s)_e) \mid w \in \mathbf{w} \}
+    \{\mathbb{W}\} &\to \{\H\}\\
+    \mathbf{w} &\mapsto \{ (w_s)_h \mid w \in \mathbf{w} \}
   \end{aligned}\right.
 \end{equation}
 
@@ -208,7 +207,8 @@ \subsection{Deferred Transfers and State Integration}
 
 Given the result of the top-level $\Delta_+$, we may define the posterior state $\chi'$, $\varphi'$ and $\iota'$ as well as the second intermediate state of the service-accounts $\delta^\ddagger$ and the \textsc{Beefy} commitment map $\beefycommitmap$:
 \begin{align}
-  \using (n, \mathbf{o}, \mathbf{t}, \beefycommitmap) &= \Delta_+(\mathsf{G}_T, \mathbf{W}^*, (\chi, \delta^\dagger, \iota, \varphi), \chi_\mathbf{g}) \\
+  \using g &= \max\left(\mathsf{G}_T, \mathsf{G}_A\cdot \mathsf{C} + \sum_{x \in \mathcal{V}(\chi_\mathbf{g})}(x)\right)\\
+  \using (n, \mathbf{o}, \mathbf{t}, \beefycommitmap) &= \Delta_+(g, \mathbf{W}^*, (\chi, \delta^\dagger, \iota, \varphi), \chi_\mathbf{g}) \\
   (\chi', \delta^\ddagger, \iota', \varphi') &\equiv \mathbf{o}
 \end{align}
 

text/definitions.tex

@@ -265,6 +265,7 @@ \subsubsection{Constants}
   \item[$\mathsf{G}_T$] The total gas allocated across all cores for Accumulation. May be no smaller than $\mathsf{G}_A\cdot\mathsf{C} + \sum_{g \in \mathcal{V}(\chi_\mathbf{g})}(g)$.
   \item[$\mathsf{H} = 8$] The size of recent history, in blocks.
   \item[$\mathsf{I} = 4$] The maximum amount of work items in a package.
+  \item[$\mathsf{J} = 8$] The maximum sum of dependency items in a work-report.
   \item[$\mathsf{K} = 16$] The maximum number of tickets which may be submitted in a single extrinsic.
   \item[$\mathsf{L} = 14,400$] The maximum age in timeslots of the lookup anchor.
   \item[$\mathsf{N} = 2$] The number of ticket entries per validator.

text/recent_history.tex

@@ -2,10 +2,10 @@ \section{Recent History}\label{sec:recenthistory}
 
 We retain in state information on the most recent $\mathsf{H}$ blocks. This is used to preclude the possibility of duplicate or out of date work-reports from being submitted.
 \begin{equation}
-  \beta \in \lseq\ltuple \isa{h}{\H}\ts\isa{\mathbf{b}}{\seq{\H?}}\ts\isa{s}{\H}\ts\isa{\mathbf{p}}{\lseq\H\rseq_{:\mathsf{C}}} \rtuple\rseq_{:\mathsf{H}}
+  \beta \in \lseq\ltuple \isa{h}{\H}\ts\isa{\mathbf{b}}{\seq{\H?}}\ts\isa{s}{\H}\ts\isa{\mathbf{p}}{\dict{\H}{\H}} \rtuple\rseq_{:\mathsf{H}}
 \end{equation}
 
-For each recent block, we retain its header hash, its state root, its accumulation-result \textsc{mmr} and the hash of each work-report made into it which is no more than the total number of cores, $\mathsf{C} = 341$.
+For each recent block, we retain its header hash, its state root, its accumulation-result \textsc{mmr} and the corresponding work-package hashes of each item reported (which is no more than the total number of cores, $\mathsf{C} = 341$).
 
 During the accumulation stage, a value with the partial transition of this state is provided which contains the update for the newly-known roots of the parent block:
 \begin{equation}
@@ -18,17 +18,17 @@ \section{Recent History}\label{sec:recenthistory}
     \label{eq:buildbeefymap}
     \using r &= \mathcal{M}_B(\orderby{s}{\se_4(s)\frown\se(h) \mid (s, h) \in \beefycommitmap}, \mathcal{H}_K) \\
     \using \mathbf{b} &= \mathcal{A}(\text{last}(\sq{\sq{}} \concat \sq{x_\mathbf{b} \mid x \orderedin \beta}), r, \mathcal{H}_K) \\
+    \using \mathbf{p} &= \{ ((g_w)_s)_h \mapsto ((g_w)_s)_e \mid g \in \xtguarantees \} \\
     \using n &= \tup{
-      \is{\mathbf{p}}{[((g_w)_s)_h \mid g \orderedin \xtguarantees]}\ts
+      \mathbf{p}\ts
       \is{h}{\mathcal{H}(\mathbf{H})}\ts\mathbf{b}\ts\is{s}{\H^0}
-      }
-    \end{aligned}
-  \end{equation}
-
-  The state-trie root is as being the zero hash, $\H^0$ which while inaccurate at the end state of the block $\beta'$, it is nevertheless safe since $\beta'$ is not utilized except to define the next block's $\beta^\dagger$, which contains a corrected value for this.
-
-  The final state transition is then:
-  \begin{equation}
-    \beta' \equiv {\overleftarrow{\beta^\dagger \doubleplus n}}^\mathsf{H}
-  \end{equation}
-
+    }
+  \end{aligned}
+\end{equation}
+
+The state-trie root is as being the zero hash, $\H^0$ which while inaccurate at the end state of the block $\beta'$, it is nevertheless safe since $\beta'$ is not utilized except to define the next block's $\beta^\dagger$, which contains a corrected value for this.
+
+The final state transition is then:
+\begin{equation}
+  \beta' \equiv {\overleftarrow{\beta^\dagger \doubleplus n}}^\mathsf{H}
+\end{equation}

text/reporting_assurance.tex

@@ -38,17 +38,17 @@ \subsubsection{Work Report}\label{sec:workreport}
 
 % TODO: places where w \in \mathbb{W} : w_o should be replaced with w_\mathbf{o} and w_r with w_\mathbf{r}
 
-We limit the number of items in the segment-root lookup dictionary to 8, and the total serialized size of a work-report may be no greater than $\mathsf{W}_R$ bytes:
+We limit the sum of the number of items in the segment-root lookup dictionary and the number of prerequisites to $\mathsf{J} = 8$, and the total serialized size of a work-report may be no greater than $\mathsf{W}_R$ bytes:
 \begin{equation}
-  \forall w \in \mathbb{W} : |w_\wr¬srlookup| \le 8\ \wedge\ |\se(w)| \leq \mathsf{W}_R
+  \forall w \in \mathbb{W} : |w_\wr¬srlookup| + |(w_x)_\mathbf{p}| \le \mathsf{J}\ \wedge\ |\se(w)| \leq \mathsf{W}_R
 \end{equation}
 
 \subsubsection{Refinement Context}
-A \emph{refinement context}, denoted by the set $\mathbb{X}$, describes the context of the chain at the point that the report's corresponding work-package was evaluated. It identifies two historical blocks, the \emph{anchor}, header hash $a$ along with its associated posterior state-root $s$ and posterior \textsc{Beefy} root $b$; and the \emph{lookup-anchor}, header hash $l$ and of timeslot $t$. Finally, it identifies the hash of an optional prerequisite work-package $p$. Formally:
+A \emph{refinement context}, denoted by the set $\mathbb{X}$, describes the context of the chain at the point that the report's corresponding work-package was evaluated. It identifies two historical blocks, the \emph{anchor}, header hash $a$ along with its associated posterior state-root $s$ and posterior \textsc{Beefy} root $b$; and the \emph{lookup-anchor}, header hash $l$ and of timeslot $t$. Finally, it identifies the hash of any prerequisite work-packages $\mathbf{p}$. Formally:
 \begin{equation}
   \mathbb{X} \equiv \ltuple\,\begin{alignedat}{7}
     \isa{a&}{\H}\ts\quad \isa{&s&}{\H}\ts\quad \isa{&b}{\H}\ts\\
-    \isa{l&}{\H}\ts\quad \isa{&t&}{\N_T}\ts\quad \isa{&p}{\H\bm{?}}
+    \isa{l&}{\H}\ts\quad \isa{&t&}{\N_T}\ts\quad \isa{&\mathbf{p}}{\{\H\}}
   \end{alignedat}\rtuple
 \end{equation}
 
@@ -282,18 +282,28 @@ \subsubsection{Contextual Validity of Reports}\label{sec:contextualvalidity}
   \forall x \in \mathbf{x} :\ \exists h \in \mathbf{A}: h_t = x_t \wedge \mathcal{H}(h) = x_h
 \end{align}
 
-We require that the work-package of the report not be the work-package of some other report made in the past. Since the work-package implies the anchor block, and the anchor block is limited to the most recent blocks, we need only ensure that the work-package not appear in our recent history:
+We require that the work-package of the report not be the work-package of some other report made in the past. Since the work-package implies the anchor block, and the anchor block is limited to the most recent blocks, we need only ensure that the work-package not appear in our recent history. Formally:
 \begin{equation}
-  \forall p \in \mathbf{p}, \forall x \in \beta : p \not\in x_\mathbf{p}
+  \forall p \in \mathbf{p}, \forall x \in \beta : p \not\in \keys{x_\mathbf{p}}
 \end{equation}
 
-We require that the prerequisite work-package, if present, be either in the extrinsic or in our recent history:
-\begin{equation}\begin{aligned}
-  &\forall w \in \mathbf{w}, (w_x)_p \ne \none :\\
-  &\quad(w_x)_p \in \mathbf{p} \cup \{ x \mid x \in b_\mathbf{p} ,\, b \in \beta \}
-\end{aligned}\end{equation}
+We require that the prerequisite work-packages, if present, and any work-packages mentioned in the segment-root lookup, be either in the extrinsic or in our recent history.
+\begin{align}
+  &\begin{aligned}
+    &\forall w \in \mathbf{w}, \forall p \in (w_x)_\mathbf{p} \cup \keys{w_\mathbf{l}} :\\
+    &\quad p \in \mathbf{p} \cup \{ x \mid x \in \keys{b_\mathbf{p}} ,\, b \in \beta \}
+  \end{aligned}
+\end{align}
+
+We require that any segment roots mentioned in the segment-root lookup be verified as correct based on our recent work-package history and the present block:
+\begin{align}
+  &\using \mathbf{p} = \{ ((g_w)_s)_h \mapsto ((g_w)_s)_e \mid g \in \xtguarantees \} \\
+  &\forall w \in \mathbf{w}: w_\mathbf{l} \subseteq \mathbf{p} \cup \bigcup_{b \in \beta} b_\mathbf{p}
+\end{align}
+
+(Note that these checks leave open the possibility of accepting work-reports in apparent dependency loops. We do not consider this a problem: the pre-accumulation stage effectively guarantees that accumulation never happens in these cases and the reports are simply ignored.)
 
-We require that all work results within the extrinsic predicted the correct code hash for their corresponding service:
+Finally, we require that all work results within the extrinsic predicted the correct code hash for their corresponding service:
 \begin{align}\label{eq:reportcodesarecorrect}
   \forall w \in \mathbf{w}, \forall r \in w_r : r_c = \delta[r_s]_c
 \end{align}

text/serialization.tex

@@ -139,7 +139,7 @@ \subsection{Block Serialization}
   \nonumber &\quad \where \xtdisputes \equiv (\mathbf{v}, \mathbf{c}, \mathbf{f}) \\
   \se(\mathbf{H}) &= \se_U(\mathbf{H})\concat\se(\mathbf{H}_s) \\
   \se_U(\mathbf{H}) &= \se(\mathbf{H}_p,\mathbf{H}_r,\mathbf{H}_x)\concat\se_4(\mathbf{H}_t)\concat\se(\maybe{\mathbf{H}_e},\maybe{\mathbf{H}_w},\var{\mathbf{H}_o},\se_2(\mathbf{H}_i),\mathbf{H}_v)\\
-  \se(x \in \mathbb{X}) &\equiv \se(x_a, x_s, x_b, x_l)\concat\se_4(x_t)\concat\se(\maybe{x_p})\\
+  \se(x \in \mathbb{X}) &\equiv \se(x_a, x_s, x_b, x_l)\concat\se_4(x_t)\concat\se(\var{x_\mathbf{p}})\\
   \se(x \in \mathbb{S}) &\equiv \se(x_h) \concat \se_4(x_l)\concat\se(x_u, x_e) \\
   \se(x \in \mathbb{L}) &\equiv \se_4(x_s)\concat\se(x_c, x_l)\concat\se_8(x_g)\concat\se(O(x_\mathbf{o}))\\
   \se(x \in \mathbb{W}) &\equiv \se(x_s, x_x, x_c, x_a, \var{x_\mathbf{o}}, \var{x_\mathbf{l}}, \var{x_\mathbf{r}}) \\