val va_codegen_success_Fast_mul1 : va_dummy:unit -> Tot va_pbool
let va_codegen_success_Fast_mul1 () =
  (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rR9) (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 0 Secret)) (va_pbool_and
    (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi)
    (va_op_reg_opr64_reg64 rR8) 0 Secret) (va_pbool_and (va_codegen_success_Xor64
    (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rR11) (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 8 Secret)) (va_pbool_and
    (va_codegen_success_Add64Wrap (va_op_dst_opr64_reg64 rR10) (va_op_opr64_reg64 rR9))
    (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) 8 Secret) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rR13) (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 16 Secret)) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx) (va_op_opr64_reg64 rR11))
    (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRbx) 16 Secret) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx64
    (va_op_dst_opr64_reg64 rRax) (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 24 Secret)) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rR14) (va_op_opr64_reg64 rR13))
    (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR14) 24 Secret) (va_pbool_and
    (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR8)) (va_ttrue
    ()))))))))))))))))))
val va_codegen_success_Fast_mul1 : va_dummy:unit -> Tot va_pbool
let va_codegen_success_Fast_mul1 () =
(va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR9)
            (va_op_dst_opr64_reg64 rR8)
            (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 0 Secret))
        (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet 0)
                (va_op_reg_opr64_reg64 rRdi)
                (va_op_reg_opr64_reg64 rR8)
                0
                Secret)
            (va_pbool_and (va_codegen_success_Xor64 (va_op_dst_opr64_reg64 rR8)
                    (va_op_opr64_reg64 rR8))
                (va_pbool_and (va_codegen_success_Mem64_lemma ())
                    (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR11)
                            (va_op_dst_opr64_reg64 rR10)
                            (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
                                (va_op_reg64_reg64 rRsi)
                                8
                                Secret))
                        (va_pbool_and (va_codegen_success_Add64Wrap (va_op_dst_opr64_reg64 rR10)
                                (va_op_opr64_reg64 rR9))
                            (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet
                                        0)
                                    (va_op_reg_opr64_reg64 rRdi)
                                    (va_op_reg_opr64_reg64 rR10)
                                    8
                                    Secret)
                                (va_pbool_and (va_codegen_success_Mem64_lemma ())
                                    (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64 rR13
                                              )
                                            (va_op_dst_opr64_reg64 rRbx)
                                            (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
                                                (va_op_reg64_reg64 rRsi)
                                                16
                                                Secret))
                                        (va_pbool_and (va_codegen_success_Adcx64Wrap (va_op_dst_opr64_reg64
                                                    rRbx)
                                                (va_op_opr64_reg64 rR11))
                                            (va_pbool_and (va_codegen_success_Store64_buffer (va_op_heaplet_mem_heaplet
                                                        0)
                                                    (va_op_reg_opr64_reg64 rRdi)
                                                    (va_op_reg_opr64_reg64 rRbx)
                                                    16
                                                    Secret)
                                                (va_pbool_and (va_codegen_success_Mem64_lemma ())
                                                    (va_pbool_and (va_codegen_success_Mulx64 (va_op_dst_opr64_reg64
                                                                rRax)
                                                            (va_op_dst_opr64_reg64 rR14)
                                                            (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet
                                                                    0)
                                                                (va_op_reg64_reg64 rRsi)
                                                                24
                                                                Secret))
                                                        (va_pbool_and (va_codegen_success_Adcx64Wrap
                                                                (va_op_dst_opr64_reg64 rR14)
                                                                (va_op_opr64_reg64 rR13))
                                                            (va_pbool_and (va_codegen_success_Store64_buffer
                                                                    (va_op_heaplet_mem_heaplet 0)
                                                                    (va_op_reg_opr64_reg64 rRdi)
                                                                    (va_op_reg_opr64_reg64 rR14)
                                                                    24
                                                                    Secret)
                                                                (va_pbool_and (va_codegen_success_Adcx64Wrap
                                                                        (va_op_dst_opr64_reg64 rRax)
                                                                        (va_op_opr64_reg64 rR8))
                                                                    (va_ttrue ()))))))))))))))))))
Vale.Curve25519.X64.FastUtil.fst.checked
Vale.X64.State.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.InsStack.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.FastUtil_helpers.fsti.checked Vale.Curve25519.Fast_lemmas_external.fsti.checked Vale.Curve25519.Fast_defs.fst.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Curve25519.X64.FastUtil.fst
Prims.unit Vale.X64.Decls.va_pbool_and Vale.X64.InsMem.va_codegen_success_Mem64_lemma Vale.X64.InsBasic.va_codegen_success_Mulx64 Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rR8 Vale.X64.Decls.va_opr_code_Mem64 Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_reg64_reg64 Vale.X64.Machine_s.rRsi Vale.Arch.HeapTypes_s.Secret Vale.X64.InsMem.va_codegen_success_Store64_buffer Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRdi Vale.X64.InsBasic.va_codegen_success_Xor64 Vale.X64.Decls.va_op_opr64_reg64 Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rR10 Vale.X64.InsBasic.va_codegen_success_Add64Wrap Vale.X64.Machine_s.rR13 Vale.X64.Machine_s.rRbx Vale.X64.InsBasic.va_codegen_success_Adcx64Wrap Vale.X64.Machine_s.rRax Vale.X64.Machine_s.rR14 Vale.X64.Decls.va_ttrue Vale.X64.Decls.va_pbool
module Vale.Curve25519.X64.FastUtil
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsStack
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open FStar.Tactics
open Vale.Curve25519.Fast_defs
open Vale.Curve25519.Fast_lemmas_external
open Vale.Curve25519.FastUtil_helpers
open Vale.X64.CPU_Features_s
#reset-options "--z3rlimit 60"
//-- Fast_mul1
#push-options "--z3rlimit 600"

val va_code_Fast_mul1 : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Fast_mul1 () =
  (va_Block (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64
    rR9) (va_op_dst_opr64_reg64 rR8) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRsi) 0 Secret)) (va_CCons (va_code_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR8) 0
    Secret) (va_CCons (va_code_Xor64 (va_op_dst_opr64_reg64 rR8) (va_op_opr64_reg64 rR8)) (va_CCons
    (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rR11)
    (va_op_dst_opr64_reg64 rR10) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRsi) 8 Secret)) (va_CCons (va_code_Add64Wrap (va_op_dst_opr64_reg64 rR10)
    (va_op_opr64_reg64 rR9)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR10) 8 Secret) (va_CCons
    (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rR13)
    (va_op_dst_opr64_reg64 rRbx) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRsi) 16 Secret)) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRbx)
    (va_op_opr64_reg64 rR11)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rRbx) 16 Secret) (va_CCons
    (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx64 (va_op_dst_opr64_reg64 rRax)
    (va_op_dst_opr64_reg64 rR14) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRsi) 24 Secret)) (va_CCons (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rR14)
    (va_op_opr64_reg64 rR13)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi) (va_op_reg_opr64_reg64 rR14) 24 Secret) (va_CCons
    (va_code_Adcx64Wrap (va_op_dst_opr64_reg64 rRax) (va_op_opr64_reg64 rR8)) (va_CNil
    ())))))))))))))))))))

val va_codegen_success_Fast_mul1 : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
val va_codegen_success_Fast_mul1 : va_dummy:unit -> Tot va_pbool
va_dummy: Prims.unit -> Vale.X64.Decls.va_pbool