proof.tex 4.92 KB
 Benoit Viguier committed Jul 12, 2019 1 2 \begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=\scriptsize}]  Benoit Viguier committed Jul 16, 2019 3 4 5  % adapt line thickness and line width, if needed  Benoit Viguier committed Sep 18, 2019 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24  \path [thick, dashed] (2.5,1) edge +(0,-6.75); \draw (2.5,1) node[anchor=north east] {\sref{sec:Coq-RFC}}; \draw (2.5,1) node[anchor=north west] {\sref{sec:C-Coq}}; \path [thick, dashed] (0,-5.75) edge +(8.5,0); \draw (8.5,-5.75) node[anchor=north east] {\sref{sec:maths}}; % SECTION III % Definition of RFC \begin{scope}[yshift=-3 cm,xshift=0 cm] \draw (0,0) -- (0.4, 0.4) -- (1.75,0.4) -- (1.75,0) -- cycle; \draw (0,0) -- (1.75,0) -- (1.75,-1) -- (0, -1) -- cycle; \draw (0.3,-0.05) node[textstyle] {Definition}; \draw (0.875,-0.5) node[textstyle, anchor=center] {\texttt{RFC}}; \draw (1.75,-1) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}}; \end{scope} % SECTION IV  Benoit Viguier committed Jul 12, 2019 25  % C code  Benoit Viguier committed Sep 27, 2019 26  \begin{scope}[yshift=-0.25 cm,xshift=2.75 cm]  Benoit Viguier committed Jul 12, 2019 27 28 29 30 31 32 33 34  \draw (0,0) -- (0.4, 0.4) -- (1.25,0.4) -- (1.25,0) -- cycle; \draw (0,0) -- (1.25,0) -- (1.25,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {code}; \draw (0.675,-0.5) node[textstyle, anchor=center] {\texttt{Prog}}; \draw (1.25,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.C}}; \end{scope} % V code  Benoit Viguier committed Sep 18, 2019 35  \begin{scope}[yshift=-0.25 cm,xshift=5 cm]  Benoit Viguier committed Jul 12, 2019 36 37 38 39 40  \draw (0,0) -- (0.4, 0.4) -- (1.25,0.4) -- (1.25,0) -- cycle; \draw (0,0) -- (1.25,0) -- (1.25,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {code}; \draw (0.675,-0.5) node[textstyle, anchor=center] {\texttt{Prog}}; \draw (1.25,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};  Benoit Viguier committed Jul 15, 2019 41  % \draw (1.25,0) node[anchor=south east, inner sep=0pt] {\includegraphics[width=.0125\textwidth]{img/coq_logo.png}};  Benoit Viguier committed Jul 12, 2019 42 43  \end{scope}  Benoit Viguier committed Sep 27, 2019 44  \path [thick, dotted, double, ->] (4,-0.75) edge (5, -0.75);  Benoit Viguier committed Jul 12, 2019 45 46  % VST Spec  Benoit Viguier committed Sep 27, 2019 47 48 49  \begin{scope}[yshift=-3 cm,xshift=2.75 cm] \draw (0,0) -- (0.4, 0.4) -- (2.75,0.4) -- (2.75,0) -- cycle; \draw (0,0) -- (2.75,0) -- (2.75,-2) -- (0, -2) -- cycle;  Benoit Viguier committed Jul 12, 2019 50  \draw (0.3,-0.05) node[textstyle] {Specification};  Benoit Viguier committed Sep 27, 2019 51  \draw (1.375,-1) node[textstyle, anchor=center, align=left] {  Benoit Viguier committed Jul 15, 2019 52  {\color{doc@lstnumbers}\textbf{Pre}}:\\  Benoit Viguier committed Sep 30, 2019 53  ~~\texttt{s}$[\!\!\{$\texttt{n}$\}\!\!]\leftarrow n \in \N$,\\  Benoit Viguier committed Sep 18, 2019 54  % ~~$n \in$ \TNaCles{u8[32]},\\  Benoit Viguier committed Sep 30, 2019 55  ~~\texttt{s}$[\!\!\{$\texttt{p}$\}\!\!]\leftarrow P \in E(\F{p^2})$\\  Benoit Viguier committed Sep 18, 2019 56  % ~~$P \in$ \TNaCles{u8[32]}\\  Benoit Viguier committed Jul 15, 2019 57  {\color{doc@lstdirective}\textbf{Post}}:\\  Benoit Viguier committed Sep 30, 2019 58  ~~\texttt{s}$[\!\!\{$\texttt{q}$\}\!\!]\leftarrow$~\texttt{RFC}$(n,P)$};  Benoit Viguier committed Jan 14, 2020 59  \draw (2.75,-2) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};  Benoit Viguier committed Jul 12, 2019 60 61  \end{scope}  Benoit Viguier committed Sep 18, 2019 62 63 64 65 66 67  % VST Theorem \begin{scope}[yshift=-3 cm,xshift=6 cm] \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle; \draw (0,0) -- (2.5,0) -- (2.5,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {Proof}; \draw (1.25,-0.5) node[textstyle, anchor=center] {\{{\color{doc@lstnumbers}\textbf{Pre}}\} \texttt{Prog} \{{\color{doc@lstdirective}\textbf{Post}}\}};  Benoit Viguier committed Jan 14, 2020 68 69  \draw (2.5,0) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}}; \draw (2.5,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};  Benoit Viguier committed Jul 12, 2019 70 71  \end{scope}  Benoit Viguier committed Sep 18, 2019 72 73  \path [thick, double] (5.625,-1.5) edge [out=-90, in=90] (5.625, -2.5); \path [thick, double, ->] (5.625, -2.5) edge [out=-90, in=180] (6, -3.5);  Benoit Viguier committed Sep 27, 2019 74  \path [thick, double, ->] (5.5,-3.75) edge [out=0, in=180] (6, -3.75);  Benoit Viguier committed Sep 18, 2019 75 76 77 78 79  % SECTION V  Benoit Viguier committed Jul 12, 2019 80  % Spec of Curve nP  Benoit Viguier committed Sep 19, 2019 81  \begin{scope}[yshift=-7.5 cm,xshift=0 cm]  Benoit Viguier committed Sep 18, 2019 82 83  \draw (0,0) -- (0.4, 0.4) -- (1.75,0.4) -- (1.75,0) -- cycle; \draw (0,0) -- (1.75,0) -- (1.75,-1) -- (0, -1) -- cycle;  Benoit Viguier committed Jul 12, 2019 84  \draw (0.3,-0.05) node[textstyle] {Definition};  Benoit Viguier committed Sep 18, 2019 85  \draw (0.875,-0.5) node[textstyle, anchor=center] {$n \cdot P$};  Benoit Viguier committed Jan 14, 2020 86  \draw (1.75,-1) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};  Benoit Viguier committed Jul 12, 2019 87 88 89  \end{scope} % Correctness Theorem  Benoit Viguier committed Sep 19, 2019 90  \begin{scope}[yshift=-7 cm,xshift=6 cm]  Benoit Viguier committed Jul 12, 2019 91  \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle;  Benoit Viguier committed Jul 15, 2019 92  \draw (0,0) -- (2.5,0) -- (2.5,-1.5) -- (0, -1.5) -- cycle;  Benoit Viguier committed Jul 12, 2019 93  \draw (0.3,-0.05) node[textstyle] {Proof};  Benoit Viguier committed Sep 18, 2019 94  \draw (1.25,-0.75) node[textstyle, anchor=center] {{\color{doc@lstnumbers}\textbf{Pre}} $\implies$\\$\text{\texttt{RFC}}(n,P) = n \cdot P$};  Benoit Viguier committed Jan 14, 2020 95 96  \draw (2.5,0) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}}; \draw (2.5,-1.5) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};  Benoit Viguier committed Jul 12, 2019 97 98  \end{scope}  Benoit Viguier committed Sep 27, 2019 99  \path [thick, double, ->] (1.75,-3.5) edge [out=0, in=-180] (2.75, -3.5);  Benoit Viguier committed Sep 18, 2019 100  \path [thick, double] (1.75,-3.5) edge [out=0, in=90] (2.25, -4);  Benoit Viguier committed Sep 19, 2019 101 102 103 104  \path [thick, double] (2.25, -4) edge [out=-90, in=90] (2.25, -7); \path [thick, double] (2.25, -7) edge [out=-90, in=-180] (3, -7.75); \path [thick, double, ->] (3, -7.75) edge [out=0, in=-180] (6, -7.75); \path [thick, double, ->] (1.75,-8) edge [out=0, in=-180] (6, -8);  Benoit Viguier committed Sep 18, 2019 105   Benoit Viguier committed Jul 12, 2019 106 107  \end{tikzpicture}