Cédric's notes

@channel Summary of our discussion on file names and code restructuring for low-level crypto (for now on the ⁠⁠⁠⁠fournet_aead⁠⁠⁠⁠ branch of F*). ⁠⁠⁠⁠FStar.Buffer⁠⁠⁠⁠ to be improved a bit, and extended with common type aliases:

type uint8_s = Seq.seq Uint8.t
type uint8_p = Buffer.buffer Uint8.t
type uint8_sl (l:nat) = s:uint8_s {Seq.length s = l}
type uint8_pl (l:nat) = b:uint8_p {Buffer.length b = l}

and similarly for uint32.t ⁠⁠⁠⁠Fstar.Buffer.Utils⁠⁠⁠⁠ to subsume ⁠⁠⁠⁠Crypto.Symmetric.Bytes⁠⁠⁠⁠, meant to include useful coding on top of buffers, such as conversion with various integers. ⁠⁠⁠⁠FStar.Buffer.Alloc⁠⁠⁠⁠ to isolate any Stack code that may implicitly allocate immutable stuff on the back-end heap, thereby escaping the Low*/Kremlin discipline. We need it for idealization, for testing, for ocaml apps such as miTLS. But we need to exclude it from concrete HACL*. ⁠⁠⁠⁠Crypto.Symmetric.Cipher⁠⁠⁠⁠ to replace ⁠⁠⁠⁠Crypto.Symmetric.BlockCipher⁠⁠⁠⁠ and multiplex between Chacha and 3 flavors or AES. ⁠⁠⁠⁠Crypto.Symmetric.PRF⁠⁠⁠⁠ to idealize it. ⁠⁠⁠⁠Crypto.Symmetric.MAC⁠⁠⁠⁠ to idealize and encode and multiplex between POLY1305 and GF128 (we may split it e.g. into ⁠⁠⁠⁠MAC⁠⁠⁠⁠ and ⁠⁠⁠⁠INT1CMA⁠⁠⁠⁠) ⁠⁠⁠⁠Crypto.AEAD⁠⁠⁠⁠ to replace ⁠⁠⁠⁠Crypto.AEAD.ChachaPoly1305.Ideal⁠⁠⁠⁠ and multiplex between Chacha20Poly1305, AES256_GCM, and possibly other combinations.
⁠⁠⁠⁠Crypto.AEAD.Test⁠⁠⁠⁠ to replace ⁠⁠⁠⁠Test⁠⁠⁠⁠ and do functionality testing (and similarly for the other files, moving test code from ML to F*) We'll atomically implement those changes by the end of this week, unless someone objects. The plan is then to integrate those files into HACL* and adapt it accordingly, so that it can entirely replace ⁠⁠⁠⁠low-level/crypto⁠⁠⁠⁠. (edited)