Commit 27e9e88c authored by Benoit Viguier's avatar Benoit Viguier
Browse files

More space, small rewrite in Conclusion

parent c80f5322
......@@ -11,7 +11,7 @@ The core of the X25519 key-exchange protocol is a scalar\hyp{}multiplication
function, which we will also refer to as X25519.
This function receives as input two arrays of $32$ bytes each.
One of them is interpreted as the little-endian encoding of a
non-negative 256-bit integer $n$ (see \ref{subsec:integer-bytes}).
non-negative 256-bit integer $n$ (see \ref{sec:Coq-RFC}).
The other is interpreted as the little-endian encoding of
the \xcoord $x_P \in \F{p}$ of a point in $E(\F{p^2})$,
using the standard mapping of integers modulo $p$ to elements in $\F{p}$.
......
......@@ -30,7 +30,6 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
In this definition \coqe{montgomery_rec} is a generic ladder instantiated
with integers and defined as follows:
\begin{lstlisting}[language=Coq]
Fixpoint montgomery_rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
......@@ -78,7 +77,6 @@ match m with
montgomery_rec n z a b c d e f x
end.
\end{lstlisting}
% The definitions of the encoding and decoding functions are detailed later
% in this section.
......@@ -120,7 +118,7 @@ Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list}~\Z \rightarrow \Z$,
a function given $n$ and a list $l$ returns its little endian decoding with radix $2^n$.
% We define it in Coq as:
\end{dfn}
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt]
Fixpoint ZofList {n:Z} (a:list Z) : Z :=
match a with
| [] => 0
......@@ -128,8 +126,6 @@ Fixpoint ZofList {n:Z} (a:list Z) : Z :=
end.
\end{lstlisting}
% \Coqe{ZofList} is used in the decoding of byte arrays and also as a
% base to verify operations over lists in TweetNaCl (see~\ref{subsec:num-repr-rfc}).
The encoding from integers to bytes is defined in a similar way:
\begin{dfn}
Let \Coqe{ListofZ32} : $\Z \rightarrow \Z \rightarrow \texttt{list}~\Z$, given
......@@ -137,8 +133,7 @@ $n$ and $a$ returns $a$'s little-endian encoding as a list with radix $2^n$.
%XXX-Peter: Again I'm confused... why are there two \rightarrows?
%XXX-Benoit it is the functional view of arguments and partial functions. It is called Currying.
\end{dfn}
% We define it in Coq as:
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt]
Fixpoint ListofZn_fp {n:Z} (a:Z) (f:nat) : list Z :=
match f with
| 0%nat => []
......@@ -150,8 +145,7 @@ Definition ListofZ32 {n:Z} (a:Z) : list Z :=
\end{lstlisting}
In order to increase the trust in our formalization, we prove that
\Coqe{ListofZ32} and \Coqe{ZofList} are inverse to each other.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt]
Lemma ListofZ32_ZofList_Zlength: forall (l:list Z),
Forall (fun x => 0 <= x < 2^n) l ->
Zlength l = 32 ->
......@@ -160,7 +154,6 @@ Lemma ListofZ32_ZofList_Zlength: forall (l:list Z),
With those tools at hand, we formally define the decoding and encoding as
specified in the RFC.
\begin{lstlisting}[language=Coq]
Definition decodeScalar25519 (l: list Z) : Z :=
ZofList 8 (clamp l).
......
......@@ -2,11 +2,11 @@
\label{subsec:num-repr-rfc}
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
in base $2^{16}$ and we use a direct mapping to represent that array as a list
in $2^{16}$ and we use a direct mapping to represent that array as a list
integers in Coq. However, in order to show the correctness of the basic operations,
we need to convert this number to a full integer.
We reuse the mapping
$\text{\coqe{ZofList}} : \Z \rightarrow \texttt{list}~\Z \rightarrow \Z$ from \sref{subsec:integer-bytes}
$\text{\coqe{ZofList}} : \Z \rightarrow \texttt{list}~\Z \rightarrow \Z$ from \sref{sec:Coq-RFC}
and define a notation where $n$ is $16$, placing us with a radix of $2^{16}$.
\begin{lstlisting}[language=Coq]
Notation "Z16.lst A" := (ZofList 16 A).
......
......@@ -38,13 +38,13 @@ Lemma Crypto_Scalarmult_RFC_eq :
Crypto_Scalarmult n p = RFC n p.
\end{lstlisting}
This proves that TweetNaCl's X25519 implementation respect RFC~7748.
\todo{fix ``This''}
Using this equality, we can directly replace \coqe{Crypto_Scalarmult} in our
specification by \coqe{RFC}, proving that TweetNaCl's X25519 implementation
respect RFC~7748.
%% PREVIOUS TEXT BELOW.
%% PREVIOUS TEXT BELOW.
% \subsection{Reflections, inversions and packing}
% \label{subsec:inversions-reflections}
......
......@@ -138,7 +138,7 @@ It is parameterized by
a \texttt{K : ecuFieldType} --- the type of fields which characteristic is not
2 or 3 --- and \texttt{M : mcuType} --- a record that packs the curve
parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
Record mcuType :=
{ cA : K; cB : K; _ : cB != 0; _ : cA^2 != 4}.
Definition oncurve (p : point K) :=
......@@ -150,7 +150,7 @@ Inductive mc : Type := MC p of oncurve p.
Lemma oncurve_mc: forall p : mc, oncurve p.
\end{lstlisting}
We define the addition on Montgomery curves in the similar way as in the Weierstra{\ss} form.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Definition add (p1 p2 : point K) :=
match p1, p2 with
| \infty, _ => p2
......@@ -186,7 +186,7 @@ corresponding property for Weierstra{\ss} curves.
\end{align*}
is an isomorphism between elliptic curves.
\end{lemma}
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Definition ec_of_mc_point p :=
match p with
| \infty => \infty
......@@ -278,19 +278,17 @@ differential additions and point doublings using projective coordinates.
\subsubsection{Scalar multiplication algorithms}
\label{subsec:ECC-ladder}
By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL} and \texttt{xADD}
with their respective formulae (\lref{lemma:xADD} and \lref{lemma:xDBL}),
By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL\&ADD} by a
combination of the formulae from \lref{lemma:xADD} and \lref{lemma:xDBL},
we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet),
similar to the one used in
TweetNaCl.
similar to the one used in TweetNaCl.
This definition is closely related to \coqe{montgomery_rec} that was used
in the definition of \coqe{RFC}, and is easily proved to correspond to it.
In Coq this correspondence proof is hidden in the proof of \coqe{RFC_Correct} shown above.
We prove its correctness for any point whose \xcoord is not 0.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Lemma opt_montgomery_x :
forall (n m : nat) (x : K),
n < 2^m -> x != 0 ->
......@@ -298,12 +296,12 @@ Lemma opt_montgomery_x :
opt_montgomery n m x = (p *+ n)#x0.
\end{lstlisting}
We can remark that for an input $x = 0$, the ladder returns $0$.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Lemma opt_montgomery_0:
forall (n m : nat), opt_montgomery n m 0 = 0.
\end{lstlisting}
Also \Oinf\ is the neutral element of $M_{a,b}(\K)$.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Lemma p_x0_0_eq_0 : forall (n : nat) (p : mc M),
p #x0 = 0%:R -> (p *+ n) #x0 = 0%R.
\end{lstlisting}
......@@ -313,7 +311,7 @@ This gives us the theorem of the correctness of the Montgomery ladder.
For all $n, m \in \N$, $x \in \K$, $P \in M_{a,b}(\K)$,
if $\chi_0(P) = x$ then \coqe{opt_montgomery} returns $\chi_0(n \cdot P)$
\end{theorem}
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]
Theorem opt_montgomery_ok (n m: nat) (x : K) :
n < 2^m ->
forall (p : mc M), p#x0 = x ->
......@@ -372,11 +370,11 @@ elements ($0, 1$) and prove \lref{lemma:Zmodp_field}.
\end{lemma}
For $a = 486662$, by using the Legendre symbol we prove that
$a^2 - 4$ and $2$ are not squares in $\F{p}$.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Fact a_not_square : forall x: Zmodp.type,
x^+2 != (Zmodp.pi 486662)^+2 - 4%:R.
\end{lstlisting}
\begin{lstlisting}[language=Coq,label=two_not_square]
\begin{lstlisting}[language=Coq,label=two_not_square,belowskip=-0.1 \baselineskip]
Fact two_not_square : forall x: Zmodp.type,
x^+2 != 2%:R.
\end{lstlisting}
......@@ -421,7 +419,7 @@ we can find a $y$ such that $(x,y)$ is either on the curve or on the quadratic t
For all $x \in \F{p}$, there exists a point $P$ in $M_{486662,1}(\F{p})$ or
in $M_{486662,2}(\F{p})$ such that the \xcoord of $P$ is $x$.
\end{lemma}
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.5 \baselineskip]
Theorem x_is_on_curve_or_twist:
forall x : Zmodp.type,
(exists (p : mc curve25519_mcuType), p#x0 = x) \/
......@@ -445,7 +443,7 @@ We can represent $\F{p^2}$ as the set $\F{p} \times \F{p}$,
in other words,
the polynomial with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way
as for $\F{p}$ we use a module in Coq.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Module Zmodp2.
Inductive type :=
Zmodp2 (x: Zmodp.type) (y:Zmodp.type).
......@@ -490,16 +488,12 @@ of formulas by using rewrite rules:
\begin{equation*}
\begin{split}
(a,0) + (b,0) &= (a+b, 0)\\
(a, 0)^{-1} &= (a^{-1}, 0)\\
% (a, 0)\cdot (0,b) &= (0, a\cdot b)\\
(a, 0)^n &= (a^n, 0)\\
(a, 0)^{-1} &= (a^{-1}, 0)
\end{split}
\qquad
\begin{split}
(a,0) \cdot (b,0) &= (a \cdot b, 0)\\
(0,a)^{-1} &= (0,(2\cdot a)^{-1})\\
% (0, a)\cdot (0,b) &= (2\cdot a\cdot b, 0)\\
~\\
(0,a)^{-1} &= (0,(2\cdot a)^{-1})
\end{split}
\end{equation*}
......@@ -514,7 +508,7 @@ As direct consequence, using \lref{lemma:curve-or-twist}, we prove that for all
$x \in \F{p}$, there exists a point $P \in \F{p^2}\times\F{p^2}$ on
$M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = (x,0) = x$.
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:
forall (x:Zmodp.type),
exists (p: mc curve25519_Fp2_mcuType),
......@@ -529,7 +523,7 @@ Define the functions $\varphi_c$, $\varphi_t$ and $\psi$\\
-- $\varphi_t: M_{486662,2}(\F{p}) \mapsto M_{486662,1}(\F{p^2})$\\
such that $\varphi((x,y)) = ((x,0), (0,y))$.\\
-- $\psi: \F{p^2} \mapsto \F{p}$\\
such that $\psi(x,y) = (x)$.
such that $\psi(x,y) = x$.
\end{dfn}
\begin{lemma}
......@@ -564,7 +558,7 @@ computation in $\F{p^2}$.
$Curve25519\_Fp(n,x)$ computes $\chi_0(n \cdot P)$.
\end{theorem}
which is formalized in Coq as:
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip]
Theorem curve25519_Fp2_ladder_ok:
forall (n : nat) (x:Zmodp.type),
(n < 2^255)%nat ->
......
......@@ -15,7 +15,7 @@ In our case we rely on:
used by Coq must be consistent in order to trust the proofs. As an axiom,
we assume that the functional extensionality is also consistent with that logic.
$$\forall x, f(x) = g(x) \implies f = g$$
\begin{lstlisting}[language=Coq]
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Lemma f_ext: forall (A B:Type),
forall (f g: A -> B),
(forall x, f(x) = g(x)) -> f = g.
......@@ -25,27 +25,24 @@ Lemma f_ext: forall (A B:Type),
Princeton allows a user to prove that a Clight code matches pure Coq
specification.
\item \textbf{CompCert}.
When compiling with CompCert we only need to trust CompCert's {assembly}
semantics, because it has been formally proven correct.
\item \textbf{CompCert}. When compiling with CompCert we only need to trust
CompCert's {assembly} semantics, because it has been formally proven correct.
However, when compiling with other C compilers like Clang or GCC, we need to
trust that the CompCert's Clight semantics matches the C17 standard.
\todo{FIXME}
\item \textbf{\texttt{clightgen}}. The tool making the translation from {C} to
{Clight}. It is the first step of the compilation.
VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
This required us to rewrite the lines into:
\begin{lstlisting}[language=C]
aux1 = a[i];
aux2 = b[i];
{Clight}, the first step of the CompCert compilation.
The VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
This needs to be rewritten into:
\begin{lstlisting}[language=Ctweetnacl,stepnumber=0,belowskip=-0.5 \baselineskip]
aux1 = a[i]; aux2 = b[i];
o[i] = aux1 + aux2;
\end{lstlisting}
The trust of the proof relies on the trust of a correct translation from the
initial version of \emph{TweetNaCl} to \emph{TweetNaclVerifiableC}.
\texttt{clightgen} comes with \texttt{-normalize} flag which
factors out function calls and assignments from inside subexpressions.
The changes required for C code to make it verifiable are now minimal.
The \texttt{-normalize} flag is taking care of this
rewritting and factors out assignments from inside subexpressions.
% The trust of the proof relies on a correct translation from the
% initial version of \emph{TweetNaCl} to \emph{TweetNaClVerifiableC}.
% The changes required for C code to make it verifiable are now minimal.
\item Finally, we must trust the \textbf{Coq kernel} and its
associated libraries; the \textbf{Ocaml compiler} on which we compiled Coq;
......@@ -62,13 +59,13 @@ we removed them.
Peter Wu and Jason A. Donenfeld brought to our attention that the original
\TNaCle{car25519} function carried a risk of undefined behavior if \texttt{c}
is a negative number.
\begin{lstlisting}[language=Ctweetnacl]
\begin{lstlisting}[language=Ctweetnacl,stepnumber=0]
c=o[i]>>16;
o[i]-=c<<16; // c < 0 = UB !
\end{lstlisting}
We replaced this statement with a logical \texttt{and}, proved correctness,
and thus solved this problem.
\begin{lstlisting}[language=Ctweetnacl]
\begin{lstlisting}[language=Ctweetnacl,stepnumber=0]
o[i]&=0xffff;
\end{lstlisting}
......@@ -101,10 +98,13 @@ the workload.
\subheading{A complete proof.}
We provide a mechanized formal proof of the correctness of the X25519
implementation in TweetNaCl.
We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq. Then we proved
that TweetNaCl's implementation of X25519 matches our formalization.
implementation in TweetNaCl from C up the mathematical definitions with a single tool.
We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq.
Then we proved that TweetNaCl's implementation of X25519 matches our formalization.
In a second step we extended the Coq library for elliptic curves \cite{BartziaS14}
by Bartzia and Strub to support Montgomery curves. Using this extension we
proved that the X25519 from the RFC and therefore its implementation in TweetNaCl matches
the mathematical definitions as given in~\cite[Sec.~2]{Ber06}.
by Bartzia and Strub to support Montgomery curves.
Using this extension we proved that the X25519 from the RFC matches the
mathematical definitions as given in~\cite[Sec.~2]{Ber06}.
Therefore in addition to proving the mathematical correctness of TweetNaCl,
we also increases the trust of other works such as
\cite{zinzindohoue2017hacl,Erbsen2016SystematicSO} which rely on RFC~7748.
......@@ -2,7 +2,7 @@
\newif\ifpublic
\usenixtrue
\publicfalse
\publictrue
\ifusenix
\input{_usenix}
......
......@@ -230,6 +230,8 @@ columns=[l]flexible,
% commentstyle={\ttfamily\color{dkgreen}},
%
%moredelim=**[is][\ttfamily\color{red}]{/&}{&/},
aboveskip=3pt,
belowskip=3pt,
literate=
% {\\forall}{{\color{dkgreen}{$\forall\;$}}}1
% {\\exists}{{$\exists\;$}}1
......@@ -355,7 +357,9 @@ literate=
stepnumber=1, % step between two line numbers
numberstyle=\tiny, % line number font size
xleftmargin=5.0ex,
literate=
aboveskip=3pt,
belowskip=1pt,
literate=,
}
\def\TNaCle{\lstinline[language=Ctweetnacl, basicstyle=\ttfamily\normalsize]}
......@@ -396,8 +400,8 @@ literate=
keywordstyle=[4]\color{doc@lstfunctions},
keywordstyle=[5]\color{doc@lstnumbers},
%
aboveskip=5pt,
belowskip=5pt,
% aboveskip=5pt,
% belowskip=5pt,
extendedchars=true,
inputencoding=utf8,
upquote=true, %
......
......@@ -34,7 +34,7 @@
\begin{scope}[yshift=-1.5 cm,xshift=3 cm]
\draw [fill=green!20] (0,0) -- (3.25,0) -- (3.25,-1.375) -- (0, -1.375) -- cycle;
\draw (0,0) node[textstyle, anchor=north west] {\textbf{Thm:}};
\draw (1.675,-0.375) node[textstyle, anchor=north] {$\forall x \in \K, n \in \N, P \in M_{a,b}(\K),$\\$x = \chi(P) \implies$\\ladder $n$ $x$ = $\chi(n \cdot P)$};
\draw (1.675,-0.375) node[textstyle, anchor=north] {$\forall x \in \K, n \in \N, P \in M_{a,b}(\K),$\\$x = \chi_0(P) \implies$\\ladder $n$ $x$ = $\chi_0(n \cdot P)$};
\end{scope}
\path [thick, double, ->] (1.5,-0.375) edge [out=0, in=-180] (3,-0.375);
......
\begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=\scriptsize}]
\draw (6.75,1.5) node[textstyle, anchor=north east] {$p = \p$\\$C = M_{486662,1}$\\$T = M_{486662,2}$\\};
\draw (6.75,1) node[textstyle, anchor=north east] {$p = \p$\\$C = M_{486662,1}$\\$T = M_{486662,2}$\\};
\begin{scope}[yshift=1.5 cm,xshift=-0.5 cm]
\begin{scope}[yshift=1 cm,xshift=-0.5 cm]
\draw [fill=green!20] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$p$ is prime};
\end{scope}
\begin{scope}[yshift=0 cm,xshift=-0.5 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\begin{scope}[yshift=-0.25 cm,xshift=-0.5 cm]
\draw[fill=white] (0.25,0) -- (1.25,0) -- (1.25,-0.75) -- (0.25, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$\F{p}$};
\end{scope}
\begin{scope}[yshift=-1 cm,xshift=1.5 cm]
\begin{scope}[yshift=-1 cm,xshift=1.25 cm]
\draw[fill=green!20] (0,0) -- (1.25,0) -- (1.25,-0.75) -- (0, -0.75) -- cycle;
\draw (0.615,-0.375) node[textstyle, anchor=center] {$\forall x \in \F{p},$\\$x^2 \neq 2$};
\end{scope}
\begin{scope}[yshift=-1 cm,xshift=2.875 cm]
\begin{scope}[yshift=-1 cm,xshift=2.625 cm]
\draw[fill=green!20] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$\forall x \in \F{p},$\\$x^2 \neq a^2-4$};
\end{scope}
\begin{scope}[yshift=-1 cm,xshift=4.5 cm]
\begin{scope}[yshift=-1 cm,xshift=4.375 cm]
\draw[fill=white] (0,0) -- (1,0) -- (1,-0.75) -- (0, -0.75) -- cycle;
\draw (0.5,-0.375) node[textstyle, anchor=center] {$C(\F{p})$};
\end{scope}
......@@ -32,41 +32,41 @@
\draw (0.5,-0.375) node[textstyle, anchor=center] {$T(\F{p})$};
\end{scope}
\path [thick, double, ->] (0.25,0.75) edge [out=-90, in=90] (0.25,0);
\path [thick, double] (1,-0.375) edge [out=0, in=180] (7,-0.375);
\path [thick, double, ->] (2.125,-0.375) edge [out=-90, in=90] (2.125,-1);
\path [thick, double, ->] (3.625,-0.375) edge [out=-90, in=90] (3.625,-1);
\path [thick, double, ->] (5,-0.375) edge [out=-90, in=90] (5,-1);
\path [thick, double, ->] (7,-0.375) edge [out=-90, in=90] (7,-1);
\path [thick, double, ->] (0.25,0.25) edge [out=-90, in=90] (0.25,-0.25);
\path [thick, double] (0.75,-0.625) edge [out=0, in=180] (7,-0.625);
\path [thick, double, ->] (1.875,-0.625) edge [out=-90, in=90] (1.875,-1);
\path [thick, double, ->] (3.375,-0.625) edge [out=-90, in=90] (3.375,-1);
\path [thick, double, ->] (4.875,-0.625) edge [out=-90, in=90] (4.875,-1);
\path [thick, double, ->] (7,-0.625) edge [out=-90, in=90] (7,-1);
\begin{scope}[yshift=-2.5 cm,xshift=1.5 cm]
\draw[fill=green!20] (-0.35,0) -- (1.85,0) -- (1.85,-1.25) -- (-0.35, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\exists P \in C(\F{p}),$\\$\exists Q \in T(\F{p})$,\\$x = \chi(P)\vee x = \chi(Q)$};
\begin{scope}[yshift=-2.5 cm,xshift=1.25 cm]
\draw[fill=green!20] (-0.40,0) -- (1.90,0) -- (1.90,-1.25) -- (-0.42, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\exists P \in C(\F{p}),$\\$\exists Q \in T(\F{p})$,\\$x = \chi_0(P)\vee x = \chi_0(Q)$};
\end{scope}
\begin{scope}[yshift=-2.5 cm,xshift=4.25 cm]
\draw[fill=green!20] (-0.20,0) -- (1.70,0) -- (1.70,-1.25) -- (-0.20, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall P \in C(\F{p}),$\\$x = \chi(P)\implies$\\lad. $n$ $x = \chi(n \cdot P)$};
\begin{scope}[yshift=-2.5 cm,xshift=4.125 cm]
\draw[fill=green!20] (-0.25,0) -- (1.70,0) -- (1.70,-1.25) -- (-0.25, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall P \in C(\F{p}),$\\$x = \chi_0(P)\implies$\\lad. $n$ $x = \chi_0(n \cdot P)$};
\end{scope}
\begin{scope}[yshift=-2.5 cm,xshift=6.25 cm]
\draw[fill=green!20] (-0.20,0) -- (1.70,0) -- (1.70,-1.25) -- (-0.20, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall Q \in T(\F{p}),$\\$x = \chi(Q)\implies$\\lad. $n$ $x = \chi(n \cdot Q)$};
\draw[fill=green!20] (-0.25,0) -- (1.70,0) -- (1.70,-1.25) -- (-0.25, -1.25) -- cycle;
\draw (0.75,0) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall Q \in T(\F{p}),$\\$x = \chi_0(Q)\implies$\\lad. $n$ $x = \chi_0(n \cdot Q)$};
\end{scope}
\path [thick, double, ->] (2.125,-1.75) edge [out=-90, in=90] (2.125,-2.5);
\path [thick, double] (2.125,-2.125) edge [out=0, in=180] (7,-2.125);
\path [thick, double] (3.625,-1.75) edge [out=-90, in=90] (3.625,-2.125);
\path [thick, double, ->] (5,-1.75) edge [out=-90, in=90] (5,-2.5);
\path [thick, double, ->] (1.875,-1.75) edge [out=-90, in=90] (1.875,-2.5);
\path [thick, double] (1.875,-2.125) edge [out=0, in=180] (7,-2.125);
\path [thick, double] (3.375,-1.75) edge [out=-90, in=90] (3.375,-2.125);
\path [thick, double, ->] (4.875,-1.75) edge [out=-90, in=90] (4.875,-2.5);
\path [thick, double, ->] (7,-1.75) edge [out=-90, in=90] (7,-2.5);
% F(p^2)
\path [thick, double, ->] (0.25,-0.75) edge [out=-90, in=90] (0.25,-2.5);
\path [thick, double, ->] (0.25,-1) edge [out=-90, in=90] (0.25,-2.5);
\begin{scope}[yshift=-2.5 cm,xshift=-0.5 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw[fill=white] (0.25,0) -- (1.25,0) -- (1.25,-0.75) -- (0.25, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$\F{p^2}$};
\end{scope}
......@@ -74,40 +74,40 @@
% C(F(p^2))
\begin{scope}[yshift=-5 cm,xshift=-0.5 cm]
\begin{scope}[yshift=-4.5 cm,xshift=-0.5 cm]
\draw[fill=white] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw (0.75,-0.375) node[textstyle, anchor=center] {$C(\F{p^2})$};
\end{scope}
\begin{scope}[yshift=-5 cm,xshift=1.5 cm]
\begin{scope}[yshift=-4.5 cm,xshift=1.5 cm]
\draw[fill=green!20] (0,0) -- (2,0) -- (2,-0.75) -- (0, -0.75) -- cycle;
\draw (1,-0.375) node[textstyle, anchor=center] {$C(\F{p}) \subset C(\F{p^2})$};
\end{scope}
\begin{scope}[yshift=-6 cm,xshift=1.5 cm]
\begin{scope}[yshift=-5.5 cm,xshift=1.5 cm]
\draw[fill=green!20] (0,0) -- (2,0) -- (2,-0.75) -- (0, -0.75) -- cycle;
\draw (1,-0.375) node[textstyle, anchor=center] {$T(\F{p}) \subset C(\F{p^2})$};
\end{scope}
\path [thick, double, ->] (1,-5.375) edge [out=0, in=-180] (1.5,-5.375);
\path [thick, double] (1.25,-5.375) edge [out=-90, in=90] (1.25,-6.375);
\path [thick, double, ->] (1.25,-6.375) edge [out=0, in=-180] (1.5,-6.375);
\path [thick, double, ->] (1,-4.875) edge [out=0, in=-180] (1.5,-4.875);
\path [thick, double] (1.25,-4.875) edge [out=-90, in=90] (1.25,-5.835);
\path [thick, double, ->] (1.25,-5.835) edge [out=0, in=-180] (1.5,-5.835);
\begin{scope}[yshift=-5 cm,xshift=4.5 cm]
\begin{scope}[yshift=-4.5 cm,xshift=4.5 cm]
\draw [fill=green!20] (0,0) -- (3.25,0) -- (3.25,-1.75) -- (0, -1.75) -- cycle;
\draw (0,0) node[textstyle, anchor=north west] {\textbf{Thm:}};
\draw (1.675,-0.375) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall P \in C(\F{p^2}),$\\$x = \chi(P)\implies$\\ladder $n$ $x = \chi(n \cdot P)$};
\draw (1.675,-0.375) node[textstyle, anchor=north] {$\forall x \in \F{p},$\\$\forall P \in C(\F{p^2}),$\\$x = \chi_0(P)\implies$\\ladder $n$ $x = \chi_0(n \cdot P)$};
\end{scope}
\path [thick, double] (2.25,-4.375) edge [out=0, in=180] (6.75,-4.375);
\path [thick, double] (2.25,-3.75) edge [out=-90, in=90] (2.25,-4.375);
\path [thick, double] (4.75,-3.75) edge [out=-90, in=90] (4.75,-4.375);
\path [thick, double] (6.75,-3.75) edge [out=-90, in=90] (6.75,-4.375);
\path [thick, double] (1.875,-4.125) edge [out=0, in=180] (7,-4.125);
\path [thick, double] (1.875,-3.75) edge [out=-90, in=90] (1.875,-4.125);
\path [thick, double] (4.875,-3.75) edge [out=-90, in=90] (4.875,-4.125);
\path [thick, double] (7,-3.75) edge [out=-90, in=90] (7,-4.125);
\path [thick, double] (3.5,-5.375) edge [out=0, in=180] (3.75,-5.375);
\path [thick, double] (3.5,-6.375) edge [out=0, in=180] (3.75,-6.375);
\path [thick, double] (3.75,-6.375) edge [out=90, in=-90] (3.75,-4.375);
\path [thick, double] (3.5,-4.875) edge [out=0, in=180] (3.75,-4.875);
\path [thick, double] (3.5,-5.835) edge [out=0, in=180] (3.75,-5.835);
\path [thick, double] (3.75,-5.835) edge [out=90, in=-90] (3.75,-4.125);
\path [thick, double, ->] (6.125,-4.375) edge [out=-90, in=90] (6.125,-5);
\path [thick, double, ->] (6.125,-4.125) edge [out=-90, in=90] (6.125,-4.5);
\end{tikzpicture}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment