val va_codegen_success_KeyExpansionRoundEven256 : round:nat8 -> rcon:nat8 -> Tot va_pbool
let va_codegen_success_KeyExpansionRoundEven256 round rcon =
  (va_pbool_and (va_codegen_success_Vspltisw (va_op_vec_opr_vec 0) 0) (va_pbool_and
    (va_codegen_success_Vspltisw (va_op_vec_opr_vec 4) 8) (va_pbool_and (va_codegen_success_Vsbox
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3)) (va_pbool_and (va_codegen_success_LoadImmShl64
    (va_op_reg_opr_reg 10) rcon) (va_pbool_and (va_codegen_success_Mtvsrws (va_op_vec_opr_vec 5)
    (va_op_reg_opr_reg 10)) (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec 2)
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 5)) (va_pbool_and (va_codegen_success_RotWord
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 4)) (va_pbool_and
    (va_codegen_success_Vspltw (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) 3) (va_pbool_and
    (va_codegen_success_Vsldoi (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 1)
    12) (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 4)) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 4)
    (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 1) 12) (va_pbool_and (va_codegen_success_Vxor
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 4)) (va_pbool_and
    (va_codegen_success_Vsldoi (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 1)
    12) (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 4)) (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 2)) (va_pbool_and (va_codegen_success_LoadImm64
    (va_op_reg_opr_reg 10) (16 `op_Multiply` (round + 1))) (va_pbool_and
    (va_codegen_success_Store128_byte16_buffer_index (va_op_heaplet_mem_heaplet 1)
    (va_op_vec_opr_vec 1) (va_op_reg_opr_reg 3) (va_op_reg_opr_reg 10) Secret) (va_ttrue
    ()))))))))))))))))))
val va_codegen_success_KeyExpansionRoundEven256 : round:nat8 -> rcon:nat8 -> Tot va_pbool
let va_codegen_success_KeyExpansionRoundEven256 round rcon =
(va_pbool_and (va_codegen_success_Vspltisw (va_op_vec_opr_vec 0) 0)
    (va_pbool_and (va_codegen_success_Vspltisw (va_op_vec_opr_vec 4) 8)
        (va_pbool_and (va_codegen_success_Vsbox (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3))
            (va_pbool_and (va_codegen_success_LoadImmShl64 (va_op_reg_opr_reg 10) rcon)
                (va_pbool_and (va_codegen_success_Mtvsrws (va_op_vec_opr_vec 5)
                        (va_op_reg_opr_reg 10))
                    (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec 2)
                            (va_op_vec_opr_vec 2)
                            (va_op_vec_opr_vec 5))
                        (va_pbool_and (va_codegen_success_RotWord (va_op_vec_opr_vec 2)
                                (va_op_vec_opr_vec 2)
                                (va_op_vec_opr_vec 4))
                            (va_pbool_and (va_codegen_success_Vspltw (va_op_vec_opr_vec 2)
                                    (va_op_vec_opr_vec 2)
                                    3)
                                (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 4)
                                        (va_op_vec_opr_vec 0)
                                        (va_op_vec_opr_vec 1)
                                        12)
                                    (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec 1)
                                            (va_op_vec_opr_vec 1)
                                            (va_op_vec_opr_vec 4))
                                        (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 4
                                                  )
                                                (va_op_vec_opr_vec 0)
                                                (va_op_vec_opr_vec 1)
                                                12)
                                            (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec
                                                        1)
                                                    (va_op_vec_opr_vec 1)
                                                    (va_op_vec_opr_vec 4))
                                                (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec
                                                            4)
                                                        (va_op_vec_opr_vec 0)
                                                        (va_op_vec_opr_vec 1)
                                                        12)
                                                    (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec
                                                                1)
                                                            (va_op_vec_opr_vec 1)
                                                            (va_op_vec_opr_vec 4))
                                                        (va_pbool_and (va_codegen_success_Vxor (va_op_vec_opr_vec
                                                                    1)
                                                                (va_op_vec_opr_vec 1)
                                                                (va_op_vec_opr_vec 2))
                                                            (va_pbool_and (va_codegen_success_LoadImm64
                                                                    (va_op_reg_opr_reg 10)
                                                                    (16 `op_Multiply` (round + 1)))
                                                                (va_pbool_and (va_codegen_success_Store128_byte16_buffer_index
                                                                        (va_op_heaplet_mem_heaplet 1
                                                                        )
                                                                        (va_op_vec_opr_vec 1)
                                                                        (va_op_reg_opr_reg 3)
                                                                        (va_op_reg_opr_reg 10)
                                                                        Secret)
                                                                    (va_ttrue ()))))))))))))))))))
Vale.AES.PPC64LE.AES256.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.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.AES256.fst
Vale.PPC64LE.Memory.nat8 Vale.PPC64LE.Decls.va_pbool_and Vale.PPC64LE.InsVector.va_codegen_success_Vspltisw Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.PPC64LE.InsVector.va_codegen_success_Vsbox Vale.PPC64LE.InsBasic.va_codegen_success_LoadImmShl64 Vale.PPC64LE.Decls.va_op_reg_opr_reg Vale.PPC64LE.InsVector.va_codegen_success_Mtvsrws Vale.PPC64LE.InsVector.va_codegen_success_Vxor Vale.PPC64LE.InsVector.va_codegen_success_RotWord Vale.PPC64LE.InsVector.va_codegen_success_Vspltw Vale.PPC64LE.InsVector.va_codegen_success_Vsldoi Vale.PPC64LE.InsBasic.va_codegen_success_LoadImm64 Prims.op_Multiply Prims.op_Addition Vale.PPC64LE.InsVector.va_codegen_success_Store128_byte16_buffer_index Vale.PPC64LE.Decls.va_op_heaplet_mem_heaplet Vale.Arch.HeapTypes_s.Secret Vale.PPC64LE.Decls.va_ttrue Vale.PPC64LE.Decls.va_pbool
module Vale.AES.PPC64LE.AES256
open Vale.Def.Opaque_s
open Vale.Def.Types_s
open FStar.Seq
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.AES.AES256_helpers_BE
#reset-options "--z3rlimit 20"
//-- KeyExpansionRoundEven256

val va_code_KeyExpansionRoundEven256 : round:nat8 -> rcon:nat8 -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_KeyExpansionRoundEven256 round rcon =
  (va_Block (va_CCons (va_code_Vspltisw (va_op_vec_opr_vec 0) 0) (va_CCons (va_code_Vspltisw
    (va_op_vec_opr_vec 4) 8) (va_CCons (va_code_Vsbox (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3))
    (va_CCons (va_code_LoadImmShl64 (va_op_reg_opr_reg 10) rcon) (va_CCons (va_code_Mtvsrws
    (va_op_vec_opr_vec 5) (va_op_reg_opr_reg 10)) (va_CCons (va_code_Vxor (va_op_vec_opr_vec 2)
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 5)) (va_CCons (va_code_RotWord (va_op_vec_opr_vec 2)
    (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 4)) (va_CCons (va_code_Vspltw (va_op_vec_opr_vec 2)
    (va_op_vec_opr_vec 2) 3) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 0)
    (va_op_vec_opr_vec 1) 12) (va_CCons (va_code_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 4)) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 0)
    (va_op_vec_opr_vec 1) 12) (va_CCons (va_code_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 4)) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 0)
    (va_op_vec_opr_vec 1) 12) (va_CCons (va_code_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 4)) (va_CCons (va_code_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 2)) (va_CCons (va_code_LoadImm64 (va_op_reg_opr_reg 10) (16 `op_Multiply`
    (round + 1))) (va_CCons (va_code_Store128_byte16_buffer_index (va_op_heaplet_mem_heaplet 1)
    (va_op_vec_opr_vec 1) (va_op_reg_opr_reg 3) (va_op_reg_opr_reg 10) Secret) (va_CNil
    ())))))))))))))))))))

val va_codegen_success_KeyExpansionRoundEven256 : round:nat8 -> rcon:nat8 -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
val va_codegen_success_KeyExpansionRoundEven256 : round:nat8 -> rcon:nat8 -> Tot va_pbool
round: Vale.PPC64LE.Memory.nat8 -> rcon: Vale.PPC64LE.Memory.nat8 -> Vale.PPC64LE.Decls.va_pbool