Validated compressed sparse row matrix-vector product

Fix a field $F$. The validated CSR matrix-vector product takes integer dimension candidates $m,n$, integer arrays $r,c$, a value array $v$ of elements of $F$, and a vector candidate $x$ of elements of $F$. All input arrays are finite; write $s=\mathrm{length}(v)$.

1. If $m\mathrm{\notin }\mathbb{N}$, $n\mathrm{\notin }\mathbb{N}$, $\mathrm{length}(r)\mathrm{\ne }m+1$, $\mathrm{length}(c)\mathrm{\ne }s$, or $\mathrm{length}(x)\mathrm{\ne }n$, return the status invalid-dimension.
2. For $i=0,\dots ,m$, check that $r_i\in \{0,\dots ,s\}$; return invalid-index if a check fails. Check $r_0=0$ and $r_m=s$, and for each $i=0,\dots ,m-1$ check $r_i\le r_{i+1}$; return invalid-index if any check fails. For each $t=0,\dots ,s-1$, check $0\le c_t<n$ and return invalid-index if a check fails.
3. Initialize $y_i=0_F$ for $0\le i<m$. For each row $i=0,\dots ,m-1$, and then each stored index $t=r_i,\dots ,r_{i+1}-1$, update $y_i\leftarrow y_i+v_t{x}_{c_t}\mathrm{.}$
4. Return the status ok together with $y\in F^m$.

For valid CSR data, each update uses exact field arithmetic. This procedure makes no floating-point rounding, backward-stability, convergence, runtime, or memory-bandwidth claim.