From ddb777c7944d608ad6336571739ed83e8380a56a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 5 May 2022 22:46:28 +0100 Subject: Fix some more references --- chapters/hls.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/chapters/hls.tex b/chapters/hls.tex index 6a6809f..f39afd3 100644 --- a/chapters/hls.tex +++ b/chapters/hls.tex @@ -1191,10 +1191,10 @@ matching state. % \NC \text{\sc Load}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] \ne \Gamma_{\rm r}[\mathit{r.u_{en}}]\qquad \Gamma_{\rm r}[\mathit{r.wr_{en}}] = 0}{((\Gamma_{\rm r}, - \Gamma_{\rm a}), (\Delta_{\rm r}, \Delta_{\rm a}), r) \downarrow_{\text{ram}} (\Delta_{\rm + \Gamma_{\rm a}), (\Delta_{\rm r}, \Delta_{\rm a}), r) \downarrow_{\text{ram}} \left(\Delta_{\rm r}\left[\startmatrix[n=1] \NC\mathit{r.en} \mapsto \mathit{r.u_{en}},\NR -\NC\mathit{r.d_{out}} \mapsto (\Gamma_{\rm a}[\mathit{r.mem}\NR\stopmatrix\right])[ \mathit{r.addr}]], \Delta_{\rm a}) }\NR +\NC\mathit{r.d_{out}} \mapsto (\Gamma_{\rm a}[\mathit{r.mem}])[ \mathit{r.addr}]\NR\stopmatrix\right], \Delta_{\rm a}\right) }\NR % \NC \text{\sc Store}\ \frac{\Gamma_{\rm r}[\mathit{r.en}] \ne \Gamma_{\rm r}[\mathit{r.u_{en}}]\qquad \Gamma_{\rm r}[\mathit{r.wr_{en}}] = 1}{((\Gamma_{\rm r}, \Gamma_{\rm a}), (\Delta_{\rm r}, @@ -1317,7 +1317,8 @@ $B_1$ and $B_2$ must be the same. \subsection[coq-mechanisation]{Coq Mechanisation} -\startplacetable[reference=tab:proof-statistics] +\startplacetable[reference={tab:proof-statistics},title={Statistics about the numbers of lines of + code in the proof and implementation of Vericert.}] \starttabulate[|l|r|r|r|r|r|] \FL \NC \NS[1][c] {\bf Coq code} \NS[1][c] {\bf Spec} \NC {\bf Total} \NC \NR -- cgit