val va_qcode_Loop_prologue
      (va_mods: va_mods_t)
      (in_b: buffer128)
      (offset: nat)
      (k_b: buffer128)
      (block: block_w)
      (hash_orig: hash256)
    : (va_quickCode unit (va_code_Loop_prologue ()))
let va_qcode_Loop_prologue (va_mods:va_mods_t) (in_b:buffer128) (offset:nat) (k_b:buffer128)
  (block:block_w) (hash_orig:hash256) : (va_quickCode unit (va_code_Loop_prologue ())) =
  (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 80 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 0)
    (va_op_reg_opr_reg 4) Secret in_b offset) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 81 column 25 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 24)
    (va_op_reg_opr_reg 6) Secret k_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 82 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_AddImm (va_op_reg_opr_reg 4) (va_op_reg_opr_reg 4) 16) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 83 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_AddImm (va_op_reg_opr_reg 6) (va_op_reg_opr_reg 6) 16) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 84 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 24))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 85 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) 4)
    (va_QEmpty (())))))))))
val va_qcode_Loop_prologue
      (va_mods: va_mods_t)
      (in_b: buffer128)
      (offset: nat)
      (k_b: buffer128)
      (block: block_w)
      (hash_orig: hash256)
    : (va_quickCode unit (va_code_Loop_prologue ()))
let va_qcode_Loop_prologue
      (va_mods: va_mods_t)
      (in_b: buffer128)
      (offset: nat)
      (k_b: buffer128)
      (block: block_w)
      (hash_orig: hash256)
    : (va_quickCode unit (va_code_Loop_prologue ())) =
(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 80 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
          (va_quick_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0)
              (va_op_vec_opr_vec 0)
              (va_op_reg_opr_reg 4)
              Secret
              in_b
              offset)
          (va_QSeq va_range1
              "***** PRECONDITION NOT MET AT line 81 column 25 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
              (va_quick_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0)
                  (va_op_vec_opr_vec 24)
                  (va_op_reg_opr_reg 6)
                  Secret
                  k_b
                  0)
              (va_QSeq va_range1
                  "***** PRECONDITION NOT MET AT line 82 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
                  (va_quick_AddImm (va_op_reg_opr_reg 4) (va_op_reg_opr_reg 4) 16)
                  (va_QSeq va_range1
                      "***** PRECONDITION NOT MET AT line 83 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
                      (va_quick_AddImm (va_op_reg_opr_reg 6) (va_op_reg_opr_reg 6) 16)
                      (va_QSeq va_range1
                          "***** PRECONDITION NOT MET AT line 84 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
                          (va_quick_Vadduwm (va_op_vec_opr_vec 23)
                              (va_op_vec_opr_vec 23)
                              (va_op_vec_opr_vec 24))
                          (va_QSeq va_range1
                              "***** PRECONDITION NOT MET AT line 85 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
                              (va_quick_Vsldoi (va_op_vec_opr_vec 24)
                                  (va_op_vec_opr_vec 24)
                                  (va_op_vec_opr_vec 24)
                                  4)
                              (va_QEmpty (())))))))))
Vale.SHA.PPC64LE.Loop.fst.checked
Vale.SHA2.Wrapper.fsti.checked Vale.SHA.PPC64LE.SHA_helpers.fsti.checked Vale.SHA.PPC64LE.Rounds.fsti.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.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Spec.SHA2.fsti.checked Spec.Loops.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.SHA.PPC64LE.Loop.fst
Vale.PPC64LE.QuickCode.va_mods_t Vale.PPC64LE.Memory.buffer128 Prims.nat Vale.SHA.PPC64LE.SHA_helpers.block_w Vale.SHA.PPC64LE.SHA_helpers.hash256 Vale.PPC64LE.QuickCodes.qblock Prims.unit Prims.Cons Vale.PPC64LE.Decls.va_code Vale.PPC64LE.InsVector.va_code_Load128_byte16_buffer Vale.PPC64LE.Decls.va_op_heaplet_mem_heaplet Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.PPC64LE.Decls.va_op_reg_opr_reg Vale.Arch.HeapTypes_s.Secret Vale.PPC64LE.InsVector.va_code_Load128_word4_buffer Vale.PPC64LE.InsBasic.va_code_AddImm Vale.PPC64LE.InsVector.va_code_Vadduwm Vale.PPC64LE.InsVector.va_code_Vsldoi 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_Load128_byte16_buffer Vale.PPC64LE.InsVector.va_quick_Load128_word4_buffer Vale.PPC64LE.InsBasic.va_quick_AddImm Vale.PPC64LE.InsVector.va_quick_Vadduwm Vale.PPC64LE.InsVector.va_quick_Vsldoi Vale.PPC64LE.QuickCodes.va_QEmpty Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCodes.quickCodes Vale.PPC64LE.QuickCode.va_quickCode Vale.SHA.PPC64LE.Loop.va_code_Loop_prologue
module Vale.SHA.PPC64LE.Loop
open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open FStar.Seq
open Vale.Arch.Types
open Vale.Arch.HeapImpl
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.QuickCode
open Vale.PPC64LE.QuickCodes
open Vale.PPC64LE.InsBasic
open Vale.PPC64LE.InsMem
open Vale.PPC64LE.InsStack
open Vale.PPC64LE.InsVector
open Vale.SHA.PPC64LE.SHA_helpers
open Spec.SHA2
open Spec.Agile.Hash
open Spec.Hash.Definitions
open Spec.Loops
open Vale.SHA.PPC64LE.Rounds
open Vale.SHA2.Wrapper
#reset-options "--z3rlimit 2000"
//-- Loop_prologue

val va_code_Loop_prologue : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Loop_prologue () =
  (va_Block (va_CCons (va_code_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_vec_opr_vec 0) (va_op_reg_opr_reg 4) Secret) (va_CCons (va_code_Load128_word4_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 24) (va_op_reg_opr_reg 6) Secret) (va_CCons
    (va_code_AddImm (va_op_reg_opr_reg 4) (va_op_reg_opr_reg 4) 16) (va_CCons (va_code_AddImm
    (va_op_reg_opr_reg 6) (va_op_reg_opr_reg 6) 16) (va_CCons (va_code_Vadduwm (va_op_vec_opr_vec
    23) (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 24)) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec
    24) (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) 4) (va_CNil ()))))))))

val va_codegen_success_Loop_prologue : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Loop_prologue () =
  (va_pbool_and (va_codegen_success_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_vec_opr_vec 0) (va_op_reg_opr_reg 4) Secret) (va_pbool_and
    (va_codegen_success_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 24)
    (va_op_reg_opr_reg 6) Secret) (va_pbool_and (va_codegen_success_AddImm (va_op_reg_opr_reg 4)
    (va_op_reg_opr_reg 4) 16) (va_pbool_and (va_codegen_success_AddImm (va_op_reg_opr_reg 6)
    (va_op_reg_opr_reg 6) 16) (va_pbool_and (va_codegen_success_Vadduwm (va_op_vec_opr_vec 23)
    (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 24)) (va_pbool_and (va_codegen_success_Vsldoi
    (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) 4) (va_ttrue ())))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Loop_prologue (va_mods:va_mods_t) (in_b:buffer128) (offset:nat) (k_b:buffer128)
val va_qcode_Loop_prologue
      (va_mods: va_mods_t)
      (in_b: buffer128)
      (offset: nat)
      (k_b: buffer128)
      (block: block_w)
      (hash_orig: hash256)
    : (va_quickCode unit (va_code_Loop_prologue ()))

    va_mods: Vale.PPC64LE.QuickCode.va_mods_t ->
    in_b: Vale.PPC64LE.Memory.buffer128 ->
    offset: Prims.nat ->
    k_b: Vale.PPC64LE.Memory.buffer128 ->
    block: Vale.SHA.PPC64LE.SHA_helpers.block_w ->
    hash_orig: Vale.SHA.PPC64LE.SHA_helpers.hash256
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit (Vale.SHA.PPC64LE.Loop.va_code_Loop_prologue ())