let a_spec = S.aff_point_c
let a_spec =
S.aff_point_c
Hacl.Impl.Ed25519.Group.fst.checked
Spec.Ed25519.Lemmas.fsti.checked Spec.Ed25519.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Exponentiation.Definitions.fst.checked Hacl.Impl.Ed25519.PointDouble.fst.checked Hacl.Impl.Ed25519.PointConstants.fst.checked Hacl.Impl.Ed25519.PointAdd.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked Hacl.Bignum25519.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked
Hacl.Impl.Ed25519.Group.fst
Spec.Ed25519.aff_point_c
module Hacl.Impl.Ed25519.Group

module ST = FStar.HyperStack.ST
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum25519
open Hacl.Impl.Ed25519.PointConstants

module LSeq = Lib.Sequence
module F51 = Hacl.Impl.Ed25519.Field51
module BE = Hacl.Impl.Exponentiation.Definitions
module S = Spec.Ed25519

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val a_spec : Type0
Type0