let block a = lbytes (block_length a)
let block a =
lbytes (block_length a)
Spec.Agile.Cipher.fsti.checked
Spec.Chacha20.fst.checked Spec.AES.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Agile.Cipher.fsti
Spec.Agile.Cipher.cipher_alg Lib.ByteSequence.lbytes Spec.Agile.Cipher.block_length
module Spec.Agile.Cipher

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

#reset-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 1"

/// This module is concerned with defining an agile stream cipher, i.e. a
/// function that given: a key; an iv (nonce); a counter, produces a fresh
/// block. We leave details of key expansion to the ``.fst``, or possibly even
/// to the low-level implementation.

val force_flush_interleaving: unit

/// Definitions
/// -----------

type cipher_alg =
  | AES128
  | AES256
  | CHACHA20

/// The AES spec itself is agile; this is the same nested agility technique used
/// for SHA2 vs. MD.
let aes_alg_of_alg (a: cipher_alg { a = AES128 \/ a = AES256 }) =
  match a with
  | AES128 -> Spec.AES.AES128
  | AES256 -> Spec.AES.AES256

/// Trying to enforce conventions: lengths for nats (spec); len for machine
/// integers (runtime).
let key_length (a: cipher_alg): size_nat =
  match a with
  | AES128 | AES256 -> Spec.AES.key_size (aes_alg_of_alg a)
  | CHACHA20 -> Spec.Chacha20.size_key

let key (a: cipher_alg) =
  match a with
  | AES128 | AES256 -> Spec.AES.aes_key (aes_alg_of_alg a)
  | CHACHA20 -> Spec.Chacha20.key

let block_length (a:cipher_alg) =
  match a with
  | AES128 | AES256 -> 16
  | CHACHA20 -> 64
val block : a: Spec.Agile.Cipher.cipher_alg -> Type0
a: Spec.Agile.Cipher.cipher_alg -> Type0