val key_offset (i: vale_impl)
    : o: UInt32.t{UInt32.v o = Vale.Wrapper.X64.AES.key_offset (vale_alg_of_vale_impl i)}
let key_offset (i: vale_impl):
  o:UInt32.t { UInt32.v o = Vale.Wrapper.X64.AES.key_offset (vale_alg_of_vale_impl i) }
=
  match i with
  | Vale_AES128 -> 176ul
  | Vale_AES256 -> 240ul
val key_offset (i: vale_impl)
    : o: UInt32.t{UInt32.v o = Vale.Wrapper.X64.AES.key_offset (vale_alg_of_vale_impl i)}
let key_offset (i: vale_impl)
    : o: UInt32.t{UInt32.v o = Vale.Wrapper.X64.AES.key_offset (vale_alg_of_vale_impl i)} =
match i with
| Vale_AES128 -> 176ul
| Vale_AES256 -> 240ul
EverCrypt.CTR.Keys.fst.checked
Vale.X64.CPU_Features_s.fst.checked Vale.Wrapper.X64.AEShash.fsti.checked Vale.Wrapper.X64.AES.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.AES.OptPublic.fsti.checked Vale.AES.Gcm_simplify.fsti.checked Vale.AES.AES_s.fst.checked Spec.Cipher.Expansion.fst.checked Spec.Cipher.Expansion.fst.checked Spec.Agile.Cipher.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked Lib.IntTypes.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
EverCrypt.CTR.Keys.fst
EverCrypt.CTR.Keys.vale_impl FStar.UInt32.__uint_to_t FStar.UInt32.t Prims.b2t Prims.op_Equality Prims.int FStar.UInt32.v Vale.Wrapper.X64.AES.key_offset EverCrypt.CTR.Keys.vale_alg_of_vale_impl
module EverCrypt.CTR.Keys

/// This is an internal-to-EverCrypt module, which provides low-level
/// definitions corresponding to Spec.Cipher.Expansion, i.e. shared between CTR
/// and AEAD.

module S = FStar.Seq
module G = FStar.Ghost

module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module B = LowStar.Buffer

open FStar.HyperStack.ST
open FStar.Integers

open Spec.Agile.Cipher
open Spec.Cipher.Expansion

friend Spec.Cipher.Expansion

#set-options "--z3rlimit 100 --max_fuel 0 --max_ifuel 0"

let _: squash (inversion impl) = allow_inversion impl

inline_for_extraction noextract
let vale_impl = a:impl { a = Vale_AES128 \/ a = Vale_AES256 }

let vale_alg_of_vale_impl (i: vale_impl) =
  match i with
  | Vale_AES128 -> Vale.AES.AES_s.AES_128
  | Vale_AES256 -> Vale.AES.AES_s.AES_256

inline_for_extraction noextract
let key_offset (i: vale_impl):
  o:UInt32.t { UInt32.v o = Vale.Wrapper.X64.AES.key_offset (vale_alg_of_vale_impl i) }
val key_offset (i: vale_impl)
    : o: UInt32.t{UInt32.v o = Vale.Wrapper.X64.AES.key_offset (vale_alg_of_vale_impl i)}
i: EverCrypt.CTR.Keys.vale_impl
  -> o:
    FStar.UInt32.t
      { FStar.UInt32.v o =
        Vale.Wrapper.X64.AES.key_offset (EverCrypt.CTR.Keys.vale_alg_of_vale_impl i) }