val va_code_KeyExpansionStdcall : alg:algorithm -> Tot va_code
let va_code_KeyExpansionStdcall alg =
  (va_Block (va_CCons (va_code_CreateHeaplets ()) (va_CCons (if (alg = AES_128) then va_Block
    (va_CCons (va_code_KeyExpansion128Stdcall ()) (va_CNil ())) else va_Block (va_CCons
    (va_code_KeyExpansion256Stdcall ()) (va_CNil ()))) (va_CCons (va_code_DestroyHeaplets ())
    (va_CNil ())))))
val va_code_KeyExpansionStdcall : alg:algorithm -> Tot va_code
let va_code_KeyExpansionStdcall alg =
(va_Block (va_CCons (va_code_CreateHeaplets ())
        (va_CCons (if (alg = AES_128)
              then va_Block (va_CCons (va_code_KeyExpansion128Stdcall ()) (va_CNil ()))
              else va_Block (va_CCons (va_code_KeyExpansion256Stdcall ()) (va_CNil ())))
            (va_CCons (va_code_DestroyHeaplets ()) (va_CNil ())))))
Vale.AES.PPC64LE.AES.fst.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.QuickCodes.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsVector.fsti.checked Vale.PPC64LE.InsMem.fsti.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.AES.PPC64LE.AES256.fsti.checked Vale.AES.PPC64LE.AES128.fsti.checked Vale.AES.AES_common_s.fst.checked Vale.AES.AES_BE_s.fst.checked Vale.AES.AES256_helpers_BE.fsti.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.PPC64LE.AES.fst
Vale.AES.AES_common_s.algorithm Vale.PPC64LE.Decls.va_Block Vale.PPC64LE.Decls.va_CCons Vale.PPC64LE.InsMem.va_code_CreateHeaplets Prims.op_Equality Vale.AES.AES_common_s.AES_128 Vale.AES.PPC64LE.AES128.va_code_KeyExpansion128Stdcall Vale.PPC64LE.Decls.va_CNil Prims.bool Vale.AES.PPC64LE.AES256.va_code_KeyExpansion256Stdcall Vale.PPC64LE.Decls.va_code Vale.PPC64LE.InsMem.va_code_DestroyHeaplets
module Vale.AES.PPC64LE.AES
open Vale.Def.Types_s
open FStar.Seq
open Vale.Arch.HeapImpl
open Vale.AES.AES_BE_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.InsBasic
open Vale.PPC64LE.InsMem
open Vale.PPC64LE.InsVector
open Vale.PPC64LE.QuickCode
open Vale.PPC64LE.QuickCodes
open Vale.Arch.Types
open Vale.Def.Opaque_s
open Vale.AES.PPC64LE.AES128
open Vale.AES.PPC64LE.AES256
#reset-options "--z3rlimit 20"
//-- KeyExpansionStdcall

[@ "opaque_to_smt" va_qattr]
val va_code_KeyExpansionStdcall : alg:algorithm -> Tot va_code
alg: Vale.AES.AES_common_s.algorithm -> Vale.PPC64LE.Decls.va_code