val va_codegen_success_Loop_rounds_0_15 : va_dummy:unit -> Tot va_pbool
let va_codegen_success_Loop_rounds_0_15 () =
  (va_pbool_and (va_codegen_success_Loop_rounds_3_7_11_body 3 (va_op_vec_opr_vec 4)) (va_pbool_and
    (va_codegen_success_Loop_rounds_3_7_11_body 7 (va_op_vec_opr_vec 8)) (va_pbool_and
    (va_codegen_success_Loop_rounds_3_7_11_body 11 (va_op_vec_opr_vec 12)) (va_pbool_and
    (va_codegen_success_Loop_rounds_1_3 ()) (va_pbool_and (va_codegen_success_Loop_rounds_0_59_a 0)
    (va_pbool_and (va_codegen_success_Loop_rounds_5_7 ()) (va_pbool_and
    (va_codegen_success_Loop_rounds_0_59_b 4) (va_pbool_and (va_codegen_success_Loop_rounds_9_11
    ()) (va_pbool_and (va_codegen_success_Loop_rounds_0_59_c 8) (va_pbool_and
    (va_codegen_success_Loop_rounds_13_15 ()) (va_pbool_and (va_codegen_success_Loop_rounds_0_59_d
    12) (va_pbool_and (va_codegen_success_Loop_rounds_16_63_body 16 (va_op_vec_opr_vec 0)
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 9) (va_op_vec_opr_vec 14)) (va_ttrue ())))))))))))))
val va_codegen_success_Loop_rounds_0_15 : va_dummy:unit -> Tot va_pbool
let va_codegen_success_Loop_rounds_0_15 () =
(va_pbool_and (va_codegen_success_Loop_rounds_3_7_11_body 3 (va_op_vec_opr_vec 4))
    (va_pbool_and (va_codegen_success_Loop_rounds_3_7_11_body 7 (va_op_vec_opr_vec 8))
        (va_pbool_and (va_codegen_success_Loop_rounds_3_7_11_body 11 (va_op_vec_opr_vec 12))
            (va_pbool_and (va_codegen_success_Loop_rounds_1_3 ())
                (va_pbool_and (va_codegen_success_Loop_rounds_0_59_a 0)
                    (va_pbool_and (va_codegen_success_Loop_rounds_5_7 ())
                        (va_pbool_and (va_codegen_success_Loop_rounds_0_59_b 4)
                            (va_pbool_and (va_codegen_success_Loop_rounds_9_11 ())
                                (va_pbool_and (va_codegen_success_Loop_rounds_0_59_c 8)
                                    (va_pbool_and (va_codegen_success_Loop_rounds_13_15 ())
                                        (va_pbool_and (va_codegen_success_Loop_rounds_0_59_d 12)
                                            (va_pbool_and (va_codegen_success_Loop_rounds_16_63_body
                                                    16
                                                    (va_op_vec_opr_vec 0)
                                                    (va_op_vec_opr_vec 1)
                                                    (va_op_vec_opr_vec 9)
                                                    (va_op_vec_opr_vec 14))
                                                (va_ttrue ())))))))))))))
Vale.SHA.PPC64LE.Rounds.fst.checked
Vale.SHA2.Wrapper.fsti.checked Vale.SHA.PPC64LE.SHA_helpers.fsti.checked Vale.SHA.PPC64LE.Rounds.Core.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.fst
Prims.unit Vale.PPC64LE.Decls.va_pbool_and Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_3_7_11_body Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_1_3 Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_0_59_a Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_5_7 Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_0_59_b Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_9_11 Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_0_59_c Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_13_15 Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_0_59_d Vale.SHA.PPC64LE.Rounds.Core.va_codegen_success_Loop_rounds_16_63_body Vale.PPC64LE.Decls.va_ttrue Vale.PPC64LE.Decls.va_pbool
module Vale.SHA.PPC64LE.Rounds
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.Core
open Vale.SHA2.Wrapper
#reset-options "--z3rlimit 2000"
//-- Loop_rounds_0_15

[@ "opaque_to_smt" va_qattr]
let va_code_Loop_rounds_0_15 () =
  (va_Block (va_CCons (va_code_Loop_rounds_3_7_11_body 3 (va_op_vec_opr_vec 4)) (va_CCons
    (va_code_Loop_rounds_3_7_11_body 7 (va_op_vec_opr_vec 8)) (va_CCons
    (va_code_Loop_rounds_3_7_11_body 11 (va_op_vec_opr_vec 12)) (va_CCons (va_Block (va_CNil ()))
    (va_CCons (va_Block (va_CNil ())) (va_CCons (va_Block (va_CNil ())) (va_CCons
    (va_code_Loop_rounds_1_3 ()) (va_CCons (va_code_Loop_rounds_0_59_a 0) (va_CCons
    (va_code_Loop_rounds_5_7 ()) (va_CCons (va_code_Loop_rounds_0_59_b 4) (va_CCons
    (va_code_Loop_rounds_9_11 ()) (va_CCons (va_code_Loop_rounds_0_59_c 8) (va_CCons
    (va_code_Loop_rounds_13_15 ()) (va_CCons (va_code_Loop_rounds_0_59_d 12) (va_CCons
    (va_code_Loop_rounds_16_63_body 16 (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 1)
    (va_op_vec_opr_vec 9) (va_op_vec_opr_vec 14)) (va_CNil ())))))))))))))))))

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