val sha512_modq (len: nat{len <= max_input_length_sha512}) (s: bytes{length s = len})
    : n: nat{n < pow2 256}
let sha512_modq (len:nat{len <= max_input_length_sha512}) (s:bytes{length s = len}) : n:nat{n < pow2 256} =
  nat_from_bytes_le (Spec.Agile.Hash.hash Spec.Hash.Definitions.SHA2_512 s) % q
val sha512_modq (len: nat{len <= max_input_length_sha512}) (s: bytes{length s = len})
    : n: nat{n < pow2 256}
let sha512_modq (len: nat{len <= max_input_length_sha512}) (s: bytes{length s = len})
    : n: nat{n < pow2 256} =
nat_from_bytes_le (Spec.Agile.Hash.hash Spec.Hash.Definitions.SHA2_512 s) % q
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
Prims.nat Prims.b2t Prims.op_LessThanOrEqual Spec.Ed25519.max_input_length_sha512 Lib.ByteSequence.bytes Prims.op_Equality Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.op_Modulus Lib.ByteSequence.nat_from_bytes_le Spec.Agile.Hash.hash Spec.Hash.Definitions.SHA2_512 Spec.Ed25519.q Prims.op_LessThan Prims.pow2
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"

inline_for_extraction
let size_signature: size_nat = 64

let q: n:nat{n < pow2 256} =
  assert_norm(pow2 252 + 27742317777372353535851937790883648493 < pow2 255 - 19);
  (pow2 252 + 27742317777372353535851937790883648493) // Group order

let max_input_length_sha512 = Some?.v (Spec.Hash.Definitions.max_input_length Spec.Hash.Definitions.SHA2_512)
let _: squash(max_input_length_sha512 > pow2 32 + 64) =
  assert_norm (max_input_length_sha512 > pow2 32 + 64)
val sha512_modq (len: nat{len <= max_input_length_sha512}) (s: bytes{length s = len})
    : n: nat{n < pow2 256}

    len: Prims.nat{len <= Spec.Ed25519.max_input_length_sha512} ->
    s: Lib.ByteSequence.bytes{Lib.Sequence.length s = len}
  -> n: Prims.nat{n < Prims.pow2 256}