val gctr_encrypt_block (icb_BE plain_LE: quad32) (alg: algorithm) (key: seq nat32) (i: int)
    : Pure quad32 (requires is_aes_key_LE alg key) (ensures fun _ -> True)
let gctr_encrypt_block (icb_BE:quad32) (plain_LE:quad32) (alg:algorithm) (key:seq nat32) (i:int) : Pure quad32
  (requires is_aes_key_LE alg key)
  (ensures fun _ -> True)
  =
  let icb_LE = reverse_bytes_quad32 (inc32 icb_BE i) in
  quad32_xor plain_LE (aes_encrypt_LE alg key icb_LE)
val gctr_encrypt_block (icb_BE plain_LE: quad32) (alg: algorithm) (key: seq nat32) (i: int)
    : Pure quad32 (requires is_aes_key_LE alg key) (ensures fun _ -> True)
let gctr_encrypt_block (icb_BE plain_LE: quad32) (alg: algorithm) (key: seq nat32) (i: int)
    : Pure quad32 (requires is_aes_key_LE alg key) (ensures fun _ -> True) =
let icb_LE = reverse_bytes_quad32 (inc32 icb_BE i) in
quad32_xor plain_LE (aes_encrypt_LE alg key icb_LE)
Vale.AES.GCTR_s.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.GCTR_s.fst
Vale.Def.Types_s.quad32 Vale.AES.AES_common_s.algorithm FStar.Seq.Base.seq Vale.Def.Types_s.nat32 Prims.int Vale.Def.Types_s.quad32_xor Vale.AES.AES_s.aes_encrypt_LE Vale.Def.Types_s.reverse_bytes_quad32 Vale.AES.GCTR_s.inc32 Vale.AES.AES_s.is_aes_key_LE Prims.l_True
module Vale.AES.GCTR_s

// IMPORTANT: Following NIST's specification, this spec is written assuming a big-endian mapping from bytes to quad32s
//            Since the AES spec (AES_s) is in little-endian, we need to byteswap each time we call AES

open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open Vale.AES.AES_s
open FStar.Seq

// The max length of pow2_32 corresponds to the max length of buffers in Low*
// length plain < pow2_32 <= spec max of 2**39 - 256;
let is_gctr_plain_LE (p:seq nat8) : prop0 = length p < pow2_32
type gctr_plain_LE:eqtype = p:seq nat8 { is_gctr_plain_LE p }
type gctr_plain_internal_LE:eqtype = seq quad32

let inc32 (cb:quad32) (i:int) : quad32 =
  Mkfour ((cb.lo0 + i) % pow2_32) cb.lo1 cb.hi2 cb.hi3

let gctr_encrypt_block (icb_BE:quad32) (plain_LE:quad32) (alg:algorithm) (key:seq nat32) (i:int) : Pure quad32
  (requires is_aes_key_LE alg key)
val gctr_encrypt_block (icb_BE plain_LE: quad32) (alg: algorithm) (key: seq nat32) (i: int)
    : Pure quad32 (requires is_aes_key_LE alg key) (ensures fun _ -> True)

    icb_BE: Vale.Def.Types_s.quad32 ->
    plain_LE: Vale.Def.Types_s.quad32 ->
    alg: Vale.AES.AES_common_s.algorithm ->
    key: FStar.Seq.Base.seq Vale.Def.Types_s.nat32 ->
    i: Prims.int
  -> Prims.Pure Vale.Def.Types_s.quad32