val va_code_Loop_rounds_48_63 : va_dummy:unit -> Tot va_code
let va_code_Loop_rounds_48_63 () =
  (va_Block (va_CCons (va_code_Loop_rounds_16_59_a 48) (va_CCons (va_code_Loop_rounds_0_59_a 48)
    (va_CCons (va_code_Loop_rounds_16_59_b 52) (va_CCons (va_code_Loop_rounds_0_59_b 52) (va_CCons
    (va_code_Loop_rounds_16_59_c 56) (va_CCons (va_code_Loop_rounds_0_59_c 56) (va_CCons
    (va_code_Loop_rounds_60_63_a ()) (va_CCons (va_code_Loop_rounds_60_63_b ()) (va_CNil
    ()))))))))))
val va_code_Loop_rounds_48_63 : va_dummy:unit -> Tot va_code
let va_code_Loop_rounds_48_63 () =
(va_Block (va_CCons (va_code_Loop_rounds_16_59_a 48)
        (va_CCons (va_code_Loop_rounds_0_59_a 48)
            (va_CCons (va_code_Loop_rounds_16_59_b 52)
                (va_CCons (va_code_Loop_rounds_0_59_b 52)
                    (va_CCons (va_code_Loop_rounds_16_59_c 56)
                        (va_CCons (va_code_Loop_rounds_0_59_c 56)
                            (va_CCons (va_code_Loop_rounds_60_63_a ())
                                (va_CCons (va_code_Loop_rounds_60_63_b ()) (va_CNil ()))))))))))
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_Block Vale.PPC64LE.Decls.va_CCons Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_16_59_a Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_0_59_a Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_16_59_b Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_0_59_b Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_16_59_c Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_0_59_c Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_60_63_a Vale.SHA.PPC64LE.Rounds.Core.va_code_Loop_rounds_60_63_b Vale.PPC64LE.Decls.va_CNil Vale.PPC64LE.Decls.va_code
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
  (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 (()))))))))))))))))))))))

[@"opaque_to_smt"]
let va_lemma_Loop_rounds_0_15 va_b0 va_s0 in_b offset k_b block hash_orig input_BE =
  let (va_mods:va_mods_t) = [va_Mod_vec 26; va_Mod_vec 25; va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec
    22; va_Mod_vec 21; va_Mod_vec 20; va_Mod_vec 19; va_Mod_vec 18; va_Mod_vec 17; va_Mod_vec 16;
    va_Mod_vec 15; va_Mod_vec 14; va_Mod_vec 13; va_Mod_vec 12; va_Mod_vec 11; va_Mod_vec 10;
    va_Mod_vec 9; va_Mod_vec 8; va_Mod_vec 7; va_Mod_vec 6; va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec
    3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 4; va_Mod_ok] in
  let va_qc = va_qcode_Loop_rounds_0_15 va_mods in_b offset k_b block hash_orig input_BE in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Loop_rounds_0_15 ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 56 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 95 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_get_reg 6 va_sM == va_get_reg 6 va_s0 + 64) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 96 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 48) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 97 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (let ks = Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) k_b in label
    va_range1
    "***** POSTCONDITION NOT MET AT line 106 column 85 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (let next_hash = Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 16 block hash_orig in l_and
    (l_and (l_and (l_and (l_and (l_and (l_and ((va_get_vec 16 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word next_hash 0)) ((va_get_vec 17 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word next_hash 1))) ((va_get_vec 18 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word next_hash 2))) ((va_get_vec 19 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word next_hash 3))) ((va_get_vec 20 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word next_hash 4))) ((va_get_vec 21 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word next_hash 5))) ((va_get_vec 22 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word next_hash 6))) ((va_get_vec 23 va_sM).hi3 ==
    Vale.Arch.Types.add_wrap32 (Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word next_hash 7)) (Vale.SHA.PPC64LE.SHA_helpers.k_index ks 16)))
    /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 112 column 40 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and
    (l_and (l_and ((va_get_vec 0 va_sM).hi3 == Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 16)
    ((va_get_vec 1 va_sM).hi3 == Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 1)) ((va_get_vec 2
    va_sM).hi3 == Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 2)) ((va_get_vec 3 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 3)) ((va_get_vec 4 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 4)) ((va_get_vec 5 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 5)) ((va_get_vec 6 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 6)) ((va_get_vec 7 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 7)) ((va_get_vec 8 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 8)) ((va_get_vec 9 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 9)) ((va_get_vec 10 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 10)) ((va_get_vec 11 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 11)) ((va_get_vec 12 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 12)) ((va_get_vec 13 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 13)) ((va_get_vec 14 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 14)) ((va_get_vec 15 va_sM).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.ws_opaque block 15)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 113 column 92 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (l_and (l_and ((va_get_vec 24 va_sM).hi3 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 17)
    ((va_get_vec 24 va_sM).hi2 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 18)) ((va_get_vec 24
    va_sM).lo1 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 19))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 26; va_Mod_vec 25; va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec 22;
    va_Mod_vec 21; va_Mod_vec 20; va_Mod_vec 19; va_Mod_vec 18; va_Mod_vec 17; va_Mod_vec 16;
    va_Mod_vec 15; va_Mod_vec 14; va_Mod_vec 13; va_Mod_vec 12; va_Mod_vec 11; va_Mod_vec 10;
    va_Mod_vec 9; va_Mod_vec 8; va_Mod_vec 7; va_Mod_vec 6; va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec
    3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 4; va_Mod_ok]) va_sM
    va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Loop_rounds_0_15 in_b offset k_b block hash_orig input_BE va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Loop_rounds_0_15 (va_code_Loop_rounds_0_15 ()) va_s0 in_b offset
    k_b block hash_orig input_BE in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 26 va_sM (va_update_vec 25 va_sM (va_update_vec 24 va_sM
    (va_update_vec 23 va_sM (va_update_vec 22 va_sM (va_update_vec 21 va_sM (va_update_vec 20 va_sM
    (va_update_vec 19 va_sM (va_update_vec 18 va_sM (va_update_vec 17 va_sM (va_update_vec 16 va_sM
    (va_update_vec 15 va_sM (va_update_vec 14 va_sM (va_update_vec 13 va_sM (va_update_vec 12 va_sM
    (va_update_vec 11 va_sM (va_update_vec 10 va_sM (va_update_vec 9 va_sM (va_update_vec 8 va_sM
    (va_update_vec 7 va_sM (va_update_vec 6 va_sM (va_update_vec 5 va_sM (va_update_vec 4 va_sM
    (va_update_vec 3 va_sM (va_update_vec 2 va_sM (va_update_vec 1 va_sM (va_update_vec 0 va_sM
    (va_update_reg 6 va_sM (va_update_reg 4 va_sM (va_update_ok va_sM
    va_s0)))))))))))))))))))))))))))))));
  va_lemma_norm_mods ([va_Mod_vec 26; va_Mod_vec 25; va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec 22;
    va_Mod_vec 21; va_Mod_vec 20; va_Mod_vec 19; va_Mod_vec 18; va_Mod_vec 17; va_Mod_vec 16;
    va_Mod_vec 15; va_Mod_vec 14; va_Mod_vec 13; va_Mod_vec 12; va_Mod_vec 11; va_Mod_vec 10;
    va_Mod_vec 9; va_Mod_vec 8; va_Mod_vec 7; va_Mod_vec 6; va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec
    3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 4]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Loop_rounds_16_47

[@ "opaque_to_smt" va_qattr]
let va_code_Loop_rounds_16_47 i =
  (va_Block (va_CCons (va_code_Loop_rounds_16_59_a i) (va_CCons (va_code_Loop_rounds_0_59_a i)
    (va_CCons (va_code_Loop_rounds_16_59_b (i + 4)) (va_CCons (va_code_Loop_rounds_0_59_b (i + 4))
    (va_CCons (va_code_Loop_rounds_16_59_c (i + 8)) (va_CCons (va_code_Loop_rounds_0_59_c (i + 8))
    (va_CCons (va_code_Loop_rounds_16_59_d (i + 12)) (va_CCons (va_code_Loop_rounds_0_59_d (i +
    12)) (va_CNil ()))))))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Loop_rounds_16_47 i =
  (va_pbool_and (va_pbool_and (va_codegen_success_Loop_rounds_16_59_a i)
    (va_codegen_success_Loop_rounds_16_59_a i)) (va_pbool_and (va_pbool_and
    (va_codegen_success_Loop_rounds_0_59_a i) (va_codegen_success_Loop_rounds_0_59_a i))
    (va_pbool_and (va_pbool_and (va_codegen_success_Loop_rounds_16_59_b (i + 4))
    (va_codegen_success_Loop_rounds_16_59_b (i + 4))) (va_pbool_and (va_pbool_and
    (va_codegen_success_Loop_rounds_0_59_b (i + 4)) (va_codegen_success_Loop_rounds_0_59_b (i +
    4))) (va_pbool_and (va_pbool_and (va_codegen_success_Loop_rounds_16_59_c (i + 8))
    (va_codegen_success_Loop_rounds_16_59_c (i + 8))) (va_pbool_and (va_pbool_and
    (va_codegen_success_Loop_rounds_0_59_c (i + 8)) (va_codegen_success_Loop_rounds_0_59_c (i +
    8))) (va_pbool_and (va_pbool_and (va_codegen_success_Loop_rounds_16_59_d (i + 12))
    (va_codegen_success_Loop_rounds_16_59_d (i + 12))) (va_pbool_and (va_pbool_and
    (va_codegen_success_Loop_rounds_0_59_d (i + 12)) (va_codegen_success_Loop_rounds_0_59_d (i +
    12))) (va_ttrue ())))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Loop_rounds_16_47 (va_mods:va_mods_t) (i:nat) (k_b:buffer128) (block:block_w)
  (hash_orig:hash256) : (va_quickCode unit (va_code_Loop_rounds_16_47 i)) =
  (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 198 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_16_59_a i block) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 199 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 i k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 201 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_16_59_b (i + 4) block) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 202 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 (i + 4) k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 204 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_16_59_c (i + 8) block) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 205 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 (i + 8) k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 207 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_quick_Loop_rounds_16_59_d (i + 12) block) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 208 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 (i + 12) k_b block hash_orig) (va_QEmpty (())))))))))))

[@"opaque_to_smt"]
let va_lemma_Loop_rounds_16_47 va_b0 va_s0 i k_b block hash_orig =
  let (va_mods:va_mods_t) = [va_Mod_vec 26; va_Mod_vec 25; va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec
    22; va_Mod_vec 21; va_Mod_vec 20; va_Mod_vec 19; va_Mod_vec 18; va_Mod_vec 17; va_Mod_vec 16;
    va_Mod_vec 15; va_Mod_vec 14; va_Mod_vec 13; va_Mod_vec 12; va_Mod_vec 11; va_Mod_vec 10;
    va_Mod_vec 9; va_Mod_vec 8; va_Mod_vec 7; va_Mod_vec 6; va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec
    3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_ok] in
  let va_qc = va_qcode_Loop_rounds_16_47 va_mods i k_b block hash_orig in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Loop_rounds_16_47 i) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 139 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 179 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (va_get_reg 6 va_sM == va_get_reg 6 va_s0 + 64) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 180 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (let ks = buffer128_as_seq (va_get_mem_heaplet 0 va_sM) k_b in label va_range1
    "***** POSTCONDITION NOT MET AT line 189 column 87 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (let next_hash = repeat_range_vale (i + 16) block hash_orig in l_and (l_and (l_and (l_and
    (l_and (l_and (l_and ((va_get_vec 16 va_sM).hi3 == word_to_nat32 (index next_hash 0))
    ((va_get_vec 17 va_sM).hi3 == word_to_nat32 (index next_hash 1))) ((va_get_vec 18 va_sM).hi3 ==
    word_to_nat32 (index next_hash 2))) ((va_get_vec 19 va_sM).hi3 == word_to_nat32 (index
    next_hash 3))) ((va_get_vec 20 va_sM).hi3 == word_to_nat32 (index next_hash 4))) ((va_get_vec
    21 va_sM).hi3 == word_to_nat32 (index next_hash 5))) ((va_get_vec 22 va_sM).hi3 ==
    word_to_nat32 (index next_hash 6))) ((va_get_vec 23 va_sM).hi3 == add_wrap32 (word_to_nat32
    (index next_hash 7)) (k_index ks (i + 16)))) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 195 column 42 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and (l_and
    (l_and (l_and ((va_get_vec 0 va_sM).hi3 == ws_opaque block (i + 16)) ((va_get_vec 1 va_sM).hi3
    == ws_opaque block (i + 1))) ((va_get_vec 2 va_sM).hi3 == ws_opaque block (i + 2)))
    ((va_get_vec 3 va_sM).hi3 == ws_opaque block (i + 3))) ((va_get_vec 4 va_sM).hi3 == ws_opaque
    block (i + 4))) ((va_get_vec 5 va_sM).hi3 == ws_opaque block (i + 5))) ((va_get_vec 6
    va_sM).hi3 == ws_opaque block (i + 6))) ((va_get_vec 7 va_sM).hi3 == ws_opaque block (i + 7)))
    ((va_get_vec 8 va_sM).hi3 == ws_opaque block (i + 8))) ((va_get_vec 9 va_sM).hi3 == ws_opaque
    block (i + 9))) ((va_get_vec 10 va_sM).hi3 == ws_opaque block (i + 10))) ((va_get_vec 11
    va_sM).hi3 == ws_opaque block (i + 11))) ((va_get_vec 12 va_sM).hi3 == ws_opaque block (i +
    12))) ((va_get_vec 13 va_sM).hi3 == ws_opaque block (i + 13))) ((va_get_vec 14 va_sM).hi3 ==
    ws_opaque block (i + 14))) ((va_get_vec 15 va_sM).hi3 == ws_opaque block (i + 15))) /\ label
    va_range1
    "***** POSTCONDITION NOT MET AT line 196 column 98 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Rounds.vaf *****"
    (l_and (l_and ((va_get_vec 24 va_sM).hi3 == k_index ks (i + 17)) ((va_get_vec 24 va_sM).hi2 ==
    k_index ks (i + 18))) ((va_get_vec 24 va_sM).lo1 == k_index ks (i + 19)))))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 26; va_Mod_vec 25; va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec 22;
    va_Mod_vec 21; va_Mod_vec 20; va_Mod_vec 19; va_Mod_vec 18; va_Mod_vec 17; va_Mod_vec 16;
    va_Mod_vec 15; va_Mod_vec 14; va_Mod_vec 13; va_Mod_vec 12; va_Mod_vec 11; va_Mod_vec 10;
    va_Mod_vec 9; va_Mod_vec 8; va_Mod_vec 7; va_Mod_vec 6; va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec
    3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Loop_rounds_16_47 i k_b block hash_orig va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Loop_rounds_16_47 (va_code_Loop_rounds_16_47 i) va_s0 i k_b block
    hash_orig in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 26 va_sM (va_update_vec 25 va_sM (va_update_vec 24 va_sM
    (va_update_vec 23 va_sM (va_update_vec 22 va_sM (va_update_vec 21 va_sM (va_update_vec 20 va_sM
    (va_update_vec 19 va_sM (va_update_vec 18 va_sM (va_update_vec 17 va_sM (va_update_vec 16 va_sM
    (va_update_vec 15 va_sM (va_update_vec 14 va_sM (va_update_vec 13 va_sM (va_update_vec 12 va_sM
    (va_update_vec 11 va_sM (va_update_vec 10 va_sM (va_update_vec 9 va_sM (va_update_vec 8 va_sM
    (va_update_vec 7 va_sM (va_update_vec 6 va_sM (va_update_vec 5 va_sM (va_update_vec 4 va_sM
    (va_update_vec 3 va_sM (va_update_vec 2 va_sM (va_update_vec 1 va_sM (va_update_vec 0 va_sM
    (va_update_reg 6 va_sM (va_update_ok va_sM va_s0))))))))))))))))))))))))))))));
  va_lemma_norm_mods ([va_Mod_vec 26; va_Mod_vec 25; va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec 22;
    va_Mod_vec 21; va_Mod_vec 20; va_Mod_vec 19; va_Mod_vec 18; va_Mod_vec 17; va_Mod_vec 16;
    va_Mod_vec 15; va_Mod_vec 14; va_Mod_vec 13; va_Mod_vec 12; va_Mod_vec 11; va_Mod_vec 10;
    va_Mod_vec 9; va_Mod_vec 8; va_Mod_vec 7; va_Mod_vec 6; va_Mod_vec 5; va_Mod_vec 4; va_Mod_vec
    3; va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 6]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Loop_rounds_48_63

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