val va_qcode_Loop_rounds_0_15
      (va_mods: va_mods_t)
      (in_b: buffer128)
      (offset: nat)
      (k_b: buffer128)
      (block: block_w)
      (hash_orig: hash256)
      (input_BE: (seq quad32))
    : (va_quickCode unit (va_code_Loop_rounds_0_15 ()))
let va_qcode_Loop_rounds_0_15 (va_mods:va_mods_t) (in_b:buffer128) (offset:nat) (k_b:buffer128)
  (block:block_w) (hash_orig:hash256) (input_BE:(seq quad32)) : (va_quickCode unit
  (va_code_Loop_rounds_0_15 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (va_arg34:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = input_BE in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 115 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (fun (_:unit) -> Vale.SHA.PPC64LE.SHA_helpers.lemma_quads_to_block_be va_arg34) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 117 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_3_7_11_body 3 (va_op_vec_opr_vec 4) in_b (offset + 1)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 118 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_3_7_11_body 7 (va_op_vec_opr_vec 8) in_b (offset + 2)) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 119 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_3_7_11_body 11 (va_op_vec_opr_vec 12) in_b (offset + 3)) (fun
    (va_s:va_state) _ -> va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 120 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    ((fun a_336 (s_337:(FStar.Seq.Base.seq a_336)) (i_338:Prims.nat) -> let (i_312:Prims.nat) =
    i_338 in Prims.b2t (Prims.op_LessThan i_312 (FStar.Seq.Base.length #a_336 s_337))) quad32
    input_BE 1) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 120 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_get_vec 4 va_s == FStar.Seq.Base.index #quad32 input_BE 1) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 121 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    ((fun a_336 (s_337:(FStar.Seq.Base.seq a_336)) (i_338:Prims.nat) -> let (i_312:Prims.nat) =
    i_338 in Prims.b2t (Prims.op_LessThan i_312 (FStar.Seq.Base.length #a_336 s_337))) quad32
    input_BE 2) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 121 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_get_vec 8 va_s == FStar.Seq.Base.index #quad32 input_BE 2) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 122 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    ((fun a_336 (s_337:(FStar.Seq.Base.seq a_336)) (i_338:Prims.nat) -> let (i_312:Prims.nat) =
    i_338 in Prims.b2t (Prims.op_LessThan i_312 (FStar.Seq.Base.length #a_336 s_337))) quad32
    input_BE 3) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 122 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_get_vec 12 va_s == FStar.Seq.Base.index #quad32 input_BE 3) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 124 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_1_3 block) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 125 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_0_59_a 0 k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 127 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_5_7 block) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 128 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_0_59_b 4 k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 130 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_9_11 block) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 131 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_0_59_c 8 k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 133 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_13_15 block) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 134 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_0_59_d 12 k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 136 column 27 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_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) block) (va_QEmpty (()))))))))))))))))))))))
val va_qcode_Loop_rounds_0_15
      (va_mods: va_mods_t)
      (in_b: buffer128)
      (offset: nat)
      (k_b: buffer128)
      (block: block_w)
      (hash_orig: hash256)
      (input_BE: (seq quad32))
    : (va_quickCode unit (va_code_Loop_rounds_0_15 ()))
let va_qcode_Loop_rounds_0_15
      (va_mods: va_mods_t)
      (in_b: buffer128)
      (offset: nat)
      (k_b: buffer128)
      (block: block_w)
      (hash_orig: hash256)
      (input_BE: (seq quad32))
    : (va_quickCode unit (va_code_Loop_rounds_0_15 ())) =
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        let va_arg34:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32) = input_BE in
        va_qPURE va_range1
          "***** PRECONDITION NOT MET AT line 115 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
          (fun (_: unit) -> Vale.SHA.PPC64LE.SHA_helpers.lemma_quads_to_block_be va_arg34)
          (va_QSeq va_range1
              "***** PRECONDITION NOT MET AT line 117 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
              (va_quick_Loop_rounds_3_7_11_body 3 (va_op_vec_opr_vec 4) in_b (offset + 1))
              (va_QSeq va_range1
                  "***** PRECONDITION NOT MET AT line 118 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                  (va_quick_Loop_rounds_3_7_11_body 7 (va_op_vec_opr_vec 8) in_b (offset + 2))
                  (va_QBind va_range1
                      "***** PRECONDITION NOT MET AT line 119 column 28 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                      (va_quick_Loop_rounds_3_7_11_body 11 (va_op_vec_opr_vec 12) in_b (offset + 3))
                      (fun (va_s: va_state) _ ->
                          va_qAssertSquash va_range1
                            "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 120 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                            ((fun a_336 (s_337: (FStar.Seq.Base.seq a_336)) (i_338: Prims.nat) ->
                                  let i_312:Prims.nat = i_338 in
                                  Prims.b2t (Prims.op_LessThan i_312
                                        (FStar.Seq.Base.length #a_336 s_337))) quad32
                                input_BE
                                1)
                            (fun _ ->
                                va_qAssert va_range1
                                  "***** PRECONDITION NOT MET AT line 120 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                  (va_get_vec 4 va_s == FStar.Seq.Base.index #quad32 input_BE 1)
                                  (va_qAssertSquash va_range1
                                      "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 121 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                      ((fun
                                            a_336
                                            (s_337: (FStar.Seq.Base.seq a_336))
                                            (i_338: Prims.nat)
                                            ->
                                            let i_312:Prims.nat = i_338 in
                                            Prims.b2t (Prims.op_LessThan i_312
                                                  (FStar.Seq.Base.length #a_336 s_337))) quad32
                                          input_BE
                                          2)
                                      (fun _ ->
                                          va_qAssert va_range1
                                            "***** PRECONDITION NOT MET AT line 121 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                            (va_get_vec 8 va_s ==
                                              FStar.Seq.Base.index #quad32 input_BE 2)
                                            (va_qAssertSquash va_range1
                                                "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 122 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                ((fun
                                                      a_336
                                                      (s_337: (FStar.Seq.Base.seq a_336))
                                                      (i_338: Prims.nat)
                                                      ->
                                                      let i_312:Prims.nat = i_338 in
                                                      Prims.b2t (Prims.op_LessThan i_312
                                                            (FStar.Seq.Base.length #a_336 s_337))) quad32
                                                    input_BE
                                                    3)
                                                (fun _ ->
                                                    va_qAssert va_range1
                                                      "***** PRECONDITION NOT MET AT line 122 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                      (va_get_vec 12 va_s ==
                                                        FStar.Seq.Base.index #quad32 input_BE 3)
                                                      (va_QSeq va_range1
                                                          "***** PRECONDITION NOT MET AT line 124 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                          (va_quick_Loop_rounds_1_3 block)
                                                          (va_QSeq va_range1
                                                              "***** PRECONDITION NOT MET AT line 125 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                              (va_quick_Loop_rounds_0_59_a 0
                                                                  k_b
                                                                  block
                                                                  hash_orig)
                                                              (va_QSeq va_range1
                                                                  "***** PRECONDITION NOT MET AT line 127 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                                  (va_quick_Loop_rounds_5_7 block)
                                                                  (va_QSeq va_range1
                                                                      "***** PRECONDITION NOT MET AT line 128 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                                      (va_quick_Loop_rounds_0_59_b 4
                                                                          k_b
                                                                          block
                                                                          hash_orig)
                                                                      (va_QSeq va_range1
                                                                          "***** PRECONDITION NOT MET AT line 130 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                                          (va_quick_Loop_rounds_9_11
                                                                              block)
                                                                          (va_QSeq va_range1
                                                                              "***** PRECONDITION NOT MET AT line 131 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                                              (va_quick_Loop_rounds_0_59_c
                                                                                  8
                                                                                  k_b
                                                                                  block
                                                                                  hash_orig)
                                                                              (va_QSeq va_range1
                                                                                  "***** PRECONDITION NOT MET AT line 133 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                                                  (va_quick_Loop_rounds_13_15
                                                                                      block)
                                                                                  (va_QSeq va_range1
                                                                                      "***** PRECONDITION NOT MET AT line 134 column 23 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                                                      (va_quick_Loop_rounds_0_59_d
                                                                                          12
                                                                                          k_b
                                                                                          block
                                                                                          hash_orig)
                                                                                      (va_QSeq va_range1
                                                                                          "***** PRECONDITION NOT MET AT line 136 column 27 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
                                                                                          (va_quick_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
                                                                                              )
                                                                                              block)
                                                                                          (va_QEmpty
                                                                                              (())))
                                                                                  ))))))))))))))))))
)
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
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 FStar.Seq.Base.seq Vale.PPC64LE.Memory.quad32 Vale.PPC64LE.QuickCodes.qblock Prims.unit Prims.Cons Vale.PPC64LE.Decls.va_code Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_3_7_11_body Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.PPC64LE.Machine_s.Block Vale.PPC64LE.Decls.ins Vale.PPC64LE.Decls.ocmp Prims.Nil Vale.PPC64LE.Machine_s.precode Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_1_3 Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_0_59_a Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_5_7 Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_0_59_b Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_9_11 Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_0_59_c Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_13_15 Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_0_59_d Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_16_63_body Vale.PPC64LE.Decls.va_state Vale.PPC64LE.QuickCodes.va_qPURE Prims.pure_post Prims.l_and Prims.eq2 Prims.int FStar.Seq.Base.length Vale.Def.Types_s.quad32 Prims.l_Forall Prims.l_imp Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThan Prims.op_LessThanOrEqual Vale.Def.Words_s.nat32 Vale.Def.Words_s.__proj__Mkfour__item__hi3 FStar.Seq.Base.index Vale.SHA.PPC64LE.SHA_helpers.ws_opaque Vale.SHA.PPC64LE.SHA_helpers.quads_to_block_be Prims.op_Addition Prims.op_Multiply Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__lo1 Vale.Def.Words_s.__proj__Mkfour__item__lo0 Vale.PPC64LE.QuickCodes.va_range1 Vale.SHA.PPC64LE.SHA_helpers.lemma_quads_to_block_be Vale.PPC64LE.QuickCodes.va_QSeq Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_3_7_11_body Vale.PPC64LE.QuickCodes.va_QBind Vale.PPC64LE.QuickCodes.va_qAssertSquash Prims.squash Vale.PPC64LE.QuickCodes.va_qAssert Vale.PPC64LE.Decls.va_get_vec Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_1_3 Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_0_59_a Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_5_7 Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_0_59_b Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_9_11 Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_0_59_c Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_13_15 Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_0_59_d Vale.SHA.PPC64LE.Rounds.Core.va_quick_Loop_rounds_16_63_body Vale.PPC64LE.QuickCodes.va_QEmpty Vale.PPC64LE.QuickCodes.quickCodes Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCode.va_quickCode Vale.SHA.PPC64LE.Rounds.va_code_Loop_rounds_0_15
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]
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 ())))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Loop_rounds_0_15 (va_mods:va_mods_t) (in_b:buffer128) (offset:nat) (k_b:buffer128)
  (block:block_w) (hash_orig:hash256) (input_BE:(seq quad32)) : (va_quickCode unit
val va_qcode_Loop_rounds_0_15
      (va_mods: va_mods_t)
      (in_b: buffer128)
      (offset: nat)
      (k_b: buffer128)
      (block: block_w)
      (hash_orig: hash256)
      (input_BE: (seq quad32))
    : (va_quickCode unit (va_code_Loop_rounds_0_15 ()))

    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 ->
    input_BE: FStar.Seq.Base.seq Vale.PPC64LE.Memory.quad32
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit
      (Vale.SHA.PPC64LE.Rounds.va_code_Loop_rounds_0_15 ())