val cswap_post:VSig.vale_post cswap_dom
let cswap_post : VSig.vale_post cswap_dom =
  fun (c:V.va_code)
    (bit:uint64)
    (p0:b64)
    (p1:b64)
    (va_s0:V.va_state)
    (va_s1:V.va_state)
    (f:V.va_fuel) ->
      FU.va_ens_Cswap2_stdcall c va_s0 IA.win (UInt64.v bit) (as_vale_buffer p0) (as_vale_buffer p1) va_s1 f
val cswap_post:VSig.vale_post cswap_dom
let cswap_post:VSig.vale_post cswap_dom =
fun
  (c: V.va_code)
  (bit: uint64)
  (p0: b64)
  (p1: b64)
  (va_s0: V.va_state)
  (va_s1: V.va_state)
  (f: V.va_fuel)
  ->
  FU.va_ens_Cswap2_stdcall c
    va_s0
    IA.win
    (UInt64.v bit)
    (as_vale_buffer p0)
    (as_vale_buffer p1)
    va_s1
    f
Vale.Stdcalls.X64.Fswap.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.X64.FastWide.fsti.checked Vale.Curve25519.X64.FastUtil.fsti.checked Vale.Curve25519.X64.FastHybrid.fsti.checked Vale.AsLowStar.Wrapper.fsti.checked Vale.AsLowStar.ValeSig.fst.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Vale.Stdcalls.X64.Fswap.fsti
Vale.X64.Decls.va_code Vale.Stdcalls.X64.Fswap.uint64 Vale.Stdcalls.X64.Fswap.b64 Vale.X64.Decls.va_state Vale.X64.Decls.va_fuel Vale.Curve25519.X64.FastUtil.va_ens_Cswap2_stdcall Vale.Interop.Assumptions.win FStar.UInt64.v Vale.X64.MemoryAdapters.as_vale_buffer Vale.Arch.HeapTypes_s.TUInt64 Prims.prop
module Vale.Stdcalls.X64.Fswap
open FStar.Mul

val z3rlimit_hack (x:nat) : squash (x < x + x + 1)
#reset-options "--z3rlimit 50"

open FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module DV = LowStar.BufferView.Down
open Vale.Def.Types_s

open Vale.Interop.Base
module IX64 = Vale.Interop.X64
module VSig = Vale.AsLowStar.ValeSig
module LSig = Vale.AsLowStar.LowStarSig
module ME = Vale.X64.Memory
module V = Vale.X64.Decls
module IA = Vale.Interop.Assumptions
module W = Vale.AsLowStar.Wrapper
open Vale.X64.MemoryAdapters
module VS = Vale.X64.State
module MS = Vale.X64.Machine_s
open Vale.AsLowStar.MemoryHelpers

module FU = Vale.Curve25519.X64.FastUtil
module FH = Vale.Curve25519.X64.FastHybrid
module FW = Vale.Curve25519.X64.FastWide

let uint64 = UInt64.t

(* A little utility to trigger normalization in types *)
noextract
let as_t (#a:Type) (x:normal a) : a = x
noextract
let as_normal_t (#a:Type) (x:a) : normal a = x

[@__reduce__] noextract
let b64 = buf_t TUInt64 TUInt64
[@__reduce__] noextract
let t64_mod = TD_Buffer TUInt64 TUInt64 default_bq
[@__reduce__] noextract
let t64_no_mod = TD_Buffer TUInt64 TUInt64 ({modified=false; strict_disjointness=false; taint=MS.Secret})
[@__reduce__] noextract
let tuint64 = TD_Base TUInt64

[@__reduce__] noextract
let cswap_dom: IX64.arity_ok_stdcall td =
  let y = [tuint64; t64_mod; t64_mod] in
  assert_norm (List.length y = 3);
  y

(* Need to rearrange the order of arguments *)
[@__reduce__] noextract
let cswap_pre : VSig.vale_pre cswap_dom =
  fun (c:V.va_code)
    (bit:uint64)
    (p0:b64)
    (p1:b64)
    (va_s0:V.va_state) ->
      FU.va_req_Cswap2_stdcall c va_s0 IA.win
        (UInt64.v bit) (as_vale_buffer p0) (as_vale_buffer p1)

[@__reduce__] noextract
val cswap_post:VSig.vale_post cswap_dom
Vale.AsLowStar.ValeSig.vale_post Vale.Stdcalls.X64.Fswap.cswap_dom