val va_qcode_Loop_rounds_3_7_11_body
      (va_mods: va_mods_t)
      (i: nat)
      (msg: vec_opr)
      (in_b: buffer128)
      (offset: nat)
    : (va_quickCode unit (va_code_Loop_rounds_3_7_11_body i msg))
let va_qcode_Loop_rounds_3_7_11_body (va_mods:va_mods_t) (i:nat) (msg:vec_opr) (in_b:buffer128)
  (offset:nat) : (va_quickCode unit (va_code_Loop_rounds_3_7_11_body i msg)) =
  (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 79 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.Core.vaf *****"
    (va_quick_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0) msg (va_op_reg_opr_reg 4) Secret
    in_b offset) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 80 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.Core.vaf *****"
    (va_quick_AddImm (va_op_reg_opr_reg 4) (va_op_reg_opr_reg 4) 16) (va_QEmpty (())))))
val va_qcode_Loop_rounds_3_7_11_body
      (va_mods: va_mods_t)
      (i: nat)
      (msg: vec_opr)
      (in_b: buffer128)
      (offset: nat)
    : (va_quickCode unit (va_code_Loop_rounds_3_7_11_body i msg))
let va_qcode_Loop_rounds_3_7_11_body
      (va_mods: va_mods_t)
      (i: nat)
      (msg: vec_opr)
      (in_b: buffer128)
      (offset: nat)
    : (va_quickCode unit (va_code_Loop_rounds_3_7_11_body i msg)) =
(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 79 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.Core.vaf *****"
          (va_quick_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0)
              msg
              (va_op_reg_opr_reg 4)
              Secret
              in_b
              offset)
          (va_QSeq va_range1
              "***** PRECONDITION NOT MET AT line 80 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.Core.vaf *****"
              (va_quick_AddImm (va_op_reg_opr_reg 4) (va_op_reg_opr_reg 4) 16)
              (va_QEmpty (())))))
Vale.SHA.PPC64LE.Rounds.Core.fst.checked
Vale.SHA2.Wrapper.fsti.checked Vale.SHA.PPC64LE.SHA_helpers.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.Rounds.Core.fst
Vale.PPC64LE.QuickCode.va_mods_t Prims.nat Vale.PPC64LE.Decls.vec_opr Vale.PPC64LE.Memory.buffer128 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_reg_opr_reg Vale.Arch.HeapTypes_s.Secret Vale.PPC64LE.InsBasic.va_code_AddImm 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.InsBasic.va_quick_AddImm Vale.PPC64LE.QuickCodes.va_QEmpty Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCodes.quickCodes Vale.PPC64LE.QuickCode.va_quickCode Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_3_7_11_body
module Vale.SHA.PPC64LE.Rounds.Core
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.SHA2.Wrapper
#reset-options "--z3rlimit 2000"
//-- Loop_rounds_3_7_11_body

[@ "opaque_to_smt" va_qattr]
let va_code_Loop_rounds_3_7_11_body i msg =
  (va_Block (va_CCons (va_code_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0) msg
    (va_op_reg_opr_reg 4) Secret) (va_CCons (va_code_AddImm (va_op_reg_opr_reg 4)
    (va_op_reg_opr_reg 4) 16) (va_CNil ()))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Loop_rounds_3_7_11_body i msg =
  (va_pbool_and (va_codegen_success_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0) msg
    (va_op_reg_opr_reg 4) Secret) (va_pbool_and (va_codegen_success_AddImm (va_op_reg_opr_reg 4)
    (va_op_reg_opr_reg 4) 16) (va_ttrue ())))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Loop_rounds_3_7_11_body (va_mods:va_mods_t) (i:nat) (msg:vec_opr) (in_b:buffer128)
val va_qcode_Loop_rounds_3_7_11_body
      (va_mods: va_mods_t)
      (i: nat)
      (msg: vec_opr)
      (in_b: buffer128)
      (offset: nat)
    : (va_quickCode unit (va_code_Loop_rounds_3_7_11_body i msg))

    va_mods: Vale.PPC64LE.QuickCode.va_mods_t ->
    i: Prims.nat ->
    msg: Vale.PPC64LE.Decls.vec_opr ->
    in_b: Vale.PPC64LE.Memory.buffer128 ->
    offset: Prims.nat
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit
      (Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_3_7_11_body i msg)