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

Fix alignment complaints from Peter

parent 93a90727
...@@ -13,14 +13,14 @@ Definition RFC (n: list Z) (p: list Z) : list Z := ...@@ -13,14 +13,14 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
let k := decodeScalar25519 n in let k := decodeScalar25519 n in
let u := decodeUCoordinate p in let u := decodeUCoordinate p in
let t := montgomery_rec let t := montgomery_rec
255 (* iterate 255 times *) 255 (* iterate 255 times *)
k (* clamped n *) k (* clamped n *)
1 (* x_2 *) 1 (* x_2 *)
u (* x_3 *) u (* x_3 *)
0 (* z_2 *) 0 (* z_2 *)
1 (* z_3 *) 1 (* z_3 *)
0 (* dummy *) 0 (* dummy *)
0 (* dummy *) 0 (* dummy *)
u (* x_1 *) in u (* x_1 *) in
let a := get_a t in let a := get_a t in
let c := get_c t in let c := get_c t in
...@@ -38,43 +38,43 @@ Fixpoint montgomery_rec (m : nat) (z : T') ...@@ -38,43 +38,43 @@ Fixpoint montgomery_rec (m : nat) (z : T')
(* b: x3 *) (* b: x3 *)
(* c: z2 *) (* c: z2 *)
(* d: z3 *) (* d: z3 *)
(* e: temporary var *) (* e: temporary var *)
(* f: temporary var *) (* f: temporary var *)
(* x: x1 *) (* x: x1 *)
(T * T * T * T * T * T) := (T * T * T * T * T * T) :=
match m with match m with
| 0%nat => (a,b,c,d,e,f) | 0%nat => (a,b,c,d,e,f)
| S n => | S n =>
let r := Getbit (Z.of_nat n) z in let r := Getbit (Z.of_nat n) z in
(* k_t = (k >> t) & 1 *) (* k_t = (k >> t) & 1 *)
(* swap <- k_t *) (* swap <- k_t *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *) (* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *) (* (z_2, z_3) = cswap(swap, z_2, z_3) *)
let e := a + c in (* A = x_2 + z_2 *) let e := a + c in (* A = x_2+ z_2 *)
let a := a - c in (* B = x_2 - z_2 *) let a := a - c in (* B = x_2- z_2 *)
let c := b + d in (* C = x_3 + z_3 *) let c := b + d in (* C = x_3+ z_3 *)
let b := b - d in (* D = x_3 - z_3 *) let b := b - d in (* D = x_3- z_3 *)
let d := e ^2 in (* AA = A^2 *) let d := e^2 in (* AA = A^2 *)
let f := a ^2 in (* BB = B^2 *) let f := a^2 in (* BB = B^2 *)
let a := c * a in (* CB = C * B *) let a := c * a in (* CB = C * B *)
let c := b * e in (* DA = D * A *) let c := b * e in (* DA = D * A *)
let e := a + c in (* x_3 = (DA + CB)^2 *) let e := a + c in (* x_3= (DA + CB)^2 *)
let a := a - c in (* z_3 = x_1 * (DA - CB)^2 *) let a := a - c in (* z_3= x_1* (DA - CB)^2 *)
let b := a ^2 in (* z_3 = x_1 * (DA - CB)^2 *) let b := a^2 in (* z_3= x_1* (DA - CB)^2 *)
let c := d - f in (* E = AA - BB *) let c := d - f in (* E = AA - BB *)
let a := c * C_121665 in let a := c * C_121665 in
(* z_2 = E * (AA + a24 * E) *) (* z_2 = E * (AA + a24 * E) *)
let a := a + d in (* z_2 = E * (AA + a24 * E) *) let a := a + d in (* z_2 = E * (AA + a24 * E) *)
let c := c * a in (* z_2 = E * (AA + a24 * E) *) let c := c * a in (* z_2 = E * (AA + a24 * E) *)
let a := d * f in (* x_2 = AA * BB *) let a := d * f in (* x_2 = AA * BB *)
let d := b * x in (* z_3 = x_1 * (DA - CB)^2 *) let d := b * x in (* z_3 = x_1* (DA - CB)^2 *)
let b := e ^2 in (* x_3 = (DA + CB)^2 *) let b := e ^2 in (* x_3 = (DA + CB)^2 *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *) (* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *) (* (z_2, z_3) = cswap(swap, z_2, z_3) *)
montgomery_rec n z a b c d e f x montgomery_rec n z a b c d e f x
end. end.
\end{lstlisting} \end{lstlisting}
......
...@@ -17,8 +17,8 @@ Class Ops (T T': Type) (Mod: T -> T):= ...@@ -17,8 +17,8 @@ Class Ops (T T': Type) (Mod: T -> T):=
C_0 : T; (* Constant 0 *) C_0 : T; (* Constant 0 *)
C_1 : T; (* Constant 1 *) C_1 : T; (* Constant 1 *)
C_121665: T; (* const (a-2)/4 *) C_121665: T; (* const (a-2)/4 *)
Sel25519: Z -> T -> T -> T; (* CSWAP *) Sel25519: Z -> T -> T -> T; (* CSWAP *)
Getbit: Z -> T' -> Z; (* ith bit *) Getbit: Z -> T' -> Z; (* ith bit *)
}. }.
Local Notation "X + Y" := (A X Y) (only parsing). Local Notation "X + Y" := (A X Y) (only parsing).
...@@ -27,49 +27,49 @@ Local Notation "X * Y" := (M X Y) (only parsing). ...@@ -27,49 +27,49 @@ Local Notation "X * Y" := (M X Y) (only parsing).
Local Notation "X ^2" := (Sq X) (at level 40, Local Notation "X ^2" := (Sq X) (at level 40,
only parsing, left associativity). only parsing, left associativity).
Fixpoint montgomery_rec (m: nat) (z: T') Fixpoint montgomery_rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) : (a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2 *) (* a: x2 *)
(* b: x3 *) (* b: x3 *)
(* c: z2 *) (* c: z2 *)
(* d: z3 *) (* d: z3 *)
(* e: temporary var *) (* e: temporary var *)
(* f: temporary var *) (* f: temporary var *)
(* x: x1 *) (* x: x1 *)
(T * T * T * T * T * T) := (T * T * T * T * T * T) :=
match m with match m with
| 0%nat => (a,b,c,d,e,f) | 0%nat => (a,b,c,d,e,f)
| S n => | S n =>
let r := Getbit (Z.of_nat n) z in let r := Getbit (Z.of_nat n) z in
(* k_t = (k >> t) & 1 *) (* k_t = (k >> t) & 1 *)
(* swap <- k_t *) (* swap <- k_t *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *) (* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *) (* (z_2, z_3) = cswap(swap, z_2, z_3) *)
let e := a + c in (* A = x_2 + z_2 *) let e := a + c in (* A = x_2+ z_2 *)
let a := a - c in (* B = x_2 - z_2 *) let a := a - c in (* B = x_2- z_2 *)
let c := b + d in (* C = x_3 + z_3 *) let c := b + d in (* C = x_3+ z_3 *)
let b := b - d in (* D = x_3 - z_3 *) let b := b - d in (* D = x_3- z_3 *)
let d := e ^2 in (* AA = A^2 *) let d := e^2 in (* AA = A^2 *)
let f := a ^2 in (* BB = B^2 *) let f := a^2 in (* BB = B^2 *)
let a := c * a in (* CB = C * B *) let a := c * a in (* CB = C * B *)
let c := b * e in (* DA = D * A *) let c := b * e in (* DA = D * A *)
let e := a + c in (* x_3 = (DA + CB)^2 *) let e := a + c in (* x_3= (DA + CB)^2 *)
let a := a - c in (* z_3 = x_1 * (DA - CB)^2 *) let a := a - c in (* z_3= x_1* (DA - CB)^2 *)
let b := a ^2 in (* z_3 = x_1 * (DA - CB)^2 *) let b := a^2 in (* z_3= x_1* (DA - CB)^2 *)
let c := d - f in (* E = AA - BB *) let c := d - f in (* E = AA - BB *)
let a := c * C_121665 in let a := c * C_121665 in
(* z_2 = E * (AA + a24 * E) *) (* z_2 = E * (AA + a24 * E) *)
let a := a + d in (* z_2 = E * (AA + a24 * E) *) let a := a + d in (* z_2 = E * (AA + a24 * E) *)
let c := c * a in (* z_2 = E * (AA + a24 * E) *) let c := c * a in (* z_2 = E * (AA + a24 * E) *)
let a := d * f in (* x_2 = AA * BB *) let a := d * f in (* x_2 = AA * BB *)
let d := b * x in (* z_3 = x_1 * (DA - CB)^2 *) let d := b * x in (* z_3 = x_1* (DA - CB)^2 *)
let b := e ^2 in (* x_3 = (DA + CB)^2 *) let b := e ^2 in (* x_3 = (DA + CB)^2 *)
let (a, b) := (Sel25519 r a b, Sel25519 r b a) in let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
(* (x_2, x_3) = cswap(swap, x_2, x_3) *) (* (x_2, x_3) = cswap(swap, x_2, x_3) *)
let (c, d) := (Sel25519 r c d, Sel25519 r d c) in let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
(* (z_2, z_3) = cswap(swap, z_2, z_3) *) (* (z_2, z_3) = cswap(swap, z_2, z_3) *)
montgomery_rec n z a b c d e f x montgomery_rec n z a b c d e f x
end. end.
...@@ -155,7 +155,7 @@ Proof. ...@@ -155,7 +155,7 @@ Proof.
apply Mid.A. (* instantiate + *) apply Mid.A. (* instantiate + *)
apply Mid.M. (* instantiate * *) apply Mid.M. (* instantiate * *)
apply Mid.Zub. (* instantiate - *) apply Mid.Zub. (* instantiate - *)
apply Mid.Sq. (* instantiate x^2 *) apply Mid.Sq. (* instantiate x^2 *)
apply Mid.C_0. (* instantiate Const 0 *) apply Mid.C_0. (* instantiate Const 0 *)
apply Mid.C_1. (* instantiate Const 1 *) apply Mid.C_1. (* instantiate Const 1 *)
apply Mid.C_121665. (* instantiate (a-2)/4 *) apply Mid.C_121665. (* instantiate (a-2)/4 *)
...@@ -177,14 +177,14 @@ Definition RFC (n: list Z) (p: list Z) : list Z := ...@@ -177,14 +177,14 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
let k := decodeScalar25519 n in let k := decodeScalar25519 n in
let u := decodeUCoordinate p in let u := decodeUCoordinate p in
let t := montgomery_rec let t := montgomery_rec
255 (* iterate 255 times *) 255 (* iterate 255 times *)
k (* clamped n *) k (* clamped n *)
1 (* x_2 *) 1 (* x_2 *)
u (* x_3 *) u (* x_3 *)
0 (* z_2 *) 0 (* z_2 *)
1 (* z_3 *) 1 (* z_3 *)
0 (* dummy *) 0 (* dummy *)
0 (* dummy *) 0 (* dummy *)
u (* x_1 *) in u (* x_1 *) in
let a := get_a t in let a := get_a t in
let c := get_c t in let c := get_c t in
......
...@@ -35,7 +35,7 @@ ...@@ -35,7 +35,7 @@
\renewcommand{\algorithmicrequire}{\textbf{Input:\ }} \renewcommand{\algorithmicrequire}{\textbf{Input:\ }}
\renewcommand{\algorithmicensure}{\textbf{Output:\ }} \renewcommand{\algorithmicensure}{\textbf{Output:\ }}
\setlength{\abovecaptionskip}{-10pt} \setlength{\abovecaptionskip}{-9pt}
\newcommand{\todo}[1]{ \newcommand{\todo}[1]{
{\color{red} \bf TODO: #1} {\color{red} \bf TODO: #1}
...@@ -233,11 +233,11 @@ columns=[l]flexible, ...@@ -233,11 +233,11 @@ columns=[l]flexible,
literate= literate=
% {\\forall}{{\color{dkgreen}{$\forall\;$}}}1 % {\\forall}{{\color{dkgreen}{$\forall\;$}}}1
% {\\exists}{{$\exists\;$}}1 % {\\exists}{{$\exists\;$}}1
{<-}{{$\leftarrow\;$}}1 {<-}{{\makebox[8pt][l]{$\leftarrow\;$}}}1
{=>}{{$\Rightarrow\;$}}1 {=>}{{$\Rightarrow\;$}}1
{==>}{{\texttt{==>}\;}}1 {==>}{{\texttt{==>}\;}}1
% {:>}{{\texttt{:>}\;}}1 % {:>}{{\texttt{:>}\;}}1
{->}{{$\rightarrow\;$}}1 {->}{{\makebox[8pt][l]{$\rightarrow\;$}}}1
{<->}{{$\leftrightarrow\;$}}1 {<->}{{$\leftrightarrow\;$}}1
{<=}{{$\leq\;$}}1 {<=}{{$\leq\;$}}1
{==}{{\texttt{==}\;}}1 {==}{{\texttt{==}\;}}1
...@@ -274,38 +274,39 @@ literate= ...@@ -274,38 +274,39 @@ literate=
{^n}{{$^n$}}1 {^n}{{$^n$}}1
{^+n}{{$^n$}}1 {^+n}{{$^n$}}1
{^m}{{$^m$}}1 {^m}{{$^m$}}1
{^2}{{$^2$}}1 {^2}{{\makebox[8pt][l]{$^2$}}}1
{^+2}{{$^2$}}1 {^+2}{{\makebox[8pt][l]{$^2$}}}1
{^3}{{$^3$}}1 {^3}{{\makebox[8pt][l]{$^3$}}}1
{^+3}{{$^3$}}1 {^+3}{{\makebox[8pt][l]{$^3$}}}1
{^nd}{{$^{nd}$}}1 {^nd}{{$^{nd}$}}1
{^rd}{{$^{rd}$}}1 {^rd}{{$^{rd}$}}1
{^th}{{$^{th}$}}1 {^th}{{$^{th}$}}1
{^255}{{$^{255}$}}1 {^255}{{$^{255}$}}1
{^-1}{{$^{-1}$}}1 {^-1}{{$^{-1}$}}1
{\%:R}{{}}1 {\%:R}{{}}1
{p1}{{p$_1$}}1 {p1}{{p\makebox[8pt][l]{$_1$}}}1
{p2}{{p$_2$}}1 {p2}{{p\makebox[8pt][l]{$_2$}}}1
{x1}{{x$_1$}}1 {x1}{{x\makebox[8pt][l]{$_1$}}}1
{x2}{{x$_2$}}1 {x2}{{x\makebox[8pt][l]{$_2$}}}1
{x3}{{x$_3$}}1 {x3}{{x\makebox[8pt][l]{$_3$}}}1
{x_1}{{x$_1$}}1 {x_1}{{x\makebox[8pt][l]{$_1$}}}1
{x_2}{{x$_2$}}1 {x_2}{{x\makebox[8pt][l]{$_2$}}}1
{x_3}{{x$_3$}}1 {x_3}{{x\makebox[8pt][l]{$_3$}}}1
{x4}{{x$_4$}}1 {x4}{{x\makebox[8pt][l]{$_4$}}}1
{y1}{{y$_1$}}1 {y1}{{y\makebox[8pt][l]{$_1$}}}1
{y2}{{y$_2$}}1 {y2}{{y\makebox[8pt][l]{$_2$}}}1
{y3}{{y$_3$}}1 {y3}{{y\makebox[8pt][l]{$_3$}}}1
{y4}{{y$_4$}}1 {y4}{{y\makebox[8pt][l]{$_4$}}}1
{z1}{{z$_1$}}1 {z1}{{z\makebox[8pt][l]{$_1$}}}1
{z2}{{z$_2$}}1 {z2}{{z\makebox[8pt][l]{$_2$}}}1
{z3}{{z$_3$}}1 {z3}{{z\makebox[8pt][l]{$_3$}}}1
{z4}{{z$_4$}}1 {z4}{{z\makebox[8pt][l]{$_4$}}}1
{z_2}{{z$_2$}}1 {z_2}{{z\makebox[8pt][l]{$_2$}}}1
{z_3}{{z$_3$}}1 {z_3}{{z\makebox[8pt][l]{$_3$}}}1
{xs}{{x$_s$}}1 {xs}{{x\makebox[8pt][l]{$_s$}}}1
{\\-}{{$-$}}1 {\\-}{{\makebox[9pt][c]{$-$}}}1
{\\+}{{$+$}}1 {\\+}{{\makebox[9pt][c]{$+$}}}1
{\\*}{{\makebox[9pt][c]{$*$}}}1
{\\boxplus}{{$\boxplus$}}1 {\\boxplus}{{$\boxplus$}}1
{\\circ}{{$\circ$}}1 {\\circ}{{$\circ$}}1
{\\GF}{{$\mathbb{F}_{2^{255}-19}$}}1 {\\GF}{{$\mathbb{F}_{2^{255}-19}$}}1
...@@ -385,7 +386,8 @@ literate= ...@@ -385,7 +386,8 @@ literate=
% basicstyle=\ttfamily\small, % 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 basicstyle=\ttfamily\footnotesize, % font that is used for the code
identifierstyle=\color{doc@lstidentifier}, identifierstyle=\color{doc@lstidentifier},
commentstyle=\color{doc@lstcomment}\itshape, commentstyle=\color{doc@lstcomment}\footnotesize,
% \itshape,
stringstyle=\color{doc@lststring}, stringstyle=\color{doc@lststring},
keywordstyle=\color{doc@lstkeyword}, keywordstyle=\color{doc@lstkeyword},
keywordstyle=[1]\color{doc@lstidentifiers2}, keywordstyle=[1]\color{doc@lstidentifiers2},
......
Supports Markdown
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