val ctr_block (a: cipher_alg) (k: key a) (iv: nonce a) (c: ctr): block a
let ctr_block (a: cipher_alg) (k: key a) (iv: nonce a) (c: ctr): block a =
  let k = expand a k in
  match a with
  | AES128 | AES256 ->
      let open Spec.AES in
      let open Lib.LoopCombinators in
      let block = create 16 (u8 0) in
      let block = repeati #(lbytes 16) (length iv) (fun i b -> b.[i] <- Seq.index iv i) block in
      let block = aes_ctr_block_add_counter block c in
      aes_encrypt_block (aes_alg_of_alg a) k block

  | CHACHA20 ->
      let open Spec.Chacha20 in
      let block = chacha20_init k iv c in
      let block' = rounds block in
      uints_to_bytes_le (sum_state block block')
val ctr_block (a: cipher_alg) (k: key a) (iv: nonce a) (c: ctr): block a
let ctr_block (a: cipher_alg) (k: key a) (iv: nonce a) (c: ctr) : block a =
let k = expand a k in
match a with
| AES128
| AES256 ->
  let open Spec.AES in
  let open Lib.LoopCombinators in
  let block = create 16 (u8 0) in
  let block = repeati #(lbytes 16) (length iv) (fun i b -> b.[ i ] <- Seq.index iv i) block in
  let block = aes_ctr_block_add_counter block c in
  aes_encrypt_block (aes_alg_of_alg a) k block
| CHACHA20 ->
  let open Spec.Chacha20 in
  let block = chacha20_init k iv c in
  let block' = rounds block in
  uints_to_bytes_le (sum_state block block')
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.Agile.Cipher.key Spec.Agile.Cipher.nonce Spec.Agile.Cipher.ctr Spec.AES.aes_encrypt_block Spec.Agile.Cipher.aes_alg_of_alg Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Agile.Cipher.aes_ctr_block_add_counter Lib.LoopCombinators.repeati Lib.ByteSequence.lbytes Lib.Sequence.length Lib.IntTypes.uint_t Prims.nat Prims.b2t Prims.op_LessThan Lib.Sequence.op_String_Assignment FStar.Seq.Base.index Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.create Lib.IntTypes.mk_int Prims.l_Forall Prims.l_imp Lib.Sequence.index Lib.Sequence.create Lib.IntTypes.u8 Lib.ByteSequence.uints_to_bytes_le Lib.IntTypes.U32 Spec.Chacha20.sum_state Spec.Chacha20.state Spec.Chacha20.rounds Spec.Chacha20.chacha20_init Spec.Agile.Cipher.block Spec.Agile.Cipher.xkey Spec.Agile.Cipher.expand
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'

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

/// As specified by the NIST. Other implementations (e.g. Vale) may perform
/// other steps beyond key expansion but this is an implementation detail.
let expand (a: cipher_alg) (k: key a): xkey a =
  match a with
  | AES128 | AES256 -> Spec.AES.aes_key_expansion (aes_alg_of_alg a) k
  | CHACHA20 -> k
val ctr_block (a: cipher_alg) (k: key a) (iv: nonce a) (c: ctr): block a

    a: Spec.Agile.Cipher.cipher_alg ->
    k: Spec.Agile.Cipher.key a ->
    iv: Spec.Agile.Cipher.nonce a ->
    c: Spec.Agile.Cipher.ctr
  -> Spec.Agile.Cipher.block a