val va_codegen_success_Callee_save_registers : win:bool -> Tot va_pbool
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
    ()))))))))))
val va_codegen_success_Callee_save_registers : win:bool -> Tot va_pbool
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 ()))))))))))
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
Prims.bool Vale.X64.Decls.va_pbool_and Vale.X64.InsStack.va_codegen_success_PushXmm Vale.X64.Decls.va_op_xmm_xmm Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRax Vale.X64.Decls.va_ttrue Vale.X64.Decls.va_pbool Vale.X64.InsStack.va_codegen_success_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
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]
val va_codegen_success_Callee_save_registers : win:bool -> Tot va_pbool
win: Prims.bool -> Vale.X64.Decls.va_pbool