val va_ens_Fast_add1
      (va_b0: va_code)
      (va_s0: va_state)
      (dst_b inA_b: buffer64)
      (inB: nat64)
      (va_sM: va_state)
      (va_fM: va_fuel)
    : prop
let va_ens_Fast_add1 (va_b0:va_code) (va_s0:va_state) (dst_b:buffer64) (inA_b:buffer64) (inB:nat64)
  (va_sM:va_state) (va_fM:va_fuel) : prop =
  (va_req_Fast_add1 va_b0 va_s0 dst_b inA_b inB /\ va_ensure_total va_b0 va_s0 va_sM va_fM /\
    va_get_ok va_sM /\ (let (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0
    (va_get_mem va_s0) in let (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1
    (va_get_mem va_s0) in let (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2
    (va_get_mem va_s0) in let (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3
    (va_get_mem va_s0) in let (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in
    let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem va_sM) in let d1 =
    Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem va_sM) in let d2 =
    Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem va_sM) in let d3 =
    Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem va_sM) in let d =
    Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3 (va_get_reg64 rRax va_sM) in d == a +
    va_get_reg64 rRdx va_s0 /\ Vale.X64.Decls.modifies_buffer dst_b (va_get_mem va_s0) (va_get_mem
    va_sM)) /\ va_state_eq va_sM (va_update_flags va_sM (va_update_mem_layout va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_reg64 rR11 va_sM (va_update_reg64 rR10 va_sM
    (va_update_reg64 rR9 va_sM (va_update_reg64 rR8 va_sM (va_update_reg64 rRdx va_sM
    (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem va_sM va_s0))))))))))))
val va_ens_Fast_add1
      (va_b0: va_code)
      (va_s0: va_state)
      (dst_b inA_b: buffer64)
      (inB: nat64)
      (va_sM: va_state)
      (va_fM: va_fuel)
    : prop
let va_ens_Fast_add1
      (va_b0: va_code)
      (va_s0: va_state)
      (dst_b inA_b: buffer64)
      (inB: nat64)
      (va_sM: va_state)
      (va_fM: va_fuel)
    : prop =
(va_req_Fast_add1 va_b0 va_s0 dst_b inA_b inB /\ va_ensure_total va_b0 va_s0 va_sM va_fM /\
  va_get_ok va_sM /\
  (let a0:Vale.Def.Types_s.nat64 = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem va_s0) in
    let a1:Vale.Def.Types_s.nat64 = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem va_s0) in
    let a2:Vale.Def.Types_s.nat64 = Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem va_s0) in
    let a3:Vale.Def.Types_s.nat64 = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem va_s0) in
    let a:Prims.nat = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in
    let d0 = Vale.X64.Decls.buffer64_read dst_b 0 (va_get_mem va_sM) in
    let d1 = Vale.X64.Decls.buffer64_read dst_b 1 (va_get_mem va_sM) in
    let d2 = Vale.X64.Decls.buffer64_read dst_b 2 (va_get_mem va_sM) in
    let d3 = Vale.X64.Decls.buffer64_read dst_b 3 (va_get_mem va_sM) in
    let d = Vale.Curve25519.Fast_defs.pow2_five d0 d1 d2 d3 (va_get_reg64 rRax va_sM) in
    d == a + va_get_reg64 rRdx va_s0 /\
    Vale.X64.Decls.modifies_buffer dst_b (va_get_mem va_s0) (va_get_mem va_sM)) /\
  va_state_eq va_sM
    (va_update_flags va_sM
        (va_update_mem_layout va_sM
            (va_update_mem_heaplet 0
                va_sM
                (va_update_reg64 rR11
                    va_sM
                    (va_update_reg64 rR10
                        va_sM
                        (va_update_reg64 rR9
                            va_sM
                            (va_update_reg64 rR8
                                va_sM
                                (va_update_reg64 rRdx
                                    va_sM
                                    (va_update_reg64 rRax
                                        va_sM
                                        (va_update_ok va_sM (va_update_mem va_sM va_s0))))))))))))
Vale.Curve25519.X64.FastUtil.fsti.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.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.Fast_defs.fst.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Curve25519.X64.FastUtil.fsti
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Vale.X64.Memory.buffer64 Vale.X64.Memory.nat64 Vale.X64.Decls.va_fuel Prims.l_and Vale.Curve25519.X64.FastUtil.va_req_Fast_add1 Vale.X64.Decls.va_ensure_total Prims.b2t Vale.X64.Decls.va_get_ok Prims.eq2 Prims.int Prims.op_Addition Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRdx Vale.X64.Decls.modifies_buffer Vale.X64.Decls.va_get_mem Prims.nat Vale.Curve25519.Fast_defs.pow2_five Vale.X64.Machine_s.rRax Vale.Def.Words_s.nat64 Vale.X64.Decls.buffer64_read Vale.Curve25519.Fast_defs.pow2_four Vale.X64.Decls.va_state_eq Vale.X64.Decls.va_update_flags Vale.X64.Decls.va_update_mem_layout Vale.X64.Decls.va_update_mem_heaplet Vale.X64.Decls.va_update_reg64 Vale.X64.Machine_s.rR11 Vale.X64.Machine_s.rR10 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rR8 Vale.X64.Decls.va_update_ok Vale.X64.Decls.va_update_mem Prims.prop
module Vale.Curve25519.X64.FastUtil
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.HeapImpl
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.QuickCode
open Vale.X64.QuickCodes
open Vale.Curve25519.Fast_defs
open Vale.X64.CPU_Features_s
//-- Fast_add1

val va_code_Fast_add1 : va_dummy:unit -> Tot va_code

val va_codegen_success_Fast_add1 : va_dummy:unit -> Tot va_pbool
let va_req_Fast_add1 (va_b0:va_code) (va_s0:va_state) (dst_b:buffer64) (inA_b:buffer64) (inB:nat64)
  : prop =
  (va_require_total va_b0 (va_code_Fast_add1 ()) va_s0 /\ va_get_ok va_s0 /\ (let
    (a0:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 0 (va_get_mem va_s0) in let
    (a1:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 1 (va_get_mem va_s0) in let
    (a2:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 2 (va_get_mem va_s0) in let
    (a3:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read inA_b 3 (va_get_mem va_s0) in let
    (a:Prims.nat) = Vale.Curve25519.Fast_defs.pow2_four a0 a1 a2 a3 in adx_enabled /\ bmi2_enabled
    /\ Vale.X64.Memory.is_initial_heap (va_get_mem_layout va_s0) (va_get_mem va_s0) /\
    (Vale.X64.Decls.buffers_disjoint dst_b inA_b \/ inA_b == dst_b) /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem va_s0) (va_get_reg64 rRdi va_s0) dst_b 4
    (va_get_mem_layout va_s0) Secret /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem va_s0)
    (va_get_reg64 rRsi va_s0) inA_b 4 (va_get_mem_layout va_s0) Secret /\ inB == va_get_reg64 rRdx
    va_s0))
let va_ens_Fast_add1 (va_b0:va_code) (va_s0:va_state) (dst_b:buffer64) (inA_b:buffer64) (inB:nat64)
val va_ens_Fast_add1
      (va_b0: va_code)
      (va_s0: va_state)
      (dst_b inA_b: buffer64)
      (inB: nat64)
      (va_sM: va_state)
      (va_fM: va_fuel)
    : prop

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    dst_b: Vale.X64.Memory.buffer64 ->
    inA_b: Vale.X64.Memory.buffer64 ->
    inB: Vale.X64.Memory.nat64 ->
    va_sM: Vale.X64.Decls.va_state ->
    va_fM: Vale.X64.Decls.va_fuel
  -> Prims.prop