val sk1:b: lbuffer uint8 32ul {recallable b}
let sk1: b:lbuffer uint8 32ul{ recallable b } =
  let open Lib.RawIntTypes in
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 [
      0x9d; 0x61; 0xb1; 0x9d; 0xef; 0xfd; 0x5a; 0x60; 0xba; 0x84; 0x4a; 0xf4; 0x92; 0xec; 0x2c; 0xc4;
      0x44; 0x49; 0xc5; 0x69; 0x7b; 0x32; 0x69; 0x19; 0x70; 0x3b; 0xac; 0x03; 0x1c; 0xae; 0x7f; 0x60
    ]) in
  assert_norm (List.Tot.length l == 32);
  createL_mglobal l
val sk1:b: lbuffer uint8 32ul {recallable b}
let sk1:b: lbuffer uint8 32ul {recallable b} =
let open Lib.RawIntTypes in
[@@ inline_let ]let l:list uint8 =
  normalize_term (List.Tot.map u8
        [
          0x9d; 0x61; 0xb1; 0x9d; 0xef; 0xfd; 0x5a; 0x60; 0xba; 0x84; 0x4a; 0xf4; 0x92; 0xec; 0x2c;
          0xc4; 0x44; 0x49; 0xc5; 0x69; 0x7b; 0x32; 0x69; 0x19; 0x70; 0x3b; 0xac; 0x03; 0x1c; 0xae;
          0x7f; 0x60
        ])
in
assert_norm (List.Tot.length l == 32);
createL_mglobal l
Hacl.Test.Ed25519.fst.checked
prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.PrintBuffer.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Ed25519.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.All.fst.checked C.String.fsti.checked C.fst.checked
Hacl.Test.Ed25519.fst
Lib.Buffer.createL_mglobal Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.buffer Prims.unit FStar.Pervasives.assert_norm Prims.eq2 Prims.int FStar.List.Tot.Base.length Lib.Buffer.lbuffer_t Lib.Buffer.MUT FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.recallable Prims.list FStar.Pervasives.normalize_term FStar.List.Tot.Base.map Prims.nat Prims.b2t Prims.op_LessThan Hacl.Test.Ed25519.u8 Prims.Cons Prims.Nil
module Hacl.Test.Ed25519

open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.PrintBuffer

module Ed25519 = Hacl.Ed25519

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

inline_for_extraction noextract
val u8: n:nat{n < 0x100} -> uint8
let u8 n = u8 n

//
// Test1
//
let msg1: b:lbuffer uint8 0ul{ recallable b } =
  let open Lib.RawIntTypes in
  [@ inline_let]
  let l:list uint8 =
    normalize_term (List.Tot.map u8 []) in
  assert_norm (List.Tot.length l == 0);
  createL_mglobal l

let sk1: b:lbuffer uint8 32ul{ recallable b } =
val sk1:b: lbuffer uint8 32ul {recallable b}
b:
Lib.Buffer.lbuffer_t Lib.Buffer.MUT
  (Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC)
  (FStar.UInt32.uint_to_t 32 <: FStar.UInt32.t) {Lib.Buffer.recallable b}