let felem_wide (s:field_spec) = lbuffer (wide s) (nwide s)
let felem_wide (s: field_spec) =
lbuffer (wide s) (nwide s)
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
Hacl.Impl.Curve25519.Fields.Core.field_spec Lib.Buffer.lbuffer Hacl.Impl.Curve25519.Fields.Core.wide Hacl.Impl.Curve25519.Fields.Core.nwide
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)
val felem_wide : s: Hacl.Impl.Curve25519.Fields.Core.field_spec -> Type0
s: Hacl.Impl.Curve25519.Fields.Core.field_spec -> Type0