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)

---

Naming convention (to be implemented in both projects):

• we have a ⁠⁠⁠⁠Flag.fsti⁠⁠⁠⁠ with e.g. an ⁠⁠⁠⁠assume val aes_prf: bool⁠⁠⁠⁠ for every game-based each crypto assumption we use in the whole development. That file also records constraints, reflecting the order of games. For instance ⁠⁠⁠⁠assume val poly1305_mac1 : b:bool { poly1305_mac1 => aes_prf }⁠⁠⁠⁠.
• we typecheck once the whole development, hence guaranteeing that every valid combination of flags yields a well-type program. This justify that, as we switch a flag in accordance to a game-based assumption, the whole program is a valid adversary for that game.
• we have a directory "real" that contains ⁠⁠⁠⁠Flag.fst⁠⁠⁠⁠ setting every boolean to false ⁠⁠⁠⁠inline let aes_prf = false⁠⁠⁠⁠. We use ⁠⁠⁠⁠--include real⁠⁠⁠⁠ whenever we extract the real implementation, either in kremlin or ocaml.
• we could have others, although typing without revealing the flags seems good enough the (meta) game-based proof. TODO: write up relationship to ⁠⁠⁠⁠strong⁠⁠⁠⁠ booleans. Roughly, they are a way to document and aggregate crypto assumptions in the development.