let scalar = lbuffer uint8 32ul
let scalar =
lbuffer uint8 32ul
Hacl.Impl.Curve25519.Generic.fst.checked
Spec.Curve25519.fst.checked prims.fst.checked Meta.Attribute.fst.checked LowStar.Monotonic.Buffer.fsti.checked Lib.Sequence.fsti.checked Lib.Loops.fsti.checked Lib.LoopCombinators.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Curve25519.Field64.Lemmas.fst.checked Hacl.Spec.Curve25519.AddAndDouble.fst.checked Hacl.Impl.Curve25519.Finv.fst.checked Hacl.Impl.Curve25519.Fields.Core.fsti.checked Hacl.Impl.Curve25519.Fields.fst.checked Hacl.Impl.Curve25519.AddAndDouble.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Curve25519.Generic.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t
module Hacl.Impl.Curve25519.Generic

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

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer

open Hacl.Impl.Curve25519.Fields

include Hacl.Impl.Curve25519.Finv
include Hacl.Impl.Curve25519.AddAndDouble

module ST = FStar.HyperStack.ST
module BSeq = Lib.ByteSequence
module LSeq = Lib.Sequence

module C = Hacl.Impl.Curve25519.Fields.Core

module S = Spec.Curve25519
module M = Hacl.Spec.Curve25519.AddAndDouble
module Lemmas = Hacl.Spec.Curve25519.Field64.Lemmas

friend Lib.LoopCombinators

#reset-options "--z3rlimit 200 --max_fuel 2 --using_facts_from '* -FStar.Seq -Hacl.Spec.*' --record_options"
//#set-options "--debug Hacl.Impl.Curve25519.Generic --debug_level ExtractNorm"
val scalar : Type0
Type0