val add_scalar: add1_t p
let add_scalar out f1 f2 =
  if EverCrypt.TargetConfig.hacl_can_compile_inline_asm then
    Vale.Inline.X64.Fadd_inline.add_scalar out f1 f2
  else
    Vale.Wrapper.X64.Fadd.add_scalar_e out f1 f2
val add_scalar: add1_t p
let add_scalar out f1 f2 =
if EverCrypt.TargetConfig.hacl_can_compile_inline_asm
then Vale.Inline.X64.Fadd_inline.add_scalar out f1 f2
else Vale.Wrapper.X64.Fadd.add_scalar_e out f1 f2
Hacl.Impl.Curve25519.Field64.Vale.fst.checked
Vale.Wrapper.X64.Fswap.fsti.checked Vale.Wrapper.X64.Fsub.fsti.checked Vale.Wrapper.X64.Fsqr.fsti.checked Vale.Wrapper.X64.Fmul.fsti.checked Vale.Wrapper.X64.Fadd.fsti.checked Vale.Inline.X64.Fswap_inline.fsti.checked Vale.Inline.X64.Fsqr_inline.fsti.checked Vale.Inline.X64.Fmul_inline.fsti.checked Vale.Inline.X64.Fadd_inline.fsti.checked Vale.Curve25519.Fast_defs.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fst.checked Lib.Buffer.fst.checked Hacl.Spec.Curve25519.Field64.Definition.fst.checked Hacl.Impl.Curve25519.Field64.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked EverCrypt.TargetConfig.fsti.checked
Hacl.Impl.Curve25519.Field64.Vale.fst
Hacl.Impl.Curve25519.Fields.Core.felem Hacl.Impl.Curve25519.Fields.Core.M64 Lib.IntTypes.uint64 EverCrypt.TargetConfig.hacl_can_compile_inline_asm Vale.Inline.X64.Fadd_inline.add_scalar FStar.Ghost.erased FStar.UInt64.t Prims.bool Vale.Wrapper.X64.Fadd.add_scalar_e
module Hacl.Impl.Curve25519.Field64.Vale

module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
open FStar.Calc

friend Lib.Buffer
friend Lib.IntTypes

open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.Sequence
open Lib.IntTypes
open Lib.Buffer

module B = Lib.Buffer
module S = Hacl.Spec.Curve25519.Field64.Definition
module P = Spec.Curve25519

module FA = Vale.Wrapper.X64.Fadd

module F64 = Hacl.Impl.Curve25519.Field64

/// We are trying to connect HACL* abstractions with regular F* libraries, so in
/// addition to ``friend``'ing ``Lib.*``, we also write a couple lemmas that we
/// prove via normalization to facilitate the job of proving that calling the
/// Vale interop signatures faithfully implements the required HACL* signature.

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 300 --z3refresh"

let buffer_is_buffer a len: Lemma
  (ensures (lbuffer a len == b:B.buffer a{B.length b == UInt32.v len}))
  [ SMTPat (lbuffer a len) ]
=
  assert_norm (lbuffer a len == b:B.buffer a{B.length b == UInt32.v len})

let as_nat_is_as_nat (b:lbuffer uint64 4ul) (h:HS.mem): Lemma
  (ensures (FA.as_nat b h == F64.as_nat h b))
  [ SMTPat (as_nat h b) ]
=
  ()

let _: squash (Vale.Curve25519.Fast_defs.prime = Spec.Curve25519.prime) =
  assert_norm (Vale.Curve25519.Fast_defs.prime = Spec.Curve25519.prime)

// This one only goes through in a reasonable amount of rlimit thanks to
// ``as_nat_is_as_nat`` and ``buffer_is_buffer`` above.
[@ CInline]
val add_scalar: add1_t p
Hacl.Impl.Curve25519.Fields.Core.add1_t Hacl.Impl.Curve25519.Field64.Vale.p