Commit e038a0af authored by Benoit Viguier's avatar Benoit Viguier
Browse files

cleaning + working on slides

parent b6a67a02
......@@ -14,8 +14,6 @@ Class Ops (T T': Type) (Mod: T -> T):=
Sel25519 : Z -> T -> T -> T;
Getbit : Z -> T' -> Z;
(* Mod : T -> T; *)
Mod_ZSel25519_eq : forall b p q, Mod (Sel25519 b p q) = Sel25519 b (Mod p) (Mod q);
Mod_ZA_eq : forall p q, Mod (A p q) = Mod (A (Mod p) (Mod q));
Mod_ZM_eq : forall p q, Mod (M p q) = Mod (M (Mod p) (Mod q));
......
(* Require Import ssreflect.
From Tweetnacl.Libs Require Import Export.
From Tweetnacl.Gen Require Import Get_abcdef.
From Tweetnacl.Gen Require Import AMZubSqSel.
From Tweetnacl.Gen Require Import UPIC.
From Tweetnacl.Gen Require Import montgomery_rec.
From Tweetnacl.Gen Require Import montgomery_rec_eq.
From Tweetnacl.Gen Require Import abstract_fn_rev.
Section CryptoScalarMult.
Context {T : Type}.
Context {T' : Type}.
Context {OT : Ops T T'}.
Context {OP : Ops_ext T T'}.
Definition CryptoScalarMult_rec (n p:T') : T' :=
let t := (montgomery_rec 255 (Clamp n) C_1 (Unpack25519 p) C_0 C_1 C_0 C_0 (Unpack25519 p)) in
let a := get_a t in
let c := get_c t in
Pack25519 (M a (Inv25519 c)).
Definition CryptoScalarMult_rev (n p: T') : T' :=
let t := (abstract_fn_rev 255 254 (Clamp n) C_1 (Unpack25519 p) C_0 C_1 C_0 C_0 (Unpack25519 p)) in
let a := get_a t in
let c := get_c t in
Pack25519 (M a (Inv25519 c)).
Lemma CryptoScalarMult_eq : forall n p, CryptoScalarMult_rev n p = CryptoScalarMult_rec n p.
Proof.
intros.
rewrite /CryptoScalarMult_rev /CryptoScalarMult_rec.
change (255) with (S (Z.to_nat 254)).
rewrite montgomery_rec_eq_fn_rev.
2: omega.
reflexivity.
Qed.
End CryptoScalarMult.
*)
\ No newline at end of file
(* Require Import ssreflect.
From Tweetnacl.Libs Require Import Export.
From Tweetnacl.Gen Require Import Get_abcdef.
From Tweetnacl.Gen Require Import AMZubSqSel.
From Tweetnacl.Gen Require Import AMZubSqSel_Prop.
From Tweetnacl.Gen Require Import UPIC.
From Tweetnacl.Gen Require Import UPIC_Prop.
(* From Tweetnacl.Gen Require Import montgomery_rec. *)
(* From Tweetnacl.Gen Require Import montgomery_rec_eq. *)
From Tweetnacl.Gen Require Import abstract_fn_rev.
From Tweetnacl.Gen Require Import abstract_fn_rev_eq.
From Tweetnacl.Gen Require Import Crypto_ScalarMult.
Section CryptoScalarMult_eq.
Context {T : Type}.
Context {T' : Type}.
Context {O_T : Ops T T'}.
Context {O_ext_T : Ops_ext T T'}.
Context {U : Type}.
Context {O_U : Ops U U}.
Context {O_ext_U : Ops_ext U U}.
Context {O_MP_TU: @Ops_Mod_P T T' U O_T O_U}.
Context {OP_ext_TU: @Ops_ext_Mod_P T T' U O_U O_ext_T O_ext_U}.
Variable P_eq : forall p, AMZubSqSel_Prop.P p = P p.
Variable P'_eq : forall p, AMZubSqSel_Prop.P' p = P' p.
Theorem Crypto_ScalarMult_eq: forall (n p:T'),
P' (CryptoScalarMult_rev n p) = CryptoScalarMult_rev (P' n) (P' p).
Proof.
intros n p.
rewrite /CryptoScalarMult_rev.
rewrite Pack25519_eq.
rewrite ?Mod_Pack25519_eq.
rewrite -P_eq.
rewrite M_eq.
rewrite Mod_ZM_eq.
symmetry.
rewrite Mod_ZM_eq.
symmetry.
f_equal ; f_equal.
{
rewrite abstract_fn_rev_eq_a.
2:omega.
rewrite C_0_eq C_1_eq.
rewrite ?P_eq ?P'_eq.
rewrite Unpack25519_eq Clamp_eq.
reflexivity.
}
{
rewrite P_eq.
rewrite Inv25519_eq.
rewrite Inv25519_mod_eq.
symmetry.
rewrite Inv25519_mod_eq.
f_equal ; f_equal.
rewrite -P_eq.
rewrite abstract_fn_rev_eq_c.
2: omega.
rewrite C_0_eq C_1_eq.
rewrite ?P_eq ?P'_eq.
rewrite Unpack25519_eq Clamp_eq.
reflexivity.
}
Qed.
End CryptoScalarMult_eq. *)
\ No newline at end of file
(* Class Ops_ext (T T': Type) :=
{
Unpack25519 : T' -> T;
Pack25519 : T -> T';
Inv25519 : T -> T;
Clamp : T' -> T';
}.
*)
\ No newline at end of file
(* From Tweetnacl.Libs Require Import Export.
From Tweetnacl.Gen Require Export UPIC.
Open Scope Z.
Class Ops_ext_List `{@Ops_ext (list Z) (list Z)} :=
{
Inv25519_Zlength : forall a, Zlength a = 16 -> Zlength (Inv25519 a) = 16;
Unpack_Zlength : forall a, Zlength a = 32 -> Zlength (Unpack25519 a) = 16;
Clamp_Zlength : forall a, Zlength a = 32 -> Zlength (Clamp a) = 32;
Pack_Zlength : forall a, Zlength a = 16 -> Zlength (Pack25519 a) = 32;
Clamp_bound : forall l,
Forall (fun x => 0 <= x < Z.pow 2 8) l ->
Forall (fun x => 0 <= x < Z.pow 2 8) (Clamp l);
Inv25519_bound: forall g,
Zlength g = 16 ->
Forall (fun x => -38 <= x < Z.pow 2 16 + 38) g ->
Forall (fun x => -38 <= x < Z.pow 2 16 + 38) (Inv25519 g);
Pack25519_bound : forall (l:list Z),
Zlength l = 16 ->
Forall (fun x => -2^62 < x < 2^62) l ->
Forall (fun x => 0 <= x < 2^8) (Pack25519 l)
}.
Close Scope Z. *)
\ No newline at end of file
(* From Tweetnacl.Libs Require Import Export.
From Tweetnacl.Gen Require Import AMZubSqSel.
From Tweetnacl.Gen Require Import UPIC.
Class Ops_ext_Mod_P {T T' U:Type} `(Ops U U) `(Ops_ext T T') `(Ops_ext U U) :=
{
P : T -> U;
P' : T' -> U;
Inv25519_eq : forall a, Mod (P (Inv25519 a)) = Mod (Inv25519 (P a));
Inv25519_mod_eq : forall a, Mod (Inv25519 a) = Mod (Inv25519 (Mod a));
Pack25519_eq : forall l, P' (Pack25519 l) = Pack25519 (P l);
Mod_Pack25519_eq : forall p, Pack25519 p = Mod p;
Unpack25519_eq : forall l, P (Unpack25519 l) = Unpack25519 (P' l);
Clamp_eq : forall l, P' (Clamp l) = Clamp (P' l);
}. *)
\ No newline at end of file
......@@ -35,63 +35,6 @@ From Tweetnacl.Mid Require Import Instances.
Open Scope Z.
(* Section Crypto_Scalarmult. *)
(* Definition Mod := (fun x => Z.modulo x (Z.pow 2 255 - 19)). *)
(* Context (Z_Ops : (Ops Z Z) modP).
Context (List_Z_Ops : Ops (list Z) (list Z) id).
Context (List_Z_Ops_Prop : @Ops_List List_Z_Ops).
Context (List_Z_Ops_Prop_Correct : @Ops_Prop_List_Z modP List_Z_Ops Z_Ops).
Local Instance List16_Ops : (Ops (@List16 Z) (List32B) id) := {}.
Proof.
apply A_List16.
apply M_List16.
apply Zub_List16.
apply Sq_List16.
apply C_0_List16.
apply C_1_List16.
apply C_121665_List16.
apply Sel25519_List16.
apply getbit_List32B.
simpl ; reflexivity.
simpl ; reflexivity.
simpl ; reflexivity.
simpl ; reflexivity.
simpl ; reflexivity.
simpl ; reflexivity.
Defined.
Local Instance List16_Z_Eq : @Ops_Mod_P (@List16 Z) (List32B) Z modP id List16_Ops Z_Ops := {
P l := (ZofList 16 (List16_to_List l));
P' l := (ZofList 8 (List32_to_List l));
}.
Proof.
- intros [a Ha] [b Hb] ; simpl List16_to_List; rewrite -A_correct; reflexivity.
- intros [a Ha] [b Hb] ; simpl List16_to_List.
apply AMZubSqSel_Correct.mult_GF_Zlengh ; assumption.
- intros [a Ha] [b Hb] ; simpl ; f_equal ; rewrite -Zub_correct; reflexivity.
- intros [a Ha] ; simpl List16_to_List ; apply Sq_GF_Zlengh ; try assumption.
- simpl List16_to_List ; f_equal; rewrite -C_121665_correct ; reflexivity.
- simpl List16_to_List ; f_equal; rewrite -C_0_correct ; reflexivity.
- simpl List16_to_List ; f_equal; rewrite -C_1_correct ; reflexivity.
- intros b [p Hp] [q Hq] ; simpl List16_to_List ; f_equal ; rewrite -Sel25519_correct ; reflexivity.
- intros b [p Hp] ; simpl ; symmetry ; rewrite GetBit_correct ; try assumption ; reflexivity.
Defined.
Local Instance List16_List_Z_Eq : @Ops_Mod_P (List16 Z) (List32B) (list Z) id id List16_Ops List_Z_Ops := {
P := List16_to_List;
P' := List32_to_List
}.
Proof.
intros [] [] ; reflexivity.
intros [] [] ; reflexivity.
intros [] [] ; reflexivity.
intros [] ; reflexivity.
reflexivity.
reflexivity.
reflexivity.
intros b [] [] ; reflexivity.
intros i [] ; reflexivity.
Defined. *)
Definition Crypto_Scalarmult n p :=
let a := get_a (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p)) in
let c := get_c (montgomery_fn List_Z_Ops 255 254 (clamp n) Low.C_1 (Unpack25519 p) Low.C_0 Low.C_1 Low.C_0 Low.C_0 (Unpack25519 p)) in
......
This diff is collapsed.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% SLIDE 1
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]{Elliptic Curves 101}
% \newcommand{\PP}{\mathcal{P}}
% \newcommand{\KK}{\mathcal{K}}
% \newcommand{\PK}{x}
% \newcommand{\PKX}{Q}
% \newcommand{\X}{{\bf x}}
% \newcommand{\E}{\mathcal{E}}
% \newcommand{\K}{\mathcal{K}}
% \newcommand{\J}{\mathcal{J}}
\newcommand{\XX}[1]{\ensuremath{{\textbf{x}}(#1)}}
\begin{center}
\begin{tikzpicture}
\newcommand*{\xlen}{-4}
\newcommand*{\ylen}{1.5}
\coordinate (cquoops) at (\xlen, \ylen);
\coordinate (cquosca) at (\xlen, \ylen-0.8);
\coordinate (cquoadd) at (\xlen, \ylen-1.6);
\coordinate (cquoxdbladd) at (\xlen, \ylen-2.4);
\coordinate (cgroupops) at (\xlen, 3*\ylen);
\coordinate (cgroupsca) at (\xlen, 3*\ylen-0.7);
\coordinate (cgroupadd) at (\xlen, 3*\ylen-1.4);
\node [anchor=west] (groupops) at (cgroupops)
{\underline{\emph{Operations on $E: B y^2 = x^3 + A x^2 + x$}}};
\node [anchor=west] (groupsca) at (cgroupsca)
{$\textcolor{rured}{(1)}\,\,P \mapsto [2]P$};
\node [anchor=west] (groupadd) at (cgroupadd)
{$\textcolor{rured}{(2)}\,\,\big\{P,Q\big\}\mapsto P + Q$};
\visible<8->{
\node [anchor=west] (quoops) at (cquoops)
{\underline{\emph{Operations on $\mathbb{F}_p$}}};
\node [anchor=west] (quosca) at (cquosca)
{$\textcolor{rured}{(1)}\,\,\XX{P} \mapsto \XX{[2]P}$};
}
\visible<16->{
\node [anchor=west] (quoadd) at (cquoadd)
{$\textcolor{rured}{(2)}\,\,\Big\{\XX{P},\XX{Q}\Big\}
\mapsto \Big\{\XX{P+Q},\XX{P-Q}\Big\}$};
}
\visible<17->{
\node [anchor=west] (cquoxdbladd) at (cquoxdbladd)
{$\implies\,\,\Big\{\XX{P},\XX{Q},\XX{P-Q}\Big\}
\mapsto \XX{P+Q}$};
}
\newcommand*{\aaa}{-6}
\newcommand*{\bbb}{7}
\newcommand*{\px}{-1.85}
\newcommand*{\py}{3.4305}
\newcommand*{\dfdxp}{4.2675}
\newcommand*{\dfdyp}{-2*\py}
\newcommand*{\pxd}{4.0868}
\newcommand*{\pyd}{7.4716}
\newcommand*{\qx}{0.9}
\newcommand*{\qy}{1.5261}
\newcommand*{\pqx}{1.42956}
\newcommand*{\pqy}{-1.15937}
\newcommand*{\qpx}{4.19886}
\newcommand*{\qpy}{7.4716}
\begin{axis}
[
axis x line = center,
axis line style = thick,
xlabel = $\mathbb{F}_p$,
axis y line = none,
ticks = none,
xmin=-4,
xmax=8,
ymin=-9,
ymax=9,
samples=200,
domain=-2.9005:5,
smooth
]
\addplot [rured,ultra thick] {sqrt(x^3+\aaa*x+\bbb)};
\addplot [rured,ultra thick] {-sqrt(x^3+\aaa*x+\bbb)};
\only<2-8>{
\addplot [msblue,ultra thick,mark=*] coordinates {(\px,sqrt(\px^3+\aaa*\px+\bbb)};
}
\only<3-8>{
\addplot [msblue,ultra thick,mark=*] coordinates {(\px,-sqrt(\px^3+\aaa*\px+\bbb)};
}
\only<4>{
\draw [thick,<-,dashed] ([yshift=0.8mm]axis cs:\px,0) -- (axis cs:\px,\py);
\draw [thick,<-,dashed] ([yshift=-0.8mm]axis cs:\px,0) -- (axis cs:\px,-\py);
}
\only<4->{
\addplot [msgreen,ultra thick,mark=*] coordinates {(\px,0)};
}
\only<5-6>{
\addplot [thick,dashed] {\py - (\dfdxp / \dfdyp) * ( x - \px )};
\addplot [msyellow,ultra thick,mark=*] coordinates {(\pxd,sqrt(\pxd^3+\aaa*\pxd+\bbb)};
}
\only<6>{
\draw [thick,<-,dashed] ([yshift=0.8mm]axis cs:\pxd,0) -- (axis cs:\pxd,\pyd);
}
\only<6-8>{
\addplot [orange,ultra thick,mark=*] coordinates {(\pxd,0)};
}
\only<7>{
\addplot [thick,dashed] {-\py - (\dfdxp / -\dfdyp) * ( x - \px )};
\addplot [msyellow,ultra thick,mark=*] coordinates {(\pxd,-sqrt(\pxd^3+\aaa*\pxd+\bbb)};
\draw [thick,<-,dashed] ([yshift=-0.8mm]axis cs:\pxd,0) -- (axis cs:\pxd,-\pyd);
}
\only<9->{
\addplot [msgreen,ultra thick,mark=*] coordinates {(\qx,0)};
}
\only<10->{
\addplot [msblue,ultra thick,mark=*] coordinates {(\px,sqrt(\px^3+\aaa*\px+\bbb)};
\addplot [msblue,ultra thick,mark=*] coordinates {(\px,-sqrt(\px^3+\aaa*\px+\bbb)};
\addplot [msblue,ultra thick,mark=*] coordinates {(\qx,sqrt(\qx^3+\aaa*\qx+\bbb)};
\addplot [msblue,ultra thick,mark=*] coordinates {(\qx,-sqrt(\qx^3+\aaa*\qx+\bbb)};
}
\only<11>{
\addplot [thick,dashed] { (\py - \qy) / (\px - \qx)*(x - \qx) + \qy};
}
\only<12>{
\addplot [thick,dashed] { (-\py + \qy) / (\px - \qx)*(x - \qx) - \qy};
}
\only<13>{
\addplot [thick,dashed] { (-\py - \qy) / (\px - \qx)*(x - \qx) + \qy};
}
\only<14>{
\addplot [thick,dashed] { (\py + \qy) / (\px - \qx)*(x - \qx) - \qy};
}
\only<11->{
\addplot [msyellow,ultra thick,mark=*] coordinates {(\pqx,sqrt(\pqx^3+\aaa*\pqx+\bbb)};
}
\only<12->{
\addplot [msyellow,ultra thick,mark=*] coordinates {(\pqx,-sqrt(\pqx^3+\aaa*\pqx+\bbb)};
}
\only<13->{
\addplot [msyellow,ultra thick,mark=*] coordinates {(\qpx,sqrt(\qpx^3+\aaa*\qpx+\bbb)};
}
\only<14->{
\addplot [msyellow,ultra thick,mark=*] coordinates {(\qpx,-sqrt(\qpx^3+\aaa*\qpx+\bbb)};
}
\only<15>{
\draw [thick,<-,dashed] ([yshift=0.8mm]axis cs:\pqx,0) -- (axis cs:\pqx,-\pqy);
\draw [thick,<-,dashed] ([yshift=-0.8mm]axis cs:\pqx,0) -- (axis cs:\pqx,\pqy);
\draw [thick,<-,dashed] ([yshift=-0.8mm]axis cs:\qpx,0) -- (axis cs:\qpx,-\qpy);
\draw [thick,<-,dashed] ([yshift=0.8mm]axis cs:\qpx,0) -- (axis cs:\qpx,\qpy);
}
\only<15->{
\addplot [orange,ultra thick,mark=*] coordinates {(\pqx,0)};
\addplot [orange,ultra thick,mark=*] coordinates {(\qpx,0)};
}
\end{axis}
\end{tikzpicture}
\end{center}
\end{frame}
......@@ -168,7 +168,7 @@
\definecolor{doc@lstfunctions}{HTML}{006600} % dark green
\definecolor{doc@lststring}{HTML}{FF5500} % orange
\definecolor{doc@lstkeyword}{HTML}{0000CC} % deep blue
\definecolor{doc@lstkeyword2}{rgb}{0.127,0.427,0.514}
\definecolor{doc@lstkeyword2}{HTML}{206c83}
\definecolor{doc@lstdirective}{HTML}{881000} % dark red
\definecolor{doc@lstconstants}{HTML}{0033AA} % dark blue
\definecolor{doc@lstidentifiers2}{HTML}{FF0033} % purple-red
......@@ -189,7 +189,7 @@
morekeywords=[1]{PROP, SEP, POST, PRE, LOCAL, DECLARE, WITH, Definition},
morekeywords=[2]{val, list, Z, tuchar, uch32, lg16, share, tint},
morekeywords=[3]{fun, tptr, mVI, mVI64, Vint, OF},
morekeywords=[4]{Forall, temp, Zlength, writable_share, gvar},
morekeywords=[4]{Forall, temp, Zlength, writable_share, readable_share, gvar},
morekeywords=[5]{ 0, 2^8, 16, 32},
sensitive=true,
mathescape=true,
......@@ -198,17 +198,18 @@
morecomment=[l]{//},
identifierstyle=\color[rgb]{0,0,0},
delim=[s][\color{doc@lstdirective}]{(*}{*)},
backgroundcolor=\color{doc@lstbackground}, % set the background color
% backgroundcolor=\color{doc@lstbackground}, % set the background color
literate=
{=>}{{$\mapsto$}}1
{<}{{$\!<\!$}}1
{<=}{{$\!\leq\!$}}1
{[\{}{$\!\!\![\!\!\{\!\!$}1
{\}]}{$\!\!\}\!\!]\!\!\!$}1
{<<(}{<\!\!\-\!\-\!\!(}1
{)--}{)\!\!\-\!\-\!\!}1
{<<(}{$\leftarrow$\!\!(}1
{)--}{)\!\!$-$}1
{fun}{{\color{doc@lstkeyword2}{$\lambda\!\!$}}}1
{2^8}{{\color{doc@lstnumbers}{$2^8$}}}1
{2^62}{{\color{doc@lstnumbers}{$2^{62}$}}}1
}
\def\VSTe{\lstinline[language=CoqVST, basicstyle=\ttfamily\normalsize]}
\def\VSTes{\lstinline[language=CoqVST, basicstyle=\scriptsize]}
......@@ -241,14 +242,13 @@ morekeywords=[1]{Section, Module, End, Require, Import, Export,
Remark, Example, Proof, Goal, Save, Qed, Defined, Hint, Resolve,
Rewrite, View, Search, Show, Print, Printing, All, Eval, Check,
Projections, inside, outside, Def}
morekeywords=[2]{list, Z, expr_inv, positive, formula_inv, bool, Prop, nat, T, Type},
morekeywords=[3]{forall, fun, match, end, with, measure, if, then, else, let, in,
ring},
morekeywords=[2]{list, Z, positive, bool, K, Prop, nat, T, Type},
morekeywords=[3]{forall, fun, match, end, with, measure, if, then, else, let, in, ring},
morekeywords=[4]{Forall, ZofList, Zlength},
morekeywords=[5]{ 0, 1, 2, 3, 16, 32, 254, true},
morekeywords=[5]{ 0, 1, 2, 3, 4, 16, 32, 254, true, false},
sensitive=true,
mathescape=true,
alsoletter = {0123456789^} ,
% mathescape=true,
alsoletter= {0123456789^} ,
% Comments delimiters, we do turn this off for the manual
morecomment=[s]{(*}{*)},
% Spaces are not displayed as a special character
......@@ -257,11 +257,9 @@ showstringspaces=false,
% String delimiters
morestring=[b]",
morestring=[d]’,
% String delimiters
% morestring=[b]",
morestring=[d]’,
% Size of tabulations
tabsize=3,
% Style for sorts keywords
% Enables ASCII chars 128 to 255
extendedchars=false,
% Case sensitivity
......@@ -272,10 +270,16 @@ breaklines=false,
% basicstyle=\small,
% Position of captions is bottom
captionpos=b,
backgroundcolor=\color{white}, % set the background color
backgroundcolor=\color{black!2}, % set the background color
% backgroundcolor=\color{doc@lstbackground}, % set the background color
% flexible columns
columns=[l]flexible,
keywordstyle=\color{doc@lstkeyword},
keywordstyle=[1]\color{doc@lstidentifiers2},
keywordstyle=[2]\color{doc@lstconstants},
keywordstyle=[3]\color{doc@lstkeyword2},
keywordstyle=[4]\color{doc@lstfunctions},
keywordstyle=[5]\color{doc@lstnumbers},
literate=
% {\\forall}{{\color{dkgreen}{$\forall\;$}}}1
% {\\exists}{{$\exists\;$}}1
......@@ -288,6 +292,7 @@ literate=
{<->}{{$\leftrightarrow\;$}}1
{<}{{$\!<\!$}}1
{<>}{{$\neq$}}1
{!=}{{$\neq$}}1
{<=}{{$\!\leq\!$}}1
% {\#}{{$^\star$}}1
% {\\o}{{$\circ\;$}}1
......@@ -312,10 +317,23 @@ literate=
{Z16.lst}{{\color{doc@lstfunctions}{$\mathbb{Z}$16.lst}}}1
{\\N}{{$\mathbb{N}$}}1
{\\Z}{{$\mathbb{Z}$}}1
{\\K}{{$\mathbb{K}$}}1
{^n}{{$^n$}}1
{^2}{{$^2$}}1
{^3}{{$^3$}}1
{^255}{{$^{255}$}}1
{p1}{{p$_1$}}1
{p2}{{p$_2$}}1
{x1}{{x$_1$}}1
{x2}{{x$_2$}}1
{y1}{{y$_1$}}1
{y2}{{y$_2$}}1
{xs}{{x$_s$}}1
{\\boxplus}{{$\boxplus$}}1
{\\circ}{{$\circ$}}1
{\\GF}{{$\mathbb{F}_{2^{255}-19}$}}1
{\\infty}{{$\infty$}}1
%
%
}[keywords,comments,strings]
......@@ -362,7 +380,7 @@ morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct,
nosimpl, when},
%
% Sorts
morekeywords=[3]{Type, Prop, Set, true, false, option},
morekeywords=[3]{Type, Prop, Set, true, false, option, bool, list, Z, positive},
%
% Various tactics, some are std Coq subsumed by ssr, for the manual purpose
morekeywords=[4]{pose, set, move, case, elim, apply, clear, hnf,
......@@ -380,6 +398,9 @@ morekeywords=[5]{by, done, exact, reflexivity, tauto, romega, omega,
% Control
morekeywords=[6]{do, last, first, try, idtac, repeat},
%
% Control
morekeywords=[7]{Forall, ZofList, Zlength, length},
%
% Comments delimiters, we do turn this off for the manual
morecomment=[s]{(*}{*)},
%
......@@ -444,12 +465,15 @@ literate=
{<==}{{$\leq\;$}}1
{\#}{{$^\star$}}1
{\\o}{{$\circ\;$}}1
{\@}{{$\cdot$}}1
% {\@}{{$\cdot$}}1
{\/\\}{{$\wedge\;$}}1
{\\\/}{{$\vee\;$}}1
{<}{{$\!<\!$}}1
{<>}{{$\neq$}}1
{!=}{{$\neq$}}1
{++}{{\texttt{++}}}1
{~}{{\ }}1
{\@\@}{{$@$}}1
% {\@\@}{{$@$}}1
{:GF}{{\color{doc@lstfunctions}{:$GF$}}}1
{2^8}{{\color{doc@lstnumbers}{$2^8$}}}1
{2^16}{{\color{doc@lstnumbers}{$2^{16}$}}}1
......@@ -459,13 +483,27 @@ literate=
{2^255-19}{{\color{doc@lstnumbers}{$2^{255}-19$}}}1
{2^255-21}{{\color{doc@lstnumbers}{$2^{255}-21$}}}1
{fun}{{\color{doc@lstkeyword2}{$\lambda\!\!$}}}1
{\\mapsto}{{$\mapsto\;$}}1
{\\hline}{{\rule{\linewidth}{0.5pt}}}1
{Z16.lst}{{\color{doc@lstfunctions}{$\mathbb{Z}$16.lst}}}1
{\\N}{{$\mathbb{N}$}}1
{\\Z}{{$\mathbb{Z}$}}1
{\\K}{{$\mathbb{K}$}}1
{^n}{{$^n$}}1
{^m}{{$^m$}}1
{^2}{{$^2$}}1
{^3}{{$^3$}}1
{^255}{{$^{255}$}}1
{p1}{{p$_1$}}1
{p2}{{p$_2$}}1
{x1}{{x$_1$}}1
{x2}{{x$_2$}}1
{y1}{{y$_1$}}1
{y2}{{y$_2$}}1
{xs}{{x$_s$}}1
{\\boxplus}{{$\boxplus$}}1