val va_qcode_KeyExpansionRoundEven256
      (va_mods: va_mods_t)
      (round rcon: nat8)
      (dst: buffer128)
      (key: (seq nat32))
    : (va_quickCode unit (va_code_KeyExpansionRoundEven256 round rcon))
let va_qcode_KeyExpansionRoundEven256 (va_mods:va_mods_t) (round:nat8) (rcon:nat8) (dst:buffer128)
  (key:(seq nat32)) : (va_quickCode unit (va_code_KeyExpansionRoundEven256 round rcon)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 67 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vspltisw (va_op_vec_opr_vec 0) 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 68 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vspltisw (va_op_vec_opr_vec 4) 8) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 69 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vsbox (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 70 column 17 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_LoadImmShl64 (va_op_reg_opr_reg 10) rcon) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 71 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Mtvsrws (va_op_vec_opr_vec 5) (va_op_reg_opr_reg 10)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 72 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 5)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 73 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_RotWord (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 4)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 74 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vspltw (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 75 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 1) 12) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 76 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 4)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 77 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 1) 12) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 78 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 4)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 79 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 4) (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 1) 12) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 80 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 4)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 81 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 2)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 82 column 14 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_LoadImm64 (va_op_reg_opr_reg 10) (16 `op_Multiply` (round + 1))) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 83 column 33 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (va_quick_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 dst (round + 1)) (fun (va_s:va_state) _ ->
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 85 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (fun (_:unit) -> Vale.Def.Types_s.quad32_xor_reveal ()) (let (va_arg27:Vale.Def.Types_s.nat8) =
    rcon in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 86 column 19 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_BE_s.lemma_shl_rcon va_arg27) (let (va_arg26:Prims.int) = round +
    1 in let (va_arg25:Vale.Def.Types_s.nat32) = rcon in let (va_arg24:Vale.Def.Types_s.quad32) =
    va_get_vec 3 va_old_s in let (va_arg23:Vale.Def.Types_s.quad32) = va_get_vec 1 va_old_s in
    va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 87 column 25 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (fun (_:unit) -> Vale.AES.AES256_helpers_BE.lemma_simd_round_key va_arg23 va_arg24 va_arg25
    va_arg26) (va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 88 column 26 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
    (fun (_:unit) -> Vale.AES.AES256_helpers_BE.expand_key_256_reveal ()) (va_QEmpty
    (()))))))))))))))))))))))))
val va_qcode_KeyExpansionRoundEven256
      (va_mods: va_mods_t)
      (round rcon: nat8)
      (dst: buffer128)
      (key: (seq nat32))
    : (va_quickCode unit (va_code_KeyExpansionRoundEven256 round rcon))
let va_qcode_KeyExpansionRoundEven256
      (va_mods: va_mods_t)
      (round rcon: nat8)
      (dst: buffer128)
      (key: (seq nat32))
    : (va_quickCode unit (va_code_KeyExpansionRoundEven256 round rcon)) =
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        va_QSeq va_range1
          "***** PRECONDITION NOT MET AT line 67 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
          (va_quick_Vspltisw (va_op_vec_opr_vec 0) 0)
          (va_QSeq va_range1
              "***** PRECONDITION NOT MET AT line 68 column 13 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
              (va_quick_Vspltisw (va_op_vec_opr_vec 4) 8)
              (va_QSeq va_range1
                  "***** PRECONDITION NOT MET AT line 69 column 10 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                  (va_quick_Vsbox (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 3))
                  (va_QSeq va_range1
                      "***** PRECONDITION NOT MET AT line 70 column 17 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                      (va_quick_LoadImmShl64 (va_op_reg_opr_reg 10) rcon)
                      (va_QSeq va_range1
                          "***** PRECONDITION NOT MET AT line 71 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                          (va_quick_Mtvsrws (va_op_vec_opr_vec 5) (va_op_reg_opr_reg 10))
                          (va_QSeq va_range1
                              "***** PRECONDITION NOT MET AT line 72 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                              (va_quick_Vxor (va_op_vec_opr_vec 2)
                                  (va_op_vec_opr_vec 2)
                                  (va_op_vec_opr_vec 5))
                              (va_QSeq va_range1
                                  "***** PRECONDITION NOT MET AT line 73 column 12 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                  (va_quick_RotWord (va_op_vec_opr_vec 2)
                                      (va_op_vec_opr_vec 2)
                                      (va_op_vec_opr_vec 4))
                                  (va_QSeq va_range1
                                      "***** PRECONDITION NOT MET AT line 74 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                      (va_quick_Vspltw (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 2) 3
                                      )
                                      (va_QSeq va_range1
                                          "***** PRECONDITION NOT MET AT line 75 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                          (va_quick_Vsldoi (va_op_vec_opr_vec 4)
                                              (va_op_vec_opr_vec 0)
                                              (va_op_vec_opr_vec 1)
                                              12)
                                          (va_QSeq va_range1
                                              "***** PRECONDITION NOT MET AT line 76 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                              (va_quick_Vxor (va_op_vec_opr_vec 1)
                                                  (va_op_vec_opr_vec 1)
                                                  (va_op_vec_opr_vec 4))
                                              (va_QSeq va_range1
                                                  "***** PRECONDITION NOT MET AT line 77 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                  (va_quick_Vsldoi (va_op_vec_opr_vec 4)
                                                      (va_op_vec_opr_vec 0)
                                                      (va_op_vec_opr_vec 1)
                                                      12)
                                                  (va_QSeq va_range1
                                                      "***** PRECONDITION NOT MET AT line 78 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                      (va_quick_Vxor (va_op_vec_opr_vec 1)
                                                          (va_op_vec_opr_vec 1)
                                                          (va_op_vec_opr_vec 4))
                                                      (va_QSeq va_range1
                                                          "***** PRECONDITION NOT MET AT line 79 column 11 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                          (va_quick_Vsldoi (va_op_vec_opr_vec 4)
                                                              (va_op_vec_opr_vec 0)
                                                              (va_op_vec_opr_vec 1)
                                                              12)
                                                          (va_QSeq va_range1
                                                              "***** PRECONDITION NOT MET AT line 80 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                              (va_quick_Vxor (va_op_vec_opr_vec 1)
                                                                  (va_op_vec_opr_vec 1)
                                                                  (va_op_vec_opr_vec 4))
                                                              (va_QSeq va_range1
                                                                  "***** PRECONDITION NOT MET AT line 81 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                                  (va_quick_Vxor (va_op_vec_opr_vec 1
                                                                        )
                                                                      (va_op_vec_opr_vec 1)
                                                                      (va_op_vec_opr_vec 2))
                                                                  (va_QSeq va_range1
                                                                      "***** PRECONDITION NOT MET AT line 82 column 14 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                                      (va_quick_LoadImm64 (va_op_reg_opr_reg
                                                                              10)
                                                                          (16
                                                                            `op_Multiply`
                                                                            (round + 1)))
                                                                      (va_QBind va_range1
                                                                          "***** PRECONDITION NOT MET AT line 83 column 33 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                                          (va_quick_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
                                                                              dst
                                                                              (round + 1))
                                                                          (fun (va_s: va_state) _ ->
                                                                              va_qPURE va_range1
                                                                                "***** PRECONDITION NOT MET AT line 85 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                                                (fun (_: unit) ->
                                                                                    Vale.Def.Types_s.quad32_xor_reveal
                                                                                      ())
                                                                                (let va_arg27:Vale.Def.Types_s.nat8
                                                                                  =
                                                                                    rcon
                                                                                  in
                                                                                  va_qPURE va_range1
                                                                                    "***** PRECONDITION NOT MET AT line 86 column 19 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                                                    (fun
                                                                                        (_: unit)
                                                                                        ->
                                                                                        Vale.AES.AES_BE_s.lemma_shl_rcon
                                                                                          va_arg27)
                                                                                    (let va_arg26:Prims.int
                                                                                      =
                                                                                        round + 1
                                                                                      in
                                                                                      let va_arg25:Vale.Def.Types_s.nat32
                                                                                      =
                                                                                        rcon
                                                                                      in
                                                                                      let va_arg24:Vale.Def.Types_s.quad32
                                                                                      =
                                                                                        va_get_vec 3
                                                                                          va_old_s
                                                                                      in
                                                                                      let va_arg23:Vale.Def.Types_s.quad32
                                                                                      =
                                                                                        va_get_vec 1
                                                                                          va_old_s
                                                                                      in
                                                                                      va_qPURE va_range1
                                                                                        "***** PRECONDITION NOT MET AT line 87 column 25 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                                                        (fun
                                                                                            (_:
                                                                                              unit)
                                                                                            ->
                                                                                            Vale.AES.AES256_helpers_BE.lemma_simd_round_key
                                                                                              va_arg23
                                                                                              va_arg24
                                                                                              va_arg25
                                                                                              va_arg26
                                                                                            )
                                                                                        (va_qPURE va_range1
                                                                                            "***** PRECONDITION NOT MET AT line 88 column 26 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.AES256.vaf *****"
                                                                                            (fun
                                                                                                (_:
                                                                                                  unit
                                                                                                )
                                                                                                ->
                                                                                                Vale.AES.AES256_helpers_BE.expand_key_256_reveal
                                                                                                  ()
                                                                                            )
                                                                                            (va_QEmpty
                                                                                                (())
                                                                                            ))))))))
                                                          )))))))))))))))
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.QuickCode.va_mods_t Vale.PPC64LE.Memory.nat8 Vale.PPC64LE.Memory.buffer128 FStar.Seq.Base.seq Vale.PPC64LE.Memory.nat32 Vale.PPC64LE.QuickCodes.qblock Prims.unit Prims.Cons Vale.PPC64LE.Decls.va_code Vale.PPC64LE.InsVector.va_code_Vspltisw Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.PPC64LE.InsVector.va_code_Vsbox Vale.PPC64LE.InsBasic.va_code_LoadImmShl64 Vale.PPC64LE.Decls.va_op_reg_opr_reg Vale.PPC64LE.InsVector.va_code_Mtvsrws Vale.PPC64LE.InsVector.va_code_Vxor Vale.PPC64LE.InsVector.va_code_RotWord Vale.PPC64LE.InsVector.va_code_Vspltw Vale.PPC64LE.InsVector.va_code_Vsldoi Vale.PPC64LE.InsBasic.va_code_LoadImm64 Prims.op_Multiply Prims.op_Addition Vale.PPC64LE.InsVector.va_code_Store128_byte16_buffer_index Vale.PPC64LE.Decls.va_op_heaplet_mem_heaplet Vale.Arch.HeapTypes_s.Secret Prims.Nil Vale.PPC64LE.Machine_s.precode Vale.PPC64LE.Decls.ins Vale.PPC64LE.Decls.ocmp Vale.PPC64LE.Decls.va_state Vale.PPC64LE.QuickCodes.va_QSeq Vale.PPC64LE.QuickCodes.va_range1 Vale.PPC64LE.InsVector.va_quick_Vspltisw Vale.PPC64LE.InsVector.va_quick_Vsbox Vale.PPC64LE.InsBasic.va_quick_LoadImmShl64 Vale.PPC64LE.InsVector.va_quick_Mtvsrws Vale.PPC64LE.InsVector.va_quick_Vxor Vale.PPC64LE.InsVector.va_quick_RotWord Vale.PPC64LE.InsVector.va_quick_Vspltw Vale.PPC64LE.InsVector.va_quick_Vsldoi Vale.PPC64LE.InsBasic.va_quick_LoadImm64 Vale.PPC64LE.QuickCodes.va_QBind Vale.PPC64LE.InsVector.va_quick_Store128_byte16_buffer_index Vale.PPC64LE.QuickCodes.va_qPURE Prims.pure_post Prims.l_and Prims.l_True Prims.l_Forall Prims.l_imp Prims.eq2 Vale.Def.Types_s.quad32 Vale.Def.Types_s.quad32_xor Vale.Def.Types_s.quad32_xor_def Vale.Def.Types_s.quad32_xor_reveal Prims.int Vale.Def.Types_s.ishl Prims.op_Modulus Vale.AES.AES_BE_s.lemma_shl_rcon Vale.AES.AES256_helpers_BE.simd_round_key_256 Vale.AES.AES256_helpers_BE.round_key_256_rcon Vale.AES.AES256_helpers_BE.lemma_simd_round_key Vale.Def.Words_s.nat32 Prims.nat Vale.AES.AES_BE_s.is_aes_key_word Vale.AES.AES_common_s.AES_256 Vale.AES.AES256_helpers_BE.expand_key_256 Vale.AES.AES256_helpers_BE.expand_key_256_def Vale.AES.AES256_helpers_BE.expand_key_256_reveal Vale.PPC64LE.QuickCodes.va_QEmpty Vale.PPC64LE.Decls.va_get_vec Vale.Def.Words_s.nat8 Vale.PPC64LE.QuickCodes.quickCodes Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCode.va_quickCode Vale.AES.PPC64LE.AES256.va_code_KeyExpansionRoundEven256
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]
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
    ()))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_KeyExpansionRoundEven256 (va_mods:va_mods_t) (round:nat8) (rcon:nat8) (dst:buffer128)
val va_qcode_KeyExpansionRoundEven256
      (va_mods: va_mods_t)
      (round rcon: nat8)
      (dst: buffer128)
      (key: (seq nat32))
    : (va_quickCode unit (va_code_KeyExpansionRoundEven256 round rcon))

    va_mods: Vale.PPC64LE.QuickCode.va_mods_t ->
    round: Vale.PPC64LE.Memory.nat8 ->
    rcon: Vale.PPC64LE.Memory.nat8 ->
    dst: Vale.PPC64LE.Memory.buffer128 ->
    key: FStar.Seq.Base.seq Vale.PPC64LE.Memory.nat32
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit
      (Vale.AES.PPC64LE.AES256.va_code_KeyExpansionRoundEven256 round rcon)