val size_signature:size_nat
let size_signature: size_nat = 64
val size_signature:size_nat
let size_signature:size_nat =
64
Spec.Ed25519.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Exponentiation.fsti.checked Spec.Ed25519.PointOps.fst.checked Spec.Ed25519.Lemmas.fsti.checked Spec.Curve25519.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Ed25519.fst
module Spec.Ed25519

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Curve25519

module LE = Lib.Exponentiation
module SE = Spec.Exponentiation
module EL = Spec.Ed25519.Lemmas

include Spec.Ed25519.PointOps

#reset-options "--fuel 0 --ifuel 0 --z3rlimit 100"
val size_signature:size_nat
n: Prims.nat{n <= Prims.pow2 32 - 1}