val va_req_Fast_add1 (va_b0: va_code) (va_s0: va_state) (dst_b inA_b: buffer64) (inB: nat64) : prop
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))
val va_req_Fast_add1 (va_b0: va_code) (va_s0: va_state) (dst_b inA_b: buffer64) (inB: nat64) : prop
let va_req_Fast_add1 (va_b0: va_code) (va_s0: va_state) (dst_b 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))
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 Prims.l_and Vale.X64.Decls.va_require_total Vale.Curve25519.X64.FastUtil.va_code_Fast_add1 Prims.b2t Vale.X64.Decls.va_get_ok Vale.X64.CPU_Features_s.adx_enabled Vale.X64.CPU_Features_s.bmi2_enabled Vale.X64.Memory.is_initial_heap Vale.X64.Decls.va_get_mem_layout Vale.X64.Decls.va_get_mem Prims.l_or Vale.X64.Decls.buffers_disjoint Prims.eq2 Vale.X64.Decls.validDstAddrs64 Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRdi Vale.Arch.HeapTypes_s.Secret Vale.X64.Decls.validSrcAddrs64 Vale.X64.Machine_s.rRsi Vale.Def.Words_s.nat64 Vale.X64.Machine_s.rRdx Prims.nat Vale.Curve25519.Fast_defs.pow2_four Vale.X64.Decls.buffer64_read 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)
val va_req_Fast_add1 (va_b0: va_code) (va_s0: va_state) (dst_b inA_b: buffer64) (inB: nat64) : 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
  -> Prims.prop