val va_qcode_Gcm_extra_bytes
      (va_mods: va_mods_t)
      (alg: algorithm)
      (inout_b: buffer128)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b hkeys_b: buffer128)
      (total_bytes: nat)
      (old_hash: quad32)
      (completed_quads: (seq quad32))
      (h_BE: quad32)
    : (va_quickCode unit (va_code_Gcm_extra_bytes alg))
let va_qcode_Gcm_extra_bytes (va_mods:va_mods_t) (alg:algorithm) (inout_b:buffer128) (key:(seq
  nat32)) (round_keys:(seq quad32)) (keys_b:buffer128) (hkeys_b:buffer128) (total_bytes:nat)
  (old_hash:quad32) (completed_quads:(seq quad32)) (h_BE:quad32) : (va_quickCode unit
  (va_code_Gcm_extra_bytes alg)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let (len:(va_int_range
    1 1)) = 1 in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 164 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (va_quick_Vmr (va_op_vec_opr_vec 11) (va_op_vec_opr_vec 7)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 165 column 26 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (va_quick_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 5) (va_op_vec_opr_vec 9)
    (va_op_reg_opr_reg 3) Secret inout_b 0) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 166 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (va_quick_Vmr (va_op_vec_opr_vec 12) (va_op_vec_opr_vec 9)) (fun (va_s:va_state) _ -> let
    (hash_input:quad32) = va_get_vec 9 va_s in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 170 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (va_quick_Ghash_extra_bytes hkeys_b total_bytes old_hash h_BE completed_quads) (fun
    (va_s:va_state) _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 171 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (FStar.Seq.Base.equal #Vale.Def.Types_s.quad32 (Vale.Arch.Types.reverse_bytes_quad32_seq
    (Vale.PPC64LE.Decls.s128 (va_get_mem_heaplet 5 va_s) inout_b)) (FStar.Seq.Base.create #quad32 1
    hash_input)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 173 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (va_quick_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 11)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 174 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (va_quick_AESEncryptBlock alg (va_get_vec 7 va_old_s) key round_keys keys_b) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 176 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 12) (va_op_vec_opr_vec 12) (va_op_vec_opr_vec 0)) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 177 column 27 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (va_quick_Store128_byte16_buffer (va_op_heaplet_mem_heaplet 5) (va_op_vec_opr_vec 12)
    (va_op_reg_opr_reg 3) Secret inout_b 0) (fun (va_s:va_state) _ -> va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 179 column 24 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
    (fun (_:unit) -> Vale.AES.GCTR_BE.gctr_partial_reveal ()) (va_QEmpty (())))))))))))))
val va_qcode_Gcm_extra_bytes
      (va_mods: va_mods_t)
      (alg: algorithm)
      (inout_b: buffer128)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b hkeys_b: buffer128)
      (total_bytes: nat)
      (old_hash: quad32)
      (completed_quads: (seq quad32))
      (h_BE: quad32)
    : (va_quickCode unit (va_code_Gcm_extra_bytes alg))
let va_qcode_Gcm_extra_bytes
      (va_mods: va_mods_t)
      (alg: algorithm)
      (inout_b: buffer128)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b hkeys_b: buffer128)
      (total_bytes: nat)
      (old_hash: quad32)
      (completed_quads: (seq quad32))
      (h_BE: quad32)
    : (va_quickCode unit (va_code_Gcm_extra_bytes alg)) =
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        let len:(va_int_range 1 1) = 1 in
        va_QSeq va_range1
          "***** PRECONDITION NOT MET AT line 164 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
          (va_quick_Vmr (va_op_vec_opr_vec 11) (va_op_vec_opr_vec 7))
          (va_QSeq va_range1
              "***** PRECONDITION NOT MET AT line 165 column 26 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
              (va_quick_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 5)
                  (va_op_vec_opr_vec 9)
                  (va_op_reg_opr_reg 3)
                  Secret
                  inout_b
                  0)
              (va_QBind va_range1
                  "***** PRECONDITION NOT MET AT line 166 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
                  (va_quick_Vmr (va_op_vec_opr_vec 12) (va_op_vec_opr_vec 9))
                  (fun (va_s: va_state) _ ->
                      let hash_input:quad32 = va_get_vec 9 va_s in
                      va_QBind va_range1
                        "***** PRECONDITION NOT MET AT line 170 column 22 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
                        (va_quick_Ghash_extra_bytes hkeys_b
                            total_bytes
                            old_hash
                            h_BE
                            completed_quads)
                        (fun (va_s: va_state) _ ->
                            va_qAssert va_range1
                              "***** PRECONDITION NOT MET AT line 171 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
                              (FStar.Seq.Base.equal #Vale.Def.Types_s.quad32
                                  (Vale.Arch.Types.reverse_bytes_quad32_seq (Vale.PPC64LE.Decls.s128
                                          (va_get_mem_heaplet 5 va_s)
                                          inout_b))
                                  (FStar.Seq.Base.create #quad32 1 hash_input))
                              (va_QSeq va_range1
                                  "***** PRECONDITION NOT MET AT line 173 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
                                  (va_quick_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 11))
                                  (va_QSeq va_range1
                                      "***** PRECONDITION NOT MET AT line 174 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
                                      (va_quick_AESEncryptBlock alg
                                          (va_get_vec 7 va_old_s)
                                          key
                                          round_keys
                                          keys_b)
                                      (va_QSeq va_range1
                                          "***** PRECONDITION NOT MET AT line 176 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
                                          (va_quick_Vxor (va_op_vec_opr_vec 12)
                                              (va_op_vec_opr_vec 12)
                                              (va_op_vec_opr_vec 0))
                                          (va_QBind va_range1
                                              "***** PRECONDITION NOT MET AT line 177 column 27 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
                                              (va_quick_Store128_byte16_buffer (va_op_heaplet_mem_heaplet
                                                      5)
                                                  (va_op_vec_opr_vec 12)
                                                  (va_op_reg_opr_reg 3)
                                                  Secret
                                                  inout_b
                                                  0)
                                              (fun (va_s: va_state) _ ->
                                                  va_qPURE va_range1
                                                    "***** PRECONDITION NOT MET AT line 179 column 24 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCMdecrypt.vaf *****"
                                                    (fun (_: unit) ->
                                                        Vale.AES.GCTR_BE.gctr_partial_reveal ())
                                                    (va_QEmpty (())))))))))))))
Vale.AES.PPC64LE.GCMdecrypt.fst.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Stack_i.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.Math.Poly2.Bits_s.fsti.checked Vale.Lib.Meta.fsti.checked Vale.Lib.Basic.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_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.GHash.fsti.checked Vale.AES.PPC64LE.GF128_Mul.fsti.checked Vale.AES.PPC64LE.GCTR.fsti.checked Vale.AES.PPC64LE.GCMencrypt.fsti.checked Vale.AES.PPC64LE.AES.fsti.checked Vale.AES.GHash_BE_s.fst.checked Vale.AES.GHash_BE.fsti.checked Vale.AES.GF128_s.fsti.checked Vale.AES.GF128.fsti.checked Vale.AES.GCTR_BE_s.fst.checked Vale.AES.GCTR_BE.fsti.checked Vale.AES.GCM_helpers_BE.fsti.checked Vale.AES.GCM_BE_s.fst.checked Vale.AES.GCM_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.GCMdecrypt.fst
Vale.PPC64LE.QuickCode.va_mods_t Vale.AES.AES_common_s.algorithm Vale.PPC64LE.Memory.buffer128 FStar.Seq.Base.seq Vale.PPC64LE.Memory.nat32 Vale.PPC64LE.Memory.quad32 Prims.nat 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.PPC64LE.InsVector.va_code_Load128_byte16_buffer Vale.PPC64LE.Decls.va_op_heaplet_mem_heaplet Vale.PPC64LE.Decls.va_op_reg_opr_reg Vale.Arch.HeapTypes_s.Secret Vale.AES.PPC64LE.GCMencrypt.va_code_Ghash_extra_bytes Vale.AES.PPC64LE.AES.va_code_AESEncryptBlock Vale.PPC64LE.InsVector.va_code_Vxor Vale.PPC64LE.InsVector.va_code_Store128_byte16_buffer 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_Vmr Vale.PPC64LE.InsVector.va_quick_Load128_byte16_buffer Vale.PPC64LE.QuickCodes.va_QBind Vale.AES.PPC64LE.GCMencrypt.va_quick_Ghash_extra_bytes Vale.PPC64LE.QuickCodes.va_qAssert FStar.Seq.Base.equal Vale.Def.Types_s.quad32 Vale.Arch.Types.reverse_bytes_quad32_seq Vale.PPC64LE.Decls.s128 Vale.PPC64LE.Decls.va_get_mem_heaplet FStar.Seq.Base.create Vale.AES.PPC64LE.AES.va_quick_AESEncryptBlock Vale.PPC64LE.Decls.va_get_vec Vale.PPC64LE.InsVector.va_quick_Vxor Vale.PPC64LE.InsVector.va_quick_Store128_byte16_buffer Vale.PPC64LE.QuickCodes.va_qPURE Prims.pure_post Prims.l_and Prims.l_True Prims.l_Forall Prims.l_imp Prims.eq2 Vale.Def.Words_s.nat32 Vale.Def.Prop_s.prop0 Vale.AES.GCTR_BE.gctr_partial Vale.AES.GCTR_BE.gctr_partial_def Vale.AES.GCTR_BE.gctr_partial_reveal Vale.PPC64LE.QuickCodes.va_QEmpty Vale.PPC64LE.QuickCodes.quickCodes Vale.PPC64LE.Decls.va_int_range Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCode.va_quickCode Vale.AES.PPC64LE.GCMdecrypt.va_code_Gcm_extra_bytes
module Vale.AES.PPC64LE.GCMdecrypt
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open FStar.Seq
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.AES.AES_BE_s
open Vale.AES.GCTR_BE_s
open Vale.AES.GCTR_BE
open Vale.AES.GCM_BE
open Vale.AES.GHash_BE_s
open Vale.AES.GHash_BE
open Vale.AES.GCM_BE_s
open Vale.AES.PPC64LE.AES
open Vale.AES.GF128_s
open Vale.AES.GF128
open Vale.Poly1305.Math
open Vale.AES.GCM_helpers_BE
open Vale.AES.PPC64LE.GHash
open Vale.AES.PPC64LE.GCTR
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.PPC64LE.Stack_i
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.PPC64LE.GF128_Mul
open Vale.Math.Poly2.Bits_s
open Vale.Lib.Meta
open Vale.AES.PPC64LE.GCMencrypt
open Vale.Lib.Basic
#reset-options "--z3rlimit 20"
//-- Gcm_extra_bytes

val va_code_Gcm_extra_bytes : alg:algorithm -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Gcm_extra_bytes alg =
  (va_Block (va_CCons (va_code_Vmr (va_op_vec_opr_vec 11) (va_op_vec_opr_vec 7)) (va_CCons
    (va_code_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 5) (va_op_vec_opr_vec 9)
    (va_op_reg_opr_reg 3) Secret) (va_CCons (va_code_Vmr (va_op_vec_opr_vec 12) (va_op_vec_opr_vec
    9)) (va_CCons (va_code_Ghash_extra_bytes ()) (va_CCons (va_code_Vmr (va_op_vec_opr_vec 0)
    (va_op_vec_opr_vec 11)) (va_CCons (va_code_AESEncryptBlock alg) (va_CCons (va_code_Vxor
    (va_op_vec_opr_vec 12) (va_op_vec_opr_vec 12) (va_op_vec_opr_vec 0)) (va_CCons
    (va_code_Store128_byte16_buffer (va_op_heaplet_mem_heaplet 5) (va_op_vec_opr_vec 12)
    (va_op_reg_opr_reg 3) Secret) (va_CNil ()))))))))))

val va_codegen_success_Gcm_extra_bytes : alg:algorithm -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Gcm_extra_bytes alg =
  (va_pbool_and (va_codegen_success_Vmr (va_op_vec_opr_vec 11) (va_op_vec_opr_vec 7)) (va_pbool_and
    (va_codegen_success_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 5) (va_op_vec_opr_vec 9)
    (va_op_reg_opr_reg 3) Secret) (va_pbool_and (va_codegen_success_Vmr (va_op_vec_opr_vec 12)
    (va_op_vec_opr_vec 9)) (va_pbool_and (va_codegen_success_Ghash_extra_bytes ()) (va_pbool_and
    (va_codegen_success_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 11)) (va_pbool_and
    (va_codegen_success_AESEncryptBlock alg) (va_pbool_and (va_codegen_success_Vxor
    (va_op_vec_opr_vec 12) (va_op_vec_opr_vec 12) (va_op_vec_opr_vec 0)) (va_pbool_and
    (va_codegen_success_Store128_byte16_buffer (va_op_heaplet_mem_heaplet 5) (va_op_vec_opr_vec 12)
    (va_op_reg_opr_reg 3) Secret) (va_ttrue ())))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Gcm_extra_bytes (va_mods:va_mods_t) (alg:algorithm) (inout_b:buffer128) (key:(seq
  nat32)) (round_keys:(seq quad32)) (keys_b:buffer128) (hkeys_b:buffer128) (total_bytes:nat)
  (old_hash:quad32) (completed_quads:(seq quad32)) (h_BE:quad32) : (va_quickCode unit
val va_qcode_Gcm_extra_bytes
      (va_mods: va_mods_t)
      (alg: algorithm)
      (inout_b: buffer128)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b hkeys_b: buffer128)
      (total_bytes: nat)
      (old_hash: quad32)
      (completed_quads: (seq quad32))
      (h_BE: quad32)
    : (va_quickCode unit (va_code_Gcm_extra_bytes alg))

    va_mods: Vale.PPC64LE.QuickCode.va_mods_t ->
    alg: Vale.AES.AES_common_s.algorithm ->
    inout_b: Vale.PPC64LE.Memory.buffer128 ->
    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 ->
    hkeys_b: Vale.PPC64LE.Memory.buffer128 ->
    total_bytes: Prims.nat ->
    old_hash: Vale.PPC64LE.Memory.quad32 ->
    completed_quads: FStar.Seq.Base.seq Vale.PPC64LE.Memory.quad32 ->
    h_BE: Vale.PPC64LE.Memory.quad32
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit
      (Vale.AES.PPC64LE.GCMdecrypt.va_code_Gcm_extra_bytes alg)