val va_lemma_Loop_rounds_0_15 : va_b0:va_code -> va_s0:va_state -> in_b:buffer128 -> offset:nat ->
  k_b:buffer128 -> block:block_w -> hash_orig:hash256 -> input_BE:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Loop_rounds_0_15 ()) va_s0 /\ va_get_ok va_s0 /\
    (Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 4 va_s0)
    in_b (offset + 1) 3 (va_get_mem_layout va_s0) Secret /\
    Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) k_b
    1 4 (va_get_mem_layout va_s0) Secret /\ (let ks = Vale.PPC64LE.Decls.buffer128_as_seq
    (va_get_mem_heaplet 0 va_s0) k_b in Vale.SHA.PPC64LE.SHA_helpers.k_reqs ks /\ va_get_reg 4
    va_s0 + 48 < pow2_64 /\ va_get_reg 6 va_s0 + 64 < pow2_64 /\ input_BE ==
    Vale.Arch.Types.reverse_bytes_quad32_seq (FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s0) in_b) offset (offset + 4)) /\
    block == Vale.SHA.PPC64LE.SHA_helpers.quads_to_block_be input_BE /\ va_get_vec 0 va_s0 ==
    FStar.Seq.Base.index #quad32 input_BE 0 /\ (let hash =
    Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 0 block hash_orig in l_and (l_and (l_and (l_and
    (l_and (l_and (l_and ((va_get_vec 16 va_s0).hi3 == Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32
    (FStar.Seq.Base.index #Vale.SHA.PPC64LE.SHA_helpers.word hash 0)) ((va_get_vec 17 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 1))) ((va_get_vec 18 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 2))) ((va_get_vec 19 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 3))) ((va_get_vec 20 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 4))) ((va_get_vec 21 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 5))) ((va_get_vec 22 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 6))) ((va_get_vec 23 va_s0).hi3 ==
    Vale.Arch.Types.add_wrap32 (Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 7)) (Vale.SHA.PPC64LE.SHA_helpers.k_index ks 0))) /\
    l_and (l_and ((va_get_vec 24 va_s0).hi3 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 1)
    ((va_get_vec 24 va_s0).hi2 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 2)) ((va_get_vec 24
    va_s0).lo1 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 3)))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg 6 va_sM == va_get_reg 6 va_s0 + 64 /\ va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 48
    /\ (let ks = Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) k_b in (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)))
    /\ 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) /\ 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))) /\ 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))))))))))))))))))))))))))))))))
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)
val va_lemma_Loop_rounds_0_15 : va_b0:va_code -> va_s0:va_state -> in_b:buffer128 -> offset:nat ->
  k_b:buffer128 -> block:block_w -> hash_orig:hash256 -> input_BE:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Loop_rounds_0_15 ()) va_s0 /\ va_get_ok va_s0 /\
    (Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 4 va_s0)
    in_b (offset + 1) 3 (va_get_mem_layout va_s0) Secret /\
    Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) k_b
    1 4 (va_get_mem_layout va_s0) Secret /\ (let ks = Vale.PPC64LE.Decls.buffer128_as_seq
    (va_get_mem_heaplet 0 va_s0) k_b in Vale.SHA.PPC64LE.SHA_helpers.k_reqs ks /\ va_get_reg 4
    va_s0 + 48 < pow2_64 /\ va_get_reg 6 va_s0 + 64 < pow2_64 /\ input_BE ==
    Vale.Arch.Types.reverse_bytes_quad32_seq (FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s0) in_b) offset (offset + 4)) /\
    block == Vale.SHA.PPC64LE.SHA_helpers.quads_to_block_be input_BE /\ va_get_vec 0 va_s0 ==
    FStar.Seq.Base.index #quad32 input_BE 0 /\ (let hash =
    Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 0 block hash_orig in l_and (l_and (l_and (l_and
    (l_and (l_and (l_and ((va_get_vec 16 va_s0).hi3 == Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32
    (FStar.Seq.Base.index #Vale.SHA.PPC64LE.SHA_helpers.word hash 0)) ((va_get_vec 17 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 1))) ((va_get_vec 18 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 2))) ((va_get_vec 19 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 3))) ((va_get_vec 20 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 4))) ((va_get_vec 21 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 5))) ((va_get_vec 22 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 6))) ((va_get_vec 23 va_s0).hi3 ==
    Vale.Arch.Types.add_wrap32 (Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 7)) (Vale.SHA.PPC64LE.SHA_helpers.k_index ks 0))) /\
    l_and (l_and ((va_get_vec 24 va_s0).hi3 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 1)
    ((va_get_vec 24 va_s0).hi2 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 2)) ((va_get_vec 24
    va_s0).lo1 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 3)))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg 6 va_sM == va_get_reg 6 va_s0 + 64 /\ va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 48
    /\ (let ks = Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) k_b in (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)))
    /\ 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) /\ 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))) /\ 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))))))))))))))))))))))))))))))))
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)
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.Decls.va_code Vale.PPC64LE.Decls.va_state 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.fuel Prims.unit FStar.Pervasives.Native.Mktuple2 Vale.PPC64LE.Decls.va_fuel Vale.PPC64LE.QuickCode.va_lemma_norm_mods Prims.Cons Vale.PPC64LE.QuickCode.mod_t Vale.PPC64LE.QuickCode.va_Mod_vec Vale.PPC64LE.QuickCode.va_Mod_reg Vale.PPC64LE.QuickCode.va_Mod_ok Prims.Nil FStar.Pervasives.assert_norm Prims.eq2 Prims.list Vale.PPC64LE.QuickCode.__proj__QProc__item__mods Vale.SHA.PPC64LE.Rounds.va_code_Loop_rounds_0_15 FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.tuple3 Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCodes.va_wp_sound_code_norm Prims.l_and Vale.PPC64LE.QuickCodes.label Vale.PPC64LE.QuickCodes.va_range1 Prims.b2t Vale.PPC64LE.Decls.va_get_ok Prims.int Vale.PPC64LE.Decls.va_get_reg Prims.op_Addition Vale.Def.Words_s.nat32 Vale.Def.Words_s.__proj__Mkfour__item__hi3 Vale.Def.Types_s.nat32 Vale.PPC64LE.Decls.va_get_vec Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 FStar.Seq.Base.index Vale.SHA.PPC64LE.SHA_helpers.word Vale.Arch.Types.add_wrap32 Vale.SHA.PPC64LE.SHA_helpers.k_index Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale Vale.SHA.PPC64LE.SHA_helpers.ws_opaque Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__lo1 Vale.Def.Types_s.quad32 Vale.PPC64LE.Decls.buffer128_as_seq Vale.PPC64LE.Decls.va_get_mem_heaplet Vale.PPC64LE.QuickCode.quickCode Vale.SHA.PPC64LE.Rounds.va_qcode_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
  (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_lemma_Loop_rounds_0_15 : va_b0:va_code -> va_s0:va_state -> in_b:buffer128 -> offset:nat ->
  k_b:buffer128 -> block:block_w -> hash_orig:hash256 -> input_BE:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Loop_rounds_0_15 ()) va_s0 /\ va_get_ok va_s0 /\
    (Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 4 va_s0)
    in_b (offset + 1) 3 (va_get_mem_layout va_s0) Secret /\
    Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) k_b
    1 4 (va_get_mem_layout va_s0) Secret /\ (let ks = Vale.PPC64LE.Decls.buffer128_as_seq
    (va_get_mem_heaplet 0 va_s0) k_b in Vale.SHA.PPC64LE.SHA_helpers.k_reqs ks /\ va_get_reg 4
    va_s0 + 48 < pow2_64 /\ va_get_reg 6 va_s0 + 64 < pow2_64 /\ input_BE ==
    Vale.Arch.Types.reverse_bytes_quad32_seq (FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s0) in_b) offset (offset + 4)) /\
    block == Vale.SHA.PPC64LE.SHA_helpers.quads_to_block_be input_BE /\ va_get_vec 0 va_s0 ==
    FStar.Seq.Base.index #quad32 input_BE 0 /\ (let hash =
    Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 0 block hash_orig in l_and (l_and (l_and (l_and
    (l_and (l_and (l_and ((va_get_vec 16 va_s0).hi3 == Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32
    (FStar.Seq.Base.index #Vale.SHA.PPC64LE.SHA_helpers.word hash 0)) ((va_get_vec 17 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 1))) ((va_get_vec 18 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 2))) ((va_get_vec 19 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 3))) ((va_get_vec 20 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 4))) ((va_get_vec 21 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 5))) ((va_get_vec 22 va_s0).hi3 ==
    Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 6))) ((va_get_vec 23 va_s0).hi3 ==
    Vale.Arch.Types.add_wrap32 (Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 7)) (Vale.SHA.PPC64LE.SHA_helpers.k_index ks 0))) /\
    l_and (l_and ((va_get_vec 24 va_s0).hi3 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 1)
    ((va_get_vec 24 va_s0).hi2 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 2)) ((va_get_vec 24
    va_s0).lo1 == Vale.SHA.PPC64LE.SHA_helpers.k_index ks 3)))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg 6 va_sM == va_get_reg 6 va_s0 + 64 /\ va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 48
    /\ (let ks = Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) k_b in (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)))
    /\ 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) /\ 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))) /\ 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_b0: Vale.PPC64LE.Decls.va_code ->
    va_s0: Vale.PPC64LE.Decls.va_state ->
    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
  -> Prims.Ghost (Vale.PPC64LE.Decls.va_state * Vale.PPC64LE.Decls.va_fuel)