From 946a1dcdce00d4a350fee92ae4931300e6170719 Mon Sep 17 00:00:00 2001
From: Guillermo Ramos
Date: Thu, 16 Jul 2015 03:17:46 +0200
Subject: File renaming

---
 defs.tex | 236 ---------------------------------------------------------------
 1 file changed, 236 deletions(-)
 delete mode 100755 defs.tex

(limited to 'defs.tex')

diff --git a/defs.tex b/defs.tex
deleted file mode 100755
index 3cc5e4c..0000000
--- a/defs.tex
+++ /dev/null
@@ -1,236 +0,0 @@
-% Source: EasyCrypt manual (https://www.easycrypt.info)
-
-%% Names
-% Tools
-\newcommand{\EasyCrypt}{\textsf{EasyCrypt}\xspace}
-\newcommand{\CertiCrypt}{\textsf{CertiCrypt}\xspace}
-\newcommand{\CertiPriv}{\textsf{CertiPriv}\xspace}
-\newcommand{\SsReflect}{\textsf{SsReflect}\xspace}
-\newcommand{\Coq}{\textsf{Coq}\xspace}
-\newcommand{\WhyThree}{\textsf{Why3}\xspace}
-
-% Languages and Logics
-\newcommand{\pWHILE}{\textsf{p}\textsc{While}\xspace}
-\newcommand{\pRHL}{\textsf{pRHL}\xspace}
-
-%% Security properties and schemes
-\newcommand{\INDCPA}{\textsf{IND-CPA}\xspace}
-\newcommand{\INDCCAone}{\textsf{IND-CCA1}\xspace}
-\newcommand{\INDCCA}{\textsf{IND-CCA}\xspace}
-\newcommand{\EFCMA}{\textsf{EF-CMA}\xspace}
-\newcommand{\LCDH}{\ensuremath{\mathsf{LCDH}}\xspace}
-\newcommand{\CDH}{\textsf{CDH}\xspace}
-\newcommand{\DDH}{\textsf{DDH}\xspace}
-\newcommand{\ElGamal}{\textsf{ElGamal}\xspace}
-\newcommand{\HElGamal}{\textsf{HElGamal}\xspace}
-\newcommand{\RSA}{\textsf{RSA}\xspace}
-\newcommand{\OAEP}{\textsf{OAEP}\xspace}
-\newcommand{\FDH}{\textsf{FDH}\xspace}
-\newcommand{\HMAC}{\textsf{HMAC}\xspace}
-\newcommand{\CS}{\textsf{CS}\xspace}
-\newcommand{\Skein}{\textsf{Skein}\xspace}
-\newcommand{\TCR}{\textsf{TCR}\xspace}
-
-\newcommand{\KG}{\mathcal{KG}}
-\newcommand{\Enc}{\mathcal{E}}
-\newcommand{\Dec}{\mathcal{D}}
-
-%% Complexity and termination
-\newcommand{\lossless}{\mathsf{lossless}}
-
-%% Sets
-\newcommand{\zeroone}{[0,1]}
-\newcommand{\bit}{\{0,1\}}
-\newcommand{\bitstring}[1]{\ensuremath{\bit^{#1}}}
-\newcommand{\bool}{\mathbb{B}}
-\newcommand{\nat}{\mathbb{N}}
-\newcommand{\real}{\mathbb{R}}
-\newcommand{\option}[1]{#1_\bot}
-
-%% Mathematics
-\newcommand{\conv}[1][]{\mathrel{\leftrightarrow^*_{#1}}}
-\renewcommand{\Pr}[2]{\mathrm{Pr}\left[#1 : #2\right]}
-\newcommand{\Prm}[3]{\mathrm{Pr}\left[#1,#3 : #2\right]}
-\newcommand{\labs}{\left\lvert}
-\newcommand{\rabs}{\right\rvert}
-\newcommand{\charfun}{\mathds{1}}
-
-%% Distribution monad
-\newcommand{\supp}{\mathsf{support}}
-\newcommand{\range}[2]{\mathsf{range}~{#1}~{#2}}
-
-%% Semantics
-\newcommand{\subst}[2]{\left[{}^{#2}/{}_{#1}\right]}
-\newcommand{\fv}{\mathsf{fv}}
-\newcommand{\modifies}{\mathsf{mod}}
-\newcommand{\glob}{\mathsf{glob}}
-\newcommand{\Env}{\mathcal{E}}
-
-%% Well-formed adversaries
-%% Program Judgements
-\newcommand{\Hoare}[3]{\left[{#1}:{#2}\Longrightarrow{#3}\right]}
-\newcommand{\Equiv}[4]{\left[{#1}\sim{#2}:{#3}\Longrightarrow{#4}\right]}
-\newcommand{\bdHoareS}[5]{{\Hoare{#1}{#2}{#3}}\,{#4}\,{#5}}
-\newcommand{\HoareLe}[4]{\bdHoareS{#1}{#2}{#3}{\leq}{#4}}
-\newcommand{\HoareEq}[4]{\bdHoareS{#1}{#2}{#3}{=}{#4}}
-\newcommand{\HoareGe}[4]{\bdHoareS{#1}{#2}{#3}{\geq}{#4}}
-
-\newcommand{\side}[1]{\langle #1 \rangle}
-\newcommand{\sidel}{\side{1}}
-\newcommand{\sider}{\side{2}}
-\newcommand{\pre}{\Psi}
-\newcommand{\post}{\Phi}
-\newcommand{\bound}{\delta}
-\newcommand{\ECinsupp}[2]{\mathec{Distr.in_supp}\,{#1}\,{#2}}
-\newcommand{\insupp}[2]{{#1}\in\mathec{supp}\,{#2}}
-
-%% Variables
-\newcommand{\var}[1]{\ensuremath{\mathit{#1}} \xspace}
-
-%% Constants and operators
-\newcommand{\true}{\mathsf{true}}
-\newcommand{\false}{\mathsf{false}}
-\newcommand{\nil}{\mathsf{nil}}
-\newcommand{\hd}{\mathsf{hd}}
-\newcommand{\tl}{\mathsf{tl}}
-\newcommand{\app}{\mathbin{+\mkern-7mu+}}
-\newcommand{\concat}{\parallel}
-\newcommand{\xor}{\oplus}
-\newcommand{\msb}[2]{[#1]^{#2}}
-\newcommand{\lsb}[2]{[#1]_{#2}}
-\newcommand{\dom}{\mathsf{dom}}
-\newcommand{\ran}{\mathsf{ran}}
-\newcommand{\fst}{\mathsf{fst}}
-\newcommand{\snd}{\mathsf{snd}}
-\newcommand{\some}[1]{#1}
-\newcommand{\none}{\bot}
-
-\newcommand{\Int}{\mathsf{Int}}
-\newcommand{\tint}{\mathsf{int}}
-
-\newcommand{\tbool}{\mathsf{bool}}
-
-%% Language
-\newcommand{\Skip}{\mathsf{skip}}
-\newcommand{\Seq}[2]{#1;\ #2}
-\newcommand{\Ass}[2]{#1 \leftarrow #2}
-\newcommand{\Rand}[2]{#1 \stackrel{\raisebox{-.25ex}[.25ex]%
-{\tiny $\mathdollar$}}{\raisebox{-.2ex}[.2ex]{$\leftarrow$}} #2}
-\newcommand{\Randi}[2]{\Rand{#1}{[0..#2]}}
-\newcommand{\Randb}[1]{\Rand{#1}{\bit}}
-\newcommand{\Randbs}[2]{\Rand{#1}{\bitstring{#2}}}
-\newcommand{\Cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}
-\newcommand{\Condt}[2]{\mathsf{if}\ #1\ \mathsf{then}\ #2}
-\newcommand{\Else}{\mathsf{else}\ }
-\newcommand{\Elsif}{\mathsf{elsif}\ }
-\newcommand{\nWhile}[3]{\mathsf{while}_{#1}\ #2\ \mathsf{do}\ #3}
-\newcommand{\While}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2}
-\newcommand{\Call}[3]{#1 \leftarrow #2\mathsf{(}#3\mathsf{)}}
-\newcommand{\Return}{\mathsf{return}}
-
-%% Language definition
-
-
-\newcounter{easycrypt}
-\lstnewenvironment{easycrypt}[2][]{
-  \renewcommand\lstlistingname{Listado de código}
-  \setcounter{lstlisting}{\value{easycrypt}}
-  \lstset{language=easycrypt,caption={#2},#1}
-}
-{\stepcounter{easycrypt}}
-
-\lstdefinelanguage{easycrypt}{
-  style=easycrypt-default,
-  keywordsprefix={'},
-  morekeywords=[1]{unit,bool,int,real,bitstring,array,list,matrix,word},
-  morekeywords=[2]{type,datatype,op,caxiom,axiom,lemma,module,pred,const,declare},
-  morekeywords=[3]{var,fun,charfun,cost},
-  morekeywords=[4]{while,if},
-  morekeywords=[5]{theory,end,clone,import,export,as,with,section},
-  morekeywords=[6]{forall,exists,lambda},
-  morekeywords=[7]{idtac,change,beta,iota,zeta,logic,delta,simplify,congr,
-    generalize,pose,split,left,right,case,intros,cut,elim,apply,rewrite,elimT,
-    subst,progress,trivial},
-  morekeywords=[8]{by,assumption,smt,reflexivity},
-  morekeywords=[9]{first,last,do,try},
-  morecomment=[n][\itshape]{(*}{*)},
-  morecomment=[n][\bfseries]{(**}{*)}
-}
-
-\lstdefinestyle{easycrypt-default}{
-  columns=fullflexible,
-  % captionpos=b,
-  frame=tb,
-  xleftmargin=.1\textwidth,
-  xrightmargin=.1\textwidth,
-  rangebeginprefix={(**\ begin\ },
-  rangeendprefix={(**\ end\ },
-  rangesuffix={\ *)},
-  includerangemarker=false,
-  basicstyle=\small\sffamily,
-  identifierstyle={},
-  keywordstyle=[1]{\itshape\color{OliveGreen}},
-  keywordstyle=[2]{\bfseries\color{Blue}},
-  keywordstyle=[3]{\bfseries},
-  keywordstyle=[4]{\bfseries},
-  keywordstyle=[5]{\bfseries\color{OliveGreen}},
-  keywordstyle=[6]{\itshape\color{Blue}},
-  keywordstyle=[7]{\color{Blue}},
-  keywordstyle=[8]{\color{Red}},
-  keywordstyle=[9]{\color{OliveGreen}},
-  literate={phi}{{$\!\phi\,$}}1
-           {phi1}{{$\!\phi_1$}}1
-           {phi2}{{$\!\phi_2$}}1
-           {phi3}{{$\!\phi_3$}}1
-           {phin}{{$\!\phi_n$}}1
-}
-
-\newcounter{bnf}
-\lstnewenvironment{bnf}[2][]{
-  \renewcommand\lstlistingname{Gramática}
-  \setcounter{lstlisting}{\value{bnf}}
-  \lstset{language=bnf,caption={#2},#1}
-}
-{\stepcounter{bnf}}
-
-\lstdefinestyle{bnf-style}{
-  frame=tb,
-  keywordstyle=[1]{\bfseries},
-  mathescape=true,
-}
-
-\lstdefinelanguage{bnf}{
-  style=bnf-style,
-  morekeywords=[1]{while,do,if,then,else,skip}
-}
-
-\newcounter{game}
-\lstnewenvironment{game}[2][]{
-  \renewcommand\lstlistingname{Juego}
-  \setcounter{lstlisting}{\value{game}}
-  \lstset{language=game,caption={#2},#1}
-}
-{\stepcounter{game}}
-
-\lstdefinestyle{game-style}{
-  frame=tb,
-  keywordstyle=[1]{\bfseries},
-  mathescape=true,
-}
-
-\lstdefinelanguage{game}{
-  style=game-style,
-}
-
-\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline
-[language=easycrypt,#1]{#2}}
-
-%% Typesetting
-\newcommand{\titledbox}[4]{{\color{#1}\fbox{\begin{minipage}{#2}{\textbf{#3:} \color{black}#4}\end{minipage}}}}
-\newcommand{\warningbox}[1]{\titledbox{red}{.9\textwidth}{Warning}{#1}}
-\newcommand{\futurebox}[1]{\titledbox{blue}{.9\textwidth}{Future}{#1}}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "memoria"
-%%% End:
\ No newline at end of file
-- 
cgit v1.2.3

