val va_qcode_Gctr_register
      (va_mods: va_mods_t)
      (alg: algorithm)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b: buffer128)
    : (va_quickCode unit (va_code_Gctr_register alg))
let va_qcode_Gctr_register (va_mods:va_mods_t) (alg:algorithm) (key:(seq nat32)) (round_keys:(seq
  quad32)) (keys_b:buffer128) : (va_quickCode unit (va_code_Gctr_register alg)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 99 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (Vale.AES.GCTR_BE_s.inc32 (va_get_vec 7 va_s) 0 == va_get_vec 7 va_s) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 100 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_quick_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 7)) (fun (va_s:va_state) _ -> va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 101 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_quick_AESEncryptBlock alg (va_get_vec 7 va_s) key round_keys keys_b) (fun (va_s:va_state) _
    -> va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 102 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    ((fun (alg_10536:Vale.AES.AES_common_s.algorithm) (key_10537:(FStar.Seq.Base.seq
    Vale.Def.Types_s.nat32)) (input_10538:Vale.Def.Types_s.quad32) ->
    Vale.AES.AES_BE_s.is_aes_key_word alg_10536 key_10537) alg key (va_get_vec 7 va_s)) (fun _ ->
    va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 102 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_get_vec 0 va_s == Vale.AES.AES_BE_s.aes_encrypt_word alg key (va_get_vec 7 va_s)) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 104 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 0)) (fun
    (va_s:va_state) _ -> let (va_arg15:(FStar.Seq.Base.seq Vale.Def.Types_s.nat32)) = key in let
    (va_arg14:Vale.AES.AES_common_s.algorithm) = alg in let (va_arg13:Vale.Def.Types_s.quad32) =
    va_get_vec 1 va_old_s in let (va_arg12:Vale.Def.Types_s.quad32) = va_get_vec 7 va_s in va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 107 column 27 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.GCTR_BE.gctr_encrypt_one_block va_arg12 va_arg13 va_arg14 va_arg15)
    (va_QEmpty (()))))))))))
val va_qcode_Gctr_register
      (va_mods: va_mods_t)
      (alg: algorithm)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b: buffer128)
    : (va_quickCode unit (va_code_Gctr_register alg))
let va_qcode_Gctr_register
      (va_mods: va_mods_t)
      (alg: algorithm)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b: buffer128)
    : (va_quickCode unit (va_code_Gctr_register alg)) =
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        va_qAssert va_range1
          "***** PRECONDITION NOT MET AT line 99 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
          (Vale.AES.GCTR_BE_s.inc32 (va_get_vec 7 va_s) 0 == va_get_vec 7 va_s)
          (va_QBind va_range1
              "***** PRECONDITION NOT MET AT line 100 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
              (va_quick_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 7))
              (fun (va_s: va_state) _ ->
                  va_QBind va_range1
                    "***** PRECONDITION NOT MET AT line 101 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
                    (va_quick_AESEncryptBlock alg (va_get_vec 7 va_s) key round_keys keys_b)
                    (fun (va_s: va_state) _ ->
                        va_qAssertSquash va_range1
                          "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 102 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
                          ((fun
                                (alg_10536: Vale.AES.AES_common_s.algorithm)
                                (key_10537: (FStar.Seq.Base.seq Vale.Def.Types_s.nat32))
                                (input_10538: Vale.Def.Types_s.quad32)
                                ->
                                Vale.AES.AES_BE_s.is_aes_key_word alg_10536 key_10537) alg
                              key
                              (va_get_vec 7 va_s))
                          (fun _ ->
                              va_qAssert va_range1
                                "***** PRECONDITION NOT MET AT line 102 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
                                (va_get_vec 0 va_s ==
                                  Vale.AES.AES_BE_s.aes_encrypt_word alg key (va_get_vec 7 va_s))
                                (va_QBind va_range1
                                    "***** PRECONDITION NOT MET AT line 104 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
                                    (va_quick_Vxor (va_op_vec_opr_vec 1)
                                        (va_op_vec_opr_vec 1)
                                        (va_op_vec_opr_vec 0))
                                    (fun (va_s: va_state) _ ->
                                        let va_arg15:(FStar.Seq.Base.seq Vale.Def.Types_s.nat32) =
                                          key
                                        in
                                        let va_arg14:Vale.AES.AES_common_s.algorithm = alg in
                                        let va_arg13:Vale.Def.Types_s.quad32 =
                                          va_get_vec 1 va_old_s
                                        in
                                        let va_arg12:Vale.Def.Types_s.quad32 = va_get_vec 7 va_s in
                                        va_qPURE va_range1
                                          "***** PRECONDITION NOT MET AT line 107 column 27 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
                                          (fun (_: unit) ->
                                              Vale.AES.GCTR_BE.gctr_encrypt_one_block va_arg12
                                                va_arg13
                                                va_arg14
                                                va_arg15)
                                          (va_QEmpty (()))))))))))
Vale.AES.PPC64LE.GCTR.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.InsStack.fsti.checked Vale.PPC64LE.InsMem.fsti.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fsti.checked Vale.Poly1305.Math.fsti.checked Vale.Lib.Basic.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.AES.Types_helpers.fsti.checked Vale.AES.PPC64LE.AES.fsti.checked Vale.AES.GCTR_BE_s.fst.checked Vale.AES.GCTR_BE.fsti.checked Vale.AES.GCM_helpers_BE.fsti.checked Vale.AES.AES_common_s.fst.checked Vale.AES.AES_BE_s.fst.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.GCTR.fst
Vale.PPC64LE.QuickCode.va_mods_t Vale.AES.AES_common_s.algorithm FStar.Seq.Base.seq Vale.PPC64LE.Memory.nat32 Vale.PPC64LE.Memory.quad32 Vale.PPC64LE.Memory.buffer128 Vale.PPC64LE.QuickCodes.qblock Prims.unit Prims.Cons Vale.PPC64LE.Decls.va_code Vale.PPC64LE.InsVector.va_code_Vmr Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.AES.PPC64LE.AES.va_code_AESEncryptBlock Vale.PPC64LE.Machine_s.Block Vale.PPC64LE.Decls.ins Vale.PPC64LE.Decls.ocmp Prims.Nil Vale.PPC64LE.Machine_s.precode Vale.PPC64LE.InsVector.va_code_Vxor Vale.PPC64LE.Decls.va_state Vale.PPC64LE.QuickCodes.va_qAssert Vale.PPC64LE.QuickCodes.va_range1 Prims.eq2 Vale.Def.Types_s.quad32 Vale.AES.GCTR_BE_s.inc32 Vale.PPC64LE.Decls.va_get_vec Vale.PPC64LE.QuickCodes.va_QBind Vale.PPC64LE.InsVector.va_quick_Vmr Vale.AES.PPC64LE.AES.va_quick_AESEncryptBlock Vale.PPC64LE.QuickCodes.va_qAssertSquash Vale.AES.AES_BE_s.is_aes_key_word Prims.squash Vale.AES.AES_BE_s.aes_encrypt_word Vale.PPC64LE.InsVector.va_quick_Vxor Vale.PPC64LE.QuickCodes.va_qPURE Prims.pure_post Prims.l_and Prims.l_Forall Prims.l_imp Vale.Def.Words_s.nat8 Vale.AES.GCTR_BE_s.gctr_encrypt Vale.Arch.Types.be_quad32_to_bytes Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_BE Vale.Def.Words.Seq_s.seq_four_to_seq_BE Vale.Def.Words_s.nat32 FStar.Seq.Base.create Vale.Def.Words_s.four Vale.Def.Types_s.quad32_xor Vale.AES.GCTR_BE.gctr_encrypt_one_block Vale.PPC64LE.QuickCodes.va_QEmpty Vale.PPC64LE.QuickCodes.quickCodes Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCode.va_quickCode Vale.AES.PPC64LE.GCTR.va_code_Gctr_register
module Vale.AES.PPC64LE.GCTR
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open FStar.Seq
open Vale.AES.AES_BE_s
open Vale.AES.PPC64LE.AES
open Vale.AES.GCTR_BE_s
open Vale.AES.GCTR_BE
open Vale.AES.GCM_helpers_BE
open Vale.Poly1305.Math
open Vale.Def.Words.Two_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.InsStack
open Vale.PPC64LE.QuickCode
open Vale.PPC64LE.QuickCodes
open Vale.AES.Types_helpers
#reset-options "--z3rlimit 30"
open Vale.Lib.Basic
#reset-options "--z3rlimit 20"
//-- Gctr_register

[@ "opaque_to_smt" va_qattr]
let va_code_Gctr_register alg =
  (va_Block (va_CCons (va_code_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 7)) (va_CCons
    (va_code_AESEncryptBlock alg) (va_CCons (va_Block (va_CNil ())) (va_CCons (va_code_Vxor
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 0)) (va_CNil ()))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Gctr_register alg =
  (va_pbool_and (va_codegen_success_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 7)) (va_pbool_and
    (va_codegen_success_AESEncryptBlock alg) (va_pbool_and (va_codegen_success_Vxor
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 0)) (va_ttrue ()))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Gctr_register (va_mods:va_mods_t) (alg:algorithm) (key:(seq nat32)) (round_keys:(seq
val va_qcode_Gctr_register
      (va_mods: va_mods_t)
      (alg: algorithm)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b: buffer128)
    : (va_quickCode unit (va_code_Gctr_register alg))

    va_mods: Vale.PPC64LE.QuickCode.va_mods_t ->
    alg: Vale.AES.AES_common_s.algorithm ->
    key: FStar.Seq.Base.seq Vale.PPC64LE.Memory.nat32 ->
    round_keys: FStar.Seq.Base.seq Vale.PPC64LE.Memory.quad32 ->
    keys_b: Vale.PPC64LE.Memory.buffer128
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit
      (Vale.AES.PPC64LE.GCTR.va_code_Gctr_register alg)