val va_qcode_Preamble (va_mods: va_mods_t) (ctx_b: buffer128)
    : (va_quickCode unit (va_code_Preamble ()))
let va_qcode_Preamble (va_mods:va_mods_t) (ctx_b:buffer128) : (va_quickCode unit (va_code_Preamble
  ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (dcba:Vale.PPC64LE.Machine_s.quad32) = Vale.PPC64LE.Decls.buffer128_read ctx_b 0
    (va_get_mem_heaplet 0 va_s) in let (hgfe:Vale.PPC64LE.Machine_s.quad32) =
    Vale.PPC64LE.Decls.buffer128_read ctx_b 1 (va_get_mem_heaplet 0 va_s) in let
    (a:Vale.Def.Types_s.nat32) = Vale.Def.Words_s.__proj__Mkfour__item__lo0 dcba in let
    (b:Vale.Def.Types_s.nat32) = Vale.Def.Words_s.__proj__Mkfour__item__lo1 dcba in let
    (c:Vale.Def.Types_s.nat32) = Vale.Def.Words_s.__proj__Mkfour__item__hi2 dcba in let
    (d:Vale.Def.Types_s.nat32) = Vale.Def.Words_s.__proj__Mkfour__item__hi3 dcba in let
    (e:Vale.Def.Types_s.nat32) = Vale.Def.Words_s.__proj__Mkfour__item__lo0 hgfe in let
    (f:Vale.Def.Types_s.nat32) = Vale.Def.Words_s.__proj__Mkfour__item__lo1 hgfe in let
    (g:Vale.Def.Types_s.nat32) = Vale.Def.Words_s.__proj__Mkfour__item__hi2 hgfe in let
    (h:Vale.Def.Types_s.nat32) = Vale.Def.Words_s.__proj__Mkfour__item__hi3 hgfe in va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 91 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_LoadImm64 (va_op_reg_opr_reg 10) 16) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 92 column 25 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 16)
    (va_op_reg_opr_reg 3) Secret ctx_b 0) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 93 column 31 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_Load128_word4_buffer_index (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 20)
    (va_op_reg_opr_reg 3) (va_op_reg_opr_reg 10) Secret ctx_b 1) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 95 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 4)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 96 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 18) (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 8)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 97 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 12)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 98 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 21) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 4)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 99 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 8)
    (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 100 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (va_quick_Vsldoi (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 12) (fun
    (va_s:va_state) _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 102 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (FStar.Seq.Base.equal #Vale.SHA.PPC64LE.SHA_helpers.word
    (Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash a b c d e f g h)
    (Vale.SHA.PPC64LE.SHA_helpers.make_ordered_hash dcba hgfe)) (va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 103 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
    (FStar.Seq.Base.equal #Vale.SHA.PPC64LE.SHA_helpers.word
    (Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash a b c d e f g h)
    (Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 (va_get_vec 16 va_s) (va_get_vec 17
    va_s) (va_get_vec 18 va_s) (va_get_vec 19 va_s) (va_get_vec 20 va_s) (va_get_vec 21 va_s)
    (va_get_vec 22 va_s) (va_get_vec 23 va_s))) (va_QEmpty (()))))))))))))))
val va_qcode_Preamble (va_mods: va_mods_t) (ctx_b: buffer128)
    : (va_quickCode unit (va_code_Preamble ()))
let va_qcode_Preamble (va_mods: va_mods_t) (ctx_b: buffer128)
    : (va_quickCode unit (va_code_Preamble ())) =
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        let dcba:Vale.PPC64LE.Machine_s.quad32 =
          Vale.PPC64LE.Decls.buffer128_read ctx_b 0 (va_get_mem_heaplet 0 va_s)
        in
        let hgfe:Vale.PPC64LE.Machine_s.quad32 =
          Vale.PPC64LE.Decls.buffer128_read ctx_b 1 (va_get_mem_heaplet 0 va_s)
        in
        let a:Vale.Def.Types_s.nat32 = Vale.Def.Words_s.__proj__Mkfour__item__lo0 dcba in
        let b:Vale.Def.Types_s.nat32 = Vale.Def.Words_s.__proj__Mkfour__item__lo1 dcba in
        let c:Vale.Def.Types_s.nat32 = Vale.Def.Words_s.__proj__Mkfour__item__hi2 dcba in
        let d:Vale.Def.Types_s.nat32 = Vale.Def.Words_s.__proj__Mkfour__item__hi3 dcba in
        let e:Vale.Def.Types_s.nat32 = Vale.Def.Words_s.__proj__Mkfour__item__lo0 hgfe in
        let f:Vale.Def.Types_s.nat32 = Vale.Def.Words_s.__proj__Mkfour__item__lo1 hgfe in
        let g:Vale.Def.Types_s.nat32 = Vale.Def.Words_s.__proj__Mkfour__item__hi2 hgfe in
        let h:Vale.Def.Types_s.nat32 = Vale.Def.Words_s.__proj__Mkfour__item__hi3 hgfe in
        va_QSeq va_range1
          "***** PRECONDITION NOT MET AT line 91 column 14 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
          (va_quick_LoadImm64 (va_op_reg_opr_reg 10) 16)
          (va_QSeq va_range1
              "***** PRECONDITION NOT MET AT line 92 column 25 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
              (va_quick_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0)
                  (va_op_vec_opr_vec 16)
                  (va_op_reg_opr_reg 3)
                  Secret
                  ctx_b
                  0)
              (va_QSeq va_range1
                  "***** PRECONDITION NOT MET AT line 93 column 31 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                  (va_quick_Load128_word4_buffer_index (va_op_heaplet_mem_heaplet 0)
                      (va_op_vec_opr_vec 20)
                      (va_op_reg_opr_reg 3)
                      (va_op_reg_opr_reg 10)
                      Secret
                      ctx_b
                      1)
                  (va_QSeq va_range1
                      "***** PRECONDITION NOT MET AT line 95 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                      (va_quick_Vsldoi (va_op_vec_opr_vec 17)
                          (va_op_vec_opr_vec 16)
                          (va_op_vec_opr_vec 16)
                          4)
                      (va_QSeq va_range1
                          "***** PRECONDITION NOT MET AT line 96 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                          (va_quick_Vsldoi (va_op_vec_opr_vec 18)
                              (va_op_vec_opr_vec 16)
                              (va_op_vec_opr_vec 16)
                              8)
                          (va_QSeq va_range1
                              "***** PRECONDITION NOT MET AT line 97 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                              (va_quick_Vsldoi (va_op_vec_opr_vec 19)
                                  (va_op_vec_opr_vec 16)
                                  (va_op_vec_opr_vec 16)
                                  12)
                              (va_QSeq va_range1
                                  "***** PRECONDITION NOT MET AT line 98 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                                  (va_quick_Vsldoi (va_op_vec_opr_vec 21)
                                      (va_op_vec_opr_vec 20)
                                      (va_op_vec_opr_vec 20)
                                      4)
                                  (va_QSeq va_range1
                                      "***** PRECONDITION NOT MET AT line 99 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                                      (va_quick_Vsldoi (va_op_vec_opr_vec 22)
                                          (va_op_vec_opr_vec 20)
                                          (va_op_vec_opr_vec 20)
                                          8)
                                      (va_QBind va_range1
                                          "***** PRECONDITION NOT MET AT line 100 column 11 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                                          (va_quick_Vsldoi (va_op_vec_opr_vec 23)
                                              (va_op_vec_opr_vec 20)
                                              (va_op_vec_opr_vec 20)
                                              12)
                                          (fun (va_s: va_state) _ ->
                                              va_qAssert va_range1
                                                "***** PRECONDITION NOT MET AT line 102 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                                                (FStar.Seq.Base.equal #Vale.SHA.PPC64LE.SHA_helpers.word
                                                    (Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash
                                                        a
                                                        b
                                                        c
                                                        d
                                                        e
                                                        f
                                                        g
                                                        h)
                                                    (Vale.SHA.PPC64LE.SHA_helpers.make_ordered_hash dcba
                                                        hgfe))
                                                (va_qAssert va_range1
                                                    "***** PRECONDITION NOT MET AT line 103 column 5 of file /home/gebner/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha/Vale.SHA.PPC64LE.vaf *****"
                                                    (FStar.Seq.Base.equal #Vale.SHA.PPC64LE.SHA_helpers.word
                                                        (Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash
                                                            a
                                                            b
                                                            c
                                                            d
                                                            e
                                                            f
                                                            g
                                                            h)
                                                        (Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32
                                                            (va_get_vec 16 va_s)
                                                            (va_get_vec 17 va_s)
                                                            (va_get_vec 18 va_s)
                                                            (va_get_vec 19 va_s)
                                                            (va_get_vec 20 va_s)
                                                            (va_get_vec 21 va_s)
                                                            (va_get_vec 22 va_s)
                                                            (va_get_vec 23 va_s)))
                                                    (va_QEmpty (()))))))))))))))
Vale.SHA.PPC64LE.fst.checked
Vale.SHA2.Wrapper.fsti.checked Vale.SHA.PPC64LE.SHA_helpers.fsti.checked Vale.SHA.PPC64LE.Loop.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.UInt8.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.SHA.PPC64LE.fst
Vale.PPC64LE.QuickCode.va_mods_t Vale.PPC64LE.Memory.buffer128 Vale.PPC64LE.QuickCodes.qblock Prims.unit Prims.Cons Vale.PPC64LE.Decls.va_code Vale.PPC64LE.InsBasic.va_code_LoadImm64 Vale.PPC64LE.Decls.va_op_reg_opr_reg Vale.PPC64LE.InsVector.va_code_Load128_word4_buffer Vale.PPC64LE.Decls.va_op_heaplet_mem_heaplet Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.Arch.HeapTypes_s.Secret Vale.PPC64LE.InsVector.va_code_Load128_word4_buffer_index Vale.PPC64LE.InsVector.va_code_Vsldoi Prims.Nil Vale.PPC64LE.Machine_s.precode Vale.PPC64LE.Decls.ins Vale.PPC64LE.Decls.ocmp Vale.PPC64LE.Decls.va_state Vale.PPC64LE.QuickCodes.va_QSeq Vale.PPC64LE.QuickCodes.va_range1 Vale.PPC64LE.InsBasic.va_quick_LoadImm64 Vale.PPC64LE.InsVector.va_quick_Load128_word4_buffer Vale.PPC64LE.InsVector.va_quick_Load128_word4_buffer_index Vale.PPC64LE.InsVector.va_quick_Vsldoi Vale.PPC64LE.QuickCodes.va_QBind Vale.PPC64LE.QuickCodes.va_qAssert FStar.Seq.Base.equal Vale.SHA.PPC64LE.SHA_helpers.word Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash Vale.SHA.PPC64LE.SHA_helpers.make_ordered_hash Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_quad32 Vale.PPC64LE.Decls.va_get_vec Vale.PPC64LE.QuickCodes.va_QEmpty Vale.PPC64LE.QuickCodes.quickCodes Vale.Def.Words_s.nat32 Vale.Def.Words_s.__proj__Mkfour__item__hi3 Vale.Def.Types_s.nat32 Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__lo1 Vale.Def.Words_s.__proj__Mkfour__item__lo0 Vale.Def.Types_s.quad32 Vale.PPC64LE.Decls.buffer128_read Vale.PPC64LE.Decls.va_get_mem_heaplet Vale.PPC64LE.Machine_s.state Vale.PPC64LE.QuickCode.va_quickCode Vale.SHA.PPC64LE.va_code_Preamble
module Vale.SHA.PPC64LE
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.Loop
open Vale.SHA2.Wrapper
#reset-options "--z3rlimit 2000"
//-- Preamble

val va_code_Preamble : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Preamble () =
  (va_Block (va_CCons (va_code_LoadImm64 (va_op_reg_opr_reg 10) 16) (va_CCons
    (va_code_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 16)
    (va_op_reg_opr_reg 3) Secret) (va_CCons (va_code_Load128_word4_buffer_index
    (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 20) (va_op_reg_opr_reg 3) (va_op_reg_opr_reg
    10) Secret) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 17) (va_op_vec_opr_vec 16)
    (va_op_vec_opr_vec 16) 4) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 18) (va_op_vec_opr_vec
    16) (va_op_vec_opr_vec 16) 8) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec 19)
    (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 12) (va_CCons (va_code_Vsldoi (va_op_vec_opr_vec
    21) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 4) (va_CCons (va_code_Vsldoi
    (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 8) (va_CCons
    (va_code_Vsldoi (va_op_vec_opr_vec 23) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 12)
    (va_CNil ())))))))))))

val va_codegen_success_Preamble : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Preamble () =
  (va_pbool_and (va_codegen_success_LoadImm64 (va_op_reg_opr_reg 10) 16) (va_pbool_and
    (va_codegen_success_Load128_word4_buffer (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 16)
    (va_op_reg_opr_reg 3) Secret) (va_pbool_and (va_codegen_success_Load128_word4_buffer_index
    (va_op_heaplet_mem_heaplet 0) (va_op_vec_opr_vec 20) (va_op_reg_opr_reg 3) (va_op_reg_opr_reg
    10) Secret) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 17) (va_op_vec_opr_vec
    16) (va_op_vec_opr_vec 16) 4) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 18)
    (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 8) (va_pbool_and (va_codegen_success_Vsldoi
    (va_op_vec_opr_vec 19) (va_op_vec_opr_vec 16) (va_op_vec_opr_vec 16) 12) (va_pbool_and
    (va_codegen_success_Vsldoi (va_op_vec_opr_vec 21) (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20)
    4) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 22) (va_op_vec_opr_vec 20)
    (va_op_vec_opr_vec 20) 8) (va_pbool_and (va_codegen_success_Vsldoi (va_op_vec_opr_vec 23)
    (va_op_vec_opr_vec 20) (va_op_vec_opr_vec 20) 12) (va_ttrue ()))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Preamble (va_mods:va_mods_t) (ctx_b:buffer128) : (va_quickCode unit (va_code_Preamble
val va_qcode_Preamble (va_mods: va_mods_t) (ctx_b: buffer128)
    : (va_quickCode unit (va_code_Preamble ()))
va_mods: Vale.PPC64LE.QuickCode.va_mods_t -> ctx_b: Vale.PPC64LE.Memory.buffer128
  -> Vale.PPC64LE.QuickCode.va_quickCode Prims.unit (Vale.SHA.PPC64LE.va_code_Preamble ())