val va_codegen_success_Callee_restore_registers : win:bool -> Tot va_pbool
let va_codegen_success_Callee_restore_registers win =
  (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rRbx)) (va_pbool_and
    (va_codegen_success_Pop (va_op_dst_opr64_reg64 rRbp)) (va_pbool_and (va_codegen_success_Pop
    (va_op_dst_opr64_reg64 rRdi)) (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64
    rRsi)) (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rR12)) (va_pbool_and
    (va_codegen_success_Pop (va_op_dst_opr64_reg64 rR13)) (va_pbool_and (va_codegen_success_Pop
    (va_op_dst_opr64_reg64 rR14)) (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64
    rR15)) (va_pbool_and (if win then va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 6)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 7)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 8)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 9)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 10)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 11)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 12)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 13)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 14)
    (va_op_reg_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 15)
    (va_op_reg_opr64_reg64 rRax)) (va_ttrue ())))))))))) else va_ttrue ()) (va_ttrue ()))))))))))
val va_codegen_success_Callee_restore_registers : win:bool -> Tot va_pbool
let va_codegen_success_Callee_restore_registers win =
(va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rRbx))
    (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rRbp))
        (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rRdi))
            (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rRsi))
                (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rR12))
                    (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rR13))
                        (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rR14))
                            (va_pbool_and (va_codegen_success_Pop (va_op_dst_opr64_reg64 rR15))
                                (va_pbool_and (if win
                                      then
                                        va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 6)
                                              (va_op_reg_opr64_reg64 rRax))
                                          (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm 7)
                                                  (va_op_reg_opr64_reg64 rRax))
                                              (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm
                                                          8)
                                                      (va_op_reg_opr64_reg64 rRax))
                                                  (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm
                                                              9)
                                                          (va_op_reg_opr64_reg64 rRax))
                                                      (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm
                                                                  10)
                                                              (va_op_reg_opr64_reg64 rRax))
                                                          (va_pbool_and (va_codegen_success_PopXmm (va_op_xmm_xmm
                                                                      11)
                                                                  (va_op_reg_opr64_reg64 rRax))
                                                              (va_pbool_and (va_codegen_success_PopXmm
                                                                      (va_op_xmm_xmm 12)
                                                                      (va_op_reg_opr64_reg64 rRax))
                                                                  (va_pbool_and (va_codegen_success_PopXmm
                                                                          (va_op_xmm_xmm 13)
                                                                          (va_op_reg_opr64_reg64 rRax
                                                                            ))
                                                                      (va_pbool_and (va_codegen_success_PopXmm
                                                                              (va_op_xmm_xmm 14)
                                                                              (va_op_reg_opr64_reg64
                                                                                  rRax))
                                                                          (va_pbool_and (va_codegen_success_PopXmm
                                                                                  (va_op_xmm_xmm 15)
                                                                                  (va_op_reg_opr64_reg64
                                                                                      rRax))
                                                                              (va_ttrue ()))))))))))
                                      else va_ttrue ())
                                    (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_Pop Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Machine_s.rRbx Vale.X64.Machine_s.rRbp Vale.X64.Machine_s.rRdi Vale.X64.Machine_s.rRsi Vale.X64.Machine_s.rR12 Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rR14 Vale.X64.Machine_s.rR15 Vale.X64.InsStack.va_codegen_success_PopXmm 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
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
  (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 (()))))))))))))

[@"opaque_to_smt"]
let va_lemma_Callee_save_registers va_b0 va_s0 win =
  let (va_mods:va_mods_t) = [va_Mod_stackTaint; va_Mod_reg64 rRax; va_Mod_reg64 rRsp; va_Mod_stack;
    va_Mod_ok] in
  let va_qc = va_qcode_Callee_save_registers va_mods win in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Callee_save_registers win) va_qc va_s0
    (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 31 column 1 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 41 column 152 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (forall i . Vale.X64.Stack_i.valid_src_stack64 i (va_get_stack va_s0) /\ va_get_reg64 rRsp
    va_sM + va_if win (fun _ -> 224) (fun _ -> 64) <= i ==> Vale.X64.Stack_i.load_stack64 i
    (va_get_stack va_sM) == Vale.X64.Stack_i.load_stack64 i (va_get_stack va_s0)) /\ label
    va_range1
    "***** POSTCONDITION NOT MET AT line 43 column 40 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_reg64 rRbx va_sM == Vale.X64.Stack_i.load_stack64 (va_get_reg64 rRsp va_sM)
    (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 44 column 44 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_reg64 rRbp va_sM == Vale.X64.Stack_i.load_stack64 (va_get_reg64 rRsp va_sM + 8)
    (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 45 column 45 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_reg64 rRdi va_sM == Vale.X64.Stack_i.load_stack64 (va_get_reg64 rRsp va_sM + 16)
    (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 46 column 45 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_reg64 rRsi va_sM == Vale.X64.Stack_i.load_stack64 (va_get_reg64 rRsp va_sM + 24)
    (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 47 column 45 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_reg64 rR12 va_sM == Vale.X64.Stack_i.load_stack64 (va_get_reg64 rRsp va_sM + 32)
    (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 48 column 45 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_reg64 rR13 va_sM == Vale.X64.Stack_i.load_stack64 (va_get_reg64 rRsp va_sM + 40)
    (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 49 column 45 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_reg64 rR14 va_sM == Vale.X64.Stack_i.load_stack64 (va_get_reg64 rRsp va_sM + 48)
    (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 50 column 45 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (va_get_reg64 rR15 va_sM == Vale.X64.Stack_i.load_stack64 (va_get_reg64 rRsp va_sM + 56)
    (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 52 column 60 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 6 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 64) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 53 column 60 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 6 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 72) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 54 column 60 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 7 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 80) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 55 column 60 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 7 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 88) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 56 column 60 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 8 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 96) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 57 column 61 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 8 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 104) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 58 column 61 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 9 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 112) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 59 column 61 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 9 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 120) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 60 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 10 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 128) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 61 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 10 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 136) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 62 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 11 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 144) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 63 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 11 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 152) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 64 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 12 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 160) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 65 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 12 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 168) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 66 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 13 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 176) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 67 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 13 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 184) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 68 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 14 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 192) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 69 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 14 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 200) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 70 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.hi64 (va_get_xmm 15 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 208) (va_get_stack va_sM)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 71 column 62 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/Vale.X64.Stack.vaf *****"
    (win ==> Vale.Arch.Types.lo64 (va_get_xmm 15 va_sM) == Vale.X64.Stack_i.load_stack64
    (va_get_reg64 rRsp va_sM + 216) (va_get_stack va_sM))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_stackTaint; va_Mod_reg64 rRax; va_Mod_reg64 rRsp; va_Mod_stack;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Callee_save_registers win va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Callee_save_registers (va_code_Callee_save_registers win) va_s0 win
    in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_stackTaint va_sM (va_update_reg64 rRax va_sM
    (va_update_reg64 rRsp va_sM (va_update_stack va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_stackTaint; va_Mod_reg64 rRax; va_Mod_reg64 rRsp; va_Mod_stack])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Callee_restore_registers

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

[@ "opaque_to_smt" va_qattr]
val va_codegen_success_Callee_restore_registers : win:bool -> Tot va_pbool
win: Prims.bool -> Vale.X64.Decls.va_pbool