val va_code_Loop_while0 : va_dummy:unit -> Tot va_code
let va_code_Loop_while0 () =
  (va_Block (va_CCons (va_While (va_cmp_gt (va_op_cmp_reg 5) (va_const_cmp 0)) (va_Block (va_CCons
    (va_code_Loop_body0 ()) (va_CNil ())))) (va_CNil ())))
val va_code_Loop_while0 : va_dummy:unit -> Tot va_code
let va_code_Loop_while0 () =
(va_Block (va_CCons (va_While (va_cmp_gt (va_op_cmp_reg 5) (va_const_cmp 0))
            (va_Block (va_CCons (va_code_Loop_body0 ()) (va_CNil ()))))
        (va_CNil ())))
Vale.SHA.PPC64LE.Loop.fst.checked
Vale.SHA2.Wrapper.fsti.checked Vale.SHA.PPC64LE.SHA_helpers.fsti.checked Vale.SHA.PPC64LE.Rounds.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.Loop.fst
Prims.unit Vale.PPC64LE.Decls.va_Block Vale.PPC64LE.Decls.va_CCons Vale.PPC64LE.Decls.va_While Vale.PPC64LE.Decls.va_cmp_gt Vale.PPC64LE.Decls.va_op_cmp_reg Vale.PPC64LE.Decls.va_const_cmp Vale.SHA.PPC64LE.Loop.va_code_Loop_body0 Vale.PPC64LE.Decls.va_CNil Vale.PPC64LE.Decls.va_code
module Vale.SHA.PPC64LE.Loop
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
open Vale.SHA2.Wrapper
#reset-options "--z3rlimit 2000"
//-- Loop_prologue

val va_code_Loop_prologue : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Loop_prologue () =
  (va_Block (va_CCons (va_code_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_vec_opr_vec 0) (va_op_reg_opr_reg 4) Secret) (va_CCons (va_code_Load128_word4_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 24) (va_op_reg_opr_reg 6) Secret) (va_CCons
    (va_code_AddImm (va_op_reg_opr_reg 4) (va_op_reg_opr_reg 4) 16) (va_CCons (va_code_AddImm
    (va_op_reg_opr_reg 6) (va_op_reg_opr_reg 6) 16) (va_CCons (va_code_Vadduwm (va_op_vec_opr_vec
    23) (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 24)) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec
    24) (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) 4) (va_CNil ()))))))))

val va_codegen_success_Loop_prologue : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Loop_prologue () =
  (va_pbool_and (va_codegen_success_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_vec_opr_vec 0) (va_op_reg_opr_reg 4) Secret) (va_pbool_and
    (va_codegen_success_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 24)
    (va_op_reg_opr_reg 6) Secret) (va_pbool_and (va_codegen_success_AddImm (va_op_reg_opr_reg 4)
    (va_op_reg_opr_reg 4) 16) (va_pbool_and (va_codegen_success_AddImm (va_op_reg_opr_reg 6)
    (va_op_reg_opr_reg 6) 16) (va_pbool_and (va_codegen_success_Vadduwm (va_op_vec_opr_vec 23)
    (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 24)) (va_pbool_and (va_codegen_success_Vsldoi
    (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) 4) (va_ttrue ())))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Loop_prologue (va_mods:va_mods_t) (in_b:buffer128) (offset:nat) (k_b:buffer128)
  (block:block_w) (hash_orig:hash256) : (va_quickCode unit (va_code_Loop_prologue ())) =
  (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 80 column 26 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Load128_byte16_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 0)
    (va_op_reg_opr_reg 4) Secret in_b offset) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 81 column 25 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 24)
    (va_op_reg_opr_reg 6) Secret k_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 82 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_AddImm (va_op_reg_opr_reg 4) (va_op_reg_opr_reg 4) 16) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 83 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_AddImm (va_op_reg_opr_reg 6) (va_op_reg_opr_reg 6) 16) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 84 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 24))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 85 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) (va_op_vec_opr_vec 24) 4)
    (va_QEmpty (())))))))))


val va_lemma_Loop_prologue : va_b0:va_code -> va_s0:va_state -> in_b:buffer128 -> offset:nat ->
  k_b:buffer128 -> block:block_w -> hash_orig:hash256
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Loop_prologue ()) va_s0 /\ va_get_ok va_s0 /\ (let
    hash = Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 0 block hash_orig in
    Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 4 va_s0)
    in_b offset 1 (va_get_mem_layout va_s0) Secret /\ Vale.PPC64LE.Decls.validSrcAddrs128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) k_b 1 (va_get_mem_layout va_s0) Secret /\
    va_get_reg 4 va_s0 + 16 < pow2_64 /\ va_get_reg 6 va_s0 + 16 < pow2_64 /\ (va_get_vec 23
    va_s0).hi3 == Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 7))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let ks = Vale.PPC64LE.Decls.buffer128_read k_b 0 (va_get_mem_heaplet 0 va_sM) in let hash =
    Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 0 block hash_orig in va_get_vec 0 va_sM ==
    Vale.Def.Types_s.reverse_bytes_quad32 (Vale.PPC64LE.Decls.buffer128_read in_b offset
    (va_get_mem_heaplet 0 va_sM)) /\ va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 16 /\ va_get_reg 6
    va_sM == va_get_reg 6 va_s0 + 16 /\ (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 hash 7)) (Vale.Def.Words_s.__proj__Mkfour__item__lo0 ks) /\
    ((va_get_vec 24 va_sM).hi3 == Vale.Def.Words_s.__proj__Mkfour__item__lo1 ks /\ (va_get_vec 24
    va_sM).hi2 == Vale.Def.Words_s.__proj__Mkfour__item__hi2 ks /\ (va_get_vec 24 va_sM).lo1 ==
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 ks)) /\ va_state_eq va_sM (va_update_vec 24 va_sM
    (va_update_vec 23 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))))))))
[@"opaque_to_smt"]
let va_lemma_Loop_prologue va_b0 va_s0 in_b offset k_b block hash_orig =
  let (va_mods:va_mods_t) = [va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg
    4; va_Mod_ok] in
  let va_qc = va_qcode_Loop_prologue va_mods in_b offset k_b block hash_orig in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Loop_prologue ()) 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.Loop.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 72 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (let ks = Vale.PPC64LE.Decls.buffer128_read k_b 0 (va_get_mem_heaplet 0 va_sM) in label
    va_range1
    "***** POSTCONDITION NOT MET AT line 73 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (let hash = Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 0 block hash_orig in label va_range1
    "***** POSTCONDITION NOT MET AT line 74 column 74 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_vec 0 va_sM == Vale.Def.Types_s.reverse_bytes_quad32 (Vale.PPC64LE.Decls.buffer128_read
    in_b offset (va_get_mem_heaplet 0 va_sM))) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 75 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 16) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 76 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_reg 6 va_sM == va_get_reg 6 va_s0 + 16) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 77 column 71 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    ((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 hash 7)) (Vale.Def.Words_s.__proj__Mkfour__item__lo0 ks)) /\
    label va_range1
    "***** POSTCONDITION NOT MET AT line 78 column 65 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    ((va_get_vec 24 va_sM).hi3 == Vale.Def.Words_s.__proj__Mkfour__item__lo1 ks /\ (va_get_vec 24
    va_sM).hi2 == Vale.Def.Words_s.__proj__Mkfour__item__hi2 ks /\ (va_get_vec 24 va_sM).lo1 ==
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 ks)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 4;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Loop_prologue (in_b:buffer128) (offset:nat) (k_b:buffer128) (block:block_w)
  (hash_orig:hash256) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (let hash = Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 0 block hash_orig
    in Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 4 va_s0)
    in_b offset 1 (va_get_mem_layout va_s0) Secret /\ Vale.PPC64LE.Decls.validSrcAddrs128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) k_b 1 (va_get_mem_layout va_s0) Secret /\
    va_get_reg 4 va_s0 + 16 < pow2_64 /\ va_get_reg 6 va_s0 + 16 < pow2_64 /\ (va_get_vec 23
    va_s0).hi3 == Vale.SHA.PPC64LE.SHA_helpers.word_to_nat32 (FStar.Seq.Base.index
    #Vale.SHA.PPC64LE.SHA_helpers.word hash 7)) /\ (forall (va_x_r4:nat64) (va_x_r6:nat64)
    (va_x_v0:quad32) (va_x_v23:quad32) (va_x_v24:quad32) . let va_sM = va_upd_vec 24 va_x_v24
    (va_upd_vec 23 va_x_v23 (va_upd_vec 0 va_x_v0 (va_upd_reg 6 va_x_r6 (va_upd_reg 4 va_x_r4
    va_s0)))) in va_get_ok va_sM /\ (let ks = Vale.PPC64LE.Decls.buffer128_read k_b 0
    (va_get_mem_heaplet 0 va_sM) in let hash = Vale.SHA.PPC64LE.SHA_helpers.repeat_range_vale 0
    block hash_orig in va_get_vec 0 va_sM == Vale.Def.Types_s.reverse_bytes_quad32
    (Vale.PPC64LE.Decls.buffer128_read in_b offset (va_get_mem_heaplet 0 va_sM)) /\ va_get_reg 4
    va_sM == va_get_reg 4 va_s0 + 16 /\ va_get_reg 6 va_sM == va_get_reg 6 va_s0 + 16 /\
    (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 hash 7)) (Vale.Def.Words_s.__proj__Mkfour__item__lo0 ks) /\
    ((va_get_vec 24 va_sM).hi3 == Vale.Def.Words_s.__proj__Mkfour__item__lo1 ks /\ (va_get_vec 24
    va_sM).hi2 == Vale.Def.Words_s.__proj__Mkfour__item__hi2 ks /\ (va_get_vec 24 va_sM).lo1 ==
    Vale.Def.Words_s.__proj__Mkfour__item__hi3 ks)) ==> va_k va_sM (())))


val va_wpProof_Loop_prologue : in_b:buffer128 -> offset:nat -> k_b:buffer128 -> block:block_w ->
  hash_orig:hash256 -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Loop_prologue in_b offset k_b block hash_orig va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Loop_prologue ()) ([va_Mod_vec 24;
    va_Mod_vec 23; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 4]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Loop_prologue in_b offset k_b block hash_orig va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Loop_prologue (va_code_Loop_prologue ()) va_s0 in_b offset k_b
    block hash_orig in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 24 va_sM (va_update_vec 23 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 24; va_Mod_vec 23; 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)

[@ "opaque_to_smt" va_qattr]
let va_quick_Loop_prologue (in_b:buffer128) (offset:nat) (k_b:buffer128) (block:block_w)
  (hash_orig:hash256) : (va_quickCode unit (va_code_Loop_prologue ())) =
  (va_QProc (va_code_Loop_prologue ()) ([va_Mod_vec 24; va_Mod_vec 23; va_Mod_vec 0; va_Mod_reg 6;
    va_Mod_reg 4]) (va_wp_Loop_prologue in_b offset k_b block hash_orig) (va_wpProof_Loop_prologue
    in_b offset k_b block hash_orig))
//--
//-- Loop_rounds

val va_code_Loop_rounds : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Loop_rounds () =
  (va_Block (va_CCons (va_Block (va_CNil ())) (va_CCons (va_code_Xxmrghd (va_op_vec_opr_vec 28)
    (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 20)) (va_CCons (va_code_Xxmrghd (va_op_vec_opr_vec
    29) (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 21)) (va_CCons (va_code_Xxmrghd
    (va_op_vec_opr_vec 30) (va_op_vec_opr_vec 18) (va_op_vec_opr_vec 22)) (va_CCons
    (va_code_Xxmrghd (va_op_vec_opr_vec 31) (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 23))
    (va_CCons (va_code_Loop_prologue ()) (va_CCons (va_Block (va_CNil ())) (va_CCons
    (va_code_Loop_rounds_0_15 ()) (va_CCons (va_code_Loop_rounds_16_47 16) (va_CCons
    (va_code_Loop_rounds_16_47 32) (va_CCons (va_code_Loop_rounds_48_63 ()) (va_CCons
    (va_code_SubImm (va_op_reg_opr_reg 6) (va_op_reg_opr_reg 6) 256) (va_CCons (va_code_Vsldoi
    (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 28) (va_op_vec_opr_vec 28) 8) (va_CCons
    (va_code_Vsldoi (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 29) (va_op_vec_opr_vec 29) 8)
    (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 30) (va_op_vec_opr_vec 30)
    8) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 31) (va_op_vec_opr_vec
    31) 8) (va_CCons (va_code_Vadduwm (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16)
    (va_op_vec_opr_vec 28)) (va_CCons (va_code_Vadduwm (va_op_vec_opr_vec 17) (va_op_vec_opr_vec
    17) (va_op_vec_opr_vec 29)) (va_CCons (va_code_Vadduwm (va_op_vec_opr_vec 18)
    (va_op_vec_opr_vec 18) (va_op_vec_opr_vec 30)) (va_CCons (va_code_Vadduwm (va_op_vec_opr_vec
    19) (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 31)) (va_CCons (va_code_Vadduwm
    (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 0)) (va_CCons (va_code_Vadduwm
    (va_op_vec_opr_vec 21) (va_op_vec_opr_vec 21) (va_op_vec_opr_vec 1)) (va_CCons (va_code_Vadduwm
    (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 2)) (va_CCons (va_code_Vadduwm
    (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 3)) (va_CNil
    ()))))))))))))))))))))))))))

val va_codegen_success_Loop_rounds : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Loop_rounds () =
  (va_pbool_and (va_codegen_success_Xxmrghd (va_op_vec_opr_vec 28) (va_op_vec_opr_vec 16)
    (va_op_vec_opr_vec 20)) (va_pbool_and (va_codegen_success_Xxmrghd (va_op_vec_opr_vec 29)
    (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 21)) (va_pbool_and (va_codegen_success_Xxmrghd
    (va_op_vec_opr_vec 30) (va_op_vec_opr_vec 18) (va_op_vec_opr_vec 22)) (va_pbool_and
    (va_codegen_success_Xxmrghd (va_op_vec_opr_vec 31) (va_op_vec_opr_vec 19) (va_op_vec_opr_vec
    23)) (va_pbool_and (va_codegen_success_Loop_prologue ()) (va_pbool_and
    (va_codegen_success_Loop_rounds_0_15 ()) (va_pbool_and (va_codegen_success_Loop_rounds_16_47
    16) (va_pbool_and (va_codegen_success_Loop_rounds_16_47 32) (va_pbool_and
    (va_codegen_success_Loop_rounds_48_63 ()) (va_pbool_and (va_codegen_success_SubImm
    (va_op_reg_opr_reg 6) (va_op_reg_opr_reg 6) 256) (va_pbool_and (va_codegen_success_Vsldoi
    (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 28) (va_op_vec_opr_vec 28) 8) (va_pbool_and
    (va_codegen_success_Vsldoi (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 29) (va_op_vec_opr_vec 29)
    8) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 30)
    (va_op_vec_opr_vec 30) 8) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 3)
    (va_op_vec_opr_vec 31) (va_op_vec_opr_vec 31) 8) (va_pbool_and (va_codegen_success_Vadduwm
    (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 28)) (va_pbool_and
    (va_codegen_success_Vadduwm (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 17) (va_op_vec_opr_vec
    29)) (va_pbool_and (va_codegen_success_Vadduwm (va_op_vec_opr_vec 18) (va_op_vec_opr_vec 18)
    (va_op_vec_opr_vec 30)) (va_pbool_and (va_codegen_success_Vadduwm (va_op_vec_opr_vec 19)
    (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 31)) (va_pbool_and (va_codegen_success_Vadduwm
    (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 0)) (va_pbool_and
    (va_codegen_success_Vadduwm (va_op_vec_opr_vec 21) (va_op_vec_opr_vec 21) (va_op_vec_opr_vec
    1)) (va_pbool_and (va_codegen_success_Vadduwm (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 22)
    (va_op_vec_opr_vec 2)) (va_pbool_and (va_codegen_success_Vadduwm (va_op_vec_opr_vec 23)
    (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 3)) (va_ttrue ())))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Loop_rounds (va_mods:va_mods_t) (in_b:buffer128) (k_b:buffer128) (offset:nat)
  (hash_orig:hash256) : (va_quickCode unit (va_code_Loop_rounds ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in 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.Loop.vaf *****"
    ((fun a_1582 (s_1583:(FStar.Seq.Base.seq a_1582)) (i_1584:Prims.nat) (j_1585:Prims.nat) -> let
    (j_1545:Prims.nat) = j_1585 in Prims.b2t (Prims.op_AmpAmp (Prims.op_LessThanOrEqual i_1584
    j_1545) (Prims.op_LessThanOrEqual j_1545 (FStar.Seq.Base.length #a_1582 s_1583))))
    Vale.PPC64LE.Machine_s.quad32 (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s)
    in_b) offset (offset + 4)) (fun _ -> let (input_LE:(FStar.Seq.Base.seq
    Vale.PPC64LE.Machine_s.quad32)) = FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s) in_b) offset (offset + 4) in
    let (input_BE:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) =
    Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in let (block:block_w) =
    Vale.SHA.PPC64LE.SHA_helpers.quads_to_block_be input_BE in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 126 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Xxmrghd (va_op_vec_opr_vec 28) (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 20))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 127 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Xxmrghd (va_op_vec_opr_vec 29) (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 21))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 128 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Xxmrghd (va_op_vec_opr_vec 30) (va_op_vec_opr_vec 18) (va_op_vec_opr_vec 22))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 129 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Xxmrghd (va_op_vec_opr_vec 31) (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 23))
    (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 131 column 18 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Loop_prologue in_b offset k_b block hash_orig) (fun (va_s:va_state) _ ->
    va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 132 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.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)))
    Vale.Def.Types_s.quad32 input_BE 0) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 132 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_vec 0 va_s == FStar.Seq.Base.index #Vale.Def.Types_s.quad32 input_BE 0) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 134 column 21 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Loop_rounds_0_15 in_b offset k_b block hash_orig input_BE) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 135 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Loop_rounds_16_47 16 k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 136 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Loop_rounds_16_47 32 k_b block hash_orig) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 137 column 22 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Loop_rounds_48_63 k_b block hash_orig) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 138 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_SubImm (va_op_reg_opr_reg 6) (va_op_reg_opr_reg 6) 256) (fun (va_s:va_state) _ -> let
    (a_shuffle:quad32) = va_get_vec 16 va_s in let (b_shuffle:quad32) = va_get_vec 17 va_s in let
    (c_shuffle:quad32) = va_get_vec 18 va_s in let (d_shuffle:quad32) = va_get_vec 19 va_s in let
    (e_shuffle:quad32) = va_get_vec 20 va_s in let (f_shuffle:quad32) = va_get_vec 21 va_s in let
    (g_shuffle:quad32) = va_get_vec 22 va_s in let (h_shuffle:quad32) = va_get_vec 23 va_s in
    va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 149 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 28) (va_op_vec_opr_vec 28) 8)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 150 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 29) (va_op_vec_opr_vec 29) 8)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 151 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 30) (va_op_vec_opr_vec 30) 8)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 152 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 3) (va_op_vec_opr_vec 31) (va_op_vec_opr_vec 31) 8)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 153 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 28))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 154 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 29))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 155 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 18) (va_op_vec_opr_vec 18) (va_op_vec_opr_vec 30))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 156 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 31))
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 157 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 0)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 158 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 21) (va_op_vec_opr_vec 21) (va_op_vec_opr_vec 1)) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 159 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 2))
    (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 160 column 12 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Vadduwm (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 3)) (fun
    (va_s:va_state) _ -> let (va_arg76:Vale.SHA.PPC64LE.SHA_helpers.block_w) = block in let
    (va_arg75:Vale.Def.Types_s.quad32) = va_get_vec 23 va_s in let
    (va_arg74:Vale.Def.Types_s.quad32) = va_get_vec 22 va_s in let
    (va_arg73:Vale.Def.Types_s.quad32) = va_get_vec 21 va_s in let
    (va_arg72:Vale.Def.Types_s.quad32) = va_get_vec 20 va_s in let
    (va_arg71:Vale.Def.Types_s.quad32) = va_get_vec 19 va_s in let
    (va_arg70:Vale.Def.Types_s.quad32) = va_get_vec 18 va_s in let
    (va_arg69:Vale.Def.Types_s.quad32) = va_get_vec 17 va_s in let
    (va_arg68:Vale.Def.Types_s.quad32) = va_get_vec 16 va_s in let
    (va_arg67:Vale.Def.Types_s.quad32) = va_get_vec 23 va_old_s in let
    (va_arg66:Vale.Def.Types_s.quad32) = va_get_vec 22 va_old_s in let
    (va_arg65:Vale.Def.Types_s.quad32) = va_get_vec 21 va_old_s in let
    (va_arg64:Vale.Def.Types_s.quad32) = va_get_vec 20 va_old_s in let
    (va_arg63:Vale.Def.Types_s.quad32) = va_get_vec 19 va_old_s in let
    (va_arg62:Vale.Def.Types_s.quad32) = va_get_vec 18 va_old_s in let
    (va_arg61:Vale.Def.Types_s.quad32) = va_get_vec 17 va_old_s in let
    (va_arg60:Vale.Def.Types_s.quad32) = va_get_vec 16 va_old_s in let
    (va_arg59:Vale.Def.Types_s.quad32) = h_shuffle in let (va_arg58:Vale.Def.Types_s.quad32) =
    g_shuffle in let (va_arg57:Vale.Def.Types_s.quad32) = f_shuffle in let
    (va_arg56:Vale.Def.Types_s.quad32) = e_shuffle in let (va_arg55:Vale.Def.Types_s.quad32) =
    d_shuffle in let (va_arg54:Vale.Def.Types_s.quad32) = c_shuffle in let
    (va_arg53:Vale.Def.Types_s.quad32) = b_shuffle in let (va_arg52:Vale.Def.Types_s.quad32) =
    a_shuffle in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 162 column 17 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (fun (_:unit) -> Vale.SHA.PPC64LE.SHA_helpers.update_lemma va_arg52 va_arg53 va_arg54 va_arg55
    va_arg56 va_arg57 va_arg58 va_arg59 va_arg60 va_arg61 va_arg62 va_arg63 va_arg64 va_arg65
    va_arg66 va_arg67 va_arg68 va_arg69 va_arg70 va_arg71 va_arg72 va_arg73 va_arg74 va_arg75
    va_arg76) (va_QEmpty (())))))))))))))))))))))))))))))


val va_lemma_Loop_rounds : va_b0:va_code -> va_s0:va_state -> in_b:buffer128 -> k_b:buffer128 ->
  offset:nat -> hash_orig:hash256
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Loop_rounds ()) 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 4 (va_get_mem_layout va_s0) Secret /\ Vale.PPC64LE.Decls.validSrcAddrs128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) k_b 16 (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
    13 3 (va_get_mem_layout va_s0) Secret /\ Vale.SHA.PPC64LE.SHA_helpers.k_reqs
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s0) k_b) /\ (let input_LE =
    FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32 (Vale.PPC64LE.Decls.buffer128_as_seq
    (va_get_mem_heaplet 0 va_s0) in_b) 0 offset in let input_BE =
    Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_s0) (va_get_vec 17
    va_s0) (va_get_vec 18 va_s0) (va_get_vec 19 va_s0) (va_get_vec 20 va_s0) (va_get_vec 21 va_s0)
    (va_get_vec 22 va_s0) (va_get_vec 23 va_s0) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE hash_orig) /\ va_get_reg 4 va_s0 + 64 < pow2_64 /\ va_get_reg 6 va_s0 + 256 <
    pow2_64)))
  (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 /\ va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 64 /\
    (let (block:block_w) = Vale.SHA.PPC64LE.SHA_helpers.quads_to_block_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_sM) in_b) offset (offset + 4)))
    in Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_block
    hash_orig block /\ (let input_LE = FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) in_b) 0 (offset + 4) in let
    input_BE = Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE hash_orig))) /\ va_state_eq va_sM (va_update_vec 31 va_sM (va_update_vec 30 va_sM
    (va_update_vec 29 va_sM (va_update_vec 28 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))))))))))))))))))))))))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Loop_rounds va_b0 va_s0 in_b k_b offset hash_orig =
  let (va_mods:va_mods_t) = [va_Mod_vec 31; va_Mod_vec 30; va_Mod_vec 29; va_Mod_vec 28; 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 va_mods in_b k_b offset hash_orig in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Loop_rounds ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 88 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 114 column 24 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_reg 6 va_sM == va_get_reg 6 va_s0) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 115 column 29 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 64) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 116 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (let (block:block_w) = Vale.SHA.PPC64LE.SHA_helpers.quads_to_block_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_sM) in_b) offset (offset + 4)))
    in label va_range1
    "***** POSTCONDITION NOT MET AT line 117 column 125 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_block
    hash_orig block) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 120 column 134 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (let input_LE = FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) in_b) 0 (offset + 4) in let
    input_BE = Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE hash_orig)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 31; va_Mod_vec 30; va_Mod_vec 29; va_Mod_vec 28; 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)

[@ va_qattr]
let va_wp_Loop_rounds (in_b:buffer128) (k_b:buffer128) (offset:nat) (hash_orig:hash256)
  (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (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 4 (va_get_mem_layout va_s0) Secret /\
    Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) k_b 16
    (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 13 3 (va_get_mem_layout va_s0) Secret /\
    Vale.SHA.PPC64LE.SHA_helpers.k_reqs (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0
    va_s0) k_b) /\ (let input_LE = FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s0) in_b) 0 offset in let
    input_BE = Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_s0) (va_get_vec 17
    va_s0) (va_get_vec 18 va_s0) (va_get_vec 19 va_s0) (va_get_vec 20 va_s0) (va_get_vec 21 va_s0)
    (va_get_vec 22 va_s0) (va_get_vec 23 va_s0) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE hash_orig) /\ va_get_reg 4 va_s0 + 64 < pow2_64 /\ va_get_reg 6 va_s0 + 256 < pow2_64)
    /\ (forall (va_x_r4:nat64) (va_x_r6:nat64) (va_x_v0:quad32) (va_x_v1:quad32) (va_x_v2:quad32)
    (va_x_v3:quad32) (va_x_v4:quad32) (va_x_v5:quad32) (va_x_v6:quad32) (va_x_v7:quad32)
    (va_x_v8:quad32) (va_x_v9:quad32) (va_x_v10:quad32) (va_x_v11:quad32) (va_x_v12:quad32)
    (va_x_v13:quad32) (va_x_v14:quad32) (va_x_v15:quad32) (va_x_v16:quad32) (va_x_v17:quad32)
    (va_x_v18:quad32) (va_x_v19:quad32) (va_x_v20:quad32) (va_x_v21:quad32) (va_x_v22:quad32)
    (va_x_v23:quad32) (va_x_v24:quad32) (va_x_v25:quad32) (va_x_v26:quad32) (va_x_v28:quad32)
    (va_x_v29:quad32) (va_x_v30:quad32) (va_x_v31:quad32) . let va_sM = va_upd_vec 31 va_x_v31
    (va_upd_vec 30 va_x_v30 (va_upd_vec 29 va_x_v29 (va_upd_vec 28 va_x_v28 (va_upd_vec 26 va_x_v26
    (va_upd_vec 25 va_x_v25 (va_upd_vec 24 va_x_v24 (va_upd_vec 23 va_x_v23 (va_upd_vec 22 va_x_v22
    (va_upd_vec 21 va_x_v21 (va_upd_vec 20 va_x_v20 (va_upd_vec 19 va_x_v19 (va_upd_vec 18 va_x_v18
    (va_upd_vec 17 va_x_v17 (va_upd_vec 16 va_x_v16 (va_upd_vec 15 va_x_v15 (va_upd_vec 14 va_x_v14
    (va_upd_vec 13 va_x_v13 (va_upd_vec 12 va_x_v12 (va_upd_vec 11 va_x_v11 (va_upd_vec 10 va_x_v10
    (va_upd_vec 9 va_x_v9 (va_upd_vec 8 va_x_v8 (va_upd_vec 7 va_x_v7 (va_upd_vec 6 va_x_v6
    (va_upd_vec 5 va_x_v5 (va_upd_vec 4 va_x_v4 (va_upd_vec 3 va_x_v3 (va_upd_vec 2 va_x_v2
    (va_upd_vec 1 va_x_v1 (va_upd_vec 0 va_x_v0 (va_upd_reg 6 va_x_r6 (va_upd_reg 4 va_x_r4
    va_s0)))))))))))))))))))))))))))))))) in va_get_ok va_sM /\ (va_get_reg 6 va_sM == va_get_reg 6
    va_s0 /\ va_get_reg 4 va_sM == va_get_reg 4 va_s0 + 64 /\ (let (block:block_w) =
    Vale.SHA.PPC64LE.SHA_helpers.quads_to_block_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_sM) in_b) offset (offset + 4))) in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_block
    hash_orig block /\ (let input_LE = FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) in_b) 0 (offset + 4) in let
    input_BE = Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE hash_orig))) ==> va_k va_sM (())))


val va_wpProof_Loop_rounds : in_b:buffer128 -> k_b:buffer128 -> offset:nat -> hash_orig:hash256 ->
  va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Loop_rounds in_b k_b offset hash_orig va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Loop_rounds ()) ([va_Mod_vec 31;
    va_Mod_vec 30; va_Mod_vec 29; va_Mod_vec 28; 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_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Loop_rounds in_b k_b offset hash_orig va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Loop_rounds (va_code_Loop_rounds ()) va_s0 in_b k_b offset
    hash_orig in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 31 va_sM (va_update_vec 30 va_sM (va_update_vec 29 va_sM
    (va_update_vec 28 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 31; va_Mod_vec 30; va_Mod_vec 29; va_Mod_vec 28; 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)

[@ "opaque_to_smt" va_qattr]
let va_quick_Loop_rounds (in_b:buffer128) (k_b:buffer128) (offset:nat) (hash_orig:hash256) :
  (va_quickCode unit (va_code_Loop_rounds ())) =
  (va_QProc (va_code_Loop_rounds ()) ([va_Mod_vec 31; va_Mod_vec 30; va_Mod_vec 29; va_Mod_vec 28;
    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_wp_Loop_rounds in_b k_b offset
    hash_orig) (va_wpProof_Loop_rounds in_b k_b offset hash_orig))
//--
//-- Mod_cr0

val va_code_Mod_cr0 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Mod_cr0 () =
  (va_Block (va_CNil ()))

val va_codegen_success_Mod_cr0 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Mod_cr0 () =
  (va_ttrue ())

[@ "opaque_to_smt" va_qattr]
let va_qcode_Mod_cr0 (va_mods:va_mods_t) : (va_quickCode unit (va_code_Mod_cr0 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QEmpty (())))


val va_lemma_Mod_cr0 : va_b0:va_code -> va_s0:va_state
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Mod_cr0 ()) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_state_eq va_sM (va_update_cr0 va_sM (va_update_ok va_sM va_s0))))
[@"opaque_to_smt"]
let va_lemma_Mod_cr0 va_b0 va_s0 =
  let (va_mods:va_mods_t) = [va_Mod_cr0; va_Mod_ok] in
  let va_qc = va_qcode_Mod_cr0 va_mods in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Mod_cr0 ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 165 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_ok va_sM)) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_cr0; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Mod_cr0 (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_cr0:cr0_t) . let va_sM = va_upd_cr0 va_x_cr0 va_s0 in va_get_ok
    va_sM ==> va_k va_sM (())))


val va_wpProof_Mod_cr0 : va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Mod_cr0 va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Mod_cr0 ()) ([va_Mod_cr0]) va_s0 va_k
    ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Mod_cr0 va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Mod_cr0 (va_code_Mod_cr0 ()) va_s0 in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_cr0 va_sM (va_update_ok va_sM va_s0)));
  va_lemma_norm_mods ([va_Mod_cr0]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Mod_cr0 () : (va_quickCode unit (va_code_Mod_cr0 ())) =
  (va_QProc (va_code_Mod_cr0 ()) ([va_Mod_cr0]) va_wp_Mod_cr0 va_wpProof_Mod_cr0)
//--
//-- Loop_body0

val va_code_Loop_body0 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Loop_body0 () =
  (va_Block (va_CCons (va_code_Mod_cr0 ()) (va_CCons (va_code_Loop_rounds ()) (va_CCons
    (va_code_SubImm (va_op_reg_opr_reg 5) (va_op_reg_opr_reg 5) 1) (va_CNil ())))))

val va_codegen_success_Loop_body0 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Loop_body0 () =
  (va_pbool_and (va_codegen_success_Mod_cr0 ()) (va_pbool_and (va_codegen_success_Loop_rounds ())
    (va_pbool_and (va_codegen_success_SubImm (va_op_reg_opr_reg 5) (va_op_reg_opr_reg 5) 1)
    (va_ttrue ()))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Loop_body0 (va_mods:va_mods_t) (va_old:va_state) (va_in_hash_orig:hash256)
  (va_in_in_b:buffer128) (va_in_k_b:buffer128) (va_in_count:nat) : (va_quickCode (nat)
  (va_code_Loop_body0 ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let (hash_orig:hash256)
    = va_in_hash_orig in let (in_b:buffer128) = va_in_in_b in let (k_b:buffer128) = va_in_k_b in
    let (count:nat) = va_in_count in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 219 column 16 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Mod_cr0 ()) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 220 column 20 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_Loop_rounds in_b k_b (4 `op_Multiply` count) hash_orig) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 221 column 15 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_quick_SubImm (va_op_reg_opr_reg 5) (va_op_reg_opr_reg 5) 1) (fun (va_s:va_state) _ -> let
    (count:nat) = count + 1 in va_QEmpty ((count)))))))


val va_lemma_Loop_body0 : va_b0:va_code -> va_s0:va_state -> va_old:va_state ->
  va_in_hash_orig:hash256 -> va_in_in_b:buffer128 -> va_in_k_b:buffer128 -> va_in_count:nat
  -> Ghost (va_state & va_fuel & nat)
  (requires (va_require_total va_b0 (va_code_Loop_body0 ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 4 va_old)
    va_in_in_b (4 `op_Multiply` va_get_reg 5 va_old) (va_get_mem_layout va_s0) Secret /\
    Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) va_in_k_b
    16 (va_get_mem_layout va_s0) Secret /\ Vale.PPC64LE.Decls.validSrcAddrsOffset128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) va_in_k_b 13 3 (va_get_mem_layout va_s0)
    Secret /\ va_get_reg 4 va_old + 64 `op_Multiply` va_get_reg 5 va_old < pow2_64 /\ va_get_reg 6
    va_s0 + 256 < pow2_64 /\ va_get_reg 5 va_s0 == va_get_reg 5 va_old - va_in_count /\ va_get_reg
    4 va_s0 == va_get_reg 4 va_old + 64 `op_Multiply` va_in_count /\
    Vale.SHA.PPC64LE.SHA_helpers.k_reqs (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0
    va_s0) va_in_k_b) /\ (let input_LE = FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s0) va_in_in_b) 0 (va_in_count
    `op_Multiply` 4) in let input_BE = Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_s0) (va_get_vec 17
    va_s0) (va_get_vec 18 va_s0) (va_get_vec 19 va_s0) (va_get_vec 20 va_s0) (va_get_vec 21 va_s0)
    (va_get_vec 22 va_s0) (va_get_vec 23 va_s0) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE va_in_hash_orig) /\ va_get_reg 5 va_s0 > 0))
  (ensures (fun (va_sM, va_fM, count) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM
    /\ Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_sM) (va_get_reg 4 va_old)
    va_in_in_b (4 `op_Multiply` va_get_reg 5 va_old) (va_get_mem_layout va_sM) Secret /\
    Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_sM) (va_get_reg 6 va_sM) va_in_k_b
    16 (va_get_mem_layout va_sM) Secret /\ Vale.PPC64LE.Decls.validSrcAddrsOffset128
    (va_get_mem_heaplet 0 va_sM) (va_get_reg 6 va_sM) va_in_k_b 13 3 (va_get_mem_layout va_sM)
    Secret /\ va_get_reg 4 va_old + 64 `op_Multiply` va_get_reg 5 va_old < pow2_64 /\ va_get_reg 6
    va_sM + 256 < pow2_64 /\ va_get_reg 5 va_sM == va_get_reg 5 va_old - count /\ va_get_reg 4
    va_sM == va_get_reg 4 va_old + 64 `op_Multiply` count /\ Vale.SHA.PPC64LE.SHA_helpers.k_reqs
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) va_in_k_b) /\ (let input_LE =
    FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32 (Vale.PPC64LE.Decls.buffer128_as_seq
    (va_get_mem_heaplet 0 va_sM) va_in_in_b) 0 (count `op_Multiply` 4) in let input_BE =
    Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE va_in_hash_orig) /\ precedes_wrap (va_get_reg 5 va_sM) (va_get_reg 5 va_s0) /\
    va_state_eq 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 31 va_sM
    (va_update_vec 30 va_sM (va_update_vec 3 va_sM (va_update_vec 29 va_sM (va_update_vec 28 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 2 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 1 va_sM (va_update_vec 0 va_sM
    (va_update_reg 6 va_sM (va_update_reg 5 va_sM (va_update_reg 4 va_sM (va_update_ok va_sM
    (va_update_cr0 va_sM va_s0))))))))))))))))))))))))))))))))))))))
[@"opaque_to_smt"]
let va_lemma_Loop_body0 va_b0 va_s0 va_old va_in_hash_orig va_in_in_b va_in_k_b va_in_count =
  let va_old = va_expand_state va_old in
  let (va_mods:va_mods_t) = [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 31; va_Mod_vec 30; va_Mod_vec 3; va_Mod_vec 29; va_Mod_vec 28;
    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 2; 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 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 5; va_Mod_reg 4; va_Mod_ok; va_Mod_cr0] in
  let va_qc = va_qcode_Loop_body0 va_mods va_old va_in_hash_orig va_in_in_b va_in_k_b va_in_count in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Loop_body0 ()) va_qc va_s0 (fun va_s0
    va_sM va_g -> let count = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 171 column 1 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 202 column 86 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_sM) (va_get_reg 4 va_old)
    va_in_in_b (4 `op_Multiply` va_get_reg 5 va_old) (va_get_mem_layout va_sM) Secret) /\ label
    va_range1
    "***** POSTCONDITION NOT MET AT line 203 column 86 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_sM) (va_get_reg 6 va_sM)
    va_in_k_b 16 (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 204 column 78 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (Vale.PPC64LE.Decls.validSrcAddrsOffset128 (va_get_mem_heaplet 0 va_sM) (va_get_reg 6 va_sM)
    va_in_k_b 13 3 (va_get_mem_layout va_sM) Secret) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 206 column 47 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_reg 4 va_old + 64 `op_Multiply` va_get_reg 5 va_old < pow2_64) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 207 column 32 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_reg 6 va_sM + 256 < pow2_64) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 209 column 36 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_reg 5 va_sM == va_get_reg 5 va_old - count) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 210 column 43 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (va_get_reg 4 va_sM == va_get_reg 4 va_old + 64 `op_Multiply` count) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 212 column 49 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (Vale.SHA.PPC64LE.SHA_helpers.k_reqs (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0
    va_sM) va_in_k_b)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 216 column 138 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (let input_LE = FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) va_in_in_b) 0 (count
    `op_Multiply` 4) in let input_BE = Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE va_in_hash_orig) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 217 column 9 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.Loop.vaf *****"
    (precedes_wrap (va_get_reg 5 va_sM) (va_get_reg 5 va_s0))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([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 31; va_Mod_vec 30; va_Mod_vec 3; va_Mod_vec 29; va_Mod_vec 28;
    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 2; 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 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 5; va_Mod_reg 4; va_Mod_ok; va_Mod_cr0])
    va_sM va_s0;
  let count = va_g in
  (va_sM, va_fM, count)

[@ va_qattr]
let va_wp_Loop_body0 (va_old:va_state) (va_in_hash_orig:hash256) (va_in_in_b:buffer128)
  (va_in_k_b:buffer128) (va_in_count:nat) (va_s0:va_state) (va_k:(va_state -> nat -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0) (va_get_reg
    4 va_old) va_in_in_b (4 `op_Multiply` va_get_reg 5 va_old) (va_get_mem_layout va_s0) Secret /\
    Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) va_in_k_b
    16 (va_get_mem_layout va_s0) Secret /\ Vale.PPC64LE.Decls.validSrcAddrsOffset128
    (va_get_mem_heaplet 0 va_s0) (va_get_reg 6 va_s0) va_in_k_b 13 3 (va_get_mem_layout va_s0)
    Secret /\ va_get_reg 4 va_old + 64 `op_Multiply` va_get_reg 5 va_old < pow2_64 /\ va_get_reg 6
    va_s0 + 256 < pow2_64 /\ va_get_reg 5 va_s0 == va_get_reg 5 va_old - va_in_count /\ va_get_reg
    4 va_s0 == va_get_reg 4 va_old + 64 `op_Multiply` va_in_count /\
    Vale.SHA.PPC64LE.SHA_helpers.k_reqs (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0
    va_s0) va_in_k_b) /\ (let input_LE = FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_s0) va_in_in_b) 0 (va_in_count
    `op_Multiply` 4) in let input_BE = Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_s0) (va_get_vec 17
    va_s0) (va_get_vec 18 va_s0) (va_get_vec 19 va_s0) (va_get_vec 20 va_s0) (va_get_vec 21 va_s0)
    (va_get_vec 22 va_s0) (va_get_vec 23 va_s0) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE va_in_hash_orig) /\ va_get_reg 5 va_s0 > 0 /\ (forall (va_x_cr0:cr0_t) (va_x_ok:bool)
    (va_x_r4:nat64) (va_x_r5:nat64) (va_x_r6:nat64) (va_x_v0:quad32) (va_x_v1:quad32)
    (va_x_v10:quad32) (va_x_v11:quad32) (va_x_v12:quad32) (va_x_v13:quad32) (va_x_v14:quad32)
    (va_x_v15:quad32) (va_x_v16:quad32) (va_x_v17:quad32) (va_x_v18:quad32) (va_x_v19:quad32)
    (va_x_v2:quad32) (va_x_v20:quad32) (va_x_v21:quad32) (va_x_v22:quad32) (va_x_v23:quad32)
    (va_x_v24:quad32) (va_x_v25:quad32) (va_x_v26:quad32) (va_x_v28:quad32) (va_x_v29:quad32)
    (va_x_v3:quad32) (va_x_v30:quad32) (va_x_v31:quad32) (va_x_v4:quad32) (va_x_v5:quad32)
    (va_x_v6:quad32) (va_x_v7:quad32) (va_x_v8:quad32) (va_x_v9:quad32) (count:nat) . let va_sM =
    va_upd_vec 9 va_x_v9 (va_upd_vec 8 va_x_v8 (va_upd_vec 7 va_x_v7 (va_upd_vec 6 va_x_v6
    (va_upd_vec 5 va_x_v5 (va_upd_vec 4 va_x_v4 (va_upd_vec 31 va_x_v31 (va_upd_vec 30 va_x_v30
    (va_upd_vec 3 va_x_v3 (va_upd_vec 29 va_x_v29 (va_upd_vec 28 va_x_v28 (va_upd_vec 26 va_x_v26
    (va_upd_vec 25 va_x_v25 (va_upd_vec 24 va_x_v24 (va_upd_vec 23 va_x_v23 (va_upd_vec 22 va_x_v22
    (va_upd_vec 21 va_x_v21 (va_upd_vec 20 va_x_v20 (va_upd_vec 2 va_x_v2 (va_upd_vec 19 va_x_v19
    (va_upd_vec 18 va_x_v18 (va_upd_vec 17 va_x_v17 (va_upd_vec 16 va_x_v16 (va_upd_vec 15 va_x_v15
    (va_upd_vec 14 va_x_v14 (va_upd_vec 13 va_x_v13 (va_upd_vec 12 va_x_v12 (va_upd_vec 11 va_x_v11
    (va_upd_vec 10 va_x_v10 (va_upd_vec 1 va_x_v1 (va_upd_vec 0 va_x_v0 (va_upd_reg 6 va_x_r6
    (va_upd_reg 5 va_x_r5 (va_upd_reg 4 va_x_r4 (va_upd_ok va_x_ok (va_upd_cr0 va_x_cr0
    va_s0))))))))))))))))))))))))))))))))))) in va_get_ok va_sM /\
    Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_sM) (va_get_reg 4 va_old)
    va_in_in_b (4 `op_Multiply` va_get_reg 5 va_old) (va_get_mem_layout va_sM) Secret /\
    Vale.PPC64LE.Decls.validSrcAddrs128 (va_get_mem_heaplet 0 va_sM) (va_get_reg 6 va_sM) va_in_k_b
    16 (va_get_mem_layout va_sM) Secret /\ Vale.PPC64LE.Decls.validSrcAddrsOffset128
    (va_get_mem_heaplet 0 va_sM) (va_get_reg 6 va_sM) va_in_k_b 13 3 (va_get_mem_layout va_sM)
    Secret /\ va_get_reg 4 va_old + 64 `op_Multiply` va_get_reg 5 va_old < pow2_64 /\ va_get_reg 6
    va_sM + 256 < pow2_64 /\ va_get_reg 5 va_sM == va_get_reg 5 va_old - count /\ va_get_reg 4
    va_sM == va_get_reg 4 va_old + 64 `op_Multiply` count /\ Vale.SHA.PPC64LE.SHA_helpers.k_reqs
    (Vale.PPC64LE.Decls.buffer128_as_seq (va_get_mem_heaplet 0 va_sM) va_in_k_b) /\ (let input_LE =
    FStar.Seq.Base.slice #Vale.PPC64LE.Machine_s.quad32 (Vale.PPC64LE.Decls.buffer128_as_seq
    (va_get_mem_heaplet 0 va_sM) va_in_in_b) 0 (count `op_Multiply` 4) in let input_BE =
    Vale.Arch.Types.reverse_bytes_quad32_seq input_LE in
    Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_sM) (va_get_vec 17
    va_sM) (va_get_vec 18 va_sM) (va_get_vec 19 va_sM) (va_get_vec 20 va_sM) (va_get_vec 21 va_sM)
    (va_get_vec 22 va_sM) (va_get_vec 23 va_sM) == Vale.SHA.PPC64LE.SHA_helpers.update_multi_quads
    input_BE va_in_hash_orig) /\ precedes_wrap (va_get_reg 5 va_sM) (va_get_reg 5 va_s0) ==> va_k
    va_sM ((count))))


val va_wpProof_Loop_body0 : va_old:va_state -> va_in_hash_orig:hash256 -> va_in_in_b:buffer128 ->
  va_in_k_b:buffer128 -> va_in_count:nat -> va_s0:va_state -> va_k:(va_state -> nat -> Type0)
  -> Ghost (va_state & va_fuel & nat)
  (requires (va_t_require va_s0 /\ va_wp_Loop_body0 va_old va_in_hash_orig va_in_in_b va_in_k_b
    va_in_count va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Loop_body0 ()) ([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 31; va_Mod_vec
    30; va_Mod_vec 3; va_Mod_vec 29; va_Mod_vec 28; 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 2; 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 1; va_Mod_vec 0; va_Mod_reg 6;
    va_Mod_reg 5; va_Mod_reg 4; va_Mod_ok; va_Mod_cr0]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Loop_body0 va_old va_in_hash_orig va_in_in_b va_in_k_b va_in_count va_s0 va_k =
  let (va_sM, va_f0, count) = va_lemma_Loop_body0 (va_code_Loop_body0 ()) va_s0 va_old
    va_in_hash_orig va_in_in_b va_in_k_b va_in_count in
  va_lemma_upd_update va_sM;
  assert (va_state_eq 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 31 va_sM
    (va_update_vec 30 va_sM (va_update_vec 3 va_sM (va_update_vec 29 va_sM (va_update_vec 28 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 2 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 1 va_sM (va_update_vec 0 va_sM
    (va_update_reg 6 va_sM (va_update_reg 5 va_sM (va_update_reg 4 va_sM (va_update_ok va_sM
    (va_update_cr0 va_sM va_s0)))))))))))))))))))))))))))))))))))));
  va_lemma_norm_mods ([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 31; va_Mod_vec 30; va_Mod_vec 3; va_Mod_vec 29; va_Mod_vec 28;
    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 2; 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 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 5; va_Mod_reg 4; va_Mod_ok; va_Mod_cr0])
    va_sM va_s0;
  let va_g = (count) in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Loop_body0 (va_old:va_state) (va_in_hash_orig:hash256) (va_in_in_b:buffer128)
  (va_in_k_b:buffer128) (va_in_count:nat) : (va_quickCode nat (va_code_Loop_body0 ())) =
  (va_QProc (va_code_Loop_body0 ()) ([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 31; va_Mod_vec 30; va_Mod_vec 3; va_Mod_vec 29;
    va_Mod_vec 28; 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 2; 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 1; va_Mod_vec 0; va_Mod_reg 6; va_Mod_reg 5; va_Mod_reg 4; va_Mod_ok;
    va_Mod_cr0]) (va_wp_Loop_body0 va_old va_in_hash_orig va_in_in_b va_in_k_b va_in_count)
    (va_wpProof_Loop_body0 va_old va_in_hash_orig va_in_in_b va_in_k_b va_in_count))
//--
//-- Loop_while0

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