val alg : Type0
let alg = Spec.cipher_alg
module NotEverCrypt.CTR

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module G = FStar.Ghost

module Spec = Spec.Agile.CTR

open FStar.HyperStack.ST
open EverCrypt.Error
/
Spec.Loops.fst.checked Spec.Agile.CTR.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Error.fsti.checked
NotEverCrypt.CTR.fsti
Type0
Spec.Agile.Cipher.cipher_alg
let alg =
  
Spec.cipher_alg