more writting, more figures

readings/2_Implementation.tex

 \section{Curve25519 implementation}
 
-To \texttt{crypto\_scalarmult} we need to prove all the functions it calls:
+In order to prove the correctness of \texttt{crypto\_scalarmult},
+ we also need to do the same with all the functions subsequently called:
 \texttt{unpack25519}; \texttt{A}; \texttt{Z}; \texttt{M}; \texttt{S};
 \texttt{car25519}; \texttt{inv25519}; \texttt{set25519}; \texttt{sel25519};
 \texttt{pack25519}.
@@ -10,14 +11,14 @@ To \texttt{crypto\_scalarmult} we need to prove all the functions it calls:
 Curve25519 is defined over $\mathbb{Z}_{2^{255}-19}$. Number in that field can
 be represented by a 256-bits number. Each of them are cut into 16 limbs of 16
 bits placed into 64-bits signed container.
-\begin{lstlisting}[language=C]
+\begin{lstlisting}[language=Ctweetnacl]
 typedef long long i64;
 typedef i64 gf[16];
 \end{lstlisting}
 
 This representation allows simple definitions of addition (\texttt{A}),
 substraction (\texttt{Z}) and a (school-book) multiplication (\texttt{M}).
-\begin{lstlisting}[language=C]
+\begin{lstlisting}[language=Ctweetnacl]
 sv A(gf o,const gf a,const gf b) {
   int i;
   FOR(i,16) o[i]=a[i]+b[i];
@@ -35,11 +36,11 @@ sv M(gf o,const gf a,const gf b) {
 \end{lstlisting}
 
 The propagation of carries are taken care of a by the \texttt{car25519} function.
-\begin{lstlisting}[language=C]
+\begin{lstlisting}[language=Ctweetnacl]
 sv car25519(gf o) {
   int i;
   i64 c;
-  FOR(i,16) {
+  FOR(i,15) {
     o[i]+=(1LL<<16);
     c=o[i]>>16;
     o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
@@ -48,18 +49,67 @@ sv car25519(gf o) {
 }
 \end{lstlisting}
 
-It should be noted that this representation does not guaranties uniqueness. i.e.
-\begin{align*}
-  \exists x,y \in \texttt{gf} \text{ such that }\\
-  x \neq y\ \land \\
-  x \bmod{2^{255}-19} = y \bmod{2^{255}-19}
-\end{align*}
+The full Mongomery ladder is defined as follow:
+\begin{lstlisting}[language=Ctweetnacl]
+int crypto_scalarmult(u8 *q,
+                      const u8 *n,
+                      const u8 *p)
+{
+  u8 z[32];
+  i64 r;
+  int i;
+  gf x,a,b,c,d,e,f;
+  FOR(i,31) z[i]=n[i];
+  z[31]=(n[31]&127)|64;
+  z[0]&=248;
+  unpack25519(x,p);
+  FOR(i,16) {
+    b[i]=x[i];
+    d[i]=a[i]=c[i]=0;
+  }
+  a[0]=d[0]=1;
+  for(i=254;i>=0;--i) {
+    r=(z[i>>3]>>(i&7))&1;
+    sel25519(a,b,r);
+    sel25519(c,d,r);
+    A(e,a,c);
+    Z(a,a,c);
+    A(c,b,d);
+    Z(b,b,d);
+    S(d,e);
+    S(f,a);
+    M(a,c,a);
+    M(c,b,e);
+    A(e,a,c);
+    Z(a,a,c);
+    S(b,a);
+    Z(c,d,f);
+    M(a,c,_121665);
+    A(a,a,d);
+    M(c,c,a);
+    M(a,d,f);
+    M(d,b,x);
+    S(b,e);
+    sel25519(a,b,r);
+    sel25519(c,d,r);
+  }
+  inv25519(c,c);
+  M(a,a,c);
+  pack25519(q,a);
+  return 0;
+}
+\end{lstlisting}
+
+It should be noted that this representation does not guaranties uniqueness. i.e.\\
+$\exists x,y \in \texttt{gf} \text{ such that }$
+\vspace{-0.25cm}
+  $$x \neq y\ \ \land\ \ x \equiv y \pmod{2^{255}-19}$$
 
 \subsection{What need to be proven?}
 
 \textbf{Soundness} and \textbf{Correctness}.
 
-We show that TweetNaCl's code is \textbf{sound} also know as \textit{shape analysis} \ie
+We show that TweetNaCl's code is \textbf{sound} \ie
 
 \begin{itemize}
 \item absence of array out-of-bounds,
@@ -71,8 +121,8 @@ We show that TweetNaCl's code is \textbf{sound} also know as \textit{shape analy
 We also show that TweetNaCl's code is \textbf{correct}:
 
 \begin{itemize}
-\item Curve25519 is correctly implemented
-\item The number representation
+\item Curve25519 is correctly implemented (steps)
+\item Operations on \texttt{gf} are equivalent to operations in $\mathbb{Z}_{2^{255}-19}$
 \end{itemize}
 
 \subsection{Correctness Theorem}
@@ -81,45 +131,39 @@ The soundness is implied by the functionnal definition of the following theorem.
 Indeed, showing equivalence between the Clight representation and a Coq
 definition of the ladder garantees us the soundness.
 
-\begin{lstlisting}
+\begin{lstlisting}[language=CoqVST]
 Definition crypto_scalarmult_spec :=
- DECLARE _crypto_scalarmult_curve25519_tweet
- WITH
-  q: val, n: val, p: val, c121665:val,
+DECLARE _crypto_scalarmult_curve25519_tweet
+WITH
+  v_q: val, v_n: val, v_p: val, c121665:val,
   sh : share,
-  qq : list Z,
-  nn : list Z,
-  pp : list Z
-
- (* Preconditions *)
- PRE [ _q OF (tptr tuchar),
-       _n OF (tptr tuchar),
-       _p OF (tptr tuchar) ]
-  PROP  (writable_share sh;
-    Forall (fun x => 0 <= x < Z.pow 2 8) pp;
-    Forall (fun x => 0 <= x < Z.pow 2 8) nn;
-    Zlength qq = 32;
-    Zlength nn = 32;
-    Zlength pp = 32)
-  LOCAL(temp _q q; temp _n n; temp _p p;
-        gvar __121665 c121665)
- SEP  (sh [{ q }] <<(uch32)-- mVI qq;
-    sh [{ n }] <<(uch32)-- mVI nn;
-    sh [{ p }] <<(uch32)-- mVI pp;
-    Ews [{ c121665 }] <<(uch32)-- mVI64 c_121665)
-
- (* Resulting Postconditions *)
- POST [ tint ]
-  PROP (
-    Forall (fun x => 0 <= x < Z.pow 2 8)
-      (sc_mult nn pp);
-      (* WE CAN ADD MORE LEMMAS HERE *)
-    Zlength (sc_mult nn pp) = 32)
-  LOCAL()
-  SEP (sh [{ q }] <<(uch32)-- mVI (sc_mult nn pp);
-    sh [{ n }] <<(uch32)-- mVI nn;
-    sh [{ p }] <<(uch32)-- mVI pp;
-    Ews [{ c121665 }] <<(uch32)-- mVI64 c_121665).
+  q : list val, n : list Z, p : list Z
+(*------------------------------------------*)
+PRE [ _q OF (tptr tuchar),
+     _n OF (tptr tuchar),
+     _p OF (tptr tuchar) ]
+PROP (writable_share sh;
+      Forall (fun x => 0 <= x < 2^8) p;
+      Forall (fun x => 0 <= x < 2^8) n;
+      Zlength q = 32; Zlength n = 32;
+      Zlength p = 32)
+LOCAL(temp _q v_q; temp _n v_n; temp _p v_p;
+      gvar __121665 c121665)
+SEP  (sh [{ v_q }] <<(uch32)-- q;
+      sh [{ v_n }] <<(uch32)-- mVI n;
+      sh [{ v_p }] <<(uch32)-- mVI p;
+      Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665)
+(*------------------------------------------*)
+POST [ tint ]
+PROP (Forall (fun x => 0 <= x < 2^8)
+                  (Crypto_Scalarmult n p);
+      Zlength (Crypto_Scalarmult n p) = 32)
+LOCAL(temp ret_temp (Vint Int.zero))
+SEP  (sh [{ v_q }] <<(uch32)-- mVI
+                  (Crypto_Scalarmult n p);
+      sh [{ v_n }] <<(uch32)-- mVI n;
+      sh [{ v_p }] <<(uch32)-- mVI p;
+      Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665
 \end{lstlisting}
 
 In this theorem we declare that the function \texttt{crypto\_scalarmult} takes as
@@ -130,12 +174,13 @@ represented by a list of integers in Coq. In order to guarantee the equivalence
 we assume the values in \texttt{pp} and \texttt{nn} being bounded by $0$ included
 and $2^8$ excluded.
 
-This function computes: $$Q \leftarrow n \times P$$
+This function computes: $$Q.x \leftarrow n \times P.x$$
 
 \texttt{pp} represent the x-coordinate of $P$, \texttt{nn} represent the
 scalar by which it is be multiplied $n$ (where the bits 1, 2, 5 248, 249, 250
 are cleared and bit 6 is set).
 
-As a result of the excution of \texttt{crypto\_scalarmult}, the value \texttt{0} is returned,
-\texttt{p} and \texttt{n} points to the same locations containing the same values \texttt{pp} and \texttt{nn}.
+As a result of the excution of \texttt{crypto\_scalarmult}, the value \texttt{0}
+is returned, \texttt{p} and \texttt{n} points to the same locations containing
+the same values \texttt{pp} and \texttt{nn}.
 The pointer \texttt{q} points to the same location, but contain the x coordinate of $Q$.

readings/6_UsingVST.tex

@@ -34,13 +34,21 @@ e.g. prove \texttt{M(o,a,b)} later notice that you can have aliasing, need to re
 your theorem to prove \texttt{M(o,a,a)} (\textit{squaring}) and other variants such as:
 \texttt{M(a,a,b)} and \texttt{M(b,a,b)}.
 
-\textbf{PICTURE with memory and arrow and SAME share}
+\begin{figure}[h]
+  \include{tikz/memory_same_sh}
+  \caption{Aliasing and Separation Logic (1)}
+  \label{tk:MemSame}
+\end{figure}
 
 Prove \texttt{M(o,a,b)} where o is a \texttt{list $\Z$} and then realize that
 \texttt{o} can be a list of \textit{undefined} (\texttt{list val}). Thus needs
 to reprove the above theorem again.
 
-\textbf{PICTURE with memory and arrow and DIFFERENT SHARE}
+\begin{figure}[h]
+  \include{tikz/memory_diff_sh}
+  \caption{Memory Share and Separation Logic}
+  \label{tk:MemSame}
+\end{figure}
 
 \subsection{How to be efficient with VST?}
 
@@ -83,17 +91,19 @@ It is to be noted that the \texttt{clightgen} tool has not been formally verifie
 
 \texttt{clightgen -normalize}
 
-Assuming that \texttt{b} is of type \texttt{long long}, the following expression
-will not be type-checked by VST.
-
-\texttt{b = 1 - b;}
-
-\texttt{1} is interpreted by cligthgen as \texttt{Vint} (\textit{Value of int})
-while \texttt{b} is interpreted as \texttt{Vlong} (\textit{Value of long}),
-resulting in an error. To solve this, we need to prefix \texttt{1} by an
-explicit cast in C into the correct type. As a result, any constants used in this
-implementation had to be casted to the correct type
-(in \textit{TweetNaclVerificable}) to pass typecheck.
+% Not true since VST 2.0
+%
+% Assuming that \texttt{b} is of type \texttt{long long}, the following expression
+% will not be type-checked by VST.
+%
+% \texttt{b = 1 - b;}
+%
+% \texttt{1} is interpreted by cligthgen as \texttt{Vint} (\textit{Value of int})
+% while \texttt{b} is interpreted as \texttt{Vlong} (\textit{Value of long}),
+% resulting in an error. To solve this, we need to prefix \texttt{1} by an
+% explicit cast in C into the correct type. As a result, any constants used in this
+% implementation had to be casted to the correct type
+% (in \textit{TweetNaclVerificable}) to pass typecheck.
 
 \subsection{Verifiying for loops: head and tail recursion}
 

readings/Makefile

-FILES := $(wildcard *.tex) $(wildcard *.sty)
+FILES := $(wildcard *.tex) $(wildcard tikz/*.tex) $(wildcard *.sty)
 
 curve25519.pdf: $(FILES) collection.bib
 	latexmk -pdf curve25519.tex
 
+depend:
+		@echo $(FILES)
+
 .PHONY: clean
 
 clean:

readings/setup.sty

@@ -79,26 +79,28 @@ width=0.8\columnwidth
 \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@lstdirective}{HTML}{881000}    % dark red
 \definecolor{doc@lstconstants}{HTML}{0033AA}    % dark blue
 \definecolor{doc@lstidentifiers2}{HTML}{FF0033} % purple-red
 \definecolor{doc@lstnumbers}{HTML}{AA00AA}      % purple
 
-\definecolor{doc@lstbackground}{HTML}{FFFFFF}   % white
+\definecolor{doc@lstbackground}{HTML}{FFF8DC}   % white
 \definecolor{doc@lstframe}{HTML}{FFFFFF}        % white
 
 \lstloadlanguages{% check documentation for other languages...
   C
 }
+\def\-{\raisebox{.75pt}{-}}
 
-\lstdefinelanguage{cgimli}{%
-  morekeywords=[1]{for, if, return, extern, while},
-  morekeywords=[2]{void, int, uint32_t, uint64_t, uint8_t, void},
-  morekeywords=[3]{const, typedef},
-  morekeywords=[4]{gimli, Gimli_hash, memset, memcpy, MIN, rotate},
-  morekeywords=[5]{ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 24, 26, 32, 0x80, 0x1F, 0x9e377900},
+\lstdefinelanguage{CoqVST}{%
+  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=[5]{ 0, 2^8, 16, 32},
   sensitive=true,
-  alsoletter   = {0,1,2,3,4,5,6,7,8,9} ,
+  alsoletter   = {0123456789^} ,
    % morekeywords = [1]{1,2,3,40} ,
   % otherkeywords={<, >, \\=, |, &, ^},
   %
@@ -112,30 +114,71 @@ width=0.8\columnwidth
   keywordstyle=\color{doc@lstkeyword},
   keywordstyle=[1]\color{doc@lstidentifiers2},
   keywordstyle=[2]\color{doc@lstconstants},
+  keywordstyle=[3]\color{doc@lstkeyword2},
   % keywordstyle=[3]\color[rgb]{0.127,0.427,0.514},
   keywordstyle=[4]\color{doc@lstfunctions},
   keywordstyle=[5]\color{doc@lstnumbers},
   % alsoletter={?},
   % keywordsprefix=?,
-  delim=[l][\color{doc@lstdirective}]{\#},
+  % delim=[l][\color{doc@lstdirective}]{\#},
+  delim=[s][\color{doc@lstdirective}]{(*}{*)},
   % moredelim=[s][\color{magenta}]{<}{>},
   % moredelim=[s][\color{magenta}]{:}{,},
   % moredelim=[s][\color{magenta}]{:}{^^J},
   % moredelim=[s][\color{magenta}]{:}{\ },
   % moredelim=[l][\color{black}]{:}{/},
+  literate=
+%     % {\\forall}{{\color{doc@lstcomment}{$\forall\;$}}}1
+%     {.}{{\color{white}{.}}}1
+%     {<-}{{$\leftarrow\;$}}1
+      {=>}{{$\mapsto$}}1
+%     {==}{{\ttfamily{==}\;}}1
+%     {==>}{{\ttfamily{==>}\;}}1
+% %    {:>}{{\code{:>}\;}}1
+%     {->}{{$\rightarrow$}}1
+%     {<->}{{$\leftrightarrow$}}1
+%     {<>}{{$\neq\;$}}1
+% %    { nil }{{ [ ]}}1
+      {<}{{$\!<\!$}}1
+      {<=}{{$\!\leq\!$}}1
+%     {<<}{{$\ll\;$}}1
+%     {<<<}{{$\lll\;$}}1
+%     {>=}{{$\geq\;$}}1
+%     {\\o}{{$\circ\;$}}1
+%     {\@}{{$\cdot$}}1
+%     {/\\}{{$\wedge$}}1
+%     {\\/}{{$\vee$}}1
+%     {++}{{\ttfamily{++}}}1
+%     {~}{{$\sim$}}1
+%     {\@\@}{{$@$}}1
+%     {\\mapsto}{{$\mapsto\;$}}1
+%     {\\oplus}{{$\oplus$}}1
+%     {\\boxplus}{{$\boxplus$}}1
+%     {\\hline}{{\rule{\linewidth}{0.5pt}}}1
+      {[\{}{\!\!\![\!\!\{\!\!}1
+      {\}]}{\!\!\}\!\!]\!\!\!}1
+      {<<(}{<\!\!\-\!\-\!\!(}1
+      {)--}{)\!\!\-\!\-\!\!}1
+      {fun}{{\color{doc@lstkeyword2}{$\lambda\!\!$}}}1
+      % {\_}{\!\_\!}1
+      {2^8}{{\color{doc@lstnumbers}{$2^8$}}}1
 }
 
-\lstdefinelanguage{HASM}{%
-  morekeywords=[1]{u, v},
-  morekeywords=[2]{ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 24, 26, 32},
+\lstdefinelanguage{Ctweetnacl}{%
+  morekeywords=[1]{FOR,for, return},
+  morekeywords=[2]{sv, int, i64, gf, long, u8},
+  morekeywords=[3]{const, typedef},
+  morekeywords=[4]{A, Z, M, S, car25519, pack25519, inv25519,
+  crypto_scalarmult, unpack25519, sel25519},
+  morekeywords=[5]{ 0, 1, 1LL, 3, 7, 15, 16, 31, 32, 37, 38, 127, 64, 248, 254,_121665 },
   sensitive=true,
-  alsoletter   = {0,1,2,3,4,5,6,7,8,9} ,
+  alsoletter   = {0123456789^} ,
    % morekeywords = [1]{1,2,3,40} ,
   % otherkeywords={<, >, \\=, |, &, ^},
   %
   morestring=[b]",
   %
-  morecomment=[l]{\#},
+  morecomment=[l]{//},
   %
   identifierstyle=\color[rgb]{0,0,0},
   commentstyle=\color{doc@lstcomment}\itshape,
@@ -144,8 +187,8 @@ width=0.8\columnwidth
   keywordstyle=[1]\color{doc@lstidentifiers2},
   keywordstyle=[2]\color{doc@lstconstants},
   % keywordstyle=[3]\color[rgb]{0.127,0.427,0.514},
-  % keywordstyle=[4]\color{doc@lstfunctions},
-  % keywordstyle=[5]\color{doc@lstnumbers},
+  keywordstyle=[4]\color{doc@lstfunctions},
+  keywordstyle=[5]\color{doc@lstnumbers},
   % alsoletter={?},
   % keywordsprefix=?,
   delim=[l][\color{doc@lstdirective}]{\#},
@@ -155,39 +198,40 @@ width=0.8\columnwidth
   % moredelim=[s][\color{magenta}]{:}{\ },
   % moredelim=[l][\color{black}]{:}{/},
   literate=
-    % {\\forall}{{\color{doc@lstcomment}{$\forall\;$}}}1
-    {.}{{\color{white}{.}}}1
-    {<-}{{$\leftarrow\;$}}1
-    {=>}{{$\Rightarrow\;$}}1
-    {==}{{\ttfamily{==}\;}}1
-    {==>}{{\ttfamily{==>}\;}}1
-%    {:>}{{\code{:>}\;}}1
-    {->}{{$\rightarrow$}}1
-    {<->}{{$\leftrightarrow$}}1
-    {<>}{{$\neq\;$}}1
-%    { nil }{{ [ ]}}1
-    {<=}{{$\leq\;$}}1
-    {<<}{{$\ll\;$}}1
-    {<<<}{{$\lll\;$}}1
-    {>=}{{$\geq\;$}}1
-    {\\o}{{$\circ\;$}}1
-    {\@}{{$\cdot$}}1
-    {/\\}{{$\wedge$}}1
-    {\\/}{{$\vee$}}1
-    {++}{{\ttfamily{++}}}1
-    {~}{{$\sim$}}1
-    {\@\@}{{$@$}}1
-    {\\mapsto}{{$\mapsto\;$}}1
-    {\\oplus}{{$\oplus$}}1
-    {\\boxplus}{{$\boxplus$}}1
-    {\\hline}{{\rule{\linewidth}{0.5pt}}}1
+%     % {\\forall}{{\color{doc@lstcomment}{$\forall\;$}}}1
+%     {.}{{\color{white}{.}}}1
+%     {<-}{{$\leftarrow\;$}}1
+%     {=>}{{$\Rightarrow\;$}}1
+%     {==}{{\ttfamily{==}\;}}1
+%     {==>}{{\ttfamily{==>}\;}}1
+% %    {:>}{{\code{:>}\;}}1
+%     {->}{{$\rightarrow$}}1
+%     {<->}{{$\leftrightarrow$}}1
+%     {<>}{{$\neq\;$}}1
+% %    { nil }{{ [ ]}}1
+%     {<=}{{$\leq\;$}}1
+%     {<<}{{$\ll\;$}}1
+%     {<<<}{{$\lll\;$}}1
+%     {>=}{{$\geq\;$}}1
+%     {\\o}{{$\circ\;$}}1
+%     {\@}{{$\cdot$}}1
+%     {/\\}{{$\wedge$}}1
+%     {\\/}{{$\vee$}}1
+%     {++}{{\ttfamily{++}}}1
+%     {~}{{$\sim$}}1
+%     {\@\@}{{$@$}}1
+%     {\\mapsto}{{$\mapsto\;$}}1
+%     {\\oplus}{{$\oplus$}}1
+%     {\\boxplus}{{$\boxplus$}}1
+%     {\\hline}{{\rule{\linewidth}{0.5pt}}}1
 }
 
 \lstset{%
   lineskip=-0.1em,
   %
-%  basicstyle=\ttfamily\scriptsize, % font that is used for the code
-  basicstyle=\ttfamily\small, % font that is used for the code
+  % basicstyle=\ttfamily\scriptsize, % font that is used for the code
+  % basicstyle=\ttfamily\small, % font that is used for the code
+  basicstyle=\ttfamily\footnotesize, % font that is used for the code
   identifierstyle=\color{doc@lstidentifier},
   commentstyle=\color{doc@lstcomment}\itshape,
   stringstyle=\color{doc@lststring},

readings/tikz/memory_diff_sh.tex

+\begin{tikzpicture}
+\def\-{\raisebox{.75pt}{-}}
+
+\draw (0,0) rectangle (3,0.3);
+\draw[thick] (1,0) -- (1,0.3);
+\draw[thick] (2,0) -- (2,0.3);
+\node [anchor=east] (shn) at (0,0.15) {sh};
+\node [anchor=north] (Moab) at (1.5,-0.5) {\texttt{M(o,a,b)}};
+\draw[thick, -> ] (1.25, -0.6) -- (1.25, -0.5) -- (0.5,-0.1);
+\draw[thick, -> ] (1.6, -0.6) -- (1.6, -0.5) -- (1.5,-0.1);
+\draw[thick, -> ] (1.95, -0.6) -- (1.95, -0.5) -- (2.5,-0.1);
+
+\node [anchor=north west, text width=6cm, align=left] (Sepoab) at (-0.5,-1.8)
+  {\footnotesize{$\mathtt{sh [\!\!\{ v\_o \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ o}$\\
+  $\mathtt{sh [\!\!\{ v\_a \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ a}$\\
+  $\mathtt{sh [\!\!\{ v\_b \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ b}$}};
+
+
+\begin{scope}[yshift=0 cm,xshift=4 cm]
+  \draw (0,0) rectangle (2,0.3);
+  \draw[thick] (1,0) -- (1,0.3);
+  \node [anchor=east] (shm) at (0,0.15) {sh\;};
+
+  \draw (0,0.5) rectangle (1,0.8);
+  \node [anchor=east] (shm) at (0,0.65) {Ews};
+
+  \draw[thick] (2,0) -- (2,0.3);
+  \node [anchor=north west] (Mcaa) at (0.15,-0.5) {\texttt{M(a,c,\_121665)}};
+  \draw[thick, -> ] (0.75, -0.6) -- (0.75, -0.5) -- (0.4,-0.1);
+  \draw[thick, -> ] (1.1, -0.6) -- (1.1, -0.5) -- (0.6,-0.1);
+  \draw[thick, -> ] (2.0, -0.6) -- (2.45, -0.2) -- (2.45, 0.3) -- (2.2, 0.65) -- (1.5,0.65);
+
+  \node [anchor=north west, text width=6cm, align=left] (Sepoab) at (-0.5,-1.8)
+    {\footnotesize{$\mathtt{sh [\!\!\{ v\_a \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ a}$\\
+    $\mathtt{sh [\!\!\{ v\_c \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ c}$\\
+    $\mathtt{Ews} \mathtt{[\!\!\{ \_\_121665 \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ \_121665}$}};
+
+\end{scope}
+
+\draw[dashed] (-0.5,-1.2) -- +(7.5,0);
+\node [anchor=north west] (sep) at (-0.5,-1.2) {In Separation Logic:};
+
+\end{tikzpicture}

readings/tikz/memory_same_sh.tex

+\begin{tikzpicture}
+\def\-{\raisebox{.75pt}{-}}
+
+\draw (0,0) rectangle (3,0.3);
+\draw[thick] (1,0) -- (1,0.3);
+\draw[thick] (2,0) -- (2,0.3);
+\node [anchor=east] (shn) at (0,0.15) {sh};
+\node [anchor=north] (Moab) at (1.5,-0.5) {\texttt{M(o,a,b)}};
+\draw[thick, -> ] (1.25, -0.6) -- (1.25, -0.5) -- (0.5,-0.1);
+\draw[thick, -> ] (1.6, -0.6) -- (1.6, -0.5) -- (1.5,-0.1);
+\draw[thick, -> ] (1.95, -0.6) -- (1.95, -0.5) -- (2.5,-0.1);
+
+\node [anchor=north west, text width=6cm, align=left] (Sepoab) at (-0.5,-1.8)
+  {\footnotesize{$\mathtt{sh [\!\!\{ v\_o \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ o}$\\
+  $\mathtt{sh [\!\!\{ v\_a \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ a}$\\
+  $\mathtt{sh [\!\!\{ v\_b \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ b}$}};
+
+
+\begin{scope}[yshift=0 cm,xshift=4 cm]
+  \draw (0,0) rectangle (2,0.3);
+  \draw[thick] (1,0) -- (1,0.3);
+  % \draw[thick] (2,0) -- (2,0.3);
+  \node [anchor=east] (shm) at (0,0.15) {sh};
+  \node [anchor=north] (Mcaa) at (1,-0.5) {\texttt{M(c,c,a)}};
+  \draw[thick, -> ] (0.75, -0.6) -- (0.75, -0.5) -- (0.4,-0.1);
+  \draw[thick, -> ] (1.1, -0.6) -- (1.1, -0.5) -- (0.6,-0.1);
+  \draw[thick, -> ] (1.45, -0.6) -- (1.45, -0.5) -- (1.5,-0.1);
+
+  \node [anchor=north west, text width=6cm, align=left] (Sepoab) at (-0.5,-1.8)
+    {\footnotesize{$\mathtt{sh [\!\!\{ v\_c \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ c}$\\
+    $\mathtt{sh [\!\!\{ v\_a \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ a}$}};
+
+\end{scope}
+
+\draw[dashed] (-0.5,-1.2) -- +(7.5,0);
+\node [anchor=north west] (sep) at (-0.5,-1.2) {In Separation Logic:};
+
+\end{tikzpicture}