val va_codegen_success_Preamble : va_dummy:unit -> Tot va_pbool
let va_codegen_success_Preamble () =
  (va_pbool_and (va_codegen_success_LoadImm64 (va_op_reg_opr_reg 10) 16) (va_pbool_and
    (va_codegen_success_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 16)
    (va_op_reg_opr_reg 3) Secret) (va_pbool_and (va_codegen_success_Load128_word4_buffer_index
    (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 20) (va_op_reg_opr_reg 3) (va_op_reg_opr_reg
    10) Secret) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 17) (va_op_vec_opr_vec
    16) (va_op_vec_opr_vec 16) 4) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 18)
    (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 8) (va_pbool_and (va_codegen_success_Vsldoi
    (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 12) (va_pbool_and
    (va_codegen_success_Vsldoi (va_op_vec_opr_vec 21) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20)
    4) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 20)
    (va_op_vec_opr_vec 20) 8) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 23)
    (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 12) (va_ttrue ()))))))))))
val va_codegen_success_Preamble : va_dummy:unit -> Tot va_pbool
let va_codegen_success_Preamble () =
(va_pbool_and (va_codegen_success_LoadImm64 (va_op_reg_opr_reg 10) 16)
    (va_pbool_and (va_codegen_success_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0)
            (va_op_vec_opr_vec 16)
            (va_op_reg_opr_reg 3)
            Secret)
        (va_pbool_and (va_codegen_success_Load128_word4_buffer_index (va_op_heaplet_mem_heaplet 0)
                (va_op_vec_opr_vec 20)
                (va_op_reg_opr_reg 3)
                (va_op_reg_opr_reg 10)
                Secret)
            (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 17)
                    (va_op_vec_opr_vec 16)
                    (va_op_vec_opr_vec 16)
                    4)
                (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 18)
                        (va_op_vec_opr_vec 16)
                        (va_op_vec_opr_vec 16)
                        8)
                    (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 19)
                            (va_op_vec_opr_vec 16)
                            (va_op_vec_opr_vec 16)
                            12)
                        (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 21)
                                (va_op_vec_opr_vec 20)
                                (va_op_vec_opr_vec 20)
                                4)
                            (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 22)
                                    (va_op_vec_opr_vec 20)
                                    (va_op_vec_opr_vec 20)
                                    8)
                                (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 23)
                                        (va_op_vec_opr_vec 20)
                                        (va_op_vec_opr_vec 20)
                                        12)
                                    (va_ttrue ()))))))))))
Vale.SHA.PPC64LE.fst.checked
Vale.SHA2.Wrapper.fsti.checked Vale.SHA.PPC64LE.SHA_helpers.fsti.checked Vale.SHA.PPC64LE.Loop.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.UInt8.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.SHA.PPC64LE.fst
Prims.unit Vale.PPC64LE.Decls.va_pbool_and Vale.PPC64LE.InsBasic.va_codegen_success_LoadImm64 Vale.PPC64LE.Decls.va_op_reg_opr_reg Vale.PPC64LE.InsVector.va_codegen_success_Load128_word4_buffer Vale.PPC64LE.Decls.va_op_heaplet_mem_heaplet Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.Arch.HeapTypes_s.Secret Vale.PPC64LE.InsVector.va_codegen_success_Load128_word4_buffer_index Vale.PPC64LE.InsVector.va_codegen_success_Vsldoi Vale.PPC64LE.Decls.va_ttrue Vale.PPC64LE.Decls.va_pbool
module Vale.SHA.PPC64LE
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.Loop
open Vale.SHA2.Wrapper
#reset-options "--z3rlimit 2000"
//-- Preamble

val va_code_Preamble : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Preamble () =
  (va_Block (va_CCons (va_code_LoadImm64 (va_op_reg_opr_reg 10) 16) (va_CCons
    (va_code_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 16)
    (va_op_reg_opr_reg 3) Secret) (va_CCons (va_code_Load128_word4_buffer_index
    (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 20) (va_op_reg_opr_reg 3) (va_op_reg_opr_reg
    10) Secret) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 16)
    (va_op_vec_opr_vec 16) 4) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 18) (va_op_vec_opr_vec
    16) (va_op_vec_opr_vec 16) 8) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 19)
    (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 12) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec
    21) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 4) (va_CCons (va_code_Vsldoi
    (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 8) (va_CCons
    (va_code_Vsldoi (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 12)
    (va_CNil ())))))))))))

val va_codegen_success_Preamble : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
val va_codegen_success_Preamble : va_dummy:unit -> Tot va_pbool
va_dummy: Prims.unit -> Vale.PPC64LE.Decls.va_pbool