val buffer_is_buffer (a len: _)
    : Lemma (ensures (lbuffer a len == b: B.buffer a {B.length b == UInt32.v len}))
      [SMTPat (lbuffer a len)]
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})
val buffer_is_buffer (a len: _)
    : Lemma (ensures (lbuffer a len == b: B.buffer a {B.length b == UInt32.v len}))
      [SMTPat (lbuffer a len)]
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})
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
FStar.UInt32.t FStar.Pervasives.assert_norm Prims.eq2 Lib.Buffer.lbuffer Lib.Buffer.buffer Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n Lib.Buffer.length Lib.Buffer.MUT FStar.UInt32.v Prims.unit Prims.l_True Prims.squash Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
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) ]
val buffer_is_buffer (a len: _)
    : Lemma (ensures (lbuffer a len == b: B.buffer a {B.length b == UInt32.v len}))
      [SMTPat (lbuffer a len)]
a: Type0 -> len: FStar.UInt32.t
  -> FStar.Pervasives.Lemma
      (ensures
        Lib.Buffer.lbuffer a len ==
        b:
        Lib.Buffer.buffer a {Lib.Buffer.length b == FStar.UInt32.v len})
      [SMTPat (Lib.Buffer.lbuffer a len)]