https://github.com/project-everest/hacl-star
Tip revision: 1a7d0aa25e64c89a2190fe71cc33b0c97ced3eda authored by Aymeric Fromherz on 09 October 2019, 08:11:52 UTC
Propagate metapoly to chachapoly + rlimit
Propagate metapoly to chachapoly + rlimit
Tip revision: 1a7d0aa
README.md
## Implementations of SHA1, SHA2 and MD5 hash algorithms
### What this directory is about
This directory contains a revamped implementation of several hash algorithms. In
particular, this code demonstrates:
- the use of the latest F\* features, e.g. top-level immutable arrays
- guidelines for multiplexing and code organization.
In this directory, and more generally on the HACL\* side of things, we are
concerned with:
- static multiplexing, i.e. functions that *do not* extract, but perform static
dispatch on a finite set of cases; the typical example is:
```
inline_for_extraction noextract
let update (a: hash_alg) (s: state a) (b: bytes { B.length b % block_size a = 0 }) =
match a with
| SHA2_256 -> update_sha2_256 s b
| SHA2_512 -> update_sha2_512 s b
```
the `update` function cannot extract to C, because `state a` is either
`uint32_t *` or `uint64_t *`; however, any caller is welcome to call `update`
as long as they apply it to a constant first argument, triggering partial
evaluation by F\*
- HACL-only implementations; we do not talk about Vale; in the rare event that
HACL\* should need some generic functionality (e.g. PRNG), HACL\* will use
EverCrypt.
- single-algorithm specialized modules, i.e. `Hacl.Hash.SHA2`, which contains
monomorphic, specialized versions of all the generic hash combinators
We are not concerned with:
- dynamic multiplexing, which involves run-time tests and a uniform
representation of state, in C, for all algorithms
- other implementations, e.g. Vale.
These concerns belong in EverCrypt.
### Code structure
Tentative.
- `Hacl.Hash.Definitions`, Low\* types for states, data structures and stateful
functions, along with helper functions defined for all hash algorithms (e.g.
block size, etc.)
- `Hacl.Hash.PadFinish`, generic implementations of `pad` and `finish` for all
hash algorithms
- `Hacl.Hash.X.Core`, base functions for algorithm `X`, i.e. `alloca`, `init`,
`update`, `pad` and `finish`
- `Hacl.Hash.Agile`, a layer of static multiplexing for base functions across
all hash algorithms
- `Hacl.Hash.MerkleDamgard`, the generic construction built on top of static
multiplexing, using non-extractable higher-order functions, i.e.
`mk_update_multi`, `mk_update_last`, `mk_hash`
- `Hacl.Hash.X`, a full set of functions for algorithm `X`, including all the
base functions along with specialized, monomorphic instances of the generic
constructions above