val va_qcode_Callee_save_registers (va_mods: va_mods_t) (win: bool)
    : (va_quickCode unit (va_code_Callee_save_registers win))
let va_qcode_Callee_save_registers (va_mods:va_mods_t) (win:bool) : (va_quickCode unit
  (va_code_Callee_save_registers win)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 73 column 15 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_qInlineIf va_mods win (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 74 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 15) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 75 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 14) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 76 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 13) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 77 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 12) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 78 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 11) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 79 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 10) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 80 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 9) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 81 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 8) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 82 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 7) (va_op_reg_opr64_reg64 rRax)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 83 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_PushXmm (va_op_xmm_xmm 6) (va_op_reg_opr64_reg64 rRax)) (va_QEmpty (())))))))))))))
    (qblock va_mods (fun (va_s:va_state) -> va_QEmpty (())))) (fun (va_s:va_state) va_g -> va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 85 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_Push (va_op_reg_opr64_reg64 rR15)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 86 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_Push (va_op_reg_opr64_reg64 rR14)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 87 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_Push (va_op_reg_opr64_reg64 rR13)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 88 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_Push (va_op_reg_opr64_reg64 rR12)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 89 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_Push (va_op_reg_opr64_reg64 rRsi)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 90 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_Push (va_op_reg_opr64_reg64 rRdi)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 91 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_Push (va_op_reg_opr64_reg64 rRbp)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 92 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_quick_Push (va_op_reg_opr64_reg64 rRbx)) (va_QEmpty (()))))))))))))
val va_qcode_Callee_save_registers (va_mods: va_mods_t) (win: bool)
    : (va_quickCode unit (va_code_Callee_save_registers win))
let va_qcode_Callee_save_registers (va_mods: va_mods_t) (win: bool)
    : (va_quickCode unit (va_code_Callee_save_registers win)) =
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        va_QBind va_range1
          "***** PRECONDITION NOT MET AT line 73 column 15 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
          (va_qInlineIf va_mods
              win
              (qblock va_mods
                  (fun (va_s: va_state) ->
                      va_QSeq va_range1
                        "***** PRECONDITION NOT MET AT line 74 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                        (va_quick_PushXmm (va_op_xmm_xmm 15) (va_op_reg_opr64_reg64 rRax))
                        (va_QSeq va_range1
                            "***** PRECONDITION NOT MET AT line 75 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                            (va_quick_PushXmm (va_op_xmm_xmm 14) (va_op_reg_opr64_reg64 rRax))
                            (va_QSeq va_range1
                                "***** PRECONDITION NOT MET AT line 76 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                (va_quick_PushXmm (va_op_xmm_xmm 13) (va_op_reg_opr64_reg64 rRax))
                                (va_QSeq va_range1
                                    "***** PRECONDITION NOT MET AT line 77 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                    (va_quick_PushXmm (va_op_xmm_xmm 12)
                                        (va_op_reg_opr64_reg64 rRax))
                                    (va_QSeq va_range1
                                        "***** PRECONDITION NOT MET AT line 78 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                        (va_quick_PushXmm (va_op_xmm_xmm 11)
                                            (va_op_reg_opr64_reg64 rRax))
                                        (va_QSeq va_range1
                                            "***** PRECONDITION NOT MET AT line 79 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                            (va_quick_PushXmm (va_op_xmm_xmm 10)
                                                (va_op_reg_opr64_reg64 rRax))
                                            (va_QSeq va_range1
                                                "***** PRECONDITION NOT MET AT line 80 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                                (va_quick_PushXmm (va_op_xmm_xmm 9)
                                                    (va_op_reg_opr64_reg64 rRax))
                                                (va_QSeq va_range1
                                                    "***** PRECONDITION NOT MET AT line 81 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                                    (va_quick_PushXmm (va_op_xmm_xmm 8)
                                                        (va_op_reg_opr64_reg64 rRax))
                                                    (va_QSeq va_range1
                                                        "***** PRECONDITION NOT MET AT line 82 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                                        (va_quick_PushXmm (va_op_xmm_xmm 7)
                                                            (va_op_reg_opr64_reg64 rRax))
                                                        (va_QSeq va_range1
                                                            "***** PRECONDITION NOT MET AT line 83 column 16 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                                            (va_quick_PushXmm (va_op_xmm_xmm 6)
                                                                (va_op_reg_opr64_reg64 rRax))
                                                            (va_QEmpty (())))))))))))))
              (qblock va_mods (fun (va_s: va_state) -> va_QEmpty (()))))
          (fun (va_s: va_state) va_g ->
              va_QSeq va_range1
                "***** PRECONDITION NOT MET AT line 85 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                (va_quick_Push (va_op_reg_opr64_reg64 rR15))
                (va_QSeq va_range1
                    "***** PRECONDITION NOT MET AT line 86 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                    (va_quick_Push (va_op_reg_opr64_reg64 rR14))
                    (va_QSeq va_range1
                        "***** PRECONDITION NOT MET AT line 87 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                        (va_quick_Push (va_op_reg_opr64_reg64 rR13))
                        (va_QSeq va_range1
                            "***** PRECONDITION NOT MET AT line 88 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                            (va_quick_Push (va_op_reg_opr64_reg64 rR12))
                            (va_QSeq va_range1
                                "***** PRECONDITION NOT MET AT line 89 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                (va_quick_Push (va_op_reg_opr64_reg64 rRsi))
                                (va_QSeq va_range1
                                    "***** PRECONDITION NOT MET AT line 90 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                    (va_quick_Push (va_op_reg_opr64_reg64 rRdi))
                                    (va_QSeq va_range1
                                        "***** PRECONDITION NOT MET AT line 91 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                        (va_quick_Push (va_op_reg_opr64_reg64 rRbp))
                                        (va_QSeq va_range1
                                            "***** PRECONDITION NOT MET AT line 92 column 9 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
                                            (va_quick_Push (va_op_reg_opr64_reg64 rRbx))
                                            (va_QEmpty (()))))))))))))
Vale.X64.Stack.fst.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsVector.fsti.checked Vale.X64.InsStack.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.X64.Stack.fst
Vale.X64.QuickCode.va_mods_t Prims.bool Vale.X64.QuickCodes.qblock Prims.unit Prims.Cons Vale.X64.Decls.va_code Vale.X64.QuickCodes.if_code Vale.X64.QuickCodes.block Vale.X64.InsStack.va_code_PushXmm Vale.X64.Decls.va_op_xmm_xmm Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRax Prims.Nil Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.InsStack.va_code_Push Vale.X64.Machine_s.rR15 Vale.X64.Machine_s.rR14 Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rR12 Vale.X64.Machine_s.rRsi Vale.X64.Machine_s.rRdi Vale.X64.Machine_s.rRbp Vale.X64.Machine_s.rRbx Vale.X64.Decls.va_state Vale.X64.QuickCodes.va_QBind Vale.X64.QuickCodes.va_range1 Vale.X64.QuickCodes.va_qInlineIf Vale.X64.QuickCodes.va_QSeq Vale.X64.InsStack.va_quick_PushXmm Vale.X64.QuickCodes.va_QEmpty Vale.X64.QuickCodes.quickCodes Vale.X64.InsStack.va_quick_Push Vale.X64.State.vale_state Vale.X64.QuickCode.va_quickCode Vale.X64.Stack.va_code_Callee_save_registers
module Vale.X64.Stack
//open Vale.Def.Opaque_s
open FStar.Seq
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Types_s
open Vale.Arch.Types
//open Vale.AES.GCM_helpers
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsStack
open Vale.X64.InsVector
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.X64.CPU_Features_s
#reset-options "--z3rlimit 30"
//-- Callee_save_registers

[@ "opaque_to_smt" va_qattr]
let va_code_Callee_save_registers win =
  (va_Block (va_CCons (if win then va_Block (va_CCons (va_code_PushXmm (va_op_xmm_xmm 15)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 14)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 13)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 12)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 11)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 10)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 9)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 8)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 7)
    (va_op_reg_opr64_reg64 rRax)) (va_CCons (va_code_PushXmm (va_op_xmm_xmm 6)
    (va_op_reg_opr64_reg64 rRax)) (va_CNil ()))))))))))) else va_Block (va_CNil ())) (va_CCons
    (va_code_Push (va_op_reg_opr64_reg64 rR15)) (va_CCons (va_code_Push (va_op_reg_opr64_reg64
    rR14)) (va_CCons (va_code_Push (va_op_reg_opr64_reg64 rR13)) (va_CCons (va_code_Push
    (va_op_reg_opr64_reg64 rR12)) (va_CCons (va_code_Push (va_op_reg_opr64_reg64 rRsi)) (va_CCons
    (va_code_Push (va_op_reg_opr64_reg64 rRdi)) (va_CCons (va_code_Push (va_op_reg_opr64_reg64
    rRbp)) (va_CCons (va_code_Push (va_op_reg_opr64_reg64 rRbx)) (va_CNil ())))))))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Callee_save_registers win =
  (va_pbool_and (if win then va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 15)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 14)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 13)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 12)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 11)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 10)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 9)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 8)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 7)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PushXmm (va_op_xmm_xmm 6)
    (va_op_reg_opr64_reg64 rRax)) (va_ttrue ())))))))))) else va_ttrue ()) (va_pbool_and
    (va_codegen_success_Push (va_op_reg_opr64_reg64 rR15)) (va_pbool_and (va_codegen_success_Push
    (va_op_reg_opr64_reg64 rR14)) (va_pbool_and (va_codegen_success_Push (va_op_reg_opr64_reg64
    rR13)) (va_pbool_and (va_codegen_success_Push (va_op_reg_opr64_reg64 rR12)) (va_pbool_and
    (va_codegen_success_Push (va_op_reg_opr64_reg64 rRsi)) (va_pbool_and (va_codegen_success_Push
    (va_op_reg_opr64_reg64 rRdi)) (va_pbool_and (va_codegen_success_Push (va_op_reg_opr64_reg64
    rRbp)) (va_pbool_and (va_codegen_success_Push (va_op_reg_opr64_reg64 rRbx)) (va_ttrue
    ()))))))))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Callee_save_registers (va_mods:va_mods_t) (win:bool) : (va_quickCode unit
val va_qcode_Callee_save_registers (va_mods: va_mods_t) (win: bool)
    : (va_quickCode unit (va_code_Callee_save_registers win))
va_mods: Vale.X64.QuickCode.va_mods_t -> win: Prims.bool
  -> Vale.X64.QuickCode.va_quickCode Prims.unit (Vale.X64.Stack.va_code_Callee_save_registers win)