proof.tex 4.54 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
\begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=\scriptsize}]

Benoit Viguier's avatar
Benoit Viguier committed
3
4
5

  % adapt line thickness and line width, if needed

Benoit Viguier's avatar
Benoit Viguier committed
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's avatar
Benoit Viguier committed
25
  % C code
26
  \begin{scope}[yshift=-0.25 cm,xshift=2.75 cm]
Benoit Viguier's avatar
Benoit Viguier committed
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's avatar
Benoit Viguier committed
35
  \begin{scope}[yshift=-0.25 cm,xshift=5 cm]
Benoit Viguier's avatar
Benoit Viguier committed
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's avatar
Benoit Viguier committed
41
    % \draw (1.25,0)  node[anchor=south east, inner sep=0pt] {\includegraphics[width=.0125\textwidth]{img/coq_logo.png}};
Benoit Viguier's avatar
Benoit Viguier committed
42
43
  \end{scope}

44
  \path [thick, dotted, double, ->] (4,-0.75) edge (5, -0.75);
Benoit Viguier's avatar
Benoit Viguier committed
45
46

  % VST Spec
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's avatar
Benoit Viguier committed
50
    \draw (0.3,-0.05) node[textstyle] {Specification};
51
    \draw (1.375,-1) node[textstyle, anchor=center, align=left] {
Benoit Viguier's avatar
Benoit Viguier committed
52
      {\color{doc@lstnumbers}\textbf{Pre}}:\\
53
      ~~\texttt{s}$[\!\!\{$\texttt{n}$\}\!\!]= n \in \N$,\\
Benoit Viguier's avatar
Benoit Viguier committed
54
      % ~~$n \in$ \TNaCles{u8[32]},\\
55
      ~~\texttt{s}$[\!\!\{$\texttt{p}$\}\!\!]= P \in E(\F{p^2})$\\
Benoit Viguier's avatar
Benoit Viguier committed
56
      % ~~$P \in$ \TNaCles{u8[32]}\\
Benoit Viguier's avatar
Benoit Viguier committed
57
      {\color{doc@lstdirective}\textbf{Post}}:\\
58
      ~~\texttt{s}$[\!\!\{$\texttt{q}$\}\!\!]=$~\texttt{RFC}$(n,P)$};
Benoit Viguier's avatar
Benoit Viguier committed
59
60
  \end{scope}

Benoit Viguier's avatar
Benoit Viguier committed
61
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}}\}};
    \draw (2.5,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
Benoit Viguier's avatar
Benoit Viguier committed
68
69
  \end{scope}

Benoit Viguier's avatar
Benoit Viguier committed
70
71
  \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);
72
  \path [thick, double, ->] (5.5,-3.75) edge [out=0, in=180] (6, -3.75);
Benoit Viguier's avatar
Benoit Viguier committed
73
74
75
76
77



  % SECTION V

Benoit Viguier's avatar
Benoit Viguier committed
78
  % Spec of Curve nP
Benoit Viguier's avatar
Benoit Viguier committed
79
  \begin{scope}[yshift=-7.5 cm,xshift=0 cm]
Benoit Viguier's avatar
Benoit Viguier committed
80
81
    \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's avatar
Benoit Viguier committed
82
    \draw (0.3,-0.05) node[textstyle] {Definition};
Benoit Viguier's avatar
Benoit Viguier committed
83
    \draw (0.875,-0.5) node[textstyle, anchor=center] {$n \cdot P$};
Benoit Viguier's avatar
Benoit Viguier committed
84
85
86
  \end{scope}

  % Correctness Theorem
Benoit Viguier's avatar
Benoit Viguier committed
87
  \begin{scope}[yshift=-7 cm,xshift=6 cm]
Benoit Viguier's avatar
Benoit Viguier committed
88
    \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
89
    \draw (0,0) -- (2.5,0) -- (2.5,-1.5) -- (0, -1.5) -- cycle;
Benoit Viguier's avatar
Benoit Viguier committed
90
    \draw (0.3,-0.05) node[textstyle] {Proof};
Benoit Viguier's avatar
Benoit Viguier committed
91
    \draw (2.5,-1.5) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
Benoit Viguier's avatar
Benoit Viguier committed
92
    \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's avatar
Benoit Viguier committed
93
94
  \end{scope}

95
  \path [thick, double, ->] (1.75,-3.5) edge  [out=0, in=-180] (2.75, -3.5);
Benoit Viguier's avatar
Benoit Viguier committed
96
  \path [thick, double] (1.75,-3.5) edge [out=0, in=90] (2.25, -4);
Benoit Viguier's avatar
Benoit Viguier committed
97
98
99
100
  \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's avatar
Benoit Viguier committed
101

Benoit Viguier's avatar
Benoit Viguier committed
102
103

\end{tikzpicture}