val secret_expand: expanded:lbuffer uint8 64ul -> secret:lbuffer uint8 32ul -> Stack unit
  (requires fun h -> live h expanded /\ live h secret /\ disjoint expanded secret)
  (ensures  fun h0 _ h1 -> modifies (loc expanded) h0 h1 /\
   (let a, prefix = S.secret_expand (as_seq h0 secret) in
    as_seq h1 (gsub expanded 0ul 32ul) == a /\
    as_seq h1 (gsub expanded 32ul 32ul) == prefix))
let secret_expand expanded secret =
  assert_norm (pow2 32 <= pow2 125 - 1);
  Hacl.Streaming.SHA2.hash_512 secret 32ul expanded;
  let h_low  = sub expanded 0ul 32ul in
  let h_low0  = h_low.( 0ul) in
  let h_low31 = h_low.(31ul) in
  h_low.( 0ul) <- h_low0 &. u8 0xf8;
  h_low.(31ul) <- (h_low31 &. u8 127) |. u8 64
val secret_expand: expanded:lbuffer uint8 64ul -> secret:lbuffer uint8 32ul -> Stack unit
  (requires fun h -> live h expanded /\ live h secret /\ disjoint expanded secret)
  (ensures  fun h0 _ h1 -> modifies (loc expanded) h0 h1 /\
   (let a, prefix = S.secret_expand (as_seq h0 secret) in
    as_seq h1 (gsub expanded 0ul 32ul) == a /\
    as_seq h1 (gsub expanded 32ul 32ul) == prefix))
let secret_expand expanded secret =
assert_norm (pow2 32 <= pow2 125 - 1);
Hacl.Streaming.SHA2.hash_512 secret 32ul expanded;
let h_low = sub expanded 0ul 32ul in
let h_low0 = h_low.(0ul) in
let h_low31 = h_low.(31ul) in
h_low.(0ul) <- h_low0 &. u8 0xf8;
h_low.(31ul) <- (h_low31 &. u8 127) |. u8 64
Hacl.Ed25519.fst.checked
Spec.Ed25519.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Streaming.SHA2.fst.checked Hacl.Impl.Ed25519.Verify.fst.checked Hacl.Impl.Ed25519.Sign.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked
Hacl.Ed25519.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.Buffer.op_Array_Assignment Lib.IntTypes.op_Bar_Dot Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.op_Amp_Dot Lib.IntTypes.u8 Prims.unit Lib.IntTypes.int_t Lib.Buffer.op_Array_Access Lib.Buffer.MUT Lib.Buffer.lbuffer_t FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub Hacl.Streaming.SHA2.hash_512 FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThanOrEqual Prims.pow2 Prims.op_Subtraction
module Hacl.Ed25519

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

open Lib.IntTypes
open Lib.Buffer

module S = Spec.Ed25519

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

val secret_expand: expanded:lbuffer uint8 64ul -> secret:lbuffer uint8 32ul -> Stack unit
  (requires fun h -> live h expanded /\ live h secret /\ disjoint expanded secret)
  (ensures  fun h0 _ h1 -> modifies (loc expanded) h0 h1 /\
   (let a, prefix = S.secret_expand (as_seq h0 secret) in
    as_seq h1 (gsub expanded 0ul 32ul) == a /\
    as_seq h1 (gsub expanded 32ul 32ul) == prefix))

[@CInline]
val secret_expand: expanded:lbuffer uint8 64ul -> secret:lbuffer uint8 32ul -> Stack unit
  (requires fun h -> live h expanded /\ live h secret /\ disjoint expanded secret)
  (ensures  fun h0 _ h1 -> modifies (loc expanded) h0 h1 /\
   (let a, prefix = S.secret_expand (as_seq h0 secret) in
    as_seq h1 (gsub expanded 0ul 32ul) == a /\
    as_seq h1 (gsub expanded 32ul 32ul) == prefix))

    expanded: Lib.Buffer.lbuffer Lib.IntTypes.uint8 64ul ->
    secret: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul
  -> FStar.HyperStack.ST.Stack Prims.unit