Notes from a deep dive into BoringSSL's Curve25519 code on June 19, 2020, with
an eye for finding the path to a fully verified high-level crypto operation
using bedrock2, fiat-crypto, and rupicola.

# Crypto operations

These are the top-level operations, and depend on *scalar* (function names
usually include `sc`), *group* (`ge`), and *field* (`fe`) operations. Note that
"scalar" here does not actually mean scalar in the usual sense; the "scalars"
are members of a field modulo a parameter called _l_, which is simply a prime
field with a different modulus than the one used for "field" elements.

There are two top-level schemes provided in BoringSSL for Curve25519: Ed25519
and X25519 ([more on Curve25519
naming](https://mailarchive.ietf.org/arch/msg/cfrg/-9LEdnzVrE5RORux3Oo_oDDRksU/)).
Ed25519 is the signature system using Edwards coordinates, and X25519 is the
scheme using Montgomery X-coordinates and Diffie-Hellman. Both operations use
the same underlying curve.

These functions also depend on some SHA512 operations which are mentioned here
in parentheses but not expanded. `x25519_NEON` is also omitted (it is only used
if `BORINGSSL_X25519_NEON` is defined).

## Implementation links

[ED25519_keypair](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1879)
[ED25519_sign](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1885)
[ED25519_verify](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1924)
[X25519_keypair](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#2100)

## Callees

### Ed25519

- Scalar : `x25519_sc_reduce` `scmuladd` 
- Group : `x25519_ge_scalarmult_base` `x25519_ge_frombytes_vartime` `ge_double_scalarmult_vartime` `x25519_ge_tobytes` `ge_p3_tobytes`
- Field : `fe_neg` `fe_carry`

### X25519

- Group : `x25519_ge_scalarmult_base` `x25519_scalar_mult`
- Field : `fe_add` `fe_sub` `fe_loose_invert` `fe_mul_tlt` `fe_tobytes`

## Code graph

Here, and elsewhere, a `*` indicates a function that is low-level enough to
generate in fiat-crypto's AST but is currently not generated, and `+` indicates
a function that is already implemented with fiat-crypto's generated code.

```
ED25519_keypair
| (RAND_bytes)
| ED25519_keypair_from_seed
  | (SHA512, OPENSSL_memcpy)
  | x25519_ge_scalarmult_base
  | ge_p3_tobytes

ED25519_sign
| (SHA512, SHA512_Init, SHA512_Update, SHA512_Final)
| * x25519_sc_reduce
| x25519_ge_scalarmult_base
| * sc_muladd 

ED25519_verify
| (OPENSSL_memcpy, SHA512_Init, SHA512_Update, SHA512_Final, CRYPTO_memcmp)
| x25519_ge_frombytes_vartime
| + fe_neg
| + fe_carry
| * x25519_sc_reduce
| ge_double_scalarmult_vartime
| x25519_ge_tobytes

X25519_keypair
| (RAND_bytes)
| X25519_public_from_private
  | (OPENSSL_memcpy)
  | x25519_ge_scalarmult_base
  | + fe_add 
  | + fe_sub
  | + fe_loose_invert
  | + fe_mul_tlt
  | + fe_tobytes 

X25519
| (CRYPTO_memcmp)
| x25519_scalar_mult
```

# Scalar Operations

The top-level functions rely on just two scalar operations: `x25519_sc_reduce`
and `sc_muladd`. Both are low-level enough to be generated by fiat-crypto, in
theory, and could probably reuse parts of the field arithmetic infrastructure.
However, they might also include low-level optimizations at a similar level of
complexity to field arithmetic. (See
[https://github.com/mit-plv/fiat-crypto/issues/805](https://github.com/mit-plv/fiat-crypto/issues/805)
for some discussion).

`x25519_sc_reduce` implements full modular reduction (like `freeze`).

`sc_muladd(a, b, c)` produces `(ab + c) mod l`. Also full modular reduction,
although implementation looks like Solinas.

## Implementation links

[x25519_sc_reduce](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1057)
[sc_muladd](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1398)

## Callees

None

# Group Operations

These operations manipulate curve points (members of the curve algebraic
group). They depend on field operations mostly, but also a few uncategorized
helpers (here listed as "misc").

The function `x25519_scalar_mult` corresponds to `montladder` in the
fiat-crypto repository and a bedrock2 version exists in rupicola, but has not
at the time of writing been integrated to BoringSSL or proven to connect to the
specifications of the field operations. 

Note" `x25519_ge_scalarmult` is also defined and used in the SPAKE2 protocol,
but not for the core Ed25519.

## Implementation links

[x25519_ge_tobytes](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#479)
[ge_p3_tobytes](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#491)
[x25519_ge_frombytes_vartime](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#503)
[ge_p3_0](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#555)
[ge_cached_0](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#569)
[ge_p3_to_p2](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#576)
[x25519_ge_p3_to_cached](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#583)
[x25519_ge_p1p1_to_p2](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#591)
[x25519_ge_p1p1_to_p3](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#598)
[ge_p2_dbl](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#613)
[ge_p3_dbl](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#632)
[ge_madd](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#639)
[ge_msub](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#656)
[x25519_ge_add](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#673)
[x25519_ge_sub](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#691)
[cmov](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#718)
[x25519_ge_scalarmult_small_precomp](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#724)
[x25519_ge_scalarmult_base (if OPENSSL_SMALL defined)](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#780)
[table_select](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#792)
[x25519_ge_scalarmult_base (if OPENSSL_SMALL undefined)](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#823)
[ge_double_scalarmult_vartime](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#972)

## Callees

- Field: `fe_frombytes` `fe_0` `fe_1` `fe_cswap` `fe_add` `fe_sub` `fe_mul_impl` `fe_sq_tl` `fe_mul121666` `fe_invert` `fe_tobytes` `fe_frombytes_strict` `fe_cmov` `fe_copy_ll` `fe_carry` `fe_neg` `fe_copy_lt` `fe_copy` `fe_sq_tt` `fe_sq2_tt` `fe_isnonzero` `fe_isnegative` `fe_invert` `fe_loose_0` `fe_loose_1` `fe_pow22523`
- Misc: `equal` `negative` `slide`

Note: `fe_mul_impl` is called through various wrappers: `fe_mul_ltt` `fe_mul_llt` `fe_mul_ttt` `fe_mul_tlt` `fe_mul_ttl` `fe_mul_tll`.

## Code graph

Starting from callees of crypto operations.

```
x25519_scalar_mult
| x25519_scalar_mult_generic
  | + fe_frombytes
  | * fe_1
  | * fe_0
  | * fe_copy
  | * fe_cswap
  | + fe_sub
  | + fe_add
  | + fe_mul_tll
  | + fe_sq_tl
  | + fe_mul121666
  | + fe_mul_ttt
  | fe_invert
  | + fe_tobytes

x25519_ge_scalarmult_base (if OPENSSSL_SMALL defined)
| x25519_ge_scalarmult_small_precomp
  | + fe_frombytes_strict
  | + fe_add
  | + fe_sub
  | + fe_mul_ltt
  | ge_p3_0
    | * fe_0
    | * fe_1
  | * equal
  | cmov
    | * fe_cmov
    | * fe_copy_ll
    | + fe_carry
    | + fe_neg
  | x25519_ge_p3_to_cached
    | + fe_add
    | + fe_sub
    | * fe_copy_lt
    | + fe_mul_llt
  | x25519_ge_add
    | + fe_add
    | + fe_sub
    | + fe_mul_tll
    | + fe_carry
  | x25519_ge_p1p1_to_p3
    | + fe_mul_tll

x25519_ge_scalarmult_base (if OPENSSL_SMALL undefined)
| ge_p3_0
  | * fe_0
  | * fe_1
| table_select
  | ge_precomp_0
    | * fe_loose_1
    | * fe_loose_0
  | * negative
  | * equal
  | cmov
    | * fe_cmov
    | * fe_copy_ll
    | + fe_carry
    | + fe_neg
  | * fe_copy_ll
  | + fe_carry
  | + fe_neg
| ge_madd
  | + fe_add
  | + fe_sub
  | + fe_mul_tll
  | + fe_carry
| x25519_ge_p1p1_to_p3
  | + fe_mul_tll
| ge_p3_dbl
  | ge_p3_to_p2
    | * fe_copy
  | ge_p2_dbl
    | + fe_sq_tt
    | fe_sq2_tt
    | + fe_add
    | + fe_sq_tl
    | + fe_sub
    | + fe_carry
    | + fe_sub
| x25519_ge_p1p1_to_p2
  | + fe_mul_tll

x25519_ge_frombytes_vartime
| + fe_frombytes
| * fe_1
| + fe_sq_tt
| + fe_mul_ttt
| + fe_sub
| + fe_carry
| + fe_add
| + fe_sq_tl
| + fe_mul_ttl
| * fe_pow22523
| fe_isnonzero
| fe_isnegative

ge_double_scalarmult_vartime
| * slide
| x25519_ge_p3_to_cached
  | + fe_add
  | + fe_sub
  | * fe_copy_lt
  | + fe_mul_llt
| ge_p3_dbl
  | ge_p3_to_p2
    | * fe_copy
  | ge_p2_dbl
    | + fe_sq_tt
    | fe_sq2_tt
    | + fe_add
    | + fe_sq_tl
    | + fe_sub
    | + fe_carry
    | + fe_sub
| x25519_ge_p1p1_to_p3
  | + fe_mul_tll
| x25519_ge_add
  | + fe_add
  | + fe_sub
  | + fe_mul_tll
  | + fe_mul_tlt
  | + fe_mul_ttl
  | + fe_carry
| x25519_ge_sub
  | + fe_add
  | + fe_sub
  | + fe_mul_tll
  | + fe_mul_tlt
  | + fe_mul_ttl
  | + fe_carry
| ge_p2_dbl
  | + fe_sq_tt
  | fe_sq2_tt
  | + fe_add
  | + fe_sq_tl
  | + fe_sub
  | + fe_carry
  | + fe_sub
| ge_madd
  | + fe_add
  | + fe_sub
  | + fe_mul_tll
  | + fe_carry
| ge_msub
  | + fe_add
  | + fe_sub
  | + fe_mul_tll
  | + fe_mul_tlt
  | + fe_carry

x25519_ge_tobytes
| fe_invert
| + fe_mul_ttt
| + fe_tobytes
| fe_isnegative

ge_p3_tobytes
| fe_invert
| + fe_mul_ttt
| + fe_tobytes
| fe_isnegative
```

# Field Operations

Mostly, these are complete. However, there are a couple that aren't and seem
easy to verify given our existing proven operations.

The functions that are just wrappers (with bounds assertions) for calls to
fiat-crypto generated code are: `fe_frombytes_strict` `fe_tobytes` `fe_add`
`fe_sub` `fe_carry` `fe_mul_impl` `fe_sq_tl` `fe_sq_tt` `fe_mul_121666`
`fe_neg`

Additionally, the following functions are fairly trivial wrappers for the ones
listed above: `fe_frombytes` `fe_mul_ltt` `fe_mul_llt` `fe_mul_ttt`
`fe_mul_tlt` `fe_mul_ttl` `fe_mul_tll`

There's a bit of a special case with`fe_cmov`; it should use fiat-crypto's
`selectznz`, but there's a TODO in the codebase to make the calling conventions
match up.

That leaves the following field operations:

- `fe_0` `fe_loose_0` `fe_1` `fe_loose_1` : literal 0s and 1s
- `fe_cswap`: conditional swap of field elements
- `fe_copy` `fe_copy_lt` `fe_copy_ll`: copying content of field elements
- `fe_loose_invert` : inversion (there's a PR on fiat-crypto that does inversion -- is it the same algorithm?)
- `fe_invert` : inversion (wrapper for `fe_loose_invert`)
- `fe_isnonzero` : converts to bytes and checks if the bytes are 0
- `fe_isnegative` : converts to bytes and checks if odd
- `fe_sq2_tt` : calls `fe_sq_tt` and adds result to itself
- `fe_pow22523`: sequence of squares and multiplications

All of these should be very reasonable to write in bedrock2 and prove correct
against existing field operations (with the exception of inversion, if the PR
is a different algorithm). In terms of value added by verification,
`fe_pow22523` is probably the best, while `fe_sq2_tt`, `fe_isnonzero`, and
`fe_isnegative` would be reasonable.

### Code graph

Operations not listed here have no callees at the field level or above.

```
fe_sq2_tt
| + fe_sq_tt
| + fe_add
| + fe_carry

fe_invert
| * fe_copy_lt
| fe_loose_invert
  | + fe_sq_tl
  | + fe_sq_tt
  | + fe_mul_tlt
  | + fe_mul_ttt

fe_isnonzero
| + fe_carry
| + fe_tobytes

fe_isnegative
| + fe_tobytes

fe_pow22523
| + fe_sq_tt
| + fe_mul_ttt
```

# Misc Operations

The group level relies on a few self-contained  helper functions:

- `slide` is probably something to do with "sliding window"; it transforms an
array of bytes with low-level computations. Unclear what the specification
should be, but otherwise reasonable to write up in bedrock2.
- `negative` computes whether a signed byte is negative (not suitable for
        bedrock2, probably, because it involves typecasting to larger integers)
- `equal` computes whether two signed bytes are equal (not suitable for
        bedrock2, probably, because it involves typecasting to larger integers)