val va_code_Loop_rounds_3_7_11_body : i:nat -> msg:va_operand_vec_opr -> Tot va_code
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 ()))))
val va_code_Loop_rounds_3_7_11_body : i:nat -> msg:va_operand_vec_opr -> Tot va_code
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 ()))))
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
Prims.nat Vale.PPC64LE.Decls.va_operand_vec_opr Vale.PPC64LE.Decls.va_Block Vale.PPC64LE.Decls.va_CCons 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 Vale.PPC64LE.Decls.va_CNil Vale.PPC64LE.Decls.va_code
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]
val va_code_Loop_rounds_3_7_11_body : i:nat -> msg:va_operand_vec_opr -> Tot va_code
i: Prims.nat -> msg: Vale.PPC64LE.Decls.va_operand_vec_opr -> Vale.PPC64LE.Decls.va_code