val aes_ctr_block_add_counter (block: lbytes 16) (incr: size_nat) : Tot (lbytes 16)
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 aes_ctr_block_add_counter (block: lbytes 16) (incr: size_nat) : Tot (lbytes 16)
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'
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
Lib.ByteSequence.lbytes Lib.IntTypes.size_nat Lib.ByteSequence.nat_to_bytes_be Lib.IntTypes.SEC Prims.int Prims.op_Modulus Prims.op_Addition Prims.pow2 Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Multiply Lib.Sequence.length Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.ByteSequence.nat_from_bytes_be
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 = ()
val aes_ctr_block_add_counter (block: lbytes 16) (incr: size_nat) : Tot (lbytes 16)
block: Lib.ByteSequence.lbytes 16 -> incr: Lib.IntTypes.size_nat -> Lib.ByteSequence.lbytes 16