val f51_felem_fits (h: mem) (f: felem M51) (m: Hacl.Spec.Curve25519.Field51.Definition.scale64_5)
    : Type0
let f51_felem_fits (h:mem) (f:felem M51) (m:Hacl.Spec.Curve25519.Field51.Definition.scale64_5): Type0 =
  Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 (f51_as_felem h f) m
val f51_felem_fits (h: mem) (f: felem M51) (m: Hacl.Spec.Curve25519.Field51.Definition.scale64_5)
    : Type0
let f51_felem_fits (h: mem) (f: felem M51) (m: Hacl.Spec.Curve25519.Field51.Definition.scale64_5)
    : Type0 =
Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 (f51_as_felem h f) m
Hacl.Impl.Curve25519.Fields.Core.fsti.checked
Spec.Curve25519.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.Field64.Definition.fst.checked Hacl.Spec.Curve25519.Field51.Definition.fst.checked Hacl.Spec.Curve25519.Field51.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.Curve25519.Fields.Core.fsti
FStar.Monotonic.HyperStack.mem Hacl.Impl.Curve25519.Fields.Core.felem Hacl.Impl.Curve25519.Fields.Core.M51 Hacl.Spec.Curve25519.Field51.Definition.scale64_5 Hacl.Spec.Curve25519.Field51.Definition.felem_fits5 Hacl.Impl.Curve25519.Fields.Core.f51_as_felem
module Hacl.Impl.Curve25519.Fields.Core

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

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

module P = Spec.Curve25519

/// This module defines the core functions for which we will want to swap out
/// implementations. They are marked as assume val's since we strictly have more
/// than one implementation per index value.

#set-options "--z3rlimit 50 --fuel 0 --ifuel 1 --record_options"

/// Shared definitions for agility of the field type
/// ------------------------------------------------

type field_spec =
  | M51
  | M64

unfold noextract
let limb (s:field_spec) =
  match s with
  | M51 -> uint64
  | M64 -> uint64

unfold noextract
let limb_zero (s:field_spec) : limb s=
  match s with
  | M51 -> u64 0
  | M64 -> u64 0

unfold noextract
let nlimb (s:field_spec) : size_t =
  match s with
  | M51 -> 5ul
  | M64 -> 4ul

unfold noextract
let wide (s:field_spec) =
  match s with
  | M51 -> uint128
  | M64 -> uint64

unfold noextract
let wide_zero (s:field_spec) : wide s=
  match s with
  | M51 -> u128 0
  | M64 -> u64 0

unfold noextract
let nwide (s:field_spec) : size_t =
  match s with
  | M51 -> 5ul
  | M64 -> 8ul

inline_for_extraction noextract
let felem (s:field_spec) = lbuffer (limb s) (nlimb s)
inline_for_extraction noextract
let felem2 (s:field_spec) = lbuffer (limb s) (nlimb s +. nlimb s)
inline_for_extraction noextract
let felem_wide (s:field_spec) = lbuffer (wide s) (nwide s)
inline_for_extraction noextract
let felem_wide2 (s:field_spec) = lbuffer (wide s) (nwide s +. nwide s)


/// Introduce representation for each field + helpers to be able to state pre & posts
/// ---------------------------------------------------------------------------------

noextract
let f51_as_felem (h:mem) (f:felem M51) : GTot Hacl.Spec.Curve25519.Field51.Definition.felem5 =
  let s = as_seq h f in
  let s0 = s.[0] in
  let s1 = s.[1] in
  let s2 = s.[2] in
  let s3 = s.[3] in
  let s4 = s.[4] in
  (s0, s1, s2, s3, s4)

let f51_as_nat h e = Hacl.Spec.Curve25519.Field51.Definition.as_nat5 (f51_as_felem h e)

noextract
val f51_felem_fits (h: mem) (f: felem M51) (m: Hacl.Spec.Curve25519.Field51.Definition.scale64_5)
    : Type0

    h: FStar.Monotonic.HyperStack.mem ->
    f: Hacl.Impl.Curve25519.Fields.Core.felem Hacl.Impl.Curve25519.Fields.Core.M51 ->
    m: Hacl.Spec.Curve25519.Field51.Definition.scale64_5
  -> Type0