let xkey (a: cipher_alg) =
  match a with
  | AES128 | AES256 -> Spec.AES.aes_xkey (aes_alg_of_alg a)
  | CHACHA20 -> Spec.Chacha20.key
let xkey (a: cipher_alg) =
match a with
| AES128 | AES256 -> Spec.AES.aes_xkey (aes_alg_of_alg a)
| CHACHA20 -> Spec.Chacha20.key
Spec.Agile.Cipher.fst.checked
Spec.Chacha20.fst.checked Spec.AES.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Agile.Cipher.fst
Spec.Agile.Cipher.cipher_alg Spec.AES.aes_xkey Spec.Agile.Cipher.aes_alg_of_alg Spec.Chacha20.key
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"

let force_flush_interleaving = ()

let aes_ctr_block_add_counter (block: lbytes 16) (incr:size_nat): Tot (lbytes 16) =
  let n = nat_from_bytes_be block in
  let n' = (n + incr) % pow2 128 in
  nat_to_bytes_be 16 n'
val xkey : a: Spec.Agile.Cipher.cipher_alg -> Type0
a: Spec.Agile.Cipher.cipher_alg -> Type0